From fd2a59a25af8c4a45f6ec85303c6bad9260a069e Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Sat, 15 Aug 2026 08:27:40 +1000 Subject: [PATCH 1/7] API BREAK: return an mpz from type bounds functions These functions were originally defined to return strings with the assumptions that (1) callers were only ever invoking them to then write the result into a C source file and (2) the bound value might be something not generation-time constant. In the current implementation it can be observed that (2) was not actually true. Upcoming changes to implement `union` require inspecting the values returned from these bound functions in a way that is hacky as long as they are strings. So (1) now no longer seems true either. Lets undo these assumptions by giving callers something more flexible to deal with. --- librumur/include/rumur/TypeExpr.h | 25 +++++++++-------- librumur/src/Expr.cc | 2 +- librumur/src/TypeExpr.cc | 29 ++++++++------------ murphi2c/src/CLikeGenerator.cc | 9 ++++--- rumur/src/generate-expr.cc | 45 ++++++++++++++++--------------- rumur/src/generate-print.cc | 4 +-- rumur/src/generate-quantifier.cc | 27 +++++++++---------- rumur/src/generate-stmt.cc | 7 ++--- 8 files changed, 73 insertions(+), 75 deletions(-) diff --git a/librumur/include/rumur/TypeExpr.h b/librumur/include/rumur/TypeExpr.h index 9d4189eb..a8592490 100644 --- a/librumur/include/rumur/TypeExpr.h +++ b/librumur/include/rumur/TypeExpr.h @@ -36,11 +36,10 @@ struct RUMUR_API_WITH_RTTI TypeExpr : public Node { virtual mpz_class count() const = 0; virtual Ptr resolve() const; - /* Numeric bounds of this type as valid C code. These are only valid to use on - * TypeExprs for which is_simple() returns true. - */ - virtual std::string lower_bound() const; - virtual std::string upper_bound() const; + // Numeric bounds of this type. These are only valid to use on TypeExprs for + // which is_simple() returns true. + virtual mpz_class lower_bound() const; + virtual mpz_class upper_bound() const; // Get a string representation of this type std::string to_string() const; @@ -81,8 +80,8 @@ struct RUMUR_API_WITH_RTTI Range : public TypeExpr { bool is_simple() const override; void validate() const override; - std::string lower_bound() const override; - std::string upper_bound() const override; + mpz_class lower_bound() const override; + mpz_class upper_bound() const override; void to_stream(std::ostream &out) const override; bool constant() const override; }; @@ -101,8 +100,8 @@ struct RUMUR_API_WITH_RTTI Scalarset : public TypeExpr { bool is_simple() const override; void validate() const override; - std::string lower_bound() const override; - std::string upper_bound() const override; + mpz_class lower_bound() const override; + mpz_class upper_bound() const override; void to_stream(std::ostream &out) const override; bool constant() const override; }; @@ -127,8 +126,8 @@ struct RUMUR_API_WITH_RTTI Enum : public TypeExpr { bool is_simple() const override; void validate() const override; - std::string lower_bound() const override; - std::string upper_bound() const override; + mpz_class lower_bound() const override; + mpz_class upper_bound() const override; void to_stream(std::ostream &out) const override; bool constant() const override; bool is_boolean() const override; @@ -185,8 +184,8 @@ struct RUMUR_API_WITH_RTTI TypeExprID : public TypeExpr { Ptr resolve() const override; void validate() const override; - std::string lower_bound() const override; - std::string upper_bound() const override; + mpz_class lower_bound() const override; + mpz_class upper_bound() const override; void to_stream(std::ostream &out) const override; bool constant() const override; }; diff --git a/librumur/src/Expr.cc b/librumur/src/Expr.cc index af062479..32f65580 100644 --- a/librumur/src/Expr.cc +++ b/librumur/src/Expr.cc @@ -1570,7 +1570,7 @@ std::string Quantifier::lower_bound() const { loc); if (type != nullptr) - return type->lower_bound(); + return "VALUE_C(" + type->lower_bound().get_str() + ")"; assert(from != nullptr && "quantifier with null type and null lower bound"); diff --git a/librumur/src/TypeExpr.cc b/librumur/src/TypeExpr.cc index 278ef3a5..680531f2 100644 --- a/librumur/src/TypeExpr.cc +++ b/librumur/src/TypeExpr.cc @@ -26,11 +26,11 @@ bool TypeExpr::is_simple() const { return false; } Ptr TypeExpr::resolve() const { return Ptr(clone()); } -std::string TypeExpr::lower_bound() const { +mpz_class TypeExpr::lower_bound() const { throw Error("complex types do not have valid lower bounds", loc); } -std::string TypeExpr::upper_bound() const { +mpz_class TypeExpr::upper_bound() const { throw Error("complex types do not have valid upper bounds", loc); } @@ -218,13 +218,9 @@ void Range::validate() const { throw Error("upper bound of range is less than lower bound", loc); } -std::string Range::lower_bound() const { - return "VALUE_C(" + min->constant_fold().get_str() + ")"; -} +mpz_class Range::lower_bound() const { return min->constant_fold(); } -std::string Range::upper_bound() const { - return "VALUE_C(" + max->constant_fold().get_str() + ")"; -} +mpz_class Range::upper_bound() const { return max->constant_fold(); } void Range::to_stream(std::ostream &out) const { out << *min << ".." << *max; } @@ -260,12 +256,9 @@ void Scalarset::validate() const { throw Error("bound of scalarset is not positive", bound->loc); } -std::string Scalarset::lower_bound() const { return "VALUE_C(0)"; } +mpz_class Scalarset::lower_bound() const { return 0; } -std::string Scalarset::upper_bound() const { - mpz_class b = bound->constant_fold() - 1; - return "VALUE_C(" + b.get_str() + ")"; -} +mpz_class Scalarset::upper_bound() const { return bound->constant_fold() - 1; } void Scalarset::to_stream(std::ostream &out) const { out << "scalarset(" << *bound << ")"; @@ -302,13 +295,13 @@ void Enum::validate() const { } } -std::string Enum::lower_bound() const { return "VALUE_C(0)"; } +mpz_class Enum::lower_bound() const { return 0; } -std::string Enum::upper_bound() const { +mpz_class Enum::upper_bound() const { mpz_class size = members.size(); if (size > 0) size--; - return "VALUE_C(" + size.get_str() + ")"; + return size; } void Enum::to_stream(std::ostream &out) const { @@ -464,13 +457,13 @@ void TypeExprID::validate() const { throw Error("unresolved type symbol \"" + name + "\"", loc); } -std::string TypeExprID::lower_bound() const { +mpz_class TypeExprID::lower_bound() const { if (referent == nullptr) throw Error("unresolved type symbol \"" + name + "\"", loc); return referent->value->lower_bound(); } -std::string TypeExprID::upper_bound() const { +mpz_class TypeExprID::upper_bound() const { if (referent == nullptr) throw Error("unresolved type symbol \"" + name + "\"", loc); return referent->value->upper_bound(); diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index c070663c..b687e1f8 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -117,7 +117,8 @@ void CLikeGenerator::visit_element(const Element &n) { // find the lower bound of its index type, using some hacky mangling to align // with one of the macros from ../resources/c_prefix.c - const std::string lb = value_type + "_" + a->index_type->lower_bound(); + const std::string lb = + value_type + "_VALUE_C(" + a->index_type->lower_bound().get_str() + ")"; // emit an indexing operation, now account for this *this << "(" << *n.array << ".data[(" << *n.index << ") - " << lb << "])"; @@ -488,8 +489,10 @@ void CLikeGenerator::print(const std::string &suffix, const TypeExpr &t, // get the bounds of the index and hackily prepend the value type to produce // something corresponding to one of the macros in ../resources/c_prefix.c - const std::string lb = value_type + "_" + a->index_type->lower_bound(); - const std::string ub = value_type + "_" + a->index_type->upper_bound(); + const std::string lb = + value_type + "_VALUE_C(" + a->index_type->lower_bound().get_str() + ")"; + const std::string ub = + value_type + "_VALUE_C(" + a->index_type->upper_bound().get_str() + ")"; *this << indentation() << "for (size_t " << i << " = 0; ; ++" << i << ") {\n"; diff --git a/rumur/src/generate-expr.cc b/rumur/src/generate-expr.cc index f153cf6d..751dc670 100644 --- a/rumur/src/generate-expr.cc +++ b/rumur/src/generate-expr.cc @@ -108,10 +108,11 @@ class Generator : public ConstExprTraversal { } if (!lvalue && a.element_type->is_simple()) { - const std::string lb = a.element_type->lower_bound(); - const std::string ub = a.element_type->upper_bound(); + const std::string lb = a.element_type->lower_bound().get_str(); + const std::string ub = a.element_type->upper_bound().get_str(); *out << "handle_read(" << to_C_string(n.loc) << ", rule_name, " - << to_C_string(n) << ", s, " << lb << ", " << ub << ", "; + << to_C_string(n) << ", s, VALUE_C(" << lb << "), VALUE_C(" << ub + << "), "; } *out << "handle_index(" << to_C_string(n.loc) << ", rule_name, " @@ -177,8 +178,8 @@ class Generator : public ConstExprTraversal { assert((!n.is_lvalue() || t != nullptr) && "lvalue without a type"); if (!lvalue && n.is_lvalue() && t->is_simple()) { - const std::string lb = t->lower_bound(); - const std::string ub = t->upper_bound(); + const std::string lb = "VALUE_C(" + t->lower_bound().get_str() + ")"; + const std::string ub = "VALUE_C(" + t->upper_bound().get_str() + ")"; *out << "handle_read(" << to_C_string(n.loc) << ", rule_name, " << to_C_string(n) << ", s, " << lb << ", " << ub << ", "; } @@ -207,10 +208,11 @@ class Generator : public ConstExprTraversal { for (const Ptr &f : r->fields) { if (f->name == n.field) { if (!lvalue && f->type->is_simple()) { - const std::string lb = f->type->lower_bound(); - const std::string ub = f->type->upper_bound(); + const std::string lb = f->type->lower_bound().get_str(); + const std::string ub = f->type->upper_bound().get_str(); *out << "handle_read(" << to_C_string(n.loc) << ", rule_name, " - << to_C_string(n) << ", s, " << lb << ", " << ub << ", "; + << to_C_string(n) << ", s, VALUE_C(" << lb << "), VALUE_C(" + << ub << "), "; } *out << "handle_narrow("; if (lvalue) { @@ -348,20 +350,20 @@ class Generator : public ConstExprTraversal { << ", .offset = 0, .width = " << p->width() << "ull }; "; if (method == 1) { - const std::string lb = p->get_type()->lower_bound(); - const std::string ub = p->get_type()->upper_bound(); + const std::string lb = p->get_type()->lower_bound().get_str(); + const std::string ub = p->get_type()->upper_bound().get_str(); *out << "handle_write(" << to_C_string(n.loc) << ", rule_name, " - << "\"\", s, " << lb << ", " << ub << ", " << handle - << ", "; + << "\"\", s, VALUE_C(" << lb << "), VALUE_C(" << ub + << "), " << handle << ", "; generate_rvalue(*out, *a); *out << "); "; } else if (method == 2) { - const std::string lb = p->get_type()->lower_bound(); - const std::string ub = p->get_type()->upper_bound(); + const std::string lb = p->get_type()->lower_bound().get_str(); + const std::string ub = p->get_type()->upper_bound().get_str(); - const std::string lba = a->type()->lower_bound(); + const std::string lba = a->type()->lower_bound().get_str(); *out << "{ " << "raw_value_t v = handle_read_raw(s, "; @@ -369,17 +371,18 @@ class Generator : public ConstExprTraversal { *out << "); " << "raw_value_t v2; " << "value_t v3; " - << "static const value_t lb = " << lb << "; " - << "static const value_t ub = " << ub << "; " - << "if (v != 0 && (SUB(v, 1, &v2) || ADD(v2, " << lba - << ", &v3) " + << "static const value_t lb = VALUE_C(" << lb << "); " + << "static const value_t ub = VALUE_C(" << ub << "); " + << "if (v != 0 && (SUB(v, 1, &v2) || ADD(v2, VALUE_C(" << lba + << "), &v3) " << "|| v3 < lb || v3 > ub)) { " << "error(s, \"call to function %s passed an out-of-range value " << "%\" PRIRAWVAL \" to parameter " << (index + 1) << "\", \"" - << n.name << "\", raw_value_to_string(v + " << lba << " - 1)); " + << n.name << "\", raw_value_to_string(v + VALUE_C(" << lba + << ") - 1)); " << "} " << "handle_write_raw(s, " << handle << ", v == 0 ? v : " - << "((raw_value_t)(v3 - " << lb << ") + 1)); " + << "((raw_value_t)(v3 - VALUE_C(" << lb << ")) + 1)); " << "} "; } else if (method == 3) { diff --git a/rumur/src/generate-print.cc b/rumur/src/generate-print.cc index 3084dde9..af3d31f9 100644 --- a/rumur/src/generate-print.cc +++ b/rumur/src/generate-print.cc @@ -360,8 +360,8 @@ class Generator : public ConstTypeTraversal { void visit_range(const Range &n) final { - const std::string lb = n.lower_bound(); - const std::string ub = n.upper_bound(); + const std::string lb = "VALUE_C(" + n.lower_bound().get_str() + ")"; + const std::string ub = "VALUE_C(" + n.upper_bound().get_str() + ")"; *out << "{\n" << " raw_value_t v = handle_read_raw(s, " << current_handle << ");\n" diff --git a/rumur/src/generate-quantifier.cc b/rumur/src/generate-quantifier.cc index a3125bd9..820d092f 100644 --- a/rumur/src/generate-quantifier.cc +++ b/rumur/src/generate-quantifier.cc @@ -37,7 +37,7 @@ void generate_quantifier_header(std::ostream &out, const Quantifier &q) { assert(q.from != nullptr); generate_rvalue(out, *q.from); } else { - out << q.type->lower_bound(); + out << "VALUE_C(" << q.type->lower_bound().get_str() << ")"; } out << ";\n"; @@ -46,7 +46,7 @@ void generate_quantifier_header(std::ostream &out, const Quantifier &q) { assert(q.to != nullptr); generate_rvalue(out, *q.to); } else { - out << q.type->upper_bound(); + out << "VALUE_C(" << q.type->upper_bound().get_str() << ")"; } out << ";\n"; @@ -88,19 +88,17 @@ void generate_quantifier_header(std::ostream &out, const Quantifier &q) { // bounds. References to this quantified variable will use these when // unpacking its compressed representation, so we need to offset the values we // store from it. - const std::string lower = q.decl->type->lower_bound(); - const std::string upper = q.decl->type->upper_bound(); + const std::string lower = q.decl->type->lower_bound().get_str(); + const std::string upper = q.decl->type->upper_bound().get_str(); out << "#if !defined(__clang__) && defined(__GNUC__)\n" << " #pragma GCC diagnostic push\n" << " #pragma GCC diagnostic ignored \"-Wtype-limits\"\n" << "#endif\n" - << " ASSERT(lb >= " << lower << " && lb <= " << upper - << " && " - "\"iteration lower bound exceeds type limits\");\n" - << " ASSERT(ub >= " << lower << " && ub <= " << upper - << " && " - "\"iteration upper bound exceeds type limits\");\n" + << " ASSERT(lb >= VALUE_C(" << lower << ") && lb <= VALUE_C(" << upper + << ") && \"iteration lower bound exceeds type limits\");\n" + << " ASSERT(ub >= VALUE_C(" << lower << ") && ub <= VALUE_C(" << upper + << ") && \"iteration upper bound exceeds type limits\");\n" << "#if !defined(__clang__) && defined(__GNUC__)\n" << " #pragma GCC diagnostic pop\n" << "#endif\n"; @@ -109,11 +107,12 @@ void generate_quantifier_header(std::ostream &out, const Quantifier &q) { // value we have is in range #define V_TO_RV(x) \ ("((raw_value_t)((raw_value_t)(((raw_value_t)" + std::string(x) + \ - ") + (raw_value_t)1) - (raw_value_t)(" + q.decl->type->lower_bound() + \ - ")))") + ") + (raw_value_t)1) - (raw_value_t)(VALUE_C(" + \ + q.decl->type->lower_bound().get_str() + "))))") #define RV_TO_V(x) \ - ("((value_t)(" + std::string(x) + " - (raw_value_t)1 + (raw_value_t)(" + \ - q.decl->type->lower_bound() + ")))") + ("((value_t)(" + std::string(x) + \ + " - (raw_value_t)1 + (raw_value_t)(VALUE_C(" + \ + q.decl->type->lower_bound().get_str() + "))))") // construct the pieces of our for-loop header const std::string init = "raw_value_t " + counter + " = " + V_TO_RV("lb"); diff --git a/rumur/src/generate-stmt.cc b/rumur/src/generate-stmt.cc index 70b60be0..12bb48ef 100644 --- a/rumur/src/generate-stmt.cc +++ b/rumur/src/generate-stmt.cc @@ -106,11 +106,12 @@ class Generator : public ConstStmtTraversal { void visit_assignment(const Assignment &s) final { if (s.lhs->type()->is_simple()) { - const std::string lb = s.lhs->type()->lower_bound(); - const std::string ub = s.lhs->type()->upper_bound(); + const std::string lb = s.lhs->type()->lower_bound().get_str(); + const std::string ub = s.lhs->type()->upper_bound().get_str(); *out << "handle_write(" << to_C_string(s.loc) << ", rule_name, " - << to_C_string(*s.lhs) << ", s, " << lb << ", " << ub << ", "; + << to_C_string(*s.lhs) << ", s, VALUE_C(" << lb << "), VALUE_C(" + << ub << "), "; generate_lvalue(*out, *s.lhs); *out << ", "; generate_rvalue(*out, *s.rhs); From 34e590e0dc7c7f77a97b9ef6434369d07e895901 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Sat, 15 Aug 2026 08:27:40 +1000 Subject: [PATCH 2/7] add a test case demonstrating a 'murphi2c' failure --- tests/tests.py | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/tests/tests.py b/tests/tests.py index cacc63f4..aafa98f8 100644 --- a/tests/tests.py +++ b/tests/tests.py @@ -1366,6 +1366,47 @@ def test_murphi2c_header(model, tmp_path): assert ret == 0, "C++ compilation failed:\n{}{}".format(stdout, stderr) +@pytest.mark.xfail(raises=AssertionError, reason="FIXME", strict=True) +def test_murphi2c_type_with_space(): + """can murphi2c handle a `--value-type` with a space in it?""" + + # an arbitrary model using array indices + src = """\ + var x: array[0..1] of boolean; + + startstate begin + x[0] := true; + end; + + rule begin + x[0] := !x[0]; + end; + """ + + # run this through murphi2c with a `--value-type` with a space + args = ["murphi2c", "--value-type=signed char"] + if has_valgrind(): + args = [ + "valgrind", + "--leak-check=full", + "--show-leak-kinds=all", + "--error-exitcode=42", + "--", + ] + args + ret, stdout, stderr = run(args, src) + if has_valgrind(): + assert ret != 42, "Memory leak:\n{}{}".format(stdout, stderr) + + assert ret == 0, "Unexpected murphi2c exit:\n{}{}".format(stdout, stderr) + + # ask the C compiler if the source is valid + args = [cc()] + c_flags() + ["-c", "-o", os.devnull, "-"] + ret, out, err = run(args, stdout) + assert ret == 0, "C compilation failed:\n{}{}\nProgram:\n{}".format( + out, err, stdout + ) + + @pytest.mark.parametrize("model", MODELS) def test_murphi2xml(model): """test cases for murphi2xml""" From 14df20c428cebf13d2d5e60f0a989dd75e96f1ce Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Sat, 15 Aug 2026 08:27:40 +1000 Subject: [PATCH 3/7] murphi2c: fix handling of value types containing spaces in array indexing Using a value type like `signed char` would result in generated code that failed to compile. Aside from fixing this problem, this change also leads to more intuitive looking generated code. --- murphi2c/resources/c_prefix.c | 14 -------- murphi2c/src/CLikeGenerator.cc | 62 ++++++++++++++++++++++++++++------ tests/tests.py | 1 - 3 files changed, 52 insertions(+), 25 deletions(-) diff --git a/murphi2c/resources/c_prefix.c b/murphi2c/resources/c_prefix.c index 59f7f511..231c1a50 100644 --- a/murphi2c/resources/c_prefix.c +++ b/murphi2c/resources/c_prefix.c @@ -55,18 +55,4 @@ static __attribute__((unused)) void print_uint32_t(uint32_t v) { printf("%" PRIu static __attribute__((unused)) void print_int64_t (int64_t v) { printf("%" PRId64, v); } static __attribute__((unused)) void print_uint64_t(uint64_t v) { printf("%" PRIu64, v); } -// wrappers for producing literal expressions of value type -#define int_VALUE_C(v) (v) -#define unsigned_VALUE_C(v) (v ## u) -#define short_VALUE_C(v) ((short)(v)) -#define long_VALUE_C(v) (v ## l) -#define int8_t_VALUE_C(v) INT8_C(v) -#define uint8_t_VALUE_C(v) UINT8_C(v) -#define int16_t_VALUE_C(v) INT16_C(v) -#define uint16_t_VALUE_C(v) UINT16_C(v) -#define int32_t_VALUE_C(v) INT32_C(v) -#define uint32_t_VALUE_C(v) UINT32_C(v) -#define int64_t_VALUE_C(v) INT64_C(v) -#define uint64_t_VALUE_C(v) UINT64_C(v) - diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index b687e1f8..15fcc722 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -13,6 +13,53 @@ using namespace rumur; +/// emit a typed C numeric literal +/// +/// Numeric literals are of type `int` in C by default. To spell a literal of a +/// different type, we need a bit of specialisation. This function is best +/// effort, in the sense that pathological input may result in an expression of +/// incorrect type. +/// +/// @param c_type The desired type of the resulting literal +/// @param v The value of the literal +/// @return C code that describes the given typed literal. +static std::string c_lit(const std::string &c_type, const mpz_class &v) { + const std::string s = v.get_str(); + if (c_type == "int") + return s; + if (c_type == "unsigned" || c_type == "unsigned int") + return s + "u"; + if (c_type == "long" || c_type == "long int" || c_type == "signed long" || + c_type == "signed long int") + return s + "l"; + if (c_type == "unsigned long" || c_type == "unsigned long int") + return s + "lu"; + if (c_type == "long long" || c_type == "long long int" || + c_type == "signed long long" || c_type == "signed long long int") + return s + "ll"; + if (c_type == "unsigned long long" || c_type == "unsigned long long int") + return s + "ull"; + if (c_type == "int8_t") + return "INT8_C(" + s + ")"; + if (c_type == "uint8_t") + return "UINT8_C(" + s + ")"; + if (c_type == "int16_t") + return "INT16_C(" + s + ")"; + if (c_type == "uint16_t") + return "UINT16_C(" + s + ")"; + if (c_type == "int32_t") + return "INT32_C(" + s + ")"; + if (c_type == "uint32_t") + return "UINT32_C(" + s + ")"; + if (c_type == "int64_t") + return "INT64_C(" + s + ")"; + if (c_type == "uint64_t") + return "UINT64_C(" + s + ")"; + + // otherwise assume we can construct the value with a cast + return "((" + c_type + ")" + s + ")"; +} + void CLikeGenerator::visit_add(const Add &n) { *this << "(" << *n.lhs << " + " << *n.rhs << ")"; } @@ -115,10 +162,8 @@ void CLikeGenerator::visit_element(const Element &n) { auto a = dynamic_cast(t.get()); assert(a != nullptr && "non-array on LHS of array indexing expression"); - // find the lower bound of its index type, using some hacky mangling to align - // with one of the macros from ../resources/c_prefix.c - const std::string lb = - value_type + "_VALUE_C(" + a->index_type->lower_bound().get_str() + ")"; + // find the lower bound of its index type + const std::string lb = c_lit(value_type, a->index_type->lower_bound()); // emit an indexing operation, now account for this *this << "(" << *n.array << ".data[(" << *n.index << ") - " << lb << "])"; @@ -487,12 +532,9 @@ void CLikeGenerator::print(const std::string &suffix, const TypeExpr &t, // invent a unique symbol using our counter const std::string i = "array_index" + std::to_string(counter); - // get the bounds of the index and hackily prepend the value type to produce - // something corresponding to one of the macros in ../resources/c_prefix.c - const std::string lb = - value_type + "_VALUE_C(" + a->index_type->lower_bound().get_str() + ")"; - const std::string ub = - value_type + "_VALUE_C(" + a->index_type->upper_bound().get_str() + ")"; + // get the bounds of the index + const std::string lb = c_lit(value_type, a->index_type->lower_bound()); + const std::string ub = c_lit(value_type, a->index_type->upper_bound()); *this << indentation() << "for (size_t " << i << " = 0; ; ++" << i << ") {\n"; diff --git a/tests/tests.py b/tests/tests.py index aafa98f8..acbec348 100644 --- a/tests/tests.py +++ b/tests/tests.py @@ -1366,7 +1366,6 @@ def test_murphi2c_header(model, tmp_path): assert ret == 0, "C++ compilation failed:\n{}{}".format(stdout, stderr) -@pytest.mark.xfail(raises=AssertionError, reason="FIXME", strict=True) def test_murphi2c_type_with_space(): """can murphi2c handle a `--value-type` with a space in it?""" From 9c0c3f272763eb4018d82da25c98c2a8f12ac862 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Sat, 15 Aug 2026 08:27:40 +1000 Subject: [PATCH 4/7] murphi2c: ensure numeric literals are correctly typed This avoids the value of a numeric literal being first interpreted as an `int` with possible truncation before casting it to its eventual type. --- murphi2c/src/CLikeGenerator.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index 15fcc722..8eb3d90c 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -406,7 +406,7 @@ void CLikeGenerator::visit_neq(const Neq &n) { void CLikeGenerator::visit_not(const Not &n) { *this << "(!" << *n.rhs << ")"; } void CLikeGenerator::visit_number(const Number &n) { - *this << "((" << value_type << ")(" << n.value.get_str() << "))"; + *this << c_lit(value_type, n.value); } void CLikeGenerator::visit_or(const Or &n) { From d45c50fc367066c08f2875ba1c70b287372c58e3 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Sat, 15 Aug 2026 08:27:40 +1000 Subject: [PATCH 5/7] add another failing 'murphi2c' test case --- tests/tests.py | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/tests/tests.py b/tests/tests.py index acbec348..94d61c22 100644 --- a/tests/tests.py +++ b/tests/tests.py @@ -1406,6 +1406,48 @@ def test_murphi2c_type_with_space(): ) +@pytest.mark.xfail(raises=AssertionError, reason="FIXME", strict=True) +def test_murphi2c_type_with_space2(): + """can murphi2c handle a `--value-type` with a space in it?""" + + # an arbitrary model using printing + src = """\ + var x: 0..1; + + startstate begin + x := 0; + end; + + rule begin + x := 1 - x; + put x; + end; + """ + + # run this through murphi2c with a `--value-type` with a space + args = ["murphi2c", "--value-type=signed char"] + if has_valgrind(): + args = [ + "valgrind", + "--leak-check=full", + "--show-leak-kinds=all", + "--error-exitcode=42", + "--", + ] + args + ret, stdout, stderr = run(args, src) + if has_valgrind(): + assert ret != 42, "Memory leak:\n{}{}".format(stdout, stderr) + + assert ret == 0, "Unexpected murphi2c exit:\n{}{}".format(stdout, stderr) + + # ask the C compiler if the source is valid + args = [cc()] + c_flags() + ["-c", "-o", os.devnull, "-"] + ret, out, err = run(args, stdout) + assert ret == 0, "C compilation failed:\n{}{}\nProgram:\n{}".format( + out, err, stdout + ) + + @pytest.mark.parametrize("model", MODELS) def test_murphi2xml(model): """test cases for murphi2xml""" From 95a2e91c49068556f08d267746d139fe9bbb09ab Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Sat, 15 Aug 2026 08:27:40 +1000 Subject: [PATCH 6/7] murphi2c: fix printing of values when value type contains a space Similar to the prior change to address this in array indexing, this not only fixes a bug but leads to more intuitive generated code. --- murphi2c/resources/c_prefix.c | 14 ----------- murphi2c/src/CLikeGenerator.cc | 44 +++++++++++++++++++++++++++++++++- tests/tests.py | 1 - 3 files changed, 43 insertions(+), 16 deletions(-) diff --git a/murphi2c/resources/c_prefix.c b/murphi2c/resources/c_prefix.c index 231c1a50..c3b1ae9e 100644 --- a/murphi2c/resources/c_prefix.c +++ b/murphi2c/resources/c_prefix.c @@ -41,18 +41,4 @@ static void liveness_(const char *message __attribute__((unused))) {} void (*liveness)(const char *) = liveness_; -// various printf wrappers to deal with the user having passed --value-type -static __attribute__((unused)) void print_int (int v) { printf("%d", v); } -static __attribute__((unused)) void print_unsigned(unsigned v) { printf("%u", v); } -static __attribute__((unused)) void print_short (short v) { printf("%hd", v); } -static __attribute__((unused)) void print_long (long v) { printf("%ld", v); } -static __attribute__((unused)) void print_int8_t (int8_t v) { printf("%" PRId8 , v); } -static __attribute__((unused)) void print_uint8_t (uint8_t v) { printf("%" PRIu8 , v); } -static __attribute__((unused)) void print_int16_t (int16_t v) { printf("%" PRId16, v); } -static __attribute__((unused)) void print_uint16_t(uint16_t v) { printf("%" PRIu16, v); } -static __attribute__((unused)) void print_int32_t (int32_t v) { printf("%" PRId32, v); } -static __attribute__((unused)) void print_uint32_t(uint32_t v) { printf("%" PRIu32, v); } -static __attribute__((unused)) void print_int64_t (int64_t v) { printf("%" PRId64, v); } -static __attribute__((unused)) void print_uint64_t(uint64_t v) { printf("%" PRIu64, v); } - diff --git a/murphi2c/src/CLikeGenerator.cc b/murphi2c/src/CLikeGenerator.cc index 8eb3d90c..96cb0908 100644 --- a/murphi2c/src/CLikeGenerator.cc +++ b/murphi2c/src/CLikeGenerator.cc @@ -60,6 +60,47 @@ static std::string c_lit(const std::string &c_type, const mpz_class &v) { return "((" + c_type + ")" + s + ")"; } +/// get the printf format code for printing a given type +/// +/// See call sites of this function for why the return value includes stray +/// quote characters. +/// +/// @param c_type Type to print +/// @return Printf format code for this type +static const char *c_pri(const std::string &c_type) { + if (c_type == "unsigned" || c_type == "unsigned int") + return "u\""; + if (c_type == "long" || c_type == "long int" || c_type == "signed long" || + c_type == "signed long int") + return "ld\""; + if (c_type == "unsigned long" || c_type == "unsigned long int") + return "lu\""; + if (c_type == "long long" || c_type == "long long int" || + c_type == "signed long long" || c_type == "signed long long int") + return "lld\""; + if (c_type == "unsigned long long" || c_type == "unsigned long long int") + return "llu\""; + if (c_type == "int8_t") + return "\" PRId8"; + if (c_type == "uint8_t") + return "\" PRIu8"; + if (c_type == "int16_t") + return "\" PRId16"; + if (c_type == "uint16_t") + return "\" PRIu16"; + if (c_type == "int32_t") + return "\" PRId32"; + if (c_type == "uint32_t") + return "\" PRIu32"; + if (c_type == "int64_t") + return "\" PRId64"; + if (c_type == "uint64_t") + return "\" PRIu64"; + + // otherwise assume we can print this as an int + return "d\""; +} + void CLikeGenerator::visit_add(const Add &n) { *this << "(" << *n.lhs << " + " << *n.rhs << ")"; } @@ -591,7 +632,8 @@ void CLikeGenerator::print(const std::string &suffix, const TypeExpr &t, } // fall back case, for Ranges and Scalarsets - *this << indentation() << "print_" << value_type << "(" << e << suffix << ")"; + *this << indentation() << "printf(\"%" << c_pri(value_type) << ", (" << e + << suffix << "))"; } void CLikeGenerator::visit_put(const Put &n) { diff --git a/tests/tests.py b/tests/tests.py index 94d61c22..5da8a684 100644 --- a/tests/tests.py +++ b/tests/tests.py @@ -1406,7 +1406,6 @@ def test_murphi2c_type_with_space(): ) -@pytest.mark.xfail(raises=AssertionError, reason="FIXME", strict=True) def test_murphi2c_type_with_space2(): """can murphi2c handle a `--value-type` with a space in it?""" From 42b3d63d79cf8fe5d95f6a2adfda04c737d7f127 Mon Sep 17 00:00:00 2001 From: Matthew Fernandez Date: Sat, 15 Aug 2026 08:27:40 +1000 Subject: [PATCH 7/7] disable clang formatting on some table-like code --- rumur/src/generate-expr.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/rumur/src/generate-expr.cc b/rumur/src/generate-expr.cc index 751dc670..e0547498 100644 --- a/rumur/src/generate-expr.cc +++ b/rumur/src/generate-expr.cc @@ -306,6 +306,7 @@ class Generator : public ConstExprTraversal { * 5. We pass the original (rvalue) handle. */ + // clang-format off auto get_method = [](const Ptr ¶meter, const Ptr &argument) { @@ -327,6 +328,7 @@ class Generator : public ConstExprTraversal { assert(!"unreachable"); __builtin_unreachable(); }; + // clang-format on // Create the temporaries for each argument. {