------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.MemModel.Value
-- Description      : Representation of values in the LLVM memory model
-- Copyright        : (c) Galois, Inc 2015-2016
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Lang.Crucible.LLVM.MemModel.Value
  ( -- * LLVM Value representation
    LLVMVal(..)
  , ppLLVMValWithGlobals
  , FloatSize(..)
  , Field
  , ptrToPtrVal
  , zeroInt
  , ppTermExpr
  , explodeStringValue

  , llvmValStorableType
  , freshLLVMVal
  , isZero
  , testEqual
  ) where

import           Control.Lens (view, over, _2, (^.))
import           Control.Monad (foldM, join)
import           Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import           Data.Map (Map)
import           Data.Foldable (toList)
import           Data.Functor.Identity (Identity(..))
import           Data.Maybe (fromMaybe, mapMaybe)
import           Data.List (intersperse)
import           Numeric.Natural
import           Prettyprinter

import qualified Data.BitVector.Sized as BV
import           Data.Parameterized.Classes
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Some
import           Data.Vector (Vector)
import qualified Data.Vector as V
import qualified Text.LLVM.AST as L

import           What4.Interface
import           What4.InterpretedFloatingPoint

import           Lang.Crucible.Backend
import           Lang.Crucible.LLVM.Bytes
import           Lang.Crucible.LLVM.MemModel.Type
import           Lang.Crucible.LLVM.MemModel.Pointer
import           Lang.Crucible.Panic (panic)

data FloatSize (fi :: FloatInfo) where
  SingleSize :: FloatSize SingleFloat
  DoubleSize :: FloatSize DoubleFloat
  X86_FP80Size :: FloatSize X86_80Float

deriving instance Eq (FloatSize fi)
deriving instance Ord (FloatSize fi)
deriving instance Show (FloatSize fi)
instance TestEquality FloatSize where
  testEquality :: forall (a :: FloatInfo) (b :: FloatInfo).
FloatSize a -> FloatSize b -> Maybe (a :~: b)
testEquality FloatSize a
SingleSize FloatSize b
SingleSize = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality FloatSize a
DoubleSize FloatSize b
DoubleSize = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality FloatSize a
X86_FP80Size FloatSize b
X86_FP80Size = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality FloatSize a
_ FloatSize b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

-- | This datatype describes the variety of values that can be stored in
--   the LLVM heap.
data LLVMVal sym where
  -- | NOTE! The ValInt constructor uniformly represents both pointers and
  -- raw bitvector values.  The 'SymNat' value is an allocation block number
  -- that identifies specific allocations.  The block number '0' is special,
  -- and indicates that this value is actually a bitvector.  Non-zero block
  -- numbers correspond to pointer values, where the 'SymBV' value is an
  -- offset from the base pointer of the allocation.
  LLVMValInt :: (1 <= w) => SymNat sym -> SymBV sym w -> LLVMVal sym
  LLVMValFloat :: FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
  LLVMValStruct :: Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
  LLVMValArray :: StorageType -> Vector (LLVMVal sym) -> LLVMVal sym

  -- | LLVM Value Data given by a constant string of bytes
  LLVMValString :: ByteString -> LLVMVal sym

  -- | The zero value exists at all storage types, and represents the the value
  -- which is obtained by loading the approprite number of all zero bytes.
  -- It is useful for compactly representing large zero-initialized data structures.
  LLVMValZero :: StorageType -> LLVMVal sym

  -- | The @undef@ value exists at all storage types.
  LLVMValUndef :: StorageType -> LLVMVal sym


llvmValStorableType :: IsExprBuilder sym => LLVMVal sym -> StorageType
llvmValStorableType :: forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
llvmValStorableType LLVMVal sym
v =
  case LLVMVal sym
v of
    LLVMValInt SymNat sym
_ SymBV sym w
bv -> Bytes -> StorageType
bitvectorType (Natural -> Bytes
forall a. Integral a => a -> Bytes
bitsToBytes (NatRepr w -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
bv)))
    LLVMValFloat FloatSize fi
SingleSize SymInterpretedFloat sym fi
_ -> StorageType
floatType
    LLVMValFloat FloatSize fi
DoubleSize SymInterpretedFloat sym fi
_ -> StorageType
doubleType
    LLVMValFloat FloatSize fi
X86_FP80Size SymInterpretedFloat sym fi
_ -> StorageType
x86_fp80Type
    LLVMValStruct Vector (Field StorageType, LLVMVal sym)
fs -> Vector (Field StorageType) -> StorageType
structType (((Field StorageType, LLVMVal sym) -> Field StorageType)
-> Vector (Field StorageType, LLVMVal sym)
-> Vector (Field StorageType)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Field StorageType, LLVMVal sym) -> Field StorageType
forall a b. (a, b) -> a
fst Vector (Field StorageType, LLVMVal sym)
fs)
    LLVMValArray StorageType
tp Vector (LLVMVal sym)
vs -> Natural -> StorageType -> StorageType
arrayType (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Vector (LLVMVal sym) -> Int
forall a. Vector a -> Int
V.length Vector (LLVMVal sym)
vs)) StorageType
tp
    LLVMValString ByteString
bs -> Natural -> StorageType -> StorageType
arrayType (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (ByteString -> Int
BS.length ByteString
bs)) (Bytes -> StorageType
bitvectorType (Integer -> Bytes
Bytes Integer
1))
    LLVMValZero StorageType
tp -> StorageType
tp
    LLVMValUndef StorageType
tp -> StorageType
tp

-- | Create a fresh 'LLVMVal' of the given type.
freshLLVMVal :: IsSymInterface sym =>
                sym -> StorageType -> IO (LLVMVal sym)
freshLLVMVal :: forall sym.
IsSymInterface sym =>
sym -> StorageType -> IO (LLVMVal sym)
freshLLVMVal sym
sym StorageType
tp =
  case StorageType -> StorageTypeF StorageType
storageTypeF StorageType
tp of
    Bitvector Bytes
bytes ->
      case Natural -> Some NatRepr
mkNatRepr (Bytes -> Natural
bytesToBits Bytes
bytes) of
        Some NatRepr x
repr ->
          case NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
repr of
            Just LeqProof 1 x
