Back-end support for {r,w,rw}_ok and pointer_in_range

There is no longer a need to rewrite these early on during program
instrumentation. Instead, let the back-end handle them. For now, they
are just handled by lowering the expressions (in the SAT and SMT
back-end; there is no current support in the incremental SMT back-end
just yet). We may, in future, decide to have back-end specific (and
possibly more efficient) handling of these.

Author: tautschnig

regression/cbmc-primitives/r_w_ok_bug/test.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --pointer-check --no-simplify --no-propagation
 ^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$

regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_null/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_valid/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_valid_negated/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/same-object-03/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --no-simplify --no-propagation
 ^EXIT=0$

src/solvers/flattening/bv_pointers.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
 
 /// Map bytes according to the configured endianness. The key difference to
 /// endianness_mapt is that bv_endianness_mapt is aware of the bit-level
@@ -203,6 +204,10 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
           bv_utilst::representationt::SIGNED));
     }
   }
+  else if(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
+    return convert(simplify_expr(to_r_or_w_ok_expr(expr).lower(ns), ns));
+  else if(expr.id() == ID_pointer_in_range)
+    return convert(simplify_expr(to_pointer_in_range_expr(expr).lower(ns), ns));
 
   return SUB::convert_rest(expr);
 }

src/solvers/smt2/smt2_conv.cpp

@@ -5010,6 +5010,28 @@ exprt smt2_convt::prepare_for_convert_expr(const exprt &expr)
     !has_byte_operator(lowered_expr),
     "lower_byte_operators should remove all byte operators");
 
+  // Perform rewrites that may introduce new symbols
+  for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
+      it != itend;) // no ++it
+  {
+    if(auto r_or_w_ok = expr_try_dynamic_cast<r_or_w_ok_exprt>(*it))
+    {
+      exprt lowered = simplify_expr(r_or_w_ok->lower(ns), ns);
+      it.mutate() = lowered;
+      it.next_sibling_or_parent();
+    }
+    else if(
+      auto pointer_in_range =
+        expr_try_dynamic_cast<pointer_in_range_exprt>(*it))
+    {
+      exprt lowered = simplify_expr(pointer_in_range->lower(ns), ns);
+      it.mutate() = lowered;
+      it.next_sibling_or_parent();
+    }
+    else
+      ++it;
+  }
+
   // Now create symbols for all composite expressions present in lowered_expr:
   find_symbols(lowered_expr);
 

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1466,6 +1466,24 @@ static smt_termt convert_expr_to_smt(
     count_trailing_zeros.pretty());
 }
 
+static smt_termt convert_expr_to_smt(
+  const r_or_w_ok_exprt &r_or_w_ok,
+  const sub_expression_mapt &converted)
+{
+  UNIMPLEMENTED_FEATURE(
+    "Generation of SMT formula for r/w/rw ok expression: " +
+    r_or_w_ok.pretty());
+}
+
+static smt_termt convert_expr_to_smt(
+  const pointer_in_range_exprt &pointer_in_range,
+  const sub_expression_mapt &converted)
+{
+  UNIMPLEMENTED_FEATURE(
+    "Generation of SMT formula for pointer-in-range expression: " +
+    pointer_in_range.pretty());
+}
+
 static smt_termt dispatch_expr_to_smt_conversion(
   const exprt &expr,
   const sub_expression_mapt &converted,
@@ -1801,6 +1819,16 @@ static smt_termt dispatch_expr_to_smt_conversion(
   {
     return convert_expr_to_smt(*count_trailing_zeros, converted);
   }
+  if(const auto r_or_w_ok = expr_try_dynamic_cast<r_or_w_ok_exprt>(expr))
+  {
+    return convert_expr_to_smt(*r_or_w_ok, converted);
+  }
+  if(
+    const auto pointer_in_range =
+      expr_try_dynamic_cast<pointer_in_range_exprt>(expr))
+  {
+    return convert_expr_to_smt(*pointer_in_range, converted);
+  }
 
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for unknown kind of expression: " +