[experimental] PInfer: learning specifications from event traces

P.sln

@@ -19,6 +19,10 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CheckerCore", "Src\PChecker
 EndProject
 Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "PTool", "PTool", "{8BAB6184-8545-4E17-8199-86110AC5228F}"
 EndProject
+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Src", "Src", "{5976592D-2EC6-4991-89A9-7EC97EEC0FFD}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "PInfer", "Src\PInfer\PInfer.csproj", "{3DFC4318-5D40-41A0-B46D-F0896180B45C}"
+EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
 		Debug|Any CPU = Debug|Any CPU
@@ -41,6 +45,10 @@ Global
 		{37778F65-BDBF-4AEA-BA34-01026A223083}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{37778F65-BDBF-4AEA-BA34-01026A223083}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{37778F65-BDBF-4AEA-BA34-01026A223083}.Release|Any CPU.Build.0 = Release|Any CPU
+		{3DFC4318-5D40-41A0-B46D-F0896180B45C}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{3DFC4318-5D40-41A0-B46D-F0896180B45C}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{3DFC4318-5D40-41A0-B46D-F0896180B45C}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{3DFC4318-5D40-41A0-B46D-F0896180B45C}.Release|Any CPU.Build.0 = Release|Any CPU
 	EndGlobalSection
 	GlobalSection(SolutionProperties) = preSolution
 		HideSolutionNode = FALSE
@@ -50,6 +58,7 @@ Global
 		{41F39ADD-B75F-473F-AC41-D1A9CDA9A9CD} = {1B21372A-3030-4532-8B30-2A1A3E74527A}
 		{37778F65-BDBF-4AEA-BA34-01026A223083} = {F7D2A6F5-841A-4E22-9ECD-2E1CF736F7EA}
 		{C1A8AF94-F550-4EC7-889A-9D0CCA259502} = {8BAB6184-8545-4E17-8199-86110AC5228F}
+		{3DFC4318-5D40-41A0-B46D-F0896180B45C} = {5976592D-2EC6-4991-89A9-7EC97EEC0FFD}
 	EndGlobalSection
 	GlobalSection(ExtensibilityGlobals) = postSolution
 		SolutionGuid = {BD6B0E25-71B7-4A8F-8D0F-946BA6D47C7C}

PInferGuide.md

