fix recording old variant value at the beginning of loop body

The loop variant value is supposed to be recorded just after the loop
head (i.e., at the beginning of the loop body). Previously this was
done by computing std::next(loop_head). However, complex C loop guards
could be compiled to multiple GOTO instructions and it might be
necessarey to advance the loop_head multiple times.

The proposed change advanced the loop_head instruction pointer until the
source_location differs.

Author: SaswatPadhi

regression/contracts/variant_multi_instruction_loop_head/main.c

@@ -0,0 +1,14 @@
+int main()
+{
+  int x = 0;
+  int *y = &x;
+
+  while(*y <= 0 && *y < 10)
+    // clang-format off
+    __CPROVER_loop_invariant(1 == 1)
+    __CPROVER_decreases(10 - x)
+    // clang-format on
+    {
+      x++;
+    }
+}

regression/contracts/variant_multi_instruction_loop_head/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--apply-loop-contracts
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test fails even without the fix proposed in the commit, so it should be improved.
+It is expected to fail because the proposed invariant isn't strong enough to help prove
+termination using the specified variant.
+
+The test highlights a case where a C loop guard is compiled to multiple GOTO instructions.
+Therefore the loop_head pointer needs to be advanced multiple times to get to the loop body,
+where the initial value of the loop variant (/ ranking function) must be recorded.
+
+The proposed fix advances the pointer until the source_location differs from the original
+loop_head's source_location. However, this might still not work if the loop guard in the
+original C code was split across multiple lines in the first place.

src/goto-instrument/contracts/contracts.cpp

@@ -209,7 +209,13 @@ void code_contractst::check_apply_loop_contracts(
       converter.goto_convert(old_decreases_assignment, havoc_code, mode);
     }
 
-    goto_function.body.destructive_insert(std::next(loop_head), havoc_code);
+    // Forward the loop_head iterator until the start of the body.
+    // This is necessary because complex C loop_head conditions could be
+    // converted to multiple GOTO instructions (e.g. temporaries are introduced).
+    const auto head_loc = loop_head->source_location();
+    while(loop_head->source_location() == head_loc)
+      loop_head = std::next(loop_head);
+    goto_function.body.destructive_insert(loop_head, havoc_code);
   }
 
   // Generate: assert(invariant) just after the loop exits