diff --git a/jlisa/src/main/java/it/unive/jlisa/Main.java b/jlisa/src/main/java/it/unive/jlisa/Main.java index 7a59a8d19..b4174c9d5 100644 --- a/jlisa/src/main/java/it/unive/jlisa/Main.java +++ b/jlisa/src/main/java/it/unive/jlisa/Main.java @@ -275,6 +275,11 @@ private static void runAnalysis( throw new ParseException("Invalid numerical domain name: " + numericalDomain); } + /* + * conf.analysis = DefaultConfiguration.simpleState( + * DefaultConfiguration.defaultHeapDomain(), new Pentagon(), + * DefaultConfiguration.defaultTypeDomain()); + */ conf.analysis = new SimpleAbstractDomain<>( new JavaFieldSensitivePointBasedHeap(), domain, 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..c8f0d93c2 --- /dev/null +++ b/jlisa/src/main/java/it/unive/jlisa/analysis/value/ConstantPropagationWithIntervals.java @@ -0,0 +1,475 @@ +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 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, + 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 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"); + } + } + } + } +} 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"); + } + } +} 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())); + } + +}