From 952ffabdb3026d5b512058f4594cfa2c7037975f Mon Sep 17 00:00:00 2001 From: Falk Howar Date: Fri, 26 May 2023 09:59:20 +0200 Subject: [PATCH 1/3] experiments with information flow --- src/main/java/tools/aqua/dse/Config.java | 23 +++++++++++++++ src/main/java/tools/aqua/dse/DSE.java | 28 ++++++++++++++----- .../java/tools/aqua/dse/DSEArguments.java | 2 ++ .../dse/iflow/InformationFlowAnalysis.java | 10 +++---- 4 files changed, 51 insertions(+), 12 deletions(-) diff --git a/src/main/java/tools/aqua/dse/Config.java b/src/main/java/tools/aqua/dse/Config.java index 05be8b0..3e7f776 100644 --- a/src/main/java/tools/aqua/dse/Config.java +++ b/src/main/java/tools/aqua/dse/Config.java @@ -32,6 +32,7 @@ import java.util.Iterator; import java.util.Map; import java.util.Properties; +import java.util.Random; public class Config { @@ -72,6 +73,10 @@ 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 @@ -159,6 +164,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 +224,15 @@ private void parseProperties(Properties props) { sourceLoader = new URLClassLoader(urls); } + if (props.containsKey("iflow.fraction")) { + this.fraction = Double.parseDouble(props.getProperty("iflow.fraction")); + } + 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) { diff --git a/src/main/java/tools/aqua/dse/DSE.java b/src/main/java/tools/aqua/dse/DSE.java index 6cefd64..30f9cf3 100644 --- a/src/main/java/tools/aqua/dse/DSE.java +++ b/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 flows = new LinkedList<>(); + List> 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 slots = new TreeSet<>(); + while (slots.size() < slotCount) { + slots.add(rand.nextInt(flows.size())); + } + + for (Integer idx : slots) { + List fList = flows.get(idx); + for (String f : fList) { + ia.addFlow(f); + } } //ia.listFlows(); ia.runChecks(); diff --git a/src/main/java/tools/aqua/dse/DSEArguments.java b/src/main/java/tools/aqua/dse/DSEArguments.java index 54f3719..4bd1262 100644 --- a/src/main/java/tools/aqua/dse/DSEArguments.java +++ b/src/main/java/tools/aqua/dse/DSEArguments.java @@ -81,6 +81,8 @@ 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("random.seed", "random seed (long value)"); System.out.println(); } diff --git a/src/main/java/tools/aqua/dse/iflow/InformationFlowAnalysis.java b/src/main/java/tools/aqua/dse/iflow/InformationFlowAnalysis.java index 61f74c5..b5a339c 100644 --- a/src/main/java/tools/aqua/dse/iflow/InformationFlowAnalysis.java +++ b/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 vars) { for (Expression tv : taintVars) { Expression flow = new PropositionalCompound(tv, LogicalOperator.IMPLY, key); - //System.out.println(flow); + System.out.println(flow); flowConstraints.add(flow); } } From ec43a365b1a907b4f8979e6723ce5a0606bad6a0 Mon Sep 17 00:00:00 2001 From: Falk Howar Date: Wed, 22 May 2024 12:15:57 +0200 Subject: [PATCH 2/3] falks initial proposal for loading inheritance infro for object support in dse --- src/main/java/tools/aqua/dse/Config.java | 15 ++- .../java/tools/aqua/dse/DSEArguments.java | 1 + .../java/tools/aqua/dse/objects/Clazz.java | 45 +++++++++ .../java/tools/aqua/dse/objects/Objects.java | 98 +++++++++++++++++++ .../tools/aqua/dse/tree/ConstraintsTree.java | 3 +- .../tools/aqua/dse/tree/DecisionNode.java | 15 ++- .../trace/StaticInformationParserTest.java | 24 +++++ 7 files changed, 197 insertions(+), 4 deletions(-) create mode 100644 src/main/java/tools/aqua/dse/objects/Clazz.java create mode 100644 src/main/java/tools/aqua/dse/objects/Objects.java create mode 100644 src/test/java/tools/aqua/dse/trace/StaticInformationParserTest.java diff --git a/src/main/java/tools/aqua/dse/Config.java b/src/main/java/tools/aqua/dse/Config.java index 3e7f776..b96f760 100644 --- a/src/main/java/tools/aqua/dse/Config.java +++ b/src/main/java/tools/aqua/dse/Config.java @@ -22,6 +22,7 @@ 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; @@ -84,6 +85,8 @@ public static ExplorationStrategy fromString(String property) { private final Properties properties; + private Objects objects = null; + private Config(Properties properties) { this.properties = properties; } @@ -120,7 +123,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; } /** @@ -227,6 +235,11 @@ private void parseProperties(Properties props) { if (props.containsKey("iflow.fraction")) { this.fraction = Double.parseDouble(props.getProperty("iflow.fraction")); } + + if (props.containsKey("static.info")) { + this.objects = new Objects(props.getProperty("static.info")); + } + long seed = (new Random()).nextLong(); if (props.containsKey("random.seed")) { seed = Long.parseLong(props.getProperty("random.seed")); diff --git a/src/main/java/tools/aqua/dse/DSEArguments.java b/src/main/java/tools/aqua/dse/DSEArguments.java index 4bd1262..e1bc3f1 100644 --- a/src/main/java/tools/aqua/dse/DSEArguments.java +++ b/src/main/java/tools/aqua/dse/DSEArguments.java @@ -82,6 +82,7 @@ public void usage(String message) { 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"); printDSEOptionHelp("random.seed", "random seed (long value)"); System.out.println(); } diff --git a/src/main/java/tools/aqua/dse/objects/Clazz.java b/src/main/java/tools/aqua/dse/objects/Clazz.java new file mode 100644 index 0000000..2606b6f --- /dev/null +++ b/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(); + } +} diff --git a/src/main/java/tools/aqua/dse/objects/Objects.java b/src/main/java/tools/aqua/dse/objects/Objects.java new file mode 100644 index 0000000..3eeb829 --- /dev/null +++ b/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 extendsFct = new Function("extends", + BuiltinTypes.BOOL, BuiltinTypes.STRING, BuiltinTypes.STRING); + + public static final Function initializesFct = new Function("initializes", + BuiltinTypes.BOOL, BuiltinTypes.STRING, BuiltinTypes.STRING); + + private final HashMap clazzes = new HashMap<>(); + + public void initObjectsStructure(SolverContext ctx) { + ArrayList 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(BuiltinTypes.STRING, c.getName()), + new Constant(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(BuiltinTypes.STRING, m), + new Constant(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 getClazzes() { + return clazzes; + } +} diff --git a/src/main/java/tools/aqua/dse/tree/ConstraintsTree.java b/src/main/java/tools/aqua/dse/tree/ConstraintsTree.java index dcc781e..a2eb1d6 100644 --- a/src/main/java/tools/aqua/dse/tree/ConstraintsTree.java +++ b/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; } diff --git a/src/main/java/tools/aqua/dse/tree/DecisionNode.java b/src/main/java/tools/aqua/dse/tree/DecisionNode.java index 909ca6f..8bca3bf 100644 --- a/src/main/java/tools/aqua/dse/tree/DecisionNode.java +++ b/src/main/java/tools/aqua/dse/tree/DecisionNode.java @@ -25,6 +25,7 @@ class DecisionNode extends Node { private final Expression[] 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 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; + } } diff --git a/src/test/java/tools/aqua/dse/trace/StaticInformationParserTest.java b/src/test/java/tools/aqua/dse/trace/StaticInformationParserTest.java new file mode 100644 index 0000000..f81f925 --- /dev/null +++ b/src/test/java/tools/aqua/dse/trace/StaticInformationParserTest.java @@ -0,0 +1,24 @@ +package tools.aqua.dse.trace; + +import gov.nasa.jpf.constraints.smtlibUtility.parser.SMTLIBParserException; +import org.testng.Assert; +import org.testng.annotations.Test; +import tools.aqua.dse.objects.Objects; + +import java.io.IOException; + +public class StaticInformationParserTest { + + @Test + public void testStaticInformationParser() throws IOException, SMTLIBParserException { + + String info = + "class A { A() }" + + "class C {}" + + "class B extends A, C { B(), B(II) }"; + + Objects o = new Objects(info); + Assert.assertEquals(o.getClazzes().size(), 4); + + } +} From de2f77937db157d4e13e869789c97d8f5800fe2a Mon Sep 17 00:00:00 2001 From: Falk Howar Date: Mon, 27 May 2024 13:43:01 +0200 Subject: [PATCH 3/3] expect static info in file --- src/main/java/tools/aqua/dse/Config.java | 17 ++++++++++++++--- src/main/java/tools/aqua/dse/DSEArguments.java | 2 +- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/main/java/tools/aqua/dse/Config.java b/src/main/java/tools/aqua/dse/Config.java index b96f760..b609aec 100644 --- a/src/main/java/tools/aqua/dse/Config.java +++ b/src/main/java/tools/aqua/dse/Config.java @@ -24,8 +24,7 @@ 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; @@ -237,7 +236,19 @@ private void parseProperties(Properties props) { } if (props.containsKey("static.info")) { - this.objects = new Objects(props.getProperty("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(); diff --git a/src/main/java/tools/aqua/dse/DSEArguments.java b/src/main/java/tools/aqua/dse/DSEArguments.java index e1bc3f1..ed71241 100644 --- a/src/main/java/tools/aqua/dse/DSEArguments.java +++ b/src/main/java/tools/aqua/dse/DSEArguments.java @@ -82,7 +82,7 @@ public void usage(String message) { 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"); + printDSEOptionHelp("static.info", "static information on inheritance and constructors for objects (filename)"); printDSEOptionHelp("random.seed", "random seed (long value)"); System.out.println(); }