Complexity graph

doc/cprover-manual/complexity-graph.md

@@ -0,0 +1,116 @@
+[CPROVER Manual TOC](../)
+
+## Complexity Graph
+
+This tool is meant to help decompose CBMC proofs.
+It does this by producing a control-flow graph that contains information about where CBMC may run into issues.
+
+```
+goto-instrument FILE.goto FLAGS
+```
+
+The recommended file to use is `FUNCTION_harness1.goto` which is produced from the Makefile provided in the starter kit. If this is not available, use `goto-cc` to compile all relevant source files into a `.goto` file.
+We recommend this file because it is produced before any program transformations are made, which can complicate the graph.
+
+## Relevant FLAGS
+
+  --show-complexity-graph FILE.dot
+  instructs CBMC to write the graph to the .dot file
+  This can be compiled to a PDF by using the command
+  ```
+  dot -Tpdf FILE.dot -o FILE.pdf
+  ```
+
+
+  --complexity-graph-roots FUNCTION-NAME
+  Instructs CBMC to generate the graph spanned by this function. This flag can be passed multiple times and produces one graph spanned by all roots. If no roots are provided, all functions in the provided source files will be used.
+  Typically this will be `FUNCTION_harness`.
+
+
+  --remove-function-body FUNCTION-NAME
+  Removes the body of a function, which has the effect of removing all outedges of that vertex from the graph.
+
+
+  --omit-function FUNCTION-NAME
+  Omits a function from the graph entirely. Useful for removing high-indegree sink nodes to reduce visual clutter.
+
+
+  --constant-propagator
+  Recommended to run for the reason that it simplifies the underlying program, and hence the graph.
+
+
+  --omit-function-pointers
+  Removes function pointer edges from the graph, which have a habit of producing visual clutter.
+
+
+  --add-library
+  Includes the CBMC library for functions like `malloc`, `free`, etc.
+
+  --complexity-graph-global-scores
+  Uses a more global notion of scoring, where the "global score" for a node is the number of paths to that node multiplied by the sum of the global scores of its children. 
+
+The following flags can be used with the main CBMC executable
+```
+cbmc FILE.goto FLAGS
+```
+
+  --show-complexity-graph-with-symex FILE.dot
+  Write the complexity graph with symbolic execution information to FILE.dot.
+
+
+  --show-complexity-graph-with-solver FILE.dot
+  Write the complexity graph with symbolic execution and solver formula information to FILE.dot.
+  This flag requires the addition of `--write-solver-stats-to FILE.out` to obtain solver formula information.
+
+
+  --complexity-graph-instructions
+  When used with '--show-complexity-graph-with-symex' or '--show-complexity-graph-with-solver' displays the instructions of the program that have a high cost in symbolic execution and/or the solver formula.
+
+## Reading the graph
+
+### Node shapes
+
+- Rectangluar nodes: normal functions
+- Elliptical nodes: private functions
+- Diamond nodes: functions with no body
+- Arrow-shaped nodes: function pointers
+- Pentagon: standard/CBMC library functions
+
+### Node colors
+
+The intensity of red coloring on a node is a display of its complexity relative to other nodes in the graph.
+
+When using `--show-complexity-graph-with-symex` with `--complexity-graph-instructions`, intensity of pink on instructions shows the complexity of that instruction in symbolic execution, and intensity of yellow shows the complexity of that instruction in the creation of the solver formula.
+
+
+## Sample interaction
+
+Suppose we have a function `foobar` and we'd like to do a proof for it.
+After creating a GOTO file `foobar_harness1.goto` with the starter kit or `goto-cc`, try the following
+
+```
+goto-instrument foobar_harness1.goto --show-complexity-graph graph.dot --complexity-graph-roots foobar
+```
+Followed by
+```
+dot -Tpdf graph.dot -o graph.pdf
+```
+
+This will display the call graph for foobar.
+The first step is to take steps to clean the graph.
+
+Likely, you can ignore function pointers at this point. See [this page](http://cprover.diffblue.com/md__home_travis_build_diffblue_cbmc_doc_architectural_restrict-function-pointer.html) for how to restrict function pointers - the information provided in the graph displays CBMC's sound overapproximation of what functions can be targets of which function pointers.
+
+Additionally, there may be some high-indegree functions in the graph that don't appear to be useful and just complicate the graph.
+Let's say one of those functions is `notuseful`.
+We can then run a new command
+```
+goto-instrument foobar_harness1.goto --show-complexity-graph graph.dot --complexity-graph-roots foobar --complexity-graph-omit-function-pointers --complexity-graph-omit-function notuseful
+```
+Which should provide a cleaner graph to inspect.
+
+
+When doing a proof, you should use information provided in the graph along with some domain knowledge about the codebase to decide where to decompose. See `doc/cprover-manual/contracts-functions.md` for a tutorial on proof decomposition using function contracts, which we refer to as abstracting a function.
+It's good to abstract functions that are complex. In the case that there is a simple function `g` that calls a complex function `f`, it may be better to abstract `g` if the contract is easier to write.
+A good way to approximate where a contract is easy to write is by how many memory locations a function can write to.
+

src/cbmc/cbmc_parse_options.cpp

@@ -58,6 +58,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/set_properties.h>
+#include <goto-programs/show_complexity_graph.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
@@ -334,8 +335,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("trace", true);
   }
 
