Add a new delegate to allow API tracing

[daniel-raffler]

This is a preliminary draft for adding API tracing to JavaSMT with the help of a new delegate. The idea is to record all API calls and generate a new Java program from them. By running this program the exact sequence of calls can then be recreated. The main application here is debugging, where the traces allow us to create easy to reproduce examples for solver errors. This is especially useful when the error occurs as part of a larger program where it can be hard to pin down the exact sequence of JavaSMT calls that are needed to trigger the bug.

We use a new delegate to implement this feature. Setting solver.trace to true will enable tracing, and the output will be stored in a file called trace*.java

TODO

• Finish the implementation. Currently we only have (parts of) the ArrayFormulaManager, IntegerFormulaManager, BooleanFormulaManager, UFManager and ProverEnvironment
• Write the trace to a file while it's being created. We'll need this to debug segfaults as the trace is otherwise lost done
• Consider adding an option to skip duplicate calls. (The trace is currently way too long) Fixed, but not committed yet
• Write a simple delta-debugger to shrink the trace down even further3 Maybe later..

We're now using ddSmt, see comment #505 (comment)

Things left to do

• Add support for missing formula managers in the script
  Still missing: floating point, quantifier, strings and separation logic. At least the first two should still be added before merging
• Handle solver options in the script
  Model generation and global definitions are now turned on by default. Other options can be added by the user
• Fix undo point in the trace logger
  Done, but we should double check the Rebuilder Should be fine now, but still needs to be cleaned up
• Merge Add support for indexed functions #507
• Add user documentation for debugging with the tracer (see the comment below)
• Update the changelog
• Run some tests in CPAchecker to see if there are still issues in the script
• Add support for quantifiers and interpolation to the Smtlib translation script
• Test with more solvers

[daniel-raffler]

Write a simple delta-debugger to shrink the trace down even further

I started working on the delta-debugger today and wrote a python script to reduce the size of the traces. So far it does little more that some dead-code elimination, but that's already enough to bring down the size of the trace by a factor of ten. I believe that another factor of two should be possible with some aggressive optimization.

The issue now is that I don't quite know where to put such a script in JavaSMT. We could handle this as a separate project, or maybe include it in the JavaSMT source tree, similar to the Example projects. However, neither really seems quite ideal.

@baierd, @kfriedberger: What is your opinion?

Here is the file in question:

#!/usr/bin/env python3
import re
import sys
from collections import defaultdict
from pathlib import Path


# Read a trace file
def readTrace(path):
    with open(path) as file:
        return [line.rstrip() for line in file]


# Build a map with line numbers for all variable definitions
def getLinesForDefinitions(trace):
    lineNumber = 1
    lineDefs = dict()
    for line in trace:
        if line.find('=') >= 0:
            leftSide = line[0:(line.find('=') - 1)]
            name = re.match('var (.*)', leftSide)
            lineDefs[name.group(1)] = lineNumber
        lineNumber = lineNumber + 1
    return lineDefs


# Build a dependency graph for the definitions
# Maps from variables to the places where they are used
def buildDependencies(lineDefs, trace):
    lineNumber = 1
    deps = defaultdict(list)
    for line in trace:
        expr = line[(line.find('=') + 2):] if line.find('=') >= 0 else line
        object = expr[0:expr.find('.')]
        if object[0].islower():
            deps[lineDefs[object]].append(lineNumber)
        # FIXME Parse the expression to get the variables
        for m in re.finditer('(config|logger|notifier|var[0-9]+)', expr):
            deps[lineDefs[m.group()]].append(lineNumber)
        lineNumber += 1
    return deps


# Collect all top-level statements
# Top-level statements are:
#  *.addConstraint(*)
#  *.isUnsat()
#  *.getModel()
#  *.asList()
# FIXME Finish this list
def usedTopLevel(lineDefs, trace):
    tl = set()
    for line in trace:
        m = re.fullmatch(
            'var (var[0-9]+) = (var[0-9]+).(isUnsat\\(\\)|getModel\\(\\)|asList\\(\\)|addConstraint\\((var[0-9]+)\\));',
            line)
        if m != None:
            tl.add(lineDefs[m.group(1)])
    return tl


# Calculate the closure of all used definitions, starting with the top-level statements
def usedClosure(tl, deps):
    cl = set()
    st = set(tl)
    while cl.union(st) != cl:
        cl = cl.union(st)
        st = set()
        for (key, val) in deps.items():
            if set(val).intersection(cl) != set():
                st.add(key)
    return cl


# Keep only statements and definitions that are used
def filterUnused(used, trace):
    lineNumber = 1
    reduced = []
    for line in trace:
        if line.find('=') == -1 or lineNumber in used:
            reduced.append(line)
        lineNumber += 1
    return reduced


