Adds support for pointer history variables in function contracts

This adds support for history variables in function contracts.
History variables are (1) declared and (2) assigned to the
value that their corresponding variable has at function call time.
Currently, only pointers are supported.

Author: ArenBabikian

src/ansi-c/c_typecheck_expr.cpp

@@ -2575,6 +2575,20 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(ok_expr);
   }
+  else if(identifier == CPROVER_PREFIX "old")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << identifier << " expects one operands" << eom;
+      throw 0;
+    }
+
+    old_exprt old_expr(ID_old, expr.arguments()[0]);
+    old_expr.add_source_location() = source_location;
+
+    return std::move(old_expr);
+  }
   else if(identifier==CPROVER_PREFIX "isinff" ||
           identifier==CPROVER_PREFIX "isinfd" ||
           identifier==CPROVER_PREFIX "isinfld" ||

src/ansi-c/cprover_builtin_headers.h

@@ -12,6 +12,7 @@ __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
 __CPROVER_bool __CPROVER_r_ok(const void *, __CPROVER_size_t);
 __CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t);
+void __CPROVER_old(const void *);
 
 // bitvector analysis
 __CPROVER_bool __CPROVER_get_flag(const void *, const char *);

src/ansi-c/library/cprover.h

@@ -35,6 +35,7 @@ __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
 __CPROVER_bool __CPROVER_r_ok(const void *, __CPROVER_size_t);
 __CPROVER_bool __CPROVER_w_ok(const void *, __CPROVER_size_t);
+void __CPROVER_old(const void *);
 
 #if 0
 __CPROVER_bool __CPROVER_equal();

src/goto-instrument/code_contracts.cpp

@@ -21,6 +21,9 @@ Date: February 2016
 
 #include <linking/static_lifetime_init.h>
 
+#include <fstream>
+#include <iostream>
+#include <map>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_util.h>
@@ -234,6 +237,121 @@ void code_contractst::add_quantified_variable(
   }
 }
 
