exception based error handling for SMT2 files

Author: Daniel Kroening

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\)'"\)$
 --

src/solvers/smt2/smt2_parser.cpp

@@ -26,7 +26,7 @@ class smt2_parsert:public smt2_tokenizert
   bool parse() override
   {
     command_sequence();
-    return !ok;
+    return false;
   }
 
   struct idt
@@ -51,12 +51,12 @@ class smt2_parsert:public smt2_tokenizert
     const typet type;
   };
 
+  bool exit;
+
   /// This skips tokens until all bracketed expressions are closed
   void skip_to_end_of_list();
 
 protected:
-  bool exit;
-
   // we override next_token to track the parenthesis level
   std::size_t parenthesis_level;
   tokent next_token() override;

src/solvers/smt2/smt2_parser.h

@@ -121,99 +121,88 @@ 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();
+    if(e.is_not_nil())
     {
-      exprt e=expression();
-      if(e.is_not_nil())
-      {
-        expand_function_applications(e);
-        define_constants(e);
-        solver.set_to_true(e);
-      }
+      expand_function_applications(e);
+      define_constants(e);
+      solver.set_to_true(e);
     }
-    else if(c=="check-sat")
+  }
+  else if(c == "check-sat")
+  {
+    switch(solver())
     {
-      switch(solver())
-      {
-      case decision_proceduret::resultt::D_SATISFIABLE:
-        std::cout << "sat\n";
-        break;
+    case decision_proceduret::resultt::D_SATISFIABLE:
+      std::cout << "sat\n";
+      break;
 
-      case decision_proceduret::resultt::D_UNSATISFIABLE:
-        std::cout << "unsat\n";
-        break;
+    case decision_proceduret::resultt::D_UNSATISFIABLE:
+      std::cout << "unsat\n";
+      break;
 
-      case decision_proceduret::resultt::D_ERROR:
-        std::cout << "error\n";
-      }
-    }
-    else if(c=="check-sat-assuming")
-    {
-      std::cout << "not yet implemented\n";
-    }
-    else if(c=="display")
-    {
-      // this is a command that Z3 appears to implement
-      exprt e=expression();
-      if(e.is_not_nil())
-      {
-        std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
-      }
-    }
-    else if(c=="simplify")
-    {
-      // this is a command that Z3 appears to implement
-      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);
-        std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
-      }
+    case decision_proceduret::resultt::D_ERROR:
+      std::cout << "error\n";
     }
-    #if 0
-    // TODO:
-    | ( declare-const hsymboli hsorti )
-    | ( declare-datatype hsymboli hdatatype_deci)
-    | ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
-    | ( declare-fun hsymboli ( hsorti ??? ) hsorti )
-    | ( declare-sort hsymboli hnumerali )
-    | ( define-fun hfunction_def i )
-    | ( define-fun-rec hfunction_def i )
-    | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
-    | ( define-sort hsymboli ( hsymboli ??? ) hsorti )
-    | ( echo hstringi )
-    | ( exit )
-    | ( get-assertions )
-    | ( get-assignment )
-    | ( get-info hinfo_flag i )
-    | ( get-model )
-    | ( get-option hkeywordi )
-    | ( get-proof )
-    | ( get-unsat-assumptions )
-    | ( get-unsat-core )
-    | ( get-value ( htermi + ) )
-    | ( pop hnumerali )
-    | ( push hnumerali )
-    | ( reset )
-    | ( reset-assertions )
-    | ( set-info hattributei )
-    | ( set-option hoptioni )
-    #endif  
-    else
-      smt2_parsert::command(c);
   }
-  catch(const char *error)
+  else if(c == "check-sat-assuming")
+  {
+    std::cout << "not yet implemented\n";
+  }
+  else if(c == "display")
   {
-    std::cout << "error: " << error << '\n';
+    // this is a command that Z3 appears to implement
+    exprt e = expression();
+    if(e.is_not_nil())
+    {
+      std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
+    }
   }
-  catch(const std::string &error)
+  else if(c == "simplify")
   {
-    std::cout << "error: " << error << '\n';
+    // this is a command that Z3 appears to implement
+    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);
+      std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
+    }
   }
+#if 0
+  // TODO:
+  | ( declare-const hsymboli hsorti )
+  | ( declare-datatype hsymboli hdatatype_deci)
+  | ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
+  | ( declare-fun hsymboli ( hsorti ??? ) hsorti )
+  | ( declare-sort hsymboli hnumerali )
+  | ( define-fun hfunction_def i )
+  | ( define-fun-rec hfunction_def i )
+  | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
+  | ( define-sort hsymboli ( hsymboli ??? ) hsorti )
+  | ( echo hstringi )
+  | ( exit )
+  | ( get-assertions )
+  | ( get-assignment )
+  | ( get-info hinfo_flag i )
+  | ( get-model )
+  | ( get-option hkeywordi )
+  | ( get-proof )
+  | ( get-unsat-assumptions )
+  | ( get-unsat-core )
+  | ( get-value ( htermi + ) )
+  | ( pop hnumerali )
+  | ( push hnumerali )
+  | ( reset )
+  | ( reset-assertions )
+  | ( set-info hattributei )
+  | ( set-option hoptioni )
+#endif
+  else
+    smt2_parsert::command(c);
 }
 
 class smt2_message_handlert : public message_handlert
@@ -261,10 +250,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;

src/solvers/smt2/smt2_solver.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,8 +190,7 @@ 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()
@@ -272,18 +270,10 @@ void smt2_tokenizert::get_token_from_stream()
           return;
         }
         else
-        {
-          error() << "unknown numeral token" << eom;
-          token=ERROR;
-          return;
-        }
+          throw error("unknown numeral token");
       }
       else
-      {
-        error() << "unexpected EOF in numeral token" << eom;
-        token=ERROR;
-        return;
-      }
+        throw error("unexpected EOF in numeral token");
       break;
 
     default: // likely a simple symbol or a numeral
@@ -302,9 +292,9 @@ void smt2_tokenizert::get_token_from_stream()
       else
       {
         // illegal character, error
-        error() << "unexpected character `" << ch << '\'' << eom;
-        token=ERROR;
-        return;
+        std::ostringstream msg;
+        msg << "unexpected character `" << ch << '\'';
+        throw error(msg.str());
       }
     }
   }

src/solvers/smt2/smt2_tokenizer.cpp

@@ -9,30 +9,60 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_SMT2_SMT2_TOKENIZER_H
 #define CPROVER_SOLVERS_SMT2_SMT2_TOKENIZER_H
 
+#include <util/exception_utils.h>
 #include <util/parser.h>
 
 #include <string>
 
 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;
 
   virtual tokent next_token();
@@ -49,17 +79,20 @@ class smt2_tokenizert:public parsert
     }
   }
 
-  mstreamt &error()
-  {
-    ok=false;
-    messaget::error().source_location.set_line(line_no);
-    return messaget::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)
+  {
+    return smt2_errort(std::move(message), line_no);
+  }
+
+  smt2_errort error(const std::ostringstream &message)
+  {
+    return smt2_errort(message.str(), line_no);
+  }
+
 private:
   tokent get_decimal_numeral();
   tokent get_hex_numeral();

src/solvers/smt2/smt2_tokenizer.h

@@ -33,60 +33,63 @@ class smt2irept:public smt2_tokenizert
 
 bool smt2irept::parse()
 {
-  std::stack<irept> stack;
-  result.clear();
-
-  while(true)
+  try
   {
-    switch(next_token())
+    std::stack<irept> 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(smt2_errort)
+  {
+    return true;
+  }
 }
 
 irept smt2irep(std::istream &in)