CONTRACTS: Move code to utils

- Move havoc_assigns_clauset from contract/assigns
  to utils
- Moving functions for tracking assigns clause replacement
  to utils to break circular dependency
- Unified interface for adding "disable:check" pragmas on
  locations, instructions and programs

Author: Remi Delmas

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

@@ -13,10 +13,6 @@ Author: Remi Delmas, [email protected]
 
 #include <map>
 
-#include <langapi/language_util.h>
-
-#include <ansi-c/c_expr.h>
-
 #include <util/c_types.h>
 #include <util/format_expr.h>
 #include <util/format_type.h>
@@ -26,27 +22,12 @@ Author: Remi Delmas, [email protected]
 #include <util/pointer_predicates.h>
 #include <util/std_code.h>
 
+#include <ansi-c/c_expr.h>
+#include <langapi/language_util.h>
+
 #include "instrument_spec_assigns.h"
 #include "utils.h"
 
-static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[] =
-  " (assigned by the contract of ";
-
-static irep_idt make_tracking_comment(
-  const exprt &target,
-  const irep_idt &function_id,
-  const namespacet &ns)
-{
-  return from_expr(ns, target.id(), target) +
-         ASSIGNS_CLAUSE_REPLACEMENT_TRACKING + id2string(function_id) + ")";
-}
-
-bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
-{
-  return id2string(comment).find(ASSIGNS_CLAUSE_REPLACEMENT_TRACKING) !=
-         std::string::npos;
-}
-
 void havoc_assigns_clause_targetst::get_instructions(goto_programt &dest)
 {
   // snapshotting instructions and well-definedness checks
@@ -80,7 +61,8 @@ void havoc_assigns_clause_targetst::havoc_if_valid(
   goto_programt &dest)
 {
   const irep_idt &tracking_comment =
-    make_tracking_comment(car.target(), function_id, ns);
+    make_assigns_clause_replacement_tracking_comment(
+      car.target(), function_id, ns);
 
   source_locationt source_location_no_checks(source_location);
   add_pragma_disable_pointer_checks(source_location_no_checks);

src/goto-instrument/contracts/havoc_assigns_clause_targets.h

@@ -21,8 +21,6 @@ class goto_programt;
 class goto_functionst;
 class message_handlert;
 
-bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment);
-
 /// Class to generate havocking instructions for target expressions of a
 /// function contract's assign clause (replacement).
 ///
@@ -73,8 +71,11 @@ class havoc_assigns_clause_targetst : public instrument_spec_assignst
   void get_instructions(goto_programt &dest);
 
 private:
-  /// \brief Generates instructions to conditionally havoc
-  /// the given `car_exprt`.
+  /// \brief Generates instructions to conditionally havoc the given conditional
+  /// address range expression `car`, adding results to `dest`.
+  ///
+  /// Adds a special comment on the havoc instructions in order to trace back
+  /// the origin of the havoc expressions to the function being replaced.
   ///
   /// Generates these instructions for a `__CPROVER_POINTER_OBJECT(...)` target:
   ///
@@ -91,14 +92,13 @@ class havoc_assigns_clause_targetst : public instrument_spec_assignst
   ///
   /// ```
   /// IF !__car_writable GOTO skip_target
-  /// ASSIGN * ((<target.type()> *)_car_lb) = nondet_<target.type()>;
+  /// ASSIGN *((target_type *) _car_lb) = nondet(target_type);
   /// skip_target: SKIP
   /// DEAD __car_writable
   /// DEAD __car_lb
   /// DEAD __car_ub
   /// ```
-  /// Adds a special comment on the havoc instructions in order to trace back
-  /// the havoc to the replaced function.
+  /// Where `target_type` is the type of the target expression.
   void havoc_if_valid(car_exprt car, goto_programt &dest);
 
   const std::vector<exprt> &targets;

src/goto-instrument/contracts/utils.cpp

@@ -11,27 +11,15 @@ Date: September 2021
 #include "utils.h"
 
 #include <goto-programs/cfg.h>
+
 #include <util/fresh_symbol.h>
 #include <util/graph.h>
 #include <util/message.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_predicates.h>
 #include <util/simplify_expr.h>
 
-goto_programt::instructiont &
-add_pragma_disable_assigns_check(goto_programt::instructiont &instr)
-{
-  instr.source_location_nonconst().add_pragma(
-    CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK);
-  return instr;
-}
-
-goto_programt &add_pragma_disable_assigns_check(goto_programt &prog)
-{
-  Forall_goto_program_instructions(it, prog)
-    add_pragma_disable_assigns_check(*it);
-  return prog;
-}
+#include <langapi/language_util.h>
 
 static void append_safe_havoc_code_for_expr(
   const source_locationt location,
@@ -74,6 +62,63 @@ void havoc_if_validt::append_scalar_havoc_code_for_expr(
   });
 }
 
