Add a task to goto-analyzer to instrument the program with invariants

doc/cprover-manual/goto-analyzer.md

@@ -49,16 +49,21 @@ goto-analyzer  --verify --three-way-merge --vsd --vsd-values set-of-constants --
 
 I want to discharge obvious conditions and remove unreachable code:
 ```
-goto-analyzer --simplify out.gb --three-way-merge --vsd
+goto-analyzer --simplify out.gb --three-way-merge --vsd program.c
 ```
 
 
 I want to build a dependency graph:
 ```
-goto-analyzer --show --dot depgraph.dot --dependence-graph-vs
+goto-analyzer --show --dot depgraph.dot --dependence-graph-vs program.c
 ```
 
 
+I want to generate code contracts:
+```
+goto-analyzer --instrument out.gb --instrument-targets requires,ensures,function_start,function_end,backwards_goto_target --vsd --verbosity 9 program.c
+```
+
 
 ## Task
 
@@ -106,6 +111,45 @@ domain which can result in a second (or more) runs giving
 simplification.  Submitting bug reports for these is helpful but they
 may not be viable to fix.
 
+`--instrument output_file.gb`
+: Produces a new version of the GOTO binary in which
+the abstract domains have been used to insert annotations, such as assertios
+or assumptions.  If everything is working correctly these should always
+be true because they are implied by the program and are an overapproximation.
+However they can be useful for a number of reasons.  Assertions can be
+used to test the results of goto-analyze against another tool.
+Assumptions can be useful as auxilliary constraints to help other
+tools or to provide better approximations of parts of the program.
+The exact instrumentation depends on the domain.
+
+`--instrument-targets`
+: A comma separated list of where in the program instrumentation should
+be added and what kind of instrumentation should be inserted.
+Available locations are `function_start`, `function_end`, `function_call`
+(before function calls), `function_return` (after function calls),
+`any_goto_target`, `backwards_goto_target`, `after_goto_not_taken`,
+`requires` and `ensures`.  If just the locations is used, assumptions
+will be inserted apart from requires and assumes which add the
+corresponding code contracts.  If the location is given followed by
+`=assume`, `=assert` or `=nothing` then assumptions, assertions or
+nothing is inserted.  A little care is necessary when using contracts
+generated by `goto-analyzer`.  The `requires` contract is an
+over-approximations of the calling context in the analyzed program.
+So if the function has flags (read, write, append, etc.) but only one
+set is used in the program then the `requires` contract may well
+include that specific set of flags.  In that sense what is generated
+is an over-approximation (i.e. a weakening or less restrictive
+version) of the strongest pre-condition that would work for the
+program you have analysed.  In practice you may want to weaken it
+further so your verification results are more general.  Likewise the
+`ensures` contract is an over-approximation of what the function does
+in the analyzed program.  If part of the functionality of the function
+is not used then it may not be in the generated contract.  In the
+example of flags above, if the program only uses one set of flags, the
+`ensures` contract may not include changes that are possible using
+other sets of flags.  Again, it may be desirable to weaken the
+generated contract so it can be used more generally.
+
 `--unreachable-instructions`
 : Lists which instructions have a domain which is bottom
 (i.e. unreachable).  If `--function` has been used to set the program

doc/man/goto-analyzer.1

@@ -103,6 +103,28 @@ may not be viable to fix.
 Do not remove instructions from which no
 property can be reached (use with \fB\-\-simplify\fR).
 .TP
+\fB\-\-instrument\fR \fIfile_name\fR
+Writes a new version of the input program to \fIfile_name\fR in which
+the abstract domains have been used to insert annotations, such as assertios
+or assumptions.  If everything is working correctly these should always
+be true because they are implied by the program and are an overapproximation.
+However they can be useful for a number of reasons.  Assertions can be
+used to test the results of goto-analyze against another tool.
+Assumptions can be useful as auxilliary constraints to help other
+tools or to provide better approximations of parts of the program.
+The exact instrumentation depends on the domain.
+.TP
+\fB\-\-instrument\-targets\fR
+A comma separated list of where in the program instrumentation should
+be added and what kind of instrumentation should be inserted.
+Available locations are function_start, function_end, function_call
+(before function calls), function_return (after function calls),
+any_goto_target, backwards_goto_target, after_goto_not_taken, requires
+and ensures.  If just the locations is used, assumptions will be
+inserted apart from requires and assumes which add the corresponding
+code contracts.  If the location is given followed by =assume, =assert or
+=nothing then assumptions, assertions or nothing is inserted.
+.TP
 \fB\-\-unreachable\-instructions\fR
 Lists which instructions have a domain which is bottom
 (i.e. unreachable).  If \fB\-\-function\fR has been used to set the program

