Skip to content

Commit 31591f7

Browse files
kroeningkroening
authored
Merge pull request #980 from diffblue/smv-parser-cleanup3
SMV: parser cleanup
2 parents 4648700 + 2590bee commit 31591f7

File tree

4 files changed

+120
-28
lines changed

4 files changed

+120
-28
lines changed

‎src/smvlang/parser.y‎

Lines changed: 36 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -414,8 +414,6 @@ vardecl : variable_name ':' type ';'
414414

415415
assignments: assignment
416416
| assignments assignment
417-
| define
418-
| assignments define
419417
;
420418

421419
assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
@@ -427,10 +425,43 @@ assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
427425
exprt &op=to_binary_expr(stack_expr($$)).op0();
428426
unary_exprt tmp(ID_smv_next, std::move(op));
429427
tmp.swap(op);
430-
PARSER.module->add_trans(stack_expr($$));
428+
PARSER.module->add_assign_next(to_equal_expr(stack_expr($$)));
431429
}
432430
else
433-
PARSER.module->add_init(stack_expr($$));
431+
PARSER.module->add_assign_init(to_equal_expr(stack_expr($$)));
432+
}
433+
| assignment_var BECOMES_Token formula ';'
434+
{
435+
const irep_idt &identifier=stack_expr($1).get(ID_identifier);
436+
smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
437+
438+
switch(var.var_class)
439+
{
440+
case smv_parse_treet::mc_vart::UNKNOWN:
441+
var.type.make_nil();
442+
var.var_class=smv_parse_treet::mc_vart::DEFINED;
443+
break;
444+
445+
case smv_parse_treet::mc_vart::DECLARED:
446+
var.var_class=smv_parse_treet::mc_vart::DEFINED;
447+
break;
448+
449+
case smv_parse_treet::mc_vart::DEFINED:
450+
yyerror("variable `"+id2string(identifier)+"' already defined");
451+
YYERROR;
452+
break;
453+
454+
case smv_parse_treet::mc_vart::ARGUMENT:
455+
yyerror("variable `"+id2string(identifier)+"' already declared as argument");
456+
YYERROR;
457+
break;
458+
459+
default:
460+
DATA_INVARIANT(false, "unexpected variable class");
461+
}
462+
463+
binary($$, $1, ID_equal, $3);
464+
PARSER.module->add_assign_current(to_equal_expr(stack_expr($$)));
434465
}
435466
;
436467

@@ -476,7 +507,7 @@ define : assignment_var BECOMES_Token formula ';'
476507
}
477508

478509
binary($$, $1, ID_equal, $3);
479-
PARSER.module->add_define(stack_expr($$));
510+
PARSER.module->add_define(to_equal_expr(stack_expr($$)));
480511
}
481512
;
482513

