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/loop-history-variables-01/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_loop_entry(*x))
+  {
+    --y;
+    *x = *x + 1;
+    *x = *x - 1;
+  }
+  assert(*x == &z);
+}

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

@@ -0,0 +1,11 @@
+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$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that the history variable for loop entry is supported.

src/ansi-c/c_typecheck_base.cpp

@@ -731,6 +731,7 @@ void c_typecheck_baset::typecheck_declaration(
             typecheck_expr(requires);
             implicit_typecast_bool(requires);
             disallow_history_variables(requires);
+            disallow_loop_history_variables(requires);
           }
         }
 
@@ -751,6 +752,7 @@ void c_typecheck_baset::typecheck_declaration(
           {
             typecheck_expr(ensures);
             implicit_typecast_bool(ensures);
+            disallow_loop_history_variables(ensures);
           }
 
           if(return_type.id() != ID_empty)

src/ansi-c/c_typecheck_base.h

@@ -207,6 +207,7 @@ class c_typecheck_baset:
   virtual exprt
   typecheck_shuffle_vector(const side_effect_expr_function_callt &expr);
   void disallow_history_variables(const exprt &) const;
+  void disallow_loop_history_variables(const exprt &) const;
 
   virtual void make_index_type(exprt &expr);
   virtual void make_constant(exprt &expr);

src/ansi-c/c_typecheck_expr.cpp

@@ -2647,7 +2647,8 @@ 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)
     {
@@ -3925,3 +3926,20 @@ void c_typecheck_baset::disallow_history_variables(const exprt &expr) const
     throw 0;
   }
 }
+
+void c_typecheck_baset::disallow_loop_history_variables(const exprt &expr) const
+{
+  for(auto &op : expr.operands())
+  {
+    disallow_loop_history_variables(op);
+  }
+
+  if(expr.id() == ID_loop_entry)
+  {
+    error().source_location = expr.source_location();
+    error() << CPROVER_PREFIX
+      "loop_entry expressions are not allowed in function contracts"
+            << 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

@@ -145,6 +145,7 @@ void code_contractst::check_apply_loop_contracts(
   //   H: loop;
   //   E: ...
   // to
+  //   process history variables;
   //   H: assert(invariant);
   //   havoc;
   //   assume(invariant);
@@ -174,6 +175,16 @@ void code_contractst::check_apply_loop_contracts(
     return invariant_copy;
   };
 
+  // Process "loop_entry" history variables
+  std::map<exprt, exprt> parameter2history;
+  goto_programt history;
+
+  // Find and replace "loop_entry" expression in the "invariant" expression.
+  replace_old_parameter(invariant, parameter2history, loop_head->source_location, mode, history);
+
+  // Create 'loop_entry' history variables
+  insert_before_swap_and_advance(goto_function.body, loop_head, history);
+
   // Generate: assert(invariant) just before the loop
   // We use a block scope to create a temporary assertion,
   // and immediately convert it to goto instructions.
@@ -387,10 +398,19 @@ void code_contractst::replace_old_parameter(
     replace_old_parameter(op, parameter2history, location, mode, history);
   }
 
-  if(expr.id() == ID_old)
+  if(expr.id() == ID_old ||
+     expr.id() == ID_loop_entry)
   {
-    DATA_INVARIANT(
+    if (expr.id() == ID_old)
+    {
+      DATA_INVARIANT(
       expr.operands().size() == 1, CPROVER_PREFIX "old must have one operand");
+    }
+    if (expr.id() == ID_loop_entry)
+    {
+      DATA_INVARIANT(
+      expr.operands().size() == 1, CPROVER_PREFIX "loop_entry must have one operand");
+    }
 
     const auto &parameter = to_old_expr(expr).expression();
 
@@ -427,9 +447,18 @@ void code_contractst::replace_old_parameter(
     }
     else
     {
-      log.error() << CPROVER_PREFIX "old does not currently support "
+      if (expr.id() == ID_old)
+      {
+        log.error() << CPROVER_PREFIX "old does not currently support "
                   << parameter.id() << " expressions." << messaget::eom;
       throw 0;
+      }
+      if (expr.id() == ID_loop_entry)
+      {
+        log.error() << CPROVER_PREFIX "loop_entry does not currently support "
+                  << parameter.id() << " expressions." << messaget::eom;
+      throw 0;
+      }
     }
   }
 }

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)