CONTRACTS: store contracts in dedicated symbols

Contracts can now be placed on declarations or definitions, and result
in a fresh symbol being generated. That new symbol has its name prefixed
with "contracts::" to place them in a pseudo-namespace, and has
"is_property" set (which was an otherwise unused symbolt flag).

Co-authored-by: Remi Delmas <[email protected]>

Author: tautschnig

regression/contracts/named-contracts/main-contract-after-declaration.c

@@ -0,0 +1,28 @@
+int foo(int *arr, int size);
+
+int foo(int *arr, int size)
+  // clang-format off
+__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(
+  arr[0], arr[size-1];
+  size >= 10: arr[5];
+)
+__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0)
+__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value)
+  // clang-format on
+  ;
+
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/contracts/named-contracts/main-contract-after-definition.c

@@ -0,0 +1,26 @@
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  return size < 10 ? 0 : arr[5];
+}
+
+int foo(int *arr, int size)
+  // clang-format off
+__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(
+  arr[0], arr[size-1];
+  size >= 10: arr[5];
+)
+__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0)
+__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value)
+  // clang-format on
+  ;
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/contracts/named-contracts/main-definition-after-contract.c

@@ -0,0 +1,26 @@
+int foo(int *arr, int size)
+  // clang-format off
+__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(
+  arr[0], arr[size-1];
+  size >= 10: arr[5];
+)
+__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0)
+__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value)
+  // clang-format on
+  ;
+
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/contracts/named-contracts/main-no-definition.c

@@ -0,0 +1,28 @@
+int foo(int *arr, int size)
+  // clang-format off
+__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(
+  arr[0], arr[size-1];
+  size >= 10: arr[5];
+)
+__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0)
+__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value)
+  // clang-format on
+  ;
+
+int main()
+{
+  int arr[10] = {10, 9, 8, 7, 6, 5, 4, 3, 2, 1};
+  int retval = foo(arr, 10);
+  assert(arr[0] == 0);
+  assert(arr[1] == 9);
+  assert(arr[2] == 8);
+  assert(arr[3] == 7);
+  assert(arr[4] == 6);
+  assert(arr[5] == retval);
+  assert(arr[6] == 4);
+  assert(arr[7] == 3);
+  assert(arr[8] == 2);
+  assert(arr[9] == 0);
+  return 0;
+}

regression/contracts/named-contracts/test-contract-after-declaration.desc

@@ -0,0 +1,10 @@
+CORE
+main-contract-after-declaration.c
+--replace-call-with-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can have a function declaration with a contract after
+having seen an earlier declaration of that same function.

regression/contracts/named-contracts/test-contract-after-definition.desc

@@ -0,0 +1,10 @@
+CORE
+main-contract-after-definition.c
+--replace-call-with-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can have a function declaration with a contract after
+having seen that function's definition.

regression/contracts/named-contracts/test-definition-after-contract.desc

@@ -0,0 +1,11 @@
+CORE
+main-definition-after-contract.c
+--replace-call-with-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can have a function declaration with a contract and
+without body, then the function definition, and successfully replace a call to
+the function by the contract.

regression/contracts/named-contracts/test-no-definition.desc

@@ -0,0 +1,10 @@
+CORE
+main-no-definition.c
+--replace-call-with-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can have a function declaration with a contract and
+without body and replace a call to the function by the contract.

src/ansi-c/c_typecheck_base.cpp

@@ -153,7 +153,9 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
     {
       typecheck_function_body(symbol);
     }
-    else
+    else if(
+      symbol.is_macro ||
+      !to_code_with_contract_type(symbol.type).has_contract())
     {
       // we don't need the identifiers
       for(auto &parameter : to_code_type(symbol.type).parameters())
@@ -335,7 +337,15 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
     if(old_ct.has_ellipsis() && !new_ct.has_ellipsis())
       old_ct=new_ct;
     else if(!old_ct.has_ellipsis() && new_ct.has_ellipsis())
+    {
+      if(to_code_with_contract_type(new_ct).has_contract())
+      {
+        error().source_location = new_symbol.location;
+        error() << "code contract on incomplete function re-declaration" << eom;
+        throw 0;
+      }
       new_ct=old_ct;
+    }
 
     if(inlined)
     {
@@ -408,6 +418,22 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
       // overwrite type (because of parameter names)
       old_symbol.type=new_symbol.type;
     }
+    else if(to_code_with_contract_type(new_ct).has_contract())
+    {
+      // overwrite type to add contract, but keep the old parameter identifiers
+      // (if any)
+      auto new_parameters_it = new_ct.parameters().begin();
+      for(auto &p : old_ct.parameters())
+      {
+        if(new_parameters_it != new_ct.parameters().end())
+        {
+          new_parameters_it->set_identifier(p.get_identifier());
+          ++new_parameters_it;
+        }
+      }
+
+      old_symbol.type = new_symbol.type;
+    }
 
     return;
   }
