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-definition.c

@@ -0,0 +1,25 @@
+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);
+  return 0;
+}

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

@@ -0,0 +1,25 @@
+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);
+  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-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,6 +153,12 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
     {
       typecheck_function_body(symbol);
     }
+    else if(
+      !symbol.is_macro &&
+      to_code_with_contract_type(symbol.type).has_contract())
+    {
+      add_parameters_to_symbol_table(symbol);
+    }
     else
     {
       // we don't need the identifiers
@@ -335,7 +341,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)
     {
@@ -710,12 +724,14 @@ 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);
+        // We typecheck this after the function body done above, so as to have
+        // parameter symbols available.
+        code_with_contract_typet code_type =
+          to_code_with_contract_type(new_symbol.type);
 
         for(auto &expr : code_type.requires_contract())
         {
@@ -745,21 +761,62 @@ 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
+        if(new_symbol.value.is_nil())
+        {
+          for(const auto &parameter : code_type.parameters())
+          {
+            const irep_idt &identifier = parameter.get_identifier();
+
+            symbol_tablet::symbolst::const_iterator p_s_it =
+              symbol_table.symbols.find(identifier);
+            if(p_s_it != symbol_table.symbols.end())
+              symbol_table.erase(p_s_it);
+          }
+        }
       }
     }
   }

src/goto-instrument/contracts/contracts.cpp

@@ -733,6 +733,29 @@ code_contractst::create_ensures_instruction(
   return std::make_pair(std::move(ensures_program), std::move(history));
 }
 
