Fix unsigned overflow issue

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
 ===========

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

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

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()

tests/parser-overflow-declare-sort.eo

@@ -0,0 +1 @@
+(declare-sort TooBig 4294967296)