Add annotated_pointer_constant_exprt

The back-end previously created constant_exprt with an operand when
instantiating pointer-typed expressions with their solver-computed
model. This violates the contract of nullary_exprt, which a
constant_exprt should (!) be, and resulted in special-case treatment in
several places.

The annotated_pointer_constant_exprt formalises this concept of a
constant (as derived from the solver-computed model) with the additional
annotation of the original pointer that was instantiated.

Fixes: #6691

Author: tautschnig

jbmc/src/java_bytecode/java_trace_validation.cpp

@@ -68,6 +68,7 @@ bool valid_rhs_expr_high_level(const exprt &rhs)
 {
   return can_cast_expr<struct_exprt>(rhs) || can_cast_expr<array_exprt>(rhs) ||
          can_cast_expr<constant_exprt>(rhs) ||
+         can_cast_expr<annotated_pointer_constant_exprt>(rhs) ||
          can_cast_expr<address_of_exprt>(rhs) ||
          can_cast_expr<symbol_exprt>(rhs) ||
          can_cast_expr<array_list_exprt>(rhs) ||
@@ -96,14 +97,21 @@ bool check_struct_structure(const struct_exprt &expr)
     return false;
   if(const auto sub_struct = expr_try_dynamic_cast<struct_exprt>(expr.op0()))
     check_struct_structure(*sub_struct);
-  else if(!can_cast_expr<constant_exprt>(expr.op0()))
+  else if(
+    !can_cast_expr<constant_exprt>(expr.op0()) &&
+    !can_cast_expr<annotated_pointer_constant_exprt>(expr.op0()))
+  {
     return false;
+  }
   if(
-    expr.operands().size() > 1 &&
-    std::any_of(
-      ++expr.operands().begin(),
-      expr.operands().end(),
-      [&](const exprt &operand) { return operand.id() != ID_constant; }))
+    expr.operands().size() > 1 && std::any_of(
+                                    ++expr.operands().begin(),
+                                    expr.operands().end(),
+                                    [&](const exprt &operand) {
+                                      return operand.id() != ID_constant &&
+                                             operand.id() !=
+                                               ID_annotated_pointer_constant;
+                                    }))
   {
     return false;
   }
@@ -119,17 +127,21 @@ bool check_address_structure(const address_of_exprt &address)
 bool check_constant_structure(const constant_exprt &constant_expr)
 {
   if(constant_expr.has_operands())
-  {
-    const auto &operand = skip_typecast(constant_expr.operands()[0]);
-    return can_cast_expr<constant_exprt>(operand) ||
-           can_cast_expr<address_of_exprt>(operand) ||
-           can_cast_expr<plus_exprt>(operand);
-  }
+    return false;
   // All value types used in Java must be non-empty except string_typet:
   return !constant_expr.get_value().empty() ||
          constant_expr.type() == string_typet();
 }
 
+static bool check_annotated_pointer_constant_structure(
+  const annotated_pointer_constant_exprt &constant_expr)
+{
+  const auto &operand = skip_typecast(constant_expr.symbolic_pointer());
+  return can_cast_expr<constant_exprt>(operand) ||
+         can_cast_expr<address_of_exprt>(operand) ||
+         can_cast_expr<plus_exprt>(operand);
+}
+
 static void check_lhs_assumptions(
   const exprt &lhs,
   const namespacet &ns,
@@ -253,8 +265,21 @@ static void check_rhs_assumptions(
       check_constant_structure(*constant_expr),
       "RHS",
       rhs.pretty(),
-      "Expecting the first operand of a constant expression to be a constant, "
-      "address_of or plus expression, or no operands and a non-empty value.");
+      "Expecting a constant expression to have no operands and a non-empty "
+      "value.");
+  }
+  // check pointer constant rhs structure
+  else if(
+    const auto constant_expr =
+      expr_try_dynamic_cast<annotated_pointer_constant_exprt>(rhs))
+  {
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
+      check_annotated_pointer_constant_structure(*constant_expr),
+      "RHS",
+      rhs.pretty(),
+      "Expecting the operand of an annotated  pointer constant expression "
+      "to be a constant, address_of, or plus expression.");
   }
   // check byte extract rhs structure
   else if(const auto byte = expr_try_dynamic_cast<byte_extract_exprt>(rhs))

src/ansi-c/expr2c.cpp

@@ -1994,23 +1994,11 @@ std::string expr2ct::convert_constant(
       if(to_pointer_type(type).base_type().id() != ID_empty)
         dest="(("+convert(type)+")"+dest+")";
     }
