From 00a34b4829a9fe6d13bdaebfa440a7fca9c59c92 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 22 Jun 2024 11:01:10 -0700 Subject: [PATCH] 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. --- regression/ebmc/CLI/json-properties.desc | 2 +- src/ebmc/ebmc_properties.cpp | 4 +-- src/ebmc/ebmc_properties.h | 1 - src/ebmc/liveness_to_safety.cpp | 2 +- src/ebmc/report_results.cpp | 2 +- src/ebmc/show_properties.cpp | 41 ++++++++++++------------ src/smvlang/smv_typecheck.cpp | 1 + src/verilog/verilog_synthesis.cpp | 4 +++ 8 files changed, 30 insertions(+), 27 deletions(-) diff --git a/regression/ebmc/CLI/json-properties.desc b/regression/ebmc/CLI/json-properties.desc index efb427813..f40219c5d 100644 --- a/regression/ebmc/CLI/json-properties.desc +++ b/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", diff --git a/src/ebmc/ebmc_properties.cpp b/src/ebmc/ebmc_properties.cpp index 0025e38c9..7ca8ef77c 100644 --- a/src/ebmc/ebmc_properties.cpp +++ b/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; diff --git a/src/ebmc/ebmc_properties.h b/src/ebmc/ebmc_properties.h index 938517144..86ee4fb4e 100644 --- a/src/ebmc/ebmc_properties.h +++ b/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; diff --git a/src/ebmc/liveness_to_safety.cpp b/src/ebmc/liveness_to_safety.cpp index fb945dff0..22239b356 100644 --- a/src/ebmc/liveness_to_safety.cpp +++ b/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; } } } diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp index 2db60497f..07c989e7b 100644 --- a/src/ebmc/report_results.cpp +++ b/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; diff --git a/src/ebmc/show_properties.cpp b/src/ebmc/show_properties.cpp index 292024ca0..58b9b7692 100644 --- a/src/ebmc/show_properties.cpp +++ b/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(message.get_message_handler()).get_ui()) { + switch(static_cast(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++; } } diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index fa7da4ead..e1fbfb396 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/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; diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 5d5bf026d..157905d50 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/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); }