debugging

Debugging

Concolic execution logs

The binary logs of each concolic execution are stored in the disk under the temp directory. We create a sub-directory for each execution. It contains one sub-directory for the logs of each process, and the file with the combined logs of all processes.

Here is an example tree structure of the logs directory:

temp
├── execexec1
│   ├── run.trace
│   └── traces
│       └── trace-0.3584589051.1832910849.258744
│           └── proc-0.86.0
├── execexec2
│   ├── run.trace
│   └── traces
│       └── trace-0.3584589051.1832910849.259053
│           └── proc-0.101.0
├── execexec3
│   ├── run.trace
│   └── traces
│       └── trace-0.3584589051.1832910849.259248
│           └── proc-0.112.0
└── execexec4
    ├── run.trace
    └── traces
        └── trace-0.3584589051.1832910849.259407
            └── proc-0.123.0

These logs are normally deleted before CutEr exits. In order to preserve them, pass the --debug_keep_traces flag.

./cuter example foo11 '[[17]]' -r -d 5 --debug-keep-traces

Since, they are binary logs, you can use priv/cuter_print.py to view a human-readable representation.

./priv/cuter_print.py temp/execexec1/run.trace

SMT logs

CutEr starts a number of solver Erlang processes that are tasked to interface with the SMT solvers and check the satisfiability of constraints. Every invocation to a solver can be recorded for debugging. In order to record the SMT logs, pass the -ds flag.

./cuter example foo11 '[[17]]' -r -d 5 -ds

Once CutEr exits, you can find one log file per solver invocation in the current directory.

.
├── smt.log.00001
├── smt.log.00002
├── smt.log.00003
├── smt.log.00004
├── smt.log.00005
├── smt.log.00006
├── smt.log.00007

Each log files contains the SMT commands that we sent to the solver, and its reponses. You can re-run them directly.

> z3 -smt2 -T:2 smt.log.00001 
sat
((|0.4243423039.3941597187.11360| (list (tc (int 43) tn))))