Add solver.strict_parsing config option to control parsing strictness.

2024-12-01 20:23:10 +03:00 · 2021-04-20 09:59:41 -07:00 · 2021-04-20 09:59:41 -07:00 · 73b81b8431
commit 73b81b8431
parent c5ce7c4cdb
11 changed files with 110 additions and 20 deletions
--- a/what4/src/What4/Protocol/SMTLib2.hs
+++ b/what4/src/What4/Protocol/SMTLib2.hs
@ -47,6 +47,7 @@ module What4.Protocol.SMTLib2
  , nameResult
  , setProduceModels
  , smtLibEvalFuns
+  , smtlib2Options
    -- * Logic
  , SMT2.Logic(..)
  , SMT2.qf_bv
@ -128,6 +129,8 @@ import           LibBF( bfToBits )
 import           Prelude hiding (writeFile)

 import           What4.BaseTypes
+import qualified What4.Concrete as BC
+import qualified What4.Config as CFG
 import qualified What4.Expr.Builder as B
 import           What4.Expr.GroundEval
 import qualified What4.Interface as I
@ -153,6 +156,10 @@ all_supported :: SMT2.Logic
 all_supported = SMT2.allSupported
 {-# DEPRECATED all_supported "Use allSupported" #-}

+
+smtlib2Options :: [CFG.ConfigDesc]
+smtlib2Options = smtParseOptions
+
 ------------------------------------------------------------------------
 -- Floating point

@ -564,6 +571,8 @@ newWriter :: a
              --   (may be the @nullInput@ stream if no responses are expected)
          -> AcknowledgementAction t (Writer a)
             -- ^ Action to run for consuming acknowledgement messages
+          -> ResponseStrictness
+             -- ^ Be strict in parsing SMT solver responses?
          -> String
             -- ^ Name of solver for reporting purposes.
          -> Bool
@ -576,13 +585,13 @@ newWriter :: a
          -> B.SymbolVarBimap t
             -- ^ Variable bindings for names.
          -> IO (WriterConn t (Writer a))
-newWriter _ h in_h ack solver_name permitDefineFun arithOption quantSupport bindings = do
+newWriter _ h in_h ack isStrict solver_name permitDefineFun arithOption quantSupport bindings = do
  r <- newIORef Set.empty
  let initWriter =
        Writer
        { declaredTuples = r
        }
-  conn <- newWriterConn h in_h ack solver_name arithOption bindings initWriter
+  conn <- newWriterConn h in_h ack solver_name isStrict arithOption bindings initWriter
  return $! conn { supportFunctionDefs = permitDefineFun
                 , supportQuantifiers = quantSupport
                 }
@ -926,8 +935,12 @@ class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
       Streams.OutputStream Text ->
       Streams.InputStream Text ->
       IO (WriterConn t (Writer a))
-  newDefaultWriter solver ack feats sym h in_h =
-    newWriter solver h in_h ack (show solver) True feats True
+  newDefaultWriter solver ack feats sym h in_h = do
+    let cfg = I.getConfiguration sym
+    strictness <- maybe Strict
+                  (\c -> if BC.fromConcreteBool c then Strict else Lenient) <$>
+                  (CFG.getOption =<< CFG.getOptionSetting strictSMTParsing cfg)
+    newWriter solver h in_h ack strictness (show solver) True feats True
      =<< B.getSymbolVarBimap sym

  -- | Run the solver in a session.
@ -1017,7 +1030,11 @@ writeDefaultSMT2 a nm feat sym h ps = do
  bindings <- B.getSymbolVarBimap sym
  str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
  null_in <- Streams.nullInput
-  c <- newWriter a str null_in nullAcknowledgementAction nm True feat True bindings
+  let cfg = I.getConfiguration sym
+  strictness <- maybe Strict
+                (\c -> if BC.fromConcreteBool c then Strict else Lenient) <$>
+                (CFG.getOption =<< CFG.getOptionSetting strictSMTParsing cfg)
+  c <- newWriter a str null_in nullAcknowledgementAction strictness nm True feat True bindings
  setProduceModels c True
  forM_ ps (SMTWriter.assume c)
  writeCheckSat c
--- a/what4/src/What4/Protocol/SMTLib2/Response.hs
+++ b/what4/src/What4/Protocol/SMTLib2/Response.hs
@ -21,6 +21,8 @@ module What4.Protocol.SMTLib2.Response
  , SMTLib2Exception(..)
  , getSolverResponse
  , getLimitedSolverResponse
+  , smtParseOptions
+  , strictSMTParsing
  )
 where

