From 3af47189ee2b115eb0efae7f4921d693dd635651 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 30 Nov 2021 16:04:25 +0000
Subject: [PATCH] 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.
---
 regression/contracts/invar_check_large/main.c  |  6 ++++++
 .../contracts/invar_check_large/test.desc      |  2 +-
 src/goto-instrument/contracts/contracts.cpp    | 18 ++++++++++++++----
 3 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/regression/contracts/invar_check_large/main.c b/regression/contracts/invar_check_large/main.c
index cc67eb7bdc5..8f817a3a8cb 100644
--- a/regression/contracts/invar_check_large/main.c
+++ b/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)
       {
diff --git a/regression/contracts/invar_check_large/test.desc b/regression/contracts/invar_check_large/test.desc
index 3b84ac40658..e6d3e50bfb0 100644
--- a/regression/contracts/invar_check_large/test.desc
+++ b/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$
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 6efbb3f6227..26df2dfbfb3 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -773,10 +773,14 @@ 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;
 
   inlining_decoratort decorated(log.get_message_handler());
@@ -787,6 +791,12 @@ void code_contractst::apply_loop_contract(
     decorated.get_recursive_function_warnings_count() == 0,
     "Recursive functions found during inlining");
 
+  // restore internal invariants
+  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,
   // sort them topologically, and instrument them in the top-sorted order.