mirror of
https://github.com/Z3Prover/z3
synced 2026-08-01 19:54:04 +00:00
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<char>(-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 <nikolaj@cs.stanford.edu>
This commit is contained in:
parent
a3be01b9ca
commit
1c8b6cfdb8
4 changed files with 105 additions and 1 deletions
|
|
@ -483,7 +483,12 @@ scanner::token scanner::scan() {
|
|||
case '#':
|
||||
return read_bv_literal();
|
||||
case static_cast<char>(-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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -73,6 +73,7 @@
|
|||
X(bit_blaster) \
|
||||
X(var_subst) \
|
||||
X(simple_parser) \
|
||||
X(scanner_io) \
|
||||
X(api) \
|
||||
X(max_rev) \
|
||||
X(scaled_min) \
|
||||
|
|
|
|||
97
src/test/scanner_io.cpp
Normal file
97
src/test/scanner_io.cpp
Normal file
|
|
@ -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<unsigned>(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 <istream>
|
||||
#include <sstream>
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue