Added loop_entry history variables for invariants

In this commit we introduce a new expression, `__CPROVER_loop_entry`,
which can be used within loop invariants to track history of variables.
`__CPROVER_loop_entry(x)` returns the initial value of a variable just
before the very first iteration of a loop.

Co-authored-by: Aalok Thakkar <[email protected]>

regression/contracts/function_loop_history_ensures_fail/main.c

@@ -0,0 +1,13 @@
+void foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_ensures(*x == __CPROVER_loop_entry(*x) + 5)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

regression/contracts/function_loop_history_ensures_fail/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^main.c.* error: __CPROVER_loop_entry is not allowed in postconditions.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that __CPROVER_loop_entry cannot be used within ensures clause.

regression/contracts/function_loop_history_requires_fail/main.c

@@ -0,0 +1,13 @@
+void bar(int *x) __CPROVER_assigns(*x)
+  __CPROVER_requires(*x == __CPROVER_loop_entry(*x) + 5)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

regression/contracts/function_loop_history_requires_fail/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^main.c.* error: __CPROVER_loop_entry is not allowed in preconditions.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that __CPROVER_loop_entry cannot be used within requires clause.

regression/contracts/history-pointer-replace-03/test.desc

@@ -1,12 +1,11 @@
 CORE
 main.c
 --replace-all-calls-with-contracts
+^main.c.* error: __CPROVER_old is not allowed in preconditions.$
+^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^CONVERSION ERROR$
-error: __CPROVER_old expressions are not allowed in __CPROVER_requires clauses
 --
 --
-Verification:
 This test checks that history variables cannot be used as part of the
-pre-condition contract. In this case, verification should fail.
+pre-condition (requires) contract.

regression/contracts/invar_function-old_fail/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+void main()
+{
+  int *x, y, z;
+
+  x = &z;
+
+  while(y > 0)
+    __CPROVER_loop_invariant(*x == __CPROVER_old(*x))
+    {
+      --y;
+      *x = *x + 1;
+      *x = *x - 1;
+    }
+  assert(*x == z);
+}

regression/contracts/invar_function-old_fail/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c.* error: __CPROVER_old is not allowed in loop invariants.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that __CPROVER_old cannot be used within loop contracts. 

regression/contracts/invar_loop-entry_check/main.c

@@ -0,0 +1,49 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct
+{
+  int *n;
+} s;
+
+void main()
+{
+  int *x1, y1, z1;
+  x1 = &z1;
+
+  while(y1 > 0)
+    __CPROVER_loop_invariant(*x1 == __CPROVER_loop_entry(*x1))
+    {
+      --y1;
+      *x1 = *x1 + 1;
+      *x1 = *x1 - 1;
+    }
+  assert(*x1 == z1);
+
+  int x2, y2, z2;
+  x2 = z2;
+
+  while(y2 > 0)
+    __CPROVER_loop_invariant(x2 == __CPROVER_loop_entry(x2))
+    {
+      --y2;
+      x2 = x2 + 1;
+      x2 = x2 - 1;
+    }
+  assert(x2 == z2);
+
+  int y3;
+  s *s1, *s2;
+  s2->n = malloc(sizeof(int));
+  s1->n = s2->n;
+
+  while(y3 > 0)
+    __CPROVER_loop_invariant(s1->n == __CPROVER_loop_entry(s1->n))
+    {
+      --y3;
+      s1->n = s1->n + 1;
+      s1->n = s1->n - 1;
+    }
+
+  assert(*(s1->n) == *(s2->n));
+}

regression/contracts/invar_loop-entry_check/test.desc

@@ -0,0 +1,18 @@
+CORE
+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.assertion.1\] .* assertion \*x1 == z1: SUCCESS$
+^\[main.3\] .* Check loop invariant before entry: SUCCESS$
+^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.2\] .* assertion x2 == z2: SUCCESS$
+^\[main.5\] .* Check loop invariant before entry: SUCCESS$
+^\[main.6\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.3\] .* assertion \*\(s1->n\) == \*\(s2->n\): SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that __CPROVER_loop_entry is supported.

regression/contracts/invar_loop-entry_fail/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+void main()
+{
+  int x, y, z;
+  x = z;
+
+  while(y > 0)
+    __CPROVER_loop_invariant(x == __CPROVER_loop_entry(x))
+    {
+      --y;
+      x = x + 1;
+      x = x - 2;
+    }
+}

regression/contracts/invar_loop-entry_fail/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=(10|6)$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test ensures that __CPROVER_loop_entry violations are checked.

src/ansi-c/c_expr.h

@@ -200,12 +200,12 @@ inline side_effect_expr_overflowt &to_side_effect_expr_overflow(exprt &expr)
   return static_cast<side_effect_expr_overflowt &>(side_effect_expr);
 }
 
