-----------------------------------------------------------------------
-- |
-- Module           : What4.CachedArray
-- Description      : What4 array storage with a concrete backing supporting symbolic indexes
-- Copyright        : (c) Galois, Inc 2020
-- License          : BSD3
-- Maintainer       : Daniel Matichuk <dmatichuk@galois.com>
-- Stability        : provisional
--
--
-- This module provides a storage structure that supports arrays that have reads
-- from and writes to a mix of concrete and symbolic indexes. It can be thought
-- of as a multi-dimensional array that supports reading and writing contiguous
-- "chunks".  It is built on the 'Data.Parameterized.IntervalsMap' structure,
-- which computes an abstract domain over indexes (supporting symbolic
-- reads/writes).
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}

module What4.CachedArray
  (
    CachedArray
  , ArrayChunk
  , mkArrayChunk
  , evalChunk
  , writeChunk
  , writeSingle
  , readSingle
  , readChunk
  , arrayToChunk
  , chunkToArray
  , muxArrays
  , initArrayConcrete
  , initArray
  ) where

import           Control.Lens ( (.~), (&) )
import           Control.Monad ( foldM, join )
import           Control.Monad.Trans ( lift )
import           Data.Functor.Const
import           Data.Maybe ( catMaybes )
import qualified Data.Map as Map
import           Data.Maybe (mapMaybe)
import qualified Data.IORef as IO

import qualified Data.Parameterized.TraversableFC as FC
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Classes
import           Data.Parameterized.NatRepr ( type (<=) )
import qualified Data.Parameterized.Nonce as PN
import qualified Data.BitVector.Sized as BV

import qualified Lang.Crucible.Utils.MuxTree as MT

import qualified What4.Interface as W4
import qualified What4.Partial as W4
import qualified What4.Concrete as W4
import qualified What4.Utils.AbstractDomains as W4
import qualified What4.Utils.BVDomain as BVD

import qualified Data.Parameterized.IntervalsMap as IM
import           Data.Parameterized.IntervalsMap ( AsOrd(..) )

------------------------------------------------
-- Interface

-- TODO: add coalescing function for merging adjacent entries

newtype ArrayChunk sym idx tp =
  ArrayChunk { forall sym (idx :: BaseType) (tp :: BaseType).
ArrayChunk sym idx tp -> SymExpr sym idx -> IO (SymExpr sym tp)
evalChunk :: (W4.SymExpr sym idx -> IO (W4.SymExpr sym tp)) }

mkArrayChunk ::
  forall sym idx tp.
  W4.IsSymExprBuilder sym =>
  sym ->
  (W4.SymExpr sym idx -> IO (W4.SymExpr sym tp)) ->
  IO (ArrayChunk sym idx tp)
mkArrayChunk :: forall sym (idx :: BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> (SymExpr sym idx -> IO (SymExpr sym tp))
-> IO (ArrayChunk sym idx tp)
mkArrayChunk sym
_sym SymExpr sym idx -> IO (SymExpr sym tp)
f = do
  IORef (Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp))
ref <- Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp)
-> IO (IORef (Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp)))
forall a. a -> IO (IORef a)
IO.newIORef Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp)
forall k a. Map k a
Map.empty
  let f' :: SymExpr sym idx -> IO (SymExpr sym tp)
f' SymExpr sym idx
idx = do
        Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp)
m <- IORef (Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp))
-> IO (Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp))
forall a. IORef a -> IO a
IO.readIORef IORef (Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp))
ref
        case AsOrd (SymExpr sym) idx
-> Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp)
-> Maybe (SymExpr sym tp)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SymExpr sym idx -> AsOrd (SymExpr sym) idx
forall {k} (f :: k -> *) (tp :: k). f tp -> AsOrd f tp
AsOrd SymExpr sym idx
idx) Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp)
m of
          Just SymExpr sym tp
v -> SymExpr sym tp -> IO (SymExpr sym tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr sym tp
v
          Maybe (SymExpr sym tp)
Nothing -> do
            SymExpr sym tp
v <- SymExpr sym idx -> IO (SymExpr sym tp)
f SymExpr sym idx
idx
            IORef (Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp))
-> (Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp)
    -> Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
