{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternGuards #-}
module Lang.Crucible.Syntax
( IsExpr(..)
, eapp
, asEapp
, true
, false
, notExpr
, (.&&)
, (.||)
, EqExpr(..)
, OrdExpr(..)
, NumExpr(..)
, LitExpr(..)
, ConvertableToNat(..)
, rationalLit
, natToReal
, integerToReal
, realToCplx
, imagToCplx
, realPart
, imagPart
, realLit
, imagLit
, natToCplx
, nothingValue
, justValue
, vectorSize
, vectorLit
, vectorGetEntry
, vectorSetEntry
, vectorIsEmpty
, vecReplicate
, closure
, emptyIdentValueMap
, setIdentValue
, mkStruct
, getStruct
, setStruct
, concatExprs
, bigEndianLoad
, bigEndianLoadDef
, bigEndianStore
, littleEndianLoad
, littleEndianLoadDef
, littleEndianStore
) where
import Control.Lens
import qualified Data.BitVector.Sized as BV
import Data.Kind
import Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Some
import Data.Text (Text)
import qualified Data.Vector as V
import Numeric.Natural
import Lang.Crucible.CFG.Expr
import Lang.Crucible.FunctionHandle
import Lang.Crucible.Types
import What4.Utils.StringLiteral
class IsExpr e where
type ExprExt e :: Type
app :: App (ExprExt e) e tp -> e tp
asApp :: e tp -> Maybe (App (ExprExt e) e tp)
exprType :: e tp -> TypeRepr tp
eapp :: IsExpr e => ExprExtension (ExprExt e) e tp -> e tp
eapp :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
ExprExtension (ExprExt e) e tp -> e tp
eapp = App (ExprExt e) e tp -> e tp
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt e) e tp -> e tp)
-> (ExprExtension (ExprExt e) e tp -> App (ExprExt e) e tp)
-> ExprExtension (ExprExt e) e tp
-> e tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprExtension (ExprExt e) e tp -> App (ExprExt e) e tp
forall ext (f :: CrucibleType -> Type) (tp :: CrucibleType).
ExprExtension ext f tp -> App ext f tp
ExtensionApp
asEapp :: IsExpr e => e tp -> Maybe (ExprExtension (ExprExt e) e tp)
asEapp :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> Maybe (ExprExtension (ExprExt e) e tp)
asEapp e tp
e =
case e tp -> Maybe (App (ExprExt e) e tp)
forall (tp :: CrucibleType). e tp -> Maybe (App (ExprExt e) e tp)
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> Maybe (App (ExprExt e) e tp)
asApp e tp
e of
Just (ExtensionApp ExprExtension (ExprExt e) e tp
x) -> ExprExtension (ExprExt e) e tp
-> Maybe (ExprExtension (ExprExt e) e tp)
forall a. a -> Maybe a
Just ExprExtension (ExprExt e) e tp
x
Maybe (App (ExprExt e) e tp)
_ -> Maybe (ExprExtension (ExprExt e) e tp)
forall a. Maybe a
Nothing
class LitExpr e tp ty | tp -> ty where
litExpr :: IsExpr e => ty -> e tp
instance LitExpr e BoolType Bool where
litExpr :: IsExpr e => Bool -> e BoolType
litExpr Bool
b = App (ExprExt e) e BoolType -> e BoolType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (Bool -> App (ExprExt e) e BoolType
forall ext (f :: CrucibleType -> Type). Bool -> App ext f BoolType
BoolLit Bool
b)
true :: IsExpr e => e BoolType
true :: forall (e :: CrucibleType -> Type). IsExpr e => e BoolType
true = Bool -> e BoolType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Bool
True
false :: IsExpr e => e BoolType
false :: forall (e :: CrucibleType -> Type). IsExpr e => e BoolType
false = Bool -> e BoolType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Bool
False
notExpr :: IsExpr e => e BoolType -> e BoolType
notExpr :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e BoolType -> e BoolType
notExpr e BoolType
x = App (ExprExt e) e BoolType -> e BoolType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e BoolType -> App (ExprExt e) e BoolType
forall (f :: CrucibleType -> Type) ext.
f BoolType -> App ext f BoolType
Not e BoolType
x)
(.&&) :: IsExpr e => e BoolType -> e BoolType -> e BoolType
.&& :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e BoolType -> e BoolType -> e BoolType
(.&&) e BoolType
x e BoolType
y = App (ExprExt e) e BoolType -> e BoolType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e BoolType -> e BoolType -> App (ExprExt e) e BoolType
forall (f :: CrucibleType -> Type) ext.
f BoolType -> f BoolType -> App ext f BoolType
And e BoolType
x e BoolType
y)
(.||) :: IsExpr e => e BoolType -> e BoolType -> e BoolType
.|| :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e BoolType -> e BoolType -> e BoolType
(.||) e BoolType
x e BoolType
y = App (ExprExt e) e BoolType -> e BoolType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e BoolType -> e BoolType -> App (ExprExt e) e BoolType
forall (f :: CrucibleType -> Type) ext.
f BoolType -> f BoolType -> App ext f BoolType
Or e BoolType
x e BoolType
y)
infixr 3 .&&
infixr 2 .||
class EqExpr e tp where
(.==) :: IsExpr e => e tp -> e tp -> e BoolType
(./=) :: IsExpr e => e tp -> e tp -> e BoolType
e tp
x ./= e tp
y = e BoolType -> e BoolType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e BoolType -> e BoolType
notExpr (e tp
x e tp -> e tp -> e BoolType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(EqExpr e tp, IsExpr e) =>
e tp -> e tp -> e BoolType
.== e tp
y)
infix 4 .==
infix 4 ./=
class EqExpr e tp => OrdExpr e tp where
(.<) :: IsExpr e => e tp -> e tp -> e BoolType
(.<=) :: IsExpr e => e tp -> e tp -> e BoolType
e tp
x .<= e tp
y = e BoolType -> e BoolType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e BoolType -> e BoolType
notExpr (e tp
y e tp -> e tp -> e BoolType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(OrdExpr e tp, IsExpr e) =>
e tp -> e tp -> e BoolType
.< e tp
x)
(.>) :: IsExpr e => e tp -> e tp -> e BoolType
e tp
x .> e tp
y = e tp
y e tp -> e tp -> e BoolType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(OrdExpr e tp, IsExpr e) =>
e tp -> e tp -> e BoolType
.< e tp
x
(.>=) :: IsExpr e => e tp -> e tp -> e BoolType
e tp
x .>= e tp
y = e tp
y e tp -> e tp -> e BoolType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(OrdExpr e tp, IsExpr e) =>
e tp -> e tp -> e BoolType
.<= e tp
x
infix 4 .<
infix 4 .<=
infix 4 .>
infix 4 .>=
class NumExpr e tp where
(.+) :: IsExpr e => e tp -> e tp -> e tp
(.-) :: IsExpr e => e tp -> e tp -> e tp
(.*) :: IsExpr e => e tp -> e tp -> e tp
instance LitExpr e NatType Natural where
litExpr :: IsExpr e => Natural -> e NatType
litExpr Natural
n = App (ExprExt e) e NatType -> e NatType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (Natural -> App (ExprExt e) e NatType
forall ext (f :: CrucibleType -> Type).
Natural -> App ext f NatType
NatLit Natural
n)
instance EqExpr e NatType where
e NatType
x .== :: IsExpr e => e NatType -> e NatType -> e BoolType
.== e NatType
y = App (ExprExt e) e BoolType -> e BoolType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e NatType -> e NatType -> App (ExprExt e) e BoolType
forall (f :: CrucibleType -> Type) ext.
f NatType -> f NatType -> App ext f BoolType
NatEq e NatType
x e NatType
y)
instance OrdExpr e NatType where
e NatType
x .< :: IsExpr e => e NatType -> e NatType -> e BoolType
.< e NatType
y = App (ExprExt e) e BoolType -> e BoolType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e NatType -> e NatType -> App (ExprExt e) e BoolType
forall (f :: CrucibleType -> Type) ext.
f NatType -> f NatType -> App ext f BoolType
NatLt e NatType
x e NatType
y)
instance NumExpr e NatType where
e NatType
x .+ :: IsExpr e => e NatType -> e NatType -> e NatType
.+ e NatType
y = App (ExprExt e) e NatType -> e NatType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e NatType -> e NatType -> App (ExprExt e) e NatType
forall (f :: CrucibleType -> Type) ext.
f NatType -> f NatType -> App ext f NatType
NatAdd e NatType
x e NatType
y)
e NatType
x .- :: IsExpr e => e NatType -> e NatType -> e NatType
.- e NatType
y = App (ExprExt e) e NatType -> e NatType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e NatType -> e NatType -> App (ExprExt e) e NatType
forall (f :: CrucibleType -> Type) ext.
f NatType -> f NatType -> App ext f NatType
NatSub e NatType
x e NatType
y)
e NatType
x .* :: IsExpr e => e NatType -> e NatType -> e NatType
.* e NatType
y = App (ExprExt e) e NatType -> e NatType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e NatType -> e NatType -> App (ExprExt e) e NatType
forall (f :: CrucibleType -> Type) ext.
f NatType -> f NatType -> App ext f NatType
NatMul e NatType
x e NatType
y)
instance LitExpr e IntegerType Integer where
litExpr :: IsExpr e => Integer -> e IntegerType
litExpr Integer
x = App (ExprExt e) e IntegerType -> e IntegerType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (Integer -> App (ExprExt e) e IntegerType
forall ext (f :: CrucibleType -> Type).
Integer -> App ext f IntegerType
IntLit Integer
x)
class ConvertableToNat e tp where
toNat :: IsExpr e => e tp -> e NatType
rationalLit :: IsExpr e => Rational -> e RealValType
rationalLit :: forall (e :: CrucibleType -> Type).
IsExpr e =>
Rational -> e RealValType
rationalLit Rational
v = App (ExprExt e) e RealValType -> e RealValType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (Rational -> App (ExprExt e) e RealValType
forall ext (f :: CrucibleType -> Type).
Rational -> App ext f RealValType
RationalLit Rational
v)
instance EqExpr e RealValType where
e RealValType
x .== :: IsExpr e => e RealValType -> e RealValType -> e BoolType
.== e RealValType
y = App (ExprExt e) e BoolType -> e BoolType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e RealValType -> e RealValType -> App (ExprExt e) e BoolType
forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
(tp ~ BoolType) =>
f RealValType -> f RealValType -> App ext f tp
RealEq e RealValType
x e RealValType
y)
instance OrdExpr e RealValType where
e RealValType
x .< :: IsExpr e => e RealValType -> e RealValType -> e BoolType
.< e RealValType
y = App (ExprExt e) e BoolType -> e BoolType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e RealValType -> e RealValType -> App (ExprExt e) e BoolType
forall (f :: CrucibleType -> Type) ext.
f RealValType -> f RealValType -> App ext f BoolType
RealLt e RealValType
x e RealValType
y)
natToInteger :: IsExpr e => e NatType -> e IntegerType
natToInteger :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e NatType -> e IntegerType
natToInteger e NatType
x = App (ExprExt e) e IntegerType -> e IntegerType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e NatType -> App (ExprExt e) e IntegerType
forall (f :: CrucibleType -> Type) ext.
f NatType -> App ext f IntegerType
NatToInteger e NatType
x)
integerToReal :: IsExpr e => e IntegerType -> e RealValType
integerToReal :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e IntegerType -> e RealValType
integerToReal e IntegerType
x = App (ExprExt e) e RealValType -> e RealValType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e IntegerType -> App (ExprExt e) e RealValType
forall (f :: CrucibleType -> Type) ext.
f IntegerType -> App ext f RealValType
IntegerToReal e IntegerType
x)
natToReal :: IsExpr e => e NatType -> e RealValType
natToReal :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e NatType -> e RealValType
natToReal = e IntegerType -> e RealValType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e IntegerType -> e RealValType
integerToReal (e IntegerType -> e RealValType)
-> (e NatType -> e IntegerType) -> e NatType -> e RealValType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e NatType -> e IntegerType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e NatType -> e IntegerType
natToInteger
instance ConvertableToNat e RealValType where
toNat :: IsExpr e => e RealValType -> e NatType
toNat e RealValType
v = App (ExprExt e) e NatType -> e NatType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e RealValType -> App (ExprExt e) e NatType
forall (f :: CrucibleType -> Type) ext.
f RealValType -> App ext f NatType
RealToNat e RealValType
v)
realToCplx :: IsExpr e => e RealValType -> e ComplexRealType
realToCplx :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e RealValType -> e ComplexRealType
realToCplx e RealValType
v = App (ExprExt e) e ComplexRealType -> e ComplexRealType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e RealValType -> e RealValType -> App (ExprExt e) e ComplexRealType
forall (f :: CrucibleType -> Type) ext.
f RealValType -> f RealValType -> App ext f ComplexRealType
Complex e RealValType
v (Rational -> e RealValType
forall (e :: CrucibleType -> Type).
IsExpr e =>
Rational -> e RealValType
rationalLit Rational
0))
imagToCplx :: IsExpr e => e RealValType -> e ComplexRealType
imagToCplx :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e RealValType -> e ComplexRealType
imagToCplx e RealValType
v = App (ExprExt e) e ComplexRealType -> e ComplexRealType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e RealValType -> e RealValType -> App (ExprExt e) e ComplexRealType
forall (f :: CrucibleType -> Type) ext.
f RealValType -> f RealValType -> App ext f ComplexRealType
Complex (Rational -> e RealValType
forall (e :: CrucibleType -> Type).
IsExpr e =>
Rational -> e RealValType
rationalLit Rational
0) e RealValType
v)
realPart :: IsExpr e => e ComplexRealType -> e RealValType
realPart :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e ComplexRealType -> e RealValType
realPart e ComplexRealType
c = App (ExprExt e) e RealValType -> e RealValType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e ComplexRealType -> App (ExprExt e) e RealValType
forall (f :: CrucibleType -> Type) ext.
f ComplexRealType -> App ext f RealValType
RealPart e ComplexRealType
c)
imagPart :: IsExpr e => e ComplexRealType -> e RealValType
imagPart :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e ComplexRealType -> e RealValType
imagPart e ComplexRealType
c = App (ExprExt e) e RealValType -> e RealValType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e ComplexRealType -> App (ExprExt e) e RealValType
forall (f :: CrucibleType -> Type) ext.
f ComplexRealType -> App ext f RealValType
ImagPart e ComplexRealType
c)
realLit :: IsExpr e => Rational -> e ComplexRealType
realLit :: forall (e :: CrucibleType -> Type).
IsExpr e =>
Rational -> e ComplexRealType
realLit = e RealValType -> e ComplexRealType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e RealValType -> e ComplexRealType
realToCplx (e RealValType -> e ComplexRealType)
-> (Rational -> e RealValType) -> Rational -> e ComplexRealType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> e RealValType
forall (e :: CrucibleType -> Type).
IsExpr e =>
Rational -> e RealValType
rationalLit
imagLit :: IsExpr e => Rational -> e ComplexRealType
imagLit :: forall (e :: CrucibleType -> Type).
IsExpr e =>
Rational -> e ComplexRealType
imagLit = e RealValType -> e ComplexRealType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e RealValType -> e ComplexRealType
imagToCplx (e RealValType -> e ComplexRealType)
-> (Rational -> e RealValType) -> Rational -> e ComplexRealType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> e RealValType
forall (e :: CrucibleType -> Type).
IsExpr e =>
Rational -> e RealValType
rationalLit
natToCplx :: IsExpr e => e NatType -> e ComplexRealType
natToCplx :: forall (e :: CrucibleType -> Type).
IsExpr e =>
e NatType -> e ComplexRealType
natToCplx = e RealValType -> e ComplexRealType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e RealValType -> e ComplexRealType
realToCplx (e RealValType -> e ComplexRealType)
-> (e NatType -> e RealValType) -> e NatType -> e ComplexRealType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e NatType -> e RealValType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e NatType -> e RealValType
natToReal
instance ConvertableToNat e ComplexRealType where
toNat :: IsExpr e => e ComplexRealType -> e NatType
toNat = e RealValType -> e NatType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(ConvertableToNat e tp, IsExpr e) =>
e tp -> e NatType
toNat (e RealValType -> e NatType)
-> (e ComplexRealType -> e RealValType)
-> e ComplexRealType
-> e NatType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e ComplexRealType -> e RealValType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e ComplexRealType -> e RealValType
realPart
instance LitExpr e (StringType Unicode) Text where
litExpr :: IsExpr e => Text -> e (StringType Unicode)
litExpr Text
t = App (ExprExt e) e (StringType Unicode) -> e (StringType Unicode)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (StringLiteral Unicode -> App (ExprExt e) e (StringType Unicode)
forall (si :: StringInfo) ext (f :: CrucibleType -> Type).
StringLiteral si -> App ext f ('BaseToType (BaseStringType si))
StringLit (Text -> StringLiteral Unicode
UnicodeLiteral Text
t))
nothingValue :: (IsExpr e, KnownRepr TypeRepr tp) => e (MaybeType tp)
nothingValue :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(IsExpr e, KnownRepr TypeRepr tp) =>
e (MaybeType tp)
nothingValue = App (ExprExt e) e (MaybeType tp) -> e (MaybeType tp)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (TypeRepr tp -> App (ExprExt e) e (MaybeType tp)
forall (tp1 :: CrucibleType) ext (f :: CrucibleType -> Type).
TypeRepr tp1 -> App ext f ('MaybeType tp1)
NothingValue TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr)
justValue :: (IsExpr e, KnownRepr TypeRepr tp) => e tp -> e (MaybeType tp)
justValue :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(IsExpr e, KnownRepr TypeRepr tp) =>
e tp -> e (MaybeType tp)
justValue e tp
x = App (ExprExt e) e (MaybeType tp) -> e (MaybeType tp)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (TypeRepr tp -> e tp -> App (ExprExt e) e (MaybeType tp)
forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp1 -> f tp1 -> App ext f ('MaybeType tp1)
JustValue TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr e tp
x)
vectorSize :: (IsExpr e) => e (VectorType tp) -> e NatType
vectorSize :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e (VectorType tp) -> e NatType
vectorSize e (VectorType tp)
v = App (ExprExt e) e NatType -> e NatType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e (VectorType tp) -> App (ExprExt e) e NatType
forall (f :: CrucibleType -> Type) (tp1 :: CrucibleType) ext.
f (VectorType tp1) -> App ext f NatType
VectorSize e (VectorType tp)
v)
vectorIsEmpty :: (IsExpr e) => e (VectorType tp) -> e BoolType
vectorIsEmpty :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e (VectorType tp) -> e BoolType
vectorIsEmpty e (VectorType tp)
v = App (ExprExt e) e BoolType -> e BoolType
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e (VectorType tp) -> App (ExprExt e) e BoolType
forall (f :: CrucibleType -> Type) (tp1 :: CrucibleType) ext.
f (VectorType tp1) -> App ext f BoolType
VectorIsEmpty e (VectorType tp)
v)
vectorLit :: (IsExpr e) => TypeRepr tp -> V.Vector (e tp) -> e (VectorType tp)
vectorLit :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
TypeRepr tp -> Vector (e tp) -> e (VectorType tp)
vectorLit TypeRepr tp
tp Vector (e tp)
v = App (ExprExt e) e (VectorType tp) -> e (VectorType tp)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (TypeRepr tp -> Vector (e tp) -> App (ExprExt e) e (VectorType tp)
forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp1 -> Vector (f tp1) -> App ext f ('VectorType tp1)
VectorLit TypeRepr tp
tp Vector (e tp)
v)
vectorGetEntry :: (IsExpr e, KnownRepr TypeRepr tp) => e (VectorType tp) -> e NatType -> e tp
vectorGetEntry :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(IsExpr e, KnownRepr TypeRepr tp) =>
e (VectorType tp) -> e NatType -> e tp
vectorGetEntry e (VectorType tp)
v e NatType
i = App (ExprExt e) e tp -> e tp
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (TypeRepr tp
-> e (VectorType tp) -> e NatType -> App (ExprExt e) e tp
forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp -> f (VectorType tp) -> f NatType -> App ext f tp
VectorGetEntry TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr e (VectorType tp)
v e NatType
i)
vectorSetEntry :: (IsExpr e, KnownRepr TypeRepr tp )
=> e (VectorType tp)
-> e NatType
-> e tp
-> e (VectorType tp)
vectorSetEntry :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(IsExpr e, KnownRepr TypeRepr tp) =>
e (VectorType tp) -> e NatType -> e tp -> e (VectorType tp)
vectorSetEntry e (VectorType tp)
v e NatType
i e tp
x = App (ExprExt e) e (VectorType tp) -> e (VectorType tp)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (TypeRepr tp
-> e (VectorType tp)
-> e NatType
-> e tp
-> App (ExprExt e) e (VectorType tp)
forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp1
-> f (VectorType tp1)
-> f NatType
-> f tp1
-> App ext f (VectorType tp1)
VectorSetEntry TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr e (VectorType tp)
v e NatType
i e tp
x)
vecReplicate :: (IsExpr e, KnownRepr TypeRepr tp) => e NatType -> e tp -> e (VectorType tp)
vecReplicate :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(IsExpr e, KnownRepr TypeRepr tp) =>
e NatType -> e tp -> e (VectorType tp)
vecReplicate e NatType
n e tp
v = App (ExprExt e) e (VectorType tp) -> e (VectorType tp)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (TypeRepr tp
-> e NatType -> e tp -> App (ExprExt e) e (VectorType tp)
forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp1 -> f NatType -> f tp1 -> App ext f ('VectorType tp1)
VectorReplicate TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr e NatType
n e tp
v)
instance LitExpr e (FunctionHandleType args ret) (FnHandle args ret) where
litExpr :: IsExpr e => FnHandle args ret -> e (FunctionHandleType args ret)
litExpr FnHandle args ret
h = App (ExprExt e) e (FunctionHandleType args ret)
-> e (FunctionHandleType args ret)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (FnHandle args ret
-> App (ExprExt e) e (FunctionHandleType args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) ext
(f :: CrucibleType -> Type).
FnHandle args ret -> App ext f ('FunctionHandleType args ret)
HandleLit FnHandle args ret
h)
closure :: ( IsExpr e
, KnownRepr TypeRepr tp
, KnownRepr TypeRepr ret
, KnownCtx TypeRepr args
)
=> e (FunctionHandleType (args::>tp) ret)
-> e tp
-> e (FunctionHandleType args ret)
closure :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType)
(ret :: CrucibleType) (args :: Ctx CrucibleType).
(IsExpr e, KnownRepr TypeRepr tp, KnownRepr TypeRepr ret,
KnownCtx TypeRepr args) =>
e (FunctionHandleType (args ::> tp) ret)
-> e tp -> e (FunctionHandleType args ret)
closure e (FunctionHandleType (args ::> tp) ret)
h e tp
a = App (ExprExt e) e (FunctionHandleType args ret)
-> e (FunctionHandleType args ret)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (CtxRepr args
-> TypeRepr ret
-> e (FunctionHandleType (args ::> tp) ret)
-> TypeRepr tp
-> e tp
-> App (ExprExt e) e (FunctionHandleType args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
(f :: CrucibleType -> Type) (tp1 :: CrucibleType) ext.
CtxRepr args
-> TypeRepr ret
-> f (FunctionHandleType (args ::> tp1) ret)
-> TypeRepr tp1
-> f tp1
-> App ext f ('FunctionHandleType args ret)
Closure CtxRepr args
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr TypeRepr ret
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr e (FunctionHandleType (args ::> tp) ret)
h TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr e tp
a)
emptyIdentValueMap :: KnownRepr TypeRepr tp => IsExpr e => e (StringMapType tp)
emptyIdentValueMap :: forall (tp :: CrucibleType) (e :: CrucibleType -> Type).
(KnownRepr TypeRepr tp, IsExpr e) =>
e (StringMapType tp)
emptyIdentValueMap = App (ExprExt e) e (StringMapType tp) -> e (StringMapType tp)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (TypeRepr tp -> App (ExprExt e) e (StringMapType tp)
forall (tp1 :: CrucibleType) ext (f :: CrucibleType -> Type).
TypeRepr tp1 -> App ext f ('StringMapType tp1)
EmptyStringMap TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr)
setIdentValue :: (IsExpr e, KnownRepr TypeRepr tp)
=> e (StringMapType tp)
-> Text
-> e (MaybeType tp)
-> e (StringMapType tp)
setIdentValue :: forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(IsExpr e, KnownRepr TypeRepr tp) =>
e (StringMapType tp)
-> Text -> e (MaybeType tp) -> e (StringMapType tp)
setIdentValue e (StringMapType tp)
m Text
i e (MaybeType tp)
v = App (ExprExt e) e (StringMapType tp) -> e (StringMapType tp)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (TypeRepr tp
-> e (StringMapType tp)
-> e (StringType Unicode)
-> e (MaybeType tp)
-> App (ExprExt e) e (StringMapType tp)
forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp1
-> f (StringMapType tp1)
-> f (StringType Unicode)
-> f (MaybeType tp1)
-> App ext f (StringMapType tp1)
InsertStringMapEntry TypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr e (StringMapType tp)
m (Text -> e (StringType Unicode)
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Text
i) e (MaybeType tp)
v)
mkStruct :: IsExpr e
=> CtxRepr ctx
-> Ctx.Assignment e ctx
-> e (StructType ctx)
mkStruct :: forall (e :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
IsExpr e =>
CtxRepr ctx -> Assignment e ctx -> e (StructType ctx)
mkStruct CtxRepr ctx
tps Assignment e ctx
asgn = App (ExprExt e) e (StructType ctx) -> e (StructType ctx)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (CtxRepr ctx
-> Assignment e ctx -> App (ExprExt e) e (StructType ctx)
forall (ctx :: Ctx CrucibleType) (f :: CrucibleType -> Type) ext.
CtxRepr ctx -> Assignment f ctx -> App ext f ('StructType ctx)
MkStruct CtxRepr ctx
tps Assignment e ctx
asgn)
getStruct :: (IsExpr e)
=> Ctx.Index ctx tp
-> e (StructType ctx)
-> e tp
getStruct :: forall (e :: CrucibleType -> Type) (ctx :: Ctx CrucibleType)
(tp :: CrucibleType).
IsExpr e =>
Index ctx tp -> e (StructType ctx) -> e tp
getStruct Index ctx tp
i e (StructType ctx)
s
| Just (MkStruct CtxRepr ctx
_ Assignment e ctx
asgn) <- e (StructType ctx) -> Maybe (App (ExprExt e) e (StructType ctx))
forall (tp :: CrucibleType). e tp -> Maybe (App (ExprExt e) e tp)
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> Maybe (App (ExprExt e) e tp)
asApp e (StructType ctx)
s = Assignment e ctx
asgn Assignment e ctx -> Index ctx tp -> e tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
Index ctx tp
i
| Just (SetStruct CtxRepr ctx
_ e ('StructType ctx)
s' Index ctx tp1
i' e tp1
x) <- e (StructType ctx) -> Maybe (App (ExprExt e) e (StructType ctx))
forall (tp :: CrucibleType). e tp -> Maybe (App (ExprExt e) e tp)
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> Maybe (App (ExprExt e) e tp)
asApp e (StructType ctx)
s =
case Index ctx tp -> Index ctx tp1 -> Maybe (tp :~: tp1)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Index ctx a -> Index ctx b -> Maybe (a :~: b)
testEquality Index ctx tp
i Index ctx tp1
Index ctx tp1
i' of
Just tp :~: tp1
Refl -> e tp
e tp1
x
Maybe (tp :~: tp1)
Nothing -> Index ctx tp -> e (StructType ctx) -> e tp
forall (e :: CrucibleType -> Type) (ctx :: Ctx CrucibleType)
(tp :: CrucibleType).
IsExpr e =>
Index ctx tp -> e (StructType ctx) -> e tp
getStruct Index ctx tp
i e (StructType ctx)
e ('StructType ctx)
s'
| Bool
otherwise =
case e (StructType ctx) -> TypeRepr (StructType ctx)
forall (tp :: CrucibleType). e tp -> TypeRepr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> TypeRepr tp
exprType e (StructType ctx)
s of
StructRepr CtxRepr ctx
tps -> App (ExprExt e) e tp -> e tp
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (e (StructType ctx)
-> Index ctx tp -> TypeRepr tp -> App (ExprExt e) e tp
forall (f :: CrucibleType -> Type) (ctx :: Ctx CrucibleType)
(tp :: CrucibleType) ext.
f (StructType ctx) -> Index ctx tp -> TypeRepr tp -> App ext f tp
GetStruct e (StructType ctx)
s Index ctx tp
i (CtxRepr ctx
tps CtxRepr ctx -> Index ctx tp -> TypeRepr tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
Index ctx tp
i))
setStruct :: IsExpr e
=> CtxRepr ctx
-> e (StructType ctx)
-> Ctx.Index ctx tp
-> e tp
-> e (StructType ctx)
setStruct :: forall (e :: CrucibleType -> Type) (ctx :: Ctx CrucibleType)
(tp :: CrucibleType).
IsExpr e =>
CtxRepr ctx
-> e (StructType ctx) -> Index ctx tp -> e tp -> e (StructType ctx)
setStruct CtxRepr ctx
tps e (StructType ctx)
s Index ctx tp
i e tp
x
| Just (MkStruct CtxRepr ctx
_ Assignment e ctx
asgn) <- e (StructType ctx) -> Maybe (App (ExprExt e) e (StructType ctx))
forall (tp :: CrucibleType). e tp -> Maybe (App (ExprExt e) e tp)
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
e tp -> Maybe (App (ExprExt e) e tp)
asApp e (StructType ctx)
s = App (ExprExt e) e (StructType ctx) -> e (StructType ctx)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (CtxRepr ctx
-> Assignment e ctx -> App (ExprExt e) e (StructType ctx)
forall (ctx :: Ctx CrucibleType) (f :: CrucibleType -> Type) ext.
CtxRepr ctx -> Assignment f ctx -> App ext f ('StructType ctx)
MkStruct CtxRepr ctx
tps (Assignment e ctx
asgn Assignment e ctx
-> (Assignment e ctx -> Assignment e ctx) -> Assignment e ctx
forall a b. a -> (a -> b) -> b
& IndexF (Assignment e ctx) tp
-> Traversal' (Assignment e ctx) (IxValueF (Assignment e ctx) tp)
forall k m (x :: k).
IxedF k m =>
IndexF m x -> Traversal' m (IxValueF m x)
forall (x :: CrucibleType).
IndexF (Assignment e ctx) x
-> Traversal' (Assignment e ctx) (IxValueF (Assignment e ctx) x)
ixF IndexF (Assignment e ctx) tp
Index ctx tp
i ((IxValueF (Assignment e ctx) tp -> Identity (e tp))
-> Assignment e ctx -> Identity (Assignment e ctx))
-> e tp -> Assignment e ctx -> Assignment e ctx
forall s t a b. ASetter s t a b -> b -> s -> t
.~ e tp
x))
| Bool
otherwise = App (ExprExt e) e (StructType ctx) -> e (StructType ctx)
forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (CtxRepr ctx
-> e (StructType ctx)
-> Index ctx tp
-> e tp
-> App (ExprExt e) e (StructType ctx)
forall (ctx :: Ctx CrucibleType) (f :: CrucibleType -> Type)
(tp1 :: CrucibleType) ext.
CtxRepr ctx
-> f (StructType ctx)
-> Index ctx tp1
-> f tp1
-> App ext f (StructType ctx)
SetStruct CtxRepr ctx
tps e (StructType ctx)
s Index ctx tp
i e tp
x)
bigEndianStore
:: (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (BVType valWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
bigEndianStore :: forall (expr :: CrucibleType -> Type) (addrWidth :: Natural)
(valWidth :: Natural) (cellWidth :: Natural).
(IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) =>
NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (BVType valWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
bigEndianStore NatRepr addrWidth
addrWidth NatRepr cellWidth
cellWidth NatRepr valWidth
valWidth Int
num expr (BVType addrWidth)
basePtr expr (BVType valWidth)
v expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap = Int -> expr (WordMapType addrWidth (BaseBVType cellWidth))
go Int
num
where go :: Int -> expr (WordMapType addrWidth (BaseBVType cellWidth))
go Int
0 = expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap
go Int
n
| Just (Some NatRepr x
idx) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat (Integer -> Maybe (Some NatRepr))
-> Integer -> Maybe (Some NatRepr)
forall a b. (a -> b) -> a -> b
$ (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
numInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
n)) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (NatRepr cellWidth -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr cellWidth
cellWidth)
, Just LeqProof (x + cellWidth) valWidth
LeqProof <- NatRepr (x + cellWidth)
-> NatRepr valWidth -> Maybe (LeqProof (x + cellWidth) valWidth)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr x -> NatRepr cellWidth -> NatRepr (x + cellWidth)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
idx NatRepr cellWidth
cellWidth) NatRepr valWidth
valWidth
= App
(ExprExt expr) expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App
(ExprExt expr) expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth)))
-> App
(ExprExt expr) expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> BaseTypeRepr (BaseBVType cellWidth)
-> expr (BVType addrWidth)
-> expr (BaseToType (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> App
(ExprExt expr) expr (WordMapType addrWidth (BaseBVType cellWidth))
forall (w :: Natural) (tp1 :: BaseType) (f :: CrucibleType -> Type)
ext.
(1 <= w) =>
NatRepr w
-> BaseTypeRepr tp1
-> f (BVType w)
-> f (BaseToType tp1)
-> f (WordMapType w tp1)
-> App ext f (WordMapType w tp1)
InsertWordMap NatRepr addrWidth
addrWidth (NatRepr cellWidth -> BaseTypeRepr (BaseBVType cellWidth)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr cellWidth
cellWidth)
(App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> expr (BVType addrWidth)
-> expr (BVType addrWidth)
-> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) (f :: CrucibleType -> Type) ext.
(1 <= w) =>
NatRepr w -> f (BVType w) -> f (BVType w) -> App ext f (BVType w)
BVAdd NatRepr addrWidth
addrWidth expr (BVType addrWidth)
basePtr (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> BV addrWidth -> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr addrWidth
addrWidth (NatRepr addrWidth -> Integer -> BV addrWidth
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr addrWidth
addrWidth (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)))))
(App (ExprExt expr) expr (BaseToType (BaseBVType cellWidth))
-> expr (BaseToType (BaseBVType cellWidth))
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BaseToType (BaseBVType cellWidth))
-> expr (BaseToType (BaseBVType cellWidth)))
-> App (ExprExt expr) expr (BaseToType (BaseBVType cellWidth))
-> expr (BaseToType (BaseBVType cellWidth))
forall a b. (a -> b) -> a -> b
$ NatRepr x
-> NatRepr cellWidth
-> NatRepr valWidth
-> expr (BVType valWidth)
-> App (ExprExt expr) expr (BaseToType (BaseBVType cellWidth))
forall (w :: Natural) (len :: Natural) (idx :: Natural)
(f :: CrucibleType -> Type) ext.
(1 <= w, 1 <= len, (idx + len) <= w) =>
NatRepr idx
-> NatRepr len
-> NatRepr w
-> f (BVType w)
-> App ext f ('BaseToType (BaseBVType len))
BVSelect NatRepr x
idx NatRepr cellWidth
cellWidth NatRepr valWidth
valWidth expr (BVType valWidth)
v)
(Int -> expr (WordMapType addrWidth (BaseBVType cellWidth))
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
go Int
_ = [Char] -> expr (WordMapType addrWidth (BaseBVType cellWidth))
forall a. HasCallStack => [Char] -> a
error [Char]
"bad size parameters in bigEndianStore!"
littleEndianStore
:: (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (BVType valWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
littleEndianStore :: forall (expr :: CrucibleType -> Type) (addrWidth :: Natural)
(valWidth :: Natural) (cellWidth :: Natural).
(IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) =>
NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (BVType valWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
littleEndianStore NatRepr addrWidth
addrWidth NatRepr cellWidth
cellWidth NatRepr valWidth
valWidth Int
num expr (BVType addrWidth)
basePtr expr (BVType valWidth)
v expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap = Int -> expr (WordMapType addrWidth (BaseBVType cellWidth))
go Int
num
where go :: Int -> expr (WordMapType addrWidth (BaseBVType cellWidth))
go Int
0 = expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap
go Int
n
| Just (Some NatRepr x
idx) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat (Integer -> Maybe (Some NatRepr))
-> Integer -> Maybe (Some NatRepr)
forall a b. (a -> b) -> a -> b
$ (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (NatRepr cellWidth -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr cellWidth
cellWidth)
, Just LeqProof (x + cellWidth) valWidth
LeqProof <- NatRepr (x + cellWidth)
-> NatRepr valWidth -> Maybe (LeqProof (x + cellWidth) valWidth)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr x -> NatRepr cellWidth -> NatRepr (x + cellWidth)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
idx NatRepr cellWidth
cellWidth) NatRepr valWidth
valWidth
= App
(ExprExt expr) expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App
(ExprExt expr) expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth)))
-> App
(ExprExt expr) expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> BaseTypeRepr (BaseBVType cellWidth)
-> expr (BVType addrWidth)
-> expr (BaseToType (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> App
(ExprExt expr) expr (WordMapType addrWidth (BaseBVType cellWidth))
forall (w :: Natural) (tp1 :: BaseType) (f :: CrucibleType -> Type)
ext.
(1 <= w) =>
NatRepr w
-> BaseTypeRepr tp1
-> f (BVType w)
-> f (BaseToType tp1)
-> f (WordMapType w tp1)
-> App ext f (WordMapType w tp1)
InsertWordMap NatRepr addrWidth
addrWidth (NatRepr cellWidth -> BaseTypeRepr (BaseBVType cellWidth)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr cellWidth
cellWidth)
(App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> expr (BVType addrWidth)
-> expr (BVType addrWidth)
-> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) (f :: CrucibleType -> Type) ext.
(1 <= w) =>
NatRepr w -> f (BVType w) -> f (BVType w) -> App ext f (BVType w)
BVAdd NatRepr addrWidth
addrWidth expr (BVType addrWidth)
basePtr (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> BV addrWidth -> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr addrWidth
addrWidth (NatRepr addrWidth -> Integer -> BV addrWidth
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr addrWidth
addrWidth (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)))))
(App (ExprExt expr) expr (BaseToType (BaseBVType cellWidth))
-> expr (BaseToType (BaseBVType cellWidth))
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BaseToType (BaseBVType cellWidth))
-> expr (BaseToType (BaseBVType cellWidth)))
-> App (ExprExt expr) expr (BaseToType (BaseBVType cellWidth))
-> expr (BaseToType (BaseBVType cellWidth))
forall a b. (a -> b) -> a -> b
$ NatRepr x
-> NatRepr cellWidth
-> NatRepr valWidth
-> expr (BVType valWidth)
-> App (ExprExt expr) expr (BaseToType (BaseBVType cellWidth))
forall (w :: Natural) (len :: Natural) (idx :: Natural)
(f :: CrucibleType -> Type) ext.
(1 <= w, 1 <= len, (idx + len) <= w) =>
NatRepr idx
-> NatRepr len
-> NatRepr w
-> f (BVType w)
-> App ext f ('BaseToType (BaseBVType len))
BVSelect NatRepr x
idx NatRepr cellWidth
cellWidth NatRepr valWidth
valWidth expr (BVType valWidth)
v)
(Int -> expr (WordMapType addrWidth (BaseBVType cellWidth))
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
go Int
_ = [Char] -> expr (WordMapType addrWidth (BaseBVType cellWidth))
forall a. HasCallStack => [Char] -> a
error [Char]
"bad size parameters in littleEndianStore!"
concatExprs :: forall w a expr
. (IsExpr expr, 1 <= w)
=> NatRepr w
-> [expr (BVType w)]
-> (forall w'. (1 <= w') => NatRepr w' -> expr (BVType w') -> a)
-> a
concatExprs :: forall (w :: Natural) a (expr :: CrucibleType -> Type).
(IsExpr expr, 1 <= w) =>
NatRepr w
-> [expr (BVType w)]
-> (forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a)
-> a
concatExprs NatRepr w
_ [] = \forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Cannot concatenate 0 elements together"
concatExprs NatRepr w
w (expr (BVType w)
a:[expr (BVType w)]
as) = expr (BVType w)
-> [expr (BVType w)]
-> (forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a)
-> a
(1 <= w) =>
expr (BVType w)
-> [expr (BVType w)]
-> (forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a)
-> a
go expr (BVType w)
a [expr (BVType w)]
as
where go :: (1 <= w)
=> expr (BVType w)
-> [expr (BVType w)]
-> (forall w'. (1 <= w') => NatRepr w' -> expr (BVType w') -> a)
-> a
go :: (1 <= w) =>
expr (BVType w)
-> [expr (BVType w)]
-> (forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a)
-> a
go expr (BVType w)
x0 [] forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a
k = NatRepr w -> expr (BVType w) -> a
forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a
k NatRepr w
w expr (BVType w)
x0
go expr (BVType w)
x0 (expr (BVType w)
x:[expr (BVType w)]
xs) forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a
k = expr (BVType w)
-> [expr (BVType w)]
-> (forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a)
-> a
(1 <= w) =>
expr (BVType w)
-> [expr (BVType w)]
-> (forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a)
-> a
go expr (BVType w)
x [expr (BVType w)]
xs (\(NatRepr w'
w'::NatRepr w') expr (BVType w')
z ->
LeqProof 1 (w + w') -> ((1 <= (w + w')) => a) -> a
forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (LeqProof 1 w -> NatRepr w' -> LeqProof 1 (w + w')
forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
(p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof NatRepr w'
w' :: LeqProof 1 (w+w'))
(NatRepr (w + w') -> expr (BVType (w + w')) -> a
forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a
k (NatRepr w -> NatRepr w' -> NatRepr (w + w')
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr w
w NatRepr w'
w') (App (ExprExt expr) expr (BVType (w + w')) -> expr (BVType (w + w'))
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType (w + w'))
-> expr (BVType (w + w')))
-> App (ExprExt expr) expr (BVType (w + w'))
-> expr (BVType (w + w'))
forall a b. (a -> b) -> a -> b
$ NatRepr w
-> NatRepr w'
-> expr (BVType w)
-> expr (BVType w')
-> App (ExprExt expr) expr (BVType (w + w'))
forall (u :: Natural) (v :: Natural) (f :: CrucibleType -> Type)
ext.
(1 <= u, 1 <= v, 1 <= (u + v)) =>
NatRepr u
-> NatRepr v
-> f (BVType u)
-> f (BVType v)
-> App ext f ('BaseToType (BaseBVType (u + v)))
BVConcat NatRepr w
w NatRepr w'
w' expr (BVType w)
x0 expr (BVType w')
z)))
bigEndianLoad
:: (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType valWidth)
bigEndianLoad :: forall (expr :: CrucibleType -> Type) (addrWidth :: Natural)
(valWidth :: Natural) (cellWidth :: Natural).
(IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) =>
NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType valWidth)
bigEndianLoad NatRepr addrWidth
addrWidth NatRepr cellWidth
cellWidth NatRepr valWidth
valWidth Int
num expr (BVType addrWidth)
basePtr expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap =
let segs :: [expr ('BaseToType (BaseBVType cellWidth))]
segs = [ App (ExprExt expr) expr ('BaseToType (BaseBVType cellWidth))
-> expr ('BaseToType (BaseBVType cellWidth))
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr ('BaseToType (BaseBVType cellWidth))
-> expr ('BaseToType (BaseBVType cellWidth)))
-> App (ExprExt expr) expr ('BaseToType (BaseBVType cellWidth))
-> expr ('BaseToType (BaseBVType cellWidth))
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr (BaseBVType cellWidth)
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> App (ExprExt expr) expr ('BaseToType (BaseBVType cellWidth))
forall (w :: Natural) (tp1 :: BaseType) (f :: CrucibleType -> Type)
ext.
(1 <= w) =>
BaseTypeRepr tp1
-> f (BVType w)
-> f (WordMapType w tp1)
-> App ext f ('BaseToType tp1)
LookupWordMap (NatRepr cellWidth -> BaseTypeRepr (BaseBVType cellWidth)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr cellWidth
cellWidth)
(App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> expr (BVType addrWidth)
-> expr (BVType addrWidth)
-> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) (f :: CrucibleType -> Type) ext.
(1 <= w) =>
NatRepr w -> f (BVType w) -> f (BVType w) -> App ext f (BVType w)
BVAdd NatRepr addrWidth
addrWidth expr (BVType addrWidth)
basePtr
(App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> BV addrWidth -> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr addrWidth
addrWidth BV addrWidth
i))
expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap
| BV addrWidth
i <- BV addrWidth -> BV addrWidth -> [BV addrWidth]
forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned (NatRepr addrWidth -> BV addrWidth
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr addrWidth
addrWidth) (NatRepr addrWidth -> Integer -> BV addrWidth
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr addrWidth
addrWidth (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
numInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)))
] in
NatRepr cellWidth
-> [expr ('BaseToType (BaseBVType cellWidth))]
-> (forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth)
forall (w :: Natural) a (expr :: CrucibleType -> Type).
(IsExpr expr, 1 <= w) =>
NatRepr w
-> [expr (BVType w)]
-> (forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a)
-> a
concatExprs NatRepr cellWidth
cellWidth [expr ('BaseToType (BaseBVType cellWidth))]
segs ((forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth))
-> (forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth)
forall a b. (a -> b) -> a -> b
$ \NatRepr w'
w expr (BVType w')
x ->
case NatRepr w' -> NatRepr valWidth -> Maybe (w' :~: valWidth)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w'
w NatRepr valWidth
valWidth of
Just w' :~: valWidth
Refl -> expr (BVType valWidth)
expr (BVType w')
x
Maybe (w' :~: valWidth)
Nothing -> [Char] -> expr (BVType valWidth)
forall a. HasCallStack => [Char] -> a
error [Char]
"bad size parameters in bigEndianLoad!"
bigEndianLoadDef
:: (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType cellWidth)
-> expr (BVType valWidth)
bigEndianLoadDef :: forall (expr :: CrucibleType -> Type) (addrWidth :: Natural)
(valWidth :: Natural) (cellWidth :: Natural).
(IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) =>
NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType cellWidth)
-> expr (BVType valWidth)
bigEndianLoadDef NatRepr addrWidth
addrWidth NatRepr cellWidth
cellWidth NatRepr valWidth
valWidth Int
num expr (BVType addrWidth)
basePtr expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap expr (BVType cellWidth)
defVal =
let segs :: [expr (BVType cellWidth)]
segs = [ App (ExprExt expr) expr (BVType cellWidth)
-> expr (BVType cellWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType cellWidth)
-> expr (BVType cellWidth))
-> App (ExprExt expr) expr (BVType cellWidth)
-> expr (BVType cellWidth)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr (BaseBVType cellWidth)
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType cellWidth)
-> App (ExprExt expr) expr (BVType cellWidth)
forall (w :: Natural) (tp1 :: BaseType) (f :: CrucibleType -> Type)
ext.
(1 <= w) =>
BaseTypeRepr tp1
-> f (BVType w)
-> f (WordMapType w tp1)
-> f (BaseToType tp1)
-> App ext f (BaseToType tp1)
LookupWordMapWithDefault (NatRepr cellWidth -> BaseTypeRepr (BaseBVType cellWidth)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr cellWidth
cellWidth)
(App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> expr (BVType addrWidth)
-> expr (BVType addrWidth)
-> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) (f :: CrucibleType -> Type) ext.
(1 <= w) =>
NatRepr w -> f (BVType w) -> f (BVType w) -> App ext f (BVType w)
BVAdd NatRepr addrWidth
addrWidth expr (BVType addrWidth)
basePtr
(App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> BV addrWidth -> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr addrWidth
addrWidth BV addrWidth
i))
expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap
expr (BVType cellWidth)
defVal
| BV addrWidth
i <- BV addrWidth -> BV addrWidth -> [BV addrWidth]
forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned (NatRepr addrWidth -> BV addrWidth
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr addrWidth
addrWidth) (NatRepr addrWidth -> Integer -> BV addrWidth
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr addrWidth
addrWidth (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
numInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)))
] in
NatRepr cellWidth
-> [expr (BVType cellWidth)]
-> (forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth)
forall (w :: Natural) a (expr :: CrucibleType -> Type).
(IsExpr expr, 1 <= w) =>
NatRepr w
-> [expr (BVType w)]
-> (forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a)
-> a
concatExprs NatRepr cellWidth
cellWidth [expr (BVType cellWidth)]
segs ((forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth))
-> (forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth)
forall a b. (a -> b) -> a -> b
$ \NatRepr w'
w expr (BVType w')
x ->
case NatRepr w' -> NatRepr valWidth -> Maybe (w' :~: valWidth)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w'
w NatRepr valWidth
valWidth of
Just w' :~: valWidth
Refl -> expr (BVType valWidth)
expr (BVType w')
x
Maybe (w' :~: valWidth)
Nothing -> [Char] -> expr (BVType valWidth)
forall a. HasCallStack => [Char] -> a
error [Char]
"bad size parameters in bigEndianLoadDef!"
littleEndianLoad
:: (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType valWidth)
littleEndianLoad :: forall (expr :: CrucibleType -> Type) (addrWidth :: Natural)
(valWidth :: Natural) (cellWidth :: Natural).
(IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) =>
NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType valWidth)
littleEndianLoad NatRepr addrWidth
addrWidth NatRepr cellWidth
cellWidth NatRepr valWidth
valWidth Int
num expr (BVType addrWidth)
basePtr expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap =
let segs :: [expr ('BaseToType (BaseBVType cellWidth))]
segs = [ App (ExprExt expr) expr ('BaseToType (BaseBVType cellWidth))
-> expr ('BaseToType (BaseBVType cellWidth))
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr ('BaseToType (BaseBVType cellWidth))
-> expr ('BaseToType (BaseBVType cellWidth)))
-> App (ExprExt expr) expr ('BaseToType (BaseBVType cellWidth))
-> expr ('BaseToType (BaseBVType cellWidth))
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr (BaseBVType cellWidth)
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> App (ExprExt expr) expr ('BaseToType (BaseBVType cellWidth))
forall (w :: Natural) (tp1 :: BaseType) (f :: CrucibleType -> Type)
ext.
(1 <= w) =>
BaseTypeRepr tp1
-> f (BVType w)
-> f (WordMapType w tp1)
-> App ext f ('BaseToType tp1)
LookupWordMap (NatRepr cellWidth -> BaseTypeRepr (BaseBVType cellWidth)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr cellWidth
cellWidth)
(App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> expr (BVType addrWidth)
-> expr (BVType addrWidth)
-> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) (f :: CrucibleType -> Type) ext.
(1 <= w) =>
NatRepr w -> f (BVType w) -> f (BVType w) -> App ext f (BVType w)
BVAdd NatRepr addrWidth
addrWidth expr (BVType addrWidth)
basePtr
(App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> BV addrWidth -> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr addrWidth
addrWidth BV addrWidth
i))
expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap
| BV addrWidth
i <- [BV addrWidth] -> [BV addrWidth]
forall a. [a] -> [a]
reverse ([BV addrWidth] -> [BV addrWidth])
-> [BV addrWidth] -> [BV addrWidth]
forall a b. (a -> b) -> a -> b
$ BV addrWidth -> BV addrWidth -> [BV addrWidth]
forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned (NatRepr addrWidth -> BV addrWidth
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr addrWidth
addrWidth) (NatRepr addrWidth -> Integer -> BV addrWidth
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr addrWidth
addrWidth (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
numInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)))
] in
NatRepr cellWidth
-> [expr ('BaseToType (BaseBVType cellWidth))]
-> (forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth)
forall (w :: Natural) a (expr :: CrucibleType -> Type).
(IsExpr expr, 1 <= w) =>
NatRepr w
-> [expr (BVType w)]
-> (forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a)
-> a
concatExprs NatRepr cellWidth
cellWidth [expr ('BaseToType (BaseBVType cellWidth))]
segs ((forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth))
-> (forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth)
forall a b. (a -> b) -> a -> b
$ \NatRepr w'
w expr (BVType w')
x ->
case NatRepr w' -> NatRepr valWidth -> Maybe (w' :~: valWidth)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w'
w NatRepr valWidth
valWidth of
Just w' :~: valWidth
Refl -> expr (BVType valWidth)
expr (BVType w')
x
Maybe (w' :~: valWidth)
Nothing -> [Char] -> expr (BVType valWidth)
forall a. HasCallStack => [Char] -> a
error [Char]
"bad size parameters in littleEndianLoad!"
littleEndianLoadDef
:: (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType cellWidth)
-> expr (BVType valWidth)
littleEndianLoadDef :: forall (expr :: CrucibleType -> Type) (addrWidth :: Natural)
(valWidth :: Natural) (cellWidth :: Natural).
(IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) =>
NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType cellWidth)
-> expr (BVType valWidth)
littleEndianLoadDef NatRepr addrWidth
addrWidth NatRepr cellWidth
cellWidth NatRepr valWidth
valWidth Int
num expr (BVType addrWidth)
basePtr expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap expr (BVType cellWidth)
defVal =
let segs :: [expr (BVType cellWidth)]
segs = [ App (ExprExt expr) expr (BVType cellWidth)
-> expr (BVType cellWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType cellWidth)
-> expr (BVType cellWidth))
-> App (ExprExt expr) expr (BVType cellWidth)
-> expr (BVType cellWidth)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr (BaseBVType cellWidth)
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType cellWidth)
-> App (ExprExt expr) expr (BVType cellWidth)
forall (w :: Natural) (tp1 :: BaseType) (f :: CrucibleType -> Type)
ext.
(1 <= w) =>
BaseTypeRepr tp1
-> f (BVType w)
-> f (WordMapType w tp1)
-> f (BaseToType tp1)
-> App ext f (BaseToType tp1)
LookupWordMapWithDefault (NatRepr cellWidth -> BaseTypeRepr (BaseBVType cellWidth)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr cellWidth
cellWidth)
(App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> expr (BVType addrWidth)
-> expr (BVType addrWidth)
-> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) (f :: CrucibleType -> Type) ext.
(1 <= w) =>
NatRepr w -> f (BVType w) -> f (BVType w) -> App ext f (BVType w)
BVAdd NatRepr addrWidth
addrWidth expr (BVType addrWidth)
basePtr
(App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall (tp :: CrucibleType). App (ExprExt expr) expr tp -> expr tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth))
-> App (ExprExt expr) expr (BVType addrWidth)
-> expr (BVType addrWidth)
forall a b. (a -> b) -> a -> b
$ NatRepr addrWidth
-> BV addrWidth -> App (ExprExt expr) expr (BVType addrWidth)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr addrWidth
addrWidth BV addrWidth
i))
expr (WordMapType addrWidth (BaseBVType cellWidth))
wordMap
expr (BVType cellWidth)
defVal
| BV addrWidth
i <- [BV addrWidth] -> [BV addrWidth]
forall a. [a] -> [a]
reverse ([BV addrWidth] -> [BV addrWidth])
-> [BV addrWidth] -> [BV addrWidth]
forall a b. (a -> b) -> a -> b
$ BV addrWidth -> BV addrWidth -> [BV addrWidth]
forall (w :: Natural). BV w -> BV w -> [BV w]
BV.enumFromToUnsigned (NatRepr addrWidth -> BV addrWidth
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr addrWidth
addrWidth) (NatRepr addrWidth -> Integer -> BV addrWidth
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr addrWidth
addrWidth (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
numInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)))
] in
NatRepr cellWidth
-> [expr (BVType cellWidth)]
-> (forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth)
forall (w :: Natural) a (expr :: CrucibleType -> Type).
(IsExpr expr, 1 <= w) =>
NatRepr w
-> [expr (BVType w)]
-> (forall (w' :: Natural).
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> a)
-> a
concatExprs NatRepr cellWidth
cellWidth [expr (BVType cellWidth)]
segs ((forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth))
-> (forall {w' :: Natural}.
(1 <= w') =>
NatRepr w' -> expr (BVType w') -> expr (BVType valWidth))
-> expr (BVType valWidth)
forall a b. (a -> b) -> a -> b
$ \NatRepr w'
w expr (BVType w')
x ->
case NatRepr w' -> NatRepr valWidth -> Maybe (w' :~: valWidth)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w'
w NatRepr valWidth
valWidth of
Just w' :~: valWidth
Refl -> expr (BVType valWidth)
expr (BVType w')
x
Maybe (w' :~: valWidth)
Nothing -> [Char] -> expr (BVType valWidth)
forall a. HasCallStack => [Char] -> a
error [Char]
"bad size parameters in littleEndianLoadDef!"