CONTRACTS: detect and handle locals in assigns clause checking for loops

regression/contracts/detect_loop_locals/main.c

@@ -0,0 +1,12 @@
+#include <stdlib.h>
+
+int main()
+{
+  unsigned char *i = malloc(5);
+
+  while(i != i + 5)
+    __CPROVER_loop_invariant(1 == 1)
+    {
+      const char lower = *i++;
+    }
+}

regression/contracts/detect_loop_locals/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--apply-loop-contracts
+^\[main.assigns.\d+\].*line 10 Check that i is assignable: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks that loop local variables do not cause explicit checks 

regression/contracts/detect_loop_locals2/main.c

@@ -0,0 +1,28 @@
+static void foo()
+{
+  unsigned i;
+
+  for(i = 0; i < 16; i++)
+    __CPROVER_loop_invariant(1 == 1)
+    {
+      int v = 1;
+    }
+}
+
+static void bar()
+{
+  unsigned i;
+
+  for(i = 0; i < 16; i++)
+    __CPROVER_loop_invariant(1 == 1)
+    {
+      int v = 1;
+    }
+}
+
+int main()
+{
+  bar();
+  foo();
+  foo();
+}

regression/contracts/detect_loop_locals2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-loop-contracts
+^\[bar.assigns.\d+\].*Check that i is assignable: SUCCESS$
+^\[foo.assigns.\d+\].*Check that i is assignable: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks that loop local variables do not cause explicit checks 

regression/contracts/invar_check_nested_loops/test.desc

@@ -9,9 +9,10 @@ main.c
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assigns.\d+] .* line 23 Check that s is assignable: SUCCESS$
-^\[main.assigns.\d+] .* line 24 Check that a is assignable: SUCCESS$
-^\[main.assigns.\d+] .* line 27 Check that s is assignable: SUCCESS$
+^\[main\.assigns\.\d+\].*line 17 Check that s is assignable: SUCCESS$
+^\[main\.assigns\.\d+\].*line 23 Check that s is assignable: SUCCESS$
+^\[main\.assigns\.\d+\].*line 24 Check that a is assignable: SUCCESS$
+^\[main\.assigns\.\d+\].*line 27 Check that s is assignable: SUCCESS$
 ^\[main\.assertion.\d+\] .* assertion s == n: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/loop_guard_with_side_effects/test.desc

@@ -4,7 +4,6 @@ main.c
 \[check.assigns\.\d+\] line \d+ Check that \*j is assignable: SUCCESS$
 \[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS
 \[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS
-\[check.assigns\.\d+\] line \d+ Check that return_value_check is assignable: SUCCESS$
 \[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
 \[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
 \[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$
@@ -16,6 +15,7 @@ main.c
 \[main.assertion\.\d+\] line \d+ assertion j == k \+ 1: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
 --
 --
 This test demonstrates a case where the loop guard has side effects.

regression/contracts/loop_guard_with_side_effects_fail/test.desc

@@ -2,7 +2,6 @@ CORE
 main.c
 --apply-loop-contracts _ --unsigned-overflow-check
 \[check.assigns\.\d+\] line \d+ Check that \*j is assignable: FAILURE$
-\[check.assigns\.\d+\] line \d+ Check that return_value_check is assignable: SUCCESS$
 \[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
 \[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
 \[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$

src/goto-instrument/contracts/cfg_info.h

@@ -0,0 +1,197 @@
+/*******************************************************************\
+
+Module: CFG-based information for assigns clause checking simplification
+
+Author: Remi Delmas
+
+Date: June 2022
+
+\*******************************************************************/
+
+/// \file
+/// Classes providing CFG-based information about symbols to guide
+/// simplifications in function and loop assigns clause checking
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CFG_INFO_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CFG_INFO_H
+
+#include <goto-programs/goto_convert_class.h>
+
+#include <util/byte_operators.h>
+#include <util/expr_cast.h>
+#include <util/message.h>
+
+#include <goto-programs/goto_model.h>
+
+#include <analyses/dirty.h>
+#include <analyses/locals.h>
+#include <goto-instrument/havoc_utils.h>
+#include <goto-instrument/loop_utils.h>
+
+#include <set>
+#include <vector>
+
+/// Stores information about a goto function computed from its CFG.
+///
+/// The methods of this class provide information about identifiers
+/// to allow simplifying assigns clause checking assertions.
+class cfg_infot
+{
+public:
+  /// Returns true iff `ident` is locally declared.
+  virtual bool is_local(const irep_idt &ident) const = 0;
+
+  /// Returns true iff the given `ident` is either non-locally declared
+  /// or is locally-declared but dirty.
+  virtual bool is_not_local_or_dirty_local(const irep_idt &ident) const = 0;
+
+  /// Returns true iff `expr` is an access to a locally declared symbol
+  /// and does not contain `dereference` or `address_of` operations.
+  bool is_local_composite_access(const exprt &expr) const
+  {
+    // case-splitting on the lhs structure copied from symex_assignt::assign_rec
+    if(expr.id() == ID_symbol)
+    {
+      return is_local(to_symbol_expr(expr).get_identifier());
+    }
+    else if(expr.id() == ID_index)
+    {
+      return is_local_composite_access(to_index_expr(expr).array());
+    }
+    else if(expr.id() == ID_member)
+    {
+      const typet &type = to_member_expr(expr).struct_op().type();
+      if(
+        type.id() == ID_struct || type.id() == ID_struct_tag ||
+        type.id() == ID_union || type.id() == ID_union_tag)
+      {
+        return is_local_composite_access(to_member_expr(expr).compound());
+      }
+      else
+      {
+        throw unsupported_operation_exceptiont(
+          "is_local_composite_access: unexpected assignment to member of '" +
+          type.id_string() + "'");
+      }
+    }
+    else if(expr.id() == ID_if)
+    {
+      return is_local_composite_access(to_if_expr(expr).true_case()) &&
+             is_local_composite_access(to_if_expr(expr).false_case());
+    }
+    else if(expr.id() == ID_typecast)
+    {
+      return is_local_composite_access(to_typecast_expr(expr).op());
+    }
+    else if(
+      expr.id() == ID_byte_extract_little_endian ||
+      expr.id() == ID_byte_extract_big_endian)
+    {
+      return is_local_composite_access(to_byte_extract_expr(expr).op());
+    }
+    else if(expr.id() == ID_complex_real)
+    {
+      return is_local_composite_access(to_complex_real_expr(expr).op());
+    }
+    else if(expr.id() == ID_complex_imag)
+    {
+      return is_local_composite_access(to_complex_imag_expr(expr).op());
+    }
+    else
+    {
+      // matches ID_address_of, ID_dereference, etc.
+      return false;
+    }
+  }
+};
+
+// For goto_functions
+class function_cfg_infot : public cfg_infot
+{
+public:
+  explicit function_cfg_infot(const goto_functiont &_goto_function)
+    : dirty_analysis(_goto_function), locals(_goto_function)
+  {
+    parameters.insert(
+      _goto_function.parameter_identifiers.begin(),
+      _goto_function.parameter_identifiers.end());
+  }
+
+  /// Returns true iff `ident` is a local or parameter of the goto_function.
+  bool is_local(const irep_idt &ident) const override
+  {
+    return locals.is_local(ident) ||
+           (parameters.find(ident) != parameters.end());
+  }
+
+  /// Returns true iff the given `ident` is either not a goto_function local
+  /// or is a local that is dirty.
+  bool is_not_local_or_dirty_local(const irep_idt &ident) const override
+  {
+    if(is_local(ident))
+      return dirty_analysis.get_dirty_ids().find(ident) !=
+             dirty_analysis.get_dirty_ids().end();
+    else
+      return true;
+  }
+
+private:
+  const dirtyt dirty_analysis;
+  const localst locals;
+  std::unordered_set<irep_idt> parameters;
+};
+
+// For a loop in a goto_function
+class loop_cfg_infot : public cfg_infot
+{
+public:
+  loop_cfg_infot(goto_functiont &_goto_function, const loopt &loop)
+    : dirty_analysis(_goto_function)
+  {
+    for(const auto &t : loop)
+    {
+      if(t->is_decl())
+        locals.insert(t->decl_symbol().get_identifier());
+    }
+  }
+
+  /// Returns true iff `ident` is a loop local.
+  bool is_local(const irep_idt &ident) const override
+  {
+    return locals.find(ident) != locals.end();
+  }
+
+  /// Returns true iff the given `ident` is either not a loop local
+  /// or is a loop local that is dirty.
+  bool is_not_local_or_dirty_local(const irep_idt &ident) const override
+  {
+    if(is_local(ident))
+      return dirty_analysis.get_dirty_ids().find(ident) !=
+             dirty_analysis.get_dirty_ids().end();
+    else
+      return true;
+  }
+
+  void erase_locals(std::set<exprt> &exprs)
+  {
+    auto it = exprs.begin();
+    while(it != exprs.end())
+    {
+      if(
+        it->id() == ID_symbol && is_local(to_symbol_expr(*it).get_identifier()))
+      {
+        it = exprs.erase(it);
+      }
+      else
+      {
+        it++;
+      }
+    }
+  }
+
+private:
+  const dirtyt dirty_analysis;
+  std::unordered_set<irep_idt> locals;
+};
+
+#endif