-- |
-- Module           : Lang.Crucible.LLVM.Errors.MemoryError
-- Description      : Errors that arise when reading and writing memory
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Langston Barrett <lbarrett@galois.com>
-- Stability        : provisional
--
--------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.LLVM.Errors.MemoryError
( MemoryError(..)
, MemErrContext
, explain
, details
, ppMemoryError
, MemoryOp(..)
, memOpMem
, ppMemoryOp
, MemoryErrorReason(..)
, ppMemoryErrorReason
, FuncLookupError(..)
, ppFuncLookupError

, concMemoryError
, concMemoryOp
) where

import           Prelude hiding (pred)

import           Data.Text (Text)
import qualified Text.LLVM.AST as L
import           Type.Reflection (SomeTypeRep(SomeTypeRep))
import           Prettyprinter

import           What4.Interface
import           What4.Expr (GroundValue)

import           Lang.Crucible.LLVM.MemModel.Pointer (LLVMPtr, concBV)
import           Lang.Crucible.LLVM.MemModel.Common
import           Lang.Crucible.LLVM.MemModel.Type
import           Lang.Crucible.LLVM.MemModel.MemLog
import qualified Lang.Crucible.LLVM.PrettyPrint as LPP

data MemoryOp sym w
  = MemLoadOp  StorageType (Maybe String) (LLVMPtr sym w) (Mem sym)
  | MemStoreOp StorageType (Maybe String) (LLVMPtr sym w) (Mem sym)
  | MemStoreBytesOp (Maybe String) (LLVMPtr sym w) (Maybe (SymBV sym w)) (Mem sym)
  | forall wlen. (1 <= wlen) => MemCopyOp
       (Maybe String, LLVMPtr sym w) -- dest
       (Maybe String, LLVMPtr sym w) -- src
       (SymBV sym wlen) -- length
       (Mem sym)
  | MemLoadHandleOp (Maybe L.Type) (Maybe String) (LLVMPtr sym w) (Mem sym)
  | forall wlen. (1 <= wlen) => MemInvalidateOp
       Text (Maybe String) (LLVMPtr sym w) (SymBV sym wlen) (Mem sym)

memOpMem :: MemoryOp sym w -> Mem sym
memOpMem :: forall sym (w :: Nat). MemoryOp sym w -> Mem sym
memOpMem =
  \case
    MemLoadOp StorageType
_ Maybe String
_ LLVMPtr sym w
_ Mem sym
mem -> Mem sym
mem
    MemStoreOp StorageType
_ Maybe String
_ LLVMPtr sym w
_ Mem sym
mem -> Mem sym
mem
    MemStoreBytesOp Maybe String
_ LLVMPtr sym w
_ Maybe (SymBV sym w)
_ Mem sym
mem -> Mem sym
mem
    MemCopyOp (Maybe String, LLVMPtr sym w)
_ (Maybe String, LLVMPtr sym w)
_ SymBV sym wlen
_ Mem sym
mem -> Mem sym
mem
    MemLoadHandleOp Maybe Type
_ Maybe String
_ LLVMPtr sym w
_ Mem sym
mem -> Mem sym
mem
    MemInvalidateOp Text
_ Maybe String
_ LLVMPtr sym w
_ SymBV sym wlen
_ Mem sym
mem -> Mem sym
mem

data MemoryError sym where
  MemoryError :: (1 <= w) =>
    MemoryOp sym w ->
    MemoryErrorReason ->
    MemoryError sym

