Use goto-analyzer to add assumptions, assertions and code contracts

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

@@ -109,6 +109,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,29 @@
+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/analyses/ai_domain.h

@@ -45,6 +45,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "ai_history.h"
 
+#include <set>
+
 // forward reference the abstract interpreter interface
 class ai_baset;
 
@@ -155,15 +157,37 @@ class ai_domain_baset
   /// Simplifies the expression but keeps it as an l-value
   virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const;
 
-  /// Gives a Boolean condition that is true for all values represented by the
-  /// domain.  This allows domains to be converted into program invariants.
-  virtual exprt to_predicate(void) const
+  /// Gives a Boolean condition involving expression from the set that
+  /// is true for all of the states represented by the domain.  If the
+  /// set is empty then the domain can use any expressions in building
+  /// the condition.  This allows domains to be converted into program
+  /// invariants.
+  virtual exprt
+  to_predicate(const std::set<exprt> &, const namespacet &ns) const
   {
+    // Without knowing what the domain records this is the best that
+    // can be done.
     if(is_bottom())
       return false_exprt();
     else
       return true_exprt();
   }
+
+  /// A utility function to convert to generate a predicate without
+  /// grammar restrictions.
+  virtual exprt to_predicate(const namespacet &ns) const
+  {
+    std::set<exprt> empty;
+    return to_predicate(empty, ns);
+  }
+
+  /// to_predicate for a single expression.
+  virtual exprt to_predicate(const exprt &e, const namespacet &ns) const
+  {
+    std::set<exprt> single;
+    single.insert(e);
+    return to_predicate(single, ns);
+  }
 };
 
 // No virtual interface is complete without a factory!