-    else if(src.operands().size() == 1)
+    else if(
+      value == "INVALID" || has_prefix(id2string(value), "INVALID-") ||
+      value == "NULL+offset")
     {
-      const auto &annotation = to_unary_expr(src).op();
-
-      if(annotation.id() == ID_constant)
-      {
-        const irep_idt &op_value = to_constant_expr(annotation).get_value();
-
-        if(op_value=="INVALID" ||
-           has_prefix(id2string(op_value), "INVALID-") ||
-           op_value=="NULL+offset")
-          dest=id2string(op_value);
-        else
-          return convert_norep(src, precedence);
-      }
-      else
-        return convert_with_precedence(annotation, precedence);
+      dest = id2string(value);
     }
     else
     {
@@ -2029,6 +2017,15 @@ std::string expr2ct::convert_constant(
   return dest;
 }
 
+std::string expr2ct::convert_annotated_pointer_constant(
+  const annotated_pointer_constant_exprt &src,
+  unsigned &precedence)
+{
+  const auto &annotation = src.symbolic_pointer();
+
+  return convert_with_precedence(annotation, precedence);
+}
+
 /// To get the C-like representation of a given boolean value.
 /// \param boolean_value: The value of the constant bool expression
 /// \return Returns a C-like representation of the boolean value, e.g. TRUE or
@@ -3888,6 +3885,12 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_constant)
     return convert_constant(to_constant_expr(src), precedence);
 
+  else if(src.id() == ID_annotated_pointer_constant)
+  {
+    return convert_annotated_pointer_constant(
+      to_annotated_pointer_constant_expr(src), precedence);
+  }
+
   else if(src.id()==ID_string_constant)
     return '"' + MetaString(id2string(to_string_constant(src).get_value())) +
            '"';

src/ansi-c/expr2c_class.h

@@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_expr.h>
 #include <util/std_code.h>
 
+class annotated_pointer_constant_exprt;
 class qualifierst;
 class namespacet;
 
@@ -257,6 +258,9 @@ class expr2ct
   // NOLINTNEXTLINE(whitespace/line_length)
   virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence);
   virtual std::string convert_constant_bool(bool boolean_value);
+  virtual std::string convert_annotated_pointer_constant(
+    const annotated_pointer_constant_exprt &src,
+    unsigned &precedence);
 
   std::string convert_norep(const exprt &src, unsigned &precedence);
 

src/goto-programs/json_expr.cpp

@@ -31,24 +31,7 @@ Author: Peter Schrammel
 
 static exprt simplify_json_expr(const exprt &src)
 {
-  if(src.id() == ID_constant)
-  {
-    if(src.type().id() == ID_pointer)
-    {
-      const constant_exprt &c = to_constant_expr(src);
-
-      if(
-        c.get_value() != ID_NULL &&
-        (!c.value_is_zero_string() || !config.ansi_c.NULL_is_zero) &&
-        src.operands().size() == 1 &&
-        to_unary_expr(src).op().id() != ID_constant)
-      // try to simplify the constant pointer
-      {
-        return simplify_json_expr(to_unary_expr(src).op());
-      }
-    }
-  }
-  else if(src.id() == ID_typecast)
+  if(src.id() == ID_typecast)
   {
     return simplify_json_expr(to_typecast_expr(src).op());
   }
@@ -303,25 +286,8 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
     {
       result["name"] = json_stringt("pointer");
       result["type"] = json_stringt(type_string);
-      exprt simpl_expr = simplify_json_expr(expr);
-      if(
-        simpl_expr.get(ID_value) == ID_NULL ||
-        // remove typecast on NULL
-        (simpl_expr.id() == ID_constant &&
-         simpl_expr.type().id() == ID_pointer &&
-         to_unary_expr(simpl_expr).op().get(ID_value) == ID_NULL))
-      {
+      if(constant_expr.get_value() == ID_NULL)
         result["data"] = json_stringt(value_string);
-      }
-      else if(simpl_expr.id() == ID_symbol)
-      {
-        const irep_idt &ptr_id = to_symbol_expr(simpl_expr).get_identifier();
-        identifiert identifier(id2string(ptr_id));
-        DATA_INVARIANT(
-          !identifier.components.empty(),
-          "pointer identifier should have non-empty components");
-        result["data"] = json_stringt(identifier.components.back());
-      }
     }
     else if(type.id() == ID_bool)
     {
@@ -339,6 +305,46 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
       result["name"] = json_stringt("unknown");
     }
   }