# Remove all definitions that are not used (recursively)
def removeDeadCode(trace):
    lineDefs = getLinesForDefinitions(trace)
    deps = buildDependencies(lineDefs, trace)
    tl = usedTopLevel(lineDefs, trace)
    cl = usedClosure(tl, deps)
    return filterUnused(cl, trace)


# We'll use multiple passes to reduce the size of the trace:
# 1. Read the trace
# 2. Remove unused code
# 3. Remove unnecessary toplevel commands
# 4. Loop: Remove aliasing (by duplicating the definitions)
# 5.    Loop: Reduce terms
# 6. Remove unused prover environments
if __name__ == '__main__':
    arg = sys.argv
    if not len(sys.argv) == 2:
        print('Expecting a path to a trace file as argument')
        exit(-1)

    path = Path(sys.argv[1])
    if not (path.is_file()):
        print(f'Could not find file "{path}"')
        exit(-1)

    # TODO Implement steps 3-6
    # TODO Check that the reduced trace still crashes

    trace = readTrace(path)
    for line in removeDeadCode(trace):
        print(line)

The idea is to run JavaSMT with solver.trace=true to collect a trace of the crash, and then use the script to reduce the trace. Since we're "crashing" (posssibly with a segfault) there doesn't seem to be a good way to do this in one go

[daniel-raffler]

I've added a new script that converts the traces from the tests to Smtlib and then tries them out on a solver. Here is how it can be used:

1. Patch SolverBasedTest0 to run tests only for one of the solvers

@Parameters(name = "{0}")
public static Solvers[] getAllSolvers() {
  return new Solvers[] {Solvers.CVC5};
}

2. Run the tests to generate the traces

cd java-smt
rm -r traces
ant tests

3. Convert the traces to Smtlib and run them on the solver

cd scripts
./tracingTest.sh cvc5 --incremental --fp-exp

The last step requires the cvc5 binaries to be installed on the system. Alternatively you may download the files from github and then call the script with a path to the cvc5 binary:

./tracingTest.sh ~/Downloads/cvc5-Linux-x86_64-shared/bin/cvc5 --incremental --fp-exp

[baierd]

Thank you very much for your hard work!

To answer your previous question about the script and address the current state; ideally we want all to be integrated into JavaSMT in a way that we can just set 1 (or multiple) options and get the result of all of this in a single file.
This will however require some additions/changes to JavaSMT i guess.

Could you make a full list of the steps that execute either a new script or JavaSMT and what would be needed to move the steps into JavaSMT (per point in the list). E.g. 1. execute script 1 (needed because ...), 2. execute JavaSMT from script 1 (to...)...

[daniel-raffler]

Thank you very much for your hard work!

Thanks!

To answer your previous question about the script and address the current state; ideally we want all to be integrated into JavaSMT in a way that we can just set 1 (or multiple) options and get the result of all of this in a single file. This will however require some additions/changes to JavaSMT i guess.

We could have the tracer output Smtlib directly. However, collecting the trace and reducing the trace will always have to be done in two separate steps as the original run might segfault. After that there just isn't any (safe) way to recover and start with the reduction step

The current workflow therefore looks like this:

1. Run the JavaSmt program with trace=true to collect the trace
2. Convert the trace to Smtlib
3. Verify it crashes with the solver binary
4. Reduce the *.smt2 file with ddSmt

As mentioned, we could get rid of the second step by outputting Smtlib directy. The downside is that this limits our options if some of the trace can't be expressed in Smtlib. It's hard to tell how often this will happen in practice, but I think that for now it's better to output the trace as a JavaSMT program first. That way, we could still try to write our own delta-debugger for JavaSMT if the conversion to Smtlib turns out to be a problem

Could you make a full list of the steps that execute either a new script or JavaSMT and what would be needed to move the steps into JavaSMT (per point in the list). E.g. 1. execute script 1 (needed because ...), 2. execute JavaSMT from script 1 (to...)...

You can find an example run in one of my earlier runs. It should work if you apply this little patch to your update_to_intermediate_javasmt_w_mathsat_5.6.15 branch for CPAchecker

Alternatively you could just run one of the tests in IntelliJ. Tracing is enabled by default on this branch, so there is no need to set any options. I've picked bvOne() from BitvectorFormulaTest as an example:

After the run the traces can be found in traces/BitvectorFormulaManagerTest. Here is my trace for CVC5:

