copilot-theorem-3.2.1: src/Copilot/Theorem/What4.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
-- |
-- Module : Copilot.Theorem.What4
-- Description : Prove spec properties using What4.
-- Copyright : (c) Ben Selfridge, 2020
-- Maintainer : benselfridge@galois.com
-- Stability : experimental
-- Portability : POSIX
--
-- Spec properties are translated into the language of SMT solvers using
-- @What4@. A backend solver is then used to prove the property is true. The
-- technique is sound, but incomplete. If a property is proved true by this
-- technique, then it can be guaranteed to be true. However, if a property is
-- not proved true, that does not mean it isn't true. Very simple specifications
-- are unprovable by this technique, including:
--
-- @
-- a = True : a
-- @
--
-- The above specification will not be proved true. The reason is that this
-- technique does not perform any sort of induction. When proving the inner @a@
-- expression, the technique merely allocates a fresh constant standing for
-- "@a@, one timestep in the past." Nothing is asserted about the fresh
-- constant.
--
-- An example of a property that is provable by this approach is:
--
-- @
-- a = True : b
-- b = not a
--
-- -- Property: a || b
-- @
--
-- By allocating a fresh constant, @b_-1@, standing for "the value of @b@ one
-- timestep in the past", the equation for @a || b@ at some arbitrary point in
-- the future reduces to @b_-1 || not b_-1@, which is always true.
--
-- In addition to proving that the stream expression is true at some arbitrary
-- point in the future, we also prove it for the first @k@ timesteps, where @k@
-- is the maximum buffer length of all streams in the given spec. This amounts
-- to simply interpreting the spec, although external variables are still
-- represented as constants with unknown values.
module Copilot.Theorem.What4
( prove, Solver(..), SatResult(..)
) where
import qualified Copilot.Core.Expr as CE
import qualified Copilot.Core.Operators as CE
import qualified Copilot.Core.Spec as CS
import qualified Copilot.Core.Type as CT
import qualified Copilot.Core.Type.Array as CT
import qualified What4.Config as WC
import qualified What4.Expr.Builder as WB
import qualified What4.Expr.GroundEval as WG
import qualified What4.Interface as WI
import qualified What4.BaseTypes as WT
import qualified What4.Solver as WS
import qualified What4.Solver.DReal as WS
import qualified Control.Monad.Fail as Fail
import Control.Monad.State
import qualified Data.BitVector.Sized as BV
import Data.Foldable (foldrM)
import Data.List (elemIndex)
import Data.Maybe (fromJust)
import qualified Data.Map as Map
import Data.Parameterized.Classes
import Data.Parameterized.Context hiding (zipWithM)
import Data.Parameterized.NatRepr
import Data.Parameterized.Nonce
import Data.Parameterized.Some
import Data.Parameterized.SymbolRepr
import qualified Data.Parameterized.Vector as V
import Data.Word
import GHC.Float (castWord32ToFloat, castWord64ToDouble)
import GHC.TypeNats (KnownNat)
import qualified Panic as Panic
--------------------------------------------------------------------------------
-- 'prove' function
--
-- To prove properties of a spec, we translate them into What4 using the TransM
-- monad (transformer on top of IO), then negate each property and ask a backend
-- solver to produce a model for the negation.
-- | We assume round-near-even throughout, but this variable can be changed if
-- needed.
fpRM :: WI.RoundingMode
fpRM = WI.RNE
-- | No builder state needed.
data BuilderState a = EmptyState
-- | The solvers supported by the what4 backend.
data Solver = CVC4 | DReal | Yices | Z3
-- | The 'prove' function returns results of this form for each property in a
-- spec.
data SatResult = Valid | Invalid | Unknown
deriving Show
type CounterExample = [(String, Some CopilotValue)]
-- | Attempt to prove all of the properties in a spec via an SMT solver (which
-- must be installed locally on the host). Return an association list mapping
-- the names of each property to the result returned by the solver.
prove :: Solver
-- ^ Solver to use
-> CS.Spec
-- ^ Spec
-> IO [(CE.Name, SatResult)]
prove solver spec = do
-- Setup symbolic backend
Some ng <- newIONonceGenerator
sym <- WB.newExprBuilder WB.FloatIEEERepr EmptyState ng
-- Solver-specific options
case solver of
CVC4 -> WC.extendConfig WS.cvc4Options (WI.getConfiguration sym)
DReal -> WC.extendConfig WS.drealOptions (WI.getConfiguration sym)
Yices -> WC.extendConfig WS.yicesOptions (WI.getConfiguration sym)
Z3 -> WC.extendConfig WS.z3Options (WI.getConfiguration sym)
-- Build up initial translation state
let streamMap = Map.fromList $
(\stream -> (CS.streamId stream, stream)) <$> CS.specStreams spec
pow <- WI.freshTotalUninterpFn sym (WI.safeSymbol "pow") knownRepr knownRepr
logb <- WI.freshTotalUninterpFn sym (WI.safeSymbol "logb") knownRepr knownRepr
let st = TransState Map.empty Map.empty Map.empty streamMap pow logb
-- Define TransM action for proving properties. Doing this in TransM rather
-- than IO allows us to reuse the state for each property.
let proveProperties = forM (CS.specProperties spec) $ \pr -> do
let bufLen (CS.Stream _ buf _ _) = length buf
maxBufLen = maximum (0 : (bufLen <$> CS.specStreams spec))
prefix <- forM [0 .. maxBufLen - 1] $ \k -> do
XBool p <- translateExprAt sym k (CS.propertyExpr pr)
return p
XBool p <- translateExpr sym 0 (CS.propertyExpr pr)
p_and_prefix <- liftIO $ foldrM (WI.andPred sym) p prefix
not_p_and_prefix <- liftIO $ WI.notPred sym p_and_prefix
let clauses = [not_p_and_prefix]
case solver of
CVC4 -> liftIO $ WS.runCVC4InOverride sym WS.defaultLogData clauses $ \case
WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid)
WS.Unsat _ -> return (CS.propertyName pr, Valid)
WS.Unknown -> return (CS.propertyName pr, Unknown)
DReal -> liftIO $ WS.runDRealInOverride sym WS.defaultLogData clauses $ \case
WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid)
WS.Unsat _ -> return (CS.propertyName pr, Valid)
WS.Unknown -> return (CS.propertyName pr, Unknown)
Yices -> liftIO $ WS.runYicesInOverride sym WS.defaultLogData clauses $ \case
WS.Sat _ge -> return (CS.propertyName pr, Invalid)
WS.Unsat _ -> return (CS.propertyName pr, Valid)
WS.Unknown -> return (CS.propertyName pr, Unknown)
Z3 -> liftIO $ WS.runZ3InOverride sym WS.defaultLogData clauses $ \case
WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid)
WS.Unsat _ -> return (CS.propertyName pr, Valid)
WS.Unknown -> return (CS.propertyName pr, Unknown)
-- Execute the action and return the results for each property
(res, _) <- runStateT (unTransM proveProperties) st
return res
--------------------------------------------------------------------------------
-- What4 translation
-- | the state for translating Copilot expressions into What4 expressions. As we
-- translate, we generate fresh symbolic constants for external variables and
-- for stream variables. We need to only generate one constant per variable, so
-- we allocate them in a map. When we need the constant for a particular
-- variable, we check if it is already in the map, and return it if it is; if it
-- isn't, we generate a fresh constant at that point, store it in the map, and
-- return it.
--
-- We also store three immutable fields in this state, rather than wrap them up
-- in another monad transformer layer. These are initialized prior to
-- translation and are never modified. They are the map from stream ids to the
-- core stream definitions, a symbolic uninterpreted function for "pow", and a
-- symbolic uninterpreted function for "logb".
data TransState t = TransState {
-- | Map of all external variables we encounter during translation. These are
-- just fresh constants. The offset indicates how many timesteps in the past
-- this constant represents for that stream.
externVars :: Map.Map (CE.Name, Int) (XExpr t),
-- | Map of external variables at specific indices (positive), rather than
-- offset into the past. This is for interpreting streams at specific offsets.
externVarsAt :: Map.Map (CE.Name, Int) (XExpr t),
-- | Map from (stream id, negative offset) to fresh constant. These are all
-- constants representing the values of a stream at some point in the past.
-- The offset (ALWAYS NEGATIVE) indicates how many timesteps in the past
-- this constant represents for that stream.
streamConstants :: Map.Map (CE.Id, Int) (XExpr t),
-- | Map from stream ids to the streams themselves. This value is never
-- modified, but I didn't want to make this an RWS, so it's represented as a
-- stateful value.
streams :: Map.Map CE.Id CS.Stream,
-- | Binary power operator, represented as an uninterpreted function.
pow :: WB.ExprSymFn t (WB.Expr t)
(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
WT.BaseRealType,
-- | Binary logarithm operator, represented as an uninterpreted function.
logb :: WB.ExprSymFn t (WB.Expr t)
(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
WT.BaseRealType
}
newtype TransM t a = TransM { unTransM :: StateT (TransState t) IO a }
deriving ( Functor
, Applicative
, Monad
, MonadIO
, MonadState (TransState t)
)
instance Fail.MonadFail (TransM t) where
fail = error
data CopilotWhat4 = CopilotWhat4
instance Panic.PanicComponent CopilotWhat4 where
panicComponentName _ = "Copilot/What4 translation"
panicComponentIssues _ = "https://github.com/Copilot-Language/copilot-theorem/issues"
{-# NOINLINE Panic.panicComponentRevision #-}
panicComponentRevision = $(Panic.useGitRevision)
-- | Use this function rather than an error monad since it indicates that
-- copilot-core's "reify" function did something incorrectly.
panic :: MonadIO m => m a
panic = Panic.panic CopilotWhat4 "Copilot.Theorem.What4"
[ "Ill-typed core expression" ]
-- | The What4 representation of a copilot expression. We do not attempt to
-- track the type of the inner expression at the type level, but instead lump
-- everything together into the 'XExpr t' type. The only reason this is a GADT
-- is for the array case; we need to know that the array length is strictly
-- positive.
data XExpr t where
XBool :: WB.Expr t WT.BaseBoolType -> XExpr t
XInt8 :: WB.Expr t (WT.BaseBVType 8) -> XExpr t
XInt16 :: WB.Expr t (WT.BaseBVType 16) -> XExpr t
XInt32 :: WB.Expr t (WT.BaseBVType 32) -> XExpr t
XInt64 :: WB.Expr t (WT.BaseBVType 64) -> XExpr t
XWord8 :: WB.Expr t (WT.BaseBVType 8) -> XExpr t
XWord16 :: WB.Expr t (WT.BaseBVType 16) -> XExpr t
XWord32 :: WB.Expr t (WT.BaseBVType 32) -> XExpr t
XWord64 :: WB.Expr t (WT.BaseBVType 64) -> XExpr t
XFloat :: WB.Expr t (WT.BaseFloatType WT.Prec32) -> XExpr t
XDouble :: WB.Expr t (WT.BaseFloatType WT.Prec64) -> XExpr t
XEmptyArray :: XExpr t
XArray :: 1 <= n => V.Vector n (XExpr t) -> XExpr t
XStruct :: [XExpr t] -> XExpr t
-- XArray :: NatRepr n
-- -> BaseTypeRepr tp
-- -> Some (WB.Expr t)
-- XStruct :: Assignment BaseTypeRepr tps
-- -> WB.Expr t (BaseStructType tps)
-- -> XExpr t
deriving instance Show (XExpr t)
data CopilotValue a = CopilotValue { cvType :: CT.Type a
, cvVal :: a
}
valFromExpr :: WG.GroundEvalFn t -> XExpr t -> IO (Some CopilotValue)
valFromExpr ge xe = case xe of
XBool e -> Some . CopilotValue CT.Bool <$> WG.groundEval ge e
XInt8 e -> Some . CopilotValue CT.Int8 . fromBV <$> WG.groundEval ge e
XInt16 e -> Some . CopilotValue CT.Int16 . fromBV <$> WG.groundEval ge e
XInt32 e -> Some . CopilotValue CT.Int32 . fromBV <$> WG.groundEval ge e
XInt64 e -> Some . CopilotValue CT.Int64 . fromBV <$> WG.groundEval ge e
XWord8 e -> Some . CopilotValue CT.Word8 . fromBV <$> WG.groundEval ge e
XWord16 e -> Some . CopilotValue CT.Word16 . fromBV <$> WG.groundEval ge e
XWord32 e -> Some . CopilotValue CT.Word32 . fromBV <$> WG.groundEval ge e
XWord64 e -> Some . CopilotValue CT.Word64 . fromBV <$> WG.groundEval ge e
XFloat e ->
Some . CopilotValue CT.Float . castWord32ToFloat . fromBV <$> WG.groundEval ge e
XDouble e ->
Some . CopilotValue CT.Double . castWord64ToDouble . fromBV <$> WG.groundEval ge e
_ -> error "valFromExpr unhandled case"
where fromBV :: forall a w . Num a => BV.BV w -> a
fromBV = fromInteger . BV.asUnsigned
-- | A view of an XExpr as a bitvector expression, a natrepr for its width, its
-- signed/unsigned status, and the constructor used to reconstruct an XExpr from
-- it. This is a useful view for translation, as many of the operations can be
-- grouped together for all words\/ints\/floats.
data SomeBVExpr t where
SomeBVExpr :: 1 <= w
=> WB.BVExpr t w
-> NatRepr w
-> BVSign
-> (WB.BVExpr t w -> XExpr t)
-> SomeBVExpr t
-- | The sign of a bitvector -- this indicates whether it is to be interpreted
-- as a signed 'Int' or an unsigned 'Word'.
data BVSign = Signed | Unsigned
-- | If the inner expression can be viewed as a bitvector, we project out a view
-- of it as such.
asBVExpr :: XExpr t -> Maybe (SomeBVExpr t)
asBVExpr xe = case xe of
XInt8 e -> Just (SomeBVExpr e knownNat Signed XInt8)
XInt16 e -> Just (SomeBVExpr e knownNat Signed XInt16)
XInt32 e -> Just (SomeBVExpr e knownNat Signed XInt32)
XInt64 e -> Just (SomeBVExpr e knownNat Signed XInt64)
XWord8 e -> Just (SomeBVExpr e knownNat Unsigned XWord8)
XWord16 e -> Just (SomeBVExpr e knownNat Unsigned XWord16)
XWord32 e -> Just (SomeBVExpr e knownNat Unsigned XWord32)
XWord64 e -> Just (SomeBVExpr e knownNat Unsigned XWord64)
_ -> Nothing
-- | Translate a constant expression by creating a what4 literal and packaging
-- it up into an 'XExpr'.
translateConstExpr :: forall a t st fs .
WB.ExprBuilder t st fs
-> CT.Type a
-> a
-> IO (XExpr t)
translateConstExpr sym tp a = case tp of
CT.Bool -> case a of
True -> return $ XBool (WI.truePred sym)
False -> return $ XBool (WI.falsePred sym)
CT.Int8 -> XInt8 <$> WI.bvLit sym knownNat (BV.int8 a)
CT.Int16 -> XInt16 <$> WI.bvLit sym knownNat (BV.int16 a)
CT.Int32 -> XInt32 <$> WI.bvLit sym knownNat (BV.int32 a)
CT.Int64 -> XInt64 <$> WI.bvLit sym knownNat (BV.int64 a)
CT.Word8 -> XWord8 <$> WI.bvLit sym knownNat (BV.word8 a)
CT.Word16 -> XWord16 <$> WI.bvLit sym knownNat (BV.word16 a)
CT.Word32 -> XWord32 <$> WI.bvLit sym knownNat (BV.word32 a)
CT.Word64 -> XWord64 <$> WI.bvLit sym knownNat (BV.word64 a)
CT.Float -> XFloat <$> WI.floatLit sym knownRepr (toRational a)
CT.Double -> XDouble <$> WI.floatLit sym knownRepr (toRational a)
CT.Array tp -> do
elts <- traverse (translateConstExpr sym tp) (CT.arrayelems a)
Just (Some n) <- return $ someNat (length elts)
case isZeroOrGT1 n of
Left Refl -> return XEmptyArray
Right LeqProof -> do
let Just v = V.fromList n elts
return $ XArray v
CT.Struct _ -> do
elts <- forM (CT.toValues a) $ \(CT.Value tp (CT.Field a)) ->
translateConstExpr sym tp a
return $ XStruct elts
arrayLen :: KnownNat n => CT.Type (CT.Array n t) -> NatRepr n
arrayLen _ = knownNat
-- | Generate a fresh constant for a given copilot type. This will be called
-- whenever we attempt to get the constant for a given external variable or
-- stream variable, but that variable has not been accessed yet and therefore
-- has no constant allocated.
freshCPConstant :: forall t st fs a .
WB.ExprBuilder t st fs
-> String
-> CT.Type a
-> IO (XExpr t)
freshCPConstant sym nm tp = case tp of
CT.Bool -> XBool <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
CT.Int8 -> XInt8 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
CT.Int16 -> XInt16 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
CT.Int32 -> XInt32 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
CT.Int64 -> XInt64 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
CT.Word8 -> XWord8 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
CT.Word16 -> XWord16 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
CT.Word32 -> XWord32 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
CT.Word64 -> XWord64 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
CT.Float -> XFloat <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
CT.Double -> XDouble <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr
atp@(CT.Array itp) -> do
n <- return $ arrayLen atp
case isZeroOrGT1 n of
Left Refl -> return XEmptyArray
Right LeqProof -> do
Refl <- return $ minusPlusCancel n (knownNat @1)
elts :: V.Vector n (XExpr t) <- V.generateM (decNat n) (const (freshCPConstant sym "" itp))
return $ XArray elts
CT.Struct stp -> do
elts <- forM (CT.toValues stp) $ \(CT.Value ftp _) -> freshCPConstant sym "" ftp
return $ XStruct elts
-- | Get the constant for a given stream id and some offset into the past. This
-- should only be called with a strictly negative offset. When this function
-- gets called for the first time for a given (streamId, offset) pair, it
-- generates a fresh constant and stores it in an internal map. Thereafter, this
-- function will just return that constant when called with the same pair.
getStreamConstant :: WB.ExprBuilder t st fs -> CE.Id -> Int -> TransM t (XExpr t)
getStreamConstant sym streamId offset = do
scs <- gets streamConstants
case Map.lookup (streamId, offset) scs of
Just xe -> return xe
Nothing -> do
CS.Stream _ _ _ tp <- getStreamDef streamId
let nm = show streamId ++ "_" ++ show offset
xe <- liftIO $ freshCPConstant sym nm tp
modify (\st -> st { streamConstants = Map.insert (streamId, offset) xe scs })
return xe
-- | Get the constant for a given external variable and some offset into the
-- past. This should only be called with a strictly negative offset. When this
-- function gets called for the first time for a given (var, offset) pair, it
-- generates a fresh constant and stores it in an internal map. Thereafter, this
-- function will just return that constant when called with the same pair.
getExternConstant :: WB.ExprBuilder t st fs
-> CT.Type a
-> CE.Name
-> Int
-> TransM t (XExpr t)
getExternConstant sym tp var offset = do
es <- gets externVars
case Map.lookup (var, offset) es of
Just xe -> return xe
Nothing -> do
xe <- liftIO $ freshCPConstant sym var tp
modify (\st -> st { externVars = Map.insert (var, offset) xe es} )
return xe
-- | Get the constant for a given external variable at some specific timestep.
getExternConstantAt :: WB.ExprBuilder t st fs
-> CT.Type a
-> CE.Name
-> Int
-> TransM t (XExpr t)
getExternConstantAt sym tp var ix = do
es <- gets externVarsAt
case Map.lookup (var, ix) es of
Just xe -> return xe
Nothing -> do
xe <- liftIO $ freshCPConstant sym var tp
modify (\st -> st { externVarsAt = Map.insert (var, ix) xe es} )
return xe
-- | Retrieve a stream definition given its id.
getStreamDef :: CE.Id -> TransM t CS.Stream
getStreamDef streamId = fromJust <$> gets (Map.lookup streamId . streams)
-- | Translate an expression into a what4 representation. The int offset keeps
-- track of how many timesteps into the past each variable is referring to.
-- Initially the value should be zero, but when we translate a stream, the
-- offset is recomputed based on the length of that stream's prefix (subtracted)
-- and the drop index (added).
translateExpr :: WB.ExprBuilder t st fs
-> Int
-- ^ number of timesteps in the past we are currently looking
-- (must always be <= 0)
-> CE.Expr a
-> TransM t (XExpr t)
translateExpr sym offset e = case e of
CE.Const tp a -> liftIO $ translateConstExpr sym tp a
CE.Drop _tp ix streamId
-- If we are referencing a past value of this stream, just return an
-- unconstrained constant.
| offset + fromIntegral ix < 0 ->
getStreamConstant sym streamId (offset + fromIntegral ix)
-- If we are referencing a current or future value of this stream, we need
-- to translate the stream's expression, using an offset computed based on
-- the current offset (negative or 0), the drop index (positive or 0), and
-- the length of the stream's buffer (subtracted).
| otherwise -> do
CS.Stream _ buf e _ <- getStreamDef streamId
translateExpr sym (offset + fromIntegral ix - length buf) e
CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented"
CE.Var _ _ -> error "translateExpr: Var unimplemented"
CE.ExternVar tp nm _prefix -> getExternConstant sym tp nm offset
CE.Op1 op e -> liftIO . translateOp1 sym op =<< translateExpr sym offset e
CE.Op2 op e1 e2 -> do
xe1 <- translateExpr sym offset e1
xe2 <- translateExpr sym offset e2
powFn <- gets pow
logbFn <- gets logb
liftIO $ translateOp2 sym powFn logbFn op xe1 xe2
CE.Op3 op e1 e2 e3 -> do
xe1 <- translateExpr sym offset e1
xe2 <- translateExpr sym offset e2
xe3 <- translateExpr sym offset e3
liftIO $ translateOp3 sym op xe1 xe2 xe3
CE.Label _ _ _ -> error "translateExpr: Label unimplemented"
-- | Translate an expression into a what4 representation at a /specific/
-- timestep, rather than "at some indeterminate point in the future."
translateExprAt :: WB.ExprBuilder t st fs
-> Int
-- ^ Index of timestep
-> CE.Expr a
-- ^ stream expression
-> TransM t (XExpr t)
translateExprAt sym k e = do
case e of
CE.Const tp a -> liftIO $ translateConstExpr sym tp a
CE.Drop _tp ix streamId -> do
CS.Stream _ buf e tp <- getStreamDef streamId
if k' < length buf
then liftIO $ translateConstExpr sym tp (buf !! k')
else translateExprAt sym (k' - length buf) e
where k' = k + fromIntegral ix
CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented"
CE.Var _ _ -> error "translateExpr: Var unimplemented"
CE.ExternVar tp nm _prefix -> getExternConstantAt sym tp nm k
CE.Op1 op e -> liftIO . translateOp1 sym op =<< translateExprAt sym k e
CE.Op2 op e1 e2 -> do
xe1 <- translateExprAt sym k e1
xe2 <- translateExprAt sym k e2
powFn <- gets pow
logbFn <- gets logb
liftIO $ translateOp2 sym powFn logbFn op xe1 xe2
CE.Op3 op e1 e2 e3 -> do
xe1 <- translateExprAt sym k e1
xe2 <- translateExprAt sym k e2
xe3 <- translateExprAt sym k e3
liftIO $ translateOp3 sym op xe1 xe2 xe3
CE.Label _ _ _ -> error "translateExpr: Label unimplemented"
type BVOp1 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> IO (WB.BVExpr t w)
type FPOp1 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp))
type RealOp1 t = WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType)
fieldName :: KnownSymbol s => CT.Field s a -> SymbolRepr s
fieldName _ = knownSymbol
valueName :: CT.Value a -> Some SymbolRepr
valueName (CT.Value _ f) = Some (fieldName f)
translateOp1 :: forall t st fs a b .
WB.ExprBuilder t st fs
-> CE.Op1 a b
-> XExpr t
-> IO (XExpr t)
translateOp1 sym op xe = case (op, xe) of
(CE.Not, XBool e) -> XBool <$> WI.notPred sym e
(CE.Not, _) -> panic
(CE.Abs _, xe) -> numOp bvAbs fpAbs xe
where bvAbs :: BVOp1 w t
bvAbs e = do zero <- WI.bvLit sym knownNat (BV.zero knownNat)
e_neg <- WI.bvSlt sym e zero
neg_e <- WI.bvSub sym zero e
WI.bvIte sym e_neg neg_e e
fpAbs :: FPOp1 fpp t
fpAbs e = do zero <- WI.floatLit sym knownRepr 0
e_neg <- WI.floatLt sym e zero
neg_e <- WI.floatSub sym fpRM zero e
WI.floatIte sym e_neg neg_e e
(CE.Sign _, xe) -> numOp bvSign fpSign xe
where bvSign :: BVOp1 w t
bvSign e = do zero <- WI.bvLit sym knownRepr (BV.zero knownNat)
neg_one <- WI.bvLit sym knownNat (BV.mkBV knownNat (-1))
pos_one <- WI.bvLit sym knownNat (BV.mkBV knownNat 1)
e_zero <- WI.bvEq sym e zero
e_neg <- WI.bvSlt sym e zero
t <- WI.bvIte sym e_neg neg_one pos_one
WI.bvIte sym e_zero zero t
fpSign :: FPOp1 fpp t
fpSign e = do zero <- WI.floatLit sym knownRepr 0
neg_one <- WI.floatLit sym knownRepr (-1)
pos_one <- WI.floatLit sym knownRepr 1
e_zero <- WI.floatEq sym e zero
e_neg <- WI.floatLt sym e zero
t <- WI.floatIte sym e_neg neg_one pos_one
WI.floatIte sym e_zero zero t
(CE.Recip _, xe) -> fpOp recip xe
where recip :: FPOp1 fpp t
recip e = do one <- WI.floatLit sym knownRepr 1
WI.floatDiv sym fpRM one e
(CE.Exp _, xe) -> realOp (WI.realExp sym) xe
(CE.Sqrt _, xe) -> fpOp (WI.floatSqrt sym fpRM) xe
(CE.Log _, xe) -> realOp (WI.realLog sym) xe
(CE.Sin _, xe) -> realOp (WI.realSin sym) xe
(CE.Cos _, xe) -> realOp (WI.realCos sym) xe
(CE.Tan _, xe) -> realOp (WI.realTan sym) xe
(CE.Asin _, xe) -> realOp (realRecip <=< WI.realSin sym) xe
(CE.Acos _, xe) -> realOp (realRecip <=< WI.realCos sym) xe
(CE.Atan _, xe) -> realOp (realRecip <=< WI.realTan sym) xe
(CE.Sinh _, xe) -> realOp (WI.realSinh sym) xe
(CE.Cosh _, xe) -> realOp (WI.realCosh sym) xe
(CE.Tanh _, xe) -> realOp (WI.realTanh sym) xe
(CE.Asinh _, xe) -> realOp (realRecip <=< WI.realSinh sym) xe
(CE.Acosh _, xe) -> realOp (realRecip <=< WI.realCosh sym) xe
(CE.Atanh _, xe) -> realOp (realRecip <=< WI.realTanh sym) xe
(CE.BwNot _, xe) -> case xe of
XBool e -> XBool <$> WI.notPred sym e
_ -> bvOp (WI.bvNotBits sym) xe
(CE.Cast _ tp, xe) -> case (xe, tp) of
(XBool e, CT.Bool) -> return $ XBool e
(XBool e, CT.Word8) -> XWord8 <$> WI.predToBV sym e knownNat
(XBool e, CT.Word16) -> XWord16 <$> WI.predToBV sym e knownNat
(XBool e, CT.Word32) -> XWord32 <$> WI.predToBV sym e knownNat
(XBool e, CT.Word64) -> XWord64 <$> WI.predToBV sym e knownNat
(XBool e, CT.Int8) -> XInt8 <$> WI.predToBV sym e knownNat
(XBool e, CT.Int16) -> XInt16 <$> WI.predToBV sym e knownNat
(XBool e, CT.Int32) -> XInt32 <$> WI.predToBV sym e knownNat
(XBool e, CT.Int64) -> XInt64 <$> WI.predToBV sym e knownNat
(XInt8 e, CT.Int8) -> return $ XInt8 e
(XInt8 e, CT.Int16) -> XInt16 <$> WI.bvSext sym knownNat e
(XInt8 e, CT.Int32) -> XInt32 <$> WI.bvSext sym knownNat e
(XInt8 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e
(XInt16 e, CT.Int16) -> return $ XInt16 e
(XInt16 e, CT.Int32) -> XInt32 <$> WI.bvSext sym knownNat e
(XInt16 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e
(XInt32 e, CT.Int32) -> return $ XInt32 e
(XInt32 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e
(XInt64 e, CT.Int64) -> return $ XInt64 e
(XWord8 e, CT.Int16) -> XInt16 <$> WI.bvZext sym knownNat e
(XWord8 e, CT.Int32) -> XInt32 <$> WI.bvZext sym knownNat e
(XWord8 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e
(XWord8 e, CT.Word8) -> return $ XWord8 e
(XWord8 e, CT.Word16) -> XWord16 <$> WI.bvZext sym knownNat e
(XWord8 e, CT.Word32) -> XWord32 <$> WI.bvZext sym knownNat e
(XWord8 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e
(XWord16 e, CT.Int32) -> XInt32 <$> WI.bvZext sym knownNat e
(XWord16 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e
(XWord16 e, CT.Word16) -> return $ XWord16 e
(XWord16 e, CT.Word32) -> XWord32 <$> WI.bvZext sym knownNat e
(XWord16 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e
(XWord32 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e
(XWord32 e, CT.Word32) -> return $ XWord32 e
(XWord32 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e
(XWord64 e, CT.Word64) -> return $ XWord64 e
_ -> panic
(CE.GetField (CT.Struct s) _ftp extractor, XStruct xes) -> do
let fieldNameRepr = fieldName (extractor undefined)
let structFieldNameReprs = valueName <$> CT.toValues s
let mIx = elemIndex (Some fieldNameRepr) structFieldNameReprs
case mIx of
Just ix -> return $ xes !! ix
Nothing -> panic
_ -> panic
where numOp :: (forall w . BVOp1 w t)
-> (forall fpp . FPOp1 fpp t)
-> XExpr t
-> IO (XExpr t)
numOp bvOp fpOp xe = case xe of
XInt8 e -> XInt8 <$> bvOp e
XInt16 e -> XInt16 <$> bvOp e
XInt32 e -> XInt32 <$> bvOp e
XInt64 e -> XInt64 <$> bvOp e
XWord8 e -> XWord8 <$> bvOp e
XWord16 e -> XWord16 <$> bvOp e
XWord32 e -> XWord32 <$> bvOp e
XWord64 e -> XWord64 <$> bvOp e
XFloat e -> XFloat <$> fpOp e
XDouble e -> XDouble <$> fpOp e
_ -> panic
bvOp :: (forall w . BVOp1 w t) -> XExpr t -> IO (XExpr t)
bvOp f xe = case xe of
XInt8 e -> XInt8 <$> f e
XInt16 e -> XInt16 <$> f e
XInt32 e -> XInt32 <$> f e
XInt64 e -> XInt64 <$> f e
XWord8 e -> XWord8 <$> f e
XWord16 e -> XWord16 <$> f e
XWord32 e -> XWord32 <$> f e
XWord64 e -> XWord64 <$> f e
_ -> panic
fpOp :: (forall fpp . FPOp1 fpp t) -> XExpr t -> IO (XExpr t)
fpOp g xe = case xe of
XFloat e -> XFloat <$> g e
XDouble e -> XDouble <$> g e
_ -> panic
realOp :: RealOp1 t -> XExpr t -> IO (XExpr t)
realOp h xe = fpOp hf xe
where hf :: (forall fpp . FPOp1 fpp t)
hf e = do re <- WI.floatToReal sym e
hre <- h re
WI.realToFloat sym knownRepr fpRM hre
realRecip :: RealOp1 t
realRecip e = do one <- WI.realLit sym 1
WI.realDiv sym one e
type BVOp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BVExpr t w)
type FPOp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp))
type RealOp2 t = WB.Expr t WT.BaseRealType -> WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType)
type BoolCmp2 t = WB.BoolExpr t -> WB.BoolExpr t -> IO (WB.BoolExpr t)
type BVCmp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BoolExpr t)
type FPCmp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.BoolExpr t)
translateOp2 :: forall t st fs a b c .
WB.ExprBuilder t st fs
-> (WB.ExprSymFn t (WB.Expr t)
(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
WT.BaseRealType)
-- ^ Pow function
-> (WB.ExprSymFn t (WB.Expr t)
(EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)
WT.BaseRealType)
-- ^ Logb function
-> CE.Op2 a b c
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp2 sym powFn logbFn op xe1 xe2 = case (op, xe1, xe2) of
(CE.And, XBool e1, XBool e2) -> XBool <$> WI.andPred sym e1 e2
(CE.Or, XBool e1, XBool e2) -> XBool <$> WI.orPred sym e1 e2
(CE.Add _, xe1, xe2) -> numOp (WI.bvAdd sym) (WI.floatAdd sym fpRM) xe1 xe2
(CE.Sub _, xe1, xe2) -> numOp (WI.bvSub sym) (WI.floatSub sym fpRM) xe1 xe2
(CE.Mul _, xe1, xe2) -> numOp (WI.bvMul sym) (WI.floatMul sym fpRM) xe1 xe2
(CE.Mod _, xe1, xe2) -> bvOp (WI.bvSrem sym) (WI.bvUrem sym) xe1 xe2
(CE.Div _, xe1, xe2) -> bvOp (WI.bvSdiv sym) (WI.bvUdiv sym) xe1 xe2
(CE.Fdiv _, xe1, xe2) -> fpOp (WI.floatDiv sym fpRM) xe1 xe2
(CE.Pow _, xe1, xe2) -> fpOp powFn' xe1 xe2
where powFn' :: FPOp2 fpp t
powFn' e1 e2 = do re1 <- WI.floatToReal sym e1
re2 <- WI.floatToReal sym e2
let args = (Empty :> re1 :> re2)
rpow <- WI.applySymFn sym powFn args
WI.realToFloat sym knownRepr fpRM rpow
(CE.Logb _, xe1, xe2) -> fpOp logbFn' xe1 xe2
where logbFn' :: FPOp2 fpp t
logbFn' e1 e2 = do re1 <- WI.floatToReal sym e1
re2 <- WI.floatToReal sym e2
let args = (Empty :> re1 :> re2)
rpow <- WI.applySymFn sym logbFn args
WI.realToFloat sym knownRepr fpRM rpow
(CE.Eq _, xe1, xe2) -> cmp (WI.eqPred sym) (WI.bvEq sym) (WI.floatEq sym) xe1 xe2
(CE.Ne _, xe1, xe2) -> cmp neqPred bvNeq fpNeq xe1 xe2
where neqPred :: BoolCmp2 t
neqPred e1 e2 = do e <- WI.eqPred sym e1 e2
WI.notPred sym e
bvNeq :: forall w . BVCmp2 w t
bvNeq e1 e2 = do e <- WI.bvEq sym e1 e2
WI.notPred sym e
fpNeq :: forall fpp . FPCmp2 fpp t
fpNeq e1 e2 = do e <- WI.floatEq sym e1 e2
WI.notPred sym e
(CE.Le _, xe1, xe2) -> numCmp (WI.bvSle sym) (WI.bvUle sym) (WI.floatLe sym) xe1 xe2
(CE.Ge _, xe1, xe2) -> numCmp (WI.bvSge sym) (WI.bvUge sym) (WI.floatGe sym) xe1 xe2
(CE.Lt _, xe1, xe2) -> numCmp (WI.bvSlt sym) (WI.bvUlt sym) (WI.floatLt sym) xe1 xe2
(CE.Gt _, xe1, xe2) -> numCmp (WI.bvSgt sym) (WI.bvUgt sym) (WI.floatGt sym) xe1 xe2
(CE.BwAnd _, xe1, xe2) -> bvOp (WI.bvAndBits sym) (WI.bvAndBits sym) xe1 xe2
(CE.BwOr _, xe1, xe2) -> bvOp (WI.bvOrBits sym) (WI.bvOrBits sym) xe1 xe2
(CE.BwXor _, xe1, xe2) -> bvOp (WI.bvXorBits sym) (WI.bvXorBits sym) xe1 xe2
-- Note: For both shift operators, we are interpreting the shifter as an
-- unsigned bitvector regardless of whether it is a word or an int.
(CE.BwShiftL _ _, xe1, xe2) -> do
Just (SomeBVExpr e1 w1 _ ctor1) <- return $ asBVExpr xe1
Just (SomeBVExpr e2 w2 _ _ ) <- return $ asBVExpr xe2
e2' <- case testNatCases w1 w2 of
NatCaseLT LeqProof -> WI.bvTrunc sym w1 e2
NatCaseEQ -> return e2
NatCaseGT LeqProof -> WI.bvZext sym w1 e2
ctor1 <$> WI.bvShl sym e1 e2'
(CE.BwShiftR _ _, xe1, xe2) -> do
Just (SomeBVExpr e1 w1 sgn1 ctor1) <- return $ asBVExpr xe1
Just (SomeBVExpr e2 w2 _ _ ) <- return $ asBVExpr xe2
e2' <- case testNatCases w1 w2 of
NatCaseLT LeqProof -> WI.bvTrunc sym w1 e2
NatCaseEQ -> return e2
NatCaseGT LeqProof -> WI.bvZext sym w1 e2
ctor1 <$> case sgn1 of
Signed -> WI.bvAshr sym e1 e2'
Unsigned -> WI.bvLshr sym e1 e2'
-- Note: Currently, copilot does not check if array indices are out of bounds,
-- even for constant expressions. The method of translation we are using
-- simply creates a nest of if-then-else expression to check the index
-- expression against all possible indices. If the index expression is known
-- by the solver to be out of bounds (for instance, if it is a constant 5 for
-- an array of 5 elements), then the if-then-else will trivially resolve to
-- true.
(CE.Index _, xe1, xe2) -> do
case (xe1, xe2) of
(XArray xes, XWord32 ix) -> buildIndexExpr sym 0 ix xes
_ -> panic
_ -> panic
where numOp :: (forall w . BVOp2 w t)
-> (forall fpp . FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of
(XInt8 e1, XInt8 e2) -> XInt8 <$> bvOp e1 e2
(XInt16 e1, XInt16 e2) -> XInt16 <$> bvOp e1 e2
(XInt32 e1, XInt32 e2)-> XInt32 <$> bvOp e1 e2
(XInt64 e1, XInt64 e2)-> XInt64 <$> bvOp e1 e2
(XWord8 e1, XWord8 e2)-> XWord8 <$> bvOp e1 e2
(XWord16 e1, XWord16 e2)-> XWord16 <$> bvOp e1 e2
(XWord32 e1, XWord32 e2)-> XWord32 <$> bvOp e1 e2
(XWord64 e1, XWord64 e2)-> XWord64 <$> bvOp e1 e2
(XFloat e1, XFloat e2)-> XFloat <$> fpOp e1 e2
(XDouble e1, XDouble e2)-> XDouble <$> fpOp e1 e2
_ -> panic
bvOp :: (forall w . BVOp2 w t)
-> (forall w . BVOp2 w t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
bvOp opS opU xe1 xe2 = case (xe1, xe2) of
(XInt8 e1, XInt8 e2) -> XInt8 <$> opS e1 e2
(XInt16 e1, XInt16 e2) -> XInt16 <$> opS e1 e2
(XInt32 e1, XInt32 e2) -> XInt32 <$> opS e1 e2
(XInt64 e1, XInt64 e2) -> XInt64 <$> opS e1 e2
(XWord8 e1, XWord8 e2) -> XWord8 <$> opU e1 e2
(XWord16 e1, XWord16 e2) -> XWord16 <$> opU e1 e2
(XWord32 e1, XWord32 e2) -> XWord32 <$> opU e1 e2
(XWord64 e1, XWord64 e2) -> XWord64 <$> opU e1 e2
_ -> panic
fpOp :: (forall fpp . FPOp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
fpOp op xe1 xe2 = case (xe1, xe2) of
(XFloat e1, XFloat e2) -> XFloat <$> op e1 e2
(XDouble e1, XDouble e2) -> XDouble <$> op e1 e2
_ -> panic
cmp :: BoolCmp2 t
-> (forall w . BVCmp2 w t)
-> (forall fpp . FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
cmp boolOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of
(XBool e1, XBool e2) -> XBool <$> boolOp e1 e2
(XInt8 e1, XInt8 e2) -> XBool <$> bvOp e1 e2
(XInt16 e1, XInt16 e2) -> XBool <$> bvOp e1 e2
(XInt32 e1, XInt32 e2)-> XBool <$> bvOp e1 e2
(XInt64 e1, XInt64 e2)-> XBool <$> bvOp e1 e2
(XWord8 e1, XWord8 e2)-> XBool <$> bvOp e1 e2
(XWord16 e1, XWord16 e2)-> XBool <$> bvOp e1 e2
(XWord32 e1, XWord32 e2)-> XBool <$> bvOp e1 e2
(XWord64 e1, XWord64 e2)-> XBool <$> bvOp e1 e2
(XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2
(XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2
_ -> panic
numCmp :: (forall w . BVCmp2 w t)
-> (forall w . BVCmp2 w t)
-> (forall fpp . FPCmp2 fpp t)
-> XExpr t
-> XExpr t
-> IO (XExpr t)
numCmp bvSOp bvUOp fpOp xe1 xe2 = case (xe1, xe2) of
(XInt8 e1, XInt8 e2) -> XBool <$> bvSOp e1 e2
(XInt16 e1, XInt16 e2) -> XBool <$> bvSOp e1 e2
(XInt32 e1, XInt32 e2)-> XBool <$> bvSOp e1 e2
(XInt64 e1, XInt64 e2)-> XBool <$> bvSOp e1 e2
(XWord8 e1, XWord8 e2)-> XBool <$> bvUOp e1 e2
(XWord16 e1, XWord16 e2)-> XBool <$> bvUOp e1 e2
(XWord32 e1, XWord32 e2)-> XBool <$> bvUOp e1 e2
(XWord64 e1, XWord64 e2)-> XBool <$> bvUOp e1 e2
(XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2
(XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2
_ -> panic
buildIndexExpr :: 1 <= n
=> WB.ExprBuilder t st fs
-> Word32
-- ^ Index
-> WB.Expr t (WT.BaseBVType 32)
-- ^ Index
-> V.Vector n (XExpr t)
-- ^ Elements
-> IO (XExpr t)
buildIndexExpr sym curIx ix xelts = case V.uncons xelts of
(xe, Left Refl) -> return xe
(xe, Right xelts') -> do
LeqProof <- return $ V.nonEmpty xelts'
rstExpr <- buildIndexExpr sym (curIx+1) ix xelts'
curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx)
ixEq <- WI.bvEq sym curIxExpr ix
mkIte sym ixEq xe rstExpr
mkIte :: WB.ExprBuilder t st fs
-> WB.Expr t WT.BaseBoolType
-> XExpr t
-> XExpr t
-> IO (XExpr t)
mkIte sym pred xe1 xe2 = case (xe1, xe2) of
(XBool e1, XBool e2) -> XBool <$> WI.itePred sym pred e1 e2
(XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym pred e1 e2
(XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym pred e1 e2
(XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym pred e1 e2
(XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym pred e1 e2
(XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym pred e1 e2
(XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym pred e1 e2
(XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym pred e1 e2
(XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym pred e1 e2
(XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym pred e1 e2
(XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym pred e1 e2
(XStruct xes1, XStruct xes2) ->
XStruct <$> zipWithM (mkIte sym pred) xes1 xes2
(XArray xes1, XArray xes2) ->
case V.length xes1 `testEquality` V.length xes2 of
Just Refl -> XArray <$> V.zipWithM (mkIte sym pred) xes1 xes2
Nothing -> panic
_ -> panic
translateOp3 :: forall t st fs a b c d .
WB.ExprBuilder t st fs
-> CE.Op3 a b c d
-> XExpr t
-> XExpr t
-> XExpr t
-> IO (XExpr t)
translateOp3 sym (CE.Mux _) (XBool te) xe1 xe2 = case (xe1, xe2) of
(XBool e1, XBool e2) -> XBool <$> WI.itePred sym te e1 e2
(XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym te e1 e2
(XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym te e1 e2
(XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym te e1 e2
(XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym te e1 e2
(XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym te e1 e2
(XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym te e1 e2
(XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym te e1 e2
(XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym te e1 e2
(XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym te e1 e2
(XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym te e1 e2
_ -> panic
translateOp3 _ _ _ _ _ = panic