check safety of free(...)

Author: kroening

regression/cprover/safety/double_free1.desc

@@ -1,8 +1,8 @@
-KNOWNBUG
+CORE
 double_free1.c
-
-^EXIT=0$
+--safety
+^EXIT=10$
 ^SIGNAL=0$
-^program is safe / function main is safe / dereference line 6: SUCCESS$
-^program is safe / function main is safe / dereference line 8: REFUTED$
+^\[main\.free\.1\] line \d+ free argument must be valid dynamic object: SUCCESS$
+^\[main\.free\.2\] line \d+ free argument must be valid dynamic object: REFUTED$
 --

regression/cprover/safety/free_null1.c

@@ -0,0 +1,7 @@
+#include <stdlib.h>
+
+int main()
+{
+  free(0);             // safe
+  free((char *)0 + 1); // unsafe
+}

regression/cprover/safety/free_null1.desc

@@ -0,0 +1,8 @@
+CORE
+free_null1.c
+--safety
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.free\.1\] line \d+ free argument must be valid dynamic object: SUCCESS$
+^\[main\.free\.2\] line \d+ free argument must be valid dynamic object: REFUTED$
+--

src/cprover/axioms.cpp

@@ -108,7 +108,6 @@ void axiomst::live_object_fc()
     {
       if(a_it->state() != b_it->state())
         continue;
-      auto a_op = a_it->address();
       auto operands_equal = same_object(a_it->address(), b_it->address());
       auto implication =
         implies_exprt(operands_equal, equal_exprt(*a_it, *b_it));
@@ -118,6 +117,27 @@ void axiomst::live_object_fc()
   }
 }
 
+void axiomst::is_dynamic_object_fc()
+{
+  // quadratic
+  for(auto a_it = is_dynamic_object_exprs.begin();
+      a_it != is_dynamic_object_exprs.end();
+      a_it++)
+  {
+    for(auto b_it = std::next(a_it); b_it != is_dynamic_object_exprs.end();
+        b_it++)
+    {
+      if(a_it->state() != b_it->state())
+        continue;
+      auto operands_equal = same_object(a_it->address(), b_it->address());
+      auto implication =
+        implies_exprt(operands_equal, equal_exprt(*a_it, *b_it));
+      std::cout << "IS_DYNAMIC_OBJECT: " << format(implication) << '\n';
+      dest << replace(implication);
+    }
+  }
+}
+
 void axiomst::object_size()
 {
   for(const auto &src : object_size_exprs)
@@ -182,6 +202,7 @@ exprt axiomst::replace(exprt src)
 
   if(
     src.id() == ID_evaluate || src.id() == ID_state_is_cstring ||
+    src.id() == ID_state_is_dynamic_object ||
     src.id() == ID_state_object_size || src.id() == ID_state_live_object ||
     src.id() == ID_state_r_ok || src.id() == ID_state_w_ok ||
     src.id() == ID_state_rw_ok || src.id() == ID_allocate)
@@ -275,6 +296,11 @@ void axiomst::node(const exprt &src)
       dest << instance;
     }
   }
+  else if(src.id() == ID_state_is_dynamic_object)
+  {
+    const auto &is_dynamic_object_expr = to_state_is_dynamic_object_expr(src);
+    is_dynamic_object_exprs.insert(is_dynamic_object_expr);
+  }
   else if(src.id() == ID_allocate)
   {
     const auto &allocate_expr = to_allocate_expr(src);
@@ -299,10 +325,19 @@ void axiomst::node(const exprt &src)
 
     // pointer_offset(allocate(ς, s)) = 0
     auto pointer_offset_expr = pointer_offset(allocate_expr);
+    //pointer_offset_exprs.insert(pointer_offset_expr);
     auto instance3 =
       replace(equal_exprt(pointer_offset_expr, from_integer(0, pointer_offset_expr.type())));
     std::cout << "ALLOCATE3: " << format(instance3) << "\n";
     dest << instance3;
+
+    // is_dynamic_object(ς, allocate(ς, s))
+    auto is_dynamic_object_expr =
+      state_is_dynamic_object_exprt(allocate_expr.state(), allocate_expr);
+    is_dynamic_object_exprs.insert(is_dynamic_object_expr);
+    auto instance4 = replace(is_dynamic_object_expr);
+    std::cout << "ALLOCATE4: " << format(instance4) << "\n";
+    dest << instance4;
   }
   else if(src.id() == ID_deallocate_state)
   {
@@ -407,4 +442,5 @@ void axiomst::emit()
   ok_fc();
   live_object_fc();
   object_size_fc();
+  is_dynamic_object_fc();
 }

src/cprover/axioms.h

@@ -64,6 +64,9 @@ class axiomst
   std::set<state_is_cstring_exprt> is_cstring_exprs;
   void is_cstring_fc();
 
+  std::set<state_is_dynamic_object_exprt> is_dynamic_object_exprs;
+  void is_dynamic_object_fc();
+
   std::set<state_live_object_exprt> live_object_exprs;
   void live_object_fc();
 

src/cprover/c_safety_checks.cpp