IO.modifyIORef IORef (Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp))
ref (AsOrd (SymExpr sym) idx
-> SymExpr sym tp
-> Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp)
-> Map (AsOrd (SymExpr sym) idx) (SymExpr sym tp)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SymExpr sym idx -> AsOrd (SymExpr sym) idx
forall {k} (f :: k -> *) (tp :: k). f tp -> AsOrd f tp
AsOrd SymExpr sym idx
idx) SymExpr sym tp
v)
            SymExpr sym tp -> IO (SymExpr sym tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr sym tp
v
  ArrayChunk sym idx tp -> IO (ArrayChunk sym idx tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArrayChunk sym idx tp -> IO (ArrayChunk sym idx tp))
-> ArrayChunk sym idx tp -> IO (ArrayChunk sym idx tp)
forall a b. (a -> b) -> a -> b
$ (SymExpr sym idx -> IO (SymExpr sym tp)) -> ArrayChunk sym idx tp
forall sym (idx :: BaseType) (tp :: BaseType).
(SymExpr sym idx -> IO (SymExpr sym tp)) -> ArrayChunk sym idx tp
ArrayChunk SymExpr sym idx -> IO (SymExpr sym tp)
f'

writeChunk ::
  forall sym ctx tp.
  NonEmptyCtx ctx =>
  W4.IsSymExprBuilder sym =>
  sym ->
  -- | base address to write to
  Ctx.Assignment (W4.SymExpr sym) ctx ->
  -- | size of write
  W4.SymExpr sym (CtxFirst ctx) ->
  -- | symbolic value to write
  ArrayChunk sym (CtxFirst ctx) tp ->
  CachedArray sym ctx tp ->
  IO (CachedArray sym ctx tp)
writeChunk :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(NonEmptyCtx ctx, IsSymExprBuilder sym) =>
sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym (CtxFirst ctx)
-> ArrayChunk sym (CtxFirst ctx) tp
-> CachedArray sym ctx tp
-> IO (CachedArray sym ctx tp)
writeChunk sym
sym Assignment (SymExpr sym) ctx
loExpr SymExpr sym (CtxFirst ctx)
offExpr ArrayChunk sym (CtxFirst ctx) tp
chunk CachedArray sym ctx tp
arr | NonEmptyCtxRepr ctx
NonEmptyCtxRepr <- forall k (ctx :: Ctx k). NonEmptyCtx ctx => NonEmptyCtxRepr ctx
nonEmptyCtxRepr @_ @ctx =
  CachedArray sym ctx tp -> forall a. (NonEmptyCtx ctx => a) -> a
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp -> forall a. (NonEmptyCtx ctx => a) -> a
arrConstraints CachedArray sym ctx tp
arr ((NonEmptyCtx ctx => IO (CachedArray sym ctx tp))
 -> IO (CachedArray sym ctx tp))
-> (NonEmptyCtx ctx => IO (CachedArray sym ctx tp))
-> IO (CachedArray sym ctx tp)
forall a b. (a -> b) -> a -> b
$ do
  SymRange sym ctx
rng <- sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym (CtxFirst ctx)
-> IO (SymRange sym ctx)
forall sym (ctx :: Ctx BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym (CtxFirst ctx)
-> IO (SymRange sym ctx)
mkSymRangeOff sym
sym Assignment (SymExpr sym) ctx
loExpr SymExpr sym (CtxFirst ctx)
offExpr
  CachedArray sym ctx tp
arr' <- sym
-> SymRange sym ctx
-> CachedArray sym ctx tp
-> IO (CachedArray sym ctx tp)
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymRange sym ctx
-> CachedArray sym ctx tp
-> IO (CachedArray sym ctx tp)
invalidateEntries sym
sym SymRange sym ctx
rng CachedArray sym ctx tp
arr
  -- offset the incoming function so that its value at zero becomes the value at
  -- the base address
  let
    off :: SymOffset sym ctx
off = SymIndex sym ctx -> SymOffset sym ctx
forall sym (ctx :: Ctx BaseType).
(NonEmptyCtx ctx, IsSymExprBuilder sym) =>
SymIndex sym ctx -> SymOffset sym ctx
indexToOffset (SymIndex sym ctx -> SymOffset sym ctx)
-> SymIndex sym ctx -> SymOffset sym ctx
forall a b. (a -> b) -> a -> b
$ SymRange sym ctx -> SymIndex sym ctx
forall sym (ctx :: Ctx BaseType).
SymRange sym ctx -> SymIndex sym ctx
symRangeLo SymRange sym ctx
rng
    vals :: SymIndex sym ctx -> IO (W4.PartExpr (W4.Pred sym) (W4.SymExpr sym tp))
    vals :: SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
vals SymIndex sym ctx
idx' = do
        Pred sym
p <- sym -> SymRange sym ctx -> SymIndex sym ctx -> IO (Pred sym)
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymRange sym ctx -> SymIndex sym ctx -> IO (Pred sym)
isInRange sym
sym SymRange sym ctx
rng SymIndex sym ctx
idx'
        (SymOffset SymExpr sym (CtxFirst ctx)
idxOffsetExpr) <- SymIndex sym ctx -> SymOffset sym ctx
forall sym (ctx :: Ctx BaseType).
(NonEmptyCtx ctx, IsSymExprBuilder sym) =>
SymIndex sym ctx -> SymOffset sym ctx
indexToOffset (SymIndex sym ctx -> SymOffset sym ctx)
-> IO (SymIndex sym ctx) -> IO (SymOffset sym ctx)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymIndex sym ctx -> SymOffset sym ctx -> IO (SymIndex sym ctx)
forall sym (ctx :: Ctx BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> SymIndex sym ctx -> SymOffset sym ctx -> IO (SymIndex sym ctx)
subSymOffset sym
sym SymIndex sym ctx
idx' SymOffset sym ctx
off
        SymExpr sym tp
v <- ArrayChunk sym (CtxFirst (ctx '::> x)) tp
-> SymExpr sym (CtxFirst (ctx '::> x)) -> IO (SymExpr sym tp)
forall sym (idx :: BaseType) (tp :: BaseType).
ArrayChunk sym idx tp -> SymExpr sym idx -> IO (SymExpr sym tp)
evalChunk ArrayChunk sym (CtxFirst ctx) tp
ArrayChunk sym (CtxFirst (ctx '::> x)) tp
chunk SymExpr sym (CtxFirst ctx)
SymExpr sym (CtxFirst (ctx '::> x))
idxOffsetExpr
        PartExpr (Pred sym) (SymExpr sym tp)
-> IO (PartExpr (Pred sym) (SymExpr sym tp))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PartExpr (Pred sym) (SymExpr sym tp)
 -> IO (PartExpr (Pred sym) (SymExpr sym tp)))
-> PartExpr (Pred sym) (SymExpr sym tp)
-> IO (PartExpr (Pred sym) (SymExpr sym tp))
forall a b. (a -> b) -> a -> b
$ Pred sym -> SymExpr sym tp -> PartExpr (Pred sym) (SymExpr sym tp)
forall (p :: BaseType -> *) a.
IsExpr p =>
p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
W4.mkPE Pred sym
p SymExpr sym tp
v
  ArrayEntry sym ctx tp
entry <- (SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp)))
-> IO (ArrayEntry sym ctx tp)
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp)))
-> IO (ArrayEntry sym ctx tp)
mkMultiEntry SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
vals
  IntervalsMap
  AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
arr'' <- (PMuxTree sym (ArrayEntry sym ctx tp)
 -> PMuxTree sym (ArrayEntry sym ctx tp)
 -> IO (PMuxTree sym (ArrayEntry sym ctx tp)))
-> Intervals AbsIntervalEnd ctx
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
-> IO
     (IntervalsMap
        AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp)))
forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) tp.
(Monad m, OrdF f) =>
(tp -> tp -> m tp)
-> Intervals f ctx
-> tp
-> IntervalsMap f ctx tp
-> m (IntervalsMap f ctx tp)
IM.insertWithM (sym
-> (SymIndex sym ctx -> IO (Pred sym))
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> (SymIndex sym ctx -> IO (Pred sym))
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
mergeEntriesMux sym
sym (sym -> SymRange sym ctx -> SymIndex sym ctx -> IO (Pred sym)
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymRange sym ctx -> SymIndex sym ctx -> IO (Pred sym)
isInRange sym
sym SymRange sym ctx
rng)) (SymRange sym ctx -> Intervals AbsIntervalEnd ctx
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymRange sym ctx -> AbsIndex ctx
symRangeToAbs SymRange sym ctx
rng) (sym
-> ArrayEntry sym ctx tp -> PMuxTree sym (ArrayEntry sym ctx tp)
forall sym a. IsExprBuilder sym => sym -> a -> PMuxTree sym a
toPMuxTree sym
sym ArrayEntry sym ctx tp
entry)  (CachedArray sym ctx tp
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
arrMap CachedArray sym ctx tp
arr')
  CachedArray sym ctx tp -> IO (CachedArray sym ctx tp)
forall sym (idx :: Ctx BaseType) (tp :: BaseType).
CachedArray sym idx tp -> IO (CachedArray sym idx tp)
incNonce (CachedArray sym ctx tp -> IO (CachedArray sym ctx tp))
-> CachedArray sym ctx tp -> IO (CachedArray sym ctx tp)
forall a b. (a -> b) -> a -> b
$ CachedArray sym ctx tp
arr { arrMap = arr''}


writeSingle ::
  forall sym ctx tp.
  W4.IsSymExprBuilder sym =>
  sym ->
  Ctx.Assignment (W4.SymExpr sym) ctx ->
  W4.SymExpr sym  tp ->
  CachedArray sym ctx tp ->
  IO (CachedArray sym ctx tp)
writeSingle :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym tp
-> CachedArray sym ctx tp
-> IO (CachedArray sym ctx tp)
writeSingle sym
sym Assignment (SymExpr sym) ctx
symIdxExpr SymExpr sym tp
val CachedArray sym ctx tp
arr = CachedArray sym ctx tp -> forall a. (NonEmptyCtx ctx => a) -> a
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp -> forall a. (NonEmptyCtx ctx => a) -> a
arrConstraints CachedArray sym ctx tp
arr ((NonEmptyCtx ctx => IO (CachedArray sym ctx tp))
 -> IO (CachedArray sym ctx tp))
-> (NonEmptyCtx ctx => IO (CachedArray sym ctx tp))
-> IO (CachedArray sym ctx tp)
forall a b. (a -> b) -> a -> b
$ do
  CachedArray sym ctx tp
arr' <- sym
-> SymRange sym ctx
-> CachedArray sym ctx tp
-> IO (CachedArray sym ctx tp)
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymRange sym ctx
-> CachedArray sym ctx tp
-> IO (CachedArray sym ctx tp)
invalidateEntries sym
sym (SymIndex sym ctx -> SymRange sym ctx
forall sym (ctx :: Ctx BaseType).
SymIndex sym ctx -> SymRange sym ctx
SymRangeSingle SymIndex sym ctx
symIdx) CachedArray sym ctx tp
arr
  ArrayEntry sym ctx tp
entry <- sym
-> SymIndex sym ctx -> SymExpr sym tp -> IO (ArrayEntry sym ctx tp)
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymIndex sym ctx -> SymExpr sym tp -> IO (ArrayEntry sym ctx tp)
mkValEntry sym
sym SymIndex sym ctx
symIdx SymExpr sym tp
val

  IntervalsMap
  AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
arr'' <- (PMuxTree sym (ArrayEntry sym ctx tp)
 -> PMuxTree sym (ArrayEntry sym ctx tp)
 -> IO (PMuxTree sym (ArrayEntry sym ctx tp)))
-> Intervals AbsIntervalEnd ctx
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
-> IO
     (IntervalsMap
        AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp)))
forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) tp.
(Monad m, OrdF f) =>
(tp -> tp -> m tp)
-> Intervals f ctx
-> tp
-> IntervalsMap f ctx tp
-> m (IntervalsMap f ctx tp)
IM.insertWithM (sym
-> (SymIndex sym ctx -> IO (Pred sym))
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> (SymIndex sym ctx -> IO (Pred sym))
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
mergeEntriesMux sym
sym (sym -> SymIndex sym ctx -> SymIndex sym ctx -> IO (Pred sym)
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymIndex sym ctx -> SymIndex sym ctx -> IO (Pred sym)
isEqIndex sym
sym SymIndex sym ctx
symIdx)) (SymIndex sym ctx -> Intervals AbsIntervalEnd ctx
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymIndex sym ctx -> AbsIndex ctx
symIdxToAbs SymIndex sym ctx
symIdx) (sym
-> ArrayEntry sym ctx tp -> PMuxTree sym (ArrayEntry sym ctx tp)
forall sym a. IsExprBuilder sym => sym -> a -> PMuxTree sym a
toPMuxTree sym
sym ArrayEntry sym ctx tp
entry)  (CachedArray sym ctx tp
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
arrMap CachedArray sym ctx tp
arr')
  CachedArray sym ctx tp -> IO (CachedArray sym ctx tp)
forall sym (idx :: Ctx BaseType) (tp :: BaseType).
CachedArray sym idx tp -> IO (CachedArray sym idx tp)
incNonce (CachedArray sym ctx tp -> IO (CachedArray sym ctx tp))
-> CachedArray sym ctx tp -> IO (CachedArray sym ctx tp)
forall a b. (a -> b) -> a -> b
$ CachedArray sym ctx tp
arr { arrMap = arr'' }
  where
    symIdx :: SymIndex sym ctx
symIdx = Assignment (SymExpr sym) ctx -> SymIndex sym ctx
forall sym (ctx :: Ctx BaseType).
Assignment (SymExpr sym) ctx -> SymIndex sym ctx
mkSymIndex Assignment (SymExpr sym) ctx
symIdxExpr


readSingle ::
  forall sym idx tp.
  W4.IsSymExprBuilder sym =>
  sym ->
  Ctx.Assignment (W4.SymExpr sym) idx ->
  CachedArray sym idx tp ->
  IO (W4.SymExpr sym tp)
readSingle :: forall sym (idx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Assignment (SymExpr sym) idx
-> CachedArray sym idx tp
-> IO (SymExpr sym tp)
readSingle sym
sym Assignment (SymExpr sym) idx
symIdxExpr CachedArray sym idx tp
arr = sym
-> SymIndex sym idx
-> CachedArray sym idx tp
-> IO (SymExpr sym tp)
forall sym (idx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymIndex sym idx
-> CachedArray sym idx tp
-> IO (SymExpr sym tp)
readArrayBase sym
sym SymIndex sym idx
symIdx CachedArray sym idx tp
arr
  where
    symIdx :: SymIndex sym idx
symIdx = Assignment (SymExpr sym) idx
-> Maybe (AbsIndex idx) -> SymIndex sym idx
forall sym (ctx :: Ctx BaseType).
Assignment (SymExpr sym) ctx
-> Maybe (AbsIndex ctx) -> SymIndex sym ctx
SymIndex Assignment (SymExpr sym) idx
symIdxExpr Maybe (AbsIndex idx)
forall a. Maybe a
Nothing

readChunk ::
  forall sym ctx tp.
  NonEmptyCtx ctx =>
  W4.IsSymExprBuilder sym =>
  sym ->
  -- | base address to read from
  Ctx.Assignment (W4.SymExpr sym) ctx ->
  -- | size of read
  W4.SymExpr sym (CtxFirst ctx) ->
  CachedArray sym ctx tp ->
  IO (ArrayChunk sym (CtxFirst ctx) tp)
readChunk :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(NonEmptyCtx ctx, IsSymExprBuilder sym) =>
sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym (CtxFirst ctx)
-> CachedArray sym ctx tp
-> IO (ArrayChunk sym (CtxFirst ctx) tp)
readChunk sym
sym Assignment (SymExpr sym) ctx
loExpr SymExpr sym (CtxFirst ctx)
offExpr CachedArray sym ctx tp
arr | NonEmptyCtxRepr ctx
NonEmptyCtxRepr <- forall k (ctx :: Ctx k). NonEmptyCtx ctx => NonEmptyCtxRepr ctx
nonEmptyCtxRepr @_ @ctx = do
  SymRange sym ctx
rng <- sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym (CtxFirst ctx)
-> IO (SymRange sym ctx)
forall sym (ctx :: Ctx BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym (CtxFirst ctx)
-> IO (SymRange sym ctx)
mkSymRangeOff sym
sym Assignment (SymExpr sym) ctx
loExpr SymExpr sym (CtxFirst ctx)
offExpr
  let absIdx :: AbsIndex ctx
absIdx = SymRange sym ctx -> AbsIndex ctx
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymRange sym ctx -> AbsIndex ctx
symRangeToAbs SymRange sym ctx
rng
  -- offset the outgoing array so that its value at zero is the value at
  -- the base address
  ArrayChunk sym (CtxFirst (ctx '::> x)) tp
-> IO (ArrayChunk sym (CtxFirst (ctx '::> x)) tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArrayChunk sym (CtxFirst (ctx '::> x)) tp
 -> IO (ArrayChunk sym (CtxFirst (ctx '::> x)) tp))
-> ArrayChunk sym (CtxFirst (ctx '::> x)) tp
-> IO (ArrayChunk sym (CtxFirst (ctx '::> x)) tp)
forall a b. (a -> b) -> a -> b
$ (SymExpr sym (CtxFirst (ctx '::> x)) -> IO (SymExpr sym tp))
-> ArrayChunk sym (CtxFirst (ctx '::> x)) tp
forall sym (idx :: BaseType) (tp :: BaseType).
(SymExpr sym idx -> IO (SymExpr sym tp)) -> ArrayChunk sym idx tp
ArrayChunk ((SymExpr sym (CtxFirst (ctx '::> x)) -> IO (SymExpr sym tp))
 -> ArrayChunk sym (CtxFirst (ctx '::> x)) tp)
-> (SymExpr sym (CtxFirst (ctx '::> x)) -> IO (SymExpr sym tp))
-> ArrayChunk sym (CtxFirst (ctx '::> x)) tp
forall a b. (a -> b) -> a -> b
$ \SymExpr sym (CtxFirst (ctx '::> x))
idxExpr -> do
    let off :: SymOffset sym ctx
off = SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx
forall sym (ctx :: Ctx BaseType).
SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx
SymOffset SymExpr sym (CtxFirst ctx)
SymExpr sym (CtxFirst (ctx '::> x))
idxExpr
    SymIndex sym ctx
offsetIdx <- sym
-> SymIndex sym ctx -> SymOffset sym ctx -> IO (SymIndex sym ctx)
forall sym (ctx :: Ctx BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> SymIndex sym ctx -> SymOffset sym ctx -> IO (SymIndex sym ctx)
addSymOffset sym
sym (SymRange sym ctx -> SymIndex sym ctx
forall sym (ctx :: Ctx BaseType).
SymRange sym ctx -> SymIndex sym ctx
symRangeLo SymRange sym ctx
rng) SymOffset sym ctx
off
    sym
-> SymIndex sym ctx
-> CachedArray sym ctx tp
-> IO (SymExpr sym tp)
forall sym (idx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymIndex sym idx
-> CachedArray sym idx tp
-> IO (SymExpr sym tp)
readArrayBase sym
sym (SymIndex sym ctx
offsetIdx { symIdxAbs = Just absIdx}) CachedArray sym ctx tp
arr

chunkToArray ::
  forall sym idx tp.
  W4.IsSymExprBuilder sym =>
  sym ->
  W4.BaseTypeRepr idx ->
  ArrayChunk sym idx tp ->
  IO (W4.SymArray sym (Ctx.EmptyCtx Ctx.::> idx) tp)
chunkToArray :: forall sym (idx :: BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> BaseTypeRepr idx
-> ArrayChunk sym idx tp
-> IO (SymArray sym (EmptyCtx ::> idx) tp)
chunkToArray sym
sym BaseTypeRepr idx
repr ArrayChunk sym idx tp
chunk = do
  BoundVar sym idx
var <- sym -> SolverSymbol -> BaseTypeRepr idx -> IO (BoundVar sym idx)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
W4.freshBoundVar sym
sym SolverSymbol
W4.emptySymbol BaseTypeRepr idx
repr
  SymExpr sym tp
body <- ArrayChunk sym idx tp -> SymExpr sym idx -> IO (SymExpr sym tp)
forall sym (idx :: BaseType) (tp :: BaseType).
ArrayChunk sym idx tp -> SymExpr sym idx -> IO (SymExpr sym tp)
evalChunk ArrayChunk sym idx tp
chunk (sym -> BoundVar sym idx -> SymExpr sym idx
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
forall (tp :: BaseType). sym -> BoundVar sym tp -> SymExpr sym tp
W4.varExpr sym
sym BoundVar sym idx
var)
  SymFn sym (EmptyCtx ::> idx) tp
fn <- sym
-> SolverSymbol
-> Assignment (BoundVar sym) (EmptyCtx ::> idx)
-> SymExpr sym tp
-> UnfoldPolicy
-> IO (SymFn sym (EmptyCtx ::> idx) tp)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment (BoundVar sym) args
-> SymExpr sym ret
-> UnfoldPolicy
-> IO (SymFn sym args ret)
forall (args :: Ctx BaseType) (ret :: BaseType).
sym
-> SolverSymbol
-> Assignment (BoundVar sym) args
-> SymExpr sym ret
-> UnfoldPolicy
-> IO (SymFn sym args ret)
W4.definedFn sym
sym (String -> SolverSymbol
W4.safeSymbol String
"readRange") (Assignment (BoundVar sym) EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
Ctx.empty Assignment (BoundVar sym) EmptyCtx
-> BoundVar sym idx -> Assignment (BoundVar sym) (EmptyCtx ::> idx)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> BoundVar sym idx
var) SymExpr sym tp
body UnfoldPolicy
W4.AlwaysUnfold
  sym
-> SymFn sym (EmptyCtx ::> idx) tp
-> IO (SymArray sym (EmptyCtx ::> idx) tp)
forall sym (idx :: Ctx BaseType) (itp :: BaseType)
       (ret :: BaseType).
IsExprBuilder sym =>
sym
-> SymFn sym (idx ::> itp) ret
-> IO (SymArray sym (idx ::> itp) ret)
forall (idx :: Ctx BaseType) (itp :: BaseType) (ret :: BaseType).
sym
-> SymFn sym (idx ::> itp) ret
-> IO (SymArray sym (idx ::> itp) ret)
W4.arrayFromFn sym
sym SymFn sym (EmptyCtx ::> idx) tp
fn

arrayToChunk ::
  forall sym idx tp.
  W4.IsSymExprBuilder sym =>
  sym ->
  (W4.SymArray sym (Ctx.EmptyCtx Ctx.::> idx) tp) ->
  IO (ArrayChunk sym idx tp)
arrayToChunk :: forall sym (idx :: BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymArray sym (EmptyCtx ::> idx) tp -> IO (ArrayChunk sym idx tp)
arrayToChunk sym
sym SymArray sym (EmptyCtx ::> idx) tp
arr = sym
-> (SymExpr sym idx -> IO (SymExpr sym tp))
-> IO (ArrayChunk sym idx tp)
forall sym (idx :: BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> (SymExpr sym idx -> IO (SymExpr sym tp))
-> IO (ArrayChunk sym idx tp)
mkArrayChunk sym
sym ((SymExpr sym idx -> IO (SymExpr sym tp))
 -> IO (ArrayChunk sym idx tp))
-> (SymExpr sym idx -> IO (SymExpr sym tp))
-> IO (ArrayChunk sym idx tp)
forall a b. (a -> b) -> a -> b
$ \SymExpr sym idx
idx -> sym
-> SymArray sym (EmptyCtx ::> idx) tp
-> Assignment (SymExpr sym) (EmptyCtx ::> idx)
-> IO (SymExpr sym tp)
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> IO (SymExpr sym b)
forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> IO (SymExpr sym b)
W4.arrayLookup sym
sym SymArray sym (EmptyCtx ::> idx) tp
arr (Assignment (SymExpr sym) EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
Ctx.empty Assignment (SymExpr sym) EmptyCtx
-> SymExpr sym idx -> Assignment (SymExpr sym) (EmptyCtx ::> idx)
forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> SymExpr sym idx
idx)


muxArrays ::
  forall sym idx tp.
  W4.IsSymExprBuilder sym =>
  sym ->
  W4.Pred sym ->
  CachedArray sym idx tp ->
  CachedArray sym idx tp ->
  IO (CachedArray sym idx tp)
muxArrays :: forall sym (idx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Pred sym
-> CachedArray sym idx tp
-> CachedArray sym idx tp
-> IO (CachedArray sym idx tp)
muxArrays sym
sym Pred sym
p CachedArray sym idx tp
arr1 CachedArray sym idx tp
arr2 = case CachedArray sym idx tp
arr1 CachedArray sym idx tp -> CachedArray sym idx tp -> Bool
forall a. Eq a => a -> a -> Bool
== CachedArray sym idx tp
arr2 of
  Bool
True -> CachedArray sym idx tp -> IO (CachedArray sym idx tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CachedArray sym idx tp
arr1
  Bool
False -> CachedArray sym idx tp -> forall a. (NonEmptyCtx idx => a) -> a
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp -> forall a. (NonEmptyCtx ctx => a) -> a
arrConstraints CachedArray sym idx tp
arr1 ((NonEmptyCtx idx => IO (CachedArray sym idx tp))
 -> IO (CachedArray sym idx tp))
-> (NonEmptyCtx idx => IO (CachedArray sym idx tp))
-> IO (CachedArray sym idx tp)
forall a b. (a -> b) -> a -> b
$ do
    Pred sym
notp <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred sym
sym Pred sym
p
    IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
arr' <- (PMuxTree sym (ArrayEntry sym idx tp)
 -> IO (PMuxTree sym (ArrayEntry sym idx tp)))
-> (PMuxTree sym (ArrayEntry sym idx tp)
    -> IO (PMuxTree sym (ArrayEntry sym idx tp)))
-> (PMuxTree sym (ArrayEntry sym idx tp)
    -> PMuxTree sym (ArrayEntry sym idx tp)
    -> IO (PMuxTree sym (ArrayEntry sym idx tp)))
-> IntervalsMap
     AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
-> IntervalsMap
     AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
-> IO
     (IntervalsMap
        AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp)))
forall {k} (f :: k -> *) (m :: * -> *) a b c (ctx :: Ctx k).
(OrdF f, Monad m) =>
(a -> m c)
-> (b -> m c)
-> (a -> b -> m c)
-> IntervalsMap f ctx a
-> IntervalsMap f ctx b
-> m (IntervalsMap f ctx c)
IM.mergeWithM
              (sym
-> Pred sym
-> PMuxTree sym (ArrayEntry sym idx tp)
-> IO (PMuxTree sym (ArrayEntry sym idx tp))
forall sym a.
(IsExprBuilder sym, Ord a) =>
sym -> Pred sym -> PMuxTree sym a -> IO (PMuxTree sym a)
pmuxTreeAddCondition sym
sym Pred sym
p)
              (sym
-> Pred sym
-> PMuxTree sym (ArrayEntry sym idx tp)
-> IO (PMuxTree sym (ArrayEntry sym idx tp))
forall sym a.
(IsExprBuilder sym, Ord a) =>
sym -> Pred sym -> PMuxTree sym a -> IO (PMuxTree sym a)
pmuxTreeAddCondition sym
sym Pred sym
notp)
              (sym
-> Pred sym
-> PMuxTree sym (ArrayEntry sym idx tp)
-> PMuxTree sym (ArrayEntry sym idx tp)
-> IO (PMuxTree sym (ArrayEntry sym idx tp))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Pred sym
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
muxEntries sym
sym Pred sym
p)
              (CachedArray sym idx tp
-> IntervalsMap
     AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
arrMap CachedArray sym idx tp
arr1)
              (CachedArray sym idx tp
-> IntervalsMap
     AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
arrMap CachedArray sym idx tp
arr2)
    CachedArray sym idx tp -> IO (CachedArray sym idx tp)
forall sym (idx :: Ctx BaseType) (tp :: BaseType).
CachedArray sym idx tp -> IO (CachedArray sym idx tp)
incNonce (CachedArray sym idx tp -> IO (CachedArray sym idx tp))
-> CachedArray sym idx tp -> IO (CachedArray sym idx tp)
forall a b. (a -> b) -> a -> b
$ CachedArray sym idx tp
arr1 { arrMap = arr' }

-- | Initialize an array with symbolic contents at concrete locations
initArrayConcrete ::
  forall sym idx tp idx' tp'.
  W4.IsSymExprBuilder sym =>
  idx ~ (idx' Ctx.::> tp') =>
  sym ->
  W4.BaseTypeRepr tp ->
  [(Ctx.Assignment W4.ConcreteVal idx, W4.SymExpr sym tp)] ->
  IO (CachedArray sym idx tp)
initArrayConcrete :: forall sym (idx :: Ctx BaseType) (tp :: BaseType)
       (idx' :: Ctx BaseType) (tp' :: BaseType).
(IsSymExprBuilder sym, idx ~ (idx' ::> tp')) =>
sym
-> BaseTypeRepr tp
-> [(Assignment ConcreteVal idx, SymExpr sym tp)]
-> IO (CachedArray sym idx tp)
initArrayConcrete sym
sym BaseTypeRepr tp
repr [(Assignment ConcreteVal idx, SymExpr sym tp)]
m = do
  ArrayNonce
nonce <- IO ArrayNonce
freshArrayNonce
  IntervalsMap
  AbsIntervalEnd
  (idx' ::> tp')
  (PMuxTree sym (ArrayEntry sym idx tp))
im <- [(Intervals AbsIntervalEnd (idx' ::> tp'),
  PMuxTree sym (ArrayEntry sym idx tp))]
-> IntervalsMap
     AbsIntervalEnd
     (idx' ::> tp')
     (PMuxTree sym (ArrayEntry sym idx tp))
forall {k} (f :: k -> *) (ctx :: Ctx k) (a :: k) tp.
OrdF f =>
[(Intervals f (ctx ::> a), tp)] -> IntervalsMap f (ctx ::> a) tp
IM.fromList ([(Intervals AbsIntervalEnd (idx' ::> tp'),
   PMuxTree sym (ArrayEntry sym idx tp))]
 -> IntervalsMap
      AbsIntervalEnd
      (idx' ::> tp')
      (PMuxTree sym (ArrayEntry sym idx tp)))
-> IO
     [(Intervals AbsIntervalEnd (idx' ::> tp'),
       PMuxTree sym (ArrayEntry sym idx tp))]
-> IO
     (IntervalsMap
        AbsIntervalEnd
        (idx' ::> tp')
        (PMuxTree sym (ArrayEntry sym idx tp)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Assignment ConcreteVal (idx' ::> tp'), SymExpr sym tp)
 -> IO
      (Intervals AbsIntervalEnd (idx' ::> tp'),
       PMuxTree sym (ArrayEntry sym idx tp)))
-> [(Assignment ConcreteVal (idx' ::> tp'), SymExpr sym tp)]
-> IO
     [(Intervals AbsIntervalEnd (idx' ::> tp'),
       PMuxTree sym (ArrayEntry sym idx tp))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Assignment ConcreteVal idx, SymExpr sym tp)
-> IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
(Assignment ConcreteVal (idx' ::> tp'), SymExpr sym tp)
-> IO
     (Intervals AbsIntervalEnd (idx' ::> tp'),
      PMuxTree sym (ArrayEntry sym idx tp))
go [(Assignment ConcreteVal idx, SymExpr sym tp)]
[(Assignment ConcreteVal (idx' ::> tp'), SymExpr sym tp)]
m
  CachedArray sym idx tp -> IO (CachedArray sym idx tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CachedArray sym idx tp -> IO (CachedArray sym idx tp))
-> CachedArray sym idx tp -> IO (CachedArray sym idx tp)
forall a b. (a -> b) -> a -> b
$ IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
-> (forall a. (NonEmptyCtx idx => a) -> a)
-> BaseTypeRepr tp
-> ArrayNonce
-> CachedArray sym idx tp
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
IntervalsMap
  AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
-> (forall a. (NonEmptyCtx ctx => a) -> a)
-> BaseTypeRepr tp
-> ArrayNonce
-> CachedArray sym ctx tp
CachedArray IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
IntervalsMap
  AbsIntervalEnd
  (idx' ::> tp')
  (PMuxTree sym (ArrayEntry sym idx tp))
im (\NonEmptyCtx idx => a
x -> a
NonEmptyCtx idx => a
x) BaseTypeRepr tp
repr ArrayNonce
nonce
  where
    go ::
      (Ctx.Assignment W4.ConcreteVal idx, W4.SymExpr sym tp) ->
      IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
    go :: (Assignment ConcreteVal idx, SymExpr sym tp)
-> IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
go (Assignment ConcreteVal idx
cidx, SymExpr sym tp
v) = do
      SymIndex sym idx
symIdx <- sym -> Assignment ConcreteVal idx -> IO (SymIndex sym idx)
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> Assignment ConcreteVal ctx -> IO (SymIndex sym ctx)
concreteIdxToSym sym
sym Assignment ConcreteVal idx
cidx
      ArrayEntry sym idx tp
entry <- sym
-> SymIndex sym idx -> SymExpr sym tp -> IO (ArrayEntry sym idx tp)
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymIndex sym ctx -> SymExpr sym tp -> IO (ArrayEntry sym ctx tp)
mkValEntry sym
sym SymIndex sym idx
symIdx SymExpr sym tp
v
      (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
-> IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
 -> IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp)))
-> (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
-> IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
forall a b. (a -> b) -> a -> b
$ (SymIndex sym idx -> AbsIndex idx
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymIndex sym ctx -> AbsIndex ctx
symIdxToAbs SymIndex sym idx
symIdx, sym
-> ArrayEntry sym idx tp -> PMuxTree sym (ArrayEntry sym idx tp)
forall sym a. IsExprBuilder sym => sym -> a -> PMuxTree sym a
toPMuxTree sym
sym ArrayEntry sym idx tp
entry)

-- | Initialize an array with symbolic contents at symbolic locations
initArray ::
  forall sym idx tp idx' tp'.
  W4.IsSymExprBuilder sym =>
  idx ~ (idx' Ctx.::> tp') =>
  sym ->
  W4.BaseTypeRepr tp ->
  [(Ctx.Assignment (W4.SymExpr sym) idx, W4.SymExpr sym tp)] ->
  IO (CachedArray sym idx tp)
initArray :: forall sym (idx :: Ctx BaseType) (tp :: BaseType)
       (idx' :: Ctx BaseType) (tp' :: BaseType).
(IsSymExprBuilder sym, idx ~ (idx' ::> tp')) =>
sym
-> BaseTypeRepr tp
-> [(Assignment (SymExpr sym) idx, SymExpr sym tp)]
-> IO (CachedArray sym idx tp)
initArray sym
sym BaseTypeRepr tp
repr [(Assignment (SymExpr sym) idx, SymExpr sym tp)]
m = do
  ArrayNonce
nonce <- IO ArrayNonce
freshArrayNonce
  IntervalsMap
  AbsIntervalEnd
  (idx' ::> tp')
  (PMuxTree sym (ArrayEntry sym idx tp))
im <- [(Intervals AbsIntervalEnd (idx' ::> tp'),
  PMuxTree sym (ArrayEntry sym idx tp))]
-> IntervalsMap
     AbsIntervalEnd
     (idx' ::> tp')
     (PMuxTree sym (ArrayEntry sym idx tp))
forall {k} (f :: k -> *) (ctx :: Ctx k) (a :: k) tp.
OrdF f =>
[(Intervals f (ctx ::> a), tp)] -> IntervalsMap f (ctx ::> a) tp
IM.fromList ([(Intervals AbsIntervalEnd (idx' ::> tp'),
   PMuxTree sym (ArrayEntry sym idx tp))]
 -> IntervalsMap
      AbsIntervalEnd
      (idx' ::> tp')
      (PMuxTree sym (ArrayEntry sym idx tp)))
-> IO
     [(Intervals AbsIntervalEnd (idx' ::> tp'),
       PMuxTree sym (ArrayEntry sym idx tp))]
-> IO
     (IntervalsMap
        AbsIntervalEnd
        (idx' ::> tp')
        (PMuxTree sym (ArrayEntry sym idx tp)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Assignment (SymExpr sym) (idx' ::> tp'), SymExpr sym tp)
 -> IO
      (Intervals AbsIntervalEnd (idx' ::> tp'),
       PMuxTree sym (ArrayEntry sym idx tp)))
-> [(Assignment (SymExpr sym) (idx' ::> tp'), SymExpr sym tp)]
-> IO
     [(Intervals AbsIntervalEnd (idx' ::> tp'),
       PMuxTree sym (ArrayEntry sym idx tp))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Assignment (SymExpr sym) idx, SymExpr sym tp)
-> IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
(Assignment (SymExpr sym) (idx' ::> tp'), SymExpr sym tp)
-> IO
     (Intervals AbsIntervalEnd (idx' ::> tp'),
      PMuxTree sym (ArrayEntry sym idx tp))
go [(Assignment (SymExpr sym) idx, SymExpr sym tp)]
[(Assignment (SymExpr sym) (idx' ::> tp'), SymExpr sym tp)]
m
  CachedArray sym idx tp -> IO (CachedArray sym idx tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CachedArray sym idx tp -> IO (CachedArray sym idx tp))
-> CachedArray sym idx tp -> IO (CachedArray sym idx tp)
forall a b. (a -> b) -> a -> b
$ IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
-> (forall a. (NonEmptyCtx idx => a) -> a)
-> BaseTypeRepr tp
-> ArrayNonce
-> CachedArray sym idx tp
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
IntervalsMap
  AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
-> (forall a. (NonEmptyCtx ctx => a) -> a)
-> BaseTypeRepr tp
-> ArrayNonce
-> CachedArray sym ctx tp
CachedArray IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
IntervalsMap
  AbsIntervalEnd
  (idx' ::> tp')
  (PMuxTree sym (ArrayEntry sym idx tp))
im (\NonEmptyCtx idx => a
x -> a
NonEmptyCtx idx => a
x) BaseTypeRepr tp
repr ArrayNonce
nonce
  where
    go ::
      (Ctx.Assignment (W4.SymExpr sym) idx, W4.SymExpr sym tp) ->
      IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
    go :: (Assignment (SymExpr sym) idx, SymExpr sym tp)
-> IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
go (Assignment (SymExpr sym) idx
symIdxExpr, SymExpr sym tp
v) = do
      let
        symIdx :: SymIndex sym idx
symIdx = Assignment (SymExpr sym) idx
-> Maybe (AbsIndex idx) -> SymIndex sym idx
forall sym (ctx :: Ctx BaseType).
Assignment (SymExpr sym) ctx
-> Maybe (AbsIndex ctx) -> SymIndex sym ctx
SymIndex Assignment (SymExpr sym) idx
symIdxExpr Maybe (AbsIndex idx)
forall a. Maybe a
Nothing
      ArrayEntry sym idx tp
entry <- sym
-> SymIndex sym idx -> SymExpr sym tp -> IO (ArrayEntry sym idx tp)
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymIndex sym ctx -> SymExpr sym tp -> IO (ArrayEntry sym ctx tp)
mkValEntry sym
sym SymIndex sym idx
symIdx SymExpr sym tp
v
      (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
-> IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
 -> IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp)))
-> (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
-> IO (AbsIndex idx, PMuxTree sym (ArrayEntry sym idx tp))
forall a b. (a -> b) -> a -> b
$ (SymIndex sym idx -> AbsIndex idx
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymIndex sym ctx -> AbsIndex ctx
symIdxToAbs SymIndex sym idx
symIdx, sym
-> ArrayEntry sym idx tp -> PMuxTree sym (ArrayEntry sym idx tp)
forall sym a. IsExprBuilder sym => sym -> a -> PMuxTree sym a
toPMuxTree sym
sym ArrayEntry sym idx tp
entry)

---------------------------------------------------
-- Implementation

-- | A sentinel nonce that is refreshed every time the array is updated.
newtype ArrayNonce = ArrayNonce (PN.Nonce PN.GlobalNonceGenerator IO)

instance Eq ArrayNonce where
  (ArrayNonce Nonce GlobalNonceGenerator IO
i1) == :: ArrayNonce -> ArrayNonce -> Bool
== (ArrayNonce Nonce GlobalNonceGenerator IO
i2) | Just IO :~: IO
Refl <- Nonce GlobalNonceGenerator IO
-> Nonce GlobalNonceGenerator IO -> Maybe (IO :~: IO)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: * -> *) (b :: * -> *).
Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
testEquality Nonce GlobalNonceGenerator IO
i1 Nonce GlobalNonceGenerator IO
i2 = Bool
True
  ArrayNonce
_ == ArrayNonce
_ = Bool
False

instance Ord ArrayNonce where
  compare :: ArrayNonce -> ArrayNonce -> Ordering
compare (ArrayNonce Nonce GlobalNonceGenerator IO
i1) (ArrayNonce Nonce GlobalNonceGenerator IO
i2) = OrderingF IO IO -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (OrderingF IO IO -> Ordering) -> OrderingF IO IO -> Ordering
forall a b. (a -> b) -> a -> b
$ Nonce GlobalNonceGenerator IO
-> Nonce GlobalNonceGenerator IO -> OrderingF IO IO
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: * -> *) (y :: * -> *).
Nonce GlobalNonceGenerator x
-> Nonce GlobalNonceGenerator y -> OrderingF x y
compareF Nonce GlobalNonceGenerator IO
i1 Nonce GlobalNonceGenerator IO
i2

freshArrayNonce :: IO ArrayNonce
freshArrayNonce :: IO ArrayNonce
freshArrayNonce = Nonce GlobalNonceGenerator IO -> ArrayNonce
ArrayNonce (Nonce GlobalNonceGenerator IO -> ArrayNonce)
-> IO (Nonce GlobalNonceGenerator IO) -> IO ArrayNonce
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonceGenerator IO GlobalNonceGenerator
-> IO (Nonce GlobalNonceGenerator IO)
forall (m :: * -> *) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
PN.freshNonce NonceGenerator IO GlobalNonceGenerator
PN.globalNonceGenerator

-- | An array that supports reading from a stack of mixed concrete/symbolic writes efficiently.
--
-- The primary interface is intended to be 'readChunk' and 'writeChunk', which
-- allow writing contiguous subsequences of data to the array.
--
-- Note that the equality instances is based on a unique nonce (see
-- 'ArrayNonce') that is incremented each time the array is updated, and is thus
-- an identity test rather than a structural equality test.
data CachedArray sym (ctx :: Ctx.Ctx W4.BaseType) (tp :: W4.BaseType) where
  CachedArray ::
    {
      forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
arrMap :: IM.IntervalsMap AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
    , forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp -> forall a. (NonEmptyCtx ctx => a) -> a
arrConstraints :: forall a. (NonEmptyCtx ctx => a) -> a
    , forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp -> BaseTypeRepr tp
arrTypeRepr :: W4.BaseTypeRepr tp
    , forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp -> ArrayNonce
_arrNonce :: ArrayNonce
    } -> CachedArray sym ctx tp

instance Eq (CachedArray sym idx tp) where
  (CachedArray IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
_ forall a. (NonEmptyCtx idx => a) -> a
_ BaseTypeRepr tp
_ ArrayNonce
nonce1) == :: CachedArray sym idx tp -> CachedArray sym idx tp -> Bool
== (CachedArray IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
_ forall a. (NonEmptyCtx idx => a) -> a
_ BaseTypeRepr tp
_ ArrayNonce
nonce2) = ArrayNonce
nonce1 ArrayNonce -> ArrayNonce -> Bool
forall a. Eq a => a -> a -> Bool
== ArrayNonce
nonce2

incNonce ::
  CachedArray sym idx tp ->
  IO (CachedArray sym idx tp)
incNonce :: forall sym (idx :: Ctx BaseType) (tp :: BaseType).
CachedArray sym idx tp -> IO (CachedArray sym idx tp)
incNonce (CachedArray IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
am forall a. (NonEmptyCtx idx => a) -> a
ac BaseTypeRepr tp
tr ArrayNonce
_) = do
  ArrayNonce
nonce <- IO ArrayNonce
freshArrayNonce
  CachedArray sym idx tp -> IO (CachedArray sym idx tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CachedArray sym idx tp -> IO (CachedArray sym idx tp))
-> CachedArray sym idx tp -> IO (CachedArray sym idx tp)
forall a b. (a -> b) -> a -> b
$ IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
-> (forall a. (NonEmptyCtx idx => a) -> a)
-> BaseTypeRepr tp
-> ArrayNonce
-> CachedArray sym idx tp
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
IntervalsMap
  AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
-> (forall a. (NonEmptyCtx ctx => a) -> a)
-> BaseTypeRepr tp
-> ArrayNonce
-> CachedArray sym ctx tp
CachedArray IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
am (NonEmptyCtx idx => a) -> a
forall a. (NonEmptyCtx idx => a) -> a
ac BaseTypeRepr tp
tr ArrayNonce
nonce

-- | An array entry defines a set of possible values for a given
-- abstract domain. Entries may overlap, and so as an invariant we
-- preserve the fact that at each logical index, exactly one entry is valid
data ArrayEntry sym ctx tp where
  ArrayEntry ::
    { -- TODO: should we cache these results?
      forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp
-> SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
entryVals :: (SymIndex sym ctx -> IO (W4.PartExpr (W4.Pred sym) (W4.SymExpr sym tp)))
    , forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp -> ArrayNonce
entryNonce :: ArrayNonce
    } -> ArrayEntry sym ctx tp


incNonceEntry ::
  ArrayEntry sym ctx tp ->
  IO (ArrayEntry sym ctx tp)
incNonceEntry :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
incNonceEntry (ArrayEntry SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
vals ArrayNonce
_) = do
  ArrayNonce
nonce <- IO ArrayNonce
freshArrayNonce
  ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp))
-> ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
forall a b. (a -> b) -> a -> b
$ (SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp)))
-> ArrayNonce -> ArrayEntry sym ctx tp
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp)))
-> ArrayNonce -> ArrayEntry sym ctx tp
ArrayEntry SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
vals ArrayNonce
nonce

instance Eq (ArrayEntry sym ctx tp) where
  ArrayEntry sym ctx tp
e1 == :: ArrayEntry sym ctx tp -> ArrayEntry sym ctx tp -> Bool
== ArrayEntry sym ctx tp
e2 = ArrayEntry sym ctx tp -> ArrayNonce
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp -> ArrayNonce
entryNonce ArrayEntry sym ctx tp
e1 ArrayNonce -> ArrayNonce -> Bool
forall a. Eq a => a -> a -> Bool
== ArrayEntry sym ctx tp -> ArrayNonce
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp -> ArrayNonce
entryNonce ArrayEntry sym ctx tp
e2

instance Ord (ArrayEntry sym ctx tp) where
  compare :: ArrayEntry sym ctx tp -> ArrayEntry sym ctx tp -> Ordering
compare ArrayEntry sym ctx tp
e1 ArrayEntry sym ctx tp
e2 = ArrayNonce -> ArrayNonce -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (ArrayEntry sym ctx tp -> ArrayNonce
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp -> ArrayNonce
entryNonce ArrayEntry sym ctx tp
e1) (ArrayEntry sym ctx tp -> ArrayNonce
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp -> ArrayNonce
entryNonce ArrayEntry sym ctx tp
e2)

-- | A symbolic index into the array. It represents the index for a single array element,
-- although its value may be symbolic
data SymIndex sym ctx =
  SymIndex
    { -- | the symbolic index
      forall sym (ctx :: Ctx BaseType).
SymIndex sym ctx -> Assignment (SymExpr sym) ctx
_symIdxExpr :: Ctx.Assignment (W4.SymExpr sym) ctx
      -- | an optional override for the abstract domain of the index
    , forall sym (ctx :: Ctx BaseType).
SymIndex sym ctx -> Maybe (AbsIndex ctx)
symIdxAbs :: Maybe (AbsIndex ctx)
    }

deriving instance W4.IsSymExprBuilder sym => Eq (SymIndex sym ctx)
deriving instance W4.IsSymExprBuilder sym => Ord (SymIndex sym ctx)

-- | An offset is an index into the last element of the array index
-- A value range is always representable as a base + offset
newtype SymOffset sym ctx where
  SymOffset :: W4.SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx

newtype FirstIndex ctx where
  FirstIndex :: Ctx.Index ctx (CtxFirst ctx) -> FirstIndex ctx

skipFirst ::
  FirstIndex (ctx Ctx.::> tp1) -> FirstIndex (ctx Ctx.::> tp1 Ctx.::> tp2)
skipFirst :: forall {k} (ctx :: Ctx k) (tp1 :: k) (tp2 :: k).
FirstIndex (ctx ::> tp1) -> FirstIndex ((ctx ::> tp1) ::> tp2)
skipFirst (FirstIndex Index (ctx ::> tp1) (CtxFirst (ctx ::> tp1))
idx) = Index ((ctx ::> tp1) ::> tp2) (CtxFirst ((ctx ::> tp1) ::> tp2))
-> FirstIndex ((ctx ::> tp1) ::> tp2)
forall {k} (ctx :: Ctx k).
Index ctx (CtxFirst ctx) -> FirstIndex ctx
FirstIndex (Index (ctx ::> tp1) (CtxFirst (ctx ::> tp1))
-> Index ((ctx ::> tp1) ::> tp2) (CtxFirst (ctx ::> tp1))
forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
Ctx.skipIndex Index (ctx ::> tp1) (CtxFirst (ctx ::> tp1))
idx)

firstIndex ::
  forall ctx.
  NonEmptyCtx ctx =>
  Ctx.Size ctx ->
  FirstIndex ctx
firstIndex :: forall {k} (ctx :: Ctx k).
NonEmptyCtx ctx =>
Size ctx -> FirstIndex ctx
firstIndex Size ctx
sz | NonEmptyCtxRepr ctx
NonEmptyCtxRepr <- forall k (ctx :: Ctx k). NonEmptyCtx ctx => NonEmptyCtxRepr ctx
nonEmptyCtxRepr @_ @ctx =
  case Size ctx -> SizeView ctx
forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
Ctx.viewSize (Size (ctx '::> x) -> Size ctx
forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
Ctx.decSize Size ctx
Size (ctx '::> x)
sz) of
    SizeView ctx
Ctx.ZeroSize -> Index ctx (CtxFirst ctx) -> FirstIndex ctx
forall {k} (ctx :: Ctx k).
Index ctx (CtxFirst ctx) -> FirstIndex ctx
FirstIndex (Index ctx (CtxFirst ctx)
Index ('EmptyCtx '::> x) x
forall {k} (tp :: k). Index ('EmptyCtx '::> tp) tp
Ctx.baseIndex)
    Ctx.IncSize Size ctx1
_ -> FirstIndex (ctx1 '::> tp) -> FirstIndex ((ctx1 '::> tp) ::> x)
forall {k} (ctx :: Ctx k) (tp1 :: k) (tp2 :: k).
FirstIndex (ctx ::> tp1) -> FirstIndex ((ctx ::> tp1) ::> tp2)
skipFirst (Size (ctx1 '::> tp) -> FirstIndex (ctx1 '::> tp)
forall {k} (ctx :: Ctx k).
NonEmptyCtx ctx =>
Size ctx -> FirstIndex ctx
firstIndex (Size ((ctx1 '::> tp) ::> x) -> Size (ctx1 '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
Ctx.decSize Size ctx
Size ((ctx1 '::> tp) ::> x)
sz))

indexToOffset ::
  forall sym ctx.
  NonEmptyCtx ctx =>
  W4.IsSymExprBuilder sym =>
  SymIndex sym ctx ->
  SymOffset sym ctx
indexToOffset :: forall sym (ctx :: Ctx BaseType).
(NonEmptyCtx ctx, IsSymExprBuilder sym) =>
SymIndex sym ctx -> SymOffset sym ctx
indexToOffset (SymIndex Assignment (SymExpr sym) ctx
eCtx Maybe (AbsIndex ctx)
_) =
  let
    FirstIndex Index ctx (CtxFirst ctx)
idx = Size ctx -> FirstIndex ctx
forall {k} (ctx :: Ctx k).
NonEmptyCtx ctx =>
Size ctx -> FirstIndex ctx
firstIndex (Assignment (SymExpr sym) ctx -> Size ctx
forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment (SymExpr sym) ctx
eCtx)
    e :: SymExpr sym (CtxFirst ctx)
e = Assignment (SymExpr sym) ctx
eCtx Assignment (SymExpr sym) ctx
-> Index ctx (CtxFirst ctx) -> SymExpr sym (CtxFirst ctx)
forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx (CtxFirst ctx)
idx
  in SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx
forall sym (ctx :: Ctx BaseType).
SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx
SymOffset SymExpr sym (CtxFirst ctx)
e

addSymOffset ::
  forall sym ctx.
  W4.IsSymExprBuilder sym =>
  NonEmptyCtx ctx =>
  sym ->
  SymIndex sym ctx ->
  SymOffset sym ctx ->
  IO (SymIndex sym ctx)
addSymOffset :: forall sym (ctx :: Ctx BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> SymIndex sym ctx -> SymOffset sym ctx -> IO (SymIndex sym ctx)
addSymOffset sym
sym (SymIndex Assignment (SymExpr sym) ctx
eCtx Maybe (AbsIndex ctx)
_) (SymOffset SymExpr sym (CtxFirst ctx)
off) = do
  let
    FirstIndex Index ctx (CtxFirst ctx)
idx = Size ctx -> FirstIndex ctx
forall {k} (ctx :: Ctx k).
NonEmptyCtx ctx =>
Size ctx -> FirstIndex ctx
firstIndex (Assignment (SymExpr sym) ctx -> Size ctx
forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment (SymExpr sym) ctx
eCtx)
    e :: SymExpr sym (CtxFirst ctx)
e = Assignment (SymExpr sym) ctx
eCtx Assignment (SymExpr sym) ctx
-> Index ctx (CtxFirst ctx) -> SymExpr sym (CtxFirst ctx)
forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx (CtxFirst ctx)
idx
  IxValueF (Assignment (SymExpr sym) ctx) (CtxFirst ctx)
e' <- case SymExpr sym (CtxFirst ctx) -> BaseTypeRepr (CtxFirst ctx)
forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym (CtxFirst ctx)
off of
    BaseTypeRepr (CtxFirst ctx)
W4.BaseIntegerRepr -> sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intAdd sym
sym SymInteger sym
SymExpr sym (CtxFirst ctx)
e SymInteger sym
SymExpr sym (CtxFirst ctx)
off
    W4.BaseBVRepr NatRepr w
_ -> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvAdd sym
sym SymBV sym w
SymExpr sym (CtxFirst ctx)
e SymBV sym w
SymExpr sym (CtxFirst ctx)
off
    BaseTypeRepr (CtxFirst ctx)
_ -> String
-> IO (IxValueF (Assignment (SymExpr sym) ctx) (CtxFirst ctx))
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
 -> IO (IxValueF (Assignment (SymExpr sym) ctx) (CtxFirst ctx)))
-> String
-> IO (IxValueF (Assignment (SymExpr sym) ctx) (CtxFirst ctx))
forall a b. (a -> b) -> a -> b
$ String
"Unsupported type"
  SymIndex sym ctx -> IO (SymIndex sym ctx)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymIndex sym ctx -> IO (SymIndex sym ctx))
-> SymIndex sym ctx -> IO (SymIndex sym ctx)
forall a b. (a -> b) -> a -> b
$ Assignment (SymExpr sym) ctx
-> Maybe (AbsIndex ctx) -> SymIndex sym ctx
forall sym (ctx :: Ctx BaseType).
Assignment (SymExpr sym) ctx
-> Maybe (AbsIndex ctx) -> SymIndex sym ctx
SymIndex (Assignment (SymExpr sym) ctx
eCtx Assignment (SymExpr sym) ctx
-> (Assignment (SymExpr sym) ctx -> Assignment (SymExpr sym) ctx)
-> Assignment (SymExpr sym) ctx
forall a b. a -> (a -> b) -> b
& (IndexF (Assignment (SymExpr sym) ctx) (CtxFirst ctx)
-> Traversal'
     (Assignment (SymExpr sym) ctx)
     (IxValueF (Assignment (SymExpr sym) ctx) (CtxFirst ctx))
forall k m (x :: k).
IxedF k m =>
IndexF m x -> Traversal' m (IxValueF m x)
forall (x :: BaseType).
IndexF (Assignment (SymExpr sym) ctx) x
-> Traversal'
     (Assignment (SymExpr sym) ctx)
     (IxValueF (Assignment (SymExpr sym) ctx) x)
ixF IndexF (Assignment (SymExpr sym) ctx) (CtxFirst ctx)
Index ctx (CtxFirst ctx)
idx) ((IxValueF (Assignment (SymExpr sym) ctx) (CtxFirst ctx)
  -> Identity
       (IxValueF (Assignment (SymExpr sym) ctx) (CtxFirst ctx)))
 -> Assignment (SymExpr sym) ctx
 -> Identity (Assignment (SymExpr sym) ctx))
-> IxValueF (Assignment (SymExpr sym) ctx) (CtxFirst ctx)
-> Assignment (SymExpr sym) ctx
-> Assignment (SymExpr sym) ctx
forall s t a b. ASetter s t a b -> b -> s -> t
.~ IxValueF (Assignment (SymExpr sym) ctx) (CtxFirst ctx)
e') Maybe (AbsIndex ctx)
forall a. Maybe a
Nothing

negateSymOffset ::
  W4.IsSymExprBuilder sym =>
  sym ->
  SymOffset sym ctx ->
  IO (SymOffset sym ctx)
negateSymOffset :: forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymOffset sym ctx -> IO (SymOffset sym ctx)
negateSymOffset sym
sym (SymOffset SymExpr sym (CtxFirst ctx)
off) = do
  SymExpr sym (CtxFirst ctx)
e' <- case SymExpr sym (CtxFirst ctx) -> BaseTypeRepr (CtxFirst ctx)
forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym (CtxFirst ctx)
off of
    BaseTypeRepr (CtxFirst ctx)
W4.BaseIntegerRepr -> sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
W4.intNeg sym
sym SymInteger sym
SymExpr sym (CtxFirst ctx)
off
    W4.BaseBVRepr NatRepr w
_ -> sym -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W4.bvNeg sym
sym SymBV sym w
SymExpr sym (CtxFirst ctx)
off
    BaseTypeRepr (CtxFirst ctx)
_ -> String -> IO (SymExpr sym (CtxFirst ctx))
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO (SymExpr sym (CtxFirst ctx)))
-> String -> IO (SymExpr sym (CtxFirst ctx))
forall a b. (a -> b) -> a -> b
$ String
"Unsupported type"
  SymOffset sym ctx -> IO (SymOffset sym ctx)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymOffset sym ctx -> IO (SymOffset sym ctx))
-> SymOffset sym ctx -> IO (SymOffset sym ctx)
forall a b. (a -> b) -> a -> b
$ SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx
forall sym (ctx :: Ctx BaseType).
SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx
SymOffset SymExpr sym (CtxFirst ctx)
e'

-- | Previous offset from the given one, to create an exclusive upper bound
prevSymOffset ::
  W4.IsSymExprBuilder sym =>
  sym ->
  SymOffset sym ctx ->
  IO (SymOffset sym ctx)
prevSymOffset :: forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymOffset sym ctx -> IO (SymOffset sym ctx)
prevSymOffset sym
sym (SymOffset SymExpr sym (CtxFirst ctx)
off) = do
  SymExpr sym (CtxFirst ctx)
e' <- case SymExpr sym (CtxFirst ctx) -> BaseTypeRepr (CtxFirst ctx)
forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym (CtxFirst ctx)
off of
    BaseTypeRepr (CtxFirst ctx)
W4.BaseIntegerRepr -> do
      SymExpr sym 'BaseIntegerType
one <- sym -> Integer -> IO (SymExpr sym 'BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
sym Integer
1
      sym
-> SymExpr sym 'BaseIntegerType
-> SymExpr sym 'BaseIntegerType
-> IO (SymExpr sym 'BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
W4.intSub sym
sym SymExpr sym 'BaseIntegerType
SymExpr sym (CtxFirst ctx)
off SymExpr sym 'BaseIntegerType
one
    W4.BaseBVRepr NatRepr w
w -> do
      SymExpr sym ('BaseBVType w)
one <- sym -> NatRepr w -> BV w -> IO (SymExpr sym ('BaseBVType 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)
W4.bvLit sym
sym NatRepr w
w (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
1)
      sym
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W4.bvSub sym
sym SymExpr sym ('BaseBVType w)
SymExpr sym (CtxFirst ctx)
off SymExpr sym ('BaseBVType w)
one
    BaseTypeRepr (CtxFirst ctx)
_ -> String -> IO (SymExpr sym (CtxFirst ctx))
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO (SymExpr sym (CtxFirst ctx)))
-> String -> IO (SymExpr sym (CtxFirst ctx))
forall a b. (a -> b) -> a -> b
$ String
"Unsupported type"
  SymOffset sym ctx -> IO (SymOffset sym ctx)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymOffset sym ctx -> IO (SymOffset sym ctx))
-> SymOffset sym ctx -> IO (SymOffset sym ctx)
forall a b. (a -> b) -> a -> b
$ SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx
forall sym (ctx :: Ctx BaseType).
SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx
SymOffset SymExpr sym (CtxFirst ctx)
e'

subSymOffset ::
  W4.IsSymExprBuilder sym =>
  NonEmptyCtx ctx =>
  sym ->
  SymIndex sym ctx ->
  SymOffset sym ctx ->
  IO (SymIndex sym ctx)
subSymOffset :: forall sym (ctx :: Ctx BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> SymIndex sym ctx -> SymOffset sym ctx -> IO (SymIndex sym ctx)
subSymOffset sym
sym SymIndex sym ctx
idx SymOffset sym ctx
off = do
  SymOffset sym ctx
negoff <- sym -> SymOffset sym ctx -> IO (SymOffset sym ctx)
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymOffset sym ctx -> IO (SymOffset sym ctx)
negateSymOffset sym
sym SymOffset sym ctx
off
  sym
-> SymIndex sym ctx -> SymOffset sym ctx -> IO (SymIndex sym ctx)
forall sym (ctx :: Ctx BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> SymIndex sym ctx -> SymOffset sym ctx -> IO (SymIndex sym ctx)
addSymOffset sym
sym SymIndex sym ctx
idx SymOffset sym ctx
negoff

mkSymIndex ::
  forall sym ctx.
  Ctx.Assignment (W4.SymExpr sym) ctx ->
  SymIndex sym ctx
mkSymIndex :: forall sym (ctx :: Ctx BaseType).
Assignment (SymExpr sym) ctx -> SymIndex sym ctx
mkSymIndex Assignment (SymExpr sym) ctx
e = Assignment (SymExpr sym) ctx
-> Maybe (AbsIndex ctx) -> SymIndex sym ctx
forall sym (ctx :: Ctx BaseType).
Assignment (SymExpr sym) ctx
-> Maybe (AbsIndex ctx) -> SymIndex sym ctx
SymIndex Assignment (SymExpr sym) ctx
e Maybe (AbsIndex ctx)
forall a. Maybe a
Nothing

-- | Represents a symbolic range, where equality and ordering is defined on the
-- abstract domain of the underlying expression
data SymRange sym ctx =
    SymRangeSingle (SymIndex sym ctx)
  | SymRangeMulti (SymIndex sym ctx) (SymIndex sym ctx)

symRangeLo :: SymRange sym ctx -> SymIndex sym ctx
symRangeLo :: forall sym (ctx :: Ctx BaseType).
SymRange sym ctx -> SymIndex sym ctx
symRangeLo (SymRangeSingle SymIndex sym ctx
symIdx) = SymIndex sym ctx
symIdx
symRangeLo (SymRangeMulti SymIndex sym ctx
loIdx SymIndex sym ctx
_) = SymIndex sym ctx
loIdx


symRangeToAbs ::
  W4.IsSymExprBuilder sym =>
  SymRange sym ctx ->
  AbsIndex ctx
symRangeToAbs :: forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymRange sym ctx -> AbsIndex ctx
symRangeToAbs (SymRangeSingle SymIndex sym ctx
symIdx) = SymIndex sym ctx -> AbsIndex ctx
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymIndex sym ctx -> AbsIndex ctx
symIdxToAbs SymIndex sym ctx
symIdx
symRangeToAbs (SymRangeMulti SymIndex sym ctx
loIdx SymIndex sym ctx
hiIdx) =
  AbsIndex ctx -> AbsIndex ctx -> AbsIndex ctx
forall (ctx :: Ctx BaseType).
AbsIndex ctx -> AbsIndex ctx -> AbsIndex ctx
joinAbsIndex (SymIndex sym ctx -> AbsIndex ctx
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymIndex sym ctx -> AbsIndex ctx
symIdxToAbs SymIndex sym ctx
loIdx) (SymIndex sym ctx -> AbsIndex ctx
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymIndex sym ctx -> AbsIndex ctx
symIdxToAbs SymIndex sym ctx
hiIdx)


-- | Create a range that is exclusive of the given offset
-- i.e. 2 + 4 --> (2, 5)
mkSymRangeOff ::
  forall sym ctx .
  W4.IsSymExprBuilder sym =>
  NonEmptyCtx ctx =>
  sym ->
  Ctx.Assignment (W4.SymExpr sym) ctx ->
  W4.SymExpr sym (CtxFirst ctx) ->
  IO (SymRange sym ctx)
mkSymRangeOff :: forall sym (ctx :: Ctx BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> Assignment (SymExpr sym) ctx
-> SymExpr sym (CtxFirst ctx)
-> IO (SymRange sym ctx)
mkSymRangeOff sym
sym Assignment (SymExpr sym) ctx
loExpr SymExpr sym (CtxFirst ctx)
offExpr = do
  let
    lo :: SymIndex sym ctx
lo = forall sym (ctx :: Ctx BaseType).
Assignment (SymExpr sym) ctx -> SymIndex sym ctx
mkSymIndex @sym Assignment (SymExpr sym) ctx
loExpr
    off :: SymOffset sym ctx
off = SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx
forall sym (ctx :: Ctx BaseType).
SymExpr sym (CtxFirst ctx) -> SymOffset sym ctx
SymOffset SymExpr sym (CtxFirst ctx)
offExpr
  SymOffset sym ctx
offPrev <- sym -> SymOffset sym ctx -> IO (SymOffset sym ctx)
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymOffset sym ctx -> IO (SymOffset sym ctx)
prevSymOffset sym
sym SymOffset sym ctx
off
  SymIndex sym ctx
hi <- sym
-> SymIndex sym ctx -> SymOffset sym ctx -> IO (SymIndex sym ctx)
forall sym (ctx :: Ctx BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> SymIndex sym ctx -> SymOffset sym ctx -> IO (SymIndex sym ctx)
addSymOffset sym
sym SymIndex sym ctx
lo SymOffset sym ctx
offPrev
  SymRange sym ctx -> IO (SymRange sym ctx)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymRange sym ctx -> IO (SymRange sym ctx))
-> SymRange sym ctx -> IO (SymRange sym ctx)
forall a b. (a -> b) -> a -> b
$ (SymIndex sym ctx -> SymIndex sym ctx -> SymRange sym ctx
forall sym (ctx :: Ctx BaseType).
SymIndex sym ctx -> SymIndex sym ctx -> SymRange sym ctx
SymRangeMulti SymIndex sym ctx
lo SymIndex sym ctx
hi)

data NonEmptyCtxRepr (ctx :: Ctx.Ctx k) where
  NonEmptyCtxRepr :: NonEmptyCtxRepr (ctx Ctx.::> x)

type family CtxFirst (ctx :: Ctx.Ctx k) where
  CtxFirst (Ctx.EmptyCtx Ctx.::> a) = a
  CtxFirst (ctx Ctx.::> _) = CtxFirst ctx

class NonEmptyCtx (ctx :: Ctx.Ctx k) where
  type CtxHead ctx :: k
  type CtxTail ctx :: Ctx.Ctx k

  nonEmptyCtxRepr :: NonEmptyCtxRepr ctx

instance NonEmptyCtx (ctx Ctx.::> tp) where
  type CtxHead (ctx Ctx.::> tp) = tp
  type CtxTail (ctx Ctx.::> tp) = ctx
  nonEmptyCtxRepr :: NonEmptyCtxRepr (ctx ::> tp)
nonEmptyCtxRepr = NonEmptyCtxRepr (ctx ::> tp)
forall k (ctx :: Ctx k) (tp :: k). NonEmptyCtxRepr (ctx ::> tp)
NonEmptyCtxRepr

data AbsIntervalEnd tp where
  AbsIntervalEndInt :: W4.ValueBound Integer -> AbsIntervalEnd W4.BaseIntegerType
  AbsIntervalEndBV :: (1 <= w) => W4.NatRepr w -> W4.ValueBound Integer -> AbsIntervalEnd (W4.BaseBVType w)

instance Ord (AbsIntervalEnd tp) where
  compare :: AbsIntervalEnd tp -> AbsIntervalEnd tp -> Ordering
compare AbsIntervalEnd tp
a1 AbsIntervalEnd tp
a2 = OrderingF tp tp -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (OrderingF tp tp -> Ordering) -> OrderingF tp tp -> Ordering
forall a b. (a -> b) -> a -> b
$ AbsIntervalEnd tp -> AbsIntervalEnd tp -> OrderingF tp tp
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: BaseType) (y :: BaseType).
AbsIntervalEnd x -> AbsIntervalEnd y -> OrderingF x y
compareF AbsIntervalEnd tp
a1 AbsIntervalEnd tp
a2

instance Eq (AbsIntervalEnd tp) where
  AbsIntervalEnd tp
a1 == :: AbsIntervalEnd tp -> AbsIntervalEnd tp -> Bool
== AbsIntervalEnd tp
a2 = (AbsIntervalEnd tp -> AbsIntervalEnd tp -> Ordering
forall a. Ord a => a -> a -> Ordering
compare AbsIntervalEnd tp
a1 AbsIntervalEnd tp
a2) Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance TestEquality AbsIntervalEnd where
  testEquality :: forall (a :: BaseType) (b :: BaseType).
AbsIntervalEnd a -> AbsIntervalEnd b -> Maybe (a :~: b)
testEquality AbsIntervalEnd a
a1 AbsIntervalEnd b
a2 = case AbsIntervalEnd a -> AbsIntervalEnd b -> OrderingF a b
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: BaseType) (y :: BaseType).
AbsIntervalEnd x -> AbsIntervalEnd y -> OrderingF x y
compareF AbsIntervalEnd a
a1 AbsIntervalEnd b
a2 of
    OrderingF a b
EQF -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    OrderingF a b
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing

instance OrdF AbsIntervalEnd where
  compareF :: forall (x :: BaseType) (y :: BaseType).
AbsIntervalEnd x -> AbsIntervalEnd y -> OrderingF x y
compareF AbsIntervalEnd x
a1 AbsIntervalEnd y
a2 = case (AbsIntervalEnd x
a1, AbsIntervalEnd y
a2) of
    (AbsIntervalEndInt ValueBound Integer
n1, AbsIntervalEndInt ValueBound Integer
n2) -> Ordering -> OrderingF x x
forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (Ordering -> OrderingF x x) -> Ordering -> OrderingF x x
forall a b. (a -> b) -> a -> b
$ ValueBound Integer -> ValueBound Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ValueBound Integer
n1 ValueBound Integer
n2
    (AbsIntervalEndBV NatRepr w
w1 ValueBound Integer
i1, AbsIntervalEndBV NatRepr w
w2 ValueBound Integer
i2) ->
      NatRepr w
-> NatRepr w -> ((w ~ w) => OrderingF x y) -> OrderingF x y
forall j k (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k).
OrdF f =>
f a -> f b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
lexCompareF NatRepr w
w1 NatRepr w
w2 (((w ~ w) => OrderingF x y) -> OrderingF x y)
-> ((w ~ w) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$ Ordering -> OrderingF x x
forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (Ordering -> OrderingF x x) -> Ordering -> OrderingF x x
forall a b. (a -> b) -> a -> b
$ ValueBound Integer -> ValueBound Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ValueBound Integer
i1 ValueBound Integer
i2
    (AbsIntervalEndInt{}, AbsIntervalEndBV{}) -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
    (AbsIntervalEndBV{}, AbsIntervalEndInt{}) -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF


type AbsIndex (idx :: Ctx.Ctx W4.BaseType) = IM.Intervals AbsIntervalEnd idx
type AbsInterval tp = IM.IntervalF AbsIntervalEnd tp


bvDomainRange ::
  1 <= w =>
  W4.NatRepr w ->
  BVD.BVDomain w ->
  AbsInterval (W4.BaseBVType w)
bvDomainRange :: forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BVDomain w -> AbsInterval (BaseBVType w)
bvDomainRange NatRepr w
w BVDomain w
d = case BVDomain w -> (Integer, Integer)
forall (w :: Natural). BVDomain w -> (Integer, Integer)
BVD.ubounds BVDomain w
d of
  (Integer
i1, Integer
i2) -> Interval (AbsIntervalEnd (BaseBVType w))
-> AbsInterval (BaseBVType w)
forall {k} (f :: k -> *) (tp :: k).
Interval (f tp) -> IntervalF f tp
IM.mkIntervalF (Interval (AbsIntervalEnd (BaseBVType w))
 -> AbsInterval (BaseBVType w))
-> Interval (AbsIntervalEnd (BaseBVType w))
-> AbsInterval (BaseBVType w)
forall a b. (a -> b) -> a -> b
$ AbsIntervalEnd (BaseBVType w)
-> AbsIntervalEnd (BaseBVType w)
-> Interval (AbsIntervalEnd (BaseBVType w))
forall a. a -> a -> Interval a
IM.ClosedInterval (NatRepr w -> ValueBound Integer -> AbsIntervalEnd (BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> ValueBound Integer -> AbsIntervalEnd (BaseBVType w)
AbsIntervalEndBV NatRepr w
w (Integer -> ValueBound Integer
forall tp. tp -> ValueBound tp
W4.Inclusive Integer
i1)) (NatRepr w -> ValueBound Integer -> AbsIntervalEnd (BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> ValueBound Integer -> AbsIntervalEnd (BaseBVType w)
AbsIntervalEndBV NatRepr w
w (Integer -> ValueBound Integer
forall tp. tp -> ValueBound tp
W4.Inclusive Integer
i2))

exprToAbsInterval ::
  forall sym tp.
  W4.IsSymExprBuilder sym =>
  W4.SymExpr sym tp ->
  AbsInterval tp
exprToAbsInterval :: forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
SymExpr sym tp -> AbsInterval tp
exprToAbsInterval SymExpr sym tp
e = BaseTypeRepr tp -> AbstractValue tp -> AbsInterval tp
forall (tp :: BaseType).
BaseTypeRepr tp -> AbstractValue tp -> AbsInterval tp
absToInterval (SymExpr sym tp -> BaseTypeRepr tp
forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym tp
e) (SymExpr sym tp -> AbstractValue tp
forall (tp :: BaseType). SymExpr sym tp -> AbstractValue tp
forall (f :: BaseType -> *) (tp :: BaseType).
HasAbsValue f =>
f tp -> AbstractValue tp
W4.getAbsValue SymExpr sym tp
e)

absToInterval ::
  W4.BaseTypeRepr tp ->
  W4.AbstractValue tp ->
  AbsInterval tp
absToInterval :: forall (tp :: BaseType).
BaseTypeRepr tp -> AbstractValue tp -> AbsInterval tp
absToInterval BaseTypeRepr tp
repr AbstractValue tp
v = case BaseTypeRepr tp
repr of
  BaseTypeRepr tp
W4.BaseIntegerRepr -> case AbstractValue tp
v of
    W4.SingleRange Integer
x -> Interval (AbsIntervalEnd tp) -> AbsInterval tp
forall {k} (f :: k -> *) (tp :: k).
Interval (f tp) -> IntervalF f tp
IM.mkIntervalF (Interval (AbsIntervalEnd tp) -> AbsInterval tp)
-> Interval (AbsIntervalEnd tp) -> AbsInterval tp
forall a b. (a -> b) -> a -> b
$ AbsIntervalEnd tp
-> AbsIntervalEnd tp -> Interval (AbsIntervalEnd tp)
forall a. a -> a -> Interval a
IM.ClosedInterval (ValueBound Integer -> AbsIntervalEnd 'BaseIntegerType
AbsIntervalEndInt (Integer -> ValueBound Integer
forall tp. tp -> ValueBound tp
W4.Inclusive Integer
x)) (ValueBound Integer -> AbsIntervalEnd 'BaseIntegerType
AbsIntervalEndInt (Integer -> ValueBound Integer
forall tp. tp -> ValueBound tp
W4.Inclusive Integer
x))
    W4.MultiRange ValueBound Integer
lo ValueBound Integer
hi -> Interval (AbsIntervalEnd tp) -> AbsInterval tp
forall {k} (f :: k -> *) (tp :: k).
Interval (f tp) -> IntervalF f tp
IM.mkIntervalF (Interval (AbsIntervalEnd tp) -> AbsInterval tp)
-> Interval (AbsIntervalEnd tp) -> AbsInterval tp
forall a b. (a -> b) -> a -> b
$ AbsIntervalEnd tp
-> AbsIntervalEnd tp -> Interval (AbsIntervalEnd tp)
forall a. a -> a -> Interval a
IM.ClosedInterval (ValueBound Integer -> AbsIntervalEnd 'BaseIntegerType
AbsIntervalEndInt ValueBound Integer
lo) (ValueBound Integer -> AbsIntervalEnd 'BaseIntegerType
AbsIntervalEndInt ValueBound Integer
hi)
  W4.BaseBVRepr NatRepr w
w -> NatRepr w -> BVDomain w -> AbsInterval ('BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BVDomain w -> AbsInterval (BaseBVType w)
bvDomainRange NatRepr w
w BVDomain w
AbstractValue tp
v
  BaseTypeRepr tp
_ -> String -> AbsInterval tp
forall a. HasCallStack => String -> a
error String
"Unsupported type"


readArrayBase ::
  forall sym idx tp.
  W4.IsSymExprBuilder sym =>
  sym ->
  SymIndex sym idx ->
  CachedArray sym idx tp ->
  IO (W4.SymExpr sym tp)
readArrayBase :: forall sym (idx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymIndex sym idx
-> CachedArray sym idx tp
-> IO (SymExpr sym tp)
readArrayBase sym
sym SymIndex sym idx
symIdx CachedArray sym idx tp
arr = do
  let
    intersecting :: [(Intervals AbsIntervalEnd idx,
  PMuxTree sym (ArrayEntry sym idx tp))]
intersecting = IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
-> [(Intervals AbsIntervalEnd idx,
     PMuxTree sym (ArrayEntry sym idx tp))]
forall {k} (f :: k -> *) (ctx :: Ctx k) tp.
IntervalsMap f ctx tp -> [(Intervals f ctx, tp)]
IM.toList (IntervalsMap
   AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
 -> [(Intervals AbsIntervalEnd idx,
      PMuxTree sym (ArrayEntry sym idx tp))])
-> IntervalsMap
     AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
-> [(Intervals AbsIntervalEnd idx,
     PMuxTree sym (ArrayEntry sym idx tp))]
forall a b. (a -> b) -> a -> b
$ IntervalsMap
  AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
-> Intervals AbsIntervalEnd idx
-> IntervalsMap
     AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
forall {k} (f :: k -> *) (ctx :: Ctx k) tp.
OrdF f =>
IntervalsMap f ctx tp -> Intervals f ctx -> IntervalsMap f ctx tp
IM.intersecting (CachedArray sym idx tp
-> IntervalsMap
     AbsIntervalEnd idx (PMuxTree sym (ArrayEntry sym idx tp))
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
arrMap CachedArray sym idx tp
arr) (SymIndex sym idx -> Intervals AbsIntervalEnd idx
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymIndex sym ctx -> AbsIndex ctx
symIdxToAbs SymIndex sym idx
symIdx)
  [(PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
  SymExpr sym BaseBoolType)]
entries <- ((ArrayEntry sym idx tp, SymExpr sym BaseBoolType)
 -> IO
      (PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
       SymExpr sym BaseBoolType))
-> [(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]
-> IO
     [(PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
       SymExpr sym BaseBoolType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ArrayEntry sym idx tp, SymExpr sym BaseBoolType)
-> IO
     (PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
      SymExpr sym BaseBoolType)
expandEntry ([(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]
 -> IO
      [(PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
        SymExpr sym BaseBoolType)])
-> [(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]
-> IO
     [(PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
       SymExpr sym BaseBoolType)]
forall a b. (a -> b) -> a -> b
$ [[(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]]
-> [(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]]
 -> [(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)])
-> [[(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]]
-> [(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]
forall a b. (a -> b) -> a -> b
$ ((Intervals AbsIntervalEnd idx,
  PMuxTree sym (ArrayEntry sym idx tp))
 -> [(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)])
-> [(Intervals AbsIntervalEnd idx,
     PMuxTree sym (ArrayEntry sym idx tp))]
-> [[(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]]
forall a b. (a -> b) -> [a] -> [b]
map (PMuxTree sym (ArrayEntry sym idx tp)
-> [(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]
forall sym a. PMuxTree sym a -> [(a, Pred sym)]
viewPMuxTree (PMuxTree sym (ArrayEntry sym idx tp)
 -> [(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)])
-> ((Intervals AbsIntervalEnd idx,
     PMuxTree sym (ArrayEntry sym idx tp))
    -> PMuxTree sym (ArrayEntry sym idx tp))
-> (Intervals AbsIntervalEnd idx,
    PMuxTree sym (ArrayEntry sym idx tp))
-> [(ArrayEntry sym idx tp, SymExpr sym BaseBoolType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Intervals AbsIntervalEnd idx,
 PMuxTree sym (ArrayEntry sym idx tp))
-> PMuxTree sym (ArrayEntry sym idx tp)
forall a b. (a, b) -> b
snd) [(Intervals AbsIntervalEnd idx,
  PMuxTree sym (ArrayEntry sym idx tp))]
intersecting
  case [(PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
  SymExpr sym BaseBoolType)]
entries of
    [(W4.PE SymExpr sym BaseBoolType
p (AsOrd SymExpr sym tp
e), SymExpr sym BaseBoolType
path_cond)]
      | Just Bool
True <- SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred SymExpr sym BaseBoolType
path_cond
      , Just Bool
True <- SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> *).
IsExpr e =>
e BaseBoolType -> Maybe Bool
W4.asConstantPred SymExpr sym BaseBoolType
p -> SymExpr sym tp -> IO (SymExpr sym tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr sym tp
e
    [(PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
  SymExpr sym BaseBoolType)]
entryExprs -> CachedArray sym idx tp -> forall a. (NonEmptyCtx idx => a) -> a
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp -> forall a. (NonEmptyCtx ctx => a) -> a
arrConstraints CachedArray sym idx tp
arr ((NonEmptyCtx idx => IO (SymExpr sym tp)) -> IO (SymExpr sym tp))
-> (NonEmptyCtx idx => IO (SymExpr sym tp)) -> IO (SymExpr sym tp)
forall a b. (a -> b) -> a -> b
$ do

      PMuxTree sym (AsOrd (SymExpr sym) tp)
muxTree <- sym
-> [(PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
     SymExpr sym BaseBoolType)]
-> IO (PMuxTree sym (AsOrd (SymExpr sym) tp))
forall sym a.
(IsExprBuilder sym, Ord a) =>
sym -> [(PartExpr (Pred sym) a, Pred sym)] -> IO (PMuxTree sym a)
mkPMuxTreePartial sym
sym [(PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
  SymExpr sym BaseBoolType)]
entryExprs
      sym
-> (SymExpr sym BaseBoolType
    -> Maybe (AsOrd (SymExpr sym) tp)
    -> Maybe (AsOrd (SymExpr sym) tp)
    -> IO (Maybe (AsOrd (SymExpr sym) tp)))
-> PMuxTree sym (AsOrd (SymExpr sym) tp)
-> IO (Maybe (AsOrd (SymExpr sym) tp))
forall sym a.
IsExprBuilder sym =>
sym -> (Pred sym -> a -> a -> IO a) -> MuxTree sym a -> IO a
MT.collapseMuxTree sym
sym SymExpr sym BaseBoolType
-> Maybe (AsOrd (SymExpr sym) tp)
-> Maybe (AsOrd (SymExpr sym) tp)
-> IO (Maybe (AsOrd (SymExpr sym) tp))
ite PMuxTree sym (AsOrd (SymExpr sym) tp)
muxTree IO (Maybe (AsOrd (SymExpr sym) tp))
-> (Maybe (AsOrd (SymExpr sym) tp) -> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (AsOrd SymExpr sym tp
e) -> SymExpr sym tp -> IO (SymExpr sym tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr sym tp
e
        -- garbage result
        Maybe (AsOrd (SymExpr sym) tp)
Nothing -> sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
W4.freshConstant sym
sym SolverSymbol
W4.emptySymbol (CachedArray sym idx tp -> BaseTypeRepr tp
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp -> BaseTypeRepr tp
arrTypeRepr CachedArray sym idx tp
arr)

  where
    ite ::
      W4.Pred sym ->
      Maybe (AsOrd (W4.SymExpr sym) tp) ->
      Maybe (AsOrd (W4.SymExpr sym) tp) ->
      IO (Maybe (AsOrd (W4.SymExpr sym) tp))
    ite :: SymExpr sym BaseBoolType
-> Maybe (AsOrd (SymExpr sym) tp)
-> Maybe (AsOrd (SymExpr sym) tp)
-> IO (Maybe (AsOrd (SymExpr sym) tp))
ite SymExpr sym BaseBoolType
p (Just (AsOrd SymExpr sym tp
e1)) (Just (AsOrd SymExpr sym tp
e2)) = (AsOrd (SymExpr sym) tp -> Maybe (AsOrd (SymExpr sym) tp)
forall a. a -> Maybe a
Just (AsOrd (SymExpr sym) tp -> Maybe (AsOrd (SymExpr sym) tp))
-> (SymExpr sym tp -> AsOrd (SymExpr sym) tp)
-> SymExpr sym tp
-> Maybe (AsOrd (SymExpr sym) tp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymExpr sym tp -> AsOrd (SymExpr sym) tp
forall {k} (f :: k -> *) (tp :: k). f tp -> AsOrd f tp
AsOrd) (SymExpr sym tp -> Maybe (AsOrd (SymExpr sym) tp))
-> IO (SymExpr sym tp) -> IO (Maybe (AsOrd (SymExpr sym) tp))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym BaseBoolType
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym
-> SymExpr sym BaseBoolType
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
W4.baseTypeIte sym
sym SymExpr sym BaseBoolType
p SymExpr sym tp
e1 SymExpr sym tp
e2
    ite SymExpr sym BaseBoolType
_ Maybe (AsOrd (SymExpr sym) tp)
Nothing (Just AsOrd (SymExpr sym) tp
e2) = Maybe (AsOrd (SymExpr sym) tp)
-> IO (Maybe (AsOrd (SymExpr sym) tp))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (AsOrd (SymExpr sym) tp)
 -> IO (Maybe (AsOrd (SymExpr sym) tp)))
-> Maybe (AsOrd (SymExpr sym) tp)
-> IO (Maybe (AsOrd (SymExpr sym) tp))
forall a b. (a -> b) -> a -> b
$ AsOrd (SymExpr sym) tp -> Maybe (AsOrd (SymExpr sym) tp)
forall a. a -> Maybe a
Just AsOrd (SymExpr sym) tp
e2
    ite SymExpr sym BaseBoolType
_ (Just AsOrd (SymExpr sym) tp
e1) Maybe (AsOrd (SymExpr sym) tp)
Nothing = Maybe (AsOrd (SymExpr sym) tp)
-> IO (Maybe (AsOrd (SymExpr sym) tp))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (AsOrd (SymExpr sym) tp)
 -> IO (Maybe (AsOrd (SymExpr sym) tp)))
-> Maybe (AsOrd (SymExpr sym) tp)
-> IO (Maybe (AsOrd (SymExpr sym) tp))
forall a b. (a -> b) -> a -> b
$ AsOrd (SymExpr sym) tp -> Maybe (AsOrd (SymExpr sym) tp)
forall a. a -> Maybe a
Just AsOrd (SymExpr sym) tp
e1
    ite SymExpr sym BaseBoolType
_ Maybe (AsOrd (SymExpr sym) tp)
Nothing Maybe (AsOrd (SymExpr sym) tp)
Nothing = Maybe (AsOrd (SymExpr sym) tp)
-> IO (Maybe (AsOrd (SymExpr sym) tp))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (AsOrd (SymExpr sym) tp)
forall a. Maybe a
Nothing

    expandEntry ::
      (ArrayEntry sym idx tp, W4.Pred sym) ->
      IO (W4.PartExpr (W4.Pred sym) (AsOrd (W4.SymExpr sym) tp), W4.Pred sym)
    expandEntry :: (ArrayEntry sym idx tp, SymExpr sym BaseBoolType)
-> IO
     (PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
      SymExpr sym BaseBoolType)
expandEntry (ArrayEntry sym idx tp
entry, SymExpr sym BaseBoolType
path_cond) = do
      PartialWithErr () (SymExpr sym BaseBoolType) (SymExpr sym tp)
val <- ArrayEntry sym idx tp
-> SymIndex sym idx
-> IO
     (PartialWithErr () (SymExpr sym BaseBoolType) (SymExpr sym tp))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp
-> SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
entryVals ArrayEntry sym idx tp
entry SymIndex sym idx
symIdx
      (PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
 SymExpr sym BaseBoolType)
-> IO
     (PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
      SymExpr sym BaseBoolType)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
  SymExpr sym BaseBoolType)
 -> IO
      (PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
       SymExpr sym BaseBoolType))
-> (PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
    SymExpr sym BaseBoolType)
-> IO
     (PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp),
      SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ ((SymExpr sym tp -> AsOrd (SymExpr sym) tp)
-> PartialWithErr () (SymExpr sym BaseBoolType) (SymExpr sym tp)
-> PartExpr (SymExpr sym BaseBoolType) (AsOrd (SymExpr sym) tp)
forall a b.
(a -> b)
-> PartialWithErr () (SymExpr sym BaseBoolType) a
-> PartialWithErr () (SymExpr sym BaseBoolType) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SymExpr sym tp -> AsOrd (SymExpr sym) tp
forall {k} (f :: k -> *) (tp :: k). f tp -> AsOrd f tp
AsOrd PartialWithErr () (SymExpr sym BaseBoolType) (SymExpr sym tp)
val, SymExpr sym BaseBoolType
path_cond)

mkValEntry ::
  W4.IsSymExprBuilder sym =>
  sym ->
  SymIndex sym ctx ->
  W4.SymExpr sym tp ->
  IO (ArrayEntry sym ctx tp)
mkValEntry :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymIndex sym ctx -> SymExpr sym tp -> IO (ArrayEntry sym ctx tp)
mkValEntry sym
sym SymIndex sym ctx
idx SymExpr sym tp
v = do
  let vals :: SymIndex sym ctx
-> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp))
vals SymIndex sym ctx
idx' = do
        SymExpr sym BaseBoolType
p <- sym
-> SymIndex sym ctx
-> SymIndex sym ctx
-> IO (SymExpr sym BaseBoolType)
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymIndex sym ctx -> SymIndex sym ctx -> IO (Pred sym)
isEqIndex sym
sym SymIndex sym ctx
idx SymIndex sym ctx
idx'
        PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp)
-> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp)
 -> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp)))
-> PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp)
-> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp))
forall a b. (a -> b) -> a -> b
$ SymExpr sym BaseBoolType
-> SymExpr sym tp
-> PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp)
forall (p :: BaseType -> *) a.
IsExpr p =>
p BaseBoolType -> a -> PartExpr (p BaseBoolType) a
W4.mkPE SymExpr sym BaseBoolType
p SymExpr sym tp
v
  (SymIndex sym ctx
 -> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp)))
-> IO (ArrayEntry sym ctx tp)
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp)))
-> IO (ArrayEntry sym ctx tp)
mkMultiEntry SymIndex sym ctx
-> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp))
vals

mkMultiEntry ::
  (SymIndex sym ctx -> IO (W4.PartExpr (W4.Pred sym) (W4.SymExpr sym tp))) ->
  IO (ArrayEntry sym ctx tp)
mkMultiEntry :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp)))
-> IO (ArrayEntry sym ctx tp)
mkMultiEntry SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
vals = do
  ArrayNonce
nonce <- IO ArrayNonce
freshArrayNonce
  ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp))
-> ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
forall a b. (a -> b) -> a -> b
$ (SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp)))
-> ArrayNonce -> ArrayEntry sym ctx tp
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp)))
-> ArrayNonce -> ArrayEntry sym ctx tp
ArrayEntry SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
vals ArrayNonce
nonce

symIdxToAbs ::
  forall sym ctx.
  W4.IsSymExprBuilder sym =>
  SymIndex sym ctx -> AbsIndex ctx
symIdxToAbs :: forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymIndex sym ctx -> AbsIndex ctx
symIdxToAbs (SymIndex Assignment (SymExpr sym) ctx
symIdxExpr Maybe (AbsIndex ctx)
Nothing) = Assignment (IntervalF AbsIntervalEnd) ctx -> AbsIndex ctx
forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment (IntervalF f) ctx -> Intervals f ctx
IM.Intervals (Assignment (IntervalF AbsIntervalEnd) ctx -> AbsIndex ctx)
-> Assignment (IntervalF AbsIntervalEnd) ctx -> AbsIndex ctx
forall a b. (a -> b) -> a -> b
$ (forall (x :: BaseType).
 SymExpr sym x -> IntervalF AbsIntervalEnd x)
-> forall (x :: Ctx BaseType).
   Assignment (SymExpr sym) x
   -> Assignment (IntervalF AbsIntervalEnd) x
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: BaseType -> *) (g :: BaseType -> *).
(forall (x :: BaseType). f x -> g x)
-> forall (x :: Ctx BaseType). Assignment f x -> Assignment g x
FC.fmapFC (forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
SymExpr sym tp -> AbsInterval tp
exprToAbsInterval @sym) Assignment (SymExpr sym) ctx
symIdxExpr
symIdxToAbs (SymIndex Assignment (SymExpr sym) ctx
_ (Just AbsIndex ctx
absIdx)) = AbsIndex ctx
absIdx

concreteIdxToSym ::
  forall sym ctx.
  W4.IsSymExprBuilder sym =>
  sym ->
  Ctx.Assignment W4.ConcreteVal ctx ->
  IO (SymIndex sym ctx)
concreteIdxToSym :: forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> Assignment ConcreteVal ctx -> IO (SymIndex sym ctx)
concreteIdxToSym sym
sym Assignment ConcreteVal ctx
conc = do
 Assignment (SymExpr sym) ctx
symIdxExpr <- (forall (x :: BaseType). ConcreteVal x -> IO (SymExpr sym x))
-> forall (x :: Ctx BaseType).
   Assignment ConcreteVal x -> IO (Assignment (SymExpr sym) x)
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
       (m :: * -> *).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: BaseType -> *) (g :: BaseType -> *) (m :: * -> *).
Applicative m =>
(forall (x :: BaseType). f x -> m (g x))
-> forall (x :: Ctx BaseType). Assignment f x -> m (Assignment g x)
FC.traverseFC (sym -> ConcreteVal x -> IO (SymExpr sym x)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> ConcreteVal tp -> IO (SymExpr sym tp)
W4.concreteToSym sym
sym) Assignment ConcreteVal ctx
conc
 SymIndex sym ctx -> IO (SymIndex sym ctx)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymIndex sym ctx -> IO (SymIndex sym ctx))
-> SymIndex sym ctx -> IO (SymIndex sym ctx)
forall a b. (a -> b) -> a -> b
$ Assignment (SymExpr sym) ctx
-> Maybe (AbsIndex ctx) -> SymIndex sym ctx
forall sym (ctx :: Ctx BaseType).
Assignment (SymExpr sym) ctx
-> Maybe (AbsIndex ctx) -> SymIndex sym ctx
SymIndex Assignment (SymExpr sym) ctx
symIdxExpr Maybe (AbsIndex ctx)
forall a. Maybe a
Nothing


-- | Invalidate all entries within the given range
-- TODO: delete entries which are statically invalid
invalidateRange ::
  forall sym ctx tp.
  W4.IsSymExprBuilder sym =>
  sym ->
  -- | range to invalidate
  SymRange sym ctx ->
  ArrayEntry sym ctx tp ->
  IO (Maybe (ArrayEntry sym ctx tp))
invalidateRange :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymRange sym ctx
-> ArrayEntry sym ctx tp
-> IO (Maybe (ArrayEntry sym ctx tp))
invalidateRange sym
sym SymRange sym ctx
invalid_rng ArrayEntry sym ctx tp
entry = do
  let vals :: SymIndex sym ctx
-> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp))
vals SymIndex sym ctx
symIdx' = do
        SymExpr sym BaseBoolType
notThis <- sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4.notPred sym
sym (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymRange sym ctx
-> SymIndex sym ctx
-> IO (SymExpr sym BaseBoolType)
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymRange sym ctx -> SymIndex sym ctx -> IO (Pred sym)
isInRange sym
sym SymRange sym ctx
invalid_rng SymIndex sym ctx
symIdx'
        PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp)
val <- ArrayEntry sym ctx tp
-> SymIndex sym ctx
-> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp
-> SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
entryVals ArrayEntry sym ctx tp
entry SymIndex sym ctx
symIdx'
        sym
-> SymExpr sym BaseBoolType
-> PartialT sym IO (SymExpr sym tp)
-> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp))
forall sym (m :: * -> *) a.
sym -> Pred sym -> PartialT sym m a -> m (PartExpr (Pred sym) a)
W4.runPartialT sym
sym SymExpr sym BaseBoolType
notThis (PartialT sym IO (SymExpr sym tp)
 -> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp)))
-> PartialT sym IO (SymExpr sym tp)
-> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp))
forall a b. (a -> b) -> a -> b
$ PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp)
-> PartialT sym IO (SymExpr sym tp)
forall sym (m :: * -> *) a.
(IsExprBuilder sym, MonadIO m) =>
PartExpr (Pred sym) a -> PartialT sym m a
W4.returnPartial PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp)
val
  ArrayEntry sym ctx tp
entry' <- ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
incNonceEntry (ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp))
-> ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
forall a b. (a -> b) -> a -> b
$ ArrayEntry sym ctx tp
entry { entryVals = vals }
  Maybe (ArrayEntry sym ctx tp) -> IO (Maybe (ArrayEntry sym ctx tp))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (ArrayEntry sym ctx tp)
 -> IO (Maybe (ArrayEntry sym ctx tp)))
-> Maybe (ArrayEntry sym ctx tp)
-> IO (Maybe (ArrayEntry sym ctx tp))
forall a b. (a -> b) -> a -> b
$ ArrayEntry sym ctx tp -> Maybe (ArrayEntry sym ctx tp)
forall a. a -> Maybe a
Just ArrayEntry sym ctx tp
entry'


isInRange ::
  forall sym ctx.
  W4.IsSymExprBuilder sym =>
  sym ->
  SymRange sym ctx ->
  SymIndex sym ctx ->
  IO (W4.Pred sym)
isInRange :: forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymRange sym ctx -> SymIndex sym ctx -> IO (Pred sym)
isInRange sym
sym SymRange sym ctx
rng symIdx2 :: SymIndex sym ctx
symIdx2@(SymIndex Assignment (SymExpr sym) ctx
symIdxExpr Maybe (AbsIndex ctx)
_) = case SymRange sym ctx
rng of
  SymRangeSingle SymIndex sym ctx
symIdx1 -> sym -> SymIndex sym ctx -> SymIndex sym ctx -> IO (Pred sym)
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymIndex sym ctx -> SymIndex sym ctx -> IO (Pred sym)
isEqIndex sym
sym SymIndex sym ctx
symIdx1 SymIndex sym ctx
symIdx2
  SymRangeMulti (SymIndex Assignment (SymExpr sym) ctx
loIdxExpr Maybe (AbsIndex ctx)
_) (SymIndex Assignment (SymExpr sym) ctx
hiIdxExpr Maybe (AbsIndex ctx)
_) -> do
    [Pred sym]
lo <- (forall (x :: BaseType). Const (Pred sym) x -> Pred sym)
-> forall (x :: Ctx BaseType).
   Assignment (Const (Pred sym)) x -> [Pred sym]
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: BaseType -> *) a.
(forall (x :: BaseType). f x -> a)
-> forall (x :: Ctx BaseType). Assignment f x -> [a]
FC.toListFC Const (Pred sym) x -> Pred sym
forall {k} a (b :: k). Const a b -> a
forall (x :: BaseType). Const (Pred sym) x -> Pred sym
getConst (Assignment (Const (Pred sym)) ctx -> [Pred sym])
-> IO (Assignment (Const (Pred sym)) ctx) -> IO [Pred sym]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: BaseType).
 SymExpr sym x -> SymExpr sym x -> IO (Const (Pred sym) x))
-> Assignment (SymExpr sym) ctx
-> Assignment (SymExpr sym) ctx
-> IO (Assignment (Const (Pred sym)) ctx)
forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Assignment f a -> Assignment g a -> m (Assignment h a)
Ctx.zipWithM SymExpr sym x -> SymExpr sym x -> IO (Const (Pred sym) x)
forall (x :: BaseType).
SymExpr sym x -> SymExpr sym x -> IO (Const (Pred sym) x)
doLe Assignment (SymExpr sym) ctx
loIdxExpr Assignment (SymExpr sym) ctx
symIdxExpr
    [Pred sym]
hi <- (forall (x :: BaseType). Const (Pred sym) x -> Pred sym)
-> forall (x :: Ctx BaseType).
   Assignment (Const (Pred sym)) x -> [Pred sym]
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: BaseType -> *) a.
(forall (x :: BaseType). f x -> a)
-> forall (x :: Ctx BaseType). Assignment f x -> [a]
FC.toListFC Const (Pred sym) x -> Pred sym
forall {k} a (b :: k). Const a b -> a
forall (x :: BaseType). Const (Pred sym) x -> Pred sym
getConst (Assignment (Const (Pred sym)) ctx -> [Pred sym])
-> IO (Assignment (Const (Pred sym)) ctx) -> IO [Pred sym]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: BaseType).
 SymExpr sym x -> SymExpr sym x -> IO (Const (Pred sym) x))
-> Assignment (SymExpr sym) ctx
-> Assignment (SymExpr sym) ctx
-> IO (Assignment (Const (Pred sym)) ctx)
forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Assignment f a -> Assignment g a -> m (Assignment h a)
Ctx.zipWithM SymExpr sym x -> SymExpr sym x -> IO (Const (Pred sym) x)
forall (x :: BaseType).
SymExpr sym x -> SymExpr sym x -> IO (Const (Pred sym) x)
doLe Assignment (SymExpr sym) ctx
symIdxExpr Assignment (SymExpr sym) ctx
hiIdxExpr
    (Pred sym -> Pred sym -> IO (Pred sym))
-> Pred sym -> [Pred sym] -> IO (Pred sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred sym
sym) (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred sym
sym) ([Pred sym] -> IO (Pred sym)) -> [Pred sym] -> IO (Pred sym)
forall a b. (a -> b) -> a -> b
$ [Pred sym]
lo [Pred sym] -> [Pred sym] -> [Pred sym]
forall a. [a] -> [a] -> [a]
++ [Pred sym]
hi
  where
    doLe ::
      forall tp.
      W4.SymExpr sym tp ->
      W4.SymExpr sym tp ->
      IO (Const (W4.Pred sym) tp)
    doLe :: forall (x :: BaseType).
SymExpr sym x -> SymExpr sym x -> IO (Const (Pred sym) x)
doLe SymExpr sym tp
e1 SymExpr sym tp
e2 = Pred sym -> Const (Pred sym) tp
forall {k} a (b :: k). a -> Const a b
Const (Pred sym -> Const (Pred sym) tp)
-> IO (Pred sym) -> IO (Const (Pred sym) tp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case SymExpr sym tp -> BaseTypeRepr tp
forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym tp
e1 of
      W4.BaseBVRepr NatRepr w
_ -> sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W4.bvUle sym
sym SymExpr sym tp
SymBV sym w
e1 SymExpr sym tp
SymBV sym w
e2
      BaseTypeRepr tp
W4.BaseIntegerRepr -> sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intLe sym
sym SymExpr sym tp
SymInteger sym
e1 SymExpr sym tp
SymInteger sym
e2
      BaseTypeRepr tp
_ -> String -> IO (Pred sym)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"isInRange: unsupported type"

isEqIndex ::
  forall sym ctx.
  W4.IsSymExprBuilder sym =>
  sym ->
  SymIndex sym ctx ->
  SymIndex sym ctx ->
  IO (W4.Pred sym)
isEqIndex :: forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
sym -> SymIndex sym ctx -> SymIndex sym ctx -> IO (Pred sym)
isEqIndex sym
sym (SymIndex Assignment (SymExpr sym) ctx
symIdxExpr1 Maybe (AbsIndex ctx)
_) (SymIndex Assignment (SymExpr sym) ctx
symIdxExpr2 Maybe (AbsIndex ctx)
_) = do
  [Pred sym]
preds <- (forall (x :: BaseType). Const (Pred sym) x -> Pred sym)
-> forall (x :: Ctx BaseType).
   Assignment (Const (Pred sym)) x -> [Pred sym]
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: BaseType -> *) a.
(forall (x :: BaseType). f x -> a)
-> forall (x :: Ctx BaseType). Assignment f x -> [a]
FC.toListFC Const (Pred sym) x -> Pred sym
forall {k} a (b :: k). Const a b -> a
forall (x :: BaseType). Const (Pred sym) x -> Pred sym
getConst (Assignment (Const (Pred sym)) ctx -> [Pred sym])
-> IO (Assignment (Const (Pred sym)) ctx) -> IO [Pred sym]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: BaseType).
 SymExpr sym x -> SymExpr sym x -> IO (Const (Pred sym) x))