regression/goto-analyzer/instrument-basic/after_goto_not_taken.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--instrument out.gb --instrument-targets after_goto_not_taken --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting example_function\nInstruction \d+ because after_goto_not_taken... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$
+--
+^warning: ignoring
+--
+Testing instrumenting at after gotos that are not taken (i.e. the "other" branch that is not a goto_target)
+
+
+

regression/goto-analyzer/instrument-basic/any_goto_target.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--instrument out.gb --instrument-targets any_goto_target --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting example_function\nInstruction \d+ because any_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption\nInstruction \d+ because any_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1 ∧ \(10 ≤ example_function::1::1::i ∧ example_function::1::1::i ≤ max_value\)... added as assumption$
+--
+^warning: ignoring
+--
+Testing instrumenting at goto targets
+
+

regression/goto-analyzer/instrument-basic/assertions.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--instrument out.gb --instrument-targets function_call=assert,function_start=assume,function_end=assert,function_return=assume --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting main\nInstruction \d+ because function_return... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption\nInstruction \d+ because function_end... single history... condition is main#return_value = 0 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assertion\nInstruction \d+ because function_start... single history... condition is true_from_calling_context = 0 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption\nInstruction \d+ because function_call... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assertion$
+^Instrumenting example_function\nInstruction \d+ because function_end... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assertion\nInstruction \d+ because function_start... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$
+--
+^warning: ignoring
+--
+Testing the addition of assertions in a way that mimics the use of contracts
+
+

regression/goto-analyzer/instrument-basic/backwards_goto_target.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--instrument out.gb --instrument-targets backwards_goto_target --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting example_function\nInstruction \d+ because backwards_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$
+--
+^warning: ignoring
+--
+Testing instrumenting at backwards goto targets
+
+

regression/goto-analyzer/instrument-basic/default.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--instrument out.gb --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting main\nInstruction \d+ because function_start... single history... condition is true_from_calling_context = 0 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption\nInstruction \d+ because function_return... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$
+^Instrumenting example_function\nInstruction \d+ because function_start... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption\nInstruction \d+ because backwards_goto_target... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$
+--
+^warning: ignoring
+--
+Testing the default options of instrumentation with goto-analyze
+

regression/goto-analyzer/instrument-basic/ensures.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--instrument out.gb --instrument-targets ensures --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting example_function\nAdd ensures contract... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as contract$
+--
+^warning: ignoring
+--
+Testing instrumenting add ensures contract
+

regression/goto-analyzer/instrument-basic/function_call.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--instrument out.gb --instrument-targets function_call --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting main\nInstruction \d+ because function_call... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$
+--
+^warning: ignoring
+--
+Testing instrumenting at function call
+
+

regression/goto-analyzer/instrument-basic/function_end.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--instrument out.gb --instrument-targets function_end --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting main\nInstruction \d+ because function_end... single history... condition is main#return_value = 0 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$
+^Instrumenting example_function\nInstruction \d+ because function_end... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$
+--
+^warning: ignoring
+--
+Testing instrumenting at the function end
+
+

regression/goto-analyzer/instrument-basic/function_return.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--instrument out.gb --instrument-targets function_return --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting main\nInstruction \d+ because function_return... single history... condition is main::1::argument_input = 1 ∧ true_from_calling_context = 1 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$
+--
+^warning: ignoring
+--
+Testing instrumenting at function return
+
+

regression/goto-analyzer/instrument-basic/function_start.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--instrument out.gb --instrument-targets function_start --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting main\nInstruction \d+ because function_start... single history... condition is true_from_calling_context = 0 ∧ \(0 ≤ main::argc ∧ main::argc ≤ max_value\)... added as assumption$
+^Instrumenting example_function\nInstruction \d+ because function_start... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as assumption$
+--
+^warning: ignoring
+--
+Testing instrumenting at the function start
+
+

regression/goto-analyzer/instrument-basic/main.c

@@ -0,0 +1,26 @@
+int true_from_calling_context = 0;
+
+int example_function(int argument) {
+  int local = argument + 1;
+  int location = 1;
+
+  for (int i = 0; i < 10; ++i) {
+    location = 2;
+    ++local;
+  }
+
+  location = 3;
+  ++local;
+
+  return location + local;
+}
+
+int main(int argc, char **argv) {
+  true_from_calling_context = 1;
+
+  int argument_input = 1;
+
+  int ret = example_function(argument_input);
+
+  return 0;
+}

