Makes code contracts use goto_rw for write sets

This change replaces the use of local_may_alias analysis in code
contracts with the more accurate goto_rw analysis. These analyses
are used to find the set of variables written to by a loop or
function so that we know which variables to make nondeterministic
when abstracting out those pieces of code.

Author: klaas

regression/contracts/function_check_05/test.desc

@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 main.c
 --check-code-contracts
 ^\[main.assertion.1\] assertion y == 0: FAILURE$
 ^\[main.assertion.2\] assertion z == 1: SUCCESS$
 ^\[foo.1\] : SUCCESS$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 --
 --
-Contract checking does not properly havoc function calls.

src/goto-instrument/code_contracts.cpp

@@ -17,16 +17,18 @@ Date: February 2016
 #include <util/c_types.h>
 #include <util/expr_iterator.h>
 #include <util/fresh_symbol.h>
+#include <util/make_unique.h>
 #include <util/replace_symbol.h>
 
 #include <goto-programs/remove_skip.h>
 
-#include <analyses/local_may_alias.h>
+#include <analyses/goto_rw.h>
 
 #include <linking/static_lifetime_init.h>
 
+#include <pointer-analysis/value_set_analysis_fi.h>
+
 #include "loop_utils.h"
-#include "function_modifies.h"
 
 enum class contract_opst { APPLY, CHECK };
 
@@ -56,12 +58,12 @@ class code_contractst
 
   void apply_contract(
     goto_programt &goto_program,
-    const local_may_aliast &local_may_alias,
+    value_setst &value_sets,
     goto_programt::targett target);
 
   void apply_invariant(
     goto_functionst::goto_functiont &goto_function,
-    const local_may_aliast &local_may_alias,
+    value_setst &value_sets,
     const goto_programt::targett loop_head,
     const loopt &loop);
 
@@ -72,7 +74,7 @@ class code_contractst
 
   void check_apply_invariant(
     goto_functionst::goto_functiont &goto_function,
-    const local_may_aliast &local_may_alias,
+    value_setst &value_sets,
     const goto_programt::targett loop_head,
     const loopt &loop);
 
