Merge pull request #5266 from hannes-steffenhagen-diffblue/feature/solver-hardness

Collect complexity statistics of solver queries

Author: hannes-steffenhagen-diffblue

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);
 
@@ -1109,6 +1115,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 \