-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.Evaluation
-- Description      : Evaluation functions for Crucible core expressions
-- Copyright        : (c) Galois, Inc 2014-2016
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module provides operations evaluating Crucible expressions.
------------------------------------------------------------------------
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Lang.Crucible.Simulator.Evaluation
  ( EvalAppFunc
  , evalApp
  , selectedIndices
  , indexSymbolic
  , integerAsChar
  , complexRealAsChar
  , indexVectorWithSymNat
  , adjustVectorWithSymNat
  , updateVectorWithSymNat
  ) where

import           Prelude hiding (pred)

import qualified Control.Exception as Ex
import           Control.Lens
import           Control.Monad
import qualified Data.BitVector.Sized as BV
import qualified Data.Map.Strict as Map
import           Data.Maybe
import qualified Data.Text as Text
import qualified Data.Vector as V
import           Data.Word
import           Numeric ( showHex )
import           Numeric.Natural
import           GHC.Stack

import           Data.Parameterized.Classes
import           Data.Parameterized.Context as Ctx
import           Data.Parameterized.TraversableFC

import           What4.Interface
import           What4.InterpretedFloatingPoint
import           What4.Partial (pattern PE, pattern Unassigned, joinMaybePE)
import           What4.Utils.Complex
import           What4.WordMap

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Expr
import           Lang.Crucible.Simulator.Intrinsics
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Simulator.SimError
import           Lang.Crucible.Simulator.SymSequence
import           Lang.Crucible.Types

------------------------------------------------------------------------
-- Utilities


-- | Given a list of Booleans l, @selectedIndices@ returns the indices of
-- true values in @l@.
selectedIndices :: [Bool] -> [Natural]
selectedIndices :: [Bool] -> [Natural]
selectedIndices [Bool]
l = [Maybe Natural] -> [Natural]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Natural] -> [Natural]) -> [Maybe Natural] -> [Natural]
forall a b. (a -> b) -> a -> b
$ (Bool -> Natural -> Maybe Natural)
-> [Bool] -> [Natural] -> [Maybe Natural]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
Prelude.zipWith Bool -> Natural -> Maybe Natural
forall {a}. Bool -> a -> Maybe a
selectIndex [Bool]
l [Natural
1..]
  where selectIndex :: Bool -> a -> Maybe a
selectIndex Bool
True a
i  = a -> Maybe a
forall a. a -> Maybe a
Just a
i
        selectIndex Bool
False a
_ = Maybe a
forall a. Maybe a
Nothing

------------------------------------------------------------------------
-- Coercion functions

integerAsChar :: Integer -> Word16
integerAsChar :: Integer -> Word16
integerAsChar Integer
i = Integer -> Word16
forall a. Num a => Integer -> a
fromInteger ((Integer
i Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
`max` Integer
0) Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
`min` (Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
16::Int)Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))

complexRealAsChar :: (MonadFail m, IsExpr val)
                  => val BaseComplexType
                  -> m Word16
complexRealAsChar :: forall (m :: Type -> Type) (val :: BaseType -> Type).
(MonadFail m, IsExpr val) =>
val BaseComplexType -> m Word16
complexRealAsChar val BaseComplexType
v = do
  case val BaseComplexType -> Maybe Rational
forall (m :: Type -> Type) (e :: BaseType -> Type).
(MonadFail m, IsExpr e) =>
e BaseComplexType -> m Rational
cplxExprAsRational val BaseComplexType
v of
    -- Check number is printable.
    Just Rational
r | Bool
otherwise -> Word16 -> m Word16
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer -> Word16
integerAsChar (Rational -> Integer
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor Rational
r))
    Maybe Rational
Nothing -> String -> m Word16
forall a. String -> m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Symbolic value cannot be interpreted as a character."
    -- XXX: Should this be a panic?
    -- XXX: We should move this to crucible-matlab

------------------------------------------------------------------------
-- Evaluating expressions


-- | Helper method for implementing 'indexSymbolic'
indexSymbolic' :: IsSymBackend sym bak
               => bak
               -> (Pred sym -> a -> a -> IO a)
                  -- ^ Function for merging valeus
               -> ([Natural] -> IO a) -- ^ Concrete index function.
               -> [Natural] -- ^ Values of processed indices (in reverse order)
               -> [(Natural,Natural)] -- ^ Bounds on remaining indices.
               -> [SymNat sym] -- ^ Remaining indices.
               -> IO a
indexSymbolic' :: forall sym bak a.
IsSymBackend sym bak =>
bak
-> (Pred sym -> a -> a -> IO a)
-> ([Natural] -> IO a)
-> [Natural]
-> [(Natural, Natural)]
-> [SymNat sym]
-> IO a
indexSymbolic' bak
_ Pred sym -> a -> a -> IO a
_ [Natural] -> IO a
f [Natural]
p [] [SymNat sym]
_ = [Natural] -> IO a
f ([Natural] -> [Natural]
forall a. [a] -> [a]
reverse [Natural]
p)
indexSymbolic' bak
_ Pred sym -> a -> a -> IO a
_ [Natural] -> IO a
f [Natural]
p [(Natural, Natural)]
_ [] = [Natural] -> IO a
f ([Natural] -> [Natural]
forall a. [a] -> [a]
reverse [Natural]
p)
indexSymbolic' bak
bak Pred sym -> a -> a -> IO a
iteFn [Natural] -> IO a
f [Natural]
p ((Natural
l,Natural
h):[(Natural, Natural)]
nl) (SymNat sym
si:[SymNat sym]
il) = do
  let subIndex :: Natural -> IO a
subIndex Natural
idx = bak
-> (Pred sym -> a -> a -> IO a)
-> ([Natural] -> IO a)
-> [Natural]
-> [(Natural, Natural)]
-> [SymNat sym]
-> IO a
forall sym bak a.
IsSymBackend sym bak =>
bak
-> (Pred sym -> a -> a -> IO a)
-> ([Natural] -> IO a)
-> [Natural]
-> [(Natural, Natural)]
-> [SymNat sym]
-> IO a
indexSymbolic' bak
bak Pred sym -> a -> a -> IO a
iteFn [Natural] -> IO a
f (Natural
idxNatural -> [Natural] -> [Natural]
forall a. a -> [a] -> [a]
:[Natural]
p) [(Natural, Natural)]
nl [SymNat sym]
il
  case SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat SymNat sym
si of
    Just Natural
i
      | Natural
l Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
i Bool -> Bool -> Bool
&& Natural
i Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
h -> Natural -> IO a
subIndex Natural
i
      | Bool
otherwise ->
          bak -> SimErrorReason -> IO a
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (String -> String -> SimErrorReason
AssertFailureSimError String
msg String
details)
        where msg :: String
msg = String
"Index outside matrix dimensions." String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Natural, Natural, Natural) -> String
forall a. Show a => a -> String
show (Natural
l,Natural
i,Natural
h)
              details :: String
details = [String] -> String
unwords [String
"Index", Natural -> String
forall a. Show a => a -> String
show Natural
i, String
"is outside of range", (Natural, Natural) -> String
forall a. Show a => a -> String
show (Natural
l, Natural
h)]
    Maybe Natural
Nothing ->
      do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
         bak -> Natural -> Natural -> SymNat sym -> String -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Natural -> Natural -> SymNat sym -> String -> IO ()
ensureInRange bak
bak Natural
l Natural
h SymNat sym
si String
"Index outside matrix dimensions."
         let predFn :: Natural -> IO (Pred sym)
predFn Natural
i = sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
si (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
i
         (Natural -> IO (Pred sym))
-> (Pred sym -> a -> a -> IO a)
-> (Natural -> IO a)
-> Natural
-> Natural
-> IO a
forall (e :: BaseType -> Type) (m :: Type -> Type) a.
(IsExpr e, Monad m) =>
(Natural -> m (e BaseBoolType))
-> (e BaseBoolType -> a -> a -> m a)
-> (Natural -> m a)
-> Natural
-> Natural
-> m a
muxRange Natural -> IO (Pred sym)
predFn Pred sym -> a -> a -> IO a
iteFn Natural -> IO a
subIndex Natural
l Natural
h


ensureInRange ::
  IsSymBackend sym bak =>
  bak ->
  Natural ->
  Natural ->
  SymNat sym ->
  String ->
  IO ()
ensureInRange :: forall sym bak.
IsSymBackend sym bak =>
bak -> Natural -> Natural -> SymNat sym -> String -> IO ()
ensureInRange bak
bak Natural
l Natural
h SymNat sym
si String
msg =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     SymNat sym
l_sym <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
l
     SymNat sym
h_sym <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
h
     SymExpr sym BaseBoolType
inRange <- IO (IO (SymExpr sym BaseBoolType)) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (IO (IO (SymExpr sym BaseBoolType))
 -> IO (SymExpr sym BaseBoolType))
-> IO (IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym (SymExpr sym BaseBoolType
 -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymNat sym -> SymNat sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLe sym
sym SymNat sym
l_sym SymNat sym
si IO (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (IO (SymExpr sym BaseBoolType))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> SymNat sym -> SymNat sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLe sym
sym SymNat sym
si SymNat sym
h_sym
     bak -> SymExpr sym BaseBoolType -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak SymExpr sym BaseBoolType
inRange (String -> String -> SimErrorReason
AssertFailureSimError String
msg String
details)
  where details :: String
details = [String] -> String
unwords [String
"Range is", (Natural, Natural) -> String
forall a. Show a => a -> String
show (Natural
l, Natural
h)]



-- | Lookup a value in an array that may be at a symbolic offset.
--
-- This function takes a list of symbolic indices as natural numbers
-- along with a pair of lower and upper bounds for each index.
-- It assumes that the indices are all in range.
indexSymbolic :: IsSymBackend sym bak
              => bak
              -> (Pred sym -> a  -> a -> IO a)
                 -- ^ Function for combining results together.
              -> ([Natural] -> IO a) -- ^ Concrete index function.
              -> [(Natural,Natural)] -- ^ High and low bounds at the indices.
              -> [SymNat sym]
              -> IO a
indexSymbolic :: forall sym bak a.
IsSymBackend sym bak =>
bak
-> (Pred sym -> a -> a -> IO a)
-> ([Natural] -> IO a)
-> [(Natural, Natural)]
-> [SymNat sym]
-> IO a
indexSymbolic bak
sym Pred sym -> a -> a -> IO a
iteFn [Natural] -> IO a
f = bak
-> (Pred sym -> a -> a -> IO a)
-> ([Natural] -> IO a)
-> [Natural]
-> [(Natural, Natural)]
-> [SymNat sym]
-> IO a
forall sym bak a.
IsSymBackend sym bak =>
bak
-> (Pred sym -> a -> a -> IO a)
-> ([Natural] -> IO a)
-> [Natural]
-> [(Natural, Natural)]
-> [SymNat sym]
-> IO a
indexSymbolic' bak
sym Pred sym -> a -> a -> IO a
iteFn [Natural] -> IO a
f []

-- | Evaluate an indexTermterm to an index value.
evalBase :: IsSymInterface sym =>
            sym
         -> (forall utp . f utp -> IO (RegValue sym utp))
         -> BaseTerm f vtp
         -> IO (SymExpr sym vtp)
evalBase :: forall sym (f :: CrucibleType -> Type) (vtp :: BaseType).
IsSymInterface sym =>
sym
-> (forall (utp :: CrucibleType). f utp -> IO (RegValue sym utp))
-> BaseTerm f vtp
-> IO (SymExpr sym vtp)
evalBase sym
_ forall (utp :: CrucibleType). f utp -> IO (RegValue sym utp)
evalSub (BaseTerm BaseTypeRepr vtp
_tp f (BaseToType vtp)
e) = f (BaseToType vtp) -> IO (RegValue sym (BaseToType vtp))
forall (utp :: CrucibleType). f utp -> IO (RegValue sym utp)
evalSub f (BaseToType vtp)
e

-- | Get value stored in vector at a symbolic index.
indexVectorWithSymNat :: IsSymBackend sym bak
                      => bak
                      -> (Pred sym -> a -> a -> IO a)
                         -- ^ Ite function
                      -> V.Vector a
                      -> SymNat sym
                      -> IO a
indexVectorWithSymNat :: forall sym bak a.
IsSymBackend sym bak =>
bak
-> (Pred sym -> a -> a -> IO a) -> Vector a -> SymNat sym -> IO a
indexVectorWithSymNat bak
bak Pred sym -> a -> a -> IO a
iteFn Vector a
v SymNat sym
si =
  Bool -> IO a -> IO a
forall a. (?callStack::CallStack) => Bool -> a -> a
Ex.assert (Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
0) (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$
  case SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat SymNat sym
si of
    Just Natural
i | Natural
0 Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
i Bool -> Bool -> Bool
&& Natural
i Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n -> a -> IO a
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector a
v Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i)
           | Bool
otherwise -> bak -> SimErrorReason -> IO a
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (String -> String -> SimErrorReason
AssertFailureSimError String
msg String
details)
    Maybe Natural
Nothing ->
      do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
         let predFn :: Natural -> IO (Pred sym)
predFn Natural
i = sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
si (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
i
         let getElt :: Natural -> IO a
getElt Natural
i = a -> IO a
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector a
v Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i)
         bak -> Natural -> Natural -> SymNat sym -> String -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Natural -> Natural -> SymNat sym -> String -> IO ()
ensureInRange bak
bak Natural
0 (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) SymNat sym
si String
msg
         (Natural -> IO (Pred sym))
-> (Pred sym -> a -> a -> IO a)
-> (Natural -> IO a)
-> Natural
-> Natural
-> IO a
forall (e :: BaseType -> Type) (m :: Type -> Type) a.
(IsExpr e, Monad m) =>
(Natural -> m (e BaseBoolType))
-> (e BaseBoolType -> a -> a -> m a)
-> (Natural -> m a)
-> Natural
-> Natural
-> m a
muxRange Natural -> IO (Pred sym)
predFn Pred sym -> a -> a -> IO a
iteFn Natural -> IO a
getElt Natural
0 (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)
  where
  n :: Natural
n   = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
v)
  msg :: String
msg = String
"Vector index out of range"
  details :: String
details = [String] -> String
unwords [String
"Range is", (Natural, Natural) -> String
forall a. Show a => a -> String
show (Natural
0 :: Natural, Natural
n)]



-- | Update a vector at a given natural number index.
updateVectorWithSymNat :: IsSymBackend sym bak
                       => bak
                          -- ^ Symbolic backend
                       -> (Pred sym -> a -> a -> IO a)
                          -- ^ Ite function
                       -> V.Vector a
                          -- ^ Vector to update
                       -> SymNat sym
                          -- ^ Index to update
                       -> a
                          -- ^ New value to assign
                       -> IO (V.Vector a)
updateVectorWithSymNat :: forall sym bak a.
IsSymBackend sym bak =>
bak
-> (Pred sym -> a -> a -> IO a)
-> Vector a
-> SymNat sym
-> a
-> IO (Vector a)
updateVectorWithSymNat bak
bak Pred sym -> a -> a -> IO a
iteFn Vector a
v SymNat sym
si a
new_val = do
  bak
-> (Pred sym -> a -> a -> IO a)
-> Vector a
-> SymNat sym
-> (a -> IO a)
-> IO (Vector a)
forall sym bak a.
IsSymBackend sym bak =>
bak
-> (Pred sym -> a -> a -> IO a)
-> Vector a
-> SymNat sym
-> (a -> IO a)
-> IO (Vector a)
adjustVectorWithSymNat bak
bak Pred sym -> a -> a -> IO a
iteFn Vector a
v SymNat sym
si (\a
_ -> a -> IO a
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
new_val)

-- | Update a vector at a given natural number index.
adjustVectorWithSymNat :: IsSymBackend sym bak
                       => bak
                          -- ^ Symbolic backend
                       -> (Pred sym -> a -> a -> IO a)
                          -- ^ Ite function
                       -> V.Vector a
                          -- ^ Vector to update
                       -> SymNat sym
                          -- ^ Index to update
                       -> (a -> IO a)
                          -- ^ Adjustment function to apply
                       -> IO (V.Vector a)
adjustVectorWithSymNat :: forall sym bak a.
IsSymBackend sym bak =>
bak
-> (Pred sym -> a -> a -> IO a)
-> Vector a
-> SymNat sym
-> (a -> IO a)
-> IO (Vector a)
adjustVectorWithSymNat bak
bak Pred sym -> a -> a -> IO a
iteFn Vector a
v SymNat sym
si a -> IO a
adj =
  case SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat SymNat sym
si of
    Just Natural
i

      | Natural
i Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n ->
        do a
new_val <- a -> IO a
adj (Vector a
v Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i)
           Vector a -> IO (Vector a)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector a -> IO (Vector a)) -> Vector a -> IO (Vector a)
forall a b. (a -> b) -> a -> b
$ Vector a
v Vector a -> [(Int, a)] -> Vector a
forall a. Vector a -> [(Int, a)] -> Vector a
V.// [(Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i, a
new_val)]

      | Bool
