sosy-lab
Add a new delegate to allow API tracing
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 https://github.com/sosy-lab/java-smt/pull/505#issuecomment-3602201543
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 https://github.com/sosy-lab/java-smt/pull/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
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
Related PRs:
- https://github.com/sosy-lab/java-smt/pull/507
- https://github.com/sosy-lab/java-smt/pull/508
- https://github.com/sosy-lab/java-smt/pull/509
- https://github.com/sosy-lab/java-smt/pull/510
@kfriedberger Please be careful when pushing changes to this branch. It's fine for now, but I still have quite a few unpublished changes and don't want to run into merge conflicts 😅
I find this branch quite interesting and was just playing around with it yesterday. I wished for such a tracing layer some years ago, as it would simplify debugging from other tools, such as CPAchecker, and could help with bug-reports. Some SMT solvers, such as Z3, provide tracing on their side, too.
I try to keep my changes small to avoid conflicts, or open other PRs, just like you.
For the delta-debugger script, you can either add it in a new directory scripts/ or under doc/examples/. We will not package it into any released JAR file, but can keep it as part of this repository, until the scripts grow further and can be moved into their own project.
I find this branch quite interesting and was just playing around with it yesterday. I wished for such a tracing layer some years ago, as it would simplify debugging from other tools, such as CPAchecker, and could help with bug-reports. Some SMT solvers, such as Z3, provide tracing on their side, too.
I try to keep my changes small to avoid conflicts, or open other PRs, just like you.
For the delta-debugger script, you can either add it in a new directory
scripts/or underdoc/examples/. We will not package it into any released JAR file, but can keep it as part of this repository, until the scripts grow further and can be moved into their own project.
Thanks! I've merged most of my outstanding commits now. The rest is just for integrating the other PRs that are still open.
I also added the python script to reduce the trace under scripts now. It's fine if this isn't shipped to users. They could just send their traces to us and we'll then have a closer look
Since the traces were still much too large I've now added a script to convert JavaSMT traces into SMTLIB traces. The idea is to first convert the trace and then use a delta-debugger like ddSmt to reduce the size of the SMTLIB trace. While this won't work for all traces, it does save us from having to write our own delta-debugger for JavaSMT traces. If there is a bug in a solver we generally have multiple runs in CPAchecker that trigger the bug, and there is hope that at least one of them can be successfully converted to SMTLIB. Should this turns out to be too restrictive in practice we may still add our own delta-debugger for JavaSMT at a later point
Example workflow for debugging https://github.com/sosy-lab/java-smt/issues/481:
- Run CPAchecker with tracing enabled
daniel@notebook:~/workspace/cpachecker$ bin/cpachecker --lassoRankerAnalysis --option solver.trace=true --option solver.tracefile=traces/trace_%s.java --spec test/programs/benchmarks/properties/termination.prp test/programs/benchmarks/termination-crafted/NonTermination3-2.c
- Translate the JavaSMT trace to SMTLIB
(.venv) daniel@notebook:~/workspace/java-smt/scripts$ ./traceToSmtlib.py ../../cpachecker/output/trace/traceXXX.java > ~/trace.smt2
- Check the trace crashes
daniel@notebook:~/Downloads/mathsat-5.6.14-linux-x86_64/bin$ ./mathsat ~/trace.smt2
- Reduce with ddSmt
daniel@notebook:~/workspace/ddSMT/bin$ ./ddsmt -v -j 4 --match-out '(error "Invalid model")' ~/trace.smt2 ~/reduced.smt2 ~/Downloads/mathsat-5.6.14-linux-x86_64/bin/mathsat
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:
- Patch
SolverBasedTest0to run tests only for one of the solvers
@Parameters(name = "{0}")
public static Solvers[] getAllSolvers() {
return new Solvers[] {Solvers.CVC5};
}
- Run the tests to generate the traces
cd java-smt
rm -r traces
ant tests
- 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
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...)...
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:
- Run the JavaSmt program with
trace=trueto collect the trace - Convert the trace to Smtlib
- Verify it crashes with the solver binary
- Reduce the
*.smt2file 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
I believe this is ready for review now
The approach now uses a two step process: We first run the program with trace=true to generate a JavaSMT trace and then use a script to convert this trace into SMTLIB output. This then allows us to use an existing delta-debugger like ddSmt to reduce the size of the SMTLIB file, as the trace would otherwise grow fairly large
Some examples for how to use the tracing mode can be found in my earlier comments here and here. Notice that traces are now no longer generated automatically for the tests. So the second example requires you to first revert 3068d81 and ce46f96
The last CI run with tracing enabled can be found here. On CVC5, MathSAT and Z3 most of the test are passing just fine. Other solvers still have more issues, mostly due to limitations in the visitor and heavy formula rewriting
Test results with tracing enabled:
The tracing delegate now supports all formula managers in JavaSMT. Trace translation to SMTLIB is still more limited and we don't support enumerations, strings or separation logic at this point. However, these could easily be added. Translation to SMTLIB is also not possible if more than one SolverContext is needed, or if multiple ProverEnvironments are used at the same time (sequential use is fine)
For testing purposes I did run part of svcomp in CPAchecker with tracing enabled. You can find the results here. The largest issue is the lack of support for bvextract while tracing. However, this can be fixed later, once we figured out how to handle indexed functions in JavaSMT. Other than that there were no new exceptions and the generated traces seem to run fine on MathSAT
@baierd, @kfriedberger Is there anything that is still missing from this PR?