{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeOperators              #-}

-- |
-- Module      : Copilot.Theorem.What4.Translate
-- Description : Translate Copilot specifications into What4
-- Copyright   : (c) Galois Inc., 2021-2022
-- Maintainer  : robdockins@galois.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Translate Copilot specifications to What4 formulas using the 'TransM' monad.
module Copilot.Theorem.What4.Translate
  ( -- * Translation into What4
    TransState(..)
  , TransM
  , runTransM
  , LocalEnv
  , translateExpr
  , translateConstExpr
  , getStreamValue
  , getExternConstant
    -- * What4 representations of Copilot expressions
  , XExpr(..)
    -- * Stream offsets
  , StreamOffset(..)
    -- * Auxiliary functions
  , panic
  ) where

import           Control.Monad                  (forM, zipWithM)
import qualified Control.Monad.Fail             as Fail
import           Control.Monad.IO.Class         (MonadIO (..))
import           Control.Monad.State            (MonadState (..), StateT (..),
                                                 gets, modify)
import qualified Data.BitVector.Sized           as BV
import           Data.IORef                     (newIORef, modifyIORef,
                                                 readIORef)
import           Data.List                      (elemIndex, genericIndex,
                                                 genericLength)
import qualified Data.Map                       as Map
import           Data.Maybe                     (fromJust)
import           Data.Parameterized.Classes     (KnownRepr (..))
import           Data.Parameterized.Context     (EmptyCtx, type (::>))
import           Data.Parameterized.NatRepr     (LeqProof (..), NatCases (..),
                                                 NatRepr, decNat, isZeroOrGT1,
                                                 knownNat, minusPlusCancel,
                                                 mkNatRepr, testNatCases)
import           Data.Parameterized.Some        (Some (..))
import           Data.Parameterized.SymbolRepr  (SymbolRepr, knownSymbol)
import qualified Data.Parameterized.Vector      as V
import           Data.Type.Equality             (TestEquality (..), (:~:) (..))
import           Data.Word                      (Word32)
import           GHC.TypeLits                   (KnownSymbol)
import           GHC.TypeNats                   (KnownNat, type (<=))
import qualified Panic                          as Panic

import qualified What4.BaseTypes                as WT
import qualified What4.Interface                as WI
import qualified What4.InterpretedFloatingPoint as WFP
import qualified What4.SpecialFunctions         as WSF

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 Copilot.PrettyPrint            as CP

-- Translation into What4

-- | 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 'streams', an immutable field, in this state, rather than wrap
-- it up in another monad transformer layer. This is initialized prior to
-- translation and is never modified. This maps from stream ids to the
-- core stream definitions.
data TransState sym = TransState {
  -- | Map keeping track of all external variables encountered during
  -- translation.
  forall sym. TransState sym -> Map Name (Some Type)
mentionedExternals :: Map.Map CE.Name (Some CT.Type),
  -- | Memo table for external variables, indexed by the external stream name
  -- and a stream offset.
  forall sym. TransState sym -> Map (Name, StreamOffset) (XExpr sym)
externVars :: Map.Map (CE.Name, StreamOffset) (XExpr sym),
  -- | Memo table for stream values, indexed by the stream 'CE.Id' and offset.
  forall sym. TransState sym -> Map (Id, StreamOffset) (XExpr sym)
streamValues :: Map.Map (CE.Id, StreamOffset) (XExpr sym),
  -- | 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.
  forall sym. TransState sym -> Map Id Stream
streams :: Map.Map CE.Id CS.Stream,
  -- | A list of side conditions that must be true in order for all applications
  -- of partial functions (e.g., 'CE.Div') to be well defined.
  forall sym. TransState sym -> [Pred sym]
sidePreds :: [WI.Pred sym]
  }

newtype TransM sym a = TransM { forall sym a. TransM sym a -> StateT (TransState sym) IO a
unTransM :: StateT (TransState sym) IO a }
  deriving ( forall a b. a -> TransM sym b -> TransM sym a
forall a b. (a -> b) -> TransM sym a -> TransM sym b
forall sym a b. a -> TransM sym b -> TransM sym a
forall sym a b. (a -> b) -> TransM sym a -> TransM sym b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TransM sym b -> TransM sym a
$c<$ :: forall sym a b. a -> TransM sym b -> TransM sym a
fmap :: forall a b. (a -> b) -> TransM sym a -> TransM sym b
$cfmap :: forall sym a b. (a -> b) -> TransM sym a -> TransM sym b
Functor
           , forall sym. Functor (TransM sym)
forall a. a -> TransM sym a
forall sym a. a -> TransM sym a
forall a b. TransM sym a -> TransM sym b -> TransM sym a
forall a b. TransM sym a -> TransM sym b -> TransM sym b
forall a b. TransM sym (a -> b) -> TransM sym a -> TransM sym b
forall sym a b. TransM sym a -> TransM sym b -> TransM sym a
forall sym a b. TransM sym a -> TransM sym b -> TransM sym b
forall sym a b. TransM sym (a -> b) -> TransM sym a -> TransM sym b
forall a b c.
(a -> b -> c) -> TransM sym a -> TransM sym b -> TransM sym c
forall sym a b c.
(a -> b -> c) -> TransM sym a -> TransM sym b -> TransM sym c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. TransM sym a -> TransM sym b -> TransM sym a
$c<* :: forall sym a b. TransM sym a -> TransM sym b -> TransM sym a
*> :: forall a b. TransM sym a -> TransM sym b -> TransM sym b
$c*> :: forall sym a b. TransM sym a -> TransM sym b -> TransM sym b
liftA2 :: forall a b c.
(a -> b -> c) -> TransM sym a -> TransM sym b -> TransM sym c
$cliftA2 :: forall sym a b c.
(a -> b -> c) -> TransM sym a -> TransM sym b -> TransM sym c
<*> :: forall a b. TransM sym (a -> b) -> TransM sym a -> TransM sym b
$c<*> :: forall sym a b. TransM sym (a -> b) -> TransM sym a -> TransM sym b
pure :: forall a. a -> TransM sym a
$cpure :: forall sym a. a -> TransM sym a
Applicative
           , forall sym. Applicative (TransM sym)
forall a. a -> TransM sym a
forall sym a. a -> TransM sym a
forall a b. TransM sym a -> TransM sym b -> TransM sym b
forall a b. TransM sym a -> (a -> TransM sym b) -> TransM sym b
forall sym a b. TransM sym a -> TransM sym b -> TransM sym b
forall sym a b. TransM sym a -> (a -> TransM sym b) -> TransM sym b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TransM sym a
$creturn :: forall sym a. a -> TransM sym a
>> :: forall a b. TransM sym a -> TransM sym b -> TransM sym b
$c>> :: forall sym a b. TransM sym a -> TransM sym b -> TransM sym b
>>= :: forall a b. TransM sym a -> (a -> TransM sym b) -> TransM sym b
$c>>= :: forall sym a b. TransM sym a -> (a -> TransM sym b) -> TransM sym b
Monad
           , forall sym. Monad (TransM sym)
forall a. Name -> TransM sym a
forall sym a. Name -> TransM sym a
forall (m :: * -> *).
Monad m -> (forall a. Name -> m a) -> MonadFail m
fail :: forall a. Name -> TransM sym a
$cfail :: forall sym a. Name -> TransM sym a
Fail.MonadFail
           , forall sym. Monad (TransM sym)
forall a. IO a -> TransM sym a
forall sym a. IO a -> TransM sym a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> TransM sym a
$cliftIO :: forall sym a. IO a -> TransM sym a
MonadIO
           , MonadState (TransState sym)
           )

-- | Translate a Copilot specification using the given 'TransM' computation.
runTransM :: CS.Spec -> TransM sym a -> IO a
runTransM :: forall sym a. Spec -> TransM sym a -> IO a
runTransM Spec
spec TransM sym a
m = do
  -- Build up initial translation state
  let streamMap :: Map Id Stream
streamMap = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$
        (\Stream
stream -> (Stream -> Id
CS.streamId Stream
stream, Stream
stream)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec -> [Stream]
CS.specStreams Spec
spec
      st :: TransState sym
st = TransState
           { mentionedExternals :: Map Name (Some Type)
mentionedExternals = forall a. Monoid a => a
mempty
           , externVars :: Map (Name, StreamOffset) (XExpr sym)
externVars = forall a. Monoid a => a
mempty
           , streamValues :: Map (Id, StreamOffset) (XExpr sym)
streamValues = forall a. Monoid a => a
mempty
           , streams :: Map Id Stream
streams = Map Id Stream
streamMap
           , sidePreds :: [Pred sym]
sidePreds = []
           }

  (a
res, TransState sym
_) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall sym a. TransM sym a -> StateT (TransState sym) IO a
unTransM TransM sym a
m) TransState sym
st
  forall (m :: * -> *) a. Monad m => a -> m a
return a
res

-- | An environment used to translate local Copilot variables to What4.
type LocalEnv sym = Map.Map CE.Name (StreamOffset -> TransM sym (XExpr sym))

-- | Compute the value of a stream expression at the given offset in the given
-- local environment.
translateExpr :: forall sym a.
                 WFP.IsInterpretedFloatSymExprBuilder sym
              => sym
              -> LocalEnv sym
              -- ^ Environment for local variables
              -> CE.Expr a
              -- ^ Expression to translate
              -> StreamOffset
              -- ^ Offset to compute
              -> TransM sym (XExpr sym)
translateExpr :: forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym LocalEnv sym
localEnv Expr a
e StreamOffset
offset = case Expr a
e of
  CE.Const Type a
tp a
a -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym a.
IsInterpretedFloatExprBuilder sym =>
sym -> Type a -> a -> IO (XExpr sym)
translateConstExpr sym
sym Type a
tp a
a
  CE.Drop Type a
_tp DropIdx
ix Id
streamId -> forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Id -> StreamOffset -> TransM sym (XExpr sym)
getStreamValue sym
sym Id
streamId (StreamOffset -> DropIdx -> StreamOffset
addOffset StreamOffset
offset DropIdx
ix)
  CE.Local Type a1
_tpa Type a
_tpb Name
nm Expr a1
e1 Expr a
body -> do
    IORef (Map StreamOffset (XExpr sym))
ref <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. a -> IO (IORef a)
newIORef forall a. Monoid a => a
mempty)

    -- Look up a stream value by offset, using an IORef to cache values that
    -- have already been looked up previously. Caching values in this way avoids
    -- exponential blowup.
    --
    -- Note that using a single IORef to store all local variables means that it
    -- is possible for local variables to escape their lexical scope. See issue
    -- #253 for more information. This is an issue that is shared in common with
    -- `copilot-c99` and the Copilot interpreter.
    let f :: StreamOffset -> TransM sym (XExpr sym)
        f :: StreamOffset -> TransM sym (XExpr sym)
f StreamOffset
offset' = do
          Map StreamOffset (XExpr sym)
m <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. IORef a -> IO a
readIORef IORef (Map StreamOffset (XExpr sym))
ref)
          case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup StreamOffset
offset' Map StreamOffset (XExpr sym)
m of
            -- If we have looked up this value before, return the cached value.
            Just XExpr sym
x -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
x
            -- Otherwise, translate the expression and cache it for subsequent
            -- lookups.
            Maybe (XExpr sym)
Nothing ->
              do XExpr sym
x <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym LocalEnv sym
localEnv Expr a1
e1 StreamOffset
offset'
                 forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (Map StreamOffset (XExpr sym))
ref (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert StreamOffset
offset' XExpr sym
x))
                 forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
x

    let localEnv' :: LocalEnv sym
localEnv' = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
nm StreamOffset -> TransM sym (XExpr sym)
f LocalEnv sym
localEnv
    forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym LocalEnv sym
localEnv' Expr a
body StreamOffset
offset
  CE.Var Type a
_tp Name
nm ->
    case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
nm LocalEnv sym
localEnv of
      Maybe (StreamOffset -> TransM sym (XExpr sym))
Nothing -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [Name
"translateExpr: unknown var " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Name
nm]
      Just StreamOffset -> TransM sym (XExpr sym)
f  -> StreamOffset -> TransM sym (XExpr sym)
f StreamOffset
offset
  CE.ExternVar Type a
tp Name
nm Maybe [a]
_prefix -> forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Type a -> Name -> StreamOffset -> TransM sym (XExpr sym)
getExternConstant sym
sym Type a
tp Name
nm StreamOffset
offset
  CE.Op1 Op1 a1 a
op Expr a1
e1 -> do
    XExpr sym
xe1 <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym LocalEnv sym
localEnv Expr a1
e1 StreamOffset
offset
    forall sym a b.
IsInterpretedFloatExprBuilder sym =>
sym -> Expr b -> Op1 a b -> XExpr sym -> TransM sym (XExpr sym)
translateOp1 sym
sym Expr a
e Op1 a1 a
op XExpr sym
xe1
  CE.Op2 Op2 a1 b a
op Expr a1
e1 Expr b
e2 -> do
    XExpr sym
xe1 <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym LocalEnv sym
localEnv Expr a1
e1 StreamOffset
offset
    XExpr sym
xe2 <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym LocalEnv sym
localEnv Expr b
e2 StreamOffset
offset
    forall sym a b c.
IsInterpretedFloatExprBuilder sym =>
sym
-> Expr c
-> Op2 a b c
-> XExpr sym
-> XExpr sym
-> TransM sym (XExpr sym)
translateOp2 sym
sym Expr a
e Op2 a1 b a
op XExpr sym
xe1 XExpr sym
xe2
  CE.Op3 Op3 a1 b c a
op Expr a1
e1 Expr b
e2 Expr c
e3 -> do
    XExpr sym
xe1 <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym LocalEnv sym
localEnv Expr a1
e1 StreamOffset
offset
    XExpr sym
xe2 <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym LocalEnv sym
localEnv Expr b
e2 StreamOffset
offset
    XExpr sym
xe3 <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym LocalEnv sym
localEnv Expr c
e3 StreamOffset
offset
    forall sym a b c d.
IsInterpretedFloatExprBuilder sym =>
sym
-> Expr d
-> Op3 a b c d
-> XExpr sym
-> XExpr sym
-> XExpr sym
-> TransM sym (XExpr sym)
translateOp3 sym
sym Expr a
e Op3 a1 b c a
op XExpr sym
xe1 XExpr sym
xe2 XExpr sym
xe3
  CE.Label Type a
_ Name
_ Expr a
e1 ->
    forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym LocalEnv sym
localEnv Expr a
e1 StreamOffset
offset

-- | Compute and cache the value of a stream with the given identifier at the
-- given offset.
getStreamValue :: WFP.IsInterpretedFloatSymExprBuilder sym
               => sym
               -> CE.Id
               -> StreamOffset
               -> TransM sym (XExpr sym)
getStreamValue :: forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Id -> StreamOffset -> TransM sym (XExpr sym)
getStreamValue sym
sym Id
streamId StreamOffset
offset = do
  Map (Id, StreamOffset) (XExpr sym)
svs <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall sym. TransState sym -> Map (Id, StreamOffset) (XExpr sym)
streamValues
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Id
streamId, StreamOffset
offset) Map (Id, StreamOffset) (XExpr sym)
svs of
    Just XExpr sym
xe -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
    Maybe (XExpr sym)
Nothing -> do
      Stream
streamDef <- forall sym. Id -> TransM sym Stream
getStreamDef Id
streamId
      XExpr sym