+  else if(expr.id() == ID_annotated_pointer_constant)
+  {
+    const annotated_pointer_constant_exprt &c =
+      to_annotated_pointer_constant_expr(expr);
+    exprt simpl_expr = simplify_json_expr(c.symbolic_pointer());
+
+    if(simpl_expr.id() == ID_symbol)
+    {
+      result["name"] = json_stringt("pointer");
+
+      const typet &type = expr.type();
+
+      std::unique_ptr<languaget> lang;
+      if(mode != ID_unknown)
+        lang = std::unique_ptr<languaget>(get_language_from_mode(mode));
+      if(!lang)
+        lang = std::unique_ptr<languaget>(get_default_language());
+
+      const typet &underlying_type =
+        type.id() == ID_c_bit_field
+          ? to_c_bit_field_type(type).underlying_type()
+          : type;
+
+      std::string type_string;
+      bool error = lang->from_type(underlying_type, type_string, ns);
+      CHECK_RETURN(!error);
+      result["type"] = json_stringt(type_string);
+
+      const irep_idt &ptr_id = to_symbol_expr(simpl_expr).get_identifier();
+      identifiert identifier(id2string(ptr_id));
+      DATA_INVARIANT(
+        !identifier.components.empty(),
+        "pointer identifier should have non-empty components");
+      result["data"] = json_stringt(identifier.components.back());
+    }
+    else if(simpl_expr.id() == ID_constant)
+      return json(simpl_expr, ns, mode);
+    else
+      result["name"] = json_stringt("unknown");
+  }
   else if(expr.id() == ID_array)
   {
     result["name"] = json_stringt("array");

src/solvers/flattening/bv_pointers.cpp

@@ -805,10 +805,8 @@ exprt bv_pointerst::bv_get_rec(
     numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
   pointer.offset=binary2integer(value_offset, true);
 
-  // we add the elaborated expression as operand
-  result.copy_to_operands(pointer_logic.pointer_expr(pointer, pt));
-
-  return std::move(result);
+  return annotated_pointer_constant_exprt{
+    bvrep, pointer_logic.pointer_expr(pointer, pt)};
 }
 
 bvt bv_pointerst::encode(std::size_t addr, const pointer_typet &type) const

src/util/format_expr.cpp

@@ -189,13 +189,6 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
     {
       return os << "INVALID-POINTER";
     }
-    else if(src.operands().size() == 1)
-    {
-      const auto &unary_expr = to_unary_expr(src);
-      const auto &pointer_type = to_pointer_type(src.type());
-      return os << "pointer(" << format(unary_expr.op()) << ", "
-                << format(pointer_type.base_type()) << ')';
-    }
     else
     {
       const auto &pointer_type = to_pointer_type(src.type());
@@ -308,6 +301,12 @@ void format_expr_configt::setup()
     return format_rec(os, to_constant_expr(expr));
   };
 
+  expr_map[ID_annotated_pointer_constant] =
+    [](std::ostream &os, const exprt &expr) -> std::ostream & {
+    const auto &annotated_pointer = to_annotated_pointer_constant_expr(expr);
+    return os << format(annotated_pointer.symbolic_pointer());
+  };
+
   expr_map[ID_typecast] =
     [](std::ostream &os, const exprt &expr) -> std::ostream & {
     return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "

src/util/irep_ids.def

@@ -867,6 +867,7 @@ IREP_ID_ONE(empty_union)
 IREP_ID_ONE(bitreverse)
 IREP_ID_ONE(saturating_minus)
 IREP_ID_ONE(saturating_plus)
+IREP_ID_ONE(annotated_pointer_constant)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree

src/util/pointer_expr.h

@@ -794,4 +794,83 @@ inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
   return ret;
 }
 
+/// \brief Pointer-typed bitvector constant annotated with the pointer
+/// expression that the bitvector is the numeric representation of.
+/// This variation of a constant expression is only used in the context of a
+/// GOTO trace, to give both the numeric value and the symbolic value of a
+/// pointer, e.g. numeric value "0xabcd0004" but symbolic value
+/// "&some_object + 4". The numeric value is stored in the usual value slot and
+/// the symbolic value is accessed using the `symbolic_pointer` method
+/// introduced by this class.
+class annotated_pointer_constant_exprt : public unary_exprt
+{
+public:
+  annotated_pointer_constant_exprt(
+    const irep_idt &_value,
+    const exprt &_pointer)
+    : unary_exprt(ID_annotated_pointer_constant, _pointer, _pointer.type())
+  {
+    set_value(_value);
+  }
+
+  const irep_idt &get_value() const
+  {
+    return get(ID_value);
+  }
+
+  void set_value(const irep_idt &value)
+  {
+    set(ID_value, value);
+  }
+
+  exprt &symbolic_pointer()
+  {
+    return op0();
+  }
+
+  const exprt &symbolic_pointer() const
+  {
+    return op0();
+  }
+};
+
+template <>
+inline bool can_cast_expr<annotated_pointer_constant_exprt>(const exprt &base)
+{
+  return base.id() == ID_annotated_pointer_constant;
+}
+
+inline void validate_expr(const annotated_pointer_constant_exprt &value)
+{
+  validate_operands(
+    value, 1, "Annotated pointer constant must have one operand");
+}
+
+/// \brief Cast an exprt to an \ref annotated_pointer_constant_exprt
+///
+/// \a expr must be known to be \ref annotated_pointer_constant_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref annotated_pointer_constant_exprt
+inline const annotated_pointer_constant_exprt &
+to_annotated_pointer_constant_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_annotated_pointer_constant);
+  const annotated_pointer_constant_exprt &ret =
+    static_cast<const annotated_pointer_constant_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_annotated_pointer_constant_expr(const exprt &)
+inline annotated_pointer_constant_exprt &
+to_annotated_pointer_constant_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_annotated_pointer_constant);
+  annotated_pointer_constant_exprt &ret =
+    static_cast<annotated_pointer_constant_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_POINTER_EXPR_H