+static const code_with_contract_typet &
+get_contract(const irep_idt &function, const namespacet &ns)
+{
+  const std::string function_str = id2string(function);
+  const symbolt &function_symbol = ns.lookup(function);
+
+  const symbolt *contract_sym;
+  if(ns.lookup("contract::" + function_str, contract_sym))
+  {
+    // no contract provided in the source or just an empty assigns clause
+    return to_code_with_contract_type(function_symbol.type);
+  }
+
+  const auto &type = to_code_with_contract_type(contract_sym->type);
+  if(type != function_symbol.type)
+  {
+    throw invalid_input_exceptiont(
+      "Contract of '" + function_str + "' has different signature.");
+  }
+
+  return type;
+}
+
 void code_contractst::apply_function_contract(
   const irep_idt &function,
   const source_locationt &location,
@@ -745,14 +768,13 @@ void code_contractst::apply_function_contract(
   // function pointers.
   PRECONDITION(const_target->call_function().id() == ID_symbol);
 
-  // Retrieve the function type, which is needed to extract the contract
-  // components.
   const irep_idt &target_function =
     to_symbol_expr(const_target->call_function()).get_identifier();
   const symbolt &function_symbol = ns.lookup(target_function);
-  const auto &type = to_code_with_contract_type(function_symbol.type);
+  const code_typet &function_type = to_code_type(function_symbol.type);
 
   // Isolate each component of the contract.
+  const auto &type = get_contract(target_function, ns);
   auto assigns_clause = type.assigns();
   auto requires = conjunction(type.requires());
   auto ensures = conjunction(type.ensures());
@@ -770,7 +792,7 @@ void code_contractst::apply_function_contract(
   // if true, the call return variable variable was created during replacement
   bool call_ret_is_fresh_var = false;
 
-  if(type.return_type() != empty_typet())
+  if(function_type.return_type() != empty_typet())
   {
     // Check whether the function's return value is not disregarded.
     if(target->call_lhs().is_not_nil())
@@ -797,14 +819,15 @@ void code_contractst::apply_function_contract(
         // fresh variable to replace __CPROVER_return_value with.
         call_ret_is_fresh_var = true;
         const symbolt &fresh = get_fresh_aux_symbol(
-          type.return_type(),
+          function_type.return_type(),
           id2string(target_function),
           "ignored_return_value",
           const_target->source_location(),
           symbol_table.lookup_ref(target_function).mode,
           ns,
           symbol_table);
-        symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type());
+        symbol_exprt ret_val(
+          CPROVER_PREFIX "return_value", function_type.return_type());
         auto fresh_sym_expr = fresh.symbol_expr();
         common_replace.insert(ret_val, fresh_sym_expr);
         call_ret_opt = fresh_sym_expr;
@@ -1234,11 +1257,6 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function)
   const auto &goto_function = function_obj->second;
   auto &function_body = function_obj->second.body;
 
-  // Get assigns clause for function
-  const symbolt &function_symbol = ns.lookup(function);
-  const auto &function_with_contract =
-    to_code_with_contract_type(function_symbol.type);
-
   instrument_spec_assignst instrument_spec_assigns(
     function, goto_functions, symbol_table, log.get_message_handler());
 
@@ -1282,8 +1300,8 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function)
   insert_before_swap_and_advance(
     function_body, instruction_it, snapshot_static_locals);
 
-  // Track targets mentionned in the specification
-  for(auto &target : function_with_contract.assigns())
+  // Track targets mentioned in the specification
+  for(auto &target : get_contract(function, ns).assigns())
   {
     goto_programt payload;
     instrument_spec_assigns.track_spec_target(target, payload);
@@ -1292,6 +1310,7 @@ void code_contractst::check_frame_conditions_function(const irep_idt &function)
 
   // Track formal parameters
   goto_programt snapshot_function_parameters;
+  const symbolt &function_symbol = ns.lookup(function);
   for(const auto &param : to_code_type(function_symbol.type).parameters())
   {
     goto_programt payload;
@@ -1419,9 +1438,7 @@ void code_contractst::add_contract_check(
 {
   PRECONDITION(!dest.instructions.empty());
 
-  const symbolt &function_symbol = ns.lookup(mangled_function);
-  const auto &code_type = to_code_with_contract_type(function_symbol.type);
-
+  const auto &code_type = get_contract(wrapper_function, ns);
   auto assigns = code_type.assigns();
   auto requires = conjunction(code_type.requires());
   auto ensures = conjunction(code_type.ensures());
@@ -1445,6 +1462,7 @@ void code_contractst::add_contract_check(
   goto_programt check;
 
   // prepare function call including all declarations
+  const symbolt &function_symbol = ns.lookup(mangled_function);
   code_function_callt call(function_symbol.symbol_expr());
 
   // Create a replace_symbolt object, for replacing expressions in the callee

src/goto-instrument/horn_encoding.cpp

@@ -699,12 +699,6 @@ static exprt simplifying_not(exprt src)
     return not_exprt(src);
 }
 
-static bool has_contract(const code_with_contract_typet &contract)
-{
-  return !contract.assigns().empty() || !contract.requires().empty() ||
-         !contract.ensures().empty();
-}
-
 void state_encodingt::function_call_symbol(
   goto_programt::const_targett loc,
   encoding_targett &dest)
@@ -1007,7 +1001,7 @@ void state_encoding(
       const auto &symbol = ns.lookup(f->first);
       if(
         f->first == goto_functionst::entry_point() ||
-        has_contract(to_code_with_contract_type(symbol.type)))
+        to_code_with_contract_type(symbol.type).has_contract())
       {
         dest.annotation("");
         dest.annotation("function " + id2string(f->first));

src/linking/linking.cpp

@@ -1101,6 +1101,11 @@ void linkingt::duplicate_non_type_symbol(
   symbolt &old_symbol,
   symbolt &new_symbol)
 {
+  // we do not permit multiple contracts to be defined, or cases where only one
+  // of the symbols is a contract
+  if(old_symbol.is_property || new_symbol.is_property)
+    link_error(old_symbol, new_symbol, "conflict on code contract");
+
   // see if it is a function or a variable
 
   bool is_code_old_symbol=old_symbol.type.id()==ID_code;