var config = Configuration.builder().setOption("solver.tracefile", "traces/BitvectorFormulaManagerTest/trace_bvOne[CVC5]_16125334828171.java").build();
var logger = LogManager.createNullLogManager();
var notifier = ShutdownNotifier.createDummy();
var context = SolverContextFactory.createSolverContext(config, logger, notifier, SolverContextFactory.Solvers.CVC5);
var mgr = context.getFormulaManager();
var var0 = mgr.getBitvectorFormulaManager().makeVariable(FormulaType.getBitvectorTypeWithSize(1), "x1");
var var1 = mgr.getBitvectorFormulaManager().makeBitvector(1, 0L);
var var2 = mgr.getBitvectorFormulaManager().makeBitvector(1, 1L);
var var3 = mgr.getBitvectorFormulaManager().equal(var0, var1);
var var5 = context.newProverEnvironment();
var5.push();
var var6 = var5.addConstraint(var3);
var var7 = var5.isUnsat();
var5.close();
var var8 = mgr.getBitvectorFormulaManager().equal(var0, var2);
var var10 = context.newProverEnvironment();
var10.push();
var var11 = var10.addConstraint(var8);
var var12 = var10.isUnsat();
var10.close();
var var13 = mgr.getBitvectorFormulaManager().makeVariable(FormulaType.getBitvectorTypeWithSize(2), "x2");
var var14 = mgr.getBitvectorFormulaManager().makeBitvector(2, 0L);
var var15 = mgr.getBitvectorFormulaManager().makeBitvector(2, 1L);
var var16 = mgr.getBitvectorFormulaManager().equal(var13, var14);
var var18 = context.newProverEnvironment();
var18.push();
var var19 = var18.addConstraint(var16);
var var20 = var18.isUnsat();
var18.close();
var var21 = mgr.getBitvectorFormulaManager().equal(var13, var15);
var var23 = context.newProverEnvironment();
var23.push();
var var24 = var23.addConstraint(var21);
var var25 = var23.isUnsat();
var23.close();
var var26 = mgr.getBitvectorFormulaManager().makeVariable(FormulaType.getBitvectorTypeWithSize(4), "x4");
var var27 = mgr.getBitvectorFormulaManager().makeBitvector(4, 0L);
var var28 = mgr.getBitvectorFormulaManager().makeBitvector(4, 1L);
var var29 = mgr.getBitvectorFormulaManager().equal(var26, var27);
var var31 = context.newProverEnvironment();
var31.push();
var var32 = var31.addConstraint(var29);
var var33 = var31.isUnsat();
var31.close();
var var34 = mgr.getBitvectorFormulaManager().equal(var26, var28);
var var36 = context.newProverEnvironment();
var36.push();
var var37 = var36.addConstraint(var34);
var var38 = var36.isUnsat();
var36.close();
var var39 = mgr.getBitvectorFormulaManager().makeVariable(FormulaType.getBitvectorTypeWithSize(32), "x32");
var var40 = mgr.getBitvectorFormulaManager().makeBitvector(32, 0L);
var var41 = mgr.getBitvectorFormulaManager().makeBitvector(32, 1L);
var var42 = mgr.getBitvectorFormulaManager().equal(var39, var40);
var var44 = context.newProverEnvironment();
var44.push();
var var45 = var44.addConstraint(var42);
var var46 = var44.isUnsat();
var44.close();
var var47 = mgr.getBitvectorFormulaManager().equal(var39, var41);
var var49 = context.newProverEnvironment();
var49.push();
var var50 = var49.addConstraint(var47);
var var51 = var49.isUnsat();
var49.close();
var var52 = mgr.getBitvectorFormulaManager().makeVariable(FormulaType.getBitvectorTypeWithSize(64), "x64");
var var53 = mgr.getBitvectorFormulaManager().makeBitvector(64, 0L);
var var54 = mgr.getBitvectorFormulaManager().makeBitvector(64, 1L);
var var55 = mgr.getBitvectorFormulaManager().equal(var52, var53);
var var57 = context.newProverEnvironment();
var57.push();
var var58 = var57.addConstraint(var55);
var var59 = var57.isUnsat();
var57.close();
var var60 = mgr.getBitvectorFormulaManager().equal(var52, var54);
var var62 = context.newProverEnvironment();
var62.push();
var var63 = var62.addConstraint(var60);
var var64 = var62.isUnsat();
var62.close();
var var65 = mgr.getBitvectorFormulaManager().makeVariable(FormulaType.getBitvectorTypeWithSize(1000), "x1000");
var var66 = mgr.getBitvectorFormulaManager().makeBitvector(1000, 0L);
var var67 = mgr.getBitvectorFormulaManager().makeBitvector(1000, 1L);
var var68 = mgr.getBitvectorFormulaManager().equal(var65, var66);
var var70 = context.newProverEnvironment();
var70.push();
var var71 = var70.addConstraint(var68);
var var72 = var70.isUnsat();
var70.close();
var var73 = mgr.getBitvectorFormulaManager().equal(var65, var67);
var var75 = context.newProverEnvironment();
var75.push();
var var76 = var75.addConstraint(var73);
var var77 = var75.isUnsat();
var75.close();
context.close();

