Merge pull request #6804 from thomasspriggs/tas/object_size_exprt

Add class for object size expressions

Author: thomasspriggs

src/ansi-c/c_typecheck_expr.cpp

@@ -2363,8 +2363,7 @@ exprt c_typecheck_baset::do_special_functions(
 
     typecheck_function_call_arguments(expr);
 
-    unary_exprt object_size_expr(
-      ID_object_size, expr.arguments()[0], size_type());
+    object_size_exprt object_size_expr(expr.arguments()[0], size_type());
     object_size_expr.add_source_location() = source_location;
 
     return std::move(object_size_expr);

src/ansi-c/goto_check_c.cpp

@@ -1476,7 +1476,7 @@ bool goto_check_ct::requires_pointer_primitive_check(const exprt &expr)
   // pointer_object and pointer_offset just extract a subset of bits from the
   // pointer. If that pointer was unconstrained (non-deterministic), the result
   // will equally be non-deterministic.
-  return expr.id() == ID_object_size || expr.id() == ID_r_ok ||
+  return can_cast_expr<object_size_exprt>(expr) || expr.id() == ID_r_ok ||
          expr.id() == ID_w_ok || expr.id() == ID_rw_ok ||
          expr.id() == ID_is_dynamic_object;
 }

src/solvers/flattening/bv_pointers.cpp

@@ -700,14 +700,15 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     return bv_utils.sign_extension(offset_bv, width);
   }
   else if(
-    expr.id() == ID_object_size &&
-    to_unary_expr(expr).op().type().id() == ID_pointer)
+    const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
   {
     // we postpone until we know the objects
-    std::size_t width=boolbv_width(expr.type());
+    std::size_t width = boolbv_width(object_size->type());
 
     postponed_list.emplace_back(
-      prop.new_variables(width), convert_bv(to_unary_expr(expr).op()), expr);
+      prop.new_variables(width),
+      convert_bv(object_size->pointer()),
+      *object_size);
 
     return postponed_list.back().bv;
   }
@@ -935,10 +936,11 @@ void bv_pointerst::do_postponed(
       prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
-  else if(postponed.expr.id()==ID_object_size)
+  else if(
+    const auto postponed_object_size =
+      expr_try_dynamic_cast<object_size_exprt>(postponed.expr))
   {
-    const auto &type =
-      to_pointer_type(to_unary_expr(postponed.expr).op().type());
+    const auto &type = to_pointer_type(postponed_object_size->pointer().type());
     const auto &objects = pointer_logic.objects;
     std::size_t number=0;
 
@@ -955,7 +957,7 @@ void bv_pointerst::do_postponed(
         continue;
 
       const exprt object_size = typecast_exprt::conditional_cast(
-        size_expr.value(), postponed.expr.type());
+        size_expr.value(), postponed_object_size->type());
 
       // only compare object part
       pointer_typet pt = pointer_type(expr.type());

src/solvers/smt2/smt2_conv.cpp

@@ -25,7 +25,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/invariant.h>
 #include <util/mathematical_expr.h>
 #include <util/namespace.h>
-#include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>
@@ -233,10 +232,9 @@ void smt2_convt::write_footer()
 
 void smt2_convt::define_object_size(
   const irep_idt &id,
-  const exprt &expr)
+  const object_size_exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_object_size);
-  const exprt &ptr = to_unary_expr(expr).op();
+  const exprt &ptr = expr.pointer();
   std::size_t size_width = boolbv_width(expr.type());
   std::size_t pointer_width = boolbv_width(ptr.type());
   std::size_t number = 0;
@@ -2018,9 +2016,10 @@ void smt2_convt::convert_expr(const exprt &expr)
 
     out << ")"; // mk-... or concat
   }
-  else if(expr.id()==ID_object_size)
+  else if(
+    const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
   {
-    out << "|" << object_sizes[expr] << "|";
+    out << "|" << object_sizes[*object_size] << "|";
   }
   else if(expr.id()==ID_let)
   {
@@ -4848,22 +4847,18 @@ void smt2_convt::find_symbols(const exprt &expr)
       defined_expressions[expr]=id;
     }
   }
