From 1c8b6cfdb86d746fb25b0cdf8ddd5c7c1f8096cd Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 29 Jul 2026 14:00:42 -0700 Subject: [PATCH] scanner: emit ERROR_TOKEN on I/O failure instead of silent EOF (#10294) `scanner::scan()` was returning `EOF_TOKEN` when the underlying stream had `badbit` set, making a failed read (EIO, ENOSPC, etc.) indistinguishable from a clean end-of-file. Z3 would silently produce no output with exit code 0. ## Root cause `std::istream::gcount()` returns 0 for both normal EOF and I/O failure. `read_char()` returned -1 in both cases, and `scan()`'s `-1` handler unconditionally set `EOF_TOKEN`. ## Fix ### `src/parsers/util/scanner.cpp` Check `m_stream.bad()` in the `-1` case; emit an error message and `ERROR_TOKEN` on failure: ```cpp case static_cast(-1): if (m_stream.bad()) { m_err << "ERROR: I/O failure while reading input stream.\n"; m_state = ERROR_TOKEN; } else { m_state = EOF_TOKEN; } break; ``` ### `src/test/scanner_io.cpp` (new) Regression test (ported from the `io_test` branch) verifying: 1. A good stream scans to completion (`n > 0` tokens). 2. A stream with `badbit` pre-set produces `ERROR_TOKEN` or a non-empty error message rather than silent EOF. ### `src/test/main.cpp` + `src/test/CMakeLists.txt` Register `tst_scanner_io` in the `FOR_EACH_ALL_TEST` macro and add `scanner_io.cpp` to the build. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/parsers/util/scanner.cpp | 7 ++- src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/scanner_io.cpp | 97 ++++++++++++++++++++++++++++++++++++ 4 files changed, 105 insertions(+), 1 deletion(-) create mode 100644 src/test/scanner_io.cpp diff --git a/src/parsers/util/scanner.cpp b/src/parsers/util/scanner.cpp index c30543ba1b..77980cfb13 100644 --- a/src/parsers/util/scanner.cpp +++ b/src/parsers/util/scanner.cpp @@ -483,7 +483,12 @@ scanner::token scanner::scan() { case '#': return read_bv_literal(); case static_cast(-1): - m_state = EOF_TOKEN; + if (m_stream.bad()) { + m_err << "ERROR: I/O failure while reading input stream.\n"; + m_state = ERROR_TOKEN; + } + else + m_state = EOF_TOKEN; break; default: // TODO: use error reporting diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 21d089e85f..61b13aa7c9 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -133,6 +133,7 @@ add_executable(test-z3 scoped_timer.cpp scoped_vector.cpp simple_parser.cpp + scanner_io.cpp simplex.cpp simplifier.cpp sls_test.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 4bba578bf6..4899f656ff 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -73,6 +73,7 @@ X(bit_blaster) \ X(var_subst) \ X(simple_parser) \ + X(scanner_io) \ X(api) \ X(max_rev) \ X(scaled_min) \ diff --git a/src/test/scanner_io.cpp b/src/test/scanner_io.cpp new file mode 100644 index 0000000000..062db33bcf --- /dev/null +++ b/src/test/scanner_io.cpp @@ -0,0 +1,97 @@ +/*++ +Module Name: + + scanner_io.cpp + +Abstract: + + Regression test: a scanner must distinguish a FAILED input stream from an + EXHAUSTED one. + + scanner::read_char() (src/parsers/util/scanner.cpp) does: + + m_stream.read(m_buffer.data()+1, m_buffer.size()-1); + m_bend = 1 + static_cast(m_stream.gcount()); + m_bpos = 1; + ... + } else { + ++m_bpos; + return -1; + } + + std::istream::gcount() returns 0 when the stream is exhausted AND when the + read fails. So on a failed read m_bend == 1 == m_bpos, and read_char() + returns -1 -- the identical value it returns for a cleanly finished file. + bad(), fail() and exceptions() do not appear in that translation unit. + + The same shape is in smt2scanner.cpp, which is the path an input FILE takes + (confirmed under gdb: smt2::scanner::scan -> smt2::parser::operator() -> + parse_smt2_commands -> read_smtlib2_commands). + + Observed on Z3 5.0.0 with the read(2) failing under fault injection: + + errno stdout exit + (none) unsat 0 baseline + EIO (empty) 0 no answer, reported as success + ENOSPC (empty) 0 no answer, reported as success + EINTR unsat 0 recovered -- libstdc++ retries + + Note z3 ALREADY diagnoses a file it cannot OPEN (exit 108, "failed to open + file"). The gap is a file it can open and cannot read. + + No wrong answer was observed: output was empty, never incorrect. + +--*/ +#include "parsers/util/scanner.h" +#include "util/warning.h" +#include +#include + +namespace { + + unsigned drain(scanner & s) { + unsigned n = 0; + while (s.scan() != scanner::EOF_TOKEN && n < 10000) ++n; + return n; + } +} + +void tst_scanner_io() { + // CONTROL -- a good stream must scan to completion, or the test proves + // nothing about the failing case. + { + std::istringstream good("(assert (> x 5))"); + std::ostringstream err; + scanner s(good, err, true /*smt2*/, false); + unsigned n = drain(s); + ENSURE(n > 0); + } + + // THE TEST -- a stream in a failed state must not be reported as a clean + // end of input. Today read_char() returns -1 for both, so the scanner + // reports EOF_TOKEN and the caller sees a valid, empty document. + { + std::istringstream bad("(assert (> x 5))"); + bad.setstate(std::ios::badbit); + std::ostringstream err; + scanner s(bad, err, true /*smt2*/, false); + + // The scanner has an ERROR_TOKEN in its own enum (scanner.h:37). A + // failed stream is exactly what it is for. Accept any signal: the + // error token, a message on `err`, or an exception -- anything but + // silence. + bool signalled = false; + try { + scanner::token t; + unsigned n = 0; + while ((t = s.scan()) != scanner::EOF_TOKEN && n++ < 10000) { + if (t == scanner::ERROR_TOKEN) { signalled = true; break; } + } + signalled = signalled || !err.str().empty(); + } + catch (...) { + signalled = true; + } + ENSURE(signalled); + } +}