Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
2aeb4c7
murphi2c: print nicer colourised error messages
Smattr Sep 8, 2026
18b99fe
murphi2c: nicer colourised error messages for unsupported features too
Smattr Sep 8, 2026
5ac576e
murphi2murphi: print nicer colourised error messages
Smattr Sep 8, 2026
fa40e03
murphi2smv: print nicer colourised error messages
Smattr Sep 8, 2026
2532abb
fix mistakenly disabled clang-format
Smattr Sep 8, 2026
2a687c6
murphi2uclid: print nicer colourised error messages
Smattr Sep 8, 2026
64e096e
murphi2xml: print nicer colourised error messages
Smattr Sep 8, 2026
7185c93
murphi2c: remove unnecessary duplication of input stream
Smattr Sep 8, 2026
c32c114
murphi2c: remove an unnecessary use of 'std::string'
Smattr Sep 8, 2026
e0a9a24
murphi2murphi: remove unnecessary duplication of input stream
Smattr Sep 8, 2026
cce4bdf
murphi2smv: remove unnecessary duplication of input stream
Smattr Sep 8, 2026
2f56d13
murphi2smv: remove an unnecessary use of 'std::string'
Smattr Sep 8, 2026
18eb62f
murphi2smv: remove another unnecessary use of 'std::string'
Smattr Sep 8, 2026
275f688
murphi2uclid: remove unnecessary duplication of input stream
Smattr Sep 8, 2026
d2013f4
murphi2uclid: remove an unnecessary use of 'std::string'
Smattr Sep 8, 2026
d30b38d
murphi2uclid: remove another unnecessary use of 'std::string'
Smattr Sep 8, 2026
f8a1f60
murphi2xml: remove unnecessary duplication of input stream
Smattr Sep 8, 2026
2d44493
murphi2xml: remove an unnecessary use of 'std::string'
Smattr Sep 8, 2026
a8df199
rumur: de-duplicate 'isatty' calls
Smattr Sep 8, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions misc/_murphi2c
Original file line number Diff line number Diff line change
Expand Up @@ -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' \
Expand Down
1 change: 1 addition & 0 deletions misc/_murphi2murphi
Original file line number Diff line number Diff line change
Expand Up @@ -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]' \
Expand Down
1 change: 1 addition & 0 deletions misc/_murphi2smv
Original file line number Diff line number Diff line change
Expand Up @@ -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' \
Expand Down
1 change: 1 addition & 0 deletions misc/_murphi2xml
Original file line number Diff line number Diff line change
Expand Up @@ -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]' \
Expand Down
6 changes: 6 additions & 0 deletions murphi2c/doc/murphi2c.1
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
68 changes: 19 additions & 49 deletions murphi2c/src/check.cc
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
7 changes: 4 additions & 3 deletions murphi2c/src/check.h
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

#include <rumur/rumur.h>

// 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);
146 changes: 123 additions & 23 deletions murphi2c/src/main.cc
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@
#include "resources.h"
#include <cassert>
#include <cstddef>
#include <cstdio>
#include <cstdlib>
#include <cstring>
#include <fstream>
#include <getopt.h>
#include <iostream>
Expand All @@ -17,25 +19,25 @@
#include <string>
#include <sys/stat.h>
#include <unistd.h>
#include <utility>
#include <vector>

// a pair of input streams
using dup_t =
std::pair<std::shared_ptr<std::istream>, std::shared_ptr<std::istream>>;

static std::string in_filename = "<stdin>";
static dup_t in;
static const char *in_filename = "<stdin>";
static std::shared_ptr<std::istream> in;
static std::shared_ptr<std::ostream> 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' },
Expand Down Expand Up @@ -89,6 +91,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);
Expand All @@ -112,43 +128,114 @@ static void parse_args(int argc, char **argv) {
in_filename = argv[optind];

auto i = std::make_shared<std::ifstream>(in_filename);
auto j = std::make_shared<std::ifstream>(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<std::istream> make_stdin_buf() {

// read stdin into memory
auto buffer = std::make_shared<std::stringstream>();
*buffer << std::cin.rdbuf();

// duplicate the buffer
auto copy = std::make_shared<std::istringstream>(buffer->str());
return buffer;
}

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 "";
}

return dup_t(buffer, copy);
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<unsigned long>(location.begin.line);
auto loc_col = static_cast<unsigned long>(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
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<rumur::Model> m;
try {
m = rumur::parse_model(*in.first);
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;
}

Expand All @@ -162,13 +249,25 @@ 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;
}

// 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';
in->seekg(0);
print_location(*in, e.loc);
return EXIT_FAILURE;
}

// name any rules that are unnamed, so they get valid C symbols
rumur::sanitise_rule_names(*m);
Expand All @@ -178,7 +277,8 @@ int main(int argc, char **argv) {
bool pack = compares_complex_values(*m);

// parse comments from the source code
std::vector<rumur::Comment> comments = rumur::parse_comments(*in.second);
in->seekg(0);
std::vector<rumur::Comment> comments = rumur::parse_comments(*in);

// output code
if (source) {
Expand Down
6 changes: 6 additions & 0 deletions murphi2murphi/doc/murphi2murphi.1
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading