Added support for loop_entry history variable.

1. Created a new predicate __CPROVER_loop_entry which can be used in the loop invariant
   to keep track of the value of a variable at the start of the loop.
2. Modified the code contract to support this history variable.

Author: Aalok Thakkar

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

@@ -3,8 +3,8 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=(1|64)$
 ^SIGNAL=0$
+^main.c.* error: __CPROVER_old expressions are not allowed in this context$
 ^CONVERSION ERROR$
-error: __CPROVER_old expressions are not allowed in __CPROVER_requires clauses
 --
 --
 Verification:

regression/contracts/loop-history-variables-01/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 == __CPROVER_loop_entry(*s1))
+    {
+      --y3;
+      s1->n = s1->n + 1;
+      s1->n = s1->n - 1;
+    }
+
+  assert(s1->n == s2->n);
+}

regression/contracts/loop-history-variables-01/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/loop-history-variables-02/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/loop-history-variables-02/test.desc

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

regression/contracts/loop-history-variables-03/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/loop-history-variables-03/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^main.c.* error: __CPROVER_loop_entry expressions are not allowed in this context$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that __CPROVER_loop_entry cannot be
+used for function contracts.

regression/contracts/loop-history-variables-04/main.c

@@ -0,0 +1,16 @@
+#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;
+    }
+  assert(x == z);
+}

regression/contracts/loop-history-variables-04/test.desc

@@ -0,0 +1,12 @@
+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$
+^\[main.assertion.1\] .* assertion x == z: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+This test checks that __CPROVER_loop_entry is sound.

src/ansi-c/c_expr.h

@@ -202,10 +202,11 @@ inline side_effect_expr_overflowt &to_side_effect_expr_overflow(exprt &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
+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 +216,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,8 @@ void c_typecheck_baset::typecheck_declaration(
           {
             typecheck_expr(requires);
             implicit_typecast_bool(requires);
-            disallow_history_variables(requires);
+            disallow_history_variables(requires, ID_old);
+            disallow_history_variables(requires, ID_loop_entry);
           }
         }
 
@@ -751,6 +752,7 @@ void c_typecheck_baset::typecheck_declaration(
           {
             typecheck_expr(ensures);
             implicit_typecast_bool(ensures);
+            disallow_history_variables(ensures, ID_loop_entry);
           }
 
           if(return_type.id() != ID_empty)

src/ansi-c/c_typecheck_base.h

@@ -206,7 +206,7 @@ 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_history_variables(const exprt &, const irep_idt &) const;
 
   virtual void make_index_type(exprt &expr);
   virtual void make_constant(exprt &expr);

src/ansi-c/c_typecheck_code.cpp

@@ -820,6 +820,7 @@ void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
     {
       typecheck_expr(invariant);
       implicit_typecast_bool(invariant);
+      disallow_history_variables(invariant, ID_old);
     }
   }
 }

src/ansi-c/c_typecheck_expr.cpp

@@ -2704,7 +2704,21 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    old_exprt old_expr(expr.arguments()[0]);
+    history_exprt old_expr(expr.arguments()[0], ID_old);
+    old_expr.add_source_location() = source_location;
+
+    return std::move(old_expr);
+  }
+  else if(identifier == CPROVER_PREFIX "loop_entry")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects one operand" << eom;
+      throw 0;
+    }
+
+    history_exprt old_expr(expr.arguments()[0], ID_loop_entry);
     old_expr.add_source_location() = source_location;
 
     return std::move(old_expr);
