Skip to content

Commit 3d7eb16

Browse files
committed
SMV: set type
This fixes typechecking for set literals, assignments from set literals to variables of the element type, and typechecking for the "in" set membership operator.
1 parent 6e6127d commit 3d7eb16

File tree

9 files changed

+162
-55
lines changed

9 files changed

+162
-55
lines changed
Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
KNOWNBUG
1+
CORE broken-smt-backend
22
smv_set2.smv
3-
--bdd
4-
^\[spec1\] x in my_set: PROVED$
5-
^EXIT=0$
3+
4+
^\[spec1\] x in \{ 1, 2 \}: REFUTED$
5+
^\[spec2\] x in 1 \| x in 2: REFUTED$
6+
^EXIT=10$
67
^SIGNAL=0$
78
--
89
^warning: ignoring
910
--
10-
The smv_setin operator is not implemented.
Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
MODULE main
22

3-
DEFINE my_set := {1, 2};
4-
53
VAR x : 1..3;
64
ASSIGN init(x) := {1, 2, 3};
75
next(x) := x;
86

9-
SPEC x in my_set;
7+
SPEC x in {1, 2};
8+
9+
-- the rhs set can be a singleton
10+
SPEC (x in 1) | (x in 2);
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
smv_set3.smv
3+
--bdd
4+
^\[spec1\] x in my_set: PROVED$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
10+
The smv_setin operator does not work with symbols on the RHS.

src/hw_cbmc_irep_ids.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ IREP_ID_ONE(smv_next)
2323
IREP_ID_ONE(smv_iff)
2424
IREP_ID_TWO(C_smv_iff, "#smv_iff")
2525
IREP_ID_ONE(smv_resize)
26+
IREP_ID_ONE(smv_set)
2627
IREP_ID_ONE(smv_setin)
2728
IREP_ID_ONE(smv_setnotin)
2829
IREP_ID_ONE(smv_signed_cast)

src/smvlang/expr2smv.cpp

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
1515

1616
/*******************************************************************\
1717
18-
Function: expr2smvt::convert_nondet_choice
18+
Function: expr2smvt::convert_smv_set
1919
2020
Inputs:
2121
@@ -25,7 +25,7 @@ Function: expr2smvt::convert_nondet_choice
2525
2626
\*******************************************************************/
2727

28-
expr2smvt::resultt expr2smvt::convert_nondet_choice(const exprt &src)
28+
expr2smvt::resultt expr2smvt::convert_smv_set(const exprt &src)
2929
{
3030
std::string dest = "{ ";
3131

@@ -656,6 +656,9 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
656656
else if(src.id() == ID_mod)
657657
return convert_binary(to_mod_expr(src), src.id_string(), precedencet::MULT);
658658

659+
else if(src.id() == ID_smv_set)
660+
return convert_smv_set(src);
661+
659662
else if(src.id() == ID_smv_setin)
660663
return convert_binary(to_binary_expr(src), "in", precedencet::IN);
661664

@@ -788,19 +791,13 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
788791
else if(src.id()==ID_constant)
789792
return convert_constant(to_constant_expr(src));
790793

791-
else if(src.id()=="smv_nondet_choice")
792-
return convert_nondet_choice(src);
793-
794-
else if(src.id() == ID_constraint_select_one)
795-
return convert_nondet_choice(src);
796-
797794
else if(src.id()==ID_nondet_bool)
798795
{
799-
exprt nondet_choice_expr("smv_nondet_choice");
800-
nondet_choice_expr.operands().clear();
801-
nondet_choice_expr.operands().push_back(false_exprt());
802-
nondet_choice_expr.operands().push_back(true_exprt());
803-
return convert_nondet_choice(nondet_choice_expr);
796+
exprt smv_set_expr(ID_smv_set);
797+
smv_set_expr.operands().clear();
798+
smv_set_expr.operands().push_back(false_exprt());
799+
smv_set_expr.operands().push_back(true_exprt());
800+
return convert_smv_set(smv_set_expr);
804801
}
805802

806803
else if(src.id()==ID_cond)
@@ -902,6 +899,10 @@ std::string type2smv(const typet &type, const namespacet &ns)
902899
{
903900
return type.get_string(ID_from) + ".." + type.get_string(ID_to);
904901
}
902+
else if(type.id() == ID_smv_set)
903+
{
904+
return "set";
905+
}
905906
else if(type.id()=="submodule")
906907
{
907908
auto code = type.get_string(ID_identifier);

src/smvlang/expr2smv_class.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ class expr2smvt
8585

8686
virtual resultt convert_rec(const exprt &);
8787

88-
resultt convert_nondet_choice(const exprt &);
88+
resultt convert_smv_set(const exprt &);
8989

9090
resultt convert_binary(
9191
const binary_exprt &src,

src/smvlang/parser.y

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,6 @@ static void new_module(YYSTYPE &module)
176176
%token LTLWFF_Token "LTLWFF"
177177
%token PSLWFF_Token "PSLWFF"
178178
%token COMPWFF_Token "COMPWFF"
179-
%token IN_Token "IN"
180179
%token MIN_Token "MIN"
181180
%token MAX_Token "MAX"
182181
%token MIRROR_Token "MIRROR"
@@ -289,7 +288,7 @@ static void new_module(YYSTYPE &module)
289288
%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
290289
%left EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token
291290
%left union_Token
292-
%left IN_Token NOTIN_Token
291+
%left in_Token
293292
%left mod_Token /* Precedence from CMU SMV, different from NuSMV */
294293
%left LTLT_Token GTGT_Token
295294
%left PLUS_Token MINUS_Token
@@ -673,7 +672,7 @@ formula : term
673672
term : variable_identifier
674673
| next_Token '(' term ')' { init($$, ID_smv_next); mto($$, $3); }
675674
| '(' formula ')' { $$=$2; }
676-
| '{' formula_list '}' { $$=$2; stack_expr($$).id("smv_nondet_choice"); }
675+
| '{' formula_list '}' { $$=$2; stack_expr($$).id(ID_smv_set); }
677676
| INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); }
678677
| DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
679678
| ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
@@ -709,8 +708,7 @@ term : variable_identifier
709708
| term GT_Token term { binary($$, $1, ID_gt, $3); }
710709
| term GE_Token term { binary($$, $1, ID_ge, $3); }
711710
| term union_Token term { binary($$, $1, ID_smv_union, $3); }
712-
| term IN_Token term { binary($$, $1, ID_smv_setin, $3); }
713-
| term NOTIN_Token term { binary($$, $1, ID_smv_setnotin, $3); }
711+
| term in_Token term { binary($$, $1, ID_smv_setin, $3); }
714712
| extend_Token '(' term ',' term ')' { binary($$, $3, ID_smv_extend, $5); }
715713
| resize_Token '(' term ',' term ')' { binary($$, $3, ID_smv_resize, $5); }
716714
| signed_Token '(' term ')' { init($$, ID_smv_signed_cast); mto($$, $3); }

src/smvlang/scanner.l

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,6 @@ void newlocation(YYSTYPE &x)
101101
"LTLWFF" token(LTLWFF_Token);
102102
"PSLWFF" token(PSLWFF_Token);
103103
"COMPWFF" token(COMPWFF_Token);
104-
"IN" token(IN_Token);
105104
"MIN" token(MIN_Token);
106105
"MAX" token(MAX_Token);
107106
"MIRROR" token(MIRROR_Token);

0 commit comments

Comments
 (0)