CONTRACTS: loop assigns clause inference function

src/goto-instrument/Makefile

@@ -23,6 +23,8 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_loop_contract_mode.cpp \
       contracts/dynamic-frames/dfcc_loop_tags.cpp \
       contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp \
+      contracts/dynamic-frames/dfcc_root_object.cpp \
+      contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
       contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \

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

@@ -0,0 +1,106 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Remi Delmas, [email protected]
+
+\*******************************************************************/
+#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>
+
+#include "dfcc_root_object.h"
+
+/// Builds a call expression `object_whole(expr)`
+static exprt
+make_object_whole_call_expr(const exprt &expr, const namespacet &ns)
+{
+  const symbolt &object_whole_sym = ns.lookup(CPROVER_PREFIX "object_whole");
+  const code_typet &object_whole_code_type =
+    to_code_type(object_whole_sym.type);
+  return side_effect_expr_function_callt(
+    object_whole_sym.symbol_expr(),
+    {{expr}},
+    object_whole_code_type.return_type(),
+    expr.source_location());
+}
+
+/// Returns true iff \p expr contains at least one identifier found in
+/// \p identifiers.
+static bool
+depends_on(const exprt &expr, std::unordered_set<irep_idt> identifiers)
+{
+  const std::unordered_set<irep_idt> ids = find_symbol_identifiers(expr);
+  for(const auto &id : ids)
+  {
+    if(identifiers.find(id) != identifiers.end())
+      return true;
+  }
+  return false;
+}
+
+assignst dfcc_infer_loop_assigns(
+  const local_may_aliast &local_may_alias,
+  const loopt &loop_instructions,
+  const source_locationt &loop_head_location,
+  const namespacet &ns)
+{
+  // infer
+  assignst assigns;
+  get_assigns(local_may_alias, loop_instructions, assigns);
+
+  // compute locals
+  std::unordered_set<irep_idt> loop_locals;
+  for(const auto &target : loop_instructions)
+  {
+    if(target->is_decl())
+      loop_locals.insert(target->decl_symbol().get_identifier());
+  }
+
+  // widen or drop targets that depend on loop-locals or are non-constant,
+  // ie. depend on other locations assigned by the loop.
+  // e.g: if the loop assigns {i, a[i]}, then a[i] is non-constant.
+  havoc_utils_is_constantt is_constant(assigns, ns);
+  assignst result;
+  for(const auto &expr : assigns)
+  {
+    if(depends_on(expr, loop_locals))
+    {
+      // Target depends on loop locals, attempt widening to the root object
+      auto root_objects = dfcc_root_objects(expr);
+      for(const auto &root_object : root_objects)
+      {
+        if(!depends_on(root_object, loop_locals))
+        {
+          address_of_exprt address_of_root_object(root_object);
+          address_of_root_object.add_source_location() =
+            root_object.source_location();
+          result.emplace(
+            make_object_whole_call_expr(address_of_root_object, ns));
+        }
+      }
+    }
+    else
+    {
+      address_of_exprt address_of_expr(expr);
+      address_of_expr.add_source_location() = expr.source_location();
+      if(!is_constant(address_of_expr))
+      {
+        // Target address is not constant, widening to the whole object
+        result.emplace(make_object_whole_call_expr(address_of_expr, ns));
+      }
+      else
+      {
+        result.emplace(expr);
+      }
+    }
+  }
+
+  return result;
+}

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

@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Remi Delmas, [email protected]
+
+\*******************************************************************/
+
+/// \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.
+assignst dfcc_infer_loop_assigns(
+  const local_may_aliast &local_may_alias,
+  const loopt &loop_instructions,
+  const source_locationt &loop_head_location,
+  const namespacet &ns);
+
+#endif

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

