Skip to content

Commit 11066d1

Browse files
kroeningkroening
committed
SMV: type checking of simple types
This moves lowering of the SMV simple types from the SMV parser to the type checker.
1 parent 79a2e1e commit 11066d1

File tree

3 files changed

+78
-31
lines changed

3 files changed

+78
-31
lines changed

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,31 +18,36 @@ IREP_ID_ONE(E)
1818
IREP_ID_ONE(G)
1919
IREP_ID_ONE(X)
2020
IREP_ID_ONE(smv_abs)
21+
IREP_ID_ONE(smv_array)
2122
IREP_ID_ONE(smv_bitimplies)
2223
IREP_ID_ONE(smv_bit_selection)
2324
IREP_ID_ONE(smv_bool)
2425
IREP_ID_ONE(smv_cases)
2526
IREP_ID_ONE(smv_count)
2627
IREP_ID_ONE(smv_enumeration)
2728
IREP_ID_ONE(smv_extend)
29+
IREP_ID_ONE(smv_identifier)
30+
IREP_ID_ONE(smv_iff)
2831
IREP_ID_ONE(smv_max)
2932
IREP_ID_ONE(smv_min)
33+
IREP_ID_ONE(smv_module_instance)
3034
IREP_ID_ONE(smv_next)
31-
IREP_ID_ONE(smv_identifier)
32-
IREP_ID_ONE(smv_iff)
3335
IREP_ID_TWO(C_smv_iff, "#smv_iff")
36+
IREP_ID_ONE(smv_range)
3437
IREP_ID_ONE(smv_resize)
3538
IREP_ID_ONE(smv_toint)
3639
IREP_ID_ONE(smv_set)
3740
IREP_ID_ONE(smv_setin)
3841
IREP_ID_ONE(smv_setnotin)
3942
IREP_ID_ONE(smv_signed_cast)
43+
IREP_ID_ONE(smv_signed_word)
4044
IREP_ID_ONE(smv_sizeof)
41-
IREP_ID_ONE(smv_module_instance)
4245
IREP_ID_ONE(smv_swconst)
4346
IREP_ID_ONE(smv_union)
4447
IREP_ID_ONE(smv_unsigned_cast)
48+
IREP_ID_ONE(smv_unsigned_word)
4549
IREP_ID_ONE(smv_uwconst)
50+
IREP_ID_ONE(smv_word)
4651
IREP_ID_ONE(smv_word1)
4752
IREP_ID_ONE(smv_word_constant)
4853
IREP_ID_ONE(smv_H)

‎src/smvlang/parser.y‎

Lines changed: 15 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -556,42 +556,33 @@ type_specifier:
556556
;
557557

558558
simple_type_specifier:
559-
array_Token NUMBER_Token DOTDOT_Token NUMBER_Token of_Token simple_type_specifier
559+
array_Token integer_constant DOTDOT_Token integer_constant of_Token simple_type_specifier
560560
{
561-
init($$, ID_array);
562-
int start=atoi(stack_expr($2).id().c_str());
563-
int end=atoi(stack_expr($4).id().c_str());
564-
565-
if(end < start)
566-
{
567-
yyerror("array must end with number >= `"+std::to_string(start)+"'");
568-
YYERROR;
569-
}
570-
571-
stack_type($$).set(ID_size, end-start+1);
572-
stack_type($$).set(ID_offset, start);
561+
init($$, ID_smv_array);
562+
stack_type($$).set(ID_from, stack_expr($2));
563+
stack_type($$).set(ID_to, stack_expr($4));
573564
stack_type($$).add_subtype()=stack_type($6);
574565
}
575566
| boolean_Token { init($$, ID_bool); }
576-
| word_Token '[' NUMBER_Token ']'
567+
| word_Token '[' integer_constant ']'
577568
{
578-
init($$, ID_unsignedbv);
579-
stack_type($$).set(ID_width, stack_expr($3).id());
569+
init($$, ID_smv_word);
570+
stack_type($$).set(ID_width, stack_expr($3));
580571
}
581-
| signed_Token word_Token '[' NUMBER_Token ']'
572+
| signed_Token word_Token '[' integer_constant ']'
582573
{
583-
init($$, ID_signedbv);
584-
stack_type($$).set(ID_width, stack_expr($4).id());
574+
init($$, ID_smv_signed_word);
575+
stack_type($$).set(ID_width, stack_expr($4));
585576
}
586-
| unsigned_Token word_Token '[' NUMBER_Token ']'
577+
| unsigned_Token word_Token '[' integer_constant ']'
587578
{
588-
init($$, ID_unsignedbv);
589-
stack_type($$).set(ID_width, stack_expr($4).id());
579+
init($$, ID_smv_unsigned_word);
580+
stack_type($$).set(ID_width, stack_expr($4));
590581
}
591582
| '{' enum_list '}' { $$=$2; }
592-
| NUMBER_Token DOTDOT_Token NUMBER_Token
583+
| integer_constant DOTDOT_Token integer_constant
593584
{
594-
init($$, ID_range);
585+
init($$, ID_smv_range);
595586
stack_type($$).set(ID_from, stack_expr($1));
596587
stack_type($$).set(ID_to, stack_expr($3));
597588
}

