what4 1.3 → 1.4

raw patch · 45 files changed

+5182/−85 lines, 45 filesdep +BoundedChandep +megaparsecdep +ordered-containersdep −data-binary-ieee754dep ~basedep ~bv-sizeddep ~containers

Dependencies added: BoundedChan, megaparsec, ordered-containers, parsec, s-cargot, stm, time, unliftio

Dependencies removed: data-binary-ieee754

Dependency ranges changed: base, bv-sized, containers, directory, exceptions, hedgehog, libBF, parameterized-utils, process, tasty, tasty-hedgehog, tasty-hunit, tasty-sugar, temporary, text

Files

• CHANGES.md +33/−0
• LICENSE +1/−1
• README.md +7/−0
• doc/implementation.md +1/−1
• src/What4/Expr/App.hs +2/−0
• src/What4/Expr/AppTheory.hs +1/−1
• src/What4/Expr/Builder.hs +59/−18
• src/What4/Expr/VarIdentification.hs +2/−3
• src/What4/Interface.hs +88/−6
• src/What4/ProblemFeatures.hs +9/−3
• src/What4/Protocol/Online.hs +47/−0
• src/What4/Protocol/SExp.hs +6/−0
• src/What4/Protocol/SMTLib2.hs +454/−18
• src/What4/Protocol/SMTLib2/Parse.hs +1/−1
• src/What4/Protocol/SMTLib2/Response.hs +5/−1
• src/What4/Protocol/SMTLib2/Syntax.hs +52/−3
• src/What4/Protocol/SMTWriter.hs +110/−2
• src/What4/Protocol/VerilogWriter.hs +1/−0
• src/What4/Serialize/FastSExpr.hs +184/−0
• src/What4/Serialize/Log.hs +436/−0
• src/What4/Serialize/Normalize.hs +162/−0
• src/What4/Serialize/Parser.hs +1070/−0
• src/What4/Serialize/Printer.hs +779/−0
• src/What4/Serialize/SETokens.hs +259/−0
• src/What4/Solver.hs +12/−0
• src/What4/Solver/Boolector.hs +3/−2
• src/What4/Solver/CVC4.hs +4/−4
• src/What4/Solver/CVC5.hs +380/−0
• src/What4/Solver/Yices.hs +15/−0
• src/What4/Solver/Z3.hs +95/−3
• src/What4/Utils/AbstractDomains.hs +1/−0
• src/What4/Utils/OnlyIntRepr.hs +1/−0
• src/What4/Utils/Serialize.hs +127/−0
• test/Abduct.hs +155/−0
• test/AdapterTest.hs +1/−0
• test/ExprBuilderSMTLib2.hs +3/−1
• test/ExprsTest.hs +58/−0
• test/InvariantSynthesis.hs +153/−0
• test/OnlineSolverTest.hs +6/−2
• test/SerializeTestUtils.hs +58/−0
• test/SerializeTests.hs +20/−0
• test/SolverParserTest.hs +1/−1
• test/SymFnTests.hs +242/−0
• test/TestTemplate.hs +4/−3
• what4.cabal +74/−11

@@ -1,3 +1,36 @@+# 1.4 (January 2023)++* Allow building with GHC 9.4.++* Remove the `MonadFail` instance for `VarRecorder`, as this instance is no+  longer straightforward to define due to upstream changes in `base-4.17.0.0`.+  This instance ultimately called `error` anyways, so any uses of `fail` at type+  `VarRecorder` can be replaced with `error` without any change in behavior.++* Remove a dependency on `data-binary-ieee754`, which has been deprecated.++* Deprecate `allSupported` which represents the SMT logic `ALL_SUPPORTED`,+  and add `allLogic` instead which represents the SMTLib standard logic `ALL`.++* Add support for the cvc5 SMT solver.++* Add a `get-abduct` feature which is compatible with cvc5.++* Add modules to support serialization and deserialization of what4 terms into+  an s-expression format that is a superset of SMTLib2. See the+  `What4.Serialize.Printer`, `What4.Serialize.Parser`, and+  `What4.Serialize.FastSExpr` modules. Note that these modules have names that+  conflict with the now deprecated what4-serialize package, from which they were+  copied. If you are updating to this version of what4, delete your dependency+  on what4-serialize.++* Add support Syntax-Guided Synthesis (SyGuS) in CVC5 (through the+  `runCVC5SyGuS` function) and Constrained Horn Clauses (CHC) in Z3 (through the+  `runZ3Horn` function).++* Make `what4` smarter about simplifying `intMin x y` and `intMax x y`+  expressions when either `x <= y` or `y <= x` can be statically determined.+ # 1.3 (April 2022)  * Allow building with GHC 9.2.

@@ -1,4 +1,4 @@-Copyright (c) 2013-2020 Galois Inc.+Copyright (c) 2013-2023 Galois Inc. All rights reserved.  Redistribution and use in source and binary forms, with or without

@@ -224,6 +224,12 @@ Additional implementation and operational documentation can be found in the [implementation documentation in doc/implementation.md](doc/implementation.md). +To serialize and deserialize what4 terms, see the following modules:++* `What4.Serialize.Printer` (to serialize what4 terms into an s-expression format)+* `What4.Serialize.Parser` (to deserialize what4 terms)+* `What4.Serialize.FastSExpr` (provides a faster s-expression parser than the default, intended to be used in conjunction with the higher-level parsing in `What4.Serialize.Parser`)+ ## Formula Construction vs Solving  In what4, building expressions and solving expressions are orthogonal concerns.@@ -273,6 +279,7 @@ - Z3 versions 4.8.7 through 4.8.12 - Yices 2.6.1 and 2.6.2 - CVC4 1.7 and 1.8+- CVC5 1.0.2 - Boolector 3.2.1 and 3.2.2 - STP 2.3.3     (However, note https://github.com/stp/stp/issues/363, which prevents

@@ -2,7 +2,7 @@  What4 provides a language to represent symbolic computations and the ability to perform those computations using one of several SMT-solvers, including Yices, Z3, CVC4, and others.+solvers, including Yices, Z3, CVC4, CVC5, and others.  ## What4 Language 

@@ -1722,6 +1722,8 @@ instance IsSymFn (ExprSymFn t) where   fnArgTypes = symFnArgTypes   fnReturnType = symFnReturnType+  fnTestEquality = testExprSymFnEq+  fnCompare f g = compareF (symFnId f) (symFnId g)   -------------------------------------------------------------------------------

@@ -33,7 +33,7 @@    | FloatingPointTheory    | ArrayTheory    | StructTheory-     -- ^ Theory attributed to structs (equivalent to records in CVC4/Z3, tuples in Yices)+     -- ^ Theory attributed to structs (equivalent to records in CVC4/CVC5/Z3, tuples in Yices)    | FnTheory      -- ^ Theory attributed application functions.    deriving (Eq, Ord)

@@ -134,6 +134,8 @@   , SymFnInfo(..)   , symFnArgTypes   , symFnReturnType+  , SomeExprSymFn(..)+  , ExprSymFnWrapper(..)      -- * SymbolVarBimap   , SymbolVarBimap@@ -187,7 +189,6 @@ import qualified Data.BitVector.Sized as BV import           Data.Bimap (Bimap) import qualified Data.Bimap as Bimap-import qualified Data.Binary.IEEE754 as IEEE754  import           Data.Hashable import           Data.IORef@@ -208,6 +209,7 @@ import           Data.Ratio (numerator, denominator) import           Data.Set (Set) import qualified Data.Set as Set+import           GHC.Float (castFloatToWord32, castDoubleToWord64) import qualified LibBF as BF  import           What4.BaseTypes@@ -247,19 +249,19 @@ toDouble :: Rational -> Double toDouble = fromRational -cachedEval :: (HashableF k, TestEquality k)+cachedEval :: (HashableF k, TestEquality k, MonadIO m)            => PH.HashTable RealWorld k a            -> k tp-           -> IO (a tp)-           -> IO (a tp)+           -> m (a tp)+           -> m (a tp) cachedEval tbl k action = do-  mr <- stToIO $ PH.lookup tbl k+  mr <- liftIO $ stToIO $ PH.lookup tbl k   case mr of     Just r -> return r     Nothing -> do       r <- action       seq r $ do-      stToIO $ PH.insert tbl k r+      liftIO $ stToIO $ PH.insert tbl k r       return r  ------------------------------------------------------------------------@@ -319,8 +321,20 @@ data ExprSymFnWrapper t c    = forall a r . (c ~ (a ::> r)) => ExprSymFnWrapper (ExprSymFn t a r) -data SomeSymFn sym = forall args ret . SomeSymFn (SymFn sym args ret)+data SomeExprSymFn t = forall args ret . SomeExprSymFn (ExprSymFn t args ret) +instance Eq (SomeExprSymFn t) where+  (SomeExprSymFn fn1) == (SomeExprSymFn fn2) =+    isJust $ fnTestEquality fn1 fn2++instance Ord (SomeExprSymFn t) where+  compare (SomeExprSymFn fn1) (SomeExprSymFn fn2) =+    toOrdering $ fnCompare fn1 fn2++instance Show (SomeExprSymFn t) where+  show (SomeExprSymFn f) = show f++ ------------------------------------------------------------------------ -- ExprBuilder @@ -751,12 +765,12 @@ -- -- It is used when an action may modify a value, and we only want to run a -- second action if the value changed.-runIfChanged :: Eq e+runIfChanged :: (Eq e, Monad m)              => e-             -> (e -> IO e) -- ^ First action to run+             -> (e -> m e) -- ^ First action to run              -> r           -- ^ Result if no change.-             -> (e -> IO r) -- ^ Second action to run-             -> IO r+             -> (e -> m r) -- ^ Second action to run+             -> m r runIfChanged x f unChanged onChange = do   y <- f x   if x == y then@@ -807,11 +821,14 @@              -> ExprBuilder t st fs              -> ExprSymFn t idx ret              -> IO (Bool,ExprSymFn t idx ret)-evalSimpleFn tbl sym f =+evalSimpleFn tbl sym f = do+  let n = symFnId f   case symFnInfo f of-    UninterpFnInfo{} -> return (False, f)+    UninterpFnInfo{} -> do+      CachedSymFn changed f' <- cachedEval (fnTable tbl) n $+        return $! CachedSymFn False f+      return (changed, f')     DefinedFnInfo vars e evalFn -> do-      let n = symFnId f       let nm = symFnName f       CachedSymFn changed f' <-         cachedEval (fnTable tbl) n $ do@@ -3668,10 +3685,10 @@   iFloatLitRational sym fi x = iRealToFloat sym fi RNE =<< realLit sym x   iFloatLitSingle sym x =     iFloatFromBinary sym SingleFloatRepr-      =<< (bvLit sym knownNat $ BV.word32 $ IEEE754.floatToWord x)+      =<< (bvLit sym knownNat $ BV.word32 $ castFloatToWord32 x)   iFloatLitDouble sym x =     iFloatFromBinary sym DoubleFloatRepr-      =<< (bvLit sym knownNat $ BV.word64 $ IEEE754.doubleToWord x)+      =<< (bvLit sym knownNat $ BV.word64 $ castDoubleToWord64 x)   iFloatLitLongDouble sym x =     iFloatFromBinary sym X86_80FloatRepr       =<< (bvLit sym knownNat $ BV.mkBV knownNat $ fp80ToBits x)@@ -3853,10 +3870,10 @@   iFloatLitRational sym = floatLitRational sym . floatInfoToPrecisionRepr   iFloatLitSingle sym x =     floatFromBinary sym knownRepr-      =<< (bvLit sym knownNat $ BV.word32 $ IEEE754.floatToWord x)+      =<< (bvLit sym knownNat $ BV.word32 $ castFloatToWord32 x)   iFloatLitDouble sym x =     floatFromBinary sym knownRepr-      =<< (bvLit sym knownNat $ BV.word64 $ IEEE754.doubleToWord x)+      =<< (bvLit sym knownNat $ BV.word64 $ castDoubleToWord64 x)   iFloatLitLongDouble sym (X86_80Val e s) = do     el <- bvLit sym (knownNat @16) $ BV.word16 e     sl <- bvLit sym (knownNat @64) $ BV.word64 s@@ -4027,6 +4044,30 @@      MatlabSolverFnInfo f _ _ -> do        evalMatlabSolverFn f sym args      _ -> sbNonceExpr sym $! FnApp fn args++  substituteBoundVars sym subst e = do+    tbls <- stToIO $ do+      expr_tbl <- PH.newSized $ PM.size subst+      fn_tbl <- PH.new+      PM.traverseWithKey_ (PH.insert expr_tbl . BoundVarExpr) subst+      return $ EvalHashTables+        { exprTable = expr_tbl+        , fnTable  = fn_tbl+        }+    evalBoundVars' tbls sym e++  substituteSymFns sym subst e = do+    tbls <- stToIO $ do+      expr_tbl <- PH.new+      fn_tbl <- PH.newSized $ PM.size subst+      PM.traverseWithKey_+        (\(SymFnWrapper f) (SymFnWrapper g) -> PH.insert fn_tbl (symFnId f) (CachedSymFn True g))+        subst+      return $ EvalHashTables+        { exprTable = expr_tbl+        , fnTable  = fn_tbl+        }+    evalBoundVars' tbls sym e   instance IsInterpretedFloatExprBuilder (ExprBuilder t st fs) => IsInterpretedFloatSymExprBuilder (ExprBuilder t st fs)

@@ -138,7 +138,6 @@   deriving ( Functor            , Applicative            , Monad-           , MonadFail            , MonadST s            ) @@ -194,7 +193,7 @@   VR $ existQuantifiers %= Map.insert e (Some info)   recordAssertionVars ExistsOnly p x addExistVar ExistsForall _ _ _ _ _ = do-  fail $ "what4 does not allow existental variables to appear inside forall quantifier."+  error $ "what4 does not allow existental variables to appear inside forall quantifier."  addForallVar :: BM.Polarity -- ^ Polarity of formula              -> NonceAppExpr t BaseBoolType -- ^ Top term@@ -229,7 +228,7 @@   VR $ forallQuantifiers %= Map.insert e (Some info)   recordExprVars ExistsForall x addBothVar ExistsForall _ _ _ _ = do-  fail $ "what4 does not allow existental variables to appear inside forall quantifier."+  error $ "what4 does not allow existental variables to appear inside forall quantifier."  -- | Record variables in a predicate that we are checking satisfiability of. recordAssertionVars :: Scope

@@ -38,6 +38,12 @@    [@instance 'HashableF' ('SymExpr' sym)@] +  [@instance 'OrdF' ('BoundVar' sym)@]++  [@instance 'TestEquality' ('BoundVar' sym)@]++  [@instance 'HashableF' ('BoundVar' sym)@]+ The canonical implementation of these interface classes is found in "What4.Expr.Builder". -} {-# LANGUAGE CPP #-}@@ -72,6 +78,8 @@     -- ** Expression recognizers   , IsExpr(..)   , IsSymFn(..)+  , SomeSymFn(..)+  , SymFnWrapper(..)   , UnfoldPolicy(..)   , shouldUnfold @@ -202,6 +210,7 @@ import qualified Data.Parameterized.Context as Ctx import           Data.Parameterized.Ctx import           Data.Parameterized.Utils.Endian (Endian(..))+import           Data.Parameterized.Map (MapF) import           Data.Parameterized.NatRepr import           Data.Parameterized.TraversableFC import qualified Data.Parameterized.Vector as Vector@@ -587,7 +596,7 @@ -- of an undefined function is _not_ guaranteed to be equivalant to a free -- constant, and no guarantees are made about what properties such values -- will satisfy.-class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)+class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)       , TestEquality (SymAnnotation sym), OrdF (SymAnnotation sym)       , HashableF (SymAnnotation sym)       ) => IsExprBuilder sym where@@ -740,14 +749,42 @@   -- | Return the minimum value of two integers.   intMin :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)   intMin sym x y =-    do p <- intLe sym x y-       intIte sym p x y+    do x_le_y <- intLe sym x y+       y_le_x <- intLe sym y x+       case (asConstantPred x_le_y, asConstantPred y_le_x) of+         -- x <= y+         (Just True, _) -> return x+         -- x < y+         (_, Just False) -> return x+         -- y < x+         (Just False, _) -> return y+         -- y <= x+         (_, Just True) -> return y+         _ ->+           do let rng_x = integerBounds x+              let rng_y = integerBounds y+              unsafeSetAbstractValue (rangeMin rng_x rng_y) <$>+                intIte sym x_le_y x y    -- | Return the maximum value of two integers.   intMax :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)   intMax sym x y =-    do p <- intLe sym x y-       intIte sym p y x+    do x_le_y <- intLe sym x y+       y_le_x <- intLe sym y x+       case (asConstantPred x_le_y, asConstantPred y_le_x) of+         -- x <= y+         (Just True, _) -> return y+         -- x < y+         (_, Just False) -> return y+         -- y < x+         (Just False, _) -> return x+         -- y <= x+         (_, Just True) -> return x+         _ ->+           do let rng_x = integerBounds x+              let rng_y = integerBounds y+              unsafeSetAbstractValue (rangeMax rng_x rng_y) <$>+                intIte sym x_le_y y x    -- | If-then-else applied to integers.   intIte :: sym -> Pred sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)@@ -2690,15 +2727,43 @@ -- 'IsSymExprBuilder'. type family SymFn sym :: Ctx BaseType -> BaseType -> Type +data SomeSymFn sym = forall args ret . SomeSymFn (SymFn sym args ret)++-- | Wrapper for `SymFn` that concatenates the arguments and the return types.+--+-- This is useful for implementing `TestEquality` and `OrdF` instances for+-- `SymFn`, and for using `SymFn` as a key or a value in a `MapF`.+data SymFnWrapper sym ctx where+  SymFnWrapper :: forall sym args ret . SymFn sym args ret -> SymFnWrapper sym (args ::> ret)++instance IsSymFn (SymFn sym) => TestEquality (SymFnWrapper sym) where+  testEquality (SymFnWrapper fn1) (SymFnWrapper fn2) = fnTestEquality fn1 fn2++instance IsSymFn (SymFn sym) => OrdF (SymFnWrapper sym) where+  compareF (SymFnWrapper fn1) (SymFnWrapper fn2) = fnCompare fn1 fn2+ -- | A class for extracting type representatives from symbolic functions-class IsSymFn fn where+class IsSymFn (fn :: Ctx BaseType -> BaseType -> Type) where   -- | Get the argument types of a function.   fnArgTypes :: fn args ret -> Ctx.Assignment BaseTypeRepr args    -- | Get the return type of a function.   fnReturnType :: fn args ret -> BaseTypeRepr ret +  -- | Test whether two functions are equal.+  --+  -- The implementation may be incomplete, that is, if it returns `Just` then+  -- the functions are equal, while if it returns `Nothing` then the functions+  -- may or may not be equal. The result of `freshTotalUninterpFn` or+  -- `definedFn` tests equal with itself.+  fnTestEquality :: fn args1 ret1 -> fn args2 ret2 -> Maybe ((args1 ::> ret1) :~: (args2 ::> ret2)) +  -- | Compare two functions for ordering.+  --+  -- The underlying equality test is provided by `fnTestEquality`.+  fnCompare :: fn args1 ret1 -> fn args2 ret2 -> OrderingF (args1 ::> ret1) (args2 ::> ret2)++ -- | Describes when we unfold the body of defined functions. data UnfoldPolicy   = NeverUnfold@@ -2741,6 +2806,7 @@ class ( IsExprBuilder sym       , IsSymFn (SymFn sym)       , OrdF (SymExpr sym)+      , OrdF (BoundVar sym)       ) => IsSymExprBuilder sym where    ----------------------------------------------------------------------@@ -2885,6 +2951,22 @@              -> Ctx.Assignment (SymExpr sym) args                 -- ^ Arguments to function              -> IO (SymExpr sym ret)++  -- | Apply a variable substitution (variable to symbolic expression mapping)+  -- to a symbolic expression.+  substituteBoundVars ::+    sym ->+    MapF (BoundVar sym) (SymExpr sym) ->+    SymExpr sym tp ->+    IO (SymExpr sym tp)++  -- | Apply a function substitution (function to function mapping) to a+  -- symbolic expression.+  substituteSymFns ::+    sym ->+    MapF (SymFnWrapper sym) (SymFnWrapper sym) ->+    SymExpr sym tp ->+    IO (SymExpr sym tp)  -- | This returns true if the value corresponds to a concrete value. baseIsConcrete :: forall e bt

@@ -45,6 +45,7 @@   , useUnsatAssumptions   , useUninterpFunctions   , useDefinedFunctions+  , useProduceAbducts   , hasProblemFeature   ) where @@ -93,20 +94,20 @@  -- | Indicates whether the problem uses structs ----- Structs are modeled using constructors in CVC4/Z3, and tuples+-- Structs are modeled using constructors in CVC4/CVC5/Z3, and tuples -- in Yices. useStructs :: ProblemFeatures useStructs = ProblemFeatures 0x100  -- | Indicates whether the problem uses strings -----   Strings have some symbolic support in CVC4 and Z3.+--   Strings have some symbolic support in CVC4, CVC5, and Z3. useStrings :: ProblemFeatures useStrings = ProblemFeatures 0x200  -- | Indicates whether the problem uses floating-point -----   Floating-point has some symbolic support in CVC4 and Z3.+--   Floating-point has some symbolic support in CVC4, CVC5, and Z3. useFloatingPoint :: ProblemFeatures useFloatingPoint = ProblemFeatures 0x400 @@ -129,6 +130,11 @@ --   defined functions. useDefinedFunctions :: ProblemFeatures useDefinedFunctions = ProblemFeatures 0x4000++-- | Indicates if the solver is able and configured to +--   produce abducts.+useProduceAbducts :: ProblemFeatures+useProduceAbducts = ProblemFeatures 0x8000  -- | Tests if one set of problem features subsumes another. --   In particular, @hasProblemFeature x y@ is true iff

@@ -32,12 +32,15 @@   , reset   , inNewFrame   , inNewFrameWithVars+  , inNewFrame2Open+  , inNewFrame2Close   , check   , checkAndGetModel   , checkWithAssumptions   , checkWithAssumptionsAndModel   , getModel   , getUnsatCore+  , getAbducts   , getUnsatAssumptions   , getSatResult   , checkSatisfiable@@ -236,6 +239,39 @@         do assume conn p            check proc rsn +-- | @get-abuct nm t@ queries the solver for the first abduct, which is returned+--   as an SMT function definition named @nm@. The remaining abducts are obtained+--   from the solver by successive invocations of the @get-abduct-next@ command,+--   which return SMT functions bound to the same @nm@ as the first. The name @nm@+--   is bound within the current assertion frame.+--   Note that this is an unstable API; we expect that the return type will change +--   to a parsed expression in the future+getAbducts ::+  SMTReadWriter solver =>+  SolverProcess scope solver ->+  Int ->+  Text ->+  BoolExpr scope ->+  IO [String]+getAbducts proc n nm t =+  if (n > 0) then do +    let conn = solverConn proc+    unless (supportedFeatures conn `hasProblemFeature` useProduceAbducts) $+      fail $ show $ pretty (smtWriterName conn) <+> pretty "is not configured to produce abducts"+    f <- mkFormula conn t+    -- get the first abduct using the get-abduct command+    addCommandNoAck conn (getAbductCommand conn nm f)+    abd1 <- smtAbductResult conn conn nm f+    -- get the remaining abducts using get-abduct-next commands+    if (n > 1) then do+      let rest = n - 1+      abdRest <- forM [1..rest] $ \_ -> do+        addCommandNoAck conn (getAbductNextCommand conn)+        smtAbductNextResult conn conn+      return (abd1:abdRest)+    else return [abd1]+  else return []+ -- | Check if the formula is satisifiable in the current --   solver state.  This is done in a --   fresh frame, which is exited after the continuation@@ -326,6 +362,17 @@ -- | Perform an action in the scope of a solver assumption frame. inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver -> m a -> m a inNewFrame p action = inNewFrameWithVars p [] action++-- | Open a second solver assumption frame.+-- For abduction, we want the final assertion to be a in a new frame, so that it +-- can be closed before asking for abducts. The following two commands allow frame 2 +-- to be pushed and popped independently of other commands+inNewFrame2Open :: SMTReadWriter solver => SolverProcess scope solver -> IO ()+inNewFrame2Open sp = let c = solverConn sp in addCommand c (push2Command c)++-- | Close a second solver assumption frame.+inNewFrame2Close :: SMTReadWriter solver => SolverProcess scope solver -> IO ()+inNewFrame2Close sp = let c = solverConn sp in addCommand c (pop2Command c)  -- | Perform an action in the scope of a solver assumption frame, where the given -- bound variables are considered free within that frame.

@@ -19,6 +19,7 @@   , asAtomList   , asNegAtomList   , skipSpaceOrNewline+  , sExpToString   ) where  #if !MIN_VERSION_base(4,13,0)@@ -111,3 +112,8 @@   go (SAtom a:ys) = (a:) <$> go ys   go _ = Nothing asAtomList _ = Nothing++sExpToString :: SExp -> String+sExpToString (SAtom t) = Text.unpack t+sExpToString (SString t) = ('"' : Text.unpack t) ++ ['"']+sExpToString (SApp ss) = ('(' : Data.String.unwords (map sExpToString ss)) ++ [')']

