From 2aeb4c7d0812479b47a6a1483f2b4d72ca22d326 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 01/19] murphi2c: print nicer colourised error messages MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #338 “location information in parsing rejections” --- misc/_murphi2c | 1 + murphi2c/doc/murphi2c.1 | 6 +++ murphi2c/src/main.cc | 103 +++++++++++++++++++++++++++++++++++++++- 3 files changed, 108 insertions(+), 2 deletions(-) diff --git a/misc/_murphi2c b/misc/_murphi2c index ae3d32a3..c1c9517b 100644 --- a/misc/_murphi2c +++ b/misc/_murphi2c @@ -3,6 +3,7 @@ # Zsh completion script for Murphi2C _arguments \ + '--colour[enable or disable ANSI colour codes]: :(auto off on)' \ '--header[generate a C header]' \ '--help[display help information]' \ {--output,-o}'[path to write source/header to]:filename:_files' \ diff --git a/murphi2c/doc/murphi2c.1 b/murphi2c/doc/murphi2c.1 index 8d1a081b..b713b94c 100644 --- a/murphi2c/doc/murphi2c.1 +++ b/murphi2c/doc/murphi2c.1 @@ -23,6 +23,12 @@ See .BR rumur(1) for more information about Rumur or Murphi. .SH OPTIONS +\fB\-\-colour\fR [\fBauto\fR | \fBoff\fR | \fBon\fR] +.RS +Enable or disable the use of ANSI colour codes in error messages. The default is +\fBauto\fR, to auto-detect based on whether the stderr is a TTY. +.RE +.PP \fB\-\-header\fR .RS Generate a C header, as opposed to a source file. diff --git a/murphi2c/src/main.cc b/murphi2c/src/main.cc index cdea1b7c..d8d46d83 100644 --- a/murphi2c/src/main.cc +++ b/murphi2c/src/main.cc @@ -7,7 +7,9 @@ #include "resources.h" #include #include +#include #include +#include #include #include #include @@ -31,11 +33,16 @@ static std::shared_ptr out; // output C source? (as opposed to C header) static bool source = true; +/// use colour in error messages? +static enum { AUTO, ON, OFF } color = AUTO; + static void parse_args(int argc, char **argv) { for (;;) { static struct option options[] = { // clang-format off + { "color", required_argument, 0, 132 }, + { "colour", required_argument, 0, 132 }, { "header", no_argument, 0, 128 }, { "help", no_argument, 0, 'h' }, { "output", required_argument, 0, 'o' }, @@ -89,6 +96,20 @@ static void parse_args(int argc, char **argv) { std::cout << "Murphi2C version " << rumur_get_version() << '\n'; exit(EXIT_SUCCESS); + case 132: // --color, --colour + if (strcmp(optarg, "auto") == 0) { + color = AUTO; + } else if (strcmp(optarg, "on") == 0) { + color = ON; + } else if (strcmp(optarg, "off") == 0) { + color = OFF; + } else { + std::cerr << "invalid --colour argument \"" << optarg << "\"\n" + << "valid arguments are \"auto\", \"off\", and \"on\"\n"; + exit(EXIT_FAILURE); + } + break; + default: std::cerr << "unexpected error\n"; exit(EXIT_FAILURE); @@ -133,6 +154,78 @@ static dup_t make_stdin_dup() { return dup_t(buffer, copy); } +static bool use_colors() { + if (color == AUTO) + color = isatty(STDERR_FILENO) ? ON : OFF; + return color == ON; +} + +static const char *bold() { + if (use_colors()) + return "\033[1m"; + return ""; +} + +static const char *green() { + if (use_colors()) + return "\033[32m"; + return ""; +} + +static const char *red() { + if (use_colors()) + return "\033[31m"; + return ""; +} + +static const char *reset() { + if (use_colors()) + return "\033[0m"; + return ""; +} + +static const char *white() { + if (use_colors()) + return "\033[37m"; + return ""; +} + +static void print_location(std::istream &src, const rumur::location &location) { + + // the type of position.line and position.column changes across Bison + // releases, so avoid some -Wsign-compare warnings by casting them in advance + auto loc_line = static_cast(location.begin.line); + auto loc_col = static_cast(location.begin.column); + + std::string line; + unsigned long lineno = 0; + while (lineno < loc_line) { + if (!std::getline(src, line)) + return; + lineno++; + } + + // print the line, and construct an underline indicating the column location + std::ostringstream buf; + unsigned long col = 1; + for (const char &c : line) { + if (col == loc_col) { + buf << green() << bold() << '^' << reset(); + } else if (col < loc_col) { + if (c == '\t') { + buf << '\t'; + } else { + buf << ' '; + } + } + std::cerr << c; + col++; + } + std::cerr << '\n'; + + std::cerr << buf.str() << '\n'; +} + int main(int argc, char **argv) { // parse command line options @@ -148,7 +241,10 @@ int main(int argc, char **argv) { try { m = rumur::parse_model(*in.first); } catch (rumur::Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + print_location(*in.second, e.loc); return EXIT_FAILURE; } @@ -162,7 +258,10 @@ int main(int argc, char **argv) { resolve_symbols(*m); validate(*m); } catch (rumur::Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + print_location(*in.second, e.loc); return EXIT_FAILURE; } From 18b99fe9408f1985a09a025d54571a80c65d55c2 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 02/19] murphi2c: nicer colourised error messages for unsupported features too MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #338 “location information in parsing rejections” --- murphi2c/src/check.cc | 68 ++++++++++++------------------------------- murphi2c/src/check.h | 7 +++-- murphi2c/src/main.cc | 9 +++++- 3 files changed, 31 insertions(+), 53 deletions(-) diff --git a/murphi2c/src/check.cc b/murphi2c/src/check.cc index f7231a86..e7e68080 100644 --- a/murphi2c/src/check.cc +++ b/murphi2c/src/check.cc @@ -11,76 +11,46 @@ namespace { class Check : public ConstTraversal { public: - bool ok = true; - - void visit_choose(const Choose &) final { - if (ok) { - std::cerr << "choose rules are not supported\n"; - ok = false; - } + void visit_choose(const Choose &n) final { + throw Error("choose rules are not supported", n.loc); } - void visit_ismember(const IsMember &) final { - if (ok) { - std::cerr << "ismember expressions are not supported\n"; - ok = false; - } + void visit_ismember(const IsMember &n) final { + throw Error("ismember expressions are not supported", n.loc); } - void visit_isundefined(const IsUndefined &) final { - if (ok) { - std::cerr << "isundefined expressions are not supported\n"; - ok = false; - } + void visit_isundefined(const IsUndefined &n) final { + throw Error("isundefined expressions are not supported", n.loc); } - void visit_multiset(const Multiset &) final { - if (ok) { - std::cerr << "multiset types are not supported\n"; - ok = false; - } + void visit_multiset(const Multiset &n) final { + throw Error("multiset types are not supported", n.loc); } - void visit_multisetadd(const MultisetAdd &) final { - if (ok) { - std::cerr << "multiset types are not supported\n"; - ok = false; - } + void visit_multisetadd(const MultisetAdd &n) final { + throw Error("multiset types are not supported", n.loc); } - void visit_multisetcount(const MultisetCount &) final { - if (ok) { - std::cerr << "multiset types are not supported\n"; - ok = false; - } + void visit_multisetcount(const MultisetCount &n) final { + throw Error("multiset types are not supported", n.loc); } - void visit_multisetremove(const MultisetRemove &) final { - if (ok) { - std::cerr << "multiset types are not supported\n"; - ok = false; - } + void visit_multisetremove(const MultisetRemove &n) final { + throw Error("multiset types are not supported", n.loc); } - void visit_multisetremovepred(const MultisetRemovePred &) final { - if (ok) { - std::cerr << "multiset types are not supported\n"; - ok = false; - } + void visit_multisetremovepred(const MultisetRemovePred &n) final { + throw Error("multiset types are not supported", n.loc); } - void visit_union(const Union &) final { - if (ok) { - std::cerr << "union types are not supported\n"; - ok = false; - } + void visit_union(const Union &n) final { + throw Error("union types are not supported", n.loc); } }; } // namespace -bool check(const Node &n) { +void check(const Node &n) { Check c; c.dispatch(n); - return c.ok; } diff --git a/murphi2c/src/check.h b/murphi2c/src/check.h index 069c69a7..41a6cb31 100644 --- a/murphi2c/src/check.h +++ b/murphi2c/src/check.h @@ -2,6 +2,7 @@ #include -// validate the given AST contains no idioms that cannot be handled by murphi2c, -// and return false if any are found -bool check(const rumur::Node &n); +/// validate the given AST contains no idioms that cannot be handled by murphi2c +/// +/// Throws `rumur::Error` if anything is found that cannot be handled. +void check(const rumur::Node &n); diff --git a/murphi2c/src/main.cc b/murphi2c/src/main.cc index d8d46d83..7ea84ca4 100644 --- a/murphi2c/src/main.cc +++ b/murphi2c/src/main.cc @@ -266,8 +266,15 @@ int main(int argc, char **argv) { } // validate that this model is OK to translate - if (!check(*m)) + try { + check(*m); + } catch (rumur::Error &e) { + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + print_location(*in.second, e.loc); return EXIT_FAILURE; + } // name any rules that are unnamed, so they get valid C symbols rumur::sanitise_rule_names(*m); From 5ac576e240f9afb14f53c2240fc3f35eefacea03 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 03/19] murphi2murphi: print nicer colourised error messages MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #338 “location information in parsing rejections” --- misc/_murphi2murphi | 1 + murphi2murphi/doc/murphi2murphi.1 | 6 ++ murphi2murphi/src/main.cc | 114 +++++++++++++++++++++++++++++- 3 files changed, 118 insertions(+), 3 deletions(-) diff --git a/misc/_murphi2murphi b/misc/_murphi2murphi index 262941f7..f297176e 100644 --- a/misc/_murphi2murphi +++ b/misc/_murphi2murphi @@ -3,6 +3,7 @@ # Zsh completion script for Murphi2Murphi _arguments \ + '--colour[enable or disable ANSI colour codes]: :(auto off on)' \ '--decompose-complex-comparisons[expand array and record equality tests]' \ '--explicit-semicolons[add omitted semicolons]' \ '--help[display help information]' \ diff --git a/murphi2murphi/doc/murphi2murphi.1 b/murphi2murphi/doc/murphi2murphi.1 index 20c4732f..80190d00 100644 --- a/murphi2murphi/doc/murphi2murphi.1 +++ b/murphi2murphi/doc/murphi2murphi.1 @@ -23,6 +23,12 @@ See .BR rumur(1) for more information about Rumur or Murphi. .SH OPTIONS +\fB\-\-colour\fR [\fBauto\fR | \fBoff\fR | \fBon\fR] +.RS +Enable or disable the use of ANSI colour codes in error messages. The default is +\fBauto\fR, to auto-detect based on whether the stderr is a TTY. +.RE +.PP \fB\-\-decompose\-complex\-comparisons\fR .RS Rumur supports comparing values of complex type (records and arrays) with each diff --git a/murphi2murphi/src/main.cc b/murphi2murphi/src/main.cc index 580bcc5e..fd05b57d 100644 --- a/murphi2murphi/src/main.cc +++ b/murphi2murphi/src/main.cc @@ -11,6 +11,7 @@ #include "resources.h" #include #include +#include #include #include #include @@ -20,13 +21,18 @@ #include #include #include +#include using namespace rumur; +static const char *in_filename = ""; static std::shared_ptr in; static std::shared_ptr in_replay; static std::shared_ptr out; +/// use colour in error messages? +static enum { AUTO, ON, OFF } color = AUTO; + // buffer the contents of stdin so we can read it twice static void buffer_stdin() { @@ -46,6 +52,8 @@ static void parse_args(int argc, char **argv) { static struct option opts[] = { // clang-format off + { "color", required_argument, 0, 139 }, + { "colour", required_argument, 0, 139 }, { "decompose-complex-comparisons", no_argument, 0, 128 }, { "explicit-semicolons", no_argument, 0, 129 }, { "help", no_argument, 0, 'h' }, @@ -134,6 +142,20 @@ static void parse_args(int argc, char **argv) { std::cout << "Murphi2Murphi version " << rumur_get_version() << '\n'; exit(EXIT_SUCCESS); + case 139: // --color, --colour + if (strcmp(optarg, "auto") == 0) { + color = AUTO; + } else if (strcmp(optarg, "on") == 0) { + color = ON; + } else if (strcmp(optarg, "off") == 0) { + color = OFF; + } else { + std::cerr << "invalid --colour argument \"" << optarg << "\"\n" + << "valid arguments are \"auto\", \"off\", and \"on\"\n"; + exit(EXIT_FAILURE); + } + break; + default: std::cerr << "unexpected error\n"; exit(EXIT_FAILURE); @@ -141,6 +163,8 @@ static void parse_args(int argc, char **argv) { } if (optind == argc - 1) { + in_filename = argv[optind]; + struct stat buf; if (stat(argv[optind], &buf) < 0) { std::cerr << "failed to open " << argv[optind] << ": " << strerror(errno) @@ -174,6 +198,78 @@ static void parse_args(int argc, char **argv) { } } +static bool use_colors() { + if (color == AUTO) + color = isatty(STDERR_FILENO) ? ON : OFF; + return color == ON; +} + +static const char *bold() { + if (use_colors()) + return "\033[1m"; + return ""; +} + +static const char *green() { + if (use_colors()) + return "\033[32m"; + return ""; +} + +static const char *red() { + if (use_colors()) + return "\033[31m"; + return ""; +} + +static const char *reset() { + if (use_colors()) + return "\033[0m"; + return ""; +} + +static const char *white() { + if (use_colors()) + return "\033[37m"; + return ""; +} + +static void print_location(std::istream &src, const rumur::location &location) { + + // the type of position.line and position.column changes across Bison + // releases, so avoid some -Wsign-compare warnings by casting them in advance + auto loc_line = static_cast(location.begin.line); + auto loc_col = static_cast(location.begin.column); + + std::string line; + unsigned long lineno = 0; + while (lineno < loc_line) { + if (!std::getline(src, line)) + return; + lineno++; + } + + // print the line, and construct an underline indicating the column location + std::ostringstream buf; + unsigned long col = 1; + for (const char &c : line) { + if (col == loc_col) { + buf << green() << bold() << '^' << reset(); + } else if (col < loc_col) { + if (c == '\t') { + buf << '\t'; + } else { + buf << ' '; + } + } + std::cerr << c; + col++; + } + std::cerr << '\n'; + + std::cerr << buf.str() << '\n'; +} + int main(int argc, char **argv) { // parse command line options @@ -186,7 +282,11 @@ int main(int argc, char **argv) { try { m = parse_model(*in); } catch (Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } @@ -200,7 +300,11 @@ int main(int argc, char **argv) { resolve_symbols(*m); validate(*m); } catch (Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } @@ -239,7 +343,11 @@ int main(int argc, char **argv) { pipe.finalise(); } catch (Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } From fa40e034fb6384a19154410d22089a8967ebf5b9 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 04/19] murphi2smv: print nicer colourised error messages MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #338 “location information in parsing rejections” --- misc/_murphi2smv | 1 + murphi2smv/doc/murphi2smv.1 | 6 ++ murphi2smv/src/main.cc | 106 +++++++++++++++++++++++++++++++++++- 3 files changed, 111 insertions(+), 2 deletions(-) diff --git a/misc/_murphi2smv b/misc/_murphi2smv index d9f86412..94ff54bc 100644 --- a/misc/_murphi2smv +++ b/misc/_murphi2smv @@ -3,6 +3,7 @@ # Zsh completion script for Murphi2SMV _arguments \ + '--colour[enable or disable ANSI colour codes]: :(auto off on)' \ '--help[display help information]' \ {--numeric-type,-n}'[target numeric type]:TYPE' \ {--output,-o}'[path to write SMV to]:filename:_files' \ diff --git a/murphi2smv/doc/murphi2smv.1 b/murphi2smv/doc/murphi2smv.1 index 1b0e139a..b360027b 100644 --- a/murphi2smv/doc/murphi2smv.1 +++ b/murphi2smv/doc/murphi2smv.1 @@ -10,6 +10,12 @@ checker. See .BR rumur(1) for more information about Rumur or Murphi. .SH OPTIONS +\fB\-\-colour\fR [\fBauto\fR | \fBoff\fR | \fBon\fR] +.RS +Enable or disable the use of ANSI colour codes in error messages. The default is +\fBauto\fR, to auto-detect based on whether the stderr is a TTY. +.RE +.PP \fB\-\-help\fR or \fB\-?\fR .RS Display usage information. diff --git a/murphi2smv/src/main.cc b/murphi2smv/src/main.cc index 807865e4..680f753f 100644 --- a/murphi2smv/src/main.cc +++ b/murphi2smv/src/main.cc @@ -3,7 +3,9 @@ #include "pick_numeric_type.h" #include "resources.h" #include +#include #include +#include #include #include #include @@ -12,6 +14,7 @@ #include #include #include +#include #include // a pair of input streams @@ -25,11 +28,16 @@ static std::shared_ptr out; std::string numeric_type; +/// use colour in error messages? +static enum { AUTO, ON, OFF } color = AUTO; + static void parse_args(int argc, char **argv) { for (;;) { static struct option options[] = { // clang-format off + { "color", required_argument, 0, 129 }, + { "colour", required_argument, 0, 129 }, { "help", no_argument, 0, 'h' }, { "numeric-type", required_argument, 0, 'n' }, { "output", required_argument, 0, 'o' }, @@ -70,6 +78,20 @@ static void parse_args(int argc, char **argv) { std::cout << "Murphi2SMV version " << rumur_get_version() << '\n'; exit(EXIT_SUCCESS); + case 129: // --color, --colour + if (strcmp(optarg, "auto") == 0) { + color = AUTO; + } else if (strcmp(optarg, "on") == 0) { + color = ON; + } else if (strcmp(optarg, "off") == 0) { + color = OFF; + } else { + std::cerr << "invalid --colour argument \"" << optarg << "\"\n" + << "valid arguments are \"auto\", \"off\", and \"on\"\n"; + exit(EXIT_FAILURE); + } + break; + default: std::cerr << "unexpected error\n"; exit(EXIT_FAILURE); @@ -118,6 +140,78 @@ static std::ostream &output() { return out == nullptr ? std::cout : *out; } +static bool use_colors() { + if (color == AUTO) + color = isatty(STDERR_FILENO) ? ON : OFF; + return color == ON; +} + +static const char *bold() { + if (use_colors()) + return "\033[1m"; + return ""; +} + +static const char *green() { + if (use_colors()) + return "\033[32m"; + return ""; +} + +static const char *red() { + if (use_colors()) + return "\033[31m"; + return ""; +} + +static const char *reset() { + if (use_colors()) + return "\033[0m"; + return ""; +} + +static const char *white() { + if (use_colors()) + return "\033[37m"; + return ""; +} + +static void print_location(std::istream &src, const rumur::location &location) { + + // the type of position.line and position.column changes across Bison + // releases, so avoid some -Wsign-compare warnings by casting them in advance + auto loc_line = static_cast(location.begin.line); + auto loc_col = static_cast(location.begin.column); + + std::string line; + unsigned long lineno = 0; + while (lineno < loc_line) { + if (!std::getline(src, line)) + return; + lineno++; + } + + // print the line, and construct an underline indicating the column location + std::ostringstream buf; + unsigned long col = 1; + for (const char &c : line) { + if (col == loc_col) { + buf << green() << bold() << '^' << reset(); + } else if (col < loc_col) { + if (c == '\t') { + buf << '\t'; + } else { + buf << ' '; + } + } + std::cerr << c; + col++; + } + std::cerr << '\n'; + + std::cerr << buf.str() << '\n'; +} + int main(int argc, char **argv) { // parse command line options @@ -133,7 +227,11 @@ int main(int argc, char **argv) { try { parsed = rumur::parse(*in.first); } catch (rumur::Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + in.first->seekg(0); + print_location(*in.first, e.loc); return EXIT_FAILURE; } @@ -151,7 +249,11 @@ int main(int argc, char **argv) { resolve_symbols(*model); validate(*model); } catch (rumur::Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() + << ' ' << white() << bold() << e.what() << reset() << '\n'; + in.first->seekg(0); + print_location(*in.first, e.loc); return EXIT_FAILURE; } } From 2532abbd930d94d2a56c83473dd948925f38cc23 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 05/19] fix mistakenly disabled clang-format --- murphi2smv/src/main.cc | 6 ++---- murphi2uclid/src/main.cc | 26 ++++++++++++-------------- 2 files changed, 14 insertions(+), 18 deletions(-) diff --git a/murphi2smv/src/main.cc b/murphi2smv/src/main.cc index 680f753f..3281d59c 100644 --- a/murphi2smv/src/main.cc +++ b/murphi2smv/src/main.cc @@ -43,7 +43,7 @@ static void parse_args(int argc, char **argv) { { "output", required_argument, 0, 'o' }, { "version", no_argument, 0, 128 }, { 0, 0, 0, 0 }, - // clange-format on + // clang-format on }; int option_index = 0; @@ -136,9 +136,7 @@ static dup_t make_stdin_dup() { return dup_t{buffer, copy}; } -static std::ostream &output() { - return out == nullptr ? std::cout : *out; -} +static std::ostream &output() { return out == nullptr ? std::cout : *out; } static bool use_colors() { if (color == AUTO) diff --git a/murphi2uclid/src/main.cc b/murphi2uclid/src/main.cc index d5694bb6..f480ce9e 100644 --- a/murphi2uclid/src/main.cc +++ b/murphi2uclid/src/main.cc @@ -62,7 +62,7 @@ static void parse_args(int argc, char **argv) { { "verbose", no_argument, 0, 'v' }, { "version", no_argument, 0, 128 }, { 0, 0, 0, 0 }, - // clange-format on + // clang-format on }; int option_index = 0; @@ -153,9 +153,7 @@ static dup_t make_stdin_dup() { return dup_t(buffer, copy); } -static std::ostream &output() { - return out == nullptr ? std::cout : *out; -} +static std::ostream &output() { return out == nullptr ? std::cout : *out; } int main(int argc, char **argv) { @@ -182,17 +180,17 @@ int main(int argc, char **argv) { auto model = dynamic_cast(parsed.get()); if (model != nullptr) { - // update unique identifiers within the model - model->reindex(); + // update unique identifiers within the model + model->reindex(); - // check the model is valid - try { - resolve_symbols(*model); - validate(*model); - } catch (rumur::Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; - return EXIT_FAILURE; - } + // check the model is valid + try { + resolve_symbols(*model); + validate(*model); + } catch (rumur::Error &e) { + std::cerr << e.loc << ":" << e.what() << '\n'; + return EXIT_FAILURE; + } } // name any rules that are unnamed, so they get valid Uclid5 symbols From 2a687c682caeeed64622fe7d467237a46262ea5e Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 06/19] murphi2uclid: print nicer colourised error messages MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #338 “location information in parsing rejections” --- murphi2uclid/doc/murphi2uclid.1 | 6 ++ murphi2uclid/src/main.cc | 110 +++++++++++++++++++++++++++++++- 2 files changed, 113 insertions(+), 3 deletions(-) diff --git a/murphi2uclid/doc/murphi2uclid.1 b/murphi2uclid/doc/murphi2uclid.1 index b3896f64..44d58adb 100644 --- a/murphi2uclid/doc/murphi2uclid.1 +++ b/murphi2uclid/doc/murphi2uclid.1 @@ -9,6 +9,12 @@ be used to translate a Murphi model into a Uclid5 model. See .BR rumur(1) for more information about Rumur or Murphi. .SH OPTIONS +\fB\-\-colour\fR [\fBauto\fR | \fBoff\fR | \fBon\fR] +.RS +Enable or disable the use of ANSI colour codes in error messages. The default is +\fBauto\fR, to auto-detect based on whether the stderr is a TTY. +.RE +.PP \fB\-\-help\fR or \fB\-?\fR .RS Display usage information. diff --git a/murphi2uclid/src/main.cc b/murphi2uclid/src/main.cc index f480ce9e..b2e4dc65 100644 --- a/murphi2uclid/src/main.cc +++ b/murphi2uclid/src/main.cc @@ -18,6 +18,7 @@ #include #include #include +#include #include #include @@ -34,6 +35,9 @@ std::string module_name = "main"; std::string numeric_type; +/// use colour in error messages? +static enum { AUTO, ON, OFF } color = AUTO; + static bool is_valid_numeric_type(const char *s) { assert(s != NULL); if (strcmp(s, "integer") == 0) @@ -54,6 +58,8 @@ static void parse_args(int argc, char **argv) { for (;;) { static struct option options[] = { // clang-format off + { "color", required_argument, 0, 129 }, + { "colour", required_argument, 0, 129 }, { "help", no_argument, 0, 'h' }, { "module", required_argument, 0, 'm' }, { "numeric-type", required_argument, 0, 'n' }, @@ -109,6 +115,20 @@ static void parse_args(int argc, char **argv) { std::cout << "Murphi2Uclid version " << rumur_get_version() << '\n'; exit(EXIT_SUCCESS); + case 129: // --color, --colour + if (strcmp(optarg, "auto") == 0) { + color = AUTO; + } else if (strcmp(optarg, "on") == 0) { + color = ON; + } else if (strcmp(optarg, "off") == 0) { + color = OFF; + } else { + std::cerr << "invalid --colour argument \"" << optarg << "\"\n" + << "valid arguments are \"auto\", \"off\", and \"on\"\n"; + exit(EXIT_FAILURE); + } + break; + default: std::cerr << "unexpected error\n"; exit(EXIT_FAILURE); @@ -155,6 +175,78 @@ static dup_t make_stdin_dup() { static std::ostream &output() { return out == nullptr ? std::cout : *out; } +static bool use_colors() { + if (color == AUTO) + color = isatty(STDERR_FILENO) ? ON : OFF; + return color == ON; +} + +static const char *bold() { + if (use_colors()) + return "\033[1m"; + return ""; +} + +static const char *green() { + if (use_colors()) + return "\033[32m"; + return ""; +} + +static const char *red() { + if (use_colors()) + return "\033[31m"; + return ""; +} + +static const char *reset() { + if (use_colors()) + return "\033[0m"; + return ""; +} + +static const char *white() { + if (use_colors()) + return "\033[37m"; + return ""; +} + +static void print_location(std::istream &src, const rumur::location &location) { + + // the type of position.line and position.column changes across Bison + // releases, so avoid some -Wsign-compare warnings by casting them in advance + auto loc_line = static_cast(location.begin.line); + auto loc_col = static_cast(location.begin.column); + + std::string line; + unsigned long lineno = 0; + while (lineno < loc_line) { + if (!std::getline(src, line)) + return; + lineno++; + } + + // print the line, and construct an underline indicating the column location + std::ostringstream buf; + unsigned long col = 1; + for (const char &c : line) { + if (col == loc_col) { + buf << green() << bold() << '^' << reset(); + } else if (col < loc_col) { + if (c == '\t') { + buf << '\t'; + } else { + buf << ' '; + } + } + std::cerr << c; + col++; + } + std::cerr << '\n'; + + std::cerr << buf.str() << '\n'; +} + int main(int argc, char **argv) { // parse command line options @@ -170,7 +262,11 @@ int main(int argc, char **argv) { try { parsed = rumur::parse(*in.first); } catch (rumur::Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + in.first->seekg(0); + print_location(*in.first, e.loc); return EXIT_FAILURE; } @@ -188,7 +284,11 @@ int main(int argc, char **argv) { resolve_symbols(*model); validate(*model); } catch (rumur::Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() + << ' ' << white() << bold() << e.what() << reset() << '\n'; + in.first->seekg(0); + print_location(*in.first, e.loc); return EXIT_FAILURE; } } @@ -200,7 +300,11 @@ int main(int argc, char **argv) { try { check(*parsed); } catch (rumur::Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + in.first->seekg(0); + print_location(*in.first, e.loc); return EXIT_FAILURE; } From 64e096e0c89cf8d620a0ab126f71159af2941f13 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 07/19] murphi2xml: print nicer colourised error messages MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Github: #338 “location information in parsing rejections” --- misc/_murphi2xml | 1 + murphi2xml/doc/murphi2xml.1 | 6 +++ murphi2xml/src/main.cc | 105 +++++++++++++++++++++++++++++++++++- 3 files changed, 110 insertions(+), 2 deletions(-) diff --git a/misc/_murphi2xml b/misc/_murphi2xml index 58d75614..eee56e5d 100644 --- a/misc/_murphi2xml +++ b/misc/_murphi2xml @@ -3,6 +3,7 @@ # Zsh completion script for Murphi2XML _arguments \ + '--colour[enable or disable ANSI colour codes]: :(auto off on)' \ '--help[display help information]' \ {--output,-o}'[path to write XML to]:filename:_files' \ '--version[output version information]' \ diff --git a/murphi2xml/doc/murphi2xml.1 b/murphi2xml/doc/murphi2xml.1 index de726099..6eb0117f 100644 --- a/murphi2xml/doc/murphi2xml.1 +++ b/murphi2xml/doc/murphi2xml.1 @@ -10,6 +10,12 @@ format. See .BR rumur(1) for more information about Rumur or Murphi. .SH OPTIONS +\fB\-\-colour\fR [\fBauto\fR | \fBoff\fR | \fBon\fR] +.RS +Enable or disable the use of ANSI colour codes in error messages. The default is +\fBauto\fR, to auto-detect based on whether the stderr is a TTY. +.RE +.PP \fB\-\-help\fR or \fB\-?\fR .RS Display usage information. diff --git a/murphi2xml/src/main.cc b/murphi2xml/src/main.cc index 1b74ce65..28f588ce 100644 --- a/murphi2xml/src/main.cc +++ b/murphi2xml/src/main.cc @@ -2,7 +2,9 @@ #include "XMLPrinter.h" #include "resources.h" #include +#include #include +#include #include #include #include @@ -18,6 +20,9 @@ static std::shared_ptr in; static std::shared_ptr in_replay; static std::shared_ptr out; +/// use colour in error messages? +static enum { AUTO, ON, OFF } color = AUTO; + // buffer the contents of stdin so we can read it twice static void buffer_stdin() { @@ -35,6 +40,8 @@ static void parse_args(int argc, char **argv) { for (;;) { static struct option options[] = { + {"color", required_argument, 0, 129}, + {"colour", required_argument, 0, 129}, {"help", no_argument, 0, '?'}, {"output", required_argument, 0, 'o'}, {"version", no_argument, 0, 128}, @@ -67,6 +74,20 @@ static void parse_args(int argc, char **argv) { std::cout << "Rumur version " << rumur_get_version() << '\n'; exit(EXIT_SUCCESS); + case 129: // --color, --colour + if (strcmp(optarg, "auto") == 0) { + color = AUTO; + } else if (strcmp(optarg, "on") == 0) { + color = ON; + } else if (strcmp(optarg, "off") == 0) { + color = OFF; + } else { + std::cerr << "invalid --colour argument \"" << optarg << "\"\n" + << "valid arguments are \"auto\", \"off\", and \"on\"\n"; + exit(EXIT_FAILURE); + } + break; + default: std::cerr << "unexpected error\n"; exit(EXIT_FAILURE); @@ -109,6 +130,78 @@ static void parse_args(int argc, char **argv) { } } +static bool use_colors() { + if (color == AUTO) + color = isatty(STDERR_FILENO) ? ON : OFF; + return color == ON; +} + +static const char *bold() { + if (use_colors()) + return "\033[1m"; + return ""; +} + +static const char *green() { + if (use_colors()) + return "\033[32m"; + return ""; +} + +static const char *red() { + if (use_colors()) + return "\033[31m"; + return ""; +} + +static const char *reset() { + if (use_colors()) + return "\033[0m"; + return ""; +} + +static const char *white() { + if (use_colors()) + return "\033[37m"; + return ""; +} + +static void print_location(std::istream &src, const rumur::location &location) { + + // the type of position.line and position.column changes across Bison + // releases, so avoid some -Wsign-compare warnings by casting them in advance + auto loc_line = static_cast(location.begin.line); + auto loc_col = static_cast(location.begin.column); + + std::string line; + unsigned long lineno = 0; + while (lineno < loc_line) { + if (!std::getline(src, line)) + return; + lineno++; + } + + // print the line, and construct an underline indicating the column location + std::ostringstream buf; + unsigned long col = 1; + for (const char &c : line) { + if (col == loc_col) { + buf << green() << bold() << '^' << reset(); + } else if (col < loc_col) { + if (c == '\t') { + buf << '\t'; + } else { + buf << ' '; + } + } + std::cerr << c; + col++; + } + std::cerr << '\n'; + + std::cerr << buf.str() << '\n'; +} + int main(int argc, char **argv) { // Parse command line options @@ -121,7 +214,11 @@ int main(int argc, char **argv) { try { m = rumur::parse_model(*in); } catch (rumur::Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } @@ -134,7 +231,11 @@ int main(int argc, char **argv) { resolve_symbols(*m); validate(*m); } catch (rumur::Error &e) { - std::cerr << e.loc << ":" << e.what() << '\n'; + std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' + << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' + << white() << bold() << e.what() << reset() << '\n'; + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } From 7185c93c1e47c9e29fab5b64369f1c0013175097 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 08/19] murphi2c: remove unnecessary duplication of input stream Instead of duplicating this in memory, we can just rely on being able to rewind a single stream. --- murphi2c/src/main.cc | 40 +++++++++++++++++----------------------- 1 file changed, 17 insertions(+), 23 deletions(-) diff --git a/murphi2c/src/main.cc b/murphi2c/src/main.cc index 7ea84ca4..38d836a4 100644 --- a/murphi2c/src/main.cc +++ b/murphi2c/src/main.cc @@ -19,15 +19,10 @@ #include #include #include -#include #include -// a pair of input streams -using dup_t = - std::pair, std::shared_ptr>; - static std::string in_filename = ""; -static dup_t in; +static std::shared_ptr in; static std::shared_ptr out; // output C source? (as opposed to C header) @@ -133,25 +128,21 @@ static void parse_args(int argc, char **argv) { in_filename = argv[optind]; auto i = std::make_shared(in_filename); - auto j = std::make_shared(in_filename); - if (!i->is_open() || !j->is_open()) { + if (!i->is_open()) { std::cerr << "failed to open " << in_filename << '\n'; exit(EXIT_FAILURE); } - in = dup_t(i, j); + in = i; } } -static dup_t make_stdin_dup() { +static std::shared_ptr make_stdin_buf() { // read stdin into memory auto buffer = std::make_shared(); *buffer << std::cin.rdbuf(); - // duplicate the buffer - auto copy = std::make_shared(buffer->str()); - - return dup_t(buffer, copy); + return buffer; } static bool use_colors() { @@ -231,20 +222,20 @@ int main(int argc, char **argv) { // parse command line options parse_args(argc, argv); - // if we are reading from stdin, duplicate it so that we can parse it both as - // Murphi and for comments - if (in.first == nullptr) - in = make_stdin_dup(); + // if we are reading from stdin, duplicate it so that we can seek it + if (in == nullptr) + in = make_stdin_buf(); // parse input model rumur::Ptr m; try { - m = rumur::parse_model(*in.first); + m = rumur::parse_model(*in); } catch (rumur::Error &e) { std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' << white() << bold() << e.what() << reset() << '\n'; - print_location(*in.second, e.loc); + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } @@ -261,7 +252,8 @@ int main(int argc, char **argv) { std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' << white() << bold() << e.what() << reset() << '\n'; - print_location(*in.second, e.loc); + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } @@ -272,7 +264,8 @@ int main(int argc, char **argv) { std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' << white() << bold() << e.what() << reset() << '\n'; - print_location(*in.second, e.loc); + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } @@ -284,7 +277,8 @@ int main(int argc, char **argv) { bool pack = compares_complex_values(*m); // parse comments from the source code - std::vector comments = rumur::parse_comments(*in.second); + in->seekg(0); + std::vector comments = rumur::parse_comments(*in); // output code if (source) { From c32c1147cf0b507a3328905c86c8d81a4ebdd0a6 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 09/19] murphi2c: remove an unnecessary use of 'std::string' --- murphi2c/src/main.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/murphi2c/src/main.cc b/murphi2c/src/main.cc index 38d836a4..fbd3284a 100644 --- a/murphi2c/src/main.cc +++ b/murphi2c/src/main.cc @@ -21,7 +21,7 @@ #include #include -static std::string in_filename = ""; +static const char *in_filename = ""; static std::shared_ptr in; static std::shared_ptr out; From e0a9a244018c11225bc17334f7116402dbacf7e0 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 10/19] murphi2murphi: remove unnecessary duplication of input stream Instead of duplicating this in memory, we can just rely on being able to rewind a single stream. --- murphi2murphi/src/main.cc | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/murphi2murphi/src/main.cc b/murphi2murphi/src/main.cc index fd05b57d..f77a0bc2 100644 --- a/murphi2murphi/src/main.cc +++ b/murphi2murphi/src/main.cc @@ -27,7 +27,6 @@ using namespace rumur; static const char *in_filename = ""; static std::shared_ptr in; -static std::shared_ptr in_replay; static std::shared_ptr out; /// use colour in error messages? @@ -41,9 +40,8 @@ static void buffer_stdin() { buf << std::cin.rdbuf(); buf.flush(); - // put this into two buffers we can read from + // put this into a buffer we can read from in = std::make_shared(buf.str()); - in_replay = std::make_shared(buf.str()); } static void parse_args(int argc, char **argv) { @@ -184,14 +182,6 @@ static void parse_args(int argc, char **argv) { exit(EXIT_FAILURE); } in = i; - - // open the input again that we need for replay during XML output - auto i2 = std::make_shared(argv[optind]); - if (!i2->is_open()) { - std::cerr << "failed to open " << argv[optind] << '\n'; - exit(EXIT_FAILURE); - } - in_replay = i2; } else { // we are going to read data from stdin buffer_stdin(); @@ -312,7 +302,8 @@ int main(int argc, char **argv) { Pipeline pipe; // add output generator - Printer p(*in_replay, out == nullptr ? std::cout : *out); + in->seekg(0); + Printer p(*in, out == nullptr ? std::cout : *out); pipe.add_stage(p); // are we adding semi-colons? From cce4bdf6033b7e48d881a1640d877922ebdb6df1 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 11/19] murphi2smv: remove unnecessary duplication of input stream Instead of duplicating this in memory, we can just rely on being able to rewind a single stream. --- murphi2smv/src/main.cc | 39 +++++++++++++++------------------------ 1 file changed, 15 insertions(+), 24 deletions(-) diff --git a/murphi2smv/src/main.cc b/murphi2smv/src/main.cc index 3281d59c..5edbc97e 100644 --- a/murphi2smv/src/main.cc +++ b/murphi2smv/src/main.cc @@ -15,14 +15,9 @@ #include #include #include -#include - -// a pair of input streams -using dup_t = - std::pair, std::shared_ptr>; static std::string in_filename{""}; -static dup_t in; +static std::shared_ptr in; static std::string out_filename{"-"}; static std::shared_ptr out; @@ -115,25 +110,21 @@ static void parse_args(int argc, char **argv) { in_filename = argv[optind]; auto i = std::make_shared(in_filename); - auto j = std::make_shared(in_filename); - if (!i->is_open() || !j->is_open()) { + if (!i->is_open()) { std::cerr << "failed to open " << in_filename << '\n'; exit(EXIT_FAILURE); } - in = dup_t{i, j}; + in = i; } } -static dup_t make_stdin_dup() { +static std::shared_ptr make_stdin_buf() { // read stdin into memory auto buffer = std::make_shared(); *buffer << std::cin.rdbuf(); - // duplicate the buffer - auto copy = std::make_shared(buffer->str()); - - return dup_t{buffer, copy}; + return buffer; } static std::ostream &output() { return out == nullptr ? std::cout : *out; } @@ -215,21 +206,20 @@ int main(int argc, char **argv) { // parse command line options parse_args(argc, argv); - // if we are reading from stdin, duplicate it so that we can parse it both as - // Murphi and for comments - if (in.first == nullptr) - in = make_stdin_dup(); + // if we are reading from stdin, buffer it so that we can seek it + if (in == nullptr) + in = make_stdin_buf(); // parse input rumur::Ptr parsed; try { - parsed = rumur::parse(*in.first); + parsed = rumur::parse(*in); } catch (rumur::Error &e) { std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' << white() << bold() << e.what() << reset() << '\n'; - in.first->seekg(0); - print_location(*in.first, e.loc); + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } @@ -250,8 +240,8 @@ int main(int argc, char **argv) { std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' << white() << bold() << e.what() << reset() << '\n'; - in.first->seekg(0); - print_location(*in.first, e.loc); + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } } @@ -261,7 +251,8 @@ int main(int argc, char **argv) { numeric_type = pick_numeric_type(*parsed); // parse comments from the source code - std::vector comments = rumur::parse_comments(*in.second); + in->seekg(0); + std::vector comments = rumur::parse_comments(*in); // only *now* open the output file, to avoid creating an empty file if any of // the preceding steps fail From 2f56d133d178d19d8f66fdb1f256985ed2425f26 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 12/19] murphi2smv: remove an unnecessary use of 'std::string' --- murphi2smv/src/main.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/murphi2smv/src/main.cc b/murphi2smv/src/main.cc index 5edbc97e..311b1b65 100644 --- a/murphi2smv/src/main.cc +++ b/murphi2smv/src/main.cc @@ -16,7 +16,7 @@ #include #include -static std::string in_filename{""}; +static const char *in_filename = ""; static std::shared_ptr in; static std::string out_filename{"-"}; static std::shared_ptr out; From 18eb62f7ec0b2838698f5e336960f798eb04597c Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 13/19] murphi2smv: remove another unnecessary use of 'std::string' --- murphi2smv/src/main.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/murphi2smv/src/main.cc b/murphi2smv/src/main.cc index 311b1b65..6228a9e0 100644 --- a/murphi2smv/src/main.cc +++ b/murphi2smv/src/main.cc @@ -18,7 +18,7 @@ static const char *in_filename = ""; static std::shared_ptr in; -static std::string out_filename{"-"}; +static const char *out_filename = "-"; static std::shared_ptr out; std::string numeric_type; @@ -256,7 +256,7 @@ int main(int argc, char **argv) { // only *now* open the output file, to avoid creating an empty file if any of // the preceding steps fail - if (out_filename != "-") { + if (strcmp(out_filename, "-") != 0) { auto o = std::make_shared(out_filename); if (!o->is_open()) { std::cerr << "failed to open " << out_filename << '\n'; From 275f688c5fc9b41c10b80410eed2798d684b3f3d Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 14/19] murphi2uclid: remove unnecessary duplication of input stream Instead of duplicating this in memory, we can just rely on being able to rewind a single stream. --- murphi2uclid/src/main.cc | 40 ++++++++++++++++------------------------ 1 file changed, 16 insertions(+), 24 deletions(-) diff --git a/murphi2uclid/src/main.cc b/murphi2uclid/src/main.cc index b2e4dc65..8bd5bb7b 100644 --- a/murphi2uclid/src/main.cc +++ b/murphi2uclid/src/main.cc @@ -19,15 +19,10 @@ #include #include #include -#include #include -// a pair of input streams -using dup_t = - std::pair, std::shared_ptr>; - static std::string in_filename = ""; -static dup_t in; +static std::shared_ptr in; static std::string out_filename = "-"; static std::shared_ptr out; @@ -152,25 +147,21 @@ static void parse_args(int argc, char **argv) { in_filename = argv[optind]; auto i = std::make_shared(in_filename); - auto j = std::make_shared(in_filename); - if (!i->is_open() || !j->is_open()) { + if (!i->is_open()) { std::cerr << "failed to open " << in_filename << '\n'; exit(EXIT_FAILURE); } - in = dup_t(i, j); + in = i; } } -static dup_t make_stdin_dup() { +static std::shared_ptr make_stdin_buf() { // read stdin into memory auto buffer = std::make_shared(); *buffer << std::cin.rdbuf(); - // duplicate the buffer - auto copy = std::make_shared(buffer->str()); - - return dup_t(buffer, copy); + return buffer; } static std::ostream &output() { return out == nullptr ? std::cout : *out; } @@ -254,19 +245,19 @@ int main(int argc, char **argv) { // if we are reading from stdin, duplicate it so that we can parse it both as // Murphi and for comments - if (in.first == nullptr) - in = make_stdin_dup(); + if (in == nullptr) + in = make_stdin_buf(); // parse input rumur::Ptr parsed; try { - parsed = rumur::parse(*in.first); + parsed = rumur::parse(*in); } catch (rumur::Error &e) { std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' << white() << bold() << e.what() << reset() << '\n'; - in.first->seekg(0); - print_location(*in.first, e.loc); + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } @@ -287,8 +278,8 @@ int main(int argc, char **argv) { std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' << white() << bold() << e.what() << reset() << '\n'; - in.first->seekg(0); - print_location(*in.first, e.loc); + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } } @@ -303,8 +294,8 @@ int main(int argc, char **argv) { std::cerr << white() << bold() << in_filename << ':' << e.loc << ':' << reset() << ' ' << red() << bold() << "error:" << reset() << ' ' << white() << bold() << e.what() << reset() << '\n'; - in.first->seekg(0); - print_location(*in.first, e.loc); + in->seekg(0); + print_location(*in, e.loc); return EXIT_FAILURE; } @@ -313,7 +304,8 @@ int main(int argc, char **argv) { numeric_type = pick_numeric_type(*parsed); // parse comments from the source code - std::vector comments = rumur::parse_comments(*in.second); + in->seekg(0); + std::vector comments = rumur::parse_comments(*in); // only *now* open the output file, to avoid creating an empty file if any of // the preceding steps fail From d2013f4dc731b2acc491910867d76307e434781f Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 15/19] murphi2uclid: remove an unnecessary use of 'std::string' --- murphi2uclid/src/main.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/murphi2uclid/src/main.cc b/murphi2uclid/src/main.cc index 8bd5bb7b..b271f4e1 100644 --- a/murphi2uclid/src/main.cc +++ b/murphi2uclid/src/main.cc @@ -21,7 +21,7 @@ #include #include -static std::string in_filename = ""; +static const char *in_filename = ""; static std::shared_ptr in; static std::string out_filename = "-"; static std::shared_ptr out; From d30b38d31d6589e2bb00a4353e2880738b547c22 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 16/19] murphi2uclid: remove another unnecessary use of 'std::string' --- murphi2uclid/src/main.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/murphi2uclid/src/main.cc b/murphi2uclid/src/main.cc index b271f4e1..cb562a8a 100644 --- a/murphi2uclid/src/main.cc +++ b/murphi2uclid/src/main.cc @@ -23,7 +23,7 @@ static const char *in_filename = ""; static std::shared_ptr in; -static std::string out_filename = "-"; +static const char *out_filename = "-"; static std::shared_ptr out; std::string module_name = "main"; @@ -309,7 +309,7 @@ int main(int argc, char **argv) { // only *now* open the output file, to avoid creating an empty file if any of // the preceding steps fail - if (out_filename != "-") { + if (strcmp(out_filename, "-") != 0) { auto o = std::make_shared(out_filename); if (!o->is_open()) { std::cerr << "failed to open " << out_filename << '\n'; From f8a1f609cc5c3333fe490e2f57005890d5bd146a Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 17/19] murphi2xml: remove unnecessary duplication of input stream Instead of duplicating this in memory, we can just rely on being able to rewind a single stream. --- murphi2xml/src/main.cc | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/murphi2xml/src/main.cc b/murphi2xml/src/main.cc index 28f588ce..d5d88bd0 100644 --- a/murphi2xml/src/main.cc +++ b/murphi2xml/src/main.cc @@ -17,7 +17,6 @@ static std::string in_filename = ""; static std::shared_ptr in; -static std::shared_ptr in_replay; static std::shared_ptr out; /// use colour in error messages? @@ -31,9 +30,8 @@ static void buffer_stdin() { buf << std::cin.rdbuf(); buf.flush(); - // put this into two buffers we can read from + // put this into a buffer we can read from in = std::make_shared(buf.str()); - in_replay = std::make_shared(buf.str()); } static void parse_args(int argc, char **argv) { @@ -116,14 +114,6 @@ static void parse_args(int argc, char **argv) { exit(EXIT_FAILURE); } in = i; - - // open the input again that we need for replay during XML output - auto i2 = std::make_shared(in_filename); - if (!i2->is_open()) { - std::cerr << "failed to open " << in_filename << '\n'; - exit(EXIT_FAILURE); - } - in_replay = i2; } else { // we are going to read data from stdin buffer_stdin(); @@ -241,8 +231,9 @@ int main(int argc, char **argv) { assert(m != nullptr); + in->seekg(0); { - XMLPrinter p(in_filename, *in_replay, out == nullptr ? std::cout : *out); + XMLPrinter p(in_filename, *in, out == nullptr ? std::cout : *out); p.dispatch(*m); } From 2d444931cb16169d31b34f5d60cf8108f0ddbbb3 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 18/19] murphi2xml: remove an unnecessary use of 'std::string' --- murphi2xml/src/main.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/murphi2xml/src/main.cc b/murphi2xml/src/main.cc index d5d88bd0..4ddacf9b 100644 --- a/murphi2xml/src/main.cc +++ b/murphi2xml/src/main.cc @@ -15,7 +15,7 @@ #include #include -static std::string in_filename = ""; +static const char *in_filename = ""; static std::shared_ptr in; static std::shared_ptr out; From a8df199140f8f14297dd31b7dba06189b0a79450 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Mon, 7 Sep 2026 17:04:38 -0700 Subject: [PATCH 19/19] rumur: de-duplicate 'isatty' calls --- rumur/src/main.cc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/rumur/src/main.cc b/rumur/src/main.cc index 7725c37d..9eeaf666 100644 --- a/rumur/src/main.cc +++ b/rumur/src/main.cc @@ -544,8 +544,9 @@ static void parse_args(int argc, char **argv) { } static bool use_colors() { - return options.color == Color::ON || - (options.color == Color::AUTO && isatty(STDERR_FILENO)); + if (options.color == Color::AUTO) + options.color = isatty(STDERR_FILENO) ? Color::ON : Color::OFF; + return options.color == Color::ON; } static std::string bold() {