allow contracts on function declarations

This changes the grammar of the C frontend to allow contracts on function
declarations.  This also removes the requirement that the contract clauses
appear in any particular order.

Author: kroening

src/ansi-c/ansi_c_convert_type.cpp

@@ -245,6 +245,24 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   {
     UNREACHABLE;
   }
+  else if(type.id() == ID_C_spec_requires)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+    requires = to_unary_expr(as_expr).op();
+  }
+  else if(type.id() == ID_C_spec_assigns)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+    assigns = to_unary_expr(as_expr).op();
+  }
+  else if(type.id() == ID_C_spec_ensures)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+    ensures = to_unary_expr(as_expr).op();
+  }
   else
     other.push_back(type);
 }
@@ -290,6 +308,16 @@ void ansi_c_convert_typet::write(typet &type)
 
     type.swap(other.front());
 
+    // the contract expressions are meant for function types only
+    if(requires.is_not_nil())
+      type.add(ID_C_spec_requires) = std::move(requires);
+
+    if(assigns.is_not_nil())
+      type.add(ID_C_spec_assigns) = std::move(assigns);
+
+    if(ensures.is_not_nil())
+      type.add(ID_C_spec_ensures) = std::move(ensures);
+
     if(constructor || destructor)
     {
       if(constructor && destructor)

src/ansi-c/ansi_c_convert_type.h

@@ -45,6 +45,9 @@ class ansi_c_convert_typet:public messaget
   exprt msc_based; // this is Visual Studio
   bool constructor, destructor;
 
+  // contracts
+  exprt requires, assigns, ensures;
+
   // storage spec
   c_storage_spect c_storage_spec;
 
@@ -82,6 +85,10 @@ class ansi_c_convert_typet:public messaget
     msc_based.make_nil();
     gcc_attribute_mode.make_nil();
 
+    requires.make_nil();
+    assigns.make_nil();
+    ensures.make_nil();
+
     packed=aligned=constructor=destructor=false;
 
     other.clear();

src/ansi-c/c_typecheck_base.cpp

@@ -644,19 +644,6 @@ void c_typecheck_baset::typecheck_declaration(
     // mark as 'already typechecked'
     already_typechecked_typet::make_already_typechecked(declaration.type());
 
-    irept contract;
-
-    {
-      exprt spec_assigns = declaration.spec_assigns();
-      contract.add(ID_C_spec_assigns).swap(spec_assigns);
-
-      exprt spec_ensures = declaration.spec_ensures();
-      contract.add(ID_C_spec_ensures).swap(spec_ensures);
-
-      exprt spec_requires = declaration.spec_requires();
-      contract.add(ID_C_spec_requires).swap(spec_requires);
-    }
-
     // Now do declarators, if any.
     for(auto &declarator : declaration.declarators())
     {
@@ -728,45 +715,7 @@ void c_typecheck_baset::typecheck_declaration(
       irep_idt identifier=symbol.name;
       declarator.set_name(identifier);
 
-      // If the declarator is for a function definition, typecheck it.
-      if(can_cast_type<code_typet>(declarator.type()))
-      {
-        typecheck_assigns(to_code_type(declarator.type()), contract);
-      }
-
       typecheck_symbol(symbol);
-
-      // add code contract (if any); we typecheck this after the
-      // function body done above, so as to have parameter symbols
-      // available
-      symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
-
-      typecheck_assigns_exprs(
-        static_cast<codet &>(contract), ID_C_spec_assigns);
-      typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_requires);
-
-      typet ret_type = void_type();
-      if(new_symbol.type.id()==ID_code)
-        ret_type=to_code_type(new_symbol.type).return_type();
-      assert(parameter_map.empty());
-      if(ret_type.id()!=ID_empty)
-        parameter_map[CPROVER_PREFIX "return_value"] = ret_type;
-      typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_ensures);
-      parameter_map.clear();
-
-      exprt assigns_to_add =
-        static_cast<const exprt &>(contract.find(ID_C_spec_assigns));
-      if(assigns_to_add.is_not_nil())
-        to_code_with_contract_type(new_symbol.type).assigns() = assigns_to_add;
-      exprt requires_to_add =
-        static_cast<const exprt &>(contract.find(ID_C_spec_requires));
-      if(requires_to_add.is_not_nil())
-        to_code_with_contract_type(new_symbol.type).requires() =
-          requires_to_add;
-      exprt ensures_to_add =
-        static_cast<const exprt &>(contract.find(ID_C_spec_ensures));
-      if(ensures_to_add.is_not_nil())
-        to_code_with_contract_type(new_symbol.type).ensures() = ensures_to_add;
     }
   }
 }

src/ansi-c/c_typecheck_type.cpp

@@ -515,6 +515,27 @@ void c_typecheck_baset::typecheck_code_type(code_typet &type)
     error() << "function must not return function type" << eom;
     throw 0;
   }