+  options.set_option("symex-record-coverage", cmdline.get_values ("symex-record-coverage"));
   if(cmdline.isset("symex-coverage-report"))
   {
+    options.set_option("symex-record-coverage", true);
     options.set_option(
       "symex-coverage-report",
       cmdline.get_value("symex-coverage-report"));
@@ -372,6 +375,51 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   parse_solver_options(cmdline, options);
 }
 
+void set_complexity_graph_options (const cmdlinet &cmdline, optionst &options) {
+  if (cmdline.isset ("show-complexity-graph-with-symex")
+      || cmdline.isset ("show-complexity-graph-with-solver")) {
+    options.set_option("symex-record-coverage", true);
+  }
+
+  options.set_option ("show-complexity-graph", cmdline.get_values ("show-complexity-graph"));
+  options.set_option ("show-complexity-graph-with-symex", cmdline.get_values ("show-complexity-graph-with-symex"));
+  options.set_option ("show-complexity-graph-with-solver", cmdline.get_values ("show-complexity-graph-with-solver"));
+  if (cmdline.isset ("complexity-graph-root")) 
+  {
+    std::stringstream stream;
+    for (const std::string &val : cmdline.get_values("complexity-graph-root")) 
+    {
+      stream << val << ",";
+    }
+    options.set_option ("complexity-graph-roots", stream.str());
+  }
+
+  if (cmdline.isset ("complexity-graph-omit-function")) 
+  {
+    std::stringstream stream;
+    for (const std::string &val : cmdline.get_values("complexity-graph-omit-function")) 
+    {
+      stream << val << ",";
+    }
+    options.set_option ("complexity-graph-omit-function", stream.str());
+  }
+
+  if (cmdline.isset ("complexity-graph-global-scores")) 
+  {
+    options.set_option ("complexity-graph-global-scores", true);
+  }
+
+  if (cmdline.isset ("complexity-graph-omit-function-pointers")) 
+  {
+    options.set_option ("complexity-graph-omit-function-pointers", true);
+  }
+
+  if (cmdline.isset ("complexity-graph-instructions")) 
+  {
+    options.set_option ("complexity-graph-instructions", true);
+  }
+}
+
 /// invoke main modules
 int cbmc_parse_optionst::doit()
 {
@@ -499,6 +547,8 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_SUCCESS;
   }
 
+  set_complexity_graph_options (cmdline, options);
+
   int get_goto_program_ret =
     get_goto_program(goto_model, options, cmdline, ui_message_handler);
 
@@ -635,6 +685,7 @@ int cbmc_parse_optionst::doit()
       verifier = util_make_unique<
         all_properties_verifier_with_trace_storaget<multi_path_symex_checkert>>(
         options, ui_message_handler, goto_model);
+      // TODO: this is the branch triggered by default
     }
   }
   else
@@ -894,6 +945,8 @@ void cbmc_parse_optionst::help()
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show loaded symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    HELP_SHOW_COMPLEXITY_GRAPH
+    HELP_SHOW_COMPLEXITY_GRAPH_CBMC
     HELP_VALIDATE
     "\n"
     "Program instrumentation options:\n"

src/cbmc/cbmc_parse_options.h

@@ -51,6 +51,9 @@ class optionst;
   OPT_SOLVER \
   OPT_STRING_REFINEMENT_CBMC \
   OPT_SHOW_GOTO_FUNCTIONS \
+  "(symex-record-coverage)" \
+  OPT_COMPLEXITY_GRAPH \
+  OPT_COMPLEXITY_GRAPH_CBMC \
   OPT_SHOW_PROPERTIES \
   "(show-symbol-table)(show-parse-tree)" \
   "(drop-unused-functions)" \

src/goto-checker/multi_path_symex_checker.cpp

@@ -21,6 +21,8 @@ Author: Daniel Kroening, Peter Schrammel
 #include "counterexample_beautification.h"
 #include "goto_symex_fault_localizer.h"
 