‎src/smvlang/smv_typecheck.cpp‎

Lines changed: 55 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -365,18 +365,69 @@ Function: smv_typecheckt::check_type
365365

366366
void smv_typecheckt::check_type(typet &type)
367367
{
368-
if(type.id() == ID_range)
368+
if(type.id() == ID_smv_array)
369369
{
370-
auto range = smv_ranget::from_type(to_range_type(type));
370+
auto from = numeric_cast_v<mp_integer>(
371+
to_constant_expr(static_cast<const exprt &>(type.find(ID_from))));
372+
auto to = numeric_cast_v<mp_integer>(
373+
to_constant_expr(static_cast<const exprt &>(type.find(ID_to))));
371374

372-
if(range.from > range.to)
373-
throw errort().with_location(type.source_location()) << "range is empty";
375+
if(to < from)
376+
throw errort().with_location(type.source_location())
377+
<< "array must end with number >= `" << from << '\'';
378+
379+
type.id(ID_array);
380+
type.remove(ID_from);
381+
type.remove(ID_to);
382+
type.set(ID_size, integer2string(to - from + 1));
383+
type.set(ID_offset, integer2string(from));
384+
385+
// recursive call
386+
check_type(to_type_with_subtype(type).subtype());
374387
}
375388
else if(type.id() == ID_smv_enumeration)
376389
{
377390
// normalize the ordering of elements
378391
to_smv_enumeration_type(type).normalize();
379392
}
393+
else if(type.id() == ID_smv_range)
394+
{
395+
auto from = numeric_cast_v<mp_integer>(
396+
to_constant_expr(static_cast<const exprt &>(type.find(ID_from))));
397+
auto to = numeric_cast_v<mp_integer>(
398+
to_constant_expr(static_cast<const exprt &>(type.find(ID_to))));
399+
400+
if(from > to)
401+
throw errort().with_location(type.source_location()) << "range is empty";
402+
403+
type.id(ID_range);
404+
type.set(ID_from, integer2string(from));
405+
type.set(ID_to, integer2string(to));
406+
}
407+
else if(type.id() == ID_smv_signed_word)
408+
{
409+
auto width = numeric_cast_v<mp_integer>(
410+
to_constant_expr(static_cast<const exprt &>(type.find(ID_width))));
411+
412+
if(width < 1)
413+
throw errort().with_location(type.source_location())
414+
<< "word width must be 1 or larger";
415+
416+
type.id(ID_signedbv);
417+
type.set(ID_width, integer2string(width));
418+
}
419+
else if(type.id() == ID_smv_word || type.id() == ID_smv_unsigned_word)
420+
{
421+
auto width = numeric_cast_v<mp_integer>(
422+
to_constant_expr(static_cast<const exprt &>(type.find(ID_width))));
423+
424+
if(width < 1)
425+
throw errort().with_location(type.source_location())
426+
<< "word width must be 1 or larger";
427+
428+
type.id(ID_unsignedbv);
429+
type.set(ID_width, integer2string(width));
430+
}
380431
}
381432

382433
/*******************************************************************\

0 commit comments

Comments
 (0)