+optionalt<exprt> code_contractst::replace_old_parameter(
+  exprt expr,
+  std::map<exprt, exprt> &parameter2ghost,
+  source_locationt location,
+  const irep_idt &function,
+  const irep_idt &mode,
+  std::list<goto_programt::instructiont> &instructions)
+{
+  bool modified = false;
+
+  for(auto &op : expr.operands())
+  {
+    auto op_result = replace_old_parameter(
+      op, parameter2ghost, location, function, mode, instructions);
+    if(op_result.has_value())
+    {
+      op = *op_result;
+      modified = true;
+    }
+  }
+
+  if(expr.id() == ID_old)
+  {
+    DATA_INVARIANT(expr.operands().size() == 1, "old must have one operands");
+
+    const auto &parameter = to_old_expr(expr).variable();
+
+    // TODO: generalize below
+    PRECONDITION(parameter.id() == ID_dereference);
+
+    exprt ret;
+    if(parameter.id() == ID_dereference)
+    {
+      const auto &dereference_expr = to_dereference_expr(parameter);
+      const auto &cur_pointer = dereference_expr.pointer();
+
+      std::map<exprt, exprt>::iterator it = parameter2ghost.find(cur_pointer);
+
+      if(it == parameter2ghost.end())
+      {
+        // 1. Create a temporary symbol expression that represents the
+        // history variable
+        symbol_exprt tmp_symbol =
+          new_tmp_symbol(cur_pointer.type(), location, function, mode)
+            .symbol_expr();
+
+        // 2. Associate the above temporary variable to it's corresponding
+        // expression
+        parameter2ghost[cur_pointer] = tmp_symbol;
+
+        // 3. Add the required instructions to the instructions list
+        // 3.1 Declare the newly created temporary variable
+        instructions.push_back(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
+        instructions.push_back(goto_programt::make_assignment(
+          dereference_exprt(tmp_symbol),
+          dereference_exprt(cur_pointer),
+          location));
+      }
+
+      ret = dereference_exprt(parameter2ghost[cur_pointer]);
+    }
+
+    return ret;
+  }
+  else if(modified)
+    return std::move(expr);
+  else
+    return {};
+}
+
+std::pair<goto_programt::instructiont, std::list<goto_programt::instructiont>>
+code_contractst::create_ensures_instruction(
+  exprt expression,
+  source_locationt location,
+  const irep_idt &function,
+  const irep_idt &mode,
+  bool isEnforces)
+{
+  std::map<exprt, exprt> parameter2ghost;
+  std::list<goto_programt::instructiont> instructions;
+
+  // Create instruction corresponding to the ensures clause
+  goto_programt::instructiont instruction;
+  if(isEnforces)
+    instruction = goto_programt::make_assertion(expression, location);
+  else
+    instruction = goto_programt::make_assumption(expression, location);
+
+  // Find and replace "old" expression in the above instruction
+  if(has_subexpr(instruction.get_condition(), [](const exprt &expr) {
+       return expr.id() == ID_old;
+     }))
+  {
+    auto old_cond = replace_old_parameter(
+      instruction.get_condition(),
+      parameter2ghost,
+      location,
+      function,
+      mode,
+      instructions);
+    if(old_cond.has_value())
+    {
+      instruction.set_condition(*old_cond);
+    }
+  }
+
+  // return a pair containing:
+  // 1. the instruction corresponding to the ensures clause
+  // 2. instructions related to initializing the history variables
+  return std::make_pair(instruction, instructions);
+}
+
 bool code_contractst::apply_function_contract(
   const irep_idt &function_id,
   goto_programt &goto_program,
@@ -301,7 +419,7 @@ bool code_contractst::apply_function_contract(
   }
 
   // Replace formal parameters
-  code_function_callt::argumentst::const_iterator a_it=
+  code_function_callt::argumentst::const_iterator a_it =
     call.arguments().begin();
   for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
       p_it != type.parameters().end() && a_it != call.arguments().end();
@@ -353,7 +471,25 @@ bool code_contractst::apply_function_contract(
   // function call with a SKIP statement.
   if(ensures.is_not_nil())
   {
-    *target = goto_programt::make_assumption(ensures, target->source_location);
+    // get all the relevant instructions related to history variables
+    std::
+      pair<goto_programt::instructiont, std::list<goto_programt::instructiont>>
+        ensures_pair = create_ensures_instruction(
+          ensures,
+          ensures.source_location(),
+          function,
+          function_symbol.mode,
+          false);
+
+    // add all the history variable initializations
+    std::list<goto_programt::instructiont>::iterator it;
+    for(it = ensures_pair.second.begin(); it != ensures_pair.second.end(); ++it)
+    {
+      goto_program.insert_before(target, std::move(*it));
+    }
+
+    // add the ensures instructions
+    *target = std::move(ensures_pair.first);
   }
   else
   {
@@ -793,6 +929,7 @@ void code_contractst::add_contract_check(
   // if(nondet)
   //   decl ret
   //   decl parameter1 ...
+  //   decl ghost_parameter1 ... [optional]
   //   assume(requires)  [optional]
   //   ret=function(parameter1, ...)
   //   assert(ensures)
@@ -821,7 +958,7 @@ void code_contractst::add_contract_check(
                        .symbol_expr();
     check.add(goto_programt::make_decl(r, skip->source_location));
 
-    call.lhs()=r;
+    call.lhs() = r;
     return_stmt = code_returnt(r);
 
     symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
@@ -860,6 +997,32 @@ void code_contractst::add_contract_check(
   code_contractst::add_quantified_variable(
     requires, replace, function_symbol.mode);
 
+  // rewrite any use of __CPROVER_return_value
+  exprt ensures_cond = ensures;
+  replace(ensures_cond);
+
+  // Prepare the history variables handling
+  std::pair<goto_programt::instructiont, std::list<goto_programt::instructiont>>
+    ensures_pair;
+
+  if(ensures.is_not_nil())
+  {
+    // get all the relevant instructions related to history variables
+    ensures_pair = create_ensures_instruction(
+      ensures_cond,
+      ensures.source_location(),
+      wrapper_fun,
+      function_symbol.mode,
+      true);
+
+    // add all the history variable initializations
+    std::list<goto_programt::instructiont>::iterator it;
+    for(it = ensures_pair.second.begin(); it != ensures_pair.second.end(); ++it)
+    {
+      check.add(std::move(*it));
+    }
+  }
+
   // assume(requires)
   if(requires.is_not_nil())
   {
@@ -874,15 +1037,10 @@ void code_contractst::add_contract_check(
   // ret=mangled_fun(parameter1, ...)
   check.add(goto_programt::make_function_call(call, skip->source_location));
 
-  // rewrite any use of __CPROVER_return_value
-  exprt ensures_cond = ensures;
-  replace(ensures_cond);
-
   // assert(ensures)
   if(ensures.is_not_nil())
   {
-    check.add(
-      goto_programt::make_assertion(ensures_cond, ensures.source_location()));
+    check.add(std::move(ensures_pair.first));
   }
 
   if(code_type.return_type() != empty_typet())

src/goto-instrument/code_contracts.h

@@ -14,6 +14,7 @@ Date: February 2016
 #ifndef CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
 #define CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
 
+#include <map>
 #include <set>
 #include <string>
 #include <unordered_set>
@@ -175,6 +176,27 @@ class code_contractst
     exprt expression,
     replace_symbolt &replace,
     irep_idt mode);
+
+  /// This function recursively identifies the "old" expressions within expr
+  /// and replaces them with correspoding history variables.
+  optionalt<exprt> replace_old_parameter(
+    exprt expr,
+    std::map<exprt, exprt> &parameter2ghost,
+    source_locationt location,
+    const irep_idt &function,
+    const irep_idt &mode,
+    std::list<goto_programt::instructiont> &instructions);
+
+  /// This function creates and returns an instruction that corresponds to the
+  /// ensures clause. It also returns a list of instructions related to
+  /// initializing history variables, if required.
+  std::pair<goto_programt::instructiont, std::list<goto_programt::instructiont>>
+  create_ensures_instruction(
+    exprt expression,
+    source_locationt location,
+    const irep_idt &function,
+    const irep_idt &mode,
+    bool isEnforces);
 };
 
 #define FLAG_REPLACE_CALL "replace-call-with-contract"

src/util/irep_ids.def

@@ -684,6 +684,7 @@ IREP_ID_TWO(C_qualifier, #qualifier)
 IREP_ID_TWO(C_array_ini, #array_ini)
 IREP_ID_ONE(r_ok)
 IREP_ID_ONE(w_ok)
+IREP_ID_ONE(old)
 IREP_ID_ONE(super_class)
 IREP_ID_ONE(exceptions_thrown_list)
 IREP_ID_TWO(C_java_method_type, #java_method_type)

src/util/pointer_expr.h

@@ -462,6 +462,30 @@ class null_pointer_exprt : public constant_exprt
   }
 };
 
+/// \brief A base class for a predicate that indicates the pre-function-call
+/// value of a variable passed as a parameter to a function
+class old_exprt : public unary_predicate_exprt
+{
+public:
+  explicit old_exprt(irep_idt id, exprt variable)
+    : unary_predicate_exprt(id, std::move(variable))
+  {
+  }
+
+  const exprt &variable() const
+  {
+    return op0();
+  }
+};
+
+inline const old_exprt &to_old_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_old);
+  auto &ret = static_cast<const old_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 /// \brief A base class for a predicate that indicates that an
 /// address range is ok to read or write
 class r_or_w_ok_exprt : public binary_predicate_exprt