-> Assignment (SymExpr sym) ctx
-> Assignment (SymExpr sym) ctx
-> IO (Assignment (Const (Pred sym)) ctx)
forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Assignment f a -> Assignment g a -> m (Assignment h a)
Ctx.zipWithM (\SymExpr sym x
e1 SymExpr sym x
e2 -> Pred sym -> Const (Pred sym) x
forall {k} a (b :: k). a -> Const a b
Const (Pred sym -> Const (Pred sym) x)
-> IO (Pred sym) -> IO (Const (Pred sym) x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymExpr sym x -> SymExpr sym x -> IO (Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
W4.isEq sym
sym SymExpr sym x
e1 SymExpr sym x
e2) Assignment (SymExpr sym) ctx
symIdxExpr1 Assignment (SymExpr sym) ctx
symIdxExpr2
  (Pred sym -> Pred sym -> IO (Pred sym))
-> Pred sym -> [Pred sym] -> IO (Pred sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred sym
sym) (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
W4.truePred sym
sym) [Pred sym]
preds

-- | Invalidate all existing symbolic entries at exactly this index
invalidateEntries ::
  forall sym ctx tp.
  W4.IsSymExprBuilder sym =>
  sym ->
  SymRange sym ctx ->
  CachedArray sym ctx tp ->
  IO (CachedArray sym ctx tp)
invalidateEntries :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymRange sym ctx
-> CachedArray sym ctx tp
-> IO (CachedArray sym ctx tp)
invalidateEntries sym
sym SymRange sym ctx
symRange CachedArray sym ctx tp
arr = CachedArray sym ctx tp -> forall a. (NonEmptyCtx ctx => a) -> a
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp -> forall a. (NonEmptyCtx ctx => a) -> a
arrConstraints CachedArray sym ctx tp
arr ((NonEmptyCtx ctx => IO (CachedArray sym ctx tp))
 -> IO (CachedArray sym ctx tp))
-> (NonEmptyCtx ctx => IO (CachedArray sym ctx tp))
-> IO (CachedArray sym ctx tp)
forall a b. (a -> b) -> a -> b
$ do
  NonEmptyCtxRepr ctx
NonEmptyCtxRepr <- NonEmptyCtxRepr ctx -> IO (NonEmptyCtxRepr ctx)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmptyCtxRepr ctx -> IO (NonEmptyCtxRepr ctx))
-> NonEmptyCtxRepr ctx -> IO (NonEmptyCtxRepr ctx)
forall a b. (a -> b) -> a -> b
$ forall k (ctx :: Ctx k). NonEmptyCtx ctx => NonEmptyCtxRepr ctx
nonEmptyCtxRepr @_ @ctx
  IntervalsMap
  AbsIntervalEnd (ctx ::> x) (PMuxTree sym (ArrayEntry sym ctx tp))
cmap <- Intervals AbsIntervalEnd (ctx ::> x)
-> (PMuxTree sym (ArrayEntry sym ctx tp)
    -> IO (Maybe (PMuxTree sym (ArrayEntry sym ctx tp))))
-> IntervalsMap
     AbsIntervalEnd (ctx ::> x) (PMuxTree sym (ArrayEntry sym ctx tp))
-> IO
     (IntervalsMap
        AbsIntervalEnd (ctx ::> x) (PMuxTree sym (ArrayEntry sym ctx tp)))
forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (a :: k) tp.
(Monad m, OrdF f) =>
Intervals f (ctx ::> a)
-> (tp -> m (Maybe tp))
-> IntervalsMap f (ctx ::> a) tp
-> m (IntervalsMap f (ctx ::> a) tp)
IM.mapMIntersecting AbsIndex ctx
Intervals AbsIntervalEnd (ctx ::> x)
absIndex (\PMuxTree sym (ArrayEntry sym ctx tp)
v -> PMuxTree sym (ArrayEntry sym ctx tp)
-> Maybe (PMuxTree sym (ArrayEntry sym ctx tp))
getMaybe (PMuxTree sym (ArrayEntry sym ctx tp)
 -> Maybe (PMuxTree sym (ArrayEntry sym ctx tp)))
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
-> IO (Maybe (PMuxTree sym (ArrayEntry sym ctx tp)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (ArrayEntry sym ctx tp -> IO (Maybe (ArrayEntry sym ctx tp)))
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
forall sym a b.
(IsExprBuilder sym, Ord a, Ord b) =>
sym -> (a -> IO (Maybe b)) -> PMuxTree sym a -> IO (PMuxTree sym b)
pmuxTreeMaybeOp sym
sym (sym
-> SymRange sym ctx
-> ArrayEntry sym ctx tp
-> IO (Maybe (ArrayEntry sym ctx tp))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymRange sym ctx
-> ArrayEntry sym ctx tp
-> IO (Maybe (ArrayEntry sym ctx tp))
invalidateRange sym
sym SymRange sym ctx
symRange) PMuxTree sym (ArrayEntry sym ctx tp)
v) (CachedArray sym (ctx ::> x) tp
-> IntervalsMap
     AbsIntervalEnd
     (ctx ::> x)
     (PMuxTree sym (ArrayEntry sym (ctx ::> x) tp))
forall (ctx :: Ctx BaseType) sym (tp :: BaseType).
CachedArray sym ctx tp
-> IntervalsMap
     AbsIntervalEnd ctx (PMuxTree sym (ArrayEntry sym ctx tp))
arrMap CachedArray sym ctx tp
CachedArray sym (ctx ::> x) tp
arr)
  CachedArray sym ctx tp -> IO (CachedArray sym ctx tp)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CachedArray sym ctx tp -> IO (CachedArray sym ctx tp))
-> CachedArray sym ctx tp -> IO (CachedArray sym ctx tp)
forall a b. (a -> b) -> a -> b
$ CachedArray sym ctx tp
arr { arrMap = cmap }
  where
    absIndex :: AbsIndex ctx
absIndex = SymRange sym ctx -> AbsIndex ctx
forall sym (ctx :: Ctx BaseType).
IsSymExprBuilder sym =>
SymRange sym ctx -> AbsIndex ctx
symRangeToAbs SymRange sym ctx
symRange
    getMaybe :: PMuxTree sym (ArrayEntry sym ctx tp) -> Maybe (PMuxTree sym (ArrayEntry sym ctx tp))
    getMaybe :: PMuxTree sym (ArrayEntry sym ctx tp)
-> Maybe (PMuxTree sym (ArrayEntry sym ctx tp))
getMaybe PMuxTree sym (ArrayEntry sym ctx tp)
mt | PMuxTree sym (ArrayEntry sym ctx tp) -> Bool
forall sym tp. PMuxTree sym tp -> Bool
isEmptyPMuxTree PMuxTree sym (ArrayEntry sym ctx tp)
mt = Maybe (PMuxTree sym (ArrayEntry sym ctx tp))
forall a. Maybe a
Nothing
    getMaybe PMuxTree sym (ArrayEntry sym ctx tp)
mt = PMuxTree sym (ArrayEntry sym ctx tp)
-> Maybe (PMuxTree sym (ArrayEntry sym ctx tp))
forall a. a -> Maybe a
Just PMuxTree sym (ArrayEntry sym ctx tp)
mt

buildMuxTree :: (W4.IsExprBuilder sym, Ord a) => sym -> a -> [(a, W4.Pred sym)] -> IO (MT.MuxTree sym a)
buildMuxTree :: forall sym a.
(IsExprBuilder sym, Ord a) =>
sym -> a -> [(a, Pred sym)] -> IO (MuxTree sym a)
buildMuxTree sym
sym a
a [(a, Pred sym)]
as =
  (MuxTree sym a -> (a, Pred sym) -> IO (MuxTree sym a))
-> MuxTree sym a -> [(a, Pred sym)] -> IO (MuxTree sym a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\MuxTree sym a
mt (a
a',Pred sym
p) -> sym
-> Pred sym -> MuxTree sym a -> MuxTree sym a -> IO (MuxTree sym a)
forall a sym.
(Ord a, IsExprBuilder sym) =>
sym
-> Pred sym -> MuxTree sym a -> MuxTree sym a -> IO (MuxTree sym a)
MT.mergeMuxTree sym
sym Pred sym
p (sym -> a -> MuxTree sym a
forall sym a. IsExprBuilder sym => sym -> a -> MuxTree sym a
MT.toMuxTree sym
sym a
a') MuxTree sym a
mt) (sym -> a -> MuxTree sym a
forall sym a. IsExprBuilder sym => sym -> a -> MuxTree sym a
MT.toMuxTree sym
sym a
a) [(a, Pred sym)]
as


joinAbsIndex ::
  AbsIndex ctx ->
  AbsIndex ctx ->
  AbsIndex ctx
joinAbsIndex :: forall (ctx :: Ctx BaseType).
AbsIndex ctx -> AbsIndex ctx -> AbsIndex ctx
joinAbsIndex (IM.Intervals Assignment (IntervalF AbsIntervalEnd) ctx
idx1) (IM.Intervals Assignment (IntervalF AbsIntervalEnd) ctx
idx2) = Assignment (IntervalF AbsIntervalEnd) ctx
-> Intervals AbsIntervalEnd ctx
forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment (IntervalF f) ctx -> Intervals f ctx
IM.Intervals (Assignment (IntervalF AbsIntervalEnd) ctx
 -> Intervals AbsIntervalEnd ctx)
-> Assignment (IntervalF AbsIntervalEnd) ctx
-> Intervals AbsIntervalEnd ctx
forall a b. (a -> b) -> a -> b
$ (forall (x :: BaseType).
 IntervalF AbsIntervalEnd x
 -> IntervalF AbsIntervalEnd x -> IntervalF AbsIntervalEnd x)
-> Assignment (IntervalF AbsIntervalEnd) ctx
-> Assignment (IntervalF AbsIntervalEnd) ctx
-> Assignment (IntervalF AbsIntervalEnd) ctx
forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith IntervalF AbsIntervalEnd x
-> IntervalF AbsIntervalEnd x -> IntervalF AbsIntervalEnd x
forall {k} (f :: k -> *) (a :: k).
OrdF f =>
IntervalF f a -> IntervalF f a -> IntervalF f a
forall (x :: BaseType).
IntervalF AbsIntervalEnd x
-> IntervalF AbsIntervalEnd x -> IntervalF AbsIntervalEnd x
IM.mergeIntervalsF Assignment (IntervalF AbsIntervalEnd) ctx
idx1 Assignment (IntervalF AbsIntervalEnd) ctx
idx2


muxEntries ::
  W4.IsSymExprBuilder sym =>
  sym ->
  W4.Pred sym ->
  PMuxTree sym (ArrayEntry sym ctx tp) ->
  PMuxTree sym (ArrayEntry sym ctx tp) ->
  IO (PMuxTree sym (ArrayEntry sym ctx tp))
muxEntries :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
IsSymExprBuilder sym =>
sym
-> Pred sym
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
muxEntries sym
sym Pred sym
p PMuxTree sym (ArrayEntry sym ctx tp)
mtT PMuxTree sym (ArrayEntry sym ctx tp)
mtF = sym
-> Pred sym
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
forall a sym.
(Ord a, IsExprBuilder sym) =>
sym
-> Pred sym -> MuxTree sym a -> MuxTree sym a -> IO (MuxTree sym a)
MT.mergeMuxTree sym
sym Pred sym
p PMuxTree sym (ArrayEntry sym ctx tp)
mtT PMuxTree sym (ArrayEntry sym ctx tp)
mtF

mergeEntries ::
  forall sym ctx tp.
  W4.IsSymExprBuilder sym =>
  NonEmptyCtx ctx =>
  sym ->
  (SymIndex sym ctx -> IO (W4.Pred sym)) ->
  ArrayEntry sym ctx tp ->
  ArrayEntry sym ctx tp ->
  IO (ArrayEntry sym ctx tp)
mergeEntries :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> (SymIndex sym ctx -> IO (Pred sym))
-> ArrayEntry sym ctx tp
-> ArrayEntry sym ctx tp
-> IO (ArrayEntry sym ctx tp)
mergeEntries sym
sym SymIndex sym ctx -> IO (Pred sym)
pickLeftFn ArrayEntry sym ctx tp
e1 ArrayEntry sym ctx tp
e2 = do
  let vals :: SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
vals SymIndex sym ctx
symIdx' = do
        Pred sym
pickLeft <- SymIndex sym ctx -> IO (Pred sym)
pickLeftFn SymIndex sym ctx
symIdx'
        PartExpr (Pred sym) (SymExpr sym tp)
val1 <- ArrayEntry sym ctx tp
-> SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp
-> SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
entryVals ArrayEntry sym ctx tp
e1 SymIndex sym ctx
symIdx'
        PartExpr (Pred sym) (SymExpr sym tp)
val2 <- ArrayEntry sym ctx tp
-> SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp
-> SymIndex sym ctx -> IO (PartExpr (Pred sym) (SymExpr sym tp))
entryVals ArrayEntry sym ctx tp
e2 SymIndex sym ctx
symIdx'
        sym
-> (Pred sym
    -> SymExpr sym tp
    -> SymExpr sym tp
    -> PartialT sym IO (SymExpr sym tp))
-> Pred sym
-> PartExpr (Pred sym) (SymExpr sym tp)
-> PartExpr (Pred sym) (SymExpr sym tp)
-> IO (PartExpr (Pred sym) (SymExpr sym tp))
forall sym (m :: * -> *) a.
(IsExprBuilder sym, MonadIO m) =>
sym
-> (Pred sym -> a -> a -> PartialT sym m a)
-> Pred sym
-> PartExpr (Pred sym) a
-> PartExpr (Pred sym) a
-> m (PartExpr (Pred sym) a)
W4.mergePartial sym
sym (\Pred sym
p SymExpr sym tp
a SymExpr sym tp
b -> IO (SymExpr sym tp) -> PartialT sym IO (SymExpr sym tp)
forall (m :: * -> *) a. Monad m => m a -> PartialT sym m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (SymExpr sym tp) -> PartialT sym IO (SymExpr sym tp))
-> IO (SymExpr sym tp) -> PartialT sym IO (SymExpr sym tp)
forall a b. (a -> b) -> a -> b
$ sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
W4.baseTypeIte sym
sym Pred sym
p SymExpr sym tp
a SymExpr sym tp
b)
          Pred sym
pickLeft PartExpr (Pred sym) (SymExpr sym tp)
val1 PartExpr (Pred sym) (SymExpr sym tp)
val2
  ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
incNonceEntry (ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp))
-> ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp)
forall a b. (a -> b) -> a -> b
$ ArrayEntry sym ctx tp
e1 { entryVals = vals }

