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

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)
     {

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

@@ -174,6 +174,17 @@ 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" variable
+  replace_old_parameter(invariant, parameter2history, loop_head->source_location, mode, history);
+
+  // Create 'loop_entry' history variables
+  insert_before_swap_and_advance(havoc_code, 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,11 @@ 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(
-      expr.operands().size() == 1, CPROVER_PREFIX "old must have one operand");
+      expr.operands().size() == 1, "history variable must have one operand");
 
     const auto &parameter = to_old_expr(expr).expression();
 
@@ -427,7 +439,7 @@ void code_contractst::replace_old_parameter(
     }
     else
     {
-      log.error() << CPROVER_PREFIX "old does not currently support "
+      log.error() << "history variables do 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)