Move rw_ok rewriting to separate pass

This reverts selected changes from "r/w/rw_ok and pointer_in_range
depend on deallocated and dead_object" for transformations of goto
programs can now safely introduce rw_ok expressions into the goto
program. Not all analyses, however, are able to cope with these
expressions. Dependence graphs (and any analyses building upon these),
for example, also require this rewriting. goto-instrument is adjusted
accordingly.

Author: tautschnig

regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc

@@ -1,7 +1,7 @@
 CORE new-smt-backend
 test.c
 --malloc-may-fail --malloc-fail-null
-^\[free.precondition.\d+] line \d+ double free: SUCCESS$
+^\[main.precondition_instance.\d+] line \d+ double free: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc

@@ -4,7 +4,7 @@ test.c
 ^EXIT=0$
 ^SIGNAL=0$
 Checking assertions
-^\[free.precondition.1\] line \d+ free argument must be NULL or valid pointer: SUCCESS
+^\[EVP_MD_CTX_free.precondition_instance.1\] line \d+ free argument must be NULL or valid pointer: SUCCESS
 --
 Invariant check failed
 --

src/cbmc/cbmc_parse_options.cpp

@@ -406,6 +406,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 
   // Options for process_goto_program
+  options.set_option("rewrite-rw-ok", true);
   options.set_option("rewrite-union", true);
 
   if(cmdline.isset("smt1"))

src/cprover/state_encoding.cpp

@@ -294,20 +294,6 @@ exprt state_encodingt::evaluate_expr_rec(
                                          : ID_state_rw_ok;
     return ternary_exprt(new_id, state, pointer, size, what.type());
   }
-  else if(
-    const auto r_or_w_ok_expr =
-      expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(what))
-  {
-    // we replace prophecy expressions by our state
-    auto pointer =
-      evaluate_expr_rec(loc, state, r_or_w_ok_expr->pointer(), bound_symbols);
-    auto size =
-      evaluate_expr_rec(loc, state, r_or_w_ok_expr->size(), bound_symbols);
-    auto new_id = what.id() == ID_prophecy_r_ok   ? ID_state_r_ok
-                  : what.id() == ID_prophecy_w_ok ? ID_state_w_ok
-                                                  : ID_state_rw_ok;
-    return ternary_exprt(new_id, state, pointer, size, what.type());
-  }
   else if(what.id() == ID_is_cstring)
   {
     // we need to add the state

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -393,6 +393,7 @@ int goto_analyzer_parse_optionst::doit()
 
   // Preserve backwards compatibility in processing
   options.set_option("partial-inline", true);
+  options.set_option("rewrite-rw-ok", false);
   options.set_option("rewrite-union", false);
   options.set_option("remove-returns", true);
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -65,6 +65,7 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   options.set_option("show-properties", cmdline.isset("show-properties"));
 
   // Options for process_goto_program
+  options.set_option("rewrite-rw-ok", false);
   options.set_option("rewrite-union", true);
 }
 

src/goto-instrument/contracts/instrument_spec_assigns.cpp

@@ -644,13 +644,9 @@ exprt instrument_spec_assignst::target_validity_expr(
   // (or is NULL if we allow it explicitly).
   // This assertion will be falsified whenever `start_address` is invalid or
   // not of the right size (or is NULL if we do not allow it explicitly).
-  symbol_exprt deallocated =
-    ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
-  symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
-  auto result = or_exprt{
-    not_exprt{car.condition()},
-    prophecy_w_ok_exprt{
-      car.target_start_address(), car.target_size(), deallocated, dead}};
+  auto result =
+    or_exprt{not_exprt{car.condition()},
+             w_ok_exprt{car.target_start_address(), car.target_size()}};
 
   if(allow_null_target)
     result.add_to_operands(null_object(car.target_start_address()));

src/goto-instrument/contracts/utils.cpp

@@ -178,11 +178,7 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
     const auto size_of_expr_opt = size_of_expr(expr.type(), ns);
     CHECK_RETURN(size_of_expr_opt.has_value());
 
-    symbol_exprt deallocated =
-      ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
-    symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
-    validity_checks.push_back(prophecy_r_ok_exprt{
-      deref->pointer(), *size_of_expr_opt, deallocated, dead});
+    validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt});
   }
 
   for(const auto &op : expr.operands())

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -45,6 +45,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/restrict_function_pointers.h>
+#include <goto-programs/rewrite_rw_ok.h>
 #include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
@@ -569,6 +570,7 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-reaching-definitions"))
     {
       do_indirect_call_and_rtti_removal();
+      rewrite_rw_ok(goto_model);
 
       const namespacet ns(goto_model.symbol_table);
       reaching_definitions_analysist rd_analysis(ns);
@@ -581,6 +583,7 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-dependence-graph"))
     {
       do_indirect_call_and_rtti_removal();
+      rewrite_rw_ok(goto_model);
 
       const namespacet ns(goto_model.symbol_table);
       dependence_grapht dependence_graph(ns);
@@ -1767,6 +1770,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   {
     do_indirect_call_and_rtti_removal();
     do_remove_returns();
+    rewrite_rw_ok(goto_model);
 
     log.warning() << "**** WARNING: Experimental option --full-slice, "
                   << "analysis results may be unsound. See "

src/goto-programs/Makefile

@@ -56,6 +56,7 @@ SRC = allocate_objects.cpp \
       remove_vector.cpp \
       remove_virtual_functions.cpp \
       restrict_function_pointers.cpp \
+      rewrite_rw_ok.cpp \
       rewrite_union.cpp \
       resolve_inherited_component.cpp \
       safety_checker.cpp \