mergeEntriesMux ::
  forall sym ctx tp.
  W4.IsSymExprBuilder sym =>
  NonEmptyCtx ctx =>
  sym ->
  (SymIndex sym ctx -> IO (W4.Pred sym)) ->
  PMuxTree sym (ArrayEntry sym ctx tp) ->
  PMuxTree sym (ArrayEntry sym ctx tp) ->
  IO (PMuxTree sym (ArrayEntry sym ctx tp))
mergeEntriesMux :: forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> (SymIndex sym ctx -> IO (Pred sym))
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
mergeEntriesMux sym
sym SymIndex sym ctx -> IO (Pred sym)
pickLeftFn = sym
-> (ArrayEntry sym ctx tp
    -> ArrayEntry sym ctx tp -> IO (ArrayEntry sym ctx tp))
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> PMuxTree sym (ArrayEntry sym ctx tp)
-> IO (PMuxTree sym (ArrayEntry sym ctx tp))
forall sym a b c.
(IsExprBuilder sym, Ord c) =>
sym
-> (a -> b -> IO c)
-> PMuxTree sym a
-> PMuxTree sym b
-> IO (PMuxTree sym c)
pmuxTreeBinOp sym
sym (sym
-> (SymIndex sym ctx -> IO (Pred sym))
-> ArrayEntry sym ctx tp
-> ArrayEntry sym ctx tp
-> IO (ArrayEntry sym ctx tp)
forall sym (ctx :: Ctx BaseType) (tp :: BaseType).
(IsSymExprBuilder sym, NonEmptyCtx ctx) =>
sym
-> (SymIndex sym ctx -> IO (Pred sym))
-> ArrayEntry sym ctx tp
-> ArrayEntry sym ctx tp
-> IO (ArrayEntry sym ctx tp)
mergeEntries sym
sym SymIndex sym ctx -> IO (Pred sym)
pickLeftFn)

