{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.Eval.What4
( Value
, primTable
) where
import qualified Control.Exception as X
import Control.Concurrent.MVar
import Control.Monad (foldM)
import Control.Monad.IO.Class
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Parameterized.Context
import Data.Parameterized.TraversableFC
import Data.Parameterized.Some
import qualified Data.BitVector.Sized as BV
import qualified What4.Interface as W4
import qualified What4.SWord as SW
import qualified What4.Utils.AbstractDomains as W4
import Cryptol.Backend
import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) )
import Cryptol.Backend.SeqMap
import Cryptol.Backend.WordValue
import Cryptol.Backend.What4
import Cryptol.Eval.Generic
import Cryptol.Eval.Prims
import Cryptol.Eval.Type (TValue(..))
import Cryptol.Eval.Value
import qualified Cryptol.SHA as SHA
import Cryptol.TypeCheck.Solver.InfNat( Nat'(..) )
import Cryptol.Utils.Ident
import Cryptol.Utils.Panic
import Cryptol.Utils.RecordMap
type Value sym = GenValue (What4 sym)
primTable :: W4.IsSymExprBuilder sym => What4 sym -> IO EvalOpts -> Map.Map PrimIdent (Prim (What4 sym))
primTable :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> IO EvalOpts -> Map PrimIdent (Prim (What4 sym))
primTable What4 sym
sym IO EvalOpts
getEOpts =
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall sym.
IsSymExprBuilder sym =>
What4 sym -> Map PrimIdent (Prim (What4 sym))
suiteBPrims What4 sym
sym) forall a b. (a -> b) -> a -> b
$
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall sym.
IsSymExprBuilder sym =>
What4 sym -> Map PrimIdent (Prim (What4 sym))
primeECPrims What4 sym
sym) forall a b. (a -> b) -> a -> b
$
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall sym. Backend sym => sym -> Map PrimIdent (Prim sym)
genericFloatTable What4 sym
sym) forall a b. (a -> b) -> a -> b
$
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall sym.
Backend sym =>
sym -> IO EvalOpts -> Map PrimIdent (Prim sym)
genericPrimTable What4 sym
sym IO EvalOpts
getEOpts) forall a b. (a -> b) -> a -> b
$
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Text
n, Prim (What4 sym)
v) -> (Text -> PrimIdent
prelPrim Text
n, Prim (What4 sym)
v))
[
(Text
"@" , forall sym.
Backend sym =>
sym
-> IndexDirection
-> (Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> TValue
-> SInteger sym
-> SEval sym (GenValue sym))
-> (Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> TValue
-> Integer
-> [IndexSegment sym]
-> SEval sym (GenValue sym))
-> Prim sym
indexPrim What4 sym
sym IndexDirection
IndexForward (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> SInteger (What4 sym)
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_int What4 sym
sym) (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> Integer
-> [IndexSegment (What4 sym)]
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_segs What4 sym
sym))
, (Text
"!" , forall sym.
Backend sym =>
sym
-> IndexDirection
-> (Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> TValue
-> SInteger sym
-> SEval sym (GenValue sym))
-> (Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> TValue
-> Integer
-> [IndexSegment sym]
-> SEval sym (GenValue sym))
-> Prim sym
indexPrim What4 sym
sym IndexDirection
IndexBackward (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> SInteger (What4 sym)
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_int What4 sym
sym) (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> Integer
-> [IndexSegment (What4 sym)]
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_segs What4 sym
sym))
, (Text
"update" , forall sym.
Backend sym =>
sym
-> (Nat'
-> TValue
-> WordValue sym
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (WordValue sym))
-> (Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym)))
-> Prim sym
updatePrim What4 sym
sym (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> WordValue (What4 sym)
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (WordValue (What4 sym))
updateFrontSym_word What4 sym
sym) (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateFrontSym What4 sym
sym))
, (Text
"updateEnd" , forall sym.
Backend sym =>
sym
-> (Nat'
-> TValue
-> WordValue sym
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (WordValue sym))
-> (Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> Either (SInteger sym) (WordValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym)))
-> Prim sym
updatePrim What4 sym
sym (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> WordValue (What4 sym)
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (WordValue (What4 sym))
updateBackSym_word What4 sym
sym) (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateBackSym What4 sym
sym))
]
primeECPrims :: W4.IsSymExprBuilder sym => What4 sym -> Map.Map PrimIdent (Prim (What4 sym))
primeECPrims :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> Map PrimIdent (Prim (What4 sym))
primeECPrims What4 sym
sym = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [ (Text -> PrimIdent
primeECPrim Text
n, Prim (What4 sym)
v) | (Text
n,Prim (What4 sym)
v) <- [(Text, Prim (What4 sym))]
prims ]
where
~> :: a -> b -> (a, b)
(~>) = (,)
prims :: [(Text, Prim (What4 sym))]
prims =
[
Text
"ec_double" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
s ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SymExpr sym BaseIntegerType
p' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
p
SymExpr sym ProjectivePoint
s' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
s
forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"Prime ECC"
SymFn
sym
((EmptyCtx ::> BaseIntegerType) ::> ProjectivePoint)
ProjectivePoint
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"ec_double"
(forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr) BaseTypeRepr ProjectivePoint
projectivePointRepr
SymExpr sym ProjectivePoint
z <- forall (m :: * -> *) 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
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
sym
((EmptyCtx ::> BaseIntegerType) ::> ProjectivePoint)
ProjectivePoint
fn (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
p' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
s')
forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint What4 sym
sym SymExpr sym ProjectivePoint
z
, Text
"ec_add_nonzero" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
s ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
t ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SymExpr sym BaseIntegerType
p' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
p
SymExpr sym ProjectivePoint
s' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
s
SymExpr sym ProjectivePoint
t' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
t
forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"Prime ECC"
SymFn
sym
(((EmptyCtx ::> BaseIntegerType) ::> ProjectivePoint)
::> ProjectivePoint)
ProjectivePoint
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"ec_add_nonzero"
(forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr) BaseTypeRepr ProjectivePoint
projectivePointRepr
SymExpr sym ProjectivePoint
z <- forall (m :: * -> *) 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
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
sym
(((EmptyCtx ::> BaseIntegerType) ::> ProjectivePoint)
::> ProjectivePoint)
ProjectivePoint
fn (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
p' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
s' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
t')
forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint What4 sym
sym SymExpr sym ProjectivePoint
z
, Text
"ec_mult" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
k ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
s ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SymExpr sym BaseIntegerType
p' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
p
SymExpr sym BaseIntegerType
k' <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
k
SymExpr sym ProjectivePoint
s' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
s
forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"Prime ECC"
SymFn
sym
(((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
::> ProjectivePoint)
ProjectivePoint
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"ec_mult"
(forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr) BaseTypeRepr ProjectivePoint
projectivePointRepr
SymExpr sym ProjectivePoint
z <- forall (m :: * -> *) 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
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
sym
(((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
::> ProjectivePoint)
ProjectivePoint
fn (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
p' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
k' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
s')
forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint What4 sym
sym SymExpr sym ProjectivePoint
z
, Text
"ec_twin_mult" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
j ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
s ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
k ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
t ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SymExpr sym BaseIntegerType
p' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
p
SymExpr sym BaseIntegerType
j' <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
j
SymExpr sym ProjectivePoint
s' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
s
SymExpr sym BaseIntegerType
k' <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
k
SymExpr sym ProjectivePoint
t' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
t
forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"Prime ECC"
SymFn
sym
(((((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
::> ProjectivePoint)
::> BaseIntegerType)
::> ProjectivePoint)
ProjectivePoint
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"ec_twin_mult"
(forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr)
BaseTypeRepr ProjectivePoint
projectivePointRepr
SymExpr sym ProjectivePoint
z <- forall (m :: * -> *) 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
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
sym
(((((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
::> ProjectivePoint)
::> BaseIntegerType)
::> ProjectivePoint)
ProjectivePoint
fn (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
p' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
j' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
s' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
k' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
t')
forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint What4 sym
sym SymExpr sym ProjectivePoint
z
]
type ProjectivePoint = W4.BaseStructType (EmptyCtx ::> W4.BaseIntegerType ::> W4.BaseIntegerType ::> W4.BaseIntegerType)
projectivePointRepr :: W4.BaseTypeRepr ProjectivePoint
projectivePointRepr :: BaseTypeRepr ProjectivePoint
projectivePointRepr = forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
W4.knownRepr
toProjectivePoint :: W4.IsSymExprBuilder sym =>
What4 sym -> Value sym -> SEval (What4 sym) (W4.SymExpr sym ProjectivePoint)
toProjectivePoint :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym Value sym
v =
do SymExpr sym BaseIntegerType
x <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
"x" Value sym
v
SymExpr sym BaseIntegerType
y <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
"y" Value sym
v
SymExpr sym BaseIntegerType
z <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
"z" Value sym
v
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
W4.mkStruct (forall sym. What4 sym -> sym
w4 What4 sym
sym) (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
x forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
y forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
z)
fromProjectivePoint :: W4.IsSymExprBuilder sym =>
What4 sym -> W4.SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint What4 sym
sym SymExpr sym ProjectivePoint
p = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
do Value sym
x <- forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) 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 (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym ProjectivePoint
p (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @0)
Value sym
y <- forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) 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 (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym ProjectivePoint
p (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @1)
Value sym
z <- forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) 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 (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym ProjectivePoint
p (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @2)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord forall a b. (a -> b) -> a -> b
$ forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields [ (String -> Ident
packIdent String
"x",forall (f :: * -> *) a. Applicative f => a -> f a
pure Value sym
x), (String -> Ident
packIdent String
"y",forall (f :: * -> *) a. Applicative f => a -> f a
pure Value sym
y),(String -> Ident
packIdent String
"z",forall (f :: * -> *) a. Applicative f => a -> f a
pure Value sym
z) ]
suiteBPrims :: W4.IsSymExprBuilder sym => What4 sym -> Map.Map PrimIdent (Prim (What4 sym))
suiteBPrims :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> Map PrimIdent (Prim (What4 sym))
suiteBPrims What4 sym
sym = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [ (Text -> PrimIdent
suiteBPrim Text
n, Prim (What4 sym)
v) | (Text
n,Prim (What4 sym)
v) <- [(Text, Prim (What4 sym))]
prims ]
where
~> :: a -> b -> (a, b)
(~>) = (,)
prims :: [(Text, Prim (What4 sym))]
prims =
[ Text
"AESEncRound" forall a b. a -> b -> (a, b)
~>
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES encryption"
forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
"AESEncRound" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
st
, Text
"AESEncFinalRound" forall a b. a -> b -> (a, b)
~>
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES encryption"
forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
"AESEncFinalRound" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
st
, Text
"AESDecRound" forall a b. a -> b -> (a, b)
~>
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES decryption"
forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
"AESDecRound" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
st
, Text
"AESDecFinalRound" forall a b. a -> b -> (a, b)
~>
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES decryption"
forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
"AESDecFinalRound" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
st
, Text
"AESInvMixColumns" forall a b. a -> b -> (a, b)
~>
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES key expansion"
forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
"AESInvMixColumns" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
st
, Text
"AESKeyExpand" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
k ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do SeqMap (What4 sym) (GenValue (What4 sym))
ss <- forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
st
Some Assignment (SymExpr sym) x
ws <- forall {k} (m :: * -> *) (f :: k -> *).
Applicative m =>
Int -> (Int -> m (Some f)) -> m (Some (Assignment f))
generateSomeM (forall a. Num a => Integer -> a
fromInteger Integer
k) (\Int
i -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"AESKeyExpand" SeqMap (What4 sym) (GenValue (What4 sym))
ss (forall a. Integral a => a -> Integer
toInteger Int
i))
let args :: Assignment BaseTypeRepr x
args = forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Assignment (SymExpr sym) x
ws
Some Assignment BaseTypeRepr x
ret <- forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> *).
Int -> (Int -> Some f) -> Some (Assignment f)
generateSome (Int
4forall a. Num a => a -> a -> a
*(forall a. Num a => Integer -> a
fromInteger Integer
k forall a. Num a => a -> a -> a
+ Int
7)) (\Int
_ -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32)))
forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES key expansion"
SymFn sym x ('BaseStructType x)
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym (Text
"AESKeyExpand" forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (forall a. Show a => a -> String
show Integer
k)) Assignment BaseTypeRepr x
args (forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr ('BaseStructType ctx)
W4.BaseStructRepr Assignment BaseTypeRepr x
ret)
SymExpr sym ('BaseStructType x)
z <- forall (m :: * -> *) 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
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn sym x ('BaseStructType x)
fn Assignment (SymExpr sym) x
ws
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq (Integer
4forall a. Num a => a -> a -> a
*(Integer
kforall a. Num a => a -> a -> a
+Integer
7)) forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex (forall a. Num a => Integer -> a
fromInteger Integer
i) (forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment BaseTypeRepr x
ret) of
Just (Some Index x x
idx) | Just x :~: BaseBVType 32
W4.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (Assignment BaseTypeRepr x
retforall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
!Index x x
idx) (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32)) ->
forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym ('BaseStructType x)
z Index x x
idx)
Maybe (Some (Index x))
_ -> forall a. String -> [String] -> a
evalPanic String
"AESKeyExpand" [String
"Index out of range", forall a. Show a => a -> String
show Integer
k, forall a. Show a => a -> String
show Integer
i]
, Text
"processSHA2_224" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
xs ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do [W4Eval sym (GenValue (What4 sym))]
blks <- forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
xs
forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"SHA-224"
SymExpr sym (BaseStructType SHA256State)
initSt <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA256State -> IO (SymExpr sym (BaseStructType SHA256State))
mkSHA256InitialState What4 sym
sym SHA256State
SHA.initialSHA224State)
SymExpr sym (BaseStructType SHA256State)
finalSt <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SymExpr sym (BaseStructType SHA256State)
st W4Eval sym (GenValue (What4 sym))
blk -> forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA256State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA256State))
processSHA256Block What4 sym
sym SymExpr sym (BaseStructType SHA256State)
st forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< W4Eval sym (GenValue (What4 sym))
blk) SymExpr sym (BaseStructType SHA256State)
initSt [W4Eval sym (GenValue (What4 sym))]
blks
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
7 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
i ->
case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex (forall a. Num a => Integer -> a
fromInteger Integer
i) (forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize :: Size SHA256State) of
Just (Some Index SHA256State x
idx) ->
do SymExpr sym x
z <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym (BaseStructType SHA256State)
finalSt Index SHA256State x
idx
case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym x
z) (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32)) of
Just x :~: BaseBVType 32
W4.Refl -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 SymExpr sym x
z
Maybe (x :~: BaseBVType 32)
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_224" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
Maybe (Some (Index SHA256State))
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_224" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
, Text
"processSHA2_256" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
xs ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do [W4Eval sym (GenValue (What4 sym))]
blks <- forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
xs
forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"SHA-256"
SymExpr sym (BaseStructType SHA256State)
initSt <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA256State -> IO (SymExpr sym (BaseStructType SHA256State))
mkSHA256InitialState What4 sym
sym SHA256State
SHA.initialSHA256State)
SymExpr sym (BaseStructType SHA256State)
finalSt <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SymExpr sym (BaseStructType SHA256State)
st W4Eval sym (GenValue (What4 sym))
blk -> forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA256State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA256State))
processSHA256Block What4 sym
sym SymExpr sym (BaseStructType SHA256State)
st forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< W4Eval sym (GenValue (What4 sym))
blk) SymExpr sym (BaseStructType SHA256State)
initSt [W4Eval sym (GenValue (What4 sym))]
blks
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
8 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
i ->
case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex (forall a. Num a => Integer -> a
fromInteger Integer
i) (forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize :: Size SHA256State) of
Just (Some Index SHA256State x
idx) ->
do SymExpr sym x
z <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym (BaseStructType SHA256State)
finalSt Index SHA256State x
idx
case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym x
z) (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32)) of
Just x :~: BaseBVType 32
W4.Refl -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 SymExpr sym x
z
Maybe (x :~: BaseBVType 32)
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_256" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
Maybe (Some (Index SHA256State))
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_256" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
, Text
"processSHA2_384" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
xs ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do [W4Eval sym (GenValue (What4 sym))]
blks <- forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
xs
forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"SHA-384"
SymExpr sym (BaseStructType SHA512State)
initSt <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA512State -> IO (SymExpr sym (BaseStructType SHA512State))
mkSHA512InitialState What4 sym
sym SHA512State
SHA.initialSHA384State)
SymExpr sym (BaseStructType SHA512State)
finalSt <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SymExpr sym (BaseStructType SHA512State)
st W4Eval sym (GenValue (What4 sym))
blk -> forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA512State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA512State))
processSHA512Block What4 sym
sym SymExpr sym (BaseStructType SHA512State)
st forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< W4Eval sym (GenValue (What4 sym))
blk) SymExpr sym (BaseStructType SHA512State)
initSt [W4Eval sym (GenValue (What4 sym))]
blks
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
6 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
i ->
case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex (forall a. Num a => Integer -> a
fromInteger Integer
i) (forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize :: Size SHA512State) of
Just (Some Index SHA512State x
idx) ->
do SymExpr sym x
z <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym (BaseStructType SHA512State)
finalSt Index SHA512State x
idx
case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym x
z) (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @64)) of
Just x :~: BaseBVType 64
W4.Refl -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 64 -> SEval (What4 sym) (Value sym)
fromWord64 SymExpr sym x
z
Maybe (x :~: BaseBVType 64)
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_384" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
Maybe (Some (Index SHA512State))
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_384" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
, Text
"processSHA2_512" forall a b. a -> b -> (a, b)
~>
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
xs ->
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
do [W4Eval sym (GenValue (What4 sym))]
blks <- forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
xs
forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"SHA-512"
SymExpr sym (BaseStructType SHA512State)
initSt <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA512State -> IO (SymExpr sym (BaseStructType SHA512State))
mkSHA512InitialState What4 sym
sym SHA512State
SHA.initialSHA512State)
SymExpr sym (BaseStructType SHA512State)
finalSt <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SymExpr sym (BaseStructType SHA512State)
st W4Eval sym (GenValue (What4 sym))
blk -> forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA512State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA512State))
processSHA512Block What4 sym
sym SymExpr sym (BaseStructType SHA512State)
st forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< W4Eval sym (GenValue (What4 sym))
blk) SymExpr sym (BaseStructType SHA512State)
initSt [W4Eval sym (GenValue (What4 sym))]
blks
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
8 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
i ->
case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex (forall a. Num a => Integer -> a
fromInteger Integer
i) (forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize :: Size SHA512State) of
Just (Some Index SHA512State x
idx) ->
do SymExpr sym x
z <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym (BaseStructType SHA512State)
finalSt Index SHA512State x
idx
case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym x
z) (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @64)) of
Just x :~: BaseBVType 64
W4.Refl -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 64 -> SEval (What4 sym) (Value sym)
fromWord64 SymExpr sym x
z
Maybe (x :~: BaseBVType 64)
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_512" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
Maybe (Some (Index SHA512State))
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_512" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
]
type SHA256State =
EmptyCtx ::>
W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::>
W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32
type SHA512State =
EmptyCtx ::>
W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64 ::>
W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64
mkSHA256InitialState :: W4.IsSymExprBuilder sym =>
What4 sym ->
SHA.SHA256State ->
IO (W4.SymExpr sym (W4.BaseStructType SHA256State))
mkSHA256InitialState :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA256State -> IO (SymExpr sym (BaseStructType SHA256State))
mkSHA256InitialState What4 sym
sym (SHA.SHA256S Word32
s0 Word32
s1 Word32
s2 Word32
s3 Word32
s4 Word32
s5 Word32
s6 Word32
s7) =
do SymExpr sym (BaseBVType 32)
z0 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s0
SymExpr sym (BaseBVType 32)
z1 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s1
SymExpr sym (BaseBVType 32)
z2 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s2
SymExpr sym (BaseBVType 32)
z3 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s3
SymExpr sym (BaseBVType 32)
z4 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s4
SymExpr sym (BaseBVType 32)
z5 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s5
SymExpr sym (BaseBVType 32)
z6 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s6
SymExpr sym (BaseBVType 32)
z7 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s7
forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
W4.mkStruct (forall sym. What4 sym -> sym
w4 What4 sym
sym) (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z0 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z1 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z2 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z3 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z4 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z5 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z6 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z7)
where lit :: Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
w = forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32) (Word32 -> BV 32
BV.word32 Word32
w)
mkSHA512InitialState :: W4.IsSymExprBuilder sym =>
What4 sym ->
SHA.SHA512State ->
IO (W4.SymExpr sym (W4.BaseStructType SHA512State))
mkSHA512InitialState :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA512State -> IO (SymExpr sym (BaseStructType SHA512State))
mkSHA512InitialState What4 sym
sym (SHA.SHA512S Word64
s0 Word64
s1 Word64
s2 Word64
s3 Word64
s4 Word64
s5 Word64
s6 Word64
s7) =
do SymExpr sym (BaseBVType 64)
z0 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s0
SymExpr sym (BaseBVType 64)
z1 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s1
SymExpr sym (BaseBVType 64)
z2 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s2
SymExpr sym (BaseBVType 64)
z3 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s3
SymExpr sym (BaseBVType 64)
z4 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s4
SymExpr sym (BaseBVType 64)
z5 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s5
SymExpr sym (BaseBVType 64)
z6 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s6
SymExpr sym (BaseBVType 64)
z7 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s7
forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
W4.mkStruct (forall sym. What4 sym -> sym
w4 What4 sym
sym) (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z0 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z1 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z2 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z3 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z4 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z5 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z6 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z7)
where lit :: Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
w = forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @64) (Word64 -> BV 64
BV.word64 Word64
w)
processSHA256Block :: W4.IsSymExprBuilder sym =>
What4 sym ->
W4.SymExpr sym (W4.BaseStructType SHA256State) ->
Value sym ->
SEval (What4 sym) (W4.SymExpr sym (W4.BaseStructType SHA256State))
processSHA256Block :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA256State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA256State))
processSHA256Block What4 sym
sym SymExpr sym (BaseStructType SHA256State)
st Value sym
blk =
do let ss :: SeqMap (What4 sym) (Value sym)
ss = forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq Value sym
blk
SymExpr sym (BaseBVType 32)
b0 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
0
SymExpr sym (BaseBVType 32)
b1 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
1
SymExpr sym (BaseBVType 32)
b2 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
2
SymExpr sym (BaseBVType 32)
b3 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
3
SymExpr sym (BaseBVType 32)
b4 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
4
SymExpr sym (BaseBVType 32)
b5 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
5
SymExpr sym (BaseBVType 32)
b6 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
6
SymExpr sym (BaseBVType 32)
b7 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
7
SymExpr sym (BaseBVType 32)
b8 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
8
SymExpr sym (BaseBVType 32)
b9 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
9
SymExpr sym (BaseBVType 32)
b10 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
10
SymExpr sym (BaseBVType 32)
b11 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
11
SymExpr sym (BaseBVType 32)
b12 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
12
SymExpr sym (BaseBVType 32)
b13 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
13
SymExpr sym (BaseBVType 32)
b14 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
14
SymExpr sym (BaseBVType 32)
b15 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
15
let args :: Assignment
(SymExpr sym)
(((((((((((((((((EmptyCtx ::> BaseStructType SHA256State)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
args = forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseStructType SHA256State)
st forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
SymExpr sym (BaseBVType 32)
b0 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b1 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b2 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b3 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
SymExpr sym (BaseBVType 32)
b4 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b5 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b6 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b7 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
SymExpr sym (BaseBVType 32)
b8 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b9 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b10 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b11 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
SymExpr sym (BaseBVType 32)
b12 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b13 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b14 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b15
let ret :: BaseTypeRepr (BaseStructType SHA256State)
ret = forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym (BaseStructType SHA256State)
st
SymFn
sym
(((((((((((((((((EmptyCtx ::> BaseStructType SHA256State)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
(BaseStructType SHA256State)
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"processSHA256Block" (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Assignment
(SymExpr sym)
(((((((((((((((((EmptyCtx ::> BaseStructType SHA256State)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
args) BaseTypeRepr (BaseStructType SHA256State)
ret
forall (m :: * -> *) 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
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
sym
(((((((((((((((((EmptyCtx ::> BaseStructType SHA256State)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
(BaseStructType SHA256State)
fn Assignment
(SymExpr sym)
(((((((((((((((((EmptyCtx ::> BaseStructType SHA256State)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
args
processSHA512Block :: W4.IsSymExprBuilder sym =>
What4 sym ->
W4.SymExpr sym (W4.BaseStructType SHA512State) ->
Value sym ->
SEval (What4 sym) (W4.SymExpr sym (W4.BaseStructType SHA512State))
processSHA512Block :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA512State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA512State))
processSHA512Block What4 sym
sym SymExpr sym (BaseStructType SHA512State)
st Value sym
blk =
do let ss :: SeqMap (What4 sym) (Value sym)
ss = forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq Value sym
blk
SymExpr sym (BaseBVType 64)
b0 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
0
SymExpr sym (BaseBVType 64)
b1 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
1
SymExpr sym (BaseBVType 64)
b2 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
2
SymExpr sym (BaseBVType 64)
b3 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
3
SymExpr sym (BaseBVType 64)
b4 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
4
SymExpr sym (BaseBVType 64)
b5 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
5
SymExpr sym (BaseBVType 64)
b6 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
6
SymExpr sym (BaseBVType 64)
b7 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
7
SymExpr sym (BaseBVType 64)
b8 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
8
SymExpr sym (BaseBVType 64)
b9 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
9
SymExpr sym (BaseBVType 64)
b10 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
10
SymExpr sym (BaseBVType 64)
b11 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
11
SymExpr sym (BaseBVType 64)
b12 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
12
SymExpr sym (BaseBVType 64)
b13 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
13
SymExpr sym (BaseBVType 64)
b14 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
14
SymExpr sym (BaseBVType 64)
b15 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
15
let args :: Assignment
(SymExpr sym)
(((((((((((((((((EmptyCtx ::> BaseStructType SHA512State)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
args = forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseStructType SHA512State)
st forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
SymExpr sym (BaseBVType 64)
b0 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b1 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b2 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b3 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
SymExpr sym (BaseBVType 64)
b4 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b5 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b6 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b7 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
SymExpr sym (BaseBVType 64)
b8 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b9 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b10 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b11 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
SymExpr sym (BaseBVType 64)
b12 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b13 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b14 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b15
let ret :: BaseTypeRepr (BaseStructType SHA512State)
ret = forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym (BaseStructType SHA512State)
st
SymFn
sym
(((((((((((((((((EmptyCtx ::> BaseStructType SHA512State)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
(BaseStructType SHA512State)
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"processSHA512Block" (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Assignment
(SymExpr sym)
(((((((((((((((((EmptyCtx ::> BaseStructType SHA512State)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
args) BaseTypeRepr (BaseStructType SHA512State)
ret
forall (m :: * -> *) 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
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
sym
(((((((((((((((((EmptyCtx ::> BaseStructType SHA512State)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
(BaseStructType SHA512State)
fn Assignment
(SymExpr sym)
(((((((((((((((((EmptyCtx ::> BaseStructType SHA512State)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
::> BaseBVType 64)
args
addUninterpWarning :: MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning :: forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
nm = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ (forall sym. What4 sym -> MVar (Set Text)
w4uninterpWarns What4 sym
sym) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> Set a -> Set a
Set.insert Text
nm))
getUninterpFn :: W4.IsSymExprBuilder sym =>
What4 sym ->
Text ->
Assignment W4.BaseTypeRepr args ->
W4.BaseTypeRepr ret ->
IO (W4.SymFn sym args ret)
getUninterpFn :: forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
funNm Assignment BaseTypeRepr args
args BaseTypeRepr ret
ret =
forall a b. MVar a -> (a -> IO (a, b)) -> IO b
modifyMVar (forall sym. What4 sym -> MVar (What4FunCache sym)
w4funs What4 sym
sym) forall a b. (a -> b) -> a -> b
$ \What4FunCache sym
m ->
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
funNm What4FunCache sym
m of
Maybe (SomeSymFn sym)
Nothing ->
do SymFn sym args ret
fn <- forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
W4.freshTotalUninterpFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) (String -> SolverSymbol
W4.safeSymbol (Text -> String
Text.unpack Text
funNm)) Assignment BaseTypeRepr args
args BaseTypeRepr ret
ret
let m' :: What4FunCache sym
m' = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
funNm (forall sym (args :: Ctx BaseType) (ret :: BaseType).
SymFn sym args ret -> SomeSymFn sym
SomeSymFn SymFn sym args ret
fn) What4FunCache sym
m
forall (m :: * -> *) a. Monad m => a -> m a
return (What4FunCache sym
m', SymFn sym args ret
fn)
Just (SomeSymFn SymFn sym args ret
fn)
| Just args :~: args
W4.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality Assignment BaseTypeRepr args
args (forall (fn :: Ctx BaseType -> BaseType -> *) (args :: Ctx BaseType)
(ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
W4.fnArgTypes SymFn sym args ret
fn)
, Just ret :~: ret
W4.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality BaseTypeRepr ret
ret (forall (fn :: Ctx BaseType -> BaseType -> *) (args :: Ctx BaseType)
(ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
W4.fnReturnType SymFn sym args ret
fn)
-> forall (m :: * -> *) a. Monad m => a -> m a
return (What4FunCache sym
m, SymFn sym args ret
fn)
| Bool
otherwise -> forall a. HasCallStack => String -> [String] -> a
panic String
"getUninterpFn"
[ String
"Function" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Text
funNm forall a. [a] -> [a] -> [a]
++ String
"used at incompatible types"
, String
"Created with types:"
, forall a. Show a => a -> String
show (forall (fn :: Ctx BaseType -> BaseType -> *) (args :: Ctx BaseType)
(ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
W4.fnArgTypes SymFn sym args ret
fn) forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (fn :: Ctx BaseType -> BaseType -> *) (args :: Ctx BaseType)
(ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
W4.fnReturnType SymFn sym args ret
fn)
, String
"Requested at types:"
, forall a. Show a => a -> String
show Assignment BaseTypeRepr args
args forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BaseTypeRepr ret
ret
]
toWord32 :: W4.IsSymExprBuilder sym =>
What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 32)
toWord32 :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
nm SeqMap (What4 sym) (GenValue (What4 sym))
ss Integer
i =
do SWord sym
x <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord What4 sym
sym String
nm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
ss Integer
i
case SWord sym
x of
SW.DBV SymBV sym w
x' | Just w :~: 32
W4.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV sym w
x') (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SymBV sym w
x'
SWord sym
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
nm [String
"Unexpected word size", forall a. Show a => a -> String
show (forall sym. SWord sym -> Integer
SW.bvWidth SWord sym
x)]
fromWord32 :: W4.IsSymExprBuilder sym => W4.SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 :: forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
32 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. SWord sym -> WordValue sym
wordVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
SW.DBV
toWord64 :: W4.IsSymExprBuilder sym =>
What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 64)
toWord64 :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
nm SeqMap (What4 sym) (GenValue (What4 sym))
ss Integer
i =
do SWord sym
x <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord What4 sym
sym String
nm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
ss Integer
i
case SWord sym
x of
SW.DBV SymBV sym w
x' | Just w :~: 64
W4.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV sym w
x') (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @64) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SymBV sym w
x'
SWord sym
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
nm [String
"Unexpected word size", forall a. Show a => a -> String
show (forall sym. SWord sym -> Integer
SW.bvWidth SWord sym
x)]
fromWord64 :: W4.IsSymExprBuilder sym => W4.SymBV sym 64 -> SEval (What4 sym) (Value sym)
fromWord64 :: forall sym.
IsSymExprBuilder sym =>
SymBV sym 64 -> SEval (What4 sym) (Value sym)
fromWord64 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
64 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. SWord sym -> WordValue sym
wordVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
SW.DBV
applyAESStateFunc :: forall sym. W4.IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
funNm Value sym
x =
do let ss :: SeqMap (What4 sym) (Value sym)
ss = forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq Value sym
x
SymExpr sym (BaseBVType 32)
w0 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
nm SeqMap (What4 sym) (Value sym)
ss Integer
0
SymExpr sym (BaseBVType 32)
w1 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
nm SeqMap (What4 sym) (Value sym)
ss Integer
1
SymExpr sym (BaseBVType 32)
w2 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
nm SeqMap (What4 sym) (Value sym)
ss Integer
2
SymExpr sym (BaseBVType 32)
w3 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
nm SeqMap (What4 sym) (Value sym)
ss Integer
3
SymFn
sym
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
('BaseStructType
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32))
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
funNm Assignment
BaseTypeRepr
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
argCtx (forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr ('BaseStructType ctx)
W4.BaseStructRepr Assignment
BaseTypeRepr
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
argCtx)
SymExpr
sym
('BaseStructType
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32))
z <- forall (m :: * -> *) 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
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
sym
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
('BaseStructType
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32))
fn (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
w0 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
w1 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
w2 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
w3)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
4 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
i ->
if | Integer
i forall a. Eq a => a -> a -> Bool
== Integer
0 -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr
sym
('BaseStructType
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32))
z (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @0))
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
1 -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr
sym
('BaseStructType
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32))
z (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @1))
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
2 -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr
sym
('BaseStructType
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32))
z (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @2))
| Integer
i forall a. Eq a => a -> a -> Bool
== Integer
3 -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr
sym
('BaseStructType
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32))
z (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @3))
| Bool
otherwise -> forall a. String -> [String] -> a
evalPanic String
"applyAESStateFunc" [String
"Index out of range", forall a. Show a => a -> String
show Text
funNm, forall a. Show a => a -> String
show Integer
i]
where
nm :: String
nm = Text -> String
Text.unpack Text
funNm
argCtx :: Assignment W4.BaseTypeRepr
(EmptyCtx ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32)
argCtx :: Assignment
BaseTypeRepr
((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
::> BaseBVType 32)
::> BaseBVType 32)
argCtx = forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
W4.knownRepr
indexFront_int ::
W4.IsSymExprBuilder sym =>
What4 sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) (GenValue (What4 sym)) ->
TValue ->
SInteger (What4 sym) ->
SEval (What4 sym) (Value sym)
indexFront_int :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> SInteger (What4 sym)
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_int What4 sym
sym Nat'
mblen TValue
_a SeqMap (What4 sym) (GenValue (What4 sym))
xs TValue
_ix SInteger (What4 sym)
idx
| Just Integer
i <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SInteger (What4 sym)
idx
= forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
i
| (Integer
lo, Just Integer
hi) <- (Integer, Maybe Integer)
bounds
= case forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer
-> Maybe (W4Eval sym (GenValue (What4 sym)))
-> Maybe (W4Eval sym (GenValue (What4 sym)))
f forall a. Maybe a
Nothing [Integer
lo .. Integer
hi] of
Maybe (W4Eval sym (GenValue (What4 sym)))
Nothing -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError What4 sym
sym (Maybe Integer -> EvalError
InvalidIndex forall a. Maybe a
Nothing)
Just W4Eval sym (GenValue (What4 sym))
m -> W4Eval sym (GenValue (What4 sym))
m
| Bool
otherwise
= forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a e. Exception e => e -> a
X.throw (String -> Unsupported
UnsupportedSymbolicOp String
"unbounded integer indexing"))
where
w4sym :: sym
w4sym = forall sym. What4 sym -> sym
w4 What4 sym
sym
f :: Integer
-> Maybe (W4Eval sym (GenValue (What4 sym)))
-> Maybe (W4Eval sym (GenValue (What4 sym)))
f Integer
n (Just W4Eval sym (GenValue (What4 sym))
y) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
do SymExpr sym BaseBoolType
p <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intEq sym
w4sym SInteger (What4 sym)
idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
w4sym Integer
n)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
p (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
n) W4Eval sym (GenValue (What4 sym))
y
f Integer
n Maybe (W4Eval sym (GenValue (What4 sym)))
Nothing = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
n
bounds :: (Integer, Maybe Integer)
bounds =
(case forall tp. ValueRange tp -> ValueBound tp
W4.rangeLowBound (forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> ValueRange Integer
W4.integerBounds SInteger (What4 sym)
idx) of
W4.Inclusive Integer
l -> forall a. Ord a => a -> a -> a
max Integer
l Integer
0
ValueBound Integer
_ -> Integer
0
, case (Maybe Integer
maxIdx, forall tp. ValueRange tp -> ValueBound tp
W4.rangeHiBound (forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> ValueRange Integer
W4.integerBounds SInteger (What4 sym)
idx)) of
(Just Integer
n, W4.Inclusive Integer
h) -> forall a. a -> Maybe a
Just (forall a. Ord a => a -> a -> a
min Integer
n Integer
h)
(Just Integer
n, ValueBound Integer
_) -> forall a. a -> Maybe a
Just Integer
n
(Maybe Integer, ValueBound Integer)
_ -> forall a. Maybe a
Nothing
)
maxIdx :: Maybe Integer
maxIdx =
case Nat'
mblen of
Nat Integer
n -> forall a. a -> Maybe a
Just (Integer
n forall a. Num a => a -> a -> a
- Integer
1)
Nat'
Inf -> forall a. Maybe a
Nothing
indexFront_segs ::
W4.IsSymExprBuilder sym =>
What4 sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) (GenValue (What4 sym)) ->
TValue ->
Integer ->
[IndexSegment (What4 sym)] ->
SEval (What4 sym) (Value sym)
indexFront_segs :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> Integer
-> [IndexSegment (What4 sym)]
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_segs What4 sym
sym Nat'
mblen TValue
_a SeqMap (What4 sym) (GenValue (What4 sym))
xs TValue
_ix Integer
_idx_bits [WordIndexSegment SWord (What4 sym)
idx]
| Just Integer
i <- forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
SW.bvAsUnsignedInteger SWord (What4 sym)
idx
= forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
i
| Bool
otherwise
= case forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer
-> Maybe (W4Eval sym (GenValue (What4 sym)))
-> Maybe (W4Eval sym (GenValue (What4 sym)))
f forall a. Maybe a
Nothing [Integer]
idxs of
Maybe (W4Eval sym (GenValue (What4 sym)))
Nothing -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError What4 sym
sym (Maybe Integer -> EvalError
InvalidIndex forall a. Maybe a
Nothing)
Just W4Eval sym (GenValue (What4 sym))
m -> W4Eval sym (GenValue (What4 sym))
m
where
w4sym :: sym
w4sym = forall sym. What4 sym -> sym
w4 What4 sym
sym
w :: Integer
w = forall sym. SWord sym -> Integer
SW.bvWidth SWord (What4 sym)
idx
f :: Integer
-> Maybe (W4Eval sym (GenValue (What4 sym)))
-> Maybe (W4Eval sym (GenValue (What4 sym)))
f Integer
n (Just W4Eval sym (GenValue (What4 sym))
y) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
do SymExpr sym BaseBoolType
p <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (PredBin
SW.bvEq sym
w4sym SWord (What4 sym)
idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
SW.bvLit sym
w4sym Integer
w Integer
n)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
p (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
n) W4Eval sym (GenValue (What4 sym))
y
f Integer
n Maybe (W4Eval sym (GenValue (What4 sym)))
Nothing = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
n
maxIdx :: Integer
maxIdx =
case Nat'
mblen of
Nat Integer
n | Integer
n forall a. Ord a => a -> a -> Bool
< Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
w -> Integer
nforall a. Num a => a -> a -> a
-Integer
1
Nat'
_ -> Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
w forall a. Num a => a -> a -> a
- Integer
1
idxs :: [Integer]
idxs =
case forall sym.
IsExprBuilder sym =>
SWord sym -> Maybe (Integer, Integer)
SW.unsignedBVBounds SWord (What4 sym)
idx of
Just (Integer
lo, Integer
hi) -> [Integer
lo .. forall a. Ord a => a -> a -> a
min Integer
hi Integer
maxIdx]
Maybe (Integer, Integer)
_ -> [Integer
0 .. Integer
maxIdx]
indexFront_segs What4 sym
sym Nat'
mblen TValue
_a SeqMap (What4 sym) (GenValue (What4 sym))
xs TValue
_ix Integer
idx_bits [IndexSegment (What4 sym)]
segs =
do SeqMap (What4 sym) (GenValue (What4 sym))
xs' <- forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> (SeqMap sym a -> Integer -> SEval sym (SeqMap sym a))
-> Nat'
-> SeqMap sym a
-> Integer
-> [IndexSegment sym]
-> SEval sym (SeqMap sym a)
barrelShifter What4 sym
sym (forall sym.
Backend sym =>
sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue What4 sym
sym) forall {sym} {sym} {f :: * -> *} {a}.
(SEval sym ~ SEval sym, Backend sym, Applicative f) =>
SeqMap sym a -> Integer -> f (SeqMap sym a)
shiftOp Nat'
mblen SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
idx_bits [IndexSegment (What4 sym)]
segs
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs' Integer
0
where
shiftOp :: SeqMap sym a -> Integer -> f (SeqMap sym a)
shiftOp SeqMap sym a
vs Integer
amt = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap (\Integer
i -> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
vs forall a b. (a -> b) -> a -> b
$! Integer
amtforall a. Num a => a -> a -> a
+Integer
i))
updateFrontSym ::
W4.IsSymExprBuilder sym =>
What4 sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) (GenValue (What4 sym)) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (Value sym) ->
SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateFrontSym :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateFrontSym What4 sym
sym Nat'
_len TValue
_eltTy SeqMap (What4 sym) (GenValue (What4 sym))
vs (Left SInteger (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
case forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SInteger (What4 sym)
idx of
Just Integer
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
i SEval (What4 sym) (GenValue (What4 sym))
val
Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
do SymExpr sym BaseBoolType
b <- forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq What4 sym
sym SInteger (What4 sym)
idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
i
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
b SEval (What4 sym) (GenValue (What4 sym))
val (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
i)
updateFrontSym What4 sym
sym Nat'
len TValue
_eltTy SeqMap (What4 sym) (GenValue (What4 sym))
vs (Right WordValue (What4 sym)
wv) SEval (What4 sym) (GenValue (What4 sym))
val =
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit What4 sym
sym WordValue (What4 sym)
wv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just Integer
j -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
j SEval (What4 sym) (GenValue (What4 sym))
val
Maybe Integer
Nothing ->
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap What4 sym
sym Nat'
len forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
do SymExpr sym BaseBoolType
b <- forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
wordValueEqualsInteger What4 sym
sym WordValue (What4 sym)
wv Integer
i
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
b SEval (What4 sym) (GenValue (What4 sym))
val (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
i)
updateBackSym ::
W4.IsSymExprBuilder sym =>
What4 sym ->
Nat' ->
TValue ->
SeqMap (What4 sym) (GenValue (What4 sym)) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (Value sym) ->
SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateBackSym :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateBackSym What4 sym
_ Nat'
Inf TValue
_ SeqMap (What4 sym) (GenValue (What4 sym))
_ Either (SInteger (What4 sym)) (WordValue (What4 sym))
_ SEval (What4 sym) (GenValue (What4 sym))
_ = forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"updateBackSym"]
updateBackSym What4 sym
sym (Nat Integer
n) TValue
_eltTy SeqMap (What4 sym) (GenValue (What4 sym))
vs (Left SInteger (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
case forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SInteger (What4 sym)
idx of
Just Integer
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs (Integer
n forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
i) SEval (What4 sym) (GenValue (What4 sym))
val
Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
do SymExpr sym BaseBoolType
b <- forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq What4 sym
sym SInteger (What4 sym)
idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym (Integer
n forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
i)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
b SEval (What4 sym) (GenValue (What4 sym))
val (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
i)
updateBackSym What4 sym
sym (Nat Integer
n) TValue
_eltTy SeqMap (What4 sym) (GenValue (What4 sym))
vs (Right WordValue (What4 sym)
wv) SEval (What4 sym) (GenValue (What4 sym))
val =
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit What4 sym
sym WordValue (What4 sym)
wv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just Integer
j ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs (Integer
n forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
j) SEval (What4 sym) (GenValue (What4 sym))
val
Maybe Integer
Nothing ->
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap What4 sym
sym (Integer -> Nat'
Nat Integer
n) forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
do SymExpr sym BaseBoolType
b <- forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
wordValueEqualsInteger What4 sym
sym WordValue (What4 sym)
wv (Integer
n forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
i)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
b SEval (What4 sym) (GenValue (What4 sym))
val (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
i)
updateFrontSym_word ::
W4.IsSymExprBuilder sym =>
What4 sym ->
Nat' ->
TValue ->
WordValue (What4 sym) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (GenValue (What4 sym)) ->
SEval (What4 sym) (WordValue (What4 sym))
updateFrontSym_word :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> WordValue (What4 sym)
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (WordValue (What4 sym))
updateFrontSym_word What4 sym
_ Nat'
Inf TValue
_ WordValue (What4 sym)
_ Either (SInteger (What4 sym)) (WordValue (What4 sym))
_ SEval (What4 sym) (GenValue (What4 sym))
_ = forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"updateFrontSym_word"]
updateFrontSym_word What4 sym
sym (Nat Integer
n) TValue
_eltTy WordValue (What4 sym)
w (Left SInteger (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
do SWord sym
idx' <- forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt What4 sym
sym Integer
n SInteger (What4 sym)
idx
forall sym.
Backend sym =>
sym
-> IndexDirection
-> WordValue sym
-> WordValue sym
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordByWord What4 sym
sym IndexDirection
IndexForward WordValue (What4 sym)
w (forall sym. SWord sym -> WordValue sym
wordVal SWord sym
idx') (forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
val)
updateFrontSym_word What4 sym
sym (Nat Integer
_n) TValue
_eltTy WordValue (What4 sym)
w (Right WordValue (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
forall sym.
Backend sym =>
sym
-> IndexDirection
-> WordValue sym
-> WordValue sym
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordByWord What4 sym
sym IndexDirection
IndexForward WordValue (What4 sym)
w WordValue (What4 sym)
idx (forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
val)
updateBackSym_word ::
W4.IsSymExprBuilder sym =>
What4 sym ->
Nat' ->
TValue ->
WordValue (What4 sym) ->
Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
SEval (What4 sym) (GenValue (What4 sym)) ->
SEval (What4 sym) (WordValue (What4 sym))
updateBackSym_word :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> WordValue (What4 sym)
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (WordValue (What4 sym))
updateBackSym_word What4 sym
_ Nat'
Inf TValue
_ WordValue (What4 sym)
_ Either (SInteger (What4 sym)) (WordValue (What4 sym))
_ SEval (What4 sym) (GenValue (What4 sym))
_ = forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"updateFrontSym_word"]
updateBackSym_word What4 sym
sym (Nat Integer
n) TValue
_eltTy WordValue (What4 sym)
w (Left SInteger (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
do SWord sym
idx' <- forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt What4 sym
sym Integer
n SInteger (What4 sym)
idx
forall sym.
Backend sym =>
sym
-> IndexDirection
-> WordValue sym
-> WordValue sym
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordByWord What4 sym
sym IndexDirection
IndexBackward WordValue (What4 sym)
w (forall sym. SWord sym -> WordValue sym
wordVal SWord sym
idx') (forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
val)
updateBackSym_word What4 sym
sym (Nat Integer
_n) TValue
_eltTy WordValue (What4 sym)
w (Right WordValue (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
forall sym.
Backend sym =>
sym
-> IndexDirection
-> WordValue sym
-> WordValue sym
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordByWord What4 sym
sym IndexDirection
IndexBackward WordValue (What4 sym)
w WordValue (What4 sym)
idx (forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
val)