xe <- Stream -> TransM sym (XExpr sym)
computeStreamValue Stream
streamDef
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransState sym
st ->
        TransState sym
st { streamValues :: Map (Id, StreamOffset) (XExpr sym)
streamValues =
               forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id
streamId, StreamOffset
offset) XExpr sym
xe (forall sym. TransState sym -> Map (Id, StreamOffset) (XExpr sym)
streamValues TransState sym
st) }
      forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
  where
    computeStreamValue :: Stream -> TransM sym (XExpr sym)
computeStreamValue
      (CS.Stream
        { streamId :: Stream -> Id
CS.streamId = Id
id, streamBuffer :: ()
CS.streamBuffer = [a]
buf,
          streamExpr :: ()
CS.streamExpr = Expr a
ex, streamExprType :: ()
CS.streamExprType = Type a
tp }) =
      let len :: Integer
len = forall i a. Num i => [a] -> i
genericLength [a]
buf in
      case StreamOffset
offset of
        AbsoluteOffset Integer
i
          | Integer
i forall a. Ord a => a -> a -> Bool
< Integer
0     -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [Name
"Invalid absolute offset " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Integer
i forall a. [a] -> [a] -> [a]
++
                                Name
" for stream " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Id
id]
          | Integer
i forall a. Ord a => a -> a -> Bool
< Integer
len   -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym a.
IsInterpretedFloatExprBuilder sym =>
sym -> Type a -> a -> IO (XExpr sym)
translateConstExpr sym
sym Type a
tp (forall i a. Integral i => [a] -> i -> a
genericIndex [a]
buf Integer
i))
          | Bool
otherwise -> forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym forall a. Monoid a => a
mempty Expr a
ex (Integer -> StreamOffset
AbsoluteOffset (Integer
i forall a. Num a => a -> a -> a
- Integer
len))
        RelativeOffset Integer
i
          | Integer
i forall a. Ord a => a -> a -> Bool
< Integer
0     -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [Name
"Invalid relative offset " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Integer
i forall a. [a] -> [a] -> [a]
++
                                Name
" for stream " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Id
id]
          | Integer
i forall a. Ord a => a -> a -> Bool
< Integer
len   -> let nm :: Name
nm = Name
"s" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Id
id forall a. [a] -> [a] -> [a]
++ Name
"_r" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Integer
i
                         in forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Name -> Type a -> IO (XExpr sym)
freshCPConstant sym
sym Name
nm Type a
tp)
          | Bool
otherwise -> forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym forall a. Monoid a => a
mempty Expr a
ex (Integer -> StreamOffset
RelativeOffset (Integer
i forall a. Num a => a -> a -> a
- Integer
len))

-- | Compute and cache the value of an external stream with the given name at
-- the given offset.
getExternConstant :: WFP.IsInterpretedFloatSymExprBuilder sym
                  => sym
                  -> CT.Type a
                  -> CE.Name
                  -> StreamOffset
                  -> TransM sym (XExpr sym)
getExternConstant :: forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Type a -> Name -> StreamOffset -> TransM sym (XExpr sym)
getExternConstant sym
sym Type a
tp Name
nm StreamOffset
offset = do
  Map (Name, StreamOffset) (XExpr sym)
es <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall sym. TransState sym -> Map (Name, StreamOffset) (XExpr sym)
externVars
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Name
nm, StreamOffset
offset) Map (Name, StreamOffset) (XExpr sym)
es of
    Just XExpr sym
xe -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
    Maybe (XExpr sym)
Nothing -> do
      XExpr sym
xe <- TransM sym (XExpr sym)
computeExternConstant
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \TransState sym
st ->
        TransState sym
st { externVars :: Map (Name, StreamOffset) (XExpr sym)
externVars = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Name
nm, StreamOffset
offset) XExpr sym
xe (forall sym. TransState sym -> Map (Name, StreamOffset) (XExpr sym)
externVars TransState sym
st)
           , mentionedExternals :: Map Name (Some Type)
mentionedExternals =
               forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
nm (forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type a
tp) (forall sym. TransState sym -> Map Name (Some Type)
mentionedExternals TransState sym
st)
           }
      forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
 where
   computeExternConstant :: TransM sym (XExpr sym)
computeExternConstant =
     case StreamOffset
offset of
       AbsoluteOffset Integer
i
         | Integer
i forall a. Ord a => a -> a -> Bool
< Integer
0     -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [Name
"Invalid absolute offset " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Integer
i forall a. [a] -> [a] -> [a]
++
                               Name
" for external stream " forall a. [a] -> [a] -> [a]
++ Name
nm]
         | Bool
otherwise -> let nm' :: Name
nm' = Name
nm forall a. [a] -> [a] -> [a]
++ Name
"_a" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Integer
i
                        in forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Name -> Type a -> IO (XExpr sym)
freshCPConstant sym
sym Name
nm' Type a
tp)
       RelativeOffset Integer
i
         | Integer
i forall a. Ord a => a -> a -> Bool
< Integer
0     -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [Name
"Invalid relative offset " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Integer
i forall a. [a] -> [a] -> [a]
++
                               Name
" for external stream " forall a. [a] -> [a] -> [a]
++ Name
nm]
         | Bool
otherwise -> let nm' :: Name
nm' = Name
nm forall a. [a] -> [a] -> [a]
++ Name
"_r" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show Integer
i
                        in forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Name -> Type a -> IO (XExpr sym)
freshCPConstant sym
sym Name
nm' Type a
tp)

-- | 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 sym where
  SomeBVExpr :: 1 <= w
             => WI.SymBV sym w
             -> NatRepr w
             -> BVSign
             -> (WI.SymBV sym w -> XExpr sym)
             -> SomeBVExpr sym

-- | 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
  deriving BVSign -> BVSign -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BVSign -> BVSign -> Bool
$c/= :: BVSign -> BVSign -> Bool
== :: BVSign -> BVSign -> Bool
$c== :: BVSign -> BVSign -> Bool
Eq

-- | If the inner expression can be viewed as a bitvector, we project out a view
-- of it as such.
asBVExpr :: XExpr sym -> Maybe (SomeBVExpr sym)
asBVExpr :: forall sym. XExpr sym -> Maybe (SomeBVExpr sym)
asBVExpr XExpr sym
xe = case XExpr sym
xe of
  XInt8 SymExpr sym (BaseBVType 8)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) sym.
(1 <= n) =>
SymBV sym n
-> NatRepr n
-> BVSign
-> (SymBV sym n -> XExpr sym)
-> SomeBVExpr sym
SomeBVExpr SymExpr sym (BaseBVType 8)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Signed forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8)
  XInt16 SymExpr sym (BaseBVType 16)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) sym.
(1 <= n) =>
SymBV sym n
-> NatRepr n
-> BVSign
-> (SymBV sym n -> XExpr sym)
-> SomeBVExpr sym
SomeBVExpr SymExpr sym (BaseBVType 16)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Signed forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16)
  XInt32 SymExpr sym (BaseBVType 32)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) sym.
(1 <= n) =>
SymBV sym n
-> NatRepr n
-> BVSign
-> (SymBV sym n -> XExpr sym)
-> SomeBVExpr sym
SomeBVExpr SymExpr sym (BaseBVType 32)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Signed forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32)
  XInt64 SymExpr sym (BaseBVType 64)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) sym.
(1 <= n) =>
SymBV sym n
-> NatRepr n
-> BVSign
-> (SymBV sym n -> XExpr sym)
-> SomeBVExpr sym
SomeBVExpr SymExpr sym (BaseBVType 64)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Signed forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64)
  XWord8 SymExpr sym (BaseBVType 8)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) sym.
(1 <= n) =>
SymBV sym n
-> NatRepr n
-> BVSign
-> (SymBV sym n -> XExpr sym)
-> SomeBVExpr sym
SomeBVExpr SymExpr sym (BaseBVType 8)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Unsigned forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8)
  XWord16 SymExpr sym (BaseBVType 16)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) sym.
(1 <= n) =>
SymBV sym n
-> NatRepr n
-> BVSign
-> (SymBV sym n -> XExpr sym)
-> SomeBVExpr sym
SomeBVExpr SymExpr sym (BaseBVType 16)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Unsigned forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16)
  XWord32 SymExpr sym (BaseBVType 32)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) sym.
(1 <= n) =>
SymBV sym n
-> NatRepr n
-> BVSign
-> (SymBV sym n -> XExpr sym)
-> SomeBVExpr sym
SomeBVExpr SymExpr sym (BaseBVType 32)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Unsigned forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32)
  XWord64 SymExpr sym (BaseBVType 64)
e -> forall a. a -> Maybe a
Just (forall (n :: Natural) sym.
(1 <= n) =>
SymBV sym n
-> NatRepr n
-> BVSign
-> (SymBV sym n -> XExpr sym)
-> SomeBVExpr sym
SomeBVExpr SymExpr sym (BaseBVType 64)
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat BVSign
Unsigned forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64)
  XExpr sym
_ -> forall a. Maybe a
Nothing

-- | If an 'XExpr' is a bitvector expression, use it to generate a side
-- condition involving an application of a partial function. Otherwise, do
-- nothing.
addBVSidePred1 :: WI.IsExprBuilder sym
               => XExpr sym
               -> (forall w.
                      1 <= w
                   => WI.SymBV sym w
                   -> NatRepr w
                   -> BVSign
                   -> IO (WI.Pred sym))
               -> TransM sym ()
addBVSidePred1 :: forall sym.
IsExprBuilder sym =>
XExpr sym
-> (forall (w :: Natural).
    (1 <= w) =>
    SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym))
-> TransM sym ()
addBVSidePred1 XExpr sym
xe forall (w :: Natural).
(1 <= w) =>
SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym)
makeSidePred =
  case forall sym. XExpr sym -> Maybe (SomeBVExpr sym)
asBVExpr XExpr sym
xe of
    Just (SomeBVExpr SymBV sym w
e NatRepr w
w BVSign
sgn SymBV sym w -> XExpr sym
_) -> do
      Pred sym
sidePred <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (w :: Natural).
(1 <= w) =>
SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym)
makeSidePred SymBV sym w
e NatRepr w
w BVSign
sgn
      forall sym. Pred sym -> TransM sym ()
addSidePred Pred sym
sidePred
    Maybe (SomeBVExpr sym)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | If two 'XExpr's are both bitvector expressions of the same type and
-- signedness, use them to generate a side condition involving an application of
-- a partial function. Otherwise, do nothing.
addBVSidePred2 :: WI.IsExprBuilder sym
               => XExpr sym
               -> XExpr sym
               -> (forall w.
                      1 <= w
                   => WI.SymBV sym w
                   -> WI.SymBV sym w
                   -> NatRepr w
                   -> BVSign
                   -> IO (WI.Pred sym))
               -> TransM sym ()
addBVSidePred2 :: forall sym.
IsExprBuilder sym =>
XExpr sym
-> XExpr sym
-> (forall (w :: Natural).
    (1 <= w) =>
    SymBV sym w -> SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym))
-> TransM sym ()
addBVSidePred2 XExpr sym
xe1 XExpr sym
xe2 forall (w :: Natural).
(1 <= w) =>
SymBV sym w -> SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym)
makeSidePred =
  case (forall sym. XExpr sym -> Maybe (SomeBVExpr sym)
asBVExpr XExpr sym
xe1, forall sym. XExpr sym -> Maybe (SomeBVExpr sym)
asBVExpr XExpr sym
xe2) of
    (Just (SomeBVExpr SymBV sym w
e1 NatRepr w
w1 BVSign
sgn1 SymBV sym w -> XExpr sym
_), Just (SomeBVExpr SymBV sym w
e2 NatRepr w
w2 BVSign
sgn2 SymBV sym w -> XExpr sym
_))
      |  Just w :~: w
Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w1 NatRepr w
w2
      ,  BVSign
sgn1 forall a. Eq a => a -> a -> Bool
== BVSign
sgn2
      -> do Pred sym
sidePred <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (w :: Natural).
(1 <= w) =>
SymBV sym w -> SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym)
makeSidePred SymBV sym w
e1 SymBV sym w
e2 NatRepr w
w1 BVSign
sgn1
            forall sym. Pred sym -> TransM sym ()
addSidePred Pred sym
sidePred
    (Maybe (SomeBVExpr sym), Maybe (SomeBVExpr sym))
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Translate a constant expression by creating a what4 literal and packaging
-- it up into an 'XExpr'.
translateConstExpr :: forall sym a.
                      WFP.IsInterpretedFloatExprBuilder sym
                   => sym
                   -> CT.Type a
                   -> a
                   -> IO (XExpr sym)
translateConstExpr :: forall sym a.
IsInterpretedFloatExprBuilder sym =>
sym -> Type a -> a -> IO (XExpr sym)
translateConstExpr sym
sym Type a
tp a
a = case Type a
tp of
  Type a
CT.Bool -> case a
a of
    a
Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool (forall sym. IsExprBuilder sym => sym -> Pred sym
WI.truePred sym
sym)
    a
Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool (forall sym. IsExprBuilder sym => sym -> Pred sym
WI.falsePred sym
sym)
  Type a
CT.Int8 -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Int8 -> BV 8
BV.int8 a
a)
  Type a
CT.Int16 -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Int16 -> BV 16
BV.int16 a
a)
  Type a
CT.Int32 -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Int32 -> BV 32
BV.int32 a
a)
  Type a
CT.Int64 -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Int64 -> BV 64
BV.int64 a
a)
  Type a
CT.Word8 -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Word8 -> BV 8
BV.word8 a
a)
  Type a
CT.Word16 -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Word16 -> BV 16
BV.word16 a
a)
  Type a
CT.Word32 -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (DropIdx -> BV 32
BV.word32 a
a)
  Type a
CT.Word64 -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (Word64 -> BV 64
BV.word64 a
a)
  Type a
CT.Float -> forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Float -> IO (SymInterpretedFloat sym SingleFloat)
WFP.iFloatLitSingle sym
sym a
a
  Type a
CT.Double -> forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Double -> IO (SymInterpretedFloat sym DoubleFloat)
WFP.iFloatLitDouble sym
sym a
a
  CT.Array Type t
tp -> do
    [XExpr sym]
elts <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall sym a.
IsInterpretedFloatExprBuilder sym =>
sym -> Type a -> a -> IO (XExpr sym)
translateConstExpr sym
sym Type t
tp) (forall (n :: Natural) a. Array n a -> [a]
CT.arrayelems a
a)
    Some NatRepr x
n <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Natural -> Some NatRepr
mkNatRepr (forall i a. Num i => [a] -> i
genericLength [XExpr sym]
elts)
    case forall (n :: Natural). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr x
n of
      Left x :~: 0
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return forall sym. XExpr sym
XEmptyArray
      Right LeqProof 1 x
LeqProof -> do
        let Just Vector x (XExpr sym)
v = forall (n :: Natural) a.
(1 <= n) =>
NatRepr n -> [a] -> Maybe (Vector n a)
V.fromList NatRepr x
n [XExpr sym]
elts
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) sym.
(1 <= n) =>
Vector n (XExpr sym) -> XExpr sym
XArray Vector x (XExpr sym)
v
  CT.Struct a
_ -> do
    [XExpr sym]
elts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. Struct a => a -> [Value a]
CT.toValues a
a) forall a b. (a -> b) -> a -> b
$ \(CT.Value Type t
tp (CT.Field t
a)) ->
      forall sym a.