-- | A partial mux tree
type PMuxTree sym tp = MT.MuxTree sym (Maybe tp)

viewPMuxTree :: forall sym a. PMuxTree sym a -> [(a, W4.Pred sym)]
viewPMuxTree :: forall sym a. PMuxTree sym a -> [(a, Pred sym)]
viewPMuxTree PMuxTree sym a
mt = ((Maybe a, SymExpr sym BaseBoolType)
 -> Maybe (a, SymExpr sym BaseBoolType))
-> [(Maybe a, SymExpr sym BaseBoolType)]
-> [(a, SymExpr sym BaseBoolType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe a, SymExpr sym BaseBoolType)
-> Maybe (a, SymExpr sym BaseBoolType)
go ([(Maybe a, SymExpr sym BaseBoolType)]
 -> [(a, SymExpr sym BaseBoolType)])
-> [(Maybe a, SymExpr sym BaseBoolType)]
-> [(a, SymExpr sym BaseBoolType)]
forall a b. (a -> b) -> a -> b
$ PMuxTree sym a -> [(Maybe a, SymExpr sym BaseBoolType)]
forall sym a. MuxTree sym a -> [(a, Pred sym)]
MT.viewMuxTree PMuxTree sym a
mt
  where
    go :: (Maybe a, W4.Pred sym) -> Maybe (a, W4.Pred sym)
    go :: (Maybe a, SymExpr sym BaseBoolType)
-> Maybe (a, SymExpr sym BaseBoolType)
go (Just a
a, SymExpr sym BaseBoolType
p) = (a, SymExpr sym BaseBoolType)
-> Maybe (a, SymExpr sym BaseBoolType)
forall a. a -> Maybe a
Just (a
a, SymExpr sym BaseBoolType
p)
    go (Maybe a, SymExpr sym BaseBoolType)
_ = Maybe (a, SymExpr sym BaseBoolType)
forall a. Maybe a
Nothing

isEmptyPMuxTree :: PMuxTree sym tp -> Bool
isEmptyPMuxTree :: forall sym tp. PMuxTree sym tp -> Bool
isEmptyPMuxTree PMuxTree sym tp
mt = case PMuxTree sym tp -> [(Maybe tp, Pred sym)]
forall sym a. MuxTree sym a -> [(a, Pred sym)]
MT.viewMuxTree PMuxTree sym tp
mt of
  [(Maybe tp
Nothing, Pred sym
_)] -> Bool
True
  [(Maybe tp, Pred sym)]
_ -> Bool
False

mkPMuxTree ::
  (W4.IsExprBuilder sym, Ord a) =>
  sym ->
  [(a, W4.Pred sym)] ->
  IO (PMuxTree sym a)
mkPMuxTree :: forall sym a.
(IsExprBuilder sym, Ord a) =>
sym -> [(a, Pred sym)] -> IO (PMuxTree sym a)
mkPMuxTree sym
sym [(a, Pred sym)]
ls = sym
-> Maybe a -> [(Maybe a, Pred sym)] -> IO (MuxTree sym (Maybe a))
forall sym a.
(IsExprBuilder sym, Ord a) =>
sym -> a -> [(a, Pred sym)] -> IO (MuxTree sym a)
buildMuxTree sym
sym Maybe a
forall a. Maybe a
Nothing (((a, Pred sym) -> (Maybe a, Pred sym))
-> [(a, Pred sym)] -> [(Maybe a, Pred sym)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
a, Pred sym
p) -> (a -> Maybe a
forall a. a -> Maybe a
Just a
a, Pred sym
p)) [(a, Pred sym)]
ls)