LeqProof -> SymNat sym -> SymBV sym x -> LLVMVal sym
forall (fi :: Natural) sym.
(1 <= fi) =>
SymNat sym -> SymBV sym fi -> LLVMVal sym
LLVMValInt (SymNat sym -> SymBV sym x -> LLVMVal sym)
-> IO (SymNat sym) -> IO (SymBV sym x -> LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
0
                                        IO (SymBV sym x -> LLVMVal sym)
-> IO (SymBV sym x) -> IO (LLVMVal sym)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym
-> SolverSymbol -> BaseTypeRepr ('BaseBVType x) -> IO (SymBV sym x)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
emptySymbol (NatRepr x -> BaseTypeRepr ('BaseBVType x)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr x
repr)
            Maybe (LeqProof 1 x)
Nothing -> String -> [String] -> IO (LLVMVal sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"freshLLVMVal" [String
"Non-positive value inside Bytes"]
    StorageTypeF StorageType
Float      -> FloatSize 'SingleFloat
-> SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'SingleFloat
SingleSize (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
 -> LLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat))
-> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SolverSymbol
-> FloatInfoRepr 'SingleFloat
-> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatSymExprBuilder sym =>
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (fi :: FloatInfo).
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
freshFloatConstant sym
sym SolverSymbol
emptySymbol FloatInfoRepr 'SingleFloat
SingleFloatRepr
    StorageTypeF StorageType
Double     -> FloatSize 'DoubleFloat
-> SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'DoubleFloat
DoubleSize (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
 -> LLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat))
-> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SolverSymbol
-> FloatInfoRepr 'DoubleFloat
-> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatSymExprBuilder sym =>
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (fi :: FloatInfo).
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
freshFloatConstant sym
sym SolverSymbol
emptySymbol FloatInfoRepr 'DoubleFloat
DoubleFloatRepr
    StorageTypeF StorageType
X86_FP80   -> FloatSize 'X86_80Float
-> SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'X86_80Float
X86_FP80Size (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
 -> LLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float))
-> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SolverSymbol
-> FloatInfoRepr 'X86_80Float
-> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float))
forall sym (fi :: FloatInfo).
IsInterpretedFloatSymExprBuilder sym =>
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (fi :: FloatInfo).
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
freshFloatConstant sym
sym SolverSymbol
emptySymbol FloatInfoRepr 'X86_80Float
X86_80FloatRepr
    Array Natural