+#include <goto-programs/show_complexity_graph.h>
+
 multi_path_symex_checkert::multi_path_symex_checkert(
   const optionst &options,
   ui_message_handlert &ui_message_handler,
@@ -31,6 +33,103 @@ multi_path_symex_checkert::multi_path_symex_checkert(
 {
 }
 
+// generates a complexity graph associated with the given query,
+// possibly with symex and SAT formula information.
+void generate_goto_dot (const abstract_goto_modelt &goto_model,
+                        const symex_bmct &symex,
+                        const optionst &options,
+                        ui_message_handlert &ui_message_handler,
+                        const goto_symex_property_decidert &property_decider,
+                        const std::string &type) 
+{
+  const std::string path = options.get_option(type);
+  if (!path.empty()) 
+  {
+    const auto &goto_functions = goto_model.get_goto_functions();
+
+    messaget msg(ui_message_handler);
+    const namespacet ns(goto_model.get_symbol_table());
+    const auto sorted = goto_functions.sorted();
+
+    const symex_coveraget &symex_coverage = symex.get_coverage();
+    std::map<goto_programt::const_targett, symex_infot> instr_symex_info;
+    std::map<goto_programt::const_targett, solver_infot> instr_solver_info;
+
+    // populate instr_symex_info
+    for(const auto &fun : sorted) 
+    {
+      const bool has_body = fun->second.body_available();
+
+      if (has_body) 
+      {
+        const goto_programt &body = fun->second.body;
+        forall_goto_program_instructions(from, body) 
+        {
+          const goto_programt::const_targetst to_list = symex_coverage.coverage_to (from);
+          size_t total_steps = 0;
+          double total_duration = 0.0;
+          for (goto_programt::const_targett to : to_list) 
+          {
+            total_steps += symex_coverage.num_executions(from, to);
+            total_duration += symex_coverage.duration(from, to);
+          }
+
+          symex_infot info;
+          info.steps = total_steps;
+          info.duration = total_duration;
+
+          instr_symex_info.insert ({from, info});
+        }
+      }
+    }
+
+    // populate instr_solver_info
+    with_solver_hardness(
+      property_decider.get_decision_procedure(),
+      [&instr_solver_info](solver_hardnesst &solver_hardness) 
+        {
+        // source: solver_hardness.cpp solver_hardnesst::produce_report
+        const std::vector<std::unordered_map<solver_hardnesst::hardness_ssa_keyt, solver_hardnesst::sat_hardnesst>> &hardness_stats = solver_hardness.get_hardness_stats();
+        for(std::size_t i = 0; i < hardness_stats.size(); i++) 
+        {
+          const auto &ssa_step_hardness = hardness_stats[i];
+          for(const auto &key_value_pair : ssa_step_hardness) 
+          {
+            auto const &ssa = key_value_pair.first;
+            auto const &hardness = key_value_pair.second;
+            const goto_programt::const_targett target = ssa.pc;
+
+            auto ensure_exists = instr_solver_info.find (target);
+            if (ensure_exists == instr_solver_info.end()) 
+            {
+              solver_infot solver_info;
+              instr_solver_info.insert ({target, solver_info});
+            }
+
+            auto entry = instr_solver_info.find (target);
+            solver_infot &solver_info = entry->second;
+            solver_info.clauses += hardness.clauses;
+            solver_info.literals += hardness.literals;
+            solver_info.variables += hardness.variables.size();
+          }
+        }
+      });
+
+    if (type == "show-complexity-graph") 
+    {
+      show_complexity_graph(options, goto_model, path, ui_message_handler);
+    } else if (type == "show-complexity-graph-with-symex") 
+    {
+      show_complexity_graph(options, goto_model, path, ui_message_handler, 
+                            instr_symex_info);
+    } else if (type == "show-complexity-graph-with-solver") 
+    {
+      show_complexity_graph(options, goto_model, path, ui_message_handler, 
+                            instr_symex_info, instr_solver_info);
+    } 
+  }
+}
+
 incremental_goto_checkert::resultt multi_path_symex_checkert::
 operator()(propertiest &properties)
 {
@@ -46,7 +145,12 @@ operator()(propertiest &properties)
   // we haven't got an equation yet
   if(!equation_generated)
   {
+
+    generate_goto_dot(goto_model, symex, options, ui_message_handler, property_decider, "show-complexity-graph");
+
     generate_equation();
+
+    generate_goto_dot(goto_model, symex, options, ui_message_handler, property_decider, "show-complexity-graph-with-symex");
 
     output_coverage_report(
       options.get_option("symex-coverage-report"),
@@ -67,6 +171,8 @@ operator()(propertiest &properties)
 
   run_property_decider(result, properties, solver_runtime);
 
+  generate_goto_dot(goto_model, symex, options, ui_message_handler, property_decider, "show-complexity-graph-with-solver");
+
   return result;
 }