Now you could simply copy this code into a new JavaSMT project and run it. However, even for this simple test the trace is already close to 100 lines long, and generally traces can grow much larger. This is a problem as the JVM has a limit on the code size of a method, so traces larger than ~5000 lines will generally not compile. Even if we found some way around this limitation the traces would still be way too large to report to the developers if there is a bug in one of the solver. Because of this the next step is now to convert the JavaSMT trace to Smtlib:

cd java-smt/scripts
python3 -m venv .venv/
source .venv/bin/activate
pip install -r requirements.txt

./traceToSmtlib.py --save ../traces/BitvectorFormulaManagerTest/trace_bvOne\[CVC5\]_<TIMESTAMP>.java 

deactivate

Here is the output for our test. It's mostly a line-by-line translation of the earlier JavaSMT trace:

(set-logic ALL)
(set-option :interactive-mode true)
(set-option :produce-models true)
(set-option :global-declarations true)
(declare-const var0 (_ BitVec 1))
(define-const var1 (_ BitVec 1) ((_ int_to_bv 1) 0))
(define-const var2 (_ BitVec 1) ((_ int_to_bv 1) 1))
(define-const var3 Bool (= var0 var1))
(push 1)
(push 1)
(assert var3)
(check-sat)
(pop 1)
(pop 1)
(define-const var8 Bool (= var0 var2))
(push 1)
(push 1)
(assert var8)
(check-sat)
(pop 1)
(pop 1)
(declare-const var13 (_ BitVec 2))
(define-const var14 (_ BitVec 2) ((_ int_to_bv 2) 0))
(define-const var15 (_ BitVec 2) ((_ int_to_bv 2) 1))
(define-const var16 Bool (= var13 var14))
(push 1)
(push 1)
(assert var16)
(check-sat)
(pop 1)
(pop 1)
(define-const var21 Bool (= var13 var15))
(push 1)
(push 1)
(assert var21)
(check-sat)
(pop 1)
(pop 1)
(declare-const var26 (_ BitVec 4))
(define-const var27 (_ BitVec 4) ((_ int_to_bv 4) 0))
(define-const var28 (_ BitVec 4) ((_ int_to_bv 4) 1))
(define-const var29 Bool (= var26 var27))
(push 1)
(push 1)
(assert var29)
(check-sat)
(pop 1)
(pop 1)
(define-const var34 Bool (= var26 var28))
(push 1)
(push 1)
(assert var34)
(check-sat)
(pop 1)
(pop 1)
(declare-const var39 (_ BitVec 32))
(define-const var40 (_ BitVec 32) ((_ int_to_bv 32) 0))
(define-const var41 (_ BitVec 32) ((_ int_to_bv 32) 1))
(define-const var42 Bool (= var39 var40))
(push 1)
(push 1)
(assert var42)
(check-sat)
(pop 1)
(pop 1)
(define-const var47 Bool (= var39 var41))
(push 1)
(push 1)
(assert var47)
(check-sat)
(pop 1)
(pop 1)
(declare-const var52 (_ BitVec 64))
(define-const var53 (_ BitVec 64) ((_ int_to_bv 64) 0))
(define-const var54 (_ BitVec 64) ((_ int_to_bv 64) 1))
(define-const var55 Bool (= var52 var53))
(push 1)
(push 1)
(assert var55)
(check-sat)
(pop 1)
(pop 1)
(define-const var60 Bool (= var52 var54))
(push 1)
(push 1)
(assert var60)
(check-sat)
(pop 1)
(pop 1)
(declare-const var65 (_ BitVec 1000))
(define-const var66 (_ BitVec 1000) ((_ int_to_bv 1000) 0))
(define-const var67 (_ BitVec 1000) ((_ int_to_bv 1000) 1))
(define-const var68 Bool (= var65 var66))
(push 1)
(push 1)
(assert var68)
(check-sat)
(pop 1)
(pop 1)
(define-const var73 Bool (= var65 var67))
(push 1)
(push 1)
(assert var73)
(check-sat)
(pop 1)
(pop 1)

The smt trace can then be run on any solver:

~/Downloads/cvc5-Linux-x86_64-shared/bin/cvc5 --incremental ../traces/BitvectorFormulaManagerTest/trace_bvOne\[CVC5\]_16125334828171.smt2

Since there is no crash, there is nothing to debug and we're finished. Otherwise, the next step would be to use ddSMT to reduce the size of the trace, and then report the problem to the solver developers

Finally, the bash script tracingTest.sh is just for debugging. We could try to find a way to add it to the CI, or just remove it again before merging the tracer