-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Syntax
-- Description      : Provides a typeclass and methods for constructing
--                    AST expressions.
-- Copyright        : (c) Galois, Inc 2014
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module provides typeclasses and combinators for constructing AST
-- expressions.
------------------------------------------------------------------------
{-# 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
    -- * Booleans
  , true
  , false
  , notExpr
  , (.&&)
  , (.||)
    -- * Expression classes
  , EqExpr(..)
  , OrdExpr(..)
  , NumExpr(..)
  , LitExpr(..)
    -- * Natural numbers
  , ConvertableToNat(..)
    -- * Real numbers
  , rationalLit
  , natToReal
  , integerToReal
    -- * Complex real numbers
  , realToCplx
  , imagToCplx
  , realPart
  , imagPart
  , realLit
  , imagLit
  , natToCplx
    -- * Maybe
  , nothingValue
  , justValue
    -- * Vector
  , vectorSize
  , vectorLit
  , vectorGetEntry
  , vectorSetEntry
  , vectorIsEmpty
  , vecReplicate
    -- * Function handles
  , closure
    -- * IdentValueMap
  , emptyIdentValueMap
  , setIdentValue

  -- * Structs
  , mkStruct
  , getStruct
  , setStruct

  -- * Multibyte operations
  , 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

------------------------------------------------------------------------
-- IsExpr

-- | A typeclass for injecting applications into expressions.
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

-- | Inject an extension app into the expression type
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

-- | Test if an expression is formed from an extension app
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

------------------------------------------------------------------------
-- LitExpr

-- | An expression that embeds literal values of its type.
class LitExpr e tp ty | tp -> ty where
  litExpr :: IsExpr e => ty -> e tp

------------------------------------------------------------------------
-- Booleans

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 expression
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 expression
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 .||

------------------------------------------------------------------------
-- EqExpr

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 ./=

------------------------------------------------------------------------
-- OrdExpr

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 .>=

------------------------------------------------------------------------
-- NumExpr

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

------------------------------------------------------------------------
-- Nat

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)

------------------------------------------------------------------------
-- Integer

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)

------------------------------------------------------------------------
-- ConvertableToNat

class ConvertableToNat e tp where
  -- | Convert value of type to Nat.
  -- This may be partial, it is the responsibility of the calling
  -- code that it is correct for this type.
  toNat :: IsExpr e => e tp -> e NatType

------------------------------------------------------------------------
-- RealValType

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)

------------------------------------------------------------------------
-- ComplexRealType

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

------------------------------------------------------------------------
-- String

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))

------------------------------------------------------------------------
-- Maybe

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)

------------------------------------------------------------------------
-- Vector

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)

-- | Get the entry from a zero-based index.
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)

------------------------------------------------------------------------
-- Handles

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)


----------------------------------------------------------------------
-- IdentValueMap

-- | Initialize the ident value map to the given value.
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)

-- Update the value of the ident value map with the given value.
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)

-----------------------------------------------------------------------
-- Struct

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)



-------------------------------------------------------
-- Multibyte operations

bigEndianStore
   :: (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
   => NatRepr addrWidth
   -> NatRepr cellWidth
   -> NatRepr valWidth
   -> Int -- ^ number of bytes to write
   -> 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 -- ^ number of bytes to write
   -> 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 -- ^ number of bytes to load
   -> 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 -- ^ number of bytes to load
   -> 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 -- ^ number of bytes to load
   -> 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 -- ^ number of bytes to load
   -> 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!"