Fix null-pointer error and flatten arithmetic expressions

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
   }
+
 }

src/main/gov/nasa/jpf/jdart/solvers/bounded/BoundedSolverContext.java

@@ -50,6 +50,10 @@ public Result solve(Valuation vltn) {
   @Override
   public void add(List<Expression<Boolean>> list) {
     for (Expression<Boolean> e : list) {
+      FlattenArithmeticVisitor fav = new FlattenArithmeticVisitor();
+      //System.out.println("Old Expression: " + e);
+      e = (Expression<Boolean>) 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);
     }

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);

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<Void> {
+
+  @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<Integer>) 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 <E> Expression<?> defaultVisit(Expression<E> 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;
+  }
+
+}