Adds support for pointer ghost variables in function contracts

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

Author: ArenBabikian

regression/contracts/ghost-pointer-enforce-01/main.c

@@ -0,0 +1,12 @@
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_ensures(*x == *x_ + 5)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

regression/contracts/ghost-pointer-enforce-01/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks that ghost variables are supported for variables that are
+being assigned by the function under test. By using the
+--enforce-all-contracts flag, the post-condition (which contains the ghost
+vriable) is asserted. In this case, this assertion should pass.

regression/contracts/ghost-pointer-enforce-02/main.c

@@ -0,0 +1,12 @@
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_ensures(*x < *x_ + 5)
+{
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

regression/contracts/ghost-pointer-enforce-02/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+This test checks that ghost variables are supported for variables that are
+being assigned by the function under test. By using the
+--enforce-all-contracts flag, the post-condition (which contains the ghost
+vriable) is asserted. In this case, this assertion should fail.

regression/contracts/ghost-pointer-enforce-04/main.c

@@ -0,0 +1,15 @@
+void foo(int *x, int *y) __CPROVER_assigns(*x, *y)
+  __CPROVER_ensures(*x == *y_ + 1 && *y == *x_ + 2)
+{
+  int x_initial = *x;
+  *x = *y + 1;
+  *y = x_initial + 2;
+}
+
+int main()
+{
+  int x, y;
+  foo(&x, &y);
+
+  return 0;
+}

regression/contracts/ghost-pointer-enforce-04/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks that ghost variables are supported in the case where multiple
+variables are being assgned by the function under test. By using the
+--enforce-all-contracts flag, the post-condition (which contains the ghost
+variable) is asserted. In this case, this assertion should pass.

regression/contracts/ghost-pointer-enforce-05/main.c

@@ -0,0 +1,14 @@
+void foo(int *x, int *y) __CPROVER_assigns(*x, *y)
+  __CPROVER_ensures(*x == *x_ + 2 || *y == *y_ + 3)
+{
+  *x = *x + 1;
+  *y = *y + 2;
+}
+
+int main()
+{
+  int x, y;
+  foo(&x, &y);
+
+  return 0;
+}

regression/contracts/ghost-pointer-enforce-05/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+This test checks that ghost variables are supported in the case where multiple
+variables are being assgned by the function under test. By using the
+--enforce-all-contracts flag, the post-condition (which contains the ghost
+variable) is asserted. In this case, this assertion should fail.

regression/contracts/ghost-pointer-enforce-06/main.c

@@ -0,0 +1,14 @@
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x != 3)
+  __CPROVER_ensures(*x == *x_ + 5 && *x != 8)
+{
+  int *x_ = 3;
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

regression/contracts/ghost-pointer-enforce-06/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks ensures that the declaration of a new variable (in the
+function-under-test) with the same name as the ghost variable does not
+interfere with the ghost variable handling. For this test, we use the
+--enforce-all-contracts flag. As a result, the post-condition is asserted,
+and is expected to pass.

regression/contracts/ghost-pointer-enforce-07/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_ensures(*x == *x_ + 5)
+{
+  assert(*x_ == *x);
+  *x = *x + 5;
+}
+
+int main()
+{
+  int n;
+  foo(&n);
+
+  return 0;
+}

regression/contracts/ghost-pointer-enforce-07/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=1$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+--
+Verification:
+This test checks that ghost variables are not supported when referred to from
+a function body. In such a case, the program should not parse and there
+should be a conversion error.

regression/contracts/ghost-pointer-replace-01/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x > 0)
+  __CPROVER_ensures(*x == *x_ + 2)
+{
+  *x = *x + 2;
+}
+
+int main()
+{
+  int n;
+  __CPROVER_assume(n > 0 && n < __INT_MAX__ - 2);
+  foo(&n);
+
+  assert(n > 2);
+
+  return 0;
+}

regression/contracts/ghost-pointer-replace-01/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks that ghost variables are supported with the use of the
+--replace-all-calls-with-contracts flag. In this case, the post-condition
+(which contains the ghost variable) becomes an assumption. We then manually
+assert this assumption. For this test, the assertion should succeed.

regression/contracts/ghost-pointer-replace-02/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x == 0)
+  __CPROVER_ensures(*x > *x_ + 2)
+{
+  *x = *x + 2;
+}
+
+int main()
+{
+  int n = 0;
+  foo(&n);
+
+  assert(n > 2);
+
+  return 0;
+}

regression/contracts/ghost-pointer-replace-02/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test checks that ghost variables are supported with the use of the
+--replace-all-calls-with-contracts flag. In this case, the post-condition
+(which contains the ghost variable) becomes an assumption. We then manually
+assert this assumption. For this test, the assertion should succeed.

regression/contracts/ghost-pointer-replace-03/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+void foo(int *x) __CPROVER_assigns(*x) __CPROVER_requires(*x != *x_)
+  __CPROVER_ensures(*x == *x_ + 2)
+{
+  *x = *x + 2;
+}
+
+int main()
+{
+  int n = 0;
+  foo(&n);
+
+  assert(n == 2);
+
+  return 0;
+}

regression/contracts/ghost-pointer-replace-03/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+This test checks that ghost variables may be used as part of the
+pre-condition contract, while keeping their usual semantic meaning.
+For this test, we use the --replace-all-calls-with-contracts flag, which
+asserts the pre-condition. In this case, the assertion is expected to fail.

src/ansi-c/ansi_c_parser.cpp

@@ -142,6 +142,24 @@ void ansi_c_parsert::add_declarator(
              current_scope().prefix+id2string(base_name);
     new_declarator.set_name(prefixed_name);
 
+    // For every parameter...
+    if(is_parameter)
+    {
+      // 1. create a new identifier that corresponds to the ghost variable.
+      ansi_c_identifiert ghost_identifier = scope.name_map[base_name];
+      ghost_identifier.id_class = id_class;
+
+      irep_idt ghost_prefixed_name =
+        current_scope().prefix + id2string(base_name) + "_";
+      ghost_identifier.prefixed_name = ghost_prefixed_name;
+
+      // 2. Add the new ghost variable identifier to the name map
+      // Note that the "ghost_base_name" irep corresponds to the
+      // ghost variable syntax.
+      irep_idt ghost_base_name = id2string(base_name) + "_";
+      scope.name_map[ghost_base_name] = ghost_identifier;
+    }
+
     // add to scope
     ansi_c_identifiert &identifier=scope.name_map[base_name];
     identifier.id_class=id_class;

src/ansi-c/c_typecheck_base.cpp

@@ -540,6 +540,23 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
 
     symbolt *new_p_symbol;
     move_symbol(p_symbol, new_p_symbol);
+
+    // Handling ghost variables...
+
+    // 1. Produce a symbol for the ghost variable corresponding to the
+    // parameter.
+    irep_idt identifier_ghost =
+      id2string(symbol.name) + "::" + id2string(base_name) + "_";
+
+    parameter_symbolt p_symbol_ghost;
+    p_symbol_ghost.type = p.type();
+    p_symbol_ghost.name = identifier_ghost;
+    p_symbol_ghost.base_name = base_name;
+    p_symbol_ghost.location = p.source_location();
+
+    // 2. Add the ghost variable symbol to the symbol table.
+    symbolt *new_p_symbol_ghost;
+    move_symbol(p_symbol_ghost, new_p_symbol_ghost);
   }
 
   // typecheck the body code