diff --git a/regression/smv/expressions/smv_set2.desc b/regression/smv/expressions/smv_set2.desc index ddf89fab9..3c2c347e7 100644 --- a/regression/smv/expressions/smv_set2.desc +++ b/regression/smv/expressions/smv_set2.desc @@ -1,10 +1,10 @@ -KNOWNBUG +CORE broken-smt-backend smv_set2.smv ---bdd -^\[spec1\] x in my_set: PROVED$ -^EXIT=0$ + +^\[spec1\] x in \{ 1, 2 \}: REFUTED$ +^\[spec2\] x in 1 \| x in 2: REFUTED$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -The smv_setin operator is not implemented. diff --git a/regression/smv/expressions/smv_set2.smv b/regression/smv/expressions/smv_set2.smv index 74ecc0f17..0f304289d 100644 --- a/regression/smv/expressions/smv_set2.smv +++ b/regression/smv/expressions/smv_set2.smv @@ -1,9 +1,10 @@ MODULE main -DEFINE my_set := {1, 2}; - VAR x : 1..3; ASSIGN init(x) := {1, 2, 3}; next(x) := x; -SPEC x in my_set; +SPEC x in {1, 2}; + +-- the rhs set can be a singleton +SPEC (x in 1) | (x in 2); diff --git a/regression/smv/expressions/smv_set3.desc b/regression/smv/expressions/smv_set3.desc new file mode 100644 index 000000000..c4d321222 --- /dev/null +++ b/regression/smv/expressions/smv_set3.desc @@ -0,0 +1,10 @@ +KNOWNBUG +smv_set3.smv +--bdd +^\[spec1\] x in my_set: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +The smv_setin operator does not work with symbols on the RHS. diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 7276033c0..8769bea75 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -23,6 +23,7 @@ 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_set) IREP_ID_ONE(smv_setin) IREP_ID_ONE(smv_setnotin) IREP_ID_ONE(smv_signed_cast) diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp index 4084848a6..8ab58b3e7 100644 --- a/src/smvlang/expr2smv.cpp +++ b/src/smvlang/expr2smv.cpp @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ -Function: expr2smvt::convert_nondet_choice +Function: expr2smvt::convert_smv_set Inputs: @@ -25,7 +25,7 @@ Function: expr2smvt::convert_nondet_choice \*******************************************************************/ -expr2smvt::resultt expr2smvt::convert_nondet_choice(const exprt &src) +expr2smvt::resultt expr2smvt::convert_smv_set(const exprt &src) { std::string dest = "{ "; @@ -656,6 +656,9 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src) else if(src.id() == ID_mod) return convert_binary(to_mod_expr(src), src.id_string(), precedencet::MULT); + else if(src.id() == ID_smv_set) + return convert_smv_set(src); + else if(src.id() == ID_smv_setin) return convert_binary(to_binary_expr(src), "in", precedencet::IN); @@ -788,19 +791,13 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src) else if(src.id()==ID_constant) return convert_constant(to_constant_expr(src)); - else if(src.id()=="smv_nondet_choice") - return convert_nondet_choice(src); - - else if(src.id() == ID_constraint_select_one) - return convert_nondet_choice(src); - else if(src.id()==ID_nondet_bool) { - exprt nondet_choice_expr("smv_nondet_choice"); - nondet_choice_expr.operands().clear(); - nondet_choice_expr.operands().push_back(false_exprt()); - nondet_choice_expr.operands().push_back(true_exprt()); - return convert_nondet_choice(nondet_choice_expr); + exprt smv_set_expr(ID_smv_set); + smv_set_expr.operands().clear(); + smv_set_expr.operands().push_back(false_exprt()); + smv_set_expr.operands().push_back(true_exprt()); + return convert_smv_set(smv_set_expr); } else if(src.id()==ID_cond) @@ -902,6 +899,10 @@ std::string type2smv(const typet &type, const namespacet &ns) { return type.get_string(ID_from) + ".." + type.get_string(ID_to); } + else if(type.id() == ID_smv_set) + { + return "set"; + } else if(type.id()=="submodule") { auto code = type.get_string(ID_identifier); diff --git a/src/smvlang/expr2smv_class.h b/src/smvlang/expr2smv_class.h index 10a1c7ab6..caed6efde 100644 --- a/src/smvlang/expr2smv_class.h +++ b/src/smvlang/expr2smv_class.h @@ -85,7 +85,7 @@ class expr2smvt virtual resultt convert_rec(const exprt &); - resultt convert_nondet_choice(const exprt &); + resultt convert_smv_set(const exprt &); resultt convert_binary( const binary_exprt &src, diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index 04ee871a0..f6c298e50 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -176,7 +176,6 @@ static void new_module(YYSTYPE &module) %token LTLWFF_Token "LTLWFF" %token PSLWFF_Token "PSLWFF" %token COMPWFF_Token "COMPWFF" -%token IN_Token "IN" %token MIN_Token "MIN" %token MAX_Token "MAX" %token MIRROR_Token "MIRROR" @@ -289,7 +288,7 @@ static void new_module(YYSTYPE &module) %left EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token U_Token R_Token V_Token F_Token G_Token H_Token O_Token S_Token T_Token X_Token Y_Token Z_Token EBF_Token ABF_Token EBG_Token ABG_Token %left EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token %left union_Token -%left IN_Token NOTIN_Token +%left in_Token %left mod_Token /* Precedence from CMU SMV, different from NuSMV */ %left LTLT_Token GTGT_Token %left PLUS_Token MINUS_Token @@ -673,7 +672,7 @@ formula : term term : variable_identifier | next_Token '(' term ')' { init($$, ID_smv_next); mto($$, $3); } | '(' formula ')' { $$=$2; } - | '{' formula_list '}' { $$=$2; stack_expr($$).id("smv_nondet_choice"); } + | '{' formula_list '}' { $$=$2; stack_expr($$).id(ID_smv_set); } | INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); } | DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); } | ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); } @@ -709,8 +708,7 @@ term : variable_identifier | 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); } + | term in_Token term { binary($$, $1, ID_smv_setin, $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); } diff --git a/src/smvlang/scanner.l b/src/smvlang/scanner.l index fec3a0d6e..a69c9894e 100644 --- a/src/smvlang/scanner.l +++ b/src/smvlang/scanner.l @@ -101,7 +101,6 @@ void newlocation(YYSTYPE &x) "LTLWFF" token(LTLWFF_Token); "PSLWFF" token(PSLWFF_Token); "COMPWFF" token(COMPWFF_Token); -"IN" token(IN_Token); "MIN" token(MIN_Token); "MAX" token(MAX_Token); "MIRROR" token(MIRROR_Token); diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index acb885a47..afb103da6 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -1001,7 +1001,35 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode) } else if(expr.id() == ID_smv_setin) { - expr.type()=bool_typet(); + auto &lhs = to_binary_expr(expr).lhs(); + auto &rhs = to_binary_expr(expr).rhs(); + + typecheck_expr_rec(lhs, mode); + typecheck_expr_rec(rhs, mode); + + // The RHS can be a set or a singleton + if(rhs.type().id() == ID_smv_set) + { + PRECONDITION(rhs.id() == ID_smv_set); + // do type union + typet op_type = lhs.type(); + for(auto &op : rhs.operands()) + op_type = type_union(op_type, op.type(), expr.source_location()); + // now convert + convert_expr_to(lhs, op_type); + for(auto &op : rhs.operands()) + convert_expr_to(op, op_type); + } + else + { + typet op_type = + type_union(lhs.type(), rhs.type(), expr.source_location()); + + convert_expr_to(lhs, op_type); + convert_expr_to(rhs, op_type); + } + + expr.type() = bool_typet(); } else if(expr.id() == ID_smv_setnotin) { @@ -1232,6 +1260,14 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode) << "signed operand must have unsigned word type"; } } + else if(expr.id() == ID_smv_set) + { + // a set literal + expr.type() = typet{ID_smv_set}; + + for(auto &op : expr.operands()) + typecheck_expr_rec(op, mode); + } else { throw errort().with_location(expr.find_source_location()) @@ -1271,6 +1307,33 @@ void smv_typecheckt::lower_node(exprt &expr) const { expr = typecast_exprt{to_smv_unsigned_cast_expr(expr).op(), expr.type()}; } + else if(expr.id() == ID_smv_setin) + { + auto &lhs = to_binary_expr(expr).lhs(); + auto &rhs = to_binary_expr(expr).rhs(); + if(rhs.type().id() == ID_smv_set) + { + DATA_INVARIANT( + rhs.id() == ID_smv_set, "rhs of in must be set expression"); + // this is an 'or' + exprt::operandst disjuncts; + disjuncts.reserve(rhs.operands().size()); + for(auto &op : rhs.operands()) + { + DATA_INVARIANT( + lhs.type() == op.type(), "lhs/rhs of in must have same type"); + disjuncts.push_back(equal_exprt{lhs, op}); + } + expr = disjunction(std::move(disjuncts)); + } + else + { + // RHS is a singleton; this is equality + expr.id(ID_equal); + DATA_INVARIANT( + lhs.type() == rhs.type(), "lhs/rhs of in must have same type"); + } + } } /*******************************************************************\ @@ -1285,28 +1348,50 @@ Function: smv_typecheckt::convert_expr_to \*******************************************************************/ -void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type) +void smv_typecheckt::convert_expr_to(exprt &expr, const typet &dest_type) { - PRECONDITION(type.is_not_nil()); + const auto &src_type = expr.type(); - if(expr.type() != type) + PRECONDITION(dest_type.is_not_nil()); + + if(src_type != dest_type) { - if(type.id() == ID_signedbv || type.id() == ID_unsignedbv) + if(src_type.id() == ID_smv_set && expr.id() == ID_smv_set) + { + // sets can be assigned to scalars, which yields a nondeterministic + // choice + std::string identifier = + module + "::var::" + std::to_string(nondet_count++); + + expr.set(ID_identifier, identifier); + expr.set("#smv_nondet_choice", true); + + expr.id(ID_constraint_select_one); + expr.type() = dest_type; + + // apply recursively + for(auto &op : expr.operands()) + convert_expr_to(op, dest_type); + + return; + } + + if(dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv) { // no implicit conversion } - else if(type.id() == ID_range) + else if(dest_type.id() == ID_range) { - if(expr.type().id() == ID_range) + if(src_type.id() == ID_range) { // range to range if(expr.id() == ID_constant) { // re-type the constant auto value = numeric_cast_v(to_constant_expr(expr)); - if(to_range_type(type).includes(value)) + if(to_range_type(dest_type).includes(value)) { - expr = from_integer(value, type); + expr = from_integer(value, dest_type); return; } } @@ -1318,26 +1403,40 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type) for(auto &op : expr.operands()) { if(!condition) - convert_expr_to(op, type); + convert_expr_to(op, dest_type); condition = !condition; } - expr.type() = type; + expr.type() = dest_type; return; } else { - expr = typecast_exprt{expr, type}; + expr = typecast_exprt{expr, dest_type}; return; } } + else if(src_type.id() == ID_integer) + { + // integer to range + if(expr.id() == ID_constant) + { + // re-type the constant + auto value = numeric_cast_v(to_constant_expr(expr)); + if(to_range_type(dest_type).includes(value)) + { + expr = from_integer(value, dest_type); + return; + } + } + } } - else if(type.id() == ID_bool) + else if(dest_type.id() == ID_bool) { // legacy -- convert 0/1 to false/true - if(expr.type().id() == ID_range) + if(src_type.id() == ID_range) { - auto &range_type = to_range_type(expr.type()); + auto &range_type = to_range_type(src_type); if(range_type.get_from() == 0 && range_type.get_to() == 0) { expr = false_exprt{}; @@ -1350,43 +1449,41 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type) } } } - else if(type.id() == ID_enumeration) + else if(dest_type.id() == ID_enumeration) { - auto &e_type = to_enumeration_type(type); + auto &e_type = to_enumeration_type(dest_type); - if(expr.id() == ID_constant && expr.type().id() == ID_enumeration) + if(expr.id() == ID_constant && src_type.id() == ID_enumeration) { - if(is_contained_in(to_enumeration_type(expr.type()), e_type)) + if(is_contained_in(to_enumeration_type(src_type), e_type)) { // re-type the constant - expr.type() = type; + expr.type() = dest_type; return; } else { throw errort().with_location(expr.find_source_location()) << "enum " << to_string(expr) << " not a member of " - << to_string(type); + << to_string(dest_type); } } else if(expr.id() == ID_typecast) { // created by type unions auto &op = to_typecast_expr(expr).op(); - if( - expr.type().id() == ID_enumeration && - op.type().id() == ID_enumeration) + if(src_type.id() == ID_enumeration && op.type().id() == ID_enumeration) { - convert_expr_to(op, type); + convert_expr_to(op, dest_type); expr = std::move(op); } } } throw errort().with_location(expr.find_source_location()) - << "Expected expression of type `" << to_string(type) + << "Expected expression of type `" << to_string(dest_type) << "', but got expression `" << to_string(expr) << "', which is of type `" - << to_string(expr.type()) << "'"; + << to_string(src_type) << "'"; } }