-  else if(expr.id() == ID_object_size)
+  else if(
+    const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
   {
-    const exprt &op = to_unary_expr(expr).op();
-
-    if(op.type().id()==ID_pointer)
+    if(object_sizes.find(*object_size) == object_sizes.end())
     {
-      if(object_sizes.find(expr)==object_sizes.end())
-      {
-        const irep_idt id =
-          "object_size." + std::to_string(object_sizes.size());
-        out << "(declare-fun |" << id << "| () ";
-        convert_type(expr.type());
-        out << ")" << "\n";
+      const irep_idt id = "object_size." + std::to_string(object_sizes.size());
+      out << "(declare-fun |" << id << "| () ";
+      convert_type(object_size->type());
+      out << ")"
+          << "\n";
 
-        object_sizes[expr]=id;
-      }
+      object_sizes[*object_size] = id;
     }
   }
   // clang-format off

src/solvers/smt2/smt2_conv.h

@@ -10,13 +10,14 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_SMT2_SMT2_CONV_H
 #define CPROVER_SOLVERS_SMT2_SMT2_CONV_H
 
+#include <util/pointer_expr.h>
+#include <util/std_expr.h>
+#include <util/threeval.h>
+
 #include <map>
 #include <set>
 #include <sstream>
 
-#include <util/std_expr.h>
-#include <util/threeval.h>
-
 #if !HASH_CODE
 #  include <util/irep_hash_container.h>
 #endif
@@ -216,7 +217,7 @@ class smt2_convt : public stack_decision_proceduret
   void convert_address_of_rec(
     const exprt &expr, const pointer_typet &result_type);
 
-  void define_object_size(const irep_idt &id, const exprt &expr);
+  void define_object_size(const irep_idt &id, const object_size_exprt &expr);
 
   // keeps track of all non-Boolean symbols and their value
   struct identifiert
@@ -256,7 +257,7 @@ class smt2_convt : public stack_decision_proceduret
   /// smt2 formula.
   std::unordered_map<irep_idt, bool> set_values;
 
-  defined_expressionst object_sizes;
+  std::map<object_size_exprt, irep_idt> object_sizes;
 
   typedef std::set<std::string> smt2_identifierst;
   smt2_identifierst smt2_identifiers;

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1192,6 +1192,15 @@ static smt_termt convert_expr_to_smt(
     "Generation of SMT formula for vector expression: " + vector.pretty());
 }
 
+static smt_termt convert_expr_to_smt(
+  const object_size_exprt &object_size,
+  const sub_expression_mapt &converted)
+{
+  UNIMPLEMENTED_FEATURE(
+    "Generation of SMT formula for object_size expression: " +
+    object_size.pretty());
+}
+
 static smt_termt
 convert_expr_to_smt(const let_exprt &let, const sub_expression_mapt &converted)
 {
@@ -1530,12 +1539,10 @@ static smt_termt dispatch_expr_to_smt_conversion(
   {
     return convert_expr_to_smt(*vector, converted);
   }
-#if 0
-  else if(expr.id()==ID_object_size)
+  if(const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
   {
-    out << "|" << object_sizes[expr] << "|";
+    return convert_expr_to_smt(*object_size, converted);
   }
-#endif
   if(const auto let = expr_try_dynamic_cast<let_exprt>(expr))
   {
     return convert_expr_to_smt(*let, converted);

src/util/pointer_expr.h

@@ -989,4 +989,39 @@ inline pointer_object_exprt &to_pointer_object_expr(exprt &expr)
   return ret;
 }
 
+/// Expression for finding the size (in bytes) of the object a pointer points
+/// to.
+class object_size_exprt : public unary_exprt
+{
+public:
+  explicit object_size_exprt(exprt pointer, typet type)
+    : unary_exprt(ID_object_size, std::move(pointer), std::move(type))
+  {
+  }
+
+  exprt &pointer()
+  {
+    return op();
+  }
+
+  const exprt &pointer() const
+  {
+    return op();
+  }
+};
+
+template <>
+inline bool can_cast_expr<object_size_exprt>(const exprt &base)
+{
+  return base.id() == ID_object_size;
+}
+
+inline void validate_expr(const object_size_exprt &value)
+{
+  validate_operands(value, 1, "Object size expression must have one operand.");
+  DATA_INVARIANT(
+    can_cast_type<pointer_typet>(value.pointer().type()),
+    "Object size expression must have pointer typed operand.");
+}
+
 #endif // CPROVER_UTIL_POINTER_EXPR_H

src/util/pointer_predicates.cpp

@@ -32,7 +32,7 @@ exprt same_object(const exprt &p1, const exprt &p2)
 
 exprt object_size(const exprt &pointer)
 {
-  return unary_exprt(ID_object_size, pointer, size_type());
+  return object_size_exprt(pointer, size_type());
 }
 
 exprt pointer_offset(const exprt &pointer)

src/util/simplify_expr.cpp

@@ -2398,9 +2398,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
   {
     r = simplify_is_invalid_pointer(to_unary_expr(expr));
   }
-  else if(expr.id()==ID_object_size)
+  else if(
+    const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
   {
-    r = simplify_object_size(to_unary_expr(expr));
+    r = simplify_object_size(*object_size);
   }
   else if(expr.id()==ID_good_pointer)
   {

src/util/simplify_expr_class.h

@@ -58,6 +58,7 @@ class multi_ary_exprt;
 class mult_exprt;
 class namespacet;
 class not_exprt;
+class object_size_exprt;
 class plus_exprt;
 class pointer_object_exprt;
 class pointer_offset_exprt;
@@ -173,7 +174,7 @@ class simplify_exprt
   NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &);
   NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &);
   NODISCARD resultt<> simplify_pointer_object(const pointer_object_exprt &);
-  NODISCARD resultt<> simplify_object_size(const unary_exprt &);
+  NODISCARD resultt<> simplify_object_size(const object_size_exprt &);
   NODISCARD resultt<> simplify_is_dynamic_object(const unary_exprt &);
   NODISCARD resultt<> simplify_is_invalid_pointer(const unary_exprt &);
   NODISCARD resultt<> simplify_good_pointer(const unary_exprt &);