n StorageType
ty -> StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
ty (Vector (LLVMVal sym) -> LLVMVal sym)
-> IO (Vector (LLVMVal sym)) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> IO (LLVMVal sym) -> IO (Vector (LLVMVal sym))
forall (m :: Type -> Type) a. Monad m => Int -> m a -> m (Vector a)
V.replicateM (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (sym -> StorageType -> IO (LLVMVal sym)
forall sym.
IsSymInterface sym =>
sym -> StorageType -> IO (LLVMVal sym)
freshLLVMVal sym
sym StorageType
ty)
    Struct Vector (Field StorageType)
vec -> Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall sym. Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
LLVMValStruct (Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym)
-> IO (Vector (Field StorageType, LLVMVal sym)) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Field StorageType -> IO (Field StorageType, LLVMVal sym))
-> Vector (Field StorageType)
-> IO (Vector (Field StorageType, LLVMVal sym))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse (\Field StorageType
v -> (Field StorageType
v,) (LLVMVal sym -> (Field StorageType, LLVMVal sym))
-> IO (LLVMVal sym) -> IO (Field StorageType, LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> StorageType -> IO (LLVMVal sym)
forall sym.
IsSymInterface sym =>
sym -> StorageType -> IO (LLVMVal sym)
freshLLVMVal sym
sym (Field StorageType
vField StorageType
-> Getting StorageType (Field StorageType) StorageType
-> StorageType
forall s a. s -> Getting a s a -> a
^.Getting StorageType (Field StorageType) StorageType
forall a b (f :: Type -> Type).
Functor f =>
(a -> f b) -> Field a -> f (Field b)
fieldVal)) Vector (Field StorageType)
vec

ppTermExpr :: forall sym ann.
  IsExpr (SymExpr sym) => LLVMVal sym -> Doc ann
ppTermExpr :: forall sym ann. IsExpr (SymExpr sym) => LLVMVal sym -> Doc ann
ppTermExpr LLVMVal sym
t = -- FIXME, do something with the predicate?
  case LLVMVal sym
t of
    LLVMValZero StorageType
_tp -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"0"
    LLVMValUndef StorageType
tp -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"<undef : " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> StorageType -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow StorageType
tp Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
">"
    LLVMValString ByteString
bs -> ByteString -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow ByteString
bs
    LLVMValInt SymNat sym
base SymBV sym w
off -> forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr @sym (SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
base SymBV sym w
off)
    LLVMValFloat FloatSize fi
_ SymInterpretedFloat sym fi
v -> SymInterpretedFloat sym fi -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymInterpretedFloat sym fi
v
    LLVMValStruct Vector (Field StorageType, LLVMVal sym)
v -> Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep Doc ann
forall ann. Doc ann
lbrace Doc ann
forall ann. Doc ann
rbrace Doc ann
forall ann. Doc ann
comma [Doc ann]
v''
      where v' :: [(Field StorageType, Doc ann)]
v'  = ((Field StorageType, LLVMVal sym) -> (Field StorageType, Doc ann))
-> [(Field StorageType, LLVMVal sym)]
-> [(Field StorageType, Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (ASetter
  (Field StorageType, LLVMVal sym)
  (Field StorageType, Doc ann)
  (LLVMVal sym)
  (Doc ann)
-> (LLVMVal sym -> Doc ann)
-> (Field StorageType, LLVMVal sym)
-> (Field StorageType, Doc ann)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (Field StorageType, LLVMVal sym)
  (Field StorageType, Doc ann)
  (LLVMVal sym)
  (Doc ann)
forall s t a b. Field2 s t a b => Lens s t a b
Lens
  (Field StorageType, LLVMVal sym)
  (Field StorageType, Doc ann)
  (LLVMVal sym)
  (Doc ann)
_2 LLVMVal sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => LLVMVal sym -> Doc ann
ppTermExpr) (Vector (Field StorageType, LLVMVal sym)
-> [(Field StorageType, LLVMVal sym)]
forall a. Vector a -> [a]
V.toList Vector (Field StorageType, LLVMVal sym)
v)
            v'' :: [Doc ann]
v'' = ((Field StorageType, Doc ann) -> Doc ann)
-> [(Field StorageType, Doc ann)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (\(Field StorageType
fld,Doc ann
doc) ->
                        Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
group (String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"base+" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Bytes -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (Field StorageType -> Bytes
forall v. Field v -> Bytes
fieldOffset Field StorageType
fld) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
forall ann. Doc ann
equals Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
doc))
                      [(Field StorageType, Doc ann)]
v'
    LLVMValArray StorageType
_tp Vector (LLVMVal sym)
v -> Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep Doc ann
forall ann. Doc ann
lbracket Doc ann
forall ann. Doc ann
rbracket Doc ann
forall ann. Doc ann
comma [Doc ann]
v'
      where v' :: [Doc ann]
v' = LLVMVal sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => LLVMVal sym -> Doc ann
ppTermExpr (LLVMVal sym -> Doc ann) -> [LLVMVal sym] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (LLVMVal sym) -> [LLVMVal sym]
forall a. Vector a -> [a]
V.toList Vector (LLVMVal sym)
v

-- | Coerce an 'LLVMPtr' value into a memory-storable 'LLVMVal'.
ptrToPtrVal :: (1 <= w) => LLVMPtr sym w -> LLVMVal sym
ptrToPtrVal :: forall (w :: Natural) sym. (1 <= w) => LLVMPtr sym w -> LLVMVal sym
ptrToPtrVal (LLVMPointer SymNat sym
blk SymBV sym w
off) = SymNat sym -> SymBV sym w -> LLVMVal sym
forall (fi :: Natural) sym.
(1 <= fi) =>
SymNat sym -> SymBV sym fi -> LLVMVal sym
LLVMValInt SymNat sym
blk SymBV sym w
off

zeroInt ::
  IsSymInterface sym =>
  sym ->
  Bytes ->
  (forall w. (1 <= w) => Maybe (SymNat sym, SymBV sym w) -> IO a) ->
  IO a
zeroInt :: forall sym a.
IsSymInterface sym =>
sym
-> Bytes
-> (forall (w :: Natural).
    (1 <= w) =>
    Maybe (SymNat sym, SymBV sym w) -> IO a)
-> IO a
zeroInt sym
sym Bytes
bytes forall (w :: Natural).
(1 <= w) =>
Maybe (SymNat sym, SymBV sym w) -> IO a
k
   | Some NatRepr x
w <- Natural -> Some NatRepr
mkNatRepr (Bytes -> Natural
bytesToBits Bytes
bytes)
   , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
   =   do SymNat sym
blk <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
0
          SymExpr sym (BaseBVType x)
bv  <- sym -> NatRepr x -> IO (SymExpr sym (BaseBVType x))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr x
w
          Maybe (SymNat sym, SymExpr sym (BaseBVType x)) -> IO a
forall (w :: Natural).
(1 <= w) =>
Maybe (SymNat sym, SymBV sym w) -> IO a
k ((SymNat sym, SymExpr sym (BaseBVType x))
-> Maybe (SymNat sym, SymExpr sym (BaseBVType x))
forall a. a -> Maybe a
Just (SymNat sym
blk, SymExpr sym (BaseBVType x)
bv))
zeroInt sym
_ Bytes
_ forall (w :: Natural).
(1 <= w) =>
Maybe (SymNat sym, SymBV sym w) -> IO a
k = forall (w :: Natural).
(1 <= w) =>
Maybe (SymNat sym, SymBV sym w) -> IO a
k @1 Maybe (SymNat sym, SymBV sym 1)
forall a. Maybe a
Nothing

-- | Pretty-print an 'LLVMVal'.
--
-- This is parameterized over how to display pointers, see
-- 'ppLLVMValWithGlobals'.
ppLLVMVal ::
  (Applicative f, IsExpr (SymExpr sym)) =>
  (forall w. SymNat sym -> SymBV sym w -> f (Maybe (Doc ann)))
    {- ^ Printing of pointers -} ->
  LLVMVal sym ->
  f (Doc ann)
ppLLVMVal :: forall (f :: Type -> Type) sym ann.
(Applicative f, IsExpr (SymExpr sym)) =>
(forall (w :: Natural).
 SymNat sym -> SymBV sym w -> f (Maybe (Doc ann)))
-> LLVMVal sym -> f (Doc ann)
ppLLVMVal forall (w :: Natural).
SymNat sym -> SymBV sym w -> f (Maybe (Doc ann))
ppInt =
  let typed :: a -> a -> Doc ann
typed a
doc a
tp = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
doc Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow a
tp
      pp :: LLVMVal sym -> f (Doc ann)
pp = (forall (w :: Natural).
 SymNat sym -> SymBV sym w -> f (Maybe (Doc ann)))
-> LLVMVal sym -> f (Doc ann)
forall (f :: Type -> Type) sym ann.
(Applicative f, IsExpr (SymExpr sym)) =>
(forall (w :: Natural).
 SymNat sym -> SymBV sym w -> f (Maybe (Doc ann)))
-> LLVMVal sym -> f (Doc ann)
ppLLVMVal SymNat sym -> SymBV sym w -> f (Maybe (Doc ann))
forall (w :: Natural).
SymNat sym -> SymBV sym w -> f (Maybe (Doc ann))
ppInt
  in
    \case
      (LLVMValZero StorageType
tp) -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> f (Doc ann)) -> Doc ann -> f (Doc ann)
forall a b. (a -> b) -> a -> b
$ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
angles (String -> StorageType -> Doc ann
forall {a} {a} {ann}. (Pretty a, Show a) => a -> a -> Doc ann
typed String
"zero" StorageType
tp)
      (LLVMValUndef StorageType
tp) -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> f (Doc ann)) -> Doc ann -> f (Doc ann)
forall a b. (a -> b) -> a -> b
$ Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
angles (String -> StorageType -> Doc ann
forall {a} {a} {ann}. (Pretty a, Show a) => a -> a -> Doc ann
typed String
"undef" StorageType
tp)
      (LLVMValString ByteString
bs) -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> f (Doc ann)) -> Doc ann -> f (Doc ann)
forall a b. (a -> b) -> a -> b
$ ByteString -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow ByteString
bs
      (LLVMValInt SymNat sym
blk SymBV sym w
w) -> Doc ann -> Maybe (Doc ann) -> Doc ann
forall a. a -> Maybe a -> a
fromMaybe Doc ann
otherDoc (Maybe (Doc ann) -> Doc ann) -> f (Maybe (Doc ann)) -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymNat sym -> SymBV sym w -> f (Maybe (Doc ann))
forall (w :: Natural).
SymNat sym -> SymBV sym w -> f (Maybe (Doc ann))
ppInt SymNat sym
blk SymBV sym w
w
        where
          otherDoc :: Doc ann
otherDoc =
            case SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat SymNat sym
blk of
              Just Natural
0 ->
                case (SymBV sym w -> Maybe (BV w)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymBV sym w
w) of
                  (Just (BV.BV Integer
unsigned)) -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
                    [ String
"literal integer:"
                    , String
"unsigned value = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
unsigned String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
","
                    , [String] -> String
unwords [ String
"signed value = "
                              , Integer -> String
forall a. Show a => a -> String
show (NatRepr w -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
w) Integer
unsigned) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
","
                              ]
                    , String
"width = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall a. Show a => a -> String
show (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
w)
                    ]
                  Maybe (BV w)
Nothing -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
                    [ String
"symbolic integer: "
                    , String
"width = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall a. Show a => a -> String
show (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
w)
                    ]
              Just Natural
n ->
                case SymBV sym w -> Maybe (BV w)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymBV sym w
w of
                  Just (BV.BV Integer
offset) -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
                    [ String
"concrete pointer:"
                    , String
"allocation = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
","
                    , String
"offset = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
offset
                    ]
                  Maybe (BV w)
Nothing -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
                    [ String
"pointer with concrete allocation and symbolic offset:"
                    , String
"allocation = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n
                    ]

              Maybe Natural
Nothing ->
                case SymBV sym w -> Maybe (BV w)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymBV sym w
w of
                  Just (BV.BV Integer
offset) -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$
                    String
"pointer with concrete offset " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
offset
                  Maybe (BV w)
