Skip to content

Commit e1ccf25

Browse files
kroeningkroening
committed
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.
1 parent 29a323f commit e1ccf25

File tree

5 files changed

+124
-89
lines changed

5 files changed

+124
-89
lines changed

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -245,6 +245,24 @@ void ansi_c_convert_typet::read_rec(const typet &type)
245245
{
246246
UNREACHABLE;
247247
}
248+
else if(type.id() == ID_C_spec_requires)
249+
{
250+
const exprt &as_expr =
251+
static_cast<const exprt &>(static_cast<const irept &>(type));
252+
requires = to_unary_expr(as_expr).op();
253+
}
254+
else if(type.id() == ID_C_spec_assigns)
255+
{
256+
const exprt &as_expr =
257+
static_cast<const exprt &>(static_cast<const irept &>(type));
258+
assigns = to_unary_expr(as_expr).op();
259+
}
260+
else if(type.id() == ID_C_spec_ensures)
261+
{
262+
const exprt &as_expr =
263+
static_cast<const exprt &>(static_cast<const irept &>(type));
264+
ensures = to_unary_expr(as_expr).op();
265+
}
248266
else
249267
other.push_back(type);
250268
}
@@ -290,6 +308,16 @@ void ansi_c_convert_typet::write(typet &type)
290308

291309
type.swap(other.front());
292310

311+
// the contract expressions are meant for function types only
312+
if(requires.is_not_nil())
313+
type.add(ID_C_spec_requires) = std::move(requires);
314+
315+
if(assigns.is_not_nil())
316+
type.add(ID_C_spec_assigns) = std::move(assigns);
317+
318+
if(ensures.is_not_nil())
319+
type.add(ID_C_spec_ensures) = std::move(ensures);
320+
293321
if(constructor || destructor)
294322
{
295323
if(constructor && destructor)

‎src/ansi-c/ansi_c_convert_type.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,9 @@ class ansi_c_convert_typet:public messaget
4545
exprt msc_based; // this is Visual Studio
4646
bool constructor, destructor;
4747

48+
// contracts
49+
exprt requires, assigns, ensures;
50+
4851
// storage spec
4952
c_storage_spect c_storage_spec;
5053

@@ -82,6 +85,10 @@ class ansi_c_convert_typet:public messaget
8285
msc_based.make_nil();
8386
gcc_attribute_mode.make_nil();
8487

88+
requires.make_nil();
89+
assigns.make_nil();
90+
ensures.make_nil();
91+
8592
packed=aligned=constructor=destructor=false;
8693

8794
other.clear();

‎src/ansi-c/c_typecheck_base.cpp

Lines changed: 28 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -644,19 +644,6 @@ void c_typecheck_baset::typecheck_declaration(
644644
// mark as 'already typechecked'
645645
already_typechecked_typet::make_already_typechecked(declaration.type());
646646

647-
irept contract;
648-
649-
{
650-
exprt spec_assigns = declaration.spec_assigns();
651-
contract.add(ID_C_spec_assigns).swap(spec_assigns);
652-
653-
exprt spec_ensures = declaration.spec_ensures();
654-
contract.add(ID_C_spec_ensures).swap(spec_ensures);
655-
656-
exprt spec_requires = declaration.spec_requires();
657-
contract.add(ID_C_spec_requires).swap(spec_requires);
658-
}
659-
660647
// Now do declarators, if any.
661648
for(auto &declarator : declaration.declarators())
662649
{
@@ -728,45 +715,37 @@ void c_typecheck_baset::typecheck_declaration(
728715
irep_idt identifier=symbol.name;
729716
declarator.set_name(identifier);
730717

731-
// If the declarator is for a function definition, typecheck it.
732-
if(can_cast_type<code_typet>(declarator.type()))
718+
typecheck_symbol(symbol);
719+
720+
// check the contract, if any
721+
if(symbol.type.id() == ID_code)
733722
{
734-
typecheck_assigns(to_code_type(declarator.type()), contract);
735-
}
723+
// We typecheck this after the
724+
// function body done above, so as to have parameter symbols
725+
// available
726+
symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
727+
auto &code_type = to_code_with_contract_type(new_symbol.type);
736728

737-
typecheck_symbol(symbol);
729+
if(as_const(code_type).requires().is_not_nil())
730+
{
731+
auto &requires = code_type.requires();
732+
typecheck_expr(requires);
733+
implicit_typecast_bool(requires);
734+
}
738735

739-
// add code contract (if any); we typecheck this after the
740-
// function body done above, so as to have parameter symbols
741-
// available
742-
symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
743-
744-
typecheck_assigns_exprs(
745-
static_cast<codet &>(contract), ID_C_spec_assigns);
746-
typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_requires);
747-
748-
typet ret_type = void_type();
749-
if(new_symbol.type.id()==ID_code)
750-
ret_type=to_code_type(new_symbol.type).return_type();
751-
assert(parameter_map.empty());
752-
if(ret_type.id()!=ID_empty)
753-
parameter_map[CPROVER_PREFIX "return_value"] = ret_type;
754-
typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_ensures);
755-
parameter_map.clear();
756-
757-
exprt assigns_to_add =
758-
static_cast<const exprt &>(contract.find(ID_C_spec_assigns));
759-
if(assigns_to_add.is_not_nil())
760-
to_code_with_contract_type(new_symbol.type).assigns() = assigns_to_add;
761-
exprt requires_to_add =
762-
static_cast<const exprt &>(contract.find(ID_C_spec_requires));
763-
if(requires_to_add.is_not_nil())
764-
to_code_with_contract_type(new_symbol.type).requires() =
765-
requires_to_add;
766-
exprt ensures_to_add =
767-
static_cast<const exprt &>(contract.find(ID_C_spec_ensures));
768-
if(ensures_to_add.is_not_nil())
769-
to_code_with_contract_type(new_symbol.type).ensures() = ensures_to_add;
736+
if(as_const(code_type).assigns().is_not_nil())
737+
{
738+
for(auto &op : code_type.assigns().operands())
739+
typecheck_expr(op);
740+
}
741+
742+
if(as_const(code_type).ensures().is_not_nil())
743+
{
744+
auto &ensures = code_type.ensures();
745+
typecheck_expr(ensures);
746+
implicit_typecast_bool(ensures);
747+
}
748+
}
770749
}
771750
}
772751
}