mkPMuxTreePartial ::
  forall sym a.
  (W4.IsExprBuilder sym, Ord a) =>
  sym ->
  [(W4.PartExpr (W4.Pred sym) a, W4.Pred sym)] ->
  IO (PMuxTree sym a)
mkPMuxTreePartial :: forall sym a.
(IsExprBuilder sym, Ord a) =>
sym -> [(PartExpr (Pred sym) a, Pred sym)] -> IO (PMuxTree sym a)
mkPMuxTreePartial sym
sym [(PartExpr (Pred sym) a, Pred sym)]
ls = sym -> [(a, Pred sym)] -> IO (MuxTree sym (Maybe a))
forall sym a.
(IsExprBuilder sym, Ord a) =>
sym -> [(a, Pred sym)] -> IO (PMuxTree sym a)
mkPMuxTree sym
sym ([(a, Pred sym)] -> IO (MuxTree sym (Maybe a)))
-> IO [(a, Pred sym)] -> IO (MuxTree sym (Maybe a))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([Maybe (a, Pred sym)] -> [(a, Pred sym)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (a, Pred sym)] -> [(a, Pred sym)])
-> IO [Maybe (a, Pred sym)] -> IO [(a, Pred sym)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((PartExpr (Pred sym) a, Pred sym) -> IO (Maybe (a, Pred sym)))
-> [(PartExpr (Pred sym) a, Pred sym)] -> IO [Maybe (a, Pred sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (PartExpr (Pred sym) a, Pred sym) -> IO (Maybe (a, Pred sym))
go [(PartExpr (Pred sym) a, Pred sym)]
ls)
  where
    go :: (W4.PartExpr (W4.Pred sym) a, W4.Pred sym) -> IO (Maybe (a, W4.Pred sym))
    go :: (PartExpr (Pred sym) a, Pred sym) -> IO (Maybe (a, Pred sym))
go (W4.PE Pred sym
p a
a, Pred sym
cond) = do
      Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred sym
sym Pred sym
p Pred sym
cond
      Maybe (a, Pred sym) -> IO (Maybe (a, Pred sym))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, Pred sym) -> IO (Maybe (a, Pred sym)))