regression/goto-analyzer/instrument-basic/requires.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--instrument out.gb --instrument-targets requires --verbosity 9 --vsd
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+^Instrumenting example_function\nAdd requires contract... single history... condition is example_function::argument = 1 ∧ true_from_calling_context = 1... added as contract$
+--
+^warning: ignoring
+--
+Testing instrumenting add requires contract
+
+
+

src/goto-analyzer/Makefile

@@ -5,6 +5,7 @@ SRC = goto_analyzer_languages.cpp \
       taint_parser.cpp \
       unreachable_instructions.cpp \
       show_on_source.cpp \
+      static_instrument.cpp \
       static_show_domain.cpp \
       static_simplifier.cpp \
       static_verifier.cpp \

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -34,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "build_analyzer.h"
 #include "show_on_source.h"
+#include "static_instrument.h"
 #include "static_show_domain.h"
 #include "static_simplifier.h"
 #include "static_verifier.h"
@@ -160,6 +161,18 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
       "simplify-slicing",
       !(cmdline.isset("no-simplify-slicing")));
   }
+  else if(cmdline.isset("instrument"))
+  {
+    if(cmdline.get_value("instrument") == "-")
+      throw invalid_command_line_argument_exceptiont(
+        "cannot output goto binary to stdout", "--instrument");
+
+    options.set_option("instrument", true);
+    options.set_option("outfile", cmdline.get_value("instrument"));
+    options.set_option("general-analysis", true);
+    options.set_option(
+      "instrument-targets", cmdline.get_value("instrument-targets"));
+  }
   else if(cmdline.isset("show-intervals"))
   {
     // For backwards compatibility
@@ -623,6 +636,24 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
       result = static_simplifier(
         goto_model, *analyzer, options, ui_message_handler, out);
     }
+    else if(options.get_bool_option("instrument"))
+    {
+      PRECONDITION(!outfile.empty() && outfile != "-");
+      output_stream.close();
+      output_stream.open(outfile, std::ios::binary);
+      if(options.is_set("instrument-targets") &&
+         options.get_option("instrument-targets") != "")
+      {
+        result = static_instrument(
+          goto_model, *analyzer, options.get_option("instrument-targets"), ui_message_handler, out);
+      }
+      else
+      {
+        // A reasonably sane set of defaults
+        result = static_instrument(
+          goto_model, *analyzer, "function_start=assume,function_return=assume,backwards_goto_target=assume", ui_message_handler, out);
+      }
+    }
     else if(options.get_bool_option("unreachable-instructions"))
     {
       result = static_unreachable_instructions(goto_model,
@@ -705,6 +736,8 @@ void goto_analyzer_parse_optionst::help()
     " program\n"
     " {y--no-simplify-slicing} \t do not remove instructions from which no"
     " property can be reached (use with {y--simplify})\n"
+    " {y--instrument} {ufile_name} \t use the abstract domains to generate annotations\n"
+    " {y--instrument-targets} {ulist} \t where to annotate and what annotations to use\n"
     " {y--unreachable-instructions} \t list dead code\n"
     " {y--unreachable-functions} \t list functions unreachable from the entry"
     " point\n"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -108,9 +108,14 @@ class optionst;
 #define GOTO_ANALYSER_OPTIONS_TASKS \
   "(show)(verify)(simplify):" \
   "(show-on-source)" \
+  "(instrument):" \
   "(unreachable-instructions)(unreachable-functions)" \
   "(reachable-functions)"
 
+#define GOTO_ANALYZER_OPTIONS_TASKS_CONFIG \
+  "(no-simplify-slicing)" \
+  "(instrument-targets):" \
+
 #define GOTO_ANALYSER_OPTIONS_AI \
   "(recursive-interprocedural)" \
   "(three-way-merge)" \
@@ -158,7 +163,7 @@ class optionst;
   OPT_TIMESTAMP \
   OPT_VALIDATE \
   GOTO_ANALYSER_OPTIONS_TASKS \
-  "(no-simplify-slicing)" \
+  GOTO_ANALYZER_OPTIONS_TASKS_CONFIG \
   "(show-intervals)(show-non-null)" \
   GOTO_ANALYSER_OPTIONS_AI \
   "(location-sensitive)(concurrent)" \