‎src/smvlang/smv_parse_tree.cpp‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,12 @@ std::string to_string(smv_parse_treet::modulet::itemt::item_typet i)
5858
{
5959
switch(i)
6060
{
61+
case smv_parse_treet::modulet::itemt::ASSIGN_CURRENT:
62+
return "ASSIGN CURRENT";
63+
case smv_parse_treet::modulet::itemt::ASSIGN_INIT:
64+
return "ASSIGN INIT";
65+
case smv_parse_treet::modulet::itemt::ASSIGN_NEXT:
66+
return "ASSIGN NEXT";
6167
case smv_parse_treet::modulet::itemt::INVAR: return "INVAR";
6268
case smv_parse_treet::modulet::itemt::TRANS: return "TRANS";
6369
case smv_parse_treet::modulet::itemt::INIT: return "INIT";

‎src/smvlang/smv_parse_tree.h‎

Lines changed: 49 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com
99
#ifndef CPROVER_SMV_PARSE_TREE_H
1010
#define CPROVER_SMV_PARSE_TREE_H
1111

12-
#include <unordered_set>
13-
#include <unordered_map>
14-
12+
#include <util/std_expr.h>
1513
#include <util/string_hash.h>
16-
#include <util/expr.h>
14+
15+
#include <unordered_map>
16+
#include <unordered_set>
1717

1818
class smv_parse_treet
1919
{
@@ -42,6 +42,9 @@ class smv_parse_treet
4242
{
4343
enum item_typet
4444
{
45+
ASSIGN_CURRENT,
46+
ASSIGN_INIT,
47+
ASSIGN_NEXT,
4548
CTLSPEC,
4649
LTLSPEC,
4750
INIT,
@@ -57,6 +60,21 @@ class smv_parse_treet
5760
exprt expr;
5861
source_locationt location;
5962

63+
bool is_assign_current() const
64+
{
65+
return item_type == ASSIGN_CURRENT;
66+
}
67+
68+
bool is_assign_init() const
69+
{
70+
return item_type == ASSIGN_INIT;
71+
}
72+
73+
bool is_assign_next() const
74+
{
75+
return item_type == ASSIGN_NEXT;
76+
}
77+
6078
bool is_ctlspec() const
6179
{
6280
return item_type == CTLSPEC;
@@ -86,12 +104,20 @@ class smv_parse_treet
86104
{
87105
return item_type==INIT;
88106
}
89-
107+
108+
// for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE
109+
const equal_exprt &equal_expr()
110+
{
111+
PRECONDITION(
112+
is_assign_current() || is_assign_init() || is_assign_next() ||
113+
is_define());
114+
return to_equal_expr(expr);
115+
}
90116
};
91117

92118
typedef std::list<itemt> item_listt;
93119
item_listt items;
94-
120+
95121
void add_item(
96122
itemt::item_typet item_type,
97123
const exprt &expr,
@@ -102,7 +128,22 @@ class smv_parse_treet
102128
items.back().expr=expr;
103129
items.back().location=location;
104130
}
105-
131+
132+
void add_assign_current(const equal_exprt &expr)
133+
{
134+
add_item(itemt::ASSIGN_CURRENT, expr, source_locationt::nil());
135+
}
136+
137+
void add_assign_init(const equal_exprt &expr)
138+
{
139+
add_item(itemt::ASSIGN_INIT, expr, source_locationt::nil());
140+
}
141+
142+
void add_assign_next(const equal_exprt &expr)
143+
{
144+
add_item(itemt::ASSIGN_NEXT, expr, source_locationt::nil());
145+
}
146+
106147
void add_invar(const exprt &expr)
107148
{
108149
add_item(itemt::INVAR, expr, source_locationt::nil());
@@ -118,7 +159,7 @@ class smv_parse_treet
118159
add_item(itemt::LTLSPEC, expr, source_locationt::nil());
119160
}
120161

121-
void add_define(const exprt &expr)
162+
void add_define(const equal_exprt &expr)
122163
{
123164
add_item(itemt::DEFINE, expr, source_locationt::nil());
124165
}

‎src/smvlang/smv_typecheck.cpp‎

Lines changed: 29 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ class smv_typecheckt:public typecheckt
5656
void convert(smv_parse_treet::modulet &);
5757
void convert(smv_parse_treet::mc_varst &);
5858

59-
void collect_define(const exprt &);
59+
void collect_define(const equal_exprt &);
6060
void convert_defines(exprt::operandst &invar);
6161
void convert_define(const irep_idt &identifier);
6262

@@ -1171,6 +1171,18 @@ void smv_typecheckt::typecheck(
11711171

11721172
switch(item.item_type)
11731173
{
1174+
case smv_parse_treet::modulet::itemt::ASSIGN_CURRENT:
1175+
mode = OTHER;
1176+
break;
1177+
1178+
case smv_parse_treet::modulet::itemt::ASSIGN_INIT:
1179+
mode = INIT;
1180+
break;
1181+
1182+
case smv_parse_treet::modulet::itemt::ASSIGN_NEXT:
1183+
mode = TRANS;
1184+
break;
1185+
11741186
case smv_parse_treet::modulet::itemt::INIT:
11751187
mode=INIT;
11761188
break;
@@ -1277,18 +1289,15 @@ Function: smv_typecheckt::collect_define
12771289
12781290
\*******************************************************************/
12791291

1280-
void smv_typecheckt::collect_define(const exprt &expr)
1292+
void smv_typecheckt::collect_define(const equal_exprt &expr)
12811293
{
1282-
if(expr.id()!=ID_equal || expr.operands().size()!=2)
1283-
throw errort() << "collect_define expects equality";
1284-
1285-
const exprt &op0 = to_equal_expr(expr).op0();
1286-
const exprt &op1 = to_equal_expr(expr).op1();
1294+
const exprt &lhs = expr.lhs();
1295+
const exprt &rhs = expr.rhs();
12871296

1288-
if(op0.id()!=ID_symbol)
1297+
if(lhs.id() != ID_symbol)
12891298
throw errort() << "collect_define expects symbol on left hand side";
12901299

1291-
const irep_idt &identifier = to_symbol_expr(op0).get_identifier();
1300+
const irep_idt &identifier = to_symbol_expr(lhs).get_identifier();
12921301

12931302
auto it=symbol_table.get_writeable(identifier);
12941303

@@ -1305,8 +1314,8 @@ void smv_typecheckt::collect_define(const exprt &expr)
13051314
symbol.is_state_var=false;
13061315
symbol.is_macro=false;
13071316

1308-
std::pair<define_mapt::iterator, bool> result=
1309-
define_map.insert(std::pair<irep_idt, definet>(identifier, definet(op1)));
1317+
std::pair<define_mapt::iterator, bool> result =
1318+
define_map.insert(std::pair<irep_idt, definet>{identifier, definet{rhs}});
13101319

13111320
if(!result.second)
13121321
{
@@ -1432,24 +1441,29 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
14321441
// we first need to collect all the defines
14331442

14341443
for (auto &item : smv_module.items) {
1435-
if (item.is_define())
1436-
collect_define(item.expr);
1444+
if(item.is_define() || item.is_assign_current())
1445+
collect_define(item.equal_expr());
14371446
}
14381447
// now turn them into INVARs
14391448
convert_defines(trans_invar);
14401449

14411450
// do the rest now: typecheck
14421451
for (auto &item : smv_module.items) {
1443-
if (!item.is_define())
1452+
if(!item.is_define() && !item.is_assign_current())
14441453
typecheck(item);
14451454
}
14461455

14471456
// copy to transition system
1448-
for (const auto &item : smv_module.items) {
1457+
for(const auto &item : smv_module.items)
1458+
{
14491459
if (item.is_invar())
14501460
trans_invar.push_back(item.expr);
14511461
else if (item.is_init())
14521462
trans_init.push_back(item.expr);
1463+
else if(item.is_assign_init())
1464+
trans_init.push_back(item.expr);
1465+
else if(item.is_assign_next())
1466+
trans_trans.push_back(item.expr);
14531467
else if (item.is_trans())
14541468
trans_trans.push_back(item.expr);
14551469
}

0 commit comments

Comments
 (0)