‎src/ansi-c/expr2c.cpp

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -550,6 +550,19 @@ std::string expr2ct::convert_rec(
550550
dest.resize(dest.size()-1);
551551
}
552552

553+
// contract, if any
554+
if(to_code_with_contract_type(src).requires().is_not_nil())
555+
dest += " [[requires " +
556+
convert(to_code_with_contract_type(src).requires()) + "]]";
557+
558+
if(!to_code_with_contract_type(src).assigns().operands().empty())
559+
dest += " [[assigns " +
560+
convert(to_code_with_contract_type(src).assigns()) + "]]";
561+
562+
if(to_code_with_contract_type(src).ensures().is_not_nil())
563+
dest += " [[ensures " +
564+
convert(to_code_with_contract_type(src).ensures()) + "]]";
565+
553566
return dest;
554567
}
555568
else if(src.id()==ID_vector)

‎src/ansi-c/parser.y

Lines changed: 48 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -497,27 +497,6 @@ loop_invariant_opt:
497497
{ $$=$3; }
498498
;
499499

500-
requires_opt:
501-
/* nothing */
502-
{ init($$); parser_stack($$).make_nil(); }
503-
| TOK_CPROVER_REQUIRES '(' ACSL_binding_expression ')'
504-
{ $$=$3; }
505-
;
506-
507-
ensures_opt:
508-
/* nothing */
509-
{ init($$); parser_stack($$).make_nil(); }
510-
| TOK_CPROVER_ENSURES '(' ACSL_binding_expression ')'
511-
{ $$=$3; }
512-
;
513-
514-
assigns_opt:
515-
/* nothing */
516-
{ init($$); parser_stack($$).make_nil(); }
517-
| TOK_CPROVER_ASSIGNS '(' target_list ')'
518-
{ $$=$3; }
519-
;
520-
521500
target_list:
522501
target
523502
{
@@ -2901,29 +2880,16 @@ asm_definition:
29012880

29022881
function_definition:
29032882
function_head
2904-
assigns_opt
2905-
requires_opt
2906-
ensures_opt
29072883
function_body
29082884
{
2909-
2910-
// Capture assigns clause
2911-
if(parser_stack($2).is_not_nil())
2912-
parser_stack($1).add(ID_C_spec_assigns).swap(parser_stack($2));
2913-
2914-
// Capture code contract
2915-
if(parser_stack($3).is_not_nil())
2916-
parser_stack($1).add(ID_C_spec_requires).swap(parser_stack($3));
2917-
if(parser_stack($4).is_not_nil())
2918-
parser_stack($1).add(ID_C_spec_ensures).swap(parser_stack($4));
29192885
// The head is a declaration with one declarator,
29202886
// and the body becomes the 'value'.
29212887
$$=$1;
29222888
ansi_c_declarationt &ansi_c_declaration=
29232889
to_ansi_c_declaration(parser_stack($$));
29242890

29252891
assert(ansi_c_declaration.declarators().size()==1);
2926-
ansi_c_declaration.add_initializer(parser_stack($5));
2892+
ansi_c_declaration.add_initializer(parser_stack($2));
29272893

29282894
// Kill the scope that 'function_head' creates.
29292895
PARSER.pop_scope();
@@ -3065,13 +3031,15 @@ function_head:
30653031
{
30663032
init($$, ID_declaration);
30673033
parser_stack($$).type().swap(parser_stack($1));
3034+
$2=merge($3, $2);
30683035
PARSER.add_declarator(parser_stack($$), parser_stack($2));
30693036
create_function_scope($$);
30703037
}
30713038
| type_specifier declarator post_declarator_attributes_opt
30723039
{
30733040
init($$, ID_declaration);
30743041
parser_stack($$).type().swap(parser_stack($1));
3042+
$2=merge($3, $2);
30753043
PARSER.add_declarator(parser_stack($$), parser_stack($2));
30763044
create_function_scope($$);
30773045
}
@@ -3285,6 +3253,42 @@ parameter_abstract_declarator:
32853253
| parameter_postfix_abstract_declarator
32863254
;
32873255

3256+
cprover_contract:
3257+
TOK_CPROVER_ENSURES '(' ACSL_binding_expression ')'
3258+
{
3259+
$$=$1;
3260+
set($$, ID_C_spec_ensures);
3261+
mto($$, $3);
3262+
}
3263+
| TOK_CPROVER_REQUIRES '(' ACSL_binding_expression ')'
3264+
{
3265+
$$=$1;
3266+
set($$, ID_C_spec_requires);
3267+
mto($$, $3);
3268+
}
3269+
| TOK_CPROVER_ASSIGNS '(' target_list ')'
3270+
{
3271+
$$=$1;
3272+
set($$, ID_C_spec_assigns);
3273+
parser_stack($$).operands() = std::move(parser_stack($3).operands());
3274+
}
3275+
;
3276+
3277+
cprover_contract_sequence:
3278+
cprover_contract
3279+
| cprover_contract_sequence cprover_contract
3280+
{
3281+
$$=$1;
3282+
merge($$, $2);
3283+
}
3284+
;
3285+
3286+
cprover_contract_sequence_opt:
3287+
/* nothing */
3288+
{ init($$); }
3289+
| cprover_contract_sequence
3290+
;
3291+
32883292
postfixing_abstract_declarator:
32893293
parameter_postfixing_abstract_declarator
32903294
/* The following two rules implement K&R headers! */
@@ -3323,6 +3327,7 @@ postfixing_abstract_declarator:
33233327
parameter_postfixing_abstract_declarator:
33243328
array_abstract_declarator
33253329
| '(' ')'
3330+
cprover_contract_sequence_opt
33263331
{
33273332
$$=$1;
33283333
set($$, ID_code);
@@ -3337,12 +3342,13 @@ parameter_postfixing_abstract_declarator:
33373342
id2string(PARSER.current_scope().last_declarator)+"::");
33383343
}
33393344
parameter_type_list
3340-
')' KnR_parameter_header_opt
3345+
')'
3346+
KnR_parameter_header_opt
3347+
cprover_contract_sequence_opt
33413348
{
3342-
$$=$1;
3343-
set($$, ID_code);
3344-
stack_type($$).subtype()=typet(ID_abstract);
3345-
stack_type($$).add(ID_parameters).get_sub().
3349+
set($1, ID_code);
3350+
stack_type($1).subtype()=typet(ID_abstract);
3351+
stack_type($1).add(ID_parameters).get_sub().
33463352
swap((irept::subt &)(to_type_with_subtypes(stack_type($3)).subtypes()));
33473353
PARSER.pop_scope();
33483354

@@ -3351,6 +3357,8 @@ parameter_postfixing_abstract_declarator:
33513357
adjust_KnR_parameters(parser_stack($$).add(ID_parameters), parser_stack($5));
33523358
parser_stack($$).set(ID_C_KnR, true);
33533359
}
3360+
3361+
$$ = merge($6, $1);
33543362
}
33553363
;
33563364

0 commit comments

Comments
 (0)