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, [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>
@@ -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 \

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);