Merge pull request #7060 from padhi-aws-forks/history-vars-fix

CONTRACTS: Allow `ID_index` expressions in history variables

Author: SaswatPadhi

regression/contracts/history-index/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i, n, x[10];
+  __CPROVER_assume(x[0] == x[9]);
+  while(i < n)
+    __CPROVER_loop_invariant(x[0] == __CPROVER_loop_entry(x[0]))
+    {
+      x[0] = x[9] - 1;
+      x[0]++;
+    }
+  assert(x[0] == x[9]);
+}

regression/contracts/history-index/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^Tracking history of index expressions is not supported yet\.
+--
+This test checks that `ID_index` expressions are allowed within history variables.

regression/contracts/history-invalid/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int foo(int x)
+{
+  return x;
+}
+
+int main()
+{
+  int i, n, x[10];
+  __CPROVER_assume(x[0] == x[9]);
+  while(i < n)
+    __CPROVER_loop_invariant(x[0] == __CPROVER_loop_entry(foo(x[0])))
+    {
+      x[0] = x[9] - 1;
+      x[0]++;
+    }
+  assert(x[0] == x[9]);
+}

regression/contracts/history-invalid/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-loop-contracts
+^main.c.* error: Tracking history of side_effect expressions is not supported yet.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that expressions with side effect, such as function calls,
+may not be used in history variables.

src/ansi-c/c_typecheck_expr.cpp

@@ -2732,6 +2732,18 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    const auto &param_id = expr.arguments().front().id();
+    if(!(param_id == ID_dereference || param_id == ID_member ||
+         param_id == ID_symbol || param_id == ID_ptrmember ||
+         param_id == ID_constant || param_id == ID_typecast ||
+         param_id == ID_index))
+    {
+      error().source_location = f_op.source_location();
+      error() << "Tracking history of " << param_id
+              << " expressions is not supported yet." << eom;
+      throw 0;
+    }
+
     irep_idt id = identifier == CPROVER_PREFIX "old" ? ID_old : ID_loop_entry;
 
     history_exprt old_expr(expr.arguments()[0], id);

src/goto-instrument/contracts/contracts.cpp

@@ -664,7 +664,8 @@ void code_contractst::replace_history_parameter(
     const auto &id = parameter.id();
     if(
       id == ID_dereference || id == ID_member || id == ID_symbol ||
-      id == ID_ptrmember || id == ID_constant || id == ID_typecast)
+      id == ID_ptrmember || id == ID_constant || id == ID_typecast ||
+      id == ID_index)
     {
       auto it = parameter2history.find(parameter);