diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 47e9b6b0b..c56f6fd4b 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -18,6 +18,7 @@ IREP_ID_ONE(E) IREP_ID_ONE(G) IREP_ID_ONE(X) IREP_ID_ONE(smv_abs) +IREP_ID_ONE(smv_array) IREP_ID_ONE(smv_bitimplies) IREP_ID_ONE(smv_bit_selection) IREP_ID_ONE(smv_bool) @@ -25,24 +26,28 @@ IREP_ID_ONE(smv_cases) IREP_ID_ONE(smv_count) IREP_ID_ONE(smv_enumeration) IREP_ID_ONE(smv_extend) +IREP_ID_ONE(smv_identifier) +IREP_ID_ONE(smv_iff) IREP_ID_ONE(smv_max) IREP_ID_ONE(smv_min) +IREP_ID_ONE(smv_module_instance) IREP_ID_ONE(smv_next) -IREP_ID_ONE(smv_identifier) -IREP_ID_ONE(smv_iff) IREP_ID_TWO(C_smv_iff, "#smv_iff") +IREP_ID_ONE(smv_range) IREP_ID_ONE(smv_resize) IREP_ID_ONE(smv_toint) IREP_ID_ONE(smv_set) IREP_ID_ONE(smv_setin) IREP_ID_ONE(smv_setnotin) IREP_ID_ONE(smv_signed_cast) +IREP_ID_ONE(smv_signed_word) IREP_ID_ONE(smv_sizeof) -IREP_ID_ONE(smv_module_instance) IREP_ID_ONE(smv_swconst) IREP_ID_ONE(smv_union) IREP_ID_ONE(smv_unsigned_cast) +IREP_ID_ONE(smv_unsigned_word) IREP_ID_ONE(smv_uwconst) +IREP_ID_ONE(smv_word) IREP_ID_ONE(smv_word1) IREP_ID_ONE(smv_word_constant) IREP_ID_ONE(smv_H) diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index f7745c8b5..f195b24d7 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -556,42 +556,33 @@ type_specifier: ; simple_type_specifier: - array_Token NUMBER_Token DOTDOT_Token NUMBER_Token of_Token simple_type_specifier + array_Token integer_constant DOTDOT_Token integer_constant of_Token simple_type_specifier { - init($$, ID_array); - int start=atoi(stack_expr($2).id().c_str()); - int end=atoi(stack_expr($4).id().c_str()); - - if(end < start) - { - yyerror("array must end with number >= `"+std::to_string(start)+"'"); - YYERROR; - } - - stack_type($$).set(ID_size, end-start+1); - stack_type($$).set(ID_offset, start); + init($$, ID_smv_array); + stack_type($$).set(ID_from, stack_expr($2)); + stack_type($$).set(ID_to, stack_expr($4)); stack_type($$).add_subtype()=stack_type($6); } | boolean_Token { init($$, ID_bool); } - | word_Token '[' NUMBER_Token ']' + | word_Token '[' integer_constant ']' { - init($$, ID_unsignedbv); - stack_type($$).set(ID_width, stack_expr($3).id()); + init($$, ID_smv_word); + stack_type($$).set(ID_width, stack_expr($3)); } - | signed_Token word_Token '[' NUMBER_Token ']' + | signed_Token word_Token '[' integer_constant ']' { - init($$, ID_signedbv); - stack_type($$).set(ID_width, stack_expr($4).id()); + init($$, ID_smv_signed_word); + stack_type($$).set(ID_width, stack_expr($4)); } - | unsigned_Token word_Token '[' NUMBER_Token ']' + | unsigned_Token word_Token '[' integer_constant ']' { - init($$, ID_unsignedbv); - stack_type($$).set(ID_width, stack_expr($4).id()); + init($$, ID_smv_unsigned_word); + stack_type($$).set(ID_width, stack_expr($4)); } | '{' enum_list '}' { $$=$2; } - | NUMBER_Token DOTDOT_Token NUMBER_Token + | integer_constant DOTDOT_Token integer_constant { - init($$, ID_range); + init($$, ID_smv_range); stack_type($$).set(ID_from, stack_expr($1)); stack_type($$).set(ID_to, stack_expr($3)); } diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 92f3c7cfe..9a8116988 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -365,18 +365,69 @@ Function: smv_typecheckt::check_type void smv_typecheckt::check_type(typet &type) { - if(type.id() == ID_range) + if(type.id() == ID_smv_array) { - auto range = smv_ranget::from_type(to_range_type(type)); + auto from = numeric_cast_v( + to_constant_expr(static_cast(type.find(ID_from)))); + auto to = numeric_cast_v( + to_constant_expr(static_cast(type.find(ID_to)))); - if(range.from > range.to) - throw errort().with_location(type.source_location()) << "range is empty"; + if(to < from) + throw errort().with_location(type.source_location()) + << "array must end with number >= `" << from << '\''; + + type.id(ID_array); + type.remove(ID_from); + type.remove(ID_to); + type.set(ID_size, integer2string(to - from + 1)); + type.set(ID_offset, integer2string(from)); + + // recursive call + check_type(to_type_with_subtype(type).subtype()); } else if(type.id() == ID_smv_enumeration) { // normalize the ordering of elements to_smv_enumeration_type(type).normalize(); } + else if(type.id() == ID_smv_range) + { + auto from = numeric_cast_v( + to_constant_expr(static_cast(type.find(ID_from)))); + auto to = numeric_cast_v( + to_constant_expr(static_cast(type.find(ID_to)))); + + if(from > to) + throw errort().with_location(type.source_location()) << "range is empty"; + + type.id(ID_range); + type.set(ID_from, integer2string(from)); + type.set(ID_to, integer2string(to)); + } + else if(type.id() == ID_smv_signed_word) + { + auto width = numeric_cast_v( + to_constant_expr(static_cast(type.find(ID_width)))); + + if(width < 1) + throw errort().with_location(type.source_location()) + << "word width must be 1 or larger"; + + type.id(ID_signedbv); + type.set(ID_width, integer2string(width)); + } + else if(type.id() == ID_smv_word || type.id() == ID_smv_unsigned_word) + { + auto width = numeric_cast_v( + to_constant_expr(static_cast(type.find(ID_width)))); + + if(width < 1) + throw errort().with_location(type.source_location()) + << "word width must be 1 or larger"; + + type.id(ID_unsignedbv); + type.set(ID_width, integer2string(width)); + } } /*******************************************************************\