{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}

{-|
Module      : What4.Expr.Allocator
Description : Expression allocators for controlling hash-consing
Copyright   : (c) Galois Inc, 2015-2022
License     : BSD3
Maintainer  : rdockins@galois.com
-}
module What4.Expr.Allocator
( ExprAllocator(..)
, newStorage
, newCachedStorage

, cacheStartSizeOption
, cacheStartSizeDesc
, cacheTerms
, cacheOptDesc
) where

import           Control.Lens ( (&) )
import           Control.Monad.ST (stToIO)
import           Data.IORef

import qualified Data.Parameterized.HashTable as PH
import           Data.Parameterized.Nonce

import           What4.BaseTypes
import           What4.Concrete
import           What4.Config as CFG
import           What4.Expr.App
import           What4.ProgramLoc
import           What4.Utils.AbstractDomains

------------------------------------------------------------------------
-- Cache start size

-- | Starting size for element cache when caching is enabled.
--   The default value is 100000 elements.
--
--   This option is named \"backend.cache_start_size\"
cacheStartSizeOption :: ConfigOption BaseIntegerType
cacheStartSizeOption :: ConfigOption BaseIntegerType
cacheStartSizeOption = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseIntegerType
BaseIntegerRepr String
"backend.cache_start_size"

-- | The configuration option for setting the size of the initial hash set
--   used by simple builder (measured in number of elements).
cacheStartSizeDesc :: ConfigDesc
cacheStartSizeDesc :: ConfigDesc
cacheStartSizeDesc = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption BaseIntegerType
cacheStartSizeOption OptionStyle BaseIntegerType
sty Maybe (Doc Void)
help (forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
100000))
  where sty :: OptionStyle BaseIntegerType
sty = Bound Integer -> OptionStyle BaseIntegerType
integerWithMinOptSty (forall r. r -> Bound r
CFG.Inclusive Integer
0)
        help :: Maybe (Doc Void)
help = forall a. a -> Maybe a
Just Doc Void
"Starting size for element cache"

------------------------------------------------------------------------
-- Cache terms

-- | Indicates if we should cache terms.  When enabled, hash-consing
--   is used to find and deduplicate common subexpressions.
--   Toggling this option from disabled to enabled will allocate a new
--   hash table; toggling it from enabled to disabled will discard
--   the current hash table.  The default value for this option is `False`.
--
--   This option is named \"use_cache\"
cacheTerms :: ConfigOption BaseBoolType
cacheTerms :: ConfigOption BaseBoolType
cacheTerms = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
BaseBoolRepr String
"use_cache"

cacheOptStyle ::
  NonceGenerator IO t ->
  IORef (ExprAllocator t) ->
  OptionSetting BaseIntegerType ->
  OptionStyle BaseBoolType
cacheOptStyle :: forall t.
NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> OptionStyle BaseBoolType
cacheOptStyle NonceGenerator IO t
gen IORef (ExprAllocator t)
storageRef OptionSetting BaseIntegerType
szSetting =
  OptionStyle BaseBoolType
boolOptSty forall a b. a -> (a -> b) -> b
& forall (tp :: BaseType).
(Maybe (ConcreteVal tp) -> ConcreteVal tp -> IO OptionSetResult)
-> OptionStyle tp -> OptionStyle tp
set_opt_onset
        (\Maybe (ConcreteVal BaseBoolType)
mb ConcreteVal BaseBoolType
b -> Maybe Bool -> Bool -> IO ()
f (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ConcreteVal BaseBoolType -> Bool
fromConcreteBool Maybe (ConcreteVal BaseBoolType)
mb) (ConcreteVal BaseBoolType -> Bool
fromConcreteBool ConcreteVal BaseBoolType
b) forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return OptionSetResult
optOK)
 where
 f :: Maybe Bool -> Bool -> IO ()
 f :: Maybe Bool -> Bool -> IO ()
f Maybe Bool
mb Bool
b | Maybe Bool
mb forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Bool
b = if Bool
b then IO ()
start else IO ()
stop
        | Bool
otherwise = forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

 stop :: IO ()
stop  = do ExprAllocator t
s <- forall t. NonceGenerator IO t -> IO (ExprAllocator t)
newStorage NonceGenerator IO t
gen
            forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef (ExprAllocator t)
storageRef ExprAllocator t
s

 start :: IO ()
start = do Integer
sz <- forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt OptionSetting BaseIntegerType
szSetting
            ExprAllocator t
s <- forall t. NonceGenerator IO t -> Int -> IO (ExprAllocator t)
newCachedStorage NonceGenerator IO t
gen (forall a. Num a => Integer -> a
fromInteger Integer
sz)
            forall a. IORef a -> a -> IO ()
