Merge pull request #8313 from qinheping/feature/get_assigns_ignore_cprover_variable

[CONTRACTS] Ignore cprover symbols in loop assigns inference

Author: qinheping

regression/contracts-dfcc/invar_loop_with_goto/main.c

@@ -0,0 +1,38 @@
+#include <assert.h>
+typedef struct test
+{
+  int id;
+} test;
+
+int main()
+{
+  int r, s = 1;
+  __CPROVER_assume(r >= 0);
+  while(r > 0)
+    // clang-format off
+    __CPROVER_loop_invariant(r >= 0 && s == 1)
+    __CPROVER_decreases(r)
+    // clang-format on
+    {
+      s = 1;
+      goto label_1;
+
+      if(1 == 1)
+        goto label_0;
+
+      test newAlloc0 = {0};
+
+      if(1 == 1)
+        goto label_1;
+
+    label_0:
+      r--;
+
+    label_1:
+      r--;
+    }
+  assert(r == 0);
+  assert(s == 1);
+
+  return 0;
+}

regression/contracts-dfcc/invar_loop_with_goto/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks the assigns inference correctly
+ignore __CPROVER_going_to variables.

regression/contracts/invar_loop_with_goto/main.c

@@ -0,0 +1,38 @@
+#include <assert.h>
+typedef struct test
+{
+  int id;
+} test;
+
+int main()
+{
+  int r, s = 1;
+  __CPROVER_assume(r >= 0);
+  while(r > 0)
+    // clang-format off
+    __CPROVER_loop_invariant(r >= 0 && s == 1)
+    __CPROVER_decreases(r)
+    // clang-format on
+    {
+      s = 1;
+      goto label_1;
+
+      if(1 == 1)
+        goto label_0;
+
+      test newAlloc0 = {0};
+
+      if(1 == 1)
+        goto label_1;
+
+    label_0:
+      r--;
+
+    label_1:
+      r--;
+    }
+  assert(r == 0);
+  assert(s == 1);
+
+  return 0;
+}

regression/contracts/invar_loop_with_goto/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks the assigns inference correctly
+ignore __CPROVER_going_to variables.

src/goto-instrument/contracts/contracts.cpp

@@ -220,7 +220,7 @@ void code_contractst::check_apply_loop_contracts(
     // and the inferred aliasing relation.
     try
     {
-      get_assigns(local_may_alias, loop, to_havoc);
+      infer_loop_assigns(local_may_alias, loop, to_havoc);
 
       // remove loop-local symbols from the inferred set
       cfg_info.erase_locals(to_havoc);

src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp

@@ -13,6 +13,7 @@ Author: Remi Delmas, [email protected]
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 
+#include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/havoc_utils.h>
 
 #include "dfcc_root_object.h"
@@ -53,7 +54,7 @@ assignst dfcc_infer_loop_assigns(
 {
   // infer
   assignst assigns;
-  get_assigns(local_may_alias, loop_instructions, assigns);
+  infer_loop_assigns(local_may_alias, loop_instructions, assigns);
 
   // compute locals
   std::unordered_set<irep_idt> loop_locals;

src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp

@@ -151,5 +151,7 @@ bool dfcc_is_cprover_static_symbol(const irep_idt &id)
   init_static_symbols(static_symbols);
   return static_symbols.find(id) != static_symbols.end() ||
          // auto objects from pointer derefs
-         has_suffix(id2string(id), "$object");
+         has_suffix(id2string(id), "$object") ||
+         // going_to variables converted from goto statements
+         has_prefix(id2string(id), CPROVER_PREFIX "going_to");
 }

src/goto-instrument/contracts/instrument_spec_assigns.cpp

@@ -19,6 +19,7 @@ Date: January 2022
 #include <util/fresh_symbol.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/prefix.h>
 #include <util/simplify_expr.h>
 
 #include <ansi-c/c_expr.h>
@@ -147,6 +148,13 @@ void instrument_spec_assignst::check_inclusion_assignment(
   const exprt &lhs,
   goto_programt &dest) const
 {
+  // Don't check assignable for CPROVER symbol
+  if(
+    lhs.id() == ID_symbol &&
+    has_prefix(id2string(to_symbol_expr(lhs).get_identifier()), CPROVER_PREFIX))
+  {
+    return;
+  }
   // create temporary car but do not track
   const auto car = create_car_expr(true_exprt{}, lhs);
   create_snapshot(car, dest);

src/goto-instrument/contracts/utils.cpp

@@ -18,6 +18,7 @@ Date: September 2021
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/symbol.h>
 
@@ -338,6 +339,22 @@ bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
          std::string::npos;
 }
 
+void infer_loop_assigns(
+  const local_may_aliast &local_may_alias,
+  const loopt &loop,
+  assignst &assigns)
+{
+  // Assign targets should not include cprover symbols.
+  get_assigns(local_may_alias, loop, assigns, [](const exprt &e) {
+    if(e.id() == ID_symbol)
+    {
+      const auto &s = expr_try_dynamic_cast<symbol_exprt>(e);
+      return !has_prefix(id2string(s->get_identifier()), CPROVER_PREFIX);
+    }
+    return true;
+  });
+}
+
 void widen_assigns(assignst &assigns, const namespacet &ns)
 {
   assignst result;

src/goto-instrument/contracts/utils.h

@@ -16,7 +16,9 @@ Date: September 2021
 #include <goto-programs/goto_model.h>
 #include <goto-programs/loop_ids.h>
 
+#include <analyses/local_may_alias.h>
 #include <goto-instrument/havoc_utils.h>
+#include <goto-instrument/loop_utils.h>
 
 #include <vector>
 
@@ -214,6 +216,12 @@ 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);
 
+/// Infer loop assigns using alias analysis result `local_may_alias`.
+void infer_loop_assigns(
+  const local_may_aliast &local_may_alias,
+  const loopt &loop,
+  assignst &assigns);
+
 /// 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`,

src/goto-instrument/loop_utils.cpp

@@ -42,9 +42,24 @@ void get_assigns_lhs(
   const exprt &lhs,
   assignst &assigns)
 {
-  if(lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index)
+  get_assigns_lhs(
+    local_may_alias, t, lhs, assigns, [](const exprt &e) { return true; });
+}
+
+void get_assigns_lhs(
+  const local_may_aliast &local_may_alias,
+  goto_programt::const_targett t,
+  const exprt &lhs,
+  assignst &assigns,
+  std::function<bool(const exprt &)> predicate)
+{
+  if(
+    (lhs.id() == ID_symbol || lhs.id() == ID_member || lhs.id() == ID_index) &&
+    predicate(lhs))
+  {
     assigns.insert(lhs);
-  else if(lhs.id()==ID_dereference)
+  }
+  else if(lhs.id() == ID_dereference)
   {
     const pointer_arithmetict ptr(to_dereference_expr(lhs).pointer());
     for(const auto &mod : local_may_alias.get(t, ptr.pointer))
@@ -54,15 +69,18 @@ void get_assigns_lhs(
       {
         continue;
       }
+      exprt to_insert;
       if(ptr.offset.is_nil())
-        assigns.insert(dereference_exprt{typed_mod});
+        to_insert = dereference_exprt{typed_mod};
       else
-        assigns.insert(dereference_exprt{plus_exprt{typed_mod, ptr.offset}});
+        to_insert = dereference_exprt{plus_exprt{typed_mod, ptr.offset}};
+      if(predicate(to_insert))
+        assigns.insert(std::move(to_insert));
     }
   }
-  else if(lhs.id()==ID_if)
+  else if(lhs.id() == ID_if)
   {
-    const if_exprt &if_expr=to_if_expr(lhs);
+    const if_exprt &if_expr = to_if_expr(lhs);
 
     get_assigns_lhs(local_may_alias, t, if_expr.true_case(), assigns);
     get_assigns_lhs(local_may_alias, t, if_expr.false_case(), assigns);
@@ -74,20 +92,29 @@ void get_assigns(
   const loopt &loop,
   assignst &assigns)
 {
-  for(loopt::const_iterator
-      i_it=loop.begin(); i_it!=loop.end(); i_it++)
+  get_assigns(
+    local_may_alias, loop, assigns, [](const exprt &e) { return true; });
+}
+
+void get_assigns(
+  const local_may_aliast &local_may_alias,
+  const loopt &loop,
+  assignst &assigns,
+  std::function<bool(const exprt &)> predicate)
+{
+  for(loopt::const_iterator i_it = loop.begin(); i_it != loop.end(); i_it++)
   {
-    const goto_programt::instructiont &instruction=**i_it;
+    const goto_programt::instructiont &instruction = **i_it;
 
     if(instruction.is_assign())
     {
       const exprt &lhs = instruction.assign_lhs();
-      get_assigns_lhs(local_may_alias, *i_it, lhs, assigns);
+      get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate);
     }
     else if(instruction.is_function_call())
     {
       const exprt &lhs = instruction.call_lhs();
-      get_assigns_lhs(local_may_alias, *i_it, lhs, assigns);
+      get_assigns_lhs(local_may_alias, *i_it, lhs, assigns, predicate);
     }
   }
 }

src/goto-instrument/loop_utils.h

@@ -24,12 +24,27 @@ void get_assigns(
   const loopt &loop,
   assignst &assigns);
 
+/// get all assign targets that satisfy `predicate` within the loops.
+void get_assigns(
+  const local_may_aliast &local_may_alias,
+  const loopt &loop,
+  assignst &assigns,
+  std::function<bool(const exprt &)> predicate);
+
 void get_assigns_lhs(
   const local_may_aliast &local_may_alias,
   goto_programt::const_targett t,
   const exprt &lhs,
   assignst &assigns);
 
+/// get all assign targets that satisfy `predicate` from `lhs`.
+void get_assigns_lhs(
+  const local_may_aliast &local_may_alias,
+  goto_programt::const_targett t,
+  const exprt &lhs,
+  assignst &assigns,
+  std::function<bool(const exprt &)> predicate);
+
 goto_programt::targett get_loop_exit(const loopt &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H