otherwise ->
        bak -> SimErrorReason -> IO (Vector a)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO (Vector a))
-> SimErrorReason -> IO (Vector a)
forall a b. (a -> b) -> a -> b
$ String -> String -> SimErrorReason
AssertFailureSimError String
msg (Natural -> String
forall a. Show a => a -> String
details Natural
i)

    Maybe Natural
Nothing ->
      do bak -> Natural -> Natural -> SymNat sym -> String -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Natural -> Natural -> SymNat sym -> String -> IO ()
ensureInRange bak
bak Natural
0 (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) SymNat sym
si String
msg
         Int -> (Int -> IO a) -> IO (Vector a)
forall (m :: Type -> Type) a.
Monad m =>
Int -> (Int -> m a) -> m (Vector a)
V.generateM Int
n Int -> IO a
setFn
      where
      setFn :: Int -> IO a
setFn Int
j =
        do  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
            -- Compare si and j.
            Pred sym
c <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
si (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
j)
            -- Select old value or new value
            case Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
c of
              Just Bool
True  -> a -> IO a
adj (Vector a
v Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! Int
j)
              Just Bool
False -> a -> IO a
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector a
v Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! Int
j)
              Maybe Bool
Nothing ->
                do a
new_val <- a -> IO a
adj (Vector a
v Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! Int
j)
                   Pred sym -> a -> a -> IO a
iteFn Pred sym
c a
new_val (Vector a
v Vector a -> Int -> a
forall a. Vector a -> Int -> a
V.! Int
j)

  where
  n :: Int
n = Vector a -> Int
forall a. Vector a -> Int
V.length Vector a
v
  msg :: String
msg = String
"Illegal vector index"
  details :: a -> String
details a
i = String
"Illegal index " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"given to updateVectorWithSymNat"

type EvalAppFunc sym app = forall f.
  (forall tp. f tp -> IO (RegValue sym tp)) ->
  (forall tp. app f tp -> IO (RegValue sym tp))

{-# INLINE evalApp #-}
-- | Evaluate the application.
evalApp :: forall sym bak ext.
           IsSymBackend sym bak
        => bak
        -> IntrinsicTypes sym
        -> (Int -> String -> IO ())
           -- ^ Function for logging messages.
        -> EvalAppFunc sym (ExprExtension ext)
        -> EvalAppFunc sym (App ext)
evalApp :: forall sym bak ext.
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> (Int -> String -> IO ())
-> EvalAppFunc sym (ExprExtension ext)
-> EvalAppFunc sym (App ext)
evalApp bak
bak IntrinsicTypes sym
itefns Int -> String -> IO ()
_logFn EvalAppFunc sym (ExprExtension ext)
evalExt (forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub :: forall tp. f tp -> IO (RegValue sym tp)) App ext f tp
a0 = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
  case App ext f tp
a0 of

    BaseIsEq BaseTypeRepr tp1
tp f (BaseToType tp1)
xe f (BaseToType tp1)
ye -> do
      SymExpr sym tp1
x <- sym
-> (forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp))
-> BaseTerm f tp1
-> IO (SymExpr sym tp1)
forall sym (f :: CrucibleType -> Type) (vtp :: BaseType).
IsSymInterface sym =>
sym
-> (forall (utp :: CrucibleType). f utp -> IO (RegValue sym utp))
-> BaseTerm f vtp
-> IO (SymExpr sym vtp)
evalBase sym
sym f utp -> IO (RegValue sym utp)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub (BaseTypeRepr tp1 -> f (BaseToType tp1) -> BaseTerm f tp1
forall (f :: CrucibleType -> Type) (tp :: BaseType).
BaseTypeRepr tp -> f (BaseToType tp) -> BaseTerm f tp
BaseTerm BaseTypeRepr tp1
tp f (BaseToType tp1)
xe)
      SymExpr sym tp1
y <- sym
-> (forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp))
-> BaseTerm f tp1
-> IO (SymExpr sym tp1)
forall sym (f :: CrucibleType -> Type) (vtp :: BaseType).
IsSymInterface sym =>
sym
-> (forall (utp :: CrucibleType). f utp -> IO (RegValue sym utp))
-> BaseTerm f vtp
-> IO (SymExpr sym vtp)
evalBase sym
sym f utp -> IO (RegValue sym utp)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub (BaseTypeRepr tp1 -> f (BaseToType tp1) -> BaseTerm f tp1
forall (f :: CrucibleType -> Type) (tp :: BaseType).
BaseTypeRepr tp -> f (BaseToType tp) -> BaseTerm f tp
BaseTerm BaseTypeRepr tp1
tp f (BaseToType tp1)
ye)
      sym
-> SymExpr sym tp1
-> SymExpr sym tp1
-> IO (SymExpr sym BaseBoolType)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
forall (tp :: BaseType).
sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym BaseBoolType)
isEq sym
sym SymExpr sym tp1
x SymExpr sym tp1
y

    BaseIte BaseTypeRepr tp1
