From c0495899a085774dac0357f120bc076829f2236f Mon Sep 17 00:00:00 2001 From: giacomozanatta Date: Wed, 17 Sep 2025 23:36:49 -0400 Subject: [PATCH 1/9] ConstantPropagation with IntInterval fallback --- jlisa/src/main/java/it/unive/jlisa/Main.java | 20 +- .../analysis/ConstantPropWithInterval.java | 109 ++++++++++ .../ConstantPropWithIntervalLattice.java | 195 ++++++++++++++++++ .../checkers/AssertCheckerCPInterval.java | 164 +++++++++++++++ 4 files changed, 483 insertions(+), 5 deletions(-) create mode 100644 jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java create mode 100644 jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithIntervalLattice.java create mode 100644 jlisa/src/main/java/it/unive/jlisa/checkers/AssertCheckerCPInterval.java diff --git a/jlisa/src/main/java/it/unive/jlisa/Main.java b/jlisa/src/main/java/it/unive/jlisa/Main.java index a1f3f4c9d..5cf23d08f 100644 --- a/jlisa/src/main/java/it/unive/jlisa/Main.java +++ b/jlisa/src/main/java/it/unive/jlisa/Main.java @@ -1,9 +1,9 @@ package it.unive.jlisa; +import it.unive.jlisa.analysis.ConstantPropWithInterval; import it.unive.jlisa.analysis.heap.JavaFieldSensitivePointBasedHeap; import it.unive.jlisa.analysis.type.JavaInferredTypes; -import it.unive.jlisa.analysis.value.ConstantPropagation; -import it.unive.jlisa.checkers.AssertChecker; +import it.unive.jlisa.checkers.AssertCheckerCPInterval; import it.unive.jlisa.frontend.JavaFrontend; import it.unive.jlisa.frontend.exceptions.CSVExceptionWriter; import it.unive.jlisa.frontend.exceptions.ParsingException; @@ -249,7 +249,7 @@ private static void runAnalysis( conf.optimize = false; switch (checkerName) { case "Assert": - conf.semanticChecks.add(new AssertChecker()); + conf.semanticChecks.add(new AssertCheckerCPInterval()); break; case "": break; @@ -259,15 +259,25 @@ private static void runAnalysis( ValueDomain domain; switch (numericalDomain) { case "ConstantPropagation": - domain = new ConstantPropagation(); + // domain = new ConstantPropWithIntervalLattice(); break; default: throw new ParseException("Invalid numerical domain name: " + numericalDomain); } + /* + * conf.analysis = DefaultConfiguration.simpleState( + * DefaultConfiguration.defaultHeapDomain(), new Pentagon(), + * DefaultConfiguration.defaultTypeDomain()); + */ + /* + * DefaultConfiguration.simpleDomain(new + * JavaFieldSensitivePointBasedHeap(), new + * ConstantPropWithIntervalLattice(), new JavaInferredTypes()); + */ conf.analysis = new SimpleAbstractDomain<>( new JavaFieldSensitivePointBasedHeap(), - domain, + new ConstantPropWithInterval(), new JavaInferredTypes()); LiSA lisa = new LiSA(conf); diff --git a/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java b/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java new file mode 100644 index 000000000..20b279650 --- /dev/null +++ b/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java @@ -0,0 +1,109 @@ +package it.unive.jlisa.analysis; + +import it.unive.jlisa.analysis.value.ConstantPropagation; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.SemanticOracle; +import it.unive.lisa.analysis.heap.HeapDomain; +import it.unive.lisa.analysis.lattices.Satisfiability; +import it.unive.lisa.analysis.numeric.Interval; +import it.unive.lisa.analysis.value.ValueDomain; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.ValueExpression; + +public class ConstantPropWithInterval + implements + ValueDomain { + + private final ConstantPropagation constantPropagation = new ConstantPropagation(); + + private final Interval intervals = new Interval(); + + @Override + public ConstantPropWithIntervalLattice assign( + ConstantPropWithIntervalLattice state, + Identifier id, + ValueExpression expression, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantPropWithIntervalLattice( + constantPropagation.assign(state.first, id, expression, pp, oracle), + intervals.assign(state.second, id, expression, pp, oracle)); + } + + @Override + public ConstantPropWithIntervalLattice smallStepSemantics( + ConstantPropWithIntervalLattice state, + ValueExpression expression, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantPropWithIntervalLattice( + constantPropagation.smallStepSemantics(state.first, expression, pp, oracle), + intervals.smallStepSemantics(state.second, expression, pp, oracle)); + } + + @Override + public ConstantPropWithIntervalLattice assume( + ConstantPropWithIntervalLattice state, + ValueExpression expression, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + return new ConstantPropWithIntervalLattice( + constantPropagation.smallStepSemantics(state.first, expression, dest, oracle), + intervals.smallStepSemantics(state.second, expression, dest, oracle)); + } + + @Override + public Satisfiability satisfies( + ConstantPropWithIntervalLattice state, + ValueExpression expression, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + Satisfiability constantPropSatisfiability = constantPropagation.satisfies(state.first, expression, pp, oracle); + Satisfiability intervalsSatisfiability = intervals.satisfies(state.second, expression, pp, oracle); + + if (constantPropSatisfiability.isTop() || constantPropSatisfiability.isBottom()) { + return intervalsSatisfiability; + } + return constantPropSatisfiability; + } + + @Override + public ConstantPropWithIntervalLattice makeLattice() { + return new ConstantPropWithIntervalLattice(constantPropagation.makeLattice(), intervals.makeLattice()); + } + + @Override + public ConstantPropWithIntervalLattice applyReplacement( + ConstantPropWithIntervalLattice state, + HeapDomain.HeapReplacement r, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantPropWithIntervalLattice( + constantPropagation.applyReplacement(state.first, r, pp, oracle), + intervals.applyReplacement(state.second, r, pp, oracle)); + } + + @Override + public boolean equals( + Object o) { + if (o == null || getClass() != o.getClass()) + return false; + + ConstantPropWithInterval that = (ConstantPropWithInterval) o; + return constantPropagation.equals(that.constantPropagation) && intervals.equals(that.intervals); + } + + @Override + public int hashCode() { + int result = constantPropagation.hashCode(); + result = 31 * result + intervals.hashCode(); + return result; + } +} diff --git a/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithIntervalLattice.java b/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithIntervalLattice.java new file mode 100644 index 000000000..744fc036c --- /dev/null +++ b/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithIntervalLattice.java @@ -0,0 +1,195 @@ +package it.unive.jlisa.analysis; + +import it.unive.jlisa.lattices.ConstantValue; +import it.unive.lisa.analysis.Lattice; +import it.unive.lisa.analysis.ScopeToken; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.combination.ValueCartesianCombination; +import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.util.numeric.IntInterval; +import it.unive.lisa.util.representation.MapRepresentation; +import it.unive.lisa.util.representation.StringRepresentation; +import it.unive.lisa.util.representation.StructuredRepresentation; +import java.util.Collection; +import java.util.HashMap; +import java.util.Map; +import java.util.function.Predicate; +import org.apache.commons.collections4.CollectionUtils; + +public class ConstantPropWithIntervalLattice + extends + ValueCartesianCombination, + ValueEnvironment> { + public static ConstantPropWithIntervalLattice TOP = new ConstantPropWithIntervalLattice(ConstantValue.TOP, + IntInterval.TOP); + public static ConstantPropWithIntervalLattice BOTTOM = new ConstantPropWithIntervalLattice(); + + private ConstantPropWithIntervalLattice() { + super( + new ValueEnvironment<>(ConstantValue.TOP), + new ValueEnvironment<>(IntInterval.TOP)); + } + + public ConstantPropWithIntervalLattice( + ValueEnvironment constantPropagation, + ValueEnvironment interval) { + + super(constantPropagation, interval); + } + + public ConstantPropWithIntervalLattice( + ConstantValue constantValue, + IntInterval interval) { + super( + new ValueEnvironment<>(constantValue), + new ValueEnvironment<>(interval)); + } + + @Override + public ConstantPropWithIntervalLattice pushScope( + ScopeToken token, + ProgramPoint pp) + throws SemanticException { + + return new ConstantPropWithIntervalLattice(first.pushScope(token, pp), second.pushScope(token, pp)); + } + + @Override + public ConstantPropWithIntervalLattice popScope( + ScopeToken token, + ProgramPoint pp) + throws SemanticException { + return new ConstantPropWithIntervalLattice(first.popScope(token, pp), second.popScope(token, pp)); + } + + @Override + public boolean knowsIdentifier( + Identifier id) { + return first.knowsIdentifier(id) || second.knowsIdentifier(id); + } + + @Override + public ConstantPropWithIntervalLattice forgetIdentifier( + Identifier id, + ProgramPoint pp) + throws SemanticException { + return new ConstantPropWithIntervalLattice(first.forgetIdentifier(id, pp), second.forgetIdentifier(id, pp)); + } + + @Override + public ConstantPropWithIntervalLattice forgetIdentifiers( + Iterable ids, + ProgramPoint pp) + throws SemanticException { + return new ConstantPropWithIntervalLattice(first.forgetIdentifiers(ids, pp), second.forgetIdentifiers(ids, pp)); + } + + @Override + public ConstantPropWithIntervalLattice forgetIdentifiersIf( + Predicate test, + ProgramPoint pp) + throws SemanticException { + return new ConstantPropWithIntervalLattice(first.forgetIdentifiersIf(test, pp), + second.forgetIdentifiersIf(test, pp)); + } + + @Override + public ConstantPropWithIntervalLattice mk( + ValueEnvironment constantPropagation, + ValueEnvironment interval) { + return new ConstantPropWithIntervalLattice(constantPropagation, interval); + } + + @Override + public ConstantPropWithIntervalLattice top() { + return TOP; + } + + @Override + public boolean isTop() { + return first.isTop() && second.isTop(); + } + + @Override + public ConstantPropWithIntervalLattice bottom() { + return BOTTOM; + } + + @Override + public boolean isBottom() { + return first.isBottom() && second.isBottom(); + } + + @Override + public boolean lessOrEqualAux( + ConstantPropWithIntervalLattice other) + throws SemanticException { + if (second.lessOrEqual(other.second)) { + return true; + } + if (first.lessOrEqual(other.first)) { + return true; + } + return false; + } + + @Override + public > Collection getAllLatticeInstances( + Class lattice) { + return super.getAllLatticeInstances(lattice); + } + + @Override + public ConstantPropWithIntervalLattice lubAux( + ConstantPropWithIntervalLattice other) + throws SemanticException { + return mk(first.lub(other.first), second.lub(other.second)); + } + + @Override + public ConstantPropWithIntervalLattice wideningAux( + ConstantPropWithIntervalLattice other) + throws SemanticException { + return mk(first.widening(other.first), second.widening(other.second)); + } + + @Override + public ConstantPropWithIntervalLattice glbAux( + ConstantPropWithIntervalLattice other) + throws SemanticException { + return mk(first.glb(other.first), second.glb(other.second)); + } + + @Override + public ConstantPropWithIntervalLattice narrowingAux( + ConstantPropWithIntervalLattice other) + throws SemanticException { + return mk(first.narrowing(other.first), second.narrowing(other.second)); + } + + @Override + public ConstantPropWithIntervalLattice store( + Identifier target, + Identifier source) + throws SemanticException { + return mk(first.store(target, source), second.store(target, source)); + } + + @Override + public StructuredRepresentation representation() { + if (isTop()) + return Lattice.topRepresentation(); + if (isBottom()) + return Lattice.bottomRepresentation(); + Map mapping = new HashMap<>(); + for (Identifier id : CollectionUtils.union(first.getKeys(), second.getKeys())) + mapping.put( + new StringRepresentation(id), + new StringRepresentation( + first.getState(id).toString() + ", " + second.getState(id).representation())); + return new MapRepresentation(mapping); + } + +} \ No newline at end of file diff --git a/jlisa/src/main/java/it/unive/jlisa/checkers/AssertCheckerCPInterval.java b/jlisa/src/main/java/it/unive/jlisa/checkers/AssertCheckerCPInterval.java new file mode 100644 index 000000000..5c5b9d670 --- /dev/null +++ b/jlisa/src/main/java/it/unive/jlisa/checkers/AssertCheckerCPInterval.java @@ -0,0 +1,164 @@ +package it.unive.jlisa.checkers; + +import it.unive.jlisa.analysis.ConstantPropWithIntervalLattice; +import it.unive.jlisa.program.cfg.statement.asserts.AssertStatement; +import it.unive.jlisa.program.cfg.statement.asserts.AssertionStatement; +import it.unive.jlisa.program.cfg.statement.asserts.SimpleAssert; +import it.unive.lisa.analysis.AnalysisState; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.SimpleAbstractDomain; +import it.unive.lisa.analysis.lattices.Satisfiability; +import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment; +import it.unive.lisa.analysis.nonrelational.type.TypeEnvironment; +import it.unive.lisa.checks.semantic.CheckToolWithAnalysisResults; +import it.unive.lisa.checks.semantic.SemanticCheck; +import it.unive.lisa.lattices.SimpleAbstractState; +import it.unive.lisa.lattices.heap.allocations.AllocationSites; +import it.unive.lisa.lattices.types.TypeSet; +import it.unive.lisa.program.cfg.CFG; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.program.cfg.statement.Ret; +import it.unive.lisa.program.cfg.statement.Statement; +import it.unive.lisa.symbolic.SymbolicExpression; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; + +public class AssertCheckerCPInterval + implements + SemanticCheck< + SimpleAbstractState< + HeapEnvironment, + ConstantPropWithIntervalLattice, + TypeEnvironment>, + SimpleAbstractDomain< + HeapEnvironment, + ConstantPropWithIntervalLattice, + TypeEnvironment>> { + private static final Logger LOG = LogManager.getLogger(AssertCheckerCPInterval.class); + + @Override + public boolean visit( + CheckToolWithAnalysisResults< + SimpleAbstractState< + HeapEnvironment, + ConstantPropWithIntervalLattice, + TypeEnvironment>, + SimpleAbstractDomain< + HeapEnvironment, + ConstantPropWithIntervalLattice, + TypeEnvironment>> tool, + CFG graph, + Statement node) { + + // RuntimeException property checker + if (graph.getProgram().getEntryPoints().contains(graph) && node instanceof Ret) + try { + checkRuntimeException(tool, graph, node); + } catch (SemanticException e) { + e.printStackTrace(); + } + + // assert checker + if (node instanceof AssertStatement) + try { + checkAssert(tool, graph, (AssertStatement) node); + } catch (SemanticException e) { + e.printStackTrace(); + } + + return true; + } + + private void checkRuntimeException( + CheckToolWithAnalysisResults< + SimpleAbstractState< + HeapEnvironment, + ConstantPropWithIntervalLattice, + TypeEnvironment>, + SimpleAbstractDomain< + HeapEnvironment, + ConstantPropWithIntervalLattice, + TypeEnvironment>> tool, + CFG graph, + Statement node) + throws SemanticException { + + for (var result : tool.getResultOf(graph)) { + AnalysisState< + SimpleAbstractState< + HeapEnvironment, + ConstantPropWithIntervalLattice, + TypeEnvironment>> state = result.getAnalysisStateAfter(node); + + // checking if there exists at least one exception state + boolean hasExceptionState = !state.getErrors().isBottom() && + !state.getErrors().isTop() && + state.getErrors().function != null && + !state.getErrors().function.isEmpty() || + (!state.getSmashedErrors().isBottom() && + !state.getSmashedErrors().isTop() && + !state.getSmashedErrors().function.isEmpty()); + + SimpleAbstractState, ConstantPropWithIntervalLattice, + TypeEnvironment> normaleState = state.getExecutionState(); + + // if exceptions had been thrown, we raise a warning + if (hasExceptionState) + // if the normal state is bottom, we raise a definite error + if (normaleState.isBottom()) + tool.warnOn((Statement) node, "DEFINITE: uncaught runtime exception in main method"); + // otherwise, we raise a possible error (both normal and + // exception states are not bottom) + else + tool.warnOn((Statement) node, "POSSIBLE: uncaught runtime exception in main method"); + } + } + + private void checkAssert( + CheckToolWithAnalysisResults< + SimpleAbstractState< + HeapEnvironment, + ConstantPropWithIntervalLattice, + TypeEnvironment>, + SimpleAbstractDomain< + HeapEnvironment, + ConstantPropWithIntervalLattice, + TypeEnvironment>> tool, + CFG graph, + AssertStatement node) + throws SemanticException { + for (var result : tool.getResultOf(graph)) { + AnalysisState< + SimpleAbstractState< + HeapEnvironment, + ConstantPropWithIntervalLattice, + TypeEnvironment>> state = null; + if (node instanceof SimpleAssert) + state = result.getAnalysisStateAfter(((SimpleAssert) node).getSubExpression()); + else if (node instanceof AssertionStatement) { + state = result.getAnalysisStateAfter(((AssertionStatement) node).getLeft()); + } + + for (SymbolicExpression expr : state.getExecutionExpressions()) { + + Satisfiability sat = tool.getAnalysis().satisfies(state, expr, (ProgramPoint) node); + if (!state.getExecutionState().valueState.isBottom()) { + if (!state.getExecutionState().valueState.isTop()) { + if (sat == Satisfiability.SATISFIED) { + tool.warnOn((Statement) node, "DEFINITE: the assertion holds"); + } else if (sat == Satisfiability.NOT_SATISFIED) { + tool.warnOn((Statement) node, "DEFINITE: the assertion DOES NOT hold"); + } else if (sat == Satisfiability.UNKNOWN) + tool.warnOn((Statement) node, "POSSIBLE: the assertion MAY (NOT) BE hold"); + else + LOG.error("Cannot satisfy the expression"); + } else + tool.warnOn((Statement) node, "POSSIBLE: the assertion MAY (NOT) BE hold"); + } else { + // FIXME: property proved + LOG.error("The abstract state of assert's expression is BOTTOM"); + } + } + } + } +} From f4d5f0506c00c65804aeace435169d36d47979ef Mon Sep 17 00:00:00 2001 From: giacomozanatta Date: Thu, 18 Sep 2025 08:18:29 -0400 Subject: [PATCH 2/9] Fallback only if IntInterval is not bottom --- .../it/unive/jlisa/analysis/ConstantPropWithInterval.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java b/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java index 20b279650..0cb0c72df 100644 --- a/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java +++ b/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java @@ -68,7 +68,9 @@ public Satisfiability satisfies( Satisfiability intervalsSatisfiability = intervals.satisfies(state.second, expression, pp, oracle); if (constantPropSatisfiability.isTop() || constantPropSatisfiability.isBottom()) { - return intervalsSatisfiability; + if (!intervalsSatisfiability.isBottom()) { + return intervalsSatisfiability; + } } return constantPropSatisfiability; } From 7b1d366a420a00343de6ea79e09d23e4be75b76f Mon Sep 17 00:00:00 2001 From: giacomozanatta Date: Sat, 18 Oct 2025 21:13:58 +0200 Subject: [PATCH 3/9] Remove comment --- jlisa/src/main/java/it/unive/jlisa/Main.java | 5 ----- 1 file changed, 5 deletions(-) diff --git a/jlisa/src/main/java/it/unive/jlisa/Main.java b/jlisa/src/main/java/it/unive/jlisa/Main.java index 928518aeb..839004dd0 100644 --- a/jlisa/src/main/java/it/unive/jlisa/Main.java +++ b/jlisa/src/main/java/it/unive/jlisa/Main.java @@ -279,11 +279,6 @@ private static void runAnalysis( * DefaultConfiguration.defaultHeapDomain(), new Pentagon(), * DefaultConfiguration.defaultTypeDomain()); */ - /* - * DefaultConfiguration.simpleDomain(new - * JavaFieldSensitivePointBasedHeap(), new - * ConstantPropWithIntervalLattice(), new JavaInferredTypes()); - */ conf.analysis = new SimpleAbstractDomain<>( new JavaFieldSensitivePointBasedHeap(), new ConstantPropWithInterval(), From bb1a9b2b7914a54a67d151fbcec5caf27cc834ef Mon Sep 17 00:00:00 2001 From: Giacomo Zanatta Date: Fri, 31 Oct 2025 20:20:54 +0100 Subject: [PATCH 4/9] Add ConstantValueIntInterval BaseLattice --- .../lattices/ConstantValueIntInterval.java | 118 ++++++++++++++++++ 1 file changed, 118 insertions(+) create mode 100644 jlisa/src/main/java/it/unive/jlisa/lattices/ConstantValueIntInterval.java diff --git a/jlisa/src/main/java/it/unive/jlisa/lattices/ConstantValueIntInterval.java b/jlisa/src/main/java/it/unive/jlisa/lattices/ConstantValueIntInterval.java new file mode 100644 index 000000000..12dd839c3 --- /dev/null +++ b/jlisa/src/main/java/it/unive/jlisa/lattices/ConstantValueIntInterval.java @@ -0,0 +1,118 @@ +package it.unive.jlisa.lattices; + +import it.unive.lisa.analysis.BaseLattice; +import it.unive.lisa.analysis.Lattice; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.util.numeric.IntInterval; +import it.unive.lisa.util.representation.MapRepresentation; +import it.unive.lisa.util.representation.StringRepresentation; +import it.unive.lisa.util.representation.StructuredRepresentation; +import java.util.HashMap; +import java.util.Map; + +public class ConstantValueIntInterval + implements + BaseLattice { + + public static ConstantValueIntInterval TOP = new ConstantValueIntInterval(ConstantValue.TOP, IntInterval.TOP); + public static ConstantValueIntInterval BOTTOM = new ConstantValueIntInterval(ConstantValue.BOTTOM, + IntInterval.BOTTOM); + private ConstantValue constantValue; + private IntInterval intInterval; + + public ConstantValueIntInterval( + ConstantValue constantValue, + IntInterval intInterval) { + this.constantValue = constantValue; + this.intInterval = intInterval; + } + + public ConstantValue getConstantValue() { + return constantValue; + } + + public IntInterval getIntInterval() { + return intInterval; + } + + @Override + public boolean isTop() { + return constantValue.isTop() && intInterval.isTop(); + } + + @Override + public boolean isBottom() { + return constantValue.isBottom() && intInterval.isBottom(); + } + + @Override + public ConstantValueIntInterval top() { + return TOP; + } + + @Override + public ConstantValueIntInterval bottom() { + return BOTTOM; + } + + @Override + public StructuredRepresentation representation() { + if (isTop()) { + return Lattice.topRepresentation(); + } + if (isBottom()) { + return Lattice.bottomRepresentation(); + } + Map mapping = new HashMap<>(); + mapping.put(new StringRepresentation("constantValue"), constantValue.representation()); + mapping.put(new StringRepresentation("intInterval"), intInterval.representation()); + return new MapRepresentation(mapping); + } + + @Override + public ConstantValueIntInterval lubAux( + ConstantValueIntInterval other) + throws SemanticException { + return new ConstantValueIntInterval( + constantValue.lub(other.getConstantValue()), + intInterval.lub(other.getIntInterval())); + } + + @Override + public boolean lessOrEqualAux( + ConstantValueIntInterval other) + throws SemanticException { + if (constantValue.isTop() || other.getConstantValue().isTop()) { + return intInterval.lessOrEqual(other.getIntInterval()); + } + return constantValue.lessOrEqual(other.getConstantValue()); + } + + @Override + public ConstantValueIntInterval glbAux( + ConstantValueIntInterval other) + throws SemanticException { + return new ConstantValueIntInterval(constantValue.glb( + other.getConstantValue()), + intInterval.glb(other.getIntInterval())); + } + + @Override + public ConstantValueIntInterval narrowingAux( + ConstantValueIntInterval other) + throws SemanticException { + return new ConstantValueIntInterval(constantValue.narrowing( + other.getConstantValue()), + intInterval.narrowing(other.getIntInterval())); + } + + @Override + public ConstantValueIntInterval wideningAux( + ConstantValueIntInterval other) + throws SemanticException { + return new ConstantValueIntInterval(constantValue.widening( + other.getConstantValue()), + intInterval.widening(other.getIntInterval())); + } + +} From ddcc263340ce50d6312a1ea9f216ab76717ac39b Mon Sep 17 00:00:00 2001 From: Giacomo Zanatta Date: Fri, 31 Oct 2025 21:25:52 +0100 Subject: [PATCH 5/9] Remove old domain --- .../analysis/ConstantPropWithInterval.java | 111 ---------- .../ConstantPropWithIntervalLattice.java | 195 ------------------ 2 files changed, 306 deletions(-) delete mode 100644 jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java delete mode 100644 jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithIntervalLattice.java diff --git a/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java b/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java deleted file mode 100644 index 0cb0c72df..000000000 --- a/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithInterval.java +++ /dev/null @@ -1,111 +0,0 @@ -package it.unive.jlisa.analysis; - -import it.unive.jlisa.analysis.value.ConstantPropagation; -import it.unive.lisa.analysis.SemanticException; -import it.unive.lisa.analysis.SemanticOracle; -import it.unive.lisa.analysis.heap.HeapDomain; -import it.unive.lisa.analysis.lattices.Satisfiability; -import it.unive.lisa.analysis.numeric.Interval; -import it.unive.lisa.analysis.value.ValueDomain; -import it.unive.lisa.program.cfg.ProgramPoint; -import it.unive.lisa.symbolic.value.Identifier; -import it.unive.lisa.symbolic.value.ValueExpression; - -public class ConstantPropWithInterval - implements - ValueDomain { - - private final ConstantPropagation constantPropagation = new ConstantPropagation(); - - private final Interval intervals = new Interval(); - - @Override - public ConstantPropWithIntervalLattice assign( - ConstantPropWithIntervalLattice state, - Identifier id, - ValueExpression expression, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return new ConstantPropWithIntervalLattice( - constantPropagation.assign(state.first, id, expression, pp, oracle), - intervals.assign(state.second, id, expression, pp, oracle)); - } - - @Override - public ConstantPropWithIntervalLattice smallStepSemantics( - ConstantPropWithIntervalLattice state, - ValueExpression expression, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return new ConstantPropWithIntervalLattice( - constantPropagation.smallStepSemantics(state.first, expression, pp, oracle), - intervals.smallStepSemantics(state.second, expression, pp, oracle)); - } - - @Override - public ConstantPropWithIntervalLattice assume( - ConstantPropWithIntervalLattice state, - ValueExpression expression, - ProgramPoint src, - ProgramPoint dest, - SemanticOracle oracle) - throws SemanticException { - return new ConstantPropWithIntervalLattice( - constantPropagation.smallStepSemantics(state.first, expression, dest, oracle), - intervals.smallStepSemantics(state.second, expression, dest, oracle)); - } - - @Override - public Satisfiability satisfies( - ConstantPropWithIntervalLattice state, - ValueExpression expression, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - Satisfiability constantPropSatisfiability = constantPropagation.satisfies(state.first, expression, pp, oracle); - Satisfiability intervalsSatisfiability = intervals.satisfies(state.second, expression, pp, oracle); - - if (constantPropSatisfiability.isTop() || constantPropSatisfiability.isBottom()) { - if (!intervalsSatisfiability.isBottom()) { - return intervalsSatisfiability; - } - } - return constantPropSatisfiability; - } - - @Override - public ConstantPropWithIntervalLattice makeLattice() { - return new ConstantPropWithIntervalLattice(constantPropagation.makeLattice(), intervals.makeLattice()); - } - - @Override - public ConstantPropWithIntervalLattice applyReplacement( - ConstantPropWithIntervalLattice state, - HeapDomain.HeapReplacement r, - ProgramPoint pp, - SemanticOracle oracle) - throws SemanticException { - return new ConstantPropWithIntervalLattice( - constantPropagation.applyReplacement(state.first, r, pp, oracle), - intervals.applyReplacement(state.second, r, pp, oracle)); - } - - @Override - public boolean equals( - Object o) { - if (o == null || getClass() != o.getClass()) - return false; - - ConstantPropWithInterval that = (ConstantPropWithInterval) o; - return constantPropagation.equals(that.constantPropagation) && intervals.equals(that.intervals); - } - - @Override - public int hashCode() { - int result = constantPropagation.hashCode(); - result = 31 * result + intervals.hashCode(); - return result; - } -} diff --git a/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithIntervalLattice.java b/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithIntervalLattice.java deleted file mode 100644 index 744fc036c..000000000 --- a/jlisa/src/main/java/it/unive/jlisa/analysis/ConstantPropWithIntervalLattice.java +++ /dev/null @@ -1,195 +0,0 @@ -package it.unive.jlisa.analysis; - -import it.unive.jlisa.lattices.ConstantValue; -import it.unive.lisa.analysis.Lattice; -import it.unive.lisa.analysis.ScopeToken; -import it.unive.lisa.analysis.SemanticException; -import it.unive.lisa.analysis.combination.ValueCartesianCombination; -import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; -import it.unive.lisa.program.cfg.ProgramPoint; -import it.unive.lisa.symbolic.value.Identifier; -import it.unive.lisa.util.numeric.IntInterval; -import it.unive.lisa.util.representation.MapRepresentation; -import it.unive.lisa.util.representation.StringRepresentation; -import it.unive.lisa.util.representation.StructuredRepresentation; -import java.util.Collection; -import java.util.HashMap; -import java.util.Map; -import java.util.function.Predicate; -import org.apache.commons.collections4.CollectionUtils; - -public class ConstantPropWithIntervalLattice - extends - ValueCartesianCombination, - ValueEnvironment> { - public static ConstantPropWithIntervalLattice TOP = new ConstantPropWithIntervalLattice(ConstantValue.TOP, - IntInterval.TOP); - public static ConstantPropWithIntervalLattice BOTTOM = new ConstantPropWithIntervalLattice(); - - private ConstantPropWithIntervalLattice() { - super( - new ValueEnvironment<>(ConstantValue.TOP), - new ValueEnvironment<>(IntInterval.TOP)); - } - - public ConstantPropWithIntervalLattice( - ValueEnvironment constantPropagation, - ValueEnvironment interval) { - - super(constantPropagation, interval); - } - - public ConstantPropWithIntervalLattice( - ConstantValue constantValue, - IntInterval interval) { - super( - new ValueEnvironment<>(constantValue), - new ValueEnvironment<>(interval)); - } - - @Override - public ConstantPropWithIntervalLattice pushScope( - ScopeToken token, - ProgramPoint pp) - throws SemanticException { - - return new ConstantPropWithIntervalLattice(first.pushScope(token, pp), second.pushScope(token, pp)); - } - - @Override - public ConstantPropWithIntervalLattice popScope( - ScopeToken token, - ProgramPoint pp) - throws SemanticException { - return new ConstantPropWithIntervalLattice(first.popScope(token, pp), second.popScope(token, pp)); - } - - @Override - public boolean knowsIdentifier( - Identifier id) { - return first.knowsIdentifier(id) || second.knowsIdentifier(id); - } - - @Override - public ConstantPropWithIntervalLattice forgetIdentifier( - Identifier id, - ProgramPoint pp) - throws SemanticException { - return new ConstantPropWithIntervalLattice(first.forgetIdentifier(id, pp), second.forgetIdentifier(id, pp)); - } - - @Override - public ConstantPropWithIntervalLattice forgetIdentifiers( - Iterable ids, - ProgramPoint pp) - throws SemanticException { - return new ConstantPropWithIntervalLattice(first.forgetIdentifiers(ids, pp), second.forgetIdentifiers(ids, pp)); - } - - @Override - public ConstantPropWithIntervalLattice forgetIdentifiersIf( - Predicate test, - ProgramPoint pp) - throws SemanticException { - return new ConstantPropWithIntervalLattice(first.forgetIdentifiersIf(test, pp), - second.forgetIdentifiersIf(test, pp)); - } - - @Override - public ConstantPropWithIntervalLattice mk( - ValueEnvironment constantPropagation, - ValueEnvironment interval) { - return new ConstantPropWithIntervalLattice(constantPropagation, interval); - } - - @Override - public ConstantPropWithIntervalLattice top() { - return TOP; - } - - @Override - public boolean isTop() { - return first.isTop() && second.isTop(); - } - - @Override - public ConstantPropWithIntervalLattice bottom() { - return BOTTOM; - } - - @Override - public boolean isBottom() { - return first.isBottom() && second.isBottom(); - } - - @Override - public boolean lessOrEqualAux( - ConstantPropWithIntervalLattice other) - throws SemanticException { - if (second.lessOrEqual(other.second)) { - return true; - } - if (first.lessOrEqual(other.first)) { - return true; - } - return false; - } - - @Override - public > Collection getAllLatticeInstances( - Class lattice) { - return super.getAllLatticeInstances(lattice); - } - - @Override - public ConstantPropWithIntervalLattice lubAux( - ConstantPropWithIntervalLattice other) - throws SemanticException { - return mk(first.lub(other.first), second.lub(other.second)); - } - - @Override - public ConstantPropWithIntervalLattice wideningAux( - ConstantPropWithIntervalLattice other) - throws SemanticException { - return mk(first.widening(other.first), second.widening(other.second)); - } - - @Override - public ConstantPropWithIntervalLattice glbAux( - ConstantPropWithIntervalLattice other) - throws SemanticException { - return mk(first.glb(other.first), second.glb(other.second)); - } - - @Override - public ConstantPropWithIntervalLattice narrowingAux( - ConstantPropWithIntervalLattice other) - throws SemanticException { - return mk(first.narrowing(other.first), second.narrowing(other.second)); - } - - @Override - public ConstantPropWithIntervalLattice store( - Identifier target, - Identifier source) - throws SemanticException { - return mk(first.store(target, source), second.store(target, source)); - } - - @Override - public StructuredRepresentation representation() { - if (isTop()) - return Lattice.topRepresentation(); - if (isBottom()) - return Lattice.bottomRepresentation(); - Map mapping = new HashMap<>(); - for (Identifier id : CollectionUtils.union(first.getKeys(), second.getKeys())) - mapping.put( - new StringRepresentation(id), - new StringRepresentation( - first.getState(id).toString() + ", " + second.getState(id).representation())); - return new MapRepresentation(mapping); - } - -} \ No newline at end of file From 021d7a6bfd1ca6f046154ba5848adb997fac86ca Mon Sep 17 00:00:00 2001 From: Giacomo Zanatta Date: Fri, 31 Oct 2025 21:26:04 +0100 Subject: [PATCH 6/9] Add ConstantPropagationWithIntervals domain --- .../ConstantPropagationWithIntervals.java | 459 ++++++++++++++++++ 1 file changed, 459 insertions(+) create mode 100644 jlisa/src/main/java/it/unive/jlisa/analysis/value/ConstantPropagationWithIntervals.java diff --git a/jlisa/src/main/java/it/unive/jlisa/analysis/value/ConstantPropagationWithIntervals.java b/jlisa/src/main/java/it/unive/jlisa/analysis/value/ConstantPropagationWithIntervals.java new file mode 100644 index 000000000..80af56c45 --- /dev/null +++ b/jlisa/src/main/java/it/unive/jlisa/analysis/value/ConstantPropagationWithIntervals.java @@ -0,0 +1,459 @@ +package it.unive.jlisa.analysis.value; + +import it.unive.jlisa.lattices.ConstantValue; +import it.unive.jlisa.lattices.ConstantValueIntInterval; +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.analysis.numeric.Interval; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.symbolic.SymbolicExpression; +import it.unive.lisa.symbolic.value.BinaryExpression; +import it.unive.lisa.symbolic.value.Constant; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.PushAny; +import it.unive.lisa.symbolic.value.PushInv; +import it.unive.lisa.symbolic.value.Skip; +import it.unive.lisa.symbolic.value.TernaryExpression; +import it.unive.lisa.symbolic.value.UnaryExpression; +import it.unive.lisa.symbolic.value.ValueExpression; +import it.unive.lisa.util.numeric.IntInterval; +import java.util.Arrays; +import java.util.HashSet; +import java.util.Set; +import org.apache.commons.lang3.tuple.Pair; + +public class ConstantPropagationWithIntervals implements BaseNonRelationalValueDomain { + + private final ConstantPropagation constantPropagation = new ConstantPropagation(); + private final Interval interval = new Interval(); + + @Override + public ConstantValueIntInterval top() { + return ConstantValueIntInterval.TOP; + } + + @Override + public ConstantValueIntInterval bottom() { + return ConstantValueIntInterval.BOTTOM; + } + + @Override + public boolean canProcess( + SymbolicExpression expression, + ProgramPoint pp, + SemanticOracle oracle) { + return constantPropagation.canProcess(expression, pp, oracle) || interval.canProcess(expression, pp, oracle); + } + + @Override + public ConstantValueIntInterval evalNullConstant( + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantValueIntInterval( + constantPropagation.evalNullConstant(pp, oracle), + interval.evalNullConstant(pp, oracle)); + } + + @Override + public ConstantValueIntInterval evalNonNullConstant( + Constant constant, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantValueIntInterval( + constantPropagation.evalNonNullConstant(constant, pp, oracle), + interval.evalNonNullConstant(constant, pp, oracle)); + } + + @Override + public ConstantValueIntInterval evalUnaryExpression( + UnaryExpression expression, + ConstantValueIntInterval arg, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantValueIntInterval( + constantPropagation.evalUnaryExpression(expression, arg.getConstantValue(), pp, oracle), + interval.evalUnaryExpression(expression, arg.getIntInterval(), pp, oracle)); + } + + @Override + public ConstantValueIntInterval evalBinaryExpression( + BinaryExpression expression, + ConstantValueIntInterval left, + ConstantValueIntInterval right, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantValueIntInterval( + constantPropagation.evalBinaryExpression(expression, left.getConstantValue(), right.getConstantValue(), + pp, oracle), + interval.evalBinaryExpression(expression, left.getIntInterval(), right.getIntInterval(), pp, oracle)); + } + + @Override + public ConstantValueIntInterval evalTernaryExpression( + TernaryExpression expression, + ConstantValueIntInterval left, + ConstantValueIntInterval middle, + ConstantValueIntInterval right, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantValueIntInterval( + constantPropagation.evalTernaryExpression(expression, left.getConstantValue(), + middle.getConstantValue(), right.getConstantValue(), pp, oracle), + interval.evalTernaryExpression(expression, left.getIntInterval(), middle.getIntInterval(), + right.getIntInterval(), pp, oracle)); + } + + @Override + public ConstantValueIntInterval evalValueExpression( + ValueExpression expression, + ConstantValueIntInterval[] subExpressions, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + ConstantValue[] constantValues = Arrays.stream(subExpressions) + .map(ConstantValueIntInterval::getConstantValue) + .toArray(ConstantValue[]::new); + + IntInterval[] intIntervals = Arrays.stream(subExpressions) + .map(ConstantValueIntInterval::getIntInterval) + .toArray(IntInterval[]::new); + + return new ConstantValueIntInterval( + constantPropagation.evalValueExpression(expression, constantValues, pp, oracle), + interval.evalValueExpression(expression, intIntervals, pp, oracle)); + } + + @Override + public ConstantValueIntInterval evalPushAny( + PushAny pushAny, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantValueIntInterval( + constantPropagation.evalPushAny(pushAny, pp, oracle), + interval.evalPushAny(pushAny, pp, oracle)); + } + + @Override + public ConstantValueIntInterval evalPushInv( + PushInv pushInv, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantValueIntInterval( + constantPropagation.evalPushInv(pushInv, pp, oracle), + interval.evalPushInv(pushInv, pp, oracle)); + } + + @Override + public ConstantValueIntInterval evalSkip( + Skip skip, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantValueIntInterval( + constantPropagation.evalSkip(skip, pp, oracle), + interval.evalSkip(skip, pp, oracle)); + } + + @Override + public ConstantValueIntInterval evalTypeCast( + BinaryExpression cast, + ConstantValueIntInterval left, + ConstantValueIntInterval right, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantValueIntInterval( + constantPropagation.evalTypeCast(cast, left.getConstantValue(), right.getConstantValue(), pp, oracle), + interval.evalTypeCast(cast, left.getIntInterval(), right.getIntInterval(), pp, oracle)); + } + + @Override + public ConstantValueIntInterval evalTypeConv( + BinaryExpression conv, + ConstantValueIntInterval left, + ConstantValueIntInterval right, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + return new ConstantValueIntInterval( + constantPropagation.evalTypeConv(conv, left.getConstantValue(), right.getConstantValue(), pp, oracle), + interval.evalTypeConv(conv, left.getIntInterval(), right.getIntInterval(), pp, oracle)); + } + + @Override + public Satisfiability satisfiesAbstractValue( + ConstantValueIntInterval value, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + Satisfiability constantPropSatisfiability = constantPropagation.satisfiesAbstractValue(value.getConstantValue(), + pp, oracle); + if (constantPropSatisfiability == Satisfiability.UNKNOWN + || constantPropSatisfiability == Satisfiability.BOTTOM) { + Satisfiability intervalSatisfiability = interval.satisfiesAbstractValue(value.getIntInterval(), pp, oracle); + if (intervalSatisfiability == Satisfiability.SATISFIED) { + return Satisfiability.SATISFIED; + } + } + return constantPropSatisfiability; + } + + @Override + public Satisfiability satisfiesNullConstant( + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + Satisfiability constantPropSatisfiability = constantPropagation.satisfiesNullConstant(pp, oracle); + if (constantPropSatisfiability == Satisfiability.UNKNOWN + || constantPropSatisfiability == Satisfiability.BOTTOM) { + Satisfiability intervalSatisfiability = interval.satisfiesNullConstant(pp, oracle); + if (intervalSatisfiability == Satisfiability.SATISFIED) { + return Satisfiability.SATISFIED; + } + } + return constantPropSatisfiability; + } + + @Override + public Satisfiability satisfiesNonNullConstant( + Constant constant, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + Satisfiability constantPropSatisfiability = constantPropagation.satisfiesNonNullConstant(constant, pp, oracle); + if (constantPropSatisfiability == Satisfiability.UNKNOWN + || constantPropSatisfiability == Satisfiability.BOTTOM) { + Satisfiability intervalSatisfiability = interval.satisfiesNonNullConstant(constant, pp, oracle); + if (intervalSatisfiability == Satisfiability.SATISFIED) { + return Satisfiability.SATISFIED; + } + } + return constantPropSatisfiability; + } + + @Override + public Satisfiability satisfiesUnaryExpression( + UnaryExpression expression, + ConstantValueIntInterval arg, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + Satisfiability constantPropSatisfiability = constantPropagation.satisfiesUnaryExpression(expression, + arg.getConstantValue(), pp, oracle); + if (constantPropSatisfiability == Satisfiability.UNKNOWN + || constantPropSatisfiability == Satisfiability.BOTTOM) { + Satisfiability intervalSatisfiability = interval.satisfiesUnaryExpression(expression, arg.getIntInterval(), + pp, oracle); + if (intervalSatisfiability == Satisfiability.SATISFIED) { + return Satisfiability.SATISFIED; + } + } + return constantPropSatisfiability; + } + + @Override + public Satisfiability satisfiesBinaryExpression( + BinaryExpression expression, + ConstantValueIntInterval left, + ConstantValueIntInterval right, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + Satisfiability constantPropSatisfiability = constantPropagation.satisfiesBinaryExpression(expression, + left.getConstantValue(), right.getConstantValue(), pp, oracle); + if (constantPropSatisfiability == Satisfiability.UNKNOWN + || constantPropSatisfiability == Satisfiability.BOTTOM) { + Satisfiability intervalSatisfiability = interval.satisfiesBinaryExpression(expression, + left.getIntInterval(), right.getIntInterval(), pp, oracle); + if (intervalSatisfiability == Satisfiability.SATISFIED) { + return Satisfiability.SATISFIED; + } + } + return constantPropSatisfiability; + } + + @Override + public Satisfiability satisfiesTernaryExpression( + TernaryExpression expression, + ConstantValueIntInterval left, + ConstantValueIntInterval middle, + ConstantValueIntInterval right, + ProgramPoint pp, + SemanticOracle oracle) + throws SemanticException { + Satisfiability constantPropSatisfiability = constantPropagation.satisfiesTernaryExpression(expression, + left.getConstantValue(), middle.getConstantValue(), right.getConstantValue(), pp, oracle); + if (constantPropSatisfiability == Satisfiability.UNKNOWN + || constantPropSatisfiability == Satisfiability.BOTTOM) { + Satisfiability intervalSatisfiability = interval.satisfiesTernaryExpression(expression, + left.getIntInterval(), middle.getIntInterval(), right.getIntInterval(), pp, oracle); + if (intervalSatisfiability == Satisfiability.SATISFIED) { + return Satisfiability.SATISFIED; + } + } + return constantPropSatisfiability; + } + + @Override + public ValueEnvironment assumeConstant( + ValueEnvironment environment, + Constant expression, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + Pair, + ValueEnvironment> environments = splitEnvironment(environment); + ValueEnvironment constantValueEnvironment = constantPropagation + .assumeConstant(environments.getLeft(), expression, src, dest, oracle); + ValueEnvironment intIntervalEnvironment = interval.assumeConstant(environments.getRight(), + expression, src, dest, oracle); + return mergeEnvironments(constantValueEnvironment, intIntervalEnvironment); + } + + @Override + public ValueEnvironment assumeIdentifier( + ValueEnvironment environment, + Identifier expression, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + Pair, + ValueEnvironment> environments = splitEnvironment(environment); + ValueEnvironment constantValueEnvironment = constantPropagation + .assumeIdentifier(environments.getLeft(), expression, src, dest, oracle); + ValueEnvironment intIntervalEnvironment = interval.assumeIdentifier(environments.getRight(), + expression, src, dest, oracle); + return mergeEnvironments(constantValueEnvironment, intIntervalEnvironment); + } + + @Override + public ValueEnvironment assumeUnaryExpression( + ValueEnvironment environment, + UnaryExpression expression, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + Pair, + ValueEnvironment> environments = splitEnvironment(environment); + ValueEnvironment constantValueEnvironment = constantPropagation + .assumeUnaryExpression(environments.getLeft(), expression, src, dest, oracle); + ValueEnvironment intIntervalEnvironment = interval.assumeUnaryExpression(environments.getRight(), + expression, src, dest, oracle); + return mergeEnvironments(constantValueEnvironment, intIntervalEnvironment); + } + + @Override + public ValueEnvironment assumeBinaryExpression( + ValueEnvironment environment, + BinaryExpression expression, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + Pair, + ValueEnvironment> environments = splitEnvironment(environment); + ValueEnvironment constantValueEnvironment = constantPropagation + .assumeBinaryExpression(environments.getLeft(), expression, src, dest, oracle); + ValueEnvironment intIntervalEnvironment = interval.assumeBinaryExpression(environments.getRight(), + expression, src, dest, oracle); + return mergeEnvironments(constantValueEnvironment, intIntervalEnvironment); + } + + @Override + public ValueEnvironment assumeTernaryExpression( + ValueEnvironment environment, + TernaryExpression expression, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + Pair, + ValueEnvironment> environments = splitEnvironment(environment); + ValueEnvironment constantValueEnvironment = constantPropagation + .assumeTernaryExpression(environments.getLeft(), expression, src, dest, oracle); + ValueEnvironment intIntervalEnvironment = interval.assumeTernaryExpression(environments.getRight(), + expression, src, dest, oracle); + return mergeEnvironments(constantValueEnvironment, intIntervalEnvironment); + } + + @Override + public ValueEnvironment assumeValueExpression( + ValueEnvironment environment, + ValueExpression expression, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + Pair, + ValueEnvironment> environments = splitEnvironment(environment); + ValueEnvironment constantValueEnvironment = constantPropagation + .assumeValueExpression(environments.getLeft(), expression, src, dest, oracle); + ValueEnvironment intIntervalEnvironment = interval.assumeValueExpression(environments.getRight(), + expression, src, dest, oracle); + return mergeEnvironments(constantValueEnvironment, intIntervalEnvironment); + } + + public static Pair, ValueEnvironment> + + splitEnvironment( + ValueEnvironment environment) + throws SemanticException { + + ValueEnvironment constantValueEnvironment = new ValueEnvironment<>(ConstantValue.BOTTOM); + ValueEnvironment intIntervalValueEnvironment = new ValueEnvironment<>(IntInterval.BOTTOM); + + for (Identifier id : environment.getKeys()) { + ConstantValueIntInterval value = environment.getState(id); + if (value == null) + continue; + + ConstantValue constant = value.getConstantValue(); + IntInterval interval = value.getIntInterval(); + + constantValueEnvironment = constantValueEnvironment.putState(id, constant); + intIntervalValueEnvironment = intIntervalValueEnvironment.putState(id, interval); + } + + return Pair.of(constantValueEnvironment, intIntervalValueEnvironment); + } + + public static ValueEnvironment mergeEnvironments( + ValueEnvironment constantEnv, + ValueEnvironment intervalEnv) + throws SemanticException { + + ValueEnvironment merged = new ValueEnvironment<>(ConstantValueIntInterval.BOTTOM); + + Set allIds = new HashSet<>(); + allIds.addAll(constantEnv.getKeys()); + allIds.addAll(intervalEnv.getKeys()); + + for (Identifier id : allIds) { + ConstantValue constVal = constantEnv.getState(id); + IntInterval intVal = intervalEnv.getState(id); + if (constVal == null) + constVal = ConstantValue.BOTTOM; + if (intVal == null) + intVal = IntInterval.BOTTOM; + + ConstantValueIntInterval combined = new ConstantValueIntInterval(constVal, intVal); + merged = merged.putState(id, combined); + } + + return merged; + } + +} \ No newline at end of file From 10eb8a5b47518bfcf3e5750b7c80826ab6cb193d Mon Sep 17 00:00:00 2001 From: Giacomo Zanatta Date: Fri, 31 Oct 2025 22:14:37 +0100 Subject: [PATCH 7/9] Add AssertCheckerConstantPropagationWithIntervals --- ...eckerConstantPropagationWithIntervals.java | 218 ++++++++++++++++++ 1 file changed, 218 insertions(+) create mode 100644 jlisa/src/main/java/it/unive/jlisa/checkers/AssertCheckerConstantPropagationWithIntervals.java diff --git a/jlisa/src/main/java/it/unive/jlisa/checkers/AssertCheckerConstantPropagationWithIntervals.java b/jlisa/src/main/java/it/unive/jlisa/checkers/AssertCheckerConstantPropagationWithIntervals.java new file mode 100644 index 000000000..20d7d73b6 --- /dev/null +++ b/jlisa/src/main/java/it/unive/jlisa/checkers/AssertCheckerConstantPropagationWithIntervals.java @@ -0,0 +1,218 @@ +package it.unive.jlisa.checkers; + +import it.unive.jlisa.lattices.ConstantValueIntInterval; +import it.unive.jlisa.lattices.ReachLattice; +import it.unive.jlisa.lattices.ReachLattice.ReachabilityStatus; +import it.unive.jlisa.program.cfg.statement.asserts.AssertStatement; +import it.unive.jlisa.program.cfg.statement.asserts.AssertionStatement; +import it.unive.jlisa.program.cfg.statement.asserts.SimpleAssert; +import it.unive.lisa.analysis.AnalysisState; +import it.unive.lisa.analysis.SemanticException; +import it.unive.lisa.analysis.SimpleAbstractDomain; +import it.unive.lisa.analysis.combination.ValueLatticeProduct; +import it.unive.lisa.analysis.lattices.Satisfiability; +import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment; +import it.unive.lisa.analysis.nonrelational.type.TypeEnvironment; +import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment; +import it.unive.lisa.checks.semantic.CheckToolWithAnalysisResults; +import it.unive.lisa.checks.semantic.SemanticCheck; +import it.unive.lisa.lattices.SimpleAbstractState; +import it.unive.lisa.lattices.heap.allocations.AllocationSites; +import it.unive.lisa.lattices.types.TypeSet; +import it.unive.lisa.program.cfg.CFG; +import it.unive.lisa.program.cfg.ProgramPoint; +import it.unive.lisa.program.cfg.statement.Expression; +import it.unive.lisa.program.cfg.statement.Ret; +import it.unive.lisa.program.cfg.statement.Statement; +import it.unive.lisa.symbolic.SymbolicExpression; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; + +/** + * Assert Checker It checks whether an assertion's condition holds. + * + * @author Luca Olivieri + */ +public class AssertCheckerConstantPropagationWithIntervals + implements + SemanticCheck< + SimpleAbstractState< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment>, + SimpleAbstractDomain< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment>> { + + private static final Logger LOG = LogManager.getLogger(AssertChecker.class); + + @Override + public boolean visit( + CheckToolWithAnalysisResults< + SimpleAbstractState< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment>, + SimpleAbstractDomain< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment>> tool, + CFG graph, + Statement node) { + + // RuntimeException property checker + if (graph.getProgram().getEntryPoints().contains(graph) && node instanceof Ret) + try { + checkRuntimeException(tool, graph, node); + } catch (SemanticException e) { + e.printStackTrace(); + } + + // assert checker + if (node instanceof AssertStatement) + try { + checkAssert(tool, graph, (AssertStatement) node); + } catch (SemanticException e) { + e.printStackTrace(); + } + + return true; + } + + private void checkRuntimeException( + CheckToolWithAnalysisResults< + SimpleAbstractState< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment>, + SimpleAbstractDomain< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment>> tool, + CFG graph, + Statement node) + throws SemanticException { + + for (var result : tool.getResultOf(graph)) { + AnalysisState< + SimpleAbstractState< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment>> state = result.getAnalysisStateAfter(node); + + // checking if there exists at least one exception state + boolean hasExceptionState = !state.getErrors().isBottom() && + !state.getErrors().isTop() && + !state.getErrors().function.isEmpty() || + (!state.getSmashedErrors().isBottom() && + !state.getSmashedErrors().isTop() && + !state.getSmashedErrors().function.isEmpty()); + + SimpleAbstractState< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment> normaleState = state.getExecutionState(); + + // if exceptions had been thrown, we raise a warning + if (hasExceptionState) + // if the normal state is bottom, we raise a definite error + if (normaleState.isBottom()) + tool.warnOn((Statement) node, "DEFINITE: uncaught runtime exception in main method"); + // otherwise, we raise a possible error (both normal and + // exception states are not bottom) + else + tool.warnOn((Statement) node, "POSSIBLE: uncaught runtime exception in main method"); + } + } + + private void checkAssert( + CheckToolWithAnalysisResults< + SimpleAbstractState< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment>, + SimpleAbstractDomain< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment>> tool, + CFG graph, + AssertStatement node) + throws SemanticException { + for (var result : tool.getResultOf(graph)) { + AnalysisState< + SimpleAbstractState< + HeapEnvironment, + ValueLatticeProduct>, + TypeEnvironment>> state = null; + + boolean isAssertFalse = false; + if (node instanceof SimpleAssert) { + Expression expr = ((SimpleAssert) node).getSubExpression(); + state = result.getAnalysisStateAfter(expr); + isAssertFalse = expr.toString().equals("false"); + } else if (node instanceof AssertionStatement) { + Expression expr = ((AssertionStatement) node).getLeft(); + state = result.getAnalysisStateAfter(expr); + isAssertFalse = expr.toString().equals("false"); + } + + ValueLatticeProduct> valueState = state.getExecutionState().valueState; + ReachabilityStatus reach = valueState.first.lattice; + ValueEnvironment values = valueState.second; + + if (reach == ReachabilityStatus.UNREACHABLE) { + // if the assertion is not reachable, it won't fail + tool.warnOn((Statement) node, "DEFINITE: the assertion holds"); + continue; + } + + if (isAssertFalse) { + // we do not need to query the satisfiability of of the + // expression: + // we rely on reachability to determine its status + if (reach == ReachabilityStatus.REACHABLE) + tool.warnOn((Statement) node, "DEFINITE: the assertion DOES NOT hold"); + else if (reach == ReachabilityStatus.POSSIBLY_REACHABLE) + tool.warnOn((Statement) node, "POSSIBLE: the assertion MAY (NOT) BE hold"); + continue; + } + + if (values.isBottom()) { + // the statement is (possibly) reachable, is not an assert + // false, + // but we have a bottom value state + // we cannot do much other than being conservative and + // say that the assertion might not hold + tool.warnOn((Statement) node, "POSSIBLE: the assertion MAY (NOT) BE hold"); + LOG.error("The abstract state of assert's expression is BOTTOM"); + continue; + } + + if (values.isTop()) { + // the statement is (possibly) reachable, is not an assert + // false, + // but we have a top value state + // we cannot do much other than being conservative and + // say that the assertion might not hold + tool.warnOn((Statement) node, "POSSIBLE: the assertion MAY (NOT) BE hold"); + continue; + } + + Satisfiability overall = Satisfiability.BOTTOM; + for (SymbolicExpression expr : state.getExecutionExpressions()) + overall = overall.lub(tool.getAnalysis().satisfies(state, expr, (ProgramPoint) node)); + + if (overall == Satisfiability.SATISFIED) + tool.warnOn((Statement) node, "DEFINITE: the assertion holds"); + else if (overall == Satisfiability.NOT_SATISFIED) { + if (reach == ReachLattice.ReachabilityStatus.REACHABLE) + tool.warnOn((Statement) node, "DEFINITE: the assertion DOES NOT hold"); + else if (reach == ReachLattice.ReachabilityStatus.POSSIBLY_REACHABLE) + tool.warnOn((Statement) node, "POSSIBLE: the assertion MAY (NOT) BE hold"); + } else + tool.warnOn((Statement) node, "POSSIBLE: the assertion MAY (NOT) BE hold"); + } + } +} From 02ae8f835698ad1347d42c0d6dc0b795d2c1ffbb Mon Sep 17 00:00:00 2001 From: Giacomo Zanatta Date: Fri, 31 Oct 2025 22:15:09 +0100 Subject: [PATCH 8/9] Override assume method in ConstantPropagationWithIntervals --- .../value/ConstantPropagationWithIntervals.java | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/jlisa/src/main/java/it/unive/jlisa/analysis/value/ConstantPropagationWithIntervals.java b/jlisa/src/main/java/it/unive/jlisa/analysis/value/ConstantPropagationWithIntervals.java index 80af56c45..c8f0d93c2 100644 --- a/jlisa/src/main/java/it/unive/jlisa/analysis/value/ConstantPropagationWithIntervals.java +++ b/jlisa/src/main/java/it/unive/jlisa/analysis/value/ConstantPropagationWithIntervals.java @@ -304,6 +304,22 @@ public Satisfiability satisfiesTernaryExpression( return constantPropSatisfiability; } + + @Override + public ValueEnvironment assume( + ValueEnvironment environment, + ValueExpression expression, + ProgramPoint src, + ProgramPoint dest, + SemanticOracle oracle) + throws SemanticException { + Satisfiability sat = satisfies(environment, expression, src, oracle); + if (sat == Satisfiability.NOT_SATISFIED) + return environment.bottom(); + if (sat == Satisfiability.SATISFIED) + return environment; + return BaseNonRelationalValueDomain.super.assume(environment, expression, src, dest, oracle); + } @Override public ValueEnvironment assumeConstant( ValueEnvironment environment, From 62836643a33b2fd44227bde73eb7b8a7f9460f55 Mon Sep 17 00:00:00 2001 From: Giacomo Zanatta Date: Fri, 31 Oct 2025 22:19:57 +0100 Subject: [PATCH 9/9] Rebase main with master --- jlisa/src/main/java/it/unive/jlisa/Main.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/jlisa/src/main/java/it/unive/jlisa/Main.java b/jlisa/src/main/java/it/unive/jlisa/Main.java index 12715cae8..b4174c9d5 100644 --- a/jlisa/src/main/java/it/unive/jlisa/Main.java +++ b/jlisa/src/main/java/it/unive/jlisa/Main.java @@ -1,6 +1,5 @@ package it.unive.jlisa; -import it.unive.jlisa.analysis.ConstantPropWithInterval; import it.unive.jlisa.analysis.heap.JavaFieldSensitivePointBasedHeap; import it.unive.jlisa.analysis.type.JavaInferredTypes; import it.unive.jlisa.analysis.value.ConstantPropagation; @@ -283,7 +282,7 @@ private static void runAnalysis( */ conf.analysis = new SimpleAbstractDomain<>( new JavaFieldSensitivePointBasedHeap(), - new ConstantPropWithInterval(), + domain, new JavaInferredTypes()); LiSA lisa = new LiSA(conf);