IsInterpretedFloatExprBuilder sym =>
sym -> Type a -> a -> IO (XExpr sym)
translateConstExpr sym
sym Type t
tp t
a
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. [XExpr sym] -> XExpr sym
XStruct [XExpr sym]
elts

arrayLen :: KnownNat n => CT.Type (CT.Array n t) -> NatRepr n
arrayLen :: forall (n :: Natural) t.
KnownNat n =>
Type (Array n t) -> NatRepr n
arrayLen Type (Array n t)
_ = forall (n :: Natural). KnownNat n => NatRepr n
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 sym a .
                   WFP.IsInterpretedFloatSymExprBuilder sym
                => sym
                -> String
                -> CT.Type a
                -> IO (XExpr sym)
freshCPConstant :: forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Name -> Type a -> IO (XExpr sym)
freshCPConstant sym
sym Name
nm Type a
tp = case Type a
tp of
  Type a
CT.Bool -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int8 -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int16 -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int32 -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Int64 -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word8 -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word16 -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word32 -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Word64 -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
  Type a
CT.Float -> forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    forall sym (fi :: FloatInfo).
IsInterpretedFloatSymExprBuilder sym =>
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
WFP.freshFloatConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) FloatInfoRepr SingleFloat
WFP.SingleFloatRepr
  Type a
CT.Double -> forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    forall sym (fi :: FloatInfo).
IsInterpretedFloatSymExprBuilder sym =>
sym
-> SolverSymbol
-> FloatInfoRepr fi
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
WFP.freshFloatConstant sym
sym (Name -> SolverSymbol
WI.safeSymbol Name
nm) FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr
  atp :: Type a
atp@(CT.Array Type t
itp) -> do
    let n :: NatRepr n
n = forall (n :: Natural) t.
KnownNat n =>
Type (Array n t) -> NatRepr n
arrayLen Type a
atp
    case forall (n :: Natural). NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
isZeroOrGT1 NatRepr n
n of
      Left n :~: 0
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return forall sym. XExpr sym
XEmptyArray
      Right LeqProof 1 n
LeqProof -> do
        ((n - 1) + 1) :~: n
Refl <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: Natural -> *) (m :: Natural) (g :: Natural -> *)
       (n :: Natural).
(n <= m) =>
f m -> g n -> ((m - n) + n) :~: m
minusPlusCancel NatRepr n
n (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1)
        Vector ((n - 1) + 1) (XExpr sym)
elts :: V.Vector n (XExpr t) <-
          forall (m :: * -> *) (h :: Natural) a.
Monad m =>
NatRepr h
-> (forall (n :: Natural). (n <= h) => NatRepr n -> m a)
-> m (Vector (h + 1) a)
V.generateM (forall (n :: Natural). (1 <= n) => NatRepr n -> NatRepr (n - 1)
decNat NatRepr n
n) (forall a b. a -> b -> a
const (forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Name -> Type a -> IO (XExpr sym)
freshCPConstant sym
sym Name
"" Type t
itp))
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) sym.
(1 <= n) =>
Vector n (XExpr sym) -> XExpr sym
XArray Vector ((n - 1) + 1) (XExpr sym)
elts
  CT.Struct a
stp -> do
    [XExpr sym]
elts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. Struct a => a -> [Value a]
CT.toValues a
stp) forall a b. (a -> b) -> a -> b
$ \(CT.Value Type t
ftp Field s t
_) ->
      forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Name -> Type a -> IO (XExpr sym)
freshCPConstant sym
sym Name
"" Type t
ftp
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. [XExpr sym] -> XExpr sym
XStruct [XExpr sym]
elts

-- | Retrieve a stream definition given its id.
getStreamDef :: CE.Id -> TransM sym CS.Stream
getStreamDef :: forall sym. Id -> TransM sym Stream
getStreamDef Id
streamId = forall a. HasCallStack => Maybe a -> a
fromJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
streamId forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. TransState sym -> Map Id Stream
streams)

-- | Add a side condition originating from an application of a partial function.
addSidePred :: WI.Pred sym -> TransM sym ()
addSidePred :: forall sym. Pred sym -> TransM sym ()
addSidePred Pred sym
newPred = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\TransState sym
st -> TransState sym
st { sidePreds :: [Pred sym]
sidePreds = Pred sym
newPred forall a. a -> [a] -> [a]
: forall sym. TransState sym -> [Pred sym]
sidePreds TransState sym
st })

-- * Translate Ops

-- Note [Side conditions for floating-point operations]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- We do not currently track side conditions for floating-point operations, as
-- they are unlikely to matter. A typical client of copilot-theorem will likely
-- treat floating-point operations as uninterpreted functions, and side
-- conditions involving uninterpreted functions are very unlikely to be helpful
-- except in very specific circumstances. In case we revisit this decision
-- later, we make a note of which floating-point operations could potentially
-- track side conditions as comments (but without implementing them).

type BVOp1 sym w = (KnownNat w, 1 <= w) => WI.SymBV sym w -> IO (WI.SymBV sym w)

type FPOp1 sym fi =
     WFP.FloatInfoRepr fi
  -> WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi)
  -> IO (WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi))

fieldName :: KnownSymbol s => CT.Field s a -> SymbolRepr s
fieldName :: forall (s :: Symbol) a. KnownSymbol s => Field s a -> SymbolRepr s
fieldName Field s a
_ = forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol

valueName :: CT.Value a -> Some SymbolRepr
valueName :: forall a. Value a -> Some SymbolRepr
valueName (CT.Value Type t
_ Field s t
f) = forall k (f :: k -> *) (x :: k). f x -> Some f
Some (forall (s :: Symbol) a. KnownSymbol s => Field s a -> SymbolRepr s
fieldName Field s t
f)

translateOp1 :: forall sym a b .
                WFP.IsInterpretedFloatExprBuilder sym
             => sym
             -> CE.Expr b
             -- ^ Original value we are translating (only used for error
             -- messages)
             -> CE.Op1 a b
             -> XExpr sym
             -> TransM sym (XExpr sym)
translateOp1 :: forall sym a b.
IsInterpretedFloatExprBuilder sym =>
sym -> Expr b -> Op1 a b -> XExpr sym -> TransM sym (XExpr sym)
translateOp1 sym
sym Expr b
origExpr Op1 a b
op XExpr sym
xe = case (Op1 a b
op, XExpr sym
xe) of
  (Op1 a b
CE.Not, XBool SymExpr sym BaseBoolType
e) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym SymExpr sym BaseBoolType
e
  (Op1 a b
CE.Not, XExpr sym
_) -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [Name
"Expected bool", forall a. Show a => a -> Name
show XExpr sym
xe]
  (CE.Abs Type a
_, XExpr sym
xe) -> XExpr sym -> TransM sym (XExpr sym)
translateAbs XExpr sym
xe
  (CE.Sign Type a
_, XExpr sym
xe) -> XExpr sym -> TransM sym (XExpr sym)
translateSign XExpr sym
xe

  -- We do not track any side conditions for floating-point operations
  -- (see Note [Side conditions for floating-point operations]), but we will
  -- make a note of which operations have partial inputs.

  -- The argument should not be zero
  (CE.Recip Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall (fi :: FloatInfo). FPOp1 sym fi)
-> XExpr sym -> IO (XExpr sym)
fpOp forall (fi :: FloatInfo). FPOp1 sym fi
recip XExpr sym
xe
    where
      recip :: forall fi . FPOp1 sym fi
      recip :: forall (fi :: FloatInfo). FPOp1 sym fi
recip FloatInfoRepr fi
fiRepr SymExpr sym (SymInterpretedFloatType sym fi)
e = do
        SymExpr sym (SymInterpretedFloatType sym fi)
one <- forall (fi :: FloatInfo).
FloatInfoRepr fi
-> (forall frac. Fractional frac => frac)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
fpLit FloatInfoRepr fi
fiRepr frac
1.0
        forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatDiv @_ @fi sym