tp f ('BaseToType BaseBoolType)
ce f ('BaseToType tp1)
xe f ('BaseToType tp1)
ye -> do
      SymExpr sym BaseBoolType
c <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
ce
      case SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred SymExpr sym BaseBoolType
c of
        Just Bool
True  -> f ('BaseToType tp1) -> IO (RegValue sym ('BaseToType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType tp1)
xe
        Just Bool
False -> f ('BaseToType tp1) -> IO (RegValue sym ('BaseToType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType tp1)
ye
        Maybe Bool
Nothing -> do
          SymExpr sym tp1
x <- sym
-> (forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp))
-> BaseTerm f tp1
-> IO (SymExpr sym tp1)
forall sym (f :: CrucibleType -> Type) (vtp :: BaseType).
IsSymInterface sym =>
sym
-> (forall (utp :: CrucibleType). f utp -> IO (RegValue sym utp))
-> BaseTerm f vtp
-> IO (SymExpr sym vtp)
evalBase sym
sym f utp -> IO (RegValue sym utp)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub (BaseTypeRepr tp1 -> f ('BaseToType tp1) -> BaseTerm f tp1
forall (f :: CrucibleType -> Type) (tp :: BaseType).
BaseTypeRepr tp -> f (BaseToType tp) -> BaseTerm f tp
BaseTerm BaseTypeRepr tp1
tp f ('BaseToType tp1)
xe)
          SymExpr sym tp1
y <- sym
-> (forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp))
-> BaseTerm f tp1
-> IO (SymExpr sym tp1)
forall sym (f :: CrucibleType -> Type) (vtp :: BaseType).
IsSymInterface sym =>
sym
-> (forall (utp :: CrucibleType). f utp -> IO (RegValue sym utp))
-> BaseTerm f vtp
-> IO (SymExpr sym vtp)
evalBase sym
sym f utp -> IO (RegValue sym utp)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub (BaseTypeRepr tp1 -> f ('BaseToType tp1) -> BaseTerm f tp1
forall (f :: CrucibleType -> Type) (tp :: BaseType).
BaseTypeRepr tp -> f (BaseToType tp) -> BaseTerm f tp
BaseTerm BaseTypeRepr tp1
tp f ('BaseToType tp1)
ye)
          sym
-> SymExpr sym BaseBoolType
-> SymExpr sym tp1
-> SymExpr sym tp1
-> IO (SymExpr sym tp1)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym
-> SymExpr sym BaseBoolType
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
baseTypeIte sym
sym SymExpr sym BaseBoolType
c SymExpr sym tp1
x SymExpr sym tp1
y

    ----------------------------------------------------------------------
    ExtensionApp ExprExtension ext f tp
x -> (forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp))
-> forall (tp :: CrucibleType).
   ExprExtension ext f tp -> IO (RegValue sym tp)
EvalAppFunc sym (ExprExtension ext)
evalExt f tp -> IO (RegValue sym tp)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub ExprExtension ext f tp
x

    ----------------------------------------------------------------------
    -- ()

    App ext f tp
EmptyApp -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

    ----------------------------------------------------------------------
    -- Any

    PackAny TypeRepr tp1
tp f tp1
x -> do
      RegValue sym tp1
xv <- f tp1 -> IO (RegValue sym tp1)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f tp1
x
      AnyValue sym -> IO (AnyValue sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TypeRepr tp1 -> RegValue sym tp1 -> AnyValue sym
forall (tp :: CrucibleType) sym.
TypeRepr tp -> RegValue sym tp -> AnyValue sym
AnyValue TypeRepr tp1
tp RegValue sym tp1
xv)

    UnpackAny TypeRepr tp1
tp f 'AnyType
x -> do
      AnyValue sym
xv <- f 'AnyType -> IO (RegValue sym 'AnyType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'AnyType
x
      case AnyValue sym
xv of
        AnyValue TypeRepr tp
tpv RegValue sym tp
v
          | Just tp1 :~: tp
Refl <- TypeRepr tp1 -> TypeRepr tp -> Maybe (tp1 :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr tp1
tp TypeRepr tp
tpv ->
               PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
 -> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a b. (a -> b) -> a -> b
$! SymExpr sym BaseBoolType
-> RegValue sym tp1
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
forall p v. p -> v -> PartExpr p v
PE (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) RegValue sym tp1
RegValue sym tp
v
          | Bool
otherwise ->
               PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
forall p v. PartExpr p v
Unassigned

    ----------------------------------------------------------------------
    -- Bool

    BoolLit Bool
b -> RegValue sym tp -> IO (RegValue sym tp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (RegValue sym tp -> IO (RegValue sym tp))
-> RegValue sym tp -> IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ sym -> Bool -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
backendPred sym
sym Bool
b
    Not f ('BaseToType BaseBoolType)
x -> do
      SymExpr sym BaseBoolType
r <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
x
      sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym SymExpr sym BaseBoolType
r
    And f ('BaseToType BaseBoolType)
x f ('BaseToType BaseBoolType)
y -> do
      SymExpr sym BaseBoolType
xv <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
x
      SymExpr sym BaseBoolType
yv <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
y
      sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym SymExpr sym BaseBoolType
xv SymExpr sym BaseBoolType
yv
    Or f ('BaseToType BaseBoolType)
x f ('BaseToType BaseBoolType)
y -> do
      SymExpr sym BaseBoolType
xv <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
x
      SymExpr sym BaseBoolType
yv <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
y
      sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym SymExpr sym BaseBoolType
xv SymExpr sym BaseBoolType
yv
    BoolXor f ('BaseToType BaseBoolType)
x f ('BaseToType BaseBoolType)
y -> do
      SymExpr sym BaseBoolType
xv <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
x
      SymExpr sym BaseBoolType
yv <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
y
      sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
xorPred sym
sym SymExpr sym BaseBoolType
xv SymExpr sym BaseBoolType
yv

    ----------------------------------------------------------------------
    -- Nat

    NatLit Natural
n -> sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
n
    NatIte f ('BaseToType BaseBoolType)
pe f 'NatType
xe f 'NatType
ye -> do
      SymExpr sym BaseBoolType
p <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
pe
      SymNat sym
x <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
xe
      SymNat sym
y <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
ye
      sym
-> SymExpr sym BaseBoolType
-> SymNat sym
-> SymNat sym
-> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte sym
sym SymExpr sym BaseBoolType
p SymNat sym
x SymNat sym
y
    NatEq f 'NatType
xe f 'NatType
ye -> do
      SymNat sym
x <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
xe
      SymNat sym
y <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
ye
      sym -> SymNat sym -> SymNat sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
x SymNat sym
y
    NatLt f 'NatType
xe f 'NatType
ye -> do
      SymNat sym
x <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
xe
      SymNat sym
y <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
ye
      sym -> SymNat sym -> SymNat sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLt sym
sym SymNat sym
x SymNat sym
y
    NatLe f 'NatType
xe f 'NatType
ye -> do
      SymNat sym
x <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
xe
      SymNat sym
y <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
ye
      sym -> SymNat sym -> SymNat sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLe sym
sym SymNat sym
x SymNat sym
y
    NatAdd f 'NatType
xe f 'NatType
ye -> do
      SymNat sym
x <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
xe
      SymNat sym
y <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
ye
      sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natAdd sym
sym SymNat sym
x SymNat sym
y
    NatSub f 'NatType
xe f 'NatType
ye -> do
      SymNat sym
x <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
xe
      SymNat sym
y <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
ye
      sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natSub sym
sym SymNat sym
x SymNat sym
y
    NatMul f 'NatType
xe f 'NatType
ye -> do
      SymNat sym
x <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
xe
      SymNat sym
y <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
ye
      sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natMul sym
sym SymNat sym
x SymNat sym
y
    NatDiv f 'NatType
xe f 'NatType
ye -> do
      SymNat sym
x <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
xe
      SymNat sym
y <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
ye
      sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natDiv sym
sym SymNat sym
x SymNat sym
y
    NatMod f 'NatType
xe f 'NatType
ye -> do
      SymNat sym
x <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
xe
      SymNat sym
y <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
ye
      sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natMod sym
sym SymNat sym
x SymNat sym
y

    ----------------------------------------------------------------------
    -- Int

    IntLit Integer
n -> sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym Integer
n
    IntLe f ('BaseToType BaseIntegerType)
xe f ('BaseToType BaseIntegerType)
ye -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
xe
      SymInteger sym
y <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
ye
      sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe sym
sym SymInteger sym
x SymInteger sym
y
    IntLt f ('BaseToType BaseIntegerType)
xe f ('BaseToType BaseIntegerType)
ye -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
xe
      SymInteger sym
y <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
ye
      sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym
sym SymInteger sym
x SymInteger sym
y
    IntNeg f ('BaseToType BaseIntegerType)
xe -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
xe
      sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
intNeg sym
sym SymInteger sym
x
    IntAbs f ('BaseToType BaseIntegerType)
xe -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
xe
      sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymInteger sym)
intAbs sym
sym SymInteger sym
x
    IntAdd f ('BaseToType BaseIntegerType)
xe f ('BaseToType BaseIntegerType)
ye -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
xe
      SymInteger sym
y <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
ye
      sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intAdd sym
sym SymInteger sym
x SymInteger sym
y
    IntSub f ('BaseToType BaseIntegerType)
xe f ('BaseToType BaseIntegerType)
ye -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
xe
      SymInteger sym
y <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
ye
      sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intSub sym
sym SymInteger sym
x SymInteger sym
y
    IntMul f ('BaseToType BaseIntegerType)
xe f ('BaseToType BaseIntegerType)
ye -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
xe
      SymInteger sym
y <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
ye
      sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMul sym
sym SymInteger sym
x SymInteger sym
y
    IntDiv f ('BaseToType BaseIntegerType)
xe f ('BaseToType BaseIntegerType)
ye -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
xe
      SymInteger sym
y <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
ye
      sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intDiv sym
sym SymInteger sym
x SymInteger sym
y
    IntMod f ('BaseToType BaseIntegerType)
xe f ('BaseToType BaseIntegerType)
ye -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
xe
      SymInteger sym
y <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
ye
      sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMod sym
sym SymInteger sym
x SymInteger sym
y

    --------------------------------------------------------------------
    -- Maybe

    JustValue TypeRepr tp1
_ f tp1
e -> do
      RegValue sym tp1
r <- f tp1 -> IO (RegValue sym tp1)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f tp1
e
      PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
 -> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a b. (a -> b) -> a -> b
$! SymExpr sym BaseBoolType
-> RegValue sym tp1
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
forall p v. p -> v -> PartExpr p v
PE (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) RegValue sym tp1
r
    NothingValue TypeRepr tp1
_ -> do
      PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
forall p v. PartExpr p v
Unassigned
    FromJustValue TypeRepr tp
_ f (MaybeType tp)
maybe_expr f (StringType Unicode)
msg_expr -> do
      PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
maybe_val <- f (MaybeType tp) -> IO (RegValue sym (MaybeType tp))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (MaybeType tp)
maybe_expr
      case PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
maybe_val of
        -- Special case to avoid forcing evaluation of msg.
        PE (SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred -> Just Bool
True) RegValue sym tp
v -> RegValue sym tp -> IO (RegValue sym tp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return RegValue sym tp
v
        PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
_ -> do
          SymExpr sym (BaseStringType Unicode)
msg <- f (StringType Unicode) -> IO (RegValue sym (StringType Unicode))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType Unicode)
msg_expr
          case SymExpr sym (BaseStringType Unicode)
-> Maybe (StringLiteral Unicode)
forall (si :: StringInfo).
SymExpr sym (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
asString SymExpr sym (BaseStringType Unicode)
msg of
            Just (UnicodeLiteral Text
msg') -> bak
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
-> SimErrorReason
-> IO (RegValue sym tp)
forall sym bak v.
IsSymBackend sym bak =>
bak -> PartExpr (Pred sym) v -> SimErrorReason -> IO v
readPartExpr bak
bak PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
maybe_val (String -> SimErrorReason
GenericSimError (Text -> String
Text.unpack Text
msg'))
            Maybe (StringLiteral Unicode)
Nothing ->
              bak -> SimErrorReason -> IO (RegValue sym tp)
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO (RegValue sym tp))
-> SimErrorReason -> IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$
                CallStack -> String -> SimErrorReason
Unsupported CallStack
(?callStack::CallStack) => CallStack
callStack String
"Symbolic string in fromJustValue"

    ----------------------------------------------------------------------
    -- Recursive Types

    RollRecursive SymbolRepr nm
_ CtxRepr ctx
_ f (UnrollType nm ctx)
e   -> RegValue sym (UnrollType nm ctx) -> RolledType sym nm ctx
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
RegValue sym (UnrollType nm ctx) -> RolledType sym nm ctx
RolledType (RegValue sym (UnrollType nm ctx) -> RolledType sym nm ctx)
-> IO (RegValue sym (UnrollType nm ctx))
-> IO (RolledType sym nm ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (UnrollType nm ctx) -> IO (RegValue sym (UnrollType nm ctx))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (UnrollType nm ctx)
e
    UnrollRecursive SymbolRepr nm
_ CtxRepr ctx
_ f (RecursiveType nm ctx)
e -> RolledType sym nm ctx -> RegValue sym tp
RolledType sym nm ctx -> RegValue sym (UnrollType nm ctx)
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
RolledType sym nm ctx -> RegValue sym (UnrollType nm ctx)
unroll (RolledType sym nm ctx -> RegValue sym tp)
-> IO (RolledType sym nm ctx) -> IO (RegValue sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (RecursiveType nm ctx)
-> IO (RegValue sym (RecursiveType nm ctx))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (RecursiveType nm ctx)
e

    ----------------------------------------------------------------------
    -- Vector

    VectorLit TypeRepr tp1
_ Vector (f tp1)
v -> (f tp1 -> IO (RegValue sym tp1))
-> Vector (f tp1) -> IO (Vector (RegValue 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 f tp1 -> IO (RegValue sym tp1)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub Vector (f tp1)
v
    VectorReplicate TypeRepr tp1
_ f 'NatType
n_expr f tp1
e_expr -> do
      SymNat sym
ne <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
n_expr
      case SymNat sym -> Maybe Natural
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Natural
asNat SymNat sym
ne of
        Maybe Natural
Nothing -> bak -> SimErrorReason -> IO (Vector (RegValue sym tp1))
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason -> IO (Vector (RegValue sym tp1)))
-> SimErrorReason -> IO (Vector (RegValue sym tp1))
forall a b. (a -> b) -> a -> b
$
                      CallStack -> String -> SimErrorReason
Unsupported CallStack
(?callStack::CallStack) => CallStack
callStack String
"vectors with symbolic length"
        Just Natural
n -> do
          RegValue sym tp1
e <- f tp1 -> IO (RegValue sym tp1)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f tp1
e_expr
          Vector (RegValue sym tp1) -> IO (Vector (RegValue sym tp1))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector (RegValue sym tp1) -> IO (Vector (RegValue sym tp1)))
-> Vector (RegValue sym tp1) -> IO (Vector (RegValue sym tp1))
forall a b. (a -> b) -> a -> b
$ Int -> RegValue sym tp1 -> Vector (RegValue sym tp1)
forall a. Int -> a -> Vector a
V.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) RegValue sym tp1
e
    VectorIsEmpty f (VectorType tp1)
r -> do
      Vector (RegValue sym tp1)
v <- f (VectorType tp1) -> IO (RegValue sym (VectorType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (VectorType tp1)
r
      SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$ sym -> Bool -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
backendPred sym
sym (Vector (RegValue sym tp1) -> Bool
forall a. Vector a -> Bool
V.null Vector (RegValue sym tp1)
v)
    VectorSize f (VectorType tp1)
v_expr -> do
      Vector (RegValue sym tp1)
v <- f (VectorType tp1) -> IO (RegValue sym (VectorType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (VectorType tp1)
v_expr
      sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Vector (RegValue sym tp1) -> Int
forall a. Vector a -> Int
V.length Vector (RegValue sym tp1)
v))
    VectorGetEntry TypeRepr tp
rtp f (VectorType tp)
v_expr f 'NatType
i_expr -> do
      Vector (RegValue sym tp)
v <- f (VectorType tp) -> IO (RegValue sym (VectorType tp))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (VectorType tp)
v_expr
      SymNat sym
i <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
i_expr
      bak
-> (SymExpr sym BaseBoolType
    -> RegValue sym tp -> RegValue sym tp -> IO (RegValue sym tp))
-> Vector (RegValue sym tp)
-> SymNat sym
-> IO (RegValue sym tp)
forall sym bak a.
IsSymBackend sym bak =>
bak
-> (Pred sym -> a -> a -> IO a) -> Vector a -> SymNat sym -> IO a
indexVectorWithSymNat bak
bak (sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> SymExpr sym BaseBoolType
-> RegValue sym tp
-> RegValue sym tp
-> IO (RegValue sym tp)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
sym IntrinsicTypes sym
itefns TypeRepr tp
rtp) Vector (RegValue sym tp)
v SymNat sym
i
    VectorSetEntry TypeRepr tp1
rtp f ('VectorType tp1)
v_expr f 'NatType
i_expr f tp1
n_expr -> do
      Vector (RegValue sym tp1)
v <- f ('VectorType tp1) -> IO (RegValue sym ('VectorType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('VectorType tp1)
v_expr
      SymNat sym
i <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
i_expr
      RegValue sym tp1
n <- f tp1 -> IO (RegValue sym tp1)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f tp1
n_expr
      bak
-> (SymExpr sym BaseBoolType
    -> RegValue sym tp1 -> RegValue sym tp1 -> IO (RegValue sym tp1))
-> Vector (RegValue sym tp1)
-> SymNat sym
-> RegValue sym tp1
-> IO (Vector (RegValue sym tp1))
forall sym bak a.
IsSymBackend sym bak =>
bak
-> (Pred sym -> a -> a -> IO a)
-> Vector a
-> SymNat sym
-> a
-> IO (Vector a)
updateVectorWithSymNat bak
bak (sym
-> IntrinsicTypes sym
-> TypeRepr tp1
-> SymExpr sym BaseBoolType
-> RegValue sym tp1
-> RegValue sym tp1
-> IO (RegValue sym tp1)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
sym IntrinsicTypes sym
itefns TypeRepr tp1
rtp) Vector (RegValue sym tp1)
v SymNat sym
i RegValue sym tp1
n
    VectorCons TypeRepr tp1
_ f tp1
e_expr f ('VectorType tp1)
v_expr -> do
      RegValue sym tp1
e <- f tp1 -> IO (RegValue sym tp1)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f tp1
e_expr
      Vector (RegValue sym tp1)
v <- f ('VectorType tp1) -> IO (RegValue sym ('VectorType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('VectorType tp1)
v_expr
      Vector (RegValue sym tp1) -> IO (Vector (RegValue sym tp1))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vector (RegValue sym tp1) -> IO (Vector (RegValue sym tp1)))
-> Vector (RegValue sym tp1) -> IO (Vector (RegValue sym tp1))
forall a b. (a -> b) -> a -> b
$ RegValue sym tp1
-> Vector (RegValue sym tp1) -> Vector (RegValue sym tp1)
forall a. a -> Vector a -> Vector a
V.cons RegValue sym tp1
e Vector (RegValue sym tp1)
v

    --------------------------------------------------------------------
    -- Sequence

    SequenceNil TypeRepr tp1
_tpr -> sym -> IO (SymSequence sym (RegValue sym tp1))
forall sym a. sym -> IO (SymSequence sym a)
nilSymSequence sym
sym
    SequenceCons TypeRepr tp1
_tpr f tp1
x f ('SequenceType tp1)
xs ->
      IO (IO (RegValue sym tp)) -> IO (RegValue sym tp)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (IO (IO (RegValue sym tp)) -> IO (RegValue sym tp))
-> IO (IO (RegValue sym tp)) -> IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ sym
-> RegValue sym tp1
-> SymSequence sym (RegValue sym tp1)
-> IO (SymSequence sym (RegValue sym tp1))
forall sym a.
sym -> a -> SymSequence sym a -> IO (SymSequence sym a)
consSymSequence sym
sym (RegValue sym tp1
 -> SymSequence sym (RegValue sym tp1)
 -> IO (SymSequence sym (RegValue sym tp1)))
-> IO (RegValue sym tp1)
-> IO
     (SymSequence sym (RegValue sym tp1)
      -> IO (SymSequence sym (RegValue sym tp1)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f tp1 -> IO (RegValue sym tp1)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f tp1
x IO
  (SymSequence sym (RegValue sym tp1)
   -> IO (SymSequence sym (RegValue sym tp1)))
-> IO (SymSequence sym (RegValue sym tp1))
-> IO (IO (SymSequence sym (RegValue sym tp1)))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> f ('SequenceType tp1) -> IO (RegValue sym ('SequenceType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('SequenceType tp1)
xs
    SequenceAppend TypeRepr tp1
_tpr f ('SequenceType tp1)
xs f ('SequenceType tp1)
ys ->
      IO (IO (RegValue sym tp)) -> IO (RegValue sym tp)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (IO (IO (RegValue sym tp)) -> IO (RegValue sym tp))
-> IO (IO (RegValue sym tp)) -> IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ sym
-> SymSequence sym (RegValue sym tp1)
-> SymSequence sym (RegValue sym tp1)
-> IO (SymSequence sym (RegValue sym tp1))
forall sym a.
sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
appendSymSequence sym
sym (SymSequence sym (RegValue sym tp1)
 -> SymSequence sym (RegValue sym tp1)
 -> IO (SymSequence sym (RegValue sym tp1)))
-> IO (SymSequence sym (RegValue sym tp1))
-> IO
     (SymSequence sym (RegValue sym tp1)
      -> IO (SymSequence sym (RegValue sym tp1)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f ('SequenceType tp1) -> IO (RegValue sym ('SequenceType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('SequenceType tp1)
xs IO
  (SymSequence sym (RegValue sym tp1)
   -> IO (SymSequence sym (RegValue sym tp1)))
-> IO (SymSequence sym (RegValue sym tp1))
-> IO (IO (SymSequence sym (RegValue sym tp1)))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> f ('SequenceType tp1) -> IO (RegValue sym ('SequenceType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('SequenceType tp1)
ys
    SequenceIsNil TypeRepr tp1
_tpr f (SequenceType tp1)
xs ->
      sym
-> SymSequence sym (RegValue sym tp1)
-> IO (SymExpr sym BaseBoolType)
forall sym a.
IsExprBuilder sym =>
sym -> SymSequence sym a -> IO (Pred sym)
isNilSymSequence sym
sym (SymSequence sym (RegValue sym tp1)
 -> IO (SymExpr sym BaseBoolType))
-> IO (SymSequence sym (RegValue sym tp1))
-> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (SequenceType tp1) -> IO (RegValue sym (SequenceType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (SequenceType tp1)
xs
    SequenceLength TypeRepr tp1
_tpr f (SequenceType tp1)
xs ->
      sym -> SymSequence sym (RegValue sym tp1) -> IO (SymNat sym)
forall sym a.
IsExprBuilder sym =>
sym -> SymSequence sym a -> IO (SymNat sym)
lengthSymSequence sym
sym (SymSequence sym (RegValue sym tp1) -> IO (SymNat sym))
-> IO (SymSequence sym (RegValue sym tp1)) -> IO (SymNat sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (SequenceType tp1) -> IO (RegValue sym (SequenceType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (SequenceType tp1)
xs
    SequenceHead TypeRepr tp1
tpr f (SequenceType tp1)
xs ->
      sym
-> (SymExpr sym BaseBoolType
    -> RegValue sym tp1 -> RegValue sym tp1 -> IO (RegValue sym tp1))
-> SymSequence sym (RegValue sym tp1)
-> IO
     (PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall sym a.
IsExprBuilder sym =>
sym
-> (Pred sym -> a -> a -> IO a)
-> SymSequence sym a
-> IO (PartExpr (Pred sym) a)
headSymSequence sym
sym (sym
-> IntrinsicTypes sym
-> TypeRepr tp1
-> SymExpr sym BaseBoolType
-> RegValue sym tp1
-> RegValue sym tp1
-> IO (RegValue sym tp1)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
sym IntrinsicTypes sym
itefns TypeRepr tp1
tpr) (SymSequence sym (RegValue sym tp1)
 -> IO
      (PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp1)))
-> IO (SymSequence sym (RegValue sym tp1))
-> IO
     (PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (SequenceType tp1) -> IO (RegValue sym (SequenceType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (SequenceType tp1)
xs
    SequenceTail TypeRepr tp1
_tpr f (SequenceType tp1)
xs ->
      sym
-> SymSequence sym (RegValue sym tp1)
-> IO
     (PartialWithErr
        () (SymExpr sym BaseBoolType) (SymSequence sym (RegValue sym tp1)))
forall sym a.
IsExprBuilder sym =>
sym
-> SymSequence sym a
-> IO (PartExpr (Pred sym) (SymSequence sym a))
tailSymSequence sym
sym (SymSequence sym (RegValue sym tp1)
 -> IO
      (PartialWithErr
         ()
         (SymExpr sym BaseBoolType)
         (SymSequence sym (RegValue sym tp1))))
-> IO (SymSequence sym (RegValue sym tp1))
-> IO
     (PartialWithErr
        () (SymExpr sym BaseBoolType) (SymSequence sym (RegValue sym tp1)))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (SequenceType tp1) -> IO (RegValue sym (SequenceType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (SequenceType tp1)
xs
    SequenceUncons TypeRepr tp1
tpr f (SequenceType tp1)
xs ->
      do SymSequence sym (RegValue sym tp1)
xs' <- f (SequenceType tp1) -> IO (RegValue sym (SequenceType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (SequenceType tp1)
xs
         PartialWithErr
  ()
  (SymExpr sym BaseBoolType)
  (RegValue sym tp1, SymSequence sym (RegValue sym tp1))
mu <- sym
-> (SymExpr sym BaseBoolType
    -> RegValue sym tp1 -> RegValue sym tp1 -> IO (RegValue sym tp1))
-> SymSequence sym (RegValue sym tp1)
-> IO
     (PartialWithErr
        ()
        (SymExpr sym BaseBoolType)
        (RegValue sym tp1, SymSequence sym (RegValue sym tp1)))
forall sym a.
IsExprBuilder sym =>
sym
-> (Pred sym -> a -> a -> IO a)
-> SymSequence sym a
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
unconsSymSequence sym
sym (sym
-> IntrinsicTypes sym
-> TypeRepr tp1
-> SymExpr sym BaseBoolType
-> RegValue sym tp1
-> RegValue sym tp1
-> IO (RegValue sym tp1)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
sym IntrinsicTypes sym
itefns TypeRepr tp1
tpr) SymSequence sym (RegValue sym tp1)
xs'
         ((RegValue sym tp1, SymSequence sym (RegValue sym tp1))
 -> IO
      (Assignment
         (RegValue' sym) ((EmptyCtx ::> tp1) ::> SequenceType tp1)))
-> PartialWithErr
     ()
     (SymExpr sym BaseBoolType)
     (RegValue sym tp1, SymSequence sym (RegValue sym tp1))
-> IO
     (PartialWithErr
        ()
        (SymExpr sym BaseBoolType)
        (Assignment
           (RegValue' sym) ((EmptyCtx ::> tp1) ::> SequenceType 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)
-> PartialWithErr () (SymExpr sym BaseBoolType) a
-> f (PartialWithErr () (SymExpr sym BaseBoolType) b)
traverse (\ (RegValue sym tp1
h,SymSequence sym (RegValue sym tp1)
tl) -> Assignment
  (RegValue' sym) ((EmptyCtx ::> tp1) ::> SequenceType tp1)
-> IO
     (Assignment
        (RegValue' sym) ((EmptyCtx ::> tp1) ::> SequenceType tp1))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Assignment (RegValue' sym) EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment (RegValue' sym) EmptyCtx
-> RegValue' sym tp1
-> Assignment (RegValue' sym) (EmptyCtx ::> tp1)
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.:> RegValue sym tp1 -> RegValue' sym tp1
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV RegValue sym tp1
h Assignment (RegValue' sym) (EmptyCtx ::> tp1)
-> RegValue' sym (SequenceType tp1)
-> Assignment
     (RegValue' sym) ((EmptyCtx ::> tp1) ::> SequenceType tp1)
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.:> RegValue sym (SequenceType tp1) -> RegValue' sym (SequenceType tp1)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV SymSequence sym (RegValue sym tp1)
RegValue sym (SequenceType tp1)
tl)) PartialWithErr
  ()
  (SymExpr sym BaseBoolType)
  (RegValue sym tp1, SymSequence sym (RegValue sym tp1))
mu

    --------------------------------------------------------------------
    -- Symbolic Arrays

    SymArrayLookup BaseTypeRepr b
_ f (SymbolicArrayType (idx ::> tp1) b)
a Assignment (BaseTerm f) (idx ::> tp1)
i -> do
      IO (IO (RegValue sym tp)) -> IO (RegValue sym tp)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (IO (IO (RegValue sym tp)) -> IO (RegValue sym tp))
-> IO (IO (RegValue sym tp)) -> IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseArrayType (idx ::> tp1) b)
-> Assignment (SymExpr sym) (idx ::> tp1)
-> IO (SymExpr sym b)
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> IO (SymExpr sym b)
forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> IO (SymExpr sym b)
arrayLookup sym
sym (SymExpr sym (BaseArrayType (idx ::> tp1) b)
 -> Assignment (SymExpr sym) (idx ::> tp1) -> IO (SymExpr sym b))
-> IO (SymExpr sym (BaseArrayType (idx ::> tp1) b))
-> IO
     (Assignment (SymExpr sym) (idx ::> tp1) -> IO (SymExpr sym b))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (SymbolicArrayType (idx ::> tp1) b)
-> IO (RegValue sym (SymbolicArrayType (idx ::> tp1) b))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (SymbolicArrayType (idx ::> tp1) b)
a IO (Assignment (SymExpr sym) (idx ::> tp1) -> IO (SymExpr sym b))
-> IO (Assignment (SymExpr sym) (idx ::> tp1))
-> IO (IO (SymExpr sym b))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: BaseType). BaseTerm f x -> IO (SymExpr sym x))
-> forall (x :: Ctx BaseType).
   Assignment (BaseTerm f) x -> IO (Assignment (SymExpr 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 :: BaseType -> Type) (g :: BaseType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: BaseType). f x -> m (g x))
-> forall (x :: Ctx BaseType). Assignment f x -> m (Assignment g x)
traverseFC (sym
-> (forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp))
-> BaseTerm f x
-> IO (SymExpr sym x)
forall sym (f :: CrucibleType -> Type) (vtp :: BaseType).
IsSymInterface sym =>
sym
-> (forall (utp :: CrucibleType). f utp -> IO (RegValue sym utp))
-> BaseTerm f vtp
-> IO (SymExpr sym vtp)
evalBase sym
sym f utp -> IO (RegValue sym utp)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub) Assignment (BaseTerm f) (idx ::> tp1)
i

    SymArrayUpdate  BaseTypeRepr b
_ f ('BaseToType (BaseArrayType (idx ::> itp) b))
a Assignment (BaseTerm f) (idx ::> itp)
i f (BaseToType b)
v -> do
      IO (IO (RegValue sym tp)) -> IO (RegValue sym tp)
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join (IO (IO (RegValue sym tp)) -> IO (RegValue sym tp))
-> IO (IO (RegValue sym tp)) -> IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ sym
-> SymExpr sym (BaseArrayType (idx ::> itp) b)
-> Assignment (SymExpr sym) (idx ::> itp)
-> SymExpr sym b
-> IO (SymExpr sym (BaseArrayType (idx ::> itp) b))
forall sym (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
forall (idx :: Ctx BaseType) (tp :: BaseType) (b :: BaseType).
sym
-> SymArray sym (idx ::> tp) b
-> Assignment (SymExpr sym) (idx ::> tp)
-> SymExpr sym b
-> IO (SymArray sym (idx ::> tp) b)
arrayUpdate sym
sym
        (SymExpr sym (BaseArrayType (idx ::> itp) b)
 -> Assignment (SymExpr sym) (idx ::> itp)
 -> SymExpr sym b
 -> IO (SymExpr sym (BaseArrayType (idx ::> itp) b)))
-> IO (SymExpr sym (BaseArrayType (idx ::> itp) b))
-> IO
     (Assignment (SymExpr sym) (idx ::> itp)
      -> SymExpr sym b
      -> IO (SymExpr sym (BaseArrayType (idx ::> itp) b)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f ('BaseToType (BaseArrayType (idx ::> itp) b))
-> IO (RegValue sym ('BaseToType (BaseArrayType (idx ::> itp) b)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseArrayType (idx ::> itp) b))
a
        IO
  (Assignment (SymExpr sym) (idx ::> itp)
   -> SymExpr sym b
   -> IO (SymExpr sym (BaseArrayType (idx ::> itp) b)))
-> IO (Assignment (SymExpr sym) (idx ::> itp))
-> IO
     (SymExpr sym b -> IO (SymExpr sym (BaseArrayType (idx ::> itp) b)))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: BaseType). BaseTerm f x -> IO (SymExpr sym x))
-> forall (x :: Ctx BaseType).
   Assignment (BaseTerm f) x -> IO (Assignment (SymExpr 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 :: BaseType -> Type) (g :: BaseType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: BaseType). f x -> m (g x))
-> forall (x :: Ctx BaseType). Assignment f x -> m (Assignment g x)
traverseFC (sym
-> (forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp))
-> BaseTerm f x
-> IO (SymExpr sym x)
forall sym (f :: CrucibleType -> Type) (vtp :: BaseType).
IsSymInterface sym =>
sym
-> (forall (utp :: CrucibleType). f utp -> IO (RegValue sym utp))
-> BaseTerm f vtp
-> IO (SymExpr sym vtp)
evalBase sym
sym f utp -> IO (RegValue sym utp)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub) Assignment (BaseTerm f) (idx ::> itp)
i
        IO
  (SymExpr sym b -> IO (SymExpr sym (BaseArrayType (idx ::> itp) b)))
-> IO (SymExpr sym b)
-> IO (IO (SymExpr sym (BaseArrayType (idx ::> itp) b)))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> f (BaseToType b) -> IO (RegValue sym (BaseToType b))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BaseToType b)
v

    ----------------------------------------------------------------------
    -- Handle

    HandleLit FnHandle args ret
h -> FnVal sym args ret -> IO (FnVal sym args ret)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (FnHandle args ret -> FnVal sym args ret
forall (args :: Ctx CrucibleType) (res :: CrucibleType) sym.
FnHandle args res -> FnVal sym args res
HandleFnVal FnHandle args ret
h)

    Closure CtxRepr args
_ TypeRepr ret
_ f (FunctionHandleType (args ::> tp1) ret)
h_expr TypeRepr tp1
tp f tp1
v_expr -> do
      FnVal sym (args ::> tp1) ret
h <- f (FunctionHandleType (args ::> tp1) ret)
-> IO (RegValue sym (FunctionHandleType (args ::> tp1) ret))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FunctionHandleType (args ::> tp1) ret)
h_expr
      RegValue sym tp1
v <- f tp1 -> IO (RegValue sym tp1)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f tp1
v_expr
      FnVal sym args ret -> IO (FnVal sym args ret)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (FnVal sym args ret -> IO (FnVal sym args ret))
-> FnVal sym args ret -> IO (FnVal sym args ret)
forall a b. (a -> b) -> a -> b
$! FnVal sym (args ::> tp1) ret
-> TypeRepr tp1 -> RegValue sym tp1 -> FnVal sym args ret
forall sym (args :: Ctx CrucibleType) (tp :: CrucibleType)
       (res :: CrucibleType).
FnVal sym (args ::> tp) res
-> TypeRepr tp -> RegValue sym tp -> FnVal sym args res
ClosureFnVal FnVal sym (args ::> tp1) ret
h TypeRepr tp1
tp RegValue sym tp1
v

    ----------------------------------------------------------------------
    -- RealVal

    RationalLit Rational
d -> sym -> Rational -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Rational -> IO (SymReal sym)
realLit sym
sym Rational
d
    RealNeg f ('BaseToType BaseRealType)
xe -> do
      SymReal sym
x <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
xe
      sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymReal sym)
realNeg sym
sym SymReal sym
x
    RealAdd f ('BaseToType BaseRealType)
xe f ('BaseToType BaseRealType)
ye -> do
      SymReal sym
x <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
xe
      SymReal sym
y <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
ye
      sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realAdd sym
sym SymReal sym
x SymReal sym
y
    RealSub f ('BaseToType BaseRealType)
xe f ('BaseToType BaseRealType)
ye -> do
      SymReal sym
x <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
xe
      SymReal sym
y <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
ye
      sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub sym
sym SymReal sym
x SymReal sym
y
    RealMul f ('BaseToType BaseRealType)
xe f ('BaseToType BaseRealType)
ye -> do
      SymReal sym
x <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
xe
      SymReal sym
y <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
ye
      sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul sym
sym SymReal sym
x SymReal sym
y
    RealDiv f ('BaseToType BaseRealType)
xe f ('BaseToType BaseRealType)
ye -> do
      SymReal sym
x <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
xe
      SymReal sym
y <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
ye
      sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realDiv sym
sym SymReal sym
x SymReal sym
y
    RealMod f ('BaseToType BaseRealType)
xe f ('BaseToType BaseRealType)
ye -> do
      SymReal sym
x <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
xe
      SymReal sym
y <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
ye
      sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMod sym
sym SymReal sym
x SymReal sym
y
    RealLt f ('BaseToType BaseRealType)
x_expr f ('BaseToType BaseRealType)
y_expr -> do
      SymReal sym
x <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
x_expr
      SymReal sym
y <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
y_expr
      sym -> SymReal sym -> SymReal sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLt sym
sym SymReal sym
x SymReal sym
y
    RealLe f ('BaseToType BaseRealType)
x_expr f ('BaseToType BaseRealType)
y_expr -> do
      SymReal sym
x <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
x_expr
      SymReal sym
y <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
y_expr
      sym -> SymReal sym -> SymReal sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLe sym
sym SymReal sym
x SymReal sym
y
    RealIsInteger f ('BaseToType BaseRealType)
x_expr -> do
      SymReal sym
x <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
x_expr
      sym -> SymReal sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
isInteger sym
sym SymReal sym
x

    ----------------------------------------------------------------------
    -- Float

    -- This is not necessarily considered correct, see crucible#366
    FloatUndef FloatInfoRepr fi
f -> sym
-> SolverSymbol
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
emptySymbol (sym
-> FloatInfoRepr fi
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> BaseTypeRepr (SymInterpretedFloatType sym fi)
iFloatBaseTypeRepr sym
sym FloatInfoRepr fi
f)

    FloatLit Float
f -> sym -> Float -> IO (SymInterpretedFloat sym SingleFloat)
forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Float -> IO (SymInterpretedFloat sym SingleFloat)
iFloatLitSingle sym
sym Float
f
    DoubleLit Double
d -> sym -> Double -> IO (SymInterpretedFloat sym DoubleFloat)
forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Double -> IO (SymInterpretedFloat sym DoubleFloat)
iFloatLitDouble sym
sym Double
d
    X86_80Lit X86_80Val
ld -> sym -> X86_80Val -> IO (SymInterpretedFloat sym X86_80Float)
forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> X86_80Val -> IO (SymInterpretedFloat sym X86_80Float)
iFloatLitLongDouble sym
sym X86_80Val
ld
    FloatNaN FloatInfoRepr fi
fi -> sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatNaN sym
sym FloatInfoRepr fi
fi
    FloatPInf FloatInfoRepr fi
fi -> sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatPInf sym
sym FloatInfoRepr fi
fi
    FloatNInf FloatInfoRepr fi
fi -> sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatNInf sym
sym FloatInfoRepr fi
fi
    FloatPZero FloatInfoRepr fi
fi -> sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatPZero sym
sym FloatInfoRepr fi
fi
    FloatNZero FloatInfoRepr fi
fi -> sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym -> FloatInfoRepr fi -> IO (SymInterpretedFloat sym fi)
iFloatNZero sym
sym FloatInfoRepr fi
fi
    FloatNeg FloatInfoRepr fi
_ (f ('FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
iFloatNeg @_ @fi sym
sym (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
    FloatAbs FloatInfoRepr fi
_ (f ('FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
iFloatAbs @_ @fi sym
sym (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
    FloatSqrt FloatInfoRepr fi
_ RoundingMode
rm (f ('FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatSqrt @_ @fi sym
sym RoundingMode
rm (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
    FloatAdd FloatInfoRepr fi
_ RoundingMode
rm (f ('FloatType fi)
x_expr :: f (FloatType fi)) f ('FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatAdd @_ @fi sym
sym RoundingMode
rm SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatSub FloatInfoRepr fi
_ RoundingMode
rm (f ('FloatType fi)
x_expr :: f (FloatType fi)) f ('FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatSub @_ @fi sym
sym RoundingMode
rm SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatMul FloatInfoRepr fi
_ RoundingMode
rm (f ('FloatType fi)
x_expr :: f (FloatType fi)) f ('FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatMul @_ @fi sym
sym RoundingMode
rm SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatDiv FloatInfoRepr fi
_ RoundingMode
rm (f ('FloatType fi)
x_expr :: f (FloatType fi)) f ('FloatType fi)
y_expr -> do
      -- TODO: handle division by zero
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatDiv @_ @fi sym
sym RoundingMode
rm SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatRem FloatInfoRepr fi
_ (f ('FloatType fi)
x_expr :: f (FloatType fi)) f ('FloatType fi)
y_expr -> do
      -- TODO: handle division by zero
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatRem @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatMin FloatInfoRepr fi
_ (f ('FloatType fi)
x_expr :: f (FloatType fi)) f ('FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatMin @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatMax FloatInfoRepr fi
_ (f ('FloatType fi)
x_expr :: f (FloatType fi)) f ('FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatMax @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatFMA FloatInfoRepr fi
_ RoundingMode
rm (f ('FloatType fi)
x_expr :: f (FloatType fi)) f ('FloatType fi)
y_expr f ('FloatType fi)
z_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
y_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
z <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
z_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatFMA @_ @fi sym
sym RoundingMode
rm SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y SymExpr sym (SymInterpretedFloatType sym fi)
z
    FloatEq (f (FloatType fi)
x_expr :: f (FloatType fi)) f (FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatEq @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatFpEq (f (FloatType fi)
x_expr :: f (FloatType fi)) f (FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatFpEq @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatIte FloatInfoRepr fi
_ f ('BaseToType BaseBoolType)
c_expr (f ('FloatType fi)
x_expr :: f (FloatType fi)) f ('FloatType fi)
y_expr -> do
      SymExpr sym BaseBoolType
c <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
c_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f ('FloatType fi) -> IO (RegValue sym ('FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatIte @_ @fi sym
sym SymExpr sym BaseBoolType
c SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatLt (f (FloatType fi)
x_expr :: f (FloatType fi)) f (FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatLt @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatLe (f (FloatType fi)
x_expr :: f (FloatType fi)) f (FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatLe @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatGt (f (FloatType fi)
x_expr :: f (FloatType fi)) f (FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatGt @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatGe (f (FloatType fi)
x_expr :: f (FloatType fi)) f (FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatGe @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatNe (f (FloatType fi)
x_expr :: f (FloatType fi)) f (FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatNe @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatFpApart (f (FloatType fi)
x_expr :: f (FloatType fi)) f (FloatType fi)
y_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
      SymExpr sym (SymInterpretedFloatType sym fi)
y <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
y_expr
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatFpApart @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
x SymExpr sym (SymInterpretedFloatType sym fi)
y
    FloatCast FloatInfoRepr fi
fi RoundingMode
rm (f (FloatType fi')
x_expr :: f (FloatType fi')) ->
      forall sym (fi :: FloatInfo) (fi' :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymInterpretedFloat sym fi'
-> IO (SymInterpretedFloat sym fi)
iFloatCast @_ @_ @fi' sym
sym FloatInfoRepr fi
fi RoundingMode
rm (SymExpr sym (SymInterpretedFloatType sym fi')
 -> IO (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi'))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi') -> IO (RegValue sym (FloatType fi'))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi')
x_expr
    FloatFromBinary FloatInfoRepr fi
fi f (BVType (FloatInfoToBitWidth fi))
x_expr -> sym
-> FloatInfoRepr fi
-> SymExpr sym (BaseBVType (FloatInfoToBitWidth fi))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
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 fi
fi (SymExpr sym (BaseBVType (FloatInfoToBitWidth fi))
 -> IO (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (BaseBVType (FloatInfoToBitWidth fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (BVType (FloatInfoToBitWidth fi))
-> IO (RegValue sym (BVType (FloatInfoToBitWidth fi)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType (FloatInfoToBitWidth fi))
x_expr
    FloatToBinary FloatInfoRepr fi
fi f (FloatType fi)
x_expr -> sym
-> FloatInfoRepr fi
-> SymExpr sym (SymInterpretedFloatType sym fi)
-> IO (SymExpr sym (BaseBVType (FloatInfoToBitWidth fi)))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymInterpretedFloat sym fi
-> IO (SymBV sym (FloatInfoToBitWidth fi))
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymInterpretedFloat sym fi
-> IO (SymBV sym (FloatInfoToBitWidth fi))
iFloatToBinary sym
sym FloatInfoRepr fi
fi (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym (BaseBVType (FloatInfoToBitWidth fi))))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym (BaseBVType (FloatInfoToBitWidth fi)))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
    FloatFromBV FloatInfoRepr fi
fi RoundingMode
rm f (BVType w)
x_expr -> sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (w :: Natural) (fi :: FloatInfo).
(1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
iBVToFloat sym
sym FloatInfoRepr fi
fi RoundingMode
rm (SymExpr sym (BaseBVType w)
 -> IO (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (BaseBVType w))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
x_expr
    FloatFromSBV FloatInfoRepr fi
fi RoundingMode
rm f (BVType w)
x_expr -> sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (w :: Natural) (fi :: FloatInfo).
(1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
iSBVToFloat sym
sym FloatInfoRepr fi
fi RoundingMode
rm (SymExpr sym (BaseBVType w)
 -> IO (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (BaseBVType w))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
x_expr
    FloatFromReal FloatInfoRepr fi
fi RoundingMode
rm f ('BaseToType BaseRealType)
x_expr -> sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymReal sym
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymReal sym
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymReal sym
-> IO (SymInterpretedFloat sym fi)
iRealToFloat sym
sym FloatInfoRepr fi
fi RoundingMode
rm (SymReal sym -> IO (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymReal sym)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
x_expr
    FloatToBV NatRepr w
w RoundingMode
rm (f (FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> NatRepr w
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymBV sym w)
iFloatToBV @_ @_ @fi sym
sym NatRepr w
w RoundingMode
rm (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym (BaseBVType w)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym (BaseBVType w))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
    FloatToSBV NatRepr w
w RoundingMode
rm (f (FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> NatRepr w
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymBV sym w)
iFloatToSBV @_ @_ @fi sym
sym NatRepr w
w RoundingMode
rm (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym (BaseBVType w)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym (BaseBVType w))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
    FloatToReal (f (FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (SymReal sym)
iFloatToReal @_ @fi sym
sym (SymExpr sym (SymInterpretedFloatType sym fi) -> IO (SymReal sym))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
    FloatIsNaN (f (FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsNaN @_ @fi sym
sym (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
    FloatIsInfinite (f (FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsInf @_ @fi sym
sym (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
    FloatIsZero (f (FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsZero @_ @fi sym
sym (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
    FloatIsPositive (f (FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsPos @_ @fi sym
sym (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
    FloatIsNegative (f (FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsNeg @_ @fi sym
sym (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
    FloatIsSubnormal (f (FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsSubnorm @_ @fi sym
sym (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
    FloatIsNormal (f (FloatType fi)
x_expr :: f (FloatType fi)) ->
      forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsNorm @_ @fi sym
sym (SymExpr sym (SymInterpretedFloatType sym fi)
 -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr

    ----------------------------------------------------------------------
    -- Conversions

    NatToInteger f 'NatType
x_expr -> do
      SymNat sym
x <- f 'NatType -> IO (RegValue sym 'NatType)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f 'NatType
x_expr
      sym -> SymNat sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> IO (SymInteger sym)
natToInteger sym
sym SymNat sym
x
    IntegerToReal f ('BaseToType BaseIntegerType)
x_expr -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
x_expr
      sym -> SymInteger sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymReal sym)
integerToReal sym
sym SymInteger sym
x
    RealToNat f ('BaseToType BaseRealType)
x_expr -> do
      SymReal sym
x <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
x_expr
      sym -> SymReal sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymNat sym)
realToNat sym
sym SymReal sym
x
    BvToNat NatRepr w
_ f (BVType w)
xe -> do
      sym -> SymExpr sym (BaseBVType w) -> IO (SymNat sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymNat sym)
bvToNat sym
sym (SymExpr sym (BaseBVType w) -> IO (SymNat sym))
-> IO (SymExpr sym (BaseBVType w)) -> IO (SymNat sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
    BvToInteger NatRepr w
_ f (BVType w)
xe -> do
      sym -> SymExpr sym (BaseBVType w) -> IO (SymInteger sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
bvToInteger sym
sym (SymExpr sym (BaseBVType w) -> IO (SymInteger sym))
-> IO (SymExpr sym (BaseBVType w)) -> IO (SymInteger sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
    SbvToInteger NatRepr w
_ f (BVType w)
xe -> do
      sym -> SymExpr sym (BaseBVType w) -> IO (SymInteger sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
sbvToInteger sym
sym (SymExpr sym (BaseBVType w) -> IO (SymInteger sym))
-> IO (SymExpr sym (BaseBVType w)) -> IO (SymInteger sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
    RealFloor f ('BaseToType BaseRealType)
xe ->
      sym -> SymReal sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realFloor sym
sym (SymReal sym -> IO (SymInteger sym))
-> IO (SymReal sym) -> IO (SymInteger sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
xe
    RealCeil f ('BaseToType BaseRealType)
xe ->
      sym -> SymReal sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realCeil sym
sym (SymReal sym -> IO (SymInteger sym))
-> IO (SymReal sym) -> IO (SymInteger sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
xe
    RealRound f ('BaseToType BaseRealType)
xe ->
      sym -> SymReal sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (SymInteger sym)
realRound sym
sym (SymReal sym -> IO (SymInteger sym))
-> IO (SymReal sym) -> IO (SymInteger sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
xe
    IntegerToBV NatRepr w
w f ('BaseToType BaseIntegerType)
xe -> do
      SymInteger sym
x <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
xe
      sym
-> SymInteger sym -> NatRepr w -> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
integerToBV sym
sym SymInteger sym
x NatRepr w
w

    ----------------------------------------------------------------------
    -- ComplexReal

    Complex f ('BaseToType BaseRealType)
r_expr f ('BaseToType BaseRealType)
i_expr -> do
      SymReal sym
r <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
r_expr
      SymReal sym
i <- f ('BaseToType BaseRealType)
-> IO (RegValue sym ('BaseToType BaseRealType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseRealType)
i_expr
      sym -> Complex (SymReal sym) -> IO (SymExpr sym BaseComplexType)
forall sym.
IsExprBuilder sym =>
sym -> Complex (SymReal sym) -> IO (SymCplx sym)
mkComplex sym
sym (SymReal sym
r SymReal sym -> SymReal sym -> Complex (SymReal sym)
forall a. a -> a -> Complex a
:+ SymReal sym
i)
    RealPart f ('BaseToType BaseComplexType)
c_expr -> sym -> SymExpr sym BaseComplexType -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymReal sym)
getRealPart sym
sym (SymExpr sym BaseComplexType -> IO (SymReal sym))
-> IO (SymExpr sym BaseComplexType) -> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('BaseToType BaseComplexType)
-> IO (RegValue sym ('BaseToType BaseComplexType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseComplexType)
c_expr
    ImagPart f ('BaseToType BaseComplexType)
c_expr -> sym -> SymExpr sym BaseComplexType -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> SymCplx sym -> IO (SymReal sym)
getImagPart sym
sym (SymExpr sym BaseComplexType -> IO (SymReal sym))
-> IO (SymExpr sym BaseComplexType) -> IO (SymReal sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('BaseToType BaseComplexType)
-> IO (RegValue sym ('BaseToType BaseComplexType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseComplexType)
c_expr

    --------------------------------------------------------------------
    -- BVs

    -- This is not necessarily considered correct, see crucible#366
    BVUndef NatRepr w
w ->
      sym
-> SolverSymbol
-> BaseTypeRepr (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshConstant sym
sym SolverSymbol
emptySymbol (NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr NatRepr w
w)

    BVLit NatRepr w
w BV w
bv -> sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w BV w
bv

    BVConcat NatRepr u
_ NatRepr v
_ f (BVType u)
xe f (BVType v)
ye -> do
      SymExpr sym ('BaseBVType u)
x <- f (BVType u) -> IO (RegValue sym (BVType u))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType u)
xe
      SymExpr sym ('BaseBVType v)
y <- f (BVType v) -> IO (RegValue sym (BVType v))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType v)
ye
      sym
-> SymExpr sym ('BaseBVType u)
-> SymExpr sym ('BaseBVType v)
-> IO (SymExpr sym (BaseBVType (u + v)))
forall (u :: Natural) (v :: Natural).
(1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
forall sym (u :: Natural) (v :: Natural).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
bvConcat sym
sym SymExpr sym ('BaseBVType u)
x SymExpr sym ('BaseBVType v)
y
    -- FIXME: there are probably some worthwhile special cases to exploit in "BVSelect"
    BVSelect NatRepr idx
idx NatRepr len
n NatRepr w
_ f (BVType w)
xe -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      sym
-> NatRepr idx
-> NatRepr len
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym (BaseBVType len))
forall (idx :: Natural) (n :: Natural) (w :: Natural).
(1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
bvSelect sym
sym NatRepr idx
idx NatRepr len
n SymExpr sym ('BaseBVType w)
x
    BVTrunc NatRepr r
w' NatRepr w
_ f (BVType w)
xe -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      sym
-> NatRepr r
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym (BaseBVType r))
forall (r :: Natural) (w :: Natural).
(1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
bvTrunc sym
sym NatRepr r
w' SymExpr sym ('BaseBVType w)
x
    BVZext NatRepr r
w' NatRepr w
_ f (BVType w)
xe -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      sym
-> NatRepr r
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym (BaseBVType r))
forall (u :: Natural) (r :: Natural).
(1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvZext sym
sym NatRepr r
w' SymExpr sym ('BaseBVType w)
x
    BVSext NatRepr r
w' NatRepr w
_ f (BVType w)
xe -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      sym
-> NatRepr r
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym (BaseBVType r))
forall (u :: Natural) (r :: Natural).
(1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext sym
sym NatRepr r
w' SymExpr sym ('BaseBVType w)
x
    BVNot NatRepr w
_ f ('BaseToType (BaseBVType w))
xe ->
      sym
-> SymExpr sym (BaseBVType w) -> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvNotBits sym
sym (SymExpr sym (BaseBVType w) -> IO (SymExpr sym (BaseBVType w)))
-> IO (SymExpr sym (BaseBVType w))
-> IO (SymExpr sym (BaseBVType w))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
    BVAnd NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAndBits sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVOr NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvOrBits sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVXor NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvXorBits sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVAdd NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVNeg NatRepr w
_ f ('BaseToType (BaseBVType w))
xe -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      sym
-> SymExpr sym (BaseBVType w) -> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvNeg sym
sym SymExpr sym (BaseBVType w)
x
    BVSub NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSub sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVMul NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVUdiv NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvUdiv sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVSdiv NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSdiv sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVUrem NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvUrem sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVSrem NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSrem sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y

    BVUlt NatRepr w
_ f (BVType w)
xe f (BVType w)
ye -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      SymExpr sym ('BaseBVType w)
y <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
ye
      sym
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUlt sym
sym SymExpr sym ('BaseBVType w)
x SymExpr sym ('BaseBVType w)
y
    BVSlt NatRepr w
_ f (BVType w)
xe f (BVType w)
ye -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      SymExpr sym ('BaseBVType w)
y <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
ye
      sym
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt sym
sym SymExpr sym ('BaseBVType w)
x SymExpr sym ('BaseBVType w)
y
    BoolToBV NatRepr w
w f ('BaseToType BaseBoolType)
xe -> do
      SymExpr sym BaseBoolType
x <- f ('BaseToType BaseBoolType)
-> IO (RegValue sym ('BaseToType BaseBoolType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseBoolType)
xe
      SymExpr sym (BaseBVType w)
one <- sym -> NatRepr w -> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvOne sym
sym NatRepr w
w
      SymExpr sym (BaseBVType w)
zro <- sym -> NatRepr w -> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr w
w
      sym
-> SymExpr sym BaseBoolType
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
x SymExpr sym (BaseBVType w)
one SymExpr sym (BaseBVType w)
zro
    BVNonzero NatRepr w
_ f (BVType w)
xe -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      sym -> SymExpr sym ('BaseBVType w) -> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym SymExpr sym ('BaseBVType w)
x
    BVShl NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvShl sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVLshr NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvLshr sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVAshr NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAshr sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVRol NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvRol sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVRor NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvRor sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVCountTrailingZeros NatRepr w
_ f ('BaseToType (BaseBVType w))
xe -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      sym
-> SymExpr sym (BaseBVType w) -> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvCountTrailingZeros sym
sym SymExpr sym (BaseBVType w)
x
    BVCountLeadingZeros NatRepr w
_ f ('BaseToType (BaseBVType w))
xe -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      sym
-> SymExpr sym (BaseBVType w) -> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvCountLeadingZeros sym
sym SymExpr sym (BaseBVType w)
x
    BVPopcount NatRepr w
_ f ('BaseToType (BaseBVType w))
xe -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      sym
-> SymExpr sym (BaseBVType w) -> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvPopcount sym
sym SymExpr sym (BaseBVType w)
x
    BVCarry NatRepr w
_ f (BVType w)
xe f (BVType w)
ye -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      SymExpr sym ('BaseBVType w)
y <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
ye
      (SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
-> SymExpr sym BaseBoolType
forall a b. (a, b) -> a
fst ((SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
 -> SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
-> IO (SymExpr sym BaseBoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymExpr sym BaseBoolType, SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
addUnsignedOF sym
sym SymExpr sym ('BaseBVType w)
x SymExpr sym ('BaseBVType w)
y
    BVSCarry NatRepr w
_ f (BVType w)
xe f (BVType w)
ye -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      SymExpr sym ('BaseBVType w)
y <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
ye
      (SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
-> SymExpr sym BaseBoolType
forall a b. (a, b) -> a
fst ((SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
 -> SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
-> IO (SymExpr sym BaseBoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymExpr sym BaseBoolType, SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
addSignedOF sym
sym SymExpr sym ('BaseBVType w)
x SymExpr sym ('BaseBVType w)
y
    BVSBorrow NatRepr w
_ f (BVType w)
xe f (BVType w)
ye -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      SymExpr sym ('BaseBVType w)
y <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
ye
      (SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
-> SymExpr sym BaseBoolType
forall a b. (a, b) -> a
fst ((SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
 -> SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
-> IO (SymExpr sym BaseBoolType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym BaseBoolType, SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymExpr sym BaseBoolType, SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
subSignedOF sym
sym SymExpr sym ('BaseBVType w)
x SymExpr sym ('BaseBVType w)
y
    BVUle NatRepr w
_ f (BVType w)
xe f (BVType w)
ye -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      SymExpr sym ('BaseBVType w)
y <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
ye
      sym
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUle sym
sym SymExpr sym ('BaseBVType w)
x SymExpr sym ('BaseBVType w)
y
    BVSle NatRepr w
_ f (BVType w)
xe f (BVType w)
ye -> do
      SymExpr sym ('BaseBVType w)
x <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
xe
      SymExpr sym ('BaseBVType w)
y <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
ye
      sym
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSle sym
sym SymExpr sym ('BaseBVType w)
x SymExpr sym ('BaseBVType w)
y
    BVUMin NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      SymExpr sym BaseBoolType
c <- sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUle sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
      sym
-> SymExpr sym BaseBoolType
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
c SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVUMax NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      SymExpr sym BaseBoolType
c <- sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUgt sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
      sym
-> SymExpr sym BaseBoolType
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
c SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVSMin NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      SymExpr sym BaseBoolType
c <- sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSle sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
      sym
-> SymExpr sym BaseBoolType
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
c SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
    BVSMax NatRepr w
_ f ('BaseToType (BaseBVType w))
xe f ('BaseToType (BaseBVType w))
ye -> do
      SymExpr sym (BaseBVType w)
x <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
xe
      SymExpr sym (BaseBVType w)
y <- f ('BaseToType (BaseBVType w))
-> IO (RegValue sym ('BaseToType (BaseBVType w)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseBVType w))
ye
      SymExpr sym BaseBoolType
c <- sym
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSgt sym
sym SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y
      sym
-> SymExpr sym BaseBoolType
-> SymExpr sym (BaseBVType w)
-> SymExpr sym (BaseBVType w)
-> IO (SymExpr sym (BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
c SymExpr sym (BaseBVType w)
x SymExpr sym (BaseBVType w)
y

    --------------------------------------------------------------------
    -- Word Maps

    EmptyWordMap NatRepr w
w BaseTypeRepr tp1
tp -> do
      sym -> NatRepr w -> BaseTypeRepr tp1 -> IO (WordMap sym w tp1)
forall sym (w :: Natural) (a :: BaseType).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BaseTypeRepr a -> IO (WordMap sym w a)
emptyWordMap sym
sym NatRepr w
w BaseTypeRepr tp1
tp

    InsertWordMap NatRepr w
w BaseTypeRepr tp1
tp f (BVType w)
ie f (BaseToType tp1)
ve f ('WordMapType w tp1)
me -> do
      SymExpr sym ('BaseBVType w)
i <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
ie
      SymExpr sym tp1
v <- f (BaseToType tp1) -> IO (RegValue sym (BaseToType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BaseToType tp1)
ve
      WordMap sym w tp1
m <- f ('WordMapType w tp1) -> IO (RegValue sym ('WordMapType w tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('WordMapType w tp1)
me
      sym
-> NatRepr w
-> BaseTypeRepr tp1
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym tp1
-> WordMap sym w tp1
-> IO (WordMap sym w tp1)
forall sym (w :: Natural) (a :: BaseType).
IsExprBuilder sym =>
sym
-> NatRepr w
-> BaseTypeRepr a
-> SymBV sym w
-> SymExpr sym a
-> WordMap sym w a
-> IO (WordMap sym w a)
insertWordMap sym
sym NatRepr w
w BaseTypeRepr tp1
tp SymExpr sym ('BaseBVType w)
i SymExpr sym tp1
v WordMap sym w tp1
m

    LookupWordMap BaseTypeRepr tp1
tp f (BVType w)
ie f (WordMapType w tp1)
me -> do
      SymExpr sym (BaseBVType w)
i <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
ie
      WordMap sym w tp1
m <- f (WordMapType w tp1) -> IO (RegValue sym (WordMapType w tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (WordMapType w tp1)
me
      PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp1)
x <- sym
-> NatRepr w
-> BaseTypeRepr tp1
-> SymExpr sym (BaseBVType w)
-> WordMap sym w tp1
-> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp1))
forall sym (w :: Natural) (a :: BaseType).
IsExprBuilder sym =>
sym
-> NatRepr w
-> BaseTypeRepr a
-> SymBV sym w
-> WordMap sym w a
-> IO (PartExpr (Pred sym) (SymExpr sym a))
lookupWordMap sym
sym (SymExpr sym (BaseBVType w) -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymExpr sym (BaseBVType w)
i) BaseTypeRepr tp1
tp SymExpr sym (BaseBVType w)
i WordMap sym w tp1
m
      let msg :: String
msg = String
"WordMap: read an undefined index" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                case SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV SymExpr sym (BaseBVType w)
i of
                   Maybe (BV w)
Nothing  -> String
""
                   Just (BV.BV Integer
idx) -> String
" 0x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String -> String
forall a. Integral a => a -> String -> String
showHex Integer
idx String
""
      let ex :: SimErrorReason
ex = String -> SimErrorReason
ReadBeforeWriteSimError String
msg
      bak
-> PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp1)
-> SimErrorReason
-> IO (SymExpr sym tp1)
forall sym bak v.
IsSymBackend sym bak =>
bak -> PartExpr (Pred sym) v -> SimErrorReason -> IO v
readPartExpr bak
bak PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp1)
x SimErrorReason
ex

    LookupWordMapWithDefault BaseTypeRepr tp1
tp f (BVType w)
ie f (WordMapType w tp1)
me f ('BaseToType tp1)
de -> do
      SymExpr sym (BaseBVType w)
i <- f (BVType w) -> IO (RegValue sym (BVType w))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BVType w)
ie
      WordMap sym w tp1
m <- f (WordMapType w tp1) -> IO (RegValue sym (WordMapType w tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (WordMapType w tp1)
me
      SymExpr sym tp1
d <- f ('BaseToType tp1) -> IO (RegValue sym ('BaseToType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType tp1)
de
      PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp1)
x <- sym
-> NatRepr w
-> BaseTypeRepr tp1
-> SymExpr sym (BaseBVType w)
-> WordMap sym w tp1
-> IO (PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp1))
forall sym (w :: Natural) (a :: BaseType).
IsExprBuilder sym =>
sym
-> NatRepr w
-> BaseTypeRepr a
-> SymBV sym w
-> WordMap sym w a
-> IO (PartExpr (Pred sym) (SymExpr sym a))
lookupWordMap sym
sym (SymExpr sym (BaseBVType w) -> NatRepr w
forall (w :: Natural). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymExpr sym (BaseBVType w)
i) BaseTypeRepr tp1
tp SymExpr sym (BaseBVType w)
i WordMap sym w tp1
m
      case PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp1)
x of
        PartExpr (SymExpr sym BaseBoolType) (SymExpr sym tp1)
Unassigned -> SymExpr sym tp1 -> IO (SymExpr sym tp1)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymExpr sym tp1
d
        PE SymExpr sym BaseBoolType
p SymExpr sym tp1
v -> do
          sym
-> IntrinsicTypes sym
-> TypeRepr ('BaseToType tp1)
-> ValMuxFn sym ('BaseToType tp1)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
sym IntrinsicTypes sym
itefns (BaseTypeRepr tp1 -> TypeRepr ('BaseToType tp1)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType BaseTypeRepr tp1
tp) SymExpr sym BaseBoolType
p SymExpr sym tp1
RegValue sym ('BaseToType tp1)
v SymExpr sym tp1
RegValue sym ('BaseToType tp1)
d

    ---------------------------------------------------------------------
    -- Struct

    MkStruct CtxRepr ctx
_ Assignment f ctx
exprs -> (forall (x :: CrucibleType). f x -> IO (RegValue' sym x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> IO (Assignment (RegValue' 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 (\f x
x -> RegValue sym x -> RegValue' sym x
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (RegValue sym x -> RegValue' sym x)
-> IO (RegValue sym x) -> IO (RegValue' sym x)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> IO (RegValue sym x)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f x
x) Assignment f ctx
exprs

    GetStruct f (StructType ctx)
st Index ctx tp
idx TypeRepr tp
_ -> do
      Assignment (RegValue' sym) ctx
struct <- f (StructType ctx) -> IO (RegValue sym (StructType ctx))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StructType ctx)
st
      RegValue sym tp -> IO (RegValue sym tp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (RegValue sym tp -> IO (RegValue sym tp))
-> RegValue sym tp -> IO (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ RegValue' sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV (RegValue' sym tp -> RegValue sym tp)
-> RegValue' sym tp -> RegValue sym tp
forall a b. (a -> b) -> a -> b
$ Assignment (RegValue' sym) ctx
struct Assignment (RegValue' sym) ctx -> Index ctx tp -> RegValue' sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
idx

    SetStruct CtxRepr ctx
_ f ('StructType ctx)
st Index ctx tp1
idx f tp1
x -> do
      Assignment (RegValue' sym) ctx
struct <- f ('StructType ctx) -> IO (RegValue sym ('StructType ctx))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('StructType ctx)
st
      RegValue sym tp1
v <- f tp1 -> IO (RegValue sym tp1)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f tp1
x
      Assignment (RegValue' sym) ctx
-> IO (Assignment (RegValue' sym) ctx)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Assignment (RegValue' sym) ctx
 -> IO (Assignment (RegValue' sym) ctx))
-> Assignment (RegValue' sym) ctx
-> IO (Assignment (RegValue' sym) ctx)
forall a b. (a -> b) -> a -> b
$ Assignment (RegValue' sym) ctx
struct Assignment (RegValue' sym) ctx
-> (Assignment (RegValue' sym) ctx
    -> Assignment (RegValue' sym) ctx)
-> Assignment (RegValue' sym) ctx
forall a b. a -> (a -> b) -> b
& IndexF (Assignment (RegValue' sym) ctx) tp1
-> Traversal'
     (Assignment (RegValue' sym) ctx)
     (IxValueF (Assignment (RegValue' sym) ctx) tp1)
forall k m (x :: k).
IxedF k m =>
IndexF m x -> Traversal' m (IxValueF m x)
forall (x :: CrucibleType).
IndexF (Assignment (RegValue' sym) ctx) x
-> Traversal'
     (Assignment (RegValue' sym) ctx)
     (IxValueF (Assignment (RegValue' sym) ctx) x)
ixF IndexF (Assignment (RegValue' sym) ctx) tp1
Index ctx tp1
idx ((IxValueF (Assignment (RegValue' sym) ctx) tp1
  -> Identity (RegValue' sym tp1))
 -> Assignment (RegValue' sym) ctx
 -> Identity (Assignment (RegValue' sym) ctx))
-> RegValue' sym tp1
-> Assignment (RegValue' sym) ctx
-> Assignment (RegValue' sym) ctx
forall s t a b. ASetter s t a b -> b -> s -> t
.~ RegValue sym tp1 -> RegValue' sym tp1
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV RegValue sym tp1
v

    ----------------------------------------------------------------------
    -- Variant

    InjectVariant CtxRepr ctx
ctx Index ctx tp1
idx f tp1
ve -> do
         RegValue sym tp1
v <- f tp1 -> IO (RegValue sym tp1)
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f tp1
ve
         Assignment (VariantBranch sym) ctx
-> IO (Assignment (VariantBranch sym) ctx)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Assignment (VariantBranch sym) ctx
 -> IO (Assignment (VariantBranch sym) ctx))
-> Assignment (VariantBranch sym) ctx
-> IO (Assignment (VariantBranch sym) ctx)
forall a b. (a -> b) -> a -> b
$ sym
-> CtxRepr ctx
-> Index ctx tp1
-> RegValue sym tp1
-> RegValue sym ('VariantType ctx)
forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
IsExprBuilder sym =>
sym
-> CtxRepr ctx
-> Index ctx tp
-> RegValue sym tp
-> RegValue sym (VariantType ctx)
injectVariant sym
sym CtxRepr ctx
ctx Index ctx tp1
idx RegValue sym tp1
v

    ProjectVariant CtxRepr ctx
_ctx Index ctx tp1
idx f (VariantType ctx)
ve -> do
         Assignment (VariantBranch sym) ctx
v <- f (VariantType ctx) -> IO (RegValue sym (VariantType ctx))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (VariantType ctx)
ve
         PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
 -> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a b. (a -> b) -> a -> b
$ VariantBranch sym tp1
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
forall sym (tp :: CrucibleType).
VariantBranch sym tp -> PartExpr (Pred sym) (RegValue sym tp)
unVB (VariantBranch sym tp1
 -> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
-> VariantBranch sym tp1
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
forall a b. (a -> b) -> a -> b
$ Assignment (VariantBranch sym) ctx
v Assignment (VariantBranch sym) ctx
-> Index ctx tp1 -> VariantBranch sym tp1
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp1
idx

    ----------------------------------------------------------------------
    -- IdentValueMap

    EmptyStringMap TypeRepr tp1
_ -> Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
-> IO
     (Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall k a. Map k a
Map.empty

    LookupStringMapEntry TypeRepr tp1
_ f (StringMapType tp1)
m_expr f (StringType Unicode)
i_expr -> do
      SymExpr sym (BaseStringType Unicode)
i <- f (StringType Unicode) -> IO (RegValue sym (StringType Unicode))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType Unicode)
i_expr
      Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
m <- f (StringMapType tp1) -> IO (RegValue sym (StringMapType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringMapType tp1)
m_expr
      case SymExpr sym (BaseStringType Unicode)
-> Maybe (StringLiteral Unicode)
forall (si :: StringInfo).
SymExpr sym (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
asString SymExpr sym (BaseStringType Unicode)
i of
        Just (UnicodeLiteral Text
i') -> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
 -> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a b. (a -> b) -> a -> b
$ Maybe (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
forall p v. Maybe (PartExpr p v) -> PartExpr p v
joinMaybePE (Text
-> Map
     Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
-> Maybe (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
i' Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
m)
        Maybe (StringLiteral Unicode)
Nothing -> bak
-> SimErrorReason
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason
 -> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
-> SimErrorReason
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall a b. (a -> b) -> a -> b
$
                    CallStack -> String -> SimErrorReason
Unsupported CallStack
(?callStack::CallStack) => CallStack
callStack String
"Symbolic string in lookupStringMapEntry"

    InsertStringMapEntry TypeRepr tp1
_ f ('StringMapType tp1)
m_expr f (StringType Unicode)
i_expr f (MaybeType tp1)
v_expr -> do
      Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
m <- f ('StringMapType tp1) -> IO (RegValue sym ('StringMapType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('StringMapType tp1)
m_expr
      SymExpr sym (BaseStringType Unicode)
i <- f (StringType Unicode) -> IO (RegValue sym (StringType Unicode))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType Unicode)
i_expr
      PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
v <- f (MaybeType tp1) -> IO (RegValue sym (MaybeType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (MaybeType tp1)
v_expr
      case SymExpr sym (BaseStringType Unicode)
-> Maybe (StringLiteral Unicode)
forall (si :: StringInfo).
SymExpr sym (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
asString SymExpr sym (BaseStringType Unicode)
i of
        Just (UnicodeLiteral Text
i') -> Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
-> IO
     (Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
 -> IO
      (Map
         Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))))
-> Map
     Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
-> IO
     (Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
forall a b. (a -> b) -> a -> b
$ Text
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> Map
     Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
-> Map
     Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
i' PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
v Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
m
        Maybe (StringLiteral Unicode)
Nothing -> bak
-> SimErrorReason
-> IO
     (Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak (SimErrorReason
 -> IO
      (Map
         Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))))
-> SimErrorReason
-> IO
     (Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
forall a b. (a -> b) -> a -> b
$
                     CallStack -> String -> SimErrorReason
Unsupported CallStack
(?callStack::CallStack) => CallStack
callStack String
"Symbolic string in insertStringMapEntry"

    --------------------------------------------------------------------
    -- Strings

    StringLit StringLiteral si
x -> sym -> StringLiteral si -> IO (SymString sym si)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringLiteral si -> IO (SymString sym si)
stringLit sym
sym StringLiteral si
x
    ShowValue BaseTypeRepr bt
_bt f (BaseToType bt)
x_expr -> do
      SymExpr sym bt
x <- f (BaseToType bt) -> IO (RegValue sym (BaseToType bt))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BaseToType bt)
x_expr
      sym
-> StringLiteral Unicode
-> IO (SymExpr sym (BaseStringType Unicode))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringLiteral si -> IO (SymString sym si)
stringLit sym
sym (Text -> StringLiteral Unicode
UnicodeLiteral (String -> Text
Text.pack (Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym bt -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymExpr sym bt
x))))
    ShowFloat FloatInfoRepr fi
_fi f (FloatType fi)
x_expr -> do
      SymExpr sym (SymInterpretedFloatType sym fi)
x <- f (FloatType fi) -> IO (RegValue sym (FloatType fi))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (FloatType fi)
x_expr
      sym
-> StringLiteral Unicode
-> IO (SymExpr sym (BaseStringType Unicode))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringLiteral si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringLiteral si -> IO (SymString sym si)
stringLit sym
sym (Text -> StringLiteral Unicode
UnicodeLiteral (String -> Text
Text.pack (Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (SymInterpretedFloatType sym fi) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymExpr sym (SymInterpretedFloatType sym fi)
x))))
    StringConcat StringInfoRepr si
_si f ('BaseToType (BaseStringType si))
x f ('BaseToType (BaseStringType si))
y -> do
      SymExpr sym (BaseStringType si)
x' <- f ('BaseToType (BaseStringType si))
-> IO (RegValue sym ('BaseToType (BaseStringType si)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseStringType si))
x
      SymExpr sym (BaseStringType si)
y' <- f ('BaseToType (BaseStringType si))
-> IO (RegValue sym ('BaseToType (BaseStringType si)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseStringType si))
y
      sym
-> SymExpr sym (BaseStringType si)
-> SymExpr sym (BaseStringType si)
-> IO (SymExpr sym (BaseStringType si))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym
-> SymString sym si -> SymString sym si -> IO (SymString sym si)
forall (si :: StringInfo).
sym
-> SymString sym si -> SymString sym si -> IO (SymString sym si)
stringConcat sym
sym SymExpr sym (BaseStringType si)
x' SymExpr sym (BaseStringType si)
y'
    StringEmpty StringInfoRepr si
si ->
      sym -> StringInfoRepr si -> IO (SymString sym si)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> StringInfoRepr si -> IO (SymString sym si)
forall (si :: StringInfo).
sym -> StringInfoRepr si -> IO (SymString sym si)
stringEmpty sym
sym StringInfoRepr si
si
    StringLength f (StringType si)
x -> do
      SymExpr sym ('BaseStringType si)
x' <- f (StringType si) -> IO (RegValue sym (StringType si))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType si)
x
      sym -> SymExpr sym ('BaseStringType si) -> IO (SymInteger sym)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> SymString sym si -> IO (SymInteger sym)
forall (si :: StringInfo).
sym -> SymString sym si -> IO (SymInteger sym)
stringLength sym
sym SymExpr sym ('BaseStringType si)
x'
    StringContains f (StringType si)
x f (StringType si)
y -> do
      SymExpr sym ('BaseStringType si)
x' <- f (StringType si) -> IO (RegValue sym (StringType si))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType si)
x
      SymExpr sym ('BaseStringType si)
y' <- f (StringType si) -> IO (RegValue sym (StringType si))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType si)
y
      sym
-> SymExpr sym ('BaseStringType si)
-> SymExpr sym ('BaseStringType si)
-> IO (SymExpr sym BaseBoolType)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
forall (si :: StringInfo).
sym
-> SymString sym si
-> SymString sym si
-> IO (SymExpr sym BaseBoolType)
stringContains sym
sym SymExpr sym ('BaseStringType si)
x' SymExpr sym ('BaseStringType si)
y'
    StringIsPrefixOf f (StringType si)
x f (StringType si)
y -> do
      SymExpr sym ('BaseStringType si)
x' <- f (StringType si) -> IO (RegValue sym (StringType si))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType si)
x
      SymExpr sym ('BaseStringType si)
y' <- f (StringType si) -> IO (RegValue sym (StringType si))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType si)
y
      sym
-> SymExpr sym ('BaseStringType si)
-> SymExpr sym ('BaseStringType si)
-> IO (SymExpr sym BaseBoolType)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
forall (si :: StringInfo).
sym
-> SymString sym si
-> SymString sym si
-> IO (SymExpr sym BaseBoolType)
stringIsPrefixOf sym
sym SymExpr sym ('BaseStringType si)
x' SymExpr sym ('BaseStringType si)
y'
    StringIsSuffixOf f (StringType si)
x f (StringType si)
y -> do
      SymExpr sym ('BaseStringType si)
x' <- f (StringType si) -> IO (RegValue sym (StringType si))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType si)
x
      SymExpr sym ('BaseStringType si)
y' <- f (StringType si) -> IO (RegValue sym (StringType si))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType si)
y
      sym
-> SymExpr sym ('BaseStringType si)
-> SymExpr sym ('BaseStringType si)
-> IO (SymExpr sym BaseBoolType)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
forall (si :: StringInfo).
sym
-> SymString sym si
-> SymString sym si
-> IO (SymExpr sym BaseBoolType)
stringIsSuffixOf sym
sym SymExpr sym ('BaseStringType si)
x' SymExpr sym ('BaseStringType si)
y'
    StringIndexOf f (StringType si)
x f (StringType si)
y f ('BaseToType BaseIntegerType)
k -> do
      SymExpr sym ('BaseStringType si)
x' <- f (StringType si) -> IO (RegValue sym (StringType si))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType si)
x
      SymExpr sym ('BaseStringType si)
y' <- f (StringType si) -> IO (RegValue sym (StringType si))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (StringType si)
y
      SymInteger sym
k' <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
k
      sym
-> SymExpr sym ('BaseStringType si)
-> SymExpr sym ('BaseStringType si)
-> SymInteger sym
-> IO (SymInteger sym)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym
-> SymString sym si
-> SymString sym si
-> SymInteger sym
-> IO (SymInteger sym)
forall (si :: StringInfo).
sym
-> SymString sym si
-> SymString sym si
-> SymInteger sym
-> IO (SymInteger sym)
stringIndexOf sym
sym SymExpr sym ('BaseStringType si)
x' SymExpr sym ('BaseStringType si)
y' SymInteger sym
k'
    StringSubstring StringInfoRepr si
_si f ('BaseToType (BaseStringType si))
x f ('BaseToType BaseIntegerType)
off f ('BaseToType BaseIntegerType)
len -> do
      SymExpr sym (BaseStringType si)
x' <- f ('BaseToType (BaseStringType si))
-> IO (RegValue sym ('BaseToType (BaseStringType si)))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType (BaseStringType si))
x
      SymInteger sym
off' <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
off
      SymInteger sym
len' <- f ('BaseToType BaseIntegerType)
-> IO (RegValue sym ('BaseToType BaseIntegerType))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f ('BaseToType BaseIntegerType)
len
      sym
-> SymExpr sym (BaseStringType si)
-> SymInteger sym
-> SymInteger sym
-> IO (SymExpr sym (BaseStringType si))
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym
-> SymString sym si
-> SymInteger sym
-> SymInteger sym
-> IO (SymString sym si)
forall (si :: StringInfo).
sym
-> SymString sym si
-> SymInteger sym
-> SymInteger sym
-> IO (SymString sym si)
stringSubstring sym
sym SymExpr sym (BaseStringType si)
x' SymInteger sym
off' SymInteger sym
len'

    ---------------------------------------------------------------------
    -- Introspection

    IsConcrete BaseTypeRepr b
_ f (BaseToType b)
v -> do
      Bool
x <- SymExpr sym b -> Bool
forall (e :: BaseType -> Type) (bt :: BaseType).
IsExpr e =>
e bt -> Bool
baseIsConcrete (SymExpr sym b -> Bool) -> IO (SymExpr sym b) -> IO Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (BaseToType b) -> IO (RegValue sym (BaseToType b))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (BaseToType b)
v
      SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall a b. (a -> b) -> a -> b
$! if Bool
x then sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym else sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym

    ---------------------------------------------------------------------
    -- References

    ReferenceEq TypeRepr tp1
_ f (ReferenceType tp1)
ref1 f (ReferenceType tp1)
ref2 -> do
      MuxTree sym (RefCell tp1)
cell1 <- f (ReferenceType tp1) -> IO (RegValue sym (ReferenceType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (ReferenceType tp1)
ref1
      MuxTree sym (RefCell tp1)
cell2 <- f (ReferenceType tp1) -> IO (RegValue sym (ReferenceType tp1))
forall (tp :: CrucibleType). f tp -> IO (RegValue sym tp)
evalSub f (ReferenceType tp1)
ref2
      sym
-> RegValue sym (ReferenceType tp1)
-> RegValue sym (ReferenceType tp1)
-> IO (SymExpr sym BaseBoolType)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> RegValue sym (ReferenceType tp)
-> RegValue sym (ReferenceType tp)
-> IO (Pred sym)
eqReference sym
sym MuxTree sym (RefCell tp1)
RegValue sym (ReferenceType tp1)
cell1 MuxTree sym (RefCell tp1)
RegValue sym (ReferenceType tp1)
cell2