-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Concretize
-- Description      : Get feasible concrete values from a model
-- Copyright        : (c) Galois, Inc 2024
-- License          : BSD3
-- Maintainer       : Langston Barrett <langston@galois.com>
-- Stability        : provisional
--
-- This module defines 'concRegValue', a function that takes a 'RegValue' (i.e.,
-- a symbolic value), and a model from the SMT solver ('W4GE.GroundEvalFn'), and
-- returns the concrete value that the symbolic value takes in the model.
--
-- This can be used to report specific values that lead to violations of
-- assertions, including safety assertions.
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Lang.Crucible.Concretize
  ( ConcRegValue
  , ConcRV'(..)
  , ConcAnyValue(..)
  , ConcIntrinsic
  , IntrinsicConcFn(..)
  , ConcCtx(..)
  , concRegValue
  , concRegEntry
  , concRegMap
    -- * There and back again
  , IntrinsicConcToSymFn(..)
  , concToSym
  ) where

import qualified Data.Foldable as F
import           Data.Kind (Type)
import           Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NE
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.Sequence (Seq)
import           Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Vector as V
import           Data.Word (Word16)

import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.TraversableFC (traverseFC)

import           What4.Expr (Expr, ExprBuilder, Flags, FloatModeRepr(..))
import qualified What4.Expr.GroundEval as W4GE
import           What4.Interface (SymExpr)
import qualified What4.Interface as W4I
import qualified What4.Partial as W4P

import           Lang.Crucible.FunctionHandle (FnHandle, RefCell)
import           Lang.Crucible.Simulator.Intrinsics (Intrinsic)
import           Lang.Crucible.Simulator.RegMap (RegEntry, RegMap)
import qualified Lang.Crucible.Simulator.RegMap as RM
import           Lang.Crucible.Simulator.RegValue (RegValue, FnVal)
import qualified Lang.Crucible.Simulator.RegValue as RV
import qualified Lang.Crucible.Simulator.SymSequence as SymSeq
import qualified Lang.Crucible.Utils.MuxTree as MuxTree
import           Lang.Crucible.Types
import           Lang.Crucible.Panic (panic)

