Move CPROVER_{r,w,rw}_ok processing to back-end

src/ansi-c/expr2c.cpp

@@ -3572,6 +3572,26 @@ std::string expr2ct::convert_r_or_w_ok(const r_or_w_ok_exprt &src)
   return dest;
 }
 
+std::string
+expr2ct::convert_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &src)
+{
+  // we hide prophecy expressions in C-style output
+  std::string dest = src.id() == ID_prophecy_r_ok   ? "R_OK"
+                     : src.id() == ID_prophecy_w_ok ? "W_OK"
+                                                    : "RW_OK";
+
+  dest += '(';
+
+  unsigned p;
+  dest += convert_with_precedence(src.pointer(), p);
+  dest += ", ";
+  dest += convert_with_precedence(src.size(), p);
+
+  dest += ')';
+
+  return dest;
+}
+
 std::string expr2ct::convert_pointer_in_range(const pointer_in_range_exprt &src)
 {
   std::string dest = CPROVER_PREFIX "pointer_in_range";
@@ -3590,6 +3610,26 @@ std::string expr2ct::convert_pointer_in_range(const pointer_in_range_exprt &src)
   return dest;
 }
 
+std::string expr2ct::convert_prophecy_pointer_in_range(
+  const prophecy_pointer_in_range_exprt &src)
+{
+  // we hide prophecy expressions in C-style output
+  std::string dest = CPROVER_PREFIX "pointer_in_range";
+
+  dest += '(';
+
+  unsigned p;
+  dest += convert_with_precedence(src.lower_bound(), p);
+  dest += ", ";
+  dest += convert_with_precedence(src.pointer(), p);
+  dest += ", ";
+  dest += convert_with_precedence(src.upper_bound(), p);
+
+  dest += ')';
+
+  return dest;
+}
+
 std::string expr2ct::convert_with_precedence(
   const exprt &src,
   unsigned &precedence)
@@ -4002,9 +4042,22 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id() == ID_r_ok || src.id() == ID_w_ok || src.id() == ID_rw_ok)
     return convert_r_or_w_ok(to_r_or_w_ok_expr(src));
 
+  else if(
+    auto prophecy_r_or_w_ok =
+      expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(src))
+  {
+    return convert_prophecy_r_or_w_ok(*prophecy_r_or_w_ok);
+  }
+
   else if(src.id() == ID_pointer_in_range)
     return convert_pointer_in_range(to_pointer_in_range_expr(src));
 
+  else if(src.id() == ID_prophecy_pointer_in_range)
+  {
+    return convert_prophecy_pointer_in_range(
+      to_prophecy_pointer_in_range_expr(src));
+  }
+
   auto function_string_opt = convert_function(src);
   if(function_string_opt.has_value())
     return *function_string_opt;

src/ansi-c/expr2c_class.h

@@ -28,6 +28,8 @@ class qualifierst;
 class namespacet;
 class r_or_w_ok_exprt;
 class pointer_in_range_exprt;
+class prophecy_r_or_w_ok_exprt;
+class prophecy_pointer_in_range_exprt;
 
 class expr2ct
 {
@@ -285,7 +287,10 @@ class expr2ct
   std::string convert_bitreverse(const bitreverse_exprt &src);
 
   std::string convert_r_or_w_ok(const r_or_w_ok_exprt &src);
+  std::string convert_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &src);
   std::string convert_pointer_in_range(const pointer_in_range_exprt &src);
+  std::string
+  convert_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &src);
 };
 
 #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H

src/ansi-c/goto_check_c.cpp

@@ -228,7 +228,6 @@ class goto_check_ct
   void conversion_check(const exprt &, const guardt &);
   void float_overflow_check(const exprt &, const guardt &);
   void nan_check(const exprt &, const guardt &);
-  optionalt<exprt> expand_pointer_checks(exprt);
 
   std::string array_name(const exprt &);
 
@@ -1444,6 +1443,8 @@ void goto_check_ct::pointer_primitive_check(
   const exprt pointer =
     (expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
       ? to_r_or_w_ok_expr(expr).pointer()
+    : can_cast_expr<prophecy_r_or_w_ok_exprt>(expr)
+      ? to_prophecy_r_or_w_ok_expr(expr).pointer()
       : to_unary_expr(expr).op();
 
   CHECK_RETURN(pointer.type().id() == ID_pointer);
@@ -1484,6 +1485,7 @@ bool goto_check_ct::requires_pointer_primitive_check(const exprt &expr)
   // will equally be non-deterministic.
   return can_cast_expr<object_size_exprt>(expr) || expr.id() == ID_r_ok ||
          expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
+         can_cast_expr<prophecy_r_or_w_ok_exprt>(expr) ||
          expr.id() == ID_is_dynamic_object;
 }
 
@@ -1992,62 +1994,6 @@ void goto_check_ct::check(const exprt &expr)
   check_rec(expr, identity);
 }
 
-/// expand the r_ok, w_ok, rw_ok, pointer_in_range predicates
-optionalt<exprt> goto_check_ct::expand_pointer_checks(exprt expr)
-{
-  bool modified = false;
-
-  for(auto &op : expr.operands())
-  {
-    auto op_result = expand_pointer_checks(op);
-    if(op_result.has_value())
-    {
-      op = *op_result;
-      modified = true;
-    }
-  }
-
-  if(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
-  {
-    // these get an address as first argument and a size as second
-    DATA_INVARIANT(
-      expr.operands().size() == 2, "r/w_ok must have two operands");
-
-    const auto conditions = get_pointer_dereferenceable_conditions(
-      to_r_or_w_ok_expr(expr).pointer(), to_r_or_w_ok_expr(expr).size());
-
-    exprt::operandst conjuncts;
-
-    for(const auto &c : conditions)
-      conjuncts.push_back(c.assertion);
-
-    exprt c = conjunction(conjuncts);
-    if(enable_simplify)
-      simplify(c, ns);
-    return c;
-  }
-  else if(expr.id() == ID_pointer_in_range)
-  {
-    const auto &pointer_in_range_expr = to_pointer_in_range_expr(expr);
-
-    auto expanded = pointer_in_range_expr.lower();
-
-    // rec. call
-    auto expanded_rec_opt = expand_pointer_checks(expanded);
-    if(expanded_rec_opt.has_value())
-      expanded = *expanded_rec_opt;
-
-    if(enable_simplify)
-      simplify(expanded, ns);
-
-    return expanded;
-  }
-  else if(modified)
-    return std::move(expr);
-  else
-    return {};
-}
-
 void goto_check_ct::memory_leak_check(const irep_idt &function_id)
 {
   const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
@@ -2267,8 +2213,6 @@ void goto_check_ct::goto_check(
       }
     }
 
-    i.transform([this](exprt expr) { return expand_pointer_checks(expr); });
-
     for(auto &instruction : new_code.instructions)
     {
       if(instruction.source_location().is_nil())

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