From 4a9cc434e636bdc8e5ca7f661519c31394c25d36 Mon Sep 17 00:00:00 2001 From: Malte Mues Date: Mon, 30 Nov 2020 12:25:28 +0100 Subject: [PATCH] Fix null-pointer error and flatten arithmetic expressions --- .../jdart/solvers/bounded/BoundedSolver.java | 5 +- .../solvers/bounded/BoundedSolverContext.java | 6 +- .../bounded/BoundedSolverProvider.java | 3 +- .../bounded/FlattenArithmeticVisitor.java | 77 +++++++++++++++++++ 4 files changed, 87 insertions(+), 4 deletions(-) create mode 100644 src/main/gov/nasa/jpf/jdart/solvers/bounded/FlattenArithmeticVisitor.java diff --git a/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolver.java b/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolver.java index 66b087b..8771f49 100644 --- a/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolver.java +++ b/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolver.java @@ -25,7 +25,7 @@ public class BoundedSolver extends ConstraintSolver { private final int fibonacci[] = { 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181, 6765 }; - private final int skipped[] = {2, 8, 13}; + private final int skipped[] = {2, 8, 13, 21, 200, 600}; BoundType type; public BoundedSolver(ConstraintSolver back, int bound, int itr, BoundType type) { @@ -84,7 +84,7 @@ private static boolean hasStrLenExpr(Expression e) { } if (e.getChildren() != null) { for (Expression child : e.getChildren()) { - if (hasStrLenExpr(child)) { + if (child != null && hasStrLenExpr(child)) { return true; } } @@ -128,4 +128,5 @@ public enum BoundType { fibonacci, skipped } + } diff --git a/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolverContext.java b/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolverContext.java index 2e2102b..032451f 100644 --- a/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolverContext.java +++ b/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolverContext.java @@ -50,6 +50,10 @@ public Result solve(Valuation vltn) { @Override public void add(List> list) { for (Expression e : list) { + FlattenArithmeticVisitor fav = new FlattenArithmeticVisitor(); + //System.out.println("Old Expression: " + e); + e = (Expression) e.accept(fav, null); + //System.out.println("Flattened: " + e); ctx.add(e); current.exprsn.add(e); } @@ -90,7 +94,7 @@ private Result solveWithBound(Valuation vals) { add(solver.getBoundAnalysisLimit(all)); res = ctx.solve(vals); // FIXME: This should be logger.finer - //System.out.println("Result: " + res); + //System.out.println("Result: " + res + " " + vals); if (res.equals(Result.SAT)) { assert (Boolean) all.evaluate(vals); } diff --git a/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolverProvider.java b/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolverProvider.java index eb69130..8331890 100644 --- a/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolverProvider.java +++ b/src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolverProvider.java @@ -3,6 +3,7 @@ import gov.nasa.jpf.constraints.api.ConstraintSolver; import gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory; import gov.nasa.jpf.constraints.solvers.ConstraintSolverProvider; +import gov.nasa.jpf.jdart.solvers.bounded.BoundedSolver.BoundType; import java.util.Properties; public class BoundedSolverProvider implements ConstraintSolverProvider { @@ -36,7 +37,7 @@ public ConstraintSolver createSolver(Properties config) { } if (config.containsKey("bounded.type") && config.getProperty("bounded.type") .equals("skipped")) { - type = BoundedSolver.BoundType.fibonacci; + type = BoundType.skipped; } ConstraintSolver solver = ConstraintSolverFactory.getRootFactory().createSolver(dp, config); diff --git a/src/main/gov/nasa/jpf/jdart/solvers/bounded/FlattenArithmeticVisitor.java b/src/main/gov/nasa/jpf/jdart/solvers/bounded/FlattenArithmeticVisitor.java new file mode 100644 index 0000000..ed4a165 --- /dev/null +++ b/src/main/gov/nasa/jpf/jdart/solvers/bounded/FlattenArithmeticVisitor.java @@ -0,0 +1,77 @@ +package gov.nasa.jpf.jdart.solvers.bounded; + +import gov.nasa.jpf.constraints.api.Expression; +import gov.nasa.jpf.constraints.api.Variable; +import gov.nasa.jpf.constraints.expressions.Constant; +import gov.nasa.jpf.constraints.expressions.NumericCompound; +import gov.nasa.jpf.constraints.expressions.NumericOperator; +import gov.nasa.jpf.constraints.types.BuiltinTypes; +import gov.nasa.jpf.constraints.util.DuplicatingVisitor; + +public class FlattenArithmeticVisitor extends DuplicatingVisitor { + + @Override + public Expression visit(NumericCompound n, Void data) { + Expression left = visit(n.getLeft(), data); + Expression right = visit(n.getRight(), data); + try { + if (left instanceof NumericCompound + && right instanceof Constant + && left.getType().equals(BuiltinTypes.SINT32)) { + NumericCompound leftChild = (NumericCompound) left; + if (leftChild.getLeft() instanceof Variable && leftChild.getRight() instanceof Constant) { + Variable v = (Variable) leftChild.getLeft(); + Constant c = (Constant) leftChild.getRight(); + int cNew = apply(0, (int) c.getValue(), leftChild.getOperator()); + cNew = apply(cNew, ((Constant) right).getValue(), n.getOperator()); + Constant newC = Constant.create(BuiltinTypes.SINT32, Math.abs(cNew)); + if(cNew > 0){ + return NumericCompound.create(v, NumericOperator.PLUS, newC); + }else if(cNew < 0){ + return NumericCompound.create(v, NumericOperator.MINUS, newC); + }else{ + return v; + } + } + } + } catch (IllegalArgumentException e) { + } + return n; + } + + public int apply(int newRes, int constant, NumericOperator cmp) { + if (cmp.equals(NumericOperator.PLUS)) { + return newRes + constant; + } else if (cmp.equals(NumericOperator.MINUS)) { + return newRes - constant; + } + throw new IllegalArgumentException("Cannot be applied for Operator: " + cmp); + } + + protected Expression defaultVisit(Expression expression, Void data) { + Expression[] children = expression.getChildren(); + if(children != null){ + boolean changed = false; + + for(int i = 0; i < children.length; ++i) { + Expression c = children[i]; + if (c != null) { + Expression r = (Expression) this.visit(c, data); + if (c != r) { + changed = true; + } + + children[i] = r; + } + } + + if (!changed) { + return expression; + } else { + return expression.duplicate(children); + } + } + return expression; + } + +}