@@ -0,0 +1,138 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Remi Delmas, [email protected]
+
+Date: March 2023
+
+\*******************************************************************/
+
+#include "dfcc_root_object.h"
+
+#include <util/byte_operators.h>
+#include <util/cprover_prefix.h>
+#include <util/expr.h>
+#include <util/expr_util.h>
+#include <util/pointer_expr.h>
+#include <util/std_code.h>
+
+#include <goto-programs/pointer_arithmetic.h>
+
+/// Recursively computes a set of root object expressions for \p expr.
+static void
+root_objects_rec(const exprt &expr, std::unordered_set<exprt, irep_hash> &dest)
+{
+  if(expr.id() == ID_symbol)
+  {
+    dest.insert(expr);
+  }
+  else if(expr.id() == ID_index)
+  {
+    root_objects_rec(to_index_expr(expr).array(), dest);
+  }
+  else if(expr.id() == ID_member)
+  {
+    const typet &type = to_member_expr(expr).struct_op().type();
+    DATA_INVARIANT(
+      type.id() == ID_struct || type.id() == ID_struct_tag ||
+        type.id() == ID_union || type.id() == ID_union_tag,
+      "unexpected assignment to member of '" + type.id_string() + "'");
+    root_objects_rec(to_member_expr(expr).compound(), dest);
+  }
+  else if(expr.id() == ID_if)
+  {
+    root_objects_rec(to_if_expr(expr).true_case(), dest);
+    root_objects_rec(to_if_expr(expr).false_case(), dest);
+  }
+  else if(expr.id() == ID_typecast)
+  {
+    root_objects_rec(to_typecast_expr(expr).op(), dest);
+  }
+  else if(
+    expr.id() == ID_byte_extract_little_endian ||
+    expr.id() == ID_byte_extract_big_endian)
+  {
+    root_objects_rec(to_byte_extract_expr(expr).op(), dest);
+  }
+  else if(expr.id() == ID_complex_real)
+  {
+    root_objects_rec(to_complex_real_expr(expr).op(), dest);
+  }
+  else if(expr.id() == ID_complex_imag)
+  {
+    root_objects_rec(to_complex_imag_expr(expr).op(), dest);
+  }
+  else if(const auto &deref = expr_try_dynamic_cast<dereference_exprt>(expr))
+  {
+    // normalise the dereferenced pointer into `pointer + offset`, extract
+    // pointer expression and try some simplifications
+    const exprt &pointer = pointer_arithmetict(deref->pointer()).pointer;
+    const source_locationt source_location = expr.source_location();
+    if(const auto &if_expr = expr_try_dynamic_cast<if_exprt>(pointer))
+    {
+      // split on disjunctions
+      // *(c ? true_case : false_case) => rec(*true_case); rec(*false_case)
+      dereference_exprt if_true(if_expr->true_case());
+      if_true.add_source_location() = source_location;
+      root_objects_rec(if_true, dest);
+      dereference_exprt if_false(if_expr->false_case());
+      if_false.add_source_location() = source_location;
+      root_objects_rec(if_false, dest);
+    }
+    else if(
+      const auto &address_of_expr =
+        expr_try_dynamic_cast<address_of_exprt>(pointer))
+    {
+      // *(&object + offset) => rec(object)
+      root_objects_rec(skip_typecast(address_of_expr->object()), dest);
+    }
+    else
+    {
+      // simplify *(pointer + offset) to *pointer and stop here
+      dereference_exprt deref(pointer);
+      deref.add_source_location() = source_location;
+      dest.insert(deref);
+    }
+  }
+  else
+  {
+    // Stop here for anything else.
+    dest.insert(expr);
+  }
+}
+
+/// Translates object slice expressions found in assigns clause targets to
+/// dereference expressions so that root objects can be computed.
+static exprt slice_op_to_deref(const exprt &expr)
+{
+  if(
+    const auto &function_call_expr =
+      expr_try_dynamic_cast<side_effect_expr_function_callt>(expr))
+  {
+    auto function_expr = function_call_expr->function();
+    INVARIANT(
+      function_expr.id() == ID_symbol,
+      "no function pointer calls in loop assigns clause targets");
+    auto function_id = to_symbol_expr(function_expr).get_identifier();
+    INVARIANT(
+      function_id == CPROVER_PREFIX "assignable" ||
+        function_id == CPROVER_PREFIX "object_whole" ||
+        function_id == CPROVER_PREFIX "object_from" ||
+        function_id == CPROVER_PREFIX "object_upto",
+      "can only handle built-in function calls in assigns clause targets");
+    return dereference_exprt(
+      skip_typecast(function_call_expr->arguments().at(0)));
+  }
+  else
+  {
+    return expr;
+  }
+}
+
+std::unordered_set<exprt, irep_hash> dfcc_root_objects(const exprt &expr)
+{
+  std::unordered_set<exprt, irep_hash> result;
+  root_objects_rec(slice_op_to_deref(expr), result);
+  return result;
+}

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

@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module: Dynamic frame condition checking
+
+Author: Remi Delmas, [email protected]
+
+Date: March 2023
+
+\*******************************************************************/
+
+/// \file
+/// Utility functions that compute root object expressions for assigns clause
+/// targets and LHS expressions.
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_ROOT_OBJECT_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_ROOT_OBJECT_H
+
+#include <util/irep.h>
+
+#include <unordered_set>
+
+class exprt;
+
+/// Computes a set of root object expressions from an lvalue or assigns clause
+/// target expression. A root object expression is a simpler expression that
+/// denotes the object that contains the memory location refered to by the
+/// initial expression.
+std::unordered_set<exprt, irep_hash> dfcc_root_objects(const exprt &expr);
+#endif