-/// \brief A class for an expression that indicates the pre-function-call
-/// value of an expression passed as a parameter to a function
-class old_exprt : public unary_exprt
+/// \brief A class for an expression that indicates a history variable
+class history_exprt : public unary_exprt
 {
 public:
-  explicit old_exprt(exprt variable) : unary_exprt(ID_old, std::move(variable))
+  explicit history_exprt(exprt variable, const irep_idt &id)
+    : unary_exprt(id, std::move(variable))
   {
   }
 
@@ -215,10 +215,12 @@ class old_exprt : public unary_exprt
   }
 };
 
-inline const old_exprt &to_old_expr(const exprt &expr)
+inline const history_exprt &
+to_history_expr(const exprt &expr, const irep_idt &id)
 {
-  PRECONDITION(expr.id() == ID_old);
-  auto &ret = static_cast<const old_exprt &>(expr);
+  PRECONDITION(id == ID_old || id == ID_loop_entry);
+  PRECONDITION(expr.id() == id);
+  auto &ret = static_cast<const history_exprt &>(expr);
   validate_expr(ret);
   return ret;
 }

src/ansi-c/c_typecheck_base.cpp

@@ -730,7 +730,14 @@ void c_typecheck_baset::typecheck_declaration(
           {
             typecheck_expr(requires);
             implicit_typecast_bool(requires);
-            disallow_history_variables(requires);
+            disallow_subexpr_by_id(
+              requires,
+              ID_old,
+              CPROVER_PREFIX "old is not allowed in preconditions.");
+            disallow_subexpr_by_id(
+              requires,
+              ID_loop_entry,
+              CPROVER_PREFIX "loop_entry is not allowed in preconditions.");
           }
         }
 
@@ -751,6 +758,10 @@ void c_typecheck_baset::typecheck_declaration(
           {
             typecheck_expr(ensures);
             implicit_typecast_bool(ensures);
+            disallow_subexpr_by_id(
+              ensures,
+              ID_loop_entry,
+              CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
           }
 
           if(return_type.id() != ID_empty)

src/ansi-c/c_typecheck_base.h

@@ -206,7 +206,10 @@ class c_typecheck_baset:
     const symbol_exprt &function_symbol);
   virtual exprt
   typecheck_shuffle_vector(const side_effect_expr_function_callt &expr);
-  void disallow_history_variables(const exprt &) const;
+  void disallow_subexpr_by_id(
+    const exprt &,
+    const irep_idt &,
+    const std::string &) const;
 
   virtual void make_index_type(exprt &expr);
   virtual void make_constant(exprt &expr);

src/ansi-c/c_typecheck_code.cpp

@@ -820,6 +820,10 @@ void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
     {
       typecheck_expr(invariant);
       implicit_typecast_bool(invariant);
+      disallow_subexpr_by_id(
+        invariant,
+        ID_old,
+        CPROVER_PREFIX "old is not allowed in loop invariants.");
     }
   }
 }

src/ansi-c/c_typecheck_expr.cpp

@@ -2695,7 +2695,9 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(ok_expr);
   }
-  else if(identifier == CPROVER_PREFIX "old")
+  else if(
+    (identifier == CPROVER_PREFIX "old") ||
+    (identifier == CPROVER_PREFIX "loop_entry"))
   {
     if(expr.arguments().size() != 1)
     {
@@ -2704,7 +2706,9 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    old_exprt old_expr(expr.arguments()[0]);
+    irep_idt id = identifier == CPROVER_PREFIX "old" ? ID_old : ID_loop_entry;
+
+    history_exprt old_expr(expr.arguments()[0], id);
     old_expr.add_source_location() = source_location;
 
     return std::move(old_expr);
@@ -3957,19 +3961,15 @@ void c_typecheck_baset::make_constant_index(exprt &expr)
   }
 }
 
-void c_typecheck_baset::disallow_history_variables(const exprt &expr) const
+void c_typecheck_baset::disallow_subexpr_by_id(
+  const exprt &expr,
+  const irep_idt &id,
+  const std::string &message) const
 {
-  for(auto &op : expr.operands())
-  {
-    disallow_history_variables(op);
-  }
+  if(!has_subexpr(expr, id))
+    return;
 
-  if(expr.id() == ID_old)
-  {
-    error().source_location = expr.source_location();
-    error() << CPROVER_PREFIX
-      "old expressions are not allowed in " CPROVER_PREFIX "requires clauses"
-            << eom;
-    throw 0;
-  }
+  error().source_location = expr.source_location();
+  error() << message << eom;
+  throw 0;
 }

src/ansi-c/cprover_builtin_headers.h

@@ -37,6 +37,7 @@ void __CPROVER_fence(const char *kind, ...);
 // contract-related functions
 __CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size);
 void __CPROVER_old(const void *);
+void __CPROVER_loop_entry(const void *);
 
 // pointers
 __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);