atomicWriteIORef IORef (ExprAllocator t)
storageRef ExprAllocator t
s

cacheOptDesc ::
  NonceGenerator IO t ->
  IORef (ExprAllocator t) ->
  OptionSetting BaseIntegerType ->
  ConfigDesc
cacheOptDesc :: forall t.
NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> ConfigDesc
cacheOptDesc NonceGenerator IO t
gen IORef (ExprAllocator t)
storageRef OptionSetting BaseIntegerType
szSetting =
  forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
    ConfigOption BaseBoolType
cacheTerms
    (forall t.
NonceGenerator IO t
-> IORef (ExprAllocator t)
-> OptionSetting BaseIntegerType
-> OptionStyle BaseBoolType
cacheOptStyle NonceGenerator IO t
gen IORef (ExprAllocator t)
storageRef OptionSetting BaseIntegerType
szSetting)
    (forall a. a -> Maybe a
Just Doc Void
"Use hash-consing during term construction")
    (forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
False))


------------------------------------------------------------------------
-- | ExprAllocator provides an interface for creating expressions from
-- an applications.
-- Parameter @t@ is a phantom type brand used to track nonces.
data ExprAllocator t
   = ExprAllocator { forall t.
ExprAllocator t
-> forall (tp :: BaseType).
   ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
appExpr  :: forall tp
                            .  ProgramLoc
                            -> App (Expr t) tp
                            -> AbstractValue tp
                            -> IO (Expr t tp)
                  , forall t.
ExprAllocator t
-> forall (tp :: BaseType).
   ProgramLoc
   -> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
nonceExpr :: forall tp
                             .  ProgramLoc
                             -> NonceApp t (Expr t) tp
                             -> AbstractValue tp
                             -> IO (Expr t tp)
                  }


------------------------------------------------------------------------
-- Uncached storage

-- | Create a new storage that does not do hash consing.
newStorage :: NonceGenerator IO t -> IO (ExprAllocator t)
newStorage :: forall t. NonceGenerator IO t -> IO (ExprAllocator t)
newStorage NonceGenerator IO t
g = do
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! ExprAllocator { appExpr :: forall (tp :: BaseType).
ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
appExpr = forall t (tp :: BaseType).
NonceGenerator IO t
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedExprFn NonceGenerator IO t
g
                         , nonceExpr :: forall (tp :: BaseType).
ProgramLoc
-> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
nonceExpr = forall t (tp :: BaseType).
NonceGenerator IO t
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedNonceExpr NonceGenerator IO t
g
                         }

uncachedExprFn :: NonceGenerator IO t
              -> ProgramLoc
              -> App (Expr t) tp
              -> AbstractValue tp
              -> IO (Expr t tp)
uncachedExprFn :: forall t (tp :: BaseType).
NonceGenerator IO t
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedExprFn NonceGenerator IO t
g ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v = do
  Nonce t tp
n <- forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
mkExpr Nonce t tp
n ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v

uncachedNonceExpr :: NonceGenerator IO t
                 -> ProgramLoc
                 -> NonceApp t (Expr t) tp
                 -> AbstractValue tp
                 -> IO (Expr t tp)
uncachedNonceExpr :: forall t (tp :: BaseType).
NonceGenerator IO t
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
uncachedNonceExpr NonceGenerator IO t
g ProgramLoc
pc NonceApp t (Expr t) tp
p AbstractValue tp
v = do
  Nonce t tp
n <- forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall t (tp :: BaseType). NonceAppExpr t tp -> Expr t tp
NonceAppExpr forall a b. (a -> b) -> a -> b
$ NonceAppExprCtor { nonceExprId :: Nonce t tp
nonceExprId = Nonce t tp
n
                                          , nonceExprLoc :: ProgramLoc
nonceExprLoc = ProgramLoc
pc
                                          , nonceExprApp :: NonceApp t (Expr t) tp
nonceExprApp = NonceApp t (Expr t) tp
p
                                          , nonceExprAbsValue :: AbstractValue tp
nonceExprAbsValue = AbstractValue tp
v
                                          }

------------------------------------------------------------------------
-- Cached storage

cachedNonceExpr :: NonceGenerator IO t
               -> PH.HashTable PH.RealWorld (NonceApp t (Expr t)) (Expr t)
               -> ProgramLoc
               -> NonceApp t (Expr t) tp
               -> AbstractValue tp
               -> IO (Expr t tp)
cachedNonceExpr :: forall t (tp :: BaseType).
NonceGenerator IO t
-> HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedNonceExpr NonceGenerator IO t
g HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
h ProgramLoc
pc NonceApp t (Expr t) tp
p AbstractValue tp
v = do
  Maybe (Expr t tp)
