Track hardness of solver queries

Introduces a functionality to track and collect the complexity of individual
solver queries. For SAT solvers we collect the number of clauses, literals, and
variables. The functionality matches solver queries to the SSA steps that
produced them. After running the solver, we produce a JSON report that matches
program line to GOTO instruction to SSA step to solver hardness.

At present the collection is command-line optional and only works with the
default SAT solver (minisat2). Extension to other SAT and SMT solvers should be
possible.

A simple regression test is included.

Note: the solver-hardness structure lives in the minisat2 and is accessible via
the interface of hardness-collector (which minisat2 inherits from). Hence to
find out if symex should collect the statistics one must try-cast `prop` to
`hardness-collector`. `prop` is part of the `solvert` but not directly
accessible from `decision-procedure`. So we also had to extend the interface
that initialises the SSA conversion (to include `prop` as well).

Author: petr-bauch

regression/CMakeLists.txt

@@ -60,3 +60,5 @@ if(WITH_MEMORY_ANALYZER)
   add_subdirectory(snapshot-harness)
   add_subdirectory(memory-analyzer)
 endif()
+
+add_subdirectory(solver-hardness)

regression/Makefile

@@ -30,6 +30,7 @@ DIRS = cbmc \
        goto-cc-file-local \
        linking-goto-binaries \
        symtab2gb \
+       solver-hardness \
        # Empty last line
 
 ifeq ($(OS),Windows_NT)

regression/solver-hardness/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_test_pl_tests(
+  "../chain.sh $<TARGET_FILE:cbmc>")

regression/solver-hardness/Makefile

@@ -0,0 +1,23 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+CBMC_EXE=../../../src/cbmc/cbmc
+
+test:
+	@../test.pl -e -p -c "../chain.sh $(CBMC_EXE)"
+
+tests.log: ../test.pl
+	@../test.pl -e -p -c "../chain.sh $(CBMC_EXE)"
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/solver-hardness/chain.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+
+cbmc=$1
+
+name=${*:$#}
+args=${*:2:$#-2}
+
+$cbmc ${name} ${args}
+CBMC_RETURN_CODE="$?"
+../parse_json.py "solver_hardness.json"
+exit ${CBMC_RETURN_CODE}

regression/solver-hardness/parse_json.py

@@ -0,0 +1,13 @@
+#!/usr/bin/env python
+
+import sys
+import json
+
+def main():
+  with open(sys.argv[1], "r") as json_file:
+    data = json.load(json_file)
+  print ("Valid JSON File")
+  print (json.dumps(data))
+
+if __name__ == "__main__":
+  main()

regression/solver-hardness/solver-hardness-simple/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main()
+{
+  int a;
+  int b;
+  assert(a + b < 10);
+  return 0;
+}

regression/solver-hardness/solver-hardness-simple/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--write-solver-stats-to "solver_hardness.json"
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.\d+\] line \d+ assertion a \+ b \< 10: FAILURE$
+^VERIFICATION FAILED$
+^Valid JSON File$
+\"SAT_hardness\": \{(\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+), (\"Clauses\": \d+|\"Variables\": \d+|\"Literals\": \d+)\}
+--
+^warning: ignoring

src/cbmc/cbmc_parse_options.cpp

@@ -460,6 +460,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     }
   }
 
+  if(cmdline.isset("write-solver-stats-to"))
+  {
+    options.set_option(
+      "write-solver-stats-to", cmdline.get_value("write-solver-stats-to"));
+  }
+
   if(cmdline.isset("beautify"))
     options.set_option("beautify", true);
 
@@ -1106,6 +1112,8 @@ void cbmc_parse_optionst::help()
     HELP_FLUSH
     " --verbosity #                verbosity level\n"
     HELP_TIMESTAMP
+    " --write-solver-stats-to json-file\n"
+    "                              collect the solver query complexity\n"
     "\n";
   // clang-format on
 }

src/cbmc/cbmc_parse_options.h

@@ -46,6 +46,7 @@ class optionst;
   OPT_REACHABILITY_SLICER \
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \
+  "(write-solver-stats-to):"  \
   "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
   "(object-bits):" \
   OPT_GOTO_CHECK \