Add support for quantifiers in loop contracts

This adds support for quantifiers in loop contracts.
To do so, we call the add_quantified_variable function
(introduced in a previous PR) when handling loop invariants.

Author: ArenBabikian

regression/contracts/quantifiers-loop-01/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+void main()
+{
+  int N = 64, a[64];
+  for(int i = 0; i < N; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
+      int k;
+      (0 <= k && k < N) ==> 1 == 1
+    })
+    // clang-format on
+    {
+      a[i] = 1;
+    }
+}

regression/contracts/quantifiers-loop-01/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression within
+a loop invariant.
+This test case does not check correctness of the for loop.
+Instead, it is a trivial quantified expression to ensure that
+quantifiers can be handled in loop invariants.

regression/contracts/quantifiers-loop-02/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+void main()
+{
+  int N = 64, a[64];
+  for(int i = 0; i < N; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
+      int k;
+      (0 <= k && k < i) ==> a[k] == 1
+    })
+    // clang-format on
+    {
+      a[i] = 1;
+    }
+  // clang-format off
+  assert(__CPROVER_forall {
+    int k;
+    (0 <= k && k < N) ==> a[k] == 1
+  });
+  // clang-format on
+}

regression/contracts/quantifiers-loop-02/test.desc

@@ -0,0 +1,16 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression within
+a loop invariant.
+In this test, the quantified variable has a symbolic upper limit.
+
+Known Bug:
+Currently, cbmc (using the SAT back-end) does not support quantified
+expressions where the quantified variable has a symbolic range.

regression/contracts/quantifiers-loop-03/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+void main()
+{
+  int N, a[64];
+  __CPROVER_assume(0 <= N && N < 64);
+  for(int i = 0; i < N; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
+      int k;
+      (0 <= k && k < i) ==> a[k] == 1
+    })
+    // clang-format on
+    {
+      a[i] = 1;
+    }
+  // clang-format off
+  assert(__CPROVER_forall {
+    int k;
+    (0 <= k && k < N) ==> a[k] == 1
+  });
+  // clang-format on
+}

regression/contracts/quantifiers-loop-03/test.desc

@@ -0,0 +1,18 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression within
+a loop invariant.
+In this test, the quantified variable has a symbolic upper limit.
+Additionally, the number of loop iterations is also defined by a
+symbolic value.
+
+Known Bug:
+Currently, cbmc (using the SAT back-end) does not support quantified
+expressions where the quantified variable has a symbolic range.

src/goto-instrument/code_contracts.cpp

@@ -74,7 +74,7 @@ exprt get_size(const typet &type, const namespacet &ns, messaget &log)
   return result;
 }
 
-static void check_apply_invariants(
+void code_contractst::check_apply_invariants(
   goto_functionst::goto_functiont &goto_function,
   goto_convertt &converter,
   const local_may_aliast &local_may_alias,
@@ -98,6 +98,14 @@ static void check_apply_invariants(
   if(invariant.is_nil())
     return;
 
+  // Add quantified variables in contracts to the symbol map
+  // TODO improve the structure below wrt the replace_symbolt object
+  //   In the current implementation, the add_quantified_variable
+  //   function requires a replace_symbolt object as input, which is
+  //   irrelevant in the context of loop contracts.
+  replace_symbolt replace;
+  code_contractst::add_quantified_variable(invariant, replace, mode);
+
   // change
   //   H: loop;
   //   E: ...
@@ -224,8 +232,8 @@ void code_contractst::add_quantified_variable(
     // 2. create fresh symbol
     symbolt new_symbol = get_fresh_aux_symbol(
       quantified_symbol.type(),
+      "",
       id2string(quantified_symbol.get_identifier()),
-      "tmp",
       quantified_symbol.source_location(),
       mode,
       symbol_table);

src/goto-instrument/code_contracts.h

@@ -18,15 +18,20 @@ Date: February 2016
 #include <string>
 #include <unordered_set>
 
+#include <goto-programs/goto_convert_class.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
+#include <goto-instrument/loop_utils.h>
+
 #include <util/c_types.h>
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/replace_symbol.h>
 
+#include <analyses/local_may_alias.h>
+
 class messaget;
 class assigns_clauset;
 
@@ -178,6 +183,14 @@ class code_contractst
     exprt expression,
     replace_symbolt &replace,
     irep_idt mode);
+
+  void check_apply_invariants(
+    goto_functionst::goto_functiont &goto_function,
+    goto_convertt &converter,
+    const local_may_aliast &local_may_alias,
+    const goto_programt::targett loop_head,
+    const loopt &loop,
+    const irep_idt &mode);
 };
 
 #define FLAG_REPLACE_CALL "replace-call-with-contract"