@@ -83,7 +85,7 @@ class code_contractst
 
 void code_contractst::apply_contract(
   goto_programt &goto_program,
-  const local_may_aliast &local_may_alias,
+  value_setst &value_sets,
   goto_programt::targett target)
 {
   const code_function_callt &call=to_code_function_call(target->code);
@@ -116,17 +118,27 @@ void code_contractst::apply_contract(
   }
 
   // find out what can be written by the function
-  // TODO Use a better write-set analysis.
   modifiest modifies;
-  function_modifiest function_modifies(goto_functions);
 
-  // Handle return value of the function
-  if(call.lhs().is_not_nil())
+  rw_range_set_value_sett rw_set(ns, value_sets);
+  goto_rw(goto_functions, function, rw_set);
+  forall_rw_range_set_w_objects(it, rw_set)
   {
-    function_modifies.get_modifies_lhs(local_may_alias, target,
-                                       call.lhs(), modifies);
+    // Skip over local variables of the function being called, as well as
+    // variables not in the namespace (e.g. symex::invalid_object)
+    const symbolt *symbol_ptr;
+    if(!ns.lookup(it->first, symbol_ptr))
+    {
+      const std::string &name_string = id2string(symbol_ptr->name);
+      std::string scope_prefix(id2string(ns.lookup(function).name));
+      scope_prefix += "::";
+
+      if(name_string.find(scope_prefix) == std::string::npos)
+      {
+        modifies.insert(ns.lookup(it->first).symbol_expr());
+      }
+    }
   }
-  function_modifies(call.function(), modifies);
 
   // build the havocking code
   goto_programt havoc_code;
@@ -137,7 +149,9 @@ void code_contractst::apply_contract(
 
   // TODO: return value could be nil
   if(type.return_type()!=empty_typet())
+  {
     replace.insert("__CPROVER_return_value", call.lhs());
+  }
 
   // formal parameters
   code_function_callt::argumentst::const_iterator a_it=
@@ -153,6 +167,18 @@ void code_contractst::apply_contract(
   replace(requires);
   replace(ensures);
 
+  // Havoc the return value of the function call.
+  if(type.return_type()!=empty_typet())
+  {
+    const exprt &lhs = call.lhs();
+    const exprt &rhs = side_effect_expr_nondett(call.lhs().type());
+    target->make_assignment(code_assignt(lhs, rhs));
+  }
+  else
+  {
+    target->make_skip();
+  }
+
   if(requires.is_not_nil())
   {
     goto_programt::instructiont a(ASSERT);
@@ -164,15 +190,19 @@ void code_contractst::apply_contract(
     ++target;
   }
 
-  // TODO some sort of replacement on havoc code
   goto_program.destructive_insert(target, havoc_code);
 
-  target->make_assumption(ensures);
+  {
+    goto_programt::targett a=goto_program.insert_after(target);
+    a->make_assumption(ensures);
+    a->function=target->function;
+    a->source_location=target->source_location;
+  }
 }
 
 void code_contractst::apply_invariant(
   goto_functionst::goto_functiont &goto_function,
-  const local_may_aliast &local_may_alias,
+  value_setst &value_sets,
   const goto_programt::targett loop_head,
   const loopt &loop)
 {
@@ -207,7 +237,20 @@ void code_contractst::apply_invariant(
 
   // find out what can get changed in the loop
   modifiest modifies;
-  get_modifies(local_may_alias, loop, modifies);
+
+  rw_range_set_value_sett rw_set(ns, value_sets);
+  for(const goto_programt::targett &inst : loop)
+  {
+    goto_rw(inst, rw_set);
+  }
+  forall_rw_range_set_w_objects(it, rw_set)
+  {
+    const symbolt *symbol_ptr;
+    if(!ns.lookup(it->first, symbol_ptr))
+    {
+      modifies.insert(ns.lookup(it->first).symbol_expr());
+    }
+  }
 
   // build the havocking code
   goto_programt havoc_code;
@@ -275,7 +318,8 @@ void code_contractst::check_contract(
     static_cast<const exprt&>(goto_function.type.find(ID_C_spec_ensures));
 
   // Nothing to check if ensures is nil.
-  if(ensures.is_nil()) {
+  if(ensures.is_nil())
+  {
     return;
   }
 
@@ -374,7 +418,7 @@ void code_contractst::check_contract(
 
 void code_contractst::check_apply_invariant(
   goto_functionst::goto_functiont &goto_function,
-  const local_may_aliast &local_may_alias,
+  value_setst &value_sets,
   const goto_programt::targett loop_head,
   const loopt &loop)
 {
@@ -393,7 +437,9 @@ void code_contractst::check_apply_invariant(
     static_cast<const exprt&>(
       loop_end->guard.find(ID_C_spec_loop_invariant));
   if(invariant.is_nil())
+  {
     return;
+  }
 
   // change H: loop; E: ...
   // to
@@ -408,7 +454,20 @@ void code_contractst::check_apply_invariant(
 
   // find out what can get changed in the loop
   modifiest modifies;
-  get_modifies(local_may_alias, loop, modifies);
+
+  rw_range_set_value_sett rw_set(ns, value_sets);
+  for(const goto_programt::targett &inst : loop)
+  {
+    goto_rw(inst, rw_set);
+  }
+  forall_rw_range_set_w_objects(it, rw_set)
+  {
+    const symbolt *symbol_ptr;
+    if(!ns.lookup(it->first, symbol_ptr))
+    {
+      modifies.insert(ns.lookup(it->first).symbol_expr());
+    }
+  }
 
   // build the havocking code
   goto_programt havoc_code;
@@ -477,18 +536,20 @@ const symbolt &code_contractst::new_tmp_symbol(
 
 void code_contractst::apply_code_contracts()
 {
+  auto vs = util_make_unique<value_set_analysis_fit>(ns);
+  (*vs)(goto_functions);
+  std::unique_ptr<value_setst> value_sets = std::move(vs);
+
   Forall_goto_functions(it, goto_functions)
   {
     goto_functionst::goto_functiont &goto_function = it->second;
 
-    // TODO: This aliasing check is insufficiently strong, in general.
-    local_may_aliast local_may_alias(goto_function);
     natural_loops_mutablet natural_loops(goto_function.body);
 
     for(const auto &l_it : natural_loops.loop_map)
     {
       apply_invariant(goto_function,
-                      local_may_alias,
+                      *value_sets,
                       l_it.first,
                       l_it.second);
     }
@@ -497,7 +558,7 @@ void code_contractst::apply_code_contracts()
     {
       if(it->is_function_call())
       {
-        apply_contract(goto_function.body, local_may_alias, it);
+        apply_contract(goto_function.body, *value_sets, it);
       }
     }
   }
@@ -507,6 +568,10 @@ void code_contractst::apply_code_contracts()
 
 void code_contractst::check_code_contracts()
 {
+  auto vs = util_make_unique<value_set_analysis_fit>(ns);
+  (*vs)(goto_functions);
+  std::unique_ptr<value_setst> value_sets = std::move(vs);
+
   goto_functionst::function_mapt::iterator i_it=
     goto_functions.function_map.find(INITIALIZE_FUNCTION);
   assert(i_it!=goto_functions.function_map.end());
@@ -516,14 +581,12 @@ void code_contractst::check_code_contracts()
   {
     goto_functionst::goto_functiont &goto_function = it->second;
 
-    // TODO: This aliasing check is insufficiently strong, in general.
-    local_may_aliast local_may_alias(goto_function);
     natural_loops_mutablet natural_loops(goto_function.body);
 
     for(const auto &l_it : natural_loops.loop_map)
     {
       check_apply_invariant(goto_function,
-                            local_may_alias,
+                            *value_sets,
                             l_it.first,
                             l_it.second);
     }
@@ -532,7 +595,7 @@ void code_contractst::check_code_contracts()
     {
       if(it->is_function_call())
       {
-        apply_contract(goto_function.body, local_may_alias, it);
+        apply_contract(goto_function.body, *value_sets, it);
       }
     }
   }

src/goto-instrument/loop_utils.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "loop_utils.h"
 
 #include <util/std_expr.h>
-#include <util/expr_iterator.h>
 
 #include <analyses/natural_loops.h>
 #include <analyses/local_may_alias.h>
@@ -108,41 +107,3 @@ void get_modifies(
     }
   }
 }
-
-// TODO handle aliasing at all
-void get_uses(
-  const local_may_aliast &local_may_alias,
-  const loopt &loop,
-  usest &uses)
-{
-  for(loopt::const_iterator
-      i_it=loop.begin(); i_it!=loop.end(); i_it++)
-  {
-    const goto_programt::instructiont &instruction=**i_it;
-    if(instruction.code.is_not_nil())
-    {
-      for(const_depth_iteratort it=instruction.code.depth_begin();
-          it!=instruction.code.depth_end();
-          ++it)
-      {
-        if((*it).id()==ID_symbol)
-        {
-          uses.insert(*it);
-        }
-      }
-    }
-
-    if(instruction.guard.is_not_nil())
-    {
-      for(const_depth_iteratort it=instruction.guard.depth_begin();
-          it!=instruction.guard.depth_end();
-          ++it)
-      {
-        if((*it).id()==ID_symbol)
-        {
-          uses.insert(*it);
-        }
-      }
-    }
-  }
-}

src/goto-instrument/loop_utils.h

@@ -17,19 +17,13 @@ Author: Daniel Kroening, [email protected]
 class local_may_aliast;
 
 typedef std::set<exprt> modifiest;
-typedef std::set<exprt> usest;
 typedef const natural_loops_mutablet::natural_loopt loopt;
 
 void get_modifies(
   const local_may_aliast &local_may_alias,
   const loopt &loop,
   modifiest &modifies);
 
-void get_uses(
-  const local_may_aliast &local_may_alias,
-  const loopt &loop,
-  usest &uses);
-
 void build_havoc_code(
   const goto_programt::targett loop_head,
   const modifiest &modifies,