-- | The kinds of type errors that arise while reading memory/constructing LLVM
-- values
data MemoryErrorReason =
    TypeMismatch StorageType StorageType
  | UnexpectedArgumentType Text [StorageType]
  | ApplyViewFail ValueView
  | Invalid StorageType
  | Invalidated Text
  | NoSatisfyingWrite StorageType
  | UnwritableRegion
  | UnreadableRegion
  | BadFunctionPointer FuncLookupError
  | OverlappingRegions
  deriving (MemoryErrorReason -> MemoryErrorReason -> Bool
(MemoryErrorReason -> MemoryErrorReason -> Bool)
-> (MemoryErrorReason -> MemoryErrorReason -> Bool)
-> Eq MemoryErrorReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MemoryErrorReason -> MemoryErrorReason -> Bool
== :: MemoryErrorReason -> MemoryErrorReason -> Bool
$c/= :: MemoryErrorReason -> MemoryErrorReason -> Bool
/= :: MemoryErrorReason -> MemoryErrorReason -> Bool
Eq, Eq MemoryErrorReason
Eq MemoryErrorReason =>
(MemoryErrorReason -> MemoryErrorReason -> Ordering)
-> (MemoryErrorReason -> MemoryErrorReason -> Bool)
-> (MemoryErrorReason -> MemoryErrorReason -> Bool)
-> (MemoryErrorReason -> MemoryErrorReason -> Bool)
-> (MemoryErrorReason -> MemoryErrorReason -> Bool)
-> (MemoryErrorReason -> MemoryErrorReason -> MemoryErrorReason)
-> (MemoryErrorReason -> MemoryErrorReason -> MemoryErrorReason)
-> Ord MemoryErrorReason
MemoryErrorReason -> MemoryErrorReason -> Bool
MemoryErrorReason -> MemoryErrorReason -> Ordering
MemoryErrorReason -> MemoryErrorReason -> MemoryErrorReason
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MemoryErrorReason -> MemoryErrorReason -> Ordering
compare :: MemoryErrorReason -> MemoryErrorReason -> Ordering
$c< :: MemoryErrorReason -> MemoryErrorReason -> Bool
< :: MemoryErrorReason -> MemoryErrorReason -> Bool
$c<= :: MemoryErrorReason -> MemoryErrorReason -> Bool
<= :: MemoryErrorReason -> MemoryErrorReason -> Bool
$c> :: MemoryErrorReason -> MemoryErrorReason -> Bool
> :: MemoryErrorReason -> MemoryErrorReason -> Bool
$c>= :: MemoryErrorReason -> MemoryErrorReason -> Bool
>= :: MemoryErrorReason -> MemoryErrorReason -> Bool
$cmax :: MemoryErrorReason -> MemoryErrorReason -> MemoryErrorReason
max :: MemoryErrorReason -> MemoryErrorReason -> MemoryErrorReason
$cmin :: MemoryErrorReason -> MemoryErrorReason -> MemoryErrorReason
min :: MemoryErrorReason -> MemoryErrorReason -> MemoryErrorReason
Ord)

-- | Reasons that looking up a function handle associated with an LLVM pointer
-- may fail
data FuncLookupError
  = SymbolicPointer
  | RawBitvector
  | NoOverride
  | Uncallable SomeTypeRep
  deriving (FuncLookupError -> FuncLookupError -> Bool
(FuncLookupError -> FuncLookupError -> Bool)
-> (FuncLookupError -> FuncLookupError -> Bool)
-> Eq FuncLookupError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FuncLookupError -> FuncLookupError -> Bool
== :: FuncLookupError -> FuncLookupError -> Bool
$c/= :: FuncLookupError -> FuncLookupError -> Bool
/= :: FuncLookupError -> FuncLookupError -> Bool
Eq, Eq FuncLookupError
Eq FuncLookupError =>
(FuncLookupError -> FuncLookupError -> Ordering)
-> (FuncLookupError -> FuncLookupError -> Bool)
-> (FuncLookupError -> FuncLookupError -> Bool)
-> (FuncLookupError -> FuncLookupError -> Bool)
-> (FuncLookupError -> FuncLookupError -> Bool)
-> (FuncLookupError -> FuncLookupError -> FuncLookupError)
-> (FuncLookupError -> FuncLookupError -> FuncLookupError)
-> Ord FuncLookupError
FuncLookupError -> FuncLookupError -> Bool
FuncLookupError -> FuncLookupError -> Ordering
FuncLookupError -> FuncLookupError -> FuncLookupError
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FuncLookupError -> FuncLookupError -> Ordering
compare :: FuncLookupError -> FuncLookupError -> Ordering
$c< :: FuncLookupError -> FuncLookupError -> Bool
< :: FuncLookupError -> FuncLookupError -> Bool
$c<= :: FuncLookupError -> FuncLookupError -> Bool
<= :: FuncLookupError -> FuncLookupError -> Bool
$c> :: FuncLookupError -> FuncLookupError -> Bool
> :: FuncLookupError -> FuncLookupError -> Bool
$c>= :: FuncLookupError -> FuncLookupError -> Bool
>= :: FuncLookupError -> FuncLookupError -> Bool
$cmax :: FuncLookupError -> FuncLookupError -> FuncLookupError
max :: FuncLookupError -> FuncLookupError -> FuncLookupError
$cmin :: FuncLookupError -> FuncLookupError -> FuncLookupError
min :: FuncLookupError -> FuncLookupError -> FuncLookupError
Ord)