-> Maybe (a, Pred sym) -> IO (Maybe (a, Pred sym))
forall a b. (a -> b) -> a -> b
$ (a, Pred sym) -> Maybe (a, Pred sym)
forall a. a -> Maybe a
Just (a
a, Pred sym
p')
    go (PartExpr (Pred sym) a
W4.Unassigned, Pred sym
_) = Maybe (a, Pred sym) -> IO (Maybe (a, Pred sym))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, Pred sym)
forall a. Maybe a
Nothing

pmuxTreeAddCondition ::
  forall sym a.
  W4.IsExprBuilder sym =>
  Ord a =>
  sym ->
  W4.Pred sym ->
  PMuxTree sym a ->
  IO (PMuxTree sym a)
pmuxTreeAddCondition :: forall sym a.
(IsExprBuilder sym, Ord a) =>
sym -> Pred sym -> PMuxTree sym a -> IO (PMuxTree sym a)
pmuxTreeAddCondition sym
sym Pred sym
cond PMuxTree sym a
mt = sym -> [(a, Pred sym)] -> IO (PMuxTree sym a)
forall sym a.
(IsExprBuilder sym, Ord a) =>
sym -> [(a, Pred sym)] -> IO (PMuxTree sym a)
mkPMuxTree sym
sym ([(a, Pred sym)] -> IO (PMuxTree sym a))
-> IO [(a, Pred sym)] -> IO (PMuxTree sym a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ((a, Pred sym) -> IO (a, Pred sym))
-> [(a, Pred sym)] -> IO [(a, Pred sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (a, Pred sym) -> IO (a, Pred sym)
addCond (PMuxTree sym a -> [(a, Pred sym)]
forall sym a. PMuxTree sym a -> [(a, Pred sym)]
viewPMuxTree PMuxTree sym a
mt)
  where
    addCond :: (a, W4.Pred sym) -> IO (a, W4.Pred sym)
    addCond :: (a, Pred sym) -> IO (a, Pred sym)
addCond (a
a, Pred sym
cond') = do
      Pred sym
cond'' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4.andPred sym
sym Pred sym
cond Pred sym
cond'
      (a, Pred sym) -> IO (a, Pred sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, Pred sym) -> IO (a, Pred sym))
-> (a, Pred sym) -> IO (a, Pred sym)
forall a b. (a -> b) -> a -> b
$ (a
a, Pred sym
cond'')


pmuxTreeMaybeOp ::
  (W4.IsExprBuilder sym, Ord a, Ord b) =>
  sym ->
  (a -> IO (Maybe b)) ->
  PMuxTree sym a ->
  IO (PMuxTree sym b)
pmuxTreeMaybeOp :: forall sym a b.
(IsExprBuilder sym, Ord a, Ord b) =>
sym -> (a -> IO (Maybe b)) -> PMuxTree sym a -> IO (PMuxTree sym b)
pmuxTreeMaybeOp sym
sym a -> IO (Maybe b)
f PMuxTree sym a
mt = sym
-> (Maybe a -> IO (Maybe b))
-> PMuxTree sym a
-> IO (MuxTree sym (Maybe b))
forall b sym a.
(Ord b, IsExprBuilder sym) =>
sym -> (a -> IO b) -> MuxTree sym a -> IO (MuxTree sym b)
MT.muxTreeUnaryOp sym
sym (\Maybe a
a -> Maybe (Maybe b) -> Maybe b
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe b) -> Maybe b)
-> IO (Maybe (Maybe b)) -> IO (Maybe b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> IO (Maybe b)) -> Maybe a -> IO (Maybe (Maybe b))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Maybe a -> m (Maybe b)
mapM a -> IO (Maybe b)
f Maybe a
a) PMuxTree sym a
mt

_pmuxTreeUnaryOp ::
  (W4.IsExprBuilder sym, Ord b) =>
  sym ->
  (a -> IO b) ->
  PMuxTree sym a ->
  IO (PMuxTree sym b)
_pmuxTreeUnaryOp :: forall sym b a.
(IsExprBuilder sym, Ord b) =>
sym -> (a -> IO b) -> PMuxTree sym a -> IO (PMuxTree sym b)
_pmuxTreeUnaryOp sym
sym a -> IO b
f PMuxTree sym a
mt = sym
-> (Maybe a -> IO (Maybe b))
-> PMuxTree sym a
-> IO (MuxTree sym (Maybe b))
forall b sym a.
(Ord b, IsExprBuilder sym) =>
sym -> (a -> IO b) -> MuxTree sym a -> IO (MuxTree sym b)
MT.muxTreeUnaryOp sym
sym (\Maybe a
a -> (a -> IO b) -> Maybe a -> IO (Maybe b)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Maybe a -> m (Maybe b)
mapM a -> IO b
f Maybe a
a) PMuxTree sym a
mt


pmuxTreeBinOp ::
  forall sym a b c.
  (W4.IsExprBuilder sym, Ord c) =>
  sym ->
  (a -> b -> IO c) ->
  PMuxTree sym a ->
  PMuxTree sym b ->
  IO (PMuxTree sym c)
pmuxTreeBinOp :: forall sym a b c.
(IsExprBuilder sym, Ord c) =>
sym
-> (a -> b -> IO c)
-> PMuxTree sym a
-> PMuxTree sym b
-> IO (PMuxTree sym c)
pmuxTreeBinOp sym
sym a -> b -> IO c
f PMuxTree sym a
mt1 PMuxTree sym b
mt2 = sym
-> (Maybe a -> Maybe b -> IO (Maybe c))
-> PMuxTree sym a
-> PMuxTree sym b
-> IO (MuxTree sym (Maybe c))
forall c sym a b.
(Ord c, IsExprBuilder sym) =>
sym
-> (a -> b -> IO c)
-> MuxTree sym a
-> MuxTree sym b
-> IO (MuxTree sym c)
MT.muxTreeBinOp sym
sym Maybe a -> Maybe b -> IO (Maybe c)
g PMuxTree sym a
mt1 PMuxTree sym b
mt2
  where
    g :: Maybe a -> Maybe b -> IO (Maybe c)
    g :: Maybe a -> Maybe b -> IO (Maybe c)
g (Just a
a) (Just b
b) = c -> Maybe c
forall a. a -> Maybe a
Just (c -> Maybe c) -> IO c -> IO (Maybe c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> b -> IO c
f a
a b
b
    g Maybe a
_ Maybe b
_ = Maybe c -> IO (Maybe c)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe c
forall a. Maybe a
Nothing

toPMuxTree :: W4.IsExprBuilder sym => sym -> a -> PMuxTree sym a
toPMuxTree :: forall sym a. IsExprBuilder sym => sym -> a -> PMuxTree sym a
toPMuxTree sym
sym a
a = sym -> Maybe a -> MuxTree sym (Maybe a)
forall sym a. IsExprBuilder sym => sym -> a -> MuxTree sym a
MT.toMuxTree sym
sym (a -> Maybe a
forall a. a -> Maybe a
Just a
a)