Allow disabling include-file feature

diff --git a/src/parser/options b/src/parser/options
index b3e69a9927a7640d19a192f603222578889e71bb..e16f963f49874c09cf4151221e264782d2f56054 100644 (file)
--- 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 370bdfcf0356202063b44756bf3edb99f36bbc1a..fa2a1e744c00d919ab869716ec8d547ed7f498d8 100644 (file)
--- 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 4f943a0b5e1aa434a894ba1b781e4dc3f7a429e5..b4e79b427df7c5320de6033635a5a6834d9b4e7c 100644 (file)
--- 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<Kind> 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 e1e4053ac4b316094c04135f11fd5144b2efb5ce..684a495b666660fbc0f3192126795d27a1c58191 100644 (file)
--- 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 607547bebbbfe4f3ba02e738afb5ff41783a6cde..9779bf37b9108c368e5849cccd7e7aba115a7212 100644 (file)
--- 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 29bc8d40f9695f0368480bdd5a880519581b1414..5abaa01638c1e3e1436f71089da363bf083dc7ac 100644 (file)
--- 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 be4907e8e68aa30e0a3ccac9d32343326e538c49..42324fe1e25fe0cd65dbefd40348fee6655c168c 100644 (file)
--- 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<AntlrInput*>(getInput());
   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index ab4ea14c4a804da64a5b2eef404123650de93222..93c2168b14ba31825c38332155bdfdc615ffaa3e 100644 (file)
--- 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<AntlrInput *>(getInput());
   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();