ppFuncLookupError :: FuncLookupError -> Doc ann
ppFuncLookupError :: forall ann. FuncLookupError -> Doc ann
ppFuncLookupError =
  \case
    FuncLookupError
SymbolicPointer -> Doc ann
"Cannot resolve a symbolic pointer to a function handle"
    FuncLookupError
RawBitvector -> Doc ann
"Cannot treat raw bitvector as function pointer"
    FuncLookupError
NoOverride -> Doc ann
"No implementation or override found for pointer"
    Uncallable (SomeTypeRep TypeRep a
typeRep) ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [ Doc ann
"Data associated with the pointer found, but was not a callable function:"
           , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
hang Int
2 (TypeRep a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow TypeRep a
typeRep)
           ]

type MemErrContext sym w = MemoryOp sym w

ppGSym :: Maybe String -> [Doc ann]
ppGSym :: forall ann. Maybe String -> [Doc ann]
ppGSym Maybe String
Nothing = []
ppGSym (Just String
nm) = [ Doc ann
"Global symbol", String -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow String
nm ]

ppMemoryOp :: IsExpr (SymExpr sym) => MemoryOp sym w -> Doc ann
ppMemoryOp :: forall sym (w :: Nat) ann.
IsExpr (SymExpr sym) =>
MemoryOp sym w -> Doc ann
ppMemoryOp (MemLoadOp StorageType
tp Maybe String
gsym LLVMPtr sym w
ptr Mem sym
mem)  =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [ Doc ann
"Performing overall load at type:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> StorageType -> Doc ann
forall ann. StorageType -> Doc ann
ppType StorageType
tp
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([ Doc ann
"Via pointer:" ] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ Maybe String -> [Doc ann]
forall ann. Maybe String -> [Doc ann]
ppGSym Maybe String
gsym [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [ LLVMPtr sym w -> Doc ann
forall sym (wptr :: Nat) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
ptr ]))
       , Doc ann
"In memory state:"
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Mem sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => Mem sym -> Doc ann
ppMem Mem sym
mem)
       ]

ppMemoryOp (MemStoreOp StorageType
tp Maybe String
gsym LLVMPtr sym w
ptr Mem sym
mem) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [ Doc ann
"Performing store at type:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> StorageType -> Doc ann
forall ann. StorageType -> Doc ann
ppType StorageType
tp
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([ Doc ann
"Via pointer:" ] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ Maybe String -> [Doc ann]
forall ann. Maybe String -> [Doc ann]
ppGSym Maybe String
gsym [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [ LLVMPtr sym w -> Doc ann
forall sym (wptr :: Nat) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
ptr ]))
       , Doc ann
"In memory state:"
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Mem sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => Mem sym -> Doc ann
ppMem Mem sym
mem)
       ]

ppMemoryOp (MemStoreBytesOp Maybe String
gsym LLVMPtr sym w
ptr Maybe (SymBV sym w)
Nothing Mem sym
mem) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [ Doc ann
"Performing byte array store for entire address space"
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([ Doc ann
"Via pointer:" ] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ Maybe String -> [Doc ann]
forall ann. Maybe String -> [Doc ann]
ppGSym Maybe String
gsym [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [ LLVMPtr sym w -> Doc ann
forall sym (wptr :: Nat) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
ptr ]))
       , Doc ann
"In memory state:"
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Mem sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => Mem sym -> Doc ann
ppMem Mem sym
mem)
       ]

