Skip to content

Commit 5728a30

Browse files
kroeningkroening
committed
SMV: set pretty names for top-level identifiers
Identifiers in module main now no longer carry the prefix main::var::.
1 parent d3071f4 commit 5728a30

20 files changed

+97
-61
lines changed

‎regression/ebmc/BDD/BDD1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ BDD1.smv
33
--bdd
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main::spec1\] AG \(!main::var::some_var = off\): PROVED$
6+
^\[main::spec1\] AG \(!some_var = off\): PROVED$
77
--
88
^warning: ignoring

‎regression/ebmc/range_type/range_type1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ range_type1.smv
33
--bound 10
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main::spec1\] AG main::var::x != 4: PROVED up to bound 10$
6+
^\[main::spec1\] AG x != 4: PROVED up to bound 10$
77
--
88
^warning: ignoring

‎regression/ebmc/range_type/range_type2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ range_type2.smv
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main::spec1\] AG TRUE: PROVED up to bound 10$
7-
^\[main::spec2\] AG main::var::NET_tmp9: PROVED up to bound 10$
7+
^\[main::spec2\] AG NET_tmp9: PROVED up to bound 10$
88
--
99
^warning: ignoring

‎regression/ebmc/range_type/range_type4.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ range_type4.smv
33
--bound 10
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main::spec1\] AG \(!main::var::x = 6\): PROVED up to bound 10$
6+
^\[main::spec1\] AG \(!x = 6\): PROVED up to bound 10$
77
--
88
^warning: ignoring

‎regression/ebmc/range_type/range_type5.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ range_type5.smv
33
--bound 3
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main::spec1\] AG \(!main::var::x = 6\): PROVED up to bound 3$
6+
^\[main::spec1\] AG \(!x = 6\): PROVED up to bound 3$
77
--
88
^warning: ignoring

‎regression/ebmc/small-test1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.smv
33
--bound 10 --trace
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main::spec1\] AG main::var::x = 1: REFUTED$
6+
^\[main::spec1\] AG x = 1: REFUTED$
77
--
88
^warning: ignoring

‎regression/ebmc/small-test2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.smv
33
--bound 2
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main::spec1\] AG main::var::z: REFUTED$
6+
^\[main::spec1\] AG z: REFUTED$
77
--
88
^warning: ignoring

‎regression/ebmc/smv/bdd_unsupported_property.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ bdd_unsupported_property.smv
33
--bdd
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BDD engine$
7-
^\[main::spec2\] G main::var::x = FALSE: REFUTED$
6+
^\[main::spec1\] !G x = FALSE: FAILURE: property not supported by BDD engine$
7+
^\[main::spec2\] G x = FALSE: REFUTED$
88
--
99
^warning: ignoring

‎regression/ebmc/smv/bmc_unsupported_property1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ bmc_unsupported_property1.smv
33

44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BMC engine$
7-
^\[main::spec2\] G main::var::x = FALSE: REFUTED$
6+
^\[main::spec1\] !G x = FALSE: FAILURE: property not supported by BMC engine$
7+
^\[main::spec2\] G x = FALSE: REFUTED$
88
--
99
^warning: ignoring

‎regression/ebmc/smv/bmc_unsupported_property2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ bmc_unsupported_property2.smv
33

44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BMC engine$
7-
^\[main::spec2\] G main::var::x = TRUE: PROVED up to bound 1$
6+
^\[main::spec1\] !G x = FALSE: FAILURE: property not supported by BMC engine$
7+
^\[main::spec2\] G x = TRUE: PROVED up to bound 1$
88
--
99
^warning: ignoring

‎regression/ebmc/smv/initial1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
initial1.smv
33
--bound 0
4-
^\[main::spec1\] main::var::tmp1 = TRUE: PROVED up to bound 0$
5-
^\[main::spec2\] main::var::tmp2 = TRUE: REFUTED$
4+
^\[main::spec1\] tmp1 = TRUE: PROVED up to bound 0$
5+
^\[main::spec2\] tmp2 = TRUE: REFUTED$
66
^EXIT=10$
77
^SIGNAL=0$
88
--

‎regression/ebmc/smv/smv_ltlspec1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ smv_ltlspec1.smv
33
--bdd
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main::spec1\] G main::var::x != 0: PROVED$
6+
^\[main::spec1\] G x != 0: PROVED$
77
--
88
^warning: ignoring

