Merge pull request #7228 from qinheping/assigns_inference

CONTRACTS: Add widening strategy into assigns inference

Author: feliperodri

regression/contracts/loop_assigns_inference/main.c renamed to regression/contracts/loop_assigns_inference-01/main.c

@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+#define SIZE 8
+
+void main()
+{
+  int *b = malloc(SIZE * sizeof(int));
+  for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
+    {
+      b[i] = 1;
+    }
+}

regression/contracts/loop_assigns_inference/test.desc renamed to regression/contracts/loop_assigns_inference-01/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks assigns clauses (i, __CPROVER_POINTER_OBJECT(b)) is inferred,
+and widened correctly.

regression/contracts/loop_assigns_inference-02/main.c

@@ -0,0 +1,15 @@
+#include <stdlib.h>
+
+#define SIZE 8
+
+void main()
+{
+  int b[SIZE];
+  for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
+    {
+      b[i] = 1;
+    }
+}

regression/contracts/loop_assigns_inference-02/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks assigns clauses (i, __CPROVER_POINTER_OBJECT(b)) is inferred,
+and widened correctly.

regression/contracts/loop_assigns_inference-03/main.c

@@ -208,12 +208,14 @@ void code_contractst::check_apply_loop_contracts(
     try
     {
       get_assigns(local_may_alias, loop, to_havoc);
-      // TODO: if the set contains pairs (i, a[i]),
-      // we must at least widen them to (i, pointer_object(a))
 
       // remove loop-local symbols from the inferred set
       cfg_info.erase_locals(to_havoc);
 
+      // If the set contains pairs (i, a[i]),
+      // we widen them to (i, __CPROVER_POINTER_OBJECT(a))
+      widen_assigns(to_havoc);
+
       log.debug() << "No loop assigns clause provided. Inferred targets: {";
       // Add inferred targets to the loop assigns clause.
       bool ran_once = false;

regression/contracts/loop_assigns_inference-03/test.desc

@@ -242,3 +242,29 @@ bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
   return id2string(comment).find(ASSIGNS_CLAUSE_REPLACEMENT_TRACKING) !=
          std::string::npos;
 }
+
+void widen_assigns(assignst &assigns)
+{
+  assignst result;
+
+  havoc_utils_is_constantt is_constant(assigns);
+
+  for(const auto &e : assigns)
+  {
+    if(e.id() == ID_index || e.id() == ID_dereference)
+    {
+      address_of_exprt address_of_expr(e);
+
+      // index or offset is non-constant.
+      if(!is_constant(address_of_expr))
+      {
+        result.emplace(pointer_object(address_of_expr));
+      }
+      else
+        result.emplace(e);
+    }
+    else
+      result.emplace(e);
+  }
+  assigns = result;
+}

src/goto-instrument/contracts/contracts.cpp

@@ -180,4 +180,11 @@ irep_idt make_assigns_clause_replacement_tracking_comment(
 /// \ref make_assigns_clause_replacement_tracking_comment.
 bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment);
 
+/// Widen expressions in \p assigns with the following strategy.
+/// If an expression is an array index or object dereference expression,
+/// with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant `i`,
+/// then replace it by the entire underlying object. Otherwise, e.g. for a[i] or
+/// *(b+i) when `i` is a known constant, keep the expression in the result.
+void widen_assigns(assignst &assigns);
+
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H