Skip to content

Commit a979309

Browse files
kroeningkroening
committed
SMV: clean up parse tree
This replaces the mechanism used for parsing an SMV expression. Assignments are now stored explicitly in the parse tree.
1 parent 578d1af commit a979309

File tree

5 files changed

+99
-28
lines changed

5 files changed

+99
-28
lines changed

‎src/hw_cbmc_irep_ids.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,11 @@ IREP_ID_ONE(F)
1717
IREP_ID_ONE(E)
1818
IREP_ID_ONE(G)
1919
IREP_ID_ONE(X)
20-
IREP_ID_ONE(smv_next)
2120
IREP_ID_ONE(smv_iff)
21+
IREP_ID_ONE(smv_assign_current)
22+
IREP_ID_ONE(smv_assign_init)
23+
IREP_ID_ONE(smv_assign_next)
24+
IREP_ID_ONE(smv_next)
2225
IREP_ID_TWO(C_smv_iff, "#smv_iff")
2326
IREP_ID_ONE(smv_setin)
2427
IREP_ID_ONE(smv_setnotin)

‎src/smvlang/parser.y

Lines changed: 9 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -414,31 +414,25 @@ 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 ';'
422420
{
423-
binary($$, $3, ID_equal, $6);
424-
425-
if(stack_expr($1).id()==ID_smv_next)
426-
{
427-
exprt &op=to_binary_expr(stack_expr($$)).op0();
428-
unary_exprt tmp(ID_smv_next, std::move(op));
429-
tmp.swap(op);
430-
PARSER.module->add_trans(stack_expr($$));
431-
}
432-
else
433-
PARSER.module->add_init(stack_expr($$));
421+
exprt lhs = unary_exprt{stack_expr($1).id(), std::move(stack_expr($3))};
422+
PARSER.module->add_assign(std::move(lhs), stack_expr($6));
423+
}
424+
| assignment_var BECOMES_Token formula ';'
425+
{
426+
exprt lhs = unary_exprt{ID_smv_assign_current, std::move(stack_expr($1))};
427+
PARSER.module->add_assign(std::move(lhs), stack_expr($3));
434428
}
435429
;
436430

437431
assignment_var: variable_name
438432
;
439433

440-
assignment_head: init_Token { init($$, ID_init); }
441-
| NEXT_Token { init($$, ID_smv_next); }
434+
assignment_head: init_Token { init($$, ID_smv_assign_init); }
435+
| NEXT_Token { init($$, ID_smv_assign_next); }
442436
;
443437

444438
defines: define

‎src/smvlang/smv_parse_tree.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,8 @@ 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:
62+
return "ASSIGN";
6163
case smv_parse_treet::modulet::itemt::INVAR: return "INVAR";
6264
case smv_parse_treet::modulet::itemt::TRANS: return "TRANS";
6365
case smv_parse_treet::modulet::itemt::INIT: return "INIT";

‎src/smvlang/smv_parse_tree.h

Lines changed: 21 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
1313
#include <unordered_map>
1414

1515
#include <util/string_hash.h>
16-
#include <util/expr.h>
16+
#include <util/std_expr.h>
1717