Nothing -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"pointer with symbolic offset"

      (LLVMValFloat FloatSize fi
SingleSize SymInterpretedFloat sym fi
_) -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> f (Doc ann)) -> Doc ann -> f (Doc ann)
forall a b. (a -> b) -> a -> b
$ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"symbolic float"
      (LLVMValFloat FloatSize fi
DoubleSize SymInterpretedFloat sym fi
_) -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> f (Doc ann)) -> Doc ann -> f (Doc ann)
forall a b. (a -> b) -> a -> b
$ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"symbolic double"
      (LLVMValFloat FloatSize fi
X86_FP80Size SymInterpretedFloat sym fi
_) -> Doc ann -> f (Doc ann)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> f (Doc ann)) -> Doc ann -> f (Doc ann)
forall a b. (a -> b) -> a -> b
$ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"symbolic long double"
      (LLVMValStruct Vector (Field StorageType, LLVMVal sym)
xs) -> Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep Doc ann
forall ann. Doc ann
lbrace Doc ann
forall ann. Doc ann
rbrace Doc ann
forall ann. Doc ann
semi ([Doc ann] -> Doc ann) -> f [Doc ann] -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Field StorageType, LLVMVal sym) -> f (Doc ann))
-> [(Field StorageType, LLVMVal sym)] -> f [Doc ann]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (LLVMVal sym -> f (Doc ann)
pp (LLVMVal sym -> f (Doc ann))
-> ((Field StorageType, LLVMVal sym) -> LLVMVal sym)
-> (Field StorageType, LLVMVal sym)
-> f (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall a b. (a, b) -> b
snd) (Vector (Field StorageType, LLVMVal sym)
-> [(Field StorageType, LLVMVal sym)]
forall a. Vector a -> [a]
V.toList Vector (Field StorageType, LLVMVal sym)
xs)
      (LLVMValArray StorageType
_ Vector (LLVMVal sym)
xs) -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
list ([Doc ann] -> Doc ann) -> f [Doc ann] -> f (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (LLVMVal sym -> f (Doc ann)) -> [LLVMVal sym] -> f [Doc ann]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse LLVMVal sym -> f (Doc ann)
pp (Vector (LLVMVal sym) -> [LLVMVal sym]
forall a. Vector a -> [a]
V.toList Vector (LLVMVal sym)
xs)

-- | Pretty-print an 'LLVMVal', but replace pointers to globals with the name of
--   the global when possible. Probably pretty slow on big structures.
ppLLVMValWithGlobals ::
  forall sym ann.
  (IsSymInterface sym) =>
  sym ->
  Map Natural L.Symbol {- ^ c.f. 'memImplSymbolMap' -} ->
  LLVMVal sym ->
  Doc ann
ppLLVMValWithGlobals :: forall sym ann.
IsSymInterface sym =>
sym -> Map Natural Symbol -> LLVMVal sym -> Doc ann
ppLLVMValWithGlobals sym
_sym Map Natural Symbol
symbolMap = Identity (Doc ann) -> Doc ann
forall a. Identity a -> a
runIdentity (Identity (Doc ann) -> Doc ann)
-> (LLVMVal sym -> Identity (Doc ann)) -> LLVMVal sym -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (w :: Natural).
 SymNat sym -> SymBV sym w -> Identity (Maybe (Doc ann)))
-> LLVMVal sym -> Identity (Doc ann)
forall (f :: Type -> Type) sym ann.
(Applicative f, IsExpr (SymExpr sym)) =>
(forall (w :: Natural).
 SymNat sym -> SymBV sym w -> f (Maybe (Doc ann)))
-> LLVMVal sym -> f (Doc ann)
ppLLVMVal SymNat sym -> SymBV sym w -> Identity (Maybe (Doc ann))
forall (w :: Natural).
SymNat sym -> SymBV sym w -> Identity (Maybe (Doc ann))
ppInt
  where
    ppInt :: forall w. SymNat sym -> SymBV sym w -> Identity (Maybe (Doc ann))
    ppInt :: forall (w :: Natural).
SymNat sym -> SymBV sym w -> Identity (Maybe (Doc ann))
ppInt SymNat sym
allocNum SymBV sym w
offset =
      Maybe (Doc ann) -> Identity (Maybe (Doc ann))
forall a. a -> Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Symbol -> Doc ann
forall {ann}. Symbol -> Doc ann
ppSymbol (Symbol -> Doc ann) -> Maybe Symbol -> Maybe (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
IsSymInterface sym =>
Map Natural Symbol -> LLVMPtr sym w -> Maybe Symbol
isGlobalPointer' @sym Map Natural Symbol
symbolMap (SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
allocNum SymBV sym w
offset))
    ppSymbol :: Symbol -> Doc ann
ppSymbol (L.Symbol String
symb) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Char
'@' Char -> ShowS
forall a. a -> [a] -> [a]
: String
symb)

-- | This instance tries to make things as concrete as possible.
instance IsExpr (SymExpr sym) => Pretty (LLVMVal sym) where
  pretty :: forall ann. LLVMVal sym -> Doc ann
pretty LLVMVal sym
x = Identity (Doc ann) -> Doc ann
forall a. Identity a -> a
runIdentity (Identity (Doc ann) -> Doc ann) -> Identity (Doc ann) -> Doc ann
forall a b. (a -> b) -> a -> b
$ (forall (w :: Natural).
 SymNat sym -> SymBV sym w -> Identity (Maybe (Doc ann)))
-> LLVMVal sym -> Identity (Doc ann)
forall (f :: Type -> Type) sym ann.
(Applicative f, IsExpr (SymExpr sym)) =>
(forall (w :: Natural).
 SymNat sym -> SymBV sym w -> f (Maybe (Doc ann)))
-> LLVMVal sym -> f (Doc ann)
ppLLVMVal (\SymNat sym
_ SymBV sym w
_ -> Maybe (Doc ann) -> Identity (Maybe (Doc ann))
forall a. a -> Identity a
Identity Maybe (Doc ann)
forall a. Maybe a
Nothing) LLVMVal sym
x

instance IsExpr (SymExpr sym) => Show (LLVMVal sym) where
  show :: LLVMVal sym -> String
show (LLVMValZero StorageType
_tp) = String
"0"
  show (LLVMValUndef StorageType
tp) = String
"<undef : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ StorageType -> String
forall a. Show a => a -> String
show StorageType
tp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
  show (LLVMValString  ByteString
_) = String
"<string>"
  show (LLVMValInt SymNat sym
blk SymBV sym w
w)
    | Just Natural
0 <- SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat SymNat sym
blk = String
"<int" String -> ShowS
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall a. Show a => a -> String
show (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
w) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
    | Bool
