Invoke goto_functions.update() after inlining

Inlining will alter location (instruction) numbers, which need to be
updated to once again be globally unique.

With this change, invar_check_large requires an assigns clause for the
loop as the local may alias analysis returns "UNKNOWN." The previous
result was actually unsound, because the automatically computed assigns
set did not include arr0, arr1, arr2, arr3, arr4. Once we havoc these,
however, the loop invariant is no longer strong enough to prove the
decreases clause.

Author: tautschnig

regression/contracts/invar_check_large/main.c

@@ -23,6 +23,7 @@ int main()
   int r = 1;
   while(h > l)
     // clang-format off
+    __CPROVER_assigns(arr0, arr1, arr2, arr3, arr4, h, l, r)
     __CPROVER_loop_invariant(
       // Turn off `clang-format` because it breaks the `==>` operator.
       h >= l &&

regression/contracts/invar_check_large/test.desc

@@ -1,10 +1,10 @@
-CORE
+KNOWNBUG
 main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main.assertion.1\] .* assertion 0 <= r && r < 5: SUCCESS$
 ^\[main.assertion.2\] .* assertion \*\(arr\[r\]\) == pivot: SUCCESS$
 ^\[main.assertion.3\] .* assertion 0 < r ==> arr0 <= pivot: SUCCESS$
@@ -23,3 +23,7 @@ This test checks the invariant contracts on a larger problem --- in this case,
 the partition function of quicksort, applied to a fixed-length array.
 This serves as a stop-gap test until issues to do with quantifiers and
 side-effects in loop invariants are fixed.
+
+We currently fail to prove the "decreases" clause once "arr0, arr1, arr2, arr3,
+arr4" are listed in the assigns clause. Automatic inference of the assigns
+clause failed to call these out, resulting in a spurious termination proof.

src/goto-instrument/contracts/contracts.cpp

@@ -682,14 +682,23 @@ void code_contractst::apply_loop_contract(
   const irep_idt &function_name,
   goto_functionst::goto_functiont &goto_function)
 {
-  local_may_aliast local_may_alias(goto_function);
-  natural_loops_mutablet natural_loops(goto_function.body);
+  const bool may_have_loops = std::any_of(
+    goto_function.body.instructions.begin(),
+    goto_function.body.instructions.end(),
+    [](const goto_programt::instructiont &instruction)
+    {
+    return instruction.is_backwards_goto();
+    });
 
-  if(!natural_loops.loop_map.size())
+  if(!may_have_loops)
     return;
 
   goto_function_inline(
     goto_functions, function_name, ns, log.get_message_handler());
+  goto_functions.update();
+
+  local_may_aliast local_may_alias(goto_function);
+  natural_loops_mutablet natural_loops(goto_function.body);
 
   // A graph node type that stores information about a loop.
   // We create a DAG representing nesting of various loops in goto_function,
@@ -1008,6 +1017,7 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
   // Inline all function calls.
   goto_function_inline(
     goto_functions, function_obj->first, ns, log.get_message_handler());
+  goto_functions.update();
 
   // Insert write set inclusion checks.
   check_frame_conditions(