@@ -3957,18 +3971,27 @@ 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_history_variables(
+  const exprt &expr,
+  const irep_idt &id) const
 {
   for(auto &op : expr.operands())
   {
-    disallow_history_variables(op);
+    disallow_history_variables(op, id);
   }
 
-  if(expr.id() == ID_old)
+  if(expr.id() == ID_old && id == ID_old)
+  {
+    error().source_location = expr.source_location();
+    error() << CPROVER_PREFIX "old expressions are not allowed in this context"
+            << eom;
+    throw 0;
+  }
+  else if(expr.id() == ID_loop_entry && id == ID_loop_entry)
   {
     error().source_location = expr.source_location();
     error() << CPROVER_PREFIX
-      "old expressions are not allowed in " CPROVER_PREFIX "requires clauses"
+      "loop_entry expressions are not allowed in this context"
             << 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 *);

src/goto-instrument/contracts/contracts.cpp

@@ -147,6 +147,8 @@ void code_contractst::check_apply_loop_contracts(
   //   H: loop;
   //   E: ...
   // to
+  //   process history variables;
+  //   declare and assign loop_entry variables;
   //   H: assert(invariant);
   //   havoc;
   //   assume(invariant);
@@ -176,6 +178,20 @@ void code_contractst::check_apply_loop_contracts(
     return invariant_copy;
   };
 
+  // Process "loop_entry" history variables
+  // Find and replace "loop_entry" expression in the "invariant" expression.
+  std::map<exprt, exprt> parameter2history;
+  replace_history_parameter(
+    invariant,
+    parameter2history,
+    loop_head->source_location,
+    mode,
+    havoc_code,
+    ID_loop_entry);
+
+  // Create 'loop_entry' history variables
+  insert_before_swap_and_advance(goto_function.body, loop_head, havoc_code);
+
   // Generate: assert(invariant) just before the loop
   // We use a block scope to create a temporary assertion,
   // and immediately convert it to goto instructions.
@@ -377,24 +393,23 @@ void code_contractst::add_quantified_variable(
   }
 }
 
-void code_contractst::replace_old_parameter(
+void code_contractst::replace_history_parameter(
   exprt &expr,
   std::map<exprt, exprt> &parameter2history,
   source_locationt location,
   const irep_idt &mode,
-  goto_programt &history)
+  goto_programt &history,
+  const irep_idt &id)
 {
   for(auto &op : expr.operands())
   {
-    replace_old_parameter(op, parameter2history, location, mode, history);
+    replace_history_parameter(
+      op, parameter2history, location, mode, history, id);
   }
 
-  if(expr.id() == ID_old)
+  if(expr.id() == ID_old || expr.id() == ID_loop_entry)
   {
-    DATA_INVARIANT(
-      expr.operands().size() == 1, CPROVER_PREFIX "old must have one operand");
-
-    const auto &parameter = to_old_expr(expr).expression();
+    const auto &parameter = to_history_expr(expr, id).expression();
 
     if(
       parameter.id() == ID_dereference || parameter.id() == ID_member ||
@@ -428,8 +443,8 @@ void code_contractst::replace_old_parameter(
     }
     else
     {
-      log.error() << CPROVER_PREFIX "old does not currently support "
-                  << parameter.id() << " expressions." << messaget::eom;
+      log.error() << "History variables do not support " << parameter.id()
+                  << " expressions." << messaget::eom;
       throw 0;
     }
   }
@@ -445,7 +460,8 @@ code_contractst::create_ensures_instruction(
   goto_programt history;
 
   // Find and replace "old" expression in the "expression" variable
-  replace_old_parameter(expression, parameter2history, location, mode, history);
+  replace_history_parameter(
+    expression, parameter2history, location, mode, history, ID_old);
 
   // Create instructions corresponding to the ensures clause
   goto_programt ensures_program;

src/goto-instrument/contracts/contracts.h

@@ -219,12 +219,13 @@ class code_contractst
 
   /// This function recursively identifies the "old" expressions within expr
   /// and replaces them with correspoding history variables.
-  void replace_old_parameter(
+  void replace_history_parameter(
     exprt &expr,
     std::map<exprt, exprt> &parameter2history,
     source_locationt location,
     const irep_idt &mode,
-    goto_programt &history);
+    goto_programt &history,
+    const irep_idt &id);
 
   /// This function creates and returns an instruction that corresponds to the
   /// ensures clause. It also returns a list of instructions related to

src/util/irep_ids.def

@@ -691,6 +691,7 @@ IREP_ID_ONE(r_ok)
 IREP_ID_ONE(w_ok)
 IREP_ID_ONE(rw_ok)
 IREP_ID_ONE(old)
+IREP_ID_ONE(loop_entry)
 IREP_ID_ONE(super_class)
 IREP_ID_ONE(exceptions_thrown_list)
 IREP_ID_TWO(C_java_method_type, #java_method_type)