Property description now taken from front-end

This moves the generation of the property description into the front-end,
which will enable doing lowering or model instrumentation in the front-end
while displaying the property as given in the source language.

Author: kroening

regression/ebmc/CLI/json-properties.desc

@@ -4,7 +4,7 @@ json-properties.v
 activate-multi-line-match
 \[
   \{
-    "description": "",
+    "description": "always 1 == 2",
     "location": \{
       "file": "json-properties\.v",
       "line": "3",

src/ebmc/ebmc_properties.cpp

@@ -73,7 +73,6 @@ ebmc_propertiest ebmc_propertiest::from_transition_system(
       properties.properties.back().name = symbol.display_name();
       properties.properties.back().original_expr = symbol.value;
       properties.properties.back().location = symbol.location;
-      properties.properties.back().expr_string = value_as_string;
       properties.properties.back().mode = symbol.mode;
       properties.properties.back().description =
         id2string(symbol.location.get_comment());
@@ -172,10 +171,9 @@ ebmc_propertiest ebmc_propertiest::from_command_line(
     auto &p = properties.properties.back();
     p.original_expr = expr;
     p.normalized_expr = normalize_property(expr);
-    p.expr_string = expr_as_string;
     p.mode = transition_system.main_symbol->mode;
     p.location.make_nil();
-    p.description = "command-line assertion";
+    p.description = expr_as_string;
     p.name = "command-line assertion";
 
     return properties;

src/ebmc/ebmc_properties.h

@@ -28,7 +28,6 @@ class ebmc_propertiest
     std::size_t number = 0;
     irep_idt identifier, name;
     source_locationt location;
-    std::string expr_string;
     irep_idt mode;
     exprt original_expr;
     exprt normalized_expr;

src/ebmc/liveness_to_safety.cpp

@@ -246,7 +246,7 @@ void liveness_to_safetyt::operator()()
       else
       {
         throw ebmc_errort().with_location(property.location)
-          << "no liveness-to-safety translation for " << property.expr_string;
+          << "no liveness-to-safety translation for " << property.description;
       }
     }
   }

src/ebmc/report_results.cpp

@@ -98,7 +98,7 @@ void report_results(
       if(property.is_disabled())
         continue;
 
-      message.status() << "[" << property.name << "] " << property.expr_string
+      message.status() << "[" << property.name << "] " << property.description
                        << ": ";
 
       using statust = ebmc_propertiest::propertyt::statust;

src/ebmc/show_properties.cpp

@@ -33,36 +33,37 @@ void ebmc_baset::show_properties()
 {
   unsigned p_nr=1;
 
+  auto make_xml =
+    [](const ebmc_propertiest::propertyt &p, std::size_t p_nr) -> xmlt {
+    xmlt xml("property");
+    xml.set_attribute("name", id2string(p.name));
+
+    xml.new_element("number").data = std::to_string(p_nr); // will go away
+    xml.new_element("description").data = p.description;
+
+    if(p.location.is_not_nil())
+      xml.new_element("location") = ::xml(p.location);
+
+    return xml;
+  };
+
   for(const auto &p : properties.properties)
   {
-    switch (static_cast<ui_message_handlert &>(message.get_message_handler()).get_ui()) {
+    switch(static_cast<ui_message_handlert &>(message.get_message_handler())
+             .get_ui())
+    {
     case ui_message_handlert::uit::XML_UI:
-      {
-        xmlt xml("property");
-        xml.set_attribute("name", id2string(p.name));
-        
-        xml.new_element("number").data=std::to_string(p_nr); // will go away
-        xml.new_element("expression").data=p.expr_string;
-        xml.new_element("description").data=p.description;
-
-        if(p.location.is_not_nil())
-          xml.new_element("location")=::xml(p.location);
-
-        std::cout << xml << '\n';
-      }
+      std::cout << make_xml(p, p_nr) << '\n';
       break;
 
     case ui_message_handlert::uit::PLAIN:
-      std::cout << p.name << ": ";
-      std::cout << p.expr_string;
-      if(!p.description.empty())
-        std::cout << " (" << p.description << ")";
-      std::cout << '\n';
+      std::cout << p.name << ": " << p.description << '\n';
       break;
+
     case ui_message_handlert::uit::JSON_UI:
     default:;
     }
-    
+
     p_nr++;
   }
 }

src/smvlang/smv_typecheck.cpp

@@ -1491,6 +1491,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
         spec_symbol.mode = "SMV";
         spec_symbol.value = it->expr;
         spec_symbol.location = it->location;
+        spec_symbol.location.set_comment(to_string(it->expr));
 
         if(smv_module.name == "smv::main")
           spec_symbol.pretty_name = spec_symbol.base_name;

src/verilog/verilog_synthesis.cpp

@@ -2323,6 +2323,8 @@ void verilog_synthesist::synth_assert_assume_cover(
     cond = sva_cover_exprt(cond);
   }
 
+  symbol.location.set_comment(to_string(cond));
+
   symbol.value = std::move(cond);
 }
 
@@ -2374,6 +2376,8 @@ void verilog_synthesist::synth_assert_assume_cover(
   else
     PRECONDITION(false);
 
+  symbol.location.set_comment(to_string(cond));
+
   symbol.value = std::move(cond);
 }