{-# 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 #-}
module What4.Serialize.Parser
( deserializeExpr
, deserializeExprWithConfig
, deserializeSymFn
, deserializeSymFnWithConfig
, deserializeBaseType
, readBaseTypes
, Atom(..)
, S.WellFormedSExpr(..)
, Config(..)
, defaultConfig
, SomeSymFn(..)
, type SExpr
, parseSExpr
, printSExpr
) where
import Control.Monad ( when )
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
{ forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
cSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
, forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup :: Text -> IO (Maybe (Some (W4.SymExpr sym)))
}
defaultConfig :: (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym)) => sym -> Config sym
defaultConfig :: forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
sym -> Config sym
defaultConfig sym
_sym = Config { cSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
cSymFnLookup = forall a b. a -> b -> a
const (forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
, cExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup = forall a b. a -> b -> a
const (forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
}
data ProcessorEnv sym =
ProcessorEnv
{ forall sym. ProcessorEnv sym -> sym
procSym :: sym
, forall sym. ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym))
procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
, forall sym.
ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup :: Text -> IO (Maybe (Some (W4.SymExpr sym)))
, forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv :: HM.HashMap Text (Some (W4.SymExpr sym))
, forall sym. ProcessorEnv sym -> HashMap Text (SomeSymFn sym)
procLetFnEnv :: HM.HashMap Text (SomeSymFn sym)
}
type Processor sym a = E.ExceptT String (R.ReaderT (ProcessorEnv sym) IO) a
runProcessor :: ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor :: forall sym a.
ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor ProcessorEnv sym
env Processor sym a
action = forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
R.runReaderT (forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
E.runExceptT Processor sym a
action) ProcessorEnv sym
env
lookupExpr :: Text -> Processor sym (Maybe (Some (W4.SymExpr sym)))
lookupExpr :: forall sym. Text -> Processor sym (Maybe (Some (SymExpr sym)))
lookupExpr Text
nm = do
Text -> IO (Maybe (Some (SymExpr sym)))
userLookupFn <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks forall sym.
ProcessorEnv sym -> Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup
HashMap Text (Some (SymExpr sym))
letEnv <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv
case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup Text
nm HashMap Text (Some (SymExpr sym))
letEnv of
Maybe (Some (SymExpr sym))
Nothing -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Text -> IO (Maybe (Some (SymExpr sym)))
userLookupFn Text
nm
Maybe (Some (SymExpr sym))
res -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (Some (SymExpr sym))
res
lookupFn :: Text -> Processor sym (Maybe (SomeSymFn sym))
lookupFn :: forall sym. Text -> Processor sym (Maybe (SomeSymFn sym))
lookupFn Text
nm = do
Text -> IO (Maybe (SomeSymFn sym))
userLookupFn <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks forall sym. ProcessorEnv sym -> Text -> IO (Maybe (SomeSymFn sym))
procSymFnLookup
HashMap Text (SomeSymFn sym)
letEnv <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks forall sym. ProcessorEnv sym -> HashMap Text (SomeSymFn sym)
procLetFnEnv
case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup Text
nm HashMap Text (SomeSymFn sym)
letEnv of
Maybe (SomeSymFn sym)
Nothing -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Text -> IO (Maybe (SomeSymFn sym))
userLookupFn Text
nm
Maybe (SomeSymFn sym)
res -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (SomeSymFn sym)
res
deserializeExpr ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> sym
-> SExpr
-> IO (Either String (Some (W4.SymExpr sym)))
deserializeExpr :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
deserializeExpr sym
sym = forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> Config sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
deserializeExprWithConfig sym
sym Config sym
cfg
where cfg :: Config sym
cfg = forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
sym -> Config sym
defaultConfig sym
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 :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> Config sym -> SExpr -> IO (Either String (Some (SymExpr sym)))
deserializeExprWithConfig sym
sym Config sym
cfg SExpr
sexpr = forall sym a.
ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor ProcessorEnv sym
env (forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
sexpr)
where env :: ProcessorEnv sym
env = ProcessorEnv { procSym :: sym
procSym = sym
sym
, procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
procSymFnLookup = forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
cSymFnLookup Config sym
cfg
, procExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup = forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup Config sym
cfg
, procLetEnv :: HashMap Text (Some (SymExpr sym))
procLetEnv = forall k v. HashMap k v
HM.empty
, procLetFnEnv :: HashMap Text (SomeSymFn sym)
procLetFnEnv = forall k v. HashMap k v
HM.empty
}
deserializeSymFn ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> sym
-> SExpr
-> IO (Either String (SomeSymFn sym))
deserializeSymFn :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> SExpr -> IO (Either String (SomeSymFn sym))
deserializeSymFn sym
sym = forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn sym))
deserializeSymFnWithConfig sym
sym Config sym
cfg
where cfg :: Config sym
cfg = forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
sym -> Config sym
defaultConfig sym
sym
deserializeSymFnWithConfig ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> sym
-> Config sym
-> SExpr
-> IO (Either String (SomeSymFn sym))
deserializeSymFnWithConfig :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym -> Config sym -> SExpr -> IO (Either String (SomeSymFn sym))
deserializeSymFnWithConfig sym
sym Config sym
cfg SExpr
sexpr = forall sym a.
ProcessorEnv sym -> Processor sym a -> IO (Either String a)
runProcessor ProcessorEnv sym
env (forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (SomeSymFn sym)
readSymFn SExpr
sexpr)
where env :: ProcessorEnv sym
env = ProcessorEnv { procSym :: sym
procSym = sym
sym
, procSymFnLookup :: Text -> IO (Maybe (SomeSymFn sym))
procSymFnLookup = forall sym. Config sym -> Text -> IO (Maybe (SomeSymFn sym))
cSymFnLookup Config sym
cfg
, procExprLookup :: Text -> IO (Maybe (Some (SymExpr sym)))
procExprLookup = forall sym. Config sym -> Text -> IO (Maybe (Some (SymExpr sym)))
cExprLookup Config sym
cfg
, procLetEnv :: HashMap Text (Some (SymExpr sym))
procLetEnv = forall k v. HashMap k v
HM.empty
, procLetFnEnv :: HashMap Text (SomeSymFn sym)
procLetFnEnv = forall k v. HashMap k v
HM.empty
}
deserializeBaseType ::
SExpr
-> Either String (Some BaseTypeRepr)
deserializeBaseType :: SExpr -> Either String (Some BaseTypeRepr)
deserializeBaseType SExpr
sexpr = forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType SExpr
sexpr
prefixError :: (Monoid e, E.MonadError e m) => e -> m a -> m a
prefixError :: forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError e
prefix m a
act = forall e (m :: Type -> Type) a.
MonadError e m =>
m a -> (e -> m a) -> m a
E.catchError m a
act (forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => a -> a -> a
mappend e
prefix)
fromMaybeError :: (E.MonadError e m) => e -> Maybe a -> m a
fromMaybeError :: forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError e
err = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError e
err) forall (m :: Type -> Type) a. Monad m => a -> m a
return
readBaseType ::
forall m . (E.MonadError String m)
=> SExpr
-> m (Some BaseTypeRepr)
readBaseType :: forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType SExpr
sexpr =
case SExpr
sexpr of
S.WFSAtom (AId Text
atom) ->
case (Text -> String
T.unpack Text
atom) of
String
"Bool" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseBoolType
BaseBoolRepr
String
"Int" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseIntegerType
BaseIntegerRepr
String
"Real" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseRealType
BaseRealRepr
String
"String" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
BaseStringRepr StringInfoRepr 'Unicode
UnicodeRepr)
String
"Complex" -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BaseTypeRepr 'BaseComplexType
BaseComplexRepr
String
_ -> m (Some BaseTypeRepr)
panic
S.WFSList [(S.WFSAtom (AId Text
"BV")), (S.WFSAtom (AInt Integer
w))]
| Just (Some NatRepr x
wRepr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
w
, Just LeqProof 1 x
LeqProof <- forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr x
wRepr
-> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr x
wRepr)
| Bool
otherwise
-> m (Some BaseTypeRepr)
panic
S.WFSList [(S.WFSAtom (AId Text
"Float")), (S.WFSAtom (AInt Integer
e)), (S.WFSAtom (AInt Integer
s))]
| Just (Some NatRepr x
eRepr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
e
, Just (Some NatRepr x
sRepr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
s
, Just LeqProof 2 x
LeqProof <- forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @2) NatRepr x
eRepr
, Just LeqProof 2 x
LeqProof <- forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Nat). KnownNat n => NatRepr n
knownNat @2) NatRepr x
sRepr
-> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr (forall (eb :: Nat) (sb :: Nat).
(2 <= eb, 2 <= sb) =>
NatRepr eb
-> NatRepr sb -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
FloatingPointPrecisionRepr NatRepr x
eRepr NatRepr x
sRepr)))
| Bool
otherwise -> m (Some BaseTypeRepr)
panic
S.WFSList [(S.WFSAtom (AId Text
"Struct")), SExpr
args] -> do
Some Assignment BaseTypeRepr x
tps <- forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some (Assignment BaseTypeRepr))
readBaseTypes SExpr
args
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr ('BaseStructType ctx)
BaseStructRepr Assignment BaseTypeRepr x
tps)
S.WFSList [S.WFSAtom (AId Text
"Array"), SExpr
ixArgs, SExpr
tpArg] -> do
Some Assignment BaseTypeRepr x
ixs <- forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some (Assignment BaseTypeRepr))
readBaseTypes SExpr
ixArgs
Some BaseTypeRepr x
tp <- forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType SExpr
tpArg
case forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign Assignment BaseTypeRepr x
ixs of
AssignView BaseTypeRepr x
Ctx.AssignEmpty -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"array type has no indices: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
sexpr
Ctx.AssignExtend Assignment BaseTypeRepr ctx1
_ BaseTypeRepr tp
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr Assignment BaseTypeRepr x
ixs BaseTypeRepr x
tp)
SExpr
_ -> m (Some BaseTypeRepr)
panic
where
panic :: m (Some BaseTypeRepr)
panic = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"unknown base type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
sexpr
readBaseTypes ::
forall m . (E.MonadError String m)
=> SExpr
-> m (Some (Ctx.Assignment BaseTypeRepr))
readBaseTypes :: forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some (Assignment BaseTypeRepr))
readBaseTypes sexpr :: SExpr
sexpr@(S.WFSAtom Atom
_) = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"expected list of base types: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
sexpr
readBaseTypes (S.WFSList [SExpr]
sexprs) = forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType [SExpr]
sexprs
data BVProof tp where
BVProof :: forall n. (1 <= n) => NatRepr n -> BVProof (BaseBVType n)
getBVProof :: (W4.IsExpr ex, E.MonadError String m) => ex tp -> m (BVProof tp)
getBVProof :: forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof ex tp
expr =
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType ex tp
expr of
BaseBVRepr NatRepr w
n -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (res :: Nat).
(1 <= res) =>
NatRepr res -> BVProof (BaseBVType res)
BVProof NatRepr w
n
BaseTypeRepr tp
t -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"expected BV, found %s" (forall a. Show a => a -> String
show BaseTypeRepr tp
t)
data Op sym where
FloatOp1 :: (forall fpp . sym ->
W4.SymFloat sym fpp ->
IO (W4.SymFloat sym fpp))
-> Op sym
Op1 :: Ctx.Assignment BaseTypeRepr (Ctx.EmptyCtx Ctx.::> arg1)
-> (sym ->
W4.SymExpr sym arg1 ->
IO (W4.SymExpr sym ret))
-> Op sym
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
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
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
BVOp1 :: (forall w . (1 <= w) =>
sym ->
W4.SymBV sym w ->
IO (W4.SymBV sym w))
-> Op sym
BVOp2 :: (forall w . (1 <= w) =>
sym ->
W4.SymBV sym w ->
W4.SymBV sym w ->
IO (W4.SymBV sym w))
-> Op sym
BVComp2 :: (forall w . (1 <= w) =>
sym ->
W4.SymBV sym w ->
W4.SymBV sym w ->
IO (W4.Pred sym))
-> Op sym
lookupOp :: forall sym . W4.IsSymExprBuilder sym => Text -> Maybe (Op sym)
lookupOp :: forall sym. IsSymExprBuilder sym => Text -> Maybe (Op sym)
lookupOp Text
name = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HM.lookup Text
name forall sym. IsSymExprBuilder sym => HashMap Text (Op sym)
opTable
opTable :: (W4.IsSymExprBuilder sym) => HM.HashMap Text (Op sym)
opTable :: forall sym. IsSymExprBuilder sym => HashMap Text (Op sym)
opTable =
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HM.fromList [
(Text
"andp", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred)
, (Text
"orp", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.orPred)
, (Text
"xorp", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.xorPred)
, (Text
"notp", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred)
, (Text
"floatneg", forall sym.
(forall (fpp :: FloatPrecision).
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
-> Op sym
FloatOp1 forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatNeg)
, (Text
"floatabs", forall sym.
(forall (fpp :: FloatPrecision).
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp))
-> Op sym
FloatOp1 forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatAbs)
, (Text
"intmul", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMul)
, (Text
"intadd", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intAdd)
, (Text
"intmod", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intMod)
, (Text
"intdiv", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intDiv)
, (Text
"intle", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLe)
, (Text
"intabs", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intAbs)
, (Text
"bvand", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAndBits)
, (Text
"bvor", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvOrBits)
, (Text
"bvadd", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAdd)
, (Text
"bvmul", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvMul)
, (Text
"bvudiv", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvUdiv)
, (Text
"bvurem", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvUrem)
, (Text
"bvshl", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvShl)
, (Text
"bvlshr", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvLshr)
, (Text
"bvnand", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a b. (a -> b) -> a -> b
$ \sym
sym SymBV sym w
arg1 SymBV sym w
arg2 -> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAndBits sym
sym SymBV sym w
arg1 SymBV sym w
arg2)
, (Text
"bvnor", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a b. (a -> b) -> a -> b
$ \sym
sym SymBV sym w
arg1 SymBV sym w
arg2 -> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvOrBits sym
sym SymBV sym w
arg1 SymBV sym w
arg2)
, (Text
"bvxor", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvXorBits)
, (Text
"bvxnor", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall a b. (a -> b) -> a -> b
$ \sym
sym SymBV sym w
arg1 SymBV sym w
arg2 -> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits sym
sym forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvXorBits sym
sym SymBV sym w
arg1 SymBV sym w
arg2)
, (Text
"bvsub", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSub)
, (Text
"bvsdiv", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSdiv)
, (Text
"bvsrem", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSrem)
, (Text
"bvsmod", forall a. HasCallStack => String -> a
error String
"bvsmod is not implemented")
, (Text
"bvashr", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAshr)
, (Text
"bvult", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUlt)
, (Text
"bvule", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUle)
, (Text
"bvugt", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUgt)
, (Text
"bvuge", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUge)
, (Text
"bvslt", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSlt)
, (Text
"bvsle", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSle)
, (Text
"bvsgt", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSgt)
, (Text
"bvsge", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvSge)
, (Text
"bveq", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvEq)
, (Text
"bvne", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> Op sym
BVComp2 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvNe)
, (Text
"bvneg", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp1 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNeg)
, (Text
"bvnot", forall sym.
(forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w))
-> Op sym
BVOp1 forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNotBits)
, (Text
"fnegd", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatNeg @_ @Prec64)
, (Text
"fnegs", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatNeg @_ @Prec32)
, (Text
"fabsd", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatAbs @_ @Prec64)
, (Text
"fabss", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatAbs @_ @Prec32)
, (Text
"fsqrt", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatSqrt @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
, (Text
"fsqrts", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatSqrt @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x)
, (Text
"fnand", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
W4.floatIsNaN @_ @Prec64)
, (Text
"fnans", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> IO (Pred sym)
W4.floatIsNaN @_ @Prec32)
, (Text
"frsp", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision) (fpp' :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymFloat sym fpp'
-> IO (SymFloat sym fpp)
W4.floatCast @_ @Prec32 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
, (Text
"fp_single_to_double", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym ->
forall sym (fpp :: FloatPrecision) (fpp' :: FloatPrecision).
IsExprBuilder sym =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymFloat sym fpp'
-> IO (SymFloat sym fpp)
W4.floatCast @_ @Prec64 @Prec32 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
W4.RNE)
, (Text
"fp_binary_to_double",
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym -> forall sym (eb :: Nat) (sb :: Nat).
(IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
sym
-> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> SymBV sym (eb + sb)
-> IO (SymFloat sym (FloatingPointPrecision eb sb))
W4.floatFromBinary @_ @11 @53 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr)
, (Text
"fp_binary_to_single",
forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym -> forall sym (eb :: Nat) (sb :: Nat).
(IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
sym
-> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> SymBV sym (eb + sb)
-> IO (SymFloat sym (FloatingPointPrecision eb sb))
W4.floatFromBinary @_ @8 @24 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr)
, (Text
"fp_double_to_binary", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (eb :: Nat) (sb :: Nat).
(IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
sym
-> SymFloat sym (FloatingPointPrecision eb sb)
-> IO (SymBV sym (eb + sb))
W4.floatToBinary @_ @11 @53)
, (Text
"fp_single_to_binary", forall (res :: BaseType) sym (arg2 :: BaseType).
Assignment BaseTypeRepr ('EmptyCtx ::> res)
-> (sym -> SymExpr sym res -> IO (SymExpr sym arg2)) -> Op sym
Op1 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (eb :: Nat) (sb :: Nat).
(IsExprBuilder sym, 2 <= eb, 2 <= sb) =>
sym
-> SymFloat sym (FloatingPointPrecision eb sb)
-> IO (SymBV sym (eb + sb))
W4.floatToBinary @_ @8 @24)
, (Text
"fctid", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
W4.floatToSBV @_ @64 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
, (Text
"fctidu", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
W4.floatToBV @_ @64 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
, (Text
"fctiw", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
W4.floatToSBV @_ @32 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
, (Text
"fctiwu", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
W4.floatToBV @_ @32 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
, (Text
"fcfid", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
W4.sbvToFloat @_ @64 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
, (Text
"fcfids", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
W4.sbvToFloat @_ @64 @Prec32 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
, (Text
"fcfidu", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
W4.bvToFloat @_ @64 @Prec64 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
, (Text
"fcfidus", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseBVType 64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (w :: Nat) (fpp :: FloatPrecision).
(IsExprBuilder sym, 1 <= w) =>
sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
W4.bvToFloat @_ @64 @Prec32 sym
sym forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr RoundingMode
rm SymExpr sym (BaseBVType 64)
x)
, (Text
"frti", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatRound @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x)
, (Text
"frtis", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> RoundingMode -> SymFloat sym fpp -> IO (SymFloat sym fpp)
W4.floatRound @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x)
, (Text
"fadd", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
(arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
-> SymExpr sym res
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatAdd @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y)
, (Text
"fadds", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
(arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
-> SymExpr sym res
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatAdd @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y)
, (Text
"fsub", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
(arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
-> SymExpr sym res
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatSub @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y)
, (Text
"fsubs", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
(arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
-> SymExpr sym res
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatSub @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y)
, (Text
"fmul", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
(arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
-> SymExpr sym res
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatMul @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y)
, (Text
"fmuls", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
(arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
-> SymExpr sym res
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatMul @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y)
, (Text
"fdiv", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
(arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
-> SymExpr sym res
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatDiv @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y)
, (Text
"fdivs", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType) sym
(arg4 :: BaseType).
Assignment BaseTypeRepr ((('EmptyCtx ::> res) ::> arg2) ::> arg3)
-> (sym
-> SymExpr sym res
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym arg4))
-> Op sym
Op3 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatDiv @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y)
, (Text
"fltd", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatLt @_ @Prec64)
, (Text
"flts", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatLt @_ @Prec32)
, (Text
"feqd", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatFpEq @_ @Prec64)
, (Text
"feqs", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatFpEq @_ @Prec32)
, (Text
"fled", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatLe @_ @Prec64)
, (Text
"fles", forall (res :: BaseType) (arg2 :: BaseType) sym (arg3 :: BaseType).
Assignment BaseTypeRepr (('EmptyCtx ::> res) ::> arg2)
-> (sym
-> SymExpr sym res -> SymExpr sym arg2 -> IO (SymExpr sym arg3))
-> Op sym
Op2 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> SymFloat sym fpp -> SymFloat sym fpp -> IO (Pred sym)
W4.floatLe @_ @Prec32)
, (Text
"ffma", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType)
(arg4 :: BaseType) sym (ret :: BaseType).
Assignment
BaseTypeRepr (((('EmptyCtx ::> res) ::> arg2) ::> arg3) ::> arg4)
-> (sym
-> SymExpr sym res
-> SymExpr sym arg2
-> SymExpr sym arg3
-> SymExpr sym arg4
-> IO (SymExpr sym ret))
-> Op sym
Op4 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y SymExpr sym (BaseFloatType Prec64)
z -> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm ->
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatFMA @_ @Prec64 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec64)
x SymExpr sym (BaseFloatType Prec64)
y SymExpr sym (BaseFloatType Prec64)
z)
, (Text
"ffmas", forall (res :: BaseType) (arg2 :: BaseType) (arg3 :: BaseType)
(arg4 :: BaseType) sym (ret :: BaseType).
Assignment
BaseTypeRepr (((('EmptyCtx ::> res) ::> arg2) ::> arg3) ::> arg4)
-> (sym
-> SymExpr sym res
-> SymExpr sym arg2
-> SymExpr sym arg3
-> SymExpr sym arg4
-> IO (SymExpr sym ret))
-> Op sym
Op4 forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall a b. (a -> b) -> a -> b
$ \sym
sym SymExpr sym (BaseBVType 2)
r SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y SymExpr sym (BaseFloatType Prec32)
z ->
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> SymBV sym 2
-> (RoundingMode -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
U.withRounding sym
sym SymExpr sym (BaseBVType 2)
r forall a b. (a -> b) -> a -> b
$ \RoundingMode
rm -> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
W4.floatFMA @_ @Prec32 sym
sym RoundingMode
rm SymExpr sym (BaseFloatType Prec32)
x SymExpr sym (BaseFloatType Prec32)
y SymExpr sym (BaseFloatType Prec32)
z)
]
readOneArg ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> [SExpr]
-> Processor sym (Some (W4.SymExpr sym))
readOneArg :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands = do
[Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
case [Some (Expr t)]
args of
[Some (Expr t)
arg] -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Some (Expr t)
arg
[Some (Expr t)]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"expecting 1 argument, got %d" (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some (Expr t)]
args)
readTwoArgs ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> [SExpr]
-> Processor sym (Some (W4.SymExpr sym), Some (W4.SymExpr sym))
readTwoArgs :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands = do
[Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
case [Some (Expr t)]
args of
[Some (Expr t)
arg1, Some (Expr t)
arg2] -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (Expr t)
arg1, Some (Expr t)
arg2)
[Some (Expr t)]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"expecting 2 arguments, got %d" (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some (Expr t)]
args)
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 :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr]
-> Processor
sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
readThreeArgs [SExpr]
operands = do
[Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
case [Some (Expr t)]
args of
[Some (Expr t)
arg1, Some (Expr t)
arg2, Some (Expr t)
arg3] -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (Expr t)
arg1, Some (Expr t)
arg2, Some (Expr t)
arg3)
[Some (Expr t)]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"expecting 3 arguments, got %d" (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some (Expr t)]
args)
readApp ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> SExpr
-> [SExpr]
-> Processor sym (Some (W4.SymExpr sym))
readApp :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> [SExpr] -> Processor sym (Some (SymExpr sym))
readApp (S.WFSAtom (AId Text
"call")) (S.WFSAtom (AId Text
fnName):[SExpr]
operands) = do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.asks forall sym. ProcessorEnv sym -> sym
procSym
Maybe (SomeSymFn sym)
maybeFn <- forall sym. Text -> Processor sym (Maybe (SomeSymFn sym))
lookupFn Text
fnName
case Maybe (SomeSymFn sym)
maybeFn of
Just (SomeSymFn SymFn sym dom ret
fn) -> do
[Some (Expr t)]
args <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr [SExpr]
operands
Assignment (Expr t) dom
assn <- forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment (forall (fn :: Ctx BaseType -> BaseType -> Type)
(args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
W4.fnArgTypes SymFn sym dom ret
fn) [Some (Expr t)]
args
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn ExprBuilder t st fs
sym SymFn sym dom ret
fn Assignment (Expr t) dom
assn)
Maybe (SomeSymFn sym)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"The function name `"
forall a. [a] -> [a] -> [a]
++(Text -> String
T.unpack Text
fnName)
forall a. [a] -> [a] -> [a]
++String
"` is not bound to a SymFn in the current Config."
readApp opRaw :: SExpr
opRaw@(S.WFSAtom (AId Text
"call")) [SExpr]
operands = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError
forall a b. (a -> b) -> a -> b
$ String
"Unrecognized use of `call`: " forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty (forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L (SExpr
opRawforall a. a -> [a] -> [a]
:[SExpr]
operands))))
readApp opRaw :: SExpr
opRaw@(S.WFSAtom (AId Text
operator)) [SExpr]
operands = do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError (String
"in reading expression:\n"
forall a. [a] -> [a] -> [a]
++(Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.WFSList (SExpr
opRawforall a. a -> [a] -> [a]
:[SExpr]
operands))forall a. [a] -> [a] -> [a]
++String
"\n") forall a b. (a -> b) -> a -> b
$
case forall sym. IsSymExprBuilder sym => Text -> Maybe (Op sym)
lookupOp @sym Text
operator of
Just (FloatOp1 forall (fpp :: FloatPrecision).
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
fn) -> do
[Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
case [Some (Expr t)]
args of
[Some Expr t x
a1]
| BaseFloatRepr FloatPrecisionRepr fpp
_ <- forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
a1 -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fpp :: FloatPrecision).
sym -> SymFloat sym fpp -> IO (SymFloat sym fpp)
fn ExprBuilder t st fs
sym Expr t x
a1)
[Some (Expr t)]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"Unable to unpack FloatOp1 arg in Formula.Parser readApp"
Just (Op1 Assignment BaseTypeRepr ('EmptyCtx ::> arg1)
arg_types sym -> SymExpr sym arg1 -> IO (SymExpr sym ret)
fn) -> do
[Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr ('EmptyCtx ::> arg1)
arg_types [Some (Expr t)]
args forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 ->
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymExpr sym arg1 -> IO (SymExpr sym ret)
fn ExprBuilder t st fs
sym Expr t tp
arg1)
Just (Op2 Assignment BaseTypeRepr (('EmptyCtx ::> arg1) ::> arg2)
arg_types sym -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret)
fn) -> do
[Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr (('EmptyCtx ::> arg1) ::> arg2)
arg_types [Some (Expr t)]
args forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 Ctx.:> Expr t tp
arg2 ->
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymExpr sym arg1 -> SymExpr sym arg2 -> IO (SymExpr sym ret)
fn ExprBuilder t st fs
sym Expr t tp
arg1 Expr t tp
arg2)
Just (Op3 Assignment BaseTypeRepr ((('EmptyCtx ::> arg1) ::> arg2) ::> arg3)
arg_types sym
-> SymExpr sym arg1
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym ret)
fn) -> do
[Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr ((('EmptyCtx ::> arg1) ::> arg2) ::> arg3)
arg_types [Some (Expr t)]
args forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 Ctx.:> Expr t tp
arg2 Ctx.:> Expr t tp
arg3 ->
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym arg1
-> SymExpr sym arg2
-> SymExpr sym arg3
-> IO (SymExpr sym ret)
fn ExprBuilder t st fs
sym Expr t tp
arg1 Expr t tp
arg2 Expr t tp
arg3)
Just (Op4 Assignment
BaseTypeRepr (((('EmptyCtx ::> arg1) ::> arg2) ::> arg3) ::> arg4)
arg_types sym
-> SymExpr sym arg1
-> SymExpr sym arg2
-> SymExpr sym arg3
-> SymExpr sym arg4
-> IO (SymExpr sym ret)
fn) -> do
[Some (Expr t)]
args <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
operands
forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment
BaseTypeRepr (((('EmptyCtx ::> arg1) ::> arg2) ::> arg3) ::> arg4)
arg_types [Some (Expr t)]
args forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Assignment (Expr t) ctx
Ctx.Empty Ctx.:> Expr t tp
arg1 Ctx.:> Expr t tp
arg2 Ctx.:> Expr t tp
arg3 Ctx.:> Expr t tp
arg4 ->
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym arg1
-> SymExpr sym arg2
-> SymExpr sym arg3
-> SymExpr sym arg4
-> IO (SymExpr sym ret)
fn ExprBuilder t st fs
sym Expr t tp
arg1 Expr t tp
arg2 Expr t tp
arg3 Expr t tp
arg4)
Just (BVOp1 forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
op) -> do
Some Expr t x
expr <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands
BVProof NatRepr n
_ <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
expr
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
op ExprBuilder t st fs
sym Expr t x
expr
Just (BVOp2 forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
op) -> do
(Some Expr t x
arg1, Some Expr t x
arg2) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands
BVProof NatRepr n
m <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 1: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg1
BVProof NatRepr n
n <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 2: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg2
case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr n
m NatRepr n
n of
Just n :~: n
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
op ExprBuilder t st fs
sym Expr t x
arg1 Expr t x
arg2)
Maybe (n :~: n)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"arguments to %s must be the same length, \
\but arg 1 has length %s \
\and arg 2 has length %s"
Text
operator
(forall a. Show a => a -> String
show NatRepr n
m)
(forall a. Show a => a -> String
show NatRepr n
n)
Just (BVComp2 forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
op) -> do
(Some Expr t x
arg1, Some Expr t x
arg2) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands
BVProof NatRepr n
m <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 1: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg1
BVProof NatRepr n
n <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 2: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg2
case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr n
m NatRepr n
n of
Just n :~: n
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
op ExprBuilder t st fs
sym Expr t x
arg1 Expr t x
arg2)
Maybe (n :~: n)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"arguments to %s must be the same length, \
\but arg 1 has length %s \
\and arg 2 has length %s"
Text
operator
(forall a. Show a => a -> String
show NatRepr n
m)
(forall a. Show a => a -> String
show NatRepr n
n)
Maybe (Op sym)
Nothing ->
case Text
operator of
Text
"concat" -> do
(Some Expr t x
arg1, Some Expr t x
arg2) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands
BVProof NatRepr n
_ <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 1: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg1
BVProof NatRepr n
_ <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in arg 2: " forall a b. (a -> b) -> a -> b
$ forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg2
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Nat) (v :: Nat).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
W4.bvConcat ExprBuilder t st fs
sym Expr t x
arg1 Expr t x
arg2)
Text
"=" -> do
(Some Expr t x
arg1, Some Expr t x
arg2) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands
case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg1) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg2) of
Just x :~: x
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
W4.isEq ExprBuilder t st fs
sym Expr t x
arg1 Expr t x
arg2)
Maybe (x :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
forall r. PrintfType r => String -> r
printf String
"arguments must have same types, \
\but arg 1 has type %s \
\and arg 2 has type %s"
(forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg1))
(forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg2))
Text
"ite" -> do
(Some Expr t x
test, Some Expr t x
then_, Some Expr t x
else_) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr]
-> Processor
sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
readThreeArgs [SExpr]
operands
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
test of
BaseTypeRepr x
BaseBoolRepr ->
case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
then_) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
else_) of
Just x :~: x
Refl -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
W4.baseTypeIte ExprBuilder t st fs
sym Expr t x
test Expr t x
then_ Expr t x
else_)
Maybe (x :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
forall r. PrintfType r => String -> r
printf String
"then and else branches must have same type, \
\but then has type %s \
\and else has type %s"
(forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
then_))
(forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
else_))
BaseTypeRepr x
tp -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"test expression must be a boolean; got %s" (forall a. Show a => a -> String
show BaseTypeRepr x
tp)
Text
"select" -> do
(Some Expr t x
arr, Some Expr t x
idx) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym), Some (SymExpr sym))
readTwoArgs [SExpr]
operands
ArraySingleDim BaseTypeRepr res
_ <- forall (m :: Type -> Type) (tp1 :: BaseType) (tp2 :: BaseType).
MonadError String m =>
BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
expectArrayWithIndex (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
idx) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arr)
let idx' :: Assignment (Expr t) (SingleCtx x)
idx' = forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> Expr t x
idx
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> IO (SymExpr sym b)
W4.arrayLookup ExprBuilder t st fs
sym Expr t x
arr Assignment (Expr t) (SingleCtx x)
idx')
Text
"store" -> do
(Some Expr t x
arr, Some Expr t x
idx, Some Expr t x
expr) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr]
-> Processor
sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
readThreeArgs [SExpr]
operands
ArraySingleDim BaseTypeRepr res
resRepr <- forall (m :: Type -> Type) (tp1 :: BaseType) (tp2 :: BaseType).
MonadError String m =>
BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
expectArrayWithIndex (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
idx) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arr)
case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BaseTypeRepr res
resRepr (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
expr) of
Just res :~: x
Refl ->
let idx' :: Assignment (Expr t) (SingleCtx x)
idx' = forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> Expr t x
idx
in forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
W4.arrayUpdate ExprBuilder t st fs
sym Expr t x
arr Assignment (Expr t) (SingleCtx x)
idx' Expr t x
expr)
Maybe (res :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"Array result type %s does not match %s"
(forall a. Show a => a -> String
show BaseTypeRepr res
resRepr)
(forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
expr))
Text
"updateArray" -> do
(Some Expr t x
arr, Some Expr t x
idx, Some Expr t x
expr) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr]
-> Processor
sym (Some (SymExpr sym), Some (SymExpr sym), Some (SymExpr sym))
readThreeArgs [SExpr]
operands
ArraySingleDim BaseTypeRepr res
resRepr <- forall (m :: Type -> Type) (tp1 :: BaseType) (tp2 :: BaseType).
MonadError String m =>
BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
expectArrayWithIndex (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
idx) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arr)
case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BaseTypeRepr res
resRepr (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
expr) of
Just res :~: x
Refl ->
let idx' :: Assignment (Expr t) (SingleCtx x)
idx' = forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> Expr t x
idx
in forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
W4.arrayUpdate ExprBuilder t st fs
sym Expr t x
arr Assignment (Expr t) (SingleCtx x)
idx' Expr t x
expr)
Maybe (res :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"Array result type %s does not match %s"
(forall a. Show a => a -> String
show BaseTypeRepr res
resRepr)
(forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
expr))
Text
"arrayMap" ->
case [SExpr]
operands of
[SExpr
updateSExprList, SExpr
arrSExpr] -> do
Some Expr t x
arrExpr <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
arrSExpr
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arrExpr of
BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idxReprs BaseTypeRepr xs
arrTyRepr -> do
ArrayUpdateMap (Expr t) (idx ::> tp) xs
updateMap <- forall sym t (st :: Type -> Type) fs (tp :: BaseType)
(i :: Ctx BaseType) (itp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
Assignment BaseTypeRepr (i ::> itp)
-> BaseTypeRepr tp
-> SExpr
-> Processor sym (ArrayUpdateMap (SymExpr sym) (i ::> itp) tp)
expectArrayUpdateMap Assignment BaseTypeRepr (idx ::> tp)
idxReprs BaseTypeRepr xs
arrTyRepr SExpr
updateSExprList
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
W4.sbMakeExpr ExprBuilder t st fs
sym (forall (i :: Ctx BaseType) (itp :: BaseType) (tp1 :: BaseType)
(e :: BaseType -> Type).
Assignment BaseTypeRepr (i ::> itp)
-> BaseTypeRepr tp1
-> ArrayUpdateMap e (i ::> itp) tp1
-> e (BaseArrayType (i ::> itp) tp1)
-> App e (BaseArrayType (i ::> itp) tp1)
W4.ArrayMap Assignment BaseTypeRepr (idx ::> tp)
idxReprs BaseTypeRepr xs
arrTyRepr ArrayUpdateMap (Expr t) (idx ::> tp) xs
updateMap Expr t x
arrExpr))
BaseTypeRepr x
repr -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected an array type for the value in 'arrayMap', but got", forall a. Show a => a -> String
show BaseTypeRepr x
repr]
[SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected a list of indices and an array expression, but got", forall a. Show a => a -> String
show [SExpr]
operands]
Text
"field" -> do
case [SExpr]
operands of
[SExpr
rawStruct, S.WFSAtom (AInt Integer
rawIdx)] -> do
Some Expr t x
struct <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
rawStruct
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
struct of
(BaseStructRepr Assignment BaseTypeRepr ctx
fldTpReprs) ->
case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
Ctx.intIndex (forall a. Num a => Integer -> a
fromInteger Integer
rawIdx) (forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment BaseTypeRepr ctx
fldTpReprs) of
Just (Some Index ctx x
i) -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField ExprBuilder t st fs
sym Expr t x
struct Index ctx x
i)
Maybe (Some (Index ctx))
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
[String] -> String
unwords [String
"invalid struct index, got", forall a. Show a => a -> String
show Assignment BaseTypeRepr ctx
fldTpReprs, String
"and", forall a. Show a => a -> String
show Integer
rawIdx]
BaseTypeRepr x
srepr -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected a struct, got", forall a. Show a => a -> String
show BaseTypeRepr x
srepr]
[SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected an arg and an Int, got", forall a. Show a => a -> String
show [SExpr]
operands]
Text
"struct" -> do
case [SExpr]
operands of
[S.WFSList [SExpr]
rawFldExprs] -> do
Some Assignment (Expr t) x
flds <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (Assignment (SymExpr sym)))
readExprsAsAssignment [SExpr]
rawFldExprs
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
W4.mkStruct ExprBuilder t st fs
sym Assignment (Expr t) x
flds)
[SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"struct expects a single operand, got", forall a. Show a => a -> String
show [SExpr]
operands]
Text
"sbvToInteger" -> do
(Some Expr t x
arg) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands
BVProof NatRepr n
_ <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
W4.sbvToInteger ExprBuilder t st fs
sym Expr t x
arg
Text
"bvToInteger" -> do
(Some Expr t x
arg) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
operands
BVProof NatRepr n
_ <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
W4.bvToInteger ExprBuilder t st fs
sym Expr t x
arg
Text
"integerToBV" -> do
case [SExpr]
operands of
[S.WFSAtom (ANat Nat
width), SExpr
rawValExpr] -> do
Some Expr t x
x <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
rawValExpr
case (Nat -> Some NatRepr
mkNatRepr Nat
width, forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
x) of
(Some NatRepr x
w, BaseTypeRepr x
BaseIntegerRepr)
| Just LeqProof 1 x
LeqProof <- forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w -> do
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
W4.integerToBV ExprBuilder t st fs
sym Expr t x
x NatRepr x
w)
(Some NatRepr, BaseTypeRepr x)
srepr -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected a non-zero natural and an integer, got", forall a. Show a => a -> String
show (Some NatRepr, BaseTypeRepr x)
srepr]
[SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"integerToBV expects two operands, the first of which is a nat, got", forall a. Show a => a -> String
show [SExpr]
operands]
Text
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"couldn't parse application of %s" (Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
opRaw)
readApp (S.WFSList [S.WFSAtom (AId Text
"_"), S.WFSAtom (AId Text
"extract"), S.WFSAtom (AInt Integer
iInt), S.WFSAtom (AInt Integer
jInt)])
[SExpr]
args = forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in reading extract expression: " forall a b. (a -> b) -> a -> b
$ do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
(Some Expr t x
arg) <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
args
let nInt :: Integer
nInt = Integer
iInt forall a. Num a => a -> a -> a
- Integer
jInt forall a. Num a => a -> a -> a
+ Integer
1
idxInt :: Integer
idxInt = Integer
jInt
Some NatRepr x
nNat <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in calculating extract length: " forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM Integer
nInt
Some NatRepr x
idxNat <- forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in extract lower bound: " forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM Integer
idxInt
LeqProof 1 x
LeqProof <- forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError String
"extract length must be positive" forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
nNat
BVProof NatRepr n
lenNat <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg
LeqProof (x + x) n
LeqProof <- forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError String
"invalid extract for given bitvector" forall a b. (a -> b) -> a -> b
$
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
idxNat NatRepr x
nNat) NatRepr n
lenNat
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (idx :: Nat) (n :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
W4.bvSelect ExprBuilder t st fs
sym NatRepr x
idxNat NatRepr x
nNat Expr t x
arg)
readApp (S.WFSList [S.WFSAtom (AId Text
"_"), S.WFSAtom (AId Text
extend), S.WFSAtom (AInt Integer
iInt)])
[SExpr]
args
| Text
extend forall a. Eq a => a -> a -> Bool
== Text
"zero_extend" Bool -> Bool -> Bool
||
Text
extend forall a. Eq a => a -> a -> Bool
== Text
"sign_extend" = forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError (forall r. PrintfType r => String -> r
printf String
"in reading %s expression: " Text
extend) forall a b. (a -> b) -> a -> b
$ do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
Some Expr t x
arg <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
args
Some NatRepr x
iNat <- forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM Integer
iInt
LeqProof 1 x
iPositive <- forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError String
"must extend by a positive length" forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
iNat
BVProof NatRepr n
lenNat <- forall (ex :: BaseType -> Type) (m :: Type -> Type)
(tp :: BaseType).
(IsExpr ex, MonadError String m) =>
ex tp -> m (BVProof tp)
getBVProof Expr t x
arg
let newLen :: NatRepr (n + x)
newLen = forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr n
lenNat NatRepr x
iNat
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 (forall (f :: Nat -> Type) (n :: Nat). f n -> LeqProof n n
leqRefl NatRepr n
lenNat) LeqProof 1 x
iPositive) forall a b. (a -> b) -> a -> b
$
let op :: ExprBuilder t st fs
-> NatRepr (n + x)
-> SymBV (ExprBuilder t st fs) n
-> IO (SymBV (ExprBuilder t st fs) (n + x))
op = if Text
extend forall a. Eq a => a -> a -> Bool
== Text
"zero_extend" then forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W4.bvZext else forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W4.bvSext
in forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprBuilder t st fs
-> NatRepr (n + x)
-> SymBV (ExprBuilder t st fs) n
-> IO (SymBV (ExprBuilder t st fs) (n + x))
op ExprBuilder t st fs
sym NatRepr (n + x)
newLen Expr t x
arg
readApp (S.WFSList [S.WFSAtom (AId Text
"_"), S.WFSAtom (AId Text
"bvfill"), S.WFSAtom (AInt Integer
width)]) [SExpr]
args =
forall e (m :: Type -> Type) a.
(Monoid e, MonadError e m) =>
e -> m a -> m a
prefixError String
"in reading bvfill expression" forall a b. (a -> b) -> a -> b
$ do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
Some Expr t x
arg <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (SymExpr sym))
readOneArg [SExpr]
args
case forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
arg of
BaseTypeRepr x
BaseBoolRepr -> do
Some NatRepr x
widthRep <- forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM Integer
width
LeqProof 1 x
LeqProof <- forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError String
"must extend by a positive length" forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
widthRep
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> Pred sym -> IO (SymBV sym w)
W4.bvFill ExprBuilder t st fs
sym NatRepr x
widthRep Expr t x
arg)
BaseTypeRepr x
tyrep -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Invalid argument type to bvFill: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BaseTypeRepr x
tyrep)
readApp SExpr
rator [SExpr]
rands = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"readApp could not parse the following: "
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack (Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.WFSList (SExpr
ratorforall a. a -> [a] -> [a]
:[SExpr]
rands))))
intToNatM :: (E.MonadError String m) => Integer -> m (Some NatRepr)
intToNatM :: forall (m :: Type -> Type).
MonadError String m =>
Integer -> m (Some NatRepr)
intToNatM = forall e (m :: Type -> Type) a.
MonadError e m =>
e -> Maybe a -> m a
fromMaybeError String
"integer must be non-negative to be a nat" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Maybe (Some NatRepr)
someNat
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 :: forall sym t (st :: Type -> Type) fs (tp :: BaseType)
(i :: Ctx BaseType) (itp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
Assignment BaseTypeRepr (i ::> itp)
-> BaseTypeRepr tp
-> SExpr
-> Processor sym (ArrayUpdateMap (SymExpr sym) (i ::> itp) tp)
expectArrayUpdateMap Assignment BaseTypeRepr (i ::> itp)
idxReprs BaseTypeRepr tp
arrTyRepr SExpr
updateSExprList =
case SExpr
updateSExprList of
S.L [SExpr]
items -> forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
F.foldrM SExpr
-> ArrayUpdateMap (Expr t) (i ::> itp) tp
-> ExceptT
String
(ReaderT (ProcessorEnv sym) IO)
(ArrayUpdateMap (Expr t) (i ::> itp) tp)
expectArrayUpdateEntry forall (e :: BaseType -> Type) (ctx :: Ctx BaseType)
(tp :: BaseType).
ArrayUpdateMap e ctx tp
WAU.empty [SExpr]
items
SExpr
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"Expected a list of array element updates in ArrayMap"
where
expectArrayUpdateEntry :: SExpr
-> ArrayUpdateMap (Expr t) (i ::> itp) tp
-> ExceptT
String
(ReaderT (ProcessorEnv sym) IO)
(ArrayUpdateMap (Expr t) (i ::> itp) tp)
expectArrayUpdateEntry SExpr
pair ArrayUpdateMap (Expr t) (i ::> itp) tp
updateMap =
case SExpr
pair of
S.L [S.L [SExpr]
idxListExprs, SExpr
elt] -> do
Assignment IndexLit (i ::> itp)
idxs <- forall {k} (m :: Type -> Type) (ctx :: Ctx k) (f :: k -> Type)
(g :: k -> Type).
Applicative m =>
(forall (tp :: k). Index ctx tp -> f tp -> m (g tp))
-> Assignment f ctx -> m (Assignment g ctx)
Ctx.traverseWithIndex (forall (ctx :: Ctx BaseType) (tp :: BaseType) sym.
[SExpr]
-> Index ctx tp -> BaseTypeRepr tp -> Processor sym (IndexLit tp)
parseIndexLit [SExpr]
idxListExprs) Assignment BaseTypeRepr (i ::> itp)
idxReprs
Some Expr t x
x <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
elt
case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BaseTypeRepr tp
arrTyRepr (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
x) of
Just tp :~: x
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (e :: BaseType -> Type) (tp :: BaseType)
(ctx :: Ctx BaseType).
(HashableF e, HasAbsValue e) =>
BaseTypeRepr tp
-> Assignment IndexLit ctx
-> e tp
-> ArrayUpdateMap e ctx tp
-> ArrayUpdateMap e ctx tp
WAU.insert BaseTypeRepr tp
arrTyRepr Assignment IndexLit (i ::> itp)
idxs Expr t x
x ArrayUpdateMap (Expr t) (i ::> itp) tp
updateMap)
Maybe (tp :~: x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat [ String
"Invalid element type in ArrayMap update: expected "
, forall a. Show a => a -> String
show BaseTypeRepr tp
arrTyRepr
, String
" but got "
, forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Expr t x
x)])
SExpr
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"Unexpected ArrayMap update item structure"
(!?) :: [a] -> Int -> Maybe a
[a]
lst !? :: forall a. [a] -> Int -> Maybe a
!? Int
idx
| Int
idx forall a. Ord a => a -> a -> Bool
< Int
0 = forall a. Maybe a
Nothing
| Bool
otherwise = forall {t} {a}. (Eq t, Num t) => t -> [a] -> Maybe a
go Int
idx [a]
lst
where
go :: t -> [a] -> Maybe a
go t
0 (a
x:[a]
_xs) = forall a. a -> Maybe a
Just a
x
go t
i (a
_:[a]
xs) = t -> [a] -> Maybe a
go (t
i forall a. Num a => a -> a -> a
- t
1) [a]
xs
go t
_ [] = forall a. Maybe a
Nothing
parseIndexLit :: [SExpr]
-> Ctx.Index ctx tp
-> BaseTypeRepr tp
-> Processor sym (WIL.IndexLit tp)
parseIndexLit :: forall (ctx :: Ctx BaseType) (tp :: BaseType) sym.
[SExpr]
-> Index ctx tp -> BaseTypeRepr tp -> Processor sym (IndexLit tp)
parseIndexLit [SExpr]
exprs Index ctx tp
idx BaseTypeRepr tp
repr
| Just (S.A Atom
atom) <- [SExpr]
exprs forall a. [a] -> Int -> Maybe a
!? forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index ctx tp
idx =
case (BaseTypeRepr tp
repr, Atom
atom) of
(BaseBVRepr NatRepr w
w, ABV Int
w' Integer
val)
| forall (n :: Nat). NatRepr n -> Integer
PN.intValue NatRepr w
w forall a. Eq a => a -> a -> Bool
== forall a. Integral a => a -> Integer
toInteger Int
w' ->
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> IndexLit ('BaseBVType w)
WIL.BVIndexLit NatRepr w
w (forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
val))
| Bool
otherwise -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Array update index bitvector size mismatch: expected " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show NatRepr w
w forall a. [a] -> [a] -> [a]
++ String
" but got " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
w')
(BaseTypeRepr tp
BaseIntegerRepr, AInt Integer
i) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer -> IndexLit 'BaseIntegerType
WIL.IntIndexLit Integer
i)
(BaseTypeRepr tp, Atom)
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Unexpected array update index type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BaseTypeRepr tp
repr)
| Bool
otherwise = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"Invalid or missing array update index at " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Index ctx tp
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 :: forall (m :: Type -> Type) (tp1 :: BaseType) (tp2 :: BaseType).
MonadError String m =>
BaseTypeRepr tp1 -> BaseTypeRepr tp2 -> m (ArrayJudgment tp1 tp2)
expectArrayWithIndex BaseTypeRepr tp1
dimRepr (BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp)
idxTpReprs BaseTypeRepr xs
resRepr) =
case forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign Assignment BaseTypeRepr (idx ::> tp)
idxTpReprs of
Ctx.AssignExtend Assignment BaseTypeRepr ctx1
rest BaseTypeRepr tp
idxTpRepr ->
case forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign Assignment BaseTypeRepr ctx1
rest of
AssignView BaseTypeRepr ctx1
Ctx.AssignEmpty ->
case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BaseTypeRepr tp
idxTpRepr BaseTypeRepr tp1
dimRepr of
Just tp :~: tp1
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (idx :: BaseType) (res :: BaseType).
BaseTypeRepr res
-> ArrayJudgment idx (BaseArrayType (SingleCtx idx) res)
ArraySingleDim BaseTypeRepr xs
resRepr
Maybe (tp :~: tp1)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Array index type", forall a. Show a => a -> String
show BaseTypeRepr tp
idxTpRepr,
String
"does not match", forall a. Show a => a -> String
show BaseTypeRepr tp1
dimRepr]
AssignView BaseTypeRepr ctx1
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"multidimensional arrays are not supported"
expectArrayWithIndex BaseTypeRepr tp1
_ BaseTypeRepr tp2
repr = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"expected an array, got", forall a. Show a => a -> String
show BaseTypeRepr tp2
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 :: forall sym (ctx :: Ctx BaseType) (ex :: BaseType -> Type).
(IsSymExprBuilder sym, ShowF (SymExpr sym), ShowF ex, IsExpr ex) =>
Assignment BaseTypeRepr ctx
-> [Some ex] -> Processor sym (Assignment ex ctx)
exprAssignment Assignment BaseTypeRepr ctx
tpAssns [Some ex]
exs = do
Some Assignment ex x
exsAsn <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList [Some ex]
exs
Assignment BaseTypeRepr x
exsRepr <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
FC.fmapFC forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Assignment ex x
exsAsn
case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Assignment BaseTypeRepr x
exsRepr Assignment BaseTypeRepr ctx
tpAssns of
Just x :~: ctx
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Assignment ex x
exsAsn
Maybe (x :~: ctx)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
String
"Unexpected expression types for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Assignment ex x
exsAsn
forall a. [a] -> [a] -> [a]
++ String
"\nExpected: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Assignment BaseTypeRepr ctx
tpAssns
forall a. [a] -> [a] -> [a]
++ String
"\nGot: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Assignment BaseTypeRepr x
exsRepr
readLetExpr ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> [SExpr]
-> SExpr
-> Processor sym (Some (W4.SymExpr sym))
readLetExpr :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetExpr [] SExpr
body = forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
body
readLetExpr ((S.WFSList [S.WFSAtom (AId Text
x), SExpr
e]):[SExpr]
rst) SExpr
body = do
Some (Expr t)
v <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
e
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
R.local (\ProcessorEnv (ExprBuilder t st fs)
c -> ProcessorEnv (ExprBuilder t st fs)
c {procLetEnv :: HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
procLetEnv = (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HM.insert Text
x Some (Expr t)
v) forall a b. (a -> b) -> a -> b
$ forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv ProcessorEnv (ExprBuilder t st fs)
c}) forall a b. (a -> b) -> a -> b
$
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetExpr [SExpr]
rst SExpr
body
readLetExpr [SExpr]
bindings SExpr
_body = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
String
"invalid s-expression for let-bindings: " forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show [SExpr]
bindings)
readLetFnExpr ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> [SExpr]
-> SExpr
-> Processor sym (Some (W4.SymExpr sym))
readLetFnExpr :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetFnExpr [] SExpr
body = forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
body
readLetFnExpr ((S.WFSList [S.WFSAtom (AId Text
f), SExpr
e]):[SExpr]
rst) SExpr
body = do
SomeSymFn sym
v <- forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (SomeSymFn sym)
readSymFn SExpr
e
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
R.local (\ProcessorEnv sym
c -> ProcessorEnv sym
c {procLetFnEnv :: HashMap Text (SomeSymFn sym)
procLetFnEnv = (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HM.insert Text
f SomeSymFn sym
v) forall a b. (a -> b) -> a -> b
$ forall sym. ProcessorEnv sym -> HashMap Text (SomeSymFn sym)
procLetFnEnv ProcessorEnv sym
c}) forall a b. (a -> b) -> a -> b
$
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetExpr [SExpr]
rst SExpr
body
readLetFnExpr [SExpr]
bindings SExpr
_body = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$
String
"invalid s-expression for let-bindings: " forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show [SExpr]
bindings)
readExpr ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> SExpr
-> Processor sym (Some (W4.SymExpr sym))
readExpr :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr (S.WFSAtom (AInt Integer
n)) = do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit ExprBuilder t st fs
sym Integer
n)
readExpr (S.WFSAtom (ANat Nat
_)) =
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"Bare Natural literals are no longer used"
readExpr (S.WFSAtom (ABool Bool
b)) = do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
W4.backendPred ExprBuilder t st fs
sym Bool
b
readExpr (S.WFSAtom (AFloat (Some FloatPrecisionRepr x
repr) BigFloat
bf)) = do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
W4.floatLit ExprBuilder t st fs
sym FloatPrecisionRepr x
repr BigFloat
bf)
readExpr (S.WFSAtom (AStr Some StringInfoRepr
prefix Text
content)) = do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
case Some StringInfoRepr
prefix of
(Some StringInfoRepr x
W4.UnicodeRepr) -> do
Expr t (BaseStringType 'Unicode)
s <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
W4.stringLit ExprBuilder t st fs
sym forall a b. (a -> b) -> a -> b
$ Text -> StringLiteral 'Unicode
W4.UnicodeLiteral Text
content
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ Expr t (BaseStringType 'Unicode)
s
(Some StringInfoRepr x
W4.Char8Repr) -> do
Expr t (BaseStringType 'Char8)
s <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
W4.stringLit ExprBuilder t st fs
sym forall a b. (a -> b) -> a -> b
$ ByteString -> StringLiteral 'Char8
W4.Char8Literal forall a b. (a -> b) -> a -> b
$ Text -> ByteString
T.encodeUtf8 Text
content
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall a b. (a -> b) -> a -> b
$ Expr t (BaseStringType 'Char8)
s
(Some StringInfoRepr x
W4.Char16Repr) -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"Char16 strings are not yet supported"
readExpr (S.WFSAtom (AReal Rational
_)) = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"TODO: support readExpr for real literals"
readExpr (S.WFSAtom (ABV Int
len Integer
val)) = do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
case forall a. Integral a => a -> Maybe (Some NatRepr)
someNat (forall a. Integral a => a -> Integer
toInteger Int
len) of
Just (Some NatRepr x
lenRepr) -> do
LeqProof 1 x
pf <- case forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
lenRepr of
Just LeqProof 1 x
pf -> forall (m :: Type -> Type) a. Monad m => a -> m a
return LeqProof 1 x
pf
Maybe (LeqProof 1 x)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"What4.Serialize.Parser.readExpr isPosNat failure"
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof LeqProof 1 x
pf (forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit ExprBuilder t st fs
sym NatRepr x
lenRepr (forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
lenRepr Integer
val))
Maybe (Some NatRepr)
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"SemMC.Formula.Parser.readExpr someNat failure"
readExpr (S.WFSAtom (AId Text
name)) = do
Maybe (Some (Expr t))
maybeBinding <- forall sym. Text -> Processor sym (Maybe (Some (SymExpr sym)))
lookupExpr Text
name
case Maybe (Some (Expr t))
maybeBinding of
Just Some (Expr t)
binding -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Some (Expr t)
binding
Maybe (Some (Expr t))
Nothing -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"Unbound variable encountered during deserialization: "
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
name))
readExpr (S.WFSList ((S.WFSAtom (AId Text
"let")):[SExpr]
rhs)) =
case [SExpr]
rhs of
[S.WFSList [SExpr]
bindings, SExpr
body] -> forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetExpr [SExpr]
bindings SExpr
body
[SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"ill-formed let s-expression"
readExpr (S.WFSList ((S.WFSAtom (AId Text
"letfn")):[SExpr]
rhs)) =
case [SExpr]
rhs of
[S.WFSList [SExpr]
bindings, SExpr
body] -> forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> SExpr -> Processor sym (Some (SymExpr sym))
readLetFnExpr [SExpr]
bindings SExpr
body
[SExpr]
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"ill-formed letfn s-expression"
readExpr (S.WFSList []) = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError String
"ill-formed empty s-expression"
readExpr (S.WFSList (SExpr
operator:[SExpr]
operands)) = forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> [SExpr] -> Processor sym (Some (SymExpr sym))
readApp SExpr
operator [SExpr]
operands
readExprs ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> [SExpr]
-> Processor sym [Some (W4.SymExpr sym)]
readExprs :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
exprs = forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr [SExpr]
exprs
readExprsAsAssignment ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> [SExpr]
-> Processor sym (Some (Ctx.Assignment (W4.SymExpr sym)))
readExprsAsAssignment :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym (Some (Assignment (SymExpr sym)))
readExprsAsAssignment [SExpr]
exprs = forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
[SExpr] -> Processor sym [Some (SymExpr sym)]
readExprs [SExpr]
exprs
readFnType ::
forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
=> SExpr
-> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
readFnType :: forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
SExpr -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
readFnType (S.WFSList ((S.WFSAtom (AId Text
"->")):[SExpr]
typeSExprs)) =
case forall a. [a] -> Maybe ([a], a)
unsnoc [SExpr]
typeSExprs of
Maybe ([SExpr], SExpr)
Nothing ->
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"invalid type signature for function: "
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty (forall t. [WellFormedSExpr t] -> WellFormedSExpr t
S.L [SExpr]
typeSExprs)))
Just ([SExpr]
domSExps, SExpr
retSExp) -> do
[Some BaseTypeRepr]
dom <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType [SExpr]
domSExps
Some BaseTypeRepr
ret <- forall (m :: Type -> Type).
MonadError String m =>
SExpr -> m (Some BaseTypeRepr)
readBaseType SExpr
retSExp
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([Some BaseTypeRepr]
dom, Some BaseTypeRepr
ret)
readFnType SExpr
sexpr =
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"invalid type signature for function: "
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
sexpr))
unsnoc :: [a] -> Maybe ([a], a)
unsnoc :: forall a. [a] -> Maybe ([a], a)
unsnoc [] = forall a. Maybe a
Nothing
unsnoc (a
x:[a]
xs) = case forall a. [a] -> Maybe ([a], a)
unsnoc [a]
xs of
Maybe ([a], a)
Nothing -> forall a. a -> Maybe a
Just ([], a
x)
Just ([a]
a,a
b) -> forall a. a -> Maybe a
Just (a
xforall a. a -> [a] -> [a]
:[a]
a, a
b)
readFnArgs ::
forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
=> [SExpr]
-> Processor sym [Text]
readFnArgs :: forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
[SExpr] -> Processor sym [Text]
readFnArgs [] = forall (m :: Type -> Type) a. Monad m => a -> m a
return []
readFnArgs ((S.WFSAtom (AId Text
name)):[SExpr]
rest) = do
[Text]
names <- (forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
[SExpr] -> Processor sym [Text]
readFnArgs [SExpr]
rest)
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Text
nameforall a. a -> [a] -> [a]
:[Text]
names
readFnArgs (SExpr
badArg:[SExpr]
_) =
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"invalid function argument encountered: "
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
badArg))
someVarExpr ::
forall sym . (W4.IsSymExprBuilder sym, ShowF (W4.SymExpr sym))
=> sym
-> Some (W4.BoundVar sym)
-> Some (W4.SymExpr sym)
someVarExpr :: forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
sym -> Some (BoundVar sym) -> Some (SymExpr sym)
someVarExpr sym
sym (Some BoundVar sym x
bv) = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
W4.varExpr sym
sym BoundVar sym x
bv)
readSymFn ::
forall sym t st fs . (sym ~ W4.ExprBuilder t st fs)
=> SExpr
-> Processor sym (SomeSymFn sym)
readSymFn :: forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (SomeSymFn sym)
readSymFn (S.WFSList [ S.WFSAtom (AId Text
"definedfn")
, S.WFSAtom (AStr Some StringInfoRepr
_ Text
rawSymFnName)
, SExpr
rawFnType
, S.WFSList [SExpr]
argVarsRaw
, SExpr
bodyRaw
]) = do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
SolverSymbol
symFnName <- case String -> Either SolverSymbolError SolverSymbol
W4.userSymbol (Text -> String
T.unpack Text
rawSymFnName) of
Left SolverSymbolError
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"Bad symbolic function name : "
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
rawSymFnName))
Right SolverSymbol
solverSym -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SolverSymbol
solverSym
[Text]
argNames <- forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
[SExpr] -> Processor sym [Text]
readFnArgs [SExpr]
argVarsRaw
([Some BaseTypeRepr]
argTys, Some BaseTypeRepr
_retTy) <- forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
SExpr -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
readFnType SExpr
rawFnType
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some BaseTypeRepr]
argTys forall a. Eq a => a -> a -> Bool
== forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Text]
argNames)) forall a b. (a -> b) -> a -> b
$
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"Function type expected "
forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Some BaseTypeRepr]
argTys)
forall a. [a] -> [a] -> [a]
++ String
" args but found "
forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Text]
argNames)
[Some (BoundVar (ExprBuilder t st fs))]
argVars <- forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Text
name, (Some BaseTypeRepr x
ty)) ->
case String -> Either SolverSymbolError SolverSymbol
W4.userSymbol (Text -> String
T.unpack Text
name) of
Left SolverSymbolError
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ String
"Bad arg name : " forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
name)
Right SolverSymbol
solverSym -> forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (x :: k). f x -> Some f
Some forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
W4.freshBoundVar ExprBuilder t st fs
sym SolverSymbol
solverSym BaseTypeRepr x
ty)
forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
argNames [Some BaseTypeRepr]
argTys
(Some Expr t x
body) <- let newBindings :: HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
newBindings = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HM.fromList
forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
argNames
forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
sym -> Some (BoundVar sym) -> Some (SymExpr sym)
someVarExpr ExprBuilder t st fs
sym) [Some (BoundVar (ExprBuilder t st fs))]
argVars
in forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
R.local
(\ProcessorEnv (ExprBuilder t st fs)
env -> ProcessorEnv (ExprBuilder t st fs)
env {procLetEnv :: HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
procLetEnv = forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HM.union (forall sym. ProcessorEnv sym -> HashMap Text (Some (SymExpr sym))
procLetEnv ProcessorEnv (ExprBuilder t st fs)
env) HashMap Text (Some (SymExpr (ExprBuilder t st fs)))
newBindings})
forall a b. (a -> b) -> a -> b
$ forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
SExpr -> Processor sym (Some (SymExpr sym))
readExpr SExpr
bodyRaw
Some Assignment (ExprBoundVar t) x
argVarAssignment <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList [Some (BoundVar (ExprBuilder t st fs))]
argVars
ExprSymFn t x x
symFn <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment (BoundVar sym) args
-> SymExpr sym ret
-> UnfoldPolicy
-> IO (SymFn sym args ret)
W4.definedFn ExprBuilder t st fs
sym SolverSymbol
symFnName Assignment (ExprBoundVar t) x
argVarAssignment Expr t x
body UnfoldPolicy
W4.UnfoldConcrete
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t (dom :: Ctx BaseType) (ret :: BaseType).
SymFn t dom ret -> SomeSymFn t
SomeSymFn ExprSymFn t x x
symFn
readSymFn badSExp :: SExpr
badSExp@(S.WFSList ((S.WFSAtom (AId Text
"definedfn")):[SExpr]
_)) =
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"invalid `definedfn`: " forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
badSExp))
readSymFn (S.WFSList [ S.WFSAtom (AId Text
"uninterpfn")
, S.WFSAtom (AStr Some StringInfoRepr
_ Text
rawSymFnName)
, SExpr
rawFnType
]) = do
ExprBuilder t st fs
sym <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
R.reader forall sym. ProcessorEnv sym -> sym
procSym
SolverSymbol
symFnName <- case String -> Either SolverSymbolError SolverSymbol
W4.userSymbol (Text -> String
T.unpack Text
rawSymFnName) of
Left SolverSymbolError
_ -> forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"Bad symbolic function name : "
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack Text
rawSymFnName))
Right SolverSymbol
solverSym -> forall (m :: Type -> Type) a. Monad m => a -> m a
return SolverSymbol
solverSym
([Some BaseTypeRepr]
argTys, (Some BaseTypeRepr x
retTy)) <- forall sym.
(IsSymExprBuilder sym, ShowF (SymExpr sym)) =>
SExpr -> Processor sym ([Some BaseTypeRepr], Some BaseTypeRepr)
readFnType SExpr
rawFnType
Some Assignment BaseTypeRepr x
domain <- forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> Type). [Some f] -> Some (Assignment f)
Ctx.fromList [Some BaseTypeRepr]
argTys
ExprSymFn t x x
symFn <- forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
W4.freshTotalUninterpFn ExprBuilder t st fs
sym SolverSymbol
symFnName Assignment BaseTypeRepr x
domain BaseTypeRepr x
retTy
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t (dom :: Ctx BaseType) (ret :: BaseType).
SymFn t dom ret -> SomeSymFn t
SomeSymFn ExprSymFn t x x
symFn
readSymFn badSExp :: SExpr
badSExp@(S.WFSList ((S.WFSAtom (AId Text
"uninterpfn")):[SExpr]
_)) =
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError forall a b. (a -> b) -> a -> b
$ (String
"invalid `uninterpfn`: " forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
badSExp))
readSymFn SExpr
sexpr = forall e (m :: Type -> Type) a. MonadError e m => e -> m a
E.throwError (String
"invalid function definition: "
forall a. [a] -> [a] -> [a]
++ (Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Seq String -> SExpr -> Text
printSExpr forall a. Monoid a => a
mempty SExpr
sexpr))