-----------------------------------------------------------------------
-- |
-- 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 three different kinds of functions. In order of how much
-- work they perform:
--
-- * /Grounding/ functions (e.g., 'groundRegValue') take symbolic values
--   ('RegValue's) and a model from an SMT solver ('W4GE.GroundEvalFn'), and
--   return the concrete value ('ConcRegValue') that the symbolic value takes in
--   the model. These functions can be used to report specific values that lead
--   to violations of assertions, including safety assertions.
-- * /Concretization/ functions (e.g., 'concRegValue') request a model that is
--   consistent with the current assumptions (e.g., path conditions) from the
--   symbolic backend, and then ground a value in that model. These can be used
--   to reduce the size and complexity of later queries to SMT solvers, at the
--   cost of no longer being sound from a verification standpoint.
-- * /Unique concretization/ functions (e.g., 'uniquelyConcRegValue') do the
--   same thing as concretization functions, but then check if the concrete
--   value is the /only possible/ value for the given symbolic expression in
--   /any/ model.
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# 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'(..)
  , asConcRegValue
  , asConcRegEntry
  , asConcRegMap
  , ConcAnyValue(..)
  , ConcIntrinsic
  , IntrinsicConcFn(..)
  , ConcCtx(..)
    -- * Grounding
  , groundRegValue
  , groundRegEntry
  , groundRegMap
    -- * Concretization
  , concRegValue
  , concRegEntry
  , concRegMap
    -- * Unique concretization
  , uniquelyConcRegValue
  , uniquelyConcRegEntry
  , uniquelyConcRegMap
    -- * There and back again
  , IntrinsicConcToSymFn(..)
  , concToSym
  ) where

import qualified Data.Foldable as F
import           Data.Functor.Const (Const(..))
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.Proxy (Proxy(Proxy))
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, foldlMFC)

import qualified What4.Concretize as W4C
import qualified What4.Config as W4Cfg
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 qualified What4.Protocol.Online as WPO
import qualified What4.SatResult as WSat

import qualified Lang.Crucible.Backend as CB
import qualified Lang.Crucible.Backend.Online as CBO
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 'groundRegValue'.
--
-- 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)

-- | Check if a 'RegValue' is actually concrete
asConcRegValue ::
  W4I.IsExpr (SymExpr sym) =>
  proxy sym ->
  TypeRepr tp ->
  RegValue sym tp ->
  Maybe (ConcRegValue sym tp)
asConcRegValue :: forall sym (proxy :: Type -> Type) (tp :: CrucibleType).
IsExpr (SymExpr sym) =>
proxy sym
-> TypeRepr tp -> RegValue sym tp -> Maybe (ConcRegValue sym tp)
asConcRegValue proxy sym
_proxy TypeRepr tp
tp RegValue sym tp
val =
  -- TODO: More cases could be added here.
  case TypeRepr tp -> AsBaseType tp
forall (tp :: CrucibleType). TypeRepr tp -> AsBaseType tp
asBaseType TypeRepr tp
tp of
    AsBaseType {} -> SymExpr sym bt -> Maybe (GroundValue bt)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> Maybe (GroundValue tp)
W4GE.asGround SymExpr sym bt
RegValue sym tp
val
    AsBaseType tp
_ -> Maybe (ConcRegValue sym tp)
forall a. Maybe a
Nothing

-- | Check if a 'RM.RegEntry' is actually concrete
asConcRegEntry ::
  forall sym tp.
  W4I.IsExpr (SymExpr sym) =>
  RM.RegEntry sym tp ->
  Maybe (ConcRegValue sym tp)
asConcRegEntry :: forall sym (tp :: CrucibleType).
IsExpr (SymExpr sym) =>
RegEntry sym tp -> Maybe (ConcRegValue sym tp)
asConcRegEntry (RM.RegEntry TypeRepr tp
t RegValue sym tp
v) = Proxy sym
-> TypeRepr tp -> RegValue sym tp -> Maybe (ConcRegValue sym tp)
forall sym (proxy :: Type -> Type) (tp :: CrucibleType).
IsExpr (SymExpr sym) =>
proxy sym
-> TypeRepr tp -> RegValue sym tp -> Maybe (ConcRegValue sym tp)
asConcRegValue (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @sym) TypeRepr tp
t RegValue sym tp
v