sym RoundingMode
fpRM SymExpr sym (SymInterpretedFloatType sym fi)
one SymExpr sym (SymInterpretedFloatType sym fi)
e
  -- The argument should not cause the result to overflow or underlow
  (CE.Exp Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Exp XExpr sym
xe
  -- The argument should not be less than -0
  (CE.Sqrt Type a
_, XExpr sym
xe) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    (forall (fi :: FloatInfo). FPOp1 sym fi)
-> XExpr sym -> IO (XExpr sym)
fpOp (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatSqrt @_ @fi sym
sym RoundingMode
fpRM) XExpr sym
xe
  -- The argument should not be negative or zero
  (CE.Log Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Log XExpr sym
xe
  -- The argument should not be infinite
  (CE.Sin Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Sin XExpr sym
xe
  -- The argument should not be infinite
  (CE.Cos Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Cos XExpr sym
xe
  -- The argument should not be infinite, nor should it cause the result to
  -- overflow
  (CE.Tan Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Tan XExpr sym
xe
  -- The argument should not cause the result to overflow
  (CE.Sinh Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Sinh XExpr sym
xe
  -- The argument should not cause the result to overflow
  (CE.Cosh Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Cosh XExpr sym
xe
  (CE.Tanh Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Tanh XExpr sym
xe
  -- The argument should not be outside the range [-1, 1]
  (CE.Asin Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Arcsin XExpr sym
xe
  -- The argument should not be outside the range [-1, 1]
  (CE.Acos Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Arccos XExpr sym
xe
  (CE.Atan Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Arctan XExpr sym
xe
  (CE.Asinh Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Arcsinh XExpr sym
xe
  -- The argument should not be less than 1
  (CE.Acosh Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Arccosh XExpr sym
xe
  -- The argument should not be less than or equal to -1,
  -- nor should it be greater than or equal to +1
  (CE.Atanh Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
WSF.Arctanh XExpr sym
xe
  -- The argument should not cause the result to overflow
  (CE.Ceiling Type a
_, XExpr sym
xe) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    (forall (fi :: FloatInfo). FPOp1 sym fi)
-> XExpr sym -> IO (XExpr sym)
fpOp (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatRound @_ @fi sym
sym RoundingMode
WI.RTP) XExpr sym
xe
  -- The argument should not cause the result to overflow
  (CE.Floor Type a
_, XExpr sym
xe) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    (forall (fi :: FloatInfo). FPOp1 sym fi)
-> XExpr sym -> IO (XExpr sym)
fpOp (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatRound @_ @fi sym
sym RoundingMode
WI.RTN) XExpr sym
xe
  (CE.BwNot Type a
_, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ case XExpr sym
xe of
    XBool SymExpr sym BaseBoolType
e -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym SymExpr sym BaseBoolType
e
    XExpr sym
_ -> (forall (w :: Natural). BVOp1 sym w) -> XExpr sym -> IO (XExpr sym)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
WI.bvNotBits sym
sym) XExpr sym
xe
  (CE.Cast Type a
_ Type b
tp, XExpr sym
xe) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym b a.
IsInterpretedFloatExprBuilder sym =>
sym -> Expr b -> Type a -> XExpr sym -> IO (XExpr sym)
castOp sym
sym Expr b
origExpr Type b
tp XExpr sym
xe
  (CE.GetField Type a
atp Type b
_ftp a -> Field s b
extractor, XExpr sym
xe) -> forall struct (s :: Symbol).
KnownSymbol s =>
Type struct
-> (struct -> Field s b) -> XExpr sym -> TransM sym (XExpr sym)
translateGetField Type a
atp a -> Field s b
extractor XExpr sym
xe
  where
    -- Translate an 'CE.Abs' operation and its argument into a what4
    -- representation of the appropriate type.
    translateAbs :: XExpr sym -> TransM sym (XExpr sym)
    translateAbs :: XExpr sym -> TransM sym (XExpr sym)
translateAbs XExpr sym
xe = do
      forall sym.
IsExprBuilder sym =>
XExpr sym
-> (forall (w :: Natural).
    (1 <= w) =>
    SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym))
-> TransM sym ()
addBVSidePred1 XExpr sym
xe forall a b. (a -> b) -> a -> b
$ \SymBV sym w
e NatRepr w
w BVSign
_ -> do
        -- The argument should not be INT_MIN
        SymBV sym w
bvIntMin <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr w
w (forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
w)
        SymExpr sym BaseBoolType
eqIntMin <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq sym
sym SymBV sym w
e SymBV sym w
bvIntMin
        forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym SymExpr sym BaseBoolType
eqIntMin
      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall (w :: Natural). BVOp1 sym w)
-> (forall (fi :: FloatInfo). FPOp1 sym fi)
-> XExpr sym
-> IO (XExpr sym)
numOp forall (w :: Natural). BVOp1 sym w
bvAbs forall (fi :: FloatInfo). FPOp1 sym fi
fpAbs XExpr sym
xe
      where
        bvAbs :: BVOp1 sym w
        bvAbs :: forall (w :: Natural). BVOp1 sym w
bvAbs SymBV sym w
e = do
          SymBV sym w
zero <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (forall (w :: Natural). NatRepr w -> BV w
BV.zero forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
          SymExpr sym BaseBoolType
e_neg <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSlt sym
sym SymBV sym w
e SymBV sym w
zero
          SymBV sym w
neg_e <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSub sym
sym SymBV sym w
zero SymBV sym w
e
          forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym SymExpr sym BaseBoolType
e_neg SymBV sym w
neg_e SymBV sym w
e

        fpAbs :: forall fi . FPOp1 sym fi
        fpAbs :: forall (fi :: FloatInfo). FPOp1 sym fi
fpAbs FloatInfoRepr fi
_ SymExpr sym (SymInterpretedFloatType sym fi)
e = forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi -> IO (SymInterpretedFloat sym fi)
WFP.iFloatAbs @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
e

    -- Translate a 'CE.GetField' operation and its argument into a what4
    -- representation. If the argument is not a struct, panic.
    translateGetField :: forall struct s.
                         KnownSymbol s
                      => CT.Type struct
                      -- ^ The type of the argument
                      -> (struct -> CT.Field s b)
                      -- ^ Extract a struct field
                      -> XExpr sym
                      -- ^ The argument value (should be a struct)
                      -> TransM sym (XExpr sym)
    translateGetField :: forall struct (s :: Symbol).
KnownSymbol s =>
Type struct
-> (struct -> Field s b) -> XExpr sym -> TransM sym (XExpr sym)
translateGetField Type struct
tp struct -> Field s b
extractor XExpr sym
xe = case (Type struct
tp, XExpr sym
xe) of
      (CT.Struct struct
s, XStruct [XExpr sym]
xes) ->
        case Struct struct => struct -> Maybe Id
mIx struct
s of
          Just Id
ix -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [XExpr sym]
xes forall a. [a] -> Id -> a
!! Id
ix
          Maybe Id
Nothing -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [ Name
"Could not find field " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show SymbolRepr s
fieldNameRepr
                           , forall a. Show a => a -> Name
show struct
s
                           ]
      (Type struct, XExpr sym)
_ -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValue Name
"get-field operation"
      where
        fieldNameRepr :: SymbolRepr s
        fieldNameRepr :: SymbolRepr s
fieldNameRepr = forall (s :: Symbol) a. KnownSymbol s => Field s a -> SymbolRepr s
fieldName (struct -> Field s b
extractor forall a. HasCallStack => a
undefined)

        structFieldNameReprs :: CT.Struct struct => struct -> [Some SymbolRepr]
        structFieldNameReprs :: Struct struct => struct -> [Some SymbolRepr]
structFieldNameReprs struct
s = forall a. Value a -> Some SymbolRepr
valueName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Struct a => a -> [Value a]
CT.toValues struct
s

        mIx :: CT.Struct struct => struct -> Maybe Int
        mIx :: Struct struct => struct -> Maybe Id
mIx struct
s = forall a. Eq a => a -> [a] -> Maybe Id
elemIndex (forall k (f :: k -> *) (x :: k). f x -> Some f
Some SymbolRepr s
fieldNameRepr) (Struct struct => struct -> [Some SymbolRepr]
structFieldNameReprs struct
s)

    -- Translate a 'CE.Sign' operation (i.e, 'signum') and its argument into a
    -- what4 representation of the appropriate type. We translate @signum x@ as
    -- @x > 0 ? 1 : (x < 0 ? -1 : x)@. This matches how copilot-c99 translates
    -- 'CE.Sign' to C code.
    translateSign :: XExpr sym -> TransM sym (XExpr sym)
    translateSign :: XExpr sym -> TransM sym (XExpr sym)
translateSign XExpr sym
xe = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall (w :: Natural). BVOp1 sym w)
-> (forall (fi :: FloatInfo). FPOp1 sym fi)
-> XExpr sym
-> IO (XExpr sym)
numOp forall (w :: Natural). BVOp1 sym w
bvSign forall (fi :: FloatInfo). FPOp1 sym fi
fpSign XExpr sym
xe
      where
        bvSign :: BVOp1 sym w
        bvSign :: forall (w :: Natural). BVOp1 sym w
bvSign SymBV sym w
e = do
          SymBV sym w
zero <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr (forall (w :: Natural). NatRepr w -> BV w
BV.zero forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
          SymBV sym w
neg_one <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV forall (n :: Natural). KnownNat n => NatRepr n
knownNat (-Integer
1))
          SymBV sym w
pos_one <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV forall (n :: Natural). KnownNat n => NatRepr n
knownNat Integer
1)
          SymExpr sym BaseBoolType
e_neg <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSlt sym
sym SymBV sym w
e SymBV sym w
zero
          SymExpr sym BaseBoolType
e_pos <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSgt sym
sym SymBV sym w
e SymBV sym w
zero
          SymBV sym w
t <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym SymExpr sym BaseBoolType
e_neg SymBV sym w
neg_one SymBV sym w
e
          forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym SymExpr sym BaseBoolType
e_pos SymBV sym w
pos_one SymBV sym w
t

        fpSign :: forall fi . FPOp1 sym fi
        fpSign :: forall (fi :: FloatInfo). FPOp1 sym fi
fpSign FloatInfoRepr fi
fiRepr SymExpr sym (SymInterpretedFloatType sym fi)
e = do
          SymExpr sym (SymInterpretedFloatType sym fi)
zero    <- forall (fi :: FloatInfo).
FloatInfoRepr fi
-> (forall frac. Fractional frac => frac)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
fpLit FloatInfoRepr fi
fiRepr   frac
0.0
          SymExpr sym (SymInterpretedFloatType sym fi)
neg_one <- forall (fi :: FloatInfo).
FloatInfoRepr fi
-> (forall frac. Fractional frac => frac)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
fpLit FloatInfoRepr fi
fiRepr (-frac
1.0)
          SymExpr sym (SymInterpretedFloatType sym fi)
pos_one <- forall (fi :: FloatInfo).
FloatInfoRepr fi
-> (forall frac. Fractional frac => frac)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
fpLit FloatInfoRepr fi
fiRepr   frac
1.0
          SymExpr sym BaseBoolType
e_neg <- forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
WFP.iFloatLt @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
e SymExpr sym (SymInterpretedFloatType sym fi)
zero
          SymExpr sym BaseBoolType
e_pos <- forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
WFP.iFloatGt @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
e SymExpr sym (SymInterpretedFloatType sym fi)
zero
          SymExpr sym (SymInterpretedFloatType sym fi)
t <- forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatIte @_ @fi sym
sym SymExpr sym BaseBoolType
e_neg SymExpr sym (SymInterpretedFloatType sym fi)
neg_one SymExpr sym (SymInterpretedFloatType sym fi)
e
          forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatIte @_ @fi sym
sym SymExpr sym BaseBoolType
e_pos SymExpr sym (SymInterpretedFloatType sym fi)
pos_one SymExpr sym (SymInterpretedFloatType sym fi)
t

    -- Check the type of the argument. If the argument is a bitvector value,
    -- apply the 'BVOp1'. If the argument is a floating-point value, apply the
    -- 'FPOp1'. Otherwise, 'panic'.
    numOp :: (forall w . BVOp1 sym w)
          -> (forall fpp . FPOp1 sym fpp)
          -> XExpr sym
          -> IO (XExpr sym)
    numOp :: (forall (w :: Natural). BVOp1 sym w)
-> (forall (fi :: FloatInfo). FPOp1 sym fi)
-> XExpr sym
-> IO (XExpr sym)
numOp forall (w :: Natural). BVOp1 sym w
bvOp forall (fi :: FloatInfo). FPOp1 sym fi
fpOp XExpr sym
xe = case XExpr sym
xe of
      XInt8 SymExpr sym (BaseBVType 8)
e -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
bvOp SymExpr sym (BaseBVType 8)
e
      XInt16 SymExpr sym (BaseBVType 16)
e -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
bvOp SymExpr sym (BaseBVType 16)
e
      XInt32 SymExpr sym (BaseBVType 32)
e -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
bvOp SymExpr sym (BaseBVType 32)
e
      XInt64 SymExpr sym (BaseBVType 64)
e -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
bvOp SymExpr sym (BaseBVType 64)
e
      XWord8 SymExpr sym (BaseBVType 8)
e -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
bvOp SymExpr sym (BaseBVType 8)
e
      XWord16 SymExpr sym (BaseBVType 16)
e -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
bvOp SymExpr sym (BaseBVType 16)
e
      XWord32 SymExpr sym (BaseBVType 32)
e -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
bvOp SymExpr sym (BaseBVType 32)
e
      XWord64 SymExpr sym (BaseBVType 64)
e -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
bvOp SymExpr sym (BaseBVType 64)
e
      XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e -> forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPOp1 sym fi
fpOp FloatInfoRepr SingleFloat
WFP.SingleFloatRepr SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e
      XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e -> forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPOp1 sym fi
fpOp FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e
      XExpr sym
_ -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValue Name
"numOp"

    bvOp :: (forall w . BVOp1 sym w) -> XExpr sym -> IO (XExpr sym)
    bvOp :: (forall (w :: Natural). BVOp1 sym w) -> XExpr sym -> IO (XExpr sym)
bvOp forall (w :: Natural). BVOp1 sym w
f XExpr sym
xe = case XExpr sym
xe of
      XInt8 SymExpr sym (BaseBVType 8)
e -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
f SymExpr sym (BaseBVType 8)
e
      XInt16 SymExpr sym (BaseBVType 16)
e -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
f SymExpr sym (BaseBVType 16)
e
      XInt32 SymExpr sym (BaseBVType 32)
e -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
f SymExpr sym (BaseBVType 32)
e
      XInt64 SymExpr sym (BaseBVType 64)
e -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
f SymExpr sym (BaseBVType 64)
e
      XWord8 SymExpr sym (BaseBVType 8)
e -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
f SymExpr sym (BaseBVType 8)
e
      XWord16 SymExpr sym (BaseBVType 16)
e -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
f SymExpr sym (BaseBVType 16)
e
      XWord32 SymExpr sym (BaseBVType 32)
e -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
f SymExpr sym (BaseBVType 32)
e
      XWord64 SymExpr sym (BaseBVType 64)
e -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp1 sym w
f SymExpr sym (BaseBVType 64)
e
      XExpr sym
_ -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValue Name
"bvOp"

    fpOp :: (forall fi . FPOp1 sym fi) -> XExpr sym -> IO (XExpr sym)
    fpOp :: (forall (fi :: FloatInfo). FPOp1 sym fi)
-> XExpr sym -> IO (XExpr sym)
fpOp forall (fi :: FloatInfo). FPOp1 sym fi
g XExpr sym
xe = case XExpr sym
xe of
      XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e -> forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPOp1 sym fi
g FloatInfoRepr SingleFloat
WFP.SingleFloatRepr SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e
      XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e -> forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPOp1 sym fi
g FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e
      XExpr sym
_ -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValue Name
"fpOp"

    -- Translate a special-floating operation to the corresponding what4
    -- operation. These operations will be treated as uninterpreted functions in
    -- the solver.
    fpSpecialOp :: WSF.SpecialFunction (EmptyCtx ::> WSF.R)
                -> XExpr sym -> IO (XExpr sym)
    fpSpecialOp :: SpecialFunction (EmptyCtx ::> R) -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction (EmptyCtx ::> R)
fn = (forall (fi :: FloatInfo). FPOp1 sym fi)
-> XExpr sym -> IO (XExpr sym)
fpOp (\FloatInfoRepr fi
fiRepr -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SpecialFunction (EmptyCtx ::> R)
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatSpecialFunction1 sym
sym FloatInfoRepr fi
fiRepr SpecialFunction (EmptyCtx ::> R)
fn)

    -- Construct a floating-point literal value of the appropriate type.
    fpLit :: forall fi.
             WFP.FloatInfoRepr fi
          -> (forall frac. Fractional frac => frac)
          -> IO (WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi))
    fpLit :: forall (fi :: FloatInfo).
FloatInfoRepr fi
-> (forall frac. Fractional frac => frac)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
fpLit FloatInfoRepr fi
fiRepr forall frac. Fractional frac => frac
fracLit =
      case FloatInfoRepr fi
fiRepr of
        FloatInfoRepr fi
WFP.SingleFloatRepr -> forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Float -> IO (SymInterpretedFloat sym SingleFloat)
WFP.iFloatLitSingle sym
sym forall frac. Fractional frac => frac
fracLit
        FloatInfoRepr fi
WFP.DoubleFloatRepr -> forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Double -> IO (SymInterpretedFloat sym DoubleFloat)
WFP.iFloatLitDouble sym
sym forall frac. Fractional frac => frac
fracLit
        FloatInfoRepr fi
_ -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [Name
"Expected single- or double-precision float", forall a. Show a => a -> Name
show FloatInfoRepr fi
fiRepr]

    -- A catch-all error message to use when translation cannot proceed.
    unexpectedValue :: forall m x.
                       (Panic.HasCallStack, MonadIO m)
                    => String
                    -> m x
    unexpectedValue :: forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValue Name
op =
      forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [ Name
"Unexpected value in " forall a. [a] -> [a] -> [a]
++ Name
op forall a. [a] -> [a] -> [a]
++ Name
": " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall a. Expr a -> Doc
CP.ppExpr Expr b
origExpr)
            , forall a. Show a => a -> Name
show XExpr sym
xe
            ]

type BVOp2 sym w =
     (KnownNat w, 1 <= w)
  => WI.SymBV sym w
  -> WI.SymBV sym w
  -> IO (WI.SymBV sym w)

type FPOp2 sym fi =
     WFP.FloatInfoRepr fi
  -> WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi)
  -> WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi)
  -> IO (WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi))

type BoolCmp2 sym =
     WI.Pred sym
  -> WI.Pred sym
  -> IO (WI.Pred sym)

type BVCmp2 sym w =
     (KnownNat w, 1 <= w)
  => WI.SymBV sym w
  -> WI.SymBV sym w
  -> IO (WI.Pred sym)

type FPCmp2 sym fi =
     WFP.FloatInfoRepr fi
  -> WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi)
  -> WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi)
  -> IO (WI.Pred sym)

translateOp2 :: forall sym a b c .
                WFP.IsInterpretedFloatExprBuilder sym
             => sym
             -> CE.Expr c
             -- ^ Original value we are translating (only used for error
             -- messages)
             -> CE.Op2 a b c
             -> XExpr sym
             -> XExpr sym
             -> TransM sym (XExpr sym)
translateOp2 :: forall sym a b c.
IsInterpretedFloatExprBuilder sym =>
sym
-> Expr c
-> Op2 a b c
-> XExpr sym
-> XExpr sym
-> TransM sym (XExpr sym)
translateOp2 sym
sym Expr c
origExpr Op2 a b c
op XExpr sym
xe1 XExpr sym
xe2 = case (Op2 a b c
op, XExpr sym
xe1, XExpr sym
xe2) of
  (Op2 a b c
CE.And, XBool SymExpr sym BaseBoolType
e1, XBool SymExpr sym BaseBoolType
e2) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.andPred sym
sym SymExpr sym BaseBoolType
e1 SymExpr sym BaseBoolType
e2
  (Op2 a b c
CE.And, XExpr sym
_, XExpr sym
_) -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
"and operation"
  (Op2 a b c
CE.Or, XBool SymExpr sym BaseBoolType
e1, XBool SymExpr sym BaseBoolType
e2) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.orPred sym
sym SymExpr sym BaseBoolType
e1 SymExpr sym BaseBoolType
e2
  (Op2 a b c
CE.Or, XExpr sym
_, XExpr sym
_) -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
"or operation"
  (CE.Add Type a
_, XExpr sym
xe1, XExpr sym
xe2) -> XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateAdd XExpr sym
xe1 XExpr sym
xe2
  (CE.Sub Type a
_, XExpr sym
xe1, XExpr sym
xe2) -> XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateSub XExpr sym
xe1 XExpr sym
xe2
  (CE.Mul Type a
_, XExpr sym
xe1, XExpr sym
xe2) -> XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateMul XExpr sym
xe1 XExpr sym
xe2
  (CE.Mod Type a
_, XExpr sym
xe1, XExpr sym
xe2) -> do
    -- The second argument should not be zero
    forall sym.
IsExprBuilder sym =>
XExpr sym
-> (forall (w :: Natural).
    (1 <= w) =>
    SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym))
-> TransM sym ()
addBVSidePred1 XExpr sym
xe2 forall a b. (a -> b) -> a -> b
$ \SymBV sym w
e2 NatRepr w
_ BVSign
_ -> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
WI.bvIsNonzero sym
sym SymBV sym w
e2
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall (w :: Natural). BVOp2 sym w)
-> (forall (w :: Natural). BVOp2 sym w)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSrem sym
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvUrem sym
sym) XExpr sym
xe1 XExpr sym
xe2
  (CE.Div Type a
_, XExpr sym
xe1, XExpr sym
xe2) -> do
    -- The second argument should not be zero
    forall sym.
IsExprBuilder sym =>
XExpr sym
-> (forall (w :: Natural).
    (1 <= w) =>
    SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym))
-> TransM sym ()
addBVSidePred1 XExpr sym
xe2 forall a b. (a -> b) -> a -> b
$ \SymBV sym w
e2 NatRepr w
_ BVSign
_ -> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
WI.bvIsNonzero sym
sym SymBV sym w
e2
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall (w :: Natural). BVOp2 sym w)
-> (forall (w :: Natural). BVOp2 sym w)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSdiv sym
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvUdiv sym
sym) XExpr sym
xe1 XExpr sym
xe2

  -- We do not track any side conditions for floating-point operations
  -- (see Note [Side conditions for floating-point operations]), but we will
  -- make a note of which operations have partial inputs.

  -- The second argument should not be zero
  (CE.Fdiv Type a
_, XExpr sym
xe1, XExpr sym
xe2) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    (forall (fi :: FloatInfo). FPOp2 sym fi)
-> XExpr sym -> XExpr sym -> IO (XExpr sym)
fpOp (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatDiv @_ @fi sym
sym RoundingMode
fpRM)
         XExpr sym