me <- forall a. ST RealWorld a -> IO a
stToIO forall a b. (a -> b) -> a -> b
$ forall {k} (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
PH.lookup HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
h NonceApp t (Expr t) tp
p
  case Maybe (Expr t tp)
me of
    Just Expr t tp
e -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e
    Maybe (Expr t tp)
Nothing -> do
      Nonce t tp
n <- forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
      let e :: Expr t tp
e = forall t (tp :: BaseType). NonceAppExpr t tp -> Expr t tp
NonceAppExpr forall a b. (a -> b) -> a -> b
$ NonceAppExprCtor { nonceExprId :: Nonce t tp
nonceExprId = Nonce t tp
n
                                            , nonceExprLoc :: ProgramLoc
nonceExprLoc = ProgramLoc
pc
                                            , nonceExprApp :: NonceApp t (Expr t) tp
nonceExprApp = NonceApp t (Expr t) tp
p
                                            , nonceExprAbsValue :: AbstractValue tp
nonceExprAbsValue = AbstractValue tp
v
                                            }
      seq :: forall a b. a -> b -> b
seq Expr t tp
e forall a b. (a -> b) -> a -> b
$ forall a. ST RealWorld a -> IO a
stToIO forall a b. (a -> b) -> a -> b
$ forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
h NonceApp t (Expr t) tp
p Expr t tp
e
      forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e


cachedAppExpr :: forall t tp
               . NonceGenerator IO t
              -> PH.HashTable PH.RealWorld (App (Expr t)) (Expr t)
              -> ProgramLoc
              -> App (Expr t) tp
              -> AbstractValue tp
              -> IO (Expr t tp)
cachedAppExpr :: forall t (tp :: BaseType).
NonceGenerator IO t
-> HashTable RealWorld (App (Expr t)) (Expr t)
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedAppExpr NonceGenerator IO t
g HashTable RealWorld (App (Expr t)) (Expr t)
h ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v = do
  Maybe (Expr t tp)
me <- forall a. ST RealWorld a -> IO a
stToIO forall a b. (a -> b) -> a -> b
$ forall {k} (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
PH.lookup HashTable RealWorld (App (Expr t)) (Expr t)
h App (Expr t) tp
a
  case Maybe (Expr t tp)
me of
    Just Expr t tp
e -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e
    Maybe (Expr t tp)
Nothing -> do
      Nonce t tp
n <- forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO t
g
      let e :: Expr t tp
e = forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
mkExpr Nonce t tp
n ProgramLoc
pc App (Expr t) tp
a AbstractValue tp
v
      seq :: forall a b. a -> b -> b
seq Expr t tp
e forall a b. (a -> b) -> a -> b
$ forall a. ST RealWorld a -> IO a
stToIO forall a b. (a -> b) -> a -> b
$ forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert HashTable RealWorld (App (Expr t)) (Expr t)
h App (Expr t) tp
a Expr t tp
e
      forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e

-- | Create a storage that does hash consing.
newCachedStorage :: forall t
                  . NonceGenerator IO t
                 -> Int
                 -> IO (ExprAllocator t)
newCachedStorage :: forall t. NonceGenerator IO t -> Int -> IO (ExprAllocator t)
newCachedStorage NonceGenerator IO t
g Int
sz = forall a. ST RealWorld a -> IO a
stToIO forall a b. (a -> b) -> a -> b
$ do
  HashTable RealWorld (App (Expr t)) (Expr t)
appCache  <- forall {k1} s (k2 :: k1 -> Type) (v :: k1 -> Type).
Int -> ST s (HashTable s k2 v)
PH.newSized Int
sz
  HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
predCache <- forall {k1} s (k2 :: k1 -> Type) (v :: k1 -> Type).
Int -> ST s (HashTable s k2 v)
PH.newSized Int
sz
  forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExprAllocator { appExpr :: forall (tp :: BaseType).
ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
appExpr = forall t (tp :: BaseType).
NonceGenerator IO t
-> HashTable RealWorld (App (Expr t)) (Expr t)
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedAppExpr NonceGenerator IO t
g HashTable RealWorld (App (Expr t)) (Expr t)
appCache
                        , nonceExpr :: forall (tp :: BaseType).
ProgramLoc
-> NonceApp t (Expr t) tp -> AbstractValue tp -> IO (Expr t tp)
nonceExpr = forall t (tp :: BaseType).
NonceGenerator IO t
-> HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
-> ProgramLoc
-> NonceApp t (Expr t) tp
-> AbstractValue tp
-> IO (Expr t tp)
cachedNonceExpr NonceGenerator IO t
g HashTable RealWorld (NonceApp t (Expr t)) (Expr t)
predCache
                        }