From 7fb65c4e88524cec193f4a50f9d79c4d74a721ad Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 27 Mar 2026 09:47:37 -0500
Subject: [PATCH 1/2] Fix unsigned overflow issue

---
 src/expr_parser.cpp                   | 41 ++++++++++++++++++++++++---
 tests/CMakeLists.txt                  | 16 +++++++++++
 tests/expect_error.cmake              | 18 ++++++++++++
 tests/parser-overflow-declare-sort.eo |  1 +
 4 files changed, 72 insertions(+), 4 deletions(-)
 create mode 100644 tests/expect_error.cmake
 create mode 100644 tests/parser-overflow-declare-sort.eo

diff --git a/src/expr_parser.cpp b/src/expr_parser.cpp
index 6b266974..86fce4b6 100644
--- a/src/expr_parser.cpp
+++ b/src/expr_parser.cpp
@@ -18,6 +18,35 @@
 
 namespace ethos {
 
+namespace {
+
+bool stringToUnsigned(const std::string& str,
+                      uint32_t& result,
+                      std::ostream* os = nullptr)
+{
+  if (str.empty() || str.find_first_not_of("0123456789") != std::string::npos)
+  {
+    if (os != nullptr)
+    {
+      (*os) << "String is not a numeral.";
+    }
+    return false;
+  }
+  Integer parsed(str);
+  if (!parsed.fitsUnsignedInt())
+  {
+    if (os != nullptr)
+    {
+      (*os) << "Numerals must fit into 32-bit unsigned integers.";
+    }
+    return false;
+  }
+  result = parsed.toUnsignedInt();
+  return true;
+}
+
+}  // namespace
+
 /**
  * Definition of state identifiers when parsing terms
  *
@@ -924,10 +953,14 @@ uint32_t ExprParser::tokenStrToUnsigned()
   {
     d_lex.parseError("Numeral with leading zeroes are forbidden");
   }
-  uint32_t result;
-  std::stringstream ss;
-  ss << d_lex.tokenStr();
-  ss >> result;
+  uint32_t result = 0;
+  if (!stringToUnsigned(token, result))
+  {
+    std::stringstream ss;
+    ss << "Failed to parse numeral. ";
+    stringToUnsigned(token, result, &ss);
+    d_lex.parseError(ss.str());
+  }
   return result;
 }
 
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index c9665ca0..68b9058a 100644
--- a/tests/CMakeLists.txt
+++ b/tests/CMakeLists.txt
@@ -180,7 +180,23 @@ macro(ethos_test file)
   set_tests_properties(${file} PROPERTIES TIMEOUT 40)
 endmacro()
 
+macro(ethos_fail_test file regex)
+  add_test(
+    NAME ${file}
+    COMMAND
+      ${CMAKE_COMMAND}
+      "-DTEST_BINARY=$<TARGET_FILE:ethos>"
+      "-DTEST_FILE=${CMAKE_CURRENT_LIST_DIR}/${file}"
+      "-DTEST_WORKDIR=${CMAKE_SOURCE_DIR}"
+      "-DEXPECT_REGEX=${regex}"
+      -P ${CMAKE_CURRENT_LIST_DIR}/expect_error.cmake
+  )
+  set_tests_properties(${file} PROPERTIES TIMEOUT 40)
+endmacro()
+
 foreach(file ${ethos_test_file_list})
   ethos_test(${file})
 endforeach()
 
+ethos_fail_test(parser-overflow-declare-sort.eo
+                "Numerals must fit into 32-bit unsigned integers")
diff --git a/tests/expect_error.cmake b/tests/expect_error.cmake
new file mode 100644
index 00000000..9b143900
--- /dev/null
+++ b/tests/expect_error.cmake
@@ -0,0 +1,18 @@
+execute_process(
+  COMMAND "${TEST_BINARY}" "${TEST_FILE}"
+  WORKING_DIRECTORY "${TEST_WORKDIR}"
+  RESULT_VARIABLE test_result
+  OUTPUT_VARIABLE test_stdout
+  ERROR_VARIABLE test_stderr
+)
+
+set(test_output "${test_stdout}${test_stderr}")
+
+if("${test_result}" STREQUAL "0")
+  message(FATAL_ERROR "Expected ${TEST_FILE} to fail, but it succeeded.")
+endif()
+
+if(NOT test_output MATCHES "${EXPECT_REGEX}")
+  message(FATAL_ERROR
+    "Expected output matching `${EXPECT_REGEX}` for ${TEST_FILE}, got:\n${test_output}")
+endif()
diff --git a/tests/parser-overflow-declare-sort.eo b/tests/parser-overflow-declare-sort.eo
new file mode 100644
index 00000000..04f1f3d9
--- /dev/null
+++ b/tests/parser-overflow-declare-sort.eo
@@ -0,0 +1 @@
+(declare-sort TooBig 4294967296)

From 5a55426a8412bb18d3535a827a3adab83054a498 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 27 Mar 2026 10:00:22 -0500
Subject: [PATCH 2/2] News

---
 NEWS.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/NEWS.md b/NEWS.md
index e29f9f8b..d085f167 100644
--- a/NEWS.md
+++ b/NEWS.md
@@ -9,6 +9,8 @@ ethos 0.2.3 prerelease
 - The command `declare-sort` is now allowed in proof files.
 - Fixes a bug where the character code point `\u{30000}` was incorrectly
   treated as a valid code point.
+- Fixes issue in the parser which did not guard for overflow of 32 bit unsigned
+  values.
 
 ethos 0.2.2
 ===========