-- | Check if a 'RM.RegMap' is actually concrete
asConcRegMap ::
  forall sym tp.
  W4I.IsExpr (SymExpr sym) =>
  RM.RegMap sym tp ->
  Maybe (Ctx.Assignment (ConcRV' sym) tp)
asConcRegMap :: forall sym (tp :: Ctx CrucibleType).
IsExpr (SymExpr sym) =>
RegMap sym tp -> Maybe (Assignment (ConcRV' sym) tp)
asConcRegMap (RM.RegMap Assignment (RegEntry sym) tp
assign) =
  (forall (x :: CrucibleType).
 RegEntry sym x -> Maybe (ConcRV' sym x))
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> Maybe (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 (\RegEntry sym x
re -> ConcRegValue sym x -> ConcRV' sym x
forall sym (tp :: CrucibleType).
ConcRegValue sym tp -> ConcRV' sym tp
ConcRV' (ConcRegValue sym x -> ConcRV' sym x)
-> Maybe (ConcRegValue sym x) -> Maybe (ConcRV' sym x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RegEntry sym x -> Maybe (ConcRegValue sym x)
forall sym (tp :: CrucibleType).
IsExpr (SymExpr sym) =>
RegEntry sym tp -> Maybe (ConcRegValue sym tp)
asConcRegEntry RegEntry sym x
re) Assignment (RegEntry sym) tp
assign

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

-- | Context needed for 'groundRegValue'
--
-- 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)
groundRegValue 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 'groundRegValue'
data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRV' sym tp)

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

-- | A 'FnVal' concretized by 'groundRegValue'
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)
groundRegValue 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)
groundRegValue 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 'groundRegValue'
-- 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)

---------------------------------------------------------------------
-- * 'groundRegValue'

-- | 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.
groundRegValue ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  TypeRepr tp ->
  RegValue sym tp ->
  IO (ConcRegValue sym tp)
groundRegValue :: forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> TypeRepr tp -> RegValue sym tp -> IO (ConcRegValue sym tp)
groundRegValue 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)
groundRegValue 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)
groundRegValue 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)
groundRegValue 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)
groundRegValue 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 'groundRegValue', but for 'RegEntry'
groundRegEntry ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  RegEntry sym tp ->
  IO (ConcRegValue sym tp)