@@ -710,12 +736,44 @@ void c_typecheck_baset::typecheck_declaration(
 
       // check the contract, if any
       symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
-      if(new_symbol.type.id() == ID_code)
+      if(
+        new_symbol.type.id() == ID_code &&
+        to_code_with_contract_type(new_symbol.type).has_contract())
       {
-        // We typecheck this after the
-        // function body done above, so as to have parameter symbols
-        // available
-        auto &code_type = to_code_with_contract_type(new_symbol.type);
+        code_with_contract_typet code_type =
+          to_code_with_contract_type(new_symbol.type);
+
+        // ensure parameter declarations are in the symbol table
+        std::vector<irep_idt> temporary_parameter_symbols;
+        for(auto &p : code_type.parameters())
+        {
+          if(p.get_base_name().empty())
+            continue;
+
+          // produce identifier
+          irep_idt base_name = p.get_base_name();
+          irep_idt parameter_identifier =
+            id2string(identifier) + "::" + id2string(base_name);
+
+          p.set_identifier(parameter_identifier);
+
+          if(
+            symbol_table.symbols.find(parameter_identifier) ==
+            symbol_table.symbols.end())
+          {
+            parameter_symbolt p_symbol;
+
+            p_symbol.type = p.type();
+            p_symbol.name = parameter_identifier;
+            p_symbol.base_name = base_name;
+            p_symbol.location = p.source_location();
+
+            symbolt *new_p_symbol;
+            move_symbol(p_symbol, new_p_symbol);
+
+            temporary_parameter_symbols.push_back(parameter_identifier);
+          }
+        }
 
         for(auto &expr : code_type.requires_contract())
         {
@@ -745,21 +803,52 @@ void c_typecheck_baset::typecheck_declaration(
             CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
         }
 
-        if(!as_const(code_type).ensures().empty())
+        for(auto &ensures : code_type.ensures())
         {
-          for(auto &ensures : code_type.ensures())
-          {
-            typecheck_expr(ensures);
-            implicit_typecast_bool(ensures);
-            disallow_subexpr_by_id(
-              ensures,
-              ID_loop_entry,
-              CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
-          }
+          typecheck_expr(ensures);
+          implicit_typecast_bool(ensures);
+          disallow_subexpr_by_id(
+            ensures,
+            ID_loop_entry,
+            CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
         }
 
         if(return_type.id() != ID_empty)
           parameter_map.erase(CPROVER_PREFIX "return_value");
+
+        // create a contract symbol
+        symbolt contract;
+        contract.name = "contract::" + id2string(new_symbol.name);
+        contract.base_name = new_symbol.name;
+        contract.pretty_name = new_symbol.name;
+        contract.is_property = true;
+        contract.type = code_type;
+        contract.mode = new_symbol.mode;
+        contract.module = module;
+        contract.location = new_symbol.location;
+
+        auto entry = symbol_table.insert(std::move(contract));
+        if(!entry.second)
+        {
+          error().source_location = new_symbol.location;
+          error() << "contract '" << new_symbol.display_name()
+                  << "' already set at " << entry.first.location.as_string()
+                  << eom;
+          throw 0;
+        }
+
+        // Remove the contract from the original symbol as we have created a
+        // dedicated contract symbol.
+        new_symbol.type.remove(ID_C_spec_assigns);
+        new_symbol.type.remove(ID_C_spec_ensures);
+        new_symbol.type.remove(ID_C_spec_ensures_contract);
+        new_symbol.type.remove(ID_C_spec_requires);
+        new_symbol.type.remove(ID_C_spec_requires_contract);
+
+        // remove parameter declarations if those were only added for type
+        // checking the contract
+        for(const auto &parameter_id : temporary_parameter_symbols)
+          symbol_table.remove(parameter_id);
       }
     }
   }