fix 'murphi2c' bugs

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

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

librumur/src/TypeExpr.cc

@@ -26,11 +26,11 @@ bool TypeExpr::is_simple() const { return false; }
 
 Ptr<TypeExpr> TypeExpr::resolve() const { return Ptr<TypeExpr>(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();

murphi2c/resources/c_prefix.c

@@ -41,32 +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); }
-
-// 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)
-
 

murphi2c/src/CLikeGenerator.cc

@@ -13,6 +13,94 @@
 
 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 + ")";
+}
+
+/// 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 << ")";
 }
@@ -115,9 +203,8 @@ void CLikeGenerator::visit_element(const Element &n) {
   auto a = dynamic_cast<const Array *>(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 + "_" + a->index_type->lower_bound();
+  // 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 << "])";
@@ -360,7 +447,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) {
@@ -486,10 +573,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 + "_" + a->index_type->lower_bound();
-    const std::string ub = value_type + "_" + a->index_type->upper_bound();
+    // 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";
@@ -546,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) {