diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp index 2981504db..7a7923ab5 100644 --- a/src/smvlang/expr2smv.cpp +++ b/src/smvlang/expr2smv.cpp @@ -188,6 +188,32 @@ expr2smvt::resultt expr2smvt::convert_binary_associative( /*******************************************************************\ +Function: expr2smvt::convert_extractbits + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +expr2smvt::resultt expr2smvt::convert_extractbits(const extractbits_exprt &expr) +{ + // we can do constant indices only + if(!expr.index().is_constant()) + return convert_norep(expr); + + auto op_rec = convert_rec(expr.src()); + auto high_s = integer2string( + numeric_cast_v(to_constant_expr(expr.index())) + + to_bitvector_type(expr.type()).width() - 1); + auto low_s = convert_rec(expr.index()).s; + return {precedencet::INDEX, op_rec.s + '[' + high_s + ':' + low_s + ']'}; +} + +/*******************************************************************\ + Function: expr2smvt::convert_function_application Inputs: @@ -834,6 +860,9 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src) else if(src.id() == ID_smv_unsigned_cast) return convert_function_application("unsigned", src); + else if(src.id() == ID_extractbits) + return convert_extractbits(to_extractbits_expr(src)); + else if(src.id() == ID_typecast) { return convert_typecast(to_typecast_expr(src)); diff --git a/src/smvlang/expr2smv_class.h b/src/smvlang/expr2smv_class.h index 10a1c7ab6..3082be2a2 100644 --- a/src/smvlang/expr2smv_class.h +++ b/src/smvlang/expr2smv_class.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, dkr@amazon.com #define CPROVER_SMV_EXPR2SMV_CLASS_H #include +#include #include #include #include @@ -123,6 +124,8 @@ class expr2smvt resultt convert_cond(const exprt &); + resultt convert_extractbits(const extractbits_exprt &); + resultt convert_function_application(const std::string &symbol, const exprt &); diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index a72947c1d..93b27e4f3 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -297,6 +297,7 @@ static void new_module(YYSTYPE &module) %left COLONCOLON_Token %left UMINUS /* supplies precedence for unary minus */ %left DOT_Token +%nonassoc '[' %% @@ -690,6 +691,8 @@ term : variable_identifier | 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 '[' NUMBER_Token ',' NUMBER_Token ']' // bit selection + { init($$, ID_extractbits); mto($$, $1); mto($$, $3); mto($$, $5); } | 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); }