------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.ArraySizeProfile
-- Description      : Execution feature to observe argument buffer sizes
-- Copyright        : (c) Galois, Inc 2020
-- License          : BSD3
-- Maintainer       : Samuel Breese <sbreese@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# Options -Wall #-}
{-# Language TemplateHaskell #-}
{-# Language OverloadedStrings #-}
{-# Language LambdaCase #-}
{-# Language MultiWayIf #-}
{-# Language ImplicitParams #-}
{-# Language ViewPatterns #-}
{-# Language PatternSynonyms #-}
{-# Language BangPatterns #-}
{-# Language FlexibleContexts #-}
{-# Language ScopedTypeVariables #-}
{-# Language DataKinds #-}
{-# Language KindSignatures #-}
{-# Language TypeFamilies #-}
{-# Language TypeApplications #-}
{-# Language GADTs #-}

module Lang.Crucible.LLVM.ArraySizeProfile
 ( FunctionProfile(..), funProfileName, funProfileArgs
 , ArgProfile(..), argProfileSize, argProfileInitialized
 , arraySizeProfile
 ) where

import Control.Lens.TH

import Control.Lens

import Data.Type.Equality (testEquality)
import Data.IORef
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Vector as Vector
import Data.Map (Map)
import qualified Data.Map as Map

import qualified Data.BitVector.Sized as BV
import Data.Parameterized.SymbolRepr
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.TraversableFC

import qualified Lang.Crucible.Backend as C
import qualified Lang.Crucible.CFG.Core as C
import qualified Lang.Crucible.Simulator.CallFrame as C
import qualified Lang.Crucible.Simulator.EvalStmt as C
import qualified Lang.Crucible.Simulator.ExecutionTree as C
import qualified Lang.Crucible.Simulator.GlobalState as C
import qualified Lang.Crucible.Simulator.Intrinsics as C
import qualified Lang.Crucible.Simulator.RegMap as C

import qualified Lang.Crucible.LLVM.DataLayout as C
import qualified Lang.Crucible.LLVM.Extension as C
import qualified Lang.Crucible.LLVM.MemModel as C
import qualified Lang.Crucible.LLVM.MemModel.Generic as G
import qualified Lang.Crucible.LLVM.Translation.Monad as C

import qualified What4.Interface as W4

------------------------------------------------------------------------
-- Profiles

data ArgProfile = ArgProfile
  { ArgProfile -> Maybe Int
_argProfileSize :: Maybe Int
  , ArgProfile -> Bool
_argProfileInitialized :: Bool
  } deriving (Int -> ArgProfile -> ShowS
[ArgProfile] -> ShowS
ArgProfile -> String
(Int -> ArgProfile -> ShowS)
-> (ArgProfile -> String)
-> ([ArgProfile] -> ShowS)
-> Show ArgProfile
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ArgProfile -> ShowS
showsPrec :: Int -> ArgProfile -> ShowS
$cshow :: ArgProfile -> String
show :: ArgProfile -> String
$cshowList :: [ArgProfile] -> ShowS
showList :: [ArgProfile] -> ShowS
Show, ArgProfile -> ArgProfile -> Bool
(ArgProfile -> ArgProfile -> Bool)
-> (ArgProfile -> ArgProfile -> Bool) -> Eq ArgProfile
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ArgProfile -> ArgProfile -> Bool
== :: ArgProfile -> ArgProfile -> Bool
$c/= :: ArgProfile -> ArgProfile -> Bool
/= :: ArgProfile -> ArgProfile -> Bool
Eq, Eq ArgProfile
Eq ArgProfile =>
(ArgProfile -> ArgProfile -> Ordering)
-> (ArgProfile -> ArgProfile -> Bool)
-> (ArgProfile -> ArgProfile -> Bool)
-> (ArgProfile -> ArgProfile -> Bool)
-> (ArgProfile -> ArgProfile -> Bool)
-> (ArgProfile -> ArgProfile -> ArgProfile)
-> (ArgProfile -> ArgProfile -> ArgProfile)
-> Ord ArgProfile
ArgProfile -> ArgProfile -> Bool
ArgProfile -> ArgProfile -> Ordering
ArgProfile -> ArgProfile -> ArgProfile
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 :: ArgProfile -> ArgProfile -> Ordering
compare :: ArgProfile -> ArgProfile -> Ordering
$c< :: ArgProfile -> ArgProfile -> Bool
< :: ArgProfile -> ArgProfile -> Bool
$c<= :: ArgProfile -> ArgProfile -> Bool
<= :: ArgProfile -> ArgProfile -> Bool
$c> :: ArgProfile -> ArgProfile -> Bool
> :: ArgProfile -> ArgProfile -> Bool
$c>= :: ArgProfile -> ArgProfile -> Bool
>= :: ArgProfile -> ArgProfile -> Bool
$cmax :: ArgProfile -> ArgProfile -> ArgProfile
max :: ArgProfile -> ArgProfile -> ArgProfile
$cmin :: ArgProfile -> ArgProfile -> ArgProfile
min :: ArgProfile -> ArgProfile -> ArgProfile
Ord)
makeLenses ''ArgProfile

data FunctionProfile = FunctionProfile
  { FunctionProfile -> Text
_funProfileName :: Text
  , FunctionProfile -> [ArgProfile]
_funProfileArgs :: [ArgProfile]
  } deriving (Int -> FunctionProfile -> ShowS
[FunctionProfile] -> ShowS
FunctionProfile -> String
(Int -> FunctionProfile -> ShowS)
-> (FunctionProfile -> String)
-> ([FunctionProfile] -> ShowS)
-> Show FunctionProfile
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FunctionProfile -> ShowS
showsPrec :: Int -> FunctionProfile -> ShowS
$cshow :: FunctionProfile -> String
show :: FunctionProfile -> String
$cshowList :: [FunctionProfile] -> ShowS
showList :: [FunctionProfile] -> ShowS
Show, FunctionProfile -> FunctionProfile -> Bool
(FunctionProfile -> FunctionProfile -> Bool)
-> (FunctionProfile -> FunctionProfile -> Bool)
-> Eq FunctionProfile
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FunctionProfile -> FunctionProfile -> Bool
== :: FunctionProfile -> FunctionProfile -> Bool
$c/= :: FunctionProfile -> FunctionProfile -> Bool
/= :: FunctionProfile -> FunctionProfile -> Bool
Eq, Eq FunctionProfile
Eq FunctionProfile =>
(FunctionProfile -> FunctionProfile -> Ordering)
-> (FunctionProfile -> FunctionProfile -> Bool)
-> (FunctionProfile -> FunctionProfile -> Bool)
-> (FunctionProfile -> FunctionProfile -> Bool)
-> (FunctionProfile -> FunctionProfile -> Bool)
-> (FunctionProfile -> FunctionProfile -> FunctionProfile)
-> (FunctionProfile -> FunctionProfile -> FunctionProfile)
-> Ord FunctionProfile
FunctionProfile -> FunctionProfile -> Bool
FunctionProfile -> FunctionProfile -> Ordering
FunctionProfile -> FunctionProfile -> FunctionProfile
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 :: FunctionProfile -> FunctionProfile -> Ordering
compare :: FunctionProfile -> FunctionProfile -> Ordering
$c< :: FunctionProfile -> FunctionProfile -> Bool
< :: FunctionProfile -> FunctionProfile -> Bool
$c<= :: FunctionProfile -> FunctionProfile -> Bool
<= :: FunctionProfile -> FunctionProfile -> Bool
$c> :: FunctionProfile -> FunctionProfile -> Bool
> :: FunctionProfile -> FunctionProfile -> Bool
$c>= :: FunctionProfile -> FunctionProfile -> Bool
>= :: FunctionProfile -> FunctionProfile -> Bool
$cmax :: FunctionProfile -> FunctionProfile -> FunctionProfile
max :: FunctionProfile -> FunctionProfile -> FunctionProfile
$cmin :: FunctionProfile -> FunctionProfile -> FunctionProfile
min :: FunctionProfile -> FunctionProfile -> FunctionProfile
Ord)
makeLenses ''FunctionProfile

------------------------------------------------------------------------
-- Learning a profile from an ExecState

ptrStartsAlloc ::
  W4.IsExpr (W4.SymExpr sym) =>
  C.LLVMPtr sym w ->
  Bool
ptrStartsAlloc :: forall sym (w :: Nat).
IsExpr (SymExpr sym) =>
LLVMPtr sym w -> Bool
ptrStartsAlloc (LLVMPtr sym w -> (SymNat sym, SymBV sym w)
forall sym (w :: Nat). LLVMPtr sym w -> (SymNat sym, SymBV sym w)
C.llvmPointerView -> (SymNat sym
_, SymBV sym w -> Maybe (BV w)
forall (w :: Nat). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W4.asBV -> Just (BV.BV Integer
0))) = Bool
True
ptrStartsAlloc LLVMPtr sym w
_ = Bool
False

ptrAllocSize ::
  forall sym w.
  C.IsSymInterface sym =>
  G.Mem sym ->
  C.LLVMPtr sym w ->
  Maybe Int
ptrAllocSize :: forall sym (w :: Nat).
IsSymInterface sym =>
Mem sym -> LLVMPtr sym w -> Maybe Int
ptrAllocSize Mem sym
mem (LLVMPtr sym w -> (SymNat sym, SymBV sym w)
forall sym (w :: Nat). LLVMPtr sym w -> (SymNat sym, SymBV sym w)
C.llvmPointerView -> (SymNat sym
blk, SymBV sym w
_)) =
  do Nat
a <- SymNat sym -> Maybe Nat
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Nat
W4.asNat SymNat sym
blk
     G.AllocInfo AllocType
_ Maybe (SymBV sym w)
msz Mutability
_ Alignment
_ String
_ <- Nat -> MemAllocs sym -> Maybe (AllocInfo sym)
forall sym.
IsExpr (SymExpr sym) =>
Nat -> MemAllocs sym -> Maybe (AllocInfo sym)
G.possibleAllocInfo Nat
a (Mem sym -> MemAllocs sym
forall sym. Mem sym -> MemAllocs sym
G.memAllocs Mem sym
mem)
     SymBV sym w
sz <- Maybe (SymBV sym w)
msz
     Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> (BV w -> Integer) -> BV w -> Int
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV w -> Int) -> Maybe (BV w) -> Maybe Int
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym w -> Maybe (BV w)
forall (w :: Nat). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W4.asBV SymBV sym w
sz

ptrArraySize ::
  C.IsSymInterface sym =>
  G.Mem sym ->
  C.LLVMPtr sym w ->
  Maybe Int
ptrArraySize :: forall sym (w :: Nat).
IsSymInterface sym =>
Mem sym -> LLVMPtr sym w -> Maybe Int
ptrArraySize Mem sym
mem LLVMPtr sym w
ptr
  | LLVMPtr sym w -> Bool
forall sym (w :: Nat).
IsExpr (SymExpr sym) =>
LLVMPtr sym w -> Bool
ptrStartsAlloc LLVMPtr sym w
ptr = Mem sym -> LLVMPtr sym w -> Maybe Int
forall sym (w :: Nat).
IsSymInterface sym =>
Mem sym -> LLVMPtr sym w -> Maybe Int
ptrAllocSize Mem sym
mem LLVMPtr sym w
ptr
  | Bool
otherwise = Maybe Int
forall a. Maybe a
Nothing

ptrIsInitialized ::
  ( C.IsSymInterface sym, C.HasLLVMAnn sym, C.HasPtrWidth w
  , ?memOpts :: C.MemOptions ) =>
  sym ->
  G.Mem sym ->
  C.LLVMPtr sym w ->
  IO Bool
ptrIsInitialized :: forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth w,
 ?memOpts::MemOptions) =>
sym -> Mem sym -> LLVMPtr sym w -> IO Bool
ptrIsInitialized sym
sym Mem sym
mem LLVMPtr sym w
ptr =
  sym
-> NatRepr w
-> Maybe String
-> LLVMPtr sym w
-> StorageType
-> Alignment
-> Mem sym
-> IO (PartLLVMVal sym)
forall sym (w :: Nat).
(1 <= w, IsSymInterface sym, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
sym
-> NatRepr w
-> Maybe String
-> LLVMPtr sym w
-> StorageType
-> Alignment
-> Mem sym
-> IO (PartLLVMVal sym)
G.readMem sym
sym NatRepr w
forall (w :: Nat) (w' :: Nat).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
C.PtrWidth Maybe String
forall a. Maybe a
Nothing LLVMPtr sym w
ptr (Bytes -> StorageType
C.bitvectorType Bytes
1) Alignment
C.noAlignment Mem sym
mem IO (PartLLVMVal sym) -> (PartLLVMVal sym -> IO Bool) -> IO Bool
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  C.NoErr{} -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
True
  PartLLVMVal sym
_ -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Bool
False

intrinsicArgProfile ::
  ( C.IsSymInterface sym, C.HasLLVMAnn sym, C.HasPtrWidth w
  , ?memOpts :: C.MemOptions ) =>
  sym ->
  G.Mem sym ->
  SymbolRepr nm ->
  C.CtxRepr ctx ->
  C.Intrinsic sym nm ctx ->
  IO ArgProfile
intrinsicArgProfile :: forall sym (w :: Nat) (nm :: Symbol) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth w,
 ?memOpts::MemOptions) =>
sym
-> Mem sym
-> SymbolRepr nm
-> CtxRepr ctx
-> Intrinsic sym nm ctx
-> IO ArgProfile
intrinsicArgProfile sym
sym Mem sym
mem
  (SymbolRepr "LLVM_pointer"
-> SymbolRepr nm -> Maybe ("LLVM_pointer" :~: nm)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol).
SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b)
testEquality (SymbolRepr "LLVM_pointer"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol :: SymbolRepr "LLVM_pointer") -> Just "LLVM_pointer" :~: nm
Refl)
  (Assignment TypeRepr ctx
Ctx.Empty Ctx.:> C.BVRepr (NatRepr w -> NatRepr n -> Maybe (w :~: n)
forall (a :: Nat) (b :: Nat).
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 -> Just w :~: n
Refl)) Intrinsic sym nm ctx
i =
   Maybe Int -> Bool -> ArgProfile
ArgProfile (Mem sym -> LLVMPtr sym w -> Maybe Int
forall sym (w :: Nat).
IsSymInterface sym =>
Mem sym -> LLVMPtr sym w -> Maybe Int
ptrArraySize Mem sym
mem Intrinsic sym nm ctx
LLVMPtr sym w
i) (Bool -> ArgProfile) -> IO Bool -> IO ArgProfile
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Mem sym -> LLVMPtr sym w -> IO Bool
forall sym (w :: Nat).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth w,
 ?memOpts::MemOptions) =>
sym -> Mem sym -> LLVMPtr sym w -> IO Bool
ptrIsInitialized sym
sym Mem sym
mem Intrinsic sym nm ctx
LLVMPtr sym w
i
intrinsicArgProfile sym
_ Mem sym
_ SymbolRepr nm
_ Assignment TypeRepr ctx
_ Intrinsic sym nm ctx
_ = ArgProfile -> IO ArgProfile
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ArgProfile -> IO ArgProfile) -> ArgProfile -> IO ArgProfile
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Bool -> ArgProfile
ArgProfile Maybe Int
forall a. Maybe a
Nothing Bool
False

regValueArgProfile ::
  ( C.IsSymInterface sym, C.HasLLVMAnn sym, C.HasPtrWidth w
  , ?memOpts :: C.MemOptions ) =>
  sym ->
  G.Mem sym ->
  C.TypeRepr tp ->
  C.RegValue sym tp ->
  IO ArgProfile
regValueArgProfile :: forall sym (w :: Nat) (tp :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth w,
 ?memOpts::MemOptions) =>
sym -> Mem sym -> TypeRepr tp -> RegValue sym tp -> IO ArgProfile
regValueArgProfile sym
sym Mem sym
mem (C.IntrinsicRepr SymbolRepr nm
nm CtxRepr ctx
ctx) RegValue sym tp
i = sym
-> Mem sym
-> SymbolRepr nm
-> CtxRepr ctx
-> Intrinsic sym nm ctx
-> IO ArgProfile
forall sym (w :: Nat) (nm :: Symbol) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth w,
 ?memOpts::MemOptions) =>
sym
-> Mem sym
-> SymbolRepr nm
-> CtxRepr ctx
-> Intrinsic sym nm ctx
-> IO ArgProfile
intrinsicArgProfile sym
sym Mem sym
mem SymbolRepr nm
nm CtxRepr ctx
ctx Intrinsic sym nm ctx
RegValue sym tp
i
regValueArgProfile sym
_ Mem sym
_ TypeRepr tp
_ RegValue sym tp
_ = ArgProfile -> IO ArgProfile
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ArgProfile -> IO ArgProfile) -> ArgProfile -> IO ArgProfile
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Bool -> ArgProfile
ArgProfile Maybe Int
forall a. Maybe a
Nothing Bool
False

regEntryArgProfile ::
  ( C.IsSymInterface sym, C.HasLLVMAnn sym, C.HasPtrWidth w
  , ?memOpts :: C.MemOptions ) =>
  sym ->
  G.Mem sym ->
  C.RegEntry sym tp ->
  IO ArgProfile
regEntryArgProfile :: forall sym (w :: Nat) (tp :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth w,
 ?memOpts::MemOptions) =>
sym -> Mem sym -> RegEntry sym tp -> IO ArgProfile
regEntryArgProfile sym
sym Mem sym
mem (C.RegEntry TypeRepr tp
t RegValue sym tp
v) = sym -> Mem sym -> TypeRepr tp -> RegValue sym tp -> IO ArgProfile
forall sym (w :: Nat) (tp :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth w,
 ?memOpts::MemOptions) =>
sym -> Mem sym -> TypeRepr tp -> RegValue sym tp -> IO ArgProfile
regValueArgProfile sym
sym Mem sym
mem TypeRepr tp
t RegValue sym tp
v

newtype Wrap a (b :: C.CrucibleType) = Wrap { forall a (b :: CrucibleType). Wrap a b -> a
unwrap :: a }
argProfiles ::
  ( C.IsSymInterface sym, C.HasLLVMAnn sym, C.HasPtrWidth w
  , ?memOpts :: C.MemOptions ) =>
  sym ->
  G.Mem sym ->
  Ctx.Assignment (C.RegEntry sym) ctx ->
  IO [ArgProfile]
argProfiles :: forall sym (w :: Nat) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth w,
 ?memOpts::MemOptions) =>
sym -> Mem sym -> Assignment (RegEntry sym) ctx -> IO [ArgProfile]
argProfiles sym
sym Mem sym
mem Assignment (RegEntry sym) ctx
as =
  [IO ArgProfile] -> IO [ArgProfile]
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: Type -> Type) a. Monad m => [m a] -> m [a]
sequence (Vector (IO ArgProfile) -> [IO ArgProfile]
forall a. Vector a -> [a]
Vector.toList (Vector (IO ArgProfile) -> [IO ArgProfile])
-> Vector (IO ArgProfile) -> [IO ArgProfile]
forall a b. (a -> b) -> a -> b
$ Assignment (Wrap (IO ArgProfile)) ctx
-> (forall (tp :: CrucibleType).
    Wrap (IO ArgProfile) tp -> IO ArgProfile)
-> Vector (IO ArgProfile)
forall {k} (f :: k -> Type) (tps :: Ctx k) e.
Assignment f tps -> (forall (tp :: k). f tp -> e) -> Vector e
Ctx.toVector ((forall (x :: CrucibleType).
 RegEntry sym x -> Wrap (IO ArgProfile) x)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> Assignment (Wrap (IO ArgProfile)) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (IO ArgProfile -> Wrap (IO ArgProfile) x
forall a (b :: CrucibleType). a -> Wrap a b
Wrap (IO ArgProfile -> Wrap (IO ArgProfile) x)
-> (RegEntry sym x -> IO ArgProfile)
-> RegEntry sym x
-> Wrap (IO ArgProfile) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym -> Mem sym -> RegEntry sym x -> IO ArgProfile
forall sym (w :: Nat) (tp :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth w,
 ?memOpts::MemOptions) =>
sym -> Mem sym -> RegEntry sym tp -> IO ArgProfile
regEntryArgProfile sym
sym Mem sym
mem) Assignment (RegEntry sym) ctx
as) Wrap (IO ArgProfile) tp -> IO ArgProfile
forall a (b :: CrucibleType). Wrap a b -> a
forall (tp :: CrucibleType).
Wrap (IO ArgProfile) tp -> IO ArgProfile
unwrap)

------------------------------------------------------------------------
-- Execution feature for learning profiles

updateProfiles ::
  ( C.IsSymInterface sym, C.HasLLVMAnn sym, C.HasPtrWidth (C.ArchWidth arch)
  , ?memOpts :: C.MemOptions ) =>
  C.LLVMContext arch ->
  IORef (Map Text [FunctionProfile]) ->
  C.ExecState p sym ext rtp ->
  IO ()
updateProfiles :: forall sym (arch :: LLVMArch) p ext rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth (ArchWidth arch),
 ?memOpts::MemOptions) =>
LLVMContext arch
-> IORef (Map Text [FunctionProfile])
-> ExecState p sym ext rtp
-> IO ()
updateProfiles LLVMContext arch
llvm IORef (Map Text [FunctionProfile])
cell ExecState p sym ext rtp
state
  | C.CallState ReturnHandler ret p sym ext rtp f a
_ (C.CrucibleCall BlockID blocks args
_ CallFrame sym ext blocks ret args
frame) SimState p sym ext rtp f a
sim <- ExecState p sym ext rtp
state
  , C.CallFrame { _frameCFG :: ()
C._frameCFG = CFG ext blocks initialArgs ret
cfg, _frameRegs :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> RegMap sym args
C._frameRegs = RegMap sym args
regs } <- CallFrame sym ext blocks ret args
frame
  , Just Mem sym
mem <- MemImpl sym -> Mem sym
forall sym. MemImpl sym -> Mem sym
C.memImplHeap (MemImpl sym -> Mem sym) -> Maybe (MemImpl sym) -> Maybe (Mem sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalVar Mem -> SymGlobalState sym -> Maybe (RegValue sym Mem)
forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
C.lookupGlobal (LLVMContext arch -> GlobalVar Mem
forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
C.llvmMemVar LLVMContext arch
llvm) (SimState p sym ext rtp f a
sim SimState p sym ext rtp f a
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext rtp f a)
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
^. Getting
  (SymGlobalState sym)
  (SimState p sym ext rtp f a)
  (SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals)
  = do
      [ArgProfile]
argProfs <- sym -> Mem sym -> Assignment (RegEntry sym) args -> IO [ArgProfile]
forall sym (w :: Nat) (ctx :: Ctx CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth w,
 ?memOpts::MemOptions) =>
sym -> Mem sym -> Assignment (RegEntry sym) ctx -> IO [ArgProfile]
argProfiles (SimState p sym ext rtp f a
sim SimState p sym ext rtp f a
-> Getting sym (SimState p sym ext rtp f a) sym -> sym
forall s a. s -> Getting a s a -> a
^. Getting sym (SimState p sym ext rtp f a) sym
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: Type -> Type).
(Contravariant f2, Functor f2) =>
(sym -> f2 sym)
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateSymInterface) Mem sym
mem (Assignment (RegEntry sym) args -> IO [ArgProfile])
-> Assignment (RegEntry sym) args -> IO [ArgProfile]
forall a b. (a -> b) -> a -> b
$ RegMap sym args -> Assignment (RegEntry sym) args
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap RegMap sym args
regs
      IORef (Map Text [FunctionProfile])
-> (Map Text [FunctionProfile] -> Map Text [FunctionProfile])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Map Text [FunctionProfile])
cell ((Map Text [FunctionProfile] -> Map Text [FunctionProfile])
 -> IO ())
-> (Map Text [FunctionProfile] -> Map Text [FunctionProfile])
-> IO ()
forall a b. (a -> b) -> a -> b
$ \Map Text [FunctionProfile]
profs ->
        let name :: Text
name = String -> Text
Text.pack (String -> Text)
-> (FnHandle initialArgs ret -> String)
-> FnHandle initialArgs ret
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FnHandle initialArgs ret -> String
forall a. Show a => a -> String
show (FnHandle initialArgs ret -> Text)
-> FnHandle initialArgs ret -> Text
forall a b. (a -> b) -> a -> b
$ CFG ext blocks initialArgs ret -> FnHandle initialArgs ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
C.cfgHandle CFG ext blocks initialArgs ret
cfg
            funProf :: FunctionProfile
funProf = Text -> [ArgProfile] -> FunctionProfile
FunctionProfile Text
name [ArgProfile]
argProfs
        in case Text -> Map Text [FunctionProfile] -> Maybe [FunctionProfile]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
name Map Text [FunctionProfile]
profs of
             Maybe [FunctionProfile]
Nothing -> Text
-> [FunctionProfile]
-> Map Text [FunctionProfile]
-> Map Text [FunctionProfile]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name [FunctionProfile
funProf] Map Text [FunctionProfile]
profs
             Just [FunctionProfile]
variants
               | FunctionProfile
funProf FunctionProfile -> [FunctionProfile] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [FunctionProfile]
variants -> Map Text [FunctionProfile]
profs
               | Bool
otherwise -> Text
-> [FunctionProfile]
-> Map Text [FunctionProfile]
-> Map Text [FunctionProfile]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name (FunctionProfile
funProfFunctionProfile -> [FunctionProfile] -> [FunctionProfile]
forall a. a -> [a] -> [a]
:[FunctionProfile]
variants) Map Text [FunctionProfile]
profs
  | Bool
otherwise = () -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()

arraySizeProfile ::
  forall sym ext arch p rtp.
  ( C.IsSymInterface sym, C.HasLLVMAnn sym, C.HasPtrWidth (C.ArchWidth arch)
  , ?memOpts :: C.MemOptions ) =>
  C.LLVMContext arch ->
  IORef (Map Text [FunctionProfile]) ->
  IO (C.ExecutionFeature p sym ext rtp)
arraySizeProfile :: forall sym ext (arch :: LLVMArch) p rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth (ArchWidth arch),
 ?memOpts::MemOptions) =>
LLVMContext arch
-> IORef (Map Text [FunctionProfile])
-> IO (ExecutionFeature p sym ext rtp)
arraySizeProfile LLVMContext arch
llvm IORef (Map Text [FunctionProfile])
profiles = do
  ExecutionFeature p sym ext rtp
-> IO (ExecutionFeature p sym ext rtp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ExecutionFeature p sym ext rtp
 -> IO (ExecutionFeature p sym ext rtp))
-> ((ExecState p sym ext rtp
     -> IO (ExecutionFeatureResult p sym ext rtp))
    -> ExecutionFeature p sym ext rtp)
-> (ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeature p sym ext rtp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall p sym ext rtp.
(ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
C.ExecutionFeature ((ExecState p sym ext rtp
  -> IO (ExecutionFeatureResult p sym ext rtp))
 -> IO (ExecutionFeature p sym ext rtp))
-> (ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> IO (ExecutionFeature p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ \ExecState p sym ext rtp
s -> do
    LLVMContext arch
-> IORef (Map Text [FunctionProfile])
-> ExecState p sym ext rtp
-> IO ()
forall sym (arch :: LLVMArch) p ext rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth (ArchWidth arch),
 ?memOpts::MemOptions) =>
LLVMContext arch
-> IORef (Map Text [FunctionProfile])
-> ExecState p sym ext rtp
-> IO ()
updateProfiles LLVMContext arch
llvm IORef (Map Text [FunctionProfile])
profiles ExecState p sym ext rtp
s
    ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange