Add conversion of pointer_object_exprt and a regression test for that.

Author: NlightNFotis

regression/cbmc-incr-smt2/pointers/pointer_object.c

@@ -0,0 +1,20 @@
+int main()
+{
+  int a = 10;
+  int nondet_bool;
+  int flag = 1;
+
+  int *b = &a;
+  int *c = nondet_bool ? &a : 0;
+  int *d = flag ? &a : 0;
+  int *e;
+
+  // __CPROVER_same_object is True when
+  // `__CPROVER_pointer_object(a) == __CPROVER_pointer_object(b)`
+  __CPROVER_assert(
+    __CPROVER_same_object(b, c), "expected fail as c can be null");
+  __CPROVER_assert(
+    __CPROVER_same_object(b, d), "expected success because d is &a");
+  __CPROVER_assert(
+    __CPROVER_same_object(b, e), "expected fail as e can be null");
+}

regression/cbmc-incr-smt2/pointers/pointer_object.desc

@@ -0,0 +1,10 @@
+CORE
+pointer_object.c
+--trace --verbosity 10
+\[main\.assertion\.1\] line \d+ expected fail as c can be null: FAILURE
+\[main\.assertion\.2\] line \d+ expected success because d is &a: SUCCESS
+\[main\.assertion\.3\] line \d+ expected fail as e can be null: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1142,6 +1142,29 @@ static smt_termt convert_expr_to_smt(
     mult_overflow.pretty());
 }
 
+static smt_termt convert_expr_to_smt(
+  const pointer_object_exprt &pointer_object,
+  const sub_expression_mapt &converted)
+{
+  const auto type =
+    type_try_dynamic_cast<bitvector_typet>(pointer_object.type());
+  INVARIANT(type, "Pointer object should have a bitvector-based type.");
+  const auto converted_expr = converted.at(pointer_object.pointer());
+  const std::size_t width = type->get_width();
+  const std::size_t object_bits = config.bv_encoding.object_bits;
+  INVARIANT(
+    width >= object_bits,
+    "Width should be at least as big as the number of object bits.");
+  const std::size_t ext = width - object_bits;
+  const auto extract_op = smt_bit_vector_theoryt::extract(
+    width - 1, width - object_bits)(converted_expr);
+  if(ext > 0)
+  {
+    return smt_bit_vector_theoryt::zero_extend(ext)(extract_op);
+  }
+  return extract_op;
+}
+
 static smt_termt convert_expr_to_smt(
   const shl_overflow_exprt &shl_overflow,
   const sub_expression_mapt &converted)
@@ -1437,10 +1460,13 @@ static smt_termt dispatch_expr_to_smt_conversion(
   else if(expr.id()==ID_pointer_offset)
   {
   }
-  else if(expr.id()==ID_pointer_object)
+#endif
+  else if(
+    const auto pointer_object =
+      expr_try_dynamic_cast<pointer_object_exprt>(expr))
   {
+    return convert_expr_to_smt(*pointer_object, converted);
   }
-#endif
   if(
     const auto is_dynamic_object =
       expr_try_dynamic_cast<is_dynamic_object_exprt>(expr))