Skip to content

Commit a7a7f72

Browse files
feliperodrifeliperodri
committed
Updates parser to handle contracts with function signatures
Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 0048f4c commit a7a7f72

File tree

8 files changed

+165
-23
lines changed

8 files changed

+165
-23
lines changed

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -512,7 +512,9 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
512512
if(upper.id() == ID_constant || upper.id() == ID_identifier)
513513
{
514514
dstringt upper_type = upper.type().get(ID_C_c_type);
515-
if(upper_type != ID_signed_int.c_str() && upper_type != ID_unsigned_int.c_str())
515+
if(
516+
upper_type != ID_signed_int.c_str() &&
517+
upper_type != ID_unsigned_int.c_str())
516518
{
517519
error().source_location = expr.source_location();
518520
error() << "Upper bound of range should be an integer, but got: "

‎src/ansi-c/parser.y

Lines changed: 101 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,7 @@ extern char *yyansi_ctext;
101101
%token TOK_NE "!="
102102
%token TOK_ANDAND "&&"
103103
%token TOK_OROR "||"
104+
%token TOK_RANGE ".."
104105
%token TOK_ELLIPSIS "..."
105106

106107
/*** modifying assignment operators ***/
@@ -532,15 +533,63 @@ target_list:
532533
;
533534

534535
target:
536+
deref_target
537+
| target '[' array_index ']'
538+
{ binary($$, $1, $2, ID_array_range, $3); }
539+
| target '[' array_range ']'
540+
{ binary($$, $1, $2, ID_array_range, $3); }
541+
;
542+
543+
array_index:
535544
identifier
536-
| '*' target
545+
| integer
546+
;
547+
548+
array_range:
549+
array_index ',' array_index
550+
{
551+
$$=$2;
552+
set($$, ID_int_range);
553+
mto($$, $1);
554+
mto($$, $3);
555+
}
556+
;
557+
558+
deref_target:
559+
member_target
560+
| '*' deref_target
537561
{
538562
$$=$1;
539563
set($$, ID_dereference);
540564
mto($$, $2);
541565
}
542566
;
543567

568+
member_target:
569+
primary_target
570+
| member_target '.' member_name
571+
{
572+
$$=$2;
573+
set($$, ID_member);
574+
mto($$, $1);
575+
parser_stack($$).set(ID_component_name, parser_stack($3).get(ID_C_base_name));
576+
}
577+
| member_target TOK_ARROW member_name
578+
{
579+
$$=$2;
580+
set($$, ID_ptrmember);
581+
mto($$, $1);
582+
parser_stack($$).set(ID_component_name, parser_stack($3).get(ID_C_base_name));
583+
}
584+
;
585+
586+
primary_target:
587+
identifier
588+
| '(' target ')'
589+
{ $$ = $2; }
590+
;
591+
592+
544593
statement_expression: '(' compound_statement ')'
545594
{
546595
$$=$1;
@@ -1032,17 +1081,39 @@ declaring_list:
10321081
post_declarator_attributes_opt
10331082
{
10341083
$2=merge($3, $2); // type attribute
1035-
10361084
// the symbol has to be visible during initialization
10371085
init($$, ID_declaration);
10381086
parser_stack($$).type().swap(parser_stack($1));
10391087
PARSER.add_declarator(parser_stack($$), parser_stack($2));
1088+
create_function_scope($$);
10401089
}
10411090
initializer_opt
1091+
assigns_opt
1092+
requires_opt
1093+
ensures_opt
10421094
{
1043-
// add the initializer
10441095
$$=$4;
1045-
to_ansi_c_declaration(parser_stack($$)).add_initializer(parser_stack($5));
1096+
1097+
if(parser_stack($6).is_not_nil()) // Capture assigns clause
1098+
parser_stack($$).add(ID_C_spec_assigns).swap(parser_stack($6));
1099+
1100+
// Capture code contract
1101+
if(parser_stack($7).is_not_nil())
1102+
parser_stack($$).add(ID_C_spec_requires).swap(parser_stack($7));
1103+
if(parser_stack($8).is_not_nil())
1104+
parser_stack($$).add(ID_C_spec_ensures).swap(parser_stack($8));
1105+
1106+
// add the initializer
1107+
if(parser_stack($5).is_not_nil())
1108+
{
1109+
to_ansi_c_declaration(parser_stack($$)).add_initializer(parser_stack($5));
1110+
}
1111+
1112+
// Kill the scope that 'function_head' creates.
1113+
PARSER.pop_scope();
1114+
1115+
// We are no longer in any function.
1116+
PARSER.set_function(PARSER.current_scope().prefix.substr(0, PARSER.current_scope().prefix.find_first_of(':')));
10461117
}
10471118
| type_specifier declarator
10481119
post_declarator_attributes_opt
@@ -1053,12 +1124,35 @@ declaring_list:
10531124
init($$, ID_declaration);
10541125
parser_stack($$).type().swap(parser_stack($1));
10551126
PARSER.add_declarator(parser_stack($$), parser_stack($2));
1127+
create_function_scope($$);
10561128
}
10571129
initializer_opt
1130+
assigns_opt
1131+
requires_opt
1132+
ensures_opt
10581133
{
1059-
// add the initializer
10601134
$$=$4;
1061-
to_ansi_c_declaration(parser_stack($$)).add_initializer(parser_stack($5));
1135+
1136+
if(parser_stack($6).is_not_nil()) // Capture assigns clause
1137+
parser_stack($$).add(ID_C_spec_assigns).swap(parser_stack($6));
1138+
1139+
// Capture code contract
1140+
if(parser_stack($7).is_not_nil())
1141+
parser_stack($$).add(ID_C_spec_requires).swap(parser_stack($7));
1142+
if(parser_stack($8).is_not_nil())
1143+
parser_stack($$).add(ID_C_spec_ensures).swap(parser_stack($8));
1144+
1145+
// add the initializer
1146+
if(parser_stack($5).is_not_nil())
1147+
{
1148+
to_ansi_c_declaration(parser_stack($$)).add_initializer(parser_stack($5));
1149+
}
1150+
1151+
// Kill the scope that 'function_head' creates.
1152+
PARSER.pop_scope();
1153+
1154+
// We are no longer in any function.
1155+
PARSER.set_function(PARSER.current_scope().prefix.substr(0, PARSER.current_scope().prefix.find_first_of(':')));
10621156
}
10631157
| TOK_GCC_AUTO_TYPE declarator
10641158
post_declarator_attributes_opt '=' initializer
@@ -2892,29 +2986,16 @@ asm_definition:
28922986

28932987
function_definition:
28942988
function_head
2895-
assigns_opt
2896-
requires_opt
2897-
ensures_opt
28982989
function_body
28992990
{
2900-
2901-
// Capture assigns clause
2902-
if(parser_stack($2).is_not_nil())
2903-
parser_stack($1).add(ID_C_spec_assigns).swap(parser_stack($2));
2904-
2905-
// Capture code contract
2906-
if(parser_stack($3).is_not_nil())
2907-
parser_stack($1).add(ID_C_spec_requires).swap(parser_stack($3));
2908-
if(parser_stack($4).is_not_nil())
2909-
parser_stack($1).add(ID_C_spec_ensures).swap(parser_stack($4));
29102991
// The head is a declaration with one declarator,
29112992
// and the body becomes the 'value'.
29122993
$$=$1;
29132994
ansi_c_declarationt &ansi_c_declaration=
29142995
to_ansi_c_declaration(parser_stack($$));
29152996

29162997
assert(ansi_c_declaration.declarators().size()==1);
2917-
ansi_c_declaration.add_initializer(parser_stack($5));
2998+
ansi_c_declaration.add_initializer(parser_stack($2));
29182999

29193000
// Kill the scope that 'function_head' creates.
29203001
PARSER.pop_scope();

‎src/ansi-c/parser_static.inc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -332,7 +332,8 @@ static void create_function_scope(const YYSTYPE d)
332332
ansi_c_declarationt &declaration=to_ansi_c_declaration(parser_stack(d));
333333
ansi_c_declaratort &declarator=declaration.declarator();
334334

335-
irep_idt function_name=declarator.get_base_name();
335+
std::string declarator_name(declarator.get_name().c_str());
336+
irep_idt function_name = declarator_name.substr(0, declarator_name.find_first_of(':'));
336337

337338
// record which function we are in
338339
PARSER.set_function(function_name);

‎src/ansi-c/scanner.l

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1517,6 +1517,7 @@ __decltype { if(PARSER.cpp98 &&
15171517
"&&" { loc(); return TOK_ANDAND; }
15181518
"||" { loc(); return TOK_OROR; }
15191519
"..." { loc(); return TOK_ELLIPSIS; }
1520+
".." { loc(); return TOK_RANGE; }
15201521

15211522
"*=" { loc(); return TOK_MULTASSIGN; }
15221523
"/=" { loc(); return TOK_DIVASSIGN; }

‎src/goto-instrument/dump_c.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1471,7 +1471,6 @@ void dump_ct::cleanup_expr(exprt &expr)
14711471

14721472
if(
14731473
ns.follow(bu.type()).id() == ID_union &&
1474-
bu.source_location().get_function().empty() &&
14751474
bu.op() == zero_initializer(bu.op().type(), source_locationt{}, ns)
14761475
.value_or(nil_exprt{}))
14771476
{

‎src/util/irep_ids.def

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,8 @@ IREP_ID_ONE(union)
143143
IREP_ID_ONE(class)
144144
IREP_ID_ONE(merged_type)
145145
IREP_ID_ONE(range)
146+
IREP_ID_ONE(int_range)
147+
IREP_ID_ONE(array_range)
146148
IREP_ID_ONE(from)
147149
IREP_ID_ONE(to)
148150
IREP_ID_ONE(module)

‎src/util/pointer_offset_size.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -492,6 +492,10 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
492492
{
493493
return from_integer(32/8, size_type());
494494
}
495+
else if(type.id() == ID_empty)
496+
{
497+
return from_integer(0, size_type());
498+
}
495499
else
496500
return {};
497501
}

‎src/util/std_expr.h

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -824,6 +824,58 @@ inline multi_ary_exprt &to_multi_ary_expr(exprt &expr)
824824
return static_cast<multi_ary_exprt &>(expr);
825825
}
826826

827+
/// \brief A base class for int-range expressions
828+
class int_range_exprt : public expr_protectedt
829+
{
830+
public:
831+
int_range_exprt(const irep_idt &_id, operandst _operands, typet _type)
832+
: expr_protectedt(_id, std::move(_type))
833+
{
834+
operands() = std::move(_operands);
835+
}
836+
837+
exprt &op0()
838+
{
839+
return operands().front();
840+
}
841+
842+
exprt &op1()
843+
{
844+
return operands()[1];
845+
}
846+
847+
const exprt &op0() const
848+
{
849+
return operands().front();
850+
}
851+
852+
const exprt &op1() const
853+
{
854+
return operands()[1];
855+
}
856+
};
857+
858+
/// \brief Cast an exprt to a \ref int_range_exprt
859+
///
860+
/// \a expr must be known to be \ref int_range_exprt.
861+
///
862+
/// \param expr: Source expression
863+
/// \return Object of type \ref int_range_exprt
864+
inline const int_range_exprt &to_int_range_exprt(const exprt &expr)
865+
{
866+
return static_cast<const int_range_exprt &>(expr);
867+
}
868+
869+
/// \brief Cast an exprt to a \ref int_range_exprt
870+
///
871+
/// \a expr must be known to be \ref int_range_exprt.
872+
///
873+
/// \param expr: Source expression
874+
/// \return Object of type \ref int_range_exprt
875+
inline int_range_exprt &to_int_range_exprt(exprt &expr)
876+
{
877+
return static_cast<int_range_exprt &>(expr);
878+
}
827879

828880
/// \brief The plus expression
829881
/// Associativity is not specified.

0 commit comments

Comments
 (0)