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 \

src/goto-programs/builtin_functions.cpp

@@ -669,10 +669,7 @@ void goto_convertt::do_havoc_slice(
   // char nondet_contents[argument[1]];
   // __CPROVER_array_replace(p, nondet_contents);
 
-  symbol_exprt deallocated =
-    ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr();
-  symbol_exprt dead = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
-  prophecy_w_ok_exprt ok_expr{arguments[0], arguments[1], deallocated, dead};
+  r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]);
   ok_expr.add_source_location() = source_location;
   source_locationt annotated_location = source_location;
   annotated_location.set("user-provided", false);

src/goto-programs/goto_clean_expr.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_convert_class.h"
 
-#include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/pointer_expr.h>
@@ -74,15 +73,6 @@ bool goto_convertt::needs_cleaning(const exprt &expr)
     return true;
   }
 
-  // Rewrite rw_ok and pointer_in_range front-end expressions into ones
-  // including prophecy expressions.
-  if(
-    can_cast_expr<r_or_w_ok_exprt>(expr) ||
-    can_cast_expr<pointer_in_range_exprt>(expr))
-  {
-    return true;
-  }
-
   // We can't flatten quantified expressions by introducing new literals for
   // conditional expressions.  This is because the body of the quantified
   // may refer to bound variables, which are not visible outside the scope
@@ -446,32 +436,6 @@ void goto_convertt::clean_expr(
       expr.operands().size() == 1, "ID_compound_literal has a single operand");
     expr = to_unary_expr(expr).op();
   }
-  else if(auto r_or_w_ok = expr_try_dynamic_cast<r_or_w_ok_exprt>(expr))
-  {
-    const auto &id = expr.id();
-    expr =
-      prophecy_r_or_w_ok_exprt{
-        id == ID_r_ok   ? ID_prophecy_r_ok
-        : id == ID_w_ok ? ID_prophecy_w_ok
-                        : ID_prophecy_rw_ok,
-        r_or_w_ok->pointer(),
-        r_or_w_ok->size(),
-        ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
-        ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
-        .with_source_location<exprt>(expr);
-  }
-  else if(
-    auto pointer_in_range = expr_try_dynamic_cast<pointer_in_range_exprt>(expr))
-  {
-    expr =
-      prophecy_pointer_in_range_exprt{
-        pointer_in_range->lower_bound(),
-        pointer_in_range->pointer(),
-        pointer_in_range->upper_bound(),
-        ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
-        ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
-        .with_source_location<exprt>(expr);
-  }
 }
 
 void goto_convertt::clean_expr_address_of(

src/goto-programs/process_goto_program.cpp

@@ -23,6 +23,7 @@ Author: Martin Brain, [email protected]
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
+#include <goto-programs/rewrite_rw_ok.h>
 #include <goto-programs/rewrite_union.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
@@ -70,6 +71,9 @@ bool process_goto_program(
   if(options.get_bool_option("rewrite-union"))
     rewrite_union(goto_model);
 
+  if(options.get_bool_option("rewrite-rw-ok"))
+    rewrite_rw_ok(goto_model);
+
   // add generic checks
   log.status() << "Generic Property Instrumentation" << messaget::eom;
   goto_check_c(options, goto_model, log.get_message_handler());

src/goto-programs/rewrite_rw_ok.cpp

@@ -0,0 +1,83 @@
+/*******************************************************************\
+
+Module: Rewrite {r,w,rw}_ok expressions as required by symbolic execution
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "rewrite_rw_ok.h"
+
+#include <util/expr_iterator.h>
+#include <util/pointer_expr.h>
+
+#include <goto-programs/goto_model.h>
+
+static optionalt<exprt> rewrite_rw_ok(exprt expr, const namespacet &ns)
+{
+  bool unchanged = true;
+
+  for(auto it = expr.depth_begin(), itend = expr.depth_end();
+      it != itend;) // no ++it
+  {
+    if(auto r_or_w_ok = expr_try_dynamic_cast<r_or_w_ok_exprt>(*it))
+    {
+      const auto &id = it->id();
+      exprt replacement =
+        prophecy_r_or_w_ok_exprt{
+          id == ID_r_ok   ? ID_prophecy_r_ok
+          : id == ID_w_ok ? ID_prophecy_w_ok
+                          : ID_prophecy_rw_ok,
+          r_or_w_ok->pointer(),
+          r_or_w_ok->size(),
+          ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
+          ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
+          .with_source_location<exprt>(*it);
+
+      it.mutate() = std::move(replacement);
+      unchanged = false;
+      it.next_sibling_or_parent();
+    }
+    else if(
+      auto pointer_in_range =
+        expr_try_dynamic_cast<pointer_in_range_exprt>(*it))
+    {
+      exprt replacement =
+        prophecy_pointer_in_range_exprt{
+          pointer_in_range->lower_bound(),
+          pointer_in_range->pointer(),
+          pointer_in_range->upper_bound(),
+          ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(),
+          ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr()}
+          .with_source_location<exprt>(*it);
+
+      it.mutate() = std::move(replacement);
+      unchanged = false;
+      it.next_sibling_or_parent();
+    }
+    else
+      ++it;
+  }
+
+  if(unchanged)
+    return {};
+  else
+    return std::move(expr);
+}
+
+static void rewrite_rw_ok(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns)
+{
+  for(auto &instruction : goto_function.body.instructions)
+    instruction.transform(
+      [&ns](exprt expr) { return rewrite_rw_ok(expr, ns); });
+}
+
+void rewrite_rw_ok(goto_modelt &goto_model)
+{
+  const namespacet ns(goto_model.symbol_table);
+
+  for(auto &gf_entry : goto_model.goto_functions.function_map)
+    rewrite_rw_ok(gf_entry.second, ns);
+}

src/goto-programs/rewrite_rw_ok.h

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Rewrite {r,w,rw}_ok expressions as required by symbolic execution
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+/// \file
+/// Rewrite r/w/rw_ok expressions to ones including prophecy variables recording
+/// the state.
+
+#ifndef CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H
+#define CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H
+
+class goto_modelt;
+
+/// Replace all occurrences of `r_ok_exprt`, `w_ok_exprt`, `rw_ok_exprt`,
+/// `pointer_in_range_exprt` by their prophecy variants
+/// `prophecy_r_or_w_ok_exprt` and `prophecy_pointer_in_range_exprt`,
+/// respectively.
+/// Each analysis may choose to natively support `r_ok_exprt` etc. (like
+/// `cprover_parse_optionst` does) or may instead require the expression to be
+/// lowered to other primitives (like `goto_symext`).
+void rewrite_rw_ok(goto_modelt &);
+
+#endif // CPROVER_GOTO_PROGRAMS_REWRITE_RW_OK_H

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -199,6 +199,7 @@ optionst goto_synthesizer_parse_optionst::get_options()
   options.set_option("depth", UINT32_MAX);
   options.set_option("exploration-strategy", "lifo");
   options.set_option("symex-cache-dereferences", false);
+  options.set_option("rewrite-rw-ok", true);
   options.set_option("rewrite-union", true);
   options.set_option("self-loops-to-assumptions", true);