Symbolic objects

src/main/java/tools/aqua/dse/Config.java

@@ -22,16 +22,17 @@
 import gov.nasa.jpf.constraints.solvers.SolvingService;
 import org.apache.commons.cli.CommandLine;
 import tools.aqua.dse.bounds.BoundedSolverProvider;
+import tools.aqua.dse.objects.Objects;
 
-import java.io.FileInputStream;
-import java.io.IOException;
+import java.io.*;
 import java.net.MalformedURLException;
 import java.net.URL;
 import java.net.URLClassLoader;
 import java.nio.file.Paths;
 import java.util.Iterator;
 import java.util.Map;
 import java.util.Properties;
+import java.util.Random;
 
 public class Config {
 
@@ -72,13 +73,19 @@ public static ExplorationStrategy fromString(String property) {
 
     private boolean witness = false;
 
+    private Random random = null;
+
+    private double fraction = 1.0;
+
     private ClassLoader sourceLoader = Config.class.getClassLoader();
 
     // TODO: make this configurable
     private int termination = TERMINATE_WHEN_COMPLETE;
 
     private final Properties properties;
 
+    private Objects objects = null;
+
     private Config(Properties properties) {
         this.properties = properties;
     }
@@ -115,7 +122,12 @@ public boolean isIncremental() {
      * @return
      */
     public SolverContext getSolverContext() {
-        return this.solver.createContext();
+        SolverContext ctx = this.solver.createContext();
+        // init object constraints signature
+        if (objects != null) {
+            objects.initObjectsStructure(ctx);
+        }
+        return ctx;
     }
 
     /**
@@ -159,6 +171,15 @@ public int getTermination() {
 
     public boolean isWitness() { return witness; }
 
+
+    public double getFraction() {
+        return fraction;
+    }
+
+    public Random getRandom() {
+        return random;
+    }
+
     private void parseProperties(Properties props) {
         if (props.containsKey("dse.executor.args")) {
             this.executorArgs = props.getProperty("dse.executor.args");
@@ -210,6 +231,32 @@ private void parseProperties(Properties props) {
 
             sourceLoader = new URLClassLoader(urls);
         }
+        if (props.containsKey("iflow.fraction")) {
+            this.fraction = Double.parseDouble(props.getProperty("iflow.fraction"));
+        }
+
+        if (props.containsKey("static.info")) {
+            String filename = props.getProperty("static.info");
+            StringBuilder sb = new StringBuilder();
+            try (BufferedReader r = new BufferedReader(new FileReader(filename))) {
+                String line = null;
+                while ((line = r.readLine()) != null) {
+                    sb.append(line);
+                }
+            } catch (FileNotFoundException e) {
+                throw new RuntimeException(e);
+            } catch (IOException e) {
+                throw new RuntimeException(e);
+            }
+            this.objects = new Objects(sb.toString());
+        }
+
+        long seed = (new Random()).nextLong();
+        if (props.containsKey("random.seed")) {
+            seed = Long.parseLong(props.getProperty("random.seed"));
+        }
+        System.out.println("Random seed: " + seed);
+        this.random = new Random(seed);
     }
 
     private int parseTermination(String property) {

src/main/java/tools/aqua/dse/DSE.java

@@ -29,9 +29,7 @@
 import java.io.*;
 import java.nio.file.Files;
 import java.nio.file.Paths;
-import java.util.ArrayList;
-import java.util.LinkedList;
-import java.util.List;
+import java.util.*;
 
 public class DSE {
 
@@ -47,14 +45,14 @@ public void executeAnalysis() {
         Explorer explorer = new Explorer(config);
         Executor executor = new Executor(config);
 
-        List<String> flows = new LinkedList<>();
+        List<List<String>> flows = new LinkedList<>();
 
         while (explorer.hasNextValuation()) {
             Valuation val = explorer.getNextValuation();
             Trace trace = executor.execute(val);
             if (trace != null) {
                 trace.print();
-                flows.addAll(trace.getFlows());
+                flows.add(new LinkedList<>(trace.getFlows()));
             } else {
                 System.out.println("== no trace obtained.");
             }
@@ -67,8 +65,24 @@ public void executeAnalysis() {
         System.out.println(explorer.getAnalysis());
 
         InformationFlowAnalysis ia = new InformationFlowAnalysis(config);
-        for (String f : flows) {
-            ia.addFlow(f);
+
+        int slotCount = (int) ((double) flows.size() * config.getFraction());
+        System.out.println("Flows recorded for " + flows.size() + " paths. " +
+                "Using " + slotCount + " (" + config.getFraction() +
+                ") paths for information flow analysis." );
+
+        Random rand = config.getRandom();
+
+        Set<Integer> slots = new TreeSet<>();
+        while (slots.size() < slotCount) {
+            slots.add(rand.nextInt(flows.size()));
+        }
+
+        for (Integer idx : slots) {
+            List<String> fList = flows.get(idx);
+            for (String f : fList) {
+                ia.addFlow(f);
+            }
         }
         //ia.listFlows();
         ia.runChecks();

src/main/java/tools/aqua/dse/DSEArguments.java

@@ -81,6 +81,9 @@ public void usage(String message) {
         printDSEOptionHelp("dse.bounds.type", "fibonacci: uses fibonacci seq. from index 2 (1, 2, 3, 5, ...) as steps");
         printDSEOptionHelp("dse.witness", "save witness file if possible: true / false (default)");
         printDSEOptionHelp("dse.sources", "path to folder with sources");
+        printDSEOptionHelp("iflow.fraction", "fraction of paths to use in information flow analysis (double)");
+        printDSEOptionHelp("static.info", "static information on inheritance and constructors for objects (filename)");
+        printDSEOptionHelp("random.seed", "random seed (long value)");
         System.out.println();
     }
 

src/main/java/tools/aqua/dse/iflow/InformationFlowAnalysis.java

@@ -88,17 +88,17 @@ public void runChecks() {
         solverCtx.push();
 
         for (String v : taintchecks.keySet()) {
-            //System.out.println("---");
-            //System.out.println(new PropositionalCompound(getOrCreate(v, vars), LogicalOperator.EQUIV, ExpressionUtil.TRUE));
+            System.out.println("---");
+            System.out.println(new PropositionalCompound(getOrCreate(v, vars), LogicalOperator.EQUIV, ExpressionUtil.TRUE));
             solverCtx.add(new PropositionalCompound(getOrCreate(v, vars), LogicalOperator.EQUIV, ExpressionUtil.TRUE));
 
             Variable check = getOrCreate("check", vars);
             for (String val : taintchecks.get(v)) {
-                //System.out.println(new PropositionalCompound(getOrCreate(val, vars), LogicalOperator.EQUIV, check));
+                System.out.println(new PropositionalCompound(getOrCreate(val, vars), LogicalOperator.EQUIV, check));
                 solverCtx.add(new PropositionalCompound(getOrCreate(val, vars), LogicalOperator.EQUIV, check));
             }
 
-            //System.out.println(new PropositionalCompound(check, LogicalOperator.XOR, getOrCreate(v, vars)));
+            System.out.println(new PropositionalCompound(check, LogicalOperator.XOR, getOrCreate(v, vars)));
             solverCtx.add(new PropositionalCompound(check, LogicalOperator.XOR, getOrCreate(v, vars)));
 
             boolean violation = (solverCtx.isSatisfiable() == ConstraintSolver.Result.UNSAT);
@@ -122,7 +122,7 @@ private void generate(Map<String, Variable> vars) {
 
             for (Expression tv : taintVars) {
                 Expression flow = new PropositionalCompound(tv, LogicalOperator.IMPLY, key);
-                //System.out.println(flow);
+                System.out.println(flow);
                 flowConstraints.add(flow);
             }
         }

src/main/java/tools/aqua/dse/objects/Clazz.java

@@ -0,0 +1,45 @@
+package tools.aqua.dse.objects;
+
+import java.util.Arrays;
+
+public class Clazz {
+
+    private final String name;
+    private final String[] superClasses;
+    private final String[] constructors;
+
+    public Clazz(String name, String[] superClasses, String[] constructors) {
+        this.name = name;
+        this.superClasses = superClasses;
+        this.constructors = constructors;
+    }
+
+    public String getName() {
+        return name;
+    }
+
+    public String[] getSuperClasses() {
+        return superClasses;
+    }
+
+    public String[] getConstructors() {
+        return constructors;
+    }
+
+    @Override
+    public String toString() {
+        return "Clazz{" +
+                "name='" + name + '\'' +
+                ", superClasses=" + Arrays.toString(superClasses) +
+                ", constructors=" + Arrays.toString(constructors) +
+                '}';
+    }
+
+    public boolean hasSuper(String other) {
+        return name.equals(other) || Arrays.stream(superClasses).filter( (n) -> n.equals(other) ).findFirst().isPresent();
+    }
+
+    public boolean hasConstructor(String m) {
+        return Arrays.stream(constructors).filter( (n) -> n.equals(m) ).findFirst().isPresent();
+    }
+}

src/main/java/tools/aqua/dse/objects/Objects.java

@@ -0,0 +1,98 @@
+package tools.aqua.dse.objects;
+
+import gov.nasa.jpf.constraints.api.SolverContext;
+import gov.nasa.jpf.constraints.expressions.Constant;
+import gov.nasa.jpf.constraints.expressions.LogicalOperator;
+import gov.nasa.jpf.constraints.expressions.PropositionalCompound;
+import gov.nasa.jpf.constraints.expressions.functions.Function;
+import gov.nasa.jpf.constraints.expressions.functions.FunctionExpression;
+import gov.nasa.jpf.constraints.types.BuiltinTypes;
+import gov.nasa.jpf.constraints.util.ExpressionUtil;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.HashMap;
+import java.util.stream.Collectors;
+
+public class Objects {
+
+    public static final Function<BuiltinTypes.BoolType> extendsFct = new Function("extends",
+            BuiltinTypes.BOOL, BuiltinTypes.STRING, BuiltinTypes.STRING);
+
+    public static final  Function<BuiltinTypes.BoolType> initializesFct = new Function("initializes",
+            BuiltinTypes.BOOL, BuiltinTypes.STRING, BuiltinTypes.STRING);
+
+    private final HashMap<String, Clazz> clazzes = new HashMap<>();
+
+    public void initObjectsStructure(SolverContext ctx) {
+        ArrayList<String> methods = new ArrayList<>();
+        for (Clazz c : clazzes.values()) {
+            methods.addAll(Arrays.stream(c.getConstructors()).collect(Collectors.toList()));
+            for (String other : clazzes.keySet()) {
+                FunctionExpression application = new FunctionExpression(extendsFct,
+                        new Constant<String>(BuiltinTypes.STRING, c.getName()),
+                        new Constant<String>(BuiltinTypes.STRING, other));
+
+                ctx.add(new PropositionalCompound(application, LogicalOperator.EQUIV,
+                        c.hasSuper(other) ? ExpressionUtil.TRUE : ExpressionUtil.FALSE));
+            }
+        }
+        for (Clazz c : clazzes.values()) {
+            for (String m : methods) {
+                FunctionExpression application = new FunctionExpression(initializesFct,
+                        new Constant<String>(BuiltinTypes.STRING, m),
+                        new Constant<String>(BuiltinTypes.STRING, c.getName()));
+
+                ctx.add(new PropositionalCompound(application, LogicalOperator.EQUIV,
+                        c.hasConstructor(m) ? ExpressionUtil.TRUE : ExpressionUtil.FALSE));
+            }
+        }
+    }
+
+    public Objects(String config) {
+        fromString(config);
+        String[] cNames = clazzes.keySet().toArray(new String[] {});
+        Clazz NULL = new Clazz("_NULL", cNames, new String[] {"_NULL()"});
+        clazzes.put("_NULL", NULL);
+    }
+
+    private void fromString(String text) {
+        text = text.trim();
+        while (text.startsWith("class")) {
+            int splitIndex =  text.indexOf("}");
+            String entry = text.substring(5, text.indexOf("}")).trim();
+            classFromString(entry);
+            text = text.substring(splitIndex+1).trim();
+        }
+        if (!text.isEmpty()) {
+            throw new RuntimeException("cannot parse: " + text);
+        }
+    }
+
+    private void classFromString(String text) {
+        text = text.trim();
+        int splitIndex1 =  text.indexOf("extends");
+        int splitIndex2 =  text.indexOf("{");
+        if (splitIndex1 < 0) {
+            splitIndex1 = splitIndex2;
+        }
+        String clazz = text.substring(0, splitIndex1).trim();
+        String[] superClasses = new String[] {};
+        if (splitIndex1 < splitIndex2) {
+            for (int i=0; i<superClasses.length; i++) {
+                superClasses[i] = superClasses[i].trim();
+            }
+        }
+        String[] constructors = text.substring(splitIndex2+1).trim().split(",");
+
+        for (int i=0; i<constructors.length; i++) {
+            constructors[i] = constructors[i].trim();
+        }
+        if (constructors.length == 1 && constructors[0].isEmpty()) constructors = new String[] {};
+        this.clazzes.put(clazz, new Clazz(clazz, superClasses, constructors));
+    }
+
+    public HashMap<String, Clazz> getClazzes() {
+        return clazzes;
+    }
+}

src/main/java/tools/aqua/dse/tree/ConstraintsTree.java

@@ -450,7 +450,8 @@ public Valuation findNext() {
         if ((nextOpen.parent() == null && root != nextOpen)
             || (nextOpen.parent() != null
                 && nextOpen.parent().getChild(nextOpen.childId()) != nextOpen)
-            || nextOpen.isFinal()) {
+            || nextOpen.isFinal()
+            || (nextOpen.parent() != null && nextOpen.parent().isExhausted())) {
           nextOpen = null;
           continue;
         }

src/main/java/tools/aqua/dse/tree/DecisionNode.java

@@ -25,6 +25,7 @@ class DecisionNode extends Node {
 
     private final Expression<Boolean>[] constraints;
     private final Node[] children;
+    private boolean exhausted = false;
 
     DecisionNode(DecisionNode parent, Decision d, int pos,
                  boolean explore, ExplorationStrategy strategy) {
@@ -73,10 +74,14 @@ void update(Decision d) {
     }
 
     void useUnexploredConstraint(int idx) {
+        if (constraints[idx] == null) {
+            exhausted = true;
+        }
         constraints[idx] = getConstraint(idx);
     }
 
     int missingConstraints() {
+        if (exhausted) return 0;
         int i = 0;
         for (Expression<Boolean> e : constraints) {
             if (e == null) {
@@ -133,8 +138,14 @@ String validateDecision(Decision d) {
     void print(StringBuilder out, int indent) {
         for (int i=0; i< children.length; i++) {
             indent(out, indent);
-            out.append(i).append(" : ").append(constraints[i]).append("\n");
-            children[i].print(out, indent + 1);
+            if (!exhausted || constraints[i] != null) {
+                out.append(i).append(" : ").append(constraints[i]).append("\n");
+                children[i].print(out, indent + 1);
+            }
         }
     }
+
+    public boolean isExhausted() {
+        return exhausted;
+    }
 }