Merge pull request #7487 from qinheping/goto-synthesizer

CONTRACTS: Avoid skipping transformed loop with jumps to the loop head

Author: qinheping

regression/contracts/labled_loop_head/main.c

@@ -0,0 +1,12 @@
+int main()
+{
+  int x;
+  goto label;
+  x = 2;
+label:
+  while(x < 5)
+    __CPROVER_loop_invariant(x <= 5)
+    {
+      x++;
+    }
+}

regression/contracts/labled_loop_head/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assigns.\d+\] .* Check that x is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks transformed loop won't be skipped by a jump to the loop head.

src/goto-instrument/contracts/contracts.cpp

@@ -890,6 +890,17 @@ void code_contractst::apply_loop_contract(
       throw 0;
     }
 
+    // After loop-contract instrumentation, jumps to the `loop_head` will skip
+    // some instrumented instructions. So we want to make sure that there is
+    // only one jump targeting `loop_head` from `loop_end` before loop-contract
+    // instrumentation.
+    // Add a skip before `loop_head` and let all jumps (except for the
+    // `loop_end`) that target to the `loop_head` target to the skip
+    // instead.
+    insert_before_and_update_jumps(
+      goto_function.body, loop_head, goto_programt::make_skip());
+    loop_end->set_target(loop_head);
+
     exprt assigns_clause =
       static_cast<const exprt &>(loop_end->condition().find(ID_C_spec_assigns));
     exprt invariant = static_cast<const exprt &>(

src/goto-instrument/contracts/utils.cpp

@@ -154,6 +154,19 @@ void insert_before_swap_and_advance(
   std::advance(target, offset);
 }
 
+void insert_before_and_update_jumps(
+  goto_programt &destination,
+  goto_programt::targett &target,
+  const goto_programt::instructiont &i)
+{
+  const auto new_target = destination.insert_before(target, i);
+  for(auto it : target->incoming_edges)
+  {
+    if(it->is_goto())
+      it->set_target(new_target);
+  }
+}
+
 const symbolt &new_tmp_symbol(
   const typet &type,
   const source_locationt &location,

src/goto-instrument/contracts/utils.h

@@ -11,11 +11,11 @@ Date: September 2021
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
 
-#include <vector>
+#include <goto-programs/goto_convert_class.h>
 
 #include <goto-instrument/havoc_utils.h>
 
-#include <goto-programs/goto_convert_class.h>
+#include <vector>
 
 #define IN_BASE_CASE "__in_base_case"
 #define ENTERED_LOOP "__entered_loop"
@@ -110,6 +110,30 @@ void insert_before_swap_and_advance(
   goto_programt::targett &target,
   goto_programt &payload);
 
+/// \brief Insert a goto instruction before a target instruction iterator
+///        and update targets of all jumps that points to the iterator to
+///        jumping to the inserted instruction. This method is intended
+///        to keep external instruction::targett stable, i.e. they will
+///        still point to the same instruction after inserting the new one
+///
+/// This function inserts a instruction `i` into a destination program
+/// `destination` immediately before a specified instruction iterator `target`.
+/// After insertion, update all jumps that pointing to `target` to jumping to
+/// `i` instead.
+///
+/// Different from `insert_before_swap_and_advance`, this function doesn't
+/// invalidate the iterator `target` after insertion. That is, `target` and
+/// all other instruction iterators same as `target` will still point to the
+/// same instruction after insertion.
+///
+/// \param destination: The destination program for inserting the `i`.
+/// \param target: The instruction iterator at which to insert the `i`.
+/// \param i: The goto instruction to be inserted into the `destination`.
+void insert_before_and_update_jumps(
+  goto_programt &destination,
+  goto_programt::targett &target,
+  const goto_programt::instructiont &i);
+
 /// \brief Adds a fresh and uniquely named symbol to the symbol table.
 ///
 /// \param type: The type of the new symbol.
@@ -192,7 +216,7 @@ void add_quantified_variable(
   const irep_idt &mode);
 
 /// This function recursively identifies the "old" expressions within expr
-/// and replaces them with correspoding history variables.
+/// and replaces them with corresponding history variables.
 void replace_history_parameter(
   symbol_table_baset &symbol_table,
   exprt &expr,