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. This also demonstrated
that the implementation in the test was incorrect: it would not terminate when:
*(arr[h]) == pivot && *(arr[l]) == pivot && h != r && l != r.

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 &&
@@ -61,6 +62,11 @@ int main()
           r = h;
           l++;
         }
+        else
+        {
+          h--;
+          l++;
+        }
       }
       else if(*(arr[h]) <= pivot)
       {

regression/contracts/invar_check_large/test.desc

@@ -4,7 +4,7 @@ main.c
 ^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$

src/goto-instrument/contracts/contracts.cpp

@@ -682,14 +682,22 @@ 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);
-
-  if(!natural_loops.loop_map.size())
+  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(!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 +1016,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(