diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java index c2d2056a5..bb9daecfe 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java @@ -3,6 +3,7 @@ import it.unive.lisa.analysis.heap.HeapDomain; import it.unive.lisa.analysis.heap.HeapSemanticOperation.HeapReplacement; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.type.TypeDomain; import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.program.cfg.ProgramPoint; @@ -668,5 +669,45 @@ public String toString() { TYPE_REPRESENTATION_KEY, t, VALUE_REPRESENTATION_KEY, v)).toString(); } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return heap.alias(x, y, pp, oracle); + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return heap.isReachableFrom(x, y, pp, oracle); + } + } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return heapState.alias(x, y, pp, oracle); + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return heapState.isReachableFrom(x, y, pp, oracle); } } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/combination/CartesianProduct.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/combination/CartesianProduct.java index 02a0e8b15..a1c350593 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/combination/CartesianProduct.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/combination/CartesianProduct.java @@ -5,6 +5,7 @@ import it.unive.lisa.analysis.SemanticDomain; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.Environment; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/combination/NonRelationalValueCartesianProduct.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/combination/NonRelationalValueCartesianProduct.java index 029f2af36..19fbb78e5 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/combination/NonRelationalValueCartesianProduct.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/combination/NonRelationalValueCartesianProduct.java @@ -1,8 +1,8 @@ package it.unive.lisa.analysis.combination; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.analysis.nonrelational.value.NonRelationalValueDomain; import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/MonolithicHeap.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/MonolithicHeap.java index cbbcae396..d18c636ef 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/MonolithicHeap.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/MonolithicHeap.java @@ -4,6 +4,7 @@ import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.heap.AccessChild; @@ -245,4 +246,24 @@ public boolean knowsIdentifier( Identifier id) { return false; } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java index d2dca33c0..d9282a1a5 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java @@ -3,6 +3,7 @@ import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.heap.AccessChild; @@ -25,6 +26,7 @@ import java.util.List; import java.util.Set; import java.util.function.Predicate; +import org.apache.commons.collections4.CollectionUtils; import org.apache.commons.collections4.SetUtils; /** @@ -336,4 +338,39 @@ public boolean knowsIdentifier( Identifier id) { return false; } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + if (isTop()) + return Satisfiability.UNKNOWN; + if (isBottom()) + return Satisfiability.BOTTOM; + + Set ltypes = new HashSet<>(); + for (SymbolicExpression e : rewrite(x, pp, oracle)) + ltypes.addAll(oracle.getRuntimeTypesOf(e, pp, oracle)); + Set rtypes = new HashSet<>(); + for (SymbolicExpression e : rewrite(y, pp, oracle)) + rtypes.addAll(oracle.getRuntimeTypesOf(e, pp, oracle)); + if (CollectionUtils.intersection(ltypes, rtypes).isEmpty()) + // no common types -> they cannot be "smashed" to the same location + return Satisfiability.NOT_SATISFIED; + + return Satisfiability.UNKNOWN; + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java index 83add123a..aa7c44fab 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java @@ -5,6 +5,7 @@ import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.heap.BaseHeapDomain; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment; import it.unive.lisa.program.annotations.Annotation; import it.unive.lisa.program.cfg.CodeLocation; @@ -22,6 +23,8 @@ import it.unive.lisa.symbolic.value.Variable; import it.unive.lisa.type.ReferenceType; import it.unive.lisa.type.Type; +import it.unive.lisa.util.collections.workset.VisitOnceFIFOWorkingSet; +import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.representation.StructuredRepresentation; import java.util.Collections; import java.util.HashSet; @@ -512,4 +515,74 @@ public boolean knowsIdentifier( return heapEnv.knowsIdentifier(id) || (id instanceof AllocationSite && heapEnv.getValues().stream().anyMatch(as -> as.contains((AllocationSite) id))); } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + if (isTop()) + return Satisfiability.UNKNOWN; + if (isBottom()) + return Satisfiability.BOTTOM; + + boolean atLeastOne = false; + boolean all = true; + + ExpressionSet xrs = rewrite(x, pp, oracle); + ExpressionSet yrs = rewrite(y, pp, oracle); + + for (SymbolicExpression xr : xrs) + for (SymbolicExpression yr : yrs) + if (xr instanceof MemoryPointer && yr instanceof MemoryPointer) { + HeapLocation xloc = ((MemoryPointer) xr).getReferencedLocation(); + HeapLocation yloc = ((MemoryPointer) yr).getReferencedLocation(); + if (xloc.equals(yloc)) { + atLeastOne = true; + all &= true; + } else + all = false; + } else + // they cannot be alias + all = false; + + if (all && atLeastOne) + return Satisfiability.SATISFIED; + else if (atLeastOne) + return Satisfiability.UNKNOWN; + else + return Satisfiability.NOT_SATISFIED; + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + if (isTop()) + return Satisfiability.UNKNOWN; + if (isBottom()) + return Satisfiability.BOTTOM; + + WorkingSet ws = VisitOnceFIFOWorkingSet.mk(); + rewrite(x, pp, oracle).elements().forEach(ws::push); + ExpressionSet targets = rewrite(y, pp, oracle); + + while (!ws.isEmpty()) { + SymbolicExpression current = ws.peek(); + if (targets.elements().contains(current)) + return Satisfiability.SATISFIED; + + if (current instanceof Identifier && heapEnv.knowsIdentifier((Identifier) current)) + heapEnv.getState((Identifier) current).elements().forEach(ws::push); + else + rewrite(current, pp, oracle).elements().forEach(ws::push); + } + + return Satisfiability.NOT_SATISFIED; + } } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSites.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSites.java index 29e4745ec..860ffca2c 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSites.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSites.java @@ -1,9 +1,9 @@ package it.unive.lisa.analysis.heap.pointbased; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.lattices.SetLattice; import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment; import it.unive.lisa.analysis.nonrelational.heap.NonRelationalHeapDomain; @@ -188,4 +188,26 @@ public AllocationSites unknownVariable( // possible information (top) return bottom(); } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + HeapEnvironment environment, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + HeapEnvironment environment, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/nonRedundantSet/NonRedundantPowerset.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/nonRedundantSet/NonRedundantPowerset.java index 06db495de..70ae4f6e3 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/nonRedundantSet/NonRedundantPowerset.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/nonRedundantSet/NonRedundantPowerset.java @@ -5,6 +5,7 @@ import it.unive.lisa.analysis.SemanticDomain; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.lattices.SetLattice; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/nonRedundantSet/NonRedundantPowersetOfBaseNonRelationalValueDomain.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/nonRedundantSet/NonRedundantPowersetOfBaseNonRelationalValueDomain.java index d584fc340..f2ea3eb70 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/nonRedundantSet/NonRedundantPowersetOfBaseNonRelationalValueDomain.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/nonRedundantSet/NonRedundantPowersetOfBaseNonRelationalValueDomain.java @@ -2,9 +2,9 @@ import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.analysis.nonrelational.value.NonRelationalValueDomain; import it.unive.lisa.program.cfg.ProgramPoint; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/IntegerConstantPropagation.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/IntegerConstantPropagation.java index 034d2dbcf..4daabecb7 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/IntegerConstantPropagation.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/IntegerConstantPropagation.java @@ -2,9 +2,9 @@ import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; import it.unive.lisa.program.cfg.ProgramPoint; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Interval.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Interval.java index 30f58e0c1..2c4502f93 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Interval.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Interval.java @@ -2,9 +2,9 @@ import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; import it.unive.lisa.program.cfg.ProgramPoint; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Sign.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Sign.java index 88316b457..cc0eef8b7 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Sign.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/numeric/Sign.java @@ -2,9 +2,9 @@ import it.unive.lisa.analysis.BaseLattice; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; import it.unive.lisa.program.cfg.ProgramPoint; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/CharInclusion.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/CharInclusion.java index 016d16cf8..1b4ded9d8 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/CharInclusion.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/CharInclusion.java @@ -1,9 +1,9 @@ package it.unive.lisa.analysis.string; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.value.Constant; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/ContainsCharProvider.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/ContainsCharProvider.java index dda34a0bd..50dc5bc2b 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/ContainsCharProvider.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/ContainsCharProvider.java @@ -1,7 +1,7 @@ package it.unive.lisa.analysis.string; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.lattices.Satisfiability; /** * Interface for a string analysis that exposes the {@link #containsChar(char)} diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/Prefix.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/Prefix.java index 42cdcf30f..afb53c859 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/Prefix.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/Prefix.java @@ -1,9 +1,9 @@ package it.unive.lisa.analysis.string; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.value.Constant; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/Suffix.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/Suffix.java index c721352f5..96acbd10e 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/Suffix.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/Suffix.java @@ -1,9 +1,9 @@ package it.unive.lisa.analysis.string; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.value.Constant; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/bricks/Bricks.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/bricks/Bricks.java index a21ce5c24..b983e3a23 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/bricks/Bricks.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/bricks/Bricks.java @@ -1,10 +1,9 @@ package it.unive.lisa.analysis.string.bricks; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.analysis.string.ContainsCharProvider; import it.unive.lisa.program.cfg.ProgramPoint; @@ -215,7 +214,7 @@ public Satisfiability satisfiesBinaryExpression( SemanticOracle oracle) throws SemanticException { if (left.isTop() || right.isBottom()) - return SemanticDomain.Satisfiability.UNKNOWN; + return Satisfiability.UNKNOWN; if (operator == StringContains.INSTANCE) return left.contains(right); diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/FSA.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/FSA.java index 3d27f767d..650d1aeb4 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/FSA.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/fsa/FSA.java @@ -1,9 +1,9 @@ package it.unive.lisa.analysis.string.fsa; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.analysis.numeric.Interval; import it.unive.lisa.analysis.string.ContainsCharProvider; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/tarsis/Tarsis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/tarsis/Tarsis.java index 2bd328d63..61290ee19 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/tarsis/Tarsis.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/tarsis/Tarsis.java @@ -1,10 +1,9 @@ package it.unive.lisa.analysis.string.tarsis; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.analysis.numeric.Interval; import it.unive.lisa.analysis.string.ContainsCharProvider; @@ -229,7 +228,7 @@ public Satisfiability satisfiesBinaryExpression( throws SemanticException { if (operator == StringContains.INSTANCE) return left.contains(right); - return SemanticDomain.Satisfiability.UNKNOWN; + return Satisfiability.UNKNOWN; } /** diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/taint/BaseTaint.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/taint/BaseTaint.java index a0c1cd52b..d6b7f3353 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/taint/BaseTaint.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/taint/BaseTaint.java @@ -1,8 +1,8 @@ package it.unive.lisa.analysis.taint; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain; import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; import it.unive.lisa.program.annotations.Annotation; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java index 913f5332b..82d7eb6d0 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java @@ -8,6 +8,7 @@ import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.lattices.ExpressionSet; import it.unive.lisa.analysis.lattices.FunctionalLattice; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.program.cfg.controlFlow.ControlFlowStructure; import it.unive.lisa.program.cfg.controlFlow.IfThenElse; @@ -464,4 +465,50 @@ public TracePartitioning withTopTypes() { result.put(trace.getKey(), trace.getValue().withTopTypes()); return new TracePartitioning<>(lattice, result); } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + if (isTop()) + return Satisfiability.UNKNOWN; + + if (isBottom() || function == null) + return Satisfiability.BOTTOM; + + Satisfiability result = Satisfiability.BOTTOM; + for (Entry trace : this) { + Satisfiability sat = trace.getValue().alias(x, y, pp, oracle); + if (sat == Satisfiability.BOTTOM) + return sat; + result = result.lub(sat); + } + return result; + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + if (isTop()) + return Satisfiability.UNKNOWN; + + if (isBottom() || function == null) + return Satisfiability.BOTTOM; + + Satisfiability result = Satisfiability.BOTTOM; + for (Entry trace : this) { + Satisfiability sat = trace.getValue().isReachableFrom(x, y, pp, oracle); + if (sat == Satisfiability.BOTTOM) + return sat; + result = result.lub(sat); + } + return result; + } } diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/types/InferredTypes.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/types/InferredTypes.java index 5fc83b6b1..fed8f168c 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/types/InferredTypes.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/types/InferredTypes.java @@ -3,9 +3,9 @@ import static org.apache.commons.collections4.CollectionUtils.intersection; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.inference.InferredValue; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalTypeDomain; import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment; diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/types/StaticTypes.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/types/StaticTypes.java index 99262c5fc..c2f1322c0 100644 --- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/types/StaticTypes.java +++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/types/StaticTypes.java @@ -1,9 +1,9 @@ package it.unive.lisa.analysis.types; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.inference.InferredValue; import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalTypeDomain; import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment; diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/TestParameterProvider.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/TestParameterProvider.java index 4ca5bfab2..9058aba21 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/TestParameterProvider.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/TestParameterProvider.java @@ -192,7 +192,7 @@ public static class FakePP implements ProgramPoint { @Override public CodeLocation getLocation() { - return null; + return SyntheticLocation.INSTANCE; } @Override diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java index a52c8d73c..30fe7b279 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java @@ -4,6 +4,7 @@ import static org.junit.Assert.assertFalse; import static org.junit.Assert.assertTrue; +import it.unive.lisa.TestParameterProvider; import it.unive.lisa.analysis.ScopeToken; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; @@ -16,7 +17,6 @@ import it.unive.lisa.program.cfg.CodeLocation; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.program.type.Int32Type; -import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.heap.AccessChild; import it.unive.lisa.symbolic.heap.HeapDereference; import it.unive.lisa.symbolic.heap.HeapExpression; @@ -33,7 +33,6 @@ import it.unive.lisa.type.Untyped; import java.util.Collections; import java.util.HashSet; -import java.util.Set; import org.junit.Test; public class PointBasedHeapTest { @@ -72,53 +71,10 @@ public CFG getCFG() { } }; - private final CodeLocation fakeLocation = new SourceCodeLocation("fake", 0, 0); + private final SemanticOracle fakeOracle = TestParameterProvider.provideParam(null, SemanticOracle.class); - private final ProgramPoint fakeProgramPoint = new ProgramPoint() { - - @Override - public CodeLocation getLocation() { - return fakeLocation; - } - - @Override - public CFG getCFG() { - return null; - } - }; - - private final SemanticOracle fakeOracle = new SemanticOracle() { - - @Override - public Set getRuntimeTypesOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return Collections.singleton(e.getStaticType()); - } - - @Override - public Type getDynamicTypeOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return e.getStaticType(); - } - - @Override - public ExpressionSet rewrite( - SymbolicExpression expression, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return new ExpressionSet(expression); - } - }; - - private final Variable x = new Variable(untyped, "x", fakeProgramPoint.getLocation()); - private final Variable y = new Variable(untyped, "y", fakeProgramPoint.getLocation()); + private final Variable x = new Variable(untyped, "x", pp1.getLocation()); + private final Variable y = new Variable(untyped, "y", pp1.getLocation()); private final PointBasedHeap emptyHeap = new PointBasedHeap(); private final PointBasedHeap topHeap = new PointBasedHeap().top(); @@ -131,14 +87,14 @@ public ExpressionSet rewrite( public void testAssign() throws SemanticException { Constant one = new Constant(Int32Type.INSTANCE, 1, loc1); Constant zero = new Constant(Int32Type.INSTANCE, 0, loc1); - PointBasedHeap assignResult = topHeap.assign(x, one, fakeProgramPoint, fakeOracle); + PointBasedHeap assignResult = topHeap.assign(x, one, pp1, fakeOracle); // constants do not affect heap abstract domain assertEquals(topHeap, assignResult); assignResult = topHeap.assign(x, - new BinaryExpression(intType, one, zero, NumericNonOverflowingAdd.INSTANCE, fakeLocation), - fakeProgramPoint, fakeOracle); + new BinaryExpression(intType, one, zero, NumericNonOverflowingAdd.INSTANCE, loc1), + pp1, fakeOracle); // binary expressions do not affect heap abstract domain assertEquals(assignResult, topHeap); @@ -457,26 +413,26 @@ public void testAccessChildRewrite() throws SemanticException { AccessChild accessChild = new AccessChild(untyped, x, y, loc1); ExpressionSet expectedRewritten = new ExpressionSet(alloc1); - assertEquals(expectedRewritten, xAssign.rewrite(accessChild, fakeProgramPoint, fakeOracle)); + assertEquals(expectedRewritten, xAssign.rewrite(accessChild, pp1, fakeOracle)); // y.x rewritten in x -> pp1 = empty set accessChild = new AccessChild(untyped, y, x, loc1); - assertEquals(new ExpressionSet(), xAssign.rewrite(accessChild, fakeProgramPoint, fakeOracle)); + assertEquals(new ExpressionSet(), xAssign.rewrite(accessChild, pp1, fakeOracle)); } @Test public void testIdentifierRewrite() throws SemanticException { PointBasedHeap xAssign = topHeap.assign(x, new HeapReference(untyped, - new MemoryAllocation(untyped, loc1), fakeLocation), + new MemoryAllocation(untyped, loc1), loc1), pp1, fakeOracle); // x rewritten in x -> pp1 = pp1 ExpressionSet expectedRewritten = new ExpressionSet( - new MemoryPointer(untyped, alloc1, fakeLocation)); - assertEquals(xAssign.rewrite(x, fakeProgramPoint, fakeOracle), expectedRewritten); + new MemoryPointer(untyped, alloc1, loc1)); + assertEquals(xAssign.rewrite(x, pp1, fakeOracle), expectedRewritten); // y rewritten in x -> pp1 = {y} - assertEquals(xAssign.rewrite(y, fakeProgramPoint, fakeOracle), new ExpressionSet(y)); + assertEquals(xAssign.rewrite(y, pp1, fakeOracle), new ExpressionSet(y)); } @Test @@ -486,21 +442,21 @@ public void testHeapDereferenceRewrite() throws SemanticException { new MemoryAllocation(untyped, loc1, new Annotations()), loc1), loc1); ExpressionSet expectedRewritten = new ExpressionSet(alloc1); - assertEquals(expectedRewritten, topHeap.rewrite(deref, fakeProgramPoint, fakeOracle)); + assertEquals(expectedRewritten, topHeap.rewrite(deref, pp1, fakeOracle)); // *(x) rewritten in x -> pp1 -> pp1 PointBasedHeap xAssign = topHeap.assign(x, new HeapReference(untyped, - new MemoryAllocation(untyped, loc1), fakeLocation), + new MemoryAllocation(untyped, loc1), loc1), pp1, fakeOracle); deref = new HeapDereference(untyped, x, loc1); expectedRewritten = new ExpressionSet(alloc1); - assertEquals(expectedRewritten, xAssign.rewrite(deref, fakeProgramPoint, fakeOracle)); + assertEquals(expectedRewritten, xAssign.rewrite(deref, pp1, fakeOracle)); // *(y) rewritten in x -> pp1 -> empty set - AllocationSite expectedUnknownAlloc = new StackAllocationSite(untyped, "unknown@y", true, fakeLocation); + AllocationSite expectedUnknownAlloc = new StackAllocationSite(untyped, "unknown@y", true, loc1); deref = new HeapDereference(untyped, y, loc1); expectedRewritten = new ExpressionSet(expectedUnknownAlloc); - assertEquals(expectedRewritten, xAssign.rewrite(deref, fakeProgramPoint, fakeOracle)); + assertEquals(expectedRewritten, xAssign.rewrite(deref, pp1, fakeOracle)); } } diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValueTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValueTest.java index 4c27e3221..14f4fe96c 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValueTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValueTest.java @@ -6,7 +6,7 @@ import it.unive.lisa.TestParameterProvider; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; +import it.unive.lisa.analysis.lattices.Satisfiability; import java.lang.reflect.InvocationTargetException; import java.lang.reflect.Method; import java.lang.reflect.Modifier; diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomainTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomainTest.java index 882dae999..132912569 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomainTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomainTest.java @@ -6,7 +6,7 @@ import it.unive.lisa.TestParameterProvider; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; +import it.unive.lisa.analysis.lattices.Satisfiability; import java.lang.reflect.InvocationTargetException; import java.lang.reflect.Method; import java.lang.reflect.Modifier; diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomainTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomainTest.java index fe9d04b06..38e1e5782 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomainTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomainTest.java @@ -6,7 +6,7 @@ import it.unive.lisa.TestParameterProvider; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; +import it.unive.lisa.analysis.lattices.Satisfiability; import java.lang.reflect.InvocationTargetException; import java.lang.reflect.Method; import java.lang.reflect.Modifier; diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/numeric/IntervalTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/numeric/IntervalTest.java index 7f5673fe3..0ed525a14 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/numeric/IntervalTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/numeric/IntervalTest.java @@ -4,17 +4,13 @@ import static org.junit.Assert.assertFalse; import static org.junit.Assert.assertTrue; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; +import it.unive.lisa.TestParameterProvider; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; -import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; -import it.unive.lisa.program.SourceCodeLocation; -import it.unive.lisa.program.cfg.CFG; -import it.unive.lisa.program.cfg.CodeLocation; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.program.type.Int32Type; -import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Constant; import it.unive.lisa.symbolic.value.Variable; import it.unive.lisa.symbolic.value.operator.binary.ComparisonEq; @@ -28,13 +24,11 @@ import it.unive.lisa.symbolic.value.operator.binary.NumericNonOverflowingMul; import it.unive.lisa.symbolic.value.operator.binary.NumericNonOverflowingSub; import it.unive.lisa.symbolic.value.operator.unary.NumericNegation; -import it.unive.lisa.type.Type; import it.unive.lisa.util.numeric.InfiniteIterationException; import it.unive.lisa.util.numeric.IntInterval; import java.util.ArrayList; import java.util.List; import java.util.Random; -import java.util.Set; import org.junit.Test; public class IntervalTest { @@ -42,52 +36,13 @@ public class IntervalTest { private static final int TEST_LIMIT = 5000; private final Random rand = new Random(); - private final ProgramPoint pp = new ProgramPoint() { - - @Override - public CodeLocation getLocation() { - return new SourceCodeLocation("fake", 0, 0); - } - - @Override - public CFG getCFG() { - return null; - } - }; + private final ProgramPoint pp = TestParameterProvider.provideParam(null, ProgramPoint.class);; private final Interval singleton = new Interval(); private final Variable variable = new Variable(Int32Type.INSTANCE, "x", pp.getLocation()); private final Variable varAux = new Variable(Int32Type.INSTANCE, "aux", pp.getLocation()); private final ValueEnvironment< Interval> env = new ValueEnvironment<>(singleton).putState(variable, singleton.top()); - private final SemanticOracle oracle = new SemanticOracle() { - - @Override - public Set getRuntimeTypesOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - - @Override - public Type getDynamicTypeOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - - @Override - public ExpressionSet rewrite( - SymbolicExpression expression, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - }; + private final SemanticOracle oracle = TestParameterProvider.provideParam(null, SemanticOracle.class); @Test public void testEvalConstant() { diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/fsa/ContainsTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/fsa/ContainsTest.java index 33ead1197..959727b77 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/fsa/ContainsTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/fsa/ContainsTest.java @@ -2,53 +2,21 @@ import static org.junit.Assert.assertEquals; -import it.unive.lisa.analysis.SemanticDomain; +import it.unive.lisa.TestParameterProvider; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; -import it.unive.lisa.analysis.lattices.ExpressionSet; -import it.unive.lisa.program.cfg.ProgramPoint; -import it.unive.lisa.symbolic.SymbolicExpression; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.symbolic.value.operator.binary.StringContains; -import it.unive.lisa.type.Type; import it.unive.lisa.util.datastructures.automaton.State; import it.unive.lisa.util.datastructures.automaton.Transition; import java.util.Collections; -import java.util.Set; import java.util.SortedSet; import java.util.TreeSet; import org.junit.Test; public class ContainsTest { - private final SemanticOracle oracle = new SemanticOracle() { - - @Override - public Set getRuntimeTypesOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - - @Override - public Type getDynamicTypeOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - - @Override - public ExpressionSet rewrite( - SymbolicExpression expression, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - }; + private final SemanticOracle oracle = TestParameterProvider.provideParam(null, SemanticOracle.class); @Test public void test01() throws SemanticException { @@ -82,7 +50,7 @@ public void test01() throws SemanticException { FSA fsa = new FSA(a); FSA fsa1 = new FSA(a2); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, fsa.satisfiesBinaryExpression(StringContains.INSTANCE, fsa, fsa1, null, oracle)); } @@ -118,7 +86,7 @@ public void test02() throws SemanticException { FSA fsa = new FSA(a); FSA fsa1 = new FSA(a2); - assertEquals(SemanticDomain.Satisfiability.NOT_SATISFIED, + assertEquals(Satisfiability.NOT_SATISFIED, fsa.satisfiesBinaryExpression(StringContains.INSTANCE, fsa, fsa1, null, oracle)); } @@ -154,7 +122,7 @@ public void test03() throws SemanticException { FSA fsa = new FSA(a); FSA fsa1 = new FSA(a2); - assertEquals(SemanticDomain.Satisfiability.SATISFIED, + assertEquals(Satisfiability.SATISFIED, fsa.satisfiesBinaryExpression(StringContains.INSTANCE, fsa, fsa1, null, oracle)); } @@ -192,7 +160,7 @@ public void test04() throws SemanticException { FSA fsa = new FSA(a); FSA fsa1 = new FSA(a2); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, fsa.satisfiesBinaryExpression(StringContains.INSTANCE, fsa, fsa1, null, oracle)); } @@ -227,7 +195,7 @@ public void test05() throws SemanticException { FSA fsa = new FSA(a); FSA fsa1 = new FSA(a2); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, fsa.satisfiesBinaryExpression(StringContains.INSTANCE, fsa, fsa1, null, oracle)); } diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/tarsis/ContainsTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/tarsis/ContainsTest.java index 0cd48e3ec..0a54745e2 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/tarsis/ContainsTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/tarsis/ContainsTest.java @@ -2,56 +2,23 @@ import static org.junit.Assert.assertEquals; -import it.unive.lisa.analysis.SemanticDomain; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; +import it.unive.lisa.TestParameterProvider; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; -import it.unive.lisa.analysis.lattices.ExpressionSet; -import it.unive.lisa.program.cfg.ProgramPoint; -import it.unive.lisa.symbolic.SymbolicExpression; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.symbolic.value.operator.binary.StringContains; -import it.unive.lisa.type.Type; import it.unive.lisa.util.datastructures.automaton.State; import it.unive.lisa.util.datastructures.automaton.Transition; import it.unive.lisa.util.datastructures.regex.Atom; import it.unive.lisa.util.datastructures.regex.RegularExpression; import java.util.Collections; -import java.util.Set; import java.util.SortedSet; import java.util.TreeSet; import org.junit.Test; public class ContainsTest { - private final SemanticOracle oracle = new SemanticOracle() { - - @Override - public Set getRuntimeTypesOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - - @Override - public Type getDynamicTypeOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - - @Override - public ExpressionSet rewrite( - SymbolicExpression expression, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - }; + private final SemanticOracle oracle = TestParameterProvider.provideParam(null, SemanticOracle.class); @Test public void test01() throws SemanticException { @@ -85,7 +52,7 @@ public void test01() throws SemanticException { Tarsis t1 = new Tarsis(a); Tarsis t2 = new Tarsis(a2); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -121,7 +88,7 @@ public void test02() throws SemanticException { Tarsis t1 = new Tarsis(a); Tarsis t2 = new Tarsis(a2); - assertEquals(SemanticDomain.Satisfiability.NOT_SATISFIED, + assertEquals(Satisfiability.NOT_SATISFIED, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -157,7 +124,7 @@ public void test03() throws SemanticException { Tarsis t1 = new Tarsis(a); Tarsis t2 = new Tarsis(a2); - assertEquals(SemanticDomain.Satisfiability.SATISFIED, + assertEquals(Satisfiability.SATISFIED, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -195,7 +162,7 @@ public void test04() throws SemanticException { Tarsis t1 = new Tarsis(a); Tarsis t2 = new Tarsis(a2); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -230,7 +197,7 @@ public void test05() throws SemanticException { Tarsis t1 = new Tarsis(a); Tarsis t2 = new Tarsis(a2); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -238,7 +205,7 @@ public void test05() throws SemanticException { public void test06() throws SemanticException { Tarsis t1 = new Tarsis(RegexAutomaton.topString()); Tarsis t2 = new Tarsis(RegexAutomaton.string("a")); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -246,7 +213,7 @@ public void test06() throws SemanticException { public void test07() throws SemanticException { Tarsis t1 = new Tarsis(RegexAutomaton.string("a")); Tarsis t2 = new Tarsis(RegexAutomaton.topString()); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -254,7 +221,7 @@ public void test07() throws SemanticException { public void test08() throws SemanticException { Tarsis t1 = new Tarsis(RegexAutomaton.topString().concat(RegexAutomaton.string("a"))); Tarsis t2 = new Tarsis(RegexAutomaton.string("a")); - assertEquals(SemanticDomain.Satisfiability.SATISFIED, + assertEquals(Satisfiability.SATISFIED, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -263,7 +230,7 @@ public void test09() throws SemanticException { Tarsis t1 = new Tarsis(RegexAutomaton.string("a")); Tarsis t2 = new Tarsis(RegexAutomaton.topString().concat(RegexAutomaton.string("a"))); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -271,7 +238,7 @@ public void test09() throws SemanticException { public void test10() throws SemanticException { Tarsis t1 = new Tarsis(RegexAutomaton.topString().concat(RegexAutomaton.string("a"))); Tarsis t2 = new Tarsis(RegexAutomaton.topString().concat(RegexAutomaton.string("b"))); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -279,7 +246,7 @@ public void test10() throws SemanticException { public void test11() throws SemanticException { Tarsis t1 = new Tarsis(RegexAutomaton.topString().concat(RegexAutomaton.string("a"))); Tarsis t2 = new Tarsis(RegexAutomaton.string("ba")); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -287,7 +254,7 @@ public void test11() throws SemanticException { public void test12() throws SemanticException { Tarsis t1 = new Tarsis(RegexAutomaton.string("ba")); Tarsis t2 = new Tarsis(RegexAutomaton.topString().concat(RegexAutomaton.string("a"))); - assertEquals(SemanticDomain.Satisfiability.UNKNOWN, + assertEquals(Satisfiability.UNKNOWN, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } @@ -295,7 +262,7 @@ public void test12() throws SemanticException { public void test13() throws SemanticException { Tarsis t1 = new Tarsis(RegexAutomaton.string("ba")); Tarsis t2 = new Tarsis(RegexAutomaton.topString().concat(RegexAutomaton.string("c"))); - assertEquals(SemanticDomain.Satisfiability.NOT_SATISFIED, + assertEquals(Satisfiability.NOT_SATISFIED, t1.satisfiesBinaryExpression(StringContains.INSTANCE, t1, t2, null, oracle)); } diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/types/InferredTypesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/types/InferredTypesTest.java index 38fed2e3a..1a36942b5 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/types/InferredTypesTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/types/InferredTypesTest.java @@ -4,21 +4,16 @@ import static org.junit.Assert.assertFalse; import static org.junit.Assert.assertTrue; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; +import it.unive.lisa.TestParameterProvider; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; -import it.unive.lisa.analysis.lattices.ExpressionSet; -import it.unive.lisa.imp.IMPFeatures; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.imp.types.IMPTypeSystem; -import it.unive.lisa.program.Program; -import it.unive.lisa.program.cfg.CFG; -import it.unive.lisa.program.cfg.CodeLocation; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.program.type.BoolType; import it.unive.lisa.program.type.Float32Type; import it.unive.lisa.program.type.Int32Type; import it.unive.lisa.program.type.StringType; -import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator; import it.unive.lisa.symbolic.value.operator.binary.ComparisonEq; import it.unive.lisa.symbolic.value.operator.binary.ComparisonGe; @@ -107,53 +102,9 @@ public class InferredTypesTest { private final InferredTypes domain = new InferredTypes(); - private final ProgramPoint fake = new ProgramPoint() { + private final ProgramPoint fake = TestParameterProvider.provideParam(null, ProgramPoint.class); - @Override - public CFG getCFG() { - return null; - } - - @Override - public CodeLocation getLocation() { - return null; - } - - @Override - public Program getProgram() { - return new Program(new IMPFeatures(), new IMPTypeSystem()); - } - }; - - private final SemanticOracle oracle = new SemanticOracle() { - - @Override - public Set getRuntimeTypesOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - - @Override - public Type getDynamicTypeOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - - @Override - public ExpressionSet rewrite( - SymbolicExpression expression, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - }; + private final SemanticOracle oracle = TestParameterProvider.provideParam(null, SemanticOracle.class); @Test public void testCastWithNoTokens() { diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java index 4b58b31d0..7913bbfa8 100644 --- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java +++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java @@ -7,7 +7,6 @@ import it.unive.lisa.analysis.AnalyzedCFG; import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.SemanticDomain; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.SimpleAbstractState; @@ -20,6 +19,7 @@ import it.unive.lisa.analysis.heap.HeapDomain; import it.unive.lisa.analysis.heap.MonolithicHeap; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonInterference.NonInterference; import it.unive.lisa.analysis.nonRedundantSet.ValueNonRedundantSet; import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment; @@ -134,6 +134,26 @@ public ExpressionSet rewrite( throws SemanticException { return new ExpressionSet(expression); } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } }; @Before @@ -372,6 +392,28 @@ public ExpressionSet rewrite( return new ExpressionSet(); } + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + HeapEnvironment environment, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + HeapEnvironment environment, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } + } private Object domainFor( diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalysisState.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalysisState.java index 0dfe37846..1f32d2b0c 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalysisState.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalysisState.java @@ -1,7 +1,7 @@ package it.unive.lisa.analysis; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; @@ -340,7 +340,7 @@ public AnalysisState assume( * * @throws SemanticException if an error occurs during the computation */ - public SemanticDomain.Satisfiability satisfies( + public Satisfiability satisfies( SymbolicExpression expression, ProgramPoint pp) throws SemanticException { diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/SemanticDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/SemanticDomain.java index cacfc7f54..d5b33b634 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/SemanticDomain.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/SemanticDomain.java @@ -1,11 +1,10 @@ package it.unive.lisa.analysis; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; -import it.unive.lisa.util.representation.StringRepresentation; import it.unive.lisa.util.representation.StructuredObject; -import it.unive.lisa.util.representation.StructuredRepresentation; import java.util.Collection; import java.util.HashSet; import java.util.function.Predicate; @@ -180,285 +179,6 @@ Satisfiability satisfies( SemanticOracle oracle) throws SemanticException; - /** - * The satisfiability of an expression. - * - * @author Luca Negrini - */ - public enum Satisfiability - implements - Lattice { - /** - * Represent the fact that an expression is satisfied. - */ - SATISFIED { - @Override - public Satisfiability negate() { - return NOT_SATISFIED; - } - - @Override - public Satisfiability and( - Satisfiability other) { - return other; - } - - @Override - public Satisfiability or( - Satisfiability other) { - return this; - } - - @Override - public Satisfiability lub( - Satisfiability other) - throws SemanticException { - if (other == UNKNOWN || other == NOT_SATISFIED) - return UNKNOWN; - return this; - } - - @Override - public boolean lessOrEqual( - Satisfiability other) - throws SemanticException { - return other == this || other == UNKNOWN; - } - - @Override - public Satisfiability glb( - Satisfiability other) { - if (other == BOTTOM || other == NOT_SATISFIED) - return BOTTOM; - return this; - } - }, - - /** - * Represent the fact that an expression is not satisfied. - */ - NOT_SATISFIED { - @Override - public Satisfiability negate() { - return SATISFIED; - } - - @Override - public Satisfiability and( - Satisfiability other) { - return this; - } - - @Override - public Satisfiability or( - Satisfiability other) { - return other; - } - - @Override - public Satisfiability lub( - Satisfiability other) - throws SemanticException { - if (other == UNKNOWN || other == SATISFIED) - return UNKNOWN; - return this; - } - - @Override - public boolean lessOrEqual( - Satisfiability other) - throws SemanticException { - return other == this || other == UNKNOWN; - } - - @Override - public Satisfiability glb( - Satisfiability other) { - if (other == BOTTOM || other == SATISFIED) - return BOTTOM; - return this; - } - }, - - /** - * Represent the fact that it is not possible to determine whether or - * not an expression is satisfied. - */ - UNKNOWN { - @Override - public Satisfiability negate() { - return this; - } - - @Override - public Satisfiability and( - Satisfiability other) { - if (other == NOT_SATISFIED) - return other; - - return this; - } - - @Override - public Satisfiability or( - Satisfiability other) { - if (other == SATISFIED) - return other; - - return this; - } - - @Override - public Satisfiability lub( - Satisfiability other) - throws SemanticException { - return this; - } - - @Override - public boolean lessOrEqual( - Satisfiability other) - throws SemanticException { - return other == UNKNOWN; - } - - @Override - public Satisfiability glb( - Satisfiability other) { - return other; - } - }, - - /** - * Represent the fact that the satisfiability evaluation resulted in an - * error. - */ - BOTTOM { - @Override - public Satisfiability negate() { - return this; - } - - @Override - public Satisfiability and( - Satisfiability other) { - return this; - } - - @Override - public Satisfiability or( - Satisfiability other) { - return this; - } - - @Override - public Satisfiability lub( - Satisfiability other) - throws SemanticException { - return other; - } - - @Override - public boolean lessOrEqual( - Satisfiability other) - throws SemanticException { - return true; - } - - @Override - public Satisfiability glb( - Satisfiability other) { - return this; - } - }; - - /** - * Negates the current satisfiability, getting the opposite result. - * - * @return the negation of this satisfiability instance - */ - public abstract Satisfiability negate(); - - /** - * Performs a logical and between this satisfiability and the given one. - * - * @param other the other satisfiability - * - * @return the logical and between the two satisfiability instances - */ - public abstract Satisfiability and( - Satisfiability other); - - /** - * Performs a logical or between this satisfiability and the given one. - * - * @param other the other satisfiability - * - * @return the logical or between the two satisfiability instances - */ - public abstract Satisfiability or( - Satisfiability other); - - /** - * Performs the greatest lower bound operation between this - * satisfiability and the given one. - * - * @param other the other satisfiability - * - * @return the result of the greatest lower bound - */ - public abstract Satisfiability glb( - Satisfiability other); - - /** - * Transforms a boolean value to a {@link Satisfiability} instance. - * - * @param bool the boolean to transform - * - * @return {@link #SATISFIED} if {@code bool} is {@code true}, - * {@link #NOT_SATISFIED} otherwise - */ - public static Satisfiability fromBoolean( - boolean bool) { - return bool ? SATISFIED : NOT_SATISFIED; - } - - @Override - public Satisfiability top() { - return UNKNOWN; - } - - @Override - public Satisfiability bottom() { - return BOTTOM; - } - - /** - * Yields whether or not this element can represent a {@code true} - * result. - * - * @return {@code true} if that condition holds - */ - public boolean mightBeTrue() { - return this == SATISFIED || this == UNKNOWN; - } - - /** - * Yields whether or not this element can represent a {@code false} - * result. - * - * @return {@code true} if that condition holds - */ - public boolean mightBeFalse() { - return this == NOT_SATISFIED || this == UNKNOWN; - } - - @Override - public StructuredRepresentation representation() { - return new StringRepresentation(name()); - } - } - /** * Yields a unique instance of the specific domain, of class {@code domain}, * contained inside the domain, also recursively querying inner domains diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/dataflow/DataflowDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/dataflow/DataflowDomain.java index 017711e96..32490c233 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/dataflow/DataflowDomain.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/dataflow/DataflowDomain.java @@ -4,6 +4,7 @@ import it.unive.lisa.analysis.ScopeToken; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.value.Identifier; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/MemoryOracle.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/MemoryOracle.java index 43c4ca79c..389e031e9 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/MemoryOracle.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/MemoryOracle.java @@ -3,9 +3,13 @@ import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.heap.HeapExpression; +import it.unive.lisa.symbolic.value.HeapLocation; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.MemoryPointer; import it.unive.lisa.symbolic.value.ValueExpression; import java.util.HashSet; import java.util.Set; @@ -66,4 +70,126 @@ default ExpressionSet rewrite( return new ExpressionSet(result); } + /** + * Yields whether or not the two given expressions are aliases, that is, if + * they point to the same region of memory. Note that, for this method to + * return {@link Satisfiability#SATISFIED}, both expressions should be + * pointers to other expressions. + * + * @param x the first expression + * @param y the second expression + * @param pp the {@link ProgramPoint} where the computation happens + * @param oracle the oracle for inter-domain communication + * + * @return whether or not the two expressions are aliases + * + * @throws SemanticException if something goes wrong during the computation + */ + Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException; + + /** + * Yields all the {@link Identifier}s that are reachable starting from the + * {@link Identifier} represented (directly or after rewriting) by the given + * expression. This corresponds to recursively explore the memory region + * reachable by {@code e}, traversing all possible pointers until no more + * are available. + * + * @param e the expression corresponding to the starting point + * @param pp the {@link ProgramPoint} where the computation happens + * @param oracle the oracle for inter-domain communication + * + * @return the expressions representing memory regions reachable from + * {@code e} + * + * @throws SemanticException if something goes wrong during the computation + */ + default ExpressionSet reachableFrom( + SymbolicExpression e, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + Set ws = new HashSet<>(); + ws.add(e); + + Set result = new HashSet<>(); + Set prev = new HashSet<>(); + Set locs = new HashSet<>(); + rewrite(e, pp, oracle).elements().stream().forEach(result::add); + + do { + ws.addAll(locs); + prev = new HashSet<>(result); + for (SymbolicExpression id : ws) { + ExpressionSet rewritten = rewrite(id, pp, oracle); + locs = new HashSet<>(); + for (SymbolicExpression r : rewritten) { + if (r instanceof MemoryPointer) { + HeapLocation l = ((MemoryPointer) r).getReferencedLocation(); + locs.add(l); + result.add(l); + } else + locs.add(r); + } + } + } while (!prev.equals(result)); + + return new ExpressionSet(result); + } + + /** + * Yields whether or not the {@link Identifier} represented (directly or + * after rewriting) by the second expression is reachable starting from the + * {@link Identifier} represented (directly or after rewriting) by the first + * expression. Note that, for this method to return + * {@link Satisfiability#SATISFIED}, not only {@code x} needs to be a + * pointer to another expression, but the latter should be a pointer as + * well, and so on until {@code y} is reached. + * + * @param x the first expression + * @param y the second expression + * @param pp the {@link ProgramPoint} where the computation happens + * @param oracle the oracle for inter-domain communication + * + * @return whether or not the second expression can be reached from the + * first one + * + * @throws SemanticException if something goes wrong during the computation + */ + Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException; + + /** + * Yields whether or not the {@link Identifier} represented (directly or + * after rewriting) by the second expression is reachable starting from the + * {@link Identifier} represented (directly or after rewriting) by the first + * expression, and vice versa. This is equivalent to invoking + * {@code isReachableFrom(x, y, pp, oracle).and(isReachableFrom(y, x, pp, oracle))}, + * that corresponds to the default implementation of this method. + * + * @param x the first expression + * @param y the second expression + * @param pp the {@link ProgramPoint} where the computation happens + * @param oracle the oracle for inter-domain communication + * + * @return whether or not the two expressions are mutually reachable + * + * @throws SemanticException if something goes wrong during the computation + */ + default Satisfiability areMutuallyReachable( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return isReachableFrom(x, y, pp, oracle).and(isReachableFrom(y, x, pp, oracle)); + } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/lattices/Satisfiability.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/lattices/Satisfiability.java new file mode 100644 index 000000000..7625b8ef5 --- /dev/null +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/lattices/Satisfiability.java @@ -0,0 +1,284 @@ +package it.unive.lisa.analysis.lattices; + +import it.unive.lisa.analysis.Lattice; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.util.representation.StringRepresentation; +import it.unive.lisa.util.representation.StructuredRepresentation; + +/** + * A lattice representing sets of possible Boolean values: {@code (true)}, + * {@code (false)}, {@code (true, false)} or unknown, {@code ()} or bottom. + * + * @author Luca Negrini + */ +public enum Satisfiability + implements + Lattice { + /** + * Represent the fact that an expression is satisfied. + */ + SATISFIED { + @Override + public Satisfiability negate() { + return NOT_SATISFIED; + } + + @Override + public Satisfiability and( + Satisfiability other) { + return other; + } + + @Override + public Satisfiability or( + Satisfiability other) { + return this; + } + + @Override + public Satisfiability lub( + Satisfiability other) + throws SemanticException { + if (other == UNKNOWN || other == NOT_SATISFIED) + return UNKNOWN; + return this; + } + + @Override + public boolean lessOrEqual( + Satisfiability other) + throws SemanticException { + return other == this || other == UNKNOWN; + } + + @Override + public Satisfiability glb( + Satisfiability other) { + if (other == BOTTOM || other == NOT_SATISFIED) + return BOTTOM; + return this; + } + }, + + /** + * Represent the fact that an expression is not satisfied. + */ + NOT_SATISFIED { + @Override + public Satisfiability negate() { + return SATISFIED; + } + + @Override + public Satisfiability and( + Satisfiability other) { + return this; + } + + @Override + public Satisfiability or( + Satisfiability other) { + return other; + } + + @Override + public Satisfiability lub( + Satisfiability other) + throws SemanticException { + if (other == UNKNOWN || other == SATISFIED) + return UNKNOWN; + return this; + } + + @Override + public boolean lessOrEqual( + Satisfiability other) + throws SemanticException { + return other == this || other == UNKNOWN; + } + + @Override + public Satisfiability glb( + Satisfiability other) { + if (other == BOTTOM || other == SATISFIED) + return BOTTOM; + return this; + } + }, + + /** + * Represent the fact that it is not possible to determine whether or not an + * expression is satisfied. + */ + UNKNOWN { + @Override + public Satisfiability negate() { + return this; + } + + @Override + public Satisfiability and( + Satisfiability other) { + if (other == NOT_SATISFIED) + return other; + + return this; + } + + @Override + public Satisfiability or( + Satisfiability other) { + if (other == SATISFIED) + return other; + + return this; + } + + @Override + public Satisfiability lub( + Satisfiability other) + throws SemanticException { + return this; + } + + @Override + public boolean lessOrEqual( + Satisfiability other) + throws SemanticException { + return other == UNKNOWN; + } + + @Override + public Satisfiability glb( + Satisfiability other) { + return other; + } + }, + + /** + * Represent the fact that the satisfiability evaluation resulted in an + * error. + */ + BOTTOM { + @Override + public Satisfiability negate() { + return this; + } + + @Override + public Satisfiability and( + Satisfiability other) { + return this; + } + + @Override + public Satisfiability or( + Satisfiability other) { + return this; + } + + @Override + public Satisfiability lub( + Satisfiability other) + throws SemanticException { + return other; + } + + @Override + public boolean lessOrEqual( + Satisfiability other) + throws SemanticException { + return true; + } + + @Override + public Satisfiability glb( + Satisfiability other) { + return this; + } + }; + + /** + * Negates the current satisfiability, getting the opposite result. + * + * @return the negation of this satisfiability instance + */ + public abstract Satisfiability negate(); + + /** + * Performs a logical and between this satisfiability and the given one. + * + * @param other the other satisfiability + * + * @return the logical and between the two satisfiability instances + */ + public abstract Satisfiability and( + Satisfiability other); + + /** + * Performs a logical or between this satisfiability and the given one. + * + * @param other the other satisfiability + * + * @return the logical or between the two satisfiability instances + */ + public abstract Satisfiability or( + Satisfiability other); + + /** + * Performs the greatest lower bound operation between this satisfiability + * and the given one. + * + * @param other the other satisfiability + * + * @return the result of the greatest lower bound + */ + public abstract Satisfiability glb( + Satisfiability other); + + /** + * Transforms a boolean value to a {@link Satisfiability} instance. + * + * @param bool the boolean to transform + * + * @return {@link #SATISFIED} if {@code bool} is {@code true}, + * {@link #NOT_SATISFIED} otherwise + */ + public static Satisfiability fromBoolean( + boolean bool) { + return bool ? SATISFIED : NOT_SATISFIED; + } + + @Override + public Satisfiability top() { + return UNKNOWN; + } + + @Override + public Satisfiability bottom() { + return BOTTOM; + } + + /** + * Yields whether or not this element can represent a {@code true} result. + * + * @return {@code true} if that condition holds + */ + public boolean mightBeTrue() { + return this == SATISFIED || this == UNKNOWN; + } + + /** + * Yields whether or not this element can represent a {@code false} result. + * + * @return {@code true} if that condition holds + */ + public boolean mightBeFalse() { + return this == NOT_SATISFIED || this == UNKNOWN; + } + + @Override + public StructuredRepresentation representation() { + return new StringRepresentation(name()); + } +} diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/NonRelationalElement.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/NonRelationalElement.java index 8260045a2..35e29ded8 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/NonRelationalElement.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/NonRelationalElement.java @@ -1,11 +1,11 @@ package it.unive.lisa.analysis.nonrelational; import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticEvaluator; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.lattices.FunctionalLattice; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/VariableLift.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/VariableLift.java index 0aed667bb..cd6ddd8af 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/VariableLift.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/VariableLift.java @@ -5,6 +5,7 @@ import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.lattices.FunctionalLattice; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/heap/HeapEnvironment.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/heap/HeapEnvironment.java index b42ff275c..8ef75fb21 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/heap/HeapEnvironment.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/heap/HeapEnvironment.java @@ -5,6 +5,7 @@ import it.unive.lisa.analysis.heap.HeapDomain; import it.unive.lisa.analysis.lattices.ExpressionSet; import it.unive.lisa.analysis.lattices.FunctionalLattice; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.Environment; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; @@ -175,4 +176,24 @@ public boolean equals( return false; return true; } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return lattice.alias(x, y, this, pp, oracle); + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return lattice.isReachableFrom(x, y, this, pp, oracle); + } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/heap/NonRelationalHeapDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/heap/NonRelationalHeapDomain.java index af0907f6d..c803d7225 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/heap/NonRelationalHeapDomain.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/heap/NonRelationalHeapDomain.java @@ -4,6 +4,7 @@ import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.heap.HeapSemanticOperation; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.NonRelationalDomain; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; @@ -101,4 +102,57 @@ default ExpressionSet rewrite( return new ExpressionSet(result); } + /** + * Yields whether or not the two given expressions are aliases, that is, if + * they point to the same region of memory. Note that, for this method to + * return {@link Satisfiability#SATISFIED}, both expressions should be + * pointers to other expressions. + * + * @param x the first expression + * @param y the second expression + * @param environment the environment containing information about the + * program variables + * @param pp the {@link ProgramPoint} where the computation happens + * @param oracle the oracle for inter-domain communication + * + * @return whether or not the two expressions are aliases + * + * @throws SemanticException if something goes wrong during the computation + */ + Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + HeapEnvironment environment, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException; + + /** + * Yields whether or not the {@link Identifier} represented (directly or + * after rewriting) by the second expression is reachable starting from the + * {@link Identifier} represented (directly or after rewriting) by the first + * expression. Note that, for this method to return + * {@link Satisfiability#SATISFIED}, not only {@code x} needs to be a + * pointer to another expression, but the latter should be a pointer as + * well, and so on until {@code y} is reached. + * + * @param x the first expression + * @param y the second expression + * @param environment the environment containing information about the + * program variables + * @param pp the {@link ProgramPoint} where the computation happens + * @param oracle the oracle for inter-domain communication + * + * @return whether or not the second expression can be reached from the + * first one + * + * @throws SemanticException if something goes wrong during the computation + */ + Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + HeapEnvironment environment, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValue.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValue.java index b70ee2aba..e337eff7e 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValue.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValue.java @@ -1,9 +1,9 @@ package it.unive.lisa.analysis.nonrelational.inference; import it.unive.lisa.analysis.BaseLattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.ExpressionVisitor; import it.unive.lisa.symbolic.SymbolicExpression; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/InferenceSystem.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/InferenceSystem.java index c6fae67d9..adcff252c 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/InferenceSystem.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/InferenceSystem.java @@ -2,6 +2,7 @@ import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.VariableLift; import it.unive.lisa.analysis.nonrelational.inference.InferredValue.InferredPair; import it.unive.lisa.analysis.value.ValueDomain; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomain.java index 49a956f29..31a8a95ef 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomain.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalTypeDomain.java @@ -1,9 +1,9 @@ package it.unive.lisa.analysis.nonrelational.value; import it.unive.lisa.analysis.BaseLattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.Environment; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.ExpressionVisitor; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomain.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomain.java index 3800fe629..9ba2e9270 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomain.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/value/BaseNonRelationalValueDomain.java @@ -1,9 +1,9 @@ package it.unive.lisa.analysis.nonrelational.value; import it.unive.lisa.analysis.BaseLattice; -import it.unive.lisa.analysis.SemanticDomain.Satisfiability; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.nonrelational.Environment; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.ExpressionVisitor; diff --git a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestAbstractState.java b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestAbstractState.java index bec3ad25d..71fd97e15 100644 --- a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestAbstractState.java +++ b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestAbstractState.java @@ -4,6 +4,7 @@ import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.type.Type; @@ -72,4 +73,24 @@ public TestAbstractState withTopValues() { public TestAbstractState withTopTypes() { return this; } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } } diff --git a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestDomain.java b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestDomain.java index 5e1f0a8ef..27ef6fd44 100644 --- a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestDomain.java +++ b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestDomain.java @@ -5,6 +5,7 @@ import it.unive.lisa.analysis.SemanticDomain; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; diff --git a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestHeapDomain.java b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestHeapDomain.java index a0adbf2e8..dbd74d445 100644 --- a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestHeapDomain.java +++ b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestHeapDomain.java @@ -4,6 +4,7 @@ import it.unive.lisa.analysis.SemanticOracle; import it.unive.lisa.analysis.heap.HeapDomain; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.util.representation.StringRepresentation; @@ -33,4 +34,24 @@ public ExpressionSet rewrite( throws SemanticException { return new ExpressionSet(); } + + @Override + public Satisfiability alias( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } + + @Override + public Satisfiability isReachableFrom( + SymbolicExpression x, + SymbolicExpression y, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return Satisfiability.UNKNOWN; + } } diff --git a/lisa/lisa-sdk/src/test/java/it/unive/lisa/analysis/SubstitutionTest.java b/lisa/lisa-sdk/src/test/java/it/unive/lisa/analysis/SubstitutionTest.java index 4c41642aa..3dfbf3041 100644 --- a/lisa/lisa-sdk/src/test/java/it/unive/lisa/analysis/SubstitutionTest.java +++ b/lisa/lisa-sdk/src/test/java/it/unive/lisa/analysis/SubstitutionTest.java @@ -3,8 +3,10 @@ import static it.unive.lisa.util.collections.CollectionUtilities.collect; import static org.junit.Assert.assertTrue; +import it.unive.lisa.TestAbstractState; import it.unive.lisa.analysis.heap.HeapSemanticOperation.HeapReplacement; import it.unive.lisa.analysis.lattices.ExpressionSet; +import it.unive.lisa.analysis.lattices.Satisfiability; import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.program.SyntheticLocation; import it.unive.lisa.program.cfg.CFG; @@ -14,7 +16,6 @@ import it.unive.lisa.symbolic.value.Identifier; import it.unive.lisa.symbolic.value.ValueExpression; import it.unive.lisa.symbolic.value.Variable; -import it.unive.lisa.type.Type; import it.unive.lisa.type.Untyped; import it.unive.lisa.util.collections.CollectionsDiffBuilder; import it.unive.lisa.util.representation.StructuredRepresentation; @@ -24,7 +25,6 @@ import java.util.Comparator; import java.util.HashSet; import java.util.List; -import java.util.Set; import java.util.function.Predicate; import org.junit.Test; @@ -182,37 +182,10 @@ private void check( Collection remexpected) throws SemanticException { Collector c = new Collector(); + TestAbstractState oracle = new TestAbstractState(); if (sub != null) for (HeapReplacement repl : sub) - c = c.lub(c.applyReplacement(repl, fake, new SemanticOracle() { - - @Override - public Set getRuntimeTypesOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - - @Override - public Type getDynamicTypeOf( - SymbolicExpression e, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - - @Override - public ExpressionSet rewrite( - SymbolicExpression expression, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return null; - } - })); + c = c.lub(c.applyReplacement(repl, fake, oracle)); CollectionsDiffBuilder< SymbolicExpression> add = new CollectionsDiffBuilder<>(SymbolicExpression.class, addexpected,