Merge pull request #7459 from tautschnig/cleanup/pointer-in-range

Cleanup of pointer-in-range predicate handling

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2671,7 +2671,6 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier == CPROVER_PREFIX "pointer_in_range")
   {
-    // experimental feature for CHC encodings -- do not use
     if(expr.arguments().size() != 3)
     {
       error().source_location = f_op.source_location();

src/ansi-c/expr2c.cpp

@@ -3572,6 +3572,24 @@ std::string expr2ct::convert_r_or_w_ok(const r_or_w_ok_exprt &src)
   return dest;
 }
 
+std::string expr2ct::convert_pointer_in_range(const pointer_in_range_exprt &src)
+{
+  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)
@@ -3984,6 +4002,9 @@ 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(src.id() == ID_pointer_in_range)
+    return convert_pointer_in_range(to_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

@@ -27,6 +27,7 @@ class annotated_pointer_constant_exprt;
 class qualifierst;
 class namespacet;
 class r_or_w_ok_exprt;
+class pointer_in_range_exprt;
 
 class expr2ct
 {
@@ -284,6 +285,7 @@ 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_pointer_in_range(const pointer_in_range_exprt &src);
 };
 
 #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H

src/util/pointer_expr.h

@@ -385,6 +385,21 @@ class pointer_in_range_exprt : public ternary_exprt
     PRECONDITION(op2().type().id() == ID_pointer);
   }
 
+  const exprt &lower_bound() const
+  {
+    return op0();
+  }
+
+  const exprt &pointer() const
+  {
+    return op1();
+  }
+
+  const exprt &upper_bound() const
+  {
+    return op2();
+  }
+
   // translate into equivalent conjunction
   exprt lower() const;
 };
@@ -414,7 +429,7 @@ inline pointer_in_range_exprt &to_pointer_in_range_expr(exprt &expr)
 {
   PRECONDITION(expr.id() == ID_pointer_in_range);
   DATA_INVARIANT(
-    expr.operands().size() == 3, "pointer_in_range must have one operand");
+    expr.operands().size() == 3, "pointer_in_range must have three operands");
   return static_cast<pointer_in_range_exprt &>(expr);
 }