otherwise = String
"<ptr " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall a. Show a => a -> String
show (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
w) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"
  show (LLVMValFloat FloatSize fi
SingleSize SymInterpretedFloat sym fi
_) = String
"<float>"
  show (LLVMValFloat FloatSize fi
DoubleSize SymInterpretedFloat sym fi
_) = String
"<double>"
  show (LLVMValFloat FloatSize fi
X86_FP80Size SymInterpretedFloat sym fi
_) = String
"<long double>"
  show (LLVMValStruct Vector (Field StorageType, LLVMVal sym)
xs) =
    [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
"{" ]
           [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
", " (((Field StorageType, LLVMVal sym) -> String)
-> [(Field StorageType, LLVMVal sym)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (LLVMVal sym -> String
forall a. Show a => a -> String
show (LLVMVal sym -> String)
-> ((Field StorageType, LLVMVal sym) -> LLVMVal sym)
-> (Field StorageType, LLVMVal sym)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall a b. (a, b) -> b
snd) ([(Field StorageType, LLVMVal sym)] -> [String])
-> [(Field StorageType, LLVMVal sym)] -> [String]
forall a b. (a -> b) -> a -> b
$ Vector (Field StorageType, LLVMVal sym)
-> [(Field StorageType, LLVMVal sym)]
forall a. Vector a -> [a]
V.toList Vector (Field StorageType, LLVMVal sym)
xs)
           [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"}" ]
  show (LLVMValArray StorageType
_ Vector (LLVMVal sym)
xs) =
    [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
"[" ]
           [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
", " ((LLVMVal sym -> String) -> [LLVMVal sym] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map LLVMVal sym -> String
forall a. Show a => a -> String
show ([LLVMVal sym] -> [String]) -> [LLVMVal sym] -> [String]
forall a b. (a -> b) -> a -> b
$ Vector (LLVMVal sym) -> [LLVMVal sym]
forall a. Vector a -> [a]
V.toList Vector (LLVMVal sym)
xs)
           [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"]" ]

-- | An efficient n-way @and@: it quits early if it finds any concretely false
-- values, rather than chaining a bunch of 'andPred's.
allOf :: (IsExprBuilder sym)
      => sym
      -> [Pred sym]
      -> IO (Pred sym)
allOf :: forall sym. IsExprBuilder sym => sym -> [Pred sym] -> IO (Pred sym)
allOf sym
sym [Pred sym]
xs =
  if [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and ((Pred sym -> Maybe Bool) -> [Pred sym] -> [Bool]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred [Pred sym]
xs)
  then (Pred sym -> Pred sym -> IO (Pred sym))
-> Pred sym -> [Pred sym] -> IO (Pred sym)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym) (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) [Pred sym]
xs
  else Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)

{-
-- | An efficient n-way @or@: it quits early if it finds any concretely false
-- values, rather than chaining a bunch of 'orPred's.
oneOf :: (IsExprBuilder sym)
      => sym
      -> [Pred sym]
      -> IO (Pred sym)
oneOf sym xs =
  if or (mapMaybe asConstantPred xs)
  then pure (truePred sym)
  else foldM (orPred sym) (falsePred sym) xs
-}

-- | Commute an applicative with Maybe
commuteMaybe :: Applicative n => Maybe (n a) -> n (Maybe a)
commuteMaybe :: forall (n :: Type -> Type) a.
Applicative n =>
Maybe (n a) -> n (Maybe a)
commuteMaybe (Just n a
val) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> n a -> n (Maybe a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> n a
val
commuteMaybe Maybe (n a)
Nothing    = Maybe a -> n (Maybe a)
forall a. a -> n a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing

-- | This should be used with caution: it is very inefficient to expand zeroes,
-- especially to large data structures (e.g. long arrays).
zeroExpandLLVMVal :: (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym)
                  => sym -> StorageType -> IO (LLVMVal sym)
zeroExpandLLVMVal :: forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> StorageType -> IO (LLVMVal sym)
zeroExpandLLVMVal sym
sym (StorageType StorageTypeF StorageType
tpf Bytes
_sz) =
  case StorageTypeF StorageType
tpf of
    Bitvector Bytes
bytes ->
      case Natural -> Some NatRepr
mkNatRepr (Bytes -> Natural
bytesToBits Bytes
bytes) of
        Some (NatRepr x
repr :: NatRepr w) ->
          case NatRepr 0 -> NatRepr x -> NatCases 0 x
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @0) NatRepr x
repr of
            NatCaseLT (LeqProof 1 x
LeqProof :: LeqProof 1 w) ->
              SymNat sym -> SymBV sym x -> LLVMVal sym
forall (fi :: Natural) sym.
(1 <= fi) =>
SymNat sym -> SymBV sym fi -> LLVMVal sym
LLVMValInt (SymNat sym -> SymBV sym x -> LLVMVal sym)
-> IO (SymNat sym) -> IO (SymBV sym x -> LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
0 IO (SymBV sym x -> LLVMVal sym)
-> IO (SymBV sym x) -> IO (LLVMVal sym)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> NatRepr x -> IO (SymBV sym x)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr x
repr
            NatCases 0 x
NatCaseEQ -> String -> [String] -> IO (LLVMVal sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"zeroExpandLLVMVal" [String
"Zero value inside Bytes"]
            NatCaseGT (LeqProof (x + 1) 0
LeqProof :: LeqProof (w + 1) 0) ->
              String -> [String] -> IO (LLVMVal sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"zeroExpandLLVMVal" [String
"Impossible: (w + 1) </= 0"]
    StorageTypeF StorageType
Float    -> FloatSize 'SingleFloat
-> SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'SingleFloat
SingleSize (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat)
 -> LLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat))
-> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> FloatInfoRepr 'SingleFloat
-> IO (SymExpr sym (SymInterpretedFloatType sym 'SingleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatPZero sym
sym FloatInfoRepr 'SingleFloat
SingleFloatRepr
    StorageTypeF StorageType
Double   -> FloatSize 'DoubleFloat
-> SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'DoubleFloat
DoubleSize (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat)
 -> LLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat))
-> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> FloatInfoRepr 'DoubleFloat
-> IO (SymExpr sym (SymInterpretedFloatType sym 'DoubleFloat))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatPZero sym
sym FloatInfoRepr 'DoubleFloat
DoubleFloatRepr
    StorageTypeF StorageType
X86_FP80 -> FloatSize 'X86_80Float
-> SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
-> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize 'X86_80Float
X86_FP80Size (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float)
 -> LLVMVal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float))
-> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> FloatInfoRepr 'X86_80Float
-> IO (SymExpr sym (SymInterpretedFloatType sym 'X86_80Float))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatPZero sym
sym FloatInfoRepr 'X86_80Float
X86_80FloatRepr
    Array Natural
n StorageType
ty
      | Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int) ->
        StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
ty (Vector (LLVMVal sym) -> LLVMVal sym)
-> (LLVMVal sym -> Vector (LLVMVal sym))
-> LLVMVal sym
-> LLVMVal sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> LLVMVal sym -> Vector (LLVMVal sym)
forall a. Int -> a -> Vector a
V.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n :: Int) (LLVMVal sym -> LLVMVal sym)
-> IO (LLVMVal sym) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
          sym -> StorageType -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> StorageType -> IO (LLVMVal sym)
zeroExpandLLVMVal sym
sym StorageType
ty
      | Bool
otherwise -> String -> [String] -> IO (LLVMVal sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"zeroExpandLLVMVal" [String
"Array length too large", Natural -> String
forall a. Show a => a -> String
show Natural
n]
    Struct Vector (Field StorageType)
vec ->
      Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall sym. Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym
LLVMValStruct (Vector (Field StorageType, LLVMVal sym) -> LLVMVal sym)
-> IO (Vector (Field StorageType, LLVMVal sym)) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (Field StorageType
 -> StorageType -> IO (Field StorageType, LLVMVal sym))
-> Vector (Field StorageType)
-> Vector StorageType
-> IO (Vector (Field StorageType, LLVMVal sym))
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> m c) -> Vector a -> Vector b -> m (Vector c)
V.zipWithM (\Field StorageType
f StorageType
t -> (Field StorageType
f,) (LLVMVal sym -> (Field StorageType, LLVMVal sym))
-> IO (LLVMVal sym) -> IO (Field StorageType, LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> StorageType -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> StorageType -> IO (LLVMVal sym)
zeroExpandLLVMVal sym
sym StorageType
t) Vector (Field StorageType)
vec ((Field StorageType -> StorageType)
-> Vector (Field StorageType) -> Vector StorageType
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Getting StorageType (Field StorageType) StorageType
-> Field StorageType -> StorageType
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting StorageType (Field StorageType) StorageType
forall a b (f :: Type -> Type).
Functor f =>
(a -> f b) -> Field a -> f (Field b)
fieldVal) Vector (Field StorageType)
vec)

-- | A special case for comparing values to the distinguished zero value.
--
-- Should be faster than using 'testEqual' with 'zeroExpandLLVMVal' for compound
-- values, because we 'traverse' subcomponents of vectors and structs, quitting
-- early on a constantly false answer or 'LLVMValUndef'.
--
-- Returns 'Nothing' for 'LLVMValUndef'.
isZero :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym)
       => sym -> LLVMVal sym -> IO (Maybe (Pred sym))
isZero :: forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> LLVMVal sym -> IO (Maybe (Pred sym))
isZero sym
sym LLVMVal sym
v =
  case LLVMVal sym
v of
    LLVMValStruct Vector (Field StorageType, LLVMVal sym)
fs  -> Vector (LLVMVal sym) -> IO (Maybe (Pred sym))
forall (t :: Type -> Type).
Traversable t =>
t (LLVMVal sym) -> IO (Maybe (Pred sym))
areZero' (((Field StorageType, LLVMVal sym) -> LLVMVal sym)
-> Vector (Field StorageType, LLVMVal sym) -> Vector (LLVMVal sym)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall a b. (a, b) -> b
snd Vector (Field StorageType, LLVMVal sym)
fs)
    LLVMValArray StorageType
_ Vector (LLVMVal sym)
vs -> Vector (LLVMVal sym) -> IO (Maybe (Pred sym))
forall (t :: Type -> Type).
Traversable t =>
t (LLVMVal sym) -> IO (Maybe (Pred sym))
areZero' Vector (LLVMVal sym)
vs
    LLVMValString ByteString
bs  -> Maybe (Pred sym) -> IO (Maybe (Pred sym))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe (Pred sym) -> IO (Maybe (Pred sym)))
-> Maybe (Pred sym) -> IO (Maybe (Pred sym))
forall a b. (a -> b) -> a -> b
$ Pred sym -> Maybe (Pred sym)
forall a. a -> Maybe a
Just (Pred sym -> Maybe (Pred sym)) -> Pred sym -> Maybe (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Bool -> Pred sym
forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
backendPred sym
sym (Bool -> Pred sym) -> Bool -> Pred sym
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe Word8 -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Word8 -> Bool) -> Maybe Word8 -> Bool
forall a b. (a -> b) -> a -> b
$ (Word8 -> Bool) -> ByteString -> Maybe Word8
BS.find (Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word8
0) ByteString
bs
    LLVMValZero StorageType
