Adds support for struct members in history variables

doc/cprover-manual/contracts-history-variables.md

@@ -13,8 +13,9 @@ _ensures_ clause.
 
 ### Parameters
 
-`__CPROVER_old` takes a single argument, which is the identifier corresponding to
-a parameter of the function. For now, only scalar or pointer types are supported.
+`__CPROVER_old` takes a single argument, which is the identifier
+corresponding to a parameter of the function. For now, only scalars,
+pointers, and struct members are supported.
 
 ### Semantics
 

regression/contracts/history-pointer-enforce-09/main.c

@@ -0,0 +1,23 @@
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int y;
+};
+
+void foo(struct pair *p) __CPROVER_assigns(p->y)
+  __CPROVER_ensures(p->y == __CPROVER_old(p->y) + 5)
+{
+  p->y = p->y + 5;
+}
+
+int main()
+{
+  struct pair *p = malloc(sizeof(*p));
+  p->x = 2;
+  p->y = 2;
+  foo(p);
+
+  return 0;
+}

regression/contracts/history-pointer-enforce-09/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[foo.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that history variables are supported for struct members.
+By using the --enforce-all-contracts flag, the post-condition (which contains
+the history variable) is asserted. In this case, this assertion should pass.

regression/contracts/history-pointer-enforce-10/main.c

@@ -0,0 +1,50 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int *y;
+};
+
+int z = 5;
+int w[10] = {0};
+
+void foo(struct pair *p) __CPROVER_assigns(*(p->y), z)
+  __CPROVER_ensures(*(p->y) == __CPROVER_old(*(p->y)) + __CPROVER_old(z))
+{
+  *(p->y) = *(p->y) + z;
+  z = 10;
+}
+
+void bar(struct pair *p) __CPROVER_assigns(p->y)
+  __CPROVER_ensures(p->y == __CPROVER_old(p->y) + 5)
+{
+  p->y = (p->y + 5);
+}
+
+void baz(struct pair p) __CPROVER_assigns(p)
+  __CPROVER_ensures(p == __CPROVER_old(p))
+{
+  struct pair pp = p;
+  struct pair empty = {0};
+  p = empty;
+  p = pp;
+}
+
+int main()
+{
+  struct pair *p = malloc(sizeof(*p));
+  p->y = malloc(sizeof(*(p->y)));
+  p->x = 2;
+  *(p->y) = 2;
+  foo(p);
+  assert(*(p->y) == 7);
+  p->y = w;
+  w[5] = -1;
+  bar(p);
+  assert(*(p->y) == -1);
+  baz(*p);
+
+  return 0;
+}

regression/contracts/history-pointer-enforce-10/test.desc

@@ -0,0 +1,23 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
+^\[bar.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
+^\[baz.\d+\] line \d+ Check that pp is assignable\: SUCCESS$
+^\[baz.\d+\] line \d+ Check that empty is assignable\: SUCCESS$
+^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$
+^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$
+^\[foo.\d+\] line \d+ Check that \*p\-\>y is assignable\: SUCCESS$
+^\[foo.\d+\] line \d+ Check that z is assignable\: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion \*\(p\-\>y\) == 7\: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion \*\(p\-\>y\) == -1\: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that history variables are supported for structs, symbols, and
+struct members. By using the --enforce-all-contracts flag, the postcondition
+(with history variable) is asserted. In this case, this assertion should pass.

regression/contracts/history-pointer-enforce-11/main.c

@@ -0,0 +1,23 @@
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int y;
+};
+
+void foo(struct pair *p) __CPROVER_assigns(p->y)
+  __CPROVER_ensures((p != NULL) == > (p->y == __CPROVER_old(p->y) + 5))
+    __CPROVER_ensures((p == NULL) == > (p->y == __CPROVER_old(p->y)))
+{
+  if(p != NULL)
+    p->y = p->y + 5;
+}
+
+int main()
+{
+  struct pair *p = NULL;
+  foo(p);
+
+  return 0;
+}

regression/contracts/history-pointer-enforce-11/test.desc

@@ -0,0 +1,13 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[postcondition.\d+\] Check ensures clause\: SUCCESS$
+^\[foo.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that history variables handle NULL pointers.
+History variables currently do not check for nullness while
+storing values of objects, which may lead to NULL pointer dereferences.

regression/contracts/history-pointer-replace-04/main.c

@@ -0,0 +1,24 @@
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int y;
+};
+
+void foo(struct pair *p) __CPROVER_requires(p != NULL) __CPROVER_assigns(p->y)
+  __CPROVER_ensures(p->y == __CPROVER_old(p->y) + 5)
+{
+  p->y = p->y + 5;
+}
+
+int main()
+{
+  struct pair *p = malloc(sizeof(*p));
+  p->x = 2;
+  p->y = 2;
+  foo(p);
+  assert(p->y != 7);
+
+  return 0;
+}

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

@@ -0,0 +1,14 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause\: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion p\-\>y \!\= 7\: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test checks that history variables are supported for struct members.
+By using the --replace-all-calls-with-contracts flag, the assertion in
+main should consider the ensures clause (with old value). In this case,
+this assertion should fail.

src/goto-instrument/contracts/contracts.cpp

@@ -394,23 +394,22 @@ void code_contractst::replace_old_parameter(
 
     const auto &parameter = to_old_expr(expr).expression();
 
-    // TODO: generalize below
-    if(parameter.id() == ID_dereference)
+    if(
+      parameter.id() == ID_dereference || parameter.id() == ID_member ||
+      parameter.id() == ID_symbol)
     {
-      const auto &dereference_expr = to_dereference_expr(parameter);
-
-      auto it = parameter2history.find(dereference_expr);
+      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(dereference_expr.type(), location, mode).symbol_expr();
+          new_tmp_symbol(parameter.type(), location, mode).symbol_expr();
 
         // 2. Associate the above temporary variable to it's corresponding
         // expression
-        parameter2history[dereference_expr] = tmp_symbol;
+        parameter2history[parameter] = tmp_symbol;
 
         // 3. Add the required instructions to the instructions list
         // 3.1 Declare the newly created temporary variable
@@ -419,11 +418,11 @@ void code_contractst::replace_old_parameter(
         // 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, dereference_expr, location));
+        history.add(
+          goto_programt::make_assignment(tmp_symbol, parameter, location));
       }
 
-      expr = parameter2history[dereference_expr];
+      expr = parameter2history[parameter];
     }
     else
     {