@@ -15,9 +15,12 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-}@@ -38,7 +41,11 @@   , writeCheckSat   , writeExit   , writeGetValue+  , writeGetAbduct+  , writeGetAbductNext+  , writeCheckSynth   , runCheckSat+  , runGetAbducts   , asSMT2Type   , setOption   , getVersion@@ -48,10 +55,13 @@   , setProduceModels   , smtLibEvalFuns   , smtlib2Options+  , parseFnModel+  , parseFnValues     -- * Logic   , SMT2.Logic(..)   , SMT2.qf_bv   , SMT2.allSupported+  , SMT2.hornLogic   , all_supported   , setLogic     -- * Type@@ -66,6 +76,7 @@   , Session(..)   , SMTLib2GenericSolver(..)   , writeDefaultSMT2+  , defaultFileWriter   , startSolver   , shutdownSolver   , smtAckResult@@ -90,14 +101,21 @@  import           Control.Applicative import           Control.Exception-import           Control.Monad.State.Strict+import           Control.Monad.Except+import           Control.Monad.Reader+import qualified Data.Bimap as Bimap import qualified Data.BitVector.Sized as BV import           Data.Char (digitToInt, isAscii)+import           Data.HashMap.Lazy (HashMap)+import qualified Data.HashMap.Lazy as HashMap import           Data.IORef import           Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import           Data.Monoid+import           Data.Parameterized.Classes import qualified Data.Parameterized.Context as Ctx+import           Data.Parameterized.Map (MapF)+import qualified Data.Parameterized.Map as MapF import           Data.Parameterized.NatRepr import           Data.Parameterized.Pair import           Data.Parameterized.Some@@ -121,6 +139,7 @@ import           Data.Versions (Version(..)) import qualified Data.Versions as Versions import qualified Prettyprinter as PP+import           Text.Printf (printf) import           LibBF( bfToBits )  import           Prelude hiding (writeFile)@@ -149,8 +168,8 @@  -- | Set the logic to all supported logics. all_supported :: SMT2.Logic-all_supported = SMT2.allSupported-{-# DEPRECATED all_supported "Use allSupported" #-}+all_supported = SMT2.allLogic+{-# DEPRECATED all_supported "Use allLogic instead" #-}   smtlib2Options :: [CFG.ConfigDesc]@@ -676,6 +695,8 @@    pushCommand _  = SMT2.push 1   popCommand _   = SMT2.pop 1+  push2Command _ = SMT2.push 2+  pop2Command _ = SMT2.pop 2   resetCommand _ = SMT2.resetAssertions   popManyCommands _ n = [SMT2.pop (toInteger n)] @@ -684,6 +705,9 @@    getUnsatAssumptionsCommand _ = SMT2.getUnsatAssumptions   getUnsatCoreCommand _ = SMT2.getUnsatCore+  getAbductCommand _ nm e = SMT2.getAbduct nm e+  getAbductNextCommand _ = SMT2.getAbductNext+     setOptCommand _ = SMT2.setOption    declareCommand _proxy v argTypes retType =@@ -693,6 +717,11 @@     let resolveArg (var, Some tp) = (var, asSMT2Type @a tp)      in SMT2.defineFun f (resolveArg <$> args) (asSMT2Type @a return_type) e +  synthFunCommand _proxy f args ret_tp =+    SMT2.synthFun f (map (\(var, Some tp) -> (var, asSMT2Type @a tp)) args) (asSMT2Type @a ret_tp)+  declareVarCommand _proxy v tp = SMT2.declareVar v (asSMT2Type @a tp)+  constraintCommand _proxy e = SMT2.constraint e+   stringTerm str = smtlib2StringTerm @a str   stringLength x = smtlib2StringLength @a x   stringAppend xs = smtlib2StringAppend @a xs@@ -755,6 +784,16 @@ writeGetValue :: SMTLib2Tweaks a => WriterConn t (Writer a) -> [Term] -> IO () writeGetValue w l = addCommandNoAck w $ SMT2.getValue l +writeGetAbduct :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Term -> IO ()+writeGetAbduct w nm p = addCommandNoAck w $ SMT2.getAbduct nm p++writeGetAbductNext :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()+writeGetAbductNext w = addCommandNoAck w SMT2.getAbductNext++-- | Write check-synth command+writeCheckSynth :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()+writeCheckSynth w = addCommandNoAck w SMT2.checkSynth+ parseBoolSolverValue :: MonadFail m => SExp -> m Bool parseBoolSolverValue (SAtom "true")  = return True parseBoolSolverValue (SAtom "false") = return False@@ -762,6 +801,16 @@   do v <- parseBvSolverValue (knownNat @1) s      return (if v == BV.zero knownNat then False else True) +parseIntSolverValue :: MonadFail m => SExp -> m Integer+parseIntSolverValue = \case+  SAtom v+    | [(i, "")] <- readDec (Text.unpack v) ->+      return i+  SApp ["-", x] ->+    negate <$> parseIntSolverValue x+  s ->+    fail $ "Could not parse solver value: " ++ show s+ parseRealSolverValue :: MonadFail m => SExp -> m Rational parseRealSolverValue (SAtom v) | Just (r,"") <- readDecimal (Text.unpack v) =   return r@@ -778,10 +827,11 @@ -- of the variable. parseBvSolverValue :: MonadFail m => NatRepr w -> SExp -> m (BV.BV w) parseBvSolverValue w s-  | Pair w' bv <- parseBVLitHelper s = case w' `compareNat` w of+  | Just (Pair w' bv) <- parseBVLitHelper s = case w' `compareNat` w of       NatLT zw -> return (BV.zext (addNat w' (addNat zw knownNat)) bv)       NatEQ -> return bv       NatGT _ -> return (BV.trunc w bv)+  | otherwise = fail $ "Could not parse bitvector solver value: " ++ show s  natBV :: Natural       -- ^ width@@ -792,15 +842,14 @@   Some w -> Pair w (BV.mkBV w x)  -- | Parse an s-expression and return a bitvector and its width-parseBVLitHelper :: SExp -> Pair NatRepr BV.BV+parseBVLitHelper :: SExp -> Maybe (Pair NatRepr BV.BV) parseBVLitHelper (SAtom (Text.unpack -> ('#' : 'b' : n_str))) | [(n, "")] <- readBin n_str =-  natBV (fromIntegral (length n_str)) n+  Just $ natBV (fromIntegral (length n_str)) n parseBVLitHelper (SAtom (Text.unpack -> ('#' : 'x' : n_str))) | [(n, "")] <- readHex n_str =-  natBV (fromIntegral (length n_str * 4)) n+  Just $ natBV (fromIntegral (length n_str * 4)) n parseBVLitHelper (SApp ["_", SAtom (Text.unpack -> ('b' : 'v' : n_str)), SAtom (Text.unpack -> w_str)])-  | [(n, "")] <- readDec n_str, [(w, "")] <- readDec w_str = natBV w n--- BGS: Is this correct?-parseBVLitHelper _ = natBV 0 0+  | [(n, "")] <- readDec n_str, [(w, "")] <- readDec w_str = Just $ natBV w n+parseBVLitHelper _ = Nothing  parseStringSolverValue :: MonadFail m => SExp -> m Text parseStringSolverValue (SString t) | Just t' <- unescapeText t = return t'@@ -831,10 +880,10 @@  parseFloatLitHelper :: MonadFail m => SExp -> m ParsedFloatResult parseFloatLitHelper (SApp ["fp", sign_s, expt_s, scand_s])-  | Pair sign_w sign <- parseBVLitHelper sign_s+  | Just (Pair sign_w sign) <- parseBVLitHelper sign_s   , Just Refl <- sign_w `testEquality` (knownNat @1)-  , Pair eb expt <- parseBVLitHelper expt_s-  , Pair sb scand <- parseBVLitHelper scand_s+  , Just (Pair eb expt) <- parseBVLitHelper expt_s+  , Just (Pair sb scand) <- parseBVLitHelper scand_s   = return $ ParsedFloatResult sign eb expt sb scand parseFloatLitHelper   s@(SApp ["_", SAtom (Text.unpack -> nm), SAtom (Text.unpack -> eb_s), SAtom (Text.unpack -> sb_s)])@@ -870,6 +919,341 @@     _ -> return Nothing parseBvArraySolverValue _ _ _ = return Nothing +parseFnModel ::+  sym ~ B.ExprBuilder t st fs  =>+  sym ->+  WriterConn t h ->+  [I.SomeSymFn sym] ->+  SExp ->+  IO (MapF (I.SymFnWrapper sym) (I.SymFnWrapper sym))+parseFnModel = parseFns parseDefineFun++parseFnValues ::+  sym ~ B.ExprBuilder t st fs  =>+  sym ->+  WriterConn t h ->+  [I.SomeSymFn sym] ->+  SExp ->+  IO (MapF (I.SymFnWrapper sym) (I.SymFnWrapper sym))+parseFnValues = parseFns parseLambda++parseFns ::+  sym ~ B.ExprBuilder t st fs =>+  (sym -> SExp -> IO (Text, I.SomeSymFn sym)) ->+  sym ->+  WriterConn t h ->+  [I.SomeSymFn sym] ->+  SExp ->+  IO (MapF (I.SymFnWrapper sym) (I.SymFnWrapper sym))+parseFns parse_model_fn sym conn uninterp_fns sexp = do+  fn_name_bimap <- cacheLookupFnNameBimap conn $ map (\(I.SomeSymFn fn) -> B.SomeExprSymFn fn) uninterp_fns+  defined_fns <- case sexp of+    SApp sexps -> Map.fromList <$> mapM (parse_model_fn sym) sexps+    _ -> fail $ "Could not parse model response: " ++ show sexp+  MapF.fromList <$> mapM+    (\(I.SomeSymFn uninterp_fn) -> if+      | Just nm <- Bimap.lookup (B.SomeExprSymFn uninterp_fn) fn_name_bimap+      , Just (I.SomeSymFn defined_fn) <- Map.lookup nm defined_fns+      , Just Refl <- testEquality (I.fnArgTypes uninterp_fn) (I.fnArgTypes defined_fn)+      , Just Refl <- testEquality (I.fnReturnType uninterp_fn) (I.fnReturnType defined_fn) ->+        return $ MapF.Pair (I.SymFnWrapper uninterp_fn) (I.SymFnWrapper defined_fn)+      | otherwise -> fail $ "Could not find model for function: " ++ show uninterp_fn)+    uninterp_fns++parseDefineFun :: I.IsSymExprBuilder sym => sym -> SExp -> IO (Text, I.SomeSymFn sym)+parseDefineFun sym sexp = case sexp of+  SApp ["define-fun", SAtom nm, SApp params_sexp, _ret_type_sexp , body_sexp] -> do+    fn <- parseFn sym nm params_sexp body_sexp+    return (nm, fn)+  _ -> fail $ "unexpected sexp, expected define-fun, found " ++ show sexp++parseLambda :: I.IsSymExprBuilder sym => sym -> SExp -> IO (Text, I.SomeSymFn sym)+parseLambda sym sexp = case sexp of+  SApp [SAtom nm, SApp ["lambda", SApp params_sexp, body_sexp]] -> do+    fn <- parseFn sym nm params_sexp body_sexp+    return (nm, fn)+  _ -> fail $ "unexpected sexp, expected lambda, found " ++ show sexp++parseFn :: I.IsSymExprBuilder sym => sym -> Text -> [SExp] -> SExp -> IO (I.SomeSymFn sym)+parseFn sym nm params_sexp body_sexp = do+  (nms, vars) <- unzip <$> mapM (parseVar sym) params_sexp+  case Ctx.fromList vars of+    Some vars_assign -> do+      let let_env = HashMap.fromList $ zip nms $ map (mapSome $ I.varExpr sym) vars+      proc_res <- runProcessor (ProcessorEnv { procSym = sym, procLetEnv = let_env }) $ parseExpr sym body_sexp+      Some body_expr <- either fail return proc_res+      I.SomeSymFn <$> I.definedFn sym (I.safeSymbol $ Text.unpack nm) vars_assign body_expr I.NeverUnfold++parseVar :: I.IsSymExprBuilder sym => sym -> SExp -> IO (Text, Some (I.BoundVar sym))+parseVar sym sexp = case sexp of+  SApp [SAtom nm, tp_sexp] -> do+    Some tp <- parseType tp_sexp+    var <- liftIO $ I.freshBoundVar sym (I.safeSymbol $ Text.unpack nm) tp+    return (nm, Some var)+  _ -> fail $ "unexpected variable " ++ show sexp++parseType :: SExp -> IO (Some BaseTypeRepr)+parseType sexp = case sexp of+  "Bool" -> return $ Some BaseBoolRepr+  "Int" -> return $ Some BaseIntegerRepr+  "Real" -> return $ Some BaseRealRepr+  SApp ["_", "BitVec", SAtom (Text.unpack -> m_str)]+    | [(m_n, "")] <- readDec m_str+    , Some m <- mkNatRepr m_n+    , Just LeqProof <- testLeq (knownNat @1) m ->+      return $ Some $ BaseBVRepr m+  SApp ["_", "FloatingPoint", SAtom (Text.unpack -> eb_str), SAtom (Text.unpack -> sb_str)]+    | [(eb_n, "")] <- readDec eb_str+    , Some eb <- mkNatRepr eb_n+    , Just LeqProof <- testLeq (knownNat @2) eb+    , [(sb_n, "")] <- readDec sb_str+    , Some sb <- mkNatRepr sb_n+    , Just LeqProof <- testLeq (knownNat @2) sb ->+      return $ Some $ BaseFloatRepr $ FloatingPointPrecisionRepr eb sb+  SApp ["Array", idx_tp_sexp, val_tp_sexp] -> do+    Some idx_tp <- parseType idx_tp_sexp+    Some val_tp <- parseType val_tp_sexp+    return $ Some $ BaseArrayRepr (Ctx.singleton idx_tp) val_tp+  _ -> fail $ "unexpected type " ++ show sexp+++-- | Stores a NatRepr along with proof that its type parameter is a bitvector of+-- that length. Used for easy pattern matching on the LHS of a binding in a+-- do-expression to extract the proof.+data BVProof tp where+  BVProof :: forall n . (1 <= n) => NatRepr n -> BVProof (BaseBVType n)++-- | Given an expression, monadically either returns proof that it is a+-- bitvector or throws an error.+getBVProof :: (I.IsExpr ex, MonadError String m) => ex tp -> m (BVProof tp)+getBVProof expr = case I.exprType expr of+  BaseBVRepr n -> return $ BVProof n+  t -> throwError $ "expected BV, found " ++ show t++-- | Operator type descriptions for parsing s-expression of+-- the form @(operator operands ...)@.+--+-- Code is copy-pasted and adapted from `What4.Serialize.Parser`, see+-- <https://github.com/GaloisInc/what4/issues/228>+data Op sym where+    -- | Generic unary operator description.+    Op1 ::+      Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1) ->+      (sym -> I.SymExpr sym arg1 -> IO (I.SymExpr sym ret)) ->+      Op sym+    -- | Generic binary operator description.+    Op2 ::+      Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2) ->+      Maybe Assoc ->+      (sym -> I.SymExpr sym arg1 -> I.SymExpr sym arg2 -> IO (I.SymExpr sym ret)) ->+      Op sym+    -- | Encapsulating type for a unary operation that takes one bitvector and+    -- returns another (in IO).+    BVOp1 ::+      (forall w . (1 <= w) => sym -> I.SymBV sym w -> IO (I.SymBV sym w)) ->+      Op sym+    -- | Binop with a bitvector return type, e.g., addition or bitwise operations.+    BVOp2 ::+      Maybe Assoc ->+      (forall w . (1 <= w) => sym -> I.SymBV sym w -> I.SymBV sym w -> IO (I.SymBV sym w)) ->+      Op sym+    -- | Bitvector binop with a boolean return type, i.e., comparison operators.+    BVComp2 ::+      (forall w . (1 <= w) => sym -> I.SymBV sym w -> I.SymBV sym w -> IO (I.Pred sym)) ->+      Op sym++data Assoc = RightAssoc | LeftAssoc++newtype Processor sym a = Processor (ExceptT String (ReaderT (ProcessorEnv sym) IO) a)+  deriving (Functor, Applicative, Monad, MonadIO, MonadError String, MonadReader (ProcessorEnv sym))++data ProcessorEnv sym = ProcessorEnv+  { procSym :: sym+  , procLetEnv :: HashMap Text (Some (I.SymExpr sym))+  }++runProcessor :: ProcessorEnv sym -> Processor sym a -> IO (Either String a)+runProcessor env (Processor action) = runReaderT (runExceptT action) env++opTable :: I.IsSymExprBuilder sym => HashMap Text (Op sym)+opTable = HashMap.fromList+  -- Boolean ops+  [ ("not", Op1 knownRepr I.notPred)+  , ("=>", Op2 knownRepr (Just RightAssoc) I.impliesPred)+  , ("and", Op2 knownRepr (Just LeftAssoc) I.andPred)+  , ("or", Op2 knownRepr (Just LeftAssoc) I.orPred)+  , ("xor", Op2 knownRepr (Just LeftAssoc) I.xorPred)+  -- Integer ops+  , ("-", Op2 knownRepr (Just LeftAssoc) I.intSub)+  , ("+", Op2 knownRepr (Just LeftAssoc) I.intAdd)+  , ("*", Op2 knownRepr (Just LeftAssoc) I.intMul)+  , ("div", Op2 knownRepr (Just LeftAssoc) I.intDiv)+  , ("mod", Op2 knownRepr Nothing I.intMod)+  , ("abs", Op1 knownRepr I.intAbs)+  , ("<=", Op2 knownRepr Nothing I.intLe)+  , ("<", Op2 knownRepr Nothing I.intLt)+  , (">=", Op2 knownRepr Nothing $ \sym arg1 arg2 -> I.intLe sym arg2 arg1)+  , (">", Op2 knownRepr Nothing $ \sym arg1 arg2 -> I.intLt sym arg2 arg1)+  -- Bitvector ops+  , ("bvnot", BVOp1 I.bvNotBits)+  , ("bvneg", BVOp1 I.bvNeg)+  , ("bvand", BVOp2 (Just LeftAssoc) I.bvAndBits)+  , ("bvor", BVOp2 (Just LeftAssoc) I.bvOrBits)+  , ("bvxor", BVOp2 (Just LeftAssoc) I.bvXorBits)+  , ("bvadd", BVOp2 (Just LeftAssoc) I.bvAdd)+  , ("bvsub", BVOp2 (Just LeftAssoc) I.bvSub)+  , ("bvmul", BVOp2 (Just LeftAssoc) I.bvMul)+  , ("bvudiv", BVOp2 Nothing I.bvUdiv)+  , ("bvurem", BVOp2 Nothing I.bvUrem)+  , ("bvshl", BVOp2 Nothing I.bvShl)+  , ("bvlshr", BVOp2 Nothing I.bvLshr)+  , ("bvsdiv", BVOp2 Nothing I.bvSdiv)+  , ("bvsrem", BVOp2 Nothing I.bvSrem)+  , ("bvashr", BVOp2 Nothing I.bvAshr)+  , ("bvult", BVComp2 I.bvUlt)+  , ("bvule", BVComp2 I.bvUle)+  , ("bvugt", BVComp2 I.bvUgt)+  , ("bvuge", BVComp2 I.bvUge)+  , ("bvslt", BVComp2 I.bvSlt)+  , ("bvsle", BVComp2 I.bvSle)+  , ("bvsgt", BVComp2 I.bvSgt)+  , ("bvsge", BVComp2 I.bvSge)+  ]++parseExpr ::+  forall sym . I.IsSymExprBuilder sym => sym -> SExp -> Processor sym (Some (I.SymExpr sym))+parseExpr sym sexp = case sexp of+  "true" -> return $ Some $ I.truePred sym+  "false" -> return $ Some $ I.falsePred sym+  _ | Just i <- parseIntSolverValue sexp ->+      liftIO $ Some <$> I.intLit sym i+    | Just (Pair w bv) <- parseBVLitHelper sexp+    , Just LeqProof <- testLeq (knownNat @1) w ->+      liftIO $ Some <$> I.bvLit sym w bv+  SAtom nm -> do+    env <- asks procLetEnv+    case HashMap.lookup nm env of+      Just expr -> return $ expr+      Nothing -> throwError ""+  SApp ["let", SApp bindings_sexp, body_sexp] -> do+    let_env <- HashMap.fromList <$> mapM+      (\case+        SApp [SAtom nm, expr_sexp] -> do+          Some expr <- parseExpr sym expr_sexp+          return (nm, Some expr)+        _ -> throwError "")+      bindings_sexp+    local (\prov_env -> prov_env { procLetEnv = HashMap.union let_env (procLetEnv prov_env) }) $+      parseExpr sym body_sexp+  SApp ["=", arg1, arg2] -> do+    Some arg1_expr <- parseExpr sym arg1+    Some arg2_expr <- parseExpr sym arg2+    case testEquality (I.exprType arg1_expr) (I.exprType arg2_expr) of+      Just Refl -> liftIO (Some <$> I.isEq sym arg1_expr arg2_expr)+      Nothing -> throwError ""+  SApp ["ite", arg1, arg2, arg3] -> do+    Some arg1_expr <- parseExpr sym arg1+    Some arg2_expr <- parseExpr sym arg2+    Some arg3_expr <- parseExpr sym arg3+    case I.exprType arg1_expr of+      I.BaseBoolRepr -> case testEquality (I.exprType arg2_expr) (I.exprType arg3_expr) of+        Just Refl -> liftIO (Some <$> I.baseTypeIte sym arg1_expr arg2_expr arg3_expr)+        Nothing -> throwError ""+      _ -> throwError ""+  SApp ["concat", arg1, arg2] -> do+    Some arg1_expr <- parseExpr sym arg1+    Some arg2_expr <- parseExpr sym arg2+    BVProof{} <- getBVProof arg1_expr+    BVProof{} <- getBVProof arg2_expr+    liftIO $ Some <$> I.bvConcat sym arg1_expr arg2_expr+  SApp ((SAtom operator) : operands) -> case HashMap.lookup operator (opTable @sym) of+    Just (Op1 arg_types fn) -> do+      args <- mapM (parseExpr sym) operands+      exprAssignment arg_types args >>= \case+        Ctx.Empty Ctx.:> arg1 ->+          liftIO (Some <$> fn sym arg1)+    Just (Op2 arg_types _ fn) -> do+      args <- mapM (parseExpr sym) operands+      exprAssignment arg_types args >>= \case+        Ctx.Empty Ctx.:> arg1 Ctx.:> arg2 ->+            liftIO (Some <$> fn sym arg1 arg2)+    Just (BVOp1 op) -> do+      Some arg_expr <- readOneArg sym operands+      BVProof{} <- getBVProof arg_expr+      liftIO $ Some <$> op sym arg_expr+    Just (BVOp2 _ op) -> do+      (Some arg1, Some arg2) <- readTwoArgs sym operands+      BVProof m <- prefixError "in arg 1: " $ getBVProof arg1+      BVProof n <- prefixError "in arg 2: " $ getBVProof arg2+      case testEquality m n of+        Just Refl -> liftIO (Some <$> op sym arg1 arg2)+        Nothing -> throwError $ printf "arguments to %s must be the same length, \+                                       \but arg 1 has length %s \+                                       \and arg 2 has length %s"+                                       operator+                                       (show m)+                                       (show n)+    Just (BVComp2 op) -> do+      (Some arg1, Some arg2) <- readTwoArgs sym operands+      BVProof m <- prefixError "in arg 1: " $ getBVProof arg1+      BVProof n <- prefixError "in arg 2: " $ getBVProof arg2+      case testEquality m n of+        Just Refl -> liftIO (Some <$> op sym arg1 arg2)+        Nothing -> throwError $ printf "arguments to %s must be the same length, \+                                       \but arg 1 has length %s \+                                       \and arg 2 has length %s"+                                       operator+                                       (show m)+                                       (show n)+    _ -> throwError ""+  _ -> throwError ""+-- | Verify a list of arguments has a single argument and+-- return it, else raise an error.+readOneArg ::+  I.IsSymExprBuilder sym+  => sym+  -> [SExp]+  -> Processor sym (Some (I.SymExpr sym))+readOneArg sym operands = do+  args <- mapM (parseExpr sym) operands+  case args of+    [arg] -> return arg+    _ -> throwError $ printf "expecting 1 argument, got %d" (length args)++-- | Verify a list of arguments has two arguments and return+-- it, else raise an error.+readTwoArgs ::+  I.IsSymExprBuilder sym+  => sym+  ->[SExp]+  -> Processor sym (Some (I.SymExpr sym), Some (I.SymExpr sym))+readTwoArgs sym operands = do+  args <- mapM (parseExpr sym) operands+  case args of+    [arg1, arg2] -> return (arg1, arg2)+    _ -> throwError $ printf "expecting 2 arguments, got %d" (length args)++exprAssignment ::+  forall sym ctx ex . (I.IsSymExprBuilder sym, I.IsExpr ex)+  => Ctx.Assignment BaseTypeRepr ctx+  -> [Some ex]+  -> Processor sym (Ctx.Assignment ex ctx)+exprAssignment tpAssns exs = do+  Some exsAsn <- return $ Ctx.fromList exs+  exsRepr <- return $ fmapFC I.exprType exsAsn+  case testEquality exsRepr tpAssns of+    Just Refl -> return exsAsn+    Nothing -> throwError $+      "Unexpected expression types for " -- ++ show exsAsn+      ++ "\nExpected: " ++ show tpAssns+      ++ "\nGot: " ++ show exsRepr++-- | Utility function for contextualizing errors. Prepends the given prefix+-- whenever an error is thrown.+prefixError :: (Monoid e, MonadError e m) => e -> m a -> m a+prefixError prefix act = catchError act (throwError . mappend prefix)++ ------------------------------------------------------------------------ -- Session @@ -891,6 +1275,32 @@         _ -> Nothing   getLimitedSolverResponse "get value" valRsp (sessionWriter s) (SMT2.getValue [e]) +-- | runGetAbducts s nm p n, returns n formulas (as strings) the disjunction of which entails p (along with all+--   the assertions in the context)+runGetAbducts :: SMTLib2Tweaks a+             => Session t a+             -> Int+             -> Text+             -> Term+             -> IO [String]+runGetAbducts s n nm p = +  if (n > 0) then do+    writeGetAbduct (sessionWriter s) nm p+    let valRsp = \x -> case x of+          -- SMT solver returns `(define-fun nm () Bool X)` where X is the abduct, we discard everything but the abduct+          AckSuccessSExp (SApp (_ : _ : _ : _ : abduct)) -> Just $ Data.String.unwords (map sExpToString abduct)+          _ -> Nothing+    -- get first abduct using the get-abduct command+    abd1 <- getLimitedSolverResponse "get abduct" valRsp (sessionWriter s) (SMT2.getAbduct nm p)+    if (n > 1) then do+      let rest = n - 1+      replicateM_ rest $ writeGetAbductNext (sessionWriter s)+      -- get the rest of the abducts using the get-abduct-next command+      abdRest <- forM [1..rest] $ \_ -> getLimitedSolverResponse "get abduct next" valRsp (sessionWriter s) (SMT2.getAbduct nm p)+      return (abd1:abdRest)+    else return [abd1]+  else return []+ -- | This function runs a check sat command runCheckSat :: forall b t a.                SMTLib2Tweaks b@@ -938,7 +1348,21 @@         cmd = getUnsatCoreCommand p     in getLimitedSolverResponse "unsat core" unsatCoreRsp s cmd +  smtAbductResult p s nm t =+    let abductRsp = \case+          AckSuccessSExp (SApp (_ : _ : _ : _ : abduct)) -> Just $ Data.String.unwords (map sExpToString abduct)+          _ -> Nothing+        cmd = getAbductCommand p nm t+    in getLimitedSolverResponse "get abduct" abductRsp s cmd +  smtAbductNextResult p s =+    let abductRsp = \case+          AckSuccessSExp (SApp (_ : _ : _ : _ : abduct)) -> Just $ Data.String.unwords (map sExpToString abduct)+          _ -> Nothing+        cmd = getAbductNextCommand p+    in getLimitedSolverResponse "get abduct next" abductRsp s cmd++ smtAckResult :: AcknowledgementAction t (Writer a) smtAckResult = AckAction $ getLimitedSolverResponse "get ack" $ \case                  AckSuccess -> Just ()@@ -1091,16 +1515,28 @@                  -> [B.BoolExpr t]                  -> IO () writeDefaultSMT2 a nm feat strictOpt sym h ps = do+  c <- defaultFileWriter a nm feat strictOpt sym h+  setProduceModels c True+  forM_ ps (SMTWriter.assume c)+  writeCheckSat c+  writeExit c++defaultFileWriter ::+  SMTLib2Tweaks a =>+  a ->+  String ->+  ProblemFeatures ->+  Maybe (CFG.ConfigOption I.BaseBoolType) ->+  B.ExprBuilder t st fs ->+  IO.Handle ->+  IO (WriterConn t (Writer a))+defaultFileWriter a nm feat strictOpt sym h = do   bindings <- B.getSymbolVarBimap sym   str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h   null_in <- Streams.nullInput   let cfg = I.getConfiguration sym   strictness <- parserStrictness strictOpt 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-  writeExit c+  newWriter a str null_in nullAcknowledgementAction strictness nm True feat True bindings  -- n.b. commonly used for the startSolverProcess method of the -- OnlineSolver class, so it's helpful for the type suffixes to align

@@ -17,7 +17,7 @@   ( -- * CheckSatResponse     CheckSatResponse(..)   , readCheckSatResponse-    -- * GetModelResonse+    -- * GetModelResponse   , GetModelResponse   , readGetModelResponse   , ModelResponse(..)

@@ -71,6 +71,8 @@                  | AckSat                  | AckUnsat                  | AckUnknown+                 | AckInfeasible -- SyGuS response+                 | AckFail -- SyGuS response                  | RspName Text                  | RspVersion Text                  | RspErrBehavior Text@@ -144,10 +146,12 @@       parens p = AT.char '(' *> p <* AT.char ')'       errParser = parens $ lexeme (AT.string "error")                   *> (AckError <$> lexeme parseSMTLib2String)-      specific_success_response = check_sat_response <|> get_info_response+      specific_success_response = check_sat_response <|> check_synth_response <|> get_info_response       check_sat_response = (AckSat <$ AT.string "sat")                            <|> (AckUnsat <$ AT.string "unsat")                            <|> (AckUnknown <$ AT.string "unknown")+      check_synth_response = (AckInfeasible <$ AT.string "infeasible")+                             <|> (AckFail <$ AT.string "fail")       get_info_response = parens info_response       info_response = errBhvParser                       <|> nameParser

@@ -49,10 +49,19 @@   , assertNamed   , getUnsatAssumptions   , getUnsatCore+  , getAbduct+  , getAbductNext+    -- * SyGuS+  , synthFun+  , declareVar+  , constraint+  , checkSynth     -- * Logic   , Logic(..)   , qf_bv   , allSupported+  , allLogic+  , hornLogic     -- * Sort   , Sort(..)   , boolSort@@ -184,7 +193,16 @@ -- | Set the logic to all supported logics. allSupported :: Logic allSupported = Logic "ALL_SUPPORTED"+{-# DEPRECATED allSupported "Use allLogic instead" #-} +-- | Set the logic to all supported logics.+allLogic :: Logic+allLogic = Logic "ALL"++-- | Use the Horn logic+hornLogic :: Logic+hornLogic = Logic "HORN"+ ------------------------------------------------------------------------ -- Symbol @@ -290,7 +308,7 @@ or [x] = x or l = term_app "or" l --- | Disjunction of all terms+-- | Xor of all terms xor :: [Term] -> Term xor l@(_:_:_) = term_app "xor" l xor _ = error "xor expects two or more arguments."@@ -299,7 +317,7 @@ eq :: [Term] -> Term eq = chain_app "=" --- | Construct a chainable term with the givne relation+-- | Construct a chainable term with the given relation -- -- @pairwise_app p [x1, x2, ..., xn]@ is equivalent to -- \forall_{i,j} p x_i x_j@.@@ -480,7 +498,7 @@ -- value type `t2` that always returns `c`. -- -- This uses the non-standard SMTLIB2 syntax--- @((as const (Array t1 t2)) c)@ which is supported by CVC4 and Z3+-- @((as const (Array t1 t2)) c)@ which is supported by CVC4, CVC5, and Z3 -- (and perhaps others). arrayConst :: Sort -> Sort -> Term -> Term arrayConst itp rtp c =@@ -819,6 +837,37 @@  getUnsatCore :: Command getUnsatCore = Cmd "(get-unsat-core)"++-- | Get an abduct that entails the formula, and bind it to the name+getAbduct :: Text -> Term -> Command+getAbduct nm p = Cmd $ "(get-abduct " <> Builder.fromText nm <> " " <> renderTerm p <> ")"++-- | Get the next command, called after a get-abduct command+getAbductNext :: Command+getAbductNext = Cmd "(get-abduct-next)"++-- | Declare a SyGuS function to synthesize with the given name, arguments, and+-- return type.+synthFun :: Text -> [(Text, Sort)] -> Sort -> Command+synthFun f args ret_tp = Cmd $ app "synth-fun"+  [ Builder.fromText f+  , builder_list $ map (\(var, tp) -> app (Builder.fromText var) [unSort tp]) args+  , unSort ret_tp+  ]++-- | Declare a SyGuS variable with the given name and type.+declareVar :: Text -> Sort -> Command+declareVar v tp = Cmd $ app "declare-var" [Builder.fromText v, unSort tp]++-- | Add the SyGuS constraint to the current synthesis problem.+constraint :: Term -> Command+constraint p = Cmd $ app "constraint" [renderTerm p]++-- | Ask the SyGuS solver to find a solution for the synthesis problem+-- corresponding to the current functions-to-synthesize, variables and+-- constraints.+checkSynth :: Command+checkSynth = Cmd "(check-synth)\n"  -- | Get the values associated with the terms from the last call to @check-sat@. getValue :: [Term] -> Command

@@ -69,6 +69,7 @@   , entryStackHeight   , pushEntryStack   , popEntryStack+  , cacheLookupFnNameBimap   , Command   , addCommand   , addCommandNoAck@@ -86,6 +87,10 @@   , ResponseStrictness(..)   , parserStrictness   , nullAcknowledgementAction+    -- * SyGuS+  , addSynthFun+  , addDeclareVar+  , addConstraint     -- * SMTWriter operations   , assume   , mkSMTTerm@@ -111,6 +116,8 @@ import           Control.Monad.ST import           Control.Monad.State.Strict import           Control.Monad.Trans.Maybe+import           Data.Bimap (Bimap)+import qualified Data.Bimap as Bimap import qualified Data.BitVector.Sized as BV import qualified Data.Bits as Bits import           Data.IORef@@ -820,6 +827,15 @@ cacheValueFn conn n lifetime value = cacheValue conn lifetime $ \entry ->   stToIO $ PH.insert (symFnCache entry) n value +cacheLookupFnNameBimap :: WriterConn t h -> [SomeExprSymFn t] -> IO (Bimap (SomeExprSymFn t) Text)+cacheLookupFnNameBimap conn fns = Bimap.fromList <$> mapM+  (\some_fn@(SomeExprSymFn fn) -> do+    maybe_smt_sym_fn <- cacheLookupFn conn $ symFnId fn+    case maybe_smt_sym_fn of+      Just (SMTSymFn nm _ _) -> return (some_fn, nm)+      Nothing -> fail $ "Could not find function in cache: " ++ show fn)+  fns+ -- | Run state with handle. withWriterState :: WriterConn t h -> State WriterState a -> IO a withWriterState c m = do@@ -867,12 +883,18 @@   --   later reporting unsatisfiable cores).   assertNamedCommand :: f h -> Term h -> Text -> Command h -  -- | Push 1 new scope+  -- | Generates command @(push 1)@ that opens the corresponding assertion frame   pushCommand   :: f h -> Command h -  -- | Pop 1 existing scope+  -- | Generates command @(pop 1)@ that closes the corresponding assertion frame   popCommand    :: f h -> Command h +  -- | Generates command @(push 2)@ that opens the corresponding assertion frame+  push2Command   :: f h -> Command h++  -- | Generates command @(pop 2)@ that closes the corresponding assertion frame, used for abduction+  pop2Command    :: f h -> Command h+   -- | Pop several scopes.   popManyCommands :: f h -> Int -> [Command h]   popManyCommands w n = replicate n (popCommand w)@@ -898,6 +920,12 @@   --   `checkCommand`.   getUnsatCoreCommand :: f h -> Command h +  -- | Ask the solver to return an abduct+  getAbductCommand :: f h -> Text -> Term h -> Command h++  -- | Ask the solver for the next abduct, used after a get-abduct command+  getAbductNextCommand :: f h -> Command h+   -- | Set an option/parameter.   setOptCommand :: f h -> Text -> Text -> Command h @@ -919,6 +947,23 @@                 -> Term h                 -> Command h +  -- | Declare a new SyGuS function to synthesize with the given name,+  -- arguments, and result type.+  synthFunCommand :: f h+                  -> Text+                  -> [(Text, Some TypeMap)]+                  -> TypeMap tp+                  -> Command h++  -- | Declare a new SyGuS universal variables with the given name and type.+  declareVarCommand :: f h+                    -> Text+                    -> TypeMap tp+                    -> Command h++  -- | Add a SyGuS formula to the set of synthesis constraints.+  constraintCommand :: f h -> Term h -> Command h+   -- | Declare a struct datatype if is has not been already given the number of   -- arguments in the struct.   declareStructDatatype :: WriterConn t h -> Ctx.Assignment TypeMap args -> IO ()@@ -1042,6 +1087,63 @@      assumeFormulaWithName conn p var      return var +addSynthFun ::+  SMTWriter h =>+  WriterConn t h ->+  ExprSymFn t args ret ->+  IO ()+addSynthFun conn fn =+  cacheLookupFn conn (symFnId fn) >>= \case+    Just{} ->+      fail $ "Internal error in SMTLIB exporter: function already declared."+        ++ show (symFnId fn) ++ " declared at "+        ++ show (plSourceLoc (symFnLoc fn)) ++ "."+    Nothing -> case symFnInfo fn of+      UninterpFnInfo arg_types ret_type -> do+        nm <- getSymbolName conn (FnSymbolBinding fn)+        let fn_source = fnSource (symFnName fn) (symFnLoc fn)+        smt_arg_types <- traverseFC (evalFirstClassTypeRepr conn fn_source) arg_types+        checkArgumentTypes conn smt_arg_types+        smt_ret_type <- evalFirstClassTypeRepr conn fn_source ret_type+        traverseFC_ (declareTypes conn) smt_arg_types+        declareTypes conn smt_ret_type+        smt_args <- mapM+          (\(Some tp) -> do+            var <- withWriterState conn $ freshVarName+            return (var, Some tp))+          (toListFC Some smt_arg_types)+        addCommand conn $ synthFunCommand conn nm smt_args smt_ret_type+        cacheValueFn conn (symFnId fn) DeleteNever $! SMTSymFn nm smt_arg_types smt_ret_type+      DefinedFnInfo{} ->+        fail $ "Internal error in SMTLIB exporter: defined functions cannot be synthesized."+      MatlabSolverFnInfo{} ->+        fail $ "Internal error in SMTLIB exporter: MatlabSolver functions cannot be synthesized."++addDeclareVar ::+  SMTWriter h =>+  WriterConn t h ->+  ExprBoundVar t tp ->+  IO ()+addDeclareVar conn var =+  cacheLookupExpr conn (bvarId var) >>= \case+    Just{} ->+      fail $ "Internal error in SMTLIB exporter: variable already declared."+        ++ show (bvarId var) ++ " declared at "+        ++ show (plSourceLoc (bvarLoc var)) ++ "."+    Nothing -> do+      nm <- getSymbolName conn (VarSymbolBinding var)+      let fn_source = fnSource (bvarName var) (bvarLoc var)+      smt_type <- evalFirstClassTypeRepr conn fn_source $ bvarType var+      declareTypes conn smt_type+      addCommand conn $ declareVarCommand conn nm smt_type+      cacheValueExpr conn (bvarId var) DeleteNever $! SMTName smt_type nm++addConstraint :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()+addConstraint conn p = do+  f <- mkFormula conn p+  updateProgramLoc conn (exprLoc p)+  addCommand conn $ constraintCommand conn f+ -- | Perform any necessary declarations to ensure that the mentioned type map --   sorts exist in the solver environment. declareTypes ::@@ -2981,6 +3083,12 @@   -- | Parse a list of names of assumptions that form an unsatisfiable core.   --   These correspond to previously-named assertions.   smtUnsatCoreResult :: f h -> WriterConn t h -> IO [Text]++  -- | Parse an abduct returned by the get-abduct command+  smtAbductResult :: f h -> WriterConn t h -> Text -> Term h -> IO String++  -- | Parse an abduct returned by the get-abduct-next command+  smtAbductNextResult :: f h -> WriterConn t h -> IO String    -- | Parse a list of names of assumptions that form an unsatisfiable core.   --   The boolean indicates the polarity of the atom: true for an ordinary

@@ -1,4 +1,5 @@ {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} {- Module           : What4.Protocol.VerilogWriter.AST Copyright        : (c) Galois, Inc 2020

@@ -0,0 +1,184 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+-- | This module implements a specialized s-expression parser+--+-- The parser in s-cargot is very general, but that also makes it a bit+-- inefficient.  This module implements a drop-in replacement parser for the one+-- in What4.Serialize.Parser using megaparsec.  It is completely specialized to+-- the types in this library.+module What4.Serialize.FastSExpr (+  parseSExpr+  ) where++import           Control.Applicative+import qualified Control.Monad.Fail as MF+import qualified Data.Parameterized.NatRepr as PN+import           Data.Parameterized.Some ( Some(..) )+import           Data.Ratio ( (%) )+import qualified Data.SCargot.Repr.WellFormed as SC+import qualified Data.Set as Set+import qualified Data.Text as T+import qualified LibBF as BF+import           Numeric.Natural ( Natural )+import qualified Text.Megaparsec as TM+import qualified Text.Megaparsec.Char as TMC+import qualified Text.Megaparsec.Char.Lexer as TMCL+import qualified What4.BaseTypes as WT+import qualified What4.Serialize.SETokens as WST++-- | Parse 'T.Text' into the well-formed s-expression type from s-cargot.+parseSExpr :: T.Text -> Either String (SC.WellFormedSExpr WST.Atom)+parseSExpr t =+  case TM.runParser (ws >> parse) "<input>" t of+    Left errBundle -> Left (TM.errorBundlePretty errBundle)+    Right a -> Right a++data What4ParseError = ErrorParsingHexFloat String+                     | InvalidExponentOrSignificandSize Natural Natural+  deriving (Show, Eq, Ord)++instance TM.ShowErrorComponent What4ParseError where+  showErrorComponent e =+    case e of+      ErrorParsingHexFloat hf -> "Error parsing hex float literal: " ++ hf+      InvalidExponentOrSignificandSize ex s ->+        concat [ "Invalid exponent or significand size: exponent size = "+               , show ex+               , ", significand size = "+               , show s+               ]++type Parser a = TM.Parsec What4ParseError T.Text a++parse :: Parser (SC.WellFormedSExpr WST.Atom)+parse = parseList <|> (SC.WFSAtom <$> lexeme parseAtom)++parseList :: Parser (SC.WellFormedSExpr WST.Atom)+parseList = do+  _ <- lexeme (TMC.char '(')+  items <- TM.many parse+  _ <- lexeme (TMC.char ')')+  return (SC.WFSList items)++parseId :: Parser T.Text+parseId = T.pack <$> ((:) <$> first <*> TM.many rest)+  where+    w4symbol c =  c == '@'+               || c == '+'+               || c == '-'+               || c == '='+               || c == '<'+               || c == '>'+               || c == '_'+               || c == '.'+    first = TMC.letterChar <|> TM.satisfy w4symbol+    rest = TMC.alphaNumChar <|> TM.satisfy w4symbol++parseNat :: Parser Natural+parseNat = do+  _ <- TMC.string "#u"+  TMCL.decimal++parseInt :: Parser Integer+parseInt = TMCL.decimal <|> (negate <$> (TMC.char '-' *> TMCL.decimal))++parseReal :: Parser Rational+parseReal = do+  _ <- TMC.string "#r"+  n <- TMCL.decimal+  _ <- TMC.char '/'+  d <- TMCL.decimal+  return (n % d)++parseBV :: Parser (Int, Integer)+parseBV = do+  _ <- TMC.char '#'+  t <- TM.anySingle+  case t of+    'b' -> parseBin 0 0+    'x' -> parseHex+    _ -> MF.fail ("Invalid bitvector class: " ++ show t)+  where+    parseBin :: Int -> Integer -> Parser (Int, Integer)+    parseBin !nBits !value= do+      mb <- TM.optional TMC.binDigitChar+      case mb of+        Nothing -> return (nBits, value)+        Just bitChar -> parseBin (nBits + 1) (value * 2 + if bitChar == '1' then 1 else 0)+    parseHex :: Parser (Int, Integer)+    parseHex = do+      digits <- TM.some TMC.hexDigitChar+      return (length digits * 4, read ("0x" ++ digits))++parseBool :: Parser Bool+parseBool = do+  _ <- TMC.char '#'+  TM.try (TMC.string "true" *> return True) <|> (TMC.string "false" *> return False)++parseStrInfo :: Parser (Some WT.StringInfoRepr)+parseStrInfo = TM.try (TMC.string "#char16" >> return (Some WT.Char16Repr))+           <|> TM.try (TMC.string "#char8" >> return (Some WT.Char8Repr))+           <|> return (Some WT.UnicodeRepr)++parseStr :: Parser (Some WT.StringInfoRepr, T.Text)+parseStr = do+  prefix <- parseStrInfo+  _ <- TMC.char '"'+  str <- concat <$> TM.many (parseEscaped <|> TM.some (TM.noneOf ('"':"\\")))+  _ <- TMC.char '"'+  return (prefix, T.pack str)+  where+    parseEscaped = do+      _ <- TMC.char '\\'+      c <- TM.anySingle+      return ['\\', c]++parseFloat :: Parser (Some WT.FloatPrecisionRepr, BF.BigFloat)+parseFloat = do+  _ <- TMC.string "#f#"+  -- We printed the nat reprs out in decimal+  eb :: Natural+     <- TMCL.decimal+  _ <- TMC.char '#'+  sb :: Natural+     <- TMCL.decimal+  _ <- TMC.char '#'++  -- The float value itself is printed out as a hex literal+  hexDigits <- TM.some TMC.hexDigitChar++  Some ebRepr <- return (PN.mkNatRepr eb)+  Some sbRepr <- return (PN.mkNatRepr sb)+  case (PN.testLeq (PN.knownNat @2) ebRepr, PN.testLeq (PN.knownNat @2) sbRepr) of+    (Just PN.LeqProof, Just PN.LeqProof) -> do+      let rep = WT.FloatingPointPrecisionRepr ebRepr sbRepr++      -- We know our format: it is determined by the exponent bits (eb) and the+      -- significand bits (sb) parsed above+      let fmt = BF.precBits (fromIntegral sb) <> BF.expBits (fromIntegral eb)+      let (bf, status) = BF.bfFromString 16 fmt hexDigits+      case status of+        BF.Ok -> return (Some rep, bf)+        _ -> TM.fancyFailure (Set.singleton (TM.ErrorCustom (ErrorParsingHexFloat hexDigits)))+    _ -> TM.fancyFailure (Set.singleton (TM.ErrorCustom (InvalidExponentOrSignificandSize eb sb)))+++parseAtom :: Parser WST.Atom+parseAtom = TM.try (uncurry WST.ABV <$> parseBV)+        <|> TM.try (WST.ABool <$> parseBool)+        <|> TM.try (WST.AInt <$> parseInt)+        <|> TM.try (WST.AId <$> parseId)+        <|> TM.try (WST.ANat <$> parseNat)+        <|> TM.try (WST.AReal <$> parseReal)+        <|> TM.try (uncurry WST.AStr <$> parseStr)+        <|> TM.try (uncurry WST.AFloat <$> parseFloat)++ws :: Parser ()+ws = TMCL.space TMC.space1 (TMCL.skipLineComment (T.pack ";")) empty++lexeme :: Parser a -> Parser a+lexeme = TMCL.lexeme ws

@@ -0,0 +1,436 @@+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE NondecreasingIndentation #-}+-- | Description: Log msgs via a synchronized channel+--+-- Log msgs via a synchronized channel.+--+-- With inspiration from the @monad-logger@ package.+--+-- See examples in 'SemMC.Log.Tests'.+--+-- WARNING: loggers that automatically infer the call stack (via+-- `Ghc.HasCallStack`) are not composable, in that they infer a call+-- stack at their call site. So, if you use one to build up another+-- log function, then that derived log function will infer bogus call+-- sites! Of course, it's pretty easy to write+--+--     writeLogEvent logCfg level msg+--+-- when defining a new logger, so not a big deal, just something to+-- watch out for.+module What4.Serialize.Log (+  -- * Misc+  LogLevel(..),+  LogEvent(..),+  LogMsg,+  Ghc.HasCallStack,+  -- * Implicit param logger interface+  HasLogCfg,+  logIO,+  logTrace,+  withLogCfg,+  getLogCfg,+  -- * Explicit parameter logger interface+  logIOWith,+  logEndWith,+  writeLogEvent,+  -- * Monadic logger interface+  MonadHasLogCfg(..),+  logM,+  -- * Configuration+  LogCfg,+  mkLogCfg,+  mkNonLogCfg,+  withLogging,+  -- * Log consumers+  stdErrLogEventConsumer,+  fileLogEventConsumer,+  tmpFileLogEventConsumer,+  -- * Log formatting and consumption (useful for 3rd-party consumers)+  prettyLogEvent,+  consumeUntilEnd,+  -- * Named threads+  named,+  namedIO,+  namedM+  ) where++import qualified GHC.Stack as Ghc++import qualified Control.Concurrent as Cc+import qualified Control.Exception as Cc+import           Control.Monad (when)++import qualified Data.Time.Clock as T+import qualified Data.Time.Format as T++import qualified System.IO as IO+import qualified System.IO.Unsafe as IO++import qualified UnliftIO as U++import qualified Control.Concurrent.STM as Stm+import qualified Control.Concurrent.BoundedChan as BC+import           Control.Monad.IO.Class ( MonadIO, liftIO )+import           Data.Map.Strict ( Map )+import qualified Data.Map.Strict as Map+import           System.Directory ( createDirectoryIfMissing, getTemporaryDirectory )+import           Text.Printf ( printf )++import Debug.Trace++----------------------------------------------------------------+-- * API++-- | Log levels, in increasing severity/precedence order.+data LogLevel = Debug -- ^ Fine details+              | Info  -- ^ Tracking progress+              | Warn  -- ^ Something notable or suspicious+              | Error -- ^ Something bad+              deriving (Show, Eq, Ord, Read)++type LogMsg = String++----------------------------------------------------------------+-- ** Implicit param logger interface++-- | Access to the log config.+--+-- Users should prefer 'withLogCfg' to binding the implicit param. The+-- implicit param is an implementation detail, and we could change the+-- implementation later, e.g. to use the @reflection@ package.+--+-- We use an implicit param to avoid having to change all code in 'IO'+-- that wants to log to be in 'MonadHasLogCfg' and 'MonadIO' classes.+--+-- An even more convenient but more \"unsafe\" implementation would+-- store the 'LogCfg' in a global, 'unsafePerformIO'd 'IORef'+-- (cf. @uniqueSource@ in 'Data.Unique').+type HasLogCfg = (?logCfg :: LogCfg)++-- | Satisfy a 'HasLogCfg' constraint.+--+-- Users can call this function instead of using @ImplicitParams@+-- themselves.+withLogCfg :: LogCfg -> (HasLogCfg => a) -> a+withLogCfg logCfg x = let ?logCfg = logCfg in x++-- | Recover the log config.+--+-- Useful for going between implicit and monadic interfaces. E.g.+--+-- > flip runReaderT getLogCfg ...+getLogCfg :: HasLogCfg => LogCfg+getLogCfg = ?logCfg++-- | Log in a 'MonadIO'.+--+-- If you want the name of function that called 'log' to be included+-- in the output, then you need to add a 'Ghc.HasCallStack' constraint+-- to it as well (see 'LogC'). Otherwise, one of two things will happen:+--+-- - if no enclosing function has a 'Ghc.HasCallStack' constraint,+--   then '???' will be used for the enclosing function name.+--+-- - if at least one enclosing function has a 'Ghc.HasCallStack'+--   constraint, then the name of the *closest* enclosing function+--   with that constraint will be used for the enclosing function+--   name. So, for example, if you define @outer@ by+--+--   > outer :: (MonadHasLogCfg m, Ghc.HasCallStack) => m Int+--   > outer = inner+--   >   where+--   >     inner = do+--   >       log Debug "Inside 'inner' ..."+--   >       return 42+--+--   then the call to 'log' in @inner@ will have \"outer\" as the+--   enclosing function name.+logIO :: (HasLogCfg, Ghc.HasCallStack, MonadIO m)+      => LogLevel -> LogMsg -> m ()+logIO level msg = do+  liftIO $ writeLogEvent ?logCfg Ghc.callStack level msg++-- | 'logIO' with an explicit config+logIOWith :: (Ghc.HasCallStack, MonadIO m) => LogCfg -> LogLevel -> LogMsg -> m ()+logIOWith cfg level msg =+  liftIO $ writeLogEvent cfg Ghc.callStack level msg++-- | Log in pure code using 'unsafePerformIO', like 'Debug.Trace'.+--+-- See 'logIO'.+logTrace :: (HasLogCfg, Ghc.HasCallStack) => LogLevel -> LogMsg -> a -> a+logTrace level msg x = IO.unsafePerformIO $ do+  writeLogEvent ?logCfg Ghc.callStack level msg+  return x+{-# NOINLINE logTrace #-}++----------------------------------------------------------------+-- ** Monadic logger interface++-- | Monads with logger configuration.+class MonadHasLogCfg m where+  getLogCfgM :: m LogCfg++-- | Log in a 'MonadHasLogCfg'.+--+-- See 'logIO'.+logM :: (MonadHasLogCfg m, Ghc.HasCallStack, MonadIO m)+     => LogLevel -> LogMsg -> m ()+logM level msg = do+  logCfg <- getLogCfgM+  liftIO $ writeLogEvent logCfg Ghc.callStack level msg++-- | Signal to the log consumer that there are no more log messages and+-- terminate the log consumer.  This is useful for cases where the logger is+-- running in a separate thread and the parent thread wants to wait until the+-- logger has finished logging and has successfully flushed all log messages+-- before terminating it.+logEndWith :: LogCfg -> IO ()+logEndWith cfg = case lcChan cfg of+                   Just c -> BC.writeChan c Nothing+                   Nothing -> return ()++----------------------------------------------------------------+-- ** Initialization++-- | Initialize a 'LogCfg'.+--+-- The first argument is the human friendly name to assign to the+-- current thread. Since logging should be configured as soon as+-- possible on startup, \"main\" is probably the right name.+--+-- See 'asyncNamed' for naming other threads.+--+-- Need to start a log event consumer in another thread,+-- e.g. 'stdErrLogEventConsumer', if you want anything to happen with+-- the log events.+mkLogCfg :: String -> IO LogCfg+mkLogCfg threadName = do+  chan <- BC.newBoundedChan 100+  threadMap <- do+    tid <- show <$> Cc.myThreadId+    return $ Map.fromList [ (tid, threadName) ]+  threadMapVar <- Stm.newTVarIO threadMap+  return $ LogCfg { lcChan = Just chan+                  , lcThreadMap = threadMapVar }+++-- | Initialize a 'LogCfg' that does no logging.+--+-- This can be used as a LogCfg when no logging is to be performed.+-- Runtime overhead is smaller when this configuration is specified at+-- compile time.+mkNonLogCfg :: IO LogCfg+mkNonLogCfg = do tmVar <- Stm.newTVarIO Map.empty+                 return LogCfg { lcChan = Nothing+                               , lcThreadMap = tmVar+                               }+++-- | Run an action with the given log event consumer.+--+-- In particular this provides an easy way to run one-off computations+-- that assume logging, e.g. in GHCi. Spawns the log even consumer+-- before running the action and cleans up the log event consumer+-- afterwards.+withLogging :: (U.MonadUnliftIO m, MonadIO m)+            => String -> (LogCfg -> IO ()) -> (HasLogCfg => m a) -> m a+withLogging threadName logEventConsumer action = do+  cfg <- liftIO $ mkLogCfg threadName+  U.withAsync (liftIO $ logEventConsumer cfg) $ \a -> do+  x <- withLogCfg cfg action+  liftIO $ logEndWith cfg+  U.wait a+  return x++----------------------------------------------------------------+-- ** Log event consumers++-- | Consume a log channel until it receives a shutdown message+-- (i.e. a 'Nothing').+--+-- Only messages that satisfy the predicate will be passed to the+-- continuation. For example, using @const True@ will process all log+-- messages, and using @(>= Info) . leLevel@ will only process+-- messsages with 'LogLevel' equal to 'Info' or higher, ignoring+-- 'Debug' level messages.+consumeUntilEnd ::+  (LogEvent -> Bool) -> (LogEvent -> IO ()) -> LogCfg -> IO ()+consumeUntilEnd keepEvent k cfg =+  case lcChan cfg of+    Nothing -> return ()+    Just c -> do+      mevent <- BC.readChan c+      case mevent of+        Just event -> do when (keepEvent event) $ k event+                         consumeUntilEnd keepEvent k cfg+        _ -> return ()++-- | A log event consumer that prints formatted log events to stderr.+stdErrLogEventConsumer :: (LogEvent -> Bool) -> LogCfg -> IO ()+stdErrLogEventConsumer keepEvent =+  consumeUntilEnd keepEvent $ \e -> do+    -- Use 'traceIO' because it seems to be atomic in practice,+    -- avoiding problems with interleaving output from other sources.+    traceIO (prettyLogEvent e)+    IO.hFlush IO.stderr -- Probably unnecessary.++-- | A logger that writes to a user-specified file+--+-- Note that logs are opened in the 'w' mode (i.e., overwrite).  Callers should+-- preserve old log files if they really want.+fileLogEventConsumer :: FilePath -> (LogEvent -> Bool) -> LogCfg -> IO ()+fileLogEventConsumer fp keepEvent cfg = IO.withFile fp IO.WriteMode $ \h -> do+  let k e = IO.hPutStrLn h (prettyLogEvent e) >> IO.hFlush h+  consumeUntilEnd keepEvent k cfg++-- | A log event consumer that writes formatted log events to a tmp+-- file.+tmpFileLogEventConsumer :: (LogEvent -> Bool) -> LogCfg -> IO ()+tmpFileLogEventConsumer keepEvent cfg = do+  tmpdir <- (++ "/brittle") <$> getTemporaryDirectory+  createDirectoryIfMissing True tmpdir+  (tmpFilePath, tmpFile) <- IO.openTempFile tmpdir "log.txt"+  printf "\n\nWriting logs to %s\n\n" tmpFilePath+  let k e = IO.hPutStrLn tmpFile (prettyLogEvent e) >> IO.hFlush tmpFile+  consumeUntilEnd keepEvent k cfg++----------------------------------------------------------------+-- ** Named threads++-- | Run an IO action with a human friendly thread name.+--+-- Any existing thread name will be restored when the action finishes.+named :: (U.MonadUnliftIO m, MonadIO m) => LogCfg -> String -> m a -> m a+named cfg threadName action = do+  actionIO <- U.toIO action+  liftIO $ do+    tid <- show <$> Cc.myThreadId+    mOldName <- Map.lookup tid <$> Stm.readTVarIO (lcThreadMap cfg)+    Cc.bracket_ (insert tid) (remove tid mOldName) actionIO+  where+    modify = Stm.atomically . Stm.modifyTVar' (lcThreadMap cfg)++    insert tid = modify $ Map.insert tid threadName++    remove tid Nothing        = modify $ Map.delete tid+    remove tid (Just oldName) = modify $ Map.insert tid oldName++-- | Version of 'named' for implicit log cfg.+namedIO :: (HasLogCfg, U.MonadUnliftIO m, MonadIO m)+        => String -> m a -> m a+namedIO threadName action = named ?logCfg threadName action++-- | Version of 'named' for 'MonadHasLogCfg' monads.+namedM :: (MonadHasLogCfg m, U.MonadUnliftIO m, MonadIO m)+       => String -> m a -> m a+namedM threadName action = do+  cfg <- getLogCfgM+  named cfg threadName action++----------------------------------------------------------------+-- * Internals++-- | Stored as 'String' because 'Control.Concurrent.ThreadId' docs say+-- a thread can't be GC'd as long as someone maintains a reference to+-- its 'ThreadId'!!!+type ThreadId = String++-- | A log event.+--+-- Can be converted to a string later, or thrown away.+data LogEvent = LogEvent+  { leCallSite :: (Maybe String, Ghc.SrcLoc)+    -- ^ The @Maybe String@ is the name of the enclosing function in+    -- which the logging function was called. Not always available,+    -- since it depends on the enclosing function having a+    -- 'Ghc.HasCallStack' constraint.+  , leLevel    :: LogLevel+  , leMsg      :: LogMsg+  , leThreadId :: ThreadId+    -- ^ ID of thread that generated the event.+  , leTime     :: T.UTCTime+  }++-- | Logging configuration.+data LogCfg = LogCfg+  { lcChan :: Maybe (BC.BoundedChan (Maybe LogEvent))+  , lcThreadMap :: Stm.TVar (Map ThreadId String)+    -- ^ User friendly names for threads. See 'asyncNamed'.++  -- Idea: add a predicate on log events that is used to discard log+  -- events that e.g. aren't of a high enough precedence+  -- level. E.g. only keep events of level 'Warn' or above:+  --+  -- > lcPred le = leLevel le >= Warn+  --+  -- , lcPred :: LogEvent -> Bool+  }++-- | Format a log event.+prettyLogEvent :: LogEvent -> String+prettyLogEvent le =+  printf "[%s][%s][%s][%s]\n%s"+    (show $ leLevel le) time location (leThreadId le) (leMsg le)+  where+    time :: String+    time = T.formatTime T.defaultTimeLocale "%T" (leTime le)+    location :: String+    location = printf "%s:%s"+      (prettyFun maybeFun) (Ghc.prettySrcLoc srcLoc)+    (maybeFun, srcLoc) = leCallSite le+    prettyFun Nothing = "???"+    prettyFun (Just fun) = fun++prettyThreadId :: LogCfg -> ThreadId -> IO ThreadId+prettyThreadId cfg tid = do+  mThreadName <- Map.lookup tid <$> Stm.readTVarIO (lcThreadMap cfg)+  return $ printf "%s (%s)" (maybe "???" id mThreadName) tid++-- | Write a 'LogEvent' to the underlying channel.+--+-- This is a low-level function. See 'logIO', 'logM', and 'logTrace'+-- for a high-level interface that supplies the 'LogCfg' and+-- 'Ghc.CallStack' parameters automatically.+--+-- However, those functions can't be used to build up custom loggers,+-- since they infer call stack information automatically. If you want+-- to define a custom logger (even something simple like+--+-- > debug msg = logM Debug msg+--+-- ) then use 'writeLogEvent'.+writeLogEvent :: LogCfg -> Ghc.CallStack -> LogLevel -> LogMsg -> IO ()+writeLogEvent cfg cs level msg = do+  tid <- show <$> Cc.myThreadId+  ptid <- prettyThreadId cfg tid+  time <- T.getCurrentTime+  case lcChan cfg of+    Nothing -> return ()+    Just c -> BC.writeChan c (Just (event ptid time))+  where+    event tid time = LogEvent+      { leCallSite = callSite+      , leLevel = level+      , leMsg = msg+      , leThreadId = tid+      , leTime = time+      }+    -- | The call stack has the most recent call first. Assuming+    -- 'writeLogEvent' is always called in a logging function with a+    -- 'Ghc.HasCallStack' constraint, the call stack will be non-empty+    -- -- i.e. @topSrcLoc@ will be defined -- but there may not be a+    -- lower frame corresponding to the context in which the logging+    -- function was called. To get a lower frame, some enclosing+    -- function needs a 'Ghc.HasCallStack' constraint itself.+    --+    -- And only functions with 'Ghc.HasCallStack' will get frames. See+    -- discussion at 'log'.+    callSite = case Ghc.getCallStack cs of+                 (_,topSrcLoc):rest -> case rest of+                   []                 -> (Nothing,           topSrcLoc)+                   (enclosingFun,_):_ -> (Just enclosingFun, topSrcLoc)+                 [] -> error "Do we ever not have a call site?"

@@ -0,0 +1,162 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE MultiWayIf #-}++-- | Normalization and equivalence checking for expressions+module What4.Serialize.Normalize+  ( normSymFn+  , normExpr+  , testEquivSymFn+  , testEquivExpr+  , ExprEquivResult(..)+  ) where++import qualified Data.Parameterized.Context as Ctx+import qualified Data.Parameterized.TraversableFC as FC++import qualified What4.Interface as S+import qualified What4.Expr as S+import qualified What4.Expr.Builder as B+import qualified What4.Expr.WeightedSum as WSum+import           Data.Parameterized.Classes++-- | Apply some normalizations to make function call arguments more readable.  Examples include:+--+--  * Avoid wrapping single literals in a 'B.SemiRingLiteral' and just represent them as a bare integer literals+--  * Attempt to reduce function calls with constant arguments where possible+normSymFn :: forall sym st fs t args ret. sym ~ B.ExprBuilder t st fs+          => sym+          -> B.ExprSymFn t args ret+          -> Ctx.Assignment (S.Expr t) args+          -> IO (S.Expr t ret)+normSymFn sym symFn argEs = case B.symFnInfo symFn of+  B.DefinedFnInfo argBVs expr _ -> do+    argEs' <- FC.traverseFC (normExpr sym) argEs+    expr' <- B.evalBoundVars sym expr argBVs argEs'+    normExpr sym expr'+  _ -> S.applySymFn sym symFn argEs+++normExpr :: forall sym st fs t tp+          . sym ~ B.ExprBuilder t st fs+         => sym+         -> B.Expr t tp -> IO (B.Expr t tp)+normExpr sym e = go e+  where go :: B.Expr t tp -> IO (B.Expr t tp)+        go (B.SemiRingLiteral S.SemiRingIntegerRepr val _) = S.intLit sym val+        go (B.AppExpr appExpr) = normAppExpr sym appExpr+        go x@(B.NonceAppExpr nae) =+          case B.nonceExprApp nae of+            B.FnApp fn args -> normSymFn sym fn args+            _ -> return x+        go x = return x++-- | Normalize an expression by passing it back through the builder+--+-- NOTE: We may want to audit the cases here for completeness+normAppExpr :: forall sym st fs t tp+             . sym ~ S.ExprBuilder t st fs+            => sym+            -> S.AppExpr t tp+            -> IO (S.Expr t tp)+normAppExpr sym ae = do+  e' <- go (S.appExprApp ae)+  B.sbMakeExpr sym e'+  where norm2 :: forall tp' tp'' tp'''+               . (S.Expr t tp' -> S.Expr t tp'' -> IO (S.Expr t tp'''))+              -> S.Expr t tp' -> S.Expr t tp'' -> IO (S.Expr t tp''')+        norm2 f e1 e2 = do+          e1' <- normExpr sym e1+          e2' <- normExpr sym e2+          f e1' e2'++        go :: forall tp'. S.App (S.Expr t) tp' -> IO (S.App (S.Expr t) tp')+        go (S.BaseIte _ _ test then_ else_) = do+          test' <- normExpr sym test+          then' <- normExpr sym then_+          else' <- normExpr sym else_+          Just sm' <- B.asApp <$> S.baseTypeIte sym test' then' else'+          return sm'+        go x@(S.SemiRingSum sm) =+          case WSum.sumRepr sm of+            S.SemiRingIntegerRepr -> do+              let+                smul si i = do+                    i' <- normExpr sym i+                    si' <- S.intLit sym si+                    S.intMul sym si' i'+              Just sm' <- B.asApp <$> WSum.evalM (norm2 $ S.intAdd sym) smul (S.intLit sym) sm+              return sm'+            _ -> return x+        go x@(S.SemiRingProd pd) =+          case WSum.prodRepr pd of+            S.SemiRingIntegerRepr -> do+                maybeS <- WSum.prodEvalM (norm2 $ S.intMul sym) return pd+                case maybeS of+                  Just s | Just sm' <- B.asApp s -> return sm'+                  _ -> return x+            _ -> return x+        go x@(S.SemiRingLe sr e1 e2) = do+          case sr of+            S.OrderedSemiRingIntegerRepr -> do+              Just sm' <- B.asApp <$> (norm2 $ S.intLe sym) e1 e2+              return sm'+            _ -> return x+        go x = return x++++data ExprEquivResult = ExprEquivalent | ExprNormEquivalent | ExprUnequal++testEquivExpr :: forall sym st fs t tp tp'. sym ~ S.ExprBuilder t st fs => sym -> B.Expr t tp -> B.Expr t tp' -> IO (ExprEquivResult)+testEquivExpr sym e1 e2 = case testEquality e1 e2 of+  Just Refl -> return ExprEquivalent+  _ -> do+    e1' <- normExpr sym e1+    e2' <- normExpr sym e2+    case testEquality e1' e2' of+      Just Refl -> return ExprNormEquivalent+      _ -> return ExprUnequal++testEquivSymFn :: forall sym st fs t args ret args' ret'. sym ~ S.ExprBuilder t st fs => sym -> S.SymFn sym args ret -> S.SymFn sym args' ret' -> IO (ExprEquivResult)+testEquivSymFn sym fn1 fn2 =+  let+    argTypes1 = S.fnArgTypes fn1+    argTypes2 = S.fnArgTypes fn2+    retType1 = S.fnReturnType fn1+    retType2 = S.fnReturnType fn2+  in if | Just Refl <- testEquality argTypes1 argTypes2+        , Just Refl <- testEquality retType1 retType2+        , B.symFnName fn1 == B.symFnName fn2 ->+          case (S.symFnInfo fn1, S.symFnInfo fn2) of+           (S.DefinedFnInfo argBVs1 efn1 _, S.DefinedFnInfo argBVs2 efn2 _) -> do+             args <- FC.traverseFC (\bv -> S.freshConstant sym (S.bvarName bv) (B.bvarType bv)) argBVs1+             expr1 <- B.evalBoundVars sym efn1 argBVs1 args+             expr2 <- B.evalBoundVars sym efn2 argBVs2 args+             case testEquality expr1 expr2 of+               Just Refl -> return ExprEquivalent+               Nothing -> do+                 expr1' <- normExpr sym expr1+                 expr2' <- normExpr sym expr2+                 case testEquality expr1' expr2' of+                   Just Refl -> return ExprNormEquivalent+                   Nothing -> return ExprUnequal+           (S.UninterpFnInfo _ _, S.UninterpFnInfo _ _) -> return ExprEquivalent+           (S.MatlabSolverFnInfo _ _ _, _) -> fail "Unsupported function type for equivalence check."+           (_, S.MatlabSolverFnInfo _ _ _) -> fail "Unsupported function type for equivalence check."+           (_, _) -> return ExprUnequal+        | otherwise -> return ExprUnequal

@@ -0,0 +1,1070 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE MultiWayIf #-}++-- | A parser for an s-expression representation of what4 expressions+module What4.Serialize.Parser+  ( deserializeExpr+  , deserializeExprWithConfig+  , deserializeSymFn+  , deserializeSymFnWithConfig+  , deserializeBaseType+  , readBaseTypes+  , Atom(..)+  , S.WellFormedSExpr(..)+  , Config(..)+  , defaultConfig+  , SomeSymFn(..)+  , type SExpr+  , parseSExpr+  , printSExpr+  ) where++import qualified Control.Monad.Except as E+import           Control.Monad.IO.Class ( liftIO )+import qualified Control.Monad.Reader as R+import qualified Data.BitVector.Sized as BV+import qualified Data.Foldable as F+import qualified Data.HashMap.Lazy as HM+import           Data.Kind+import qualified Data.SCargot.Repr.WellFormed as S++import           Data.Text ( Text )+import qualified Data.Text as T+import qualified Data.Text.Encoding as T+import           Text.Printf ( printf )++import qualified Data.Parameterized.NatRepr as PN+import qualified Data.Parameterized.Ctx as Ctx+import qualified Data.Parameterized.Context as Ctx+import           Data.Parameterized.Classes+import           Data.Parameterized.Some ( Some(..) )+import qualified Data.Parameterized.TraversableFC as FC+import           What4.BaseTypes++import qualified What4.Expr.ArrayUpdateMap as WAU+import qualified What4.Expr.Builder as W4+import qualified What4.IndexLit as WIL+import qualified What4.Interface as W4++import           What4.Serialize.SETokens ( Atom(..), printSExpr, parseSExpr )+import qualified What4.Utils.Serialize as U+import           What4.Serialize.Printer ( SExpr )++import           Prelude++data SomeSymFn t = forall dom ret. SomeSymFn (W4.SymFn t dom ret)++data Config sym =+  Config+  { cSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))+  -- ^ The mapping of names to defined What4 SymFns.+  , cExprLookup :: Text -> IO (Maybe (Some (W4.SymExpr sym)))+  -- ^ The mapping of names to defined What4 expressions.+  }++defaultConfig :: (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym)) => sym -> Config sym+defaultConfig _sym = Config { cSymFnLookup = const (return Nothing)+                            , cExprLookup = const (return Nothing)+                            }+++-- | The lexical environment for parsing s-expressions and+-- procesing them into What4 terms.+data ProcessorEnv sym =+  ProcessorEnv+  { procSym :: sym+  -- ^ The symbolic What4 backend being used.+  , procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))+    -- ^ The user-specified mapping of names to defined What4 SymFns.+  , procExprLookup :: Text -> IO (Maybe (Some (W4.SymExpr sym)))+  -- ^ The user-specified mapping of names to defined What4 expressions.+  , procLetEnv :: HM.HashMap Text (Some (W4.SymExpr sym))+  -- ^ The current lexical environment w.r.t. let-bindings+  -- encountered while parsing. N.B., these bindings are+  -- checked _before_ the \"global\" bindings implied by the+  -- user-specified lookup functions.+  , procLetFnEnv :: HM.HashMap Text (SomeSymFn sym)+  -- ^ The current lexical symfn environment+  -- w.r.t. letfn-bindings encountered while parsing. N.B.,+  -- these bindings are checked /before/ the \"global\"+  -- bindings implied by the user-specified lookup+  -- functions.+  }++type Processor sym a = E.ExceptT String (R.ReaderT (ProcessorEnv sym) IO) a++runProcessor :: ProcessorEnv sym -> Processor sym a -> IO (Either String a)+runProcessor env action = R.runReaderT (E.runExceptT action) env++lookupExpr :: Text -> Processor sym (Maybe (Some (W4.SymExpr sym)))+lookupExpr nm = do+  userLookupFn <- R.asks procExprLookup+  letEnv <- R.asks procLetEnv+  case HM.lookup nm letEnv of+    Nothing -> liftIO $ userLookupFn nm+    res -> return res++lookupFn :: Text -> Processor sym (Maybe (SomeSymFn sym))+lookupFn nm = do+  userLookupFn <- R.asks procSymFnLookup+  letEnv <- R.asks procLetFnEnv+  case HM.lookup nm letEnv of+    Nothing -> liftIO $ userLookupFn nm+    res -> return res+++-- | @(deserializeExpr sym)@ is equivalent+-- to @(deserializeExpr' (defaultConfig sym))@.+deserializeExpr ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => sym+  -> SExpr+  -> IO (Either String (Some (W4.SymExpr sym)))+deserializeExpr sym = deserializeExprWithConfig sym cfg+  where cfg = defaultConfig sym++deserializeExprWithConfig ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => sym+  -> Config sym+  -> SExpr+  -> IO (Either String (Some (W4.SymExpr sym)))+deserializeExprWithConfig sym cfg sexpr = runProcessor env (readExpr sexpr)+  where env = ProcessorEnv { procSym = sym+                           , procSymFnLookup = cSymFnLookup cfg+                           , procExprLookup = cExprLookup cfg+                           , procLetEnv = HM.empty+                           , procLetFnEnv = HM.empty+                           }++-- | @(deserializeSymFn sym)@ is equivalent+-- to @(deserializeSymFn' (defaultConfig sym))@.+deserializeSymFn ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => sym+  -> SExpr+  -> IO (Either String (SomeSymFn sym))+deserializeSymFn sym = deserializeSymFnWithConfig sym cfg+  where cfg = defaultConfig sym++deserializeSymFnWithConfig ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => sym+  -> Config sym+  -> SExpr+  -> IO (Either String (SomeSymFn sym))+deserializeSymFnWithConfig sym cfg sexpr = runProcessor env (readSymFn sexpr)+  where env = ProcessorEnv { procSym = sym+                           , procSymFnLookup = cSymFnLookup cfg+                           , procExprLookup = cExprLookup cfg+                           , procLetEnv = HM.empty+                           , procLetFnEnv = HM.empty+                           }+++deserializeBaseType ::+  SExpr+  -> Either String (Some BaseTypeRepr)+deserializeBaseType sexpr = readBaseType sexpr++++++-- * First pass of parsing turns the raw text into s-expressions.+--   This pass is handled by the code in What4.Serialize.SETokens++-- * Second pass of parsing: turning the s-expressions into symbolic expressions+-- and the overall templated formula++-- ** Utility functions++-- | Utility function for contextualizing errors. Prepends the given prefix+-- whenever an error is thrown.+prefixError :: (Monoid e, E.MonadError e m) => e -> m a -> m a+prefixError prefix act = E.catchError act (E.throwError . mappend prefix)++-- | Utility function for lifting a 'Maybe' into a 'MonadError'+fromMaybeError :: (E.MonadError e m) => e -> Maybe a -> m a+fromMaybeError err = maybe (E.throwError err) return+++readBaseType ::+  forall m . (E.MonadError String m)+  => SExpr+  -> m (Some BaseTypeRepr)+readBaseType sexpr =+  case sexpr of+    S.WFSAtom (AId atom) ->+      case (T.unpack atom) of+        "Bool" -> return $ Some BaseBoolRepr+        "Int" -> return $ Some BaseIntegerRepr+        "Real" -> return $ Some BaseRealRepr+        "String" -> return $ Some (BaseStringRepr UnicodeRepr)+        "Complex" -> return $ Some BaseComplexRepr+        _ -> panic+    S.WFSList [(S.WFSAtom (AId "BV")), (S.WFSAtom (AInt w))]+      | Just (Some wRepr) <- someNat w+      , Just LeqProof <- testLeq (knownNat @1) wRepr+        -> return $ Some (BaseBVRepr wRepr)+      | otherwise+        -> panic+    S.WFSList [(S.WFSAtom (AId "Float")), (S.WFSAtom (AInt e)), (S.WFSAtom (AInt s))]+      | Just (Some eRepr) <- someNat e+      , Just (Some sRepr) <- someNat s+      , Just LeqProof <- testLeq (knownNat @2) eRepr+      , Just LeqProof <- testLeq (knownNat @2) sRepr+        -> return (Some (BaseFloatRepr (FloatingPointPrecisionRepr eRepr sRepr)))+      | otherwise -> panic+    S.WFSList [(S.WFSAtom (AId "Struct")), args] -> do+      Some tps <- readBaseTypes args+      return $ Some (BaseStructRepr tps)+    S.WFSList [S.WFSAtom (AId "Array"), ixArgs, tpArg] -> do+      Some ixs <- readBaseTypes ixArgs+      Some tp <- readBaseType tpArg+      case Ctx.viewAssign ixs of+        Ctx.AssignEmpty -> E.throwError $ "array type has no indices: " ++ show sexpr+        Ctx.AssignExtend _ _ -> return $ Some (BaseArrayRepr ixs tp)+    _ -> panic+  where+    panic = E.throwError $ "unknown base type: " ++ show sexpr++readBaseTypes ::+  forall m . (E.MonadError String m)+  => SExpr+  -> m (Some (Ctx.Assignment BaseTypeRepr))+readBaseTypes sexpr@(S.WFSAtom _) = E.throwError $ "expected list of base types: " ++ show sexpr+readBaseTypes (S.WFSList sexprs) = Ctx.fromList <$> mapM readBaseType sexprs++-- ** Parsing definitions++-- | Stores a NatRepr along with proof that its type parameter is a bitvector of+-- that length. Used for easy pattern matching on the LHS of a binding in a+-- do-expression to extract the proof.+data BVProof tp where+  BVProof :: forall n. (1 <= n) => NatRepr n -> BVProof (BaseBVType n)++-- | Given an expression, monadically either returns proof that it is a+-- bitvector or throws an error.+getBVProof :: (W4.IsExpr ex, E.MonadError String m) => ex tp -> m (BVProof tp)+getBVProof expr =+  case W4.exprType expr of+    BaseBVRepr n -> return $ BVProof n+    t -> E.throwError $ printf "expected BV, found %s" (show t)+++-- | Operator type descriptions for parsing s-expression of+-- the form @(operator operands ...)@.+data Op sym where+    FloatOp1 :: (forall fpp . sym ->+                 W4.SymFloat sym fpp ->+                 IO (W4.SymFloat sym fpp))+             -> Op sym+    -- | Generic unary operator description.+    Op1 :: Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1)+        -> (sym ->+            W4.SymExpr sym arg1 ->+            IO (W4.SymExpr sym ret))+        -> Op sym+    -- | Generic dyadic operator description.+    Op2 :: Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2)+        -> (sym ->+            W4.SymExpr sym arg1 ->+            W4.SymExpr sym arg2 ->+            IO (W4.SymExpr sym ret))+        -> Op sym+    -- | Generic triadic operator description.+    Op3 :: Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2 Ctx.::> arg3)+        -> (sym ->+            W4.SymExpr sym arg1 ->+            W4.SymExpr sym arg2 ->+            W4.SymExpr sym arg3 ->+            IO (W4.SymExpr sym ret)+           )+        -> Op sym+    -- | Generic tetradic operator description.+    Op4 :: Ctx.Assignment+           BaseTypeRepr+           (Ctx.EmptyCtx Ctx.::> arg1 Ctx.::> arg2 Ctx.::> arg3 Ctx.::> arg4)+        -> ( sym ->+             W4.SymExpr sym arg1 ->+             W4.SymExpr sym arg2 ->+             W4.SymExpr sym arg3 ->+             W4.SymExpr sym arg4 ->+             IO (W4.SymExpr sym ret)+           )+        -> Op sym+    -- | Encapsulating type for a unary operation that takes one bitvector and+    -- returns another (in IO).+    BVOp1 :: (forall w . (1 <= w) =>+               sym ->+               W4.SymBV sym w ->+               IO (W4.SymBV sym w))+          -> Op sym+    -- | Binop with a bitvector return type, e.g., addition or bitwise operations.+    BVOp2 :: (forall w . (1 <= w) =>+               sym ->+               W4.SymBV sym w ->+               W4.SymBV sym w ->+               IO (W4.SymBV sym w))+          -> Op sym+    -- | Bitvector binop with a boolean return type, i.e., comparison operators.+    BVComp2 :: (forall w . (1 <= w) =>+                    sym ->+                    W4.SymBV sym w ->+                    W4.SymBV sym w ->+                    IO (W4.Pred sym))+                -> Op sym++-- | Lookup mapping operators to their Op definitions (if they exist)+lookupOp :: forall sym . W4.IsSymExprBuilder sym => Text -> Maybe (Op sym)+lookupOp name = HM.lookup name opTable+++opTable :: (W4.IsSymExprBuilder sym) => HM.HashMap Text (Op sym)+opTable =+  HM.fromList [+  -- -- -- Boolean ops -- -- --+    ("andp", Op2 knownRepr $ W4.andPred)+  , ("orp", Op2 knownRepr $ W4.orPred)+  , ("xorp", Op2 knownRepr $ W4.xorPred)+  , ("notp", Op1 knownRepr $ W4.notPred)+  -- -- -- Float ops -- -- --+  , ("floatneg", FloatOp1 W4.floatNeg)+  , ("floatabs", FloatOp1 W4.floatAbs)+  -- -- -- Integer ops -- -- --+  , ("intmul", Op2 knownRepr $ W4.intMul)+  , ("intadd", Op2 knownRepr $ W4.intAdd)+  , ("intmod", Op2 knownRepr $ W4.intMod)+  , ("intdiv", Op2 knownRepr $ W4.intDiv)+  , ("intle", Op2 knownRepr $ W4.intLe)+  , ("intabs", Op1 knownRepr $ W4.intAbs)+  -- -- -- Bitvector ops -- -- --+  , ("bvand", BVOp2 W4.bvAndBits)+  , ("bvor", BVOp2 W4.bvOrBits)+  , ("bvadd", BVOp2 W4.bvAdd)+  , ("bvmul", BVOp2 W4.bvMul)+  , ("bvudiv", BVOp2 W4.bvUdiv)+  , ("bvurem", BVOp2 W4.bvUrem)+  , ("bvshl", BVOp2 W4.bvShl)+  , ("bvlshr", BVOp2 W4.bvLshr)+  , ("bvnand", BVOp2 $ \sym arg1 arg2 -> W4.bvNotBits sym =<< W4.bvAndBits sym arg1 arg2)+  , ("bvnor", BVOp2 $ \sym arg1 arg2 -> W4.bvNotBits sym =<< W4.bvOrBits sym arg1 arg2)+  , ("bvxor", BVOp2 W4.bvXorBits)+  , ("bvxnor", BVOp2 $ \sym arg1 arg2 -> W4.bvNotBits sym =<< W4.bvXorBits sym arg1 arg2)+  , ("bvsub", BVOp2 W4.bvSub)+  , ("bvsdiv", BVOp2 W4.bvSdiv)+  , ("bvsrem", BVOp2 W4.bvSrem)+  , ("bvsmod", error "bvsmod is not implemented")+  , ("bvashr", BVOp2 W4.bvAshr)+  , ("bvult", BVComp2 W4.bvUlt)+  , ("bvule", BVComp2 W4.bvUle)+  , ("bvugt", BVComp2 W4.bvUgt)+  , ("bvuge", BVComp2 W4.bvUge)+  , ("bvslt", BVComp2 W4.bvSlt)+  , ("bvsle", BVComp2 W4.bvSle)+  , ("bvsgt", BVComp2 W4.bvSgt)+  , ("bvsge", BVComp2 W4.bvSge)+  , ("bveq", BVComp2 W4.bvEq)+  , ("bvne", BVComp2 W4.bvNe)+  , ("bvneg", BVOp1 W4.bvNeg)+  , ("bvnot", BVOp1 W4.bvNotBits)+  -- -- -- Floating point ops -- -- --+  , ("fnegd", Op1 knownRepr $ W4.floatNeg @_ @Prec64)+  , ("fnegs", Op1 knownRepr $ W4.floatNeg @_ @Prec32)+  , ("fabsd", Op1 knownRepr $ W4.floatAbs @_ @Prec64)+  , ("fabss", Op1 knownRepr $ W4.floatAbs @_ @Prec32)+  , ("fsqrt", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.floatSqrt @_ @Prec64 sym rm x)+  , ("fsqrts", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.floatSqrt @_ @Prec32 sym rm x)+  , ("fnand", Op1 knownRepr $ W4.floatIsNaN @_ @Prec64)+  , ("fnans", Op1 knownRepr $ W4.floatIsNaN @_ @Prec32)+  , ("frsp", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.floatCast @_ @Prec32 @Prec64 sym knownRepr rm x)+  , ("fp_single_to_double", Op1 knownRepr $ \sym ->+    W4.floatCast @_ @Prec64 @Prec32 sym knownRepr W4.RNE)+  , ("fp_binary_to_double",+     Op1 knownRepr $ \sym -> W4.floatFromBinary @_ @11 @53 sym knownRepr)+  , ("fp_binary_to_single",+     Op1 knownRepr $ \sym -> W4.floatFromBinary @_ @8 @24 sym knownRepr)+  , ("fp_double_to_binary", Op1 knownRepr $ W4.floatToBinary @_ @11 @53)+  , ("fp_single_to_binary", Op1 knownRepr $ W4.floatToBinary @_ @8 @24)+  , ("fctid", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.floatToSBV @_ @64 @Prec64 sym knownRepr rm x)+  , ("fctidu", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.floatToBV @_ @64 @Prec64 sym knownRepr rm x)+  , ("fctiw", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.floatToSBV @_ @32 @Prec64 sym knownRepr rm x)+  , ("fctiwu", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.floatToBV @_ @32 @Prec64 sym knownRepr rm x)+  , ("fcfid", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.sbvToFloat @_ @64 @Prec64 sym knownRepr rm x)+  , ("fcfids", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.sbvToFloat @_ @64 @Prec32 sym knownRepr rm x)+  , ("fcfidu", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.bvToFloat @_ @64 @Prec64 sym knownRepr rm x)+  , ("fcfidus", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.bvToFloat @_ @64 @Prec32 sym knownRepr rm x)+  , ("frti", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.floatRound @_ @Prec64 sym rm x)+  , ("frtis", Op2 knownRepr $ \sym r x -> U.withRounding sym r $ \rm ->+    W4.floatRound @_ @Prec32 sym rm x)+  , ("fadd", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->+    W4.floatAdd @_ @Prec64 sym rm x y)+  , ("fadds", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->+    W4.floatAdd @_ @Prec32 sym rm x y)+  , ("fsub", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->+    W4.floatSub @_ @Prec64 sym rm x y)+  , ("fsubs", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->+    W4.floatSub @_ @Prec32 sym rm x y)+  , ("fmul", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->+    W4.floatMul @_ @Prec64 sym rm x y)+  , ("fmuls", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->+    W4.floatMul @_ @Prec32 sym rm x y)+  , ("fdiv", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->+    W4.floatDiv @_ @Prec64 sym rm x y)+  , ("fdivs", Op3 knownRepr $ \sym r x y -> U.withRounding sym r $ \rm ->+    W4.floatDiv @_ @Prec32 sym rm x y)+  , ("fltd", Op2 knownRepr $ W4.floatLt @_ @Prec64)+  , ("flts", Op2 knownRepr $ W4.floatLt @_ @Prec32)+  , ("feqd", Op2 knownRepr $ W4.floatFpEq @_ @Prec64)+  , ("feqs", Op2 knownRepr $ W4.floatFpEq @_ @Prec32)+  , ("fled", Op2 knownRepr $ W4.floatLe @_ @Prec64)+  , ("fles", Op2 knownRepr $ W4.floatLe @_ @Prec32)+  , ("ffma", Op4 knownRepr $ \sym r x y z -> U.withRounding sym r $ \rm ->+    W4.floatFMA @_ @Prec64 sym rm x y z)+  , ("ffmas", Op4 knownRepr $ \sym r x y z ->+    U.withRounding sym r $ \rm -> W4.floatFMA @_ @Prec32 sym rm x y z)+  ]++-- | Verify a list of arguments has a single argument and+-- return it, else raise an error.+readOneArg ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => [SExpr]+  -> Processor sym (Some (W4.SymExpr sym))+readOneArg operands = do+  args <- readExprs operands+  case args of+    [arg] -> return arg+    _ -> E.throwError $ printf "expecting 1 argument, got %d" (length args)++-- | Verify a list of arguments has two arguments and return+-- it, else raise an error.+readTwoArgs ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => [SExpr]+  -> Processor sym (Some (W4.SymExpr sym), Some (W4.SymExpr sym))+readTwoArgs operands = do+  args <- readExprs operands+  case args of+    [arg1, arg2] -> return (arg1, arg2)+    _ -> E.throwError $ printf "expecting 2 arguments, got %d" (length args)++-- | Verify a list of arguments has three arguments and+-- return it, else raise an error.+readThreeArgs ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => [SExpr]+  -> Processor sym (Some (W4.SymExpr sym), Some (W4.SymExpr sym), Some (W4.SymExpr sym))+readThreeArgs operands = do+  args <- readExprs operands+  case args of+    [arg1, arg2, arg3] -> return (arg1, arg2, arg3)+    _ -> E.throwError $ printf "expecting 3 arguments, got %d" (length args)++++-- | Reads an "application" form, i.e. @(operator operands ...)@.+readApp ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => SExpr+  -> [SExpr]+  -> Processor sym (Some (W4.SymExpr sym))+readApp (S.WFSAtom (AId "call")) (S.WFSAtom (AId fnName):operands) = do+  sym <- R.asks procSym+  maybeFn <- lookupFn fnName+  case maybeFn of+    Just (SomeSymFn fn) -> do+      args <- mapM readExpr operands+      assn <- exprAssignment (W4.fnArgTypes fn) args+      liftIO (Some <$> W4.applySymFn sym fn assn)+    Nothing -> E.throwError $ "The function name `"+               ++(T.unpack fnName)+               ++"` is not bound to a SymFn in the current Config."+readApp opRaw@(S.WFSAtom (AId "call")) operands = E.throwError+  $ "Unrecognized use of `call`: " ++ (T.unpack (printSExpr mempty (S.L (opRaw:operands))))+readApp opRaw@(S.WFSAtom (AId operator)) operands = do+  sym <- R.reader procSym+  prefixError ("in reading expression:\n"+               ++(T.unpack $ printSExpr mempty $ S.WFSList (opRaw:operands))++"\n") $+  -- Parse an expression of the form @(fnname operands ...)@+    case lookupOp @sym operator of+      Just (FloatOp1 fn) -> do+        args <- readExprs operands+        case args of+          [Some a1]+            | BaseFloatRepr _ <- W4.exprType a1 -> liftIO (Some <$> fn sym a1)+          _ -> E.throwError "Unable to unpack FloatOp1 arg in Formula.Parser readApp"+      Just (Op1 arg_types fn) -> do+        args <- readExprs operands+        exprAssignment arg_types args >>= \case+          Ctx.Empty Ctx.:> arg1 ->+            liftIO (Some <$> fn sym arg1)+      Just (Op2 arg_types fn) -> do+        args <- readExprs operands+        exprAssignment arg_types args >>= \case+          Ctx.Empty Ctx.:> arg1 Ctx.:> arg2 ->+              liftIO (Some <$> fn sym arg1 arg2)+      Just (Op3 arg_types fn) -> do+        args <- readExprs operands+        exprAssignment arg_types args >>= \case+          Ctx.Empty Ctx.:> arg1 Ctx.:> arg2 Ctx.:> arg3 ->+              liftIO (Some <$> fn sym arg1 arg2 arg3)+      Just (Op4 arg_types fn) -> do+        args <- readExprs operands+        exprAssignment arg_types args >>= \case+          Ctx.Empty Ctx.:> arg1 Ctx.:> arg2 Ctx.:> arg3 Ctx.:> arg4 ->+              liftIO (Some <$> fn sym arg1 arg2 arg3 arg4)+      Just (BVOp1 op) -> do+        Some expr <- readOneArg operands+        BVProof _ <- getBVProof expr+        liftIO $ Some <$> op sym expr+      Just (BVOp2 op) -> do+        (Some arg1, Some arg2)  <- readTwoArgs operands+        BVProof m <- prefixError "in arg 1: " $ getBVProof arg1+        BVProof n <- prefixError "in arg 2: " $ getBVProof arg2+        case testEquality m n of+          Just Refl -> liftIO (Some <$> op sym arg1 arg2)+          Nothing -> E.throwError $ printf "arguments to %s must be the same length, \+                                         \but arg 1 has length %s \+                                         \and arg 2 has length %s"+                                         operator+                                         (show m)+                                         (show n)+      Just (BVComp2 op) -> do+        (Some arg1, Some arg2)  <- readTwoArgs operands+        BVProof m <- prefixError "in arg 1: " $ getBVProof arg1+        BVProof n <- prefixError "in arg 2: " $ getBVProof arg2+        case testEquality m n of+          Just Refl -> liftIO (Some <$> op sym arg1 arg2)+          Nothing -> E.throwError $ printf "arguments to %s must be the same length, \+                                         \but arg 1 has length %s \+                                         \and arg 2 has length %s"+                                         operator+                                         (show m)+                                         (show n)+      Nothing ->+        -- Operators/syntactic-forms with types too+        -- complicated to nicely fit in the Op type+        case operator of+          "concat" -> do+            (Some arg1, Some arg2)  <- readTwoArgs operands+            BVProof _ <- prefixError "in arg 1: " $ getBVProof arg1+            BVProof _ <- prefixError "in arg 2: " $ getBVProof arg2+            liftIO (Some <$> W4.bvConcat sym arg1 arg2)+          "=" -> do+            (Some arg1, Some arg2)  <- readTwoArgs operands+            case testEquality (W4.exprType arg1) (W4.exprType arg2) of+              Just Refl -> liftIO (Some <$> W4.isEq sym arg1 arg2)+              Nothing -> E.throwError $+                printf "arguments must have same types, \+                       \but arg 1 has type %s \+                       \and arg 2 has type %s"+                (show (W4.exprType arg1))+                (show (W4.exprType arg2))+          "ite" -> do+            (Some test, Some then_, Some else_)  <- readThreeArgs operands+            case W4.exprType test of+              BaseBoolRepr ->+                case testEquality (W4.exprType then_) (W4.exprType else_) of+                  Just Refl -> liftIO (Some <$> W4.baseTypeIte sym test then_ else_)+                  Nothing -> E.throwError $+                    printf "then and else branches must have same type, \+                           \but then has type %s \+                           \and else has type %s"+                    (show (W4.exprType then_))+                    (show (W4.exprType else_))+              tp -> E.throwError $ printf "test expression must be a boolean; got %s" (show tp)+          "select" -> do+            (Some arr, Some idx)  <- readTwoArgs operands+            ArraySingleDim _ <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)+            let idx' = Ctx.empty Ctx.:> idx+            liftIO (Some <$> W4.arrayLookup sym arr idx')+          "store" -> do+            (Some arr, Some idx, Some expr)  <- readThreeArgs operands+            ArraySingleDim resRepr <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)+            case testEquality resRepr (W4.exprType expr) of+              Just Refl ->+                let idx' = Ctx.empty Ctx.:> idx+                in liftIO (Some <$> W4.arrayUpdate sym arr idx' expr)+              Nothing -> E.throwError $ printf "Array result type %s does not match %s"+                         (show resRepr)+                         (show (W4.exprType expr))+          "updateArray" -> do+            (Some arr, Some idx, Some expr)  <- readThreeArgs operands+            ArraySingleDim resRepr <- expectArrayWithIndex (W4.exprType idx) (W4.exprType arr)+            case testEquality resRepr (W4.exprType expr) of+              Just Refl ->+                let idx' = Ctx.empty Ctx.:> idx+                in liftIO (Some <$> W4.arrayUpdate sym arr idx' expr)+              Nothing -> E.throwError $ printf "Array result type %s does not match %s"+                         (show resRepr)+                         (show (W4.exprType expr))++          "arrayMap" ->+            -- arrayMap(idxs, array)++            -- The list of indexes is a list of pairs where each pair is:+            --+            -- > (indexList, expr)+++            -- Each list of indexes is a list of 'IndexLit' (since we have multi-dimensional indexing)+            case operands of+              [updateSExprList, arrSExpr] -> do+                Some arrExpr <- readExpr arrSExpr+                case W4.exprType arrExpr of+                  BaseArrayRepr idxReprs arrTyRepr -> do+                    updateMap <- expectArrayUpdateMap idxReprs arrTyRepr updateSExprList+                    liftIO (Some <$> W4.sbMakeExpr sym (W4.ArrayMap idxReprs arrTyRepr updateMap arrExpr))+                  repr -> E.throwError $ unwords ["expected an array type for the value in 'arrayMap', but got", show repr]+              _ -> E.throwError $ unwords ["expected a list of indices and an array expression, but got", show operands]++          "field" -> do+            case operands of+              [rawStruct, S.WFSAtom (AInt rawIdx)] -> do+                Some struct  <- readExpr rawStruct+                case W4.exprType struct of+                  (BaseStructRepr fldTpReprs) ->+                    case Ctx.intIndex (fromInteger rawIdx) (Ctx.size fldTpReprs) of+                      Just (Some i) -> liftIO (Some <$> W4.structField sym struct i)+                      Nothing -> E.throwError $+                        unwords ["invalid struct index, got", show fldTpReprs, "and", show rawIdx]+                  srepr -> E.throwError $ unwords ["expected a struct, got", show srepr]+              _ -> E.throwError $ unwords ["expected an arg and an Int, got", show operands]+          "struct" -> do+            case operands of+              [S.WFSList rawFldExprs] -> do+                Some flds <- readExprsAsAssignment rawFldExprs+                liftIO (Some <$> W4.mkStruct sym flds)+              _ -> E.throwError $ unwords ["struct expects a single operand, got", show operands]+          "sbvToInteger" -> do+            (Some arg) <- readOneArg operands+            BVProof _ <- getBVProof arg+            liftIO $ Some <$> W4.sbvToInteger sym arg+          "bvToInteger" -> do+            (Some arg) <- readOneArg operands+            BVProof _ <- getBVProof arg+            liftIO $ Some <$> W4.bvToInteger sym arg+          "integerToBV" -> do+            case operands of+              [S.WFSAtom (ANat width), rawValExpr] -> do+                Some x <- readExpr rawValExpr+                case (mkNatRepr width, W4.exprType x) of+                  (Some w, BaseIntegerRepr)+                    | Just LeqProof <- isPosNat w -> do+                    liftIO (Some <$> W4.integerToBV sym x w)+                  srepr -> E.throwError $ unwords ["expected a non-zero natural and an integer, got", show srepr]+              _ -> E.throwError $ unwords ["integerToBV expects two operands, the first of which is a nat, got", show operands]+          _ -> E.throwError $ printf "couldn't parse application of %s" (printSExpr mempty opRaw)+-- Parse an expression of the form @((_ extract i j) x)@.+readApp (S.WFSList [S.WFSAtom (AId "_"), S.WFSAtom (AId "extract"), S.WFSAtom (AInt iInt), S.WFSAtom (AInt jInt)])+  args = prefixError "in reading extract expression: " $ do+  sym <- R.reader procSym+  (Some arg) <- readOneArg args+  -- The SMT-LIB spec represents extracts differently than Crucible does. Per+  -- SMT: "extraction of bits i down to j from a bitvector of size m to yield a+  -- new bitvector of size n, where n = i - j + 1". Per Crucible:+  --+  -- > -- | Select a subsequence from a bitvector.+  -- > bvSelect :: (1 <= n, idx + n <= w)+  -- >          => sym+  -- >          -> NatRepr idx  -- ^ Starting index, from 0 as least significant bit+  -- >          -> NatRepr n    -- ^ Number of bits to take+  -- >          -> SymBV sym w  -- ^ Bitvector to select from+  -- >          -> IO (SymBV sym n)+  --+  -- The "starting index" seems to be from the bottom, so that (in slightly+  -- pseudocode)+  --+  -- > > bvSelect sym 0 8 (0x01020304:[32])+  -- > 0x4:[8]+  -- > > bvSelect sym 24 8 (0x01020304:[32])+  -- > 0x1:[8]+  --+  -- Thus, n = i - j + 1, and idx = j.+  let nInt = iInt - jInt + 1+      idxInt = jInt+  Some nNat <- prefixError "in calculating extract length: " $ intToNatM nInt+  Some idxNat <- prefixError "in extract lower bound: " $ intToNatM idxInt+  LeqProof <- fromMaybeError "extract length must be positive" $ isPosNat nNat+  BVProof lenNat <- getBVProof arg+  LeqProof <- fromMaybeError "invalid extract for given bitvector" $+    testLeq (addNat idxNat nNat) lenNat+  liftIO (Some <$> W4.bvSelect sym idxNat nNat arg)+-- Parse an expression of the form @((_ zero_extend i) x)@ or @((_ sign_extend i) x)@.+readApp (S.WFSList [S.WFSAtom (AId "_"), S.WFSAtom (AId extend), S.WFSAtom (AInt iInt)])+  args+  | extend == "zero_extend" ||+    extend == "sign_extend" = prefixError (printf "in reading %s expression: " extend) $ do+      sym <- R.reader procSym+      Some arg <- readOneArg args+      Some iNat <- intToNatM iInt+      iPositive <- fromMaybeError "must extend by a positive length" $ isPosNat iNat+      BVProof lenNat <- getBVProof arg+      let newLen = addNat lenNat iNat+      liftIO $ withLeqProof (leqAdd2 (leqRefl lenNat) iPositive) $+        let op = if extend == "zero_extend" then W4.bvZext else W4.bvSext+        in Some <$> op sym newLen arg+readApp (S.WFSList [S.WFSAtom (AId "_"), S.WFSAtom (AId "bvfill"), S.WFSAtom (AInt width)]) args =+  prefixError "in reading bvfill expression" $ do+    sym <- R.reader procSym+    Some arg <- readOneArg args+    case W4.exprType arg of+      BaseBoolRepr -> do+        Some widthRep <- intToNatM width+        LeqProof <- fromMaybeError "must extend by a positive length" $ isPosNat widthRep+        liftIO (Some <$> W4.bvFill sym widthRep arg)+      tyrep -> E.throwError ("Invalid argument type to bvFill: " ++ show tyrep)+readApp rator rands = E.throwError $ ("readApp could not parse the following: "+                                      ++ (T.unpack (printSExpr mempty $ S.WFSList (rator:rands))))+++-- | Try converting an 'Integer' to a 'NatRepr' or throw an error if not+-- possible.+intToNatM :: (E.MonadError String m) => Integer -> m (Some NatRepr)+intToNatM = fromMaybeError "integer must be non-negative to be a nat" . someNat++-- | Parse a list of array updates where each entry in the list is:+--+-- > (idxs, elt)+--+-- where each @idxs@ is a list (assignment) of indexes (with type @idxReprs@)+-- and each element is an expr.+--+-- NOTE: We assume that there are no duplicates in the list and apply the+-- updates in an arbitrary order.  This is true for any map serialized by this+-- library.+expectArrayUpdateMap+  :: forall sym t st fs tp i itp+   . (sym ~ W4.ExprBuilder t st fs)+  => Ctx.Assignment BaseTypeRepr (i Ctx.::> itp)+  -> BaseTypeRepr tp+  -> SExpr+  -> Processor sym (WAU.ArrayUpdateMap (W4.SymExpr sym) (i Ctx.::> itp) tp)+expectArrayUpdateMap idxReprs arrTyRepr updateSExprList =+  case updateSExprList of+    S.L items -> F.foldrM expectArrayUpdateEntry WAU.empty items+    _ -> E.throwError "Expected a list of array element updates in ArrayMap"+  where+    expectArrayUpdateEntry pair updateMap =+      case pair of+        S.L [S.L idxListExprs, elt] -> do+          idxs <- Ctx.traverseWithIndex (parseIndexLit idxListExprs) idxReprs+          Some x <- readExpr elt+          case testEquality arrTyRepr (W4.exprType x) of+            Just Refl -> return (WAU.insert arrTyRepr idxs x updateMap)+            Nothing -> E.throwError (concat [ "Invalid element type in ArrayMap update: expected "+                                            , show arrTyRepr+                                            , " but got "+                                            , show (W4.exprType x)])+        _ -> E.throwError "Unexpected ArrayMap update item structure"++-- | Safe list indexing+--+-- This version only traverses the list once (compared to computing the length+-- and then using unsafe indexing)+(!?) :: [a] -> Int -> Maybe a+lst !? idx+  | idx < 0 = Nothing+  | otherwise = go idx lst+  where+    go 0 (x:_xs) = Just x+    go i (_:xs) = go (i - 1) xs+    go _ [] = Nothing++-- | Parse a single 'WIL.IndexLit' out of a list of 'SExpr' (at the named index)+--+-- This is used to build the assignment of indexes+parseIndexLit :: [SExpr]+               -> Ctx.Index ctx tp+               -> BaseTypeRepr tp+               -> Processor sym (WIL.IndexLit tp)+parseIndexLit exprs idx repr+  | Just (S.A atom) <- exprs !? Ctx.indexVal idx =+      case (repr, atom) of+        (BaseBVRepr w, ABV w' val)+          | PN.intValue w == toInteger w' ->+            return (WIL.BVIndexLit w (BV.mkBV w val))+          | otherwise -> E.throwError ("Array update index bitvector size mismatch: expected " ++ show w ++ " but got " ++ show w')+        (BaseIntegerRepr, AInt i) -> return (WIL.IntIndexLit i)+        _ -> E.throwError ("Unexpected array update index type: " ++ show repr)+  | otherwise = E.throwError ("Invalid or missing array update index at " ++ show idx)++data ArrayJudgment :: BaseType -> BaseType -> Type where+  ArraySingleDim :: forall idx res.+                    BaseTypeRepr res+                 -> ArrayJudgment idx (BaseArrayType (Ctx.SingleCtx idx) res)++expectArrayWithIndex :: (E.MonadError String m) => BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)+expectArrayWithIndex dimRepr (BaseArrayRepr idxTpReprs resRepr) =+  case Ctx.viewAssign idxTpReprs of+    Ctx.AssignExtend rest idxTpRepr ->+      case Ctx.viewAssign rest of+        Ctx.AssignEmpty ->+          case testEquality idxTpRepr dimRepr of+            Just Refl -> return $ ArraySingleDim resRepr+            Nothing -> E.throwError $ unwords ["Array index type", show idxTpRepr,+                                               "does not match", show dimRepr]+        _ -> E.throwError "multidimensional arrays are not supported"+expectArrayWithIndex _ repr = E.throwError $ unwords ["expected an array, got", show repr]++exprAssignment ::+  forall sym ctx ex . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym), ShowF ex, W4.IsExpr ex)+  => Ctx.Assignment BaseTypeRepr ctx+  -> [Some ex]+  -> Processor sym (Ctx.Assignment ex ctx)+exprAssignment tpAssns exs = do+  Some exsAsn <- return $ Ctx.fromList exs+  exsRepr <- return $ FC.fmapFC W4.exprType exsAsn+  case testEquality exsRepr tpAssns of+    Just Refl -> return exsAsn+    Nothing -> E.throwError $+      "Unexpected expression types for " ++ show exsAsn+      ++ "\nExpected: " ++ show tpAssns+      ++ "\nGot: " ++ show exsRepr+++-- | Given the s-expressions for the bindings and body of a+-- let, parse the bindings into the Reader monad's state and+-- then parse the body with those newly bound variables.+readLetExpr ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => [SExpr]+  -- ^ Bindings in a let-expression.+  -> SExpr+  -- ^ Body of the let-expression.+  -> Processor sym (Some (W4.SymExpr sym))+readLetExpr [] body = readExpr body+readLetExpr ((S.WFSList [S.WFSAtom (AId x), e]):rst) body = do+  v <- readExpr e+  R.local (\c -> c {procLetEnv = (HM.insert x v) $ procLetEnv c}) $+    readLetExpr rst body+readLetExpr bindings _body = E.throwError $+  "invalid s-expression for let-bindings: " ++ (show bindings)+++readLetFnExpr ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => [SExpr]+  -- ^ Bindings in a let-expression.+  -> SExpr+  -- ^ Body of the let-expression.+  -> Processor sym (Some (W4.SymExpr sym))+readLetFnExpr [] body = readExpr body+readLetFnExpr ((S.WFSList [S.WFSAtom (AId f), e]):rst) body = do+  v <- readSymFn e+  R.local (\c -> c {procLetFnEnv = (HM.insert f v) $ procLetFnEnv c}) $+    readLetExpr rst body+readLetFnExpr bindings _body = E.throwError $+  "invalid s-expression for let-bindings: " ++ (show bindings)++  +-- | Parse an arbitrary expression.+readExpr ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => SExpr+  -> Processor sym (Some (W4.SymExpr sym))+readExpr (S.WFSAtom (AInt n)) = do+  sym <- R.reader procSym+  liftIO $ (Some <$> W4.intLit sym n)+readExpr (S.WFSAtom (ANat _)) =+  E.throwError "Bare Natural literals are no longer used"+readExpr (S.WFSAtom (ABool b)) = do+  sym <- R.reader procSym+  liftIO $ return $ Some $ W4.backendPred sym b+readExpr (S.WFSAtom (AFloat (Some repr) bf)) = do+  sym <- R.reader procSym+  liftIO $ (Some <$> W4.floatLit sym repr bf)+readExpr (S.WFSAtom (AStr prefix content)) = do+  sym <- R.reader procSym+  case prefix of+    (Some W4.UnicodeRepr) -> do+      s <- liftIO $ W4.stringLit sym $ W4.UnicodeLiteral content+      return $ Some $ s+    (Some W4.Char8Repr) -> do+      s <- liftIO $ W4.stringLit sym $ W4.Char8Literal $ T.encodeUtf8 content+      return $ Some $ s+    (Some W4.Char16Repr) -> E.throwError $ "Char16 strings are not yet supported"+readExpr (S.WFSAtom (AReal _)) = E.throwError $ "TODO: support readExpr for real literals"+readExpr (S.WFSAtom (ABV len val)) = do+  -- This is a bitvector literal.+  sym <- R.reader procSym+  -- The following two patterns should never fail, given that during parsing we+  -- can only construct BVs with positive length.+  case someNat (toInteger len) of+    Just (Some lenRepr) -> do+        pf <- case isPosNat lenRepr of+                Just pf -> return pf+                Nothing -> E.throwError "What4.Serialize.Parser.readExpr isPosNat failure"+        liftIO $ withLeqProof pf (Some <$> W4.bvLit sym lenRepr (BV.mkBV lenRepr val))+    Nothing -> E.throwError "SemMC.Formula.Parser.readExpr someNat failure"+  -- Just (Some lenRepr) <- return $ someNat (toInteger len)+  -- let Just pf = isPosNat lenRepr+  -- liftIO $ withLeqProof pf (Some <$> W4.bvLit sym lenRepr val)+-- Let-bound variable+readExpr (S.WFSAtom (AId name)) = do+  maybeBinding <- lookupExpr name+  -- We first check the local lexical environment (i.e., the+  -- in-scope let-bindings) before consulting the "global"+  -- scope.+  case maybeBinding of+    -- simply return it's bound value+    Just binding -> return binding+    Nothing -> E.throwError $ ("Unbound variable encountered during deserialization: "+                               ++ (T.unpack name))+readExpr (S.WFSList ((S.WFSAtom (AId "let")):rhs)) =+  case rhs of+    [S.WFSList bindings, body] -> readLetExpr bindings body+    _ -> E.throwError "ill-formed let s-expression"+readExpr (S.WFSList ((S.WFSAtom (AId "letfn")):rhs)) =+  case rhs of+    [S.WFSList bindings, body] -> readLetFnExpr bindings body+    _ -> E.throwError "ill-formed letfn s-expression"+readExpr (S.WFSList []) = E.throwError "ill-formed empty s-expression"+readExpr (S.WFSList (operator:operands)) = readApp operator operands++++-- | Parse multiple expressions in a list.+readExprs ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => [SExpr]+  -> Processor sym [Some (W4.SymExpr sym)]+readExprs exprs = mapM readExpr exprs++readExprsAsAssignment ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => [SExpr]+  -> Processor sym (Some (Ctx.Assignment (W4.SymExpr sym)))+readExprsAsAssignment exprs = Ctx.fromList <$> readExprs exprs+++readFnType ::+  forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))+  => SExpr+  -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)+readFnType (S.WFSList ((S.WFSAtom (AId "->")):typeSExprs)) =+  case unsnoc typeSExprs of+    Nothing ->+      E.throwError $ ("invalid type signature for function: "+                      ++ (T.unpack $ printSExpr mempty (S.L typeSExprs)))+    Just (domSExps, retSExp) -> do+      dom <- mapM readBaseType domSExps+      ret <- readBaseType retSExp+      return (dom, ret)+readFnType sexpr =+  E.throwError $ ("invalid type signature for function: "+                  ++ (T.unpack $ printSExpr mempty sexpr))++-- | If the list is empty, return 'Nothing'. If the list is non-empty, return+-- @'Just' (xs, x)@, where @xs@ is equivalent to calling 'init' on the list and+-- @x@ is equivalent to calling 'last' on the list.+unsnoc :: [a] -> Maybe ([a], a)+unsnoc []     = Nothing+unsnoc (x:xs) = case unsnoc xs of+                  Nothing    -> Just ([], x)+                  Just (a,b) -> Just (x:a, b)++readFnArgs ::+  forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))+  => [SExpr]+  -> Processor sym [Text]+readFnArgs [] = return []+readFnArgs ((S.WFSAtom (AId name)):rest) = do+  names <- (readFnArgs rest)+  return $ name:names+readFnArgs (badArg:_) =+  E.throwError $ ("invalid function argument encountered: "+                  ++ (T.unpack $ printSExpr mempty badArg))++someVarExpr ::+    forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))+  => sym+  -> Some (W4.BoundVar sym)+  -> Some (W4.SymExpr sym)+someVarExpr sym (Some bv) = Some (W4.varExpr sym bv)+++readSymFn ::+  forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)+  => SExpr+  -> Processor sym (SomeSymFn sym)+readSymFn (S.WFSList [ S.WFSAtom (AId "definedfn")+                     , S.WFSAtom (AStr _ rawSymFnName)+                     , rawFnType+                     , S.WFSList argVarsRaw+                     , bodyRaw+                     ]) = do+  sym <- R.reader procSym+  symFnName <- case W4.userSymbol (T.unpack rawSymFnName) of+                 Left _ -> E.throwError $ ("Bad symbolic function name : "+                                           ++ (T.unpack rawSymFnName))+                 Right solverSym -> return solverSym+  argNames <- readFnArgs argVarsRaw+  (argTys, _retTy) <- readFnType rawFnType+  E.when (not (length argTys == length argNames)) $+    E.throwError $ "Function type expected "+    ++ (show $ length argTys)+    ++ " args but found "+    ++ (show $ length argNames)+  argVars <- mapM (\(name, (Some ty)) ->+                     case W4.userSymbol (T.unpack name) of+                       Left _ -> E.throwError $ "Bad arg name : " ++ (T.unpack name)+                       Right solverSym -> liftIO $ Some <$> W4.freshBoundVar sym solverSym ty)+             $ zip argNames argTys+  (Some body) <- let newBindings = HM.fromList+                                   $ zip argNames+                                   $ map (someVarExpr sym) argVars+                 in R.local+                    (\env -> env {procLetEnv = HM.union (procLetEnv env) newBindings})+                    $ readExpr bodyRaw+  Some argVarAssignment <- return $ Ctx.fromList argVars+  symFn <- liftIO $ W4.definedFn sym symFnName argVarAssignment body W4.UnfoldConcrete+  return $ SomeSymFn symFn+readSymFn badSExp@(S.WFSList ((S.WFSAtom (AId "definedfn")):_)) =+  E.throwError $ ("invalid `definedfn`: " ++ (T.unpack $ printSExpr mempty badSExp))+readSymFn (S.WFSList [ S.WFSAtom (AId "uninterpfn")+                     , S.WFSAtom (AStr _ rawSymFnName)+                     , rawFnType+                     ]) = do+  sym <- R.reader procSym+  symFnName <- case W4.userSymbol (T.unpack rawSymFnName) of+                 Left _ -> E.throwError $ ("Bad symbolic function name : "+                                           ++ (T.unpack rawSymFnName))+                 Right solverSym -> return solverSym+  (argTys, (Some retTy)) <- readFnType rawFnType+  Some domain <- return $ Ctx.fromList argTys+  symFn <- liftIO $ W4.freshTotalUninterpFn sym symFnName domain retTy+  return $ SomeSymFn symFn+readSymFn badSExp@(S.WFSList ((S.WFSAtom (AId "uninterpfn")):_)) =+  E.throwError $ ("invalid `uninterpfn`: " ++ (T.unpack $ printSExpr mempty badSExp))+readSymFn sexpr = E.throwError ("invalid function definition: "+                                ++ (T.unpack $ printSExpr mempty sexpr))

@@ -0,0 +1,779 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE PatternSynonyms #-}++module What4.Serialize.Printer+  (+    serializeExpr+  , serializeExprWithConfig+  , serializeSymFn+  , serializeSymFnWithConfig+  , serializeBaseType+  , convertBaseTypes+  , Config(..)+  , Result(..)+  , printSExpr+  , defaultConfig+  , SExpr+  , Atom(..)+  , SomeExprSymFn(..)+  , S.WellFormedSExpr(..)+  , ident, int, string+  , bitvec, bool, nat, real+  , ppFreeVarEnv+  , ppFreeSymFnEnv+  , pattern S.L+  , pattern S.A+  ) where++import           Numeric.Natural+import qualified Data.Foldable as F+import           Data.Set ( Set )+import qualified Data.Set as Set+import           Data.Map.Ordered (OMap)+import qualified Data.Map.Ordered as OMap+import qualified Data.BitVector.Sized as BV+import           Data.Parameterized.Some+import qualified Data.Parameterized.Context as Ctx+import qualified Data.Parameterized.NatRepr as NR+import qualified Data.Parameterized.Nonce as Nonce+import qualified Data.Parameterized.TraversableFC as FC++import           Data.Text (Text)+import qualified Data.Text as T+import qualified Data.Text.Encoding as T+import           Data.Word ( Word64 )+import qualified Control.Monad as M+import           Control.Monad.State.Strict (State)+import qualified Control.Monad.State.Strict as MS++import qualified Data.SCargot.Repr.WellFormed as S++import           What4.BaseTypes+import qualified What4.Expr as W4+import qualified What4.Expr.ArrayUpdateMap as WAU+import qualified What4.Expr.BoolMap as BooM+import qualified What4.Expr.Builder as W4+import qualified What4.Expr.WeightedSum as WSum+import qualified What4.IndexLit as WIL+import qualified What4.Interface as W4+import qualified What4.Symbol as W4+import qualified What4.Utils.StringLiteral as W4S+++import           What4.Serialize.SETokens ( Atom(..), printSExpr+                                          , ident, int, nat, string+                                          , bitvec, bool, real, float+                                          )++type SExpr = S.WellFormedSExpr Atom++data SomeExprSymFn t = forall dom ret. SomeExprSymFn (W4.ExprSymFn t dom ret)++instance Eq (SomeExprSymFn t) where+  (SomeExprSymFn fn1) == (SomeExprSymFn fn2) =+    case W4.testEquality (W4.symFnId fn1) (W4.symFnId fn2) of+      Just _ -> True+      _ -> False++instance Ord (SomeExprSymFn t) where+  compare (SomeExprSymFn fn1) (SomeExprSymFn fn2) =+    compare (Nonce.indexValue $ W4.symFnId fn1) (Nonce.indexValue $ W4.symFnId fn2) +++instance Show (SomeExprSymFn t) where+  show (SomeExprSymFn f) = show f+++type VarNameEnv t = OMap (Some (W4.ExprBoundVar t)) Text+type FnNameEnv t  = OMap (SomeExprSymFn t) Text++ppFreeVarEnv :: VarNameEnv t -> String+ppFreeVarEnv env = show $ map toStr entries+  where entries = OMap.toAscList env+        toStr :: ((Some (W4.ExprBoundVar t)), Text) -> (String, String, String)+        toStr ((Some var), newName) = ( T.unpack $ W4.solverSymbolAsText $ W4.bvarName var+                                      , show $ W4.bvarType var+                                      , T.unpack newName+                                      )++ppFreeSymFnEnv :: FnNameEnv t -> String+ppFreeSymFnEnv env = show $ map toStr entries+  where entries = OMap.toAscList env+        toStr :: ((SomeExprSymFn t), Text) -> (String, String, String)+        toStr ((SomeExprSymFn fn), newName) = ( T.unpack $ W4.solverSymbolAsText $ W4.symFnName fn+                                              , show $ W4.symFnArgTypes fn+                                              , T.unpack newName+                                              )++-- | Controls how expressions and functions are serialized.+data Config =+  Config+  { cfgAllowFreeVars :: Bool+  -- ^ When @True@, any free What4 @ExprBoundVar@+  -- encountered is simply serialized with a unique name,+  -- and the mapping from What4 ExprBoundVar to unique names+  -- is returned after serialization. When False, an error+  -- is raised when a "free" @ExprBoundVar@ is encountered.+  , cfgAllowFreeSymFns :: Bool+  -- ^ When @True@, any encountered What4 @ExprSymFn@ during+  -- serialization is simply assigned a unique name and the+  -- mapping from What4 ExprSymFn to unique name is returned+  -- after serialization. When @False, encountered+  -- ExprSymFns are serialized at the top level of the+  -- expression in a `(letfn ([f ...]) ...)`.+  }++data Result t =+  Result+  { resSExpr :: S.WellFormedSExpr Atom+  -- ^ The serialized term.+  , resFreeVarEnv :: VarNameEnv t+  -- ^ The free BoundVars that were encountered during+  -- serialization and their associated fresh name+  -- that was used to generate the s-expression.+  , resSymFnEnv :: FnNameEnv t+  -- ^ The SymFns that were encountered during serialization+  -- and their associated fresh name that was used to+  -- generate the s-expression.+  }+++defaultConfig :: Config+defaultConfig = Config { cfgAllowFreeVars = False, cfgAllowFreeSymFns = False}++-- This file is organized top-down, i.e., from high-level to low-level.++-- | Serialize a What4 Expr as a well-formed s-expression+-- (i.e., one which contains no improper lists). Equivalent+-- to @(resSExpr (serializeExpr' defaultConfig))@. Sharing+-- in the AST is achieved via a top-level let-binding around+-- the emitted expression (unless there are no terms with+-- non-atomic terms which can be shared).+serializeExpr :: W4.Expr t tp -> SExpr+serializeExpr = resSExpr . (serializeExprWithConfig defaultConfig)++-- | Serialize a What4 Expr as a well-formed s-expression+-- (i.e., one which contains no improper lists) according to+-- the configuration. Sharing in the AST is achieved via a+-- top-level let-binding around the emitted expression+-- (unless there are no terms with non-atomic terms which+-- can be shared).+serializeExprWithConfig :: Config -> W4.Expr t tp -> Result t+serializeExprWithConfig cfg expr = serializeSomething cfg (convertExprWithLet expr)++-- | Serialize a What4 ExprSymFn as a well-formed+-- s-expression (i.e., one which contains no improper+-- lists). Equivalent to @(resSExpr (serializeSymFn'+-- defaultConfig))@. Sharing in the AST is achieved via a+-- top-level let-binding around the emitted expression+-- (unless there are no terms with non-atomic terms which+-- can be shared).+serializeSymFn :: W4.ExprSymFn t dom ret -> SExpr+serializeSymFn = resSExpr . (serializeSymFnWithConfig defaultConfig)+++-- | Serialize a What4 ExprSymFn as a well-formed+-- s-expression (i.e., one which contains no improper lists)+-- according to the configuration. Sharing in the AST is+-- achieved via a top-level let-binding around the emitted+-- expression (unless there are no terms with non-atomic+-- terms which can be shared).+serializeSymFnWithConfig :: Config -> W4.ExprSymFn t dom ret -> Result t+serializeSymFnWithConfig cfg fn = serializeSomething cfg (convertSymFn fn)++-- | Run the given Memo computation to produce a well-formed+-- s-expression (i.e., one which contains no improper lists)+-- according to the configuration. Sharing in the AST is+-- achieved via a top-level let-binding around the emitted+-- expression (unless there are no terms with non-atomic+-- terms which can be shared).+serializeSomething :: Config -> Memo t SExpr -> Result t+serializeSomething cfg something =+  let (maybeLetFn, getFreeSymFnEnv) = if cfgAllowFreeSymFns cfg+                                      then (return, envFreeSymFnEnv)+                                      else (letFn, \_ -> OMap.empty)+      (sexpr, menv) = runMemo cfg $ something >>= maybeLetFn+      letBindings = map (\(varName, boundExpr) -> S.L [ ident varName, boundExpr ])+                    $ map snd+                    $ OMap.assocs+                    $ envLetBindings menv+      res = mkLet letBindings sexpr+    in Result { resSExpr = res+              , resFreeVarEnv = envFreeVarEnv menv+              , resSymFnEnv = getFreeSymFnEnv menv+              }+++serializeBaseType :: BaseTypeRepr tp -> SExpr+serializeBaseType bt = convertBaseType bt++data MemoEnv t =+  MemoEnv+  { envConfig :: !Config+  -- ^ User provided configuration for serialization.+  , envIdCounter :: !Natural+  -- ^ Internal counter for generating fresh names+  , envLetBindings :: !(OMap SKey (Text, SExpr))+  -- ^ Mapping from What4 expression nonces to the+  -- corresponding let-variable name (the @fst@) and the+  -- corresponding bound term (the @snd@).+  , envFreeVarEnv :: !(VarNameEnv t)+  -- ^ Mapping from What4 ExprBoundVar to the fresh names+  -- assigned to them for serialization purposes.+  , envFreeSymFnEnv :: !(FnNameEnv t)+  -- ^ Mapping from What4 ExprSymFn to the fresh names+  -- assigned to them for serialization purposes.+  , envBoundVars :: Set (Some (W4.ExprBoundVar t))+  -- ^ Set of currently in-scope What4 ExprBoundVars (i.e.,+  -- ExprBoundVars for whom we are serializing the body of+  -- their binding form).+  }++initEnv :: forall t . Config -> MemoEnv t+initEnv cfg = MemoEnv { envConfig = cfg+                      , envIdCounter = 0+                      , envLetBindings = OMap.empty+                      , envFreeVarEnv = OMap.empty+                      , envFreeSymFnEnv = OMap.empty+                      , envBoundVars = Set.empty+                      }++type Memo t a = State (MemoEnv t) a++runMemo :: Config -> (Memo t a) -> (a, MemoEnv t)+runMemo cfg m = MS.runState m $ initEnv cfg+++-- | Serialize the given sexpression within a @letfn@ which+-- serializes and binds all of the encountered SymFns. Note:+-- this recursively also discovers and then serializes+-- SymFns referenced within the body of the SymFns+-- encountered thus far.+letFn :: SExpr -> Memo t SExpr+letFn sexpr = go [] [] Set.empty+  where+    go :: [((SomeExprSymFn t), Text)] -> [(Text, SExpr)] -> Set Text ->  Memo t SExpr+    go [] fnBindings seen = do+      -- Although the `todo` list is empty, we may have+      -- encountered some SymFns along the way, so check for+      -- those and serialize any previously unseen SymFns.+      newFns <- MS.gets (filter (\(_symFn, varName) -> not $ Set.member varName seen)+                         . OMap.assocs+                         . envFreeSymFnEnv)+      if null newFns+        then if null fnBindings+             then return sexpr+             else let bs = map (\(name, def) -> S.L [ident name, def]) fnBindings+                  in return $ S.L [ident "letfn" , S.L bs, sexpr]+        else go newFns fnBindings seen+    go (((SomeExprSymFn nextFn), nextFnName):todo) fnBindings seen = do+      nextSExpr <- convertSymFn nextFn+      let fnBindings' = (nextFnName, nextSExpr):fnBindings+          seen' = Set.insert nextFnName seen+      go todo fnBindings' seen'+++-- | Converts the given What4 expression into an+-- s-expression and clears the let-binding cache (since it+-- just emitted a let binding with any necessary let-bound+-- vars).+convertExprWithLet :: W4.Expr t tp -> Memo t SExpr+convertExprWithLet expr = do+  b <- convertExpr expr+  bs <- map (\(varName, boundExpr) -> S.L [ ident varName, boundExpr ])+        <$> map snd+        <$> OMap.assocs+        <$> MS.gets envLetBindings+  MS.modify' (\r -> r {envLetBindings = OMap.empty})+  return $ mkLet bs b++mkLet :: [SExpr] -> SExpr -> SExpr+mkLet [] body       = body+mkLet bindings body = S.L [ident "let", S.L bindings, body]+++-- | Converts a What4 ExprSymFn into an s-expression within+-- the Memo monad (i.e., no @let@ or @letfn@s are emitted).+convertSymFn :: forall t args ret+              . W4.ExprSymFn t args ret+             -> Memo t SExpr+convertSymFn symFn@(W4.ExprSymFn _ symFnName symFnInfo _) = do+ case symFnInfo of+   W4.DefinedFnInfo argVars body _ -> do+     let sArgTs = convertBaseTypes (W4.fnArgTypes symFn)+         sRetT = convertBaseType (W4.fnReturnType symFn)+     argsWithFreshNames <- let rawArgs = FC.toListFC Some argVars+                           in mapM getBoundVarWithFreshName rawArgs+     let (origBoundVars, freshArgNames) = unzip argsWithFreshNames+     -- Convert the body with the bound variable set and+     -- free-variable mapping extended to reflect being+     -- under the function's binders.+     sExpr <- MS.withState (\ms -> let boundVars = envBoundVars ms+                                       fvEnv = envFreeVarEnv ms+                             in ms { envBoundVars = Set.union boundVars (Set.fromList origBoundVars)+                                   , envFreeVarEnv = fvEnv OMap.<>| (OMap.fromList argsWithFreshNames)})+              $ convertExprWithLet body+     return $ S.L [ ident "definedfn"+                  , string (Some W4.UnicodeRepr) $ W4.solverSymbolAsText symFnName+                  , S.L ((ident "->"):sArgTs ++ [sRetT])+                  , S.L $ map ident freshArgNames+                  , sExpr+                  ]+   W4.UninterpFnInfo argTs retT ->+     let sArgTs = convertBaseTypes argTs+         sRetT = convertBaseType retT+     in return $ S.L [ ident "uninterpfn"+                     , string (Some W4.UnicodeRepr) $ W4.solverSymbolAsText symFnName+                     , S.L ((ident "->"):sArgTs ++ [sRetT])+                     ]+   W4.MatlabSolverFnInfo _msfn _argTs _body ->+     error "MatlabSolverFnInfo SymFns are not yet supported"+  where+    getBoundVarWithFreshName ::+      (Some (W4.ExprBoundVar t)) ->+      Memo t (Some (W4.ExprBoundVar t), Text)+    getBoundVarWithFreshName someVar@(Some var) = do+      nm <- freshName (W4.bvarType var)+      return (someVar, nm)+++-- | Key for sharing SExpr construction. Internally indexes are expression nonces,+-- but the let-binding identifiers are based on insertion order to the OMap+newtype SKey = SKey {sKeyValue :: Word64}+  deriving (Eq, Ord, Show)++++freshName :: W4.BaseTypeRepr tp -> Memo t Text+freshName tp = do+  idCount <- MS.gets envIdCounter+  MS.modify' $ (\e -> e {envIdCounter = idCount + 1})+  let prefix = case tp of+                 W4.BaseBoolRepr{} -> "bool"+                 W4.BaseIntegerRepr{} -> "int"+                 W4.BaseRealRepr{} -> "real"+                 W4.BaseFloatRepr{} -> "fl"+                 W4.BaseStringRepr{} -> "str"+                 W4.BaseComplexRepr -> "cmplx"+                 W4.BaseBVRepr{} -> "bv"+                 W4.BaseStructRepr{} -> "struct"+                 W4.BaseArrayRepr{} -> "arr"+  return $ T.pack $ prefix++(show $ idCount)++freshFnName :: W4.ExprSymFn t args ret -> Memo t Text+freshFnName fn = do+  idCount <- MS.gets envIdCounter+  MS.modify' $ (\e -> e {envIdCounter = idCount + 1})+  let prefix = case W4.symFnInfo fn of +                 W4.UninterpFnInfo{} -> "ufn"+                 W4.DefinedFnInfo{} -> "dfn"+                 W4.MatlabSolverFnInfo{} -> "mfn"+  return $ T.pack $ prefix++(show $ idCount)++++exprSKey :: W4.Expr t tp -> Maybe SKey+exprSKey x = SKey . Nonce.indexValue <$> W4.exprMaybeId x++-- | Allocate a fresh variable for the given+-- nonce-key/s-expression and save the variable/expression+-- mapping in the Memo monad.+addLetBinding :: SKey -> SExpr -> W4.BaseTypeRepr tp -> Memo t Text+addLetBinding key sexp tp = do+  letVarName <- freshName tp+  curLetBindings <- MS.gets envLetBindings+  MS.modify' $ (\e -> e {envLetBindings =  curLetBindings OMap.|> (key, (letVarName, sexp))})+  return letVarName++-- | Converts a What 4 expression into an s-expression+-- within the Memo monad (i.e., no @let@ or @letfn@s are+-- emitted in the result).+convertExpr :: forall t tp . W4.Expr t tp -> Memo t SExpr+convertExpr initialExpr = do+  case exprSKey initialExpr of+    Nothing -> go initialExpr+    Just key -> do+      letCache <- MS.gets envLetBindings+      case OMap.lookup key letCache of+        Just (name, _) -> return $ ident name+        Nothing -> do+          sexp <- go initialExpr+          case sexp of+            S.A _ -> return sexp -- Don't memoize atomic s-expressions - that's just silly.+            _ -> do +              letVarName <- addLetBinding key sexp (W4.exprType initialExpr)+              return $ ident letVarName+  where go :: W4.Expr t tp -> Memo t SExpr+        go (W4.SemiRingLiteral W4.SemiRingIntegerRepr val _) = return $ int val -- do we need/want these?+        go (W4.SemiRingLiteral W4.SemiRingRealRepr val _) = return $ real val+        go (W4.SemiRingLiteral (W4.SemiRingBVRepr _ sz) val _) = return $ bitvec (natValue sz) (BV.asUnsigned val)+        go (W4.StringExpr str _) =+          case (W4.stringLiteralInfo str) of+            W4.UnicodeRepr -> return $ string (Some W4.UnicodeRepr) (W4S.fromUnicodeLit str)+            W4.Char8Repr -> return $ string (Some W4.Char8Repr) $ T.decodeUtf8 $ W4S.fromChar8Lit str+            W4.Char16Repr -> error "Char16 strings are not yet supported"+              -- TODO - there is no `W4S.toLEByteString` currently... hmm...+              -- return $ string (Some W4.Char16Repr) $ T.decodeUtf16LE $ W4S.toLEByteString $ W4S.fromChar16Lit str+        go (W4.FloatExpr prec bf _) = return $ float prec bf+        go (W4.BoolExpr b _) = return $ bool b+        go (W4.AppExpr appExpr) = convertAppExpr' appExpr+        go (W4.NonceAppExpr nae) =+          case W4.nonceExprApp nae of+            W4.FnApp fn args -> convertFnApp fn args+            W4.Forall {} -> error "Forall NonceAppExpr not yet supported"+            W4.Exists {} -> error "Exists NonceAppExpr not yet supported"+            W4.ArrayFromFn {} -> error "ArrayFromFn NonceAppExpr not yet supported"+            W4.MapOverArrays {} -> error "MapOverArrays NonceAppExpr not yet supported"+            W4.ArrayTrueOnEntries {} -> error "ArrayTrueOnEntries NonceAppExpr not yet supported"+            W4.Annotation {} -> error "Annotation NonceAppExpr not yet supported"+        go (W4.BoundVarExpr var) = convertBoundVarExpr var++-- | Serialize bound variables as the s-expression identifier `name_nonce`. This allows us to+-- preserve their human-readable name while ensuring they are globally unique w/ the nonce suffix.+convertBoundVarExpr :: forall t tp. W4.ExprBoundVar t tp -> Memo t SExpr+convertBoundVarExpr x = do+  fvsAllowed <- MS.gets (cfgAllowFreeVars . envConfig)+  bvs <- MS.gets envBoundVars+  -- If this variable is not bound (in the standard syntactic sense)+  -- and free variables are not explicitly permitted, raise an error.+  MS.when ((not $ Set.member (Some x) bvs) && (not fvsAllowed)) $+    error $+    "encountered the free What4 ExprBoundVar `"+    ++ (T.unpack (W4.solverSymbolAsText (W4.bvarName x)))+    ++ "`, but the user-specified configuration dissallows free variables."+  -- Get the renaming cache and either use the name already generated+  -- or generate a fresh name and record it.+  varEnv <- MS.gets envFreeVarEnv+  case OMap.lookup (Some x) varEnv of+    Just var -> return $ ident var+    Nothing -> do+      varName <- freshName $ W4.bvarType x+      MS.modify' $ (\e -> e {envFreeVarEnv = varEnv OMap.|> ((Some x), varName)})+      return $ ident varName+++convertAppExpr' :: forall t tp . W4.AppExpr t tp -> Memo t SExpr+convertAppExpr' = go . W4.appExprApp+  where go :: forall tp' . W4.App (W4.Expr t) tp' -> Memo t SExpr+        go (W4.BaseIte _bt _ e1 e2 e3) = do+          s1 <- goE e1+          s2 <- goE e2+          s3 <- goE e3+          return $ S.L [ident "ite", s1, s2, s3]+        go (W4.BaseEq _bt e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "=", s1, s2]+        go (W4.NotPred e) = do+          s <- goE e+          return $ S.L [ident "notp", s]+        go (W4.ConjPred bm) = convertBoolMap "andp" True bm+        go (W4.BVSlt e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "bvslt", s1, s2]+        go (W4.BVUlt e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "bvult", s1, s2]+        go (W4.BVConcat _ e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "concat", s1, s2]+        go (W4.BVSelect idx n bv) = extract i j bv+          -- See SemMC.Formula.Parser.readExtract for the explanation behind+          -- these values.+          where i = intValue n + j - 1+                j = intValue idx++        -- Note that because the SemiRing has an identity element that+        -- always gets applied, resulting in lots of additional,+        -- unnecessary elements like: "(bvand #xffffffff TERM)".+        -- These will get manifested in the stored form (but generally+        -- _not_ via DSL-generated versions since they don't output+        -- via Printer) and result in longer stored forms.  They could+        -- be eliminated by checking for the identity (e.g. "if mul ==+        -- SR.one (WSum.sumRepr sm)") but the re-loaded representation+        -- will still use the SemiRing, so it's probably not worth the+        -- effort to reduce these.+        go (W4.SemiRingSum sm) =+          case WSum.sumRepr sm of+            W4.SemiRingBVRepr W4.BVArithRepr w ->+              let smul mul e = do+                    s <- goE e+                    return $ S.L [ ident "bvmul", bitvec (natValue w) (BV.asUnsigned mul), s]+                  sval v = return $ bitvec (natValue w) (BV.asUnsigned v)+                  add x y = return $ S.L [ ident "bvadd", x, y ]+              in WSum.evalM add smul sval sm+            W4.SemiRingBVRepr W4.BVBitsRepr w ->+              let smul mul e = do+                    s <- goE e+                    return $ S.L [ ident "bvand", bitvec (natValue w) (BV.asUnsigned mul), s]+                  sval v = return $ bitvec (natValue w) (BV.asUnsigned v)+                  add x y = let op = ident "bvxor" in return $ S.L [ op, x, y ]+              in WSum.evalM add smul sval sm+            W4.SemiRingIntegerRepr ->+              let smul mul e = do+                    s <- goE e+                    return $ S.L [ ident "intmul", int mul, s]+                  sval v = return $ int v+                  add x y = return $ S.L [ ident "intadd", x, y ]+              in WSum.evalM add smul sval sm+            W4.SemiRingRealRepr    -> error "SemiRingSum RealRepr not supported"++        go (W4.SemiRingProd pd) =+          case WSum.prodRepr pd of+            W4.SemiRingBVRepr W4.BVArithRepr w -> do+              let pmul x y = return $ S.L [ ident "bvmul", x, y ]+              maybeS <- WSum.prodEvalM pmul goE pd+              case maybeS of+                Just s -> return s+                Nothing -> return $ bitvec (natValue w) 1+            W4.SemiRingBVRepr W4.BVBitsRepr w -> do+              let pmul x y = return $ S.L [ ident "bvand", x, y ]+              maybeS <- WSum.prodEvalM pmul goE pd+              case maybeS of+                Just s -> return s+                Nothing -> return $ bitvec (natValue w) 1+            W4.SemiRingIntegerRepr -> do+              let pmul x y = return $ S.L [ ident "intmul", x, y ]+              maybeS <- WSum.prodEvalM pmul goE pd+              case maybeS of+                Just s -> return s+                Nothing -> return $ int 1+            W4.SemiRingRealRepr    -> error "convertApp W4.SemiRingProd Real unsupported"++        go (W4.SemiRingLe sr e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          case sr of+            W4.OrderedSemiRingIntegerRepr -> do+              return $ S.L [ ident "intle", s1, s2]+            W4.OrderedSemiRingRealRepr -> error $ "Printer: SemiRingLe is not supported for reals"++        go (W4.BVOrBits width bs) = do+          let op = ident "bvor"+          case W4.bvOrToList bs of+            [] -> return $ bitvec (NR.natValue width) 0+            (x:xs) -> do+              e <- goE x+              let f = (\acc b -> do+                          b' <- goE b+                          return $ S.L [op, b', acc])+              M.foldM f e xs+        go (W4.BVUdiv _ e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "bvudiv", s1, s2]+        go (W4.BVUrem _ e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "bvurem", s1, s2]+        go (W4.BVSdiv _ e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "bvsdiv", s1, s2]+        go (W4.BVSrem _ e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "bvsrem", s1, s2]+        go (W4.BVShl _ e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "bvshl", s1, s2]+        go (W4.BVLshr _ e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "bvlshr", s1, s2]+        go (W4.BVAshr _ e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "bvashr", s1, s2]+        go (W4.BVZext r e) = extend "zero" (intValue r) e+        go (W4.BVSext r e) = extend "sign" (intValue r) e+        go (W4.BVFill r e) = do+          s <- goE e+          return $ S.L [ S.L [ident "_", ident "bvfill", int (intValue r)]+                       , s+                       ]++        go (W4.BVToInteger e) = do+          s <- goE e+          return $ S.L [ident "bvToInteger", s]++        go (W4.SBVToInteger e) = do+          s <- goE e+          return $ S.L [ident "sbvToInteger", s]++        go (W4.FloatNeg _repr e) = do+          s <- goE e+          return $ S.L [ident "floatneg", s]+        go (W4.FloatAbs _repr e) = do+          s <- goE e+          return $ S.L [ident "floatabs", s]++        go (W4.IntDiv e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "intdiv", s1, s2]+        go (W4.IntMod e1 e2) = do+          s1 <- goE e1+          s2 <- goE e2+          return $ S.L [ident "intmod", s1, s2]+        go (W4.IntAbs e1) = do+          s1 <- goE e1+          return $ S.L [ident "intabs", s1]+        go (W4.IntegerToBV e wRepr)  = do+          s <- goE e+          return $ S.L [ident "integerToBV"+                        , nat $ natValue wRepr+                        , s]++        go (W4.StructCtor _tps es) = do+          ss <- convertExprAssignment es+          return $ S.L [ident "struct", S.L ss]+        go (W4.StructField e ix _fieldTp) = do+          s <- goE e+          return $ S.L [ident "field"+                        , s+                        , int $ toInteger $ Ctx.indexVal ix+                        ]++        go (W4.UpdateArray _ _ e1 es e2) = do+          s1 <- goE e1+          ss <- convertExprAssignment es+          s2 <- goE e2+          case ss of+            [idx] -> return $ S.L [ ident "updateArray", s1, idx, s2]+            _ -> error $ "multidimensional arrays not supported"+        go (W4.SelectArray _ e es) = do+          s <- goE e+          ss <- convertExprAssignment es+          case ss of+            [idx] -> return $ S.L [ ident "select", s, idx]+            _ -> error $ "multidimensional arrays not supported"++        go (W4.ArrayMap _idxReprs _resRepr updateMap arr) = do+          updates <- mapM convertArrayUpdate (WAU.toList updateMap)+          arr' <- goE arr+          return $ S.L [ ident "arrayMap"+                       , S.L updates+                       , arr'+                       ]++        go app = error $ "unhandled App: " ++ show app++        convertArrayUpdate :: forall tp1 ctx . (Ctx.Assignment WIL.IndexLit ctx, W4.Expr t tp1) -> Memo t SExpr+        convertArrayUpdate (idxLits, e) = do+          e' <- goE e+          return $ S.L [ S.L (FC.toListFC convertIndexLit idxLits)+                       , e'+                       ]++        -- -- -- -- Helper functions! -- -- -- --+        +        goE :: forall tp' . W4.Expr t tp' -> Memo t SExpr+        goE = convertExpr++        extend :: forall w. Text -> Integer -> W4.Expr t (BaseBVType w) -> Memo t SExpr+        extend op r e = do+          let w = case W4.exprType e of BaseBVRepr len -> intValue len+              extension = r - w+          s <- goE e+          return $ S.L [ S.L [ ident "_", ident $ op <> "_extend", int extension ]+                        , s+                        ]++        extract :: forall tp'. Integer -> Integer -> W4.Expr t tp' -> Memo t SExpr+        extract i j bv = do+          s <- goE bv+          return $ S.L [ S.L [ ident "_", ident "extract", int i, int j ]+                        , s+                        ]++        convertBoolMap :: Text -> Bool -> BooM.BoolMap (W4.Expr t) -> Memo t SExpr+        convertBoolMap op base bm =+          let strBase b = if b+                          then S.L [ident "=", bitvec 1 0, bitvec 1 0]  -- true+                          else S.L [ident "=", bitvec 1 0, bitvec 1 1]  -- false+              strNotBase = strBase . not+          in case BooM.viewBoolMap bm of+               BooM.BoolMapUnit -> return $ strBase base+               BooM.BoolMapDualUnit -> return $ strNotBase base+               BooM.BoolMapTerms ts ->+                 let onEach e r = do+                       s <- arg e+                       return $ S.L [ident op, s, r]+                     arg (t, BooM.Positive) = goE t+                     arg (t, BooM.Negative) = do+                       s <- goE t+                       return $ S.L [ident "notp", s]+                 in F.foldrM onEach (strBase base) ts++convertIndexLit :: WIL.IndexLit tp -> SExpr+convertIndexLit il =+  case il of+    WIL.IntIndexLit iidx -> int iidx+    WIL.BVIndexLit irep bvidx -> bitvec (natValue irep) (BV.asUnsigned bvidx)++convertExprAssignment ::+  Ctx.Assignment (W4.Expr t) sh+  -> Memo t [SExpr]+convertExprAssignment es =+  mapM (\(Some e) -> convertExpr e) (FC.toListFC Some es)++convertFnApp ::+  W4.ExprSymFn t args ret+  -> Ctx.Assignment (W4.Expr t) args+  -> Memo t SExpr+convertFnApp fn args = do+  argSExprs <- convertExprAssignment args+  fnEnv <- MS.gets envFreeSymFnEnv+  case OMap.lookup (SomeExprSymFn fn) fnEnv of+    Just fnName ->+      return $ S.L $ (ident "call"):(ident fnName):argSExprs+    Nothing -> do+      varName <- freshFnName fn+      MS.modify' $ (\e -> e {envFreeSymFnEnv =  fnEnv OMap.|> ((SomeExprSymFn fn), varName)})+      return $ S.L $ (ident "call"):(ident varName):argSExprs+++convertBaseType :: BaseTypeRepr tp -> SExpr+convertBaseType tp = case tp of+  W4.BaseBoolRepr -> S.A $ AId "Bool"+  W4.BaseIntegerRepr -> S.A $ AId "Int"+  W4.BaseRealRepr -> S.A $ AId "Real"+  W4.BaseStringRepr si -> S.L [S.A $ AId "String", convertStringInfo si]+  W4.BaseComplexRepr -> S.A $ AId "Complex"+  W4.BaseBVRepr wRepr -> S.L [S.A (AId "BV"), S.A (AInt (NR.intValue wRepr)) ]+  W4.BaseStructRepr tps -> S.L [ S.A (AId "Struct"), S.L (convertBaseTypes tps) ]+  W4.BaseArrayRepr ixs repr -> S.L [S.A (AId "Array"), S.L $ convertBaseTypes ixs , convertBaseType repr]+  W4.BaseFloatRepr (W4.FloatingPointPrecisionRepr eRepr sRepr) ->+    S.L [ S.A (AId "Float"), S.A (AInt (NR.intValue eRepr)), S.A (AInt (NR.intValue sRepr)) ]++++convertStringInfo :: StringInfoRepr si -> SExpr+convertStringInfo W4.Char8Repr = ident "Char8"+convertStringInfo W4.Char16Repr = ident "Char16"+convertStringInfo W4.UnicodeRepr = ident "Unicode"++-- | Convert an Assignment of base types into a list of base+-- types SExpr, where the left-to-right syntactic ordering+-- of the types is maintained.+convertBaseTypes ::+  Ctx.Assignment BaseTypeRepr tps+  -> [SExpr]+convertBaseTypes asn = FC.toListFC convertBaseType asn

@@ -0,0 +1,259 @@+-- | Definition of the S-Expression tokens used to+-- (de)serialize What4 expressions.++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++module What4.Serialize.SETokens+    ( Atom(..)+    , string, ident, int, nat, bitvec, bool, real, float+    , string', ident'+    , printAtom+    , printSExpr+    , parseSExpr+    )+    where++import qualified Data.Foldable as F+import qualified Data.Parameterized.NatRepr as PN+import qualified Data.SCargot as SC+import qualified Data.SCargot.Comments as SC+import qualified Data.SCargot.Repr as SC+import qualified Data.SCargot.Repr.WellFormed as SC+import           Data.Semigroup+import qualified Data.Sequence as Seq+import           Data.Text (Text)+import qualified Data.Text as T+import qualified LibBF as BF+import           Numeric.Natural ( Natural )+import qualified Text.Parsec as P+import           Text.Parsec.Text ( Parser )+import           Text.Printf ( printf )+import           Data.Ratio++import           Data.Parameterized.Some ( Some(..))+import qualified What4.BaseTypes as W4++import           Prelude++data Atom =+  AId Text+  -- ^ An identifier.+  | AStr (Some W4.StringInfoRepr) Text+  -- ^ A prefix followed by a string literal+  -- (.e.g, AStr "u" "Hello World" is serialize as `#u"Hello World"`).+  | AInt Integer+  -- ^ Integer (i.e., unbounded) literal.+  | ANat Natural+  -- ^ Natural (i.e., unbounded) literal+  | AReal Rational+  -- ^ Real (i.e., unbounded) literal.+  | AFloat (Some W4.FloatPrecisionRepr) BF.BigFloat+  -- ^ A floating point literal (with precision)+  | ABV Int Integer+  -- ^ Bitvector, width and then value.+  | ABool Bool+  -- ^ Boolean literal.+  deriving (Show, Eq, Ord)++type SExpr = SC.WellFormedSExpr Atom++string :: Some W4.StringInfoRepr -> Text -> SExpr+string strInfo str = SC.A $ AStr strInfo str++string' :: Some W4.StringInfoRepr -> String -> SExpr+string' strInfo str = SC.A $ AStr strInfo (T.pack str)++-- | Lift an unquoted identifier.+ident :: Text -> SExpr+ident = SC.A . AId++ident' :: String -> SExpr+ident' = SC.A . AId . T.pack++-- | Lift an integer.+int :: Integer -> SExpr+int = SC.A . AInt++-- | Lift a natural+nat :: Natural -> SExpr+nat = SC.A . ANat++-- | Lift a real+real :: Rational -> SExpr+real = SC.A . AReal++-- | Lift a float+float :: W4.FloatPrecisionRepr fpp -> BF.BigFloat -> SExpr+float rep bf = SC.A (AFloat (Some rep) bf)++-- | Lift a bitvector.+bitvec :: Natural -> Integer -> SExpr+bitvec w v = SC.A $ ABV (fromEnum w) v++-- | Lift a boolean.+bool :: Bool -> SExpr+bool = SC.A . ABool+++-- * Output of the S-Expression Formula language+++-- | Generates the the S-expression tokens represented by the sexpr+-- argument, preceeded by a list of strings output as comments.+printSExpr :: Seq.Seq String -> SExpr -> T.Text+printSExpr comments sexpr =+  let outputFmt = SC.setIndentAmount 1 $ SC.unconstrainedPrint printAtom+  in formatComment comments <> (SC.encodeOne outputFmt $ SC.fromWellFormed sexpr)+++formatComment :: Seq.Seq String -> T.Text+formatComment c+  | Seq.null c = T.empty+  | otherwise = T.pack $ unlines $ fmap formatLine (F.toList c)+  where+    formatLine l = printf ";; %s" l+++printAtom :: Atom -> T.Text+printAtom a =+  case a of+    AId s -> s+    AStr si s -> (stringInfoToPrefix si)<>"\""<>s<>"\""+    AInt i -> T.pack (show i)+    ANat n -> T.pack $ "#u"++(show n)+    AReal r -> T.pack $ "#r"++(show (numerator r))++"/"++(show (denominator r))+    ABV w val -> formatBV w val+    ABool b -> if b then "#true" else "#false"+    AFloat (Some rep) bf -> formatFloat rep bf++-- | Format a floating point value with no rounding in base 16+formatFloat :: W4.FloatPrecisionRepr fpp -> BF.BigFloat -> T.Text+formatFloat (W4.FloatingPointPrecisionRepr eb sb) bf =+  T.pack (printf "#f#%s#%s#%s" (show eb) (show sb) (BF.bfToString 16 (BF.showFree Nothing) bf))++formatBV :: Int -> Integer -> T.Text+formatBV w val = T.pack (prefix ++ printf fmt val)+  where+    (prefix, fmt)+      | w `rem` 4 == 0 = ("#x", "%0" ++ show (w `div` 4) ++ "x")+      | otherwise = ("#b", "%0" ++ show w ++ "b")+++-- * Input and parse of the S-Expression Formula language++-- | This is only the base-level parsing of atoms.  The full language+-- parsing is handled by the base here and the Parser definitions.++parseId :: Parser Text+parseId = T.pack <$> ((:) <$> first <*> P.many rest)+  where first = P.letter P.<|> P.oneOf "@+-=<>_."+        rest = P.letter P.<|> P.digit P.<|> P.oneOf "+-=<>_."++stringInfoToPrefix :: Some W4.StringInfoRepr -> Text+stringInfoToPrefix (Some W4.Char16Repr) = "#char16"+stringInfoToPrefix (Some W4.Char8Repr) = "#char8"+stringInfoToPrefix (Some W4.UnicodeRepr) = ""+++parseStrInfo :: Parser (Some W4.StringInfoRepr)+parseStrInfo =+  P.try (P.string "#char16" >> return (Some W4.Char16Repr))+  P.<|> P.try (P.string "#char8" >> return (Some W4.Char8Repr))+  P.<|> (return (Some W4.UnicodeRepr))+++parseStr :: Parser (Some W4.StringInfoRepr, Text)+parseStr = do+  prefix <- parseStrInfo+  _ <- P.char '"'+  str <- concat <$> P.many ( do { _ <- P.char '\\'; c <- P.anyChar ; return ['\\',c]} P.<|> P.many1 (P.noneOf ('"':"\\")))+  _ <- P.char '"'+  return $ (prefix, T.pack str)++parseReal :: Parser Rational+parseReal = do+  _ <- P.string "#r"+  n <- (read :: (String -> Integer)) <$> P.many P.digit+  _ <- P.char '/'+  d <- (read :: (String -> Integer)) <$> P.many P.digit+  return $ n % d++parseInt :: Parser Integer+parseInt = do+  (read <$> P.many1 P.digit)+  P.<|> (*(-1)) . read <$> (P.char '-' >> P.many1 P.digit)++++parseNat :: Parser Natural+parseNat = do+  _ <- P.string "#u"+  n <- P.many1 P.digit+  return $ read n++parseBool :: Parser Bool+parseBool = do +  (P.try (P.string "#false" *> return False))+  P.<|> (P.string "#true" *> return True)+  +parseBV :: Parser (Int, Integer)+parseBV = P.char '#' >> ((P.char 'b' >> parseBin) P.<|> (P.char 'x' >> parseHex))+  where parseBin = P.oneOf "10" >>= \d -> parseBin' (1, if d == '1' then 1 else 0)++        parseBin' :: (Int, Integer) -> Parser (Int, Integer)+        parseBin' (bits, x) = do+          P.optionMaybe (P.oneOf "10") >>= \case+            Just d -> parseBin' (bits + 1, x * 2 + (if d == '1' then 1 else 0))+            Nothing -> return (bits, x)++        parseHex = (\s -> (length s * 4, read ("0x" ++ s))) <$> P.many1 P.hexDigit++parseFloat :: Parser (Some W4.FloatPrecisionRepr, BF.BigFloat)+parseFloat = do+  _ <- P.string "#f#"+  -- We printed the nat reprs out in decimal+  eb :: Natural+     <- read <$> P.many1 P.digit+  _ <- P.char '#'+  sb :: Natural+     <- read <$> P.many1 P.digit+  _ <- P.char '#'++  -- The float value itself is printed out as a hex literal+  hexDigits <- P.many1 P.hexDigit++  Some ebRepr <- return (PN.mkNatRepr eb)+  Some sbRepr <- return (PN.mkNatRepr sb)+  case (PN.testLeq (PN.knownNat @2) ebRepr, PN.testLeq (PN.knownNat @2) sbRepr) of+    (Just PN.LeqProof, Just PN.LeqProof) -> do+      let rep = W4.FloatingPointPrecisionRepr ebRepr sbRepr++      -- We know our format: it is determined by the exponent bits (eb) and the+      -- significand bits (sb) parsed above+      let fmt = BF.precBits (fromIntegral sb) <> BF.expBits (fromIntegral eb)+      let (bf, status) = BF.bfFromString 16 fmt hexDigits+      case status of+        BF.Ok -> return (Some rep, bf)+        _ -> P.unexpected ("Error parsing hex float: 0x" ++ hexDigits)+    _ -> P.unexpected ("Invalid exponent or significand size: " ++ show (eb, sb))+++parseAtom :: Parser Atom+parseAtom+  =     P.try (ANat  <$> parseNat)+  P.<|> P.try (uncurry AFloat <$> parseFloat)+  P.<|> P.try (AReal <$> parseReal)+  P.<|> P.try (AInt  <$> parseInt)+  P.<|> P.try (AId   <$> parseId)+  P.<|> P.try (uncurry AStr  <$> parseStr)+  P.<|> P.try (ABool <$> parseBool)+  P.<|> P.try (uncurry ABV <$> parseBV)++parseSExpr :: T.Text -> Either String SExpr+parseSExpr = SC.decodeOne $ SC.asWellFormed $ SC.withLispComments (SC.mkParser parseAtom)

@@ -53,6 +53,17 @@   , cvc4Options   , cvc4Features +    -- * CVC5+  , CVC5(..)+  , cvc5Adapter+  , cvc5Path+  , cvc5Timeout+  , runCVC5InOverride+  , writeCVC5SMT2File+  , withCVC5+  , cvc5Options+  , cvc5Features+     -- * DReal   , DReal(..)   , DRealBindings@@ -98,6 +109,7 @@ import           What4.Solver.Adapter import           What4.Solver.Boolector import           What4.Solver.CVC4+import           What4.Solver.CVC5 import           What4.Solver.DReal import           What4.Solver.ExternalABC import           What4.Solver.STP

@@ -39,6 +39,7 @@ import           What4.ProblemFeatures import           What4.Protocol.Online import qualified What4.Protocol.SMTLib2 as SMT2+import qualified What4.Protocol.SMTLib2.Syntax as Syntax import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt ) import           What4.SatResult import           What4.Solver.Adapter@@ -128,7 +129,7 @@   defaultSolverArgs _ _ = return ["--smt2", "--incremental", "--output-format=smt2", "-e=0"]   defaultFeatures _ = boolectorFeatures   setDefaultLogicAndOptions writer = do-    SMT2.setLogic writer SMT2.allSupported+    SMT2.setLogic writer Syntax.allLogic     SMT2.setProduceModels writer True  setInteractiveLogicAndOptions ::@@ -141,7 +142,7 @@     SMT2.setOption writer "global-declarations" "true"     when (SMT2.supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do       SMT2.setOption writer "produce-unsat-cores" "true"-    SMT2.setLogic writer SMT2.allSupported+    SMT2.setLogic writer Syntax.allLogic  instance OnlineSolver (SMT2.Writer Boolector) where   startSolverProcess feat mbIOh sym = do

@@ -78,7 +78,7 @@ cvc4TimeoutOLD :: ConfigOption BaseIntegerType cvc4TimeoutOLD = configOption knownRepr "cvc4_timeout" --- | Control strict parsing for Boolector solver responses (defaults+-- | Control strict parsing for CVC4 solver responses (defaults -- to solver.strict-parsing option setting). cvc4StrictParsing :: ConfigOption BaseBoolType cvc4StrictParsing = configOption knownRepr "solver.cvc4.strict_parsing"@@ -164,7 +164,7 @@                 (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.setLogic c Syntax.allLogic   SMT2.setProduceModels c True   forM_ ps $ SMT2.assume c   SMT2.writeCheckSat c@@ -196,7 +196,7 @@    setDefaultLogicAndOptions writer = do     -- Tell CVC4 to use all supported logics.-    SMT2.setLogic writer SMT2.allSupported+    SMT2.setLogic writer Syntax.allLogic     -- Tell CVC4 to produce models     SMT2.setProduceModels writer True @@ -237,7 +237,7 @@     when (supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do       SMT2.setOption writer "produce-unsat-cores" "true"     -- Tell CVC4 to use all supported logics.-    SMT2.setLogic writer SMT2.allSupported+    SMT2.setLogic writer Syntax.allLogic  instance OnlineSolver (SMT2.Writer CVC4) where   startSolverProcess feat mbIOh sym = do

@@ -0,0 +1,380 @@+------------------------------------------------------------------------+-- |+-- Module      : What4.Solver.CVC5+-- Description : Solver adapter code for cvc5+-- Copyright   : (c) Galois, Inc 2022+-- License     : BSD3+-- Maintainer  : Rob Dockins <rdockins@galois.com>+-- Stability   : provisional+--+-- CVC5-specific tweaks to the basic SMTLib2 solver interface.+------------------------------------------------------------------------+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module What4.Solver.CVC5+  ( CVC5(..)+  , cvc5Features+  , cvc5Adapter+  , cvc5Path+  , cvc5Timeout+  , cvc5Options+  , runCVC5InOverride+  , withCVC5+  , writeCVC5SMT2File+  , writeMultiAsmpCVC5SMT2File+  , runCVC5SyGuS+  , withCVC5_SyGuS+  , writeCVC5SyFile+  ) where++import           Control.Monad (forM_, when)+import           Data.Bits+import           Data.String+import           System.IO+import qualified System.IO.Streams as Streams++import           Data.Parameterized.Map (MapF)+import           Data.Parameterized.Some+import           What4.BaseTypes+import           What4.Concrete+import           What4.Config+import           What4.Expr.Builder+import           What4.Expr.GroundEval+import           What4.Interface+import           What4.ProblemFeatures+import           What4.Protocol.Online+import qualified What4.Protocol.SMTLib2 as SMT2+import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )+import qualified What4.Protocol.SMTLib2.Response as RSP+import qualified What4.Protocol.SMTLib2.Syntax as Syntax+import           What4.Protocol.SMTWriter+import           What4.SatResult+import           What4.Solver.Adapter+import           What4.Utils.Process+++intWithRangeOpt :: ConfigOption BaseIntegerType -> Integer -> Integer -> ConfigDesc+intWithRangeOpt nm lo hi = mkOpt nm sty Nothing Nothing+  where sty = integerWithRangeOptSty (Inclusive lo) (Inclusive hi)++data CVC5 = CVC5 deriving Show++-- | Path to cvc5+cvc5Path :: ConfigOption (BaseStringType Unicode)+cvc5Path = configOption knownRepr "solver.cvc5.path"++cvc5RandomSeed :: ConfigOption BaseIntegerType+cvc5RandomSeed = configOption knownRepr "solver.cvc5.random-seed"++-- | Per-check timeout, in milliseconds (zero is none)+cvc5Timeout :: ConfigOption BaseIntegerType+cvc5Timeout = configOption knownRepr "solver.cvc5.timeout"++-- | Control strict parsing for cvc5 solver responses (defaults+-- to solver.strict-parsing option setting).+cvc5StrictParsing :: ConfigOption BaseBoolType+cvc5StrictParsing = configOption knownRepr "solver.cvc5.strict_parsing"++cvc5Options :: [ConfigDesc]+cvc5Options =+  let pathOpt co = mkOpt co+                   executablePathOptSty+                   (Just "Path to CVC5 executable")+                   (Just (ConcreteString "cvc5"))+      p1 = pathOpt cvc5Path+      r1 = intWithRangeOpt cvc5RandomSeed (negate (2^(30::Int)-1)) (2^(30::Int)-1)+      tmOpt co = mkOpt co+                 integerOptSty+                 (Just "Per-check timeout in milliseconds (zero is none)")+                 (Just (ConcreteInteger 0))+      t1 = tmOpt cvc5Timeout+  in [ p1, r1, t1+     , copyOpt (const $ configOptionText cvc5StrictParsing) strictSMTParseOpt+     ] <> SMT2.smtlib2Options++cvc5Adapter :: SolverAdapter st+cvc5Adapter =+  SolverAdapter+  { solver_adapter_name = "cvc5"+  , solver_adapter_config_options = cvc5Options+  , solver_adapter_check_sat = runCVC5InOverride+  , solver_adapter_write_smt2 = writeCVC5SMT2File+  }++indexType :: [SMT2.Sort] -> SMT2.Sort+indexType [i] = i+indexType il = SMT2.smtlib2StructSort @CVC5 il++indexCtor :: [SMT2.Term] -> SMT2.Term+indexCtor [i] = i+indexCtor il = SMT2.smtlib2StructCtor @CVC5 il++instance SMT2.SMTLib2Tweaks CVC5 where+  smtlib2tweaks = CVC5++  smtlib2arrayType il r = SMT2.arraySort (indexType il) r++  smtlib2arrayConstant = Just $ \idx rtp v ->+    SMT2.arrayConst (indexType idx) rtp v+  smtlib2arraySelect a i = SMT2.arraySelect a (indexCtor i)+  smtlib2arrayUpdate a i = SMT2.arrayStore a (indexCtor i)++  smtlib2declareStructCmd _ = Nothing+  smtlib2StructSort []  = Syntax.varSort "Tuple"+  smtlib2StructSort tps = Syntax.Sort $ "(Tuple" <> foldMap f tps <> ")"+    where f x = " " <> Syntax.unSort x++  smtlib2StructCtor args = Syntax.term_app "mkTuple" args+  smtlib2StructProj _n i x = Syntax.term_app (Syntax.builder_list ["_", "tupSel", fromString (show i)]) [ x ]++cvc5Features :: ProblemFeatures+cvc5Features = useComputableReals+           .|. useIntegerArithmetic+           .|. useSymbolicArrays+           .|. useStrings+           .|. useStructs+           .|. useFloatingPoint+           .|. useUnsatCores+           .|. useUnsatAssumptions+           .|. useUninterpFunctions+           .|. useDefinedFunctions+           .|. useBitvectors+           .|. useQuantifiers+           .|. useProduceAbducts++writeMultiAsmpCVC5SMT2File+   :: ExprBuilder t st fs+   -> Handle+   -> [BoolExpr t]+   -> IO ()+writeMultiAsmpCVC5SMT2File sym h ps = do+  bindings <- getSymbolVarBimap sym+  out_str  <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h+  in_str <- Streams.nullInput+  let cfg = getConfiguration sym+  strictness <- maybe Strict+                (\c -> if fromConcreteBool c then Strict else Lenient) <$>+                (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)+  c <- SMT2.newWriter CVC5 out_str in_str nullAcknowledgementAction strictness "CVC5"+         True cvc5Features True bindings+  SMT2.setLogic c Syntax.allLogic+  SMT2.setProduceModels c True+  forM_ ps $ SMT2.assume c+  SMT2.writeCheckSat c+  SMT2.writeExit c++writeCVC5SMT2File+   :: ExprBuilder t st fs+   -> Handle+   -> [BoolExpr t]+   -> IO ()+writeCVC5SMT2File sym h ps = writeMultiAsmpCVC5SMT2File sym h ps++instance SMT2.SMTLib2GenericSolver CVC5 where+  defaultSolverPath _ = findSolverPath cvc5Path . getConfiguration++  defaultSolverArgs _ sym = do+    let cfg = getConfiguration sym+    timeout <- getOption =<< getOptionSetting cvc5Timeout cfg+    let extraOpts = case timeout of+                      Just (ConcreteInteger n) | n > 0 -> ["--tlimit-per=" ++ show n]+                      _ -> []+    return $ ["--lang", "smt2", "--incremental", "--strings-exp", "--fp-exp"] ++ extraOpts++  getErrorBehavior _ = SMT2.queryErrorBehavior++  defaultFeatures _ = cvc5Features++  supportsResetAssertions _ = True++  setDefaultLogicAndOptions writer = do+    -- Tell cvc5 to use all supported logics.+    SMT2.setLogic writer Syntax.allLogic+    -- Tell cvc5 to produce models+    SMT2.setProduceModels writer True+    -- Tell cvc5 to produce abducts+    SMT2.setOption writer "produce-abducts" "true"++runCVC5InOverride+  :: ExprBuilder t st fs+  -> LogData+  -> [BoolExpr t]+  -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a)+  -> IO a+runCVC5InOverride = SMT2.runSolverInOverride CVC5 nullAcknowledgementAction+                    (SMT2.defaultFeatures CVC5) (Just cvc5StrictParsing)++-- | Run cvc5 in a session. cvc5 will be configured to produce models, but+-- otherwise left with the default configuration.+withCVC5+  :: ExprBuilder t st fs+  -> FilePath+    -- ^ Path to cvc5 executable+  -> LogData+  -> (SMT2.Session t CVC5 -> IO a)+    -- ^ Action to run+  -> IO a+withCVC5 = SMT2.withSolver CVC5 nullAcknowledgementAction+           (SMT2.defaultFeatures CVC5) (Just cvc5StrictParsing)++setInteractiveLogicAndOptions ::+  SMT2.SMTLib2Tweaks a =>+  WriterConn t (SMT2.Writer a) ->+  IO ()+setInteractiveLogicAndOptions writer = do+    -- Tell cvc5 to acknowledge successful commands+    SMT2.setOption writer "print-success"  "true"+    -- Tell cvc5 to produce models+    SMT2.setOption writer "produce-models" "true"+    -- Tell cvc5 to make declarations global, so they are not removed by 'pop' commands+    SMT2.setOption writer "global-declarations" "true"+    -- Tell cvc5 to compute UNSAT cores, if that feature is enabled+    when (supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do+      SMT2.setOption writer "produce-unsat-cores" "true"+    -- Tell cvc5 to produce abducts, if that feature is enabled+    when (supportedFeatures writer `hasProblemFeature` useProduceAbducts) $ do+      SMT2.setOption writer "produce-abducts" "true"+    -- Tell cvc5 to use all supported logics.+    SMT2.setLogic writer Syntax.allLogic++instance OnlineSolver (SMT2.Writer CVC5) where+  startSolverProcess feat mbIOh sym = do+    timeout <- SolverGoalTimeout <$>+               (getOpt =<< getOptionSetting cvc5Timeout (getConfiguration sym))+    SMT2.startSolver CVC5 SMT2.smtAckResult setInteractiveLogicAndOptions+          timeout feat (Just cvc5StrictParsing) mbIOh sym++  shutdownSolverProcess = SMT2.shutdownSolver CVC5+++-- | `CVC5_SyGuS` implements a `SMT2.SMTLib2GenericSolver` instance that is+-- different from `CVC5` in that it provides SyGuS specific implementations for+-- `defaultSolverArgs` and `setDefaultLogicAndOptions`.+data CVC5_SyGuS = CVC5_SyGuS deriving Show++instance SMT2.SMTLib2Tweaks CVC5_SyGuS where+  smtlib2tweaks = CVC5_SyGuS++  smtlib2arrayType = SMT2.smtlib2arrayType @CVC5++  smtlib2arrayConstant = SMT2.smtlib2arrayConstant @CVC5+  smtlib2arraySelect = SMT2.smtlib2arraySelect @CVC5+  smtlib2arrayUpdate = SMT2.smtlib2arrayUpdate @CVC5++  smtlib2declareStructCmd = SMT2.smtlib2declareStructCmd @CVC5+  smtlib2StructSort = SMT2.smtlib2StructSort @CVC5+  smtlib2StructCtor = SMT2.smtlib2StructCtor @CVC5+  smtlib2StructProj = SMT2.smtlib2StructProj @CVC5++instance SMT2.SMTLib2GenericSolver CVC5_SyGuS where+  defaultSolverPath _ = SMT2.defaultSolverPath CVC5++  defaultSolverArgs _ sym = do+    let cfg = getConfiguration sym+    timeout <- getOption =<< getOptionSetting cvc5Timeout cfg+    let extraOpts = case timeout of+                      Just (ConcreteInteger n) | n > 0 -> ["--tlimit-per=" ++ show n]+                      _ -> []+    return $ ["--sygus", "--lang", "sygus2", "--strings-exp", "--fp-exp"] ++ extraOpts++  getErrorBehavior _ = SMT2.queryErrorBehavior++  defaultFeatures _ = SMT2.defaultFeatures CVC5++  supportsResetAssertions _ = SMT2.supportsResetAssertions CVC5++  setDefaultLogicAndOptions writer = do+    -- Tell cvc5 to use all supported logics.+    SMT2.setLogic writer Syntax.allLogic++-- | Find a solution to a Syntax-Guided Synthesis (SyGuS) problem.+--+-- For more information, see the [SyGuS standard](https://sygus.org/).+runCVC5SyGuS ::+  sym ~ ExprBuilder t st fs =>+  sym ->+  LogData ->+  [SomeSymFn sym] ->+  [BoolExpr t] ->+  IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())+runCVC5SyGuS sym log_data synth_fns constraints = do+  logSolverEvent sym+    (SolverStartSATQuery $ SolverStartSATQueryRec+      { satQuerySolverName = show CVC5_SyGuS+      , satQueryReason = logReason log_data+      })++  path <- SMT2.defaultSolverPath CVC5_SyGuS sym+  withCVC5_SyGuS sym path (log_data { logVerbosity = 2 }) $ \session -> do+    writeSyGuSProblem sym (SMT2.sessionWriter session) synth_fns constraints+    result <- RSP.getLimitedSolverResponse "check-synth"+      (\case+        RSP.AckSuccessSExp sexp -> Just $ Sat sexp+        RSP.AckInfeasible -> Just $ Unsat ()+        RSP.AckFail -> Just Unknown+        _ -> Nothing)+      (SMT2.sessionWriter session)+      Syntax.checkSynth++    logSolverEvent sym+      (SolverEndSATQuery $ SolverEndSATQueryRec+        { satQueryResult = forgetModelAndCore result+        , satQueryError = Nothing+        })++    traverseSatResult+      (\sexp -> SMT2.parseFnModel sym (SMT2.sessionWriter session) synth_fns sexp)+      return+      result++-- | Run CVC5 SyGuS in a session, with the default configuration.+withCVC5_SyGuS ::+  ExprBuilder t st fs ->+  FilePath ->+  LogData ->+  (SMT2.Session t CVC5_SyGuS -> IO a) ->+  IO a+withCVC5_SyGuS =+  SMT2.withSolver+    CVC5_SyGuS+    nullAcknowledgementAction+    (SMT2.defaultFeatures CVC5_SyGuS)+    (Just cvc5StrictParsing)++writeCVC5SyFile ::+  sym ~ ExprBuilder t st fs =>+  sym ->+  Handle ->+  [SomeSymFn sym] ->+  [BoolExpr t] ->+  IO ()+writeCVC5SyFile sym h synth_fns constraints = do+  writer <- SMT2.defaultFileWriter+    CVC5_SyGuS+    (show CVC5_SyGuS)+    (SMT2.defaultFeatures CVC5_SyGuS)+    (Just cvc5StrictParsing)+    sym+    h+  SMT2.setDefaultLogicAndOptions writer+  writeSyGuSProblem sym writer synth_fns constraints+  SMT2.writeExit writer++writeSyGuSProblem ::+  sym ~ ExprBuilder t st fs =>+  sym ->+  WriterConn t (SMT2.Writer CVC5_SyGuS) ->+  [SomeSymFn sym] ->+  [BoolExpr t] ->+  IO ()+writeSyGuSProblem sym writer synth_fns constraints = do+  mapM_ (\(SomeSymFn fn) -> addSynthFun writer fn) synth_fns+  mapM_ (viewSome $ addDeclareVar writer) $ foldMap (exprUninterpConstants sym) constraints+  mapM_ (addConstraint writer) constraints+  SMT2.writeCheckSynth writer

@@ -331,6 +331,9 @@    fromText t = T (Builder.fromText t) +unsupportedFeature :: String -> a+unsupportedFeature s = error ("Yices does not support " <> s)+ floatFail :: HasCallStack => a floatFail = error "Yices does not support IEEE-754 floating-point numbers" @@ -492,6 +495,8 @@    pushCommand _   = const $ safeCmd "(push)"   popCommand _    = const $ safeCmd "(pop)"+  push2Command _   = unsupportedFeature "(push 2)"+  pop2Command _    = unsupportedFeature "(pop 2)"   resetCommand _  = const $ safeCmd "(reset)"   checkCommands _  =     [ setTimeoutCommand, const $ safeCmd "(check)" ]@@ -502,6 +507,9 @@    getUnsatAssumptionsCommand _ = const $ safeCmd "(show-unsat-assumptions)"   getUnsatCoreCommand _ = const $ safeCmd "(show-unsat-core)"+  getAbductCommand _ _ _ = unsupportedFeature "abduction"+  getAbductNextCommand _ = unsupportedFeature "abduction"+   setOptCommand _ x o = setParamCommand x (Builder.fromText o)    assertCommand _ (T nm) = const $ unsafeCmd $ app "assert" [nm]@@ -520,6 +528,10 @@                  , renderTerm (yicesLambda args t)                  ] +  synthFunCommand _ _ _ _ = unsupportedFeature "SyGuS"+  declareVarCommand _ _ _ = unsupportedFeature "SyGuS"+  constraintCommand _ _ = unsupportedFeature "SyGuS"+   resetDeclaredStructs conn = resetUnitType conn    structProj _n i s = term_app "select" [s, fromIntegral (Ctx.indexVal i + 1)]@@ -589,6 +601,9 @@                  unlines [ "Could not parse unsat core result."                          , "*** Exception: " ++ displayException e                          ]+  smtAbductResult _ _ _ = unsupportedFeature "abduction"++  smtAbductNextResult _ = unsupportedFeature "abduction"   -- | Exceptions that can occur when reading responses from Yices

@@ -10,10 +10,11 @@ -- Z3-specific tweaks to the basic SMTLib2 solver interface. ------------------------------------------------------------------------ {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeApplications #-}-+{-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-} module What4.Solver.Z3   ( Z3(..)@@ -27,15 +28,21 @@   , runZ3InOverride   , withZ3   , writeZ3SMT2File+  , runZ3Horn+  , writeZ3HornSMT2File   ) where  import           Control.Monad ( when )+import qualified Data.Bimap as Bimap import           Data.Bits+import           Data.Foldable import           Data.String import           Data.Text (Text) import qualified Data.Text as T import           System.IO +import           Data.Parameterized.Map (MapF)+import           Data.Parameterized.Some import           What4.BaseTypes import           What4.Concrete import           What4.Config@@ -46,7 +53,8 @@ import           What4.Protocol.Online import qualified What4.Protocol.SMTLib2 as SMT2 import           What4.Protocol.SMTLib2.Response ( strictSMTParseOpt )-import qualified What4.Protocol.SMTLib2.Syntax as SMT2Syntax+import qualified What4.Protocol.SMTLib2.Response as RSP+import qualified What4.Protocol.SMTLib2.Syntax as Syntax import           What4.Protocol.SMTWriter import           What4.SatResult import           What4.Solver.Adapter@@ -139,7 +147,7 @@           fields = field_def <$> [1..n]           decl = app tp [app ctor fields]           decls = "(" <> decl <> ")"-       in SMT2Syntax.Cmd $ app "declare-datatypes" [ params, decls ]+       in Syntax.Cmd $ app "declare-datatypes" [ params, decls ]  z3Features :: ProblemFeatures z3Features = useNonlinearArithmetic@@ -235,3 +243,87 @@       timeout feat (Just z3StrictParsing) mbIOh sym    shutdownSolverProcess = SMT2.shutdownSolver Z3++-- | Check the satisfiability of a set of constrained Horn clauses (CHCs).+--+-- CHCs are represented as pure SMT-LIB2 implications. For more information, see+-- the [Z3 guide](https://microsoft.github.io/z3guide/docs/fixedpoints/intro/).+runZ3Horn ::+  sym ~ ExprBuilder t st fs =>+  sym ->+  LogData ->+  [SomeSymFn sym] ->+  [BoolExpr t] ->+  IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())+runZ3Horn sym log_data inv_fns horn_clauses = do+  logSolverEvent sym+    (SolverStartSATQuery $ SolverStartSATQueryRec+      { satQuerySolverName = show Z3+      , satQueryReason = logReason log_data+      })++  path <- SMT2.defaultSolverPath Z3 sym+  withZ3 sym path (log_data { logVerbosity = 2 }) $ \session -> do+    writeHornProblem sym (SMT2.sessionWriter session) inv_fns horn_clauses+    result <- RSP.getLimitedSolverResponse "check-sat"+      (\case+        RSP.AckSat -> Just $ Sat ()+        RSP.AckUnsat -> Just $ Unsat ()+        RSP.AckUnknown -> Just Unknown+        _ -> Nothing)+      (SMT2.sessionWriter session)+      Syntax.checkSat++    logSolverEvent sym+      (SolverEndSATQuery $ SolverEndSATQueryRec+        { satQueryResult = result+        , satQueryError = Nothing+        })++    traverseSatResult+      (\() -> do+        sexp <- RSP.getLimitedSolverResponse "get-value"+          (\case+            RSP.AckSuccessSExp sexp -> Just sexp+            _ -> Nothing)+          (SMT2.sessionWriter session)+          (Syntax.getValue [])+        SMT2.parseFnValues sym (SMT2.sessionWriter session) inv_fns sexp)+      return+      result++writeZ3HornSMT2File ::+  sym ~ ExprBuilder t st fs =>+  sym ->+  Handle ->+  [SomeSymFn sym] ->+  [BoolExpr t] ->+  IO ()+writeZ3HornSMT2File sym h inv_fns horn_clauses = do+  writer <- SMT2.defaultFileWriter+    Z3+    (show Z3)+    (SMT2.defaultFeatures Z3)+    (Just z3StrictParsing)+    sym+    h+  SMT2.setDefaultLogicAndOptions writer+  writeHornProblem sym writer inv_fns horn_clauses+  SMT2.writeExit writer++writeHornProblem ::+  sym ~ ExprBuilder t st fs =>+  sym ->+  WriterConn t (SMT2.Writer Z3) ->+  [SomeSymFn sym] ->+  [BoolExpr t] ->+  IO ()+writeHornProblem sym writer inv_fns horn_clauses = do+  SMT2.setLogic writer Syntax.hornLogic+  implications <- mapM+    (\clause -> foldrM (viewSome $ forallPred sym) clause $ exprUninterpConstants sym clause)+    horn_clauses+  mapM_ (SMT2.assume writer) implications+  SMT2.writeCheckSat writer+  fn_name_bimap <- cacheLookupFnNameBimap writer $ map (\(SomeSymFn fn) -> SomeExprSymFn fn) inv_fns+  SMT2.writeGetValue writer $ map fromText $ Bimap.elems fn_name_bimap

@@ -26,6 +26,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-}  module What4.Utils.AbstractDomains

@@ -8,6 +8,7 @@ restricting index types in MATLAB arrays. -} {-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-} module What4.Utils.OnlyIntRepr   ( OnlyIntRepr(..)   , toBaseTypeRepr

@@ -0,0 +1,127 @@+{-# LANGUAGE NondecreasingIndentation #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeOperators #-}+module What4.Utils.Serialize+    (+      withRounding+    , makeSymbol+    , asyncLinked+    , withAsyncLinked+    ) where++import qualified Control.Exception as E+import           Text.Printf ( printf )+import qualified Data.BitVector.Sized as BV+import           What4.BaseTypes+import qualified What4.Interface as S+import           What4.Symbol ( SolverSymbol, userSymbol )+++import qualified UnliftIO as U++----------------------------------------------------------------+-- * Async++-- | Fork an async action that is linked to the parent thread, but can+-- be safely 'U.cancel'd without also killing the parent thread.+--+-- Note that if your async doesn't return unit, then you probably want+-- to 'U.wait' for it instead, which eliminates the need for linking+-- it. Also, if you plan to cancel the async near where you fork it,+-- then 'withAsyncLinked' is a better choice than using this function+-- and subsequently canceling, since it ensures cancellation.+--+-- See https://github.com/simonmar/async/issues/25 for a perhaps more+-- robust, but also harder to use version of this. The linked version+-- is harder to use because it requires a special version of @cancel@.+asyncLinked :: (U.MonadUnliftIO m) => m () -> m (U.Async ())+asyncLinked action = do+  -- We use 'U.mask' to avoid a race condition between starting the+  -- async and running @action@. Without 'U.mask' here, an async+  -- exception (e.g. via 'U.cancel') could arrive after+  -- @handleUnliftIO@ starts to run but before @action@ starts.+  U.mask $ \restore -> do+  a <- U.async $ handleUnliftIO threadKilledHandler (restore action)+  restore $ do+  U.link a+  return a++-- | Handle asynchronous 'E.ThreadKilled' exceptions without killing the parent+-- thread. All other forms of asynchronous exceptions are rethrown.+threadKilledHandler :: Monad m => E.AsyncException -> m ()+threadKilledHandler E.ThreadKilled = return ()+threadKilledHandler e              = E.throw e++-- | A version of 'U.withAsync' that safely links the child. See+-- 'asyncLinked'.+withAsyncLinked :: (U.MonadUnliftIO m) => m () -> (U.Async () -> m a) -> m a+withAsyncLinked child parent = do+  U.mask $ \restore -> do+  U.withAsync (handleUnliftIO threadKilledHandler $ restore child) $ \a -> restore $ do+  U.link a+  parent a++-- A 'U.MonadUnliftIO' version of 'Control.Exception.handle'.+--+-- The 'U.handle' doesn't catch async exceptions, because the+-- @unliftio@ library uses the @safe-execeptions@ library, not+-- @base@, for it exception handling primitives. This is very+-- confusing if you're not expecting it!+handleUnliftIO :: (U.MonadUnliftIO m, U.Exception e)+               => (e -> m a) -> m a -> m a+handleUnliftIO h a = U.withUnliftIO $ \u ->+  E.handle (U.unliftIO u . h) (U.unliftIO u a)++-- | Try converting any 'String' into a 'SolverSymbol'. If it is an invalid+-- symbol, then error.+makeSymbol :: String -> SolverSymbol+makeSymbol name = case userSymbol sanitizedName of+                    Right symbol -> symbol+                    Left _ -> error $ printf "tried to create symbol with bad name: %s (%s)"+                                             name sanitizedName+  where+    -- We use a custom name sanitizer here because downstream clients may depend+    -- on the format of the name. It would be nice to use 'safeSymbol' here, but+    -- it mangles names with z-encoding in a way that might be unusable+    -- downstream.+    sanitizedName = map (\c -> case c of ' ' -> '_'; '.' -> '_'; _ -> c) name++withRounding+  :: forall sym tp+   . S.IsExprBuilder sym+  => sym+  -> S.SymBV sym 2+  -> (S.RoundingMode -> IO (S.SymExpr sym tp))+  -> IO (S.SymExpr sym tp)+withRounding sym r action = do+  cRNE <- roundingCond S.RNE+  cRTZ <- roundingCond S.RTZ+  cRTP <- roundingCond S.RTP+  S.iteM S.baseTypeIte sym cRNE+    (action S.RNE) $+    S.iteM S.baseTypeIte sym cRTZ+      (action S.RTZ) $+      S.iteM S.baseTypeIte sym cRTP (action S.RTP) (action S.RTN)+ where+  roundingCond :: S.RoundingMode -> IO (S.Pred sym)+  roundingCond rm =+    S.bvEq sym r =<< S.bvLit sym knownNat (BV.mkBV knownNat (roundingModeToBits rm))++roundingModeToBits :: S.RoundingMode -> Integer+roundingModeToBits = \case+  S.RNE -> 0+  S.RTZ -> 1+  S.RTP -> 2+  S.RTN -> 3+  S.RNA -> error $ "unsupported rounding mode: " ++ show S.RNA

@@ -0,0 +1,155 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeApplications #-}++module Main where++import           Test.Tasty+import           Test.Tasty.HUnit++import           Data.Foldable (forM_)+import qualified Data.Text as Text+import           Data.Parameterized.Nonce (newIONonceGenerator)+import           Data.Parameterized.Some (Some(..))++import           System.IO (FilePath, IOMode(..), openFile, hClose)+import           System.IO.Temp (withSystemTempFile)+import           What4.Config (extendConfig)+import           What4.Expr+                   ( ExprBuilder,  FloatModeRepr(..), newExprBuilder+                   , BoolExpr, IntegerExpr, GroundValue, groundEval+                   , EmptyExprBuilderState(..))+import           What4.Interface+                   ( BaseTypeRepr(..), getConfiguration+                   , freshConstant, safeSymbol, notPred+                   , impliesPred, intLit, intAdd, intLe )+import           What4.Solver+import           What4.Symbol (SolverSymbol(..))+import           What4.Protocol.SMTLib2 as SMT2+                   (assume, sessionWriter, runCheckSat, runGetAbducts, Writer)+import           What4.Protocol.SMTWriter+                   (mkSMTTerm)+import           What4.Protocol.Online++cvc5executable :: FilePath+cvc5executable = "cvc5"++-- Call the online getAbduct tactic+testGetAbductOnline ::+  ExprBuilder t st fs ->+  [BoolExpr t] ->+  BoolExpr t ->+  Int ->+  IO [String]+testGetAbductOnline sym hs g n = do+  -- Print SMT file in /tmp/+  withSystemTempFile "what4abdonline" $ \fname mirroredOutput -> do+    proc <- startSolverProcess @(SMT2.Writer CVC5) cvc5Features (Just mirroredOutput) sym+    let conn = solverConn proc+    inNewFrame proc $ do+      mapM_ (\x -> assume conn x) hs+      getAbducts proc n (Text.pack "abd") g++-- Call the offline getAbduct tactic+testGetAbductOffline ::+  ExprBuilder t st fs ->+  BoolExpr t ->+  Int ->+  IO [String]+testGetAbductOffline sym f n = do+  -- Print SMT file in /tmp/+  withSystemTempFile "what4abdoffline" $ \fname mirroredOutput -> do+    let logData = LogData { logCallbackVerbose = \_ _ -> return ()+                          , logVerbosity = 2+                          , logReason = "defaultReason"+                          , logHandle = Just mirroredOutput }+    withCVC5 sym cvc5executable logData $ \session -> do+      f_term <- mkSMTTerm (sessionWriter session) f+      runGetAbducts session n (Text.pack "abd") f_term++-- Prove f using an SMT solver, by checking if ~f is unsatisfiable+prove ::+  ExprBuilder t st fs ->+  BoolExpr t ->+  [(String, IntegerExpr t)] ->+  IO (SatResult () ())+prove sym f es = do+  -- Print SMT file in /tmp/+  withSystemTempFile "what4prove" $ \fname mirroredOutput -> do+    proc <- startSolverProcess @(SMT2.Writer CVC5) cvc5Features (Just mirroredOutput) sym+    let logData = LogData { logCallbackVerbose = \_ _ -> return ()+                           , logVerbosity = 2+                           , logReason = "defaultReason"+                           , logHandle = Just mirroredOutput }+    +    -- To prove f, we check whether not f is unsat+    notf <- notPred sym f+    withCVC5 sym cvc5executable logData $ \session -> do+      checkSatisfiable proc "test" notf++-- Tests++testAbdOnline :: ExprBuilder t st fs -> +  [BoolExpr t] -> +  BoolExpr t -> +  TestTree+testAbdOnline sym hs g = testCase "getting 3 abducts using cvc5 online" $ do+  -- Ask for 3 abducts for f+  res <- testGetAbductOnline sym hs g 3+  (length res == 3) @? "3 online abducts"++testAbdOffline :: ExprBuilder t st fs -> +  BoolExpr t -> +  [(String, IntegerExpr t)] -> +  TestTree+testAbdOffline sym f es = testCase "getting 3 abducts using cvc5 offline" $ do+  -- Ask for 3 abducts for f+  res <- testGetAbductOffline sym f 3+  (length res == 3) @? "3 offline abducts"++testSatAbd :: ExprBuilder t st fs -> +  BoolExpr t -> +  [(String, IntegerExpr t)] -> +  TestTree+testSatAbd sym f es = testCase "testing SAT query for abduction" $ do+  -- Prove f (is ~f unsatisfiable?). We expect ~f to be satisfiable+  res <- prove sym f es+  isSat res @? "sat"+++main :: IO ()+main = do+  Some ng <- newIONonceGenerator+  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng++  -- This line is necessary for working with cvc5.+  extendConfig cvc5Options (getConfiguration sym)++  -- Build this formula: ~(y >= 0 => (x + y + z) >= 0)+  +  -- First, declare fresh constants for each of the three variables x, y, z.+  x <- freshConstant sym (safeSymbol "x") BaseIntegerRepr+  y <- freshConstant sym (safeSymbol "y") BaseIntegerRepr+  z <- freshConstant sym (safeSymbol "z") BaseIntegerRepr++  -- Next, build up the clause+  zero <- intLit sym 0                    -- 0+  pxyz <- intAdd sym x =<< intAdd sym y z -- x + y + z+  ygte0 <- intLe sym zero y               -- 0 <= y+  xyzgte0 <- intLe sym zero pxyz          -- 0 <= (x + y + z) +  f <- impliesPred sym ygte0 xyzgte0      -- (0 <= y) -> (0 <= (x + y + z))++  defaultMain $ testGroup "Tests" $+    [ -- test passes if f is disproved (~f is sat)+      testSatAbd sym f [ ("x", x)+                       , ("y", y)+                       , ("z", z)+                       ],+      -- test passes if cvc5 returns 3 abducts (offline)+      testAbdOffline sym f [ ("x", x)+                           , ("y", y)+                           , ("z", z)+                           ],+      -- test passes if cvc5 returns 3 abducts (online)+      testAbdOnline sym [ygte0] xyzgte0+    ]

@@ -42,6 +42,7 @@ allAdapters :: [SolverAdapter EmptyExprBuilderState] allAdapters =   [ cvc4Adapter+  , cvc5Adapter   , yicesAdapter   , z3Adapter   , boolectorAdapter

@@ -1191,7 +1191,7 @@ main :: IO () main = do   testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"-  let solverNames = SolverName <$> [ "cvc4", "yices", "z3" ]+  let solverNames = SolverName <$> [ "cvc4", "cvc5", "yices", "z3" ]   solvers <- reportSolverVersions testLevel id              =<< (zip solverNames <$> mapM getSolverVersion solverNames)   let z3Tests =@@ -1289,6 +1289,7 @@         , testCase "Yices rounding" $ withYices roundingTest         , testCase "Yices #182 test case" $ withYices issue182Test         ]+  let cvc5Tests = cvc4Tests   let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id                             else fmap (ignoreTestBecause (nm <> " not present"))   defaultMain $ testGroup "Tests" $@@ -1309,5 +1310,6 @@     , testUnsafeSetAbstractValue2     ]     <> (skipIfNotPresent "cvc4" cvc4Tests)+    <> (skipIfNotPresent "cvc5" cvc5Tests)     <> (skipIfNotPresent "yices" yicesTests)     <> (skipIfNotPresent "z3" z3Tests)

@@ -91,7 +91,65 @@           diff nabs (>=) 0         _ -> failure   , testIntDivMod+  , testIntMinMax   ]++testIntMinMax :: TestTree+testIntMinMax = testGroup "int min/max"+  [ testProperty "(j <= c && c <= i) -> intMax j i == intMax i j == i" $+    property $ do+      c <- forAll $ Gen.integral $ Range.linear (-1000) 1000+      liftIO $ withTestSolver $ \sym -> do +        j <- freshBoundedInt sym (safeSymbol "j") Nothing (Just c)+        i <- freshBoundedInt sym (safeSymbol "i") (Just c) Nothing+        max_j_i <- intMax sym j i+        res1 <- intEq sym max_j_i i+        asConstantPred res1 @=? Just True+        max_i_j <- intMax sym i j+        res2 <- intEq sym max_i_j i+        asConstantPred res2 @=? Just True+  , testProperty "(lo_i <= i && lo_j <= j) -> (max lo_j lo_j) <= intMax i j" $+    property $ do+      lo_i <- forAll $ Gen.integral $ Range.linear (-1000) 1000+      lo_j <- forAll $ Gen.integral $ Range.linear (-1000) 1000+      liftIO $ withTestSolver $ \sym -> do+        i <- freshBoundedInt sym (safeSymbol "i") (Just lo_i) Nothing+        j <- freshBoundedInt sym (safeSymbol "j") (Just lo_j) Nothing+        lo <- intLit sym (max lo_i lo_j)+        max_i_j <- intMax sym i j+        res1 <- intLe sym lo max_i_j+        asConstantPred res1 @=? Just True+        max_j_i <- intMax sym j i+        res2 <- intLe sym lo max_j_i+        asConstantPred res2 @=? Just True   +  , testProperty "(i <= c && c <= j) -> intMin j i == intMin i j == i" $+    property $ do+      c <- forAll $ Gen.integral $ Range.linear (-1000) 1000+      liftIO $ withTestSolver $ \sym -> do+        j <- freshBoundedInt sym (safeSymbol "j") (Just c) Nothing+        i <- freshBoundedInt sym (safeSymbol "i") Nothing (Just c)+        min_j_i <- intMin sym j i+        res1 <- intEq sym min_j_i i+        asConstantPred res1 @=? Just True+        min_i_j <- intMin sym i j+        res2 <- intEq sym min_i_j i+        asConstantPred res2 @=? Just True+  , testProperty "(i <= hi_i && j <= hi_j) -> intMin i j <= (min hi_j hi_j)" $+    property $ do+      hi_i <- forAll $ Gen.integral $ Range.linear (-1000) 1000+      hi_j <- forAll $ Gen.integral $ Range.linear (-1000) 1000+      liftIO $ withTestSolver $ \sym -> do+        i <- freshBoundedInt sym (safeSymbol "i") Nothing (Just hi_i)+        j <- freshBoundedInt sym (safeSymbol "j") Nothing (Just hi_j)+        hi <- intLit sym (min hi_i hi_j)+        min_i_j <- intMin sym i j+        res1 <- intLe sym min_i_j hi+        asConstantPred res1 @=? Just True+        min_j_i <- intMin sym j i+        res2 <- intLe sym min_j_i hi+        asConstantPred res2 @=? Just True+  ]+  testIntDivMod :: TestTree testIntDivMod = testGroup "integer division and mod"

@@ -0,0 +1,153 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++import           ProbeSolvers+import           Test.Tasty+import           Test.Tasty.ExpectedFailure+import           Test.Tasty.HUnit++import           Data.Maybe+import           System.Environment++import qualified Data.BitVector.Sized as BV+import           Data.Parameterized.Context+import           Data.Parameterized.Map (MapF)+import           Data.Parameterized.Nonce++import           What4.Config+import           What4.Expr+import           What4.Interface+import           What4.SatResult+import           What4.Solver.Adapter+import qualified What4.Solver.CVC5 as CVC5+import qualified What4.Solver.Z3 as Z3++type SimpleExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs++logData :: LogData+logData = defaultLogData { logCallbackVerbose = (\_ -> putStrLn) }++withSym :: FloatModeRepr fm -> (forall t . SimpleExprBuilder t (Flags fm) -> IO a) -> IO a+withSym float_mode action = withIONonceGenerator $ \gen -> do+  sym <- newExprBuilder float_mode EmptyExprBuilderState gen+  extendConfig CVC5.cvc5Options (getConfiguration sym)+  extendConfig Z3.z3Options (getConfiguration sym)+  action sym++intProblem :: IsSymExprBuilder sym => sym -> IO ([SomeSymFn sym], [Pred sym], Pred sym)+intProblem sym = do+  inv <- freshTotalUninterpFn sym (safeSymbol "inv") knownRepr knownRepr+  i <- freshConstant sym (safeSymbol "i") knownRepr+  n <- freshConstant sym (safeSymbol "n") knownRepr+  zero <- intLit sym 0+  one <- intLit sym 1+  lt_1_n <- intLt sym one n+  inv_0_n <- applySymFn sym inv $ Empty :> zero :> n+  -- 1 < n ==> inv(0, n)+  impl0 <- impliesPred sym lt_1_n inv_0_n+  inv_i_n <- applySymFn sym inv $ Empty :> i :> n+  add_i_1 <- intAdd sym i one+  lt_add_i_1_n <- intLt sym add_i_1 n+  conj0 <- andPred sym inv_i_n lt_add_i_1_n+  inv_add_i_1_n <- applySymFn sym inv $ Empty :> add_i_1 :> n+  -- inv(i, n) /\ i+1 < n ==> inv(i+1, n)+  impl1 <- impliesPred sym conj0 inv_add_i_1_n+  le_0_i <- intLe sym zero i+  lt_i_n <- intLt sym i n+  conj1 <- andPred sym le_0_i lt_i_n+  -- inv(i, n) ==> 0 <= i /\ i < n+  impl2 <- impliesPred sym inv_i_n conj1++  -- inv(i, n) /\ not (i + 1 < n) ==> i + 1 == n+  not_lt_add_i_1_n <- notPred sym lt_add_i_1_n+  conj2 <- andPred sym inv_i_n not_lt_add_i_1_n+  eq_add_i_1_n <- intEq sym add_i_1 n+  impl3 <- notPred sym =<< impliesPred sym conj2 eq_add_i_1_n++  return ([SomeSymFn inv], [impl0, impl1, impl2], impl3)++bvProblem :: IsSymExprBuilder sym => sym -> IO ([SomeSymFn sym], [Pred sym], Pred sym)+bvProblem sym = do+  inv <- freshTotalUninterpFn sym (safeSymbol "inv") knownRepr knownRepr+  i <- freshConstant sym (safeSymbol "i") $ BaseBVRepr $ knownNat @64+  n <- freshConstant sym (safeSymbol "n") knownRepr+  zero <- bvLit sym knownNat $ BV.zero knownNat+  one <- bvLit sym knownNat $ BV.one knownNat+  ult_1_n <- bvUlt sym one n+  inv_0_n <- applySymFn sym inv $ Empty :> zero :> n+  -- 1 < n ==> inv(0, n)+  impl0 <- impliesPred sym ult_1_n inv_0_n+  inv_i_n <- applySymFn sym inv $ Empty :> i :> n+  add_i_1 <- bvAdd sym i one+  ult_add_i_1_n <- bvUlt sym add_i_1 n+  conj0 <- andPred sym inv_i_n ult_add_i_1_n+  inv_add_i_1_n <- applySymFn sym inv $ Empty :> add_i_1 :> n+  -- inv(i, n) /\ i+1 < n ==> inv(i+1, n)+  impl1 <- impliesPred sym conj0 inv_add_i_1_n+  ule_0_i <- bvUle sym zero i -- trivially true, here for similarity with int test+  ult_i_n <- bvUlt sym i n+  conj1 <- andPred sym ule_0_i ult_i_n+  -- inv(i, n) ==> 0 <= i /\ i < n+  impl2 <- impliesPred sym inv_i_n conj1++  -- inv(i, n) /\ not (i + 1 < n) ==> i + 1 == n+  not_ult_add_i_1_n <- notPred sym ult_add_i_1_n+  conj2 <- andPred sym inv_i_n not_ult_add_i_1_n+  eq_add_i_1_n <- bvEq sym add_i_1 n+  impl3 <- notPred sym =<< impliesPred sym conj2 eq_add_i_1_n++  return ([SomeSymFn inv], [impl0, impl1, impl2], impl3)++synthesis_test ::+  String ->+  (forall sym . IsSymExprBuilder sym => sym -> IO ([SomeSymFn sym], [Pred sym], Pred sym)) ->+  String ->+  (forall sym t fs .+    sym ~ SimpleExprBuilder t fs =>+    sym ->+    LogData ->+    [SomeSymFn sym] ->+    [BoolExpr t] ->+    IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())) ->+  (forall t fs a .+    SimpleExprBuilder t fs ->+    LogData ->+    [BoolExpr t] ->+    (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) ->+    IO a) ->+  TestTree+synthesis_test test_name synthesis_problem solver_name run_solver_synthesis run_solver_in_override =+  testCase (test_name ++ " " ++ solver_name ++ " test") $ withSym FloatIEEERepr $ \sym -> do+    (synth_fns, constraints, goal) <- synthesis_problem sym++    run_solver_in_override sym logData [goal] $ \res -> isSat res @? "sat"++    subst <- run_solver_synthesis sym logData synth_fns constraints >>= \case+      Sat res -> return res+      Unsat{} -> fail "Infeasible"+      Unknown -> fail "Fail"++    goal' <- substituteSymFns sym subst goal+    run_solver_in_override sym logData [goal'] $ \res -> isUnsat res @? "unsat"++main :: IO ()+main = do+  testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"+  let solverNames = map SolverName [ "cvc5", "z3" ]+  solvers <- reportSolverVersions testLevel id+    =<< (zip solverNames <$> mapM getSolverVersion solverNames)+  let skipPre4_8_9 why =+        let shouldSkip = case lookup (SolverName "z3") solvers of+              Just (SolverVersion v) -> any (`elem` [ "4.8.8" ]) $ words v+              Nothing -> True+        in if shouldSkip then expectFailBecause why else id+      failureZ3 = "failure with older Z3 versions; upgrade to at least 4.8.9"+  defaultMain $ testGroup "Tests" $+    [ synthesis_test "int" intProblem "cvc5" CVC5.runCVC5SyGuS CVC5.runCVC5InOverride+    , skipPre4_8_9 failureZ3 $ synthesis_test "int" intProblem "z3" Z3.runZ3Horn Z3.runZ3InOverride+    , synthesis_test "bv" bvProblem "cvc5" CVC5.runCVC5SyGuS CVC5.runCVC5InOverride+    ]

@@ -12,6 +12,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- for TestShow instance  import           Control.Concurrent ( threadDelay )@@ -58,6 +59,8 @@     , AnOnlineSolver @(SMT2.Writer Z3) Proxy, z3Features, z3Options, Just z3Timeout)   , (SolverName "CVC4"     ,  AnOnlineSolver @(SMT2.Writer CVC4) Proxy, cvc4Features, cvc4Options, Just cvc4Timeout)+  , (SolverName "CVC5"+    ,  AnOnlineSolver @(SMT2.Writer CVC5) Proxy, cvc5Features, cvc5Options, Just cvc5Timeout)   , (SolverName "Yices"     , AnOnlineSolver @Yices.Connection Proxy, yicesDefaultFeatures, yicesOptions, Just yicesGoalTimeout)   , (SolverName "Boolector"@@ -339,7 +342,7 @@       -- impactful due to killing the solver process itself).       --       -- This value should also be <= 60% of useableTimeThreshold to-      -- ensure that the solver runs for a siginificantly longer+      -- ensure that the solver runs for a significantly longer       -- period than the test timeout will be set to.       --       -- This value can be adjusted by the developer as needed to@@ -373,6 +376,7 @@       approxTestTimes :: [ (SolverName, Time) ]       approxTestTimes = [ (SolverName "Z3",         2.27 % Second)    -- Z3 4.8.10.  Z3 is good at self timeout.                         , (SolverName "CVC4",       7.5  % Second)    -- CVC4 1.8+                        , (SolverName "CVC5",       0.40  % Second)   -- CVC5 1.0.0                         , (SolverName "Yices",      2.9  % Second)    -- Yices 2.6.1                         , (SolverName "Boolector",  7.2  % Second)    -- Boolector 3.2.1                         , (SolverName "STP",        1.35 % Second)    -- STP 2.3.3@@ -452,7 +456,7 @@                        (longTimeTest sti Nothing)                finish <- getTime Monotonic                let deltaT = (fromInteger $ toNanoSecs $ diffTimeSpec start finish) % nano Second :: Time-               isLeft rslt @? "solver is to fast for valid timeout testing"+               isLeft rslt @? "solver is too fast for valid timeout testing"                assertBool                  ("Solver check query not interruptible (" <>                    show deltaT <> " > expected " <> show useableTimeThreshold <> ")")

@@ -0,0 +1,58 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE LambdaCase #-}++module SerializeTestUtils where++import           Control.Monad ( when )+import           Control.Monad.IO.Class ( MonadIO, liftIO )+import           Hedgehog+import           System.Directory+import qualified What4.Expr.Builder as S+import qualified What4.Interface as WI+import qualified What4.Serialize.Normalize as WN++import           Prelude+++debugFile :: FilePath+debugFile = "what4serialize.log"++debugReset :: IO ()+debugReset = do e <- doesFileExist debugFile+                when e $ removeFile debugFile++debugOut, alwaysPrint :: MonadIO m => String -> m ()+debugOut msg = liftIO $ do appendFile debugFile (msg <> "\n")+                           -- alwaysPrint  -- comment this out to disable printing+                           return ()+alwaysPrint = liftIO . putStrLn+++showSymFn :: S.ExprSymFn t args ret -> String+showSymFn fn = case S.symFnInfo fn of+  S.DefinedFnInfo _ expr _ -> (show $ WI.printSymExpr expr)+  _ -> ""++symFnEqualityTest :: ( MonadIO m+                     , MonadTest m+                     , sym ~ S.ExprBuilder t st flgs+                     ) =>+                     sym+                  -> WI.SymFn sym args ret+                  -> WI.SymFn sym arts' ret'+                  -> m ()+symFnEqualityTest sym fn1 fn2 = do+  (liftIO $ WN.testEquivSymFn sym fn1 fn2) >>= \case+    WN.ExprEquivalent -> success+    WN.ExprNormEquivalent -> success+    WN.ExprUnequal -> do+      debugOut $ "Resulting functions do not match:\n"+        ++ "fn1:\n" ++ (showSymFn fn1) ++ "\n"+        ++ "fn2:\n" ++ (showSymFn fn2)+      failure

@@ -0,0 +1,20 @@+{-# LANGUAGE ImplicitParams #-}+module Main ( main ) where++import qualified Test.Tasty as T+import qualified Control.Exception as CE++import qualified What4.Utils.Serialize as U+import qualified What4.Serialize.Log as U+import           SymFnTests+++allTests :: (U.HasLogCfg) => T.TestTree+allTests = T.testGroup "What4" symFnTests++main :: IO ()+main = do+  logCfg <- U.mkLogCfg "main"+  let ?logCfg = logCfg+  U.withAsyncLinked (U.tmpFileLogEventConsumer (const True) logCfg) $+    const $ T.defaultMain allTests `CE.finally` U.logEndWith logCfg

@@ -20,7 +20,7 @@   sugarCube :: CUBE-sugarCube = mkCUBE { inputDir = "test/responses"+sugarCube = mkCUBE { inputDirs = [ "test/responses" ]                    , rootName = "*.rsp"                    , expectedSuffix = ".exp"                    , validParams = [ ("parsing", Just ["strict", "lenient"])

@@ -0,0 +1,242 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE LambdaCase #-}++module SymFnTests where++import           Control.Monad.IO.Class ( MonadIO, liftIO )++import           Data.Parameterized.Classes ( ShowF(..) )+import           Data.Parameterized.Context ( pattern (:>), (!) )+import qualified Data.Parameterized.Context as Ctx+import           Data.Parameterized.Nonce+import           Data.Parameterized.Some+import           Data.Parameterized.TraversableFC+import qualified Data.String as String+import qualified Data.Text as T+import qualified Data.Map as Map+import qualified Data.Map.Ordered as OMap+import           Hedgehog+import qualified LibBF as BF++import           Test.Tasty+import           Test.Tasty.Hedgehog hiding (testProperty)+import           SerializeTestUtils+import qualified What4.Expr.Builder as S+import           What4.BaseTypes+import qualified What4.Interface as WI++import qualified What4.Serialize.Printer as WOUT+import qualified What4.Serialize.Parser as WIN+import qualified What4.Serialize.FastSExpr as WSF+++import           Prelude+++symFnTests :: [TestTree]+symFnTests = [+  testGroup "SymFns" (mconcat [+    testBasicArguments WIN.parseSExpr+    , testFunctionCalls WIN.parseSExpr+    , testExpressions WIN.parseSExpr+    , testBasicArguments WSF.parseSExpr+    , testFunctionCalls WSF.parseSExpr+    , testExpressions WSF.parseSExpr+    ])+  ]++data BuilderData t = NoBuilderData++floatSinglePrecision :: FloatPrecisionRepr Prec32+floatSinglePrecision = knownRepr++floatSingleType :: BaseTypeRepr (BaseFloatType Prec32)+floatSingleType = BaseFloatRepr floatSinglePrecision++testBasicArguments :: (T.Text -> Either String WIN.SExpr) -> [TestTree]+testBasicArguments parseSExpr =+    [ testProperty "same argument type" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseIntegerRepr :> BaseIntegerRepr) $ \sym bvs -> do+          let i1 = bvs ! Ctx.i1of2+          let i2 = bvs ! Ctx.i2of2+          WI.intAdd sym i1 i2+    , testProperty "different argument types" $+         withTests 1 $+         property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr) $ \sym bvs -> do+          let i1 = bvs ! Ctx.i1of2+          let b1 = bvs ! Ctx.i2of2+          WI.baseTypeIte sym b1 i1 i1+    ]+++testFunctionCalls :: (T.Text -> Either String WIN.SExpr) -> [TestTree]+testFunctionCalls parseSExpr =+    [ testProperty "no arguments" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do+          ufn <- WI.freshTotalUninterpFn sym (WI.safeSymbol "ufn") Ctx.empty BaseBoolRepr+          WI.applySymFn sym ufn Ctx.empty+    , testProperty "two inner arguments" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do+          i1 <- WI.intLit sym 0+          let b1 = WI.truePred sym+          ufn <- WI.freshTotalUninterpFn sym (WI.safeSymbol "ufn") (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr) BaseBoolRepr+          WI.applySymFn sym ufn (Ctx.empty :> i1 :> b1)+    , testProperty "argument passthrough" $+         withTests 1 $+        property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseBoolRepr :> BaseIntegerRepr) $ \sym bvs -> do+          let i1 = bvs ! Ctx.i2of2+          let b1 = bvs ! Ctx.i1of2+          ufn <- WI.freshTotalUninterpFn sym (WI.safeSymbol "ufn") (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr) BaseBoolRepr+          WI.applySymFn sym ufn (Ctx.empty :> i1 :> b1)+    ]+++testExpressions :: (T.Text -> Either String WIN.SExpr) -> [TestTree]+testExpressions parseSExpr =+    [ testProperty "negative ints" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do+          WI.intLit sym (-1)+    , testProperty "float lit" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do+          WI.floatLit sym floatSinglePrecision (BF.bfFromInt 100)+    , testProperty "simple struct" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do+          i1 <- WI.intLit sym 0+          let b1 = WI.truePred sym+          WI.mkStruct sym (Ctx.empty :> i1 :> b1)+    , testProperty "struct field access" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseStructRepr (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr)) $ \sym bvs -> do+          let struct = bvs ! Ctx.baseIndex+          i1 <- WI.structField sym struct Ctx.i1of2+          b1 <- WI.structField sym struct Ctx.i2of2+          WI.mkStruct sym (Ctx.empty :> b1 :> i1)+    --, testProperty "simple constant array" $+    --    property $ mkEquivalenceTest Ctx.empty $ \sym _ -> do+    --      i1 <- WI.intLit sym 1+    --      WI.constantArray sym (Ctx.empty :> BaseIntegerRepr) i1+    , testProperty "array update" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseArrayRepr (Ctx.empty :> BaseIntegerRepr) BaseIntegerRepr) $ \sym bvs -> do+          i1 <- WI.intLit sym 1+          i2 <- WI.intLit sym 2+          let arr = bvs ! Ctx.baseIndex+          WI.arrayUpdate sym arr (Ctx.empty :> i1) i2+    , testProperty "integer to bitvector" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseIntegerRepr) $ \sym bvs -> do+          let i1 = bvs ! Ctx.baseIndex+          WI.integerToBV sym i1 (WI.knownNat @32)+    , testProperty "float negate" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr (Ctx.empty :> floatSingleType ) $ \sym flts -> do+          let f1 = flts ! Ctx.baseIndex+          WI.floatNeg sym f1+    , testProperty "float abs" $+        withTests 1 $+        property $ mkEquivalenceTest parseSExpr (Ctx.empty :> floatSingleType ) $ \sym flts -> do+          let f1 = flts ! Ctx.baseIndex+          WI.floatAbs sym f1+    ]++mkEquivalenceTest :: forall m args ret+                   . ( MonadTest m+                     , MonadIO m+                     )+                  => (T.Text -> Either String WIN.SExpr)+                  -> Ctx.Assignment BaseTypeRepr args+                  -> (forall sym+                       . WI.IsSymExprBuilder sym+                      => sym+                      -> Ctx.Assignment (WI.SymExpr sym) args+                      -> IO (WI.SymExpr sym ret))+                  -> m ()+mkEquivalenceTest parseSExpr argTs getExpr = do+  Some r <- liftIO $ newIONonceGenerator+  sym <- liftIO $ S.newExprBuilder S.FloatRealRepr NoBuilderData r+  liftIO $ S.startCaching sym+  bvs <- liftIO $ forFC argTs $ \repr -> do+    n <- freshNonce r+    let nm = "bv" ++ show (indexValue n)+    WI.freshBoundVar sym (WI.safeSymbol nm) repr+  e <- liftIO $ getExpr sym (fmapFC (WI.varExpr sym) bvs)+  go sym bvs e+  where+    go :: forall sym t flgs st .+          ( WI.IsSymExprBuilder sym+          , sym ~ S.ExprBuilder t st flgs+          , ShowF (WI.SymExpr sym)+          )+       => sym+       -> Ctx.Assignment (WI.BoundVar sym) args+       -> WI.SymExpr sym ret+       -> m ()+    go sym bvs expr = do+      fn1 <- liftIO $ WI.definedFn sym (WI.safeSymbol "fn") bvs expr WI.NeverUnfold+      let scfg = WOUT.Config { WOUT.cfgAllowFreeVars = True+                             , WOUT.cfgAllowFreeSymFns = True+                             }+          res = WOUT.serializeSymFnWithConfig scfg fn1+          fnText = WOUT.printSExpr mempty $ WOUT.resSExpr res+          fnMap = Map.fromList $ map (\(x,y)->(y,x)) $ OMap.assocs $ WOUT.resSymFnEnv res+          exprMap = Map.fromList $+                    map (\((Some bv),freshName) ->+                           (freshName, (Some (WI.varExpr sym bv))))+                    $ OMap.assocs+                    $ WOUT.resFreeVarEnv res+      -- lcfg <- liftIO $ Log.mkLogCfg "rndtrip"+      deser <- do+        dcfg <- return $ (WIN.defaultConfig sym)+                { WIN.cSymFnLookup = \nm ->+                    case Map.lookup nm fnMap of+                      Nothing -> return Nothing+                      Just (WOUT.SomeExprSymFn fn) -> return $ Just (WIN.SomeSymFn fn)+                , WIN.cExprLookup = \nm ->+                    case Map.lookup nm exprMap of+                      Nothing -> return Nothing+                      Just (Some x) -> return $ Just (Some x)+                }+        case parseSExpr fnText of+          Left errMsg -> return $ Left errMsg+          Right sexpr -> liftIO $ WIN.deserializeSymFnWithConfig sym dcfg sexpr+      case deser of+        Left err -> do+          debugOut $ "Unexpected deserialization error: " ++ err ++ "!\n S-expression:\n"+          debugOut $ (T.unpack fnText) ++ "\n"+          failure+        Right (WIN.SomeSymFn fn2) -> do+          fn1out <- liftIO $ WI.definedFn sym (WI.safeSymbol "fn") bvs expr WI.NeverUnfold+          symFnEqualityTest sym fn1out fn2++-- | Create a 'T.TestTree' from a Hedgehog 'Property'.+--+-- Note that @tasty-hedgehog@'s version of 'testProperty' has been deprecated+-- in favor of 'testPropertyNamed', whose second argument is intended to+-- represent the name of a top-level 'Property' value to run in the event that+-- the test fails. See https://github.com/qfpl/tasty-hedgehog/pull/42.+--+-- That being said, @what4-serialize@ currently does not define any of the+-- properties that it tests as top-level values. In the+-- meantime, we avoid incurring deprecation warnings by defining our own+-- version of 'testProperty'. The downside to this workaround is that if a+-- property fails, the error message it will produce will likely suggest+-- running ill-formed Haskell code, so users will have to use context clues to+-- determine how to /actually/ reproduce the error.+testProperty :: TestName -> Property -> TestTree+testProperty name = testPropertyNamed name (String.fromString name)

@@ -11,7 +11,7 @@ module Main where  import Control.Exception-import Control.Monad ((<=<)) -- , when)+import Control.Monad ((<=<), unless) import Control.Monad.IO.Class (liftIO) import           Control.Monad.Trans.Maybe import Data.Bits@@ -22,6 +22,7 @@ import Data.Parameterized.Some import Data.String import Numeric (showHex)+import System.Exit (exitFailure) -- import System.IO  import LibBF@@ -78,8 +79,8 @@                             pure (fromString (show t), p)                        | Some t <- xs                        ]-     _ <- checkSequential $ Group "Float tests" tests-     return ()+     testsPassed <- checkSequential $ Group "Float tests" tests+     unless testsPassed exitFailure   data FUnOp

@@ -1,9 +1,9 @@ Cabal-version: 2.4 Name:          what4-Version:       1.3+Version:       1.4 Author:        Galois Inc.-Maintainer:    jhendrix@galois.com, rdockins@galois.com-Copyright:     (c) Galois, Inc 2014-2021+Maintainer:    rscott@galois.com, kquick@galois.com+Copyright:     (c) Galois, Inc 2014-2023 License:       BSD-3-Clause License-file:  LICENSE Build-type:    Simple@@ -16,7 +16,7 @@   What4 is a generic library for representing values as symbolic formulae which may   contain references to symbolic values, representing unknown variables.   It provides support for communicating with a variety of SAT and SMT solvers,-  including Z3, CVC4, Yices, Boolector, STP, and dReal.+  including Z3, CVC4, CVC5, Yices, Boolector, STP, and dReal.    The data representation types make heavy use of GADT-style type indices   to ensure type-correct manipulation of symbolic values.@@ -91,18 +91,18 @@ library   import: bldflags   build-depends:-    base >= 4.8 && < 5,+    base >= 4.10 && < 5,     async,     attoparsec >= 0.13,     bimap >= 0.2,     bifunctors >= 5,+    BoundedChan >= 1 && < 2,     bv-sized >= 1.0.0,     bytestring >= 0.10,     deriving-compat >= 0.5,     concurrent-extra >= 0.7 && < 0.8,     config-value >= 0.8 && < 0.9,     containers >= 0.5.0.0,-    data-binary-ieee754,     deepseq >= 1.3,     directory >= 1.2.2,     exceptions >= 0.10,@@ -113,19 +113,26 @@     io-streams >= 1.5,     lens >= 4.18,     libBF >= 0.6 && < 0.7,+    megaparsec >= 8 && < 10,     mtl >= 2.2.1,+    ordered-containers >= 0.2 && < 0.3,     panic >= 0.3,     parameterized-utils >= 2.1 && < 2.2,+    parsec >= 3 && < 4,     prettyprinter >= 1.7.0,     process >= 1.2,+    s-cargot >= 0.1 && < 0.2,     scientific >= 0.3.6,+    stm,     temporary >= 1.2,     template-haskell,-    text >= 1.2.4.0 && < 1.3,+    text >= 1.2.4.0 && < 2.1,     th-abstraction >=0.1 && <0.5,     th-lift >= 0.8.2 && < 0.9,     th-lift-instances >= 0.1 && < 0.2,+    time >= 1.8 && < 1.13,     transformers >= 0.4,+    unliftio >= 0.2 && < 0.3,     unordered-containers >= 0.2.10,     utf8-string >= 1.0.1,     vector >= 0.12.1,@@ -175,10 +182,18 @@     What4.Expr.WeightedSum     What4.Expr.UnaryBV +    What4.Serialize.FastSExpr+    What4.Serialize.Log+    What4.Serialize.Normalize+    What4.Serialize.Parser+    What4.Serialize.Printer+    What4.Serialize.SETokens+     What4.Solver     What4.Solver.Adapter     What4.Solver.Boolector     What4.Solver.CVC4+    What4.Solver.CVC5     What4.Solver.DReal     What4.Solver.ExternalABC     What4.Solver.STP@@ -217,6 +232,7 @@     What4.Utils.OnlyIntRepr     What4.Utils.Process     What4.Utils.ResolveBounds.BV+    What4.Utils.Serialize     What4.Utils.Streams     What4.Utils.StringLiteral     What4.Utils.Word16String@@ -236,6 +252,19 @@     parameterized-utils,     what4 +test-suite abduct+  import: testdefs-hunit+  type: exitcode-stdio-1.0+  main-is: Abduct.hs+  default-language: Haskell2010++  build-depends:+    base,+    parameterized-utils,+    what4,+    text,+    temporary+ test-suite adapter-test   import: bldflags, testdefs-hunit   type: exitcode-stdio-1.0@@ -257,7 +286,6 @@     bv-sized,     bytestring,     containers,-    data-binary-ieee754,     lens,     mtl >= 2.2.1,     process,@@ -296,7 +324,6 @@     bytestring,     clock,     containers,-    data-binary-ieee754,     exceptions,     lens,     prettyprinter,@@ -320,7 +347,6 @@     bv-sized,     bytestring,     containers,-    data-binary-ieee754,     libBF,     prettyprinter,     process,@@ -396,5 +422,42 @@                , exceptions                , io-streams                , lumberjack-               , tasty-sugar >= 1.1 && < 1.2+               , tasty-sugar >= 2.0 && < 2.1                , text++test-suite what4-serialize-tests+  default-language: Haskell2010+  type: exitcode-stdio-1.0+  ghc-options: -Wall -Wcompat -rtsopts -threaded+  hs-source-dirs: test+  main-is: SerializeTests.hs+  other-modules: SymFnTests, SerializeTestUtils+  build-depends:   what4+                 , base+                 , containers+                 , directory+                 , exceptions+                 , hedgehog+                 , libBF+                 , tasty+                 , tasty-hunit+                 , tasty-hedgehog+                 , text+                 , parameterized-utils+                 , async+                 , directory+                 , ordered-containers++test-suite invariant-synthesis+  import: bldflags, testdefs-hunit+  type: exitcode-stdio-1.0++  main-is: InvariantSynthesis.hs++  other-modules: ProbeSolvers++  build-depends:+    bv-sized,+    process,+    tasty-expected-failure >= 0.12 && < 0.13+