From 92b4b9e7a728bf95c0971fc0abec718b28534beb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Nov 2017 11:14:00 -0800 Subject: [PATCH] fix error messaging for parsers Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 16 ++++++++++++-- src/api/api_parsers.cpp | 14 +++++++++++- src/api/python/z3/z3.py | 38 +++++++++++++++++++++++++++------ src/cmd_context/cmd_context.cpp | 7 ++++++ src/cmd_context/cmd_context.h | 2 ++ 5 files changed, 67 insertions(+), 10 deletions(-) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 9f5f7dd5d..ac11e1a33 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -286,11 +286,23 @@ extern "C" { scoped_ptr ctx = alloc(cmd_context, false, &m); install_opt_cmds(*ctx.get(), to_optimize_ptr(opt)); ctx->set_ignore_check(true); - if (!parse_smt2_commands(*ctx.get(), s)) { + std::stringstream errstrm; + ctx->set_regular_stream(errstrm); + try { + if (!parse_smt2_commands(*ctx.get(), s)) { + mk_c(c)->m_parser_error_buffer = errstrm.str(); + ctx = nullptr; + SET_ERROR_CODE(Z3_PARSER_ERROR); + return; + } + } + catch (z3_exception& e) { + errstrm << e.msg(); + mk_c(c)->m_parser_error_buffer = errstrm.str(); ctx = nullptr; SET_ERROR_CODE(Z3_PARSER_ERROR); return; - } + } ptr_vector::const_iterator it = ctx->begin_assertions(); ptr_vector::const_iterator end = ctx->end_assertions(); for (; it != end; ++it) { diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 867117984..a7235ef65 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -55,7 +55,19 @@ extern "C" { psort* ps = ctx->pm().mk_psort_cnst(to_sort(sorts[i])); ctx->insert(ctx->pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps)); } - if (!parse_smt2_commands(*ctx.get(), is)) { + std::stringstream errstrm; + ctx->set_regular_stream(errstrm); + try { + if (!parse_smt2_commands(*ctx.get(), is)) { + ctx = nullptr; + mk_c(c)->m_parser_error_buffer = errstrm.str(); + SET_ERROR_CODE(Z3_PARSER_ERROR); + return of_ast(mk_c(c)->m().mk_true()); + } + } + catch (z3_exception& e) { + errstrm << e.msg(); + mk_c(c)->m_parser_error_buffer = errstrm.str(); ctx = nullptr; SET_ERROR_CODE(Z3_PARSER_ERROR); return of_ast(mk_c(c)->m().mk_true()); diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 1f050d3bd..2304491c8 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6668,11 +6668,17 @@ class Fixedpoint(Z3PPObject): def parse_string(self, s): """Parse rules and queries from a string""" - return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx) + try: + return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx) + except Z3Exception as e: + _handle_parse_error(e, self.ctx) def parse_file(self, f): """Parse rules and queries from a file""" - return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx) + try: + return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx) + except Z3Exception as e: + _handle_parse_error(e, self.ctx) def get_rules(self): """retrieve rules that have been added to fixedpoint context""" @@ -6995,15 +7001,21 @@ class Optimize(Z3PPObject): def upper_values(self, obj): if not isinstance(obj, OptimizeObjective): raise Z3Exception("Expecting objective handle returned by maximize/minimize") - return obj.upper_values() + return obj.upper_values() def from_file(self, filename): """Parse assertions and objectives from a file""" - Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename) + try: + Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename) + except Z3Exception as e: + _handle_parse_error(e, self.ctx) def from_string(self, s): """Parse assertions and objectives from a string""" - Z3_optimize_from_string(self.ctx.ref(), self.optimize, s) + try: + Z3_optimize_from_string(self.ctx.ref(), self.optimize, s) + except Z3Exception as e: + _handle_parse_error(e, self.ctx) def assertions(self): """Return an AST vector containing all added constraints.""" @@ -8071,6 +8083,12 @@ def _dict2darray(decls, ctx): i = i + 1 return sz, _names, _decls +def _handle_parse_error(ex, ctx): + msg = Z3_get_parser_error(ctx.ref()) + if msg != "": + raise Z3Exception(msg) + raise ex + def parse_smt2_string(s, sorts={}, decls={}, ctx=None): """Parse a string in SMT 2.0 format using the given sorts and decls. @@ -8089,7 +8107,10 @@ def parse_smt2_string(s, sorts={}, decls={}, ctx=None): ctx = _get_ctx(ctx) ssz, snames, ssorts = _dict2sarray(sorts, ctx) dsz, dnames, ddecls = _dict2darray(decls, ctx) - return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) + try: + return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) + except Z3Exception as e: + _handle_parse_error(e, ctx) def parse_smt2_file(f, sorts={}, decls={}, ctx=None): """Parse a file in SMT 2.0 format using the given sorts and decls. @@ -8099,7 +8120,10 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None): ctx = _get_ctx(ctx) ssz, snames, ssorts = _dict2sarray(sorts, ctx) dsz, dnames, ddecls = _dict2darray(decls, ctx) - return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) + try: + return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) + except Z3Exception as e: + _handle_parse_error(e, ctx) def Interpolant(a,ctx=None): """Create an interpolation operator. diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index a1e7a4745..ec2eea032 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -339,6 +339,13 @@ void ast_object_ref::finalize(cmd_context & ctx) { ctx.m().dec_ref(m_ast); } +void stream_ref::set(std::ostream& out) { + reset(); + m_owner = false; + m_name = "caller-owned"; + m_stream = &out; +} + void stream_ref::set(char const * name) { if (!name) { throw cmd_exception("invalid stream name"); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index b60f590a9..99d6c8284 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -128,6 +128,7 @@ public: stream_ref(std::string n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {} ~stream_ref() { reset(); } void set(char const * name); + void set(std::ostream& strm); void reset(); std::ostream & operator*() { return *m_stream; } char const * name() const { return m_name.c_str(); } @@ -404,6 +405,7 @@ public: void reset_object_refs(); void reset_user_tactics(); void set_regular_stream(char const * name) { m_regular.set(name); } + void set_regular_stream(std::ostream& out) { m_regular.set(out); } void set_diagnostic_stream(char const * name); virtual std::ostream & regular_stream() { return *m_regular; } virtual std::ostream & diagnostic_stream() { return *m_diagnostic; }