------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.MemModel.MemLog
-- Description      : Data types supporting the LLVM memory model
-- Copyright        : (c) Galois, Inc 2011-2020
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# Language ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UndecidableInstances #-}

module Lang.Crucible.LLVM.MemModel.MemLog
  (
    -- * Allocation logs
    AllocType(..)
  , Mutability(..)
  , AllocInfo(..)
  , MemAllocs(..)
  , MemAlloc(..)
  , sizeMemAllocs
  , allocMemAllocs
  , freeMemAllocs
  , muxMemAllocs
  , popMemAllocs
  , possibleAllocInfo
  , isAllocatedGeneric
    -- * Write logs
  , WriteSource(..)
  , MemWrite(..)
  , MemWrites(..)
  , MemWritesChunk(..)
  , memWritesSingleton
    -- * Memory logs
  , MemState(..)
  , MemChanges
  , memState
  , Mem(..)
  , emptyChanges
  , emptyMem
  , memEndian
  , memInsertArrayBlock
  , memMemberArrayBlock

    -- * Pretty printing
  , ppType
  , ppPtr
  , ppAllocInfo
  , ppAllocs
  , ppMem
  , ppMemWrites
  , ppWrite

    -- * Write ranges
  , writeRangesMem
  , writeSourceSize

    -- * Concretization
  , concPtr
  , concLLVMVal
  , concMem
  ) where

import           Control.Applicative ((<|>))
import           Control.Lens
import           Control.Monad.State
import           Control.Monad.Trans.Maybe
import           Data.Foldable
import           Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List.Extra as List
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.Maybe (mapMaybe)
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Text (Text)
import           Numeric.Natural
import           Prettyprinter

import qualified Data.BitVector.Sized as BV
import           Data.Parameterized.Ctx (SingleCtx)

import           What4.Interface
import           What4.Expr (GroundValue)

import           Lang.Crucible.LLVM.DataLayout (Alignment, fromAlignment, EndianForm(..))
import           Lang.Crucible.LLVM.MemModel.Pointer
import           Lang.Crucible.LLVM.MemModel.Type
import           Lang.Crucible.LLVM.MemModel.Value

--------------------------------------------------------------------------------
-- Allocations

data AllocType = StackAlloc | HeapAlloc | GlobalAlloc
  deriving (AllocType -> AllocType -> Bool
(AllocType -> AllocType -> Bool)
-> (AllocType -> AllocType -> Bool) -> Eq AllocType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AllocType -> AllocType -> Bool
== :: AllocType -> AllocType -> Bool
$c/= :: AllocType -> AllocType -> Bool
/= :: AllocType -> AllocType -> Bool
Eq, Eq AllocType
Eq AllocType =>
(AllocType -> AllocType -> Ordering)
-> (AllocType -> AllocType -> Bool)
-> (AllocType -> AllocType -> Bool)
-> (AllocType -> AllocType -> Bool)
-> (AllocType -> AllocType -> Bool)
-> (AllocType -> AllocType -> AllocType)
-> (AllocType -> AllocType -> AllocType)
-> Ord AllocType
AllocType -> AllocType -> Bool
AllocType -> AllocType -> Ordering
AllocType -> AllocType -> AllocType
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 :: AllocType -> AllocType -> Ordering
compare :: AllocType -> AllocType -> Ordering
$c< :: AllocType -> AllocType -> Bool
< :: AllocType -> AllocType -> Bool
$c<= :: AllocType -> AllocType -> Bool
<= :: AllocType -> AllocType -> Bool
$c> :: AllocType -> AllocType -> Bool
> :: AllocType -> AllocType -> Bool
$c>= :: AllocType -> AllocType -> Bool
>= :: AllocType -> AllocType -> Bool
$cmax :: AllocType -> AllocType -> AllocType
max :: AllocType -> AllocType -> AllocType
$cmin :: AllocType -> AllocType -> AllocType
min :: AllocType -> AllocType -> AllocType
Ord, Int -> AllocType -> ShowS
[AllocType] -> ShowS
AllocType -> String
(Int -> AllocType -> ShowS)
-> (AllocType -> String)
-> ([AllocType] -> ShowS)
-> Show AllocType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AllocType -> ShowS
showsPrec :: Int -> AllocType -> ShowS
$cshow :: AllocType -> String
show :: AllocType -> String
$cshowList :: [AllocType] -> ShowS
showList :: [AllocType] -> ShowS
Show)

data Mutability = Mutable | Immutable
  deriving (Mutability -> Mutability -> Bool
(Mutability -> Mutability -> Bool)
-> (Mutability -> Mutability -> Bool) -> Eq Mutability
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Mutability -> Mutability -> Bool
== :: Mutability -> Mutability -> Bool
$c/= :: Mutability -> Mutability -> Bool
/= :: Mutability -> Mutability -> Bool
Eq, Eq Mutability
Eq Mutability =>
(Mutability -> Mutability -> Ordering)
-> (Mutability -> Mutability -> Bool)
-> (Mutability -> Mutability -> Bool)
-> (Mutability -> Mutability -> Bool)
-> (Mutability -> Mutability -> Bool)
-> (Mutability -> Mutability -> Mutability)
-> (Mutability -> Mutability -> Mutability)
-> Ord Mutability
Mutability -> Mutability -> Bool
Mutability -> Mutability -> Ordering
Mutability -> Mutability -> Mutability
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 :: Mutability -> Mutability -> Ordering
compare :: Mutability -> Mutability -> Ordering
$c< :: Mutability -> Mutability -> Bool
< :: Mutability -> Mutability -> Bool
$c<= :: Mutability -> Mutability -> Bool
<= :: Mutability -> Mutability -> Bool
$c> :: Mutability -> Mutability -> Bool
> :: Mutability -> Mutability -> Bool
$c>= :: Mutability -> Mutability -> Bool
>= :: Mutability -> Mutability -> Bool
$cmax :: Mutability -> Mutability -> Mutability
max :: Mutability -> Mutability -> Mutability
$cmin :: Mutability -> Mutability -> Mutability
min :: Mutability -> Mutability -> Mutability
Ord, Int -> Mutability -> ShowS
[Mutability] -> ShowS
Mutability -> String
(Int -> Mutability -> ShowS)
-> (Mutability -> String)
-> ([Mutability] -> ShowS)
-> Show Mutability
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Mutability -> ShowS
showsPrec :: Int -> Mutability -> ShowS
$cshow :: Mutability -> String
show :: Mutability -> String
$cshowList :: [Mutability] -> ShowS
showList :: [Mutability] -> ShowS
Show)

-- | Details of a single allocation. The @Maybe SymBV@ argument is either a
-- size or @Nothing@ representing an unbounded allocation. The 'Mutability'
-- indicates whether the region is read-only. The 'String' contains source
-- location information for use in error messages.
data AllocInfo sym =
  forall w. (1 <= w) => AllocInfo AllocType (Maybe (SymBV sym w)) Mutability Alignment String

-- | Stores writeable memory allocations.
data MemAlloc sym
    -- | A collection of consecutive basic allocations.
  = Allocations (Map Natural (AllocInfo sym))
    -- | Freeing of the given block ID.
  | MemFree (SymNat sym) String
    -- | The merger of two allocations.
  | AllocMerge (Pred sym) (MemAllocs sym) (MemAllocs sym)

-- | A record of which memory regions have been allocated or freed.

-- Memory allocations are represented as a list with the invariant
-- that any two adjacent 'Allocations' constructors must be merged
-- together, and that no 'Allocations' constructor has an empty map.
newtype MemAllocs sym = MemAllocs [MemAlloc sym]

instance Semigroup (MemAllocs sym) where
  (MemAllocs [MemAlloc sym]
lhs_allocs) <> :: MemAllocs sym -> MemAllocs sym -> MemAllocs sym
<> (MemAllocs [MemAlloc sym]
rhs_allocs)
    | Just ([MemAlloc sym]
lhs_head_allocs, Allocations Map Natural (AllocInfo sym)
lhs_m) <- [MemAlloc sym] -> Maybe ([MemAlloc sym], MemAlloc sym)
forall a. [a] -> Maybe ([a], a)
List.unsnoc [MemAlloc sym]
lhs_allocs
    , Allocations Map Natural (AllocInfo sym)