ppMemoryOp (MemStoreBytesOp Maybe String
gsym LLVMPtr sym w
ptr (Just SymBV sym w
len) Mem sym
mem) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [ Doc ann
"Performing byte array store of length:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymBV sym w -> 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 SymBV sym w
len
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([ Doc ann
"Via pointer:" ] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ Maybe String -> [Doc ann]
forall ann. Maybe String -> [Doc ann]
ppGSym Maybe String
gsym [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [ LLVMPtr sym w -> Doc ann
forall sym (wptr :: Nat) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
ptr ]))
       , Doc ann
"In memory state:"
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Mem sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => Mem sym -> Doc ann
ppMem Mem sym
mem)
       ]

ppMemoryOp (MemCopyOp (Maybe String
gsym_dest, LLVMPtr sym w
dest) (Maybe String
gsym_src, LLVMPtr sym w
src) SymBV sym wlen
len Mem sym
mem) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [ Doc ann
"Performing a memory copy of" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymBV sym wlen -> 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 SymBV sym wlen
len Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"bytes"
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([ Doc ann
"Destination:" ] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ Maybe String -> [Doc ann]
forall ann. Maybe String -> [Doc ann]
ppGSym Maybe String
gsym_dest [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [ LLVMPtr sym w -> Doc ann
forall sym (wptr :: Nat) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
dest ]))
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([ Doc ann
"Source:     " ] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ Maybe String -> [Doc ann]
forall ann. Maybe String -> [Doc ann]
ppGSym Maybe String
gsym_src [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [ LLVMPtr sym w -> Doc ann
forall sym (wptr :: Nat) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
src ]))
       , Doc ann
"In memory state:"
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Mem sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => Mem sym -> Doc ann
ppMem Mem sym
mem)
       ]

ppMemoryOp (MemLoadHandleOp Maybe Type
sig Maybe String
gsym LLVMPtr sym w
ptr Mem sym
mem) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [ case Maybe Type
sig of
           Just Type
s ->
             [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep [Doc ann
"Attempting to load callable function with type:", Doc -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (Type -> Doc
LPP.ppType Type
s)]
           Maybe Type
Nothing ->
             [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep [Doc ann
"Attempting to load callable function:"]
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([ Doc ann
"Via pointer:" ] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ Maybe String -> [Doc ann]
forall ann. Maybe String -> [Doc ann]
ppGSym Maybe String
gsym [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [ LLVMPtr sym w -> Doc ann
forall sym (wptr :: Nat) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
ptr ]))
       , Doc ann
"In memory state:"
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Mem sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => Mem sym -> Doc ann
ppMem Mem sym
mem)
       ]

ppMemoryOp (MemInvalidateOp Text
msg Maybe String
gsym LLVMPtr sym w
ptr SymBV sym wlen
len Mem sym
mem) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [ Doc ann
"Performing explicit memory invalidation of" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymBV sym wlen -> 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 SymBV sym wlen
len Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"bytes"
       , Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
msg
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([ Doc ann
"Via pointer:" ] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ Maybe String -> [Doc ann]
forall ann. Maybe String -> [Doc ann]
ppGSym Maybe String
gsym [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [ LLVMPtr sym w -> Doc ann
forall sym (wptr :: Nat) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
ptr ]))
       , Doc ann
"In memory state:"
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Mem sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => Mem sym -> Doc ann
ppMem Mem sym
mem)
       ]

explain :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
explain :: forall sym ann. IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
explain (MemoryError MemoryOp sym w
_mop MemoryErrorReason
rsn) = MemoryErrorReason -> Doc ann
forall ann. MemoryErrorReason -> Doc ann
ppMemoryErrorReason MemoryErrorReason
rsn