_     -> Maybe (Pred sym) -> IO (Maybe (Pred sym))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> Maybe (Pred sym)
forall a. a -> Maybe a
Just (Pred sym -> Maybe (Pred sym)) -> Pred sym -> Maybe (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym)
    LLVMValUndef StorageType
_    -> Maybe (Pred sym) -> IO (Maybe (Pred sym))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (Pred sym)
forall a. Maybe a
Nothing
    LLVMVal sym
_                 ->
      -- For atomic types, we simply expand and compare.
      sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
testEqual sym
sym LLVMVal sym
v (LLVMVal sym -> IO (Maybe (Pred sym)))
-> IO (LLVMVal sym) -> IO (Maybe (Pred sym))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> StorageType -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> StorageType -> IO (LLVMVal sym)
zeroExpandLLVMVal sym
sym (LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
llvmValStorableType LLVMVal sym
v)
  where
    areZero :: Traversable t => t (LLVMVal sym) -> IO (Maybe (t (Pred sym)))
    areZero :: forall (t :: Type -> Type).
Traversable t =>
t (LLVMVal sym) -> IO (Maybe (t (Pred sym)))
areZero = (t (Maybe (Pred sym)) -> Maybe (t (Pred sym)))
-> IO (t (Maybe (Pred sym))) -> IO (Maybe (t (Pred sym)))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap t (Maybe (Pred sym)) -> Maybe (t (Pred sym))
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a)
sequence (IO (t (Maybe (Pred sym))) -> IO (Maybe (t (Pred sym))))
-> (t (LLVMVal sym) -> IO (t (Maybe (Pred sym))))
-> t (LLVMVal sym)
-> IO (Maybe (t (Pred sym)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LLVMVal sym -> IO (Maybe (Pred sym)))
-> t (LLVMVal sym) -> IO (t (Maybe (Pred sym)))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b)
traverse (sym -> LLVMVal sym -> IO (Maybe (Pred sym))
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> LLVMVal sym -> IO (Maybe (Pred sym))
isZero sym
sym)
    areZero' :: Traversable t => t (LLVMVal sym) -> IO (Maybe (Pred sym))
    areZero' :: forall (t :: Type -> Type).
Traversable t =>
t (LLVMVal sym) -> IO (Maybe (Pred sym))
areZero' t (LLVMVal sym)
vs =
      -- This could probably be simplified with a well-placed =<<...
      IO (IO (Maybe (Pred sym))) -> IO (Maybe (Pred sym))
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (IO (IO (Maybe (Pred sym))) -> IO (Maybe (Pred sym)))
-> IO (IO (Maybe (Pred sym))) -> IO (Maybe (Pred sym))
forall a b. (a -> b) -> a -> b
$ (Maybe (IO (Pred sym)) -> IO (Maybe (Pred sym)))
-> IO (Maybe (IO (Pred sym))) -> IO (IO (Maybe (Pred sym)))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe (IO (Pred sym)) -> IO (Maybe (Pred sym))
forall (n :: Type -> Type) a.
Applicative n =>
Maybe (n a) -> n (Maybe a)
commuteMaybe (IO (Maybe (IO (Pred sym))) -> IO (IO (Maybe (Pred sym))))
-> IO (Maybe (IO (Pred sym))) -> IO (IO (Maybe (Pred sym)))
forall a b. (a -> b) -> a -> b
$ (Maybe (t (Pred sym)) -> Maybe (IO (Pred sym)))
-> IO (Maybe (t (Pred sym))) -> IO (Maybe (IO (Pred sym)))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((t (Pred sym) -> IO (Pred sym))
-> Maybe (t (Pred sym)) -> Maybe (IO (Pred sym))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (sym -> [Pred sym] -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> [Pred sym] -> IO (Pred sym)
allOf sym
sym ([Pred sym] -> IO (Pred sym))
-> (t (Pred sym) -> [Pred sym]) -> t (Pred sym) -> IO (Pred sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (Pred sym) -> [Pred sym]
forall a. t a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList)) (IO (Maybe (t (Pred sym))) -> IO (Maybe (IO (Pred sym))))
-> IO (Maybe (t (Pred sym))) -> IO (Maybe (IO (Pred sym)))
forall a b. (a -> b) -> a -> b
$ t (LLVMVal sym) -> IO (Maybe (t (Pred sym)))
forall (t :: Type -> Type).
Traversable t =>
t (LLVMVal sym) -> IO (Maybe (t (Pred sym)))
areZero t (LLVMVal sym)
vs

-- | A predicate denoting the equality of two LLVMVals.
--
-- Returns 'Nothing' in the event that one of the values contains 'LLVMValUndef'.
testEqual :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym)
          => sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
