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. We may, in future, decide
to have back-end specific (and possibly more efficient) handling of
these.

Author: tautschnig

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

@@ -2499,6 +2499,14 @@ void smt2_convt::convert_expr(const exprt &expr)
       out << ')';
     }
   }
+  else if(expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok)
+  {
+    convert_expr(simplify_expr(to_r_or_w_ok_expr(expr).lower(ns), ns));
+  }
+  else if(expr.id() == ID_pointer_in_range)
+  {
+    convert_expr(simplify_expr(to_pointer_in_range_expr(expr).lower(ns), ns));
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,