details :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
details :: forall sym ann. IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
details (MemoryError MemoryOp sym w
mop MemoryErrorReason
_rsn) = MemoryOp sym w -> Doc ann
forall sym (w :: Nat) ann.
IsExpr (SymExpr sym) =>
MemoryOp sym w -> Doc ann
ppMemoryOp MemoryOp sym w
mop

ppMemoryError :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
ppMemoryError :: forall sym ann. IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
ppMemoryError (MemoryError MemoryOp sym w
mop MemoryErrorReason
rsn) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [MemoryErrorReason -> Doc ann
forall ann. MemoryErrorReason -> Doc ann
ppMemoryErrorReason MemoryErrorReason
rsn, MemoryOp sym w -> Doc ann
forall sym (w :: Nat) ann.
IsExpr (SymExpr sym) =>
MemoryOp sym w -> Doc ann
ppMemoryOp MemoryOp sym w
mop]

ppMemoryErrorReason :: MemoryErrorReason -> Doc ann
ppMemoryErrorReason :: forall ann. MemoryErrorReason -> Doc ann
ppMemoryErrorReason =
  \case
    TypeMismatch StorageType
ty1 StorageType
ty2 ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
      [ Doc ann
"Type mismatch: "
      , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ StorageType -> Doc ann
forall ann. StorageType -> Doc ann
ppType StorageType
ty1
                       , StorageType -> Doc ann
forall ann. StorageType -> Doc ann
ppType StorageType
ty2
                       ])
      ]
    UnexpectedArgumentType Text
txt [StorageType]
vals ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
      [ Doc ann
"Unexpected argument type:"
      , Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
txt
      , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ((StorageType -> Doc ann) -> [StorageType] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map StorageType -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow [StorageType]
vals))
      ]
    ApplyViewFail ValueView
vw ->
      Doc ann
"Failure when applying value view" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ValueView -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow ValueView
vw
    Invalid StorageType
ty ->
      Doc ann
"Load from invalid memory at type" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> StorageType -> Doc ann
forall ann. StorageType -> Doc ann
ppType StorageType
ty
    Invalidated Text
msg ->
      Doc ann
"Load from explicitly invalidated memory:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
msg
    NoSatisfyingWrite StorageType
tp ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
       [ Doc ann
"No previous write to this location was found"
       , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann
"Attempting load at type:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> StorageType -> Doc ann
forall ann. StorageType -> Doc ann
ppType StorageType
tp)
       ]
    MemoryErrorReason
UnwritableRegion ->
      Doc ann
"The region wasn't allocated, wasn't large enough, or was marked as readonly"
    MemoryErrorReason
UnreadableRegion ->
      Doc ann
"The region wasn't allocated or wasn't large enough"
    BadFunctionPointer FuncLookupError
err ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
       [ Doc ann
"The given pointer could not be resolved to a callable function"
       , FuncLookupError -> Doc ann
forall ann. FuncLookupError -> Doc ann
ppFuncLookupError FuncLookupError
err
       ]
    MemoryErrorReason
OverlappingRegions ->
      Doc ann
"Memory regions required to be disjoint"

concMemoryError ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  MemoryError sym -> IO (MemoryError sym)
concMemoryError :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemoryError sym
-> IO (MemoryError sym)
concMemoryError sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemoryError MemoryOp sym w
mop MemoryErrorReason
rsn) =
  MemoryOp sym w -> MemoryErrorReason -> MemoryError sym
