mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 19:36:20 +00:00
Code Activity

Fix TPTP frontend soundness holes

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ca1df142-d992-4e45-a8b3-859fa70a5222

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-23 23:08:21 +00:00 • committed by GitHub
parent 4a90d31050
commit 9d34bfe39a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 82 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

83
src/cmd_context/tptp_frontend.cpp
View file

@ -305,6 +305,7 @@ class tptp_parser {
};
implicit_var_scope* m_implicit_scope = nullptr;
std::unordered_set<std::string> m_seen_files;
std::vector<std::unordered_set<std::string>> m_name_filters;
// Table-driven operator dispatch
using op_builder = std::function<expr_ref(expr_ref_vector const&)>;
@ -1181,9 +1182,7 @@ class tptp_parser {
if (let_consts.size() == 1) {
replacer.insert(let_consts[0], value.get());
} else {
// For simultaneous let with tuple value, just bind first var to value
// (full tuple destructuring would require more complex handling)
replacer.insert(let_consts[0], value.get());
throw parse_error("tuple $let destructuring is not supported");
}
expr_ref result(m);
replacer(body, result);
@ -1258,13 +1257,7 @@ class tptp_parser {
// Tuple/list in formula position: [t1, t2, ...] — return first element for simplicity
if (accept(token_kind::lbrack)) {
if (accept(token_kind::rbrack))
return expr_ref(m.mk_const(symbol("$nil"), m_univ), m);
expr_ref first = parse_formula();
while (accept(token_kind::comma))
parse_formula(); // consume remaining elements
expect(token_kind::rbrack, "']'");
return first;
throw parse_error("tuple/list formulas are not supported");
}
std::string n = parse_name();
@ -1458,15 +1451,7 @@ class tptp_parser {
expect(token_kind::rbrack, "']'");
return first;
}
// Not a modal operator — it's a tuple [expr, expr, ...]
// We already consumed '[', so parse as tuple inline
if (accept(token_kind::rbrack))
return expr_ref(m.mk_const(symbol("$nil"), m_univ), m);
expr_ref first = parse_formula();
while (accept(token_kind::comma))
parse_formula(); // consume remaining elements
expect(token_kind::rbrack, "']'");
return first;
throw parse_error("tuple/list formulas are not supported");
}
// Diamond modality: <.>, <name>
@ -1663,9 +1648,17 @@ class tptp_parser {
void parse_include(std::string const& curr_file) {
expect(token_kind::lparen, "'('");
std::string file = parse_name();
std::unordered_set<std::string> selected_names;
bool has_selection = false;
if (accept(token_kind::comma)) {
if (accept(token_kind::lbrack)) {
skip_balanced(token_kind::lbrack, token_kind::rbrack);
has_selection = true;
if (!accept(token_kind::rbrack)) {
do {
selected_names.insert(parse_name());
} while (accept(token_kind::comma));
expect(token_kind::rbrack, "']'");
}
}
else {
skip_annotations_until_rparen();
@ -1673,16 +1666,23 @@ class tptp_parser {
}
expect(token_kind::rparen, "')'");
expect(token_kind::dot, "'.'");
parse_file(resolve_include(curr_file, file));
parse_file(resolve_include(curr_file, file), has_selection ? &selected_names : nullptr);
}
void parse_annotated() {
expect(token_kind::lparen, "'('");
parse_name();
std::string formula_name = parse_name();
expect(token_kind::comma, "','");
std::string role = to_lower(parse_name());
expect(token_kind::comma, "','");
if (!m_name_filters.empty() && !m_name_filters.back().contains(formula_name)) {
skip_annotations_until_rparen();
expect(token_kind::rparen, "')'");
expect(token_kind::dot, "'.'");
return;
}
if (role == "type") {
parse_type_decl_formula();
}
@ -1706,14 +1706,11 @@ class tptp_parser {
f = m.mk_not(f);
}
m_cmd.assert_expr(f);
} catch (z3_exception const& ex) {
// Sort mismatch or other semantic error in this formula — skip it
IF_VERBOSE(2, verbose_stream() << "skipping formula due to: " << ex.what() << "\n");
// Skip to '.' to resync the parser for the next annotated formula
while (!is(token_kind::eof_tok) && !is(token_kind::dot))
next();
if (is(token_kind::dot)) next();
return;
}
catch (z3_exception const& ex) {
std::ostringstream out;
out << "invalid formula '" << formula_name << "': " << ex.what();
throw parse_error(out.str());
}
}
@ -1964,18 +1961,36 @@ public:
}};
}
void parse_input(std::istream& in, std::string const& current_file) {
void parse_input(std::istream& in, std::string const& current_file, std::unordered_set<std::string> const* filter = nullptr) {
// Save parser state so that included files don't clobber the caller's lexer.
std::string saved_input = std::move(m_input);
std::unique_ptr<lexer> saved_lex = std::move(m_lex);
token saved_curr = m_curr;
bool pushed_filter = false;
if (filter) {
m_name_filters.push_back(*filter);
pushed_filter = true;
}
std::ostringstream buf;
buf << in.rdbuf();
m_input = buf.str();
m_lex = std::make_unique<lexer>(m_input);
next();
parse_toplevel(current_file);
try {
parse_toplevel(current_file);
}
catch (...) {
if (pushed_filter)
m_name_filters.pop_back();
m_input = std::move(saved_input);
m_lex = std::move(saved_lex);
m_curr = saved_curr;
throw;
}
if (pushed_filter)
m_name_filters.pop_back();
// Restore caller's parser state.
m_input = std::move(saved_input);
@ -1983,7 +1998,7 @@ public:
m_curr = saved_curr;
}
void parse_file(std::string const& filename) {
void parse_file(std::string const& filename, std::unordered_set<std::string> const* filter = nullptr) {
if (!m_seen_files.insert(filename).second) return;
std::ifstream in(filename);
if (in.fail()) {
@ -1991,7 +2006,7 @@ public:
out << "failed to open file '" << filename << "'";
throw parse_error(out.str());
}
parse_input(in, filename);
parse_input(in, filename, filter);
}
void parse_stream(std::istream& in) {

33
src/test/tptp.cpp
View file

@ -1,3 +1,5 @@
#include <cstdio>
#include <fstream>
#include <string>
#include <vector>
#include <iostream>
@ -34,6 +36,13 @@ static std::string run_tptp(char const* input) {
return out;
}
static void write_file(char const* path, char const* contents) {
std::ofstream out(path);
ENSURE(out.good());
out << contents;
ENSURE(out.good());
}
extern bool g_display_statistics;
extern bool g_display_model;
@ -113,4 +122,28 @@ R"(tff(c1,conjecture, $less($uminus(2),0)).)",
unsigned code = run_tptp("tff(c1,conjecture, $less(1/0,1)).", out, err);
ENSURE(code == ERR_PARSER);
ENSURE(err.find("denominator of rational literal cannot be zero") != std::string::npos);
char const* included = "/tmp/z3-tptp-selected-include.p";
write_file(included,
R"(fof(keep,axiom,p).
fof(poison,axiom,~ p).)");
std::string selected_include =
std::string("include('") + included + R"(',[keep]).
fof(a1,axiom,q).)";
code = run_tptp(selected_include.c_str(), out, err);
ENSURE(code == 0);
ENSURE(out.find("% SZS status Satisfiable") != std::string::npos);
std::remove(included);
code = run_tptp("tff(a1,axiom,$ite($true,0,$true)).", out, err);
ENSURE(code == ERR_PARSER);
ENSURE(err.find("TPTP parse error:") != std::string::npos);
code = run_tptp("fof(a1,axiom,[p(a),q(a)]).", out, err);
ENSURE(code == ERR_PARSER);
ENSURE(err.find("tuple/list formulas are not supported") != std::string::npos);
code = run_tptp("fof(a1,axiom,$let([X: $i, Y: $i], [X,Y] := a, X = Y)).", out, err);
ENSURE(code == ERR_PARSER);
ENSURE(err.find("tuple $let destructuring is not supported") != std::string::npos);
}