CONTRACTS: loop assigns clause inference function

Utility function for loop contracts instrumentation.

Author: Remi Delmas

src/goto-instrument/Makefile

@@ -18,6 +18,7 @@ SRC = accelerate/accelerate.cpp \
       call_sequences.cpp \
       contracts/contracts.cpp \
       contracts/dynamic-frames/dfcc_utils.cpp \
+      contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \
       contracts/dynamic-frames/dfcc_pointer_in_range.cpp \

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

@@ -0,0 +1,119 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Qinheping Hu, [email protected]
+
+Author: Remi Delmas, [email protected]
+
+Date: March 2023
+
+\*******************************************************************/
+#include "dfcc_infer_loop_assigns.h"
+
+#include <util/expr.h>
+#include <util/find_symbols.h>
+#include <util/message.h>
+#include <util/pointer_expr.h>
+#include <util/std_code.h>
+
+#include <goto-instrument/havoc_utils.h>
+
+/// Widens expressions in the given \p assigns set as follows:
+/// If an expression is an array index expression or an 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.
+/// By `constant` for the index expression, we do not mean a literal constant
+/// expression. Rather, we mean a symbol or an expression the value of which is
+/// known not to change over loop iterations, i.e. an expression that is not
+/// itself part of \p assigns.
+static void dfcc_widen_non_const(const namespacet &ns, assignst &assigns)
+{
+  assignst result;
+  const symbolt &object_whole_sym = ns.lookup(CPROVER_PREFIX "object_whole");
+  code_typet object_whole_code_type = to_code_type(object_whole_sym.type);
+  havoc_utils_is_constantt is_constant(assigns, ns);
+
+  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))
+      {
+        exprt::operandst args;
+        args.emplace_back(address_of_expr);
+        result.emplace(side_effect_expr_function_callt(
+          object_whole_sym.symbol_expr(),
+          args,
+          object_whole_code_type.return_type(),
+          address_of_expr.source_location()));
+      }
+      else
+        result.emplace(e);
+    }
+    else
+      result.emplace(e);
+  }
+  assigns.swap(result);
+}
+
+std::set<exprt> dfcc_infer_loop_assigns(
+  const local_may_aliast &local_may_alias,
+  const loopt &loop_instructions,
+  const source_locationt &loop_head_location,
+  messaget &log,
+  namespacet &ns)
+{
+  try
+  {
+    // infer
+    assignst assigns;
+    get_assigns(local_may_alias, loop_instructions, assigns);
+
+    // compute locals
+    std::set<irep_idt> loop_locals;
+    for(const auto &target : loop_instructions)
+    {
+      if(target->is_decl())
+      {
+        loop_locals.insert(target->decl_symbol().get_identifier());
+      }
+    }
+
+    // remove all targets that depend on loop-local identifiers
+    auto expr_it = assigns.begin();
+    while(expr_it != assigns.end())
+    {
+      const std::unordered_set<irep_idt> symbols =
+        find_symbol_identifiers(*expr_it);
+
+      if(std::find_if(symbols.begin(), symbols.end(), [&](const irep_idt &id) {
+           return loop_locals.find(id) != loop_locals.end();
+         }) != symbols.end())
+      {
+        expr_it = assigns.erase(expr_it);
+      }
+      else
+      {
+        expr_it++;
+      }
+    }
+
+    // widen all targets that depend on non-constant expressions
+    dfcc_widen_non_const(ns, assigns);
+    return assigns;
+  }
+  catch(const analysis_exceptiont &exc)
+  {
+    log.error() << "Failed to infer memory locations assigned by the loop at "
+                << loop_head_location
+                << ".\nPlease specify an assigns clause.\nReason:"
+                << messaget::eom;
+    throw exc;
+  }
+}

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

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Qinheping Hu, [email protected]
+
+Author: Remi Delmas, [email protected]
+
+Date: March 2023
+
+\*******************************************************************/
+
+/// \file
+/// Infer a set of assigns clause targets for a natural loop.
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INFER_LOOP_ASSIGNS_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INFER_LOOP_ASSIGNS_H
+
+#include <analyses/local_may_alias.h>
+#include <goto-instrument/loop_utils.h>
+class source_locationt;
+class messaget;
+class namespacet;
+
+// \brief Infer assigns clause targets for a loop from its instructions and a
+// may alias analysis at the function level.
+std::set<exprt> dfcc_infer_loop_assigns(
+  const local_may_aliast &local_may_alias,
+  const loopt &loop_instructions,
+  const source_locationt &loop_head_location,
+  messaget &log,
+  namespacet &ns);
+
+#endif

src/goto-instrument/contracts/dynamic-frames/module_dependencies.txt

@@ -1,3 +1,4 @@
+analyses
 ansi-c
 goto-instrument/contracts
 goto-instrument/contracts/dynamic-frames