+void havoc_assigns_targetst::append_havoc_code_for_expr(
+  const source_locationt location,
+  const exprt &expr,
+  goto_programt &dest) const
+{
+  if(expr.id() == ID_pointer_object)
+  {
+    append_object_havoc_code_for_expr(location, expr.operands().front(), dest);
+    return;
+  }
+
+  havoc_utilst::append_havoc_code_for_expr(location, expr, dest);
+}
+
+void add_pragma_disable_pointer_checks(source_locationt &location)
+{
+  location.add_pragma("disable:pointer-check");
+  location.add_pragma("disable:pointer-primitive-check");
+  location.add_pragma("disable:pointer-overflow-check");
+  location.add_pragma("disable:signed-overflow-check");
+  location.add_pragma("disable:unsigned-overflow-check");
+  location.add_pragma("disable:conversion-check");
+}
+
+goto_programt::instructiont &
+add_pragma_disable_pointer_checks(goto_programt::instructiont &instr)
+{
+  add_pragma_disable_pointer_checks(instr.source_location_nonconst());
+  return instr;
+}
+
+goto_programt &add_pragma_disable_pointer_checks(goto_programt &prog)
+{
+  Forall_goto_program_instructions(it, prog)
+    add_pragma_disable_pointer_checks(*it);
+  return prog;
+}
+
+void add_pragma_disable_assigns_check(source_locationt &location)
+{
+  location.add_pragma(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK);
+}
+
+goto_programt::instructiont &
+add_pragma_disable_assigns_check(goto_programt::instructiont &instr)
+{
+  add_pragma_disable_assigns_check(instr.source_location_nonconst());
+  return instr;
+}
+
+goto_programt &add_pragma_disable_assigns_check(goto_programt &prog)
+{
+  Forall_goto_program_instructions(it, prog)
+    add_pragma_disable_assigns_check(*it);
+  return prog;
+}
+
 exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
 {
   exprt::operandst validity_checks;
@@ -156,16 +201,6 @@ const symbolt &new_tmp_symbol(
   return new_symbol;
 }
 
-void disable_pointer_checks(source_locationt &source_location)
-{
-  source_location.add_pragma("disable:pointer-check");
-  source_location.add_pragma("disable:pointer-primitive-check");
-  source_location.add_pragma("disable:pointer-overflow-check");
-  source_location.add_pragma("disable:signed-overflow-check");
-  source_location.add_pragma("disable:unsigned-overflow-check");
-  source_location.add_pragma("disable:conversion-check");
-}
-
 void simplify_gotos(goto_programt &goto_program, namespacet &ns)
 {
   for(auto &instruction : goto_program.instructions)
@@ -226,3 +261,22 @@ bool is_loop_free(
   }
   return true;
 }
+
+/// Prefix for comments added to track assigns clause replacement.
+static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[] =
+  " (assigned by the contract of ";
+
+irep_idt make_assigns_clause_replacement_tracking_comment(
+  const exprt &target,
+  const irep_idt &function_id,
+  const namespacet &ns)
+{
+  return from_expr(ns, target.id(), target) +
+         ASSIGNS_CLAUSE_REPLACEMENT_TRACKING + id2string(function_id) + ")";
+}
+
+bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
+{
+  return id2string(comment).find(ASSIGNS_CLAUSE_REPLACEMENT_TRACKING) !=
+         std::string::npos;
+}

src/goto-instrument/contracts/utils.h

@@ -51,6 +51,46 @@ class havoc_if_validt : public havoc_utilst
   const namespacet &ns;
 };
 
+/// \brief A class that further overrides the "safe" havoc utilities,
+///        and adds support for havocing pointer_object expressions.
+class havoc_assigns_targetst : public havoc_if_validt
+{
+public:
+  havoc_assigns_targetst(const assignst &mod, const namespacet &ns)
+    : havoc_if_validt(mod, ns)
+  {
+  }
+
+  void append_havoc_code_for_expr(
+    const source_locationt location,
+    const exprt &expr,
+    goto_programt &dest) const override;
+};
+
+/// \brief Adds a pragma on a source location disable all pointer checks.
+///
+/// The disabled checks are: "pointer-check", "pointer-primitive-check",
+/// "pointer-overflow-check", "signed-overflow-check",
+//  "unsigned-overflow-check", "conversion-check".
+void add_pragma_disable_pointer_checks(source_locationt &source_location);
+
+/// \brief Adds pragmas on a GOTO instruction to disable all pointer checks.
+///
+/// \param instr: A mutable reference to the GOTO instruction.
+/// \return The same reference after mutation (i.e., adding the pragma).
+goto_programt::instructiont &
+add_pragma_disable_pointer_checks(goto_programt::instructiont &instr);
+
+/// \brief Adds pragmas on all instructions in a GOTO program
+/// to disable all pointer checks.
+///
+/// \param prog: A mutable reference to the GOTO program.
+/// \return The same reference after mutation (i.e., adding the pragmas).
+goto_programt &add_pragma_disable_pointer_checks(goto_programt &prog);
+
+/// \brief Adds a pragma on a source_locationt to disable inclusion checking.
+void add_pragma_disable_assigns_check(source_locationt &source_location);
+
 /// \brief Adds a pragma on a GOTO instruction to disable inclusion checking.
 ///
 /// \param instr: A mutable reference to the GOTO instruction.
@@ -129,9 +169,6 @@ const symbolt &new_tmp_symbol(
   std::string suffix = "tmp_cc",
   bool is_auxiliary = true);
 
-/// Add disable pragmas for all pointer checks on the given location
-void disable_pointer_checks(source_locationt &source_location);
-
 /// Turns goto instructions `IF cond GOTO label` where the condition
 /// statically simplifies to `false` into SKIP instructions.
 void simplify_gotos(goto_programt &goto_program, namespacet &ns);
@@ -224,4 +261,15 @@ class cleanert : public goto_convertt
   }
 };
 
+/// Returns an \ref irep_idt that essentially says that
+/// `target` was assigned by the contract of `function_id`.
+irep_idt make_assigns_clause_replacement_tracking_comment(
+  const exprt &target,
+  const irep_idt &function_id,
+  const namespacet &ns);
+
+/// Returns true if the given comment matches the type of comments created by
+/// \ref make_assigns_clause_replacement_tracking_comment.
+bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment);
+
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H