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. This approach might still fail if the loop
guard was split across multiple lines in the source file.

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,21 @@ 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).
+    // FIXME: This simple approach wouldn't work when
+    // the loop guard in the source file is split across multiple lines.
+    const auto head_loc = loop_head->source_location();
+    while(loop_head->source_location() == head_loc)
+      loop_head = std::next(loop_head);
+
+    // At this point, we are just past the loop head,
+    // so at the beginning of the loop body.
+    auto loop_body = loop_head;
+    loop_head--;
+
+    goto_function.body.destructive_insert(loop_body, havoc_code);
   }
 
   // Generate: assert(invariant) just after the loop exits