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,12 @@
+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 pointer objects are supported for
+loop_entry history variable. 

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,9 @@
+CORE
+main.c
+--apply-loop-contracts
+^CONVERSION ERROR$
+^EXIT=1$
+^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 @@
+oid foo(int *x) __CPROVER_assigns(*x)
+  __CPROVER_ensures(*x == __CPROVER_old(*x) + 5)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

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

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^PARSING ERROR$
+^EXIT=1$
+^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,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-04/test.desc

@@ -0,0 +1,12 @@
+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 struct objects are supported for
+loop_entry history variable. 

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

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+typedef struct
+{
+  int *n;
+} s;
+
+void main()
+{
+  int y;
+
+  s *s1, *s2;
+  s2->n = malloc(sizeof(int));
+  s1->n = s2->n;
+
+  while(y > 0)
+    __CPROVER_loop_invariant(*s1 == __CPROVER_loop_entry(*s1))
+    {
+      --y;
+      s1->n = s1->n + 1;
+      s1->n = s1->n - 1;
+    }
+
+  assert(s1->n == s2->n);
+}

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

@@ -0,0 +1,12 @@
+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 struct objects are supported for
+loop_entry history variable. 

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

@@ -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

@@ -146,6 +146,7 @@ class c_typecheck_baset:
   virtual void typecheck_start_thread(codet &code);
   virtual void typecheck_spec_loop_invariant(codet &code);
   virtual void typecheck_spec_decreases(codet &code);
+  virtual void disallow_function_history_variables(const exprt &expr) const;
 
   bool break_is_allowed;
   bool continue_is_allowed;
@@ -207,6 +208,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_code.cpp

@@ -820,6 +820,7 @@ void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
     {
       typecheck_expr(invariant);
       implicit_typecast_bool(invariant);
+      disallow_function_history_variables(invariant);
     }
   }
 }
@@ -836,3 +837,21 @@ void c_typecheck_baset::typecheck_spec_decreases(codet &code)
     }
   }
 }
+
+void c_typecheck_baset::disallow_function_history_variables(
+  const exprt &expr) const
+{
+  for(auto &op : expr.operands())
+  {
+    disallow_function_history_variables(op);
+  }
+
+  if(expr.id() == ID_old)
+  {
+    error().source_location = expr.source_location();
+    error() << CPROVER_PREFIX
+      "old expressions are not allowed in " CPROVER_PREFIX "invariant clauses"
+            << eom;
+    throw 0;
+  }
+}

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);
@@ -3973,3 +3987,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,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" expression.
+  replace_loop_entry_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.
@@ -392,7 +404,7 @@ void code_contractst::replace_old_parameter(
     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_old).expression();
 
     if(
       parameter.id() == ID_dereference || parameter.id() == ID_member ||
@@ -433,6 +445,66 @@ void code_contractst::replace_old_parameter(
   }
 }
 
+void code_contractst::replace_loop_entry_parameter(
+  exprt &expr,
+  std::map<exprt, exprt> &parameter2history,
+  source_locationt location,
+  const irep_idt &mode,
+  goto_programt &history)
+{
+  for(auto &op : expr.operands())
+  {
+    replace_loop_entry_parameter(
+      op, parameter2history, location, mode, history);
+  }
+
+  if(expr.id() == ID_loop_entry)
+  {
+    DATA_INVARIANT(
+      expr.operands().size() == 1,
+      CPROVER_PREFIX "loop_entry must have one operand");
+
+    const auto &parameter = to_history_expr(expr, ID_loop_entry).expression();
+
+    if(
+      parameter.id() == ID_dereference || parameter.id() == ID_member ||
+      parameter.id() == ID_symbol || parameter.id() == ID_ptrmember)
+    {
+      auto it = parameter2history.find(parameter);
+
+      if(it == parameter2history.end())
+      {
+        // 1. Create a temporary symbol expression that represents the
+        // history variable
+        symbol_exprt tmp_symbol =
+          new_tmp_symbol(parameter.type(), location, mode).symbol_expr();
+
+        // 2. Associate the above temporary variable to it's corresponding
+        // expression
+        parameter2history[parameter] = tmp_symbol;
+
+        // 3. Add the required instructions to the instructions list
+        // 3.1 Declare the newly created temporary variable
+        history.add(goto_programt::make_decl(tmp_symbol, location));
+
+        // 3.2 Add an assignment such that the value pointed to by the new
+        // temporary variable is equal to the value of the corresponding
+        // parameter
+        history.add(
+          goto_programt::make_assignment(tmp_symbol, parameter, location));
+      }
+
+      expr = parameter2history[parameter];
+    }
+    else
+    {
+      log.error() << CPROVER_PREFIX "loop_entry does not currently support "
+                  << parameter.id() << " expressions." << messaget::eom;
+      throw 0;
+    }
+  }
+}
+
 std::pair<goto_programt, goto_programt>
 code_contractst::create_ensures_instruction(
   codet &expression,