rhs_m : [MemAlloc sym]
rhs_tail_allocs <- [MemAlloc sym]
rhs_allocs
    = [MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs ([MemAlloc sym]
lhs_head_allocs [MemAlloc sym] -> [MemAlloc sym] -> [MemAlloc sym]
forall a. [a] -> [a] -> [a]
++ [Map Natural (AllocInfo sym) -> MemAlloc sym
forall sym. Map Natural (AllocInfo sym) -> MemAlloc sym
Allocations (Map Natural (AllocInfo sym)
-> Map Natural (AllocInfo sym) -> Map Natural (AllocInfo sym)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Natural (AllocInfo sym)
lhs_m Map Natural (AllocInfo sym)
rhs_m)] [MemAlloc sym] -> [MemAlloc sym] -> [MemAlloc sym]
forall a. [a] -> [a] -> [a]
++ [MemAlloc sym]
rhs_tail_allocs)
    | Bool
otherwise = [MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs ([MemAlloc sym]
lhs_allocs [MemAlloc sym] -> [MemAlloc sym] -> [MemAlloc sym]
forall a. [a] -> [a] -> [a]
++ [MemAlloc sym]
rhs_allocs)

instance Monoid (MemAllocs sym) where
  mempty :: MemAllocs sym
mempty = [MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs []


sizeMemAlloc :: MemAlloc sym -> Int
sizeMemAlloc :: forall sym. MemAlloc sym -> Int
sizeMemAlloc =
  \case
    Allocations Map Natural (AllocInfo sym)
m -> Map Natural (AllocInfo sym) -> Int
forall k a. Map k a -> Int
Map.size Map Natural (AllocInfo sym)
m
    MemFree{} -> Int
1
    AllocMerge{} -> Int
1

-- | Compute the size of a 'MemAllocs' log.
sizeMemAllocs :: MemAllocs sym -> Int
sizeMemAllocs :: forall sym. MemAllocs sym -> Int
sizeMemAllocs (MemAllocs [MemAlloc sym]
allocs) = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: Type -> Type) a. (Foldable t, Num a) => t a -> a
sum ((MemAlloc sym -> Int) -> [MemAlloc sym] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map MemAlloc sym -> Int
forall sym. MemAlloc sym -> Int
sizeMemAlloc [MemAlloc sym]
allocs)

-- | Returns true if this consists of a empty collection of memory allocs.
nullMemAllocs :: MemAllocs sym -> Bool
nullMemAllocs :: forall sym. MemAllocs sym -> Bool
nullMemAllocs (MemAllocs [MemAlloc sym]
xs) = [MemAlloc sym] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [MemAlloc sym]
xs

-- | Allocate a new block with the given allocation ID.
allocMemAllocs :: Natural -> AllocInfo sym -> MemAllocs sym -> MemAllocs sym
allocMemAllocs :: forall sym.
Natural -> AllocInfo sym -> MemAllocs sym -> MemAllocs sym
allocMemAllocs Natural
blk AllocInfo sym
info MemAllocs sym
ma = [MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs [Map Natural (AllocInfo sym) -> MemAlloc sym
forall sym. Map Natural (AllocInfo sym) -> MemAlloc sym
Allocations (Natural -> AllocInfo sym -> Map Natural (AllocInfo sym)
forall k a. k -> a -> Map k a
Map.singleton Natural
blk AllocInfo sym
info)] MemAllocs sym -> MemAllocs sym -> MemAllocs sym
forall a. Semigroup a => a -> a -> a
<> MemAllocs sym
ma

-- | Free the block with the given allocation ID.
freeMemAllocs :: SymNat sym -> String {- ^ Location info for debugging -} -> MemAllocs sym -> MemAllocs sym
freeMemAllocs :: forall sym. SymNat sym -> String -> MemAllocs sym -> MemAllocs sym
freeMemAllocs SymNat sym
blk String
loc (MemAllocs [MemAlloc sym]
xs) = [MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs (SymNat sym -> String -> MemAlloc sym
forall sym. SymNat sym -> String -> MemAlloc sym
MemFree SymNat sym
blk String
loc MemAlloc sym -> [MemAlloc sym] -> [MemAlloc sym]
forall a. a -> [a] -> [a]
: [MemAlloc sym]
xs)

muxMemAllocs :: IsExpr (SymExpr sym) => Pred sym -> MemAllocs sym -> MemAllocs sym -> MemAllocs sym
muxMemAllocs :: forall sym.
IsExpr (SymExpr sym) =>
Pred sym -> MemAllocs sym -> MemAllocs sym -> MemAllocs sym
muxMemAllocs Pred sym
_ (MemAllocs []) (MemAllocs []) = [MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs []
muxMemAllocs Pred sym
c MemAllocs sym
xs MemAllocs sym
ys =
  case Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
c of
    Just Bool
True -> MemAllocs sym
xs
    Just Bool
False -> MemAllocs sym
ys
    Maybe Bool
Nothing -> [MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs [Pred sym -> MemAllocs sym -> MemAllocs sym -> MemAlloc sym
forall sym.
Pred sym -> MemAllocs sym -> MemAllocs sym -> MemAlloc sym
AllocMerge Pred sym
c MemAllocs sym
xs MemAllocs sym
ys]

-- | Purge all stack allocations from the allocation log.
popMemAllocs :: forall sym. MemAllocs sym -> MemAllocs sym
popMemAllocs :: forall sym. MemAllocs sym -> MemAllocs sym
popMemAllocs (MemAllocs [MemAlloc sym]
xs) = [MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs ((MemAlloc sym -> Maybe (MemAlloc sym))
-> [MemAlloc sym] -> [MemAlloc sym]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe MemAlloc sym -> Maybe (MemAlloc sym)
popMemAlloc [MemAlloc sym]
xs)
  where
    popMemAlloc :: MemAlloc sym -> Maybe (MemAlloc sym)
    popMemAlloc :: MemAlloc sym -> Maybe (MemAlloc sym)
popMemAlloc (Allocations Map Natural (AllocInfo sym)
am) =
      if Map Natural (AllocInfo sym) -> Bool
forall k a. Map k a -> Bool
Map.null Map Natural (AllocInfo sym)
am' then Maybe (MemAlloc sym)
forall a. Maybe a
Nothing else MemAlloc sym -> Maybe (MemAlloc sym)
forall a. a -> Maybe a
Just (Map Natural (AllocInfo sym) -> MemAlloc sym
forall sym. Map Natural (AllocInfo sym) -> MemAlloc sym
Allocations Map Natural (AllocInfo sym)
am')
      where am' :: Map Natural (AllocInfo sym)
am' = (AllocInfo sym -> Bool)
-> Map Natural (AllocInfo sym) -> Map Natural (AllocInfo sym)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter AllocInfo sym -> Bool
notStackAlloc Map Natural (AllocInfo sym)
am
    popMemAlloc a :: MemAlloc sym
a@(MemFree SymNat sym
_ String
_) = MemAlloc sym -> Maybe (MemAlloc sym)
forall a. a -> Maybe a
Just MemAlloc sym
a
    popMemAlloc (AllocMerge Pred sym
c MemAllocs sym
x MemAllocs sym
y) = MemAlloc sym -> Maybe (MemAlloc sym)
forall a. a -> Maybe a
Just (Pred sym -> MemAllocs sym -> MemAllocs sym -> MemAlloc sym
forall sym.
Pred sym -> MemAllocs sym -> MemAllocs sym -> MemAlloc sym
AllocMerge Pred sym
c (MemAllocs sym -> MemAllocs sym
forall sym. MemAllocs sym -> MemAllocs sym
popMemAllocs MemAllocs sym
x) (MemAllocs sym -> MemAllocs sym
forall sym. MemAllocs sym -> MemAllocs sym
popMemAllocs MemAllocs sym
y))

    notStackAlloc :: AllocInfo sym -> Bool
    notStackAlloc :: AllocInfo sym -> Bool
notStackAlloc (AllocInfo AllocType
x Maybe (SymBV sym w)
_ Mutability
_ Alignment
_ String
_) = AllocType
x AllocType -> AllocType -> Bool
forall a. Eq a => a -> a -> Bool
/= AllocType
StackAlloc

-- | Look up the 'AllocInfo' for the given allocation number. A 'Just'
-- result indicates that the specified memory region may or may not
-- still be allocated; 'Nothing' indicates that the memory region is
-- definitely not allocated.
possibleAllocInfo ::
  forall sym.
  IsExpr (SymExpr sym) =>
  Natural ->
  MemAllocs sym ->
  Maybe (AllocInfo sym)
possibleAllocInfo :: forall sym.
IsExpr (SymExpr sym) =>
Natural -> MemAllocs sym -> Maybe (AllocInfo sym)
possibleAllocInfo Natural
n (MemAllocs [MemAlloc sym]
xs) = [Maybe (AllocInfo sym)] -> Maybe (AllocInfo sym)
forall (t :: Type -> Type) (f :: Type -> Type) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ((MemAlloc sym -> Maybe (AllocInfo sym))
-> [MemAlloc sym] -> [Maybe (AllocInfo sym)]
forall a b. (a -> b) -> [a] -> [b]
map MemAlloc sym -> Maybe (AllocInfo sym)
helper [MemAlloc sym]
xs)
  where
    helper :: MemAlloc sym -> Maybe (AllocInfo sym)
    helper :: MemAlloc sym -> Maybe (AllocInfo sym)
helper =
      \case
        MemFree SymNat sym
_ String
_ -> Maybe (AllocInfo sym)
forall a. Maybe a
Nothing
        Allocations Map Natural (AllocInfo sym)
m -> Natural -> Map Natural (AllocInfo sym) -> Maybe (AllocInfo sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Natural
n Map Natural (AllocInfo sym)
m
        AllocMerge Pred sym
cond MemAllocs sym
ma1 MemAllocs sym
ma2 ->
          case Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
cond of
            Just Bool
True -> Natural -> MemAllocs sym -> Maybe (AllocInfo sym)
forall sym.
IsExpr (SymExpr sym) =>
Natural -> MemAllocs sym -> Maybe (AllocInfo sym)
possibleAllocInfo Natural
n MemAllocs sym
ma1
            Just Bool
False -> Natural -> MemAllocs sym -> Maybe (AllocInfo sym)
forall sym.
IsExpr (SymExpr sym) =>
Natural -> MemAllocs sym -> Maybe (AllocInfo sym)
possibleAllocInfo Natural
n MemAllocs sym
ma2
            Maybe Bool
Nothing -> Natural -> MemAllocs sym -> Maybe (AllocInfo sym)
forall sym.
IsExpr (SymExpr sym) =>
Natural -> MemAllocs sym -> Maybe (AllocInfo sym)
possibleAllocInfo Natural
n MemAllocs sym
ma1 Maybe (AllocInfo sym)
-> Maybe (AllocInfo sym) -> Maybe (AllocInfo sym)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> Natural -> MemAllocs sym -> Maybe (AllocInfo sym)
forall sym.
IsExpr (SymExpr sym) =>
Natural -> MemAllocs sym -> Maybe (AllocInfo sym)
possibleAllocInfo Natural
n MemAllocs sym
ma2


-- | Generalized function for checking whether a memory region ID is allocated.
--
-- The first predicate indicates whether the region was allocated, the second
-- indicates whether it has *not* been freed.
isAllocatedGeneric ::
  forall sym.
  (IsExpr (SymExpr sym), IsExprBuilder sym) =>
  sym ->
  (AllocInfo sym -> IO (Pred sym)) ->
  SymNat sym ->
  MemAllocs sym ->
  IO (Pred sym, Pred sym)
isAllocatedGeneric :: forall sym.
(IsExpr (SymExpr sym), IsExprBuilder sym) =>
sym
-> (AllocInfo sym -> IO (Pred sym))
-> SymNat sym
-> MemAllocs sym
-> IO (Pred sym, Pred sym)
isAllocatedGeneric sym
sym AllocInfo sym -> IO (Pred sym)
inAlloc SymNat sym
blk = IO (Pred sym)
-> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
go (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)) (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
truePred sym
sym))
  where
    go :: IO (Pred sym) -> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
    go :: IO (Pred sym)
-> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
go IO (Pred sym)
fallback IO (Pred sym)
fallbackFreed (MemAllocs []) = (,) (Pred sym -> Pred sym -> (Pred sym, Pred sym))
-> IO (Pred sym) -> IO (Pred sym -> (Pred sym, Pred sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (Pred sym)
fallback IO (Pred sym -> (Pred sym, Pred sym))
-> IO (Pred sym) -> IO (Pred sym, Pred 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
<*> IO (Pred sym)
fallbackFreed
    go IO (Pred sym)
fallback IO (Pred sym)
fallbackFreed (MemAllocs (MemAlloc sym
alloc : [MemAlloc sym]
r)) =
      case MemAlloc sym
alloc of
        Allocations Map Natural (AllocInfo sym)
am ->
          case SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat SymNat sym
blk of
            Just Natural
b -> -- concrete block number, look up entry
              case Natural -> Map Natural (AllocInfo sym) -> Maybe (AllocInfo sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Natural
b Map Natural (AllocInfo sym)
am of
                Maybe (AllocInfo sym)
Nothing -> IO (Pred sym)
-> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
go IO (Pred sym)
fallback IO (Pred sym)
fallbackFreed ([MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs [MemAlloc sym]
r)
                Just AllocInfo sym
ba -> (,) (Pred sym -> Pred sym -> (Pred sym, Pred sym))
-> IO (Pred sym) -> IO (Pred sym -> (Pred sym, Pred sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AllocInfo sym -> IO (Pred sym)
inAlloc AllocInfo sym
ba IO (Pred sym -> (Pred sym, Pred sym))
-> IO (Pred sym) -> IO (Pred sym, Pred 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
<*> IO (Pred sym)
fallbackFreed
            Maybe Natural
Nothing -> -- symbolic block number, need to check all entries
              (Natural
 -> AllocInfo sym
 -> IO (Pred sym, Pred sym)
 -> IO (Pred sym, Pred sym))
-> IO (Pred sym, Pred sym)
-> Map Natural (AllocInfo sym)
-> IO (Pred sym, Pred sym)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Natural
-> AllocInfo sym
-> IO (Pred sym, Pred sym)
-> IO (Pred sym, Pred sym)
checkEntry (IO (Pred sym)
-> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
go IO (Pred sym)
fallback IO (Pred sym)
fallbackFreed ([MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs [MemAlloc sym]
r)) Map Natural (AllocInfo sym)
am
              where
                checkEntry :: Natural
-> AllocInfo sym
-> IO (Pred sym, Pred sym)
-> IO (Pred sym, Pred sym)
checkEntry Natural
a AllocInfo sym
ba IO (Pred sym, Pred sym)
k =
                  do
                     Pred sym
sameBlock <- 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
blk (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
a
                     case Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
sameBlock of
                       Just Bool
True ->
                         -- This is where where this block was allocated, and it
                         -- couldn't have been freed before it was allocated.
                         (, sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) (Pred sym -> (Pred sym, Pred sym))
-> IO (Pred sym) -> IO (Pred sym, Pred sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AllocInfo sym -> IO (Pred sym)
inAlloc AllocInfo sym
ba
                       Just Bool
False -> IO (Pred sym, Pred sym)
k
                       Maybe Bool
Nothing ->
                         do (Pred sym
fallback', Pred sym
fallbackFreed') <- IO (Pred sym, Pred sym)
k
                            Pred sym
here <- sym -> Pred sym -> IO (Pred sym) -> IO (Pred sym) -> IO (Pred sym)
forall sym (m :: Type -> Type).
(IsExpr (SymExpr sym), IsExprBuilder sym, MonadIO m) =>
sym -> Pred sym -> m (Pred sym) -> m (Pred sym) -> m (Pred sym)
itePredM sym
sym Pred sym
sameBlock (AllocInfo sym -> IO (Pred sym)
inAlloc AllocInfo sym
ba) (Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Pred sym
fallback')
                            (Pred sym, Pred sym) -> IO (Pred sym, Pred sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym
here, Pred sym
fallbackFreed')
        MemFree SymNat sym
a String
_ ->
          do Pred sym
sameBlock <- 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
blk SymNat sym
a
             case Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
sameBlock of
               Just Bool
True  ->
                 -- If it was freed, it also must have been allocated beforehand.
                 (Pred sym, Pred sym) -> IO (Pred sym, Pred sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym, sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)
               Just Bool
False -> IO (Pred sym)
-> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
go IO (Pred sym)
fallback IO (Pred sym)
fallbackFreed ([MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs [MemAlloc sym]
r)
               Maybe Bool
Nothing    ->
                 do (Pred sym
inRest, Pred sym
notFreedInRest) <-
                      IO (Pred sym)
-> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
go IO (Pred sym)
fallback IO (Pred sym)
fallbackFreed ([MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs [MemAlloc sym]
r)
                    Pred sym
notSameBlock <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
sameBlock
                    (Pred sym
inRest,) (Pred sym -> (Pred sym, Pred sym))
-> IO (Pred sym) -> IO (Pred sym, 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
notSameBlock Pred sym
notFreedInRest
        AllocMerge Pred sym
_ (MemAllocs []) (MemAllocs []) ->
          IO (Pred sym)
-> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
go IO (Pred sym)
fallback IO (Pred sym)
fallbackFreed ([MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs [MemAlloc sym]
r)
        AllocMerge Pred sym
c MemAllocs sym
xr MemAllocs sym
yr ->
          do (Pred sym
inRest, Pred sym
notFreedInRest) <- IO (Pred sym)
-> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
go IO (Pred sym)
fallback IO (Pred sym)
fallbackFreed ([MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs [MemAlloc sym]
r) -- TODO: wrap this in a delay
             (Pred sym
inTrue, Pred sym
notFreedInTrue) <- IO (Pred sym)
-> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
go (Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Pred sym
inRest) (Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Pred sym
notFreedInRest) MemAllocs sym
xr
             (Pred sym
inFalse, Pred sym
notFreedInFalse) <- IO (Pred sym)
-> IO (Pred sym) -> MemAllocs sym -> IO (Pred sym, Pred sym)
go (Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Pred sym
inRest) (Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Pred sym
notFreedInRest) MemAllocs sym
yr
             (,) (Pred sym -> Pred sym -> (Pred sym, Pred sym))
-> IO (Pred sym) -> IO (Pred sym -> (Pred sym, Pred sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
c Pred sym
inTrue Pred sym
inFalse
                 IO (Pred sym -> (Pred sym, Pred sym))
-> IO (Pred sym) -> IO (Pred sym, Pred 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 -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym Pred sym
c Pred sym
notFreedInTrue Pred sym
notFreedInFalse

--------------------------------------------------------------------------------
-- Writes

data WriteSource sym w
    -- | @MemCopy src len@ copies @len@ bytes from [src..src+len).
  = MemCopy (LLVMPtr sym w) (SymBV sym w)
    -- | @MemSet val len@ fills the destination with @len@ copies of byte @val@.
  | MemSet (SymBV sym 8) (SymBV sym w)
    -- | @MemStore val ty al@ writes value @val@ with type @ty@ at the destination.
    --   with alignment at least @al@.
  | MemStore (LLVMVal sym) StorageType Alignment
    -- | @MemArrayStore block (Just len)@ writes byte-array @block@ of size
    -- @len@ at the destination; @MemArrayStore block Nothing@ writes byte-array
    -- @block@ of unbounded size
  | MemArrayStore (SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)) (Maybe (SymBV sym w))
    -- | @MemInvalidate len@ flags @len@ bytes as uninitialized.
  | MemInvalidate Text (SymBV sym w)

data MemWrite sym
    -- | @MemWrite dst src@ represents a write to @dst@ from the given source.
  = forall w. (1 <= w) => MemWrite (LLVMPtr sym w) (WriteSource sym w)
    -- | The merger of two memories.
  | WriteMerge (Pred sym) (MemWrites sym) (MemWrites sym)


--------------------------------------------------------------------------------
-- Memory

-- | A symbolic representation of the LLVM heap.
--
-- This representation is designed to support a variety of operations
-- including reads and writes of symbolic data to symbolic addresses,
-- symbolic memcpy and memset, and merging two memories in a single
-- memory using an if-then-else operation.
--
-- A common use case is that the symbolic simulator will branch into
-- two execution states based on a symbolic branch, make different
-- memory modifications on each branch, and then need to merge the two
-- memories to resume execution along a single path using the branch
-- condition.  To support this, our memory representation supports
-- "branch frames", at any point one can insert a fresh branch frame
-- (see `branchMem`), and then at some later point merge two memories
-- back into a single memory (see `mergeMem`).  Our `mergeMem`
-- implementation is able to efficiently merge memories, but requires
-- that one only merge memories that were identical prior to the last
-- branch.
data Mem sym = Mem { forall sym. Mem sym -> EndianForm
memEndianForm :: EndianForm, forall sym. Mem sym -> MemState sym
_memState :: MemState sym, forall sym. Mem sym -> Set Natural
memArrayBlocks :: Set Natural }

memState :: Lens' (Mem sym) (MemState sym)
memState :: forall sym (f :: Type -> Type).
Functor f =>
(MemState sym -> f (MemState sym)) -> Mem sym -> f (Mem sym)
memState = (Mem sym -> MemState sym)
-> (Mem sym -> MemState sym -> Mem sym)
-> Lens (Mem sym) (Mem sym) (MemState sym) (MemState sym)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens Mem sym -> MemState sym
forall sym. Mem sym -> MemState sym
_memState (\Mem sym
s MemState sym
v -> Mem sym
s { _memState = v })

-- | A state of memory as of a stack push, branch, or merge.  Counts
-- of the total number of allocations and writes are kept for
-- performance metrics.
data MemState sym =
    -- | Represents initial memory and changes since then.
    -- Changes are stored in order, with more recent changes closer to the head
    -- of the list.
    EmptyMem !Int !Int (MemChanges sym)
    -- | Represents a push of a stack frame, and changes since that stack push.
    -- The text value gives a user-consumable name for the stack frame.
    -- Changes are stored in order, with more recent changes closer to the head
    -- of the list.
  | StackFrame !Int !Int Text (MemChanges sym) (MemState sym)
    -- | Represents a push of a branch frame, and changes since that branch.
    -- Changes are stored in order, with more recent changes closer to the head
    -- of the list.
  | BranchFrame !Int !Int (MemChanges sym) (MemState sym)

type MemChanges sym = (MemAllocs sym, MemWrites sym)

-- | Memory writes are represented as a list of chunks of writes.
--   Chunks alternate between being indexed and being flat.
newtype MemWrites sym = MemWrites [MemWritesChunk sym]

-- | Returns true if this consists of a empty collection of memory writes
nullMemWrites :: MemWrites sym -> Bool
nullMemWrites :: forall sym. MemWrites sym -> Bool
nullMemWrites (MemWrites [MemWritesChunk sym]
ws) = [MemWritesChunk sym] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [MemWritesChunk sym]
ws

-- | A chunk of memory writes is either indexed or flat (unindexed).
--   An indexed chunk consists of writes to addresses with concrete
--   base pointers and is represented as a map. A flat chunk consists of
--   writes to addresses with symbolic base pointers. A merge of two
--   indexed chunks is a indexed chunk, while any other merge is part of
--   a flat chunk.
data MemWritesChunk sym =
    MemWritesChunkFlat [MemWrite sym]
  | MemWritesChunkIndexed (IntMap [MemWrite sym])

instance Semigroup (MemWrites sym) where
  (MemWrites [MemWritesChunk sym]
lhs_writes) <> :: MemWrites sym -> MemWrites sym -> MemWrites sym
<> (MemWrites [MemWritesChunk sym]
rhs_writes)
    | Just ([MemWritesChunk sym]
lhs_head_writes, MemWritesChunk sym
lhs_tail_write) <- [MemWritesChunk sym]
-> Maybe ([MemWritesChunk sym], MemWritesChunk sym)
forall a. [a] -> Maybe ([a], a)
List.unsnoc [MemWritesChunk sym]
lhs_writes
    , MemWritesChunkIndexed IntMap [MemWrite sym]
lhs_tail_indexed_writes <- MemWritesChunk sym
lhs_tail_write
    , MemWritesChunk sym
rhs_head_write : [MemWritesChunk sym]
rhs_tail_writes <- [MemWritesChunk sym]
rhs_writes
    , (MemWritesChunkIndexed IntMap [MemWrite sym]
rhs_head_indexed_writes) <- MemWritesChunk sym
rhs_head_write = do
      let merged_chunk :: MemWritesChunk sym
merged_chunk = IntMap [MemWrite sym] -> MemWritesChunk sym
forall sym. IntMap [MemWrite sym] -> MemWritesChunk sym
MemWritesChunkIndexed (IntMap [MemWrite sym] -> MemWritesChunk sym)
-> IntMap [MemWrite sym] -> MemWritesChunk sym
forall a b. (a -> b) -> a -> b
$ (Int -> [MemWrite sym] -> [MemWrite sym] -> Maybe [MemWrite sym])
-> (IntMap [MemWrite sym] -> IntMap [MemWrite sym])
-> (IntMap [MemWrite sym] -> IntMap [MemWrite sym])
-> IntMap [MemWrite sym]
-> IntMap [MemWrite sym]
-> IntMap [MemWrite sym]
forall a b c.
(Int -> a -> b -> Maybe c)
-> (IntMap a -> IntMap c)
-> (IntMap b -> IntMap c)
-> IntMap a
-> IntMap b
-> IntMap c
IntMap.mergeWithKey
            (\Int
_ [MemWrite sym]
lhs_alloc_writes [MemWrite sym]
rhs_alloc_writes ->
              [MemWrite sym] -> Maybe [MemWrite sym]
forall a. a -> Maybe a
Just ([MemWrite sym] -> Maybe [MemWrite sym])
-> [MemWrite sym] -> Maybe [MemWrite sym]
forall a b. (a -> b) -> a -> b
$ [MemWrite sym]
lhs_alloc_writes [MemWrite sym] -> [MemWrite sym] -> [MemWrite sym]
forall a. [a] -> [a] -> [a]
++ [MemWrite sym]
rhs_alloc_writes)
            IntMap [MemWrite sym] -> IntMap [MemWrite sym]
forall a. a -> a
id
            IntMap [MemWrite sym] -> IntMap [MemWrite sym]
forall a. a -> a
id
            IntMap [MemWrite sym]
lhs_tail_indexed_writes
            IntMap [MemWrite sym]
rhs_head_indexed_writes
      [MemWritesChunk sym] -> MemWrites sym
forall sym. [MemWritesChunk sym] -> MemWrites sym
MemWrites ([MemWritesChunk sym] -> MemWrites sym)
-> [MemWritesChunk sym] -> MemWrites sym
forall a b. (a -> b) -> a -> b
$ [MemWritesChunk sym]
lhs_head_writes [MemWritesChunk sym]
-> [MemWritesChunk sym] -> [MemWritesChunk sym]
forall a. [a] -> [a] -> [a]
++ [MemWritesChunk sym
merged_chunk] [MemWritesChunk sym]
-> [MemWritesChunk sym] -> [MemWritesChunk sym]
forall a. [a] -> [a] -> [a]
++ [MemWritesChunk sym]
rhs_tail_writes
    | Bool
otherwise = [MemWritesChunk sym] -> MemWrites sym
forall sym. [MemWritesChunk sym] -> MemWrites sym
MemWrites ([MemWritesChunk sym] -> MemWrites sym)
-> [MemWritesChunk sym] -> MemWrites sym
forall a b. (a -> b) -> a -> b
$ [MemWritesChunk sym]
lhs_writes [MemWritesChunk sym]
-> [MemWritesChunk sym] -> [MemWritesChunk sym]
forall a. [a] -> [a] -> [a]
++ [MemWritesChunk sym]
rhs_writes

instance Monoid (MemWrites sym) where
  mempty :: MemWrites sym
mempty = [MemWritesChunk sym] -> MemWrites sym
forall sym. [MemWritesChunk sym] -> MemWrites sym
MemWrites []


memWritesSingleton ::
  (IsExprBuilder sym, 1 <= w) =>
  LLVMPtr sym w ->
  WriteSource sym w ->
  MemWrites sym
memWritesSingleton :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
LLVMPtr sym w -> WriteSource sym w -> MemWrites sym
memWritesSingleton LLVMPtr sym w
ptr WriteSource sym w
src
  | Just Natural
blk <- SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat (LLVMPtr sym w -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
llvmPointerBlock LLVMPtr sym w
ptr)
  , WriteSource sym w -> Bool
forall sym (w :: Natural). WriteSource sym w -> Bool
isIndexableSource WriteSource sym w
src =
    [MemWritesChunk sym] -> MemWrites sym
forall sym. [MemWritesChunk sym] -> MemWrites sym
MemWrites
      [ IntMap [MemWrite sym] -> MemWritesChunk sym
forall sym. IntMap [MemWrite sym] -> MemWritesChunk sym
MemWritesChunkIndexed (IntMap [MemWrite sym] -> MemWritesChunk sym)
-> IntMap [MemWrite sym] -> MemWritesChunk sym
forall a b. (a -> b) -> a -> b
$
          Int -> [MemWrite sym] -> IntMap [MemWrite sym]
forall a. Int -> a -> IntMap a
IntMap.singleton (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
blk) [LLVMPtr sym w -> WriteSource sym w -> MemWrite sym
forall sym (w :: Natural).
(1 <= w) =>
LLVMPtr sym w -> WriteSource sym w -> MemWrite sym
MemWrite LLVMPtr sym w
ptr WriteSource sym w
src]
      ]
  | Bool
otherwise = [MemWritesChunk sym] -> MemWrites sym
forall sym. [MemWritesChunk sym] -> MemWrites sym
MemWrites [[MemWrite sym] -> MemWritesChunk sym
forall sym. [MemWrite sym] -> MemWritesChunk sym
MemWritesChunkFlat [LLVMPtr sym w -> WriteSource sym w -> MemWrite sym
forall sym (w :: Natural).
(1 <= w) =>
LLVMPtr sym w -> WriteSource sym w -> MemWrite sym
MemWrite LLVMPtr sym w
ptr WriteSource sym w
src]]
  where
    isIndexableSource ::  WriteSource sym w -> Bool
    isIndexableSource :: forall sym (w :: Natural). WriteSource sym w -> Bool
isIndexableSource = \case
      MemStore{} -> Bool
True
      MemArrayStore{} -> Bool
True
      MemSet{} -> Bool
True
      MemInvalidate{} -> Bool
True
      MemCopy{} -> Bool
False



emptyChanges :: MemChanges sym
emptyChanges :: forall sym. MemChanges sym
emptyChanges = (MemAllocs sym
forall a. Monoid a => a
mempty, MemWrites sym
forall a. Monoid a => a
mempty)

emptyMem :: EndianForm -> Mem sym
emptyMem :: forall sym. EndianForm -> Mem sym
emptyMem EndianForm
e = Mem { memEndianForm :: EndianForm
memEndianForm = EndianForm
e, _memState :: MemState sym
_memState = Int -> Int -> MemChanges sym -> MemState sym
forall sym. Int -> Int -> MemChanges sym -> MemState sym
EmptyMem Int
0 Int
0 MemChanges sym
forall sym. MemChanges sym
emptyChanges, memArrayBlocks :: Set Natural
memArrayBlocks = Set Natural
forall a. Set a
Set.empty }

memEndian :: Mem sym -> EndianForm
memEndian :: forall sym. Mem sym -> EndianForm
memEndian = Mem sym -> EndianForm
forall sym. Mem sym -> EndianForm
memEndianForm

memInsertArrayBlock :: IsExprBuilder sym => SymNat sym -> Mem sym -> Mem sym
memInsertArrayBlock :: forall sym. IsExprBuilder sym => SymNat sym -> Mem sym -> Mem sym
memInsertArrayBlock SymNat sym
blk Mem sym
mem = case SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat SymNat sym
blk of
  Just Natural
blk_no -> Mem sym
mem { memArrayBlocks = Set.insert blk_no (memArrayBlocks mem) }
  Maybe Natural
Nothing -> Mem sym
mem { memArrayBlocks = Set.empty }

memMemberArrayBlock :: IsExprBuilder sym => SymNat sym -> Mem sym -> Bool
memMemberArrayBlock :: forall sym. IsExprBuilder sym => SymNat sym -> Mem sym -> Bool
memMemberArrayBlock SymNat sym
blk Mem sym
mem = case SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat SymNat sym
blk of
  Just Natural
blk_no -> Natural -> Set Natural -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Natural
blk_no (Mem sym -> Set Natural
forall sym. Mem sym -> Set Natural
memArrayBlocks Mem sym
mem)
  Maybe Natural
Nothing -> Bool
False


--------------------------------------------------------------------------------
-- Pretty printing

ppMerge :: IsExpr e
        => (v -> Doc ann)
        -> e tp
        -> [v]
        -> [v]
        -> Doc ann
ppMerge :: forall (e :: BaseType -> Type) v ann (tp :: BaseType).
IsExpr e =>
(v -> Doc ann) -> e tp -> [v] -> [v] -> Doc ann
ppMerge v -> Doc ann
vpp e tp
c [v]
x [v]
y =
  Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
  [ Doc ann
"Condition:"
  , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (e tp -> Doc ann
forall (tp :: BaseType) ann. e tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr e tp
c)
  , [v] -> Doc ann -> Doc ann
ppAllocList [v]
x Doc ann
"True Branch:"
  , [v] -> Doc ann -> Doc ann
ppAllocList [v]
y Doc ann
"False Branch:"
  ]
  where ppAllocList :: [v] -> Doc ann -> Doc ann
ppAllocList [] Doc ann
d = Doc ann
d Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"<none>"
        ppAllocList [v]
xs Doc ann
d = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [Doc ann
d, 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 ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (v -> Doc ann) -> [v] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map v -> Doc ann
vpp [v]
xs)]

ppAlignment :: Alignment -> Doc ann
ppAlignment :: forall ann. Alignment -> Doc ann
ppAlignment Alignment
a =
  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
$ Bytes -> String
forall a. Show a => a -> String
show (Alignment -> Bytes
fromAlignment Alignment
a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-byte-aligned"

ppAllocInfo :: IsExpr (SymExpr sym) => (Natural, AllocInfo sym) -> Doc ann
ppAllocInfo :: forall sym ann.
IsExpr (SymExpr sym) =>
(Natural, AllocInfo sym) -> Doc ann
ppAllocInfo (Natural
base, AllocInfo AllocType
atp Maybe (SymBV sym w)
sz Mutability
mut Alignment
alignment String
loc) =
  AllocType -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow AllocType
atp
  Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Natural -> Doc ann
forall ann. Natural -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Natural
base
  Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
-> (SymBV sym w -> Doc ann) -> Maybe (SymBV sym w) -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
forall a. Monoid a => a
mempty 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 Maybe (SymBV sym w)
sz
  Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Mutability -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Mutability
mut
  Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Alignment -> Doc ann
forall ann. Alignment -> Doc ann
ppAlignment Alignment
alignment
  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
loc

ppAlloc :: IsExpr (SymExpr sym) => MemAlloc sym -> Doc ann
ppAlloc :: forall sym ann. IsExpr (SymExpr sym) => MemAlloc sym -> Doc ann
ppAlloc (Allocations Map Natural (AllocInfo sym)
xs) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ ((Natural, AllocInfo sym) -> Doc ann)
-> [(Natural, AllocInfo sym)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Natural, AllocInfo sym) -> Doc ann
forall sym ann.
IsExpr (SymExpr sym) =>
(Natural, AllocInfo sym) -> Doc ann
ppAllocInfo ([(Natural, AllocInfo sym)] -> [(Natural, AllocInfo sym)]
forall a. [a] -> [a]
reverse (Map Natural (AllocInfo sym) -> [(Natural, AllocInfo sym)]
forall k a. Map k a -> [(k, a)]
Map.assocs Map Natural (AllocInfo sym)
xs))
ppAlloc (MemFree SymNat sym
base String
loc) =
  Doc ann
"Free" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymNat sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => SymNat sym -> Doc ann
printSymNat SymNat sym
base 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
loc
ppAlloc (AllocMerge Pred sym
c (MemAllocs [MemAlloc sym]
x) (MemAllocs [MemAlloc sym]
y)) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [Doc ann
"Merge", (MemAlloc sym -> Doc ann)
-> Pred sym -> [MemAlloc sym] -> [MemAlloc sym] -> Doc ann
forall (e :: BaseType -> Type) v ann (tp :: BaseType).
IsExpr e =>
(v -> Doc ann) -> e tp -> [v] -> [v] -> Doc ann
ppMerge MemAlloc sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => MemAlloc sym -> Doc ann
ppAlloc Pred sym
c [MemAlloc sym]
x [MemAlloc sym]
y]

ppAllocs :: IsExpr (SymExpr sym) => MemAllocs sym -> Doc ann
ppAllocs :: forall sym ann. IsExpr (SymExpr sym) => MemAllocs sym -> Doc ann
ppAllocs (MemAllocs [MemAlloc sym]
xs) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (MemAlloc sym -> Doc ann) -> [MemAlloc sym] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map MemAlloc sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => MemAlloc sym -> Doc ann
ppAlloc [MemAlloc sym]
xs

ppWrite :: IsExpr (SymExpr sym) => MemWrite sym -> Doc ann
ppWrite :: forall sym ann. IsExpr (SymExpr sym) => MemWrite sym -> Doc ann
ppWrite (MemWrite LLVMPtr sym w
d (MemCopy LLVMPtr sym w
s SymBV sym w
l)) = do
  Doc ann
"memcopy" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LLVMPtr sym w -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
d Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LLVMPtr sym w -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
s 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
l
ppWrite (MemWrite LLVMPtr sym w
d (MemSet SymBV sym 8
v SymBV sym w
l)) = do
  Doc ann
"memset" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LLVMPtr sym w -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
d Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymBV sym 8 -> 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 8
v 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
l
ppWrite (MemWrite LLVMPtr sym w
d (MemStore LLVMVal sym
v StorageType
_ Alignment
_)) = do
  Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'*' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> LLVMPtr sym w -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
d Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LLVMVal sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => LLVMVal sym -> Doc ann
ppTermExpr LLVMVal sym
v
ppWrite (MemWrite LLVMPtr sym w
d (MemArrayStore SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
arr Maybe (SymBV sym w)
_)) = do
  Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'*' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> LLVMPtr sym w -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
d Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8) -> 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 SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
arr
ppWrite (MemWrite LLVMPtr sym w
d (MemInvalidate Text
msg SymBV sym w
l)) = do
  Doc ann
"invalidate" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
msg) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LLVMPtr sym w -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr LLVMPtr sym w
d 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
l
ppWrite (WriteMerge Pred sym
c (MemWrites [MemWritesChunk sym]
x) (MemWrites [MemWritesChunk sym]
y)) = do
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [Doc ann
"merge", (MemWritesChunk sym -> Doc ann)
-> Pred sym
-> [MemWritesChunk sym]
-> [MemWritesChunk sym]
-> Doc ann
forall (e :: BaseType -> Type) v ann (tp :: BaseType).
IsExpr e =>
(v -> Doc ann) -> e tp -> [v] -> [v] -> Doc ann
ppMerge MemWritesChunk sym -> Doc ann
forall sym ann.
IsExpr (SymExpr sym) =>
MemWritesChunk sym -> Doc ann
ppMemWritesChunk Pred sym
c [MemWritesChunk sym]
x [MemWritesChunk sym]
y]

ppMemWritesChunk :: IsExpr (SymExpr sym) => MemWritesChunk sym -> Doc ann
ppMemWritesChunk :: forall sym ann.
IsExpr (SymExpr sym) =>
MemWritesChunk sym -> Doc ann
ppMemWritesChunk = \case
  MemWritesChunkFlat [] ->
    Doc ann
"No writes"
  MemWritesChunkFlat [MemWrite sym]
flat_writes ->
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (MemWrite sym -> Doc ann) -> [MemWrite sym] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map MemWrite sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => MemWrite sym -> Doc ann
ppWrite [MemWrite sym]
flat_writes
  MemWritesChunkIndexed IntMap [MemWrite sym]
indexed_writes ->
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
    [ Doc ann
"Indexed chunk:"
    , 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 ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ ((Int, [MemWrite sym]) -> Doc ann)
-> [(Int, [MemWrite sym])] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map
        (\(Int
blk, [MemWrite sym]
blk_writes) ->
          case [MemWrite sym]
blk_writes of
            [] -> Doc ann
forall a. Monoid a => a
mempty
            [MemWrite sym]
_  -> Int -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Int
blk Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"|->" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
softline Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<>
                    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 ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (MemWrite sym -> Doc ann) -> [MemWrite sym] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map MemWrite sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => MemWrite sym -> Doc ann
ppWrite [MemWrite sym]
blk_writes))
        (IntMap [MemWrite sym] -> [(Int, [MemWrite sym])]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap [MemWrite sym]
indexed_writes))
    ]

ppMemWrites :: IsExpr (SymExpr sym) => MemWrites sym -> Doc ann
ppMemWrites :: forall sym ann. IsExpr (SymExpr sym) => MemWrites sym -> Doc ann
ppMemWrites (MemWrites [MemWritesChunk sym]
ws) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (MemWritesChunk sym -> Doc ann)
-> [MemWritesChunk sym] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map MemWritesChunk sym -> Doc ann
forall sym ann.
IsExpr (SymExpr sym) =>
MemWritesChunk sym -> Doc ann
ppMemWritesChunk [MemWritesChunk sym]
ws

ppMemChanges :: IsExpr (SymExpr sym) => MemChanges sym -> [Doc ann]
ppMemChanges :: forall sym ann. IsExpr (SymExpr sym) => MemChanges sym -> [Doc ann]
ppMemChanges (MemAllocs sym
al,MemWrites sym
wl)
  | MemAllocs sym -> Bool
forall sym. MemAllocs sym -> Bool
nullMemAllocs MemAllocs sym
al Bool -> Bool -> Bool
&& MemWrites sym -> Bool
forall sym. MemWrites sym -> Bool
nullMemWrites MemWrites sym
wl = [Doc ann
"No writes or allocations"]
  | Bool
otherwise =
      (if MemAllocs sym -> Bool
forall sym. MemAllocs sym -> Bool
nullMemAllocs MemAllocs sym
al then [] else [Doc ann
"Allocations:", Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (MemAllocs sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => MemAllocs sym -> Doc ann
ppAllocs MemAllocs sym
al)]) [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<>
      (if MemWrites sym -> Bool
forall sym. MemWrites sym -> Bool
nullMemWrites MemWrites sym
wl then [] else [Doc ann
"Writes:", Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (MemWrites sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => MemWrites sym -> Doc ann
ppMemWrites MemWrites sym
wl)])

ppMemState :: (MemChanges sym -> [Doc ann]) -> MemState sym -> Doc ann
ppMemState :: forall sym ann.
(MemChanges sym -> [Doc ann]) -> MemState sym -> Doc ann
ppMemState MemChanges sym -> [Doc ann]
f (EmptyMem Int
_ Int
_ MemChanges sym
d) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (Doc ann
"Base memory" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Doc ann -> Doc ann) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2) (MemChanges sym -> [Doc ann]
f MemChanges sym
d))
ppMemState MemChanges sym -> [Doc ann]
f (StackFrame Int
_ Int
_ Text
nm MemChanges sym
d MemState sym
ms) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ((Doc ann
"Stack frame" 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
nm) Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Doc ann -> Doc ann) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2) (MemChanges sym -> [Doc ann]
f MemChanges sym
d) [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [(MemChanges sym -> [Doc ann]) -> MemState sym -> Doc ann
forall sym ann.
(MemChanges sym -> [Doc ann]) -> MemState sym -> Doc ann
ppMemState MemChanges sym -> [Doc ann]
f MemState sym
ms])
ppMemState MemChanges sym -> [Doc ann]
f (BranchFrame Int
_ Int
_ MemChanges sym
d MemState sym
ms) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (Doc ann
"Branch frame" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Doc ann -> Doc ann) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2) (MemChanges sym -> [Doc ann]
f MemChanges sym
d) [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [(MemChanges sym -> [Doc ann]) -> MemState sym -> Doc ann
forall sym ann.
(MemChanges sym -> [Doc ann]) -> MemState sym -> Doc ann
ppMemState MemChanges sym -> [Doc ann]
f MemState sym
ms])

ppMem :: IsExpr (SymExpr sym) => Mem sym -> Doc ann
ppMem :: forall sym ann. IsExpr (SymExpr sym) => Mem sym -> Doc ann
ppMem Mem sym
m = (MemChanges sym -> [Doc ann]) -> MemState sym -> Doc ann
forall sym ann.
(MemChanges sym -> [Doc ann]) -> MemState sym -> Doc ann
ppMemState MemChanges sym -> [Doc ann]
forall sym ann. IsExpr (SymExpr sym) => MemChanges sym -> [Doc ann]
ppMemChanges (Mem sym
mMem sym
-> Getting (MemState sym) (Mem sym) (MemState sym) -> MemState sym
forall s a. s -> Getting a s a -> a
^.Getting (MemState sym) (Mem sym) (MemState sym)
forall sym (f :: Type -> Type).
Functor f =>
(MemState sym -> f (MemState sym)) -> Mem sym -> f (Mem sym)
memState)


------------------------------------------------------------------------------
-- Write ranges

multiUnion :: (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a
multiUnion :: forall k a. (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a
multiUnion = (a -> a -> a) -> Map k a -> Map k a -> Map k a
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>)

-- | This will return 'Just' if the size of the write is bounded and 'Nothing'
-- is the size of the write is unbounded.
writeSourceSize ::
  (IsExprBuilder sym, 1 <= w) =>
  sym ->
  NatRepr w ->
  WriteSource sym w ->
  MaybeT IO (SymBV sym w)
writeSourceSize :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> WriteSource sym w -> MaybeT IO (SymBV sym w)
writeSourceSize sym
sym NatRepr w
w = \case
  MemCopy LLVMPtr sym w
_src SymBV sym w
sz -> SymBV sym w -> MaybeT IO (SymBV sym w)
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymBV sym w
sz
  MemSet SymBV sym 8
_val SymBV sym w
sz -> SymBV sym w -> MaybeT IO (SymBV sym w)
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymBV sym w
sz
  MemStore LLVMVal sym
_val StorageType
st Alignment
_align ->
    IO (SymBV sym w) -> MaybeT IO (SymBV sym w)
forall a. IO a -> MaybeT IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymBV sym w) -> MaybeT IO (SymBV sym w))
-> IO (SymBV sym w) -> MaybeT IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$ sym -> NatRepr w -> BV w -> IO (SymBV sym w)
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 NatRepr w
w (BV w -> IO (SymBV sym w)) -> BV w -> IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$ NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (Integer -> BV w) -> Integer -> BV w
forall a b. (a -> b) -> a -> b
$ Bytes -> Integer
forall a. Integral a => a -> Integer
toInteger (Bytes -> Integer) -> Bytes -> Integer
forall a b. (a -> b) -> a -> b
$ Bytes -> StorageType -> Bytes
typeEnd Bytes
0 StorageType
st
  MemArrayStore SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
_arr Maybe (SymBV sym w)
Nothing -> IO (Maybe (SymBV sym w)) -> MaybeT IO (SymBV sym w)
forall (m :: Type -> Type) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe (SymBV sym w)) -> MaybeT IO (SymBV sym w))
-> IO (Maybe (SymBV sym w)) -> MaybeT IO (SymBV sym w)
forall a b. (a -> b) -> a -> b
$ Maybe (SymBV sym w) -> IO (Maybe (SymBV sym w))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (SymBV sym w)
forall a. Maybe a
Nothing
  MemArrayStore SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
_arr (Just SymBV sym w
sz) -> SymBV sym w -> MaybeT IO (SymBV sym w)
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymBV sym w
sz
  MemInvalidate Text
_nm SymBV sym w
sz -> SymBV sym w -> MaybeT IO (SymBV sym w)
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymBV sym w
sz

writeRangesMemWrite ::
  (IsExprBuilder sym, HasPtrWidth w) =>
  sym ->
  MemWrite sym ->
  MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWrite :: forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemWrite sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWrite sym
sym = \case
  MemWrite LLVMPtr sym w
ptr WriteSource sym w
wsrc
    | Just w :~: w
Refl <- 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 ?ptrWidth::NatRepr w
NatRepr w
?ptrWidth (LLVMPtr sym w -> NatRepr w
forall sym (w :: Natural).
IsExprBuilder sym =>
LLVMPtr sym w -> NatRepr w
ptrWidth LLVMPtr sym w
ptr) ->
      case SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat (LLVMPtr sym w -> SymNat sym
forall sym (w :: Natural). LLVMPtr sym w -> SymNat sym
llvmPointerBlock LLVMPtr sym w
LLVMPtr sym w
ptr) of
        Just Natural
blk -> do
          SymExpr sym (BaseBVType w)
sz <- sym -> NatRepr w -> WriteSource sym w -> MaybeT IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> WriteSource sym w -> MaybeT IO (SymBV sym w)
writeSourceSize sym
sym ?ptrWidth::NatRepr w
NatRepr w
?ptrWidth WriteSource sym w
wsrc
          Map
  Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall a. a -> MaybeT IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Map
   Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> MaybeT
      IO
      (Map
         Natural
         [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]))
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall a b. (a -> b) -> a -> b
$ Natural
-> [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall k a. k -> a -> Map k a
Map.singleton Natural
blk [(LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Natural). LLVMPtr sym w -> SymBV sym w
llvmPointerOffset LLVMPtr sym w
LLVMPtr sym w
ptr, SymExpr sym (BaseBVType w)
sz)]
        Maybe Natural
Nothing -> IO
  (Maybe
     (Map
        Natural
        [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]))
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall (m :: Type -> Type) a. m (Maybe a) -> MaybeT m a
MaybeT (IO
   (Maybe
      (Map
         Natural
         [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]))
 -> MaybeT
      IO
      (Map
         Natural
         [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]))
-> IO
     (Maybe
        (Map
           Natural
           [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]))
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall a b. (a -> b) -> a -> b
$ Maybe
  (Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> IO
     (Maybe
        (Map
           Natural
           [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe
  (Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall a. Maybe a
Nothing
    | Bool
otherwise -> String
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall a. String -> MaybeT IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"foo"
  WriteMerge Pred sym
_p MemWrites sym
ws1 MemWrites sym
ws2 ->
    Map
  Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall k a. (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a
multiUnion (Map
   Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
      -> Map
           Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> MemWrites sym
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemWrites sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWrites sym
sym MemWrites sym
ws1 MaybeT
  IO
  (Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
   -> Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym
-> MemWrites sym
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemWrites sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWrites sym
sym MemWrites sym
ws2

writeRangesMemWritesChunk ::
  (IsExprBuilder sym, HasPtrWidth w) =>
  sym ->
  MemWritesChunk sym ->
  MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWritesChunk :: forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemWritesChunk sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWritesChunk sym
sym = \case
  MemWritesChunkFlat [MemWrite sym]
ws -> (Map
   Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> [Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map
  Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall k a. (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a
multiUnion Map
  Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall k a. Map k a
Map.empty ([Map
    Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     [Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (MemWrite sym
 -> MaybeT
      IO
      (Map
         Natural
         [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]))
-> [MemWrite sym]
-> MaybeT
     IO
     [Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (sym
-> MemWrite sym
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemWrite sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWrite sym
sym) [MemWrite sym]
ws
  MemWritesChunkIndexed IntMap [MemWrite sym]
mp ->
    (Map
   Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> [Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map
  Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall k a. (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a
multiUnion Map
  Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall k a. Map k a
Map.empty ([Map
    Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     [Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (MemWrite sym
 -> MaybeT
      IO
      (Map
         Natural
         [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]))
-> [MemWrite sym]
-> MaybeT
     IO
     [Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (sym
-> MemWrite sym
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemWrite sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWrite sym
sym) ([[MemWrite sym]] -> [MemWrite sym]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat ([[MemWrite sym]] -> [MemWrite sym])
-> [[MemWrite sym]] -> [MemWrite sym]
forall a b. (a -> b) -> a -> b
$ IntMap [MemWrite sym] -> [[MemWrite sym]]
forall a. IntMap a -> [a]
IntMap.elems IntMap [MemWrite sym]
mp)

writeRangesMemWrites ::
  (IsExprBuilder sym, HasPtrWidth w) =>
  sym ->
  MemWrites sym ->
  MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWrites :: forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemWrites sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWrites sym
sym (MemWrites [MemWritesChunk sym]
ws) =
  (Map
   Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> [Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map
  Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall k a. (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a
multiUnion Map
  Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall k a. Map k a
Map.empty ([Map
    Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     [Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (MemWritesChunk sym
 -> MaybeT
      IO
      (Map
         Natural
         [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]))
-> [MemWritesChunk sym]
-> MaybeT
     IO
     [Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (sym
-> MemWritesChunk sym
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemWritesChunk sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWritesChunk sym
sym) [MemWritesChunk sym]
ws

writeRangesMemChanges ::
  (IsExprBuilder sym, HasPtrWidth w) =>
  sym ->
  MemChanges sym ->
  MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemChanges :: forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemChanges sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemChanges sym
sym (MemAllocs sym
_as, MemWrites sym
ws) = sym
-> MemWrites sym
-> MaybeT
     IO
     (Map
        Natural
        [(SymExpr sym ('BaseBVType w), SymExpr sym ('BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemWrites sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemWrites sym
sym MemWrites sym
ws

writeRangesMemState ::
  (IsExprBuilder sym, HasPtrWidth w) =>
  sym ->
  MemState sym ->
  MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemState :: forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemState sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemState sym
sym = \case
  EmptyMem Int
_a Int
_w MemChanges sym
chs -> sym
-> MemChanges sym
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemChanges sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemChanges sym
sym MemChanges sym
chs
  StackFrame Int
_a Int
_w Text
_nm MemChanges sym
chs MemState sym
st ->
    Map
  Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall k a. (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a
multiUnion (Map
   Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
      -> Map
           Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> MemChanges sym
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemChanges sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemChanges sym
sym MemChanges sym
chs MaybeT
  IO
  (Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
   -> Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym
-> MemState sym
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemState sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemState sym
sym MemState sym
st
  BranchFrame Int
_a Int
_w MemChanges sym
chs MemState sym
st ->
    Map
  Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
-> Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
forall k a. (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a
multiUnion (Map
   Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
 -> Map
      Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
      -> Map
           Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> MemChanges sym
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemChanges sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemChanges sym
sym MemChanges sym
chs MaybeT
  IO
  (Map
     Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))]
   -> Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall a b. MaybeT IO (a -> b) -> MaybeT IO a -> MaybeT IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym
-> MemState sym
-> MaybeT
     IO
     (Map
        Natural [(SymExpr sym (BaseBVType w), SymExpr sym (BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemState sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemState sym
sym MemState sym
st

-- | Compute the ranges (pairs of the form pointer offset and size) for all
-- memory writes, indexed by the pointer base. The result is Nothing if the
-- memory contains any writes with symbolic pointer base, or without size.
writeRangesMem ::
  (IsExprBuilder sym, HasPtrWidth w) =>
  sym ->
  Mem sym ->
  MaybeT IO ((Map Natural [(SymBV sym w, SymBV sym w)]))
writeRangesMem :: forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> Mem sym -> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMem sym
sym Mem sym
mem = sym
-> MemState sym
-> MaybeT
     IO
     (Map
        Natural
        [(SymExpr sym ('BaseBVType w), SymExpr sym ('BaseBVType w))])
forall sym (w :: Natural).
(IsExprBuilder sym, HasPtrWidth w) =>
sym
-> MemState sym
-> MaybeT IO (Map Natural [(SymBV sym w, SymBV sym w)])
writeRangesMemState sym
sym (MemState sym
 -> MaybeT
      IO
      (Map
         Natural
         [(SymExpr sym ('BaseBVType w), SymExpr sym ('BaseBVType w))]))
-> MemState sym
-> MaybeT
     IO
     (Map
        Natural
        [(SymExpr sym ('BaseBVType w), SymExpr sym ('BaseBVType w))])
forall a b. (a -> b) -> a -> b
$ Mem sym
mem Mem sym
-> Getting (MemState sym) (Mem sym) (MemState sym) -> MemState sym
forall s a. s -> Getting a s a -> a
^. Getting (MemState sym) (Mem sym) (MemState sym)
forall sym (f :: Type -> Type).
Functor f =>
(MemState sym -> f (MemState sym)) -> Mem sym -> f (Mem sym)
memState


------------------------------------------------------------------------------
-- Concretization

concAllocInfo ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  AllocInfo sym -> IO (AllocInfo sym)
concAllocInfo :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> AllocInfo sym
-> IO (AllocInfo sym)
concAllocInfo sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (AllocInfo AllocType
atp Maybe (SymBV sym w)
sz Mutability
m Alignment
a String
nm) =
  do Maybe (SymBV sym w)
sz' <- (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 :: Natural).
(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)
sz
     AllocInfo sym -> IO (AllocInfo sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AllocType
-> Maybe (SymBV sym w)
-> Mutability
-> Alignment
-> String
-> AllocInfo sym
forall sym (w :: Natural).
(1 <= w) =>
AllocType
-> Maybe (SymBV sym w)
-> Mutability
-> Alignment
-> String
-> AllocInfo sym
AllocInfo AllocType
atp Maybe (SymBV sym w)
sz' Mutability
m Alignment
a String
nm)

concAlloc ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  MemAlloc sym -> IO (MemAllocs sym)
concAlloc :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemAlloc sym
-> IO (MemAllocs sym)
concAlloc sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (Allocations Map Natural (AllocInfo sym)
m) =
  do Map Natural (AllocInfo sym)
m' <- (AllocInfo sym -> IO (AllocInfo sym))
-> Map Natural (AllocInfo sym) -> IO (Map Natural (AllocInfo 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) -> Map Natural a -> f (Map Natural b)
traverse (sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> AllocInfo sym
-> IO (AllocInfo sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> AllocInfo sym
-> IO (AllocInfo sym)
concAllocInfo sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc) Map Natural (AllocInfo sym)
m
     MemAllocs sym -> IO (MemAllocs sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs [Map Natural (AllocInfo sym) -> MemAlloc sym
forall sym. Map Natural (AllocInfo sym) -> MemAlloc sym
Allocations Map Natural (AllocInfo sym)
m'])
concAlloc sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemFree SymNat sym
blk String
loc) =
  do SymNat sym
blk' <- sym -> SymExpr sym BaseIntegerType -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymNat sym)
integerToNat sym
sym (SymExpr sym BaseIntegerType -> IO (SymNat sym))
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym (Integer -> IO (SymExpr sym BaseIntegerType))
-> IO Integer -> IO (SymExpr sym BaseIntegerType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< SymExpr sym BaseIntegerType -> IO Integer
SymExpr sym BaseIntegerType -> IO (GroundValue BaseIntegerType)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (SymExpr sym BaseIntegerType -> IO Integer)
-> IO (SymExpr sym BaseIntegerType) -> IO Integer
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymNat sym -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> IO (SymInteger sym)
natToInteger sym
sym SymNat sym
blk
     MemAllocs sym -> IO (MemAllocs sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([MemAlloc sym] -> MemAllocs sym
forall sym. [MemAlloc sym] -> MemAllocs sym
MemAllocs [SymNat sym -> String -> MemAlloc sym
forall sym. SymNat sym -> String -> MemAlloc sym
MemFree SymNat sym
blk' String
loc])
concAlloc sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (AllocMerge Pred sym
p MemAllocs sym
m1 MemAllocs sym
m2) =
  do Bool
b <- Pred sym -> IO (GroundValue BaseBoolType)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Pred sym
p
     if Bool
b then sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemAllocs sym
-> IO (MemAllocs sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemAllocs sym
-> IO (MemAllocs sym)
concMemAllocs sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemAllocs sym
m1
          else sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemAllocs sym
-> IO (MemAllocs sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemAllocs sym
-> IO (MemAllocs sym)
concMemAllocs sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemAllocs sym
m2

concMemAllocs ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  MemAllocs sym -> IO (MemAllocs sym)
concMemAllocs :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemAllocs sym
-> IO (MemAllocs sym)
concMemAllocs sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemAllocs [MemAlloc sym]
cs) =
  [MemAllocs sym] -> MemAllocs sym
forall m. Monoid m => [m] -> m
forall (t :: Type -> Type) m. (Foldable t, Monoid m) => t m -> m
fold ([MemAllocs sym] -> MemAllocs sym)
-> IO [MemAllocs sym] -> IO (MemAllocs sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (MemAlloc sym -> IO (MemAllocs sym))
-> [MemAlloc sym] -> IO [MemAllocs 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) -> [a] -> f [b]
traverse (sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemAlloc sym
-> IO (MemAllocs sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemAlloc sym
-> IO (MemAllocs sym)
concAlloc sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc) [MemAlloc sym]
cs

concLLVMVal ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  LLVMVal sym -> IO (LLVMVal sym)
concLLVMVal :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMVal sym
-> IO (LLVMVal sym)
concLLVMVal sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (LLVMValInt SymNat sym
blk SymBV sym w
off) =
  do SymNat sym
blk' <- sym -> SymExpr sym BaseIntegerType -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymNat sym)
integerToNat sym
sym (SymExpr sym BaseIntegerType -> IO (SymNat sym))
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym (Integer -> IO (SymExpr sym BaseIntegerType))
-> IO Integer -> IO (SymExpr sym BaseIntegerType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< SymExpr sym BaseIntegerType -> IO Integer
SymExpr sym BaseIntegerType -> IO (GroundValue BaseIntegerType)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (SymExpr sym BaseIntegerType -> IO Integer)
-> IO (SymExpr sym BaseIntegerType) -> IO Integer
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymNat sym -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> IO (SymInteger sym)
natToInteger sym
sym SymNat sym
blk
     SymBV sym w
off' <- sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(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 w
off
     LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymNat sym -> SymBV sym w -> LLVMVal sym
forall (w :: Natural) sym.
(1 <= w) =>
SymNat sym -> SymBV sym w -> LLVMVal sym
LLVMValInt SymNat sym
blk' SymBV sym w
off')
concLLVMVal sym
_sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
_conc (LLVMValFloat FloatSize fi
fs SymInterpretedFloat sym fi
fi) =
  LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
forall (fi :: FloatInfo) sym.
FloatSize fi -> SymInterpretedFloat sym fi -> LLVMVal sym
LLVMValFloat FloatSize fi
fs SymInterpretedFloat sym fi
fi) -- TODO concreteize floats
concLLVMVal sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (LLVMValStruct Vector (Field StorageType, LLVMVal sym)
fs) =
  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, LLVMVal sym)
 -> IO (Field StorageType, LLVMVal sym))
-> Vector (Field StorageType, LLVMVal sym)
-> 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
fi,LLVMVal sym
v) -> (,) (Field StorageType
 -> LLVMVal sym -> (Field StorageType, LLVMVal sym))
-> IO (Field StorageType)
-> IO (LLVMVal sym -> (Field StorageType, LLVMVal sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Field StorageType -> IO (Field StorageType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Field StorageType
fi IO (LLVMVal sym -> (Field StorageType, LLVMVal sym))
-> IO (LLVMVal sym) -> IO (Field StorageType, 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
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMVal sym
-> IO (LLVMVal sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMVal sym
-> IO (LLVMVal sym)
concLLVMVal sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc LLVMVal sym
v) Vector (Field StorageType, LLVMVal sym)
fs
concLLVMVal sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (LLVMValArray StorageType
st Vector (LLVMVal sym)
vs) =
  StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
forall sym. StorageType -> Vector (LLVMVal sym) -> LLVMVal sym
LLVMValArray StorageType
st (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
<$> (LLVMVal sym -> IO (LLVMVal sym))
-> Vector (LLVMVal sym) -> IO (Vector (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 (sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMVal sym
-> IO (LLVMVal sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMVal sym
-> IO (LLVMVal sym)
concLLVMVal sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc) Vector (LLVMVal sym)
vs
concLLVMVal sym
_ forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
_ v :: LLVMVal sym
v@LLVMValString{} = LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure LLVMVal sym
v
concLLVMVal sym
_ forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
_ v :: LLVMVal sym
v@LLVMValZero{} = LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure LLVMVal sym
v
concLLVMVal sym
_ forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
_ (LLVMValUndef StorageType
st) =
  LLVMVal sym -> IO (LLVMVal sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StorageType -> LLVMVal sym
forall sym. StorageType -> LLVMVal sym
LLVMValZero StorageType
st) -- ??? does it make sense to turn Undef into Zero?


concWriteSource ::
  (IsExprBuilder sym, 1 <= w) =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  WriteSource sym w -> IO (WriteSource sym w)
concWriteSource :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> WriteSource sym w
-> IO (WriteSource sym w)
concWriteSource sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemCopy LLVMPtr sym w
src SymBV sym w
len) =
  LLVMPtr sym w -> SymBV sym w -> WriteSource sym w
LLVMPointer sym w -> SymBV sym w -> WriteSource sym w
forall sym (w :: Natural).
LLVMPtr sym w -> SymBV sym w -> WriteSource sym w
MemCopy (LLVMPointer sym w -> SymBV sym w -> WriteSource sym w)
-> IO (LLVMPointer sym w) -> IO (SymBV sym w -> WriteSource 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 :: Natural).
(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) IO (SymBV sym w -> WriteSource sym w)
-> IO (SymBV sym w) -> IO (WriteSource 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 w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(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 w
len)
concWriteSource sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemSet SymBV sym 8
val SymBV sym w
len) =
  SymBV sym 8 -> SymBV sym w -> WriteSource sym w
forall sym (w :: Natural).
SymBV sym 8 -> SymBV sym w -> WriteSource sym w
MemSet (SymBV sym 8 -> SymBV sym w -> WriteSource sym w)
-> IO (SymBV sym 8) -> IO (SymBV sym w -> WriteSource 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))
-> SymBV sym 8
-> IO (SymBV sym 8)
forall sym (w :: Natural).
(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 8
val) IO (SymBV sym w -> WriteSource sym w)
-> IO (SymBV sym w) -> IO (WriteSource 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 w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(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 w
len)
concWriteSource sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemStore LLVMVal sym
val StorageType
st Alignment
a) =
  LLVMVal sym -> StorageType -> Alignment -> WriteSource sym w
forall sym (w :: Natural).
LLVMVal sym -> StorageType -> Alignment -> WriteSource sym w
MemStore (LLVMVal sym -> StorageType -> Alignment -> WriteSource sym w)
-> IO (LLVMVal sym)
-> IO (StorageType -> Alignment -> WriteSource 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))
-> LLVMVal sym
-> IO (LLVMVal sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMVal sym
-> IO (LLVMVal sym)
concLLVMVal sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc LLVMVal sym
val IO (StorageType -> Alignment -> WriteSource sym w)
-> IO StorageType -> IO (Alignment -> WriteSource 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
<*> StorageType -> IO StorageType
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure StorageType
st IO (Alignment -> WriteSource sym w)
-> IO Alignment -> IO (WriteSource 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
<*> Alignment -> IO Alignment
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Alignment
a

concWriteSource sym
_sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
_conc (MemArrayStore SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
arr Maybe (SymBV sym w)
Nothing) =
  -- TODO, concretize the actual array
  WriteSource sym w -> IO (WriteSource sym w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
-> Maybe (SymBV sym w) -> WriteSource sym w
forall sym (w :: Natural).
SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
-> Maybe (SymBV sym w) -> WriteSource sym w
MemArrayStore SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
arr Maybe (SymBV sym w)
forall a. Maybe a
Nothing)
concWriteSource sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemArrayStore SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
arr (Just SymBV sym w
sz)) =
  -- TODO, concretize the actual array
  SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
-> Maybe (SymBV sym w) -> WriteSource sym w
forall sym (w :: Natural).
SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
-> Maybe (SymBV sym w) -> WriteSource sym w
MemArrayStore SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)
arr (Maybe (SymBV sym w) -> WriteSource sym w)
-> (SymBV sym w -> Maybe (SymBV sym w))
-> SymBV sym w
-> WriteSource sym w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymBV sym w -> Maybe (SymBV sym w)
forall a. a -> Maybe a
Just (SymBV sym w -> WriteSource sym w)
-> IO (SymBV sym w) -> IO (WriteSource 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))
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(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 w
sz

concWriteSource sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemInvalidate Text
nm SymBV sym w
len) =
  Text -> SymBV sym w -> WriteSource sym w
forall sym (w :: Natural). Text -> SymBV sym w -> WriteSource sym w
MemInvalidate Text
nm (SymBV sym w -> WriteSource sym w)
-> IO (SymBV sym w) -> IO (WriteSource 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))
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(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 w
len

concMemWrite ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  MemWrite sym -> IO (MemWrites sym)
concMemWrite :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrite sym
-> IO (MemWrites sym)
concMemWrite sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemWrite LLVMPtr sym w
ptr WriteSource sym w
wsrc) =
  do LLVMPointer sym w
ptr' <- sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> LLVMPtr sym w
-> IO (LLVMPtr sym w)
forall sym (w :: Natural).
(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
     WriteSource sym w
wsrc' <- sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> WriteSource sym w
-> IO (WriteSource sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> WriteSource sym w
-> IO (WriteSource sym w)
concWriteSource sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc WriteSource sym w
wsrc
     MemWrites sym -> IO (MemWrites sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MemWrites sym -> IO (MemWrites sym))
-> MemWrites sym -> IO (MemWrites sym)
forall a b. (a -> b) -> a -> b
$ LLVMPtr sym w -> WriteSource sym w -> MemWrites sym
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
LLVMPtr sym w -> WriteSource sym w -> MemWrites sym
memWritesSingleton LLVMPtr sym w
LLVMPointer sym w
ptr' WriteSource sym w
wsrc'
concMemWrite sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (WriteMerge Pred sym
p MemWrites sym
m1 MemWrites sym
m2) =
  do Bool
b <- Pred sym -> IO (GroundValue BaseBoolType)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Pred sym
p
     if Bool
b then sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrites sym
-> IO (MemWrites sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrites sym
-> IO (MemWrites sym)
concMemWrites sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemWrites sym
m1
          else sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrites sym
-> IO (MemWrites sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrites sym
-> IO (MemWrites sym)
concMemWrites sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemWrites sym
m2

concMemWrites ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  MemWrites sym -> IO (MemWrites sym)
concMemWrites :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrites sym
-> IO (MemWrites sym)
concMemWrites sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemWrites [MemWritesChunk sym]
cs) =
  [MemWrites sym] -> MemWrites sym
forall m. Monoid m => [m] -> m
forall (t :: Type -> Type) m. (Foldable t, Monoid m) => t m -> m
fold ([MemWrites sym] -> MemWrites sym)
-> IO [MemWrites sym] -> IO (MemWrites sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (MemWritesChunk sym -> IO (MemWrites sym))
-> [MemWritesChunk sym] -> IO [MemWrites sym]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWritesChunk sym
-> IO (MemWrites sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWritesChunk sym
-> IO (MemWrites sym)
concMemWritesChunk sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc) [MemWritesChunk sym]
cs

concMemWritesChunk ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  MemWritesChunk sym -> IO (MemWrites sym)
concMemWritesChunk :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWritesChunk sym
-> IO (MemWrites sym)
concMemWritesChunk sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemWritesChunkFlat [MemWrite sym]
ws) =
  [MemWrites sym] -> MemWrites sym
forall m. Monoid m => [m] -> m
forall (t :: Type -> Type) m. (Foldable t, Monoid m) => t m -> m
fold ([MemWrites sym] -> MemWrites sym)
-> IO [MemWrites sym] -> IO (MemWrites sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (MemWrite sym -> IO (MemWrites sym))
-> [MemWrite sym] -> IO [MemWrites sym]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrite sym
-> IO (MemWrites sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrite sym
-> IO (MemWrites sym)
concMemWrite sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc) [MemWrite sym]
ws
concMemWritesChunk sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemWritesChunkIndexed IntMap [MemWrite sym]
mp) =
  [MemWrites sym] -> MemWrites sym
forall m. Monoid m => [m] -> m
forall (t :: Type -> Type) m. (Foldable t, Monoid m) => t m -> m
fold ([MemWrites sym] -> MemWrites sym)
-> IO [MemWrites sym] -> IO (MemWrites sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (MemWrite sym -> IO (MemWrites sym))
-> [MemWrite sym] -> IO [MemWrites sym]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrite sym
-> IO (MemWrites sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrite sym
-> IO (MemWrites sym)
concMemWrite sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc) ([[MemWrite sym]] -> [MemWrite sym]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat (IntMap [MemWrite sym] -> [[MemWrite sym]]
forall a. IntMap a -> [a]
IntMap.elems IntMap [MemWrite sym]
mp))

concMemChanges ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  MemChanges sym -> IO (MemChanges sym)
concMemChanges :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemChanges sym
-> IO (MemChanges sym)
concMemChanges sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemAllocs sym
as, MemWrites sym
ws) =
  (,) (MemAllocs sym -> MemWrites sym -> (MemAllocs sym, MemWrites sym))
-> IO (MemAllocs sym)
-> IO (MemWrites sym -> (MemAllocs sym, MemWrites 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))
-> MemAllocs sym
-> IO (MemAllocs sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemAllocs sym
-> IO (MemAllocs sym)
concMemAllocs sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemAllocs sym
as IO (MemWrites sym -> (MemAllocs sym, MemWrites sym))
-> IO (MemWrites sym) -> IO (MemAllocs sym, MemWrites 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
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrites sym
-> IO (MemWrites sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemWrites sym
-> IO (MemWrites sym)
concMemWrites sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemWrites sym
ws


concMemState ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  MemState sym -> IO (MemState sym)
concMemState :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemState sym
-> IO (MemState sym)
concMemState sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (EmptyMem Int
a Int
w MemChanges sym
chs) =
  Int -> Int -> MemChanges sym -> MemState sym
forall sym. Int -> Int -> MemChanges sym -> MemState sym
EmptyMem Int
a Int
w (MemChanges sym -> MemState sym)
-> IO (MemChanges sym) -> IO (MemState 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))
-> MemChanges sym
-> IO (MemChanges sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemChanges sym
-> IO (MemChanges sym)
concMemChanges sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemChanges sym
chs
concMemState sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (StackFrame Int
a Int
w Text
nm MemChanges sym
frm MemState sym
stk) =
  Int
-> Int -> Text -> MemChanges sym -> MemState sym -> MemState sym
forall sym.
Int
-> Int -> Text -> MemChanges sym -> MemState sym -> MemState sym
StackFrame Int
a Int
w Text
nm (MemChanges sym -> MemState sym -> MemState sym)
-> IO (MemChanges sym) -> IO (MemState sym -> MemState 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))
-> MemChanges sym
-> IO (MemChanges sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemChanges sym
-> IO (MemChanges sym)
concMemChanges sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemChanges sym
frm IO (MemState sym -> MemState sym)
-> IO (MemState sym) -> IO (MemState 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
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemState sym
-> IO (MemState sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemState sym
-> IO (MemState sym)
concMemState sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemState sym
stk
concMemState sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (BranchFrame Int
a Int
w MemChanges sym
frm MemState sym
stk) =
  Int -> Int -> MemChanges sym -> MemState sym -> MemState sym
forall sym.
Int -> Int -> MemChanges sym -> MemState sym -> MemState sym
BranchFrame Int
a Int
w (MemChanges sym -> MemState sym -> MemState sym)
-> IO (MemChanges sym) -> IO (MemState sym -> MemState 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))
-> MemChanges sym
-> IO (MemChanges sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemChanges sym
-> IO (MemChanges sym)
concMemChanges sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemChanges sym
frm IO (MemState sym -> MemState sym)
-> IO (MemState sym) -> IO (MemState 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
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemState sym
-> IO (MemState sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemState sym
-> IO (MemState sym)
concMemState sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc MemState sym
stk

concMem ::
  IsExprBuilder sym =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  Mem sym -> IO (Mem sym)
concMem :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Mem sym
-> IO (Mem sym)
concMem sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Mem sym
mem = do
  MemState sym
conc_st <- sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemState sym
-> IO (MemState sym)
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> MemState sym
-> IO (MemState sym)
concMemState sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (MemState sym -> IO (MemState sym))
-> MemState sym -> IO (MemState sym)
forall a b. (a -> b) -> a -> b
$ Mem sym
mem Mem sym
-> Getting (MemState sym) (Mem sym) (MemState sym) -> MemState sym
forall s a. s -> Getting a s a -> a
^. Getting (MemState sym) (Mem sym) (MemState sym)
forall sym (f :: Type -> Type).
Functor f =>
(MemState sym -> f (MemState sym)) -> Mem sym -> f (Mem sym)
memState
  Mem sym -> IO (Mem sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Mem sym -> IO (Mem sym)) -> Mem sym -> IO (Mem sym)
forall a b. (a -> b) -> a -> b
$ Mem sym
mem Mem sym -> (Mem sym -> Mem sym) -> Mem sym
forall a b. a -> (a -> b) -> b
& (MemState sym -> Identity (MemState sym))
-> Mem sym -> Identity (Mem sym)
forall sym (f :: Type -> Type).
Functor f =>
(MemState sym -> f (MemState sym)) -> Mem sym -> f (Mem sym)
memState ((MemState sym -> Identity (MemState sym))
 -> Mem sym -> Identity (Mem sym))
-> MemState sym -> Mem sym -> Mem sym
forall s t a b. ASetter s t a b -> b -> s -> t
.~ MemState sym
conc_st