Merge pull request #452 from diffblue/smvlang-pretty-names

kroening · web-flow · commit 3c311747376b · 2024-04-23T14:22:03.000-07:00
SMV: set pretty names for top-level identifiers
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -6,17 +6,21 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <cstring>
+#include "expr2smv.h"
 
 #include <util/lispexpr.h>
 #include <util/lispirep.h>
+#include <util/namespace.h>
 #include <util/std_expr.h>
-
-#include "expr2smv.h"
+#include <util/symbol.h>
 
 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
@@ -8,6 +8,5 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/expr.h>
 
-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
@@ -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 <util/namespace.h>
 #include <util/symbol_table.h>
 
+#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