1818
class smv_parse_treet
1919
{
@@ -42,6 +42,7 @@ class smv_parse_treet
4242
{
4343
enum item_typet
4444
{
45+
ASSIGN,
4546
CTLSPEC,
4647
LTLSPEC,
4748
INIT,
@@ -57,6 +58,14 @@ class smv_parse_treet
5758
exprt expr;
5859
source_locationt location;
5960

61+
// for ASSIGN
62+
exprt assignment_lhs, assignment_rhs;
63+
64+
bool is_assign() const
65+
{
66+
return item_type == ASSIGN;
67+
}
68+
6069
bool is_ctlspec() const
6170
{
6271
return item_type == CTLSPEC;
@@ -102,7 +111,16 @@ class smv_parse_treet
102111
items.back().expr=expr;
103112
items.back().location=location;
104113
}
105-
114+
115+
void add_assign(exprt lhs, exprt rhs)
116+
{
117+
items.push_back(itemt{});
118+
items.back().item_type = itemt::ASSIGN;
119+
items.back().assignment_lhs = std::move(lhs);
120+
items.back().assignment_rhs = std::move(rhs);
121+
items.back().location = source_locationt::nil();
122+
}
123+
106124
void add_invar(const exprt &expr)
107125
{
108126
add_item(itemt::INVAR, expr, source_locationt::nil());
@@ -182,7 +200,7 @@ class smv_parse_treet
182200
typedef std::unordered_map<irep_idt, modulet, irep_id_hash> modulest;
183201

184202
modulest modules;
185-
203+
186204
void swap(smv_parse_treet &smv_parse_tree);
187205
void clear();
188206
};

‎src/smvlang/smv_typecheck.cpp

Lines changed: 63 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1167,34 +1167,49 @@ Function: smv_typecheckt::typecheck
11671167
void smv_typecheckt::typecheck(
11681168
smv_parse_treet::modulet::itemt &item)
11691169
{
1170-
modet mode;
1171-
11721170
switch(item.item_type)
11731171
{
1172+
case smv_parse_treet::modulet::itemt::ASSIGN:
1173+
{
1174+
DATA_INVARIANT(
1175+
item.expr.id() == ID_equal, "ASSIGN expression must be equality");
1176+
auto &equal_expr = to_equal_expr(item.expr);
1177+
1178+
DATA_INVARIANT(
1179+
equal_expr.lhs().id() == ID_smv_assign_current ||
1180+
equal_expr.lhs().id() == ID_smv_assign_init ||
1181+
equal_expr.lhs().id() == ID_smv_assign_next,
1182+
"ASSIGN lhs must be current, init or next");
1183+
1184+
auto &symbol_expr = to_unary_expr(equal_expr.lhs()).op();
1185+
auto &nil_type = static_cast<const typet &>(get_nil_irep());
1186+
typecheck(symbol_expr, nil_type, OTHER);
1187+
typecheck(equal_expr.rhs(), symbol_expr.type(), OTHER);
1188+
}
1189+
break;
1190+
11741191
case smv_parse_treet::modulet::itemt::INIT:
1175-
mode=INIT;
1192+
typecheck(item.expr, bool_typet(), INIT);
11761193
break;
11771194

11781195
case smv_parse_treet::modulet::itemt::TRANS:
1179-
mode=TRANS;
1196+
typecheck(item.expr, bool_typet(), TRANS);
11801197
break;
11811198

11821199
case smv_parse_treet::modulet::itemt::CTLSPEC:
1183-
mode = CTL;
1200+
typecheck(item.expr, bool_typet(), CTL);
11841201
break;
11851202

11861203
case smv_parse_treet::modulet::itemt::LTLSPEC:
1187-
mode = LTL;
1204+
typecheck(item.expr, bool_typet(), LTL);
11881205
break;
11891206

11901207
case smv_parse_treet::modulet::itemt::DEFINE:
11911208
case smv_parse_treet::modulet::itemt::INVAR:
11921209
case smv_parse_treet::modulet::itemt::FAIRNESS:
11931210
default:
1194-
mode=OTHER;
1211+
typecheck(item.expr, bool_typet(), OTHER);
11951212
}
1196-
1197-
typecheck(item.expr, bool_typet(), mode);
11981213
}
11991214

12001215
/*******************************************************************\
@@ -1452,6 +1467,45 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
14521467
trans_init.push_back(item.expr);
14531468
else if (item.is_trans())
14541469
trans_trans.push_back(item.expr);
1470+
else if(item.is_assign())
1471+
{
1472+
DATA_INVARIANT(
1473+
item.expr.id() == ID_equal, "ASSIGN expression must be equality");
1474+
auto &equal_expr = to_equal_expr(item.expr);
1475+
auto &symbol_expr = to_unary_expr(equal_expr.lhs()).op();
1476+
1477+
auto &identifier = to_symbol_expr(symbol_expr).get_identifier();
1478+
auto s_it = symbol_table.get_writeable(identifier);
1479+
1480+
if(s_it == nullptr)
1481+
{
1482+
throw errort().with_location(symbol_expr.find_source_location())
1483+
<< "variable `" << identifier << "' not found";
1484+
}
1485+
1486+
symbolt &symbol = *s_it;
1487+
symbol.is_input = false;
1488+
1489+
if(equal_expr.lhs().id() == ID_smv_assign_current)
1490+
{
1491+
trans_invar.push_back(equal_exprt{symbol_expr, equal_expr.rhs()});
1492+
}
1493+
else if(equal_expr.lhs().id() == ID_smv_assign_init)
1494+
{
1495+
symbol.is_state_var = true;
1496+
trans_init.push_back(equal_exprt{symbol_expr, equal_expr.rhs()});
1497+
}
1498+
else if(equal_expr.lhs().id() == ID_smv_assign_next)
1499+
{
1500+
symbol.is_state_var = true;
1501+
exprt next_symbol_expr = symbol_expr;
1502+
next_symbol_expr.id(ID_next_symbol);
1503+
trans_trans.push_back(
1504+
equal_exprt{next_symbol_expr, equal_expr.rhs()});
1505+
}
1506+
else
1507+
DATA_INVARIANT(false, "ASSIGN must be current/init/next");
1508+
}
14551509
}
14561510

14571511
module_symbol.value =

0 commit comments

Comments
 (0)