Merge pull request diffblue#48 from diffblue/goto-analyzer-fixes

Goto analyzer fixes

Author: danpoe

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -26,6 +26,7 @@ Function: abstract_environmentt::eval
 
   Inputs:
    expr - the expression to evaluate
+   ns - the current namespace
 
  Outputs: The abstract_object representing the value of the expression
 
@@ -139,7 +140,7 @@ Function: abstract_environmentt::assign
    expr - the expression to assign to
    value - the value to assign to the expression
 
- Outputs: ?
+ Outputs: A boolean, true if the assignment has changed the domain.
 
  Purpose: Assign a value to an expression
 
@@ -274,34 +275,43 @@ bool abstract_environmentt::assign(
 Function: abstract_environmentt::assume
 
   Inputs:
-   expr - the expression inside the assume
+   expr - the expression that is to be assumed
+   ns - the current namespace
 
- Outputs: ?
+ Outputs: True if the assume changed the domain.
 
- Purpose: ?
+ Purpose: Reduces the domain to (an over-approximation) of the cases
+          when the the expression holds.  Used to implement assume
+          statements and conditional branches.
 
 \*******************************************************************/
 
 bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
 {
+  // We should only attempt to assume Boolean things
+  // This should be enforced by the well-structured-ness of the goto-program
+  assert(expr.type().id()==ID_bool);
+
+  // Evaluate the expression
   abstract_object_pointert res = eval(expr, ns);
-  std::string not_implemented_string=__func__;
-  not_implemented_string.append(" not implemented");
-  throw not_implemented_string;
-  // Need abstract_booleant
-#if 0
-  abstract_booleant *b = dynamic_cast<abstract_booleant>(res);
 
-  assert(b != NULL);
+  exprt possibly_constant = res->to_constant();
 
-  if (b->to_constant().is_false())
+  if (possibly_constant.id()!=ID_nil)  // I.E. actually a value
   {
-    make_bottom();
-    return true;
+    assert(possibly_constant.type().id()==ID_bool); // Should be of the right type
+
+    if (possibly_constant.is_false())
+    {
+      bool currently_bottom = get_is_bottom();
+      make_bottom();
+      return !currently_bottom;
+    }
   }
-  else
-    return false;
-#endif
+
+  // TODO - need a way of converting x==23 into an assign for the value of x
+  
+  return false;
 }
 
 
@@ -372,9 +382,9 @@ Function: abstract_environmentt::merge
   Inputs:
    env - the other environment
 
- Outputs: ?
+ Outputs: A Boolean, true when the merge has changed something
 
- Purpose: ?
+ Purpose: Computes the join between "this" and "b"
 
 \*******************************************************************/
 
@@ -466,7 +476,7 @@ Function: abstract_environmentt::havoc
   Inputs:
    havoc_string - debug string to track down havoc causing.
 
- Outputs:
+ Outputs: None
 
  Purpose: Set the domain to top
 
@@ -482,9 +492,9 @@ void abstract_environmentt::havoc(const std::string &havoc_string)
 
 Function: abstract_environmentt::make_top
 
-  Inputs:
+  Inputs: None
 
- Outputs:
+ Outputs: None
 
  Purpose: Set the domain to top
 
@@ -493,7 +503,6 @@ Function: abstract_environmentt::make_top
 void abstract_environmentt::make_top()
 {
   // since we assume anything is not in the map is top this is sufficient
-  // TODO: need a flag for bottom
   map.clear();
   is_bottom=false;
 }
@@ -502,9 +511,9 @@ void abstract_environmentt::make_top()
 
 Function: abstract_environmentt::make_bottom
 
-  Inputs:
+  Inputs: None
 
- Outputs:
+ Outputs: None
 
  Purpose: Set the domain to top
 
@@ -556,10 +565,10 @@ Function: abstract_environmentt::output
 
   Inputs:
    out - the stream to write to
-   ai - ?
-   ns - ?
+   ai - the abstract interpreter that contains this domain
+   ns - the current namespace
 
- Outputs:
+ Outputs: None
 
  Purpose: Print out all the values in the abstract object map
 

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -71,17 +71,15 @@ void variable_sensitivity_domaint::transform(
   case GOTO:
     {
       // TODO(tkiley): add support for flow sensitivity
-#if 0
-      if (flow_sensitivity == FLOW_SENSITIVE)
+      if (1) // (flow_sensitivity == FLOW_SENSITIVE)
       {
         locationt next=from;
         next++;
         if(next==to)
-          assume(not_exprt(instruction.guard));
+          abstract_state.assume(not_exprt(instruction.guard), ns);
         else
-          assume(instruction.guard);
+          abstract_state.assume(instruction.guard, ns);
       }
-#endif
     }
     break;
 
@@ -102,6 +100,8 @@ void variable_sensitivity_domaint::transform(
   case ASSERT:
     // Conditions on the program, do not alter the data or information
     // flow and thus can be ignored.
+    // Checking of assertions can only be reasonably done once the fix-point
+    // has been computed, i.e. after all of the calls to transform.
     break;
 
   case SKIP:
@@ -233,14 +233,16 @@ bool variable_sensitivity_domaint::merge(
 Function: variable_sensitivity_domaint::ai_simplify
 
   Inputs:
-   condition - the expression to evaluate to true or false
+   condition - the expression to simplify
    ns - the namespace
    lhs - is the expression on the left hand side
 
  Outputs: True if simplified the condition. False otherwise. condition
           will be updated with the simplified condition if it has worked
 
- Purpose: To resolve a condition down to a possibly known boolean value
+ Purpose: Use the information in the domain to simplify the expression
+          with respect to the current location.  This may be able to
+          reduce some values to constants.
 
 \*******************************************************************/
 

src/analyses/variable-sensitivity/variable_sensitivity_domain.h

@@ -4,6 +4,60 @@
 
  Author: Thomas Kiley, [email protected]
 
+There are different ways of handling arrays, structures, unions and
+pointers.  Our existing solution basically ignores them which is
+imprecise at best and out-right wrong at worst.  For one project we
+needed to do better.  We could have implemented a particular way of
+handling them in an existing domain, created a new one with it, etc.
+This would work but it means duplicate code and it is is inflexible when
+the same person / the next person comes along and says "actually, we
+really care about the pointer precision but less so the array so could
+you just ...".  Thus the idea was to do this properly:
+
+1. Build a "non-relational domain" and allow the abstractions used for
+individual variables to be different.
+
+2. Give the user the option of which abstractions are used for structs,
+unions, arrays and pointers.  These are the sensitivity options
+discussed above.
+
+3. Have the domain options control which kind of abstractions are used
+for the individual values, i.e. constants, intervals, etc.
+
+
+This is implemented in three parts:
+
+abstract_objectt : The base / interface for abstractions of a single
+variable.  The interface for these is effectively create (as top,
+bottom, from a constant or copy), transform, merge, convert to constant
+if possible.  Child classes add additional bits of interface, for
+example array abstractions need a "read element" and a "write element"
+method, structures need a "read field" and "write field", etc.  These
+objects are intended to be immutable and thus operations tend to produce
+pointers.  This is so that we can easily produce copy-on-write maps of
+them which we need for scaling and performance.  There are also children
+of these for the constant abstraction of one value, the interval
+abstraction of one value (to be implemented), etc.
+
+abstract_environment : This contains the map from variable names for
+abstract_objectt's (the "non-relational" part of the domain).  The map
+itself if copy-on-write for performance and scalability but this is all
+wrapped up nicely in @danpoe's sharing_map.  The interface here is
+evaluate (exprt -> abstract_objectt*), assign (name, abstract_objectt*
+-> bool), assume (exprt -> bool) and merge.  It has a factory to build
+abstract_objectt* from types or constants but apart from that, doesn't
+know anything about which actual abstract_objectt's are being used.  As
+long as program variables that are arrays have an abstract_objectt which
+has the array interface, and so on for structs, unions, etc. then the
+abstractions used for values can be freely mixed and matched in any way
+the user can get the factory to build.
+
+variable_sensitivity_domaint : Implements the ai_domain_baset interface
+using an abstract_environment.  The only real code here is the
+'transform' method which looks at the instruction type and converts that
+into calls to eval, assume, assign and merge.
+
+
 \*******************************************************************/
 #ifndef CPROVER_GOTO_ANALYZER_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
 #define CPROVER_GOTO_ANALYZER_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -4,6 +4,98 @@ Module: Goto-Analyser Command Line Option Processing
 
 Author: Daniel Kroening, [email protected]
 
+Goto-analyze is the tool front-end for CPROVER's classic style abstract
+interpretation analyses.  By "classic style" I mean, domains are C++
+objects, transformers are computed using C++ functions and the
+fix-points are computed by iteration.  This is in contrast to 2LS's
+approach where everything is computed using quantifier-elimination.
+
+The analyses are mostly in analyses/ and although they are used in other
+places in the code, the goal is that goto-analyze should eventually
+provide an executable front-end for all of them.
+
+There are a lot of different analyses and a lot of ways they can be
+used.  Goto-analyze has five, largely independent, sets of options:
+
+1. Task : What you do once you've computed the domains.
+2. Abstract interpreter : What kind of abstract interpretation you do.
+3. Domain : What domain you use.
+4. Sensitivity : How that domain handles things like arrays, pointers, etc.
+   (see variable_sensitivity_domain.h)
+5. Output : What you do with the results.
+
+Formally speaking, 2, 3 and 4 are an artificial distinction as they are
+all really parts of the "what domain" question.  However they correspond
+to parts of our code architecture, so ... they should stay.
+
+Ideally, the cross product of options should be supported but ... in
+practice there will always be ones that are not meaningful.  Those
+should give errors.  In addition there are some analyses which are
+currently stand alone as they don't fit directly in to this model.  For
+example the unwind bounds analysis, which is both the task, the abstract
+interpreter and the output.  Where possible these should be integrated /
+support the other options.  In the case of the unwind analysis this
+means the domain and it's sensitivity should be configurable.
+
+
+Task
+----
+
+Tasks are implemented by the relevant file in goto-analyze/static_*. At
+the moment they are each responsible for building the domain / using the
+other options.  As much as possible of this code should be shared.  Some
+of these inherit from messaget.  They all probably should.
+
+Show : Prints out the domains for inspection or further use.
+
+Verify : Uses the domain to check all assertions in the code, marking
+each one "SUCCESS" (the assertion always holds), "FAILURE if
+reachable" (the assertion never holds), "UNKNOWN" (the assertion may or
+may not hold).  This is implemented using domain_simplify().
+
+Simplify : Generates a new goto program with branch conditions,
+assertions, assumptions and assignments simplified using the information
+in the domain (again using domain_simplify()).  This task is intended to
+be used as a preprocessing step for other analysis.
+
+Invariants : (Not implemented yet) Use the domains to add assume()
+statements to the code giving invariants generated from the domain.
+These assumes don't reduce the space of possible executions; they make
+existing invariants explicit.  Again, intended as a preprocessing step.
+
+
+Abstract Interpreter
+--------------------
+
+This option is effectively about how we compute the fix-point(s) /
+which child class of ai_baset we use.  I.E.  ait<domainT> or
+concurrency_aware_ait<domainT>, etc.   For migrating / refactor /
+unifying with the pointer analysis code we might want a
+location_insensitive_ait<domainT> or something but this is not urgent.
+We will need a context_aware_ait<domainT>, quite possibly the one
+@danpoe has written elsewhere.
+
+
+Domain
+------
+
+Which child of ai_domain_baset we use to represent the abstract state at
+each location / implement the transformers.  I expect most of these will
+be non-relational (i.e. an abstract object for each variable) due to the
+cost of implementing effective non-relational domains in this style vs.
+using 2LS.  The exception might be equalities, which we could implement
+here.
+
+
+Output
+------
+
+Text, XML, JSON plus some others for specific domains such as dependence
+graphs in DOT format.
+
+
+
+
 \*******************************************************************/
 
 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H