@ -31,15 +33,36 @@ import           Data.Text ( Text )
 import qualified Data.Text as Text
 import qualified Data.Text.Lazy as Lazy
 import qualified Data.Text.Lazy.Builder as Builder
+import qualified Prettyprinter.Util as PPU
 import qualified System.IO.Streams as Streams
 import qualified System.IO.Streams.Attoparsec.Text as AStreams

+import qualified What4.BaseTypes as BT
+import qualified What4.Concrete as BC
+import qualified What4.Config as CFG
 import           What4.Protocol.SExp
 import qualified What4.Protocol.SMTLib2.Syntax as SMT2
 import qualified What4.Protocol.SMTWriter as SMTWriter
 import           What4.Utils.Process ( filterAsync )


+strictSMTParsing :: CFG.ConfigOption BT.BaseBoolType
+strictSMTParsing = CFG.configOption BT.BaseBoolRepr "solver.strict_parsing"
+
+smtParseOptions :: [CFG.ConfigDesc]
+smtParseOptions =
+  [
+    CFG.mkOpt strictSMTParsing CFG.boolOptSty
+    (Just $ PPU.reflow $
+     Text.concat ["Strictly parse SMT responses and fail on"
+                 , "unrecognized data (the default)."
+                 , "This might need to be disabled when running"
+                 , "the SMT solver in verbose mode."
+                 ])
+    (Just (BC.ConcreteBool True))
+  ]
+
+
 data SMTResponse = AckSuccess
                 | AckUnsupported
                 | AckError Text
@ -59,7 +82,9 @@ getSolverResponse :: SMTWriter.WriterConn t h
                  -> IO (Either SomeException SMTResponse)
 getSolverResponse conn = do
  mb <- tryJust filterAsync
-        (AStreams.parseFromStream rspParser (SMTWriter.connInputHandle conn))
+        (AStreams.parseFromStream
+          (rspParser (SMTWriter.strictParsing conn))
+          (SMTWriter.connInputHandle conn))
  return mb


@ -98,8 +123,8 @@ getLimitedSolverResponse intent handleResponse conn cmd =
                ]


-rspParser :: AT.Parser SMTResponse
-rspParser =
+rspParser :: SMTWriter.ResponseStrictness -> AT.Parser SMTResponse
+rspParser strictness =
  let lexeme p = skipSpaceOrNewline *> p
      parens p = AT.char '(' *> p <* AT.char ')'
      errParser = parens $ lexeme (AT.string "error") *>
@ -134,7 +159,11 @@ rspParser =
      -- sometimes verbose output mode will generate interim text
      -- before the actual ack; the following skips lines of input
      -- that aren't recognized.
-      (AckSkipped <$> AT.takeWhile1 (not . AT.isEndOfLine) <*> rspParser)
+      (case strictness of
+         SMTWriter.Strict -> empty
+         SMTWriter.Lenient -> AckSkipped
+                              <$> AT.takeWhile1 (not . AT.isEndOfLine)
+                              <*> (rspParser strictness))
     )

 parseSMTLib2String :: AT.Parser Text
--- a/what4/src/What4/Protocol/SMTWriter.hs
+++ b/what4/src/What4/Protocol/SMTWriter.hs
@ -57,6 +57,7 @@ module What4.Protocol.SMTWriter
              , supportFunctionArguments
              , supportQuantifiers
              , supportedFeatures
+              , strictParsing
              , connHandle
              , connInputHandle
              , smtWriterName
@ -82,6 +83,7 @@ module What4.Protocol.SMTWriter
  , assumeFormulaWithFreshName
  , DefineStyle(..)
  , AcknowledgementAction(..)
+  , ResponseStrictness(..)
  , nullAcknowledgementAction
    -- * SMTWriter operations
  , assume
@ -612,6 +614,9 @@ data WriterConn t (h :: Type) =
               -- indices.
             , supportQuantifiers :: !Bool
               -- ^ Allow the SMT writer to generate problems with quantifiers.
+             , strictParsing :: !ResponseStrictness
+               -- ^ Be strict in parsing SMTLib2 responses; no
+               -- verbosity or variants allowed
             , supportedFeatures :: !ProblemFeatures
               -- ^ Indicates features supported by the solver.
             , entryStack :: !(IORef [StackEntry t h])