forall (w :: Nat) sym.
(1 <= w) =>
MemoryOp sym w -> MemoryErrorReason -> MemoryError sym
MemoryError (MemoryOp sym w -> MemoryErrorReason -> MemoryError sym)
-> IO (MemoryOp sym w) -> IO (MemoryErrorReason -> MemoryError sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemoryOp sym w
-> IO (MemoryOp sym w)
forall (w :: Nat) sym.
(1 <= w, IsExprBuilder sym) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemoryOp sym w
-> IO (MemoryOp sym w)
concMemoryOp sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemoryOp sym w
mop IO (MemoryErrorReason -> MemoryError sym)
-> IO MemoryErrorReason -> IO (MemoryError 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
<*> MemoryErrorReason -> IO MemoryErrorReason
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure MemoryErrorReason
rsn

concMemoryOp ::
  (1 <= w, IsExprBuilder sym) =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  MemoryOp sym w -> IO (MemoryOp sym w)
concMemoryOp :: forall (w :: Nat) sym.
(1 <= w, IsExprBuilder sym) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemoryOp sym w
-> IO (MemoryOp sym w)
concMemoryOp sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemLoadOp StorageType
tp Maybe String
gsym LLVMPtr sym w
ptr Mem sym
mem) =
  StorageType
-> Maybe String -> LLVMPtr sym w -> Mem sym -> MemoryOp sym w
forall sym (w :: Nat).
StorageType
-> Maybe String -> LLVMPtr sym w -> Mem sym -> MemoryOp sym w
MemLoadOp StorageType
tp Maybe String
gsym (LLVMPointer sym w -> Mem sym -> MemoryOp sym w)
-> IO (LLVMPointer sym w) -> IO (Mem sym -> MemoryOp sym w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMPtr sym w
-> IO (LLVMPtr sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w)
-> IO (RegValue sym (LLVMPointerType w))
concPtr sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc LLVMPtr sym w
ptr IO (Mem sym -> MemoryOp sym w)
-> IO (Mem sym) -> IO (MemoryOp sym w)
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
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
concMem sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Mem sym
mem
concMemoryOp sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemStoreOp StorageType
tp Maybe String
gsym LLVMPtr sym w
ptr Mem sym
mem) =
  StorageType
-> Maybe String -> LLVMPtr sym w -> Mem sym -> MemoryOp sym w
forall sym (w :: Nat).
StorageType
-> Maybe String -> LLVMPtr sym w -> Mem sym -> MemoryOp sym w
MemStoreOp StorageType
tp Maybe String
gsym (LLVMPointer sym w -> Mem sym -> MemoryOp sym w)
-> IO (LLVMPointer sym w) -> IO (Mem sym -> MemoryOp sym w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMPtr sym w
-> IO (LLVMPtr sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w)
-> IO (RegValue sym (LLVMPointerType w))
concPtr sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc LLVMPtr sym w
ptr IO (Mem sym -> MemoryOp sym w)
-> IO (Mem sym) -> IO (MemoryOp sym w)
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
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
concMem sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Mem sym
mem
concMemoryOp sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemStoreBytesOp Maybe String
gsym LLVMPtr sym w
ptr Maybe (SymBV sym w)
len Mem sym
mem) =
  Maybe String
-> LLVMPtr sym w
-> Maybe (SymBV sym w)
-> Mem sym
-> MemoryOp sym w
forall sym (w :: Nat).
Maybe String
-> LLVMPtr sym w
-> Maybe (SymBV sym w)
-> Mem sym
-> MemoryOp sym w
MemStoreBytesOp Maybe String
gsym (LLVMPointer sym w
 -> Maybe (SymBV sym w) -> Mem sym -> MemoryOp sym w)
-> IO (LLVMPointer sym w)
-> IO (Maybe (SymBV sym w) -> Mem sym -> MemoryOp sym w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
    sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMPtr sym w
-> IO (LLVMPtr sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w)
-> IO (RegValue sym (LLVMPointerType w))
concPtr sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc LLVMPtr sym w
ptr IO (Maybe (SymBV sym w) -> Mem sym -> MemoryOp sym w)
-> IO (Maybe (SymBV sym w)) -> IO (Mem sym -> MemoryOp sym w)
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
<*>
    (SymBV sym w -> IO (SymBV sym w))
-> Maybe (SymBV sym w) -> IO (Maybe (SymBV sym w))
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) -> Maybe a -> f (Maybe b)
traverse (sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym w
-> IO (SymBV sym w)
concBV sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc) Maybe (SymBV sym w)
len IO (Mem sym -> MemoryOp sym w)
-> IO (Mem sym) -> IO (MemoryOp sym w)
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
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
concMem sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Mem sym
mem
concMemoryOp sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemLoadHandleOp Maybe Type
tp Maybe String
gsym LLVMPtr sym w
ptr Mem sym
mem) =
  Maybe Type
