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.

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, [email protected]
 #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>
@@ -1767,6 +1768,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 \