xe1
         XExpr sym
xe2

  -- None of the following should happen:
  --
  -- * The first argument is negative, and the second argument is a finite
  --   noninteger
  --
  -- * The first argument is zero, and the second argument is negative
  --
  -- * The arguments cause the result to overflow
  --
  -- * The arguments cause the result to underflow
  (CE.Pow Type a
_, XExpr sym
xe1, XExpr sym
xe2) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction ((EmptyCtx ::> R) ::> R)
-> XExpr sym -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction ((EmptyCtx ::> R) ::> R)
WSF.Pow XExpr sym
xe1 XExpr sym
xe2
  -- The second argument should not be negative or zero
  (CE.Logb Type a
_, XExpr sym
xe1, XExpr sym
xe2) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall (fi :: FloatInfo). FPOp2 sym fi)
-> XExpr sym -> XExpr sym -> IO (XExpr sym)
fpOp forall (fi :: FloatInfo). FPOp2 sym fi
logbFn XExpr sym
xe1 XExpr sym
xe2
    where
      logbFn :: forall fi . FPOp2 sym fi
      -- Implement logb(e1,e2) as log(e2)/log(e1). This matches how copilot-c99
      -- translates Logb to C code.
      logbFn :: forall (fi :: FloatInfo). FPOp2 sym fi
logbFn FloatInfoRepr fi
fiRepr SymExpr sym (SymInterpretedFloatType sym fi)
e1 SymExpr sym (SymInterpretedFloatType sym fi)
e2 = do
        SymExpr sym (SymInterpretedFloatType sym fi)
re1 <- forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SpecialFunction (EmptyCtx ::> R)
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatSpecialFunction1 sym
sym FloatInfoRepr fi
fiRepr SpecialFunction (EmptyCtx ::> R)
WSF.Log SymExpr sym (SymInterpretedFloatType sym fi)
e1
        SymExpr sym (SymInterpretedFloatType sym fi)
re2 <- forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SpecialFunction (EmptyCtx ::> R)
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatSpecialFunction1 sym
sym FloatInfoRepr fi
fiRepr SpecialFunction (EmptyCtx ::> R)
WSF.Log SymExpr sym (SymInterpretedFloatType sym fi)
e2
        forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatDiv @_ @fi sym
sym RoundingMode
fpRM SymExpr sym (SymInterpretedFloatType sym fi)
re2 SymExpr sym (SymInterpretedFloatType sym fi)
re1
  (CE.Atan2 Type a
_, XExpr sym
xe1, XExpr sym
xe2) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SpecialFunction ((EmptyCtx ::> R) ::> R)
-> XExpr sym -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction ((EmptyCtx ::> R) ::> R)
WSF.Arctan2 XExpr sym
xe1 XExpr sym
xe2
  (CE.Eq Type a
_, XExpr sym
xe1, XExpr sym
xe2) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    BoolCmp2 sym
-> (forall (w :: Natural). BVCmp2 sym w)
-> (forall (fi :: FloatInfo). FPCmp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
cmp (forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.eqPred sym
sym)
        (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq sym
sym)
        (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
WFP.iFloatEq @_ @fi sym
sym)
        XExpr sym
xe1
        XExpr sym
xe2
  (CE.Ne Type a
_, XExpr sym
xe1, XExpr sym
xe2) -> XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateNe XExpr sym
xe1 XExpr sym
xe2
  (CE.Le Type a
_, XExpr sym
xe1, XExpr sym
xe2) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    (forall (w :: Natural). BVCmp2 sym w)
-> (forall (w :: Natural). BVCmp2 sym w)
-> (forall (fi :: FloatInfo). FPCmp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
numCmp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSle sym
sym)
           (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUle sym
sym)
           (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
WFP.iFloatLe @_ @fi sym
sym)
           XExpr sym
xe1
           XExpr sym
xe2
  (CE.Ge Type a
_, XExpr sym
xe1, XExpr sym
xe2) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    (forall (w :: Natural). BVCmp2 sym w)
-> (forall (w :: Natural). BVCmp2 sym w)
-> (forall (fi :: FloatInfo). FPCmp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
numCmp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSge sym
sym)
           (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUge sym
sym)
           (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
WFP.iFloatGe @_ @fi sym
sym)
           XExpr sym
xe1
           XExpr sym
xe2
  (CE.Lt Type a
_, XExpr sym
xe1, XExpr sym
xe2) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    (forall (w :: Natural). BVCmp2 sym w)
-> (forall (w :: Natural). BVCmp2 sym w)
-> (forall (fi :: FloatInfo). FPCmp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
numCmp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSlt sym
sym)
           (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUlt sym
sym)
           (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
WFP.iFloatLt @_ @fi sym
sym)
           XExpr sym
xe1
           XExpr sym
xe2
  (CE.Gt Type a
_, XExpr sym
xe1, XExpr sym
xe2) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
    (forall (w :: Natural). BVCmp2 sym w)
-> (forall (w :: Natural). BVCmp2 sym w)
-> (forall (fi :: FloatInfo). FPCmp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
numCmp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvSgt sym
sym)
           (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUgt sym
sym)
           (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
WFP.iFloatGt @_ @fi sym
sym)
           XExpr sym
xe1
           XExpr sym
xe2
  (CE.BwAnd Type a
_, XExpr sym
xe1, XExpr sym
xe2) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall (w :: Natural). BVOp2 sym w)
-> (forall (w :: Natural). BVOp2 sym w)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAndBits sym
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAndBits sym
sym) XExpr sym
xe1 XExpr sym
xe2
  (CE.BwOr Type a
_, XExpr sym
xe1, XExpr sym
xe2) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall (w :: Natural). BVOp2 sym w)
-> (forall (w :: Natural). BVOp2 sym w)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvOrBits sym
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvOrBits sym
sym) XExpr sym
xe1 XExpr sym
xe2
  (CE.BwXor Type a
_, XExpr sym
xe1, XExpr sym
xe2) ->
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ (forall (w :: Natural). BVOp2 sym w)
-> (forall (w :: Natural). BVOp2 sym w)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
bvOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvXorBits sym
sym) (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvXorBits sym
sym) XExpr sym
xe1 XExpr sym
xe2
  (CE.BwShiftL Type a
_ Type b
_, XExpr sym
xe1, XExpr sym
xe2) -> XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateBwShiftL XExpr sym
xe1 XExpr sym
xe2
  (CE.BwShiftR Type a
_ Type b
_, XExpr sym
xe1, XExpr sym
xe2) -> XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateBwShiftR XExpr sym
xe1 XExpr sym
xe2
  (CE.Index Type (Array n c)
_, XExpr sym
xe1, XExpr sym
xe2) -> XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateIndex XExpr sym
xe1 XExpr sym
xe2
  where
    -- Translate an 'CE.Add' operation and its arguments into a what4
    -- representation of the appropriate type.
    translateAdd :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
    translateAdd :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateAdd XExpr sym
xe1 XExpr sym
xe2 = do
      forall sym.
IsExprBuilder sym =>
XExpr sym
-> XExpr sym
-> (forall (w :: Natural).
    (1 <= w) =>
    SymBV sym w -> SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym))
-> TransM sym ()
addBVSidePred2 XExpr sym
xe1 XExpr sym
xe2 forall a b. (a -> b) -> a -> b
$ \SymBV sym w
e1 SymBV sym w
e2 NatRepr w
_ BVSign
sgn ->
        -- The arguments should not result in signed overflow or underflow
        case BVSign
sgn of
          BVSign
Signed -> do
            (SymExpr sym BaseBoolType
wrap, SymBV sym w
_) <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
WI.addSignedOF sym
sym SymBV sym w
e1 SymBV sym w
e2
            forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym SymExpr sym BaseBoolType
wrap
          BVSign
Unsigned -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym
WI.truePred sym
sym

      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
        (forall (w :: Natural). BVOp2 sym w)
-> (forall (fi :: FloatInfo). FPOp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
numOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAdd sym
sym)
              (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatAdd @_ @fi sym
sym RoundingMode
fpRM)
              XExpr sym
xe1
              XExpr sym
xe2

    -- Translate a 'CE.Sub' operation and its arguments into a what4
    -- representation of the appropriate type.
    translateSub :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
    translateSub :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateSub XExpr sym
xe1 XExpr sym
xe2 = do
      forall sym.
IsExprBuilder sym =>
XExpr sym
-> XExpr sym
-> (forall (w :: Natural).
    (1 <= w) =>
    SymBV sym w -> SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym))
-> TransM sym ()
addBVSidePred2 XExpr sym
xe1 XExpr sym
xe2 forall a b. (a -> b) -> a -> b
$ \SymBV sym w
e1 SymBV sym w
e2 NatRepr w
_ BVSign
sgn ->
        -- The arguments should not result in signed overflow or underflow
        case BVSign
sgn of
          BVSign
Signed -> do
            (SymExpr sym BaseBoolType
wrap, SymBV sym w
_) <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
WI.subSignedOF sym
sym SymBV sym w
e1 SymBV sym w
e2
            forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym SymExpr sym BaseBoolType
wrap
          BVSign
Unsigned -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym
WI.truePred sym
sym

      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
        (forall (w :: Natural). BVOp2 sym w)
-> (forall (fi :: FloatInfo). FPOp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
numOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvSub sym
sym)
              (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatSub @_ @fi sym
sym RoundingMode
fpRM)
              XExpr sym
xe1
              XExpr sym
xe2

    -- Translate a 'CE.Mul' operation and its arguments into a what4
    -- representation of the appropriate type.
    translateMul :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
    translateMul :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateMul XExpr sym
xe1 XExpr sym
xe2 = do
      forall sym.
IsExprBuilder sym =>
XExpr sym
-> XExpr sym
-> (forall (w :: Natural).
    (1 <= w) =>
    SymBV sym w -> SymBV sym w -> NatRepr w -> BVSign -> IO (Pred sym))
-> TransM sym ()
addBVSidePred2 XExpr sym
xe1 XExpr sym
xe2 forall a b. (a -> b) -> a -> b
$ \SymBV sym w
e1 SymBV sym w
e2 NatRepr w
_ BVSign
sgn ->
        -- The arguments should not result in signed overflow or underflow
        case BVSign
sgn of
          BVSign
Signed -> do
            (SymExpr sym BaseBoolType
wrap, SymBV sym w
_) <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym, SymBV sym w)
WI.mulSignedOF sym
sym SymBV sym w
e1 SymBV sym w
e2
            forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym SymExpr sym BaseBoolType
wrap
          BVSign
Unsigned -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym
WI.truePred sym
sym

      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
        (forall (w :: Natural). BVOp2 sym w)