-> Maybe String -> LLVMPtr sym w -> Mem sym -> MemoryOp sym w
forall sym (w :: Nat).
Maybe Type
-> Maybe String -> LLVMPtr sym w -> Mem sym -> MemoryOp sym w
MemLoadHandleOp Maybe Type
tp Maybe String
gsym (LLVMPointer sym w -> Mem sym -> MemoryOp sym w)
-> IO (LLVMPointer sym w) -> IO (Mem sym -> MemoryOp sym w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMPtr sym w
-> IO (LLVMPtr sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w)
-> IO (RegValue sym (LLVMPointerType w))
concPtr sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc LLVMPtr sym w
ptr IO (Mem sym -> MemoryOp sym w)
-> IO (Mem sym) -> IO (MemoryOp sym w)
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
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
concMem sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Mem sym
mem
concMemoryOp sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemCopyOp (Maybe String
gsym_dest, LLVMPtr sym w
dest) (Maybe String
gsym_src, LLVMPtr sym w
src) SymBV sym wlen
len Mem sym
mem) =
  do LLVMPointer sym w
dest' <- sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMPtr sym w
-> IO (LLVMPtr sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w)
-> IO (RegValue sym (LLVMPointerType w))
concPtr sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc LLVMPtr sym w
dest
     LLVMPointer sym w
src'  <- sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMPtr sym w
-> IO (LLVMPtr sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w)
-> IO (RegValue sym (LLVMPointerType w))
concPtr sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc LLVMPtr sym w
src
     SymBV sym wlen
len'  <- sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym wlen
-> IO (SymBV sym wlen)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym w
-> IO (SymBV sym w)
concBV sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc SymBV sym wlen
len
     Mem sym
mem'  <- sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
concMem sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Mem sym
mem
     MemoryOp sym w -> IO (MemoryOp sym w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((Maybe String, LLVMPtr sym w)
-> (Maybe String, LLVMPtr sym w)
-> SymBV sym wlen
-> Mem sym
-> MemoryOp sym w
forall sym (w :: Nat) (wlen :: Nat).
(1 <= wlen) =>
(Maybe String, LLVMPtr sym w)
-> (Maybe String, LLVMPtr sym w)
-> SymBV sym wlen
-> Mem sym
-> MemoryOp sym w
MemCopyOp (Maybe String
gsym_dest, LLVMPtr sym w
LLVMPointer sym w
dest') (Maybe String
gsym_src, LLVMPtr sym w
LLVMPointer sym w
src') SymBV sym wlen
len' Mem sym
mem')
concMemoryOp sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemInvalidateOp Text
msg Maybe String
gsym LLVMPtr sym w
ptr SymBV sym wlen
len Mem sym
mem) =
  Text
-> Maybe String
-> LLVMPtr sym w
-> SymBV sym wlen
-> Mem sym
-> MemoryOp sym w
forall sym (w :: Nat) (wlen :: Nat).
(1 <= wlen) =>
Text
-> Maybe String
-> LLVMPtr sym w
-> SymBV sym wlen
-> Mem sym
-> MemoryOp sym w
MemInvalidateOp Text
msg Maybe String
gsym (LLVMPointer sym w -> SymBV sym wlen -> Mem sym -> MemoryOp sym w)
-> IO (LLVMPointer sym w)
-> IO (SymBV sym wlen -> Mem sym -> MemoryOp sym w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
    sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMPtr sym w
-> IO (LLVMPtr sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w)
-> IO (RegValue sym (LLVMPointerType w))
concPtr sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc LLVMPtr sym w
ptr IO (SymBV sym wlen -> Mem sym -> MemoryOp sym w)
-> IO (SymBV sym wlen) -> IO (Mem sym -> MemoryOp sym w)
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
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym wlen
-> IO (SymBV sym wlen)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym w
-> IO (SymBV sym w)
concBV sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc SymBV sym wlen
len IO (Mem sym -> MemoryOp sym w)
-> IO (Mem sym) -> IO (MemoryOp sym w)
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
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
concMem sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Mem sym
mem