@@ -0,0 +1,124 @@
+# PInfer - Automatic Invariant Learning from Traces
+## Prerequisites
+> Note that PInfer has only been tested on Amazon Linux.
+
+### Installing Z3 (before building P)
+1. Clone the Z3 repository: https://github.com/Z3Prover/z3 by `git clone git@github.com:Z3Prover/z3.git`
+2. Run `python scripts/mk_make.py -x --dotnet`
+3. `cd build; make -j$(nproc)`
+4. `sudo make install`
+5. Add `export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:/path-to-z3/build/"` to `.bashrc` (or `.zshrc` if using Zsh) where `path-to-z3` is the directory of the cloned Z3 repository in step 1.
+
+#### Environment setups
+- Follow the instruction of [P language here](https://p-org.github.io/P/getstarted/install/) and install dotnet. The version used for developing is 8.0.401.
+- Install Java 22 and maven
+    + For amazon linux, [follow the guide here](https://docs.aws.amazon.com/corretto/latest/corretto-22-ug/generic-linux-install.html#rpm-linux-install-instruct)
+    + Maven version: Apache Maven 3.5.2. Can be installed via `sudo yum install maven`
+- Install PJavaRuntime: go to [Src/Runtimes/PJavaRuntimes](./Src/PRuntimes/PJavaRuntime/) and run `mvn install`
+- Compile P: run `dotnet build -c Release` under the root of this repo. 
+
+## Step 1: Getting traces
+### Using the python script for generating traces
+There is a `1_prepare_traces.py` under `Tutoiral/PInfer`. To use this script to generate traces, first add an entry to `configurations` dictionary in `Tutoiral/PInfer/constants.py`.
+The key should be the name of the folder under `Tutorial/PInfer` that contains the P source code of the benchmark, and the value is a list of names of test cases to run to obtain the traces. 
+
+You may optionally set an environment variable called `PINFER_TRACE_DIR` (e.g. `export PINFER_TRACE_DIR=/home/PInferTraces) that specifies the path to store the generated traces. 
+
+After making the changes, run with
+```
+> python3 1_prepare_traces.py --benchmarks [names of benchmarks] --num_traces [a list of numbers representing number of traces to generate] [--trace_dir <path-to-store-traces>]
+```
+
+For instance, to generate 10k traces for Paxos storing into `$PINFER_TRACE_DIR`, run the following
+> `python3 1_prepare_traces.py --benchmarks paxos --num_traces 10000`
+
+### Event filters
+By default, the generated traces have all Send and Announce events being recorded.
+For some benchmarks, we may want to only record events that are relevant to the protocol.
+To do so, add an entry in `event_combs` dictionary in `constants.py`, where the key is the name of directory of the benchmark and the value is in the form of `[(e1, e2, e3...)]` where `e1, e2, e3...` are events that are relevant to the protocol.
+
+**Removing traces:** If you want to remove certain traces, simply delete the files. You don't need to remove the metadata in the JSON file.
+
+**How are trace metadata being used?** When checking `n` events of type e1, e2, ..., en, PInfer will first look for any *exact* match on the index, i.e. a folder that have traces that contains events that are *exactly* of type e1, ..., en. If no such folder is found, PInfer looks for any folder that holds traces that is a superset of (e1, ..., en). 
+
+> Alternatively, some of the codebase have `generateTrace.sh`. You can simply run `./generateTrace.sh <num schedules> <e1> <e2> ... <en>` and it will gather traces containing e1, e2,...,en using all test cases. 
+
+## Step 2: Running PInfer
+For our benchmarks, simply execute `run.sh` under the benchmark folders. 
+
+To setup your own experiments:
+### Fully-automated mode
+Simply run `p infer`, it will infer combinations of events that might yield interesting properties and then perform the search over the lattice.
+
+If traces are stored under some other paths, you can run it with `p infer -t <path-to-traces>`. Note that there must be a `metadata.json` under the provided path. 
+
+If traces were generated using `1_prepare_traces.py`, then under `PINFER_TRACE_DIR`, traces are stored in folders that have the same name as the benchmark. For example `PINFER_TRACE_DIR/paxos/10000` stores 10k traces for paxos. This is the path you will need to pass to PInfer using `-t` commandline argument. For example, running PInfer under `paxos` with 10k traces is
+
+```
+> p infer -t $PINFER_TRACE_DIR/paxos/10000
+```
+
+To enable SMT-based pruning, add a `-z3` flag, e.g.,
+```
+> p infer -t $PINFER_TRACE_DIR/paxos/10000 -z3
+```
+
+Default parameters (upper bounds): 
+- `term_depth`: 2
+- `num_guards`: 2
+- `num_filters`: 2
+- `exists`: 1
+- `config_event`: null
+
+`arity` is determined by the maximum arity of prediates generated. 
+
+These can be configured using command line argumets:
+> p infer -td <`max term depth`> -max-guards <`max conj in guards`> -max-filters <`max conj. in filters`> -ce <`event name`>
+
+### Hints
+Hints is a construct in P program that provides manual hints for PInfer. 
+
+Hints can be defined as follows:
+```
+hint <hint name> (e1: Event1 ... en: EventN) {
+    term_depth =  <int>;
+    exists =      <int>;
+    num_guards =  <int>;
+    num_filters = <int>;
+    arity =       <int>;
+    config_event = <event name>;
+    include_guards = <bool expr>;    // predicates that must be included in the guards, e.g. e0.key == e1.key; conjuntion only.
+    include_filters = <bool expr>;   // similar, but must be included in filters
+}
+```
+
+If any of the field is not provided, the default values are:
+- `exists` = 0
+- `num_guards` = 0
+- `num_filters` = 0
+- `arity` = 1
+- `config_event` = null
+- `include_guards` = true
+- `include_filters` = true
+
+#### Generating SpecMiner for a hint
+> p infer --action compile --hint <`name of the hint`>
+
+PInfer will generate the SpecMiner specifically for the provided hint.
+
+#### Searching the space defined by a hint
+> p infer --action run --hint <`name of hint`> \[--traces <`folder`>\]
+
+PInfer will search the formula in the form of `forall* G -> exists* F /\ R` that holds for all traces. PInfer starts with the provided parameters in the hint and search till the upperbound. 
+By default PInfer looks for traces under `traces` folder. Notice that the traces must be indexed, i.e. having a `metadata.json` mapping sets of events to folders containing corresponding traces.
+
+#### Searching a specific grid
+**exact hints:** Mainly used for debugging purposes. When declaring a hint with `exact` keyword, i.e. `hint exact ...` then running it, PInfer will only check the search space defined by the given parameters in the hint but will not go up the grid. 
+
+#### List out predicates generated
+> p infer -lp
+#### List out terms generated
+> p infer -lt
+
+## Step 3: Outputs
+After PInfer finishes, invariants will be stored in `invariants.txt` in the folder PInfer was executed. Another file `inv_running.txt` will be updated as PInfer finds new invariants. Mined properties are pretty-printted. 

PInferTemplates/FromDaikon.java

@@ -0,0 +1,235 @@
+import java.util.stream.Collectors;
+
+public class FromDaikon {
+    public int numExists;
+    private Map<Set<Integer>, List<Main.RawPredicate>> termsToPredicates;
+    private List<Main.RawTerm> terms;
+    private String templateHeaderCar;
+    private String templateHeaderCdr;
+    private int pruningLevel;
+    private static final String[] QUANTIFIERS = { %QUANTIFIERS% };
+    private static final String[] VARNAME = { %QUANTIFIED_VARS% };
+    private static final String[] FILTERED_INVS = { "!= null", ".getClass().getName()", "[] ==" };
+    private static final String[] COMP_OPS = { "!=", "<=", "<", ">=", ">" };
+    private static final Map<String, String> substs = new HashMap<>();
+
+    public FromDaikon(Map<Set<Integer>, List<Main.RawPredicate>> termsToPredicates,
+                      List<Main.RawTerm> terms, String templateFamily, int numExtQuantfiers, int pruningLevel) {
+        this.termsToPredicates = termsToPredicates;
+        this.terms = terms;
+        this.templateHeaderCar = "";
+        this.templateHeaderCdr = "";
+        this.numExists = numExtQuantfiers;
+        this.pruningLevel = pruningLevel;
+        StringBuilder sb = new StringBuilder();
+        switch (templateFamily) {
+            case "Forall":
+                for (int i = 0; i < QUANTIFIERS.length; ++i) {
+                    sb.append("∀").append(VARNAME[i])
+                            .append(": ").append(QUANTIFIERS[i]).append(i == QUANTIFIERS.length - 1 ? " :: " : " ");
+                }
+                templateHeaderCar = sb.toString();
+                break;
+            case "Exists":
+                for (int i = 0; i < QUANTIFIERS.length; ++i) {
+                    sb.append("∃").append(VARNAME[i])
+                            .append(":").append(QUANTIFIERS[i]).append(i == QUANTIFIERS.length - 1 ? " :: " : " ");
+                }
+                templateHeaderCar = sb.toString();
+                break;
+            case "ForallExists":
+                for (int i = 0; i < QUANTIFIERS.length - numExtQuantfiers; ++i) {
+                    sb.append("∀").append(VARNAME[i])
+                            .append(":").append(QUANTIFIERS[i]).append(i == QUANTIFIERS.length - numExtQuantfiers - 1 ? " :: " : " ");
+                }
+                templateHeaderCar = sb.toString();
+                sb = new StringBuilder();
+                for (int i = QUANTIFIERS.length - numExtQuantfiers; i < QUANTIFIERS.length; ++i) {
+                    sb.append("∃").append(VARNAME[i])
+                            .append(":").append(QUANTIFIERS[i]).append(i == QUANTIFIERS.length - 1 ? " :: " : " ");
+                }
+                templateHeaderCdr = sb.toString();
+                break;
+            default:
+                throw new IllegalArgumentException("Unknown template family: " + templateFamily);
+        }
+        substs.put(".toString", "");
+        substs.put("one of", "∈");
+        substs.put(".getPayload()", "");
+        substs.put("[] elements", "");
+        substs.put("(elementwise)", "");
+    }
+
+    public String getFormulaHeader(String guards, String filters) {
+        String guardsStr = runSubst(guards);
+        String arrow = guardsStr.length() == 0 ? " " : " -> ";
+        return this.templateHeaderCar + guardsStr + arrow + this.templateHeaderCdr + runSubst(filters);
+    }
+
+    public String convertOutput(String line, List<Main.RawPredicate> guards, List<Main.RawPredicate> filters,
+                                List<Main.RawTerm> forallTerms, List<Main.RawTerm> existsTerms) {
+        if (!checkValidity(line, guards, filters, forallTerms, existsTerms)) {
+            return null;
+        }
+        List<Main.RawTerm> substTerms = new ArrayList<>();
+        for (int i = 0; i < forallTerms.size(); ++i) {
+            if (line.contains("f" + i)) {
+                substTerms.add(forallTerms.get(i));
+                line = line.replace("f" + i, forallTerms.get(i).shortRepr());
+            }
+        }
+        for (int i = 0; i < existsTerms.size(); ++i) {
+            String fieldPHName = "f" + (i + forallTerms.size());
+            if (line.contains(fieldPHName)) {
+                // do not check sorted by for aggregated array
+                if (line.contains("sorted by")) return null;
+                substTerms.add(existsTerms.get(i));
+                line = line.replace(fieldPHName, existsTerms.get(i).shortRepr());
+            }
+        }
+        boolean didSth = !substTerms.isEmpty();
+        if (!didSth && !line.contains("_num_e_exists_")) return null;
+        if (line.contains("_num_e_exists_")) {
+            // _num_e_exists_ should be on lhs
+            if (!line.startsWith("_num_e_exists_")) return null;
+            // check # exists is related not only existentially quantified events
+            if (didSth) {
+                Set<Integer> boundedEvents = substTerms.stream()
+                        .flatMap(x -> x.events().stream())
+                        .collect(Collectors.toSet());
+                boolean containsForallEvent = false;
+                for (int i = 0; i < QUANTIFIERS.length - numExists; ++i) {
+                    if (boundedEvents.contains(i)) {
+                        containsForallEvent = true;
+                        break;
+                    }
+                }
+                if (!containsForallEvent) return null;
+            }
+        }
+        return runSubst(line);
+    }
+
+    private String runSubst(String line) {
+        for (var subst : substs.entrySet()) {
+            line = line.replace(subst.getKey(), subst.getValue());
+        }
+        if (line.contains(" in ")) {
+            line = line.replace(" in ", " == ");
+        }
+        line = line.replace("[]", "");
+        return line;
+    }
+
+    private boolean isNumber(String x) {
+        if (x == null || x.isEmpty()) return false;
+        try {
+            Double.parseDouble(x);
+        } catch (NumberFormatException e) {
+            return false;
+        }
+        return true;
+    }
+
+    private boolean containsTerm(String line, int forallTermCount, int existsTermCount) {
+        for (int i = 0; i < forallTermCount + existsTermCount; ++i) {
+            if (line.contains("f" + i)) return true;
+        }
+        return false;
+    }
+
+    private Main.RawTerm getTermByTemplateField(String f, List<Main.RawTerm> forallTerms, List<Main.RawTerm> existsTerms) {
+        for (int i = 0; i < forallTerms.size(); ++i) {
+            if (f.contains("f" + i)) return forallTerms.get(i);
+        }
+        for (int i = 0; i < existsTerms.size(); ++i) {
+            if (f.contains("f" + (i + forallTerms.size()))) return existsTerms.get(i);
+        }
+        return null;
+    }
+
+    private Map.Entry<List<Main.RawTerm>, List<Main.RawTerm>> 
+        getTermSubsts(String line, List<Main.RawTerm> forallTerms, List<Main.RawTerm> existsTerms) {
+        List<Main.RawTerm> forallSubsts = new ArrayList<>();
+        List<Main.RawTerm> existsSubsts = new ArrayList<>();
+        for (int i = 0; i < forallTerms.size(); ++i) {
+            if (line.contains("f" + i)) forallSubsts.add(forallTerms.get(i));
+        }
+        for (int i = 0; i < existsTerms.size(); ++i) {
+            int j = i + forallTerms.size();
+            if (line.contains("f" + j)) existsSubsts.add(existsTerms.get(i));
+        }
+        return new AbstractMap.SimpleEntry<>(forallSubsts, existsSubsts);
+    }
+
+    private boolean checkValidity(String line, List<Main.RawPredicate> guards,
+                                    List<Main.RawPredicate> filters,
+                                    List<Main.RawTerm> forallTerms,
+                                    List<Main.RawTerm> existsTerms) {
+        if (pruningLevel == 0) {
+            return true;
+        }
+        if (pruningLevel >= 1) {
+            // prune nullptr comparisons
+            // and type name comparisons
+            for (var stub : FILTERED_INVS) {
+                if (line.contains(stub)) return false;
+            }
+        }
+        if (pruningLevel >= 2) {
+            // prune if the set of terms of the mined property
+            // equals to some selected atomic predicates
+            Set<Integer> minedPropertyBoundedTerms = new HashSet<>();
+            for (int i = 0; i < forallTerms.size(); ++i) {
+                if (line.contains("f" + i)) {
+                    minedPropertyBoundedTerms.add(forallTerms.get(i).order());
+                }
+            }
+            for (int i = 0; i < existsTerms.size(); ++i) {
+                if (line.contains("f" + (i + forallTerms.size()))) {
+                    minedPropertyBoundedTerms.add(existsTerms.get(i).order());
+                }
+            }
+            for (Main.RawPredicate p: guards) {
+                if (p.terms().equals(minedPropertyBoundedTerms)) return false;
+            }
+            for (Main.RawPredicate p: filters) {
+                if (p.terms().equals(minedPropertyBoundedTerms)) return false;
+            }
+        }
+        if (pruningLevel >= 3) {
+            // exclude comparisons with constants
+            for (String op: COMP_OPS) {
+                if (line.contains(op)) {
+                    String[] args = line.split(op);
+                    if (args.length < 2) continue;
+                    String lhs = args[0].trim();
+                    String rhs = args[1].trim();
+                    if (op.equals("!=")) {
+                        var lhsTerm = getTermByTemplateField(lhs, forallTerms, existsTerms);
+                        var rhsTerm = getTermByTemplateField(rhs, forallTerms, existsTerms);
+                        if (lhsTerm != null && rhsTerm != null) {
+                            if (lhsTerm.shortRepr().endsWith(".index()")
+                                    && rhsTerm.shortRepr().endsWith(".index()")) return false;
+                        }
+                    }
+                    boolean rhsIsConst = isNumber(rhs) || (rhs.startsWith("\"") && rhs.endsWith("\""));
+                    if (!containsTerm(lhs, forallTerms.size(), existsTerms.size())) {
+                        if (!rhsIsConst && !rhs.startsWith("size") && containsTerm(rhs, forallTerms.size(), existsTerms.size())) {
+                            // if a comparison does not involve a term on lhs,
+                            // it should not involve a term on rhs either (avoid `_num_e_exists_ > [some term]`)
+                            // however, we do want to see size([some term]) / config constants on rhs.
+                            return false;
+                        }
+                        break;
+                    }
+                    // if (rhsIsConst) {
+                    //     return false;
+                    // }
+                    break;
+                }
+            }
+        }
+        return true;
+    }
+}