diff --git a/CHANGELOG b/CHANGELOG index de26baf5b..414302293 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,7 @@ +# EBMC 5.9 + +* SMV: word constants + # EBMC 5.8 * AIG/netlist engine: fix for conversion of extract bits operator diff --git a/regression/smv/word/word_constants1.desc b/regression/smv/word/word_constants1.desc new file mode 100644 index 000000000..1313aeb6f --- /dev/null +++ b/regression/smv/word/word_constants1.desc @@ -0,0 +1,7 @@ +CORE +word_constants1.smv +--bound 0 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/word_constants1.smv b/regression/smv/word/word_constants1.smv new file mode 100644 index 000000000..26a48f971 --- /dev/null +++ b/regression/smv/word/word_constants1.smv @@ -0,0 +1,18 @@ +MODULE main + +SPEC uwconst(123, 8) = 0d8_123; +SPEC uwconst(123, 8) = 0ud8_123; +SPEC uwconst(123, 8) = 0h_7b; +SPEC uwconst(123, 8) = 0uh_7b; +SPEC uwconst(123, 8) = 0o8_173; +SPEC uwconst(123, 8) = 0uo8_173; +SPEC uwconst(123, 8) = 0b_01111011; +SPEC uwconst(123, 8) = 0ub_01111011; +SPEC uwconst(123, 8) = 0b8_1111011; +SPEC uwconst(123, 8) = 0ub8_1111011; + +SPEC swconst(123, 8) = 0sd8_123; +SPEC swconst(123, 8) = 0sh_7b; +SPEC swconst(123, 8) = 0so8_173; +SPEC swconst(123, 8) = 0sb_01111011; +SPEC swconst(123, 8) = 0sb8_1111011; diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 87ca0a2a7..fcfca60c2 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -41,6 +41,7 @@ IREP_ID_ONE(smv_union) IREP_ID_ONE(smv_unsigned_cast) IREP_ID_ONE(smv_uwconst) IREP_ID_ONE(smv_word1) +IREP_ID_ONE(smv_word_constant) IREP_ID_ONE(smv_H) IREP_ID_ONE(smv_bounded_H) IREP_ID_ONE(smv_O) diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index 31f0973f6..d876587d1 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -320,8 +320,9 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &module_name) %token IDENTIFIER_Token "identifier" %token QIDENTIFIER_Token "quoted identifier" -%token STRING_Token "quoted string" +%token STRING_Token "quoted string" %token NUMBER_Token "number" +%token WORD_CONSTANT_Token "word constant" /* operator precedence, low to high */ %right IMPLIES_Token @@ -815,6 +816,7 @@ formula : basic_expr constant : boolean_constant | integer_constant + | word_constant ; boolean_constant: @@ -841,6 +843,15 @@ integer_constant: } ; +word_constant: + WORD_CONSTANT_Token + { + init($$, ID_constant); + stack_expr($$).set(ID_value, stack_expr($1).id()); + stack_expr($$).type() = typet{ID_smv_word_constant}; + } + ; + basic_expr : constant | identifier { diff --git a/src/smvlang/scanner.l b/src/smvlang/scanner.l index 289115877..e3281493a 100644 --- a/src/smvlang/scanner.l +++ b/src/smvlang/scanner.l @@ -188,6 +188,11 @@ void newlocation(YYSTYPE &x) stack_expr(yysmvlval).id(yytext); return NUMBER_Token; } +0[us]?[bBoOdDhH][0-9]*_[0-9a-fA-F][_0-9a-fA-F]* { + newstack(yysmvlval); + stack_expr(yysmvlval).id(yytext); + return WORD_CONSTANT_Token; + } \"[^\"]*\" { newstack(yysmvlval); std::string tmp(yytext); diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 170e3a40e..7312d9796 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -90,6 +90,7 @@ class smv_typecheckt:public typecheckt void typecheck(smv_parse_treet::modulet::itemt &); void typecheck_expr_rec(exprt &, modet); void convert_expr_to(exprt &, const typet &dest); + exprt convert_word_constant(const constant_exprt &); smv_parse_treet::modulet *modulep; @@ -582,6 +583,123 @@ void smv_typecheckt::typecheck(exprt &expr, modet mode) /*******************************************************************\ +Function: convert_word_constant + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +exprt smv_typecheckt::convert_word_constant(const constant_exprt &src_expr) +{ + auto &src = id2string(src_expr.get_value()); + + DATA_INVARIANT(src[0] == '0', "word constant grammar"); + + std::size_t index = 1; + bool is_signed = false; + + DATA_INVARIANT(index < src.size(), "word constant length"); + + switch(src[index]) + { + case 's': + case 'S': + is_signed = true; + index++; + break; + + case 'u': + case 'U': + // this is the default + index++; + break; + + default:; + } + + DATA_INVARIANT(index < src.size(), "word constant length"); + + unsigned base; + switch(src[index]) + { + case 'd': + case 'D': + base = 10; + break; + + case 'h': + case 'H': + base = 16; + break; + + case 'b': + case 'B': + base = 2; + break; + + case 'o': + case 'O': + base = 8; + break; + + default: + DATA_INVARIANT(false, "word constant base"); + } + + index++; + + DATA_INVARIANT(index < src.size(), "word constant length"); + + std::optional bits = {}; + + // optional number of bits + if(isdigit(src[index])) + { + std::string bits_str; + for(; index < src.size() && isdigit(src[index]); index++) + { + bits_str += src[index]; + } + + bits = string2integer(bits_str); + } + + std::string digits; + digits.reserve(src.size()); + + for(; index < src.size(); index++) + { + if(src[index] != '_') + digits.push_back(src[index]); + } + + if(!bits.has_value()) + { + if(base == 10) + throw errort{}.with_location(src_expr.source_location()) + << "decimal word constant without width"; + else if(base == 2) + bits = digits.size(); + else if(base == 8) + bits = digits.size() * 3; + else if(base == 16) + bits = digits.size() * 4; + } + + auto digits_int = string2integer(digits, base); + + auto type = + bitvector_typet{is_signed ? ID_signedbv : ID_unsignedbv, bits.value()}; + + return from_integer(digits_int, type).with_source_location(src_expr); +} + +/*******************************************************************\ + Function: smv_typecheckt::typecheck_expr_rec Inputs: @@ -845,6 +963,11 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode) { // good as is } + else if(type.id() == ID_smv_word_constant) + { + // turn into signedbv/unsignedbv + expr = convert_word_constant(to_constant_expr(expr)); + } else { PRECONDITION(false);