testEqual :: forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
testEqual sym
sym LLVMVal sym
v1 LLVMVal sym
v2 =
  case (LLVMVal sym
v1, LLVMVal sym
v2) of
    (LLVMValInt SymNat sym
blk1 SymBV sym w
off1, LLVMValInt SymNat sym
blk2 SymBV sym w
off2) ->
      case NatRepr w -> NatRepr w -> Maybe (w :~: w)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
off1) (SymBV sym w -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
off2) of
        Maybe (w :~: w)
Nothing   -> IO (Maybe (Pred sym))
false
        Just w :~: w
Refl ->
          sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
blk1 SymNat sym
blk2 IO (Pred sym)
-> (Pred sym -> IO (Maybe (Pred sym))) -> IO (Maybe (Pred sym))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Pred sym
p1 ->
            Pred sym -> Maybe (Pred sym)
forall a. a -> Maybe a
Just (Pred sym -> Maybe (Pred sym))
-> IO (Pred sym) -> IO (Maybe (Pred sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
off1 SymBV sym w
SymBV sym w
off2)
    (LLVMValFloat (FloatSize fi
sz1 :: FloatSize fi1) SymInterpretedFloat sym fi
flt1, LLVMValFloat FloatSize fi
sz2 SymInterpretedFloat sym fi
flt2) ->
      case FloatSize fi -> FloatSize fi -> Maybe (fi :~: fi)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: FloatInfo) (b :: FloatInfo).
FloatSize a -> FloatSize b -> Maybe (a :~: b)
testEquality FloatSize fi
sz1 FloatSize fi
sz2 of
        Maybe (fi :~: fi)
Nothing   -> IO (Maybe (Pred sym))
false
        Just fi :~: fi
Refl -> Pred sym -> Maybe (Pred sym)
forall a. a -> Maybe a
Just (Pred sym -> Maybe (Pred sym))
-> IO (Pred sym) -> IO (Maybe (Pred sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatEq @_ @fi1 sym
sym SymInterpretedFloat sym fi
flt1 SymInterpretedFloat sym fi
SymInterpretedFloat sym fi
flt2
    (LLVMValArray StorageType
tp1 Vector (LLVMVal sym)
vec1, LLVMValArray StorageType
tp2 Vector (LLVMVal sym)
vec2) ->
      Bool -> IO (Maybe (Pred sym)) -> IO (Maybe (Pred sym))
andAlso (StorageType
tp1 StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp2 Bool -> Bool -> Bool
&& Vector (LLVMVal sym) -> Int
forall a. Vector a -> Int
V.length Vector (LLVMVal sym)
vec1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (LLVMVal sym) -> Int
forall a. Vector a -> Int
V.length Vector (LLVMVal sym)
vec2) (Vector (LLVMVal sym)
-> Vector (LLVMVal sym) -> IO (Maybe (Pred sym))
allEqual Vector (LLVMVal sym)
vec1 Vector (LLVMVal sym)
vec2)
    (LLVMValStruct Vector (Field StorageType, LLVMVal sym)
vec1, LLVMValStruct Vector (Field StorageType, LLVMVal sym)
vec2) ->
      let (Vector (Field StorageType)
si1, Vector (Field StorageType)
si2) = (((Field StorageType, LLVMVal sym) -> Field StorageType)
-> Vector (Field StorageType, LLVMVal sym)
-> Vector (Field StorageType)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Field StorageType, LLVMVal sym) -> Field StorageType
forall a b. (a, b) -> a
fst Vector (Field StorageType, LLVMVal sym)
vec1, ((Field StorageType, LLVMVal sym) -> Field StorageType)
-> Vector (Field StorageType, LLVMVal sym)
-> Vector (Field StorageType)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Field StorageType, LLVMVal sym) -> Field StorageType
forall a b. (a, b) -> a
fst Vector (Field StorageType, LLVMVal sym)
vec2)
          (Vector (LLVMVal sym)
fd1, Vector (LLVMVal sym)
fd2) = (((Field StorageType, LLVMVal sym) -> LLVMVal sym)
-> Vector (Field StorageType, LLVMVal sym) -> Vector (LLVMVal sym)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall a b. (a, b) -> b
snd Vector (Field StorageType, LLVMVal sym)
vec1, ((Field StorageType, LLVMVal sym) -> LLVMVal sym)
-> Vector (Field StorageType, LLVMVal sym) -> Vector (LLVMVal sym)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Field StorageType, LLVMVal sym) -> LLVMVal sym
forall a b. (a, b) -> b
snd Vector (Field StorageType, LLVMVal sym)
vec2)
      in Bool -> IO (Maybe (Pred sym)) -> IO (Maybe (Pred sym))
andAlso (Vector (Field StorageType, LLVMVal sym) -> Int
forall a. Vector a -> Int
V.length Vector (Field StorageType, LLVMVal sym)
vec1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (Field StorageType, LLVMVal sym) -> Int
forall a. Vector a -> Int
V.length Vector (Field StorageType, LLVMVal sym)
vec2 Bool -> Bool -> Bool
&& Vector Bool -> Bool
V.and ((Field StorageType -> Field StorageType -> Bool)
-> Vector (Field StorageType)
-> Vector (Field StorageType)
-> Vector Bool
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith Field StorageType -> Field StorageType -> Bool
forall a. Eq a => a -> a -> Bool
(==) Vector (Field StorageType)
si1 Vector (Field StorageType)
si2))
                 (Vector (LLVMVal sym)
-> Vector (LLVMVal sym) -> IO (Maybe (Pred sym))
allEqual Vector (LLVMVal sym)
fd1 Vector (LLVMVal sym)
fd2)

    (LLVMValString ByteString
bs1, LLVMValString ByteString
bs2) -> if ByteString
bs1 ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
bs2 then IO (Maybe (Pred sym))
true else IO (Maybe (Pred sym))
false
    (LLVMValString ByteString
bs, v :: LLVMVal sym
v@LLVMValArray{}) ->
      do LLVMVal sym