@@ -206,6 +206,37 @@ void c_safety_checks(
     it->apply([&f, &ns, &dest](const exprt &expr) {
       c_safety_checks(f, expr, ns, dest);
     });
+
+    if(it->is_function_call())
+    {
+      const auto &function = it->call_function();
+      if(function.id() == ID_symbol)
+      {
+        const auto &identifier = to_symbol_expr(function).get_identifier();
+        if(identifier == "free")
+        {
+          if(
+            it->call_arguments().size() == 1 &&
+            it->call_arguments()[0].type().id() == ID_pointer)
+          {
+            // Must be dynamically allocated and still alive,
+            // or, alternatively, NULL.
+            const auto &pointer = it->call_arguments()[0];
+            auto condition = or_exprt(
+              equal_exprt(
+                pointer, null_pointer_exprt(to_pointer_type(pointer.type()))),
+              and_exprt(
+                live_object_exprt(pointer), is_dynamic_object_exprt(pointer)));
+            auto source_location = it->source_location();
+            source_location.set_property_class("free");
+            source_location.set_comment(
+              "free argument must be valid dynamic object");
+            dest.add(goto_programt::make_assertion(condition, source_location));
+          }
+        }
+      }
+    }
+
     std::size_t n = dest.instructions.size();
     if(n != 0)
     {
@@ -222,6 +253,9 @@ void c_safety_checks(goto_modelt &goto_model)
 
   for(auto &f : goto_model.goto_functions.function_map)
     c_safety_checks(f, ns);
+
+  // update the numbering
+  goto_model.goto_functions.compute_location_numbers();
 }
 
 void no_assertions(goto_functionst::function_mapt::value_type &f)

src/cprover/format_hooks.cpp

@@ -75,9 +75,19 @@ void format_hooks()
   add_format_hook(
     ID_state_is_cstring,
     [](std::ostream &os, const exprt &expr) -> std::ostream & {
-      const auto &is_cstring_expr = to_binary_expr(expr);
-      return os << "is_cstring(" << format(is_cstring_expr.op0()) << ", "
-                << format(is_cstring_expr.op1()) << ')';
+      const auto &is_cstring_expr = to_state_is_cstring_expr(expr);
+      return os << "is_cstring(" << format(is_cstring_expr.state()) << ", "
+                << format(is_cstring_expr.address()) << ')';
+    });
+
+  add_format_hook(
+    ID_state_is_dynamic_object,
+    [](std::ostream &os, const exprt &expr) -> std::ostream & {
+      const auto &is_dynamic_object_expr =
+        to_state_is_dynamic_object_expr(expr);
+      return os << "is_dynamic_object("
+                << format(is_dynamic_object_expr.state()) << ", "
+                << format(is_dynamic_object_expr.address()) << ')';
     });
 
   add_format_hook(

src/cprover/simplify_state_expr.cpp

@@ -211,6 +211,29 @@ exprt simplify_live_object_expr(binary_exprt src, const namespacet &ns)
   return std::move(src);
 }
 
+exprt simplify_is_dynamic_object_expr(state_is_dynamic_object_exprt src)
+{
+  const auto &pointer = src.address();
+
+  auto object = simplify_object_expression(pointer);
+
+  if(object.id() == ID_object_address)
+  {
+    // these are not dynamic
+    return false_exprt();
+  }
+
+  // A store does not affect the result.
+  // is_dynamic_object(ς[A:=V]), p) --> is_dynamic_object(ς, p)
+  if(src.state().id() == ID_update_state)
+  {
+    src.state() = to_update_state_expr(src.state()).state();
+    return std::move(src);
+  }
+
+  return std::move(src);
+}
+
 exprt simplify_object_size_expr(
   state_object_size_exprt src,
   const namespacet &ns)
@@ -414,6 +437,11 @@ exprt simplify_state_expr_node(
     return simplify_is_cstring_expr(
       to_state_is_cstring_expr(src), address_taken, ns);
   }
+  else if(src.id() == ID_state_is_dynamic_object)
+  {
+    return simplify_is_dynamic_object_expr(
+      to_state_is_dynamic_object_expr(src));
+  }
   else if(src.id() == ID_plus)
   {
     auto &plus_expr = to_plus_expr(src);

src/cprover/state.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_expr.h>
 
 const irep_idt ID_state_is_cstring = "state_is_cstring";
+const irep_idt ID_state_is_dynamic_object = "state_is_dynamic_object";
 const irep_idt ID_state_live_object = "state_live_object";
 const irep_idt ID_state_object_size = "state_object_size";
 const irep_idt ID_state_r_ok = "state_r_ok";

src/cprover/state.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_expr.h>
 
 extern const irep_idt ID_state_is_cstring;
+extern const irep_idt ID_state_is_dynamic_object;
 extern const irep_idt ID_state_live_object;
 extern const irep_idt ID_state_object_size;
 extern const irep_idt ID_state_r_ok;
@@ -387,6 +388,62 @@ inline state_is_cstring_exprt &to_state_is_cstring_expr(exprt &expr)
   return ret;
 }
 
+class state_is_dynamic_object_exprt : public binary_predicate_exprt
+{
+public:
+  state_is_dynamic_object_exprt(exprt state, exprt address)
+    : binary_predicate_exprt(
+        std::move(state),
+        ID_state_is_dynamic_object,
+        std::move(address))
+  {
+    PRECONDITION(this->state().type().id() == ID_state);
+    PRECONDITION(this->address().type().id() == ID_pointer);
+  }
+
+  const exprt &state() const
+  {
+    return op0();
+  }
+
+  exprt &state()
+  {
+    return op0();
+  }
+
+  const exprt &address() const
+  {
+    return op1();
+  }
+};
+
+/// \brief Cast an exprt to a \ref state_is_dynamic_object_exprt
+///
+/// \a expr must be known to be \ref state_is_dynamic_object_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref state_is_dynamic_object_exprt
+inline const state_is_dynamic_object_exprt &
+to_state_is_dynamic_object_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_state_is_dynamic_object);
+  const state_is_dynamic_object_exprt &ret =
+    static_cast<const state_is_dynamic_object_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_state_is_dynamic_object_expr(const exprt &)
+inline state_is_dynamic_object_exprt &
+to_state_is_dynamic_object_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_state_is_dynamic_object);
+  state_is_dynamic_object_exprt &ret =
+    static_cast<state_is_dynamic_object_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 class state_object_size_exprt : public binary_exprt
 {
 public: