Handle infinity in the back-end and in the simplifier

We need to support at least object_size operations over infinity in the
back-end as the postponed evaluation iterates over all objects, which
may include ones that have infinite size.

Author: tautschnig

regression/cbmc/infinity1/main.c

@@ -0,0 +1,6 @@
+int A[__CPROVER_constant_infinity_uint];
+
+int main()
+{
+  __CPROVER_assert(__CPROVER_OBJECT_SIZE(A) > 0, "infinity is positive");
+}

regression/cbmc/infinity1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/solvers/flattening/bv_pointers.cpp

@@ -941,9 +941,17 @@ void bv_pointerst::do_postponed(
       if(!size_expr.has_value())
         continue;
 
-      const exprt object_size = typecast_exprt::conditional_cast(
+      exprt object_size = typecast_exprt::conditional_cast(
         size_expr.value(), postponed_object_size->type());
 
+      if(
+        size_expr->id() == ID_infinity &&
+        can_cast_type<integer_bitvector_typet>(object_size.type()))
+      {
+        object_size = to_integer_bitvector_type(postponed_object_size->type())
+                        .largest_expr();
+      }
+
       // only compare object part
       pointer_typet pt = pointer_type(expr.type());
       bvt bv = object_literals(encode(number, pt), type);

src/solvers/smt2/smt2_conv.cpp

@@ -245,6 +245,12 @@ void smt2_convt::define_object_size(
   {
     const typet &type = o.type();
     auto size_expr = size_of_expr(type, ns);
+    if(
+      size_expr.has_value() && size_expr->id() == ID_infinity &&
+      can_cast_type<integer_bitvector_typet>(expr.type()))
+    {
+      size_expr = to_integer_bitvector_type(expr.type()).largest_expr();
+    }
     const auto object_size =
       numeric_cast<mp_integer>(size_expr.value_or(nil_exprt()));
 
@@ -4962,6 +4968,12 @@ void smt2_convt::find_symbols(const exprt &expr)
       convert_type(object_size->type());
       out << ")"
           << "\n";
+      out << "(declare-fun |op_" << id << "| () ";
+      convert_type(object_size->op().type());
+      out << ")\n";
+      out << "(assert (= |op_" << id << "| ";
+      convert_expr(object_size->op());
+      out << "))\n";
 
       object_sizes[*object_size] = id;
     }

src/util/pointer_offset_size.cpp

@@ -300,6 +300,8 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
 
     if(size.is_nil())
       return {};
+    else if(size.id() == ID_infinity)
+      return infinity_exprt{sub.value().type()};
 
     const auto size_casted =
       typecast_exprt::conditional_cast(size, sub.value().type());

src/util/simplify_expr_int.cpp

@@ -1263,6 +1263,29 @@ simplify_exprt::simplify_inequality(const binary_relation_exprt &expr)
     return simplify_inequality_pointer_object(expr);
   }
 
+  if(tmp0.id() == ID_infinity)
+  {
+    if(expr.id() == ID_ge)
+      return true_exprt{};
+    else if(expr.id() == ID_gt)
+      return changed(simplify_inequality(notequal_exprt{tmp0, tmp1}));
+    else if(expr.id() == ID_le)
+      return changed(simplify_inequality(equal_exprt{tmp0, tmp1}));
+    else if(expr.id() == ID_lt)
+      return false_exprt{};
+  }
+  else if(tmp1.id() == ID_infinity)
+  {
+    if(expr.id() == ID_ge)
+      return changed(simplify_inequality(equal_exprt{tmp0, tmp1}));
+    else if(expr.id() == ID_gt)
+      return false_exprt{};
+    else if(expr.id() == ID_le)
+      return true_exprt{};
+    else if(expr.id() == ID_lt)
+      return changed(simplify_inequality(notequal_exprt{tmp0, tmp1}));
+  }
+
   if(tmp0.type().id()==ID_c_enum_tag)
     tmp0.type()=ns.follow_tag(to_c_enum_tag_type(tmp0.type()));
 
@@ -1568,6 +1591,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
     return changed(simplify_if(if_expr));
   }
 
+  if(expr.op0().id() == ID_infinity)
+  {
+    if(expr.id() == ID_equal)
+      return false_exprt{};
+    else if(expr.id() == ID_notequal)
+      return true_exprt{};
+  }
+
   // do we deal with pointers?
   if(expr.op1().type().id()==ID_pointer)
   {