bsv <- sym -> ByteString -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
explodeStringValue sym
sym ByteString
bs
         sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
testEqual sym
sym LLVMVal sym
bsv LLVMVal sym
v
    (v :: LLVMVal sym
v@LLVMValArray{}, LLVMValString ByteString
bs) ->
      do LLVMVal sym
bsv <- sym -> ByteString -> IO (LLVMVal sym)
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
explodeStringValue sym
sym ByteString
bs
         sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
testEqual sym
sym LLVMVal sym
v LLVMVal sym
bsv

    (LLVMValZero StorageType
tp1, LLVMValZero StorageType
tp2) -> if StorageType
tp1 StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp2 then IO (Maybe (Pred sym))
true else IO (Maybe (Pred sym))
false
    (LLVMValZero StorageType
tp, LLVMVal sym
other) -> StorageType -> LLVMVal sym -> IO (Maybe (Pred sym))
compareZero StorageType
tp LLVMVal sym
other
    (LLVMVal sym
other, LLVMValZero StorageType
tp) -> StorageType -> LLVMVal sym -> IO (Maybe (Pred sym))
compareZero StorageType
tp LLVMVal sym
other
    (LLVMValUndef StorageType
_, LLVMVal sym
_) -> Maybe (Pred sym) -> IO (Maybe (Pred sym))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (Pred sym)
forall a. Maybe a
Nothing
    (LLVMVal sym
_, LLVMValUndef StorageType
_) -> Maybe (Pred sym) -> IO (Maybe (Pred sym))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (Pred sym)
forall a. Maybe a
Nothing
    (LLVMVal sym
_, LLVMVal sym
_) -> IO (Maybe (Pred sym))
false -- type mismatch

  where true :: IO (Maybe (Pred sym))
true = Maybe (Pred sym) -> IO (Maybe (Pred sym))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> Maybe (Pred sym)
forall a. a -> Maybe a
Just (Pred sym -> Maybe (Pred sym)) -> Pred sym -> Maybe (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym)
        false :: IO (Maybe (Pred sym))
false = Maybe (Pred sym) -> IO (Maybe (Pred sym))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> Maybe (Pred sym)
forall a. a -> Maybe a
Just (Pred sym -> Maybe (Pred sym)) -> Pred sym -> Maybe (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)

        andAlso :: Bool -> IO (Maybe (Pred sym)) -> IO (Maybe (Pred sym))
andAlso Bool
b IO (Maybe (Pred sym))
x = if Bool
b then IO (Maybe (Pred sym))
x else IO (Maybe (Pred sym))
false

        allEqual :: Vector (LLVMVal sym)
-> Vector (LLVMVal sym) -> IO (Maybe (Pred sym))
allEqual Vector (LLVMVal sym)
vs1 Vector (LLVMVal sym)
vs2 =
          (Maybe (Pred sym) -> Maybe (Pred sym) -> IO (Maybe (Pred sym)))
-> Maybe (Pred sym)
-> Vector (Maybe (Pred sym))
-> IO (Maybe (Pred sym))
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Maybe (Pred sym)
x Maybe (Pred sym)
y -> Maybe (IO (Pred sym)) -> IO (Maybe (Pred sym))
forall (n :: Type -> Type) a.
Applicative n =>
Maybe (n a) -> n (Maybe a)
commuteMaybe (sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym (Pred sym -> Pred sym -> IO (Pred sym))
-> Maybe (Pred sym) -> Maybe (Pred sym -> IO (Pred sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Pred sym)
x Maybe (Pred sym -> IO (Pred sym))
-> Maybe (Pred sym) -> Maybe (IO (Pred sym))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Maybe (Pred sym)
y)) (Pred sym -> Maybe (Pred sym)
forall a. a -> Maybe a
Just (Pred sym -> Maybe (Pred sym)) -> Pred sym -> Maybe (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) (Vector (Maybe (Pred sym)) -> IO (Maybe (Pred sym)))
-> IO (Vector (Maybe (Pred sym))) -> IO (Maybe (Pred sym))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<<
            (LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym)))
-> Vector (LLVMVal sym)
-> Vector (LLVMVal sym)
-> IO (Vector (Maybe (Pred sym)))
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> m c) -> Vector a -> Vector b -> m (Vector c)
V.zipWithM (sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
testEqual sym
sym) Vector (LLVMVal sym)
vs1 Vector (LLVMVal sym)
vs2

        -- This is probably inefficient:
        compareZero :: StorageType -> LLVMVal sym -> IO (Maybe (Pred sym))
compareZero StorageType
tp LLVMVal sym
other =
          Bool -> IO (Maybe (Pred sym)) -> IO (Maybe (Pred sym))
andAlso (LLVMVal sym -> StorageType
forall sym. IsExprBuilder sym => LLVMVal sym -> StorageType
llvmValStorableType LLVMVal sym
other StorageType -> StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageType
tp) (IO (Maybe (Pred sym)) -> IO (Maybe (Pred sym)))
-> IO (Maybe (Pred sym)) -> IO (Maybe (Pred sym))
forall a b. (a -> b) -> a -> b
$ sym -> LLVMVal sym -> IO (Maybe (Pred sym))
forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> LLVMVal sym -> IO (Maybe (Pred sym))
isZero sym
sym LLVMVal sym
other


-- | Turns a bytestring into an explicit array of bytes
explodeStringValue :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
  sym -> ByteString -> IO (LLVMVal sym)
explodeStringValue :: forall sym.
(IsExprBuilder sym, IsInterpretedFloatExprBuilder sym) =>
sym -> ByteString -> IO (LLVMVal sym)
explodeStringValue sym
sym ByteString
bs =
  do SymNat sym
blk <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
0
     Vector (LLVMVal sym)
vs <- Int -> (Int -> IO (LLVMVal sym)) -> IO (Vector (LLVMVal sym))
forall (m :: Type -> Type) a.
Monad m =>
Int -> (Int -> m a) -> m (Vector a)
V.generateM (ByteString -> Int
BS.length ByteString
bs)
              (\Int
i -> SymNat sym -> SymExpr sym (BaseBVType 8) -> LLVMVal sym
forall (fi :: Natural) sym.
(1 <= fi) =>
SymNat sym -> SymBV sym fi -> LLVMVal sym
LLVMValInt SymNat sym
blk (SymExpr sym (BaseBVType 8) -> LLVMVal sym)
-> IO (SymExpr sym (BaseBVType 8)) -> IO (LLVMVal sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> NatRepr 8 -> BV 8 -> IO (SymExpr sym (BaseBVType 8))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) (Word8 -> BV 8
BV.word8 (HasCallStack => ByteString -> Int -> Word8
ByteString -> Int -> Word8
BS.index ByteString
bs Int
i)))
     LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray (Bytes -> StorageType
bitvectorType (Integer -> Bytes
Bytes Integer
1)) Vector (LLVMVal sym)
vs)