diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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. diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/doc/implementation.md b/doc/implementation.md --- a/doc/implementation.md +++ b/doc/implementation.md @@ -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 diff --git a/src/What4/Expr/App.hs b/src/What4/Expr/App.hs --- a/src/What4/Expr/App.hs +++ b/src/What4/Expr/App.hs @@ -1722,6 +1722,8 @@ instance IsSymFn (ExprSymFn t) where fnArgTypes = symFnArgTypes fnReturnType = symFnReturnType + fnTestEquality = testExprSymFnEq + fnCompare f g = compareF (symFnId f) (symFnId g) ------------------------------------------------------------------------------- diff --git a/src/What4/Expr/AppTheory.hs b/src/What4/Expr/AppTheory.hs --- a/src/What4/Expr/AppTheory.hs +++ b/src/What4/Expr/AppTheory.hs @@ -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) diff --git a/src/What4/Expr/Builder.hs b/src/What4/Expr/Builder.hs --- a/src/What4/Expr/Builder.hs +++ b/src/What4/Expr/Builder.hs @@ -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) diff --git a/src/What4/Expr/VarIdentification.hs b/src/What4/Expr/VarIdentification.hs --- a/src/What4/Expr/VarIdentification.hs +++ b/src/What4/Expr/VarIdentification.hs @@ -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 diff --git a/src/What4/Interface.hs b/src/What4/Interface.hs --- a/src/What4/Interface.hs +++ b/src/What4/Interface.hs @@ -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 diff --git a/src/What4/ProblemFeatures.hs b/src/What4/ProblemFeatures.hs --- a/src/What4/ProblemFeatures.hs +++ b/src/What4/ProblemFeatures.hs @@ -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 diff --git a/src/What4/Protocol/Online.hs b/src/What4/Protocol/Online.hs --- a/src/What4/Protocol/Online.hs +++ b/src/What4/Protocol/Online.hs @@ -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. diff --git a/src/What4/Protocol/SExp.hs b/src/What4/Protocol/SExp.hs --- a/src/What4/Protocol/SExp.hs +++ b/src/What4/Protocol/SExp.hs @@ -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)) ++ [')'] diff --git a/src/What4/Protocol/SMTLib2.hs b/src/What4/Protocol/SMTLib2.hs --- a/src/What4/Protocol/SMTLib2.hs +++ b/src/What4/Protocol/SMTLib2.hs @@ -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 +-- +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 diff --git a/src/What4/Protocol/SMTLib2/Parse.hs b/src/What4/Protocol/SMTLib2/Parse.hs --- a/src/What4/Protocol/SMTLib2/Parse.hs +++ b/src/What4/Protocol/SMTLib2/Parse.hs @@ -17,7 +17,7 @@ ( -- * CheckSatResponse CheckSatResponse(..) , readCheckSatResponse - -- * GetModelResonse + -- * GetModelResponse , GetModelResponse , readGetModelResponse , ModelResponse(..) diff --git a/src/What4/Protocol/SMTLib2/Response.hs b/src/What4/Protocol/SMTLib2/Response.hs --- a/src/What4/Protocol/SMTLib2/Response.hs +++ b/src/What4/Protocol/SMTLib2/Response.hs @@ -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 diff --git a/src/What4/Protocol/SMTLib2/Syntax.hs b/src/What4/Protocol/SMTLib2/Syntax.hs --- a/src/What4/Protocol/SMTLib2/Syntax.hs +++ b/src/What4/Protocol/SMTLib2/Syntax.hs @@ -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 diff --git a/src/What4/Protocol/SMTWriter.hs b/src/What4/Protocol/SMTWriter.hs --- a/src/What4/Protocol/SMTWriter.hs +++ b/src/What4/Protocol/SMTWriter.hs @@ -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 diff --git a/src/What4/Protocol/VerilogWriter.hs b/src/What4/Protocol/VerilogWriter.hs --- a/src/What4/Protocol/VerilogWriter.hs +++ b/src/What4/Protocol/VerilogWriter.hs @@ -1,4 +1,5 @@ {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {- Module : What4.Protocol.VerilogWriter.AST Copyright : (c) Galois, Inc 2020 diff --git a/src/What4/Serialize/FastSExpr.hs b/src/What4/Serialize/FastSExpr.hs new file mode 100644 --- /dev/null +++ b/src/What4/Serialize/FastSExpr.hs @@ -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) "" 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 diff --git a/src/What4/Serialize/Log.hs b/src/What4/Serialize/Log.hs new file mode 100644 --- /dev/null +++ b/src/What4/Serialize/Log.hs @@ -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?" diff --git a/src/What4/Serialize/Normalize.hs b/src/What4/Serialize/Normalize.hs new file mode 100644 --- /dev/null +++ b/src/What4/Serialize/Normalize.hs @@ -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 diff --git a/src/What4/Serialize/Parser.hs b/src/What4/Serialize/Parser.hs new file mode 100644 --- /dev/null +++ b/src/What4/Serialize/Parser.hs @@ -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)) diff --git a/src/What4/Serialize/Printer.hs b/src/What4/Serialize/Printer.hs new file mode 100644 --- /dev/null +++ b/src/What4/Serialize/Printer.hs @@ -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 diff --git a/src/What4/Serialize/SETokens.hs b/src/What4/Serialize/SETokens.hs new file mode 100644 --- /dev/null +++ b/src/What4/Serialize/SETokens.hs @@ -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) diff --git a/src/What4/Solver.hs b/src/What4/Solver.hs --- a/src/What4/Solver.hs +++ b/src/What4/Solver.hs @@ -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 diff --git a/src/What4/Solver/Boolector.hs b/src/What4/Solver/Boolector.hs --- a/src/What4/Solver/Boolector.hs +++ b/src/What4/Solver/Boolector.hs @@ -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 diff --git a/src/What4/Solver/CVC4.hs b/src/What4/Solver/CVC4.hs --- a/src/What4/Solver/CVC4.hs +++ b/src/What4/Solver/CVC4.hs @@ -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 diff --git a/src/What4/Solver/CVC5.hs b/src/What4/Solver/CVC5.hs new file mode 100644 --- /dev/null +++ b/src/What4/Solver/CVC5.hs @@ -0,0 +1,380 @@ +------------------------------------------------------------------------ +-- | +-- Module : What4.Solver.CVC5 +-- Description : Solver adapter code for cvc5 +-- Copyright : (c) Galois, Inc 2022 +-- License : BSD3 +-- Maintainer : Rob Dockins +-- 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 diff --git a/src/What4/Solver/Yices.hs b/src/What4/Solver/Yices.hs --- a/src/What4/Solver/Yices.hs +++ b/src/What4/Solver/Yices.hs @@ -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 diff --git a/src/What4/Solver/Z3.hs b/src/What4/Solver/Z3.hs --- a/src/What4/Solver/Z3.hs +++ b/src/What4/Solver/Z3.hs @@ -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 diff --git a/src/What4/Utils/AbstractDomains.hs b/src/What4/Utils/AbstractDomains.hs --- a/src/What4/Utils/AbstractDomains.hs +++ b/src/What4/Utils/AbstractDomains.hs @@ -26,6 +26,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} module What4.Utils.AbstractDomains diff --git a/src/What4/Utils/OnlyIntRepr.hs b/src/What4/Utils/OnlyIntRepr.hs --- a/src/What4/Utils/OnlyIntRepr.hs +++ b/src/What4/Utils/OnlyIntRepr.hs @@ -8,6 +8,7 @@ restricting index types in MATLAB arrays. -} {-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeOperators #-} module What4.Utils.OnlyIntRepr ( OnlyIntRepr(..) , toBaseTypeRepr diff --git a/src/What4/Utils/Serialize.hs b/src/What4/Utils/Serialize.hs new file mode 100644 --- /dev/null +++ b/src/What4/Utils/Serialize.hs @@ -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 diff --git a/test/Abduct.hs b/test/Abduct.hs new file mode 100644 --- /dev/null +++ b/test/Abduct.hs @@ -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 + ] diff --git a/test/AdapterTest.hs b/test/AdapterTest.hs --- a/test/AdapterTest.hs +++ b/test/AdapterTest.hs @@ -42,6 +42,7 @@ allAdapters :: [SolverAdapter EmptyExprBuilderState] allAdapters = [ cvc4Adapter + , cvc5Adapter , yicesAdapter , z3Adapter , boolectorAdapter diff --git a/test/ExprBuilderSMTLib2.hs b/test/ExprBuilderSMTLib2.hs --- a/test/ExprBuilderSMTLib2.hs +++ b/test/ExprBuilderSMTLib2.hs @@ -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) diff --git a/test/ExprsTest.hs b/test/ExprsTest.hs --- a/test/ExprsTest.hs +++ b/test/ExprsTest.hs @@ -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" diff --git a/test/InvariantSynthesis.hs b/test/InvariantSynthesis.hs new file mode 100644 --- /dev/null +++ b/test/InvariantSynthesis.hs @@ -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 + ] diff --git a/test/OnlineSolverTest.hs b/test/OnlineSolverTest.hs --- a/test/OnlineSolverTest.hs +++ b/test/OnlineSolverTest.hs @@ -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 <> ")") diff --git a/test/SerializeTestUtils.hs b/test/SerializeTestUtils.hs new file mode 100644 --- /dev/null +++ b/test/SerializeTestUtils.hs @@ -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 diff --git a/test/SerializeTests.hs b/test/SerializeTests.hs new file mode 100644 --- /dev/null +++ b/test/SerializeTests.hs @@ -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 diff --git a/test/SolverParserTest.hs b/test/SolverParserTest.hs --- a/test/SolverParserTest.hs +++ b/test/SolverParserTest.hs @@ -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"]) diff --git a/test/SymFnTests.hs b/test/SymFnTests.hs new file mode 100644 --- /dev/null +++ b/test/SymFnTests.hs @@ -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) diff --git a/test/TestTemplate.hs b/test/TestTemplate.hs --- a/test/TestTemplate.hs +++ b/test/TestTemplate.hs @@ -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 diff --git a/what4.cabal b/what4.cabal --- a/what4.cabal +++ b/what4.cabal @@ -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 +