From: Morgan Deters Date: Fri, 7 Jun 2013 19:23:36 +0000 (-0400) Subject: Allow disabling include-file feature X-Git-Tag: cvc5-1.0.0~7287^2~104 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=931b5641dfffcd3779239e014406aa057e21e0f7;p=cvc5.git Allow disabling include-file feature --- diff --git a/src/parser/options b/src/parser/options index b3e69a992..e16f963f4 100644 --- a/src/parser/options +++ b/src/parser/options @@ -17,4 +17,8 @@ option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT option szsCompliant --szs-compliant bool :default false temporary support for szs ontolotogy, print if conjecture is found +# this is just to support security in the online version +# (--no-include-file disables filesystem access in TPTP and SMT2 parsers) +undocumented-option canIncludeFile /--no-include-file bool :default true + endmodule diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 370bdfcf0..fa2a1e744 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -47,7 +47,8 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par d_done(false), d_checksEnabled(true), d_strictMode(strictMode), - d_parseOnly(parseOnly) { + d_parseOnly(parseOnly), + d_canIncludeFile(true) { d_input->setParser(*this); } diff --git a/src/parser/parser.h b/src/parser/parser.h index 4f943a0b5..b4e79b427 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -158,6 +158,12 @@ class CVC4_PUBLIC Parser { /** Are we only parsing? */ bool d_parseOnly; + /** + * Can we include files? (Set to false for security purposes in + * e.g. the online version.) + */ + bool d_canIncludeFile; + /** The set of operators available in the current logic. */ std::set d_logicOperators; @@ -252,6 +258,10 @@ public: bool strictModeEnabled() { return d_strictMode; } + bool allowIncludeFile() { d_canIncludeFile = true; } + bool disallowIncludeFile() { d_canIncludeFile = false; } + bool canIncludeFile() const { return d_canIncludeFile; } + /** * Returns a variable, given a name. * diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index e1e4053ac..684a495b6 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -54,6 +54,7 @@ void ParserBuilder::init(ExprManager* exprManager, d_exprManager = exprManager; d_checksEnabled = true; d_strictMode = false; + d_canIncludeFile = true; d_mmap = false; d_parseOnly = false; } @@ -106,6 +107,12 @@ Parser* ParserBuilder::build() parser->disableChecks(); } + if( d_canIncludeFile ) { + parser->allowIncludeFile(); + } else { + parser->disallowIncludeFile(); + } + return parser; } @@ -151,7 +158,8 @@ ParserBuilder& ParserBuilder::withOptions(const Options& options) { .withMmap(options[options::memoryMap]) .withChecks(options[options::semanticChecks]) .withStrictMode(options[options::strictParsing]) - .withParseOnly(options[options::parseOnly]); + .withParseOnly(options[options::parseOnly]) + .withIncludeFile(options[options::canIncludeFile]); } ParserBuilder& ParserBuilder::withStrictMode(bool flag) { @@ -159,6 +167,11 @@ ParserBuilder& ParserBuilder::withStrictMode(bool flag) { return *this; } +ParserBuilder& ParserBuilder::withIncludeFile(bool flag) { + d_canIncludeFile = flag; + return *this; +} + ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) { d_inputType = STREAM_INPUT; d_streamInput = &input; diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 607547beb..9779bf37b 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -71,6 +71,9 @@ class CVC4_PUBLIC ParserBuilder { /** Should we parse in strict mode? */ bool d_strictMode; + /** Should we allow include-file commands? */ + bool d_canIncludeFile; + /** Should we memory-map a file input? */ bool d_mmap; @@ -149,6 +152,13 @@ public: */ ParserBuilder& withStrictMode(bool flag = true); + /** + * Should the include-file commands be enabled? + * + * (Default: yes) + */ + ParserBuilder& withIncludeFile(bool flag = true); + /** Set the parser to use the given stream for its input. */ ParserBuilder& withStreamInput(std::istream& input); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 29bc8d40f..5abaa0163 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -197,7 +197,10 @@ parseCommand returns [CVC4::Command* cmd = NULL] * the RPAREN_TOK is properly eaten and we are in a good state to read * the included file's tokens. */ | LPAREN_TOK INCLUDE_TOK str[name] RPAREN_TOK - { if(PARSER_STATE->strictModeEnabled()) { + { if(!PARSER_STATE->canIncludeFile()) { + PARSER_STATE->parseError("include-file feature was disabled for this run."); + } + if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); } PARSER_STATE->includeFile(name); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index be4907e8e..42324fe1e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -242,6 +242,11 @@ static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) { } void Smt2::includeFile(const std::string& filename) { + // security for online version + if(!canIncludeFile()) { + parseError("include-file feature was disabled for this run."); + } + // Get the lexer AntlrInput* ai = static_cast(getInput()); pANTLR3_LEXER lexer = ai->getAntlr3Lexer(); diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index ab4ea14c4..93c2168b1 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -128,6 +128,11 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){ void Tptp::includeFile(std::string fileName){ + // security for online version + if(!canIncludeFile()) { + parseError("include-file feature was disabled for this run."); + } + // Get the lexer AntlrInput * ai = static_cast(getInput()); pANTLR3_LEXER lexer = ai->getAntlr3Lexer();