‎regression/ebmc/smv/smv_ltlspec2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ smv_ltlspec2.smv
33
--bdd
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[smv::main::spec1\] G F main::var::x = 3: PROVED$
6+
^\[smv::main::spec1\] G F x = 3: PROVED$
77
--
88
^warning: ignoring
99
--

‎regression/ebmc/smv/smv_ltlspec3.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ smv_ltlspec3.smv
33
--bound 10 --numbered-trace
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main::spec1\] X X main::var::x = TRUE: REFUTED$
7-
^main::var::x@0 = FALSE$
8-
^main::var::x@1 = FALSE$
9-
^main::var::x@2 = FALSE$
6+
^\[main::spec1\] X X x = TRUE: REFUTED$
7+
^x@0 = FALSE$
8+
^x@1 = FALSE$
9+
^x@2 = FALSE$
1010
--
1111
^warning: ignoring

‎regression/ebmc/traces/numbered1.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ waveform1.smv
55
^SIGNAL=0$
66
^\[main::spec1\] .* REFUTED$
77
^Counterexample:$
8-
^main::var::y@0 = 0$
9-
^main::var::y@10 = 100$
10-
^main::var::y@20 = 200$
8+
^y@0 = 0$
9+
^y@10 = 100$
10+
^y@20 = 200$
1111
--
1212
^warning: ignoring

‎regression/ebmc/traces/waveform1.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@ waveform1.smv
55
^SIGNAL=0$
66
^\[main::spec1\] .* REFUTED$
77
^Counterexample:$
8-
^ 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$
9-
^main::var::x 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$
10-
^main::var::y 0 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 190 200$
11-
^main::var::z 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0$
8+
^ 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$
9+
^x 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$
10+
^y 0 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 190 200$
11+
^z 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0$
1212
--
1313
^warning: ignoring

‎src/smvlang/expr2smv.cpp

Lines changed: 27 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -6,17 +6,23 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#include <cstring>
9+
//#include <cstring>
10+
11+
#include "expr2smv.h"
1012

1113
#include <util/lispexpr.h>
1214
#include <util/lispirep.h>
15+
#include <util/namespace.h>
1316
#include <util/std_expr.h>
14-
15-
#include "expr2smv.h"
17+
#include <util/symbol.h>
1618

1719
class expr2smvt
1820
{
1921
public:
22+
explicit expr2smvt(const namespacet &__ns) : ns(__ns)
23+
{
24+
}
25+
2026
bool convert_nondet_choice(const exprt &src, std::string &dest, unsigned precedence);
2127

2228
bool convert_binary(const exprt &src, std::string &dest, const std::string &symbol, unsigned precedence);
@@ -34,7 +40,8 @@ class expr2smvt
3440

3541
bool convert(const exprt &src, std::string &dest);
3642

37-
bool convert_symbol(const exprt &src, std::string &dest, unsigned &precedence);
43+
bool
44+
convert_symbol(const symbol_exprt &, std::string &dest, unsigned &precedence);
3845

3946
bool convert_next_symbol(const exprt &src, std::string &dest, unsigned &precedence);
4047

@@ -45,6 +52,9 @@ class expr2smvt
4552
bool convert_norep(const exprt &src, std::string &dest, unsigned &precedence);
4653

4754
bool convert(const typet &src, std::string &dest);
55+
56+
protected:
57+
const namespacet &ns;
4858
};
4959

5060
/*
@@ -312,15 +322,15 @@ Function: expr2smvt::convert_symbol
312322
\*******************************************************************/
313323

314324
bool expr2smvt::convert_symbol(
315-
const exprt &src,
325+
const symbol_exprt &src,
316326
std::string &dest,
317327
unsigned &precedence)
318328
{
319329
precedence=SMV_MAX_PRECEDENCE;
320-
dest=src.get_string(ID_identifier);
321-
322-
if(strncmp(dest.c_str(), "smv::", 5)==0)
323-
dest.erase(0, 5);
330+
331+
auto &symbol = ns.lookup(src);
332+
333+
dest = id2string(symbol.display_name());
324334

325335
return false;
326336
}
@@ -343,7 +353,8 @@ bool expr2smvt::convert_next_symbol(
343353
unsigned &precedence)
344354
{
345355
std::string tmp;
346-
convert_symbol(src, tmp, precedence);
356+
convert_symbol(
357+
symbol_exprt{src.get(ID_identifier), src.type()}, tmp, precedence);
347358

348359
dest="next("+tmp+")";
349360

@@ -468,7 +479,7 @@ bool expr2smvt::convert(
468479
to_unary_expr(src), dest, src.id_string() + " ", precedence = 7);
469480

470481
else if(src.id()==ID_symbol)
471-
return convert_symbol(src, dest, precedence);
482+
return convert_symbol(to_symbol_expr(src), dest, precedence);
472483

473484
else if(src.id()==ID_next_symbol)
474485
return convert_next_symbol(src, dest, precedence);
@@ -527,9 +538,9 @@ Function: expr2smv
527538
528539
\*******************************************************************/
529540

530-
bool expr2smv(const exprt &expr, std::string &code)
541+
bool expr2smv(const exprt &expr, std::string &code, const namespacet &ns)
531542
{
532-
expr2smvt expr2smv;
543+
expr2smvt expr2smv(ns);
533544
return expr2smv.convert(expr, code);
534545
}
535546

@@ -545,14 +556,14 @@ Function: type2smv
545556
546557
\*******************************************************************/
547558

548-
bool type2smv(const typet &type, std::string &code)
559+
bool type2smv(const typet &type, std::string &code, const namespacet &ns)
549560
{
550561
if(type.id()==ID_bool)
551562
code="boolean";
552563
else if(type.id()==ID_array)
553564
{
554565
std::string tmp;
555-
if(type2smv(to_array_type(type).element_type(), tmp))
566+
if(type2smv(to_array_type(type).element_type(), tmp, ns))
556567
return true;
557568
code="array ";
558569
code+="..";
@@ -587,7 +598,7 @@ bool type2smv(const typet &type, std::string &code)
587598
{
588599
if(first) first=false; else code+=", ";
589600
std::string tmp;
590-
expr2smv(*it, tmp);
601+
expr2smv(*it, tmp, ns);
591602
code+=tmp;
592603
}
593604
code+=')';

‎src/smvlang/expr2smv.h

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,5 @@ Author: Daniel Kroening, [email protected]
88

99
#include <util/expr.h>
1010

11-
bool expr2smv(const exprt &expr, std::string &code);
12-
bool type2smv(const typet &type, std::string &code);
13-
11+
bool expr2smv(const exprt &, std::string &code, const namespacet &);
12+
bool type2smv(const typet &, std::string &code, const namespacet &);

‎src/smvlang/smv_language.cpp

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,14 @@ Author: Daniel Kroening, [email protected]
77
\*******************************************************************/
88

99
#include "smv_language.h"
10-
#include "smv_typecheck.h"
11-
#include "smv_parser.h"
12-
#include "expr2smv.h"
1310

11+
#include <util/namespace.h>
1412
#include <util/symbol_table.h>
1513

14+
#include "expr2smv.h"
15+
#include "smv_parser.h"
16+
#include "smv_typecheck.h"
17+
1618
/*******************************************************************\
1719
1820
Function: smv_languaget::parse
@@ -153,7 +155,9 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &)
153155
if(it->second.type.id()!="submodule")
154156
{
155157
std::string msg;
156-
type2smv(it->second.type, msg);
158+
symbol_tablet symbol_table;
159+
namespacet ns(symbol_table);
160+
type2smv(it->second.type, msg, ns);
157161
out << " " << it->first << ": "
158162
<< msg << ";" << std::endl;
159163
}
@@ -168,7 +172,9 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &)
168172
if(it->second.type.id()=="submodule")
169173
{
170174
std::string msg;
171-
type2smv(it->second.type, msg);
175+
symbol_tablet symbol_table;
176+
namespacet ns(symbol_table);
177+
type2smv(it->second.type, msg, ns);
172178
out << " " << it->first << ": "
173179
<< msg << ";" << std::endl;
174180
}
@@ -201,7 +207,7 @@ Function: smv_languaget::from_expr
201207
bool smv_languaget::from_expr(const exprt &expr, std::string &code,
202208
const namespacet &ns)
203209
{
204-
return expr2smv(expr, code);
210+
return expr2smv(expr, code, ns);
205211
}
206212

207213
/*******************************************************************\
@@ -221,7 +227,7 @@ bool smv_languaget::from_type(
221227
std::string &code,
222228
const namespacet &ns)
223229
{
224-
return type2smv(type, code);
230+
return type2smv(type, code, ns);
225231
}
226232

227233
/*******************************************************************\

0 commit comments

Comments
 (0)