groundRegEntry :: forall sym t (tp :: CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t -> RegEntry sym tp -> IO (ConcRegValue sym tp)
groundRegEntry 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)
groundRegValue 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 'groundRegEntry', but for a whole 'RegMap'
groundRegMap ::
  (SymExpr sym ~ Expr t) =>
  W4I.IsExprBuilder sym =>
  ConcCtx sym t ->
  RegMap sym tps ->
  IO (Ctx.Assignment (ConcRV' sym) tps)
groundRegMap :: forall sym t (tps :: Ctx CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> RegMap sym tps -> IO (Assignment (ConcRV' sym) tps)
groundRegMap 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)
groundRegEntry ConcCtx sym t
ctx) Assignment (RegEntry sym) tps
m

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

-- | Generate a model and pick a feasible concrete value from it
concRegValue ::
  forall tp sym bak solver scope st fs.
  ( CB.IsSymBackend sym bak
  , sym ~ ExprBuilder scope st fs
  , SymExpr sym ~ Expr scope
  , bak ~ CBO.OnlineBackend solver scope st fs
  , WPO.OnlineSolver solver
  ) =>
  bak ->
  MapF SymbolRepr (IntrinsicConcFn scope) ->
  TypeRepr tp ->
  RegValue sym tp ->
  IO (Either W4C.ConcretizationFailure (ConcRegValue sym tp))
concRegValue :: forall (tp :: CrucibleType) sym bak solver scope
       (st :: Type -> Type) fs.
(IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs,
 OnlineSolver solver) =>
bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> TypeRepr tp
-> RegValue sym tp
-> IO (Either ConcretizationFailure (ConcRegValue sym tp))
concRegValue bak
bak MapF SymbolRepr (IntrinsicConcFn scope)
iFns TypeRepr tp
tp RegValue sym tp
v = bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> RegEntry (ExprBuilder scope st fs) tp
-> IO
     (Either
        ConcretizationFailure (ConcRegValue (ExprBuilder scope st fs) tp))
forall (tp :: CrucibleType) sym bak solver scope
       (st :: Type -> Type) fs.
(IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs,
 OnlineSolver solver) =>
bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> RegEntry sym tp
-> IO (Either ConcretizationFailure (ConcRegValue sym tp))
concRegEntry bak
bak MapF SymbolRepr (IntrinsicConcFn scope)
iFns (TypeRepr tp
-> RegValue (ExprBuilder scope st fs) tp
-> RegEntry (ExprBuilder scope st fs) tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RM.RegEntry TypeRepr tp
tp RegValue sym tp
RegValue (ExprBuilder scope st fs) tp
v)

-- | Generate a model and pick a feasible concrete value from it
concRegEntry ::
  forall tp sym bak solver scope st fs.
  ( CB.IsSymBackend sym bak
  , sym ~ ExprBuilder scope st fs
  , SymExpr sym ~ Expr scope
  , bak ~ CBO.OnlineBackend solver scope st fs
  , WPO.OnlineSolver solver
  ) =>
  bak ->
  MapF SymbolRepr (IntrinsicConcFn scope) ->
  RM.RegEntry sym tp ->
  IO (Either W4C.ConcretizationFailure (ConcRegValue sym tp))
concRegEntry :: forall (tp :: CrucibleType) sym bak solver scope
       (st :: Type -> Type) fs.
(IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs,
 OnlineSolver solver) =>
bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> RegEntry sym tp
-> IO (Either ConcretizationFailure (ConcRegValue sym tp))
concRegEntry bak
bak MapF SymbolRepr (IntrinsicConcFn scope)
iFns RegEntry sym tp
re = do
  Either
  ConcretizationFailure (Assignment (ConcRV' sym) (EmptyCtx ::> tp))
res <- bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> RegMap sym (EmptyCtx ::> tp)
-> IO
     (Either
        ConcretizationFailure (Assignment (ConcRV' sym) (EmptyCtx ::> tp)))
forall (tps :: Ctx CrucibleType) sym bak solver scope
       (st :: Type -> Type) fs.
(IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs,
 OnlineSolver solver) =>
bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> RegMap sym tps
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
concRegMap bak
bak MapF SymbolRepr (IntrinsicConcFn scope)
iFns (Assignment (RegEntry sym) (EmptyCtx ::> tp)
-> RegMap sym (EmptyCtx ::> tp)
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RM.RegMap (RegEntry sym tp -> Assignment (RegEntry sym) (EmptyCtx ::> tp)
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton RegEntry sym tp
re))
  case Either
  ConcretizationFailure (Assignment (ConcRV' sym) (EmptyCtx ::> tp))
res of
    Left ConcretizationFailure
e -> Either
  ConcretizationFailure (ConcRegValue (ExprBuilder scope st fs) tp)
-> IO
     (Either
        ConcretizationFailure (ConcRegValue (ExprBuilder scope st fs) tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ConcretizationFailure
-> Either
     ConcretizationFailure (ConcRegValue (ExprBuilder scope st fs) tp)
forall a b. a -> Either a b
Left ConcretizationFailure
e)
    Right (Assignment (ConcRV' sym) ctx
Ctx.Empty Ctx.:> ConcRV' ConcRegValue sym tp
concV) -> Either
  ConcretizationFailure (ConcRegValue (ExprBuilder scope st fs) tp)
-> IO
     (Either
        ConcretizationFailure (ConcRegValue (ExprBuilder scope st fs) tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ConcRegValue (ExprBuilder scope st fs) tp
-> Either
     ConcretizationFailure (ConcRegValue (ExprBuilder scope st fs) tp)
forall a b. b -> Either a b
Right ConcRegValue sym tp
ConcRegValue (ExprBuilder scope st fs) tp
concV)

-- | Like 'concRegValue', but for a whole 'RegMap'
concRegMap ::
  forall tps sym bak solver scope st fs.
  ( CB.IsSymBackend sym bak
  , sym ~ ExprBuilder scope st fs
  , SymExpr sym ~ Expr scope
  , bak ~ CBO.OnlineBackend solver scope st fs
  , WPO.OnlineSolver solver
  ) =>
  bak ->
  MapF SymbolRepr (IntrinsicConcFn scope) ->
  RegMap sym tps ->
  IO (Either W4C.ConcretizationFailure (Ctx.Assignment (ConcRV' sym) tps))
concRegMap :: forall (tps :: Ctx CrucibleType) sym bak solver scope
       (st :: Type -> Type) fs.
(IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs,
 OnlineSolver solver) =>
bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> RegMap sym tps
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
concRegMap bak
bak MapF SymbolRepr (IntrinsicConcFn scope)
iFns RegMap sym tps
m = do
  case RegMap sym tps -> Maybe (Assignment (ConcRV' sym) tps)
forall sym (tp :: Ctx CrucibleType).
IsExpr (SymExpr sym) =>
RegMap sym tp -> Maybe (Assignment (ConcRV' sym) tp)
asConcRegMap RegMap sym tps
m of
    Just Assignment (ConcRV' sym) tps
concM -> Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Assignment (ConcRV' sym) tps
-> Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
forall a b. b -> Either a b
Right Assignment (ConcRV' sym) tps
concM)
    Maybe (Assignment (ConcRV' sym) tps)
Nothing ->
      IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
withEnabledOnline (IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
 -> IO
      (Either ConcretizationFailure (Assignment (ConcRV' sym) tps)))
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a b. (a -> b) -> a -> b
$ do
        let err :: a
err = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"concRegValue" [String
"requires online solving to be enabled"]
        BoolExpr scope
cond <- bak -> IO (Pred (ExprBuilder scope st fs))
forall sym bak. IsSymBackend sym bak => bak -> IO (Pred sym)
CB.getPathCondition bak
bak
        OnlineBackend solver scope st fs
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
-> (SolverProcess scope solver
    -> IO
         (Either ConcretizationFailure (Assignment (ConcRV' sym) tps)))
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall solver scope (st :: Type -> Type) fs a.
OnlineSolver solver =>
OnlineBackend solver scope st fs
-> IO a -> (SolverProcess scope solver -> IO a) -> IO a
CBO.withSolverProcess bak
OnlineBackend solver scope st fs
bak IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall {a}. a
err ((SolverProcess scope solver
  -> IO
       (Either ConcretizationFailure (Assignment (ConcRV' sym) tps)))
 -> IO
      (Either ConcretizationFailure (Assignment (ConcRV' sym) tps)))
-> (SolverProcess scope solver
    -> IO
         (Either ConcretizationFailure (Assignment (ConcRV' sym) tps)))
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a b. (a -> b) -> a -> b
$ \SolverProcess scope solver
sp -> do
          SatResult (GroundEvalFn scope) ()
msat <- SolverProcess scope solver
-> String
-> [BoolExpr scope]
-> IO (SatResult (GroundEvalFn scope) ())
forall solver scope.
SMTReadWriter solver =>
SolverProcess scope solver
-> String
-> [BoolExpr scope]
-> IO (SatResult (GroundEvalFn scope) ())
WPO.checkWithAssumptionsAndModel SolverProcess scope solver
sp String
"concRegValue" [BoolExpr scope
cond]
          case SatResult (GroundEvalFn scope) ()
msat of
            SatResult (GroundEvalFn scope) ()
WSat.Unknown -> Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
 -> IO
      (Either ConcretizationFailure (Assignment (ConcRV' sym) tps)))
-> Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a b. (a -> b) -> a -> b
$ ConcretizationFailure
-> Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
forall a b. a -> Either a b
Left ConcretizationFailure
W4C.SolverUnknown
            WSat.Unsat {} -> Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
 -> IO
      (Either ConcretizationFailure (Assignment (ConcRV' sym) tps)))
-> Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a b. (a -> b) -> a -> b
$ ConcretizationFailure
-> Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
forall a b. a -> Either a b
Left ConcretizationFailure
W4C.UnsatInitialAssumptions
            WSat.Sat GroundEvalFn scope
mdl -> do
              let ctx :: ConcCtx sym scope
ctx = ConcCtx { model :: GroundEvalFn scope
model = GroundEvalFn scope
mdl, intrinsicConcFuns :: MapF SymbolRepr (IntrinsicConcFn scope)
intrinsicConcFuns = MapF SymbolRepr (IntrinsicConcFn scope)
iFns }
              Assignment (ConcRV' sym) tps
expr <- forall sym t (tps :: Ctx CrucibleType).
(SymExpr sym ~ Expr t, IsExprBuilder sym) =>
ConcCtx sym t
-> RegMap sym tps -> IO (Assignment (ConcRV' sym) tps)
groundRegMap @sym ConcCtx sym scope
ctx RegMap sym tps
m
              Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Assignment (ConcRV' sym) tps
-> Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
forall a b. b -> Either a b
Right Assignment (ConcRV' sym) tps
expr)
  where
    withEnabledOnline :: IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
withEnabledOnline IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
f = do
      let sym :: ExprBuilder scope st fs
sym = bak -> ExprBuilder scope st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
CB.backendGetSym bak
bak
      let conf :: Config
conf = ExprBuilder scope st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
W4I.getConfiguration ExprBuilder scope st fs
sym
      OptionSetting BaseBoolType
enabledOpt <- ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
W4Cfg.getOptionSetting ConfigOption BaseBoolType
CBO.enableOnlineBackend Config
conf
      Bool
wasEnabled <- OptionSetting BaseBoolType -> IO Bool
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
W4Cfg.getOpt OptionSetting BaseBoolType
enabledOpt
      [Doc Void]
_ <- OptionSetting BaseBoolType -> Bool -> IO [Doc Void]
forall (tp :: BaseType) a.
Opt tp a =>
OptionSetting tp -> a -> IO [Doc Void]
W4Cfg.setOpt OptionSetting BaseBoolType
enabledOpt Bool
True
      Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
r <- IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
f
      [Doc Void]
_ <- OptionSetting BaseBoolType -> Bool -> IO [Doc Void]
forall (tp :: BaseType) a.
Opt tp a =>
OptionSetting tp -> a -> IO [Doc Void]
W4Cfg.setOpt OptionSetting BaseBoolType
enabledOpt Bool
wasEnabled
      Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
r

---------------------------------------------------------------------
-- * 'uniquelyConcRegValue'

-- | Generate a model and pick a feasible concrete value from it
uniquelyConcRegValue ::
  forall tp sym bak solver scope st fm.
  ( CB.IsSymBackend sym bak
  , sym ~ ExprBuilder scope st (Flags fm)
  , SymExpr sym ~ Expr scope
  , bak ~ CBO.OnlineBackend solver scope st (Flags fm)
  , WPO.OnlineSolver solver
  ) =>
  bak ->
  FloatModeRepr fm ->
  MapF SymbolRepr (IntrinsicConcFn scope) ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  TypeRepr tp ->
  RegValue sym tp ->
  IO (Either W4C.UniqueConcretizationFailure (ConcRegValue sym tp))
uniquelyConcRegValue :: forall (tp :: CrucibleType) sym bak solver scope
       (st :: Type -> Type) (fm :: FloatMode).
(IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm),
 SymExpr sym ~ Expr scope,
 bak ~ OnlineBackend solver scope st (Flags fm),
 OnlineSolver solver) =>
bak
-> FloatModeRepr fm
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> MapF SymbolRepr IntrinsicConcToSymFn
-> TypeRepr tp
-> RegValue sym tp
-> IO (Either UniqueConcretizationFailure (ConcRegValue sym tp))
uniquelyConcRegValue bak
bak FloatModeRepr fm
fm MapF SymbolRepr (IntrinsicConcFn scope)
iFns MapF SymbolRepr IntrinsicConcToSymFn
sFns TypeRepr tp
tp RegValue sym tp
v =
  bak
-> FloatModeRepr fm
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> MapF SymbolRepr IntrinsicConcToSymFn
-> RegEntry (ExprBuilder scope st (Flags fm)) tp
-> IO
     (Either
        UniqueConcretizationFailure
        (ConcRegValue (ExprBuilder scope st (Flags fm)) tp))
forall (tp :: CrucibleType) sym bak solver scope
       (st :: Type -> Type) (fm :: FloatMode).
(IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm),
 SymExpr sym ~ Expr scope,
 bak ~ OnlineBackend solver scope st (Flags fm),
 OnlineSolver solver) =>
bak
-> FloatModeRepr fm
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> MapF SymbolRepr IntrinsicConcToSymFn
-> RegEntry sym tp
-> IO (Either UniqueConcretizationFailure (ConcRegValue sym tp))
uniquelyConcRegEntry bak
bak FloatModeRepr fm
fm MapF SymbolRepr (IntrinsicConcFn scope)
iFns MapF SymbolRepr IntrinsicConcToSymFn
sFns (TypeRepr tp
-> RegValue (ExprBuilder scope st (Flags fm)) tp
-> RegEntry (ExprBuilder scope st (Flags fm)) tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RM.RegEntry TypeRepr tp
tp RegValue sym tp
RegValue (ExprBuilder scope st (Flags fm)) tp
v)

-- | Generate a model and pick a feasible concrete value from it
uniquelyConcRegEntry ::
  forall tp sym bak solver scope st fm.
  ( CB.IsSymBackend sym bak
  , sym ~ ExprBuilder scope st (Flags fm)
  , SymExpr sym ~ Expr scope
  , bak ~ CBO.OnlineBackend solver scope st (Flags fm)
  , WPO.OnlineSolver solver
  ) =>
  bak ->
  FloatModeRepr fm ->
  MapF SymbolRepr (IntrinsicConcFn scope) ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  RM.RegEntry sym tp ->
  IO (Either W4C.UniqueConcretizationFailure (ConcRegValue sym tp))
uniquelyConcRegEntry :: forall (tp :: CrucibleType) sym bak solver scope
       (st :: Type -> Type) (fm :: FloatMode).
(IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm),
 SymExpr sym ~ Expr scope,
 bak ~ OnlineBackend solver scope st (Flags fm),
 OnlineSolver solver) =>
bak
-> FloatModeRepr fm
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> MapF SymbolRepr IntrinsicConcToSymFn
-> RegEntry sym tp
-> IO (Either UniqueConcretizationFailure (ConcRegValue sym tp))
uniquelyConcRegEntry bak
bak FloatModeRepr fm
fm MapF SymbolRepr (IntrinsicConcFn scope)
iFns MapF SymbolRepr IntrinsicConcToSymFn
sFns RegEntry sym tp
re = do
  Either
  UniqueConcretizationFailure
  (Assignment (ConcRV' sym) (EmptyCtx ::> tp))
res <- bak
-> FloatModeRepr fm
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> MapF SymbolRepr IntrinsicConcToSymFn
-> RegMap sym (EmptyCtx ::> tp)
-> IO
     (Either
        UniqueConcretizationFailure
        (Assignment (ConcRV' sym) (EmptyCtx ::> tp)))
forall (tps :: Ctx CrucibleType) sym bak solver scope
       (st :: Type -> Type) (fm :: FloatMode).
(IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm),
 SymExpr sym ~ Expr scope,
 bak ~ OnlineBackend solver scope st (Flags fm),
 OnlineSolver solver) =>
bak
-> FloatModeRepr fm
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> MapF SymbolRepr IntrinsicConcToSymFn
-> RegMap sym tps
-> IO
     (Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps))
uniquelyConcRegMap bak
bak FloatModeRepr fm
fm MapF SymbolRepr (IntrinsicConcFn scope)
iFns MapF SymbolRepr IntrinsicConcToSymFn
sFns (Assignment (RegEntry sym) (EmptyCtx ::> tp)
-> RegMap sym (EmptyCtx ::> tp)
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RM.RegMap (RegEntry sym tp -> Assignment (RegEntry sym) (EmptyCtx ::> tp)
forall {k} (f :: k -> Type) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
Ctx.singleton RegEntry sym tp
re))
  case Either
  UniqueConcretizationFailure
  (Assignment (ConcRV' sym) (EmptyCtx ::> tp))
res of
    Left UniqueConcretizationFailure
e -> Either
  UniqueConcretizationFailure
  (ConcRegValue (ExprBuilder scope st (Flags fm)) tp)
-> IO
     (Either
        UniqueConcretizationFailure
        (ConcRegValue (ExprBuilder scope st (Flags fm)) tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (UniqueConcretizationFailure
-> Either
     UniqueConcretizationFailure
     (ConcRegValue (ExprBuilder scope st (Flags fm)) tp)
forall a b. a -> Either a b
Left UniqueConcretizationFailure
e)
    Right (Assignment (ConcRV' sym) ctx
Ctx.Empty Ctx.:> ConcRV' ConcRegValue sym tp
concV) -> Either
  UniqueConcretizationFailure
  (ConcRegValue (ExprBuilder scope st (Flags fm)) tp)
-> IO
     (Either
        UniqueConcretizationFailure
        (ConcRegValue (ExprBuilder scope st (Flags fm)) tp))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ConcRegValue (ExprBuilder scope st (Flags fm)) tp
-> Either
     UniqueConcretizationFailure
     (ConcRegValue (ExprBuilder scope st (Flags fm)) tp)
forall a b. b -> Either a b
Right ConcRegValue sym tp
ConcRegValue (ExprBuilder scope st (Flags fm)) tp
concV)

-- | Like 'concRegValue', but for a whole 'RegMap'
uniquelyConcRegMap ::
  forall tps sym bak solver scope st fm.
  ( CB.IsSymBackend sym bak
  , sym ~ ExprBuilder scope st (Flags fm)
  , SymExpr sym ~ Expr scope
  , bak ~ CBO.OnlineBackend solver scope st (Flags fm)
  , WPO.OnlineSolver solver
  ) =>
  bak ->
  FloatModeRepr fm ->
  MapF SymbolRepr (IntrinsicConcFn scope) ->
  MapF SymbolRepr IntrinsicConcToSymFn ->
  RegMap sym tps ->
  IO (Either W4C.UniqueConcretizationFailure (Ctx.Assignment (ConcRV' sym) tps))
uniquelyConcRegMap :: forall (tps :: Ctx CrucibleType) sym bak solver scope
       (st :: Type -> Type) (fm :: FloatMode).
(IsSymBackend sym bak, sym ~ ExprBuilder scope st (Flags fm),
 SymExpr sym ~ Expr scope,
 bak ~ OnlineBackend solver scope st (Flags fm),
 OnlineSolver solver) =>
bak
-> FloatModeRepr fm
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> MapF SymbolRepr IntrinsicConcToSymFn
-> RegMap sym tps
-> IO
     (Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps))
uniquelyConcRegMap bak
bak FloatModeRepr fm
fm MapF SymbolRepr (IntrinsicConcFn scope)
iFns MapF SymbolRepr IntrinsicConcToSymFn
sFns RegMap sym tps
m = do
  case RegMap sym tps -> Maybe (Assignment (ConcRV' sym) tps)
forall sym (tp :: Ctx CrucibleType).
IsExpr (SymExpr sym) =>
RegMap sym tp -> Maybe (Assignment (ConcRV' sym) tp)
asConcRegMap RegMap sym tps
m of
    Just Assignment (ConcRV' sym) tps
concM -> Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO
     (Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Assignment (ConcRV' sym) tps
-> Either
     UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
forall a b. b -> Either a b
Right Assignment (ConcRV' sym) tps
concM)
    Maybe (Assignment (ConcRV' sym) tps)
Nothing -> do
      -- First, check to see if there are a models of the symbolic values.
      Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
concM_ <- bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> RegMap sym tps
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall (tps :: Ctx CrucibleType) sym bak solver scope
       (st :: Type -> Type) fs.
(IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs,
 OnlineSolver solver) =>
bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> RegMap sym tps
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
concRegMap bak
bak MapF SymbolRepr (IntrinsicConcFn scope)
iFns RegMap sym tps
m
      case Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
concM_ of
        Left ConcretizationFailure
e -> Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO
     (Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (UniqueConcretizationFailure
-> Either
     UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
forall a b. a -> Either a b
Left (ConcretizationFailure -> UniqueConcretizationFailure
W4C.GroundingFailure ConcretizationFailure
e))
        Right Assignment (ConcRV' sym) tps
concM -> do
          -- We found a model, so check to see if this is the only possible
          -- model for these symbolic values.  We do this by adding a blocking
          -- clause that assumes the `RegValue`s are /not/ equal to the
          -- model we found in the previous step. If this is unsatisfiable,
          -- the `RegValue`s can only be equal to the first model, so we can
          -- conclude they are concrete. If it is satisfiable, on the other
          -- hand, the `RegValue`s can be multiple values, so they are truly
          -- symbolic.
          let sym :: ExprBuilder scope st (Flags fm)
sym = bak -> ExprBuilder scope st (Flags fm)
forall sym bak. HasSymInterface sym bak => bak -> sym
CB.backendGetSym bak
bak
          let notEq ::
                forall tp.
                ConcRV' sym tp ->
                RM.RegEntry sym tp ->
                IO (Const (W4I.Pred sym) tp)
              notEq :: forall (tp :: CrucibleType).
ConcRV' sym tp -> RegEntry sym tp -> IO (Const (Pred sym) tp)
notEq (ConcRV' ConcRegValue sym tp
concV) (RM.RegEntry TypeRepr tp
tp RegValue sym tp
v) = do
                RegValue (ExprBuilder scope st (Flags fm)) tp
symV <- ExprBuilder scope st (Flags fm)
-> MapF SymbolRepr IntrinsicConcToSymFn
-> FloatModeRepr fm
-> TypeRepr tp
-> ConcRegValue (ExprBuilder scope st (Flags fm)) tp
-> IO (RegValue (ExprBuilder scope st (Flags fm)) 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 ExprBuilder scope st (Flags fm)
sym MapF SymbolRepr IntrinsicConcToSymFn
sFns FloatModeRepr fm
fm TypeRepr tp
tp ConcRegValue sym tp
ConcRegValue (ExprBuilder scope st (Flags fm)) tp
concV
                Expr scope BaseBoolType
p <- ExprBuilder scope st (Flags fm)
-> Pred (ExprBuilder scope st (Flags fm))
-> IO (Pred (ExprBuilder scope st (Flags fm)))
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
W4I.notPred ExprBuilder scope st (Flags fm)
sym (Expr scope BaseBoolType -> IO (Expr scope BaseBoolType))
-> IO (Expr scope BaseBoolType) -> IO (Expr scope BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ExprBuilder scope st (Flags fm)
-> TypeRepr tp
-> RegValue (ExprBuilder scope st (Flags fm)) tp
-> RegValue (ExprBuilder scope st (Flags fm)) tp
-> IO (Pred (ExprBuilder scope st (Flags fm)))
forall sym (tp :: CrucibleType).
IsInterpretedFloatExprBuilder sym =>
sym
-> TypeRepr tp
-> RegValue sym tp
-> RegValue sym tp
-> IO (Pred sym)
RV.eqRegValue ExprBuilder scope st (Flags fm)
sym TypeRepr tp
tp RegValue (ExprBuilder scope st (Flags fm)) tp
symV RegValue sym tp
RegValue (ExprBuilder scope st (Flags fm)) tp
v
                Const (Expr scope BaseBoolType) tp
-> IO (Const (Expr scope BaseBoolType) tp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Expr scope BaseBoolType -> Const (Expr scope BaseBoolType) tp
forall {k} a (b :: k). a -> Const a b
Const Expr scope BaseBoolType
p)
          let RM.RegMap Assignment (RegEntry sym) tps
mAssign = RegMap sym tps
m
          Assignment (Const (Expr scope BaseBoolType)) tps
preds <- (forall (x :: CrucibleType).
 ConcRV' sym x
 -> RegEntry sym x -> IO (Const (Expr scope BaseBoolType) x))
-> Assignment (ConcRV' sym) tps
-> Assignment (RegEntry sym) tps
-> IO (Assignment (Const (Expr scope BaseBoolType)) 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 ConcRV' sym x -> RegEntry sym x -> IO (Const (Pred sym) x)
ConcRV' sym x
-> RegEntry sym x -> IO (Const (Expr scope BaseBoolType) x)
forall (tp :: CrucibleType).
ConcRV' sym tp -> RegEntry sym tp -> IO (Const (Pred sym) tp)
forall (x :: CrucibleType).
ConcRV' sym x
-> RegEntry sym x -> IO (Const (Expr scope BaseBoolType) x)
notEq Assignment (ConcRV' sym) tps
concM Assignment (RegEntry sym) tps
mAssign
          Pred (ExprBuilder scope st (Flags fm))
p <-
            (forall (x :: CrucibleType).
 Pred (ExprBuilder scope st (Flags fm))
 -> Const (Expr scope BaseBoolType) x
 -> IO (Pred (ExprBuilder scope st (Flags fm))))
-> Pred (ExprBuilder scope st (Flags fm))
-> Assignment (Const (Expr scope BaseBoolType)) tps
-> IO (Pred (ExprBuilder scope st (Flags fm)))
forall {k} {l} (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
       b (f :: k -> Type) (c :: l).
(FoldableFC t, Monad m) =>
(forall (x :: k). b -> f x -> m b) -> b -> t f c -> m b
foldlMFC
              (\Pred (ExprBuilder scope st (Flags fm))
p (Const Expr scope BaseBoolType
p') -> ExprBuilder scope st (Flags fm)
-> Pred (ExprBuilder scope st (Flags fm))
-> Pred (ExprBuilder scope st (Flags fm))
-> IO (Pred (ExprBuilder scope st (Flags fm)))
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
W4I.andPred ExprBuilder scope st (Flags fm)
sym Pred (ExprBuilder scope st (Flags fm))
p Pred (ExprBuilder scope st (Flags fm))
Expr scope BaseBoolType
p')
              (ExprBuilder scope st (Flags fm)
-> Pred (ExprBuilder scope st (Flags fm))
forall sym. IsExprBuilder sym => sym -> Pred sym
W4I.truePred ExprBuilder scope st (Flags fm)
sym)
              Assignment (Const (Expr scope BaseBoolType)) tps
preds

          FrameIdentifier
frm <- bak -> IO FrameIdentifier
forall sym bak. IsSymBackend sym bak => bak -> IO FrameIdentifier
CB.pushAssumptionFrame bak
bak
          ProgramLoc
loc <- ExprBuilder scope st (Flags fm) -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
W4I.getCurrentProgramLoc ExprBuilder scope st (Flags fm)
sym
          bak -> Assumption (ExprBuilder scope st (Flags fm)) -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
CB.addAssumption bak
bak (ProgramLoc
-> String
-> Pred (ExprBuilder scope st (Flags fm))
-> Assumption (ExprBuilder scope st (Flags fm))
forall (e :: BaseType -> Type).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
CB.GenericAssumption ProgramLoc
loc String
"uniquelyConcRegMap" Pred (ExprBuilder scope st (Flags fm))
p)
          Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
concM_' <- bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> RegMap sym tps
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
forall (tps :: Ctx CrucibleType) sym bak solver scope
       (st :: Type -> Type) fs.
(IsSymBackend sym bak, sym ~ ExprBuilder scope st fs,
 SymExpr sym ~ Expr scope, bak ~ OnlineBackend solver scope st fs,
 OnlineSolver solver) =>
bak
-> MapF SymbolRepr (IntrinsicConcFn scope)
-> RegMap sym tps
-> IO (Either ConcretizationFailure (Assignment (ConcRV' sym) tps))
concRegMap bak
bak MapF SymbolRepr (IntrinsicConcFn scope)
iFns RegMap sym tps
m
          Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
res <-
            case Either ConcretizationFailure (Assignment (ConcRV' sym) tps)
concM_' of
              Left ConcretizationFailure
W4C.UnsatInitialAssumptions -> Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO
     (Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Assignment (ConcRV' sym) tps
-> Either
     UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
forall a b. b -> Either a b
Right Assignment (ConcRV' sym) tps
concM)
              Left ConcretizationFailure
e -> Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO
     (Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (UniqueConcretizationFailure
-> Either
     UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
forall a b. a -> Either a b
Left (ConcretizationFailure -> UniqueConcretizationFailure
W4C.GroundingFailure ConcretizationFailure
e))
              Right Assignment (ConcRV' sym) tps
_ -> Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO
     (Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (UniqueConcretizationFailure
-> Either
     UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
forall a b. a -> Either a b
Left UniqueConcretizationFailure
W4C.MultipleModels)
          CrucibleAssumptions (SymExpr (ExprBuilder scope st (Flags fm)))
_ <- bak
-> FrameIdentifier
-> IO
     (CrucibleAssumptions (SymExpr (ExprBuilder scope st (Flags fm))))
forall sym bak.
IsSymBackend sym bak =>
bak -> FrameIdentifier -> IO (Assumptions sym)
CB.popAssumptionFrame bak
bak FrameIdentifier
frm
          Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
-> IO
     (Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Either UniqueConcretizationFailure (Assignment (ConcRV' sym) tps)
res

---------------------------------------------------------------------
-- * '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"