@ -701,6 +706,8 @@ newWriterConn :: OutputStream Text
              -- ^ An action to consume solver acknowledgement responses
              -> String
              -- ^ Name of solver for reporting purposes.
+              -> ResponseStrictness
+              -- ^ Be strict in parsing responses?
              -> ProblemFeatures
              -- ^ Indicates what features are supported by the solver.
              -> SymbolVarBimap t
@ -708,7 +715,7 @@ newWriterConn :: OutputStream Text
              -- canonical name (if any).
              -> cs -- ^ State information specific to the type of connection
              -> IO (WriterConn t cs)
-newWriterConn h in_h ack solver_name features bindings cs = do
+newWriterConn h in_h ack solver_name beStrict features bindings cs = do
  entry <- newStackEntry
  stk_ref <- newIORef [entry]
  r <- newIORef emptyState
@ -718,6 +725,7 @@ newWriterConn h in_h ack solver_name features bindings cs = do
                       , supportFunctionDefs      = False
                       , supportFunctionArguments = False
                       , supportQuantifiers       = False
+                       , strictParsing            = beStrict
                       , supportedFeatures        = features
                       , entryStack   = stk_ref
                       , stateRef     = r
@ -726,6 +734,12 @@ newWriterConn h in_h ack solver_name features bindings cs = do
                       , consumeAcknowledgement = ack
                       }

+-- | Strictness level for parsing solver responses
+data ResponseStrictness
+  = Lenient
+  | Strict
+  deriving (Eq)
+
 -- | Status to indicate when term value will be uncached.
 data TermLifetime
   = DeleteNever
--- a/what4/src/What4/Solver/Boolector.hs
+++ b/what4/src/What4/Solver/Boolector.hs
@ -58,7 +58,7 @@ boolectorOptions =
      executablePathOptSty
      (Just "Path to boolector executable")
      (Just (ConcreteString "boolector"))
-  ]
+  ] <> SMT2.smtlib2Options

 boolectorAdapter :: SolverAdapter st
 boolectorAdapter =
--- a/what4/src/What4/Solver/CVC4.hs
+++ b/what4/src/What4/Solver/CVC4.hs
@ -45,6 +45,7 @@ import           What4.Expr.Builder
 import           What4.Expr.GroundEval
 import           What4.Protocol.Online
 import qualified What4.Protocol.SMTLib2 as SMT2
+import qualified What4.Protocol.SMTLib2.Response as RSP
 import qualified What4.Protocol.SMTLib2.Syntax as Syntax
 import           What4.Protocol.SMTWriter
 import           What4.Utils.Process
@ -78,7 +79,7 @@ cvc4Options =
          integerOptSty
          (Just "Per-check timeout in milliseconds (zero is none)")
          (Just (ConcreteInteger 0))
-  ]
+  ] <> SMT2.smtlib2Options

 cvc4Adapter :: SolverAdapter st
 cvc4Adapter =
@ -130,7 +131,11 @@ writeMultiAsmpCVC4SMT2File sym h ps = do
  bindings <- getSymbolVarBimap sym
  out_str  <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
  in_str <- Streams.nullInput
-  c <- SMT2.newWriter CVC4 out_str in_str nullAcknowledgementAction "CVC4"
+  let cfg = getConfiguration sym
+  strictness <- maybe Strict
+                (\c -> if fromConcreteBool c then Strict else Lenient) <$>
+                (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)
+  c <- SMT2.newWriter CVC4 out_str in_str nullAcknowledgementAction strictness "CVC4"
         True cvc4Features True bindings
  SMT2.setLogic c SMT2.allSupported
  SMT2.setProduceModels c True
--- a/what4/src/What4/Solver/DReal.hs
+++ b/what4/src/What4/Solver/DReal.hs
@ -56,6 +56,7 @@ import           What4.SatResult
 import           What4.Expr.Builder
 import           What4.Expr.GroundEval
 import qualified What4.Protocol.SMTLib2 as SMT2
+import qualified What4.Protocol.SMTLib2.Response as RSP
 import qualified What4.Protocol.SMTWriter as SMTWriter
 import           What4.Utils.Process
 import           What4.Utils.Streams (logErrorStream)
@ -74,7 +75,7 @@ drealOptions =
      executablePathOptSty
      (Just "Path to dReal executable")
      (Just (ConcreteString "dreal"))
-  ]
+  ] <> SMT2.smtlib2Options

 drealAdapter :: SolverAdapter st
 drealAdapter =