-- | Newtype to allow partial application of 'ConcRegValue'.
--
-- Type families cannot appear partially applied.
type ConcRV' :: Type -> CrucibleType -> Type
newtype ConcRV' sym tp = ConcRV' { forall sym (tp :: CrucibleType).
ConcRV' sym tp -> ConcRegValue sym tp
unConcRV' :: ConcRegValue sym tp }

-- | Defines the \"concrete\" interpretations of 'CrucibleType' (as opposed
-- to the \"symbolic\" interpretations, which are defined by 'RegValue'), as
-- returned by 'concRegValue'.
--
-- Unlike What4\'s 'W4GE.GroundValue', this type family is parameterized
-- by @sym@, the symbolic backend. This is because Crucible makes use of
-- \"interpreted\" floating point numbers ('SymInterpretedFloatType'). What4\'s
-- @SymFloat@ always uses an IEEE-754 interpretation of symbolic floats, whereas
-- 'SymInterpretedFloatType' can use IEEE-754, real numbers, or uninterpreted
-- functions depending on how the symbolic backend is configured.
type ConcRegValue :: Type -> CrucibleType -> Type
type family ConcRegValue sym tp where
  ConcRegValue sym (BaseToType bt) = W4GE.GroundValue bt
  ConcRegValue sym (FloatType fi) = W4GE.GroundValue (SymInterpretedFloatType sym fi)
  ConcRegValue sym AnyType = ConcAnyValue sym
  ConcRegValue sym UnitType = ()
  ConcRegValue sym NatType = Integer
  ConcRegValue sym CharType = Word16
  ConcRegValue sym (FunctionHandleType a r) = ConcFnVal sym a r
  ConcRegValue sym (MaybeType tp) = Maybe (ConcRegValue sym tp)
  ConcRegValue sym (VectorType tp) = V.Vector (ConcRV' sym tp)
  ConcRegValue sym (SequenceType tp) = Seq (ConcRV' sym tp)
  ConcRegValue sym (StructType ctx) = Ctx.Assignment (ConcRV' sym) ctx
  ConcRegValue sym (VariantType ctx) = Ctx.Assignment (ConcVariantBranch sym) ctx
  ConcRegValue sym (ReferenceType tp) = NonEmpty (RefCell tp)
  ConcRegValue sym (WordMapType w tp) = ()  -- TODO: possible to do something meaningful?
  ConcRegValue sym (RecursiveType nm ctx) = ConcRegValue sym (UnrollType nm ctx)
  ConcRegValue sym (IntrinsicType nm ctx) = ConcIntrinsic nm ctx
  ConcRegValue sym (StringMapType tp) = Map Text (ConcRV' sym tp)

---------------------------------------------------------------------
-- * ConcCtx

-- | Context needed for 'concRegValue'
--
-- The @t@ parameter matches that on 'W4GE.GroundEvalFn' and 'Expr', namely, it
-- is a phantom type brand used to relate nonces to a specific nonce generator
-- (similar to the @s@ parameter of the @ST@ monad). It also appears as the
-- first argument to 'ExprBuilder'.
data ConcCtx sym t
  = ConcCtx
  { -- | Model returned from SMT solver
    forall sym t. ConcCtx sym t -> GroundEvalFn t
model :: W4GE.GroundEvalFn t
    -- | How to ground intrinsics
  , forall sym t. ConcCtx sym t -> MapF SymbolRepr (IntrinsicConcFn t)
intrinsicConcFuns :: MapF SymbolRepr (IntrinsicConcFn t)
  }

-- | Helper, not exported
ground ::
  ConcCtx sym t ->
  Expr t tp ->
  IO (ConcRegValue sym (BaseToType tp))
ground :: forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground (ConcCtx (W4GE.GroundEvalFn forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
ge) MapF SymbolRepr (IntrinsicConcFn t)
_) = Expr t tp -> IO (GroundValue tp)
Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
ge

---------------------------------------------------------------------
-- * Helpers

-- | Helper, not exported
ite ::
  (SymExpr sym ~ Expr t) =>
  ConcCtx sym t ->
  W4I.Pred sym ->
  a ->
  a ->
  IO a
ite :: forall sym t a.
(SymExpr sym ~ Expr t) =>
ConcCtx sym t -> Pred sym -> a -> a -> IO a
ite ConcCtx sym t
ctx Pred sym
p a
t a
f = do
  Bool
b <- ConcCtx sym t
-> Expr t BaseBoolType
-> IO (ConcRegValue sym (BaseToType BaseBoolType))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Pred sym
Expr t BaseBoolType
p
  a -> IO a
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (if Bool
b then a
t else a
f)

-- | Helper, not exported
iteIO ::
  (SymExpr sym ~ Expr t) =>
  ConcCtx sym t ->
  W4I.Pred sym ->
  IO a ->
  IO a ->
  IO a
iteIO :: forall sym t a.
(SymExpr sym ~ Expr t) =>
ConcCtx sym t -> Pred sym -> IO a -> IO a -> IO a
iteIO ConcCtx sym t
ctx Pred sym
p IO a
t IO a
f = do
  Bool
b <- ConcCtx sym t
-> Expr t BaseBoolType
-> IO (ConcRegValue sym (BaseToType BaseBoolType))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Pred sym
Expr t BaseBoolType
p
  if Bool
b then IO a
t else IO a
f

-- | Helper, not exported
concPartial ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  W4P.Partial (W4I.Pred sym) (RegValue sym tp) ->
  IO (Maybe (ConcRegValue sym tp))
concPartial :: forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp
-> Partial (Pred sym) (RegValue sym tp)
-> IO (Maybe (ConcRegValue sym tp))
concPartial ConcCtx sym t
ctx TypeRepr tp
tp (W4P.Partial Pred sym
p RegValue sym tp
v) =
  ConcCtx sym t
-> Pred sym
-> IO (Maybe (ConcRegValue sym tp))
-> IO (Maybe (ConcRegValue sym tp))
-> IO (Maybe (ConcRegValue sym tp))
forall sym t a.
(SymExpr sym ~ Expr t) =>
ConcCtx sym t -> Pred sym -> IO a -> IO a -> IO a
iteIO ConcCtx sym t
ctx Pred sym
p (ConcRegValue sym tp -> Maybe (ConcRegValue sym tp)
forall a. a -> Maybe a
Just (ConcRegValue sym tp -> Maybe (ConcRegValue sym tp))
-> IO (ConcRegValue sym tp) -> IO (Maybe (ConcRegValue sym tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
concRegValue ConcCtx sym t
ctx TypeRepr tp
tp RegValue sym tp
v) (Maybe (ConcRegValue sym tp) -> IO (Maybe (ConcRegValue sym tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (ConcRegValue sym tp)
forall a. Maybe a
Nothing)

-- | Helper, not exported
concPartialWithErr ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  W4P.PartialWithErr e (W4I.Pred sym) (RegValue sym tp) ->
  IO (Maybe (ConcRegValue sym tp))
concPartialWithErr :: forall sym t (tp :: CrucibleType) e.
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp
-> PartialWithErr e (Pred sym) (RegValue sym tp)
-> IO (Maybe (ConcRegValue sym tp))
concPartialWithErr ConcCtx sym t
ctx TypeRepr tp
tp =
  \case
    W4P.Err e
_ -> Maybe (ConcRegValue sym tp) -> IO (Maybe (ConcRegValue sym tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (ConcRegValue sym tp)
forall a. Maybe a
Nothing
    W4P.NoErr Partial (Pred sym) (RegValue sym tp)
pv -> ConcCtx sym t
-> TypeRepr tp
-> Partial (Pred sym) (RegValue sym tp)
-> IO (Maybe (ConcRegValue sym tp))
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp
-> Partial (Pred sym) (RegValue sym tp)
-> IO (Maybe (ConcRegValue sym tp))
concPartial ConcCtx sym t
ctx TypeRepr tp
tp Partial (Pred sym) (RegValue sym tp)
pv

---------------------------------------------------------------------
-- * Intrinsics

-- | Open type family for defining how intrinsics are concretized
type ConcIntrinsic :: Symbol -> Ctx CrucibleType -> Type
type family ConcIntrinsic nm ctx

-- | Function for concretizing an intrinsic type
type IntrinsicConcFn :: Type -> Symbol -> Type
newtype IntrinsicConcFn t nm
  = IntrinsicConcFn
    (forall sym ctx.
      SymExpr sym ~ Expr t =>
      W4I.IsExprBuilder sym =>
      ConcCtx sym t ->
      Ctx.Assignment TypeRepr ctx ->
      Intrinsic sym nm ctx ->
      IO (ConcRegValue sym (IntrinsicType nm ctx)))

-- | Helper, not exported
tryConcIntrinsic ::
  forall sym nm ctx t.
  SymExpr sym ~ Expr t =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  SymbolRepr nm ->
  Ctx.Assignment TypeRepr ctx ->
  RegValue sym (IntrinsicType nm ctx) ->
  Maybe (IO (ConcRegValue sym (IntrinsicType nm ctx)))
tryConcIntrinsic :: forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType) t.
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> SymbolRepr nm
-> Assignment TypeRepr ctx
-> RegValue sym (IntrinsicType nm ctx)
-> Maybe (IO (ConcRegValue sym (IntrinsicType nm ctx)))
tryConcIntrinsic ConcCtx sym t
ctx SymbolRepr nm
nm Assignment TypeRepr ctx
tyCtx RegValue sym (IntrinsicType nm ctx)
v = do
    case SymbolRepr nm
-> MapF SymbolRepr (IntrinsicConcFn t)
-> Maybe (IntrinsicConcFn t nm)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup SymbolRepr nm
nm (ConcCtx sym t -> MapF SymbolRepr (IntrinsicConcFn t)
forall sym t. ConcCtx sym t -> MapF SymbolRepr (IntrinsicConcFn t)
intrinsicConcFuns ConcCtx sym t
ctx) of
      Maybe (IntrinsicConcFn t nm)
Nothing -> Maybe (IO (ConcIntrinsic nm ctx))
Maybe (IO (ConcRegValue sym (IntrinsicType nm ctx)))
forall a. Maybe a
Nothing
      Just (IntrinsicConcFn forall sym (ctx :: Ctx CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> Assignment TypeRepr ctx
-> Intrinsic sym nm ctx
-> IO (ConcRegValue sym (IntrinsicType nm ctx))
f) -> IO (ConcIntrinsic nm ctx) -> Maybe (IO (ConcIntrinsic nm ctx))
forall a. a -> Maybe a
Just (forall sym (ctx :: Ctx CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> Assignment TypeRepr ctx
-> Intrinsic sym nm ctx
-> IO (ConcRegValue sym (IntrinsicType nm ctx))
f @sym @ctx ConcCtx sym t
ctx Assignment TypeRepr ctx
tyCtx Intrinsic sym nm ctx
RegValue sym (IntrinsicType nm ctx)
v)

---------------------------------------------------------------------
-- * Any

-- | An 'AnyValue' concretized by 'concRegValue'
data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRV' sym tp)

---------------------------------------------------------------------
-- * FnVal

-- | A 'FnVal' concretized by 'concRegValue'
data ConcFnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where
  ConcClosureFnVal ::
    !(ConcFnVal sym (args ::> tp) ret) ->
    !(TypeRepr tp) ->
    !(ConcRV' sym tp) ->
    ConcFnVal sym args ret

  ConcVarargsFnVal ::
    !(FnHandle (args ::> VectorType AnyType) ret) ->
    !(CtxRepr addlArgs) ->
    ConcFnVal sym (args <+> addlArgs) ret

  ConcHandleFnVal ::
    !(FnHandle a r) ->
    ConcFnVal sym a r

-- | Helper, not exported
concFnVal ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  CtxRepr args ->
  TypeRepr ret ->
  FnVal sym args ret ->
  IO (ConcFnVal sym args ret)
concFnVal :: forall sym t (args :: Ctx CrucibleType) (ret :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> CtxRepr args
-> TypeRepr ret
-> FnVal sym args ret
-> IO (ConcFnVal sym args ret)
concFnVal ConcCtx sym t
ctx CtxRepr args
args TypeRepr ret
ret =
  \case
    RV.ClosureFnVal FnVal sym (args ::> tp) ret
fv TypeRepr tp
t RegValue sym tp
v -> do
      ConcFnVal sym (args ::> tp) ret
concV <- ConcCtx sym t
-> CtxRepr (args ::> tp)
-> TypeRepr ret
-> FnVal sym (args ::> tp) ret
-> IO (ConcFnVal sym (args ::> tp) ret)
forall sym t (args :: Ctx CrucibleType) (ret :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> CtxRepr args
-> TypeRepr ret
-> FnVal sym args ret
-> IO (ConcFnVal sym args ret)
concFnVal ConcCtx sym t
ctx (CtxRepr args
args CtxRepr args -> TypeRepr tp -> CtxRepr (args ::> tp)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> TypeRepr tp
t) TypeRepr ret
ret FnVal sym (args ::> tp) ret
fv
      ConcRegValue sym tp
v' <- ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
concRegValue ConcCtx sym t
ctx TypeRepr tp
t RegValue sym tp
v
      ConcFnVal sym args ret -> IO (ConcFnVal sym args ret)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ConcFnVal sym (args ::> tp) ret
-> TypeRepr tp -> ConcRV' sym tp -> ConcFnVal sym args ret
forall sym (args :: Ctx CrucibleType) (args :: CrucibleType)
       (ret :: CrucibleType).
ConcFnVal sym (args ::> args) ret
-> TypeRepr args -> ConcRV' sym args -> ConcFnVal sym args ret
ConcClosureFnVal ConcFnVal sym (args ::> tp) ret
concV TypeRepr tp
t (ConcRegValue sym tp -> ConcRV' sym tp
forall sym (tp :: CrucibleType).
ConcRegValue sym tp -> ConcRV' sym tp
ConcRV' ConcRegValue sym tp
v'))
    RV.VarargsFnVal FnHandle (args1 ::> VectorType AnyType) ret
hdl CtxRepr addlArgs
extra ->
      ConcFnVal sym args ret -> IO (ConcFnVal sym args ret)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (FnHandle (args1 ::> VectorType AnyType) ret
-> CtxRepr addlArgs -> ConcFnVal sym (args1 <+> addlArgs) ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (addlArgs :: Ctx CrucibleType) sym.
FnHandle (args ::> VectorType AnyType) ret
-> CtxRepr addlArgs -> ConcFnVal sym (args <+> addlArgs) ret
ConcVarargsFnVal FnHandle (args1 ::> VectorType AnyType) ret
hdl CtxRepr addlArgs
extra)
    RV.HandleFnVal FnHandle args ret
hdl ->
      ConcFnVal sym args ret -> IO (ConcFnVal sym args ret)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (FnHandle args ret -> ConcFnVal sym args ret
forall (a :: Ctx CrucibleType) (r :: CrucibleType) sym.
FnHandle a r -> ConcFnVal sym a r
ConcHandleFnVal FnHandle args ret
hdl)

---------------------------------------------------------------------
-- * Reference

-- | Helper, not exported
concMux ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  MuxTree.MuxTree sym a ->
  IO (NonEmpty a)
concMux :: forall sym t a.
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t -> MuxTree sym a -> IO (NonEmpty a)
concMux ConcCtx sym t
ctx MuxTree sym a
mt = do
  [a]
l <- [(a, Expr t BaseBoolType)] -> IO [a]
go (MuxTree sym a -> [(a, Pred sym)]
forall sym a. MuxTree sym a -> [(a, Pred sym)]
MuxTree.viewMuxTree MuxTree sym a
mt)
  case [a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [a]
l of
    -- This is impossible because the only way to make a MuxTree is with
    -- `toMuxTree`, which uses `truePred`.
    Maybe (NonEmpty a)
Nothing ->
      String -> [String] -> IO (NonEmpty a)
forall a. HasCallStack => String -> [String] -> a
panic String
"Lang.Crucible.Concretize.concMux"
        [ String
"Impossible: Mux tree had no feasible branches?" ]
    Just NonEmpty a
ne -> NonEmpty a -> IO (NonEmpty a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure NonEmpty a
ne
  where
    go :: [(a, Expr t BaseBoolType)] -> IO [a]
go [] = [a] -> IO [a]
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure []
    go ((a
val, Expr t BaseBoolType
p):[(a, Expr t BaseBoolType)]
xs) = do
      [a] -> [a]
f <- ConcCtx sym t
-> Pred sym -> ([a] -> [a]) -> ([a] -> [a]) -> IO ([a] -> [a])
forall sym t a.
(SymExpr sym ~ Expr t) =>
ConcCtx sym t -> Pred sym -> a -> a -> IO a
ite ConcCtx sym t
ctx Pred sym
Expr t BaseBoolType
p (a
vala -> [a] -> [a]
forall a. a -> [a] -> [a]
:) [a] -> [a]
forall a. a -> a
id
      [a] -> [a]
f ([a] -> [a]) -> IO [a] -> IO [a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Expr t BaseBoolType)] -> IO [a]
go [(a, Expr t BaseBoolType)]
xs

---------------------------------------------------------------------
-- * Sequence

-- | Helper, not exported
concSymSequence ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  SymSeq.SymSequence sym (RegValue sym tp) ->
  IO (Seq (ConcRV' sym tp))
concSymSequence :: forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp
-> SymSequence sym (RegValue sym tp)
-> IO (Seq (ConcRV' sym tp))
concSymSequence ConcCtx sym t
ctx TypeRepr tp
tp =
  (Pred sym -> IO Bool)
-> (RegValue sym tp -> IO (ConcRV' sym tp))
-> SymSequence sym (RegValue sym tp)
-> IO (Seq (ConcRV' sym tp))
forall sym a b.
(Pred sym -> IO Bool)
-> (a -> IO b) -> SymSequence sym a -> IO (Seq b)
SymSeq.concretizeSymSequence
    (ConcCtx sym t
-> Expr t BaseBoolType
-> IO (ConcRegValue sym (BaseToType BaseBoolType))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx)
    ((ConcRegValue sym tp -> ConcRV' sym tp)
-> IO (ConcRegValue sym tp) -> IO (ConcRV' sym tp)
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ConcRegValue sym tp -> ConcRV' sym tp
forall sym (tp :: CrucibleType).
ConcRegValue sym tp -> ConcRV' sym tp
ConcRV' (IO (ConcRegValue sym tp) -> IO (ConcRV' sym tp))
-> (RegValue sym tp -> IO (ConcRegValue sym tp))
-> RegValue sym tp
-> IO (ConcRV' sym tp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
concRegValue ConcCtx sym t
ctx TypeRepr tp
tp)

---------------------------------------------------------------------
-- * StringMap

-- | Helper, not exported
concStringMap ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  RegValue sym (StringMapType tp) ->
  IO (Map Text (ConcRV' sym tp))
concStringMap :: forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp
-> RegValue sym (StringMapType tp)
-> IO (Map Text (ConcRV' sym tp))
concStringMap ConcCtx sym t
ctx TypeRepr tp
tp RegValue sym (StringMapType tp)
v = [(Text, ConcRV' sym tp)] -> Map Text (ConcRV' sym tp)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Text, ConcRV' sym tp)] -> Map Text (ConcRV' sym tp))
-> IO [(Text, ConcRV' sym tp)] -> IO (Map Text (ConcRV' sym tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp))]
-> IO [(Text, ConcRV' sym tp)]
go (Map
  Text (PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp))
-> [(Text,
     PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp))]
forall k a. Map k a -> [(k, a)]
Map.toList Map
  Text (PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp))
RegValue sym (StringMapType tp)
v)
  where
    go :: [(Text, PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp))]
-> IO [(Text, ConcRV' sym tp)]
go [] = [(Text, ConcRV' sym tp)] -> IO [(Text, ConcRV' sym tp)]
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure []
    go ((Text
t, PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp)
v'):[(Text, PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp))]
xs) =
      ConcCtx sym t
-> TypeRepr tp
-> PartialWithErr () (Pred sym) (RegValue sym tp)
-> IO (Maybe (ConcRegValue sym tp))
forall sym t (tp :: CrucibleType) e.
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp
-> PartialWithErr e (Pred sym) (RegValue sym tp)
-> IO (Maybe (ConcRegValue sym tp))
concPartialWithErr ConcCtx sym t
ctx TypeRepr tp
tp PartialWithErr () (Pred sym) (RegValue sym tp)
PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp)
v' IO (Maybe (ConcRegValue sym tp))
-> (Maybe (ConcRegValue sym tp) -> IO [(Text, ConcRV' sym tp)])
-> IO [(Text, ConcRV' sym tp)]
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>=
        \case
          Maybe (ConcRegValue sym tp)
Nothing -> [(Text, PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp))]
-> IO [(Text, ConcRV' sym tp)]
go [(Text, PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp))]
xs
          Just ConcRegValue sym tp
v'' -> ((Text
t, ConcRegValue sym tp -> ConcRV' sym tp
forall sym (tp :: CrucibleType).
ConcRegValue sym tp -> ConcRV' sym tp
ConcRV' ConcRegValue sym tp
v'')(Text, ConcRV' sym tp)
-> [(Text, ConcRV' sym tp)] -> [(Text, ConcRV' sym tp)]
forall a. a -> [a] -> [a]
:) ([(Text, ConcRV' sym tp)] -> [(Text, ConcRV' sym tp)])
-> IO [(Text, ConcRV' sym tp)] -> IO [(Text, ConcRV' sym tp)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp))]
-> IO [(Text, ConcRV' sym tp)]
go [(Text, PartialWithErr () (Expr t BaseBoolType) (RegValue sym tp))]
xs

---------------------------------------------------------------------
-- * Variant

-- | Note that we do not attempt to \"normalize\" variants in 'concRegValue'
-- in any way. If the model reports that multiple branches of a variant are
-- plausible, then multiple branches might be included as 'Just's.
newtype ConcVariantBranch sym tp
  = ConcVariantBranch (Maybe (ConcRV' sym tp))

-- | Helper, not exported
concVariant ::
  forall sym variants t.
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  Ctx.Assignment TypeRepr variants ->
  RegValue sym (VariantType variants) ->
  IO (ConcRegValue sym (VariantType variants))
concVariant :: forall sym (variants :: Ctx CrucibleType) t.
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> Assignment TypeRepr variants
-> RegValue sym (VariantType variants)
-> IO (ConcRegValue sym (VariantType variants))
concVariant ConcCtx sym t
ctx Assignment TypeRepr variants
tps RegValue sym (VariantType variants)
vs = (forall (x :: CrucibleType).
 TypeRepr x -> VariantBranch sym x -> IO (ConcVariantBranch sym x))
-> Assignment TypeRepr variants
-> Assignment (VariantBranch sym) variants
-> IO (Assignment (ConcVariantBranch sym) variants)
forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
       (h :: k -> Type) (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 TypeRepr x -> VariantBranch sym x -> IO (ConcVariantBranch sym x)
forall (x :: CrucibleType).
TypeRepr x -> VariantBranch sym x -> IO (ConcVariantBranch sym x)
concBranch Assignment TypeRepr variants
tps Assignment (VariantBranch sym) variants
RegValue sym (VariantType variants)
vs
  where
    concBranch :: forall tp. TypeRepr tp -> RV.VariantBranch sym tp -> IO (ConcVariantBranch sym tp)
    concBranch :: forall (x :: CrucibleType).
TypeRepr x -> VariantBranch sym x -> IO (ConcVariantBranch sym x)
concBranch TypeRepr tp
tp (RV.VB PartExpr (Pred sym) (RegValue sym tp)
v) = do
      Maybe (ConcRegValue sym tp)
v' <- ConcCtx sym t
-> TypeRepr tp
-> PartExpr (Pred sym) (RegValue sym tp)
-> IO (Maybe (ConcRegValue sym tp))
forall sym t (tp :: CrucibleType) e.
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp
-> PartialWithErr e (Pred sym) (RegValue sym tp)
-> IO (Maybe (ConcRegValue sym tp))
concPartialWithErr ConcCtx sym t
ctx TypeRepr tp
tp PartExpr (Pred sym) (RegValue sym tp)
v
      case Maybe (ConcRegValue sym tp)
v' of
        Just ConcRegValue sym tp
v'' -> ConcVariantBranch sym tp -> IO (ConcVariantBranch sym tp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe (ConcRV' sym tp) -> ConcVariantBranch sym tp
forall sym (tp :: CrucibleType).
Maybe (ConcRV' sym tp) -> ConcVariantBranch sym tp
ConcVariantBranch (ConcRV' sym tp -> Maybe (ConcRV' sym tp)
forall a. a -> Maybe a
Just (ConcRegValue sym tp -> ConcRV' sym tp
forall sym (tp :: CrucibleType).
ConcRegValue sym tp -> ConcRV' sym tp
ConcRV' ConcRegValue sym tp
v'')))
        Maybe (ConcRegValue sym tp)
Nothing -> ConcVariantBranch sym tp -> IO (ConcVariantBranch sym tp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe (ConcRV' sym tp) -> ConcVariantBranch sym tp
forall sym (tp :: CrucibleType).
Maybe (ConcRV' sym tp) -> ConcVariantBranch sym tp
ConcVariantBranch Maybe (ConcRV' sym tp)
forall a. Maybe a
Nothing)

---------------------------------------------------------------------
-- * 'concRegValue'

-- | Pick a feasible concrete value from the model
--
-- This function does not attempt to \"normalize\" variants nor mux trees in any
-- way. If the model reports that multiple branches of a variant or mux tree are
-- plausible, then multiple branches might be included in the result.
concRegValue ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  RegValue sym tp ->
  IO (ConcRegValue sym tp)
concRegValue :: forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
concRegValue ConcCtx sym t
ctx TypeRepr tp
tp RegValue sym tp
v =
  case (TypeRepr tp
tp, RegValue sym tp
v) of
    -- Base types
    (TypeRepr tp
BoolRepr, RegValue sym tp
_) -> ConcCtx sym t
-> Expr t BaseBoolType
-> IO (ConcRegValue sym (BaseToType BaseBoolType))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Expr t BaseBoolType
RegValue sym tp
v
    (BVRepr NatRepr n
_width, RegValue sym tp
_) -> ConcCtx sym t
-> Expr t (BaseBVType n)
-> IO (ConcRegValue sym ('BaseToType (BaseBVType n)))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Expr t (BaseBVType n)
RegValue sym tp
v
    (TypeRepr tp
ComplexRealRepr, RegValue sym tp
_) -> ConcCtx sym t
-> Expr t BaseComplexType
-> IO (ConcRegValue sym ('BaseToType BaseComplexType))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Expr t BaseComplexType
RegValue sym tp
v
    (FloatRepr FloatInfoRepr flt
_fpp, RegValue sym tp
_) -> ConcCtx sym t
-> Expr t (SymInterpretedFloatType sym flt)
-> IO
     (ConcRegValue sym (BaseToType (SymInterpretedFloatType sym flt)))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Expr t (SymInterpretedFloatType sym flt)
RegValue sym tp
v
    (IEEEFloatRepr FloatPrecisionRepr ps
_fpp, RegValue sym tp
_) -> ConcCtx sym t
-> Expr t (BaseFloatType ps)
-> IO (ConcRegValue sym ('BaseToType (BaseFloatType ps)))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Expr t (BaseFloatType ps)
RegValue sym tp
v
    (TypeRepr tp
IntegerRepr, RegValue sym tp
_) -> ConcCtx sym t
-> Expr t BaseIntegerType
-> IO (ConcRegValue sym ('BaseToType BaseIntegerType))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Expr t BaseIntegerType
RegValue sym tp
v
    (TypeRepr tp
NatRepr, RegValue sym tp
_) -> ConcCtx sym t
-> Expr t BaseIntegerType
-> IO (ConcRegValue sym ('BaseToType BaseIntegerType))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx (SymNat sym -> SymInteger sym
forall sym. SymNat sym -> SymInteger sym
W4I.natToIntegerPure SymNat sym
RegValue sym tp
v)
    (TypeRepr tp
RealValRepr, RegValue sym tp
_) -> ConcCtx sym t
-> Expr t BaseRealType
-> IO (ConcRegValue sym ('BaseToType BaseRealType))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Expr t BaseRealType
RegValue sym tp
v
    (StringRepr StringInfoRepr si
_, RegValue sym tp
_) -> ConcCtx sym t
-> Expr t (BaseStringType si)
-> IO (ConcRegValue sym ('BaseToType (BaseStringType si)))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Expr t (BaseStringType si)
RegValue sym tp
v
    (SymbolicArrayRepr Assignment BaseTypeRepr (idx ::> tp1)
_idxs BaseTypeRepr t
_tp', RegValue sym tp
_) -> ConcCtx sym t
-> Expr t (BaseArrayType (idx ::> tp1) t)
-> IO
     (ConcRegValue sym ('BaseToType (BaseArrayType (idx ::> tp1) t)))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Expr t (BaseArrayType (idx ::> tp1) t)
RegValue sym tp
v
    (SymbolicStructRepr Assignment BaseTypeRepr ctx
_tys, RegValue sym tp
_) -> ConcCtx sym t
-> Expr t (BaseStructType ctx)
-> IO (ConcRegValue sym ('BaseToType (BaseStructType ctx)))
forall sym t (tp :: BaseType).
ConcCtx sym t -> Expr t tp -> IO (ConcRegValue sym (BaseToType tp))
ground ConcCtx sym t
ctx Expr t (BaseStructType ctx)
RegValue sym tp
v

    -- Trivial cases
    (TypeRepr tp
UnitRepr, ()) -> () -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
    (TypeRepr tp
CharRepr, RegValue sym tp
_) -> Word16 -> IO Word16
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Word16
RegValue sym tp
v

    -- Simple recursive cases
    (TypeRepr tp
AnyRepr, RV.AnyValue TypeRepr tp
tp' RegValue sym tp
v') ->
      TypeRepr tp -> ConcRV' sym tp -> ConcAnyValue sym
forall sym (tp :: CrucibleType).
TypeRepr tp -> ConcRV' sym tp -> ConcAnyValue sym
ConcAnyValue TypeRepr tp
tp' (ConcRV' sym tp -> ConcAnyValue sym)
-> (ConcRegValue sym tp -> ConcRV' sym tp)
-> ConcRegValue sym tp
-> ConcAnyValue sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConcRegValue sym tp -> ConcRV' sym tp
forall sym (tp :: CrucibleType).
ConcRegValue sym tp -> ConcRV' sym tp
ConcRV' (ConcRegValue sym tp -> ConcAnyValue sym)
-> IO (ConcRegValue sym tp) -> IO (ConcAnyValue sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
concRegValue ConcCtx sym t
ctx TypeRepr tp
tp' RegValue sym tp
v'
    (RecursiveRepr SymbolRepr nm
symb CtxRepr ctx
tyCtx, RV.RolledType RegValue sym (UnrollType nm ctx)
v') ->
      ConcCtx sym t
-> TypeRepr (UnrollType nm ctx)
-> RegValue sym (UnrollType nm ctx)
-> IO (ConcRegValue sym (UnrollType nm ctx))
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
concRegValue ConcCtx sym t
ctx (SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
IsRecursiveType nm =>
SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
forall (ctx :: Ctx CrucibleType).
SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
unrollType SymbolRepr nm
symb CtxRepr ctx
tyCtx) RegValue sym (UnrollType nm ctx)
v'
    (StructRepr CtxRepr ctx
tps, RegValue sym tp
_) ->
      (forall (x :: CrucibleType).
 TypeRepr x -> RegValue' sym x -> IO (ConcRV' sym x))
-> CtxRepr ctx
-> Assignment (RegValue' sym) ctx
-> IO (Assignment (ConcRV' sym) ctx)
forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
       (h :: k -> Type) (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 (\TypeRepr x
tp' (RV.RV RegValue sym x
v') -> ConcRegValue sym x -> ConcRV' sym x
forall sym (tp :: CrucibleType).
ConcRegValue sym tp -> ConcRV' sym tp
ConcRV' (ConcRegValue sym x -> ConcRV' sym x)
-> IO (ConcRegValue sym x) -> IO (ConcRV' sym x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ConcCtx sym t
-> TypeRepr x -> RegValue sym x -> IO (ConcRegValue sym x)
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
concRegValue ConcCtx sym t
ctx TypeRepr x
tp' RegValue sym x
v') CtxRepr ctx
tps Assignment (RegValue' sym) ctx
RegValue sym tp
v
    (VectorRepr TypeRepr tp1
tp', RegValue sym tp
_) ->
      (RegValue sym tp1 -> IO (ConcRV' sym tp1))
-> Vector (RegValue sym tp1) -> IO (Vector (ConcRV' sym tp1))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ((ConcRegValue sym tp1 -> ConcRV' sym tp1)
-> IO (ConcRegValue sym tp1) -> IO (ConcRV' sym tp1)
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ConcRegValue sym tp1 -> ConcRV' sym tp1
forall sym (tp :: CrucibleType).
ConcRegValue sym tp -> ConcRV' sym tp
ConcRV' (IO (ConcRegValue sym tp1) -> IO (ConcRV' sym tp1))
-> (RegValue sym tp1 -> IO (ConcRegValue sym tp1))
-> RegValue sym tp1
-> IO (ConcRV' sym tp1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConcCtx sym t
-> TypeRepr tp1 -> RegValue sym tp1 -> IO (ConcRegValue sym tp1)
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
concRegValue ConcCtx sym t
ctx TypeRepr tp1
tp') Vector (RegValue sym tp1)
RegValue sym tp
v

    -- Cases with helper functions
    (MaybeRepr TypeRepr tp1
tp', RegValue sym tp
_) ->
      ConcCtx sym t
-> TypeRepr tp1
-> PartialWithErr () (Pred sym) (RegValue sym tp1)
-> IO (Maybe (ConcRegValue sym tp1))
forall sym t (tp :: CrucibleType) e.
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp
-> PartialWithErr e (Pred sym) (RegValue sym tp)
-> IO (Maybe (ConcRegValue sym tp))
concPartialWithErr ConcCtx sym t
ctx TypeRepr tp1
tp' PartialWithErr () (Pred sym) (RegValue sym tp1)
RegValue sym tp
v
    (FunctionHandleRepr CtxRepr ctx
args TypeRepr ret
ret, RegValue sym tp
_) ->
      ConcCtx sym t
-> CtxRepr ctx
-> TypeRepr ret
-> FnVal sym ctx ret
-> IO (ConcFnVal sym ctx ret)
forall sym t (args :: Ctx CrucibleType) (ret :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> CtxRepr args
-> TypeRepr ret
-> FnVal sym args ret
-> IO (ConcFnVal sym args ret)
concFnVal ConcCtx sym t
ctx CtxRepr ctx
args TypeRepr ret
ret FnVal sym ctx ret
RegValue sym tp
v
    (IntrinsicRepr SymbolRepr nm
nm CtxRepr ctx
tyCtx, RegValue sym tp
_) ->
      case ConcCtx sym t
-> SymbolRepr nm
-> CtxRepr ctx
-> RegValue sym ('IntrinsicType nm ctx)
-> Maybe (IO (ConcRegValue sym ('IntrinsicType nm ctx)))
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType) t.
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> SymbolRepr nm
-> Assignment TypeRepr ctx
-> RegValue sym (IntrinsicType nm ctx)
-> Maybe (IO (ConcRegValue sym (IntrinsicType nm ctx)))
tryConcIntrinsic ConcCtx sym t
ctx SymbolRepr nm
nm CtxRepr ctx
tyCtx RegValue sym tp
RegValue sym ('IntrinsicType nm ctx)
v of
        Maybe (IO (ConcRegValue sym ('IntrinsicType nm ctx)))
Nothing ->
          let strNm :: String
strNm = Text -> String
Text.unpack (SymbolRepr nm -> Text
forall (nm :: Symbol). SymbolRepr nm -> Text
symbolRepr SymbolRepr nm
nm) in
          String -> IO (ConcIntrinsic nm ctx)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
"Missing concretization function for intrinsic: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
strNm)
        Just IO (ConcRegValue sym ('IntrinsicType nm ctx))
r -> IO (ConcRegValue sym tp)
IO (ConcRegValue sym ('IntrinsicType nm ctx))
r
    (ReferenceRepr TypeRepr a
_, RegValue sym tp
_) ->
      ConcCtx sym t
-> MuxTree sym (RefCell a) -> IO (NonEmpty (RefCell a))
forall sym t a.
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t -> MuxTree sym a -> IO (NonEmpty a)
concMux ConcCtx sym t
ctx MuxTree sym (RefCell a)
RegValue sym tp
v
    (SequenceRepr TypeRepr tp1
tp', RegValue sym tp
_) ->
      ConcCtx sym t
-> TypeRepr tp1
-> SymSequence sym (RegValue sym tp1)
-> IO (Seq (ConcRV' sym tp1))
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp
-> SymSequence sym (RegValue sym tp)
-> IO (Seq (ConcRV' sym tp))
concSymSequence ConcCtx sym t
ctx TypeRepr tp1
tp' SymSequence sym (RegValue sym tp1)
RegValue sym tp
v
    (StringMapRepr TypeRepr tp1
tp', RegValue sym tp
_) ->
      ConcCtx sym t
-> TypeRepr tp1
-> RegValue sym ('StringMapType tp1)
-> IO (Map Text (ConcRV' sym tp1))
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp
-> RegValue sym (StringMapType tp)
-> IO (Map Text (ConcRV' sym tp))
concStringMap ConcCtx sym t
ctx TypeRepr tp1
tp' RegValue sym tp
RegValue sym ('StringMapType tp1)
v
    (VariantRepr CtxRepr ctx
tps, RegValue sym tp
_) ->
      ConcCtx sym t
-> CtxRepr ctx
-> RegValue sym ('VariantType ctx)
-> IO (ConcRegValue sym ('VariantType ctx))
forall sym (variants :: Ctx CrucibleType) t.
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> Assignment TypeRepr variants
-> RegValue sym (VariantType variants)
-> IO (ConcRegValue sym (VariantType variants))
concVariant ConcCtx sym t
ctx CtxRepr ctx
tps RegValue sym tp
RegValue sym ('VariantType ctx)
v

    -- Incomplete cases
    (WordMapRepr NatRepr n
_ BaseTypeRepr tp1
_, RegValue sym tp
_) -> () -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()

-- | Like 'concRegValue', but for 'RegEntry'
concRegEntry ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  RegEntry sym tp ->
  IO (ConcRegValue sym tp)
concRegEntry :: forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t -> RegEntry sym tp -> IO (ConcRegValue sym tp)
concRegEntry ConcCtx sym t
ctx RegEntry sym tp
e = ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
concRegValue ConcCtx sym t
ctx (RegEntry sym tp -> TypeRepr tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
RM.regType RegEntry sym tp
e) (RegEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
RM.regValue RegEntry sym tp
e)

-- | Like 'concRegEntry', but for a whole 'RegMap'
concRegMap ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  RegMap sym tps ->
  IO (Ctx.Assignment (ConcRV' sym) tps)
concRegMap :: forall sym t (tps :: Ctx CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> RegMap sym tps -> IO (Assignment (ConcRV' sym) tps)
concRegMap ConcCtx sym t
ctx (RM.RegMap Assignment (RegEntry sym) tps
m) = (forall (x :: CrucibleType). RegEntry sym x -> IO (ConcRV' sym x))
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> IO (Assignment (ConcRV' sym) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC ((ConcRegValue sym x -> ConcRV' sym x)
-> IO (ConcRegValue sym x) -> IO (ConcRV' sym x)
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ConcRegValue sym x -> ConcRV' sym x
forall sym (tp :: CrucibleType).
ConcRegValue sym tp -> ConcRV' sym tp
ConcRV' (IO (ConcRegValue sym x) -> IO (ConcRV' sym x))
-> (RegEntry sym x -> IO (ConcRegValue sym x))
-> RegEntry sym x
-> IO (ConcRV' sym x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConcCtx sym t -> RegEntry sym x -> IO (ConcRegValue sym x)
forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t -> RegEntry sym tp -> IO (ConcRegValue sym tp)
concRegEntry ConcCtx sym t
ctx) Assignment (RegEntry sym) tps
m

---------------------------------------------------------------------
-- * concToSym

-- | Function for re-symbolizing an intrinsic type
type IntrinsicConcToSymFn :: Symbol -> Type
newtype IntrinsicConcToSymFn nm
  = IntrinsicConcToSymFn
    (forall sym ctx.
      W4I.IsExprBuilder sym =>
      sym ->
      Ctx.Assignment TypeRepr ctx ->
      ConcIntrinsic nm ctx ->
      IO (RegValue sym (IntrinsicType nm ctx)))

-- | Helper, not exported
concToSymAny ::
  (sym ~ ExprBuilder scope st (Flags fm)) =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  FloatModeRepr fm ->
  ConcRegValue sym AnyType ->
  IO (RegValue sym AnyType)
concToSymAny :: forall sym scope (st :: Type -> Type) (fm :: FloatMode).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> ConcRegValue sym AnyType
-> IO (RegValue sym AnyType)
concToSymAny sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm (ConcAnyValue TypeRepr tp
tp' (ConcRV' ConcRegValue (ExprBuilder scope st (Flags fm)) tp
v')) =
  TypeRepr tp
-> RegValue (ExprBuilder scope st (Flags fm)) tp
-> AnyValue (ExprBuilder scope st (Flags fm))
forall (tp :: CrucibleType) sym.
TypeRepr tp -> RegValue sym tp -> AnyValue sym
RV.AnyValue TypeRepr tp
tp' (RegValue (ExprBuilder scope st (Flags fm)) tp
 -> AnyValue (ExprBuilder scope st (Flags fm)))
-> IO (RegValue (ExprBuilder scope st (Flags fm)) tp)
-> IO (AnyValue (ExprBuilder scope st (Flags fm)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
concToSym sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr tp
tp' ConcRegValue sym tp
ConcRegValue (ExprBuilder scope st (Flags fm)) tp
v'

-- | Helper, not exported
concToSymFn ::
  (sym ~ ExprBuilder scope st (Flags fm)) =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  FloatModeRepr fm ->
  Ctx.Assignment (TypeRepr) as ->
  TypeRepr r ->
  ConcRegValue sym (FunctionHandleType as r) ->
  IO (RegValue sym (FunctionHandleType as r))
concToSymFn :: forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (as :: Ctx CrucibleType) (r :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> Assignment TypeRepr as
-> TypeRepr r
-> ConcRegValue sym (FunctionHandleType as r)
-> IO (RegValue sym (FunctionHandleType as r))
concToSymFn sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm Assignment TypeRepr as
as TypeRepr r
r ConcRegValue sym (FunctionHandleType as r)
f =
  case ConcRegValue sym (FunctionHandleType as r)
f of
    ConcClosureFnVal ConcFnVal (ExprBuilder scope st (Flags fm)) (as ::> tp) r
clos TypeRepr tp
vtp (ConcRV' ConcRegValue (ExprBuilder scope st (Flags fm)) tp
v) -> do
      RegValue (ExprBuilder scope st (Flags fm)) tp
v' <- sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
concToSym sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr tp
vtp ConcRegValue sym tp
ConcRegValue (ExprBuilder scope st (Flags fm)) tp
v
      FnVal (ExprBuilder scope st (Flags fm)) (as ::> tp) r
clos' <- sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> Assignment TypeRepr (as ::> tp)
-> TypeRepr r
-> ConcRegValue sym (FunctionHandleType (as ::> tp) r)
-> IO (RegValue sym (FunctionHandleType (as ::> tp) r))
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (as :: Ctx CrucibleType) (r :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> Assignment TypeRepr as
-> TypeRepr r
-> ConcRegValue sym (FunctionHandleType as r)
-> IO (RegValue sym (FunctionHandleType as r))
concToSymFn sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm (Assignment TypeRepr as
as Assignment TypeRepr as
-> TypeRepr tp -> Assignment TypeRepr (as ::> tp)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> TypeRepr tp
vtp) TypeRepr r
r ConcFnVal (ExprBuilder scope st (Flags fm)) (as ::> tp) r
ConcRegValue sym (FunctionHandleType (as ::> tp) r)
clos
      FnVal (ExprBuilder scope st (Flags fm)) as r
-> IO (FnVal (ExprBuilder scope st (Flags fm)) as r)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (FnVal (ExprBuilder scope st (Flags fm)) (as ::> tp) r
-> TypeRepr tp
-> RegValue (ExprBuilder scope st (Flags fm)) tp
-> FnVal (ExprBuilder scope st (Flags fm)) as r
forall sym (args :: Ctx CrucibleType) (tp :: CrucibleType)
       (res :: CrucibleType).
FnVal sym (args ::> tp) res
-> TypeRepr tp -> RegValue sym tp -> FnVal sym args res
RV.ClosureFnVal FnVal (ExprBuilder scope st (Flags fm)) (as ::> tp) r
clos' TypeRepr tp
vtp RegValue (ExprBuilder scope st (Flags fm)) tp
v')

    ConcVarargsFnVal FnHandle (args ::> VectorType AnyType) r
hdl CtxRepr addlArgs
extra ->
      FnVal (ExprBuilder scope st (Flags fm)) as r
-> IO (FnVal (ExprBuilder scope st (Flags fm)) as r)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (FnHandle (args ::> VectorType AnyType) r
-> CtxRepr addlArgs
-> FnVal (ExprBuilder scope st (Flags fm)) (args <+> addlArgs) r
forall (args1 :: Ctx CrucibleType) (res :: CrucibleType)
       (addlArgs :: Ctx CrucibleType) sym.
FnHandle (args1 ::> VectorType AnyType) res
-> CtxRepr addlArgs -> FnVal sym (args1 <+> addlArgs) res
RV.VarargsFnVal FnHandle (args ::> VectorType AnyType) r
hdl CtxRepr addlArgs
extra)

    ConcHandleFnVal FnHandle as r
hdl ->
      FnVal (ExprBuilder scope st (Flags fm)) as r
-> IO (FnVal (ExprBuilder scope st (Flags fm)) as r)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (FnHandle as r -> FnVal (ExprBuilder scope st (Flags fm)) as r
forall (args :: Ctx CrucibleType) (res :: CrucibleType) sym.
FnHandle args res -> FnVal sym args res
RV.HandleFnVal FnHandle as r
hdl)

-- | Helper, not exported
concToSymIntrinsic ::
  W4I.IsExprBuilder sym =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  SymbolRepr nm ->
  CtxRepr ctx ->
  ConcRegValue sym (IntrinsicType nm ctx) ->
  IO (RegValue sym (IntrinsicType nm ctx))
concToSymIntrinsic :: forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
IsExprBuilder sym =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> SymbolRepr nm
-> CtxRepr ctx
-> ConcRegValue sym (IntrinsicType nm ctx)
-> IO (RegValue sym (IntrinsicType nm ctx))
concToSymIntrinsic sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns SymbolRepr nm
nm CtxRepr ctx
tyCtx ConcRegValue sym (IntrinsicType nm ctx)
v =
  case SymbolRepr nm
-> MapF SymbolRepr IntrinsicConcToSymFn
-> Maybe (IntrinsicConcToSymFn nm)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup SymbolRepr nm
nm MapF SymbolRepr IntrinsicConcToSymFn
iFns of
    Maybe (IntrinsicConcToSymFn nm)
Nothing ->
      let strNm :: String
strNm = Text -> String
Text.unpack (SymbolRepr nm -> Text
forall (nm :: Symbol). SymbolRepr nm -> Text
symbolRepr SymbolRepr nm
nm) in
      String -> IO (Intrinsic sym nm ctx)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
"Missing concretization function for intrinsic: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
strNm)
    Just (IntrinsicConcToSymFn forall sym (ctx :: Ctx CrucibleType).
IsExprBuilder sym =>
sym
-> Assignment TypeRepr ctx
-> ConcIntrinsic nm ctx
-> IO (RegValue sym (IntrinsicType nm ctx))
f) -> sym
-> CtxRepr ctx
-> ConcIntrinsic nm ctx
-> IO (RegValue sym (IntrinsicType nm ctx))
forall sym (ctx :: Ctx CrucibleType).
IsExprBuilder sym =>
sym
-> Assignment TypeRepr ctx
-> ConcIntrinsic nm ctx
-> IO (RegValue sym (IntrinsicType nm ctx))
f sym
sym CtxRepr ctx
tyCtx ConcIntrinsic nm ctx
ConcRegValue sym (IntrinsicType nm ctx)
v

-- | Helper, not exported
concToSymMaybe ::
  (sym ~ ExprBuilder scope st (Flags fm)) =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  FloatModeRepr fm ->
  TypeRepr tp ->
  ConcRegValue sym (MaybeType tp) ->
  IO (RegValue sym (MaybeType tp))
concToSymMaybe :: forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym (MaybeType tp)
-> IO (RegValue sym (MaybeType tp))
concToSymMaybe sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr tp
tp =
  \case
    Maybe (ConcRegValue (ExprBuilder scope st (Flags fm)) tp)
ConcRegValue sym (MaybeType tp)
Nothing -> PartialWithErr
  ()
  (Expr scope BaseBoolType)
  (RegValue (ExprBuilder scope st (Flags fm)) tp)
-> IO
     (PartialWithErr
        ()
        (Expr scope BaseBoolType)
        (RegValue (ExprBuilder scope st (Flags fm)) tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (()
-> PartialWithErr
     ()
     (Expr scope BaseBoolType)
     (RegValue (ExprBuilder scope st (Flags fm)) tp)
forall e p v. e -> PartialWithErr e p v
W4P.Err ())
    Just ConcRegValue (ExprBuilder scope st (Flags fm)) tp
v ->
      sym
-> RegValue (ExprBuilder scope st (Flags fm)) tp
-> PartExpr
     (Pred sym) (RegValue (ExprBuilder scope st (Flags fm)) tp)
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
W4P.justPartExpr sym
sym (RegValue (ExprBuilder scope st (Flags fm)) tp
 -> PartialWithErr
      ()
      (Expr scope BaseBoolType)
      (RegValue (ExprBuilder scope st (Flags fm)) tp))
-> IO (RegValue (ExprBuilder scope st (Flags fm)) tp)
-> IO
     (PartialWithErr
        ()
        (Expr scope BaseBoolType)
        (RegValue (ExprBuilder scope st (Flags fm)) tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
concToSym sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr tp
tp ConcRegValue sym tp
ConcRegValue (ExprBuilder scope st (Flags fm)) tp
v

-- | Helper, not exported
concToSymRef ::
  W4I.IsExprBuilder sym =>
  sym ->
  ConcRegValue sym (ReferenceType tp) ->
  IO (RegValue sym (ReferenceType tp))
concToSymRef :: forall sym (tp :: CrucibleType).
IsExprBuilder sym =>
sym
-> ConcRegValue sym (ReferenceType tp)
-> IO (RegValue sym (ReferenceType tp))
concToSymRef sym
sym (RefCell tp
v NE.:| [RefCell tp]
_) = MuxTree sym (RefCell tp) -> IO (MuxTree sym (RefCell tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (sym -> RefCell tp -> MuxTree sym (RefCell tp)
forall sym a. IsExprBuilder sym => sym -> a -> MuxTree sym a
MuxTree.toMuxTree sym
sym RefCell tp
v)

-- | Helper, not exported
concToSymVariant ::
  forall sym tps scope st fm.
  (sym ~ ExprBuilder scope st (Flags fm)) =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  FloatModeRepr fm ->
  CtxRepr tps ->
  ConcRegValue sym (VariantType tps) ->
  IO (RegValue sym (VariantType tps))
concToSymVariant :: forall sym (tps :: Ctx CrucibleType) scope (st :: Type -> Type)
       (fm :: FloatMode).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> CtxRepr tps
-> ConcRegValue sym (VariantType tps)
-> IO (RegValue sym (VariantType tps))
concToSymVariant sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm CtxRepr tps
tps ConcRegValue sym (VariantType tps)
v = (forall (x :: CrucibleType).
 TypeRepr x
 -> ConcVariantBranch (ExprBuilder scope st (Flags fm)) x
 -> IO (VariantBranch (ExprBuilder scope st (Flags fm)) x))
-> CtxRepr tps
-> Assignment
     (ConcVariantBranch (ExprBuilder scope st (Flags fm))) tps
-> IO
     (Assignment (VariantBranch (ExprBuilder scope st (Flags fm))) tps)
forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
       (h :: k -> Type) (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 TypeRepr x -> ConcVariantBranch sym x -> IO (VariantBranch sym x)
TypeRepr x
-> ConcVariantBranch (ExprBuilder scope st (Flags fm)) x
-> IO (VariantBranch (ExprBuilder scope st (Flags fm)) x)
forall (tp :: CrucibleType).
TypeRepr tp
-> ConcVariantBranch sym tp -> IO (VariantBranch sym tp)
forall (x :: CrucibleType).
TypeRepr x
-> ConcVariantBranch (ExprBuilder scope st (Flags fm)) x
-> IO (VariantBranch (ExprBuilder scope st (Flags fm)) x)
go CtxRepr tps
tps Assignment
  (ConcVariantBranch (ExprBuilder scope st (Flags fm))) tps
ConcRegValue sym (VariantType tps)
v
  where
    go :: forall tp. TypeRepr tp -> ConcVariantBranch sym tp -> IO (RV.VariantBranch sym tp)
    go :: forall (tp :: CrucibleType).
TypeRepr tp
-> ConcVariantBranch sym tp -> IO (VariantBranch sym tp)
go TypeRepr tp
tp (ConcVariantBranch Maybe (ConcRV' sym tp)
b) =
      case Maybe (ConcRV' sym tp)
b of
        Maybe (ConcRV' sym tp)
Nothing -> VariantBranch sym tp -> IO (VariantBranch sym tp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp
forall sym (tp :: CrucibleType).
PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp
RV.VB (()
-> PartialWithErr
     ()
     (Expr scope BaseBoolType)
     (RegValue (ExprBuilder scope st (Flags fm)) tp)
forall e p v. e -> PartialWithErr e p v
W4P.Err ()))
        Just (ConcRV' ConcRegValue sym tp
v') ->
          PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp
PartialWithErr
  ()
  (Expr scope BaseBoolType)
  (RegValue (ExprBuilder scope st (Flags fm)) tp)
-> VariantBranch sym tp
forall sym (tp :: CrucibleType).
PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp
RV.VB (PartialWithErr
   ()
   (Expr scope BaseBoolType)
   (RegValue (ExprBuilder scope st (Flags fm)) tp)
 -> VariantBranch sym tp)
-> (RegValue (ExprBuilder scope st (Flags fm)) tp
    -> PartialWithErr
         ()
         (Expr scope BaseBoolType)
         (RegValue (ExprBuilder scope st (Flags fm)) tp))
-> RegValue (ExprBuilder scope st (Flags fm)) tp
-> VariantBranch sym tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym
-> RegValue (ExprBuilder scope st (Flags fm)) tp
-> PartExpr
     (Pred sym) (RegValue (ExprBuilder scope st (Flags fm)) tp)
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
W4P.justPartExpr sym
sym (RegValue (ExprBuilder scope st (Flags fm)) tp
 -> VariantBranch sym tp)
-> IO (RegValue (ExprBuilder scope st (Flags fm)) tp)
-> IO (VariantBranch sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
concToSym sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr tp
tp ConcRegValue sym tp
v'

-- | Inject a 'ConcRegValue' back into a 'RegValue'.
concToSym ::
  (sym ~ ExprBuilder scope st (Flags fm)) =>
  sym ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  FloatModeRepr fm ->
  TypeRepr tp ->
  ConcRegValue sym tp ->
  IO (RegValue sym tp)
concToSym :: forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
concToSym sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr tp
tp ConcRegValue sym tp
v =
  case TypeRepr tp
tp of
    -- Base types
    TypeRepr tp
BoolRepr -> sym
-> BaseTypeRepr BaseBoolType
-> GroundValue BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym BaseTypeRepr BaseBoolType
BaseBoolRepr GroundValue BaseBoolType
ConcRegValue sym tp
v
    BVRepr NatRepr n
width -> sym
-> BaseTypeRepr (BaseBVType n)
-> GroundValue (BaseBVType n)
-> IO (SymExpr sym (BaseBVType n))
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym (NatRepr n -> BaseTypeRepr (BaseBVType n)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr n
width) GroundValue (BaseBVType n)
ConcRegValue sym tp
v
    TypeRepr tp
ComplexRealRepr -> sym
-> BaseTypeRepr BaseComplexType
-> GroundValue BaseComplexType
-> IO (SymExpr sym BaseComplexType)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym BaseTypeRepr BaseComplexType
BaseComplexRepr GroundValue BaseComplexType
ConcRegValue sym tp
v
    FloatRepr FloatInfoRepr flt
fi ->
      case FloatModeRepr fm
fm of
        FloatModeRepr fm
FloatIEEERepr ->
          sym
-> FloatPrecisionRepr (FloatInfoToPrecision flt)
-> BigFloat
-> IO (SymFloat sym (FloatInfoToPrecision flt))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
forall (fpp :: FloatPrecision).
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
W4I.floatLit sym
sym (FloatInfoRepr flt -> FloatPrecisionRepr (FloatInfoToPrecision flt)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> FloatPrecisionRepr (FloatInfoToPrecision fi)
floatInfoToPrecisionRepr FloatInfoRepr flt
fi) BigFloat
ConcRegValue sym tp
v
        FloatModeRepr fm
FloatUninterpretedRepr -> do
          Expr scope (BaseBVType (FloatInfoToBitWidth flt))
sv <- sym
-> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth flt))
-> GroundValue (BaseBVType (FloatInfoToBitWidth flt))
-> IO (SymExpr sym (BaseBVType (FloatInfoToBitWidth flt)))
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym (FloatInfoRepr flt
-> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth flt))
forall (fi :: FloatInfo).
FloatInfoRepr fi
-> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
floatInfoToBVTypeRepr FloatInfoRepr flt
fi) GroundValue (BaseBVType (FloatInfoToBitWidth flt))
ConcRegValue sym tp
v
          sym
-> FloatInfoRepr flt
-> SymExpr sym (BaseBVType (FloatInfoToBitWidth flt))
-> IO (SymInterpretedFloat sym flt)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
iFloatFromBinary sym
sym FloatInfoRepr flt
fi SymExpr sym (BaseBVType (FloatInfoToBitWidth flt))
Expr scope (BaseBVType (FloatInfoToBitWidth flt))
sv
        FloatModeRepr fm
FloatRealRepr ->
          sym
-> FloatInfoRepr flt
-> Rational
-> IO (SymInterpretedFloat sym flt)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
iFloatLitRational sym
sym FloatInfoRepr flt
fi Rational
ConcRegValue sym tp
v
    IEEEFloatRepr FloatPrecisionRepr ps
fpp -> sym
-> BaseTypeRepr (BaseFloatType ps)
-> GroundValue (BaseFloatType ps)
-> IO (SymExpr sym (BaseFloatType ps))
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym (FloatPrecisionRepr ps -> BaseTypeRepr (BaseFloatType ps)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr ps
fpp) GroundValue (BaseFloatType ps)
ConcRegValue sym tp
v
    TypeRepr tp
IntegerRepr -> sym
-> BaseTypeRepr BaseIntegerType
-> GroundValue BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym BaseTypeRepr BaseIntegerType
BaseIntegerRepr GroundValue BaseIntegerType
ConcRegValue sym tp
v
    TypeRepr tp
NatRepr -> sym -> SymExpr sym BaseIntegerType -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymNat sym)
W4I.integerToNat sym
sym (Expr scope BaseIntegerType -> IO (SymNat sym))
-> IO (Expr scope BaseIntegerType) -> IO (SymNat sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> BaseTypeRepr BaseIntegerType
-> GroundValue BaseIntegerType
-> IO (SymExpr sym BaseIntegerType)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym BaseTypeRepr BaseIntegerType
BaseIntegerRepr GroundValue BaseIntegerType
ConcRegValue sym tp
v
    TypeRepr tp
RealValRepr -> sym
-> BaseTypeRepr BaseRealType
-> GroundValue BaseRealType
-> IO (SymExpr sym BaseRealType)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym BaseTypeRepr BaseRealType
BaseRealRepr GroundValue BaseRealType
ConcRegValue sym tp
v
    StringRepr StringInfoRepr si
si -> sym
-> BaseTypeRepr (BaseStringType si)
-> GroundValue (BaseStringType si)
-> IO (SymExpr sym (BaseStringType si))
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym (StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr ('BaseStringType si)
BaseStringRepr StringInfoRepr si
si) GroundValue (BaseStringType si)
ConcRegValue sym tp
v
    SymbolicArrayRepr Assignment BaseTypeRepr (idx ::> tp1)
idxs BaseTypeRepr t
tp' -> sym
-> BaseTypeRepr (BaseArrayType (idx ::> tp1) t)
-> GroundValue (BaseArrayType (idx ::> tp1) t)
-> IO (SymExpr sym (BaseArrayType (idx ::> tp1) t))
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym (Assignment BaseTypeRepr (idx ::> tp1)
-> BaseTypeRepr t -> BaseTypeRepr (BaseArrayType (idx ::> tp1) t)
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr ('BaseArrayType (idx ::> tp) xs)
BaseArrayRepr Assignment BaseTypeRepr (idx ::> tp1)
idxs BaseTypeRepr t
tp') GroundValue (BaseArrayType (idx ::> tp1) t)
ConcRegValue sym tp
v
    SymbolicStructRepr Assignment BaseTypeRepr ctx
tys -> sym
-> BaseTypeRepr (BaseStructType ctx)
-> GroundValue (BaseStructType ctx)
-> IO (SymExpr sym (BaseStructType ctx))
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym (Assignment BaseTypeRepr ctx -> BaseTypeRepr (BaseStructType ctx)
forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr ('BaseStructType ctx)
BaseStructRepr Assignment BaseTypeRepr ctx
tys) GroundValue (BaseStructType ctx)
ConcRegValue sym tp
v

    -- Trivial cases
    TypeRepr tp
UnitRepr -> () -> IO ()
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
    TypeRepr tp
CharRepr -> Word16 -> IO Word16
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Word16
ConcRegValue sym tp
v

    -- Simple recursive cases
    RecursiveRepr SymbolRepr nm
symb CtxRepr ctx
tyCtx ->
      RegValue (ExprBuilder scope st (Flags fm)) (UnrollType nm ctx)
-> RolledType (ExprBuilder scope st (Flags fm)) nm ctx
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
RegValue sym (UnrollType nm ctx) -> RolledType sym nm ctx
RV.RolledType (RegValue (ExprBuilder scope st (Flags fm)) (UnrollType nm ctx)
 -> RolledType (ExprBuilder scope st (Flags fm)) nm ctx)
-> IO
     (RegValue (ExprBuilder scope st (Flags fm)) (UnrollType nm ctx))
-> IO (RolledType (ExprBuilder scope st (Flags fm)) nm ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr (UnrollType nm ctx)
-> ConcRegValue sym (UnrollType nm ctx)
-> IO (RegValue sym (UnrollType nm ctx))
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
concToSym sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm (SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
IsRecursiveType nm =>
SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
forall (ctx :: Ctx CrucibleType).
SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
unrollType SymbolRepr nm
symb CtxRepr ctx
tyCtx) ConcRegValue sym tp
ConcRegValue sym (UnrollType nm ctx)
v
    SequenceRepr TypeRepr tp1
tp' -> do
      [RegValue (ExprBuilder scope st (Flags fm)) tp1]
l <- (ConcRV' (ExprBuilder scope st (Flags fm)) tp1
 -> IO (RegValue (ExprBuilder scope st (Flags fm)) tp1))
-> [ConcRV' (ExprBuilder scope st (Flags fm)) tp1]
-> IO [RegValue (ExprBuilder scope st (Flags fm)) tp1]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp1
-> ConcRegValue sym tp1
-> IO (RegValue sym tp1)
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
concToSym sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr tp1
tp' (ConcRegValue (ExprBuilder scope st (Flags fm)) tp1
 -> IO (RegValue (ExprBuilder scope st (Flags fm)) tp1))
-> (ConcRV' (ExprBuilder scope st (Flags fm)) tp1
    -> ConcRegValue (ExprBuilder scope st (Flags fm)) tp1)
-> ConcRV' (ExprBuilder scope st (Flags fm)) tp1
-> IO (RegValue (ExprBuilder scope st (Flags fm)) tp1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConcRV' (ExprBuilder scope st (Flags fm)) tp1
-> ConcRegValue (ExprBuilder scope st (Flags fm)) tp1
forall sym (tp :: CrucibleType).
ConcRV' sym tp -> ConcRegValue sym tp
unConcRV') (Seq (ConcRV' (ExprBuilder scope st (Flags fm)) tp1)
-> [ConcRV' (ExprBuilder scope st (Flags fm)) tp1]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
F.toList Seq (ConcRV' (ExprBuilder scope st (Flags fm)) tp1)
ConcRegValue sym tp
v)
      sym
-> [RegValue (ExprBuilder scope st (Flags fm)) tp1]
-> IO
     (SymSequence sym (RegValue (ExprBuilder scope st (Flags fm)) tp1))
forall sym a. sym -> [a] -> IO (SymSequence sym a)
SymSeq.fromListSymSequence sym
sym [RegValue (ExprBuilder scope st (Flags fm)) tp1]
l
    StringMapRepr TypeRepr tp1
tp' ->
      (ConcRV' (ExprBuilder scope st (Flags fm)) tp1
 -> IO
      (PartExpr
         (Expr scope BaseBoolType)
         (RegValue (ExprBuilder scope st (Flags fm)) tp1)))
-> Map Text (ConcRV' (ExprBuilder scope st (Flags fm)) tp1)
-> IO
     (Map
        Text
        (PartExpr
           (Expr scope BaseBoolType)
           (RegValue (ExprBuilder scope st (Flags fm)) tp1)))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Map Text a -> f (Map Text b)
traverse ((RegValue (ExprBuilder scope st (Flags fm)) tp1
 -> PartExpr
      (Expr scope BaseBoolType)
      (RegValue (ExprBuilder scope st (Flags fm)) tp1))
-> IO (RegValue (ExprBuilder scope st (Flags fm)) tp1)
-> IO
     (PartExpr
        (Expr scope BaseBoolType)
        (RegValue (ExprBuilder scope st (Flags fm)) tp1))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (sym
-> RegValue (ExprBuilder scope st (Flags fm)) tp1
-> PartExpr
     (SymExpr sym BaseBoolType)
     (RegValue (ExprBuilder scope st (Flags fm)) tp1)
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
W4P.justPartExpr sym
sym) (IO (RegValue (ExprBuilder scope st (Flags fm)) tp1)
 -> IO
      (PartExpr
         (Expr scope BaseBoolType)
         (RegValue (ExprBuilder scope st (Flags fm)) tp1)))
-> (ConcRV' (ExprBuilder scope st (Flags fm)) tp1
    -> IO (RegValue (ExprBuilder scope st (Flags fm)) tp1))
-> ConcRV' (ExprBuilder scope st (Flags fm)) tp1
-> IO
     (PartExpr
        (Expr scope BaseBoolType)
        (RegValue (ExprBuilder scope st (Flags fm)) tp1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp1
-> ConcRegValue sym tp1
-> IO (RegValue sym tp1)
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
concToSym sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr tp1
tp' (ConcRegValue (ExprBuilder scope st (Flags fm)) tp1
 -> IO (RegValue (ExprBuilder scope st (Flags fm)) tp1))
-> (ConcRV' (ExprBuilder scope st (Flags fm)) tp1
    -> ConcRegValue (ExprBuilder scope st (Flags fm)) tp1)
-> ConcRV' (ExprBuilder scope st (Flags fm)) tp1
-> IO (RegValue (ExprBuilder scope st (Flags fm)) tp1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConcRV' (ExprBuilder scope st (Flags fm)) tp1
-> ConcRegValue (ExprBuilder scope st (Flags fm)) tp1
forall sym (tp :: CrucibleType).
ConcRV' sym tp -> ConcRegValue sym tp
unConcRV') Map Text (ConcRV' (ExprBuilder scope st (Flags fm)) tp1)
ConcRegValue sym tp
v
    StructRepr CtxRepr ctx
tps ->
      (forall (x :: CrucibleType).
 TypeRepr x
 -> ConcRV' (ExprBuilder scope st (Flags fm)) x
 -> IO (RegValue' (ExprBuilder scope st (Flags fm)) x))
-> CtxRepr ctx
-> Assignment (ConcRV' (ExprBuilder scope st (Flags fm))) ctx
-> IO
     (Assignment (RegValue' (ExprBuilder scope st (Flags fm))) ctx)
forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
       (h :: k -> Type) (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 (\TypeRepr x
tp' (ConcRV' ConcRegValue (ExprBuilder scope st (Flags fm)) x
v') -> RegValue (ExprBuilder scope st (Flags fm)) x
-> RegValue' (ExprBuilder scope st (Flags fm)) x
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV.RV (RegValue (ExprBuilder scope st (Flags fm)) x
 -> RegValue' (ExprBuilder scope st (Flags fm)) x)
-> IO (RegValue (ExprBuilder scope st (Flags fm)) x)
-> IO (RegValue' (ExprBuilder scope st (Flags fm)) x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr x
-> ConcRegValue sym x
-> IO (RegValue sym x)
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
concToSym sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr x
tp' ConcRegValue sym x
ConcRegValue (ExprBuilder scope st (Flags fm)) x
v') CtxRepr ctx
tps Assignment (ConcRV' (ExprBuilder scope st (Flags fm))) ctx
ConcRegValue sym tp
v
    VectorRepr TypeRepr tp1
tp' ->
      (ConcRV' (ExprBuilder scope st (Flags fm)) tp1
 -> IO (RegValue (ExprBuilder scope st (Flags fm)) tp1))
-> Vector (ConcRV' (ExprBuilder scope st (Flags fm)) tp1)
-> IO (Vector (RegValue (ExprBuilder scope st (Flags fm)) tp1))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse (sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp1
-> ConcRegValue sym tp1
-> IO (RegValue sym tp1)
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym tp
-> IO (RegValue sym tp)
concToSym sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr tp1
tp' (ConcRegValue (ExprBuilder scope st (Flags fm)) tp1
 -> IO (RegValue (ExprBuilder scope st (Flags fm)) tp1))
-> (ConcRV' (ExprBuilder scope st (Flags fm)) tp1
    -> ConcRegValue (ExprBuilder scope st (Flags fm)) tp1)
-> ConcRV' (ExprBuilder scope st (Flags fm)) tp1
-> IO (RegValue (ExprBuilder scope st (Flags fm)) tp1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConcRV' (ExprBuilder scope st (Flags fm)) tp1
-> ConcRegValue (ExprBuilder scope st (Flags fm)) tp1
forall sym (tp :: CrucibleType).
ConcRV' sym tp -> ConcRegValue sym tp
unConcRV') Vector (ConcRV' (ExprBuilder scope st (Flags fm)) tp1)
ConcRegValue sym tp
v

    -- Cases with helper functions
    TypeRepr tp
AnyRepr -> sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> ConcRegValue sym AnyType
-> IO (RegValue sym AnyType)
forall sym scope (st :: Type -> Type) (fm :: FloatMode).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> ConcRegValue sym AnyType
-> IO (RegValue sym AnyType)
concToSymAny sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm ConcRegValue sym tp
ConcRegValue sym AnyType
v
    MaybeRepr TypeRepr tp1
tp' -> sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp1
-> ConcRegValue sym ('MaybeType tp1)
-> IO (RegValue sym ('MaybeType tp1))
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (tp :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue sym (MaybeType tp)
-> IO (RegValue sym (MaybeType tp))
concToSymMaybe sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm TypeRepr tp1
tp' ConcRegValue sym tp
ConcRegValue sym ('MaybeType tp1)
v
    FunctionHandleRepr CtxRepr ctx
args TypeRepr ret
ret -> sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> CtxRepr ctx
-> TypeRepr ret
-> ConcRegValue sym ('FunctionHandleType ctx ret)
-> IO (RegValue sym ('FunctionHandleType ctx ret))
forall sym scope (st :: Type -> Type) (fm :: FloatMode)
       (as :: Ctx CrucibleType) (r :: CrucibleType).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> Assignment TypeRepr as
-> TypeRepr r
-> ConcRegValue sym (FunctionHandleType as r)
-> IO (RegValue sym (FunctionHandleType as r))
concToSymFn sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm CtxRepr ctx
args TypeRepr ret
ret ConcRegValue sym tp
ConcRegValue sym ('FunctionHandleType ctx ret)
v
    IntrinsicRepr SymbolRepr nm
nm CtxRepr ctx
tyCtx -> sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> SymbolRepr nm
-> CtxRepr ctx
-> ConcRegValue sym ('IntrinsicType nm ctx)
-> IO (RegValue sym ('IntrinsicType nm ctx))
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
IsExprBuilder sym =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> SymbolRepr nm
-> CtxRepr ctx
-> ConcRegValue sym (IntrinsicType nm ctx)
-> IO (RegValue sym (IntrinsicType nm ctx))
concToSymIntrinsic sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns SymbolRepr nm
nm CtxRepr ctx
tyCtx ConcRegValue sym tp
ConcRegValue sym ('IntrinsicType nm ctx)
v
    ReferenceRepr TypeRepr a
_tp' -> sym
-> ConcRegValue sym ('ReferenceType a)
-> IO (RegValue sym ('ReferenceType a))
forall sym (tp :: CrucibleType).
IsExprBuilder sym =>
sym
-> ConcRegValue sym (ReferenceType tp)
-> IO (RegValue sym (ReferenceType tp))
concToSymRef sym
sym ConcRegValue sym tp
ConcRegValue sym ('ReferenceType a)
v
    VariantRepr CtxRepr ctx
tps -> sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> CtxRepr ctx
-> ConcRegValue sym ('VariantType ctx)
-> IO (RegValue sym ('VariantType ctx))
forall sym (tps :: Ctx CrucibleType) scope (st :: Type -> Type)
       (fm :: FloatMode).
(sym ~ ExprBuilder scope st (Flags fm)) =>
sym
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> CtxRepr tps
-> ConcRegValue sym (VariantType tps)
-> IO (RegValue sym (VariantType tps))
concToSymVariant sym
sym MapF SymbolRepr IntrinsicConcToSymFn
iFns FloatModeRepr fm
fm CtxRepr ctx
tps ConcRegValue sym tp
ConcRegValue sym ('VariantType ctx)
v

    -- Incomplete cases
    WordMapRepr NatRepr n
_ BaseTypeRepr tp1
_ -> String -> IO (WordMap (ExprBuilder scope st (Flags fm)) n tp1)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"concToSym does not yet support WordMap"