diff --git a/jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc b/jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc index 683e08b45cf..4a862844e86 100644 --- a/jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc +++ b/jbmc/regression/jbmc/classpath-invalid/test_jar_warning.desc @@ -3,7 +3,7 @@ Test --classpath ./NotHere.jar ^EXIT=6$ ^SIGNAL=0$ -Warning: failed to access JAR file `./NotHere.jar' +Warning: failed to access JAR file './NotHere.jar' Error: Could not find or load main class Test -- -- diff --git a/jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc b/jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc index 1a9a4040b8a..59bce83911f 100644 --- a/jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc +++ b/jbmc/regression/jbmc/classpath-invalid/test_path_warning.desc @@ -3,7 +3,7 @@ Test --classpath `../../../../scripts/format_classpath.sh ./NotHere target/classes` ^EXIT=0$ ^SIGNAL=0$ -Warning: failed to access directory `./NotHere' +Warning: failed to access directory './NotHere' -- -- Note: 'java' does not emit such a warning. diff --git a/jbmc/regression/jbmc/lambda1/test_goto_functions.desc b/jbmc/regression/jbmc/lambda1/test_goto_functions.desc index 0f05e4ea2e1..89ee8d3d221 100644 --- a/jbmc/regression/jbmc/lambda1/test_goto_functions.desc +++ b/jbmc/regression/jbmc/lambda1/test_goto_functions.desc @@ -1,14 +1,14 @@ CORE Lambdatest --verbosity 10 --show-goto-functions --function Lambdatest.main -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` -lambda function reference lambda\$new\$0 in class \"Lambdatest\" -lambda function reference lambda\$new\$1 in class \"Lambdatest\" -lambda function reference lambda\$captureReference\$2 in class \"Lambdatest\" -lambda function reference lambda\$captureInt\$3 in class \"Lambdatest\" -lambda function reference lambda\$captureThisPrimitive\$4 in class \"Lambdatest\" -lambda function reference lambda\$captureThisReference\$5 in class \"Lambdatest\" -lambda function reference lambda\$captureAndCall\$6 in class \"Lambdatest\" -lambda function reference lambda\$captureAndAssign\$7 in class \"Lambdatest\" -lambda function reference lambda\$static\$0 in class \"B\" +lambda function reference lambda\$new\$0 in class 'Lambdatest' +lambda function reference lambda\$new\$1 in class 'Lambdatest' +lambda function reference lambda\$captureReference\$2 in class 'Lambdatest' +lambda function reference lambda\$captureInt\$3 in class 'Lambdatest' +lambda function reference lambda\$captureThisPrimitive\$4 in class 'Lambdatest' +lambda function reference lambda\$captureThisReference\$5 in class 'Lambdatest' +lambda function reference lambda\$captureAndCall\$6 in class 'Lambdatest' +lambda function reference lambda\$captureAndAssign\$7 in class 'Lambdatest' +lambda function reference lambda\$static\$0 in class 'B' ^EXIT=0$ ^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda2/test.desc b/jbmc/regression/jbmc/lambda2/test.desc index 43b63c8a77b..b405658cd9f 100644 --- a/jbmc/regression/jbmc/lambda2/test.desc +++ b/jbmc/regression/jbmc/lambda2/test.desc @@ -1,7 +1,7 @@ CORE symex-driven-lazy-loading-expected-failure org.symphonyoss.symphony.clients.model.SymStream --show-goto-functions --verbosity 10 -cp `../../../../scripts/format_classpath.sh . target/classes` -lambda function reference toSymUser in class "org\.symphonyoss\.symphony\.clients\.model\.SymStream" +lambda function reference toSymUser in class 'org\.symphonyoss\.symphony\.clients\.model\.SymStream' ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 28f8439c48f..cc55bc738ea 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -2101,13 +2101,11 @@ void java_bytecode_parsert::read_bootstrapmethods_entry() log.debug() << "lambda function reference " - << id2string( - lambda_method_handle->get_method_descriptor().base_method_name()) - << " in class \"" << parse_tree.parsed_class.name << "\"" - << "\n interface type is " - << id2string(pool_entry(interface_type_argument.ref1).s) - << "\n method type is " - << id2string(pool_entry(method_type_argument.ref1).s) << messaget::eom; + << lambda_method_handle->get_method_descriptor().base_method_name() + << " in class " << messaget::quote_begin << parse_tree.parsed_class.name + << messaget::quote_end << "\n interface type is " + << pool_entry(interface_type_argument.ref1).s << "\n method type is " + << pool_entry(method_type_argument.ref1).s << messaget::eom; parse_tree.parsed_class.add_method_handle( bootstrap_method_index, *lambda_method_handle); } diff --git a/jbmc/src/java_bytecode/java_class_loader_base.cpp b/jbmc/src/java_bytecode/java_class_loader_base.cpp index 57a8a31d37b..24efaaf881c 100644 --- a/jbmc/src/java_bytecode/java_class_loader_base.cpp +++ b/jbmc/src/java_bytecode/java_class_loader_base.cpp @@ -34,7 +34,8 @@ void java_class_loader_baset::add_classpath_entry( } else { - log.warning() << "Warning: failed to access JAR file `" << path << "'" + log.warning() << "Warning: failed to access JAR file " + << messaget::quote_begin << path << messaget::quote_end << messaget::eom; } } @@ -47,7 +48,8 @@ void java_class_loader_baset::add_classpath_entry( } else { - log.warning() << "Warning: failed to access directory `" << path << "'" + log.warning() << "Warning: failed to access directory " + << messaget::quote_begin << path << messaget::quote_end << messaget::eom; } } diff --git a/regression/goto-cc-file-local/old-flag-name/test.desc b/regression/goto-cc-file-local/old-flag-name/test.desc index fa6f0e20b17..4fa9efb29f7 100644 --- a/regression/goto-cc-file-local/old-flag-name/test.desc +++ b/regression/goto-cc-file-local/old-flag-name/test.desc @@ -4,7 +4,7 @@ final-link assertion-check old-flag ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -^The `--export-function-local-symbols` flag is deprecated. Please use `--export-file-local-symbols` instead.$ +^The '--export-function-local-symbols' flag is deprecated. Please use '--export-file-local-symbols' instead.$ -- ^warning: ignoring ^\*\*\*\* WARNING: no body for function diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index eaa4d5b25fe..41c7d532690 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -77,8 +77,9 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) // versions of Visual Studio insist to use this in their C library, and // GCC just warns as well. warning().source_location = symbol.value.find_source_location(); - warning() << "'extern' symbol '" << new_name - << "' should not have an initializer" << eom; + warning() << quote_begin << "extern" << quote_end << " symbol " + << quote_begin << new_name << quote_end + << " should not have an initializer" << eom; } } else if(!is_function && symbol.value.id()==ID_code) diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 3954d80f21d..1736855a704 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -558,7 +558,8 @@ void c_typecheck_baset::typecheck_switch_case(code_switch_caset &code) if(!case_is_allowed) { error().source_location = code.source_location(); - error() << "did not expect `case' here" << eom; + error() << "did not expect " << quote_begin << "case" << quote_end + << " here" << eom; throw 0; } @@ -575,7 +576,8 @@ void c_typecheck_baset::typecheck_gcc_switch_case_range( if(!case_is_allowed) { error().source_location = code.source_location(); - error() << "did not expect `case' here" << eom; + error() << "did not expect " << quote_begin << "case" << quote_end + << " here" << eom; throw 0; } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index d11cb25f32c..afc0f3ca884 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -812,8 +812,8 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr) if(s_it == symbol_table.symbols.end()) { error().source_location = expr.source_location(); - error() << "failed to find bound symbol `" << identifier - << "' in symbol table" << eom; + error() << "failed to find bound symbol " << quote_begin << identifier + << quote_end << " in symbol table" << eom; throw 0; } diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index 71821c14941..6974e6cf25e 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -486,8 +486,8 @@ const symbolt &cpp_typecheckt::instantiate_template( if(new_decl.member_spec().is_virtual()) { error().source_location=new_decl.source_location(); - error() << "invalid use of `virtual' in template declaration" - << eom; + error() << "invalid use of " << quote_begin << "virtual" << quote_end + << " in template declaration" << eom; throw 0; } diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index b162bb60889..1201882af20 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -981,7 +981,8 @@ void cpp_typecheckt::typecheck_expr_this(exprt &expr) if(cpp_scopes.current_scope().class_identifier.empty()) { error().source_location=expr.find_source_location(); - error() << "`this' is not allowed here" << eom; + error() << quote_begin << "this" << quote_end << " is not allowed here" + << eom; throw 0; } diff --git a/src/cpp/cpp_typecheck_function.cpp b/src/cpp/cpp_typecheck_function.cpp index e7968615198..154b037dae4 100644 --- a/src/cpp/cpp_typecheck_function.cpp +++ b/src/cpp/cpp_typecheck_function.cpp @@ -56,8 +56,8 @@ void cpp_typecheckt::convert_parameter( if(symbol_table.move(symbol, new_symbol)) { error().source_location=symbol.location; - error() << "cpp_typecheckt::convert_parameter: symbol_table.move(\"" - << symbol.name << "\") failed" << eom; + error() << "cpp_typecheckt::convert_parameter: symbol_table.move(" + << quote_begin << symbol.name << quote_end << ") failed" << eom; throw 0; } diff --git a/src/goto-analyzer/taint_parser.cpp b/src/goto-analyzer/taint_parser.cpp index 8ced332a632..6479c6619ca 100644 --- a/src/goto-analyzer/taint_parser.cpp +++ b/src/goto-analyzer/taint_parser.cpp @@ -64,9 +64,13 @@ bool taint_parser( else { messaget message(message_handler); - message.error() << "taint rule must have \"kind\" which is " - "\"source\" or \"sink\" or \"sanitizer\"" - << messaget::eom; + message.error() << "taint rule must have " << messaget::quote_begin + << "kind" << messaget::quote_end << " which is " + << messaget::quote_begin << "source" + << messaget::quote_end << " or " << messaget::quote_begin + << "sink" << messaget::quote_end << " or " + << messaget::quote_begin << "sanitizer" + << messaget::quote_end << messaget::eom; return true; } @@ -75,8 +79,8 @@ bool taint_parser( if(function.empty()) { messaget message(message_handler); - message.error() << "taint rule must have \"function\"" - << messaget::eom; + message.error() << "taint rule must have " << messaget::quote_begin + << "function" << messaget::quote_end << messaget::eom; return true; } else @@ -101,10 +105,13 @@ bool taint_parser( else { messaget message(message_handler); - message.error() << "taint rule must have \"where\"" - << " which is \"return_value\" or \"this\" " - << "or \"parameter1\"..." - << messaget::eom; + message.error() << "taint rule must have " << messaget::quote_begin + << "where" << messaget::quote_end << " which is " + << messaget::quote_begin << "return_value" + << messaget::quote_end << " or " << messaget::quote_begin + << "this" << messaget::quote_end << " or " + << messaget::quote_begin << "parameter1" + << messaget::quote_end << "..." << messaget::eom; return true; } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 3631189d812..0a49ec521ab 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -662,10 +662,12 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror) if(cmdline.isset("export-function-local-symbols")) { - log.warning() - << "The `--export-function-local-symbols` flag is deprecated. " - "Please use `--export-file-local-symbols` instead." - << messaget::eom; + log.warning() << "The " << messaget::quote_begin + << "--export-function-local-symbols" << messaget::quote_end + << " flag is deprecated. " + "Please use " + << messaget::quote_begin << "--export-file-local-symbols" + << messaget::quote_end << " instead." << messaget::eom; } } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 58629491f1e..6bde1eb04cd 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -677,12 +677,16 @@ void linkingt::duplicate_object_symbol( log.warning().source_location = new_symbol.location; log.warning() << "conflicting initializers for" - << " variable '" << old_symbol.name << "'\n"; - log.warning() << "using old value in module " << old_symbol.module - << " " << old_symbol.value.find_source_location() << '\n' + << " variable " << messaget::quote_begin + << old_symbol.name << messaget::quote_end << '\n'; + log.warning() << "using old value in module " << messaget::quote_begin + << old_symbol.module << messaget::quote_end << " " + << old_symbol.value.find_source_location() << '\n' << from_expr(ns, old_symbol.name, tmp_old) << '\n'; - log.warning() << "ignoring new value in module " << new_symbol.module - << " " << new_symbol.value.find_source_location() << '\n' + log.warning() << "ignoring new value in module " + << messaget::quote_begin << new_symbol.module + << messaget::quote_end << " " + << new_symbol.value.find_source_location() << '\n' << from_expr(ns, new_symbol.name, tmp_new) << messaget::eom; } diff --git a/src/linking/linking_diagnostics.cpp b/src/linking/linking_diagnostics.cpp index 626c2e3324c..0ba3a68577f 100644 --- a/src/linking/linking_diagnostics.cpp +++ b/src/linking/linking_diagnostics.cpp @@ -370,11 +370,14 @@ void linking_diagnosticst::error( messaget log{message_handler}; log.error().source_location = new_symbol.location; - log.error() << msg << " '" << old_symbol.display_name() << "'" << '\n'; - log.error() << "old definition in module '" << old_symbol.module << "' " + log.error() << msg << ' ' << messaget::quote_begin + << old_symbol.display_name() << messaget::quote_end << '\n'; + log.error() << "old definition in module " << messaget::quote_begin + << old_symbol.module << messaget::quote_end << ' ' << old_symbol.location << '\n' << type_to_string_verbose(old_symbol) << '\n'; - log.error() << "new definition in module '" << new_symbol.module << "' " + log.error() << "new definition in module " << messaget::quote_begin + << new_symbol.module << messaget::quote_end << ' ' << new_symbol.location << '\n' << type_to_string_verbose(new_symbol) << messaget::eom; } @@ -387,11 +390,14 @@ void linking_diagnosticst::warning( messaget log{message_handler}; log.warning().source_location = new_symbol.location; - log.warning() << msg << " '" << old_symbol.display_name() << "'\n"; - log.warning() << "old definition in module " << old_symbol.module << " " + log.warning() << msg << ' ' << messaget::quote_begin + << old_symbol.display_name() << messaget::quote_end << '\n'; + log.warning() << "old definition in module " << messaget::quote_begin + << old_symbol.module << messaget::quote_end << ' ' << old_symbol.location << '\n' << type_to_string_verbose(old_symbol) << '\n'; - log.warning() << "new definition in module " << new_symbol.module << " " + log.warning() << "new definition in module " << messaget::quote_begin + << new_symbol.module << messaget::quote_end << ' ' << new_symbol.location << '\n' << type_to_string_verbose(new_symbol) << messaget::eom; } diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index cf69f40f523..cbe6ecb8ebc 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -210,7 +210,8 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) const auto &message = id2string(parsed.get_sub()[1].id()); messaget log{message_handler}; log.error() << "SMT2 solver returned error message:\n" - << "\t\"" << message << "\"" << messaget::eom; + << "\t" << messaget::quote_begin << message + << messaget::quote_end << messaget::eom; return decision_proceduret::resultt::D_ERROR; } } diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 7af950d095a..573d1e43ee4 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -1107,8 +1107,9 @@ static exprt get_char_array_and_concretize( const auto array_expr = expr_try_dynamic_cast(*concretized_array)) { - stream << std::string(4, ' ') << "- as_string: \"" - << string_of_array(*array_expr) << "\"\n"; + stream << std::string(4, ' ') + << "- as_string: " << messaget::quote_begin + << string_of_array(*array_expr) << messaget::quote_end << '\n'; } else stream << std::string(2, ' ') << "- warning: not an array" diff --git a/src/statement-list/statement_list_entry_point.cpp b/src/statement-list/statement_list_entry_point.cpp index 7bb7b1b1cef..97a2323297a 100644 --- a/src/statement-list/statement_list_entry_point.cpp +++ b/src/statement-list/statement_list_entry_point.cpp @@ -52,8 +52,9 @@ static bool is_main_symbol_invalid( if(found) { messaget message(message_handler); - message.error() << "main symbol `" << main_symbol_name - << "' is ambiguous" << messaget::eom; + message.error() << "main symbol " << messaget::quote_begin + << main_symbol_name << messaget::quote_end + << " is ambiguous" << messaget::eom; return true; } else @@ -66,7 +67,8 @@ static bool is_main_symbol_invalid( else { messaget message(message_handler); - message.error() << "main symbol `" << main_symbol_name << "' not found" + message.error() << "main symbol " << messaget::quote_begin + << main_symbol_name << messaget::quote_end << " not found" << messaget::eom; return true; } @@ -225,8 +227,9 @@ bool statement_list_entry_point( if(main.value.is_nil()) { messaget message(message_handler); - message.error() << "main symbol `" << id2string(main_symbol_name) - << "' has no body" << messaget::eom; + message.error() << "main symbol " << messaget::quote_begin + << main_symbol_name << messaget::quote_end << " has no body" + << messaget::eom; return true; } diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index 641c5c35c93..1498704ee63 100644 --- a/src/util/cout_message.cpp +++ b/src/util/cout_message.cpp @@ -70,6 +70,14 @@ console_message_handlert::console_message_handlert(bool _always_flush) /// \param c: ECMA-48 command code std::string console_message_handlert::command(unsigned c) const { + // messaget::quote_begin and messaget::quote_end render as a single + // quote on every UI; we agree with ui_message_handlert here on what + // '<' / '>' mean. If quote_begin / quote_end are ever re-encoded to + // values outside the SGR range (see comment in message.cpp), this + // arm needs to be updated in lock-step. + if(c == '<' || c == '>') + return "'"; + if(!use_SGR) return std::string(); diff --git a/src/util/message.cpp b/src/util/message.cpp index 38ab1cfd26d..8d4ffee8c10 100644 --- a/src/util/message.cpp +++ b/src/util/message.cpp @@ -95,6 +95,16 @@ const messaget::commandt messaget::bright_yellow(93); const messaget::commandt messaget::bright_blue(94); const messaget::commandt messaget::bright_magenta(95); const messaget::commandt messaget::bright_cyan(96); +// quote_begin and quote_end use the ASCII codes for '<' (60) and '>' +// (62), which happen to fall inside ECMA-48's SGR ideogram-styling +// parameter range (60..65). The overload is safe today because nothing +// uses ideogram modes via this same mechanism, but if a future styling +// command is added with a code in 60..65 there will be a clash with no +// compile-time signal. Either re-encode quote_begin/quote_end to a +// value above the SGR range (e.g. >= 256) or pick non-overlapping +// codes for any new ideogram styles. +const messaget::commandt messaget::quote_begin('<'); +const messaget::commandt messaget::quote_end('>'); /// Parse a (user-)provided string as a verbosity level and set it as the /// verbosity of dest. diff --git a/src/util/message.h b/src/util/message.h index ec1624855e8..9e0673239d4 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -382,6 +382,16 @@ class messaget /// render underlined text static const commandt underline; + /// Start quoted text. Renders as a single `'` on the PLAIN, XML and + /// JSON UIs, and as `'` on the console handler. The structured UIs + /// deliberately do not emit "" / "" tags; see the + /// comment in `ui_message_handlert::command()` for the rationale. + static const commandt quote_begin; + + /// End quoted text. Counterpart to \ref quote_begin; same per-UI + /// rendering. + static const commandt quote_end; + mstreamt &get_mstream(unsigned message_level) const { mstream.message_level=message_level; diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index 69302626dc7..87d4dc4626c 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -117,6 +117,60 @@ ui_message_handlert::~ui_message_handlert() } } +std::string ui_message_handlert::command(unsigned c) const +{ + // quote_begin / quote_end render as a single quote on every currently + // supported UI. Handled before the message_handler null-check so this + // also applies when the handler is constructed via the cmdlinet ctor, + // which leaves message_handler null for XML_UI / JSON_UI. We + // considered emitting `` / `` tags for XML output (see + // PR #5696 discussion) but kept single quotes for backwards + // compatibility; messages reach the XML serialiser through xmlt::data + // and would be escaped, so any tag-based quoting would have to bypass + // the message-text plumbing entirely. + if(c == '<' || c == '>') + return "'"; + + if(!message_handler) + return std::string(); + + // SGR (Select Graphic Rendition) style codes carry no useful + // information for machine-consumable output, so the structured UIs + // strip them entirely. Centralised here so future additions or + // removals of formatting commands only need to be made in one place. + if((_ui == uit::XML_UI || _ui == uit::JSON_UI) && is_sgr_style_command(c)) + return std::string(); + + return message_handler->command(c); +} + +bool ui_message_handlert::is_sgr_style_command(unsigned c) +{ + switch(c) + { + case 0: // reset + case 1: // bold + case 2: // faint + case 3: // italic + case 4: // underline + case 31: // red + case 32: // green + case 33: // yellow + case 34: // blue + case 35: // magenta + case 36: // cyan + case 91: // bright_red + case 92: // bright_green + case 93: // bright_yellow + case 94: // bright_blue + case 95: // bright_magenta + case 96: // bright_cyan + return true; + default: + return false; + } +} + const char *ui_message_handlert::level_string(unsigned level) { if(level==1) diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 8d92e33b816..b58126133a2 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -94,13 +94,17 @@ class ui_message_handlert : public message_handlert const char *level_string(unsigned level); - std::string command(unsigned c) const override - { - if(message_handler) - return message_handler->command(c); - else - return std::string(); - } + std::string command(unsigned c) const override; + +public: + /// Returns true iff \p c is a Select Graphic Rendition (SGR) parameter + /// value used by messaget for terminal styling -- 0..4 (reset/bold/ + /// faint/italic/underline) and 31..36 / 91..96 (foreground colours and + /// their bright variants). The values listed here are kept in lock-step + /// with the corresponding `messaget::commandt` constants in message.h / + /// message.cpp; if a new styling command is added there, it should be + /// added here too so it is suppressed on the structured UIs. + static bool is_sgr_style_command(unsigned c); }; #define OPT_FLUSH "(flush)" diff --git a/unit/Makefile b/unit/Makefile index fa46a11d30c..d7ae52d8682 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -185,6 +185,7 @@ SRC += analyses/ai/ai.cpp \ util/mathematical_types.cpp \ util/memory_info.cpp \ util/message.cpp \ + util/ui_message.cpp \ util/optional_utils.cpp \ util/output_file.cpp \ util/parse_options.cpp \ diff --git a/unit/util/ui_message.cpp b/unit/util/ui_message.cpp new file mode 100644 index 00000000000..f95f751ff4d --- /dev/null +++ b/unit/util/ui_message.cpp @@ -0,0 +1,139 @@ +/*******************************************************************\ + +Module: ui_message_handlert tests + +Author: Michael Tautschnig + +\*******************************************************************/ + +#include +#include +#include + +#include + +#include +#include +#include + +/// Construct a ui_message_handlert via the cmdlinet ctor (the usual +/// path for every CBMC tool). For XML_UI / JSON_UI the cmdlinet ctor +/// leaves the underlying message_handler null; this is the +/// configuration that exercises the regression fixed in this PR. The +/// XML/JSON ctors write a header to std::cout, so we redirect cout to +/// a throw-away stream around the call. +static std::unique_ptr +make_handler(ui_message_handlert::uit ui) +{ + cmdlinet cmdline; + // Register the options before we can set them; the cmdlinet ctor + // for ui_message_handlert dispatches on isset("xml-ui") / + // isset("json-ui"). + const char *argv0[] = {"unit-test"}; + cmdline.parse(1, argv0, "(xml-ui)(json-ui)"); + switch(ui) + { + case ui_message_handlert::uit::PLAIN: + break; + case ui_message_handlert::uit::XML_UI: + cmdline.set("xml-ui"); + break; + case ui_message_handlert::uit::JSON_UI: + cmdline.set("json-ui"); + break; + } + + std::ostringstream sink; + std::streambuf *const saved = std::cout.rdbuf(sink.rdbuf()); + auto handler = std::make_unique(cmdline, "test"); + std::cout.rdbuf(saved); + return handler; +} + +/// quote_begin and quote_end are encoded as the ASCII codes for '<' +/// (60) and '>' (62) respectively. ui_message_handlert::command must +/// render both as a single quote on every UI; in particular the XML +/// and JSON variants -- where the underlying message_handler is null +/// when constructed via the cmdlinet ctor -- must also do so +/// (regression: prior to PR #5696's reorder the structured UIs +/// silently dropped these characters). +TEST_CASE( + "ui_message_handlert renders quote_begin/quote_end as ' (PLAIN)", + "[core][util][ui_message]") +{ + auto handler = make_handler(ui_message_handlert::uit::PLAIN); + // command() is protected on ui_message_handlert; call through the + // message_handlert public interface. + const message_handlert &mh = *handler; + CHECK(mh.command('<') == "'"); + CHECK(mh.command('>') == "'"); +} + +TEST_CASE( + "ui_message_handlert renders quote_begin/quote_end as ' (XML)", + "[core][util][ui_message]") +{ + auto handler = make_handler(ui_message_handlert::uit::XML_UI); + const message_handlert &mh = *handler; + CHECK(mh.command('<') == "'"); + CHECK(mh.command('>') == "'"); +} + +TEST_CASE( + "ui_message_handlert renders quote_begin/quote_end as ' (JSON)", + "[core][util][ui_message]") +{ + auto handler = make_handler(ui_message_handlert::uit::JSON_UI); + const message_handlert &mh = *handler; + CHECK(mh.command('<') == "'"); + CHECK(mh.command('>') == "'"); +} + +/// is_sgr_style_command must return true for every messaget styling +/// command and false for the quote commands and arbitrary other codes. +/// The point of the helper is to be the single source of truth for +/// "which commands are SGR-style"; this test pins the helper's output +/// against the messaget::commandt constants so that adding or +/// removing a styling command in messaget without updating the helper +/// (or vice versa) is caught at unit-test time. +TEST_CASE( + "ui_message_handlert::is_sgr_style_command matches messaget styling codes", + "[core][util][ui_message]") +{ + // Every styling command on messaget should be classified as SGR. + for(const auto &cmd : + {messaget::reset, + messaget::bold, + messaget::faint, + messaget::italic, + messaget::underline, + messaget::red, + messaget::green, + messaget::yellow, + messaget::blue, + messaget::magenta, + messaget::cyan, + messaget::bright_red, + messaget::bright_green, + messaget::bright_yellow, + messaget::bright_blue, + messaget::bright_magenta, + messaget::bright_cyan}) + { + CHECK(ui_message_handlert::is_sgr_style_command(cmd.command)); + } + + // quote_begin / quote_end are commands but NOT SGR-style. + CHECK_FALSE( + ui_message_handlert::is_sgr_style_command(messaget::quote_begin.command)); + CHECK_FALSE( + ui_message_handlert::is_sgr_style_command(messaget::quote_end.command)); + + // Arbitrary non-styling codes outside the SGR ranges should be rejected. + CHECK_FALSE(ui_message_handlert::is_sgr_style_command(5)); + CHECK_FALSE(ui_message_handlert::is_sgr_style_command(30)); + CHECK_FALSE(ui_message_handlert::is_sgr_style_command(37)); + CHECK_FALSE(ui_message_handlert::is_sgr_style_command(90)); + CHECK_FALSE(ui_message_handlert::is_sgr_style_command(97)); + CHECK_FALSE(ui_message_handlert::is_sgr_style_command(256)); +}