@ -106,7 +107,13 @@ writeDRealSMT2File sym h ps = do
  bindings <- getSymbolVarBimap sym
  out_str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
  in_str <- Streams.nullInput
-  c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction "dReal"
+  let cfg = getConfiguration sym
+  strictness <- maybe SMTWriter.Strict
+                (\c -> if fromConcreteBool c
+                       then SMTWriter.Strict
+                       else SMTWriter.Lenient) <$>
+                (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)
+  c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction strictness "dReal"
          False useComputableReals False bindings
  SMT2.setProduceModels c True
  SMT2.setLogic c (SMT2.Logic "QF_NRA")
@ -299,7 +306,14 @@ runDRealInOverride sym logData ps modelFn = do

      in_str <- Streams.nullInput

-      c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction "dReal"
+      let cfg = getConfiguration sym
+      strictness <- maybe SMTWriter.Strict
+                    (\c -> if fromConcreteBool c
+                           then SMTWriter.Strict
+                           else SMTWriter.Lenient) <$>
+                    (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)
+
+      c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction strictness "dReal"
             False useComputableReals False bindings

      -- Set the dReal default logic
--- a/what4/src/What4/Solver/ExternalABC.hs
+++ b/what4/src/What4/Solver/ExternalABC.hs
@ -53,7 +53,7 @@ abcOptions =
      executablePathOptSty
      (Just "ABC executable path")
      (Just (ConcreteString "abc"))
-  ]
+  ] <> SMT2.smtlib2Options

 externalABCAdapter :: SolverAdapter st
 externalABCAdapter =
--- a/what4/src/What4/Solver/STP.hs
+++ b/what4/src/What4/Solver/STP.hs
@ -57,7 +57,7 @@ stpOptions =
          (Just "Path to STP executable.")
          (Just (ConcreteString "stp"))
  , intWithRangeOpt stpRandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1)
-  ]
+  ] <> SMT2.smtlib2Options

 stpAdapter :: SolverAdapter st
 stpAdapter =
--- a/what4/src/What4/Solver/Yices.hs
+++ b/what4/src/What4/Solver/Yices.hs
@ -451,7 +451,7 @@ newConnection stream in_stream ack reqFeatures timeout bindings = do
                     , yicesTimeout = timeout
                     , yicesUnitDeclared = unitRef
                     }
-  conn <- newWriterConn stream in_stream (ack earlyUnsatRef) nm features' bindings c
+  conn <- newWriterConn stream in_stream (ack earlyUnsatRef) nm Strict features' bindings c
  return $! conn { supportFunctionDefs = True
                 , supportFunctionArguments = True
                 , supportQuantifiers = efSolver
--- a/what4/src/What4/Solver/Z3.hs
+++ b/what4/src/What4/Solver/Z3.hs
@ -69,7 +69,7 @@ z3Options =
      integerOptSty
      (Just "Per-check timeout in milliseconds (zero is none)")
      (Just (ConcreteInteger 0))
-  ]
+  ] <> SMT2.smtlib2Options

 z3Adapter :: SolverAdapter st
 z3Adapter =
--- a/what4/test/SolverParserTest.hs
+++ b/what4/test/SolverParserTest.hs
@ -23,6 +23,8 @@ sugarCube :: CUBE
 sugarCube = mkCUBE { inputDir = "test/responses"
                   , rootName = "*.rsp"
                   , expectedSuffix = ".exp"
+                   , validParams = [ ("parsing", Just ["strict", "lenient"])
+                                   ]
                   }

 ingredients :: [Ingredient]
@ -40,6 +42,14 @@ main = do testSweets <- findSugar sugarCube
 mkTest :: Sweets -> Natural -> Expectation -> IO [TestTree]
 mkTest s n e = do
  expect <- readFile $ expectedFile e
+  let strictness =
+        let strictVal pmtch =
+              if paramMatchVal "strict" pmtch
+              then Strict
+              else if paramMatchVal "lenient" pmtch
+                   then Lenient
+                   else error "Invalid strictness specification"
+        in maybe Strict strictVal $ lookup "parsing" $ expParamsMatch e
  return
    [
      testCase (rootMatchName s <> " #" <> show n) $ do
@ -50,6 +60,7 @@ mkTest s n e = do
             inpStrm
             (AckAction $ undefined)
             "test-solver"
+             strictness
             noFeatures
             emptySymbolVarBimap
             ()