+
+  // check the contract, if any
+  if(to_code_with_contract_type(as_const(type)).requires().is_not_nil())
+  {
+    auto &requires = to_code_with_contract_type(type).requires();
+    typecheck_expr(requires);
+    implicit_typecast_bool(requires);
+  }
+
+  if(to_code_with_contract_type(as_const(type)).assigns().is_not_nil())
+  {
+    for(auto &op : to_code_with_contract_type(type).assigns().operands())
+      typecheck_expr(op);
+  }
+
+  if(to_code_with_contract_type(as_const(type)).ensures().is_not_nil())
+  {
+    auto &ensures = to_code_with_contract_type(type).ensures();
+    typecheck_expr(ensures);
+    implicit_typecast_bool(ensures);
+  }
 }
 
 void c_typecheck_baset::typecheck_array_type(array_typet &type)

src/ansi-c/expr2c.cpp

@@ -550,6 +550,16 @@ std::string expr2ct::convert_rec(
         dest.resize(dest.size()-1);
     }
 
+    // contract, if any
+    if(to_code_with_contract_type(src).requires().is_not_nil())
+      dest += " [[requires " + convert(to_code_with_contract_type(src).requires()) + "]]";
+
+    if(!to_code_with_contract_type(src).assigns().operands().empty())
+      dest += " [[assigns " + convert(to_code_with_contract_type(src).assigns()) + "]]";
+
+    if(to_code_with_contract_type(src).ensures().is_not_nil())
+      dest += " [[ensures " + convert(to_code_with_contract_type(src).ensures()) + "]]";
+
     return dest;
   }
   else if(src.id()==ID_vector)

src/ansi-c/parser.y

@@ -497,27 +497,6 @@ loop_invariant_opt:
         { $$=$3; }
         ;
 
-requires_opt:
-        /* nothing */
-        { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_REQUIRES '(' ACSL_binding_expression ')'
-        { $$=$3; }
-        ;
-
-ensures_opt:
-        /* nothing */
-        { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_ENSURES '(' ACSL_binding_expression ')'
-        { $$=$3; }
-        ;
-
-assigns_opt:
-        /* nothing */
-        { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_ASSIGNS '(' target_list ')'
-        { $$=$3; }
-        ;
-
 target_list:
           target
         {
@@ -1008,6 +987,7 @@ post_declarator_attribute:
           parser_stack($$).set(ID_flavor, ID_gcc);
           parser_stack($$).operands().swap(parser_stack($4).operands());
         }
+        | cprover_contract
         | gcc_attribute_specifier
         ;
 
@@ -2901,29 +2881,16 @@ asm_definition:
 
 function_definition:
           function_head
-          assigns_opt
-          requires_opt
-          ensures_opt
           function_body
         {
-
-          // Capture assigns clause
-          if(parser_stack($2).is_not_nil())
-            parser_stack($1).add(ID_C_spec_assigns).swap(parser_stack($2));
-
-          // Capture code contract
-          if(parser_stack($3).is_not_nil())
-            parser_stack($1).add(ID_C_spec_requires).swap(parser_stack($3));
-          if(parser_stack($4).is_not_nil())
-            parser_stack($1).add(ID_C_spec_ensures).swap(parser_stack($4));
           // The head is a declaration with one declarator,
           // and the body becomes the 'value'.
           $$=$1;
           ansi_c_declarationt &ansi_c_declaration=
             to_ansi_c_declaration(parser_stack($$));
 
           assert(ansi_c_declaration.declarators().size()==1);
-          ansi_c_declaration.add_initializer(parser_stack($5));
+          ansi_c_declaration.add_initializer(parser_stack($2));
 
           // Kill the scope that 'function_head' creates.
           PARSER.pop_scope();
@@ -3065,13 +3032,15 @@ function_head:
         {
           init($$, ID_declaration);
           parser_stack($$).type().swap(parser_stack($1));
+          $2=merge($3, $2);
           PARSER.add_declarator(parser_stack($$), parser_stack($2));
           create_function_scope($$);
         }
         | type_specifier declarator post_declarator_attributes_opt
         {
           init($$, ID_declaration);
           parser_stack($$).type().swap(parser_stack($1));
+          $2=merge($3, $2);
           PARSER.add_declarator(parser_stack($$), parser_stack($2));
           create_function_scope($$);
         }
@@ -3285,6 +3254,27 @@ parameter_abstract_declarator:
         | parameter_postfix_abstract_declarator
         ;
 
+cprover_contract:
+          TOK_CPROVER_ENSURES '(' ACSL_binding_expression ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_ensures);
+          mto($$, $3);
+        }
+        | TOK_CPROVER_REQUIRES '(' ACSL_binding_expression ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_requires);
+          mto($$, $3);
+        }
+        | TOK_CPROVER_ASSIGNS '(' target_list ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_assigns);
+          parser_stack($$).operands() = std::move(parser_stack($3).operands());
+        }
+        ;
+
 postfixing_abstract_declarator:
           parameter_postfixing_abstract_declarator
         /* The following two rules implement K&R headers! */