From: Christopher L. Conway Date: Thu, 18 Feb 2010 23:24:26 +0000 (+0000) Subject: Adding --no-checking option to disable semantic checks in parser X-Git-Tag: cvc5-1.0.0~9244 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9f8f4ae9ef9d9d79973b77b6c61af4c5db034841;p=cvc5.git Adding --no-checking option to disable semantic checks in parser --- diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index ff9957c5c..8ace8e778 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -58,7 +58,8 @@ enum OptionValue { SMTCOMP, STATS, SEGV_NOSPIN, - PARSE_ONLY + PARSE_ONLY, + NO_CHECKING };/* enum OptionValue */ // FIXME add a comment here describing the option array @@ -74,7 +75,8 @@ static struct option cmdlineOptions[] = { { "smtcomp" , no_argument , NULL, SMTCOMP }, { "stats" , no_argument , NULL, STATS }, { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }, - { "parse-only" , no_argument , NULL, PARSE_ONLY } + { "parse-only" , no_argument , NULL, PARSE_ONLY }, + { "no-checking", no_argument , NULL, NO_CHECKING } };/* if you add things to the above, please remember to update usage.h! */ /** Full argv[0] */ @@ -176,6 +178,10 @@ throw(OptionException) { opts->parseOnly = true; break; + case NO_CHECKING: + opts->semanticChecks = false; + break; + case '?': throw OptionException(string("can't understand option"));// + argv[optind - 1] + "'"); diff --git a/src/main/main.cpp b/src/main/main.cpp index d0ad72fc4..e54bbb5f6 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -111,6 +111,10 @@ int main(int argc, char *argv[]) { parser = Parser::getNewParser(&exprMgr, options.lang, argv[firstArgIndex]); } + if(!options.semanticChecks) { + parser->disableChecks(); + } + // Parse and execute commands until we are done Command* cmd; while((cmd = parser->parseNextCommand())) { diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index af3ce9d1b..49a2f7362 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -37,19 +37,20 @@ namespace CVC4 { namespace parser { AntlrParser::AntlrParser(const antlr::ParserSharedInputState& state, int k) : - antlr::LLkParser(state, k) { + antlr::LLkParser(state, k), d_checksEnabled(true) { } AntlrParser::AntlrParser(antlr::TokenBuffer& tokenBuf, int k) : - antlr::LLkParser(tokenBuf, k) { + antlr::LLkParser(tokenBuf, k), d_checksEnabled(true) { } AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : - antlr::LLkParser(lexer, k) { + antlr::LLkParser(lexer, k), d_checksEnabled(true) { } Expr AntlrParser::getSymbol(std::string name, SymbolType type) { Assert( isDeclared(name,type) ); + switch( type ) { case SYM_VARIABLE: // Functions share var namespace case SYM_FUNCTION: @@ -295,41 +296,48 @@ void AntlrParser::parseError(string message) LT(1).get()->getColumn()); } -bool AntlrParser::checkDeclaration(string varName, +void AntlrParser::checkDeclaration(string varName, DeclarationCheck check, SymbolType type) throw (antlr::SemanticException) { + if(!d_checksEnabled) { + return; + } + switch(check) { case CHECK_DECLARED: if( !isDeclared(varName, type) ) { parseError("Symbol " + varName + " not declared"); - } else { - return true; } + break; + case CHECK_UNDECLARED: if( isDeclared(varName, type) ) { parseError("Symbol " + varName + " previously declared"); - } else { - return true; } + break; + case CHECK_NONE: - return true; + break; + default: Unhandled("Unknown check type!"); } } -bool AntlrParser::checkFunction(string name) +void AntlrParser::checkFunction(string name) throw (antlr::SemanticException) { - if( !isFunction(name) ) { + if( d_checksEnabled && !isFunction(name) ) { parseError("Expecting function symbol, found '" + name + "'"); } - - return true; } -bool AntlrParser::checkArity(Kind kind, unsigned int numArgs) +void AntlrParser::checkArity(Kind kind, unsigned int numArgs) throw (antlr::SemanticException) { + if(!d_checksEnabled) { + return; + } + unsigned int min = minArity(kind); unsigned int max = maxArity(kind); @@ -345,8 +353,16 @@ bool AntlrParser::checkArity(Kind kind, unsigned int numArgs) ss << "found " << numArgs; parseError(ss.str()); } - return true; } +void AntlrParser::enableChecks() { + d_checksEnabled = true; +} + +void AntlrParser::disableChecks() { + d_checksEnabled = false; +} + + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 52b4b4490..5c3f2f1f1 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -74,6 +74,12 @@ public: */ virtual Expr parseExpr() = 0; + /** Enable semantic checks during parsing. */ + void enableChecks(); + + /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */ + void disableChecks(); + protected: /** @@ -140,39 +146,38 @@ protected: * Checks if a symbol has been declared. * @param name the symbol name * @param type the symbol type + * @return true iff the symbol has been declared with the given type */ bool isDeclared(std::string name, SymbolType type = SYM_VARIABLE); /** - * Return true if the the declaration policy we want to enforce holds + * Checks if the declaration policy we want to enforce holds * for the given symbol. * @param name the symbol to check * @param check the kind of check to perform * @param type the type of the symbol - * @return true if the check holds - * @throws SemanticException if the check fails + * @throws SemanticException if checks are enabled and the check fails */ - bool checkDeclaration(std::string name, + void checkDeclaration(std::string name, DeclarationCheck check, SymbolType type = SYM_VARIABLE) throw (antlr::SemanticException); /** - * Returns true if the given name is bound to a function. + * Checks whether the given name is bound to a function. * @param name the name to check - * @return true if name is bound to a function - * @throws SemanticException if name is not bound to a function + * @throws SemanticException if checks are enabled and name is not bound to a function */ - bool checkFunction(std::string name) throw (antlr::SemanticException); + void checkFunction(std::string name) throw (antlr::SemanticException); /** * Check that kind can accept numArgs arguments. * @param kind the built-in operator to check * @param numArgs the number of actual arguments - * @throws SemanticException if the operator kind cannot be + * @throws SemanticException if checks are enabled and the operator kind cannot be * applied to numArgs arguments. */ - bool checkArity(Kind kind, unsigned int numArgs) throw (antlr::SemanticException); + void checkArity(Kind kind, unsigned int numArgs) throw (antlr::SemanticException); /** * Returns the type for the variable with the given name. @@ -317,6 +322,8 @@ protected: } } +// bool checksEnabled(); + private: /** The expression manager */ @@ -332,6 +339,9 @@ private: /** The sort table */ SymbolTable d_sortTable; + /** Are semantic checks enabled during parsing? */ + bool d_checksEnabled; + /** Lookup a symbol in the given namespace. */ Expr getSymbol(std::string var_name, SymbolType type); }; diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index e953244df..0cdf9f36b 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -154,7 +154,7 @@ identifier[DeclarationCheck check = CHECK_NONE, returns [std::string id] : x:IDENTIFIER { id = x->getText(); - AlwaysAssert( checkDeclaration(id, check, type) ); } + checkDeclaration(id, check, type); } ; /** @@ -381,6 +381,6 @@ functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f] std::string name; } : name = identifier[check,SYM_FUNCTION] - { AlwaysAssert( checkFunction(name) ); + { checkFunction(name); f = getFunction(name); } ; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index ef23d3883..b9e2d576e 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -132,5 +132,14 @@ Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, return getNewParser(em, lang, &input, "", false); } +void Parser::disableChecks() { + d_antlrParser->disableChecks(); +} + +void Parser::enableChecks() { + d_antlrParser->enableChecks(); +} + + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index bc4fd6018..170e1af31 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -84,6 +84,12 @@ public: */ bool done() const; + /** Enable semantic checks during parsing. */ + void enableChecks(); + + /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */ + void disableChecks(); + private: /** diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index a9f06d92c..39cadd47f 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -16,7 +16,6 @@ header "post_include_hpp" { #include "parser/antlr_parser.h" #include "expr/command.h" -#include "util/Assert.h" } header "post_include_cpp" { @@ -123,7 +122,7 @@ annotatedFormula returns [CVC4::Expr formula] } : /* a built-in operator application */ LPAREN kind = builtinOp annotatedFormulas[args] RPAREN - { AlwaysAssert( checkArity(kind, args.size()) ); + { checkArity(kind, args.size()); formula = mkExpr(kind,args); } | /* A non-built-in function application */ @@ -213,7 +212,7 @@ functionSymbol returns [CVC4::Expr fun] string name; } : name = functionName[CHECK_DECLARED] - { AlwaysAssert( checkFunction(name) ); + { checkFunction(name); fun = getFunction(name); } ; @@ -316,6 +315,6 @@ returns [std::string id] } : x:IDENTIFIER { id = x->getText(); - AlwaysAssert( checkDeclaration(id, check,type) ); } + checkDeclaration(id, check,type); } ; diff --git a/src/util/options.h b/src/util/options.h index 0a1766c09..cad00a61b 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -45,8 +45,12 @@ struct Options { /** The CNF conversion */ CVC4::CnfConversion d_cnfConversion; + /** Should we exit after parsing? */ bool parseOnly; + /** Should the parser do semantic checks? */ + bool semanticChecks; + Options() : binary_name(), smtcomp_mode(false), statistics(false), @@ -55,7 +59,8 @@ struct Options { verbosity(0), lang(parser::Parser::LANG_AUTO), d_cnfConversion(CVC4::CNF_VAR_INTRODUCTION), - parseOnly(false) + parseOnly(false), + semanticChecks(true) {} };/* struct Options */