Refactor code contracts utility functions

In this change, we move two of the "static" functions within
contracts.cpp to utils.cpp (a new file in contracts module).

We also fix the #include dependence -- assigns should not #include
contracts.h, it should be the other way round.

Author: SaswatPadhi

src/goto-instrument/contracts/assigns.cpp

@@ -15,8 +15,11 @@ Date: July 2021
 
 #include <goto-instrument/havoc_utils.h>
 
+#include <langapi/language_util.h>
+
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 
 assigns_clauset::targett::targett(

src/goto-instrument/contracts/assigns.h

@@ -14,9 +14,12 @@ Date: July 2021
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
 
-#include "contracts.h"
+#include <unordered_set>
 
-#include <util/pointer_offset_size.h>
+#include <goto-programs/goto_model.h>
+
+#include <util/message.h>
+#include <util/pointer_expr.h>
 
 /// \brief A class for representing assigns clauses in code contracts
 class assigns_clauset

src/goto-instrument/contracts/contracts.cpp

@@ -24,6 +24,8 @@ Date: February 2016
 
 #include <goto-programs/remove_skip.h>
 
+#include <langapi/language_util.h>
+
 #include <util/c_types.h>
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
@@ -35,62 +37,7 @@ Date: February 2016
 
 #include "assigns.h"
 #include "memory_predicates.h"
-
-// Create a lexicographic less-than relation between two tuples of variables.
-// This is used in the implementation of multidimensional decreases clauses.
-static exprt create_lexicographic_less_than(
-  const std::vector<symbol_exprt> &lhs,
-  const std::vector<symbol_exprt> &rhs)
-{
-  PRECONDITION(lhs.size() == rhs.size());
-
-  if(lhs.empty())
-  {
-    return false_exprt();
-  }
-
-  // Store conjunctions of equalities.
-  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
-  // l2, l3>.
-  // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
-  // s1 == l1 && s2 == l2 && s3 == l3>.
-  // In fact, the last element is unnecessary, so we do not create it.
-  exprt::operandst equality_conjunctions(lhs.size());
-  equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
-  for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
-  {
-    binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
-    equality_conjunctions[i] =
-      and_exprt(equality_conjunctions[i - 1], component_i_equality);
-  }
-
-  // Store inequalities between the i-th components of the input vectors
-  // (i.e. lhs and rhs).
-  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
-  // l2, l3>.
-  // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
-  // s2 == l2 && s3 < l3>.
-  exprt::operandst lexicographic_individual_comparisons(lhs.size());
-  lexicographic_individual_comparisons[0] =
-    binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
-  for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
-  {
-    binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
-    lexicographic_individual_comparisons[i] =
-      and_exprt(equality_conjunctions[i - 1], component_i_less_than);
-  }
-  return disjunction(lexicographic_individual_comparisons);
-}
-
-static void insert_before_swap_and_advance(
-  goto_programt &program,
-  goto_programt::targett &target,
-  goto_programt &payload)
-{
-  const auto offset = payload.instructions.size();
-  program.insert_before_swap(target, payload);
-  std::advance(target, offset);
-}
+#include "utils.h"
 
 void code_contractst::check_apply_loop_contracts(
   goto_functionst::goto_functiont &goto_function,
@@ -289,7 +236,8 @@ void code_contractst::check_apply_loop_contracts(
     // after the loop is smaller than the value before the loop.
     // Here, we use the lexicographic order.
     code_assertt monotonic_decreasing_assertion{
-      create_lexicographic_less_than(new_decreases_vars, old_decreases_vars)};
+      generate_lexicographic_less_than_check(
+        new_decreases_vars, old_decreases_vars)};
     monotonic_decreasing_assertion.add_source_location() =
       loop_head->source_location;
     converter.goto_convert(monotonic_decreasing_assertion, havoc_code, mode);

src/goto-instrument/contracts/contracts.h

@@ -25,8 +25,6 @@ Date: February 2016
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
-#include <langapi/language_util.h>
-
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>

src/goto-instrument/contracts/utils.cpp

@@ -0,0 +1,65 @@
+/*******************************************************************\
+
+Module: Utility functions for code contracts.
+
+Author: Saswat Padhi, saspadhi@amazon.com
+
+Date: September 2021
+
+\*******************************************************************/
+
+#include "utils.h"
+
+exprt generate_lexicographic_less_than_check(
+  const std::vector<symbol_exprt> &lhs,
+  const std::vector<symbol_exprt> &rhs)
+{
+  PRECONDITION(lhs.size() == rhs.size());
+
+  if(lhs.empty())
+  {
+    return false_exprt();
+  }
+
+  // Store conjunctions of equalities.
+  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
+  // l2, l3>.
+  // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
+  // s1 == l1 && s2 == l2 && s3 == l3>.
+  // In fact, the last element is unnecessary, so we do not create it.
+  exprt::operandst equality_conjunctions(lhs.size());
+  equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
+  for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
+  {
+    binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
+    equality_conjunctions[i] =
+      and_exprt(equality_conjunctions[i - 1], component_i_equality);
+  }
+
+  // Store inequalities between the i-th components of the input vectors
+  // (i.e. lhs and rhs).
+  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
+  // l2, l3>.
+  // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
+  // s2 == l2 && s3 < l3>.
+  exprt::operandst lexicographic_individual_comparisons(lhs.size());
+  lexicographic_individual_comparisons[0] =
+    binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
+  for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
+  {
+    binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
+    lexicographic_individual_comparisons[i] =
+      and_exprt(equality_conjunctions[i - 1], component_i_less_than);
+  }
+  return disjunction(lexicographic_individual_comparisons);
+}
+
+void insert_before_swap_and_advance(
+  goto_programt &destination,
+  goto_programt::targett &target,
+  goto_programt &payload)
+{
+  const auto offset = payload.instructions.size();
+  destination.insert_before_swap(target, payload);
+  std::advance(target, offset);
+}

src/goto-instrument/contracts/utils.h

@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+Module: Utility functions for code contracts.
+
+Author: Saswat Padhi, saspadhi@amazon.com
+
+Date: September 2021
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
+
+#include <vector>
+
+#include <goto-programs/goto_model.h>
+
+/// \brief Generate a lexicographic less-than comparison over ordered tuples
+///
+/// This function creates an expression representing a lexicographic less-than
+/// comparison, lhs < rhs, between two ordered tuples of variables.
+/// This is used in instrumentation of decreases clauses.
+///
+/// \param lhs A vector of variables representing the LHS of the comparison
+/// \param rhs A vector of variables representing the RHS of the comparison
+/// \return A lexicographic less-than comparison expression: LHS < RHS
+exprt generate_lexicographic_less_than_check(
+  const std::vector<symbol_exprt> &lhs,
+  const std::vector<symbol_exprt> &rhs);
+
+/// \brief Insert a goto program before a target instruction iterator
+///        and advance the iterator.
+///
+/// This function inserts all instruction from a goto program `payload` into a
+/// destination program `destination` immediately before a specified instruction
+/// iterator `target`.
+/// After insertion, `target` is advanced by the size of the `payload`,
+/// and `payload` is destroyed.
+///
+/// \param program The destination program for inserting the `payload`
+/// \param target The instruction iterator at which to insert the `payload`
+/// \param payload The goto program to be inserted into the `destination`
+void insert_before_swap_and_advance(
+  goto_programt &destination,
+  goto_programt::targett &target,
+  goto_programt &payload);
+
+#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H