-> (forall (fi :: FloatInfo). FPOp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
numOp (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvMul sym
sym)
              (\(FloatInfoRepr fi
_ :: WFP.FloatInfoRepr fi) -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatMul @_ @fi sym
sym RoundingMode
fpRM)
              XExpr sym
xe1
              XExpr sym
xe2

    -- Translate an 'CE.Ne' operation and its arguments into a what4
    -- representation of the appropriate type.
    translateNe :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
    translateNe :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateNe XExpr sym
xe1 XExpr sym
xe2 = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ BoolCmp2 sym
-> (forall (w :: Natural). BVCmp2 sym w)
-> (forall (fi :: FloatInfo). FPCmp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
cmp BoolCmp2 sym
neqPred forall (w :: Natural). BVCmp2 sym w
bvNeq forall (fi :: FloatInfo). FPCmp2 sym fi
fpNeq XExpr sym
xe1 XExpr sym
xe2
      where
        neqPred :: BoolCmp2 sym
        neqPred :: BoolCmp2 sym
neqPred SymExpr sym BaseBoolType
e1 SymExpr sym BaseBoolType
e2 = do
          SymExpr sym BaseBoolType
e <- forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.eqPred sym
sym SymExpr sym BaseBoolType
e1 SymExpr sym BaseBoolType
e2
          forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym SymExpr sym BaseBoolType
e

        bvNeq :: forall w . BVCmp2 sym w
        bvNeq :: forall (w :: Natural). BVCmp2 sym w
bvNeq SymBV sym w
e1 SymBV sym w
e2 = do
          SymExpr sym BaseBoolType
e <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq sym
sym SymBV sym w
e1 SymBV sym w
e2
          forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym SymExpr sym BaseBoolType
e

        fpNeq :: forall fi . FPCmp2 sym fi
        fpNeq :: forall (fi :: FloatInfo). FPCmp2 sym fi
fpNeq FloatInfoRepr fi
_ SymExpr sym (SymInterpretedFloatType sym fi)
e1 SymExpr sym (SymInterpretedFloatType sym fi)
e2 = do
          SymExpr sym BaseBoolType
e <- forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
WFP.iFloatEq @_ @fi sym
sym SymExpr sym (SymInterpretedFloatType sym fi)
e1 SymExpr sym (SymInterpretedFloatType sym fi)
e2
          forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred sym
sym SymExpr sym BaseBoolType
e

    -- Translate a 'CE.BwShiftL' operation and its arguments into a what4
    -- representation.
    --
    -- Note: we are interpreting the shifter as an unsigned bitvector regardless
    -- of whether it is a word or an int.
    translateBwShiftL :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
    translateBwShiftL :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateBwShiftL XExpr sym
xe1 XExpr sym
xe2 = do
      -- These partial pattern matches on Just should always succeed because
      -- BwShiftL should always have bitvectors as arguments.
      Just (SomeBVExpr SymBV sym w
e1 NatRepr w
w1 BVSign
sgn1 SymBV sym w -> XExpr sym
ctor1) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. XExpr sym -> Maybe (SomeBVExpr sym)
asBVExpr XExpr sym
xe1
      Just (SomeBVExpr SymBV sym w
e2 NatRepr w
w2 BVSign
_    SymBV sym w -> XExpr sym
_    ) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. XExpr sym -> Maybe (SomeBVExpr sym)
asBVExpr XExpr sym
xe2

      SymBV sym w
e2' <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ case forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr w
w1 NatRepr w
w2 of
          NatCaseLT LeqProof (w + 1) w
LeqProof -> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym NatRepr w
w1 SymBV sym w
e2
          NatCases w w
NatCaseEQ -> forall (m :: * -> *) a. Monad m => a -> m a
return SymBV sym w
e2
          NatCaseGT LeqProof (w + 1) w
LeqProof -> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym NatRepr w
w1 SymBV sym w
e2
      SymBV sym w
res <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvShl sym
sym SymBV sym w
e1 SymBV sym w
e2'

      -- The second argument should not be greater than or equal to the bit
      -- width
      SymBV sym w
wBV <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr w
w1 forall a b. (a -> b) -> a -> b
$ forall (w :: Natural). NatRepr w -> BV w
BV.width NatRepr w
w1
      SymExpr sym BaseBoolType
notTooLarge <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUlt sym
sym SymBV sym w
e2' SymBV sym w
wBV
      forall sym. Pred sym -> TransM sym ()
addSidePred SymExpr sym BaseBoolType
notTooLarge

      case BVSign
sgn1 of
        BVSign
Unsigned -> do
          -- Non-zero bits should not be shifted out
          SymBV sym w
otherDirection <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvLshr sym
sym SymBV sym w
res SymBV sym w
e2'
          SymExpr sym BaseBoolType
noWrap <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq sym
sym SymBV sym w
e1 SymBV sym w
otherDirection
          forall sym. Pred sym -> TransM sym ()
addSidePred SymExpr sym BaseBoolType
noWrap
        BVSign
Signed -> do
          -- Bits that disagree with the sign bit should not be shifted out
          SymBV sym w
otherDirection <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAshr sym
sym SymBV sym w
res SymBV sym w
e2'
          SymExpr sym BaseBoolType
noWrap <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq sym
sym SymBV sym w
e1 SymBV sym w
otherDirection
          forall sym. Pred sym -> TransM sym ()
addSidePred SymExpr sym BaseBoolType
noWrap

      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SymBV sym w -> XExpr sym
ctor1 SymBV sym w
res

    -- Translate a 'CE.BwShiftL' operation and its arguments into a what4
    -- representation.
    --
    -- Note: we are interpreting the shifter as an unsigned bitvector regardless
    -- of whether it is a word or an int.
    translateBwShiftR :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
    translateBwShiftR :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateBwShiftR XExpr sym
xe1 XExpr sym
xe2 = do
      -- These partial pattern matches on Just should always succeed because
      -- BwShiftL should always have bitvectors as arguments.
      Just (SomeBVExpr SymBV sym w
e1 NatRepr w
w1 BVSign
sgn1 SymBV sym w -> XExpr sym
ctor1) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. XExpr sym -> Maybe (SomeBVExpr sym)
asBVExpr XExpr sym
xe1
      Just (SomeBVExpr SymBV sym w
e2 NatRepr w
w2 BVSign
_    SymBV sym w -> XExpr sym
_    ) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. XExpr sym -> Maybe (SomeBVExpr sym)
asBVExpr XExpr sym
xe2

      SymBV sym w
e2' <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ case forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr w
w1 NatRepr w
w2 of
        NatCaseLT LeqProof (w + 1) w
LeqProof -> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym NatRepr w
w1 SymBV sym w
e2
        NatCases w w
NatCaseEQ -> forall (m :: * -> *) a. Monad m => a -> m a
return SymBV sym w
e2
        NatCaseGT LeqProof (w + 1) w
LeqProof -> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym NatRepr w
w1 SymBV sym w
e2

      -- The second argument should not be greater than or equal to the bit
      -- width
      SymBV sym w
wBV <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym NatRepr w
w1 forall a b. (a -> b) -> a -> b
$ forall (w :: Natural). NatRepr w -> BV w
BV.width NatRepr w
w1
      SymExpr sym BaseBoolType
notTooLarge <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUlt sym
sym SymBV sym w
e2' SymBV sym w
wBV
      forall sym. Pred sym -> TransM sym ()
addSidePred SymExpr sym BaseBoolType
notTooLarge

      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SymBV sym w -> XExpr sym
ctor1 forall a b. (a -> b) -> a -> b
$ case BVSign
sgn1 of
        BVSign
Signed -> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvAshr sym
sym SymBV sym w
e1 SymBV sym w
e2'
        BVSign
Unsigned -> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvLshr sym
sym SymBV sym w
e1 SymBV sym w
e2'

    -- Translate an 'CE.Index' operation and its arguments into a what4
    -- representation. This checks that the first argument is an 'XArray' and
    -- the second argument is an 'XWord32', invoking 'panic' is this invariant
    -- is not upheld.
    --
    -- Note: Currently, copilot only checks if array indices are out of bounds
    -- as a side condition. 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.
    translateIndex :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
    translateIndex :: XExpr sym -> XExpr sym -> TransM sym (XExpr sym)
translateIndex XExpr sym
xe1 XExpr sym
xe2 = case (XExpr sym
xe1, XExpr sym
xe2) of
      (XArray Vector n (XExpr sym)
xes, XWord32 SymExpr sym (BaseBVType 32)
ix) -> do
        -- The second argument should not be out of bounds (i.e., greater than
        -- or equal to the length of the array)
        SymExpr sym (BaseBVType 32)
xesLenBV <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat forall a b. (a -> b) -> a -> b
$ forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV forall (n :: Natural). KnownNat n => NatRepr n
knownNat
                           forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) a. Vector n a -> Id
V.lengthInt Vector n (XExpr sym)
xes
        SymExpr sym BaseBoolType
inRange <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvUlt sym
sym SymExpr sym (BaseBVType 32)
ix SymExpr sym (BaseBVType 32)
xesLenBV
        forall sym. Pred sym -> TransM sym ()
addSidePred SymExpr sym BaseBoolType
inRange

        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (n :: Natural).
(1 <= n, IsInterpretedFloatExprBuilder sym) =>
sym -> SymBV sym 32 -> Vector n (XExpr sym) -> IO (XExpr sym)
buildIndexExpr sym
sym SymExpr sym (BaseBVType 32)
ix Vector n (XExpr sym)
xes
      (XExpr sym, XExpr sym)
_ -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
"index operation"

    -- Check the types of the arguments. If the arguments are bitvector values,
    -- apply the 'BVOp2'. If the arguments are floating-point values, apply the
    -- 'FPOp2'. Otherwise, 'panic'.
    numOp :: (forall w . BVOp2 sym w)
          -> (forall fi . FPOp2 sym fi)
          -> XExpr sym
          -> XExpr sym
          -> IO (XExpr sym)
    numOp :: (forall (w :: Natural). BVOp2 sym w)
-> (forall (fi :: FloatInfo). FPOp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
numOp forall (w :: Natural). BVOp2 sym w
bvOp forall (fi :: FloatInfo). FPOp2 sym fi
fpOp XExpr sym
xe1 XExpr sym
xe2 = case (XExpr sym
xe1, XExpr sym
xe2) of
      (XInt8 SymExpr sym (BaseBVType 8)
e1, XInt8 SymExpr sym (BaseBVType 8)
e2) -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
bvOp SymExpr sym (BaseBVType 8)
e1 SymExpr sym (BaseBVType 8)
e2
      (XInt16 SymExpr sym (BaseBVType 16)
e1, XInt16 SymExpr sym (BaseBVType 16)
e2) -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
bvOp SymExpr sym (BaseBVType 16)
e1 SymExpr sym (BaseBVType 16)
e2
      (XInt32 SymExpr sym (BaseBVType 32)
e1, XInt32 SymExpr sym (BaseBVType 32)
e2) -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
bvOp SymExpr sym (BaseBVType 32)
e1 SymExpr sym (BaseBVType 32)
e2
      (XInt64 SymExpr sym (BaseBVType 64)
e1, XInt64 SymExpr sym (BaseBVType 64)
e2) -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
bvOp SymExpr sym (BaseBVType 64)
e1 SymExpr sym (BaseBVType 64)
e2
      (XWord8 SymExpr sym (BaseBVType 8)
e1, XWord8 SymExpr sym (BaseBVType 8)
e2) -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
bvOp SymExpr sym (BaseBVType 8)
e1 SymExpr sym (BaseBVType 8)
e2
      (XWord16 SymExpr sym (BaseBVType 16)
e1, XWord16 SymExpr sym (BaseBVType 16)
e2) -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
bvOp SymExpr sym (BaseBVType 16)
e1 SymExpr sym (BaseBVType 16)
e2
      (XWord32 SymExpr sym (BaseBVType 32)
e1, XWord32 SymExpr sym (BaseBVType 32)
e2) -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
bvOp SymExpr sym (BaseBVType 32)
e1 SymExpr sym (BaseBVType 32)
e2
      (XWord64 SymExpr sym (BaseBVType 64)
e1, XWord64 SymExpr sym (BaseBVType 64)
e2) -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
bvOp SymExpr sym (BaseBVType 64)
e1 SymExpr sym (BaseBVType 64)
e2
      (XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e1, XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e2) -> forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPOp2 sym fi
fpOp FloatInfoRepr SingleFloat
WFP.SingleFloatRepr SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e1 SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e2
      (XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e1, XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e2) -> forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPOp2 sym fi
fpOp FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e1 SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e2
      (XExpr sym, XExpr sym)
_ -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
"numOp"

    -- Check the types of the arguments. If the arguments are signed bitvector
    -- values, apply the first 'BVOp2'. If the arguments are unsigned bitvector
    -- values, apply the second 'BVOp2'. Otherwise, 'panic'.
    bvOp :: (forall w . BVOp2 sym w)
         -> (forall w . BVOp2 sym w)
         -> XExpr sym
         -> XExpr sym
         -> IO (XExpr sym)
    bvOp :: (forall (w :: Natural). BVOp2 sym w)
-> (forall (w :: Natural). BVOp2 sym w)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
bvOp forall (w :: Natural). BVOp2 sym w
opS forall (w :: Natural). BVOp2 sym w
opU XExpr sym
xe1 XExpr sym
xe2 = case (XExpr sym
xe1, XExpr sym
xe2) of
      (XInt8 SymExpr sym (BaseBVType 8)
e1, XInt8 SymExpr sym (BaseBVType 8)
e2) -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
opS SymExpr sym (BaseBVType 8)
e1 SymExpr sym (BaseBVType 8)
e2
      (XInt16 SymExpr sym (BaseBVType 16)
e1, XInt16 SymExpr sym (BaseBVType 16)
e2) -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
opS SymExpr sym (BaseBVType 16)
e1 SymExpr sym (BaseBVType 16)
e2
      (XInt32 SymExpr sym (BaseBVType 32)
e1, XInt32 SymExpr sym (BaseBVType 32)
e2) -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
opS SymExpr sym (BaseBVType 32)
e1 SymExpr sym (BaseBVType 32)
e2
      (XInt64 SymExpr sym (BaseBVType 64)
e1, XInt64 SymExpr sym (BaseBVType 64)
e2) -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
opS SymExpr sym (BaseBVType 64)
e1 SymExpr sym (BaseBVType 64)
e2
      (XWord8 SymExpr sym (BaseBVType 8)
e1, XWord8 SymExpr sym (BaseBVType 8)
e2) -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
opU SymExpr sym (BaseBVType 8)
e1 SymExpr sym (BaseBVType 8)
e2
      (XWord16 SymExpr sym (BaseBVType 16)
e1, XWord16 SymExpr sym (BaseBVType 16)
e2) -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
opU SymExpr sym (BaseBVType 16)
e1 SymExpr sym (BaseBVType 16)
e2
      (XWord32 SymExpr sym (BaseBVType 32)
e1, XWord32 SymExpr sym (BaseBVType 32)
e2) -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
opU SymExpr sym (BaseBVType 32)
e1 SymExpr sym (BaseBVType 32)
e2
      (XWord64 SymExpr sym (BaseBVType 64)
e1, XWord64 SymExpr sym (BaseBVType 64)
e2) -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVOp2 sym w
opU SymExpr sym (BaseBVType 64)
e1 SymExpr sym (BaseBVType 64)
e2
      (XExpr sym, XExpr sym)
_ -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
"bvOp"

    fpOp :: (forall fi . FPOp2 sym fi)
         -> XExpr sym
         -> XExpr sym
         -> IO (XExpr sym)
    fpOp :: (forall (fi :: FloatInfo). FPOp2 sym fi)
-> XExpr sym -> XExpr sym -> IO (XExpr sym)
fpOp forall (fi :: FloatInfo). FPOp2 sym fi
op XExpr sym
xe1 XExpr sym
xe2 = case (XExpr sym
xe1, XExpr sym
xe2) of
      (XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e1, XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e2) -> forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPOp2 sym fi
op FloatInfoRepr SingleFloat
WFP.SingleFloatRepr SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e1 SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e2
      (XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e1, XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e2) -> forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPOp2 sym fi
op FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e1 SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e2
      (XExpr sym, XExpr sym)
_ -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
"fpOp"

    -- Translate a special-floating operation to the corresponding what4
    -- operation. These operations will be treated as uninterpreted functions in
    -- the solver.
    fpSpecialOp :: WSF.SpecialFunction (EmptyCtx ::> WSF.R ::> WSF.R)
                -> XExpr sym -> XExpr sym -> IO (XExpr sym)
    fpSpecialOp :: SpecialFunction ((EmptyCtx ::> R) ::> R)
-> XExpr sym -> XExpr sym -> IO (XExpr sym)
fpSpecialOp SpecialFunction ((EmptyCtx ::> R) ::> R)
fn = (forall (fi :: FloatInfo). FPOp2 sym fi)
-> XExpr sym -> XExpr sym -> IO (XExpr sym)
fpOp (\FloatInfoRepr fi
fiRepr -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SpecialFunction ((EmptyCtx ::> R) ::> R)
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatSpecialFunction2 sym
sym FloatInfoRepr fi
fiRepr SpecialFunction ((EmptyCtx ::> R) ::> R)
fn)

    -- Check the types of the arguments. If the arguments are bitvector values,
    -- apply the 'BVCmp2'. If the arguments are floating-point values, apply the
    -- 'FPCmp2'. Otherwise, 'panic'.
    cmp :: BoolCmp2 sym
        -> (forall w . BVCmp2 sym w)
        -> (forall fi . FPCmp2 sym fi)
        -> XExpr sym
        -> XExpr sym
        -> IO (XExpr sym)
    cmp :: BoolCmp2 sym
-> (forall (w :: Natural). BVCmp2 sym w)
-> (forall (fi :: FloatInfo). FPCmp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
cmp BoolCmp2 sym
boolOp forall (w :: Natural). BVCmp2 sym w
bvOp forall (fi :: FloatInfo). FPCmp2 sym fi
fpOp XExpr sym
xe1 XExpr sym
xe2 = case (XExpr sym
xe1, XExpr sym
xe2) of
      (XBool SymExpr sym BaseBoolType
e1, XBool SymExpr sym BaseBoolType
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BoolCmp2 sym
boolOp SymExpr sym BaseBoolType
e1 SymExpr sym BaseBoolType
e2
      (XInt8 SymExpr sym (BaseBVType 8)
e1, XInt8 SymExpr sym (BaseBVType 8)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvOp SymExpr sym (BaseBVType 8)
e1 SymExpr sym (BaseBVType 8)
e2
      (XInt16 SymExpr sym (BaseBVType 16)
e1, XInt16 SymExpr sym (BaseBVType 16)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvOp SymExpr sym (BaseBVType 16)
e1 SymExpr sym (BaseBVType 16)
e2
      (XInt32 SymExpr sym (BaseBVType 32)
e1, XInt32 SymExpr sym (BaseBVType 32)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvOp SymExpr sym (BaseBVType 32)
e1 SymExpr sym (BaseBVType 32)
e2
      (XInt64 SymExpr sym (BaseBVType 64)
e1, XInt64 SymExpr sym (BaseBVType 64)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvOp SymExpr sym (BaseBVType 64)
e1 SymExpr sym (BaseBVType 64)
e2
      (XWord8 SymExpr sym (BaseBVType 8)
e1, XWord8 SymExpr sym (BaseBVType 8)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvOp SymExpr sym (BaseBVType 8)
e1 SymExpr sym (BaseBVType 8)
e2
      (XWord16 SymExpr sym (BaseBVType 16)
e1, XWord16 SymExpr sym (BaseBVType 16)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvOp SymExpr sym (BaseBVType 16)
e1 SymExpr sym (BaseBVType 16)
e2
      (XWord32 SymExpr sym (BaseBVType 32)
e1, XWord32 SymExpr sym (BaseBVType 32)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvOp SymExpr sym (BaseBVType 32)
e1 SymExpr sym (BaseBVType 32)
e2
      (XWord64 SymExpr sym (BaseBVType 64)
e1, XWord64 SymExpr sym (BaseBVType 64)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvOp SymExpr sym (BaseBVType 64)
e1 SymExpr sym (BaseBVType 64)
e2
      (XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e1, XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPCmp2 sym fi
fpOp FloatInfoRepr SingleFloat
WFP.SingleFloatRepr SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e1 SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e2
      (XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e1, XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPCmp2 sym fi
fpOp FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e1 SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e2
      (XExpr sym, XExpr sym)
_ -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
"cmp"

    -- Check the types of the arguments. If the arguments are signed bitvector
    -- values, apply the first 'BVCmp2'. If the arguments are unsigned bitvector
    -- values, apply the second 'BVCmp2'. If the arguments are floating-point
    -- values, apply the 'FPCmp2'. Otherwise, 'panic'.
    numCmp :: (forall w . BVCmp2 sym w)
           -> (forall w . BVCmp2 sym w)
           -> (forall fi . FPCmp2 sym fi)
           -> XExpr sym
           -> XExpr sym
           -> IO (XExpr sym)
    numCmp :: (forall (w :: Natural). BVCmp2 sym w)
-> (forall (w :: Natural). BVCmp2 sym w)
-> (forall (fi :: FloatInfo). FPCmp2 sym fi)
-> XExpr sym
-> XExpr sym
-> IO (XExpr sym)
numCmp forall (w :: Natural). BVCmp2 sym w
bvSOp forall (w :: Natural). BVCmp2 sym w
bvUOp forall (fi :: FloatInfo). FPCmp2 sym fi
fpOp XExpr sym
xe1 XExpr sym
xe2 = case (XExpr sym
xe1, XExpr sym
xe2) of
      (XInt8 SymExpr sym (BaseBVType 8)
e1, XInt8 SymExpr sym (BaseBVType 8)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvSOp SymExpr sym (BaseBVType 8)
e1 SymExpr sym (BaseBVType 8)
e2
      (XInt16 SymExpr sym (BaseBVType 16)
e1, XInt16 SymExpr sym (BaseBVType 16)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvSOp SymExpr sym (BaseBVType 16)
e1 SymExpr sym (BaseBVType 16)
e2
      (XInt32 SymExpr sym (BaseBVType 32)
e1, XInt32 SymExpr sym (BaseBVType 32)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvSOp SymExpr sym (BaseBVType 32)
e1 SymExpr sym (BaseBVType 32)
e2
      (XInt64 SymExpr sym (BaseBVType 64)
e1, XInt64 SymExpr sym (BaseBVType 64)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvSOp SymExpr sym (BaseBVType 64)
e1 SymExpr sym (BaseBVType 64)
e2
      (XWord8 SymExpr sym (BaseBVType 8)
e1, XWord8 SymExpr sym (BaseBVType 8)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvUOp SymExpr sym (BaseBVType 8)
e1 SymExpr sym (BaseBVType 8)
e2
      (XWord16 SymExpr sym (BaseBVType 16)
e1, XWord16 SymExpr sym (BaseBVType 16)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvUOp SymExpr sym (BaseBVType 16)
e1 SymExpr sym (BaseBVType 16)
e2
      (XWord32 SymExpr sym (BaseBVType 32)
e1, XWord32 SymExpr sym (BaseBVType 32)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvUOp SymExpr sym (BaseBVType 32)
e1 SymExpr sym (BaseBVType 32)
e2
      (XWord64 SymExpr sym (BaseBVType 64)
e1, XWord64 SymExpr sym (BaseBVType 64)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural). BVCmp2 sym w
bvUOp SymExpr sym (BaseBVType 64)
e1 SymExpr sym (BaseBVType 64)
e2
      (XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e1, XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPCmp2 sym fi
fpOp FloatInfoRepr SingleFloat
WFP.SingleFloatRepr SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e1 SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e2
      (XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e1, XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fi :: FloatInfo). FPCmp2 sym fi
fpOp FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e1 SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e2
      (XExpr sym, XExpr sym)
_ -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
"numCmp"

    -- A catch-all error message to use when translation cannot proceed.
    unexpectedValues :: forall m x.
                        (Panic.HasCallStack, MonadIO m)
                     => String
                     -> m x
    unexpectedValues :: forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
op =
      forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [ Name
"Unexpected values in " forall a. [a] -> [a] -> [a]
++ Name
op forall a. [a] -> [a] -> [a]
++ Name
": " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall a. Expr a -> Doc
CP.ppExpr Expr c
origExpr)
            , forall a. Show a => a -> Name
show XExpr sym
xe1, forall a. Show a => a -> Name
show XExpr sym
xe2
            ]

translateOp3 :: forall sym a b c d .
                WFP.IsInterpretedFloatExprBuilder sym
             => sym
             -> CE.Expr d
             -- ^ Original value we are translating (only used for error
             -- messages)
             -> CE.Op3 a b c d
             -> XExpr sym
             -> XExpr sym
             -> XExpr sym
             -> TransM sym (XExpr sym)
translateOp3 :: forall sym a b c d.
IsInterpretedFloatExprBuilder sym =>
sym
-> Expr d
-> Op3 a b c d
-> XExpr sym
-> XExpr sym
-> XExpr sym
-> TransM sym (XExpr sym)
translateOp3 sym
sym Expr d
origExpr Op3 a b c d
op XExpr sym
xe1 XExpr sym
xe2 XExpr sym
xe3 = case (Op3 a b c d
op, XExpr sym
xe1, XExpr sym
xe2, XExpr sym
xe3) of
    (CE.Mux Type b
_, XBool SymExpr sym BaseBoolType
te, XExpr sym
xe1, XExpr sym
xe2) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Pred sym -> XExpr sym -> XExpr sym -> IO (XExpr sym)
mkIte sym
sym SymExpr sym BaseBoolType
te XExpr sym
xe1 XExpr sym
xe2
    (CE.Mux Type b
_, XExpr sym
_, XExpr sym
_, XExpr sym
_) -> forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
"mux operation"
  where
    unexpectedValues :: forall m x . (Panic.HasCallStack, MonadIO m)
                     => String -> m x
    unexpectedValues :: forall (m :: * -> *) x. (HasCallStack, MonadIO m) => Name -> m x
unexpectedValues Name
op =
      forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [ Name
"Unexpected values in " forall a. [a] -> [a] -> [a]
++ Name
op forall a. [a] -> [a] -> [a]
++ Name
":"
            , forall a. Show a => a -> Name
show (forall a. Expr a -> Doc
CP.ppExpr Expr d
origExpr), forall a. Show a => a -> Name
show XExpr sym
xe1, forall a. Show a => a -> Name
show XExpr sym
xe2, forall a. Show a => a -> Name
show XExpr sym
xe3
            ]

-- | Construct an expression that indexes into an array by building a chain of
-- @if@ expressions, where each expression checks if the current index is equal
-- to a given index in the array. If the indices are equal, return the element
-- of the array at that index. Otherwise, proceed to the next @if@ expression,
-- which checks the next index in the array.
buildIndexExpr :: forall sym n.
                  (1 <= n, WFP.IsInterpretedFloatExprBuilder sym)
               => sym
               -> WI.SymBV sym 32
               -- ^ Index
               -> V.Vector n (XExpr sym)
               -- ^ Elements
               -> IO (XExpr sym)
buildIndexExpr :: forall sym (n :: Natural).
(1 <= n, IsInterpretedFloatExprBuilder sym) =>
sym -> SymBV sym 32 -> Vector n (XExpr sym) -> IO (XExpr sym)
buildIndexExpr sym
sym SymBV sym 32
ix = forall (n' :: Natural).
(1 <= n') =>
DropIdx -> Vector n' (XExpr sym) -> IO (XExpr sym)
loop DropIdx
0
  where
    loop :: forall n'.
            (1 <= n')
         => Word32
         -> V.Vector n' (XExpr sym)
         -> IO (XExpr sym)
    loop :: forall (n' :: Natural).
(1 <= n') =>
DropIdx -> Vector n' (XExpr sym) -> IO (XExpr sym)
loop DropIdx
curIx Vector n' (XExpr sym)
xelts = case forall (n :: Natural) a.
Vector n a -> (a, Either (n :~: 1) (Vector (n - 1) a))
V.uncons Vector n' (XExpr sym)
xelts of
      -- Base case, exactly one element left
      (XExpr sym
xe, Left n' :~: 1
Refl) -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
      -- Recursive case
      (XExpr sym
xe, Right Vector (n' - 1) (XExpr sym)
xelts') -> do
        LeqProof 1 (n' - 1)
LeqProof <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) a. Vector n a -> LeqProof 1 n
V.nonEmpty Vector (n' - 1) (XExpr sym)
xelts'
        XExpr sym
rstExpr <- forall (n' :: Natural).
(1 <= n') =>
DropIdx -> Vector n' (XExpr sym) -> IO (XExpr sym)
loop (DropIdx
curIxforall a. Num a => a -> a -> a
+DropIdx
1) Vector (n' - 1) (XExpr sym)
xelts'
        SymBV sym 32
curIxExpr <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
WI.bvLit sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat (DropIdx -> BV 32
BV.word32 DropIdx
curIx)
        SymExpr sym BaseBoolType
ixEq <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
WI.bvEq sym
sym SymBV sym 32
curIxExpr SymBV sym 32
ix
        forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Pred sym -> XExpr sym -> XExpr sym -> IO (XExpr sym)
mkIte sym
sym SymExpr sym BaseBoolType
ixEq XExpr sym
xe XExpr sym
rstExpr

-- | Construct an @if@ expression of the appropriate type.
mkIte :: WFP.IsInterpretedFloatExprBuilder sym
      => sym
      -> WI.Pred sym
      -> XExpr sym
      -> XExpr sym
      -> IO (XExpr sym)
mkIte :: forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Pred sym -> XExpr sym -> XExpr sym -> IO (XExpr sym)
mkIte sym
sym Pred sym
pred XExpr sym
xe1 XExpr sym
xe2 = case (XExpr sym
xe1, XExpr sym
xe2) of
  (XBool Pred sym
e1, XBool Pred sym
e2) -> forall sym. SymExpr sym BaseBoolType -> XExpr sym
XBool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.itePred sym
sym Pred sym
pred Pred sym
e1 Pred sym
e2
  (XInt8 SymExpr sym (BaseBVType 8)
e1, XInt8 SymExpr sym (BaseBVType 8)
e2) -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym Pred sym
pred SymExpr sym (BaseBVType 8)
e1 SymExpr sym (BaseBVType 8)
e2
  (XInt16 SymExpr sym (BaseBVType 16)
e1, XInt16 SymExpr sym (BaseBVType 16)
e2) -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym Pred sym
pred SymExpr sym (BaseBVType 16)
e1 SymExpr sym (BaseBVType 16)
e2
  (XInt32 SymExpr sym (BaseBVType 32)
e1, XInt32 SymExpr sym (BaseBVType 32)
e2) -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym Pred sym
pred SymExpr sym (BaseBVType 32)
e1 SymExpr sym (BaseBVType 32)
e2
  (XInt64 SymExpr sym (BaseBVType 64)
e1, XInt64 SymExpr sym (BaseBVType 64)
e2) -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym Pred sym
pred SymExpr sym (BaseBVType 64)
e1 SymExpr sym (BaseBVType 64)
e2
  (XWord8 SymExpr sym (BaseBVType 8)
e1, XWord8 SymExpr sym (BaseBVType 8)
e2) -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym Pred sym
pred SymExpr sym (BaseBVType 8)
e1 SymExpr sym (BaseBVType 8)
e2
  (XWord16 SymExpr sym (BaseBVType 16)
e1, XWord16 SymExpr sym (BaseBVType 16)
e2) -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym Pred sym
pred SymExpr sym (BaseBVType 16)
e1 SymExpr sym (BaseBVType 16)
e2
  (XWord32 SymExpr sym (BaseBVType 32)
e1, XWord32 SymExpr sym (BaseBVType 32)
e2) -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym Pred sym
pred SymExpr sym (BaseBVType 32)
e1 SymExpr sym (BaseBVType 32)
e2
  (XWord64 SymExpr sym (BaseBVType 64)
e1, XWord64 SymExpr sym (BaseBVType 64)
e2) -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
WI.bvIte sym
sym Pred sym
pred SymExpr sym (BaseBVType 64)
e1 SymExpr sym (BaseBVType 64)
e2
  (XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e1, XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e2) ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatIte @_ @WFP.SingleFloat sym
sym Pred sym
pred SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e1 SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e2
  (XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e1, XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e2) ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
WFP.iFloatIte @_ @WFP.DoubleFloat sym
sym Pred sym
pred SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e1 SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e2
  (XStruct [XExpr sym]
xes1, XStruct [XExpr sym]
xes2) ->
    forall sym. [XExpr sym] -> XExpr sym
XStruct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Pred sym -> XExpr sym -> XExpr sym -> IO (XExpr sym)
mkIte sym
sym Pred sym
pred) [XExpr sym]
xes1 [XExpr sym]
xes2
  (XExpr sym
XEmptyArray, XExpr sym
XEmptyArray) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall sym. XExpr sym
XEmptyArray
  (XArray Vector n (XExpr sym)
xes1, XArray Vector n (XExpr sym)
xes2) ->
    case forall (n :: Natural) a. Vector n a -> NatRepr n
V.length Vector n (XExpr sym)
xes1 forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` forall (n :: Natural) a. Vector n a -> NatRepr n
V.length Vector n (XExpr sym)
xes2 of
      Just n :~: n
Refl -> forall (n :: Natural) sym.
(1 <= n) =>
Vector n (XExpr sym) -> XExpr sym
XArray forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c (n :: Natural).
Monad m =>
(a -> b -> m c) -> Vector n a -> Vector n b -> m (Vector n c)
V.zipWithM (forall sym.
IsInterpretedFloatExprBuilder sym =>
sym -> Pred sym -> XExpr sym -> XExpr sym -> IO (XExpr sym)
mkIte sym
sym Pred sym
pred) Vector n (XExpr sym)
xes1 Vector n (XExpr sym)
xes2
      Maybe (n :~: n)
Nothing -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [ Name
"Array length mismatch in ite"
                       , forall a. Show a => a -> Name
show (forall (n :: Natural) a. Vector n a -> NatRepr n
V.length Vector n (XExpr sym)
xes1)
                       , forall a. Show a => a -> Name
show (forall (n :: Natural) a. Vector n a -> NatRepr n
V.length Vector n (XExpr sym)
xes2)
                       ]
  (XExpr sym, XExpr sym)
_ -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [Name
"Unexpected values in ite", forall a. Show a => a -> Name
show XExpr sym
xe1, forall a. Show a => a -> Name
show XExpr sym
xe2]

-- | Cast an 'XExpr' to another 'XExpr' of a possibly differing type.
castOp :: WFP.IsInterpretedFloatExprBuilder sym
       => sym
       -> CE.Expr b
       -- ^ Original value we are translating (only used for error
       -- messages)
       -> CT.Type a
       -- ^ Type we are casting to
       -> XExpr sym
       -- ^ Value to cast
       -> IO (XExpr sym)
castOp :: forall sym b a.
IsInterpretedFloatExprBuilder sym =>
sym -> Expr b -> Type a -> XExpr sym -> IO (XExpr sym)
castOp sym
sym Expr b
origExpr Type a
tp XExpr sym
xe = case (XExpr sym
xe, Type a
tp) of
  -- "safe" casts that cannot lose information
  (XBool SymExpr sym BaseBoolType
_, Type a
CT.Bool)     -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
  (XBool SymExpr sym BaseBoolType
e, Type a
CT.Word8)    -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV sym
sym SymExpr sym BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
  (XBool SymExpr sym BaseBoolType
e, Type a
CT.Word16)   -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV sym
sym SymExpr sym BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
  (XBool SymExpr sym BaseBoolType
e, Type a
CT.Word32)   -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV sym
sym SymExpr sym BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
  (XBool SymExpr sym BaseBoolType
e, Type a
CT.Word64)   -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV sym
sym SymExpr sym BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
  (XBool SymExpr sym BaseBoolType
e, Type a
CT.Int8)     -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV sym
sym SymExpr sym BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
  (XBool SymExpr sym BaseBoolType
e, Type a
CT.Int16)    -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV sym
sym SymExpr sym BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
  (XBool SymExpr sym BaseBoolType
e, Type a
CT.Int32)    -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV sym
sym SymExpr sym BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat
  (XBool SymExpr sym BaseBoolType
e, Type a
CT.Int64)    -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
WI.predToBV sym
sym SymExpr sym BaseBoolType
e forall (n :: Natural). KnownNat n => NatRepr n
knownNat

  (XInt8 SymExpr sym (BaseBVType 8)
_, Type a
CT.Int8)     -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
  (XInt8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Int16)    -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 8)
e
  (XInt8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Int32)    -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 8)
e
  (XInt8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Int64)    -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 8)
e
  (XInt16 SymExpr sym (BaseBVType 16)
_, Type a
CT.Int16)   -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
  (XInt16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Int32)   -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 16)
e
  (XInt16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Int64)   -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 16)
e
  (XInt32 SymExpr sym (BaseBVType 32)
_, Type a
CT.Int32)   -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
  (XInt32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Int64)   -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvSext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 32)
e
  (XInt64 SymExpr sym (BaseBVType 64)
_, Type a
CT.Int64)   -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe

  (XWord8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Int16)   -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 8)
e
  (XWord8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Int32)   -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 8)
e
  (XWord8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Int64)   -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 8)
e
  (XWord8 SymExpr sym (BaseBVType 8)
_, Type a
CT.Word8)   -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
  (XWord8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Word16)  -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 8)
e
  (XWord8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Word32)  -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 8)
e
  (XWord8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Word64)  -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 8)
e
  (XWord16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Int32)  -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 16)
e
  (XWord16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Int64)  -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 16)
e
  (XWord16 SymExpr sym (BaseBVType 16)
_, Type a
CT.Word16) -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
  (XWord16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Word32) -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 16)
e
  (XWord16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Word64) -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 16)
e
  (XWord32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Int64)  -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 32)
e
  (XWord32 SymExpr sym (BaseBVType 32)
_, Type a
CT.Word32) -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe
  (XWord32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Word64) -> forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
WI.bvZext sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 32)
e
  (XWord64 SymExpr sym (BaseBVType 64)
_, Type a
CT.Word64) -> forall (m :: * -> *) a. Monad m => a -> m a
return XExpr sym
xe

  -- "unsafe" casts, which may lose information
  -- unsigned truncations
  (XWord64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Word32) -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 64)
e
  (XWord64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Word16) -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 64)
e
  (XWord64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Word8)  -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 64)
e
  (XWord32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Word16) -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 32)
e
  (XWord32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Word8)  -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 32)
e
  (XWord16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Word8)  -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 16)
e

  -- signed truncations
  (XInt64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Int32)   -> forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 64)
e
  (XInt64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Int16)   -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 64)
e
  (XInt64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Int8)    -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 64)
e
  (XInt32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Int16)   -> forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 32)
e
  (XInt32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Int8)    -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 32)
e
  (XInt16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Int8)    -> forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
WI.bvTrunc sym
sym forall (n :: Natural). KnownNat n => NatRepr n
knownNat SymExpr sym (BaseBVType 16)
e

  -- signed integer to float
  (XInt64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Float)   ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iSBVToFloat sym
sym FloatInfoRepr SingleFloat
WFP.SingleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 64)
e
  (XInt32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Float)   ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iSBVToFloat sym
sym FloatInfoRepr SingleFloat
WFP.SingleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 32)
e
  (XInt16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Float)   ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iSBVToFloat sym
sym FloatInfoRepr SingleFloat
WFP.SingleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 16)
e
  (XInt8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Float)    ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iSBVToFloat sym
sym FloatInfoRepr SingleFloat
WFP.SingleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 8)
e

  -- unsigned integer to float
  (XWord64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Float)  ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iBVToFloat sym
sym FloatInfoRepr SingleFloat
WFP.SingleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 64)
e
  (XWord32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Float)  ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iBVToFloat sym
sym FloatInfoRepr SingleFloat
WFP.SingleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 32)
e
  (XWord16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Float)  ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iBVToFloat sym
sym FloatInfoRepr SingleFloat
WFP.SingleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 16)
e
  (XWord8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Float)   ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
XFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iBVToFloat sym
sym FloatInfoRepr SingleFloat
WFP.SingleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 8)
e

  -- signed integer to double
  (XInt64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Double)  ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iSBVToFloat sym
sym FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 64)
e
  (XInt32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Double)  ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iSBVToFloat sym
sym FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 32)
e
  (XInt16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Double)  ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iSBVToFloat sym
sym FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 16)
e
  (XInt8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Double)   ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iSBVToFloat sym
sym FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 8)
e

  -- unsigned integer to double
  (XWord64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Double) ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iBVToFloat sym
sym FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 64)
e
  (XWord32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Double) ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iBVToFloat sym
sym FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 32)
e
  (XWord16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Double) ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iBVToFloat sym
sym FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 16)
e
  (XWord8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Double)  ->
    forall sym.
SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
XDouble forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural) (fi :: FloatInfo).
(IsInterpretedFloatExprBuilder sym, 1 <= w) =>
sym
-> FloatInfoRepr fi
-> RoundingMode
-> SymBV sym w
-> IO (SymInterpretedFloat sym fi)
WFP.iBVToFloat sym
sym FloatInfoRepr DoubleFloat
WFP.DoubleFloatRepr RoundingMode
fpRM SymExpr sym (BaseBVType 8)
e

  -- unsigned to signed conversion
  (XWord64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Int64)  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XInt64 SymExpr sym (BaseBVType 64)
e
  (XWord32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Int32)  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XInt32 SymExpr sym (BaseBVType 32)
e
  (XWord16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Int16)  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XInt16 SymExpr sym (BaseBVType 16)
e
  (XWord8 SymExpr sym (BaseBVType 8)
e,  Type a
CT.Int8)   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XInt8 SymExpr sym (BaseBVType 8)
e

  -- signed to unsigned conversion
  (XInt64 SymExpr sym (BaseBVType 64)
e, Type a
CT.Word64)  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
XWord64 SymExpr sym (BaseBVType 64)
e
  (XInt32 SymExpr sym (BaseBVType 32)
e, Type a
CT.Word32)  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
XWord32 SymExpr sym (BaseBVType 32)
e
  (XInt16 SymExpr sym (BaseBVType 16)
e, Type a
CT.Word16)  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
XWord16 SymExpr sym (BaseBVType 16)
e
  (XInt8 SymExpr sym (BaseBVType 8)
e, Type a
CT.Word8)    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
XWord8 SymExpr sym (BaseBVType 8)
e

  (XExpr sym, Type a)
_ -> forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [Name
"Could not compute cast", forall a. Show a => a -> Name
show (forall a. Expr a -> Doc
CP.ppExpr Expr b
origExpr), forall a. Show a => a -> Name
show XExpr sym
xe]

-- * What4 representations of Copilot expressions

-- | 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 sym@ 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 sym where
  XBool       :: WI.SymExpr sym WT.BaseBoolType -> XExpr sym
  XInt8       :: WI.SymExpr sym (WT.BaseBVType 8) -> XExpr sym
  XInt16      :: WI.SymExpr sym (WT.BaseBVType 16) -> XExpr sym
  XInt32      :: WI.SymExpr sym (WT.BaseBVType 32) -> XExpr sym
  XInt64      :: WI.SymExpr sym (WT.BaseBVType 64) -> XExpr sym
  XWord8      :: WI.SymExpr sym (WT.BaseBVType 8) -> XExpr sym
  XWord16     :: WI.SymExpr sym (WT.BaseBVType 16) -> XExpr sym
  XWord32     :: WI.SymExpr sym (WT.BaseBVType 32) -> XExpr sym
  XWord64     :: WI.SymExpr sym (WT.BaseBVType 64) -> XExpr sym
  XFloat      :: WI.SymExpr
                   sym
                   (WFP.SymInterpretedFloatType sym WFP.SingleFloat)
              -> XExpr sym
  XDouble     :: WI.SymExpr
                   sym
                   (WFP.SymInterpretedFloatType sym WFP.DoubleFloat)
              -> XExpr sym
  XEmptyArray :: XExpr sym
  XArray      :: 1 <= n => V.Vector n (XExpr sym) -> XExpr sym
  XStruct     :: [XExpr sym] -> XExpr sym

instance WI.IsExprBuilder sym => Show (XExpr sym) where
  show :: XExpr sym -> Name
show (XBool SymExpr sym BaseBoolType
e)    = Name
"XBool " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym BaseBoolType
e)
  show (XInt8 SymExpr sym (BaseBVType 8)
e)    = Name
"XInt8 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 8)
e)
  show (XInt16 SymExpr sym (BaseBVType 16)
e)   = Name
"XInt16 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 16)
e)
  show (XInt32 SymExpr sym (BaseBVType 32)
e)   = Name
"XInt32 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 32)
e)
  show (XInt64 SymExpr sym (BaseBVType 64)
e)   = Name
"XInt64 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 64)
e)
  show (XWord8 SymExpr sym (BaseBVType 8)
e)   = Name
"XWord8 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 8)
e)
  show (XWord16 SymExpr sym (BaseBVType 16)
e)  = Name
"XWord16 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 16)
e)
  show (XWord32 SymExpr sym (BaseBVType 32)
e)  = Name
"XWord32 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 32)
e)
  show (XWord64 SymExpr sym (BaseBVType 64)
e)  = Name
"XWord64 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 64)
e)
  show (XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e)   = Name
"XFloat " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e)
  show (XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e)  = Name
"XDouble " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Name
show (forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e)
  show XExpr sym
XEmptyArray  = Name
"[]"
  show (XArray Vector n (XExpr sym)
vs)  = forall a. Show a => [a] -> ShowS
showList (forall (n :: Natural) a. Vector n a -> [a]
V.toList Vector n (XExpr sym)
vs) Name
""
  show (XStruct [XExpr sym]
xs) = Name
"XStruct " forall a. [a] -> [a] -> [a]
++ forall a. Show a => [a] -> ShowS
showList [XExpr sym]
xs Name
""

-- * Stream offsets

-- | Streams expressions are evaluated in two possible modes. The \"absolute\"
-- mode computes the value of a stream expression relative to the beginning of
-- time @t=0@.  The \"relative\" mode is useful for inductive proofs and the
-- offset values are conceptually relative to some arbitrary, but fixed, index
-- @j>=0@. In both cases, negative indexes are not allowed.
--
-- The main difference between these modes is the interpretation of streams for
-- the first values, which are in the \"buffer\" range.  For absolute indices,
-- the actual fixed values for the streams are returned; for relative indices,
-- uninterpreted values are generated for the values in the stream buffer. For
-- both modes, stream values after their buffer region are defined by their
-- recurrence expression.
data StreamOffset
  = AbsoluteOffset !Integer
  | RelativeOffset !Integer
 deriving (StreamOffset -> StreamOffset -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StreamOffset -> StreamOffset -> Bool
$c/= :: StreamOffset -> StreamOffset -> Bool
== :: StreamOffset -> StreamOffset -> Bool
$c== :: StreamOffset -> StreamOffset -> Bool
Eq, Eq StreamOffset
StreamOffset -> StreamOffset -> Bool
StreamOffset -> StreamOffset -> Ordering
StreamOffset -> StreamOffset -> StreamOffset
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: StreamOffset -> StreamOffset -> StreamOffset
$cmin :: StreamOffset -> StreamOffset -> StreamOffset
max :: StreamOffset -> StreamOffset -> StreamOffset
$cmax :: StreamOffset -> StreamOffset -> StreamOffset
>= :: StreamOffset -> StreamOffset -> Bool
$c>= :: StreamOffset -> StreamOffset -> Bool
> :: StreamOffset -> StreamOffset -> Bool
$c> :: StreamOffset -> StreamOffset -> Bool
<= :: StreamOffset -> StreamOffset -> Bool
$c<= :: StreamOffset -> StreamOffset -> Bool
< :: StreamOffset -> StreamOffset -> Bool
$c< :: StreamOffset -> StreamOffset -> Bool
compare :: StreamOffset -> StreamOffset -> Ordering
$ccompare :: StreamOffset -> StreamOffset -> Ordering
Ord, Id -> StreamOffset -> ShowS
[StreamOffset] -> ShowS
StreamOffset -> Name
forall a.
(Id -> a -> ShowS) -> (a -> Name) -> ([a] -> ShowS) -> Show a
showList :: [StreamOffset] -> ShowS
$cshowList :: [StreamOffset] -> ShowS
show :: StreamOffset -> Name
$cshow :: StreamOffset -> Name
showsPrec :: Id -> StreamOffset -> ShowS
$cshowsPrec :: Id -> StreamOffset -> ShowS
Show)

-- | Increment a stream offset by a drop amount.
addOffset :: StreamOffset -> CE.DropIdx -> StreamOffset
addOffset :: StreamOffset -> DropIdx -> StreamOffset
addOffset (AbsoluteOffset Integer
i) DropIdx
j = Integer -> StreamOffset
AbsoluteOffset (Integer
i forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger DropIdx
j)
addOffset (RelativeOffset Integer
i) DropIdx
j = Integer -> StreamOffset
RelativeOffset (Integer
i forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> Integer
toInteger DropIdx
j)

-- * Auxiliary definitions

-- | We assume round-near-even throughout, but this variable can be changed if
-- needed.
fpRM :: WI.RoundingMode
fpRM :: RoundingMode
fpRM = RoundingMode
WI.RNE

data CopilotWhat4 = CopilotWhat4

instance Panic.PanicComponent CopilotWhat4 where
  panicComponentName :: CopilotWhat4 -> Name
panicComponentName CopilotWhat4
_ = Name
"Copilot/What4 translation"
  panicComponentIssues :: CopilotWhat4 -> Name
panicComponentIssues CopilotWhat4
_ = Name
"https://github.com/Copilot-Language/copilot/issues"

  {-# NOINLINE Panic.panicComponentRevision #-}
  panicComponentRevision :: CopilotWhat4 -> (Name, Name)
panicComponentRevision = $(Panic.useGitRevision)

-- | Use this function rather than an error monad since it indicates that
-- something in the implementation of @copilot-theorem@ is incorrect.
panic :: (Panic.HasCallStack, MonadIO m) => [String] -> m a
panic :: forall (m :: * -> *) a. (HasCallStack, MonadIO m) => [Name] -> m a
panic [Name]
msg = forall a b.
(PanicComponent a, HasCallStack) =>
a -> Name -> [Name] -> b
Panic.panic CopilotWhat4
CopilotWhat4 Name
"Copilot.Theorem.What4" [Name]
msg