Skip to content

Commit 3ec49b5

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 2a129e6 commit 3ec49b5

22 files changed

+103
-68
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\] EG main::var::x = FALSE: FAILURE: property not supported by BMC engine$
7-
^\[main::spec2\] G main::var::x = FALSE: REFUTED$
6+
^\[main::spec1\] EG 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\] EG 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\] EG 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/bmc_unsupported_property3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ bmc_unsupported_property3.smv
33
--aig
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by netlist BMC engine$
7-
^\[main::spec2\] G main::var::x = FALSE: REFUTED$
6+
^\[main::spec1\] !G x = FALSE: FAILURE: property not supported by netlist BMC engine$
7+
^\[main::spec2\] G x = FALSE: REFUTED$
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,10 +3,10 @@ smv_ltlspec3.smv
33
--bound 10 --numbered-trace
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main::spec1\] X X main::var::x = TRUE: REFUTED$
6+
^\[main::spec1\] X X x = TRUE: REFUTED$
77
^Counterexample with 3 states:$
8-
^main::var::x@0 = FALSE$
9-
^main::var::x@1 = FALSE$
10-
^main::var::x@2 = FALSE$
8+
^x@0 = FALSE$
9+
^x@1 = FALSE$
10+
^x@2 = FALSE$
1111
--
1212
^warning: ignoring

‎regression/ebmc/smv/smv_ltlspec4.desc

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,12 @@ smv_ltlspec4.smv
33
--bound 10 --numbered-trace
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main::spec1\] F main::var::x = 0: REFUTED$
7-
^main::var::x@0 = 1$
8-
^main::var::x@1 = 2$
9-
^main::var::x@2 = 2$
10-
^\[main::spec2\] F main::var::x = 2: PROVED up to bound 10$
6+
^\[main::spec1\] F x = 0: REFUTED$
7+
^Counterexample with 3 states:$
8+
^x@0 = 1$
9+
^x@1 = 2$
10+
^x@2 = 2$
11+
^\[main::spec2\] F x = 2: PROVED up to bound 10$
1112
--
1213
^warning: ignoring
1314
--

‎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 with 21 states:$
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: 25 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -6,17 +6,21 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#include <cstring>
9+
#include "expr2smv.h"
1010

1111
#include <util/lispexpr.h>
1212
#include <util/lispirep.h>
13+
#include <util/namespace.h>
1314
#include <util/std_expr.h>
14-
15-
#include "expr2smv.h"
15+
#include <util/symbol.h>
1616

1717
class expr2smvt
1818
{
1919
public:
20+
explicit expr2smvt(const namespacet &__ns) : ns(__ns)
21+
{
22+
}
23+
2024
bool convert_nondet_choice(const exprt &src, std::string &dest, unsigned precedence);
2125

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

3539
bool convert(const exprt &src, std::string &dest);
3640

37-
bool convert_symbol(const exprt &src, std::string &dest, unsigned &precedence);
41+
bool
42+
convert_symbol(const symbol_exprt &, std::string &dest, unsigned &precedence);
3843

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

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

4752
bool convert(const typet &src, std::string &dest);
53+
54+
protected:
55+
const namespacet &ns;
4856
};
4957

5058
/*
@@ -312,15 +320,15 @@ Function: expr2smvt::convert_symbol
312320
\*******************************************************************/
313321

314322
bool expr2smvt::convert_symbol(
315-
const exprt &src,
323+
const symbol_exprt &src,
316324
std::string &dest,
317325
unsigned &precedence)
318326
{
319327
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);
328+
329+
auto &symbol = ns.lookup(src);
330+
331+
dest = id2string(symbol.display_name());
324332

325333
return false;
326334
}
@@ -343,7 +351,8 @@ bool expr2smvt::convert_next_symbol(
343351
unsigned &precedence)
344352
{
345353
std::string tmp;
346-
convert_symbol(src, tmp, precedence);
354+
convert_symbol(
355+
symbol_exprt{src.get(ID_identifier), src.type()}, tmp, precedence);
347356

348357
dest="next("+tmp+")";
349358

@@ -468,7 +477,7 @@ bool expr2smvt::convert(
468477
to_unary_expr(src), dest, src.id_string() + " ", precedence = 7);
469478

470479
else if(src.id()==ID_symbol)
471-
return convert_symbol(src, dest, precedence);
480+
return convert_symbol(to_symbol_expr(src), dest, precedence);
472481

473482
else if(src.id()==ID_next_symbol)
474483
return convert_next_symbol(src, dest, precedence);
@@ -527,9 +536,9 @@ Function: expr2smv
527536
528537
\*******************************************************************/
529538

530-
bool expr2smv(const exprt &expr, std::string &code)
539+
bool expr2smv(const exprt &expr, std::string &code, const namespacet &ns)
531540
{
532-
expr2smvt expr2smv;
541+
expr2smvt expr2smv(ns);
533542
return expr2smv.convert(expr, code);
534543
}
535544

@@ -545,14 +554,14 @@ Function: type2smv
545554
546555
\*******************************************************************/
547556

548-
bool type2smv(const typet &type, std::string &code)
557+
bool type2smv(const typet &type, std::string &code, const namespacet &ns)
549558
{
550559
if(type.id()==ID_bool)
551560
code="boolean";
552561
else if(type.id()==ID_array)
553562
{
554563
std::string tmp;
555-
if(type2smv(to_array_type(type).element_type(), tmp))
564+
if(type2smv(to_array_type(type).element_type(), tmp, ns))
556565
return true;
557566
code="array ";
558567
code+="..";
@@ -587,7 +596,7 @@ bool type2smv(const typet &type, std::string &code)
587596
{
588597
if(first) first=false; else code+=", ";
589598
std::string tmp;
590-
expr2smv(*it, tmp);
599+
expr2smv(*it, tmp, ns);
591600
code+=tmp;
592601
}
593602
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)