diff --git a/regression/smt2_solver/function-applications/function-application2.desc b/regression/smt2_solver/function-applications/function-application2.desc index 06f951172a7..d1a337f6a9c 100644 --- a/regression/smt2_solver/function-applications/function-application2.desc +++ b/regression/smt2_solver/function-applications/function-application2.desc @@ -1,7 +1,7 @@ CORE function-application2.smt2 -^EXIT=134$ +^EXIT=20$ ^SIGNAL=0$ ^\(error "line 5: type mismatch in function definition: expected `\(_ BitVec 16\)' but got `\(_ BitVec 8\)'"\)$ -- diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 598c01c688b..c3524bd4905 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -12,44 +12,63 @@ Author: Daniel Kroening, kroening@kroening.com #include +smt2_parsert::tokent smt2_parsert::next_token() +{ + const auto token = smt2_tokenizert::next_token(); + + if(token == OPEN) + parenthesis_level++; + else if(token == CLOSE) + parenthesis_level--; + + return token; +} + +void smt2_parsert::skip_to_end_of_list() +{ + while(parenthesis_level > 0) + if(next_token() == END_OF_FILE) + return; +} + void smt2_parsert::command_sequence() { exit=false; - while(next_token()==OPEN) + while(!exit) { - if(next_token()!=SYMBOL) + if(peek() == END_OF_FILE) { - error() << "expected symbol as command" << eom; + exit = true; return; } - command(buffer); + if(next_token() != OPEN) + throw error("command must start with '('"); - if(exit) - return; + if(next_token() != SYMBOL) + { + ignore_command(); + throw error("expected symbol as command"); + } + + command(buffer); switch(next_token()) { case END_OF_FILE: - error() << "expected closing parenthesis at end of command," - " but got EOF" << eom; - return; + throw error( + "expected closing parenthesis at end of command," + " but got EOF"); case CLOSE: // what we expect break; default: - error() << "expected end of command" << eom; - return; + throw error("expected ')' at end of command"); } } - - if(token!=END_OF_FILE) - { - error() << "unexpected token in command sequence" << eom; - } } void smt2_parsert::ignore_command() @@ -73,14 +92,14 @@ void smt2_parsert::ignore_command() break; case END_OF_FILE: - error() << "unexpected EOF in command" << eom; - return; + throw error("unexpected EOF in command"); default: next_token(); } } } + exprt::operandst smt2_parsert::operands() { exprt::operandst result; @@ -126,10 +145,7 @@ irep_idt smt2_parsert::rename_id(const irep_idt &id) const exprt smt2_parsert::let_expression() { if(next_token()!=OPEN) - { - error() << "expected bindings after let" << eom; - return nil_exprt(); - } + throw error("expected bindings after let"); std::vector> bindings; @@ -138,10 +154,7 @@ exprt smt2_parsert::let_expression() next_token(); if(next_token()!=SYMBOL) - { - error() << "expected symbol in binding" << eom; - return nil_exprt(); - } + throw error("expected symbol in binding"); irep_idt identifier=buffer; @@ -149,20 +162,14 @@ exprt smt2_parsert::let_expression() exprt value=expression(); if(next_token()!=CLOSE) - { - error() << "expected ')' after value in binding" << eom; - return nil_exprt(); - } + throw error("expected ')' after value in binding"); bindings.push_back( std::pair(identifier, value)); } if(next_token()!=CLOSE) - { - error() << "expected ')' at end of bindings" << eom; - return nil_exprt(); - } + throw error("expected ')' at end of bindings"); // save the renaming map renaming_mapt old_renaming_map=renaming_map; @@ -180,10 +187,7 @@ exprt smt2_parsert::let_expression() exprt expr=expression(); if(next_token()!=CLOSE) - { - error() << "expected ')' after let" << eom; - return nil_exprt(); - } + throw error("expected ')' after let"); exprt result=expr; @@ -211,8 +215,9 @@ exprt smt2_parsert::quantifier_expression(irep_idt id) { if(next_token()!=OPEN) { - error() << "expected bindings after " << id << eom; - return nil_exprt(); + std::ostringstream msg; + msg << "expected bindings after " << id; + throw error(msg.str()); } std::vector bindings; @@ -222,29 +227,20 @@ exprt smt2_parsert::quantifier_expression(irep_idt id) next_token(); if(next_token()!=SYMBOL) - { - error() << "expected symbol in binding" << eom; - return nil_exprt(); - } + throw error("expected symbol in binding"); irep_idt identifier=buffer; typet type=sort(); if(next_token()!=CLOSE) - { - error() << "expected ')' after sort in binding" << eom; - return nil_exprt(); - } + throw error("expected ')' after sort in binding"); bindings.push_back(symbol_exprt(identifier, type)); } if(next_token()!=CLOSE) - { - error() << "expected ')' at end of bindings" << eom; - return nil_exprt(); - } + throw error("expected ')' at end of bindings"); // go forwards, add to id_map for(const auto &b : bindings) @@ -258,8 +254,9 @@ exprt smt2_parsert::quantifier_expression(irep_idt id) if(next_token()!=CLOSE) { - error() << "expected ')' after " << id << eom; - return nil_exprt(); + std::ostringstream msg; + msg << "expected ')' after " << id; + throw error(msg.str()); } exprt result=expr; @@ -289,18 +286,12 @@ exprt smt2_parsert::function_application( // check the arguments if(op.size()!=f.type.variables().size()) - { - error() << "wrong number of arguments for function" << eom; - return nil_exprt(); - } + throw error("wrong number of arguments for function"); for(std::size_t i=0; isecond.type); } - error() << "2 unknown symbol " << id << eom; - return nil_exprt(); + std::ostringstream msg; + msg << "2 unknown symbol " << id; + throw error(msg.str()); } } break; @@ -695,53 +645,35 @@ exprt smt2_parsert::function_application() { // indexed identifier if(next_token()!=SYMBOL) - { - error() << "expected symbol after '_'" << eom; - return nil_exprt(); - } + throw error("expected symbol after '_'"); irep_idt id=buffer; // hash it if(id=="extract") { if(next_token()!=NUMERAL) - { - error() << "expected numeral after extract" << eom; - return nil_exprt(); - } + throw error("expected numeral after extract"); auto upper=std::stoll(buffer); if(next_token()!=NUMERAL) - { - error() << "expected two numerals after extract" << eom; - return nil_exprt(); - } + throw error("expected two numerals after extract"); auto lower=std::stoll(buffer); if(next_token()!=CLOSE) - { - error() << "expected ')' after extract" << eom; - return nil_exprt(); - } + throw error("expected ')' after extract"); auto op=operands(); if(op.size()!=1) - { - error() << "extract takes one operand" << eom; - return nil_exprt(); - } + throw error("extract takes one operand"); auto upper_e=from_integer(upper, integer_typet()); auto lower_e=from_integer(lower, integer_typet()); if(uppersecond.type); - error() << "1 unknown symbol " << identifier << eom; - return nil_exprt(); + std::ostringstream msg; + msg << "1 unknown symbol " << identifier; + throw error(msg.str()); } } @@ -910,12 +838,10 @@ exprt smt2_parsert::expression() return function_application(); case END_OF_FILE: - error() << "EOF in an expression" << eom; - return nil_exprt(); + throw error("EOF in an expression"); default: - error() << "unexpected token in an expression" << eom; - return nil_exprt(); + throw error("unexpected token in an expression"); } } @@ -932,49 +858,39 @@ typet smt2_parsert::sort() return real_typet(); else { - error() << "unexpected sort: `" << buffer << '\'' << eom; - return nil_typet(); + std::ostringstream msg; + msg << "unexpected sort: `" << buffer << '\''; + throw error(msg.str()); } case OPEN: if(next_token()!=SYMBOL) - { - error() << "expected symbol after '(' in a sort " << eom; - return nil_typet(); - } + throw error("expected symbol after '(' in a sort "); if(buffer=="_") { // indexed identifier if(next_token()!=SYMBOL) - { - error() << "expected symbol after '_' in a sort" << eom; - return nil_typet(); - } + throw error("expected symbol after '_' in a sort"); if(buffer=="BitVec") { if(next_token()!=NUMERAL) - { - error() << "expected numeral as bit-width" << eom; - return nil_typet(); - } + throw error("expected numeral as bit-width"); auto width=std::stoll(buffer); // eat the ')' if(next_token()!=CLOSE) - { - error() << "expected ')' at end of sort" << eom; - return nil_typet(); - } + throw error("expected ')' at end of sort"); return unsignedbv_typet(width); } else { - error() << "unexpected sort: `" << buffer << '\'' << eom; - return nil_typet(); + std::ostringstream msg; + msg << "unexpected sort: `" << buffer << '\''; + throw error(msg.str()); } } else if(buffer == "Array") @@ -985,10 +901,7 @@ typet smt2_parsert::sort() // eat the ')' if(next_token() != CLOSE) - { - error() << "expected ')' at end of Array sort" << eom; - return nil_typet(); - } + throw error("expected ')' at end of Array sort"); // we can turn arrays that map an unsigned bitvector type // to something else into our 'array_typet' @@ -998,30 +911,26 @@ typet smt2_parsert::sort() return array_typet(range, size); } else - { - error() << "unsupported array sort" << eom; - return nil_typet(); - } + throw error("unsupported array sort"); } else { - error() << "unexpected sort: `" << buffer << '\'' << eom; - return nil_typet(); + std::ostringstream msg; + msg << "unexpected sort: `" << buffer << '\''; + throw error(msg.str()); } default: - error() << "unexpected token in a sort " << buffer << eom; - return nil_typet(); + std::ostringstream msg; + msg << "unexpected token in a sort: `" << buffer << '\''; + throw error(msg.str()); } } typet smt2_parsert::function_signature_definition() { if(next_token()!=OPEN) - { - error() << "expected '(' at beginning of signature" << eom; - return nil_typet(); - } + throw error("expected '(' at beginning of signature"); if(peek()==CLOSE) { @@ -1034,16 +943,10 @@ typet smt2_parsert::function_signature_definition() while(peek()!=CLOSE) { if(next_token()!=OPEN) - { - error() << "expected '(' at beginning of parameter" << eom; - return nil_typet(); - } + throw error("expected '(' at beginning of parameter"); if(next_token()!=SYMBOL) - { - error() << "expected symbol in parameter" << eom; - return nil_typet(); - } + throw error("expected symbol in parameter"); mathematical_function_typet::variablet var; std::string id=buffer; @@ -1056,10 +959,7 @@ typet smt2_parsert::function_signature_definition() entry.definition=nil_exprt(); if(next_token()!=CLOSE) - { - error() << "expected ')' at end of parameter" << eom; - return nil_typet(); - } + throw error("expected ')' at end of parameter"); } next_token(); // eat the ')' @@ -1072,10 +972,7 @@ typet smt2_parsert::function_signature_definition() typet smt2_parsert::function_signature_declaration() { if(next_token()!=OPEN) - { - error() << "expected '(' at beginning of signature" << eom; - return nil_typet(); - } + throw error("expected '(' at beginning of signature"); if(peek()==CLOSE) { @@ -1088,26 +985,17 @@ typet smt2_parsert::function_signature_declaration() while(peek()!=CLOSE) { if(next_token()!=OPEN) - { - error() << "expected '(' at beginning of parameter" << eom; - return nil_typet(); - } + throw error("expected '(' at beginning of parameter"); if(next_token()!=SYMBOL) - { - error() << "expected symbol in parameter" << eom; - return nil_typet(); - } + throw error("expected symbol in parameter"); mathematical_function_typet::variablet var; var.type()=sort(); domain.push_back(var); if(next_token()!=CLOSE) - { - error() << "expected ')' at end of parameter" << eom; - return nil_typet(); - } + throw error("expected ')' at end of parameter"); } next_token(); // eat the ')' @@ -1125,69 +1013,60 @@ void smt2_parsert::command(const std::string &c) // accepted by Z3 and CVC4 if(next_token()!=SYMBOL) { - error() << "expected a symbol after " << c << eom; - ignore_command(); - return; + std::ostringstream msg; + msg << "expected a symbol after `" << c << '\''; + throw error(msg.str()); } - irep_idt id=buffer; + irep_idt id = buffer; + auto type = sort(); if(id_map.find(id)!=id_map.end()) { - error() << "identifier `" << id << "' defined twice" << eom; - ignore_command(); - return; + std::ostringstream msg; + msg << "identifier `" << id << "' defined twice"; + throw error(msg.str()); } auto &entry = id_map[id]; - entry.type = sort(); + entry.type = type; entry.definition = nil_exprt(); } else if(c=="declare-fun") { if(next_token()!=SYMBOL) - { - error() << "expected a symbol after declare-fun" << eom; - ignore_command(); - return; - } + throw error("expected a symbol after declare-fun"); irep_idt id=buffer; + auto type = function_signature_declaration(); if(id_map.find(id)!=id_map.end()) { - error() << "identifier `" << id << "' defined twice" << eom; - ignore_command(); - return; + std::ostringstream msg; + msg << "identifier `" << id << "' defined twice"; + throw error(msg.str()); } - auto &entry=id_map[id]; - entry.type=function_signature_declaration(); - entry.definition=nil_exprt(); + auto &entry = id_map[id]; + entry.type = type; + entry.definition = nil_exprt(); } else if(c=="define-fun") { if(next_token()!=SYMBOL) - { - error() << "expected a symbol after define-fun" << eom; - ignore_command(); - return; - } + throw error("expected a symbol after define-fun"); const irep_idt id=buffer; if(id_map.find(id)!=id_map.end()) { - error() << "identifier `" << id << "' defined twice" << eom; - ignore_command(); - return; + std::ostringstream msg; + msg << "identifier `" << id << "' defined twice"; + throw error(msg.str()); } - // create the entry - id_map[id]; - - auto signature=function_signature_definition(); - exprt body=expression(); + const auto signature = function_signature_definition(); + const auto body = expression(); // check type of body if(signature.id() == ID_mathematical_function) @@ -1195,21 +1074,23 @@ void smt2_parsert::command(const std::string &c) const auto &f_signature = to_mathematical_function_type(signature); if(body.type() != f_signature.codomain()) { - error() << "type mismatch in function definition: expected `" - << smt2_format(f_signature.codomain()) << "' but got `" - << smt2_format(body.type()) << '\'' << eom; - return; + std::ostringstream msg; + msg << "type mismatch in function definition: expected `" + << smt2_format(f_signature.codomain()) << "' but got `" + << smt2_format(body.type()) << '\''; + throw error(msg.str()); } } else if(body.type() != signature) { - error() << "type mismatch in function definition: expected `" - << smt2_format(signature) << "' but got `" - << smt2_format(body.type()) << '\'' << eom; - return; + std::ostringstream msg; + msg << "type mismatch in function definition: expected `" + << smt2_format(signature) << "' but got `" << smt2_format(body.type()) + << '\''; + throw error(msg.str()); } - // set up the entry + // create the entry auto &entry=id_map[id]; entry.type=signature; entry.definition=body; diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 1c787bc93d3..8f5d1a2010f 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -18,16 +18,15 @@ Author: Daniel Kroening, kroening@kroening.com class smt2_parsert:public smt2_tokenizert { public: - explicit smt2_parsert(std::istream &_in): - smt2_tokenizert(_in), - exit(false) + explicit smt2_parsert(std::istream &_in) + : smt2_tokenizert(_in), exit(false), parenthesis_level(0) { } bool parse() override { command_sequence(); - return !ok; + return false; } struct idt @@ -43,8 +42,16 @@ class smt2_parsert:public smt2_tokenizert using id_mapt=std::map; id_mapt id_map; -protected: bool exit; + + /// This skips tokens until all bracketed expressions are closed + void skip_to_end_of_list(); + +protected: + // we override next_token to track the parenthesis level + std::size_t parenthesis_level; + tokent next_token() override; + void command_sequence(); virtual void command(const std::string &); diff --git a/src/solvers/smt2/smt2_solver.cpp b/src/solvers/smt2/smt2_solver.cpp index 73c274551d3..bc493dd831c 100644 --- a/src/solvers/smt2/smt2_solver.cpp +++ b/src/solvers/smt2/smt2_solver.cpp @@ -127,11 +127,10 @@ void smt2_solvert::expand_function_applications(exprt &expr) void smt2_solvert::command(const std::string &c) { - try { - if(c=="assert") + if(c == "assert") { - exprt e=expression(); + exprt e = expression(); if(e.is_not_nil()) { expand_function_applications(e); @@ -139,7 +138,7 @@ void smt2_solvert::command(const std::string &c) solver.set_to_true(e); } } - else if(c=="check-sat") + else if(c == "check-sat") { switch(solver()) { @@ -158,14 +157,14 @@ void smt2_solvert::command(const std::string &c) status = NOT_SOLVED; } } - else if(c=="check-sat-assuming") + else if(c == "check-sat-assuming") { - std::cout << "not yet implemented\n"; + throw error("not yet implemented"); } - else if(c=="display") + else if(c == "display") { // this is a command that Z3 appears to implement - exprt e=expression(); + exprt e = expression(); if(e.is_not_nil()) std::cout << smt2_format(e) << '\n'; } @@ -174,16 +173,16 @@ void smt2_solvert::command(const std::string &c) std::vector ops; if(next_token() != OPEN) - throw "get-value expects list as argument"; + throw error("get-value expects list as argument"); while(peek() != CLOSE && peek() != END_OF_FILE) ops.push_back(expression()); // any term if(next_token() != CLOSE) - throw "get-value expects ')' at end of list"; + throw error("get-value expects ')' at end of list"); if(status != SAT) - throw "model is not available"; + throw error("model is not available"); std::vector values; values.reserve(ops.size()); @@ -191,14 +190,14 @@ void smt2_solvert::command(const std::string &c) for(const auto &op : ops) { if(op.id() != ID_symbol) - throw "get-value expects symbol"; + throw error("get-value expects symbol"); const auto &identifier = to_symbol_expr(op).get_identifier(); const auto id_map_it = id_map.find(identifier); if(id_map_it == id_map.end()) - throw "unexpected symbol " + id2string(identifier); + throw error("unexpected symbol " + id2string(identifier)); exprt value; @@ -208,7 +207,7 @@ void smt2_solvert::command(const std::string &c) value = solver.get(id_map_it->second.definition); if(value.is_nil()) - throw "no value for " + id2string(identifier); + throw error("no value for " + id2string(identifier)); values.push_back(value); } @@ -226,19 +225,19 @@ void smt2_solvert::command(const std::string &c) std::cout << ")\n"; } - else if(c=="simplify") + else if(c == "simplify") { // this is a command that Z3 appears to implement - exprt e=expression(); + exprt e = expression(); if(e.is_not_nil()) { const symbol_tablet symbol_table; const namespacet ns(symbol_table); - exprt e_simplified=simplify_expr(e, ns); + exprt e_simplified = simplify_expr(e, ns); std::cout << smt2_format(e) << '\n'; } } - #if 0 +#if 0 // TODO: | ( declare-const hsymboli hsorti ) | ( declare-datatype hsymboli hdatatype_deci) @@ -265,18 +264,10 @@ void smt2_solvert::command(const std::string &c) | ( reset-assertions ) | ( set-info hattributei ) | ( set-option hoptioni ) - #endif +#endif else smt2_parsert::command(c); } - catch(const char *error) - { - std::cout << "error: " << error << '\n'; - } - catch(const std::string &error) - { - std::cout << "error: " << error << '\n'; - } } class smt2_message_handlert : public message_handlert @@ -324,10 +315,25 @@ int solver(std::istream &in) smt2_solvert smt2_solver(in, boolbv); smt2_solver.set_message_handler(message_handler); + bool error_found = false; - smt2_solver.parse(); + while(!smt2_solver.exit) + { + try + { + smt2_solver.parse(); + } + catch(const smt2_solvert::smt2_errort &error) + { + smt2_solver.skip_to_end_of_list(); + error_found = true; + messaget message(message_handler); + message.error().source_location.set_line(error.get_line_no()); + message.error() << error.what() << messaget::eom; + } + } - if(!smt2_solver) + if(error_found) return 20; else return 0; diff --git a/src/solvers/smt2/smt2_tokenizer.cpp b/src/solvers/smt2/smt2_tokenizer.cpp index d96db803bec..c2fe95448d3 100644 --- a/src/solvers/smt2/smt2_tokenizer.cpp +++ b/src/solvers/smt2/smt2_tokenizer.cpp @@ -159,8 +159,7 @@ smt2_tokenizert::tokent smt2_tokenizert::get_quoted_symbol() } // Hmpf. Eof before end of quoted symbol. This is an error. - error() << "EOF within quoted symbol" << eom; - return ERROR; + throw error("EOF within quoted symbol"); } smt2_tokenizert::tokent smt2_tokenizert::get_string_literal() @@ -191,15 +190,21 @@ smt2_tokenizert::tokent smt2_tokenizert::get_string_literal() } // Hmpf. Eof before end of string literal. This is an error. - error() << "EOF within string literal" << eom; - return ERROR; + throw error("EOF within string literal"); } smt2_tokenizert::tokent smt2_tokenizert::next_token() { if(peeked) - return peeked=false, token; + peeked = false; + else + get_token_from_stream(); + + return token; +} +void smt2_tokenizert::get_token_from_stream() +{ char ch; while(in->get(ch)) @@ -231,60 +236,68 @@ smt2_tokenizert::tokent smt2_tokenizert::next_token() case '(': // produce sub-expression - return token=OPEN; + token = OPEN; + return; case ')': // done with sub-expression - return token=CLOSE; + token = CLOSE; + return; case '|': // quoted symbol - return token=get_quoted_symbol(); + token = get_quoted_symbol(); + return; case '"': // string literal - return token=get_string_literal(); + token = get_string_literal(); + return; case ':': // keyword - return token=get_simple_symbol(); + token = get_simple_symbol(); + return; case '#': if(in->get(ch)) { if(ch=='b') - return token=get_bin_numeral(); + { + token = get_bin_numeral(); + return; + } else if(ch=='x') - return token=get_hex_numeral(); - else { - error() << "unknown numeral token" << eom; - return token=ERROR; + token = get_hex_numeral(); + return; } + else + throw error("unknown numeral token"); } else - { - error() << "unexpected EOF in numeral token" << eom; - return token=ERROR; - } + throw error("unexpected EOF in numeral token"); break; default: // likely a simple symbol or a numeral if(isdigit(ch)) { in->unget(); - return token=get_decimal_numeral(); + token = get_decimal_numeral(); + return; } else if(is_simple_symbol_character(ch)) { in->unget(); - return token=get_simple_symbol(); + token = get_simple_symbol(); + return; } else { // illegal character, error - error() << "unexpected character `" << ch << '\'' << eom; - return token=ERROR; + std::ostringstream msg; + msg << "unexpected character `" << ch << '\''; + throw error(msg.str()); } } } - return token=END_OF_FILE; + token = END_OF_FILE; } diff --git a/src/solvers/smt2/smt2_tokenizer.h b/src/solvers/smt2/smt2_tokenizer.h index 328c5d8fcb1..62016c24367 100644 --- a/src/solvers/smt2/smt2_tokenizer.h +++ b/src/solvers/smt2/smt2_tokenizer.h @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_SMT2_SMT2_TOKENIZER_H #define CPROVER_SOLVERS_SMT2_SMT2_TOKENIZER_H +#include #include #include @@ -16,26 +17,55 @@ Author: Daniel Kroening, kroening@kroening.com class smt2_tokenizert:public parsert { public: - explicit smt2_tokenizert(std::istream &_in): - ok(true), peeked(false), token(NONE) + explicit smt2_tokenizert(std::istream &_in) : peeked(false), token(NONE) { in=&_in; line_no=1; } - operator bool() + class smt2_errort : public cprover_exception_baset { - return ok; - } + public: + smt2_errort(const std::string &_message, unsigned _line_no) + : message(_message), line_no(_line_no) + { + } + + smt2_errort(std::string &&_message, unsigned _line_no) + : message(std::move(_message)), line_no(_line_no) + { + } + + std::string what() const override + { + return message; + } + + unsigned get_line_no() const + { + return line_no; + } + + protected: + const std::string message; + unsigned line_no; + }; protected: std::string buffer; - bool ok, peeked; - using tokent=enum { NONE, END_OF_FILE, ERROR, STRING_LITERAL, - NUMERAL, SYMBOL, OPEN, CLOSE }; + bool peeked; + using tokent = enum { + NONE, + END_OF_FILE, + STRING_LITERAL, + NUMERAL, + SYMBOL, + OPEN, + CLOSE + }; tokent token; - tokent next_token(); + virtual tokent next_token(); tokent peek() { @@ -43,17 +73,24 @@ class smt2_tokenizert:public parsert return token; else { - next_token(); + get_token_from_stream(); peeked=true; return token; } } - mstreamt &error() + /// skip any tokens until all parentheses are closed + /// or the end of file is reached + void skip_to_end_of_list(); + + smt2_errort error(std::string &&message) { - ok=false; - messaget::error().source_location.set_line(line_no); - return messaget::error(); + return smt2_errort(std::move(message), line_no); + } + + smt2_errort error(const std::ostringstream &message) + { + return smt2_errort(message.str(), line_no); } private: @@ -64,6 +101,9 @@ class smt2_tokenizert:public parsert tokent get_quoted_symbol(); tokent get_string_literal(); static bool is_simple_symbol_character(char); + + /// read a token from the input stream and store it in 'token' + void get_token_from_stream(); }; #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H diff --git a/src/solvers/smt2/smt2irep.cpp b/src/solvers/smt2/smt2irep.cpp index baf77e5175d..4311cec1b81 100644 --- a/src/solvers/smt2/smt2irep.cpp +++ b/src/solvers/smt2/smt2irep.cpp @@ -33,60 +33,65 @@ class smt2irept:public smt2_tokenizert bool smt2irept::parse() { - std::stack stack; - result.clear(); - - while(true) + try { - switch(next_token()) + std::stack stack; + result.clear(); + + while(true) { - case END_OF_FILE: - error() << "unexpected end of file" << eom; - return true; - - case STRING_LITERAL: - case NUMERAL: - case SYMBOL: - if(stack.empty()) + switch(next_token()) { - result=irept(buffer); - return false; // all done! - } - else - stack.top().get_sub().push_back(irept(buffer)); - break; - - case OPEN: // '(' - // produce sub-irep - stack.push(irept()); - break; - - case CLOSE: // ')' - // done with sub-irep - if(stack.empty()) - { - error() << "unexpected ')'" << eom; - return true; - } - else - { - irept tmp=stack.top(); - stack.pop(); + case END_OF_FILE: + throw error("unexpected end of file"); + case STRING_LITERAL: + case NUMERAL: + case SYMBOL: if(stack.empty()) { - result=tmp; + result = irept(buffer); return false; // all done! } + else + stack.top().get_sub().push_back(irept(buffer)); + break; - stack.top().get_sub().push_back(tmp); + case OPEN: // '(' + // produce sub-irep + stack.push(irept()); break; - } - default: - return true; + case CLOSE: // ')' + // done with sub-irep + if(stack.empty()) + throw error("unexpected ')'"); + else + { + irept tmp = stack.top(); + stack.pop(); + + if(stack.empty()) + { + result = tmp; + return false; // all done! + } + + stack.top().get_sub().push_back(tmp); + break; + } + + default: + throw error("unexpected token"); + } } } + catch(const smt2_errort &e) + { + messaget::error().source_location.set_line(e.get_line_no()); + messaget::error() << e.what() << eom; + return true; + } } irept smt2irep(std::istream &in)