From d6d772c7f45b6f5341839bb09d716d924ebc24d4 Mon Sep 17 00:00:00 2001
From: John Regehr <regehr@cs.utah.edu>
Date: Tue, 21 Apr 2026 16:44:58 -0600
Subject: [PATCH] float printing was lossy in 2 places, fix this

---
 ir/constant.cpp | 10 ++++++++--
 ir/type.cpp     | 23 ++++++++++++++++++++++-
 2 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/ir/constant.cpp b/ir/constant.cpp
index 5a3dee67c..9e9a2468f 100644
--- a/ir/constant.cpp
+++ b/ir/constant.cpp
@@ -6,6 +6,7 @@
 #include "util/compiler.h"
 #include <bit>
 #include <cassert>
+#include <charconv>
 #include <cmath>
 // TODO: remove cstring when migrated to std::bit_cast
 #include <cstring>
@@ -66,8 +67,13 @@ static string bits_to_float(Type &type, const string &val) {
   uint64_t num = strtoull(val.c_str(), nullptr, 10);
   TO fp = mbit_cast<TI, TO>(num);
   auto fpclass = fpclassify(fp);
-  return fpclass == FP_NAN || fpclass == FP_SUBNORMAL ? to_hex(type, val)
-                                                      : to_string(fp);
+  if (fpclass == FP_NAN || fpclass == FP_SUBNORMAL)
+    return to_hex(type, val);
+  char buf[64];
+  auto [ptr, ec] = to_chars(buf, buf + sizeof(buf), fp,
+                            chars_format::scientific);
+  *ptr = '\0';
+  return buf;
 }
 
 static string int_to_readable_float(Type &type, const string &val) {
diff --git a/ir/type.cpp b/ir/type.cpp
index 720ca44d6..f98a881c0 100644
--- a/ir/type.cpp
+++ b/ir/type.cpp
@@ -8,6 +8,8 @@
 #include "util/compiler.h"
 #include <array>
 #include <cassert>
+#include <charconv>
+#include <cstring>
 #include <numeric>
 #include <sstream>
 
@@ -639,7 +641,26 @@ void FloatType::printVal(ostream &os, const State &s, const expr &e) const {
   } else if (f.isInf().isTrue()) {
     os << (f.isFPNegative().isTrue() ? "-oo" : "+oo");
   } else {
-    os << f.float2Real().numeral_string();
+    uint64_t bits = strtoull(e.numeral_string().data(), nullptr, 10);
+    if (fpType == Float) {
+      float fp;
+      memcpy(&fp, &bits, sizeof(fp));
+      char buf[64];
+      auto [p, ec] = to_chars(buf, buf + sizeof(buf), fp,
+                              chars_format::scientific);
+      *p = '\0';
+      os << buf;
+    } else if (fpType == Double) {
+      double fp;
+      memcpy(&fp, &bits, sizeof(fp));
+      char buf[64];
+      auto [p, ec] = to_chars(buf, buf + sizeof(buf), fp,
+                              chars_format::scientific);
+      *p = '\0';
+      os << buf;
+    } else {
+      os << f.float2Real().numeral_string();
+    }
   }
   os << ')';
 }