From 3ec49b525ff424485977f07ef9cc1362ef1cc188 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 21 Apr 2024 16:04:19 -0700 Subject: [PATCH] SMV: set pretty names for top-level identifiers Identifiers in module main now no longer carry the prefix main::var::. --- regression/ebmc/BDD/BDD1.desc | 2 +- regression/ebmc/range_type/range_type1.desc | 2 +- regression/ebmc/range_type/range_type2.desc | 2 +- regression/ebmc/range_type/range_type4.desc | 2 +- regression/ebmc/range_type/range_type5.desc | 2 +- regression/ebmc/small-test1/test.desc | 2 +- regression/ebmc/small-test2/test.desc | 2 +- .../ebmc/smv/bdd_unsupported_property.desc | 4 +- .../ebmc/smv/bmc_unsupported_property1.desc | 4 +- .../ebmc/smv/bmc_unsupported_property2.desc | 4 +- .../ebmc/smv/bmc_unsupported_property3.desc | 4 +- regression/ebmc/smv/initial1.desc | 4 +- regression/ebmc/smv/smv_ltlspec1.desc | 2 +- regression/ebmc/smv/smv_ltlspec2.desc | 2 +- regression/ebmc/smv/smv_ltlspec3.desc | 8 ++-- regression/ebmc/smv/smv_ltlspec4.desc | 11 ++--- regression/ebmc/traces/numbered1.desc | 6 +-- regression/ebmc/traces/waveform1.desc | 8 ++-- src/smvlang/expr2smv.cpp | 41 +++++++++++-------- src/smvlang/expr2smv.h | 5 +-- src/smvlang/smv_language.cpp | 20 +++++---- src/smvlang/smv_typecheck.cpp | 34 +++++++++++---- 22 files changed, 103 insertions(+), 68 deletions(-) diff --git a/regression/ebmc/BDD/BDD1.desc b/regression/ebmc/BDD/BDD1.desc index 7ffde124a..649e39aa2 100644 --- a/regression/ebmc/BDD/BDD1.desc +++ b/regression/ebmc/BDD/BDD1.desc @@ -3,6 +3,6 @@ BDD1.smv --bdd ^EXIT=0$ ^SIGNAL=0$ -^\[main::spec1\] AG \(!main::var::some_var = off\): PROVED$ +^\[main::spec1\] AG \(!some_var = off\): PROVED$ -- ^warning: ignoring diff --git a/regression/ebmc/range_type/range_type1.desc b/regression/ebmc/range_type/range_type1.desc index b16bfa575..1bd21a32e 100644 --- a/regression/ebmc/range_type/range_type1.desc +++ b/regression/ebmc/range_type/range_type1.desc @@ -3,6 +3,6 @@ range_type1.smv --bound 10 ^EXIT=0$ ^SIGNAL=0$ -^\[main::spec1\] AG main::var::x != 4: PROVED up to bound 10$ +^\[main::spec1\] AG x != 4: PROVED up to bound 10$ -- ^warning: ignoring diff --git a/regression/ebmc/range_type/range_type2.desc b/regression/ebmc/range_type/range_type2.desc index ac4c9b349..c4d238377 100644 --- a/regression/ebmc/range_type/range_type2.desc +++ b/regression/ebmc/range_type/range_type2.desc @@ -4,6 +4,6 @@ range_type2.smv ^EXIT=0$ ^SIGNAL=0$ ^\[main::spec1\] AG TRUE: PROVED up to bound 10$ -^\[main::spec2\] AG main::var::NET_tmp9: PROVED up to bound 10$ +^\[main::spec2\] AG NET_tmp9: PROVED up to bound 10$ -- ^warning: ignoring diff --git a/regression/ebmc/range_type/range_type4.desc b/regression/ebmc/range_type/range_type4.desc index 5c8422e15..49991cb4b 100644 --- a/regression/ebmc/range_type/range_type4.desc +++ b/regression/ebmc/range_type/range_type4.desc @@ -3,6 +3,6 @@ range_type4.smv --bound 10 ^EXIT=0$ ^SIGNAL=0$ -^\[main::spec1\] AG \(!main::var::x = 6\): PROVED up to bound 10$ +^\[main::spec1\] AG \(!x = 6\): PROVED up to bound 10$ -- ^warning: ignoring diff --git a/regression/ebmc/range_type/range_type5.desc b/regression/ebmc/range_type/range_type5.desc index 74664675c..ef6f95259 100644 --- a/regression/ebmc/range_type/range_type5.desc +++ b/regression/ebmc/range_type/range_type5.desc @@ -3,6 +3,6 @@ range_type5.smv --bound 3 ^EXIT=0$ ^SIGNAL=0$ -^\[main::spec1\] AG \(!main::var::x = 6\): PROVED up to bound 3$ +^\[main::spec1\] AG \(!x = 6\): PROVED up to bound 3$ -- ^warning: ignoring diff --git a/regression/ebmc/small-test1/test.desc b/regression/ebmc/small-test1/test.desc index 775500ca4..01ce9e93b 100644 --- a/regression/ebmc/small-test1/test.desc +++ b/regression/ebmc/small-test1/test.desc @@ -3,6 +3,6 @@ main.smv --bound 10 --trace ^EXIT=10$ ^SIGNAL=0$ -^\[main::spec1\] AG main::var::x = 1: REFUTED$ +^\[main::spec1\] AG x = 1: REFUTED$ -- ^warning: ignoring diff --git a/regression/ebmc/small-test2/test.desc b/regression/ebmc/small-test2/test.desc index d7e7ae61b..8e84aa5aa 100644 --- a/regression/ebmc/small-test2/test.desc +++ b/regression/ebmc/small-test2/test.desc @@ -3,6 +3,6 @@ main.smv --bound 2 ^EXIT=10$ ^SIGNAL=0$ -^\[main::spec1\] AG main::var::z: REFUTED$ +^\[main::spec1\] AG z: REFUTED$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/bdd_unsupported_property.desc b/regression/ebmc/smv/bdd_unsupported_property.desc index 53fa65ac0..85624f367 100644 --- a/regression/ebmc/smv/bdd_unsupported_property.desc +++ b/regression/ebmc/smv/bdd_unsupported_property.desc @@ -3,7 +3,7 @@ bdd_unsupported_property.smv --bdd ^EXIT=10$ ^SIGNAL=0$ -^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BDD engine$ -^\[main::spec2\] G main::var::x = FALSE: REFUTED$ +^\[main::spec1\] !G x = FALSE: FAILURE: property not supported by BDD engine$ +^\[main::spec2\] G x = FALSE: REFUTED$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/bmc_unsupported_property1.desc b/regression/ebmc/smv/bmc_unsupported_property1.desc index b18e1ed1a..e1b60e7d1 100644 --- a/regression/ebmc/smv/bmc_unsupported_property1.desc +++ b/regression/ebmc/smv/bmc_unsupported_property1.desc @@ -3,7 +3,7 @@ bmc_unsupported_property1.smv ^EXIT=10$ ^SIGNAL=0$ -^\[main::spec1\] EG main::var::x = FALSE: FAILURE: property not supported by BMC engine$ -^\[main::spec2\] G main::var::x = FALSE: REFUTED$ +^\[main::spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$ +^\[main::spec2\] G x = FALSE: REFUTED$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/bmc_unsupported_property2.desc b/regression/ebmc/smv/bmc_unsupported_property2.desc index fcb52b210..b9daf9b57 100644 --- a/regression/ebmc/smv/bmc_unsupported_property2.desc +++ b/regression/ebmc/smv/bmc_unsupported_property2.desc @@ -3,7 +3,7 @@ bmc_unsupported_property2.smv ^EXIT=10$ ^SIGNAL=0$ -^\[main::spec1\] EG main::var::x = FALSE: FAILURE: property not supported by BMC engine$ -^\[main::spec2\] G main::var::x = TRUE: PROVED up to bound 1$ +^\[main::spec1\] EG x = FALSE: FAILURE: property not supported by BMC engine$ +^\[main::spec2\] G x = TRUE: PROVED up to bound 1$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/bmc_unsupported_property3.desc b/regression/ebmc/smv/bmc_unsupported_property3.desc index 8640ec9d2..a464d9501 100644 --- a/regression/ebmc/smv/bmc_unsupported_property3.desc +++ b/regression/ebmc/smv/bmc_unsupported_property3.desc @@ -3,7 +3,7 @@ bmc_unsupported_property3.smv --aig ^EXIT=10$ ^SIGNAL=0$ -^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by netlist BMC engine$ -^\[main::spec2\] G main::var::x = FALSE: REFUTED$ +^\[main::spec1\] !G x = FALSE: FAILURE: property not supported by netlist BMC engine$ +^\[main::spec2\] G x = FALSE: REFUTED$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/initial1.desc b/regression/ebmc/smv/initial1.desc index 43ca566e8..e9cd78b86 100644 --- a/regression/ebmc/smv/initial1.desc +++ b/regression/ebmc/smv/initial1.desc @@ -1,8 +1,8 @@ CORE initial1.smv --bound 0 -^\[main::spec1\] main::var::tmp1 = TRUE: PROVED up to bound 0$ -^\[main::spec2\] main::var::tmp2 = TRUE: REFUTED$ +^\[main::spec1\] tmp1 = TRUE: PROVED up to bound 0$ +^\[main::spec2\] tmp2 = TRUE: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/smv/smv_ltlspec1.desc b/regression/ebmc/smv/smv_ltlspec1.desc index eb52b11ac..05bfdb7a5 100644 --- a/regression/ebmc/smv/smv_ltlspec1.desc +++ b/regression/ebmc/smv/smv_ltlspec1.desc @@ -3,6 +3,6 @@ smv_ltlspec1.smv --bdd ^EXIT=0$ ^SIGNAL=0$ -^\[main::spec1\] G main::var::x != 0: PROVED$ +^\[main::spec1\] G x != 0: PROVED$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/smv_ltlspec2.desc b/regression/ebmc/smv/smv_ltlspec2.desc index 0cda50b46..47298d4cc 100644 --- a/regression/ebmc/smv/smv_ltlspec2.desc +++ b/regression/ebmc/smv/smv_ltlspec2.desc @@ -3,7 +3,7 @@ smv_ltlspec2.smv --bdd ^EXIT=0$ ^SIGNAL=0$ -^\[smv::main::spec1\] G F main::var::x = 3: PROVED$ +^\[smv::main::spec1\] G F x = 3: PROVED$ -- ^warning: ignoring -- diff --git a/regression/ebmc/smv/smv_ltlspec3.desc b/regression/ebmc/smv/smv_ltlspec3.desc index 0b435985f..6fb16061c 100644 --- a/regression/ebmc/smv/smv_ltlspec3.desc +++ b/regression/ebmc/smv/smv_ltlspec3.desc @@ -3,10 +3,10 @@ smv_ltlspec3.smv --bound 10 --numbered-trace ^EXIT=10$ ^SIGNAL=0$ -^\[main::spec1\] X X main::var::x = TRUE: REFUTED$ +^\[main::spec1\] X X x = TRUE: REFUTED$ ^Counterexample with 3 states:$ -^main::var::x@0 = FALSE$ -^main::var::x@1 = FALSE$ -^main::var::x@2 = FALSE$ +^x@0 = FALSE$ +^x@1 = FALSE$ +^x@2 = FALSE$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/smv_ltlspec4.desc b/regression/ebmc/smv/smv_ltlspec4.desc index 93b6fff8a..f96cb0e12 100644 --- a/regression/ebmc/smv/smv_ltlspec4.desc +++ b/regression/ebmc/smv/smv_ltlspec4.desc @@ -3,11 +3,12 @@ smv_ltlspec4.smv --bound 10 --numbered-trace ^EXIT=10$ ^SIGNAL=0$ -^\[main::spec1\] F main::var::x = 0: REFUTED$ -^main::var::x@0 = 1$ -^main::var::x@1 = 2$ -^main::var::x@2 = 2$ -^\[main::spec2\] F main::var::x = 2: PROVED up to bound 10$ +^\[main::spec1\] F x = 0: REFUTED$ +^Counterexample with 3 states:$ +^x@0 = 1$ +^x@1 = 2$ +^x@2 = 2$ +^\[main::spec2\] F x = 2: PROVED up to bound 10$ -- ^warning: ignoring -- diff --git a/regression/ebmc/traces/numbered1.desc b/regression/ebmc/traces/numbered1.desc index 7945483aa..f2b583d3a 100644 --- a/regression/ebmc/traces/numbered1.desc +++ b/regression/ebmc/traces/numbered1.desc @@ -5,8 +5,8 @@ waveform1.smv ^SIGNAL=0$ ^\[main::spec1\] .* REFUTED$ ^Counterexample with 21 states:$ -^main::var::y@0 = 0$ -^main::var::y@10 = 100$ -^main::var::y@20 = 200$ +^y@0 = 0$ +^y@10 = 100$ +^y@20 = 200$ -- ^warning: ignoring diff --git a/regression/ebmc/traces/waveform1.desc b/regression/ebmc/traces/waveform1.desc index af2254285..51fdb8d59 100644 --- a/regression/ebmc/traces/waveform1.desc +++ b/regression/ebmc/traces/waveform1.desc @@ -5,9 +5,9 @@ waveform1.smv ^SIGNAL=0$ ^\[main::spec1\] .* REFUTED$ ^Counterexample:$ -^ 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$ -^main::var::x 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$ -^main::var::y 0 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 190 200$ -^main::var::z 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0$ +^ 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$ +^x 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20$ +^y 0 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 190 200$ +^z 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0$ -- ^warning: ignoring diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp index 0b5f21eb3..278defb6d 100644 --- a/src/smvlang/expr2smv.cpp +++ b/src/smvlang/expr2smv.cpp @@ -6,17 +6,21 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include +#include "expr2smv.h" #include #include +#include #include - -#include "expr2smv.h" +#include class expr2smvt { public: + explicit expr2smvt(const namespacet &__ns) : ns(__ns) + { + } + bool convert_nondet_choice(const exprt &src, std::string &dest, unsigned precedence); bool convert_binary(const exprt &src, std::string &dest, const std::string &symbol, unsigned precedence); @@ -34,7 +38,8 @@ class expr2smvt bool convert(const exprt &src, std::string &dest); - bool convert_symbol(const exprt &src, std::string &dest, unsigned &precedence); + bool + convert_symbol(const symbol_exprt &, std::string &dest, unsigned &precedence); bool convert_next_symbol(const exprt &src, std::string &dest, unsigned &precedence); @@ -45,6 +50,9 @@ class expr2smvt bool convert_norep(const exprt &src, std::string &dest, unsigned &precedence); bool convert(const typet &src, std::string &dest); + +protected: + const namespacet &ns; }; /* @@ -312,15 +320,15 @@ Function: expr2smvt::convert_symbol \*******************************************************************/ bool expr2smvt::convert_symbol( - const exprt &src, + const symbol_exprt &src, std::string &dest, unsigned &precedence) { precedence=SMV_MAX_PRECEDENCE; - dest=src.get_string(ID_identifier); - - if(strncmp(dest.c_str(), "smv::", 5)==0) - dest.erase(0, 5); + + auto &symbol = ns.lookup(src); + + dest = id2string(symbol.display_name()); return false; } @@ -343,7 +351,8 @@ bool expr2smvt::convert_next_symbol( unsigned &precedence) { std::string tmp; - convert_symbol(src, tmp, precedence); + convert_symbol( + symbol_exprt{src.get(ID_identifier), src.type()}, tmp, precedence); dest="next("+tmp+")"; @@ -468,7 +477,7 @@ bool expr2smvt::convert( to_unary_expr(src), dest, src.id_string() + " ", precedence = 7); else if(src.id()==ID_symbol) - return convert_symbol(src, dest, precedence); + return convert_symbol(to_symbol_expr(src), dest, precedence); else if(src.id()==ID_next_symbol) return convert_next_symbol(src, dest, precedence); @@ -527,9 +536,9 @@ Function: expr2smv \*******************************************************************/ -bool expr2smv(const exprt &expr, std::string &code) +bool expr2smv(const exprt &expr, std::string &code, const namespacet &ns) { - expr2smvt expr2smv; + expr2smvt expr2smv(ns); return expr2smv.convert(expr, code); } @@ -545,14 +554,14 @@ Function: type2smv \*******************************************************************/ -bool type2smv(const typet &type, std::string &code) +bool type2smv(const typet &type, std::string &code, const namespacet &ns) { if(type.id()==ID_bool) code="boolean"; else if(type.id()==ID_array) { std::string tmp; - if(type2smv(to_array_type(type).element_type(), tmp)) + if(type2smv(to_array_type(type).element_type(), tmp, ns)) return true; code="array "; code+=".."; @@ -587,7 +596,7 @@ bool type2smv(const typet &type, std::string &code) { if(first) first=false; else code+=", "; std::string tmp; - expr2smv(*it, tmp); + expr2smv(*it, tmp, ns); code+=tmp; } code+=')'; diff --git a/src/smvlang/expr2smv.h b/src/smvlang/expr2smv.h index 3e5a9f8f3..16a76b7eb 100644 --- a/src/smvlang/expr2smv.h +++ b/src/smvlang/expr2smv.h @@ -8,6 +8,5 @@ Author: Daniel Kroening, kroening@kroening.com #include -bool expr2smv(const exprt &expr, std::string &code); -bool type2smv(const typet &type, std::string &code); - +bool expr2smv(const exprt &, std::string &code, const namespacet &); +bool type2smv(const typet &, std::string &code, const namespacet &); diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp index 35d988eea..4b83f2c6a 100644 --- a/src/smvlang/smv_language.cpp +++ b/src/smvlang/smv_language.cpp @@ -7,12 +7,14 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include "smv_language.h" -#include "smv_typecheck.h" -#include "smv_parser.h" -#include "expr2smv.h" +#include #include +#include "expr2smv.h" +#include "smv_parser.h" +#include "smv_typecheck.h" + /*******************************************************************\ Function: smv_languaget::parse @@ -153,7 +155,9 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &) if(it->second.type.id()!="submodule") { std::string msg; - type2smv(it->second.type, msg); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + type2smv(it->second.type, msg, ns); out << " " << it->first << ": " << msg << ";" << std::endl; } @@ -168,7 +172,9 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &) if(it->second.type.id()=="submodule") { std::string msg; - type2smv(it->second.type, msg); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + type2smv(it->second.type, msg, ns); out << " " << it->first << ": " << msg << ";" << std::endl; } @@ -201,7 +207,7 @@ Function: smv_languaget::from_expr bool smv_languaget::from_expr(const exprt &expr, std::string &code, const namespacet &ns) { - return expr2smv(expr, code); + return expr2smv(expr, code, ns); } /*******************************************************************\ @@ -221,7 +227,7 @@ bool smv_languaget::from_type( std::string &code, const namespacet &ns) { - return type2smv(type, code); + return type2smv(type, code, ns); } /*******************************************************************\ diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 9d5580269..f6e1d320d 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -6,19 +6,21 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include -#include -#include +#include "smv_typecheck.h" #include #include #include +#include #include #include -#include "smv_typecheck.h" #include "expr2smv.h" +#include +#include +#include + class smv_typecheckt:public typecheckt { public: @@ -351,6 +353,16 @@ void smv_typecheckt::instantiate( symbol.name=new_prefix+id2string(symbol.base_name); symbol.module=smv_module.name; + if(smv_module.name == "smv::main") + { + symbol.pretty_name = + id2string(instance) + '.' + id2string(symbol.base_name); + } + else + { + symbol.pretty_name = strip_smv_prefix(symbol.name); + } + rename_map.insert( std::pair(s_it2->first, symbol.symbol_expr())); @@ -1121,7 +1133,8 @@ Function: smv_typecheckt::to_string std::string smv_typecheckt::to_string(const exprt &expr) { std::string result; - expr2smv(expr, result); + namespacet ns(symbol_table); + expr2smv(expr, result, ns); return result; } @@ -1140,7 +1153,8 @@ Function: smv_typecheckt::to_string std::string smv_typecheckt::to_string(const typet &type) { std::string result; - type2smv(type, result); + namespacet ns(symbol_table); + type2smv(type, result, ns); return result; } @@ -1228,11 +1242,17 @@ void smv_typecheckt::convert(smv_parse_treet::mc_varst &vars) symbol.base_name=it->first; if(var.identifier=="") + { symbol.name=module+"::var::"+id2string(symbol.base_name); + + if(module == "smv::main") + symbol.pretty_name = symbol.base_name; + else + symbol.pretty_name = strip_smv_prefix(symbol.name); + } else symbol.name=var.identifier; - symbol.pretty_name = strip_smv_prefix(symbol.name); symbol.value.make_nil(); symbol.is_input=true; symbol.is_state_var=false;