diff --git a/CHANGELOG b/CHANGELOG index 81b911aba..0dc09ce68 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -3,6 +3,7 @@ * SystemVerilog: typedefs from package scopes * SystemVerilog: assignment patterns with keys for structs * SMV: LTL V operator, xnor operator +* SMV: word types and operators # EBMC 5.5 diff --git a/regression/smv/word/basic1.desc b/regression/smv/word/basic1.desc new file mode 100644 index 000000000..4602bcfab --- /dev/null +++ b/regression/smv/word/basic1.desc @@ -0,0 +1,9 @@ +CORE +basic1.smv +--bound 0 --trace +^ s1 = 0sd8_123 \(01111011\)$ +^ u1 = 0ud8_123 \(01111011\)$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/basic1.smv b/regression/smv/word/basic1.smv new file mode 100644 index 000000000..661466238 --- /dev/null +++ b/regression/smv/word/basic1.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR u1 : word[8]; + +ASSIGN u1 := uwconst(123, 8); + +VAR s1 : signed word[8]; + +ASSIGN s1 := swconst(123, 8); + +SPEC FALSE diff --git a/regression/smv/word/basic2.desc b/regression/smv/word/basic2.desc new file mode 100644 index 000000000..825184401 --- /dev/null +++ b/regression/smv/word/basic2.desc @@ -0,0 +1,8 @@ +CORE +basic2.smv +--bdd +^\[live\] G F counter = 0ud8_10: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/basic2.smv b/regression/smv/word/basic2.smv new file mode 100644 index 000000000..f5b1c6afe --- /dev/null +++ b/regression/smv/word/basic2.smv @@ -0,0 +1,8 @@ +MODULE main + +VAR counter : word[8]; + +ASSIGN init(counter) := uwconst(0, 8); +ASSIGN next(counter) := counter + uwconst(1, 8); + +LTLSPEC NAME live := G F counter = uwconst(10, 8) diff --git a/regression/smv/word/bitwise1.desc b/regression/smv/word/bitwise1.desc new file mode 100644 index 000000000..179df2d92 --- /dev/null +++ b/regression/smv/word/bitwise1.desc @@ -0,0 +1,14 @@ +CORE +bitwise1.smv + +^\[.*\] !0ud8_123 = 0ud8_132: PROVED$ +^\[.*\] !0sd8_123 = -0sd8_124: PROVED$ +^\[.*\] \(0ud8_123 \& 0ud8_7\) = 0ud8_3: PROVED$ +^\[.*\] \(0ud8_123 \| 0ud8_7\) = 0ud8_127: PROVED$ +^\[.*\] \(0ud8_123 xor 0ud8_7\) = 0ud8_124: PROVED$ +^\[.*\] \(0ud8_123 xnor 0ud8_7\) = 0ud8_131: PROVED$ +^\[.*\] \(0ud8_123 <-> 0ud8_7\) = 0ud8_131: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/bitwise1.smv b/regression/smv/word/bitwise1.smv new file mode 100644 index 000000000..77c462b0b --- /dev/null +++ b/regression/smv/word/bitwise1.smv @@ -0,0 +1,23 @@ +MODULE main + +-- negation +SPEC !uwconst(123, 8) = uwconst(132, 8) +SPEC !swconst(123, 8) = swconst(-124, 8) + +-- and +SPEC (uwconst(123, 8) & uwconst(7, 8)) = uwconst(3, 8) + +-- or +SPEC (uwconst(123, 8) | uwconst(7, 8)) = uwconst(127, 8) + +-- xor +SPEC (uwconst(123, 8) xor uwconst(7, 8)) = uwconst(124, 8) + +-- xnor +SPEC (uwconst(123, 8) xnor uwconst(7, 8)) = uwconst(131, 8) + +-- implication +--SPEC (uwconst(123, 8) -> uwconst(7, 8)) = uwconst(135, 8) + +-- iff +SPEC (uwconst(123, 8) <-> uwconst(7, 8)) = uwconst(131, 8) diff --git a/regression/smv/word/concat1.desc b/regression/smv/word/concat1.desc new file mode 100644 index 000000000..d1326406b --- /dev/null +++ b/regression/smv/word/concat1.desc @@ -0,0 +1,10 @@ +CORE +concat1.smv + +^\[.*\] 0ud8_123 :: 0ud8_1 = 0ud16_31489: PROVED$ +^\[.*\] 0sd8_123 :: 0sd8_1 = 0ud16_31489: PROVED$ +^\[.*\] 0sd8_123 :: 0ud8_1 = 0ud16_31489: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/concat1.smv b/regression/smv/word/concat1.smv new file mode 100644 index 000000000..6f441f443 --- /dev/null +++ b/regression/smv/word/concat1.smv @@ -0,0 +1,7 @@ +MODULE main + +SPEC uwconst(123, 8) :: uwconst(1, 8) = uwconst(31489, 16) + +-- concatenation is unsigned +SPEC swconst(123, 8) :: swconst(1, 8) = uwconst(31489, 16) +SPEC swconst(123, 8) :: uwconst(1, 8) = uwconst(31489, 16) diff --git a/regression/smv/word/extend1.desc b/regression/smv/word/extend1.desc new file mode 100644 index 000000000..6f2d13d6f --- /dev/null +++ b/regression/smv/word/extend1.desc @@ -0,0 +1,7 @@ +KNOWNBUG +extend1.smv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/extend1.smv b/regression/smv/word/extend1.smv new file mode 100644 index 000000000..3637ea4ec --- /dev/null +++ b/regression/smv/word/extend1.smv @@ -0,0 +1,4 @@ +MODULE main + +SPEC extend(uwconst(1, 1), 7) = uwconst(1, 8) +SPEC extend(swconst(-1, 1), 7) = swconst(-1, 8) diff --git a/regression/smv/word/extractbits1.desc b/regression/smv/word/extractbits1.desc new file mode 100644 index 000000000..106946ec4 --- /dev/null +++ b/regression/smv/word/extractbits1.desc @@ -0,0 +1,7 @@ +CORE +shift1.smv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/extractbits1.smv b/regression/smv/word/extractbits1.smv new file mode 100644 index 000000000..d28f33bb8 --- /dev/null +++ b/regression/smv/word/extractbits1.smv @@ -0,0 +1,8 @@ +MODULE main + +SPEC uwconst(123, 8)[0:0] = uwconst(1, 1) +SPEC uwconst(123, 8)[7:7] = uwconst(0, 1) + +-- always unsigned +SPEC swconst(123, 8)[0:0] = uwconst(1, 1) +SPEC swconst(123, 8)[7:7] = uwconst(0, 1) diff --git a/regression/smv/word/resize1.desc b/regression/smv/word/resize1.desc new file mode 100644 index 000000000..22fb92de0 --- /dev/null +++ b/regression/smv/word/resize1.desc @@ -0,0 +1,7 @@ +KNOWNBUG +resize1.smv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/resize1.smv b/regression/smv/word/resize1.smv new file mode 100644 index 000000000..70f4d7f7b --- /dev/null +++ b/regression/smv/word/resize1.smv @@ -0,0 +1,4 @@ +MODULE main + +SPEC resize(uwconst(1, 1), 8) = uwconst(1, 8) +SPEC resize(swconst(123, 1), 1) = swconst(-1, 1) diff --git a/regression/smv/word/shift1.desc b/regression/smv/word/shift1.desc new file mode 100644 index 000000000..60c54ff8d --- /dev/null +++ b/regression/smv/word/shift1.desc @@ -0,0 +1,19 @@ +CORE +shift1.smv + +^\[.*\] 0ud8_123 >> 0 = 0ud8_123: PROVED$ +^\[.*\] 0ud8_123 >> 1 = 0ud8_61: PROVED$ +^\[.*\] 0ud8_123 >> 8 = 0ud8_0: PROVED$ +^\[.*\] 0ud8_123 << 0 = 0ud8_123: PROVED$ +^\[.*\] 0ud8_123 << 1 = 0ud8_246: PROVED$ +^\[.*\] 0ud8_123 << 2 = 0ud8_236: PROVED$ +^\[.*\] 0sd8_123 >> 0 = 0sd8_123: PROVED$ +^\[.*\] 0sd8_123 >> 1 = 0sd8_61: PROVED$ +^\[.*\] 0sd8_123 >> 8 = 0sd8_0: PROVED$ +^\[.*\] 0sd8_123 << 0 = 0sd8_123: PROVED$ +^\[.*\] 0sd8_123 << 1 = -0sd8_10: PROVED$ +^\[.*\] 0sd8_123 << 2 = -0sd8_20: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/shift1.smv b/regression/smv/word/shift1.smv new file mode 100644 index 000000000..08c9c3577 --- /dev/null +++ b/regression/smv/word/shift1.smv @@ -0,0 +1,15 @@ +MODULE main + +SPEC uwconst(123, 8) >> 0 = uwconst(123, 8) +SPEC uwconst(123, 8) >> 1 = uwconst(61, 8) +SPEC uwconst(123, 8) >> 8 = uwconst(0, 8) +SPEC uwconst(123, 8) << 0 = uwconst(123, 8) +SPEC uwconst(123, 8) << 1 = uwconst(246, 8) +SPEC uwconst(123, 8) << 2 = uwconst(236, 8) + +SPEC swconst(123, 8) >> 0 = swconst(123, 8) +SPEC swconst(123, 8) >> 1 = swconst(61, 8) +SPEC swconst(123, 8) >> 8 = swconst(0, 8) +SPEC swconst(123, 8) << 0 = swconst(123, 8) +SPEC swconst(123, 8) << 1 = swconst(-10, 8) +SPEC swconst(123, 8) << 2 = swconst(-20, 8) diff --git a/regression/smv/word/signed1.desc b/regression/smv/word/signed1.desc new file mode 100644 index 000000000..bd9667771 --- /dev/null +++ b/regression/smv/word/signed1.desc @@ -0,0 +1,7 @@ +KNOWNBUG +signed1.smv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/signed1.smv b/regression/smv/word/signed1.smv new file mode 100644 index 000000000..c259caf8f --- /dev/null +++ b/regression/smv/word/signed1.smv @@ -0,0 +1,3 @@ +MODULE main + +SPEC signed(uwconst(1, 1)) = swconst(-1, 1) diff --git a/regression/smv/word/sizeof1.desc b/regression/smv/word/sizeof1.desc new file mode 100644 index 000000000..b92443ad6 --- /dev/null +++ b/regression/smv/word/sizeof1.desc @@ -0,0 +1,7 @@ +CORE +sizeof1.smv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/sizeof1.smv b/regression/smv/word/sizeof1.smv new file mode 100644 index 000000000..656b668e4 --- /dev/null +++ b/regression/smv/word/sizeof1.smv @@ -0,0 +1,4 @@ +MODULE main + +SPEC sizeof(uwconst(0, 1)) = 1 +SPEC sizeof(swconst(123, 8)) = 8 diff --git a/regression/smv/word/unsigned1.desc b/regression/smv/word/unsigned1.desc new file mode 100644 index 000000000..d06b7ac7f --- /dev/null +++ b/regression/smv/word/unsigned1.desc @@ -0,0 +1,7 @@ +KNOWNBUG +unsigned1.smv + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/smv/word/unsigned1.smv b/regression/smv/word/unsigned1.smv new file mode 100644 index 000000000..11070da30 --- /dev/null +++ b/regression/smv/word/unsigned1.smv @@ -0,0 +1,3 @@ +MODULE main + +SPEC unsigned(swconst(-1, 1)) = uwconst(1, 1) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 140ad3b0f..2169e98cc 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -17,12 +17,20 @@ IREP_ID_ONE(F) IREP_ID_ONE(E) IREP_ID_ONE(G) IREP_ID_ONE(X) +IREP_ID_ONE(smv_bitimplies) +IREP_ID_ONE(smv_extend) IREP_ID_ONE(smv_next) IREP_ID_ONE(smv_iff) IREP_ID_TWO(C_smv_iff, "#smv_iff") +IREP_ID_ONE(smv_resize) IREP_ID_ONE(smv_setin) IREP_ID_ONE(smv_setnotin) +IREP_ID_ONE(smv_signed_cast) +IREP_ID_ONE(smv_sizeof) +IREP_ID_ONE(smv_swconst) IREP_ID_ONE(smv_union) +IREP_ID_ONE(smv_unsigned_cast) +IREP_ID_ONE(smv_uwconst) IREP_ID_ONE(smv_H) IREP_ID_ONE(smv_bounded_H) IREP_ID_ONE(smv_O) diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp index 9cd6fc932..a41642fbf 100644 --- a/src/smvlang/expr2smv.cpp +++ b/src/smvlang/expr2smv.cpp @@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr2smv.h" +#include +#include #include #include #include @@ -114,7 +116,7 @@ class expr2smvt precedencet &precedence); bool convert_constant( - const exprt &src, + const constant_exprt &, std::string &dest, precedencet &precedence); @@ -508,14 +510,13 @@ Function: expr2smvt::convert_constant \*******************************************************************/ bool expr2smvt::convert_constant( - const exprt &src, + const constant_exprt &src, std::string &dest, precedencet &precedence) { precedence = precedencet::MAX; - const typet &type=src.type(); - const std::string &value=src.get_string(ID_value); + const typet &type = src.type(); if(type.id()==ID_bool) { @@ -528,7 +529,19 @@ bool expr2smvt::convert_constant( type.id()==ID_natural || type.id()==ID_range || type.id()==ID_enumeration) - dest=value; + { + dest = id2string(src.get_value()); + } + else if(type.id() == ID_signedbv || type.id() == ID_unsignedbv) + { + auto value_int = numeric_cast_v(src); + auto value_abs = value_int < 0 ? -value_int : value_int; + auto minus = value_int < 0 ? "-" : ""; + auto sign_specifier = type.id() == ID_signedbv ? 's' : 'u'; + auto word_width = to_bitvector_type(type).width(); + dest = minus + std::string("0") + sign_specifier + 'd' + + std::to_string(word_width) + '_' + integer2string(value_abs); + } else return convert_norep(src, dest, precedence); @@ -611,20 +624,25 @@ bool expr2smvt::convert( return convert_unary( to_not_expr(src), dest, "!", precedence = precedencet::NOT); - else if(src.id()==ID_and) + else if(src.id() == ID_and || src.id() == ID_bitand) return convert_binary(src, dest, "&", precedence = precedencet::AND); - else if(src.id()==ID_or) + else if(src.id() == ID_or || src.id() == ID_bitor) return convert_binary(src, dest, "|", precedence = precedencet::OR); - else if(src.id()==ID_implies) + else if(src.id() == ID_implies || src.id() == ID_smv_bitimplies) return convert_binary(src, dest, "->", precedence = precedencet::IMPLIES); - else if(src.id() == ID_xor) + else if(src.id() == ID_xor || src.id() == ID_bitxor) return convert_binary(src, dest, "xor", precedence = precedencet::OR); - else if(src.id() == ID_xnor) - return convert_binary(src, dest, "xnor", precedence = precedencet::OR); + else if(src.id() == ID_xnor || src.id() == ID_bitxnor) + { + if(src.get_bool(ID_C_smv_iff)) + return convert_binary(src, dest, "<->", precedence = precedencet::IFF); + else + return convert_binary(src, dest, "xnor", precedence = precedencet::OR); + } else if( src.id() == ID_AG || src.id() == ID_EG || src.id() == ID_AF || @@ -716,7 +734,7 @@ bool expr2smvt::convert( return convert_next_symbol(src, dest, precedence); else if(src.id()==ID_constant) - return convert_constant(src, dest, precedence); + return convert_constant(to_constant_expr(src), dest, precedence); else if(src.id()=="smv_nondet_choice") return convert_nondet_choice(src, dest, precedence); @@ -736,6 +754,24 @@ bool expr2smvt::convert( else if(src.id()==ID_cond) return convert_cond(src, dest); + else if(src.id() == ID_concatenation) + { + return convert_binary( + to_binary_expr(src), dest, "::", precedence = precedencet::CONCAT); + } + + else if(src.id() == ID_shl) + { + return convert_binary( + to_binary_expr(src), dest, "<<", precedence = precedencet::SHIFT); + } + + else if(src.id() == ID_lshr || src.id() == ID_ashr) + { + return convert_binary( + to_binary_expr(src), dest, ">>", precedence = precedencet::SHIFT); + } + else // no SMV language expression for internal representation return convert_norep(src, dest, precedence); @@ -838,6 +874,16 @@ bool type2smv(const typet &type, std::string &code, const namespacet &ns) code+=')'; } } + else if(type.id() == ID_signedbv) + { + code = + "signed word[" + std::to_string(to_signedbv_type(type).width()) + ']'; + } + else if(type.id() == ID_unsignedbv) + { + code = + "unsigned word[" + std::to_string(to_unsignedbv_type(type).width()) + ']'; + } else return true; diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index 946de69f2..a5e2bd76b 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -264,6 +264,8 @@ static void new_module(YYSTYPE &module) %token LT_Token "<" %token GT_Token ">" %token NOTEQUAL_Token "!=" +%token LTLT_Token "<<" +%token GTGT_Token ">>" %token INC_Token %token DEC_Token @@ -289,8 +291,10 @@ static void new_module(YYSTYPE &module) %left union_Token %left IN_Token NOTIN_Token %left mod_Token /* Precedence from CMU SMV, different from NuSMV */ +%left LTLT_Token GTGT_Token %left PLUS_Token MINUS_Token %left TIMES_Token DIVIDE_Token +%left COLONCOLON_Token %left UMINUS /* supplies precedence for unary minus */ %left DOT_Token @@ -476,6 +480,21 @@ simple_type_specifier: stack_type($$).add_subtype()=stack_type($6); } | boolean_Token { init($$, ID_bool); } + | word_Token '[' NUMBER_Token ']' + { + init($$, ID_unsignedbv); + stack_type($$).set(ID_width, stack_expr($3).id()); + } + | signed_Token word_Token '[' NUMBER_Token ']' + { + init($$, ID_signedbv); + stack_type($$).set(ID_width, stack_expr($4).id()); + } + | unsigned_Token word_Token '[' NUMBER_Token ']' + { + init($$, ID_unsignedbv); + stack_type($$).set(ID_width, stack_expr($4).id()); + } | '{' enum_list '}' { $$=$2; } | NUMBER_Token DOTDOT_Token NUMBER_Token { @@ -669,6 +688,9 @@ term : variable_name | MINUS_Token term %prec UMINUS { init($$, ID_unary_minus); mto($$, $2); } | term mod_Token term { binary($$, $1, ID_mod, $3); } + | term GTGT_Token term { binary($$, $1, ID_shr, $3); } + | term LTLT_Token term { binary($$, $1, ID_shl, $3); } + | term COLONCOLON_Token term { binary($$, $1, ID_concatenation, $3); } | term TIMES_Token term { binary($$, $1, ID_mult, $3); } | term DIVIDE_Token term { binary($$, $1, ID_div, $3); } | term PLUS_Token term { binary($$, $1, ID_plus, $3); } @@ -680,6 +702,23 @@ term : variable_name | term OR_Token term { j_binary($$, $1, ID_or, $3); } | term AND_Token term { j_binary($$, $1, ID_and, $3); } | NOT_Token term { init($$, ID_not); mto($$, $2); } + | term EQUAL_Token term { binary($$, $1, ID_equal, $3); } + | term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); } + | term LT_Token term { binary($$, $1, ID_lt, $3); } + | term LE_Token term { binary($$, $1, ID_le, $3); } + | term GT_Token term { binary($$, $1, ID_gt, $3); } + | term GE_Token term { binary($$, $1, ID_ge, $3); } + | term union_Token term { binary($$, $1, ID_smv_union, $3); } + | term IN_Token term { binary($$, $1, ID_smv_setin, $3); } + | term NOTIN_Token term { binary($$, $1, ID_smv_setnotin, $3); } + | extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); } + | resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); } + | signed_Token '(' term ')' { init($$, ID_smv_signed_cast); mto($$, $3); } + | sizeof_Token '(' term ')' { init($$, ID_smv_sizeof); mto($$, $3); } + | swconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_swconst, $5); } + | unsigned_Token '(' term ')' { init($$, ID_smv_unsigned_cast); mto($$, $3); } + | uwconst_Token '(' term ',' term ')' { binary($$, $3, ID_smv_uwconst, $5); } + /* CTL */ | AX_Token term { init($$, ID_AX); mto($$, $2); } | AF_Token term { init($$, ID_AF); mto($$, $2); } | AG_Token term { init($$, ID_AG); mto($$, $2); } @@ -690,21 +729,13 @@ term : variable_name | A_Token '[' term R_Token term ']' { binary($$, $3, ID_AR, $5); } | E_Token '[' term U_Token term ']' { binary($$, $3, ID_EU, $5); } | E_Token '[' term R_Token term ']' { binary($$, $3, ID_ER, $5); } + /* LTL */ | F_Token term { init($$, ID_F); mto($$, $2); } | G_Token term { init($$, ID_G); mto($$, $2); } | X_Token term { init($$, ID_X); mto($$, $2); } | term U_Token term { binary($$, $1, ID_U, $3); } | term R_Token term { binary($$, $1, ID_R, $3); } | term V_Token term { binary($$, $1, ID_R, $3); } - | term EQUAL_Token term { binary($$, $1, ID_equal, $3); } - | term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); } - | term LT_Token term { binary($$, $1, ID_lt, $3); } - | term LE_Token term { binary($$, $1, ID_le, $3); } - | term GT_Token term { binary($$, $1, ID_gt, $3); } - | term GE_Token term { binary($$, $1, ID_ge, $3); } - | term union_Token term { binary($$, $1, ID_smv_union, $3); } - | term IN_Token term { binary($$, $1, ID_smv_setin, $3); } - | term NOTIN_Token term { binary($$, $1, ID_smv_setnotin, $3); } /* LTL PAST */ | Y_Token term { $$ = $1; stack_expr($$).id(ID_smv_Y); mto($$, $2); } | Z_Token term { $$ = $1; stack_expr($$).id(ID_smv_Z); mto($$, $2); } diff --git a/src/smvlang/scanner.l b/src/smvlang/scanner.l index 518ce8c2d..5de6861ab 100644 --- a/src/smvlang/scanner.l +++ b/src/smvlang/scanner.l @@ -203,6 +203,8 @@ void newlocation(YYSTYPE &x) "|" return OR_Token; "&" return AND_Token; "->" return IMPLIES_Token; +">>" return GTGT_Token; +"<<" return LTLT_Token; "<->" return EQUIV_Token; "=" return EQUAL_Token; "<=" return LE_Token; @@ -213,6 +215,7 @@ void newlocation(YYSTYPE &x) ":=" return BECOMES_Token; "." return DOT_Token; ".." return DOTDOT_Token; +"::" return COLONCOLON_Token; . return yytext[0]; diff --git a/src/smvlang/smv_range.h b/src/smvlang/smv_range.h index c9e60fdb3..4da6b09d3 100644 --- a/src/smvlang/smv_range.h +++ b/src/smvlang/smv_range.h @@ -73,6 +73,12 @@ class smv_ranget return {from - other.from, to - other.to}; } + // unary minus + smv_ranget operator-() const + { + return {-to, -from}; + } + smv_ranget operator*(const smv_ranget &other) const { mp_integer p1 = from * other.from; diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 09c0aefb0..c1ed26f3a 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "smv_typecheck.h" #include +#include #include #include #include @@ -565,7 +566,15 @@ typet smv_typecheckt::type_union( if(type2.is_nil()) return type1; - + + if( + type1.id() == ID_signedbv || type1.id() == ID_unsignedbv || + type2.id() == ID_signedbv || type2.id() == ID_unsignedbv) + { + throw errort() << "no type union for types" << to_string(type1) << " and " + << to_string(type2); + } + // both enums? if(type1.id()==ID_enumeration && type2.id()==ID_enumeration) { @@ -698,28 +707,73 @@ void smv_typecheckt::typecheck_expr_rec( } else if( expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_xor || - expr.id() == ID_xnor || expr.id() == ID_not || expr.id() == ID_implies) + expr.id() == ID_xnor || expr.id() == ID_not || expr.id() == ID_implies || + expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_bitxor || + expr.id() == ID_bitxnor || expr.id() == ID_bitnot || + expr.id() == ID_smv_bitimplies) { + PRECONDITION(!expr.operands().empty()); + for(auto &op : expr.operands()) typecheck_expr_rec(op, mode); - expr.type() = bool_typet{}; + auto &op0_type = to_multi_ary_expr(expr).op0().type(); + + // boolean or bit-wise? + if(op0_type.id() == ID_signedbv || op0_type.id() == ID_unsignedbv) + { + auto new_id = irep_idt(); + + if(expr.id() == ID_and) + new_id = ID_bitand; + else if(expr.id() == ID_or) + new_id = ID_bitor; + else if(expr.id() == ID_xor) + new_id = ID_bitxor; + else if(expr.id() == ID_xnor) + new_id = ID_bitxnor; + else if(expr.id() == ID_not) + new_id = ID_bitnot; + else if(expr.id() == ID_implies) + new_id = ID_smv_bitimplies; + else + new_id = expr.id(); + + expr.id(new_id); + + expr.type() = op0_type; + } + else + { + expr.type() = bool_typet{}; + } for(auto &op : expr.operands()) convert_expr_to(op, expr.type()); } else if(expr.id() == ID_smv_iff) { - for(auto &op : expr.operands()) - typecheck_expr_rec(op, mode); - - expr.type() = bool_typet{}; + auto &binary_expr = to_binary_expr(expr); + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); - for(auto &op : expr.operands()) - convert_expr_to(op, expr.type()); + auto &op0_type = binary_expr.op0().type(); - expr.set(ID_C_smv_iff, true); - expr.id(ID_equal); + if(op0_type.id() == ID_signedbv || op0_type.id() == ID_unsignedbv) + { + expr.set(ID_C_smv_iff, true); + expr.id(ID_bitxnor); + convert_expr_to(binary_expr.rhs(), op0_type); + expr.type() = op0_type; + } + else + { + expr.type() = bool_typet{}; + convert_expr_to(binary_expr.lhs(), expr.type()); + convert_expr_to(binary_expr.rhs(), expr.type()); + expr.set(ID_C_smv_iff, true); + expr.id(ID_equal); + } } else if(expr.id()==ID_constraint_select_one) { @@ -766,7 +820,9 @@ void smv_typecheckt::typecheck_expr_rec( if(expr.id()==ID_lt || expr.id()==ID_le || expr.id()==ID_gt || expr.id()==ID_ge) { - if(op0.type().id()!=ID_range) + if( + op0.type().id() != ID_range && op0.type().id() != ID_signedbv && + op0.type().id() != ID_unsignedbv) { throw errort().with_location(expr.find_source_location()) << "Expected number type for " << to_string(expr); @@ -823,7 +879,9 @@ void smv_typecheckt::typecheck_expr_rec( expr.type() = new_range.to_type(); } } - else if(dest_type.id() != ID_range) + else if( + dest_type.id() != ID_range && dest_type.id() != ID_signedbv && + dest_type.id() != ID_unsignedbv) { throw errort().with_location(expr.find_source_location()) << "Expected number type for " << to_string(expr); @@ -1063,6 +1121,225 @@ void smv_typecheckt::typecheck_expr_rec( { expr.type()=bool_typet(); } + else if(expr.id() == ID_unary_minus) + { + auto &uminus_expr = to_unary_minus_expr(expr); + typecheck_expr_rec(uminus_expr.op(), mode); + auto &op_type = uminus_expr.op().type(); + + if(op_type.id() == ID_range) + { + uminus_expr.type() = + (-smv_ranget::from_type(to_range_type(op_type))).to_type(); + } + else + throw errort().with_location(expr.source_location()) + << "Operand to unary minus must be integer, but got " + << to_string(op_type); + + // constant folding + if(uminus_expr.op().is_constant()) + expr = from_integer( + -numeric_cast_v(to_constant_expr(uminus_expr.op())), + uminus_expr.type()); + } + else if(expr.id() == ID_smv_swconst) + { + auto &binary_expr = to_binary_expr(expr); + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); + PRECONDITION(binary_expr.lhs().is_constant()); + PRECONDITION(binary_expr.rhs().is_constant()); + auto bits = numeric_cast_v(to_constant_expr(binary_expr.rhs())); + auto type = signedbv_typet{bits}; + auto value = + numeric_cast_v(to_constant_expr(binary_expr.lhs())); + expr = + from_integer(value, type).with_source_location(expr.source_location()); + } + else if(expr.id() == ID_smv_uwconst) + { + auto &binary_expr = to_binary_expr(expr); + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); + PRECONDITION(binary_expr.lhs().is_constant()); + PRECONDITION(binary_expr.rhs().is_constant()); + auto bits = numeric_cast_v(to_constant_expr(binary_expr.rhs())); + auto type = unsignedbv_typet{bits}; + auto value = + numeric_cast_v(to_constant_expr(binary_expr.lhs())); + expr = + from_integer(value, type).with_source_location(expr.source_location()); + } + else if( + expr.id() == ID_shr || expr.id() == ID_shl || expr.id() == ID_lshr || + expr.id() == ID_ashr) + { + auto &binary_expr = to_binary_expr(expr); + + // The LHS must be a word type. + typecheck_expr_rec(binary_expr.lhs(), mode); + + binary_expr.type() = binary_expr.lhs().type(); + + if(binary_expr.type().id() == ID_signedbv) + { + if(expr.id() == ID_shr) + expr.id(ID_ashr); + } + else if(binary_expr.type().id() == ID_unsignedbv) + { + if(expr.id() == ID_shr) + expr.id(ID_lshr); + } + else + { + throw errort().with_location(expr.find_source_location()) + << "Shift operand must be word type"; + } + + // The RHS must be an integer constant + typecheck_expr_rec(binary_expr.rhs(), mode); + + if( + binary_expr.rhs().type().id() != ID_range && + binary_expr.rhs().type().id() != ID_natural) + throw errort().with_location(expr.find_source_location()) + << "Shift distance must be integer, but got " + << to_string(binary_expr.rhs().type()); + + if(binary_expr.rhs().id() != ID_constant) + throw errort().with_location(expr.find_source_location()) + << "Shift distance must be constant"; + + // distance must be 0...w, where w is the number of bits of the LHS + auto distance = + numeric_cast_v(to_constant_expr(binary_expr.rhs())); + + if(distance < 0) + throw errort().with_location(expr.find_source_location()) + << "Shift distance must not be negative"; + + auto bits = to_bitvector_type(binary_expr.type()).get_width(); + + if(distance > bits) + throw errort().with_location(expr.find_source_location()) + << "Shift distance is too large"; + + binary_expr.rhs() = + from_integer(distance, natural_typet{}) + .with_source_location(binary_expr.rhs().source_location()); + } + else if(expr.id() == ID_concatenation) + { + auto &binary_expr = to_binary_expr(expr); + + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); + + if( + binary_expr.lhs().type().id() != ID_signedbv && + binary_expr.lhs().type().id() != ID_unsignedbv) + { + throw errort().with_location(expr.find_source_location()) + << "Concatenation operand must have word type"; + } + + if( + binary_expr.rhs().type().id() != ID_signedbv && + binary_expr.rhs().type().id() != ID_unsignedbv) + { + throw errort().with_location(expr.find_source_location()) + << "Concatenation operand must have word type"; + } + + auto bits = to_bitvector_type(binary_expr.lhs().type()).get_width() + + to_bitvector_type(binary_expr.rhs().type()).get_width(); + + binary_expr.type() = unsignedbv_typet{bits}; + } + else if(expr.id() == ID_smv_sizeof) + { + auto &op = to_unary_expr(expr).op(); + typecheck_expr_rec(op, mode); + if(op.type().id() == ID_signedbv || op.type().id() == ID_unsignedbv) + { + auto bits = to_bitvector_type(op.type()).get_width(); + expr = from_integer(bits, range_typet{bits, bits}); + } + else + { + throw errort().with_location(expr.find_source_location()) + << "sizeof operand must have word type"; + } + } + else if(expr.id() == ID_smv_resize) + { + auto &binary_expr = to_binary_expr(expr); + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); + PRECONDITION(binary_expr.rhs().is_constant()); + auto &lhs_type = binary_expr.lhs().type(); + auto new_bits = + numeric_cast_v(to_constant_expr(binary_expr.rhs())); + + if(lhs_type.id() == ID_signedbv) + expr.type() = signedbv_typet{new_bits}; + else if(lhs_type.id() == ID_unsignedbv) + expr.type() = unsignedbv_typet{new_bits}; + else + { + throw errort().with_location(expr.find_source_location()) + << "resize operand must have word type"; + } + } + else if(expr.id() == ID_smv_extend) + { + auto &binary_expr = to_binary_expr(expr); + typecheck_expr_rec(binary_expr.lhs(), mode); + typecheck_expr_rec(binary_expr.rhs(), mode); + PRECONDITION(binary_expr.rhs().is_constant()); + auto &lhs_type = binary_expr.lhs().type(); + auto old_bits = to_bitvector_type(lhs_type).get_width(); + auto new_bits = old_bits + numeric_cast_v( + to_constant_expr(binary_expr.rhs())); + + if(lhs_type.id() == ID_signedbv) + expr.type() = signedbv_typet{new_bits}; + else if(lhs_type.id() == ID_unsignedbv) + expr.type() = unsignedbv_typet{new_bits}; + else + { + throw errort().with_location(expr.find_source_location()) + << "extend operand must have word type"; + } + } + else if(expr.id() == ID_smv_unsigned_cast) + { + // a reinterpret cast + auto &op = to_unary_expr(expr).op(); + typecheck_expr_rec(op, mode); + if(op.type().id() == ID_signedbv) + expr.type() = unsignedbv_typet{to_signedbv_type(op.type()).get_width()}; + else + { + throw errort().with_location(expr.find_source_location()) + << "unsigned operand must have signed word type"; + } + } + else if(expr.id() == ID_smv_signed_cast) + { + // a reinterpret cast + auto &op = to_unary_expr(expr).op(); + typecheck_expr_rec(op, mode); + if(op.type().id() == ID_unsignedbv) + expr.type() = signedbv_typet{to_unsignedbv_type(op.type()).get_width()}; + else + { + throw errort().with_location(expr.find_source_location()) + << "signed operand must have unsigned word type"; + } + } else { throw errort().with_location(expr.find_source_location()) @@ -1091,30 +1368,36 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type) if(expr.type() != type) { - smv_ranget e=convert_type(expr.type()); - smv_ranget t=convert_type(type); - - if(e.is_contained_in(t) && expr.type().id() != ID_enumeration) + if(type.id() == ID_signedbv || type.id() == ID_unsignedbv) + { + } + else { - if(e.is_singleton()) + smv_ranget e = convert_type(expr.type()); + smv_ranget t = convert_type(type); + + if(e.is_contained_in(t) && expr.type().id() != ID_enumeration) { - if(type.id()==ID_bool) + if(e.is_singleton()) { - if(e.from==0) - expr=false_exprt(); + if(type.id() == ID_bool) + { + if(e.from == 0) + expr = false_exprt(); + else + expr = true_exprt(); + } else - expr=true_exprt(); + { + expr = exprt(ID_constant, type); + expr.set(ID_value, integer2string(e.from)); + } } else - { - expr=exprt(ID_constant, type); - expr.set(ID_value, integer2string(e.from)); - } - } - else - expr = typecast_exprt{expr, type}; + expr = typecast_exprt{expr, type}; - return; + return; + } } throw errort().with_location(expr.find_source_location())