axioms for state_object_size

Author: kroening

regression/cprover/safety/array_bounds2.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 array_bounds2.c
 --safety
 ^EXIT=10$

regression/cprover/safety/r_ok5.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 r_ok5.c
 
 ^EXIT=0$

regression/cprover/safety/simple_equality1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 simple_equality1.c
 --safety
 ^EXIT=10$

src/cprover/axioms.cpp

@@ -15,6 +15,7 @@ Module: Axioms
 #include <util/c_types.h>
 #include <util/format_expr.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
 
 #include "simplify_state_expr.h"
 #include "state.h"
@@ -96,6 +97,24 @@ void axiomst::is_cstring(decision_proceduret &dest)
   }
 }
 
+void axiomst::live_object(decision_proceduret &dest)
+{
+}
+
+void axiomst::object_size(decision_proceduret &dest)
+{
+  for(const auto &src : object_size_exprs)
+  {
+    auto src_simplified = simplify_state_expr_node(src, address_taken, ns);
+    if(src_simplified != src)
+    {
+      auto equal = equal_exprt(src, src_simplified);
+      std::cout << "OBJECT_SIZE: " << format(equal) << '\n';
+      dest << replace(equal);
+    }
+  }
+}
+
 exprt axiomst::replace(exprt src)
 {
   src.type() = replace(src.type());
@@ -211,23 +230,25 @@ void axiomst::node(const exprt &src, decision_proceduret &dest)
 
     {
       // X_ok(p, s)
-      //  --> live_object(p) ∧ offset(p)≥0 ∧ offset(p)+s≤object_size(p)
-      auto live_object =
-        binary_predicate_exprt(state, ID_state_live_object, pointer);
+      //  <--> live_object(p) ∧ offset(p)≥0 ∧ offset(p)+s≤object_size(p)
+      auto live_object = state_live_object_exprt(state, pointer);
+      live_object_exprs.insert(live_object);
+      auto live_object_simplified =
+        simplify_state_expr_node(live_object, address_taken, ns);
       auto ssize_type = signed_size_type();
       auto offset = pointer_offset_exprt(pointer, ssize_type);
       auto offset_simplified =
         simplify_state_expr_node(offset, address_taken, ns);
       auto lower = binary_relation_exprt(
         offset_simplified, ID_ge, from_integer(0, ssize_type));
-      auto object_size =
-        binary_exprt(state, ID_state_object_size, pointer, ssize_type);
+      auto object_size = state_object_size_exprt(state, pointer, ssize_type);
+      object_size_exprs.insert(object_size);
       auto size_casted = typecast_exprt::conditional_cast(size, ssize_type);
       auto upper = binary_relation_exprt(
         plus_exprt(offset_simplified, size_casted), ID_le, object_size);
 
-      auto instance =
-        replace(implies_exprt(src, and_exprt(live_object, lower, upper)));
+      auto instance = replace(
+        equal_exprt(src, and_exprt(live_object_simplified, lower, upper)));
       std::cout << "AXIOMd: " << format(instance) << "\n";
       dest << instance;
     }
@@ -255,4 +276,6 @@ void axiomst::emit(decision_proceduret &dest)
 
   evaluate(dest);
   is_cstring(dest);
+  live_object(dest);
+  object_size(dest);
 }

src/cprover/simplify_state_expr.cpp

@@ -395,11 +395,29 @@ exprt simplify_state_expr_node(
   {
     auto &pointer_offset_expr = to_pointer_offset_expr(src);
 
-    // pointer_offset(❝x❞) -> 0
     if(pointer_offset_expr.pointer().id() == ID_object_address)
     {
+      // pointer_offset(❝x❞) -> 0
       return from_integer(0, pointer_offset_expr.type());
     }
+    else if(pointer_offset_expr.pointer().id() == ID_element_address)
+    {
+      const auto &element_address_expr =
+        to_element_address_expr(pointer_offset_expr.pointer());
+      if(element_address_expr.base().id() == ID_object_address)
+      {
+        // pointer_offset(element_address(❝x❞, y)) -> y*sizeof(x)
+        auto size_opt = size_of_expr(element_address_expr.element_type(), ns);
+        if(size_opt.has_value())
+        {
+          auto product = mult_exprt(
+            typecast_exprt::conditional_cast(
+              element_address_expr.index(), src.type()),
+            typecast_exprt::conditional_cast(*size_opt, src.type()));
+          return product;
+        }
+      }
+    }
   }
   else if(src.id() == ID_state_object_size)
   {