-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.Translation.Expr
-- Description      : Translation-time LLVM expressions
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
-----------------------------------------------------------------------

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE ImplicitParams        #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PatternGuards         #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE ViewPatterns          #-}

module Lang.Crucible.LLVM.Translation.Expr
  ( LLVMExpr(..)
  , ScalarView(..)
  , asScalar
  , asVectorWithType
  , asVector

  , pattern PointerExpr
  , pattern BitvectorAsPointerExpr
  , pointerAsBitvectorExpr

  , unpackOne
  , unpackVec
  , unpackArgs
  , zeroExpand
  , undefExpand
  , explodeVector

  , constToLLVMVal
  , transValue
  , transTypedValue
  , transTypeAndValue
  , liftConstant

  , callIsNull
  , callIntToBool
  , callAlloca
  , callPushFrame
  , callPopFrame
  , callPtrAddOffset
  , callPtrSubtract
  , callLoad
  , callStore
  ) where

import Control.Lens hiding ((:>))
import Control.Monad
import Control.Monad.Except
import qualified Data.ByteString as BS
import Data.Foldable (toList)
import qualified Data.List as List
--import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.String
import qualified Data.Vector as V
import Numeric.Natural
import GHC.Exts ( Proxy#, proxy# )

import qualified Data.BitVector.Sized as BV
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Context ( pattern (:>) )
import           Data.Parameterized.NatRepr as NatRepr
import           Data.Parameterized.Some
import           Data.Text (Text)

import qualified Text.LLVM.AST as L

import qualified Lang.Crucible.CFG.Core as C
import           Lang.Crucible.CFG.Expr
import           Lang.Crucible.CFG.Generator
import           Lang.Crucible.CFG.Extension ()

import           Lang.Crucible.LLVM.DataLayout
import           Lang.Crucible.LLVM.Extension
import           Lang.Crucible.LLVM.MemType
import           Lang.Crucible.LLVM.MemModel
import           Lang.Crucible.LLVM.Translation.Constant
import           Lang.Crucible.LLVM.Translation.Monad
import           Lang.Crucible.LLVM.Translation.Types
import           Lang.Crucible.LLVM.TypeContext

import           Lang.Crucible.Syntax
import           Lang.Crucible.Types

import           What4.InterpretedFloatingPoint (X86_80Val(..))

-------------------------------------------------------------------------
-- LLVMExpr
--
-- As noted in "Lang.Crucible.LLVM.Translation.Types", this code uses
-- a polymorphic continuation-passing style to convert to
-- strongly-typed Crucible types from less-strongly-typed LLVM
-- types. As part of that, the LLVM architecture (notably the pointer
-- width) must be unified between the outer context and the
-- continuation; the 'proxy#' arguments here and below represent a
-- 'Proxy# arch' type that is used to maintain that architecture
-- definition and corresponding pointer width for the conversions.

-- | An intermediate form of LLVM expressions that retains some structure
--   that would otherwise be more difficult to retain if we translated directly
--   into crucible expressions.
data LLVMExpr s (arch :: LLVMArch) where
   BaseExpr   :: TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
   ZeroExpr   :: MemType -> LLVMExpr s arch
   UndefExpr  :: MemType -> LLVMExpr s arch
   VecExpr    :: MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
   StructExpr :: Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch

instance Show (LLVMExpr s arch) where
  show :: LLVMExpr s arch -> String
show (BaseExpr TypeRepr tp
ty Expr LLVM s tp
x)  = Expr LLVM s tp -> String
forall k (f :: k -> Type) (tp :: k). ShowF f => f tp -> String
forall (tp :: CrucibleType). Expr LLVM s tp -> String
C.showF Expr LLVM s tp
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRepr tp -> String
forall a. Show a => a -> String
show TypeRepr tp
ty
  show (ZeroExpr MemType
mt)    = String
"<zero :" String -> ShowS
forall a. [a] -> [a] -> [a]
++ MemType -> String
forall a. Show a => a -> String
show MemType
mt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
  show (UndefExpr MemType
mt)   = String
"<undef :" String -> ShowS
forall a. [a] -> [a] -> [a]
++ MemType -> String
forall a. Show a => a -> String
show MemType
mt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
  show (VecExpr MemType
_mt Seq (LLVMExpr s arch)
xs) = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " ((LLVMExpr s arch -> String) -> [LLVMExpr s arch] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map LLVMExpr s arch -> String
forall a. Show a => a -> String
show (Seq (LLVMExpr s arch) -> [LLVMExpr s arch]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq (LLVMExpr s arch)
xs)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
  show (StructExpr Seq (MemType, LLVMExpr s arch)
xs)  = String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " (((MemType, LLVMExpr s arch) -> String)
-> [(MemType, LLVMExpr s arch)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (MemType, LLVMExpr s arch) -> String
forall {a} {a}. Show a => (a, a) -> String
f (Seq (MemType, LLVMExpr s arch) -> [(MemType, LLVMExpr s arch)]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq (MemType, LLVMExpr s arch)
xs)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
    where f :: (a, a) -> String
f (a
_mt,a
x) = a -> String
forall a. Show a => a -> String
show a
x


data ScalarView s (arch :: LLVMArch) where
  Scalar    :: Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
  NotScalar :: ScalarView s arch

-- | Examine an LLVM expression and return the corresponding
--   crucible expression, if it is a scalar.
asScalar :: (?lc :: TypeContext, HasPtrWidth (ArchWidth arch))
         => LLVMExpr s arch
         -> ScalarView s arch
asScalar :: forall (arch :: LLVMArch) s.
(?lc::TypeContext, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch -> ScalarView s arch
asScalar (BaseExpr TypeRepr tp
tp Expr LLVM s tp
xs)
  = Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
forall (arch :: LLVMArch) (tp :: CrucibleType) s.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
Scalar Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# TypeRepr tp
tp Expr LLVM s tp
xs
asScalar (ZeroExpr MemType
llvmtp)
  = let ?err = ?err::String -> ScalarView s arch
String -> ScalarView s arch
forall a. HasCallStack => String -> a
error
     in Proxy# arch
-> MemType
-> (forall {tp :: CrucibleType}.
    Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
-> ScalarView s arch
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
    Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
zeroExpand Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# MemType
llvmtp ((forall {tp :: CrucibleType}.
  Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
 -> ScalarView s arch)
-> (forall {tp :: CrucibleType}.
    Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
-> ScalarView s arch
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
archProxy TypeRepr tp
tpr Expr LLVM s tp
ex -> Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
forall (arch :: LLVMArch) (tp :: CrucibleType) s.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
Scalar Proxy# arch
archProxy TypeRepr tp
tpr Expr LLVM s tp
ex
asScalar (UndefExpr MemType
llvmtp)
  = let ?err = ?err::String -> ScalarView s arch
String -> ScalarView s arch
forall a. HasCallStack => String -> a
error
     in Proxy# arch
-> MemType
-> (forall {tp :: CrucibleType}.
    Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
-> ScalarView s arch
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
    Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
undefExpand Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# MemType
llvmtp ((forall {tp :: CrucibleType}.
  Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
 -> ScalarView s arch)
-> (forall {tp :: CrucibleType}.
    Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch)
-> ScalarView s arch
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
archProxy TypeRepr tp
tpr Expr LLVM s tp
ex -> Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
forall (arch :: LLVMArch) (tp :: CrucibleType) s.
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> ScalarView s arch
Scalar Proxy# arch
archProxy TypeRepr tp
tpr Expr LLVM s tp
ex
asScalar LLVMExpr s arch
_ = ScalarView s arch
forall s (arch :: LLVMArch). ScalarView s arch
NotScalar

-- | Turn the expression into an explicit vector.
asVectorWithType :: LLVMExpr s arch -> Maybe (MemType, Seq (LLVMExpr s arch))
asVectorWithType :: forall s (arch :: LLVMArch).
LLVMExpr s arch -> Maybe (MemType, Seq (LLVMExpr s arch))
asVectorWithType LLVMExpr s arch
v =
  case LLVMExpr s arch
v of
    ZeroExpr (VecType Natural
n MemType
t)  -> (MemType, Seq (LLVMExpr s arch))
-> Maybe (MemType, Seq (LLVMExpr s arch))
forall a. a -> Maybe a
Just (MemType
t, Int -> LLVMExpr s arch -> Seq (LLVMExpr s arch)
forall a. Int -> a -> Seq a
Seq.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
t))
    UndefExpr (VecType Natural
n MemType
t) -> (MemType, Seq (LLVMExpr s arch))
-> Maybe (MemType, Seq (LLVMExpr s arch))
forall a. a -> Maybe a
Just (MemType
t, Int -> LLVMExpr s arch -> Seq (LLVMExpr s arch)
forall a. Int -> a -> Seq a
Seq.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
t))
    VecExpr MemType
t Seq (LLVMExpr s arch)
s             -> (MemType, Seq (LLVMExpr s arch))
-> Maybe (MemType, Seq (LLVMExpr s arch))
forall a. a -> Maybe a
Just (MemType
t, Seq (LLVMExpr s arch)
s)
    LLVMExpr s arch
_                       -> Maybe (MemType, Seq (LLVMExpr s arch))
forall a. Maybe a
Nothing

asVector :: LLVMExpr s arch -> Maybe (Seq (LLVMExpr s arch))
asVector :: forall s (arch :: LLVMArch).
LLVMExpr s arch -> Maybe (Seq (LLVMExpr s arch))
asVector = ((MemType, Seq (LLVMExpr s arch)) -> Seq (LLVMExpr s arch))
-> Maybe (MemType, Seq (LLVMExpr s arch))
-> Maybe (Seq (LLVMExpr s arch))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (MemType, Seq (LLVMExpr s arch)) -> Seq (LLVMExpr s arch)
forall a b. (a, b) -> b
snd (Maybe (MemType, Seq (LLVMExpr s arch))
 -> Maybe (Seq (LLVMExpr s arch)))
-> (LLVMExpr s arch -> Maybe (MemType, Seq (LLVMExpr s arch)))
-> LLVMExpr s arch
-> Maybe (Seq (LLVMExpr s arch))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LLVMExpr s arch -> Maybe (MemType, Seq (LLVMExpr s arch))
forall s (arch :: LLVMArch).
LLVMExpr s arch -> Maybe (MemType, Seq (LLVMExpr s arch))
asVectorWithType


nullPointerExpr :: (HasPtrWidth w) => Expr LLVM s (LLVMPointerType w)
nullPointerExpr :: forall (w :: Natural) s.
HasPtrWidth w =>
Expr LLVM s (LLVMPointerType w)
nullPointerExpr = NatRepr w
-> Expr LLVM s NatType
-> Expr LLVM s (BVType w)
-> Expr LLVM s (LLVMPointerType w)
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s NatType
-> Expr LLVM s (BVType w)
-> Expr LLVM s (LLVMPointerType w)
PointerExpr NatRepr w
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (App LLVM (Expr LLVM s) NatType -> Expr LLVM s NatType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (Natural -> App LLVM (Expr LLVM s) NatType
forall ext (f :: CrucibleType -> Type).
Natural -> App ext f NatType
NatLit Natural
0)) (App LLVM (Expr LLVM s) (BVType w) -> Expr LLVM s (BVType w)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (NatRepr w -> BV w -> App LLVM (Expr LLVM s) (BVType w)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr w
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth)))

pattern PointerExpr
    :: (1 <= w)
    => NatRepr w
    -> Expr LLVM s NatType
    -> Expr LLVM s (BVType w)
    -> Expr LLVM s (LLVMPointerType w)
pattern $mPointerExpr :: forall {r} {w :: Natural} {s}.
(1 <= w) =>
Expr LLVM s (LLVMPointerType w)
-> (NatRepr w
    -> Expr LLVM s NatType -> Expr LLVM s (BVType w) -> r)
-> ((# #) -> r)
-> r
$bPointerExpr :: forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s NatType
-> Expr LLVM s (BVType w)
-> Expr LLVM s (LLVMPointerType w)
PointerExpr w blk off = App (ExtensionApp (LLVM_PointerExpr w blk off))

pattern BitvectorAsPointerExpr
    :: (1 <= w)
    => NatRepr w
    -> Expr LLVM s (BVType w)
    -> Expr LLVM s (LLVMPointerType w)
pattern $mBitvectorAsPointerExpr :: forall {r} {w :: Natural} {s}.
(1 <= w) =>
Expr LLVM s (LLVMPointerType w)
-> (NatRepr w -> Expr LLVM s (BVType w) -> r) -> ((# #) -> r) -> r
$bBitvectorAsPointerExpr :: forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr w ex = PointerExpr w (App (NatLit 0)) ex

pointerAsBitvectorExpr
    :: (1 <= w)
    => NatRepr w
    -> Expr LLVM s (LLVMPointerType w)
    -> LLVMGenerator s arch ret (Expr LLVM s (BVType w))
pointerAsBitvectorExpr :: forall (w :: Natural) s (arch :: LLVMArch) (ret :: CrucibleType).
(1 <= w) =>
NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s (BVType w))
pointerAsBitvectorExpr NatRepr w
_ (BitvectorAsPointerExpr NatRepr w
_ Expr LLVM s (BVType w)
ex) =
     Expr LLVM s (BVType w)
-> Generator
     LLVM s (LLVMState arch) ret IO (Expr LLVM s (BVType w))
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr LLVM s (BVType w)
ex
pointerAsBitvectorExpr NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex =
  do Expr LLVM s (LLVMPointerType w)
ex' <- Expr LLVM s (LLVMPointerType w)
-> Generator
     LLVM s (LLVMState arch) ret IO (Expr LLVM s (LLVMPointerType w))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forceEvaluation Expr LLVM s (LLVMPointerType w)
ex
     let blk :: Expr LLVM s NatType
blk = App LLVM (Expr LLVM s) NatType -> Expr LLVM s NatType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (ExprExtension LLVM (Expr LLVM s) NatType
-> App LLVM (Expr LLVM s) NatType
forall ext (f :: CrucibleType -> Type) (tp :: CrucibleType).
ExprExtension ext f tp -> App ext f tp
ExtensionApp (NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMExtensionExpr (Expr LLVM s) NatType
forall (w :: Natural) (a :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> a (LLVMPointerType w) -> LLVMExtensionExpr a NatType
LLVM_PointerBlock NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex'))
     let off :: Expr LLVM s (BVType w)
off = App LLVM (Expr LLVM s) (BVType w) -> Expr LLVM s (BVType w)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (ExprExtension LLVM (Expr LLVM s) (BVType w)
-> App LLVM (Expr LLVM s) (BVType w)
forall ext (f :: CrucibleType -> Type) (tp :: CrucibleType).
ExprExtension ext f tp -> App ext f tp
ExtensionApp (NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMExtensionExpr (Expr LLVM s) (BVType w)
forall (w :: Natural) (a :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w
-> a (LLVMPointerType w)
-> LLVMExtensionExpr a ('BaseToType (BaseBVType w))
LLVM_PointerOffset NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex'))
     Expr LLVM s BoolType
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s BoolType
-> Expr ext s (StringType Unicode) -> Generator ext s t ret m ()
assertExpr (Expr LLVM s NatType
blk Expr LLVM s NatType -> Expr LLVM s NatType -> Expr LLVM s BoolType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(EqExpr e tp, IsExpr e) =>
e tp -> e tp -> e BoolType
.== Natural -> Expr LLVM s NatType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Natural
0)
                (Text -> Expr LLVM s (StringType Unicode)
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Text
"Expected bitvector, but found pointer")
     Expr LLVM s (BVType w)
-> Generator
     LLVM s (LLVMState arch) ret IO (Expr LLVM s (BVType w))
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr LLVM s (BVType w)
off



-- | Given a list of LLVMExpressions, "unpack" them into an assignment
--   of crucible expressions.
unpackArgs :: forall s a arch
    . (?err :: String -> a
      ,HasPtrWidth (ArchWidth arch)
      )
   => [LLVMExpr s arch]
   -> (forall ctx. Proxy# arch -> CtxRepr ctx -> Ctx.Assignment (Expr LLVM s) ctx -> a)
   -> a
unpackArgs :: forall s a (arch :: LLVMArch).
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
[LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
unpackArgs = CtxRepr EmptyCtx
-> Assignment (Expr LLVM s) EmptyCtx
-> [LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx
-> Assignment (Expr LLVM s) ctx
-> [LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
go CtxRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment (Expr LLVM s) EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
 where go :: CtxRepr ctx
          -> Ctx.Assignment (Expr LLVM s) ctx
          -> [LLVMExpr s arch]
          -> (forall ctx'. Proxy# arch -> CtxRepr ctx' -> Ctx.Assignment (Expr LLVM s) ctx' -> a)
          -> a
       go :: forall (ctx :: Ctx CrucibleType).
CtxRepr ctx
-> Assignment (Expr LLVM s) ctx
-> [LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
go CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn [] forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a
k = Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a
forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn
       go CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn (LLVMExpr s arch
v:[LLVMExpr s arch]
vs) forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a
k = LLVMExpr s arch
-> (forall (tpr :: CrucibleType).
    Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch
-> (forall (tpr :: CrucibleType).
    Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
unpackOne LLVMExpr s arch
v (\Proxy# arch
_ TypeRepr tpr
tyr Expr LLVM s tpr
ex -> CtxRepr (ctx ::> tpr)
-> Assignment (Expr LLVM s) (ctx ::> tpr)
-> [LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx
-> Assignment (Expr LLVM s) ctx
-> [LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
go (CtxRepr ctx
ctx CtxRepr ctx -> TypeRepr tpr -> CtxRepr (ctx ::> tpr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> TypeRepr tpr
tyr) (Assignment (Expr LLVM s) ctx
asgn Assignment (Expr LLVM s) ctx
-> Expr LLVM s tpr -> Assignment (Expr LLVM s) (ctx ::> tpr)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> Expr LLVM s tpr
ex) [LLVMExpr s arch]
vs Proxy# arch -> CtxRepr ctx' -> Assignment (Expr LLVM s) ctx' -> a
forall (ctx :: Ctx CrucibleType).
Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a
k)

unpackOne
   :: (?err :: String -> a, HasPtrWidth (ArchWidth arch))
   => LLVMExpr s arch
   -> (forall tpr. Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
   -> a
unpackOne :: forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch
-> (forall (tpr :: CrucibleType).
    Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
unpackOne (BaseExpr TypeRepr tp
tyr Expr LLVM s tp
ex) forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k = Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# TypeRepr tp
tyr Expr LLVM s tp
ex
unpackOne (UndefExpr MemType
tp) forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k = Proxy# arch
-> MemType
-> (forall (tpr :: CrucibleType).
    Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
    Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
undefExpand Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# MemType
tp Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k
unpackOne (ZeroExpr MemType
tp) forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k = Proxy# arch
-> MemType
-> (forall (tpr :: CrucibleType).
    Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
    Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
zeroExpand Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# MemType
tp Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k
unpackOne (StructExpr Seq (MemType, LLVMExpr s arch)
vs) forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k =
  [LLVMExpr s arch]
-> (forall {ctx :: Ctx CrucibleType}.
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall s a (arch :: LLVMArch).
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
[LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
unpackArgs (((MemType, LLVMExpr s arch) -> LLVMExpr s arch)
-> [(MemType, LLVMExpr s arch)] -> [LLVMExpr s arch]
forall a b. (a -> b) -> [a] -> [b]
map (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a, b) -> b
snd ([(MemType, LLVMExpr s arch)] -> [LLVMExpr s arch])
-> [(MemType, LLVMExpr s arch)] -> [LLVMExpr s arch]
forall a b. (a -> b) -> a -> b
$ Seq (MemType, LLVMExpr s arch) -> [(MemType, LLVMExpr s arch)]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq (MemType, LLVMExpr s arch)
vs) ((forall {ctx :: Ctx CrucibleType}.
  Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
 -> a)
-> (forall {ctx :: Ctx CrucibleType}.
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
archProxy CtxRepr ctx
struct_ctx Assignment (Expr LLVM s) ctx
struct_asgn ->
      Proxy# arch
-> TypeRepr ('StructType ctx) -> Expr LLVM s ('StructType ctx) -> a
forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k Proxy# arch
archProxy (CtxRepr ctx -> TypeRepr ('StructType ctx)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
StructRepr CtxRepr ctx
struct_ctx) (CtxRepr ctx
-> Assignment (Expr LLVM s) ctx -> Expr LLVM s ('StructType ctx)
forall (e :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
IsExpr e =>
CtxRepr ctx -> Assignment e ctx -> e (StructType ctx)
mkStruct CtxRepr ctx
struct_ctx Assignment (Expr LLVM s) ctx
struct_asgn)
unpackOne (VecExpr MemType
tp Seq (LLVMExpr s arch)
vs) forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k =
  MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr -> Proxy# arch
-> TypeRepr tp
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tp) -> a)
-> a
forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# TypeRepr tp
tpr (Seq (LLVMExpr s arch) -> [LLVMExpr s arch]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList Seq (LLVMExpr s arch)
vs) ((Expr LLVM s (VectorType tp) -> a) -> a)
-> (Expr LLVM s (VectorType tp) -> a) -> a
forall a b. (a -> b) -> a -> b
$ Proxy# arch
-> TypeRepr (VectorType tp) -> Expr LLVM s (VectorType tp) -> a
forall (tpr :: CrucibleType).
Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tpr)

unpackVec :: forall tpr s arch a
    . ( ?err :: String -> a
      , HasPtrWidth (ArchWidth arch)
      )
   => Proxy# arch
   -> TypeRepr tpr
   -> [LLVMExpr s arch]
   -> (Expr LLVM s (VectorType tpr) -> a)
   -> a
unpackVec :: forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
_archProxy TypeRepr tpr
tpr = [Expr LLVM s tpr]
-> [LLVMExpr s arch] -> (Expr LLVM s (VectorType tpr) -> a) -> a
go [] ([LLVMExpr s arch] -> (Expr LLVM s (VectorType tpr) -> a) -> a)
-> ([LLVMExpr s arch] -> [LLVMExpr s arch])
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LLVMExpr s arch] -> [LLVMExpr s arch]
forall a. [a] -> [a]
reverse
  where go :: [Expr LLVM s tpr] -> [LLVMExpr s arch] -> (Expr LLVM s (VectorType tpr) -> a) -> a
        go :: [Expr LLVM s tpr]
-> [LLVMExpr s arch] -> (Expr LLVM s (VectorType tpr) -> a) -> a
go [Expr LLVM s tpr]
vs [] Expr LLVM s (VectorType tpr) -> a
k = Expr LLVM s (VectorType tpr) -> a
k (TypeRepr tpr
-> Vector (Expr LLVM s tpr) -> Expr LLVM s (VectorType tpr)
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
TypeRepr tp -> Vector (e tp) -> e (VectorType tp)
vectorLit TypeRepr tpr
tpr (Vector (Expr LLVM s tpr) -> Expr LLVM s (VectorType tpr))
-> Vector (Expr LLVM s tpr) -> Expr LLVM s (VectorType tpr)
forall a b. (a -> b) -> a -> b
$ [Expr LLVM s tpr] -> Vector (Expr LLVM s tpr)
forall a. [a] -> Vector a
V.fromList [Expr LLVM s tpr]
vs)
        go [Expr LLVM s tpr]
vs (LLVMExpr s arch
x:[LLVMExpr s arch]
xs) Expr LLVM s (VectorType tpr) -> a
k = LLVMExpr s arch
-> (forall {tpr :: CrucibleType}.
    Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch
-> (forall (tpr :: CrucibleType).
    Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
unpackOne LLVMExpr s arch
x ((forall {tpr :: CrucibleType}.
  Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
 -> a)
-> (forall {tpr :: CrucibleType}.
    Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
_archProxy' TypeRepr tpr
tpr' Expr LLVM s tpr
v ->
                           case TypeRepr tpr -> TypeRepr tpr -> Maybe (tpr :~: tpr)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr tpr
tpr TypeRepr tpr
tpr' of
                             Just tpr :~: tpr
Refl -> [Expr LLVM s tpr]
-> [LLVMExpr s arch] -> (Expr LLVM s (VectorType tpr) -> a) -> a
go (Expr LLVM s tpr
Expr LLVM s tpr
vExpr LLVM s tpr -> [Expr LLVM s tpr] -> [Expr LLVM s tpr]
forall a. a -> [a] -> [a]
:[Expr LLVM s tpr]
vs) [LLVMExpr s arch]
xs Expr LLVM s (VectorType tpr) -> a
k
                             Maybe (tpr :~: tpr)
Nothing -> ?err::String -> a
String -> a
?err (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"type mismatch in array value", TypeRepr tpr -> String
forall a. Show a => a -> String
show TypeRepr tpr
tpr, TypeRepr tpr -> String
forall a. Show a => a -> String
show TypeRepr tpr
tpr']

zeroExpand :: (?err :: String -> a, HasPtrWidth (ArchWidth arch))
           => Proxy# arch
           -> MemType
           -> (forall tp. Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
           -> a
zeroExpand :: forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
    Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
zeroExpand Proxy# arch
_proxyArch (IntType Natural
w) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
  case Natural -> Some NatRepr
mkNatRepr Natural
w of
    Some NatRepr x
w' | Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w' ->
      Proxy# arch
-> TypeRepr (LLVMPointerType x)
-> Expr LLVM s (LLVMPointerType x)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (NatRepr x -> TypeRepr (LLVMPointerType x)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr x
w') (Expr LLVM s (LLVMPointerType x) -> a)
-> Expr LLVM s (LLVMPointerType x) -> a
forall a b. (a -> b) -> a -> b
$
         NatRepr x
-> Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x)
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr x
w' (Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x))
-> Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x)
forall a b. (a -> b) -> a -> b
$
         App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x))
-> App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x)
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BV x -> App LLVM (Expr LLVM s) (BVType x)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr x
w' (NatRepr x -> BV x
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr x
w')

    Some NatRepr
_ -> ?err::String -> a
String -> a
?err (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"illegal integer size", Natural -> String
forall a. Show a => a -> String
show Natural
w]

zeroExpand Proxy# arch
_proxyArch (StructType StructInfo
si) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
   [LLVMExpr s arch]
-> (forall {ctx :: Ctx CrucibleType}.
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall s a (arch :: LLVMArch).
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
[LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
unpackArgs ((MemType -> LLVMExpr s arch) -> [MemType] -> [LLVMExpr s arch]
forall a b. (a -> b) -> [a] -> [b]
map MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr [MemType]
tps) ((forall {ctx :: Ctx CrucibleType}.
  Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
 -> a)
-> (forall {ctx :: Ctx CrucibleType}.
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
archProxy CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn -> Proxy# arch
-> TypeRepr ('StructType ctx) -> Expr LLVM s ('StructType ctx) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
archProxy (CtxRepr ctx -> TypeRepr ('StructType ctx)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
StructRepr CtxRepr ctx
ctx) (CtxRepr ctx
-> Assignment (Expr LLVM s) ctx -> Expr LLVM s ('StructType ctx)
forall (e :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
IsExpr e =>
CtxRepr ctx -> Assignment e ctx -> e (StructType ctx)
mkStruct CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn)
 where tps :: [MemType]
tps = (FieldInfo -> MemType) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> [a] -> [b]
map FieldInfo -> MemType
fiType ([FieldInfo] -> [MemType]) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> a -> b
$ Vector FieldInfo -> [FieldInfo]
forall a. Vector a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (Vector FieldInfo -> [FieldInfo])
-> Vector FieldInfo -> [FieldInfo]
forall a b. (a -> b) -> a -> b
$ StructInfo -> Vector FieldInfo
siFields StructInfo
si
zeroExpand Proxy# arch
proxyArch (ArrayType Natural
n MemType
tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
  MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr -> Proxy# arch
-> TypeRepr tp
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tp) -> a)
-> a
forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
proxyArch TypeRepr tp
tpr (Int -> LLVMExpr s arch -> [LLVMExpr s arch]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
tp)) ((Expr LLVM s (VectorType tp) -> a) -> a)
-> (Expr LLVM s (VectorType tp) -> a) -> a
forall a b. (a -> b) -> a -> b
$ Proxy# arch
-> TypeRepr (VectorType tp) -> Expr LLVM s (VectorType tp) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch (TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tpr)
zeroExpand Proxy# arch
proxyArch (VecType Natural
n MemType
tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
  MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr -> Proxy# arch
-> TypeRepr tp
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tp) -> a)
-> a
forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
proxyArch TypeRepr tp
tpr (Int -> LLVMExpr s arch -> [LLVMExpr s arch]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
tp)) ((Expr LLVM s (VectorType tp) -> a) -> a)
-> (Expr LLVM s (VectorType tp) -> a) -> a
forall a b. (a -> b) -> a -> b
$ Proxy# arch
-> TypeRepr (VectorType tp) -> Expr LLVM s (VectorType tp) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch (TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tpr)
zeroExpand Proxy# arch
proxyArch (PtrType SymType
_tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k = Proxy# arch
-> TypeRepr (LLVMPointerType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch TypeRepr (LLVMPointerType (ArchWidth arch))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall (w :: Natural) s.
HasPtrWidth w =>
Expr LLVM s (LLVMPointerType w)
nullPointerExpr
zeroExpand Proxy# arch
proxyArch MemType
PtrOpaqueType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k = Proxy# arch
-> TypeRepr (LLVMPointerType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch TypeRepr (LLVMPointerType (ArchWidth arch))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall (w :: Natural) s.
HasPtrWidth w =>
Expr LLVM s (LLVMPointerType w)
nullPointerExpr
zeroExpand Proxy# arch
proxyArch MemType
FloatType   forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k  = Proxy# arch
-> TypeRepr ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch (FloatInfoRepr 'SingleFloat -> TypeRepr ('FloatType 'SingleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'SingleFloat
SingleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (Float -> App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
forall ext (f :: CrucibleType -> Type).
Float -> App ext f ('FloatType 'SingleFloat)
FloatLit Float
0))
zeroExpand Proxy# arch
proxyArch MemType
DoubleType  forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k  = Proxy# arch
-> TypeRepr ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
proxyArch (FloatInfoRepr 'DoubleFloat -> TypeRepr ('FloatType 'DoubleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'DoubleFloat
DoubleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (Double -> App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
forall ext (f :: CrucibleType -> Type).
Double -> App ext f ('FloatType 'DoubleFloat)
DoubleLit Double
0))
zeroExpand Proxy# arch
_prxyArch MemType
X86_FP80Type forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
_ = ?err::String -> a
String -> a
?err String
"Cannot zero expand x86_fp80 values"
zeroExpand Proxy# arch
_prxyArch MemType
MetadataType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
_ = ?err::String -> a
String -> a
?err String
"Cannot zero expand metadata"

undefExpand :: ( ?err :: String -> a
               , HasPtrWidth (ArchWidth arch)
               )
            => Proxy# arch
            -> MemType
            -> (forall tp. Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
            -> a
undefExpand :: forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> MemType
-> (forall (tp :: CrucibleType).
    Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
-> a
undefExpand Proxy# arch
_archProxy (IntType Natural
w) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
  case Natural -> Some NatRepr
mkNatRepr Natural
w of
    Some NatRepr x
w' | Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w' ->
      Proxy# arch
-> TypeRepr (LLVMPointerType x)
-> Expr LLVM s (LLVMPointerType x)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (NatRepr x -> TypeRepr (LLVMPointerType x)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr x
w') (Expr LLVM s (LLVMPointerType x) -> a)
-> Expr LLVM s (LLVMPointerType x) -> a
forall a b. (a -> b) -> a -> b
$
         NatRepr x
-> Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x)
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr x
w' (Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x))
-> Expr LLVM s (BVType x) -> Expr LLVM s (LLVMPointerType x)
forall a b. (a -> b) -> a -> b
$
         App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x))
-> App LLVM (Expr LLVM s) (BVType x) -> Expr LLVM s (BVType x)
forall a b. (a -> b) -> a -> b
$ NatRepr x -> App LLVM (Expr LLVM s) (BVType x)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> App ext f ('BaseToType (BaseBVType w))
BVUndef NatRepr x
w'

    Some NatRepr
_ -> ?err::String -> a
String -> a
?err (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"illegal integer size", Natural -> String
forall a. Show a => a -> String
show Natural
w]
undefExpand Proxy# arch
_archProxy (PtrType SymType
_tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
   Proxy# arch
-> TypeRepr (LLVMPointerType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# TypeRepr (LLVMPointerType (ArchWidth arch))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr (Expr LLVM s (LLVMPointerType (ArchWidth arch)) -> a)
-> Expr LLVM s (LLVMPointerType (ArchWidth arch)) -> a
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch)
-> Expr LLVM s (BVType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr (ArchWidth arch)
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (Expr LLVM s (BVType (ArchWidth arch))
 -> Expr LLVM s (LLVMPointerType (ArchWidth arch)))
-> Expr LLVM s (BVType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$ App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
 -> Expr LLVM s (BVType (ArchWidth arch)))
-> App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch)
-> App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> App ext f ('BaseToType (BaseBVType w))
BVUndef NatRepr (ArchWidth arch)
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth
undefExpand Proxy# arch
_archProxy MemType
PtrOpaqueType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
   Proxy# arch
-> TypeRepr (LLVMPointerType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# TypeRepr (LLVMPointerType (ArchWidth arch))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr (Expr LLVM s (LLVMPointerType (ArchWidth arch)) -> a)
-> Expr LLVM s (LLVMPointerType (ArchWidth arch)) -> a
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch)
-> Expr LLVM s (BVType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr (ArchWidth arch)
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth (Expr LLVM s (BVType (ArchWidth arch))
 -> Expr LLVM s (LLVMPointerType (ArchWidth arch)))
-> Expr LLVM s (BVType (ArchWidth arch))
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$ App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
 -> Expr LLVM s (BVType (ArchWidth arch)))
-> App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch)
-> App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> App ext f ('BaseToType (BaseBVType w))
BVUndef NatRepr (ArchWidth arch)
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth
undefExpand Proxy# arch
_archProxy (StructType StructInfo
si) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
   [LLVMExpr s arch]
-> (forall {ctx :: Ctx CrucibleType}.
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall s a (arch :: LLVMArch).
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
[LLVMExpr s arch]
-> (forall (ctx :: Ctx CrucibleType).
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
unpackArgs ((MemType -> LLVMExpr s arch) -> [MemType] -> [LLVMExpr s arch]
forall a b. (a -> b) -> [a] -> [b]
map MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr [MemType]
tps) ((forall {ctx :: Ctx CrucibleType}.
  Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
 -> a)
-> (forall {ctx :: Ctx CrucibleType}.
    Proxy# arch -> CtxRepr ctx -> Assignment (Expr LLVM s) ctx -> a)
-> a
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
archProxy CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn -> Proxy# arch
-> TypeRepr ('StructType ctx) -> Expr LLVM s ('StructType ctx) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
archProxy (CtxRepr ctx -> TypeRepr ('StructType ctx)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
StructRepr CtxRepr ctx
ctx) (CtxRepr ctx
-> Assignment (Expr LLVM s) ctx -> Expr LLVM s ('StructType ctx)
forall (e :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
IsExpr e =>
CtxRepr ctx -> Assignment e ctx -> e (StructType ctx)
mkStruct CtxRepr ctx
ctx Assignment (Expr LLVM s) ctx
asgn)
 where tps :: [MemType]
tps = (FieldInfo -> MemType) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> [a] -> [b]
map FieldInfo -> MemType
fiType ([FieldInfo] -> [MemType]) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> a -> b
$ Vector FieldInfo -> [FieldInfo]
forall a. Vector a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (Vector FieldInfo -> [FieldInfo])
-> Vector FieldInfo -> [FieldInfo]
forall a b. (a -> b) -> a -> b
$ StructInfo -> Vector FieldInfo
siFields StructInfo
si
undefExpand Proxy# arch
archProxy (ArrayType Natural
n MemType
tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
  MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr -> Proxy# arch
-> TypeRepr tp
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tp) -> a)
-> a
forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
archProxy TypeRepr tp
tpr (Int -> LLVMExpr s arch -> [LLVMExpr s arch]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
tp)) ((Expr LLVM s (VectorType tp) -> a) -> a)
-> (Expr LLVM s (VectorType tp) -> a) -> a
forall a b. (a -> b) -> a -> b
$ Proxy# arch
-> TypeRepr (VectorType tp) -> Expr LLVM s (VectorType tp) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tpr)
undefExpand Proxy# arch
archProxy (VecType Natural
n MemType
tp) forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
  MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr -> Proxy# arch
-> TypeRepr tp
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tp) -> a)
-> a
forall (tpr :: CrucibleType) s (arch :: LLVMArch) a.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
Proxy# arch
-> TypeRepr tpr
-> [LLVMExpr s arch]
-> (Expr LLVM s (VectorType tpr) -> a)
-> a
unpackVec Proxy# arch
archProxy TypeRepr tp
tpr (Int -> LLVMExpr s arch -> [LLVMExpr s arch]
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
tp)) ((Expr LLVM s (VectorType tp) -> a) -> a)
-> (Expr LLVM s (VectorType tp) -> a) -> a
forall a b. (a -> b) -> a -> b
$ Proxy# arch
-> TypeRepr (VectorType tp) -> Expr LLVM s (VectorType tp) -> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (TypeRepr tp -> TypeRepr (VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
tpr)
undefExpand Proxy# arch
_archProxy MemType
FloatType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
  Proxy# arch
-> TypeRepr ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (FloatInfoRepr 'SingleFloat -> TypeRepr ('FloatType 'SingleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'SingleFloat
SingleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (FloatInfoRepr 'SingleFloat
-> App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type).
FloatInfoRepr fi -> App ext f ('FloatType fi)
FloatUndef FloatInfoRepr 'SingleFloat
SingleFloatRepr))
undefExpand Proxy# arch
_archProxy MemType
DoubleType forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
  Proxy# arch
-> TypeRepr ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (FloatInfoRepr 'DoubleFloat -> TypeRepr ('FloatType 'DoubleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'DoubleFloat
DoubleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (FloatInfoRepr 'DoubleFloat
-> App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type).
FloatInfoRepr fi -> App ext f ('FloatType fi)
FloatUndef FloatInfoRepr 'DoubleFloat
DoubleFloatRepr))
undefExpand Proxy# arch
_archProxy MemType
X86_FP80Type forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k =
  Proxy# arch
-> TypeRepr ('FloatType 'X86_80Float)
-> Expr LLVM s ('FloatType 'X86_80Float)
-> a
forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
k Proxy# arch
forall {k} (a :: k). Proxy# a
proxy# (FloatInfoRepr 'X86_80Float -> TypeRepr ('FloatType 'X86_80Float)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'X86_80Float
X86_80FloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'X86_80Float)
-> Expr LLVM s ('FloatType 'X86_80Float)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (FloatInfoRepr 'X86_80Float
-> App LLVM (Expr LLVM s) ('FloatType 'X86_80Float)
forall (fi :: FloatInfo) ext (f :: CrucibleType -> Type).
FloatInfoRepr fi -> App ext f ('FloatType fi)
FloatUndef FloatInfoRepr 'X86_80Float
X86_80FloatRepr))
undefExpand Proxy# arch
_archPrxy MemType
tp forall (tp :: CrucibleType).
Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a
_ = ?err::String -> a
String -> a
?err (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"cannot undef expand type:", MemType -> String
forall a. Show a => a -> String
show MemType
tp]


explodeVector :: Natural -> LLVMExpr s arch -> Maybe (Seq (LLVMExpr s arch))
explodeVector :: forall s (arch :: LLVMArch).
Natural -> LLVMExpr s arch -> Maybe (Seq (LLVMExpr s arch))
explodeVector Natural
n (UndefExpr (VecType Natural
n' MemType
tp)) | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n' = Seq (LLVMExpr s arch) -> Maybe (Seq (LLVMExpr s arch))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int -> LLVMExpr s arch -> Seq (LLVMExpr s arch)
forall a. Int -> a -> Seq a
Seq.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
tp))
explodeVector Natural
n (ZeroExpr (VecType Natural
n' MemType
tp)) | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n' = Seq (LLVMExpr s arch) -> Maybe (Seq (LLVMExpr s arch))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int -> LLVMExpr s arch -> Seq (LLVMExpr s arch)
forall a. Int -> a -> Seq a
Seq.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
tp))
explodeVector Natural
n (VecExpr MemType
_tp Seq (LLVMExpr s arch)
xs)
  | Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Seq (LLVMExpr s arch) -> Int
forall a. Seq a -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length Seq (LLVMExpr s arch)
xs) = Seq (LLVMExpr s arch) -> Maybe (Seq (LLVMExpr s arch))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Seq (LLVMExpr s arch)
xs
explodeVector Natural
n (BaseExpr (VectorRepr TypeRepr tp1
tpr) Expr LLVM s tp
v) =
    let xs :: [LLVMExpr s arch]
xs = [ TypeRepr tp1 -> Expr LLVM s tp1 -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr TypeRepr tp1
tpr (App (ExprExt (Expr LLVM s)) (Expr LLVM s) tp1 -> Expr LLVM s tp1
forall (tp :: CrucibleType).
App (ExprExt (Expr LLVM s)) (Expr LLVM s) tp -> Expr LLVM s tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App (ExprExt (Expr LLVM s)) (Expr LLVM s) tp1 -> Expr LLVM s tp1)
-> App (ExprExt (Expr LLVM s)) (Expr LLVM s) tp1 -> Expr LLVM s tp1
forall a b. (a -> b) -> a -> b
$ TypeRepr tp1
-> Expr LLVM s ('VectorType tp1)
-> Expr LLVM s NatType
-> App LLVM (Expr LLVM s) tp1
forall (tp :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp -> f (VectorType tp) -> f NatType -> App ext f tp
VectorGetEntry TypeRepr tp1
tpr Expr LLVM s tp
Expr LLVM s ('VectorType tp1)
v (Natural -> Expr LLVM s NatType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Natural
i)) | Natural
i <- [Natural
0..Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1] ]
     in Seq (LLVMExpr s arch) -> Maybe (Seq (LLVMExpr s arch))
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
xs)
explodeVector Natural
_ LLVMExpr s arch
_ = Maybe (Seq (LLVMExpr s arch))
forall a. Maybe a
Nothing


---------------------------------------------------------------------------
-- Translations

liftConstant ::
  HasPtrWidth (ArchWidth arch) =>
  LLVMConst ->
  LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant :: forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
c = case LLVMConst
c of
  ZeroConst MemType
mt ->
    LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
mt
  UndefConst MemType
mt ->
    LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
mt
  IntConst NatRepr w
w BV w
i ->
    LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr (LLVMPointerType w)
-> Expr LLVM s (LLVMPointerType w) -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (NatRepr w -> TypeRepr (LLVMPointerType w)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr w
w) (NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr w
w (App LLVM (Expr LLVM s) (BVType w) -> Expr LLVM s (BVType w)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (NatRepr w -> BV w -> App LLVM (Expr LLVM s) (BVType w)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr w
w BV w
i)))
  FloatConst Float
f ->
    LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat) -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (FloatInfoRepr 'SingleFloat -> TypeRepr ('FloatType 'SingleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'SingleFloat
SingleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
-> Expr LLVM s ('FloatType 'SingleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (Float -> App LLVM (Expr LLVM s) ('FloatType 'SingleFloat)
forall ext (f :: CrucibleType -> Type).
Float -> App ext f ('FloatType 'SingleFloat)
FloatLit Float
f))
  DoubleConst Double
d ->
    LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat) -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (FloatInfoRepr 'DoubleFloat -> TypeRepr ('FloatType 'DoubleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'DoubleFloat
DoubleFloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
-> Expr LLVM s ('FloatType 'DoubleFloat)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (Double -> App LLVM (Expr LLVM s) ('FloatType 'DoubleFloat)
forall ext (f :: CrucibleType -> Type).
Double -> App ext f ('FloatType 'DoubleFloat)
DoubleLit Double
d))
  LongDoubleConst (L.FP80_LongDouble Word16
ex Word64
man) ->
    LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('FloatType 'X86_80Float)
-> Expr LLVM s ('FloatType 'X86_80Float) -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (FloatInfoRepr 'X86_80Float -> TypeRepr ('FloatType 'X86_80Float)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'X86_80Float
X86_80FloatRepr) (App LLVM (Expr LLVM s) ('FloatType 'X86_80Float)
-> Expr LLVM s ('FloatType 'X86_80Float)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (X86_80Val -> App LLVM (Expr LLVM s) ('FloatType 'X86_80Float)
forall ext (f :: CrucibleType -> Type).
X86_80Val -> App ext f ('FloatType 'X86_80Float)
X86_80Lit (Word16 -> Word64 -> X86_80Val
X86_80Val Word16
ex Word64
man)))
  StringConst ByteString
bs ->
    -- TODO? Should we have a StringExpr? It seems like this case doesn't
    --  actually ever arise...
    do [LLVMExpr s arch]
vs <- (Word8
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [Word8]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (\Word8
b -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant (NatRepr 8 -> BV 8 -> LLVMConst
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> LLVMConst
IntConst NatRepr 8
forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Word8 -> BV 8
BV.word8 Word8
b))) (ByteString -> [Word8]
BS.unpack ByteString
bs)
       LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
VecExpr MemType
i8 (Seq (LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
vs)
  ArrayConst MemType
mt [LLVMConst]
vs ->
    do [LLVMExpr s arch]
vs' <- (LLVMConst
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [LLVMConst]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (\LLVMConst
c' -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
c') [LLVMConst]
vs
       LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
VecExpr MemType
mt (Seq (LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
vs')
  VectorConst MemType
mt [LLVMConst]
vs ->
    do [LLVMExpr s arch]
vs' <- (LLVMConst
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [LLVMConst]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (\LLVMConst
c' -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
c') [LLVMConst]
vs
       LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
VecExpr MemType
mt (Seq (LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
vs')
  StructConst StructInfo
si [LLVMConst]
vs ->
    do [LLVMExpr s arch]
vs' <- (LLVMConst
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [LLVMConst]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (\LLVMConst
c' -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
c') [LLVMConst]
vs
       let ts :: [MemType]
ts = (FieldInfo -> MemType) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> [a] -> [b]
map FieldInfo -> MemType
fiType ([FieldInfo] -> [MemType]) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> a -> b
$ Vector FieldInfo -> [FieldInfo]
forall a. Vector a -> [a]
V.toList (StructInfo -> Vector FieldInfo
siFields StructInfo
si)
       Bool
-> Generator LLVM s (LLVMState arch) ret IO ()
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless ([LLVMExpr s arch] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [LLVMExpr s arch]
vs' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [MemType] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [MemType]
ts)
              (String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Type mismatch in structure constant")
       LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
StructExpr ([(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList ([MemType] -> [LLVMExpr s arch] -> [(MemType, LLVMExpr s arch)]
forall a b. [a] -> [b] -> [(a, b)]
zip [MemType]
ts [LLVMExpr s arch]
vs')))
  SymbolConst Symbol
sym Integer
0 ->
    do GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
       Expr
  LLVM
  s
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
base <- StmtExtension
  LLVM
  (Expr LLVM s)
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Generator
     LLVM
     s
     (LLVMState arch)
     ret
     IO
     (Expr
        LLVM
        s
        ('IntrinsicType
           "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch))))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr (ArchWidth arch)
-> GlobalVar Mem
-> GlobalSymbol
-> LLVMStmt
     (Expr LLVM s)
     ('IntrinsicType
        "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> GlobalSymbol
-> LLVMStmt
     f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
LLVM_ResolveGlobal ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth GlobalVar Mem
memVar (Symbol -> GlobalSymbol
GlobalSymbol Symbol
sym))
       LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TypeRepr
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Expr
     LLVM
     s
     ('IntrinsicType
        "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr TypeRepr
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr Expr
  LLVM
  s
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
base)
  SymbolConst Symbol
sym Integer
off ->
    do GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
       Expr
  LLVM
  s
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
base <- StmtExtension
  LLVM
  (Expr LLVM s)
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Generator
     LLVM
     s
     (LLVMState arch)
     ret
     IO
     (Expr
        LLVM
        s
        ('IntrinsicType
           "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch))))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr (ArchWidth arch)
-> GlobalVar Mem
-> GlobalSymbol
-> LLVMStmt
     (Expr LLVM s)
     ('IntrinsicType
        "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> GlobalSymbol
-> LLVMStmt
     f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
LLVM_ResolveGlobal ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth GlobalVar Mem
memVar (Symbol -> GlobalSymbol
GlobalSymbol Symbol
sym))
       let off' :: Expr LLVM s (BVType (ArchWidth arch))
off' = App (ExprExt (Expr LLVM s)) (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall (tp :: CrucibleType).
App (ExprExt (Expr LLVM s)) (Expr LLVM s) tp -> Expr LLVM s tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (App
   (ExprExt (Expr LLVM s)) (Expr LLVM s) (BVType (ArchWidth arch))
 -> Expr LLVM s (BVType (ArchWidth arch)))
-> App
     (ExprExt (Expr LLVM s)) (Expr LLVM s) (BVType (ArchWidth arch))
-> Expr LLVM s (BVType (ArchWidth arch))
forall a b. (a -> b) -> a -> b
$ NatRepr (ArchWidth arch)
-> BV (ArchWidth arch)
-> App LLVM (Expr LLVM s) (BVType (ArchWidth arch))
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth (NatRepr (ArchWidth arch) -> Integer -> BV (ArchWidth arch)
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth Integer
off)
       Expr
  LLVM
  s
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
ptr  <- StmtExtension
  LLVM
  (Expr LLVM s)
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Generator
     LLVM
     s
     (LLVMState arch)
     ret
     IO
     (Expr
        LLVM
        s
        ('IntrinsicType
           "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch))))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr (ArchWidth arch)
-> GlobalVar Mem
-> Expr
     LLVM
     s
     ('IntrinsicType
        "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Expr LLVM s (BVType (ArchWidth arch))
-> LLVMStmt
     (Expr LLVM s)
     ('IntrinsicType
        "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> f (LLVMPointerType wptr)
-> f (BVType wptr)
-> LLVMStmt f (LLVMPointerType wptr)
LLVM_PtrAddOffset ?ptrWidth::NatRepr (ArchWidth arch)
NatRepr (ArchWidth arch)
?ptrWidth GlobalVar Mem
memVar Expr
  LLVM
  s
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
base Expr LLVM s (BVType (ArchWidth arch))
off')
       LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TypeRepr
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> Expr
     LLVM
     s
     ('IntrinsicType
        "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
-> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr TypeRepr
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr Expr
  LLVM
  s
  ('IntrinsicType
     "LLVM_pointer" (EmptyCtx ::> BVType (ArchWidth arch)))
ptr)

transTypeAndValue ::
  L.Typed L.Value ->
  LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
transTypeAndValue :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
transTypeAndValue Typed Value
v =
 do let err :: String -> a
err String
msg =
         Doc Void -> [Doc Void] -> a
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule
           Doc Void
"Invalid value type"
           [ String -> Doc Void
forall a. IsString a => String -> a
fromString String
msg ]
    MemType
tp <- (String -> Generator LLVM s (LLVMState arch) ret IO MemType)
-> (MemType -> Generator LLVM s (LLVMState arch) ret IO MemType)
-> Either String MemType
-> Generator LLVM s (LLVMState arch) ret IO MemType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> Generator LLVM s (LLVMState arch) ret IO MemType
forall {a}. String -> a
err MemType -> Generator LLVM s (LLVMState arch) ret IO MemType
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either String MemType
 -> Generator LLVM s (LLVMState arch) ret IO MemType)
-> Either String MemType
-> Generator LLVM s (LLVMState arch) ret IO MemType
forall a b. (a -> b) -> a -> b
$ Type -> Either String MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError String m) =>
Type -> m MemType
liftMemType (Type -> Either String MemType) -> Type -> Either String MemType
forall a b. (a -> b) -> a -> b
$ Typed Value -> Type
forall a. Typed a -> Type
L.typedType Typed Value
v
    (\LLVMExpr s arch
ex -> (MemType
tp, LLVMExpr s arch
ex)) (LLVMExpr s arch -> (MemType, LLVMExpr s arch))
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
-> Generator
     LLVM s (LLVMState arch) ret IO (MemType, LLVMExpr s arch)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
transValue MemType
tp (Typed Value -> Value
forall a. Typed a -> a
L.typedValue Typed Value
v)

transTypedValue ::
  L.Typed L.Value ->
  LLVMGenerator s arch ret (LLVMExpr s arch)
transTypedValue :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
Typed Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
transTypedValue Typed Value
v = (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a, b) -> b
snd ((MemType, LLVMExpr s arch) -> LLVMExpr s arch)
-> Generator
     LLVM s (LLVMState arch) ret IO (MemType, LLVMExpr s arch)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
transTypeAndValue Typed Value
v

-- | Translate an LLVM Value into an expression.
transValue :: forall s arch ret.
              MemType
           -> L.Value
           -> LLVMGenerator s arch ret (LLVMExpr s arch)

transValue :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
transValue MemType
ty Value
L.ValUndef =
  LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
UndefExpr MemType
ty

transValue MemType
ty Value
L.ValZeroInit =
  LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty

transValue ty :: MemType
ty@(PtrType SymType
_) Value
L.ValNull =
  LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty
transValue ty :: MemType
ty@MemType
PtrOpaqueType Value
L.ValNull =
  LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty

transValue ty :: MemType
ty@(PtrType SymType
_) (L.ValInteger Integer
0) =
  LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty
transValue ty :: MemType
ty@MemType
PtrOpaqueType (L.ValInteger Integer
0) =
  LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty

transValue ty :: MemType
ty@(PtrType SymType
_) v :: Value
v@(L.ValInteger Integer
_) =
  Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError (Expr LLVM s (StringType Unicode)
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ String -> Expr LLVM s (StringType Unicode)
forall a. IsString a => String -> a
fromString (String -> Expr LLVM s (StringType Unicode))
-> String -> Expr LLVM s (StringType Unicode)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Attempted to use integer ", Value -> String
forall a. Show a => a -> String
show Value
v, String
" as pointer: ", MemType -> String
forall a. Show a => a -> String
show MemType
ty]
transValue ty :: MemType
ty@MemType
PtrOpaqueType v :: Value
v@(L.ValInteger Integer
_) =
  Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError (Expr LLVM s (StringType Unicode)
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ String -> Expr LLVM s (StringType Unicode)
forall a. IsString a => String -> a
fromString (String -> Expr LLVM s (StringType Unicode))
-> String -> Expr LLVM s (StringType Unicode)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Attempted to use integer ", Value -> String
forall a. Show a => a -> String
show Value
v, String
" as pointer: ", MemType -> String
forall a. Show a => a -> String
show MemType
ty]

transValue ty :: MemType
ty@(IntType Natural
_) Value
L.ValNull =
  LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ MemType -> LLVMExpr s arch
forall s (arch :: LLVMArch). MemType -> LLVMExpr s arch
ZeroExpr MemType
ty

transValue MemType
_ (L.ValString [Word8]
str) = do
  let eight :: NatRepr 8
eight = NatRepr 8
forall (n :: Natural). KnownNat n => NatRepr n
knownNat :: NatRepr 8
  let bv8 :: TypeRepr (LLVMPointerType 8)
bv8   = NatRepr 8 -> TypeRepr (LLVMPointerType 8)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr 8
eight
  let chars :: Vector (Expr LLVM s (LLVMPointerType 8))
chars = [Expr LLVM s (LLVMPointerType 8)]
-> Vector (Expr LLVM s (LLVMPointerType 8))
forall a. [a] -> Vector a
V.fromList ([Expr LLVM s (LLVMPointerType 8)]
 -> Vector (Expr LLVM s (LLVMPointerType 8)))
-> [Expr LLVM s (LLVMPointerType 8)]
-> Vector (Expr LLVM s (LLVMPointerType 8))
forall a b. (a -> b) -> a -> b
$ (Word8 -> Expr LLVM s (LLVMPointerType 8))
-> [Word8] -> [Expr LLVM s (LLVMPointerType 8)]
forall a b. (a -> b) -> [a] -> [b]
map (NatRepr 8
-> Expr LLVM s (BVType 8) -> Expr LLVM s (LLVMPointerType 8)
forall (w :: Natural) s.
(1 <= w) =>
NatRepr w
-> Expr LLVM s (BVType w) -> Expr LLVM s (LLVMPointerType w)
BitvectorAsPointerExpr NatRepr 8
eight (Expr LLVM s (BVType 8) -> Expr LLVM s (LLVMPointerType 8))
-> (Word8 -> Expr LLVM s (BVType 8))
-> Word8
-> Expr LLVM s (LLVMPointerType 8)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. App LLVM (Expr LLVM s) (BVType 8) -> Expr LLVM s (BVType 8)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) (BVType 8) -> Expr LLVM s (BVType 8))
-> (Word8 -> App LLVM (Expr LLVM s) (BVType 8))
-> Word8
-> Expr LLVM s (BVType 8)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr 8 -> BV 8 -> App LLVM (Expr LLVM s) (BVType 8)
forall (w :: Natural) ext (f :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> BV w -> App ext f ('BaseToType (BaseBVType w))
BVLit NatRepr 8
eight (BV 8 -> App LLVM (Expr LLVM s) (BVType 8))
-> (Word8 -> BV 8) -> Word8 -> App LLVM (Expr LLVM s) (BVType 8)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr 8 -> Integer -> BV 8
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr 8
eight (Integer -> BV 8) -> (Word8 -> Integer) -> Word8 -> BV 8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> (Word8 -> Int) -> Word8 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> Int
forall a. Enum a => a -> Int
fromEnum) ([Word8] -> [Expr LLVM s (LLVMPointerType 8)])
-> [Word8] -> [Expr LLVM s (LLVMPointerType 8)]
forall a b. (a -> b) -> a -> b
$ [Word8]
str
  LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('VectorType (LLVMPointerType 8))
-> Expr LLVM s ('VectorType (LLVMPointerType 8)) -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (TypeRepr (LLVMPointerType 8)
-> TypeRepr ('VectorType (LLVMPointerType 8))
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr (LLVMPointerType 8)
bv8) (App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8))
-> Expr LLVM s ('VectorType (LLVMPointerType 8))
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8))
 -> Expr LLVM s ('VectorType (LLVMPointerType 8)))
-> App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8))
-> Expr LLVM s ('VectorType (LLVMPointerType 8))
forall a b. (a -> b) -> a -> b
$ TypeRepr (LLVMPointerType 8)
-> Vector (Expr LLVM s (LLVMPointerType 8))
-> App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8))
forall (tp1 :: CrucibleType) (f :: CrucibleType -> Type) ext.
TypeRepr tp1 -> Vector (f tp1) -> App ext f ('VectorType tp1)
VectorLit TypeRepr (LLVMPointerType 8)
bv8 (Vector (Expr LLVM s (LLVMPointerType 8))
 -> App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8)))
-> Vector (Expr LLVM s (LLVMPointerType 8))
-> App LLVM (Expr LLVM s) ('VectorType (LLVMPointerType 8))
forall a b. (a -> b) -> a -> b
$ Vector (Expr LLVM s (LLVMPointerType 8))
chars)

transValue MemType
_ (L.ValIdent Ident
i) = do
  IdentMap s
m <- Getting (IdentMap s) (LLVMState arch s) (IdentMap s)
-> Generator LLVM s (LLVMState arch) ret IO (IdentMap s)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting (IdentMap s) (LLVMState arch s) (IdentMap s)
forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(IdentMap s -> f (IdentMap s))
-> LLVMState arch s -> f (LLVMState arch s)
identMap
  case Ident
-> IdentMap s -> Maybe (Either (Some (Reg s)) (Some (Atom s)))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
i IdentMap s
m of
    Maybe (Either (Some (Reg s)) (Some (Atom s)))
Nothing -> do
      Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError (Expr LLVM s (StringType Unicode)
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ String -> Expr LLVM s (StringType Unicode)
forall a. IsString a => String -> a
fromString (String -> Expr LLVM s (StringType Unicode))
-> String -> Expr LLVM s (StringType Unicode)
forall a b. (a -> b) -> a -> b
$ String
"Could not find identifier " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Ident -> String
forall a. Show a => a -> String
show Ident
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
    Just (Left (Some Reg s x
r)) -> do
      Expr LLVM s x
e <- Reg s x -> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s x)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Reg s tp -> Generator ext s t ret m (Expr ext s tp)
readReg Reg s x
r
      LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr x -> Expr LLVM s x -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (Reg s x -> TypeRepr x
forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg Reg s x
r) Expr LLVM s x
e
    Just (Right (Some Atom s x
a)) -> do
      LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMExpr s arch
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ TypeRepr x -> Expr LLVM s x -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr (Atom s x -> TypeRepr x
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s x
a) (Atom s x -> Expr LLVM s x
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr Atom s x
a)

transValue (IntType Natural
n) (L.ValInteger Integer
i) =
  ExceptT String (Generator LLVM s (LLVMState arch) ret IO) LLVMConst
-> Generator
     LLVM s (LLVMState arch) ret IO (Either String LLVMConst)
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT (Natural
-> Integer
-> ExceptT
     String (Generator LLVM s (LLVMState arch) ret IO) LLVMConst
forall (m :: Type -> Type).
MonadError String m =>
Natural -> Integer -> m LLVMConst
intConst Natural
n Integer
i) Generator LLVM s (LLVMState arch) ret IO (Either String LLVMConst)
-> (Either String LLVMConst
    -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b.
Generator LLVM s (LLVMState arch) ret IO a
-> (a -> Generator LLVM s (LLVMState arch) ret IO b)
-> Generator LLVM s (LLVMState arch) ret IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Left String
err -> String
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
err
    Right LLVMConst
c  -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
c

transValue (IntType Natural
1) (L.ValBool Bool
b) =
  LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant (Bool -> LLVMConst
boolConst Bool
b)

transValue MemType
FloatType (L.ValFloat Float
f) =
  LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant (Float -> LLVMConst
FloatConst Float
f)

transValue MemType
DoubleType (L.ValDouble Double
d) =
  LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant (Double -> LLVMConst
DoubleConst Double
d)

transValue (StructType StructInfo
_) (L.ValStruct [Typed Value]
vs) = do
     [(MemType, LLVMExpr s arch)]
vs' <- (Typed Value
 -> Generator
      LLVM s (LLVMState arch) ret IO (MemType, LLVMExpr s arch))
-> [Typed Value]
-> Generator
     LLVM s (LLVMState arch) ret IO [(MemType, LLVMExpr s arch)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (\Typed Value
v -> Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
transTypeAndValue Typed Value
v) [Typed Value]
vs
     LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
StructExpr (Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList ([(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch))
-> [(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ [(MemType, LLVMExpr s arch)]
vs')

transValue (StructType StructInfo
_) (L.ValPackedStruct [Typed Value]
vs) =  do
     [(MemType, LLVMExpr s arch)]
vs' <- (Typed Value
 -> Generator
      LLVM s (LLVMState arch) ret IO (MemType, LLVMExpr s arch))
-> [Typed Value]
-> Generator
     LLVM s (LLVMState arch) ret IO [(MemType, LLVMExpr s arch)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (\Typed Value
v -> Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
Typed Value -> LLVMGenerator s arch ret (MemType, LLVMExpr s arch)
transTypeAndValue Typed Value
v) [Typed Value]
vs
     LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
StructExpr (Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList ([(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch))
-> [(MemType, LLVMExpr s arch)] -> Seq (MemType, LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ [(MemType, LLVMExpr s arch)]
vs')

transValue (ArrayType Natural
_ MemType
tp) (L.ValArray Type
_ [Value]
vs) = do
     [LLVMExpr s arch]
vs' <- (Value
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [Value]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (\Value
v -> MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
transValue MemType
tp Value
v) [Value]
vs
     LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
VecExpr MemType
tp (Seq (LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
vs')

transValue (VecType Natural
_ MemType
tp) (L.ValVector Type
_ [Value]
vs) = do
     [LLVMExpr s arch]
vs' <- (Value
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> [Value]
-> Generator LLVM s (LLVMState arch) ret IO [LLVMExpr s arch]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (\Value
v -> MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType -> Value -> LLVMGenerator s arch ret (LLVMExpr s arch)
transValue MemType
tp Value
v) [Value]
vs
     LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall s (arch :: LLVMArch).
MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
VecExpr MemType
tp (Seq (LLVMExpr s arch) -> LLVMExpr s arch)
-> Seq (LLVMExpr s arch) -> LLVMExpr s arch
forall a b. (a -> b) -> a -> b
$ [LLVMExpr s arch] -> Seq (LLVMExpr s arch)
forall a. [a] -> Seq a
Seq.fromList [LLVMExpr s arch]
vs')

transValue MemType
_ (L.ValSymbol Symbol
symbol) = do
     LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant (Symbol -> Integer -> LLVMConst
SymbolConst Symbol
symbol Integer
0)

transValue MemType
_ (L.ValConstExpr ConstExpr' BlockLabel
cexp) =
  do Either String LLVMConst
res <- ExceptT String (Generator LLVM s (LLVMState arch) ret IO) LLVMConst
-> Generator
     LLVM s (LLVMState arch) ret IO (Either String LLVMConst)
forall e (m :: Type -> Type) a. ExceptT e m a -> m (Either e a)
runExceptT (ConstExpr' BlockLabel
-> ExceptT
     String (Generator LLVM s (LLVMState arch) ret IO) LLVMConst
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError String m, HasPtrWidth wptr) =>
ConstExpr' BlockLabel -> m LLVMConst
transConstantExpr ConstExpr' BlockLabel
cexp)
     case Either String LLVMConst
res of
       Left String
err -> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError (Expr LLVM s (StringType Unicode)
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ String -> Expr LLVM s (StringType Unicode)
forall a. IsString a => String -> a
fromString (String -> Expr LLVM s (StringType Unicode))
-> String -> Expr LLVM s (StringType Unicode)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String
"Error translating constant", String
err]
       Right LLVMConst
cv -> LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
forall (arch :: LLVMArch) s (ret :: CrucibleType).
HasPtrWidth (ArchWidth arch) =>
LLVMConst -> LLVMGenerator s arch ret (LLVMExpr s arch)
liftConstant LLVMConst
cv

transValue MemType
ty Value
v =
  Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
       (ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Expr ext s (StringType Unicode) -> Generator ext s t ret m a
reportError (Expr LLVM s (StringType Unicode)
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> Expr LLVM s (StringType Unicode)
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ String -> Expr LLVM s (StringType Unicode)
forall a. IsString a => String -> a
fromString (String -> Expr LLVM s (StringType Unicode))
-> String -> Expr LLVM s (StringType Unicode)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"unsupported LLVM value:", Value -> String
forall a. Show a => a -> String
show Value
v, String
"of type", MemType -> String
forall a. Show a => a -> String
show MemType
ty]


callIsNull
   :: (1 <= w)
   => NatRepr w
   -> Expr LLVM s (LLVMPointerType w)
   -> LLVMGenerator s arch ret (Expr LLVM s BoolType)
callIsNull :: forall (w :: Natural) s (arch :: LLVMArch) (ret :: CrucibleType).
(1 <= w) =>
NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
callIsNull NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex = App LLVM (Expr LLVM s) BoolType -> Expr LLVM s BoolType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App LLVM (Expr LLVM s) BoolType -> Expr LLVM s BoolType)
-> (Expr LLVM s BoolType -> App LLVM (Expr LLVM s) BoolType)
-> Expr LLVM s BoolType
-> Expr LLVM s BoolType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr LLVM s BoolType -> App LLVM (Expr LLVM s) BoolType
forall (f :: CrucibleType -> Type) ext.
f BoolType -> App ext f BoolType
Not (Expr LLVM s BoolType -> Expr LLVM s BoolType)
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
forall (w :: Natural) s (arch :: LLVMArch) (ret :: CrucibleType).
(1 <= w) =>
NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
callIntToBool NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex

callIntToBool
  :: (1 <= w)
  => NatRepr w
  -> Expr LLVM s (LLVMPointerType w)
  -> LLVMGenerator s arch ret (Expr LLVM s BoolType)
callIntToBool :: forall (w :: Natural) s (arch :: LLVMArch) (ret :: CrucibleType).
(1 <= w) =>
NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
callIntToBool NatRepr w
w (BitvectorAsPointerExpr NatRepr w
_ Expr LLVM s (BVType w)
bv) =
  case Expr LLVM s (BVType w)
bv of
    App (BVLit NatRepr w
_ BV w
i) -> if BV w
i BV w -> BV w -> Bool
forall a. Eq a => a -> a -> Bool
== NatRepr w -> BV w
forall (w :: Natural). NatRepr w -> BV w
BV.zero NatRepr w
NatRepr w
w then Expr LLVM s BoolType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr LLVM s BoolType
forall (e :: CrucibleType -> Type). IsExpr e => e BoolType
false else Expr LLVM s BoolType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr LLVM s BoolType
forall (e :: CrucibleType -> Type). IsExpr e => e BoolType
true
    Expr LLVM s (BVType w)
_ -> Expr LLVM s BoolType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (App LLVM (Expr LLVM s) BoolType -> Expr LLVM s BoolType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (NatRepr w
-> Expr LLVM s (BVType w) -> App LLVM (Expr LLVM s) BoolType
forall (w :: Natural) (f :: CrucibleType -> Type) ext.
(1 <= w) =>
NatRepr w -> f (BVType w) -> App ext f BoolType
BVNonzero NatRepr w
w Expr LLVM s (BVType w)
bv))
callIntToBool NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex =
  do Expr LLVM s (LLVMPointerType w)
ex' <- Expr LLVM s (LLVMPointerType w)
-> Generator
     LLVM s (LLVMState arch) ret IO (Expr LLVM s (LLVMPointerType w))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Expr ext s tp -> Generator ext s t ret m (Expr ext s tp)
forceEvaluation Expr LLVM s (LLVMPointerType w)
ex
     let blk :: Expr LLVM s NatType
blk = App LLVM (Expr LLVM s) NatType -> Expr LLVM s NatType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (ExprExtension LLVM (Expr LLVM s) NatType
-> App LLVM (Expr LLVM s) NatType
forall ext (f :: CrucibleType -> Type) (tp :: CrucibleType).
ExprExtension ext f tp -> App ext f tp
ExtensionApp (NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMExtensionExpr (Expr LLVM s) NatType
forall (w :: Natural) (a :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w -> a (LLVMPointerType w) -> LLVMExtensionExpr a NatType
LLVM_PointerBlock NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex'))
     let off :: Expr LLVM s (BVType w)
off = App LLVM (Expr LLVM s) (BVType w) -> Expr LLVM s (BVType w)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (ExprExtension LLVM (Expr LLVM s) (BVType w)
-> App LLVM (Expr LLVM s) (BVType w)
forall ext (f :: CrucibleType -> Type) (tp :: CrucibleType).
ExprExtension ext f tp -> App ext f tp
ExtensionApp (NatRepr w
-> Expr LLVM s (LLVMPointerType w)
-> LLVMExtensionExpr (Expr LLVM s) (BVType w)
forall (w :: Natural) (a :: CrucibleType -> Type).
(1 <= w) =>
NatRepr w
-> a (LLVMPointerType w)
-> LLVMExtensionExpr a ('BaseToType (BaseBVType w))
LLVM_PointerOffset NatRepr w
w Expr LLVM s (LLVMPointerType w)
ex'))
     Expr LLVM s BoolType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s BoolType)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Expr LLVM s NatType
blk Expr LLVM s NatType -> Expr LLVM s NatType -> Expr LLVM s BoolType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
(EqExpr e tp, IsExpr e) =>
e tp -> e tp -> e BoolType
./= Natural -> Expr LLVM s NatType
forall (e :: CrucibleType -> Type) (tp :: CrucibleType) ty.
(LitExpr e tp ty, IsExpr e) =>
ty -> e tp
litExpr Natural
0 Expr LLVM s BoolType
-> Expr LLVM s BoolType -> Expr LLVM s BoolType
forall (e :: CrucibleType -> Type).
IsExpr e =>
e BoolType -> e BoolType -> e BoolType
.|| (App LLVM (Expr LLVM s) BoolType -> Expr LLVM s BoolType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (NatRepr w
-> Expr LLVM s (BVType w) -> App LLVM (Expr LLVM s) BoolType
forall (w :: Natural) (f :: CrucibleType -> Type) ext.
(1 <= w) =>
NatRepr w -> f (BVType w) -> App ext f BoolType
BVNonzero NatRepr w
w Expr LLVM s (BVType w)
off)))

callAlloca
   :: wptr ~ ArchWidth arch
   => Expr LLVM s (BVType wptr)
   -> Alignment
   -> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
callAlloca :: forall (wptr :: Natural) (arch :: LLVMArch) s
       (ret :: CrucibleType).
(wptr ~ ArchWidth arch) =>
Expr LLVM s (BVType wptr)
-> Alignment
-> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
callAlloca Expr LLVM s (BVType wptr)
sz Alignment
alignment = do
   GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
   String
loc <- Position -> String
forall a. Show a => a -> String
show (Position -> String)
-> Generator LLVM s (LLVMState arch) ret IO Position
-> Generator LLVM s (LLVMState arch) ret IO String
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Generator LLVM s (LLVMState arch) ret IO Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Position
getPosition
   StmtExtension LLVM (Expr LLVM s) (LLVMPointerType wptr)
-> Generator
     LLVM s (LLVMState arch) ret IO (Expr LLVM s (LLVMPointerType wptr))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr wptr
-> GlobalVar Mem
-> Expr LLVM s (BVType wptr)
-> Alignment
-> String
-> LLVMStmt (Expr LLVM s) (LLVMPointerType wptr)
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> f (BVType wptr)
-> Alignment
-> String
-> LLVMStmt
     f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
LLVM_Alloca ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth GlobalVar Mem
memVar Expr LLVM s (BVType wptr)
sz Alignment
alignment String
loc)

callPushFrame :: Text -> LLVMGenerator s arch ret ()
callPushFrame :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
Text -> LLVMGenerator s arch ret ()
callPushFrame Text
nm = do
   GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
   Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
 -> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ StmtExtension LLVM (Expr LLVM s) 'UnitType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (Text -> GlobalVar Mem -> LLVMStmt (Expr LLVM s) 'UnitType
forall (f :: CrucibleType -> Type).
Text -> GlobalVar Mem -> LLVMStmt f 'UnitType
LLVM_PushFrame Text
nm GlobalVar Mem
memVar)

callPopFrame :: LLVMGenerator s arch ret ()
callPopFrame :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
LLVMGenerator s arch ret ()
callPopFrame = do
   GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
   Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
 -> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ StmtExtension LLVM (Expr LLVM s) 'UnitType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (GlobalVar Mem -> LLVMStmt (Expr LLVM s) 'UnitType
forall (f :: CrucibleType -> Type).
GlobalVar Mem -> LLVMStmt f 'UnitType
LLVM_PopFrame GlobalVar Mem
memVar)

callPtrAddOffset ::
       wptr ~ ArchWidth arch
    => Expr LLVM s (LLVMPointerType wptr)
    -> Expr LLVM s (BVType wptr)
    -> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
callPtrAddOffset :: forall (wptr :: Natural) (arch :: LLVMArch) s
       (ret :: CrucibleType).
(wptr ~ ArchWidth arch) =>
Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (BVType wptr)
-> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
callPtrAddOffset Expr LLVM s (LLVMPointerType wptr)
base Expr LLVM s (BVType wptr)
off = do
    GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
    StmtExtension LLVM (Expr LLVM s) (LLVMPointerType wptr)
-> Generator
     LLVM s (LLVMState arch) ret IO (Expr LLVM s (LLVMPointerType wptr))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr wptr
-> GlobalVar Mem
-> Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (BVType wptr)
-> LLVMStmt (Expr LLVM s) (LLVMPointerType wptr)
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> f (LLVMPointerType wptr)
-> f (BVType wptr)
-> LLVMStmt f (LLVMPointerType wptr)
LLVM_PtrAddOffset ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth GlobalVar Mem
memVar Expr LLVM s (LLVMPointerType wptr)
base Expr LLVM s (BVType wptr)
off)

callPtrSubtract ::
       wptr ~ ArchWidth arch
    => Expr LLVM s (LLVMPointerType wptr)
    -> Expr LLVM s (LLVMPointerType wptr)
    -> LLVMGenerator s arch ret (Expr LLVM s (BVType wptr))
callPtrSubtract :: forall (wptr :: Natural) (arch :: LLVMArch) s
       (ret :: CrucibleType).
(wptr ~ ArchWidth arch) =>
Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (LLVMPointerType wptr)
-> LLVMGenerator s arch ret (Expr LLVM s (BVType wptr))
callPtrSubtract Expr LLVM s (LLVMPointerType wptr)
x Expr LLVM s (LLVMPointerType wptr)
y = do
    GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
    StmtExtension LLVM (Expr LLVM s) (BVType wptr)
-> Generator
     LLVM s (LLVMState arch) ret IO (Expr LLVM s (BVType wptr))
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (NatRepr wptr
-> GlobalVar Mem
-> Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (LLVMPointerType wptr)
-> LLVMStmt (Expr LLVM s) (BVType wptr)
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
NatRepr wptr
-> GlobalVar Mem
-> f (LLVMPointerType wptr)
-> f (LLVMPointerType wptr)
-> LLVMStmt f ('BaseToType (BaseBVType wptr))
LLVM_PtrSubtract ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth GlobalVar Mem
memVar Expr LLVM s (LLVMPointerType wptr)
x Expr LLVM s (LLVMPointerType wptr)
y)

callLoad :: MemType
         -> TypeRepr tp
         -> LLVMExpr s arch
         -> Alignment
         -> LLVMGenerator s arch ret (LLVMExpr s arch)
callLoad :: forall (tp :: CrucibleType) s (arch :: LLVMArch)
       (ret :: CrucibleType).
MemType
-> TypeRepr tp
-> LLVMExpr s arch
-> Alignment
-> LLVMGenerator s arch ret (LLVMExpr s arch)
callLoad MemType
typ TypeRepr tp
expectTy (LLVMExpr s arch -> ScalarView s arch
forall (arch :: LLVMArch) s.
(?lc::TypeContext, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch -> ScalarView s arch
asScalar -> Scalar Proxy# arch
_ TypeRepr tp
PtrRepr Expr LLVM s tp
ptr) Alignment
align =
   do GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
      StorageType
typ' <- MemType -> Generator LLVM s (LLVMState arch) ret IO StorageType
forall (m :: Type -> Type) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
typ
      Expr LLVM s tp
v <- StmtExtension LLVM (Expr LLVM s) tp
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (GlobalVar Mem
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> TypeRepr tp
-> StorageType
-> Alignment
-> LLVMStmt (Expr LLVM s) tp
forall (wptr :: Natural) (f :: CrucibleType -> Type)
       (a :: CrucibleType).
HasPtrWidth wptr =>
GlobalVar Mem
-> f (LLVMPointerType wptr)
-> TypeRepr a
-> StorageType
-> Alignment
-> LLVMStmt f a
LLVM_Load GlobalVar Mem
memVar Expr LLVM s tp
Expr LLVM s (LLVMPointerType (ArchWidth arch))
ptr TypeRepr tp
expectTy StorageType
typ' Alignment
align)
      LLVMExpr s arch
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
forall (tp :: CrucibleType) s (arch :: LLVMArch).
TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
BaseExpr TypeRepr tp
expectTy Expr LLVM s tp
v)
callLoad MemType
_ TypeRepr tp
_ LLVMExpr s arch
_ Alignment
_ =
  String
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
 -> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch))
-> String
-> Generator LLVM s (LLVMState arch) ret IO (LLVMExpr s arch)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Unexpected argument type in callLoad"]

callStore :: MemType
          -> LLVMExpr s arch
          -> LLVMExpr s arch
          -> Alignment
          -> LLVMGenerator s arch ret ()
callStore :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType
-> LLVMExpr s arch
-> LLVMExpr s arch
-> Alignment
-> LLVMGenerator s arch ret ()
callStore MemType
typ (LLVMExpr s arch -> ScalarView s arch
forall (arch :: LLVMArch) s.
(?lc::TypeContext, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch -> ScalarView s arch
asScalar -> Scalar Proxy# arch
_ TypeRepr tp
PtrRepr Expr LLVM s tp
ptr) (ZeroExpr MemType
_mt) Alignment
_align =
 do GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
    StorageType
typ'   <- MemType -> Generator LLVM s (LLVMState arch) ret IO StorageType
forall (m :: Type -> Type) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
typ
    Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
 -> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ StmtExtension LLVM (Expr LLVM s) 'UnitType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (GlobalVar Mem
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> Bytes
-> LLVMStmt (Expr LLVM s) 'UnitType
forall (wptr :: Natural) (f :: CrucibleType -> Type).
HasPtrWidth wptr =>
GlobalVar Mem
-> f (LLVMPointerType wptr) -> Bytes -> LLVMStmt f 'UnitType
LLVM_MemClear GlobalVar Mem
memVar Expr LLVM s tp
Expr LLVM s (LLVMPointerType (ArchWidth arch))
ptr (StorageType -> Bytes
storageTypeSize StorageType
typ'))

callStore MemType
typ (LLVMExpr s arch -> ScalarView s arch
forall (arch :: LLVMArch) s.
(?lc::TypeContext, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch -> ScalarView s arch
asScalar -> Scalar Proxy# arch
_ TypeRepr tp
PtrRepr Expr LLVM s tp
ptr) LLVMExpr s arch
v Alignment
align =
 do let ?err = ?err::String -> Generator LLVM s (LLVMState arch) ret IO ()
String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail
    LLVMExpr s arch
-> (forall {tpr :: CrucibleType}.
    Proxy# arch
    -> TypeRepr tpr
    -> Expr LLVM s tpr
    -> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a (arch :: LLVMArch) s.
(?err::String -> a, HasPtrWidth (ArchWidth arch)) =>
LLVMExpr s arch
-> (forall (tpr :: CrucibleType).
    Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
-> a
unpackOne LLVMExpr s arch
v ((forall {tpr :: CrucibleType}.
  Proxy# arch
  -> TypeRepr tpr
  -> Expr LLVM s tpr
  -> Generator LLVM s (LLVMState arch) ret IO ())
 -> Generator LLVM s (LLVMState arch) ret IO ())
-> (forall {tpr :: CrucibleType}.
    Proxy# arch
    -> TypeRepr tpr
    -> Expr LLVM s tpr
    -> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ \Proxy# arch
_ TypeRepr tpr
vtpr Expr LLVM s tpr
vexpr -> do
      GlobalVar Mem
memVar <- Generator LLVM s (LLVMState arch) ret IO (GlobalVar Mem)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar
      StorageType
typ' <- MemType -> Generator LLVM s (LLVMState arch) ret IO StorageType
forall (m :: Type -> Type) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
typ
      Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
 -> Generator LLVM s (LLVMState arch) ret IO ())
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ StmtExtension LLVM (Expr LLVM s) 'UnitType
-> Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s 'UnitType)
forall (m :: Type -> Type) ext s (tp :: CrucibleType)
       (t :: Type -> Type) (ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
StmtExtension ext (Expr ext s) tp
-> Generator ext s t ret m (Expr ext s tp)
extensionStmt (GlobalVar Mem
-> Expr LLVM s (LLVMPointerType (ArchWidth arch))
-> TypeRepr tpr
-> StorageType
-> Alignment
-> Expr LLVM s tpr
-> LLVMStmt (Expr LLVM s) 'UnitType
forall (wptr :: Natural) (f :: CrucibleType -> Type)
       (tp :: CrucibleType).
HasPtrWidth wptr =>
GlobalVar Mem
-> f (LLVMPointerType wptr)
-> TypeRepr tp
-> StorageType
-> Alignment
-> f tp
-> LLVMStmt f 'UnitType
LLVM_Store GlobalVar Mem
memVar Expr LLVM s tp
Expr LLVM s (LLVMPointerType (ArchWidth arch))
ptr TypeRepr tpr
vtpr StorageType
typ' Alignment
align Expr LLVM s tpr
vexpr)

callStore MemType
_ LLVMExpr s arch
_ LLVMExpr s arch
_ Alignment
_ =
  String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Generator LLVM s (LLVMState arch) ret IO ())
-> String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Unexpected argument type in callStore"]