diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,10 @@ +2022-11-07 + * Version bump (3.12). (#389) + * Add functionality for bisimulation proofs of Copilot specifications. (#363) + * Use pretty-printer from copilot-prettyprinter. (#383) + * Replace uses of Copilot.Core.Type.Equality with definitions from + base:Data.Type.Equality. (#379) + 2022-09-07 * Version bump (3.11). (#376) diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal --- a/copilot-theorem.cabal +++ b/copilot-theorem.cabal @@ -14,7 +14,7 @@ . -version : 3.11 +version : 3.12 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -45,25 +45,26 @@ -fno-warn-missing-signatures -fcontext-stack=100 - build-depends : base >= 4.9 && < 5 - , bimap (>= 0.3 && < 0.4) || (>= 0.5 && < 0.6) - , bv-sized >= 1.0.2 && < 1.1 - , containers >= 0.4 && < 0.7 - , data-default >= 0.7 && < 0.8 - , directory >= 1.3 && < 1.4 - , libBF >= 0.6.2 && < 0.7 - , mtl >= 2.0 && < 2.4 - , panic >= 0.4.0 && < 0.5 - , parsec >= 2.0 && < 3.2 - , parameterized-utils >= 2.1.1 && < 2.2 - , pretty >= 1.0 && < 1.2 - , process >= 1.6 && < 1.7 - , random >= 1.1 && < 1.3 - , transformers >= 0.5 && < 0.7 - , xml >= 1.3 && < 1.4 - , what4 >= 1.1 && < 1.4 + build-depends : base >= 4.9 && < 5 + , bimap (>= 0.3 && < 0.4) || (>= 0.5 && < 0.6) + , bv-sized >= 1.0.2 && < 1.1 + , containers >= 0.4 && < 0.7 + , data-default >= 0.7 && < 0.8 + , directory >= 1.3 && < 1.4 + , libBF >= 0.6.2 && < 0.7 + , mtl >= 2.0 && < 2.4 + , panic >= 0.4.0 && < 0.5 + , parsec >= 2.0 && < 3.2 + , parameterized-utils >= 2.1.1 && < 2.2 + , pretty >= 1.0 && < 1.2 + , process >= 1.6 && < 1.7 + , random >= 1.1 && < 1.3 + , transformers >= 0.5 && < 0.7 + , xml >= 1.3 && < 1.4 + , what4 >= 1.3 && < 1.4 - , copilot-core >= 3.11 && < 3.12 + , copilot-core >= 3.12 && < 3.13 + , copilot-prettyprinter >= 3.12 && < 3.13 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove @@ -106,3 +107,4 @@ , Copilot.Theorem.TransSys.Operators , Copilot.Theorem.TransSys.Type + , Copilot.Theorem.What4.Translate diff --git a/src/Copilot/Theorem/TransSys/Type.hs b/src/Copilot/Theorem/TransSys/Type.hs --- a/src/Copilot/Theorem/TransSys/Type.hs +++ b/src/Copilot/Theorem/TransSys/Type.hs @@ -8,7 +8,7 @@ , U (..) ) where -import Copilot.Core.Type.Equality +import Data.Type.Equality -- | A type at both value and type level. -- @@ -19,11 +19,11 @@ Real :: Type Double -- | Proofs of type equality. -instance EqualType Type where - Bool =~= Bool = Just Refl - Integer =~= Integer = Just Refl - Real =~= Real = Just Refl - _ =~= _ = Nothing +instance TestEquality Type where + testEquality Bool Bool = Just Refl + testEquality Integer Integer = Just Refl + testEquality Real Real = Just Refl + testEquality _ _ = Nothing -- | Unknown types. -- diff --git a/src/Copilot/Theorem/What4.hs b/src/Copilot/Theorem/What4.hs --- a/src/Copilot/Theorem/What4.hs +++ b/src/Copilot/Theorem/What4.hs @@ -26,929 +26,421 @@ -- @What4@. A backend solver is then used to prove the property is true. The -- technique is sound, but incomplete. If a property is proved true by this -- technique, then it can be guaranteed to be true. However, if a property is --- not proved true, that does not mean it isn't true. Very simple specifications --- are unprovable by this technique, including: --- --- @ --- a = True : a --- @ --- --- The above specification will not be proved true. The reason is that this --- technique does not perform any sort of induction. When proving the inner @a@ --- expression, the technique merely allocates a fresh constant standing for --- "@a@, one timestep in the past." Nothing is asserted about the fresh --- constant. --- --- An example of a property that is provable by this approach is: --- --- @ --- a = True : b --- b = not a --- --- -- Property: a || b --- @ --- --- By allocating a fresh constant, @b_-1@, standing for "the value of @b@ one --- timestep in the past", the equation for @a || b@ at some arbitrary point in --- the future reduces to @b_-1 || not b_-1@, which is always true. --- --- In addition to proving that the stream expression is true at some arbitrary --- point in the future, we also prove it for the first @k@ timesteps, where @k@ --- is the maximum buffer length of all streams in the given spec. This amounts --- to simply interpreting the spec, although external variables are still --- represented as constants with unknown values. - -module Copilot.Theorem.What4 - ( prove, Solver(..), SatResult(..) - ) where - -import qualified Copilot.Core.Expr as CE -import qualified Copilot.Core.Operators as CE -import qualified Copilot.Core.Spec as CS -import qualified Copilot.Core.Type as CT -import qualified Copilot.Core.Type.Array as CT - -import qualified What4.Config as WC -import qualified What4.Expr.Builder as WB -import qualified What4.Expr.GroundEval as WG -import qualified What4.Interface as WI -import qualified What4.BaseTypes as WT -import qualified What4.Solver as WS -import qualified What4.Solver.DReal as WS - -import qualified Control.Monad.Fail as Fail -import Control.Monad.State -import qualified Data.BitVector.Sized as BV -import Data.Foldable (foldrM) -import Data.List (elemIndex) -import Data.Maybe (fromJust) -import qualified Data.Map as Map -import Data.Parameterized.Classes -import Data.Parameterized.Context hiding (zipWithM) -import Data.Parameterized.NatRepr -import Data.Parameterized.Nonce -import Data.Parameterized.Some -import Data.Parameterized.SymbolRepr -import qualified Data.Parameterized.Vector as V -import Data.Word -import LibBF ( bfToDouble - , bfFromDouble - , bfPosZero - , pattern NearEven ) -import GHC.TypeNats (KnownNat) -import qualified Panic as Panic - --- 'prove' function --- --- To prove properties of a spec, we translate them into What4 using the TransM --- monad (transformer on top of IO), then negate each property and ask a backend --- solver to produce a model for the negation. - --- | We assume round-near-even throughout, but this variable can be changed if --- needed. -fpRM :: WI.RoundingMode -fpRM = WI.RNE - --- | No builder state needed. -data BuilderState a = EmptyState - --- | The solvers supported by the what4 backend. -data Solver = CVC4 | DReal | Yices | Z3 - --- | The 'prove' function returns results of this form for each property in a --- spec. -data SatResult = Valid | Invalid | Unknown - deriving Show - -type CounterExample = [(String, Some CopilotValue)] - --- | Attempt to prove all of the properties in a spec via an SMT solver (which --- must be installed locally on the host). Return an association list mapping --- the names of each property to the result returned by the solver. -prove :: Solver - -- ^ Solver to use - -> CS.Spec - -- ^ Spec - -> IO [(CE.Name, SatResult)] -prove solver spec = do - -- Setup symbolic backend - Some ng <- newIONonceGenerator - sym <- WB.newExprBuilder WB.FloatIEEERepr EmptyState ng - - -- Solver-specific options - case solver of - CVC4 -> WC.extendConfig WS.cvc4Options (WI.getConfiguration sym) - DReal -> WC.extendConfig WS.drealOptions (WI.getConfiguration sym) - Yices -> WC.extendConfig WS.yicesOptions (WI.getConfiguration sym) - Z3 -> WC.extendConfig WS.z3Options (WI.getConfiguration sym) - - -- Build up initial translation state - let streamMap = Map.fromList $ - (\stream -> (CS.streamId stream, stream)) <$> CS.specStreams spec - pow <- WI.freshTotalUninterpFn sym (WI.safeSymbol "pow") knownRepr knownRepr - logb <- WI.freshTotalUninterpFn sym (WI.safeSymbol "logb") knownRepr knownRepr - let st = TransState Map.empty Map.empty Map.empty streamMap pow logb - - -- Define TransM action for proving properties. Doing this in TransM rather - -- than IO allows us to reuse the state for each property. - let proveProperties = forM (CS.specProperties spec) $ \pr -> do - let bufLen (CS.Stream _ buf _ _) = length buf - maxBufLen = maximum (0 : (bufLen <$> CS.specStreams spec)) - prefix <- forM [0 .. maxBufLen - 1] $ \k -> do - XBool p <- translateExprAt sym k (CS.propertyExpr pr) - return p - XBool p <- translateExpr sym 0 (CS.propertyExpr pr) - p_and_prefix <- liftIO $ foldrM (WI.andPred sym) p prefix - not_p_and_prefix <- liftIO $ WI.notPred sym p_and_prefix - - let clauses = [not_p_and_prefix] - case solver of - CVC4 -> liftIO $ WS.runCVC4InOverride sym WS.defaultLogData clauses $ \case - WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid) - WS.Unsat _ -> return (CS.propertyName pr, Valid) - WS.Unknown -> return (CS.propertyName pr, Unknown) - DReal -> liftIO $ WS.runDRealInOverride sym WS.defaultLogData clauses $ \case - WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid) - WS.Unsat _ -> return (CS.propertyName pr, Valid) - WS.Unknown -> return (CS.propertyName pr, Unknown) - Yices -> liftIO $ WS.runYicesInOverride sym WS.defaultLogData clauses $ \case - WS.Sat _ge -> return (CS.propertyName pr, Invalid) - WS.Unsat _ -> return (CS.propertyName pr, Valid) - WS.Unknown -> return (CS.propertyName pr, Unknown) - Z3 -> liftIO $ WS.runZ3InOverride sym WS.defaultLogData clauses $ \case - WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid) - WS.Unsat _ -> return (CS.propertyName pr, Valid) - WS.Unknown -> return (CS.propertyName pr, Unknown) - - -- Execute the action and return the results for each property - (res, _) <- runStateT (unTransM proveProperties) st - return res - --- What4 translation - --- | the state for translating Copilot expressions into What4 expressions. As we --- translate, we generate fresh symbolic constants for external variables and --- for stream variables. We need to only generate one constant per variable, so --- we allocate them in a map. When we need the constant for a particular --- variable, we check if it is already in the map, and return it if it is; if it --- isn't, we generate a fresh constant at that point, store it in the map, and --- return it. --- --- We also store three immutable fields in this state, rather than wrap them up --- in another monad transformer layer. These are initialized prior to --- translation and are never modified. They are the map from stream ids to the --- core stream definitions, a symbolic uninterpreted function for "pow", and a --- symbolic uninterpreted function for "logb". -data TransState t = TransState { - -- | Map of all external variables we encounter during translation. These are - -- just fresh constants. The offset indicates how many timesteps in the past - -- this constant represents for that stream. - externVars :: Map.Map (CE.Name, Int) (XExpr t), - -- | Map of external variables at specific indices (positive), rather than - -- offset into the past. This is for interpreting streams at specific offsets. - externVarsAt :: Map.Map (CE.Name, Int) (XExpr t), - -- | Map from (stream id, negative offset) to fresh constant. These are all - -- constants representing the values of a stream at some point in the past. - -- The offset (ALWAYS NEGATIVE) indicates how many timesteps in the past - -- this constant represents for that stream. - streamConstants :: Map.Map (CE.Id, Int) (XExpr t), - -- | Map from stream ids to the streams themselves. This value is never - -- modified, but I didn't want to make this an RWS, so it's represented as a - -- stateful value. - streams :: Map.Map CE.Id CS.Stream, - -- | Binary power operator, represented as an uninterpreted function. - pow :: WB.ExprSymFn t - (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) - WT.BaseRealType, - -- | Binary logarithm operator, represented as an uninterpreted function. - logb :: WB.ExprSymFn t - (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) - WT.BaseRealType - } - -newtype TransM t a = TransM { unTransM :: StateT (TransState t) IO a } - deriving ( Functor - , Applicative - , Monad - , MonadIO - , MonadState (TransState t) - ) - -instance Fail.MonadFail (TransM t) where - fail = error - -data CopilotWhat4 = CopilotWhat4 - -instance Panic.PanicComponent CopilotWhat4 where - panicComponentName _ = "Copilot/What4 translation" - panicComponentIssues _ = "https://github.com/Copilot-Language/copilot/issues" - - {-# NOINLINE Panic.panicComponentRevision #-} - panicComponentRevision = $(Panic.useGitRevision) - --- | Use this function rather than an error monad since it indicates that --- copilot-core's "reify" function did something incorrectly. -panic :: MonadIO m => m a -panic = Panic.panic CopilotWhat4 "Copilot.Theorem.What4" - [ "Ill-typed core expression" ] - --- | The What4 representation of a copilot expression. We do not attempt to --- track the type of the inner expression at the type level, but instead lump --- everything together into the 'XExpr t' type. The only reason this is a GADT --- is for the array case; we need to know that the array length is strictly --- positive. -data XExpr t where - XBool :: WB.Expr t WT.BaseBoolType -> XExpr t - XInt8 :: WB.Expr t (WT.BaseBVType 8) -> XExpr t - XInt16 :: WB.Expr t (WT.BaseBVType 16) -> XExpr t - XInt32 :: WB.Expr t (WT.BaseBVType 32) -> XExpr t - XInt64 :: WB.Expr t (WT.BaseBVType 64) -> XExpr t - XWord8 :: WB.Expr t (WT.BaseBVType 8) -> XExpr t - XWord16 :: WB.Expr t (WT.BaseBVType 16) -> XExpr t - XWord32 :: WB.Expr t (WT.BaseBVType 32) -> XExpr t - XWord64 :: WB.Expr t (WT.BaseBVType 64) -> XExpr t - XFloat :: WB.Expr t (WT.BaseFloatType WT.Prec32) -> XExpr t - XDouble :: WB.Expr t (WT.BaseFloatType WT.Prec64) -> XExpr t - XEmptyArray :: XExpr t - XArray :: 1 <= n => V.Vector n (XExpr t) -> XExpr t - XStruct :: [XExpr t] -> XExpr t - -- XArray :: NatRepr n - -- -> BaseTypeRepr tp - -- -> Some (WB.Expr t) - -- XStruct :: Assignment BaseTypeRepr tps - -- -> WB.Expr t (BaseStructType tps) - -- -> XExpr t - -deriving instance Show (XExpr t) - -data CopilotValue a = CopilotValue { cvType :: CT.Type a - , cvVal :: a - } - -valFromExpr :: WG.GroundEvalFn t -> XExpr t -> IO (Some CopilotValue) -valFromExpr ge xe = case xe of - XBool e -> Some . CopilotValue CT.Bool <$> WG.groundEval ge e - XInt8 e -> Some . CopilotValue CT.Int8 . fromBV <$> WG.groundEval ge e - XInt16 e -> Some . CopilotValue CT.Int16 . fromBV <$> WG.groundEval ge e - XInt32 e -> Some . CopilotValue CT.Int32 . fromBV <$> WG.groundEval ge e - XInt64 e -> Some . CopilotValue CT.Int64 . fromBV <$> WG.groundEval ge e - XWord8 e -> Some . CopilotValue CT.Word8 . fromBV <$> WG.groundEval ge e - XWord16 e -> Some . CopilotValue CT.Word16 . fromBV <$> WG.groundEval ge e - XWord32 e -> Some . CopilotValue CT.Word32 . fromBV <$> WG.groundEval ge e - XWord64 e -> Some . CopilotValue CT.Word64 . fromBV <$> WG.groundEval ge e - XFloat e -> - Some . CopilotValue CT.Float . realToFrac . fst . bfToDouble NearEven <$> WG.groundEval ge e - XDouble e -> - Some . CopilotValue CT.Double . fst . bfToDouble NearEven <$> WG.groundEval ge e - _ -> error "valFromExpr unhandled case" - where - fromBV :: forall a w . Num a => BV.BV w -> a - fromBV = fromInteger . BV.asUnsigned - --- | A view of an XExpr as a bitvector expression, a natrepr for its width, its --- signed/unsigned status, and the constructor used to reconstruct an XExpr from --- it. This is a useful view for translation, as many of the operations can be --- grouped together for all words\/ints\/floats. -data SomeBVExpr t where - SomeBVExpr :: 1 <= w - => WB.BVExpr t w - -> NatRepr w - -> BVSign - -> (WB.BVExpr t w -> XExpr t) - -> SomeBVExpr t - --- | The sign of a bitvector -- this indicates whether it is to be interpreted --- as a signed 'Int' or an unsigned 'Word'. -data BVSign = Signed | Unsigned - --- | If the inner expression can be viewed as a bitvector, we project out a view --- of it as such. -asBVExpr :: XExpr t -> Maybe (SomeBVExpr t) -asBVExpr xe = case xe of - XInt8 e -> Just (SomeBVExpr e knownNat Signed XInt8) - XInt16 e -> Just (SomeBVExpr e knownNat Signed XInt16) - XInt32 e -> Just (SomeBVExpr e knownNat Signed XInt32) - XInt64 e -> Just (SomeBVExpr e knownNat Signed XInt64) - XWord8 e -> Just (SomeBVExpr e knownNat Unsigned XWord8) - XWord16 e -> Just (SomeBVExpr e knownNat Unsigned XWord16) - XWord32 e -> Just (SomeBVExpr e knownNat Unsigned XWord32) - XWord64 e -> Just (SomeBVExpr e knownNat Unsigned XWord64) - _ -> Nothing - --- | Translate a constant expression by creating a what4 literal and packaging --- it up into an 'XExpr'. -translateConstExpr :: forall a t st fs . - WB.ExprBuilder t st fs - -> CT.Type a - -> a - -> IO (XExpr t) -translateConstExpr sym tp a = case tp of - CT.Bool -> case a of - True -> return $ XBool (WI.truePred sym) - False -> return $ XBool (WI.falsePred sym) - CT.Int8 -> XInt8 <$> WI.bvLit sym knownNat (BV.int8 a) - CT.Int16 -> XInt16 <$> WI.bvLit sym knownNat (BV.int16 a) - CT.Int32 -> XInt32 <$> WI.bvLit sym knownNat (BV.int32 a) - CT.Int64 -> XInt64 <$> WI.bvLit sym knownNat (BV.int64 a) - CT.Word8 -> XWord8 <$> WI.bvLit sym knownNat (BV.word8 a) - CT.Word16 -> XWord16 <$> WI.bvLit sym knownNat (BV.word16 a) - CT.Word32 -> XWord32 <$> WI.bvLit sym knownNat (BV.word32 a) - CT.Word64 -> XWord64 <$> WI.bvLit sym knownNat (BV.word64 a) - CT.Float -> XFloat <$> WI.floatLit sym knownRepr (bfFromDouble (realToFrac a)) - CT.Double -> XDouble <$> WI.floatLit sym knownRepr (bfFromDouble a) - CT.Array tp -> do - elts <- traverse (translateConstExpr sym tp) (CT.arrayelems a) - Just (Some n) <- return $ someNat (length elts) - case isZeroOrGT1 n of - Left Refl -> return XEmptyArray - Right LeqProof -> do - let Just v = V.fromList n elts - return $ XArray v - CT.Struct _ -> do - elts <- forM (CT.toValues a) $ \(CT.Value tp (CT.Field a)) -> - translateConstExpr sym tp a - return $ XStruct elts - -arrayLen :: KnownNat n => CT.Type (CT.Array n t) -> NatRepr n -arrayLen _ = knownNat - --- | Generate a fresh constant for a given copilot type. This will be called --- whenever we attempt to get the constant for a given external variable or --- stream variable, but that variable has not been accessed yet and therefore --- has no constant allocated. -freshCPConstant :: forall t st fs a . - WB.ExprBuilder t st fs - -> String - -> CT.Type a - -> IO (XExpr t) -freshCPConstant sym nm tp = case tp of - CT.Bool -> XBool <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - CT.Int8 -> XInt8 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - CT.Int16 -> XInt16 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - CT.Int32 -> XInt32 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - CT.Int64 -> XInt64 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - CT.Word8 -> XWord8 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - CT.Word16 -> XWord16 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - CT.Word32 -> XWord32 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - CT.Word64 -> XWord64 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - CT.Float -> XFloat <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - CT.Double -> XDouble <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr - atp@(CT.Array itp) -> do - n <- return $ arrayLen atp - case isZeroOrGT1 n of - Left Refl -> return XEmptyArray - Right LeqProof -> do - Refl <- return $ minusPlusCancel n (knownNat @1) - elts :: V.Vector n (XExpr t) <- V.generateM (decNat n) (const (freshCPConstant sym "" itp)) - return $ XArray elts - CT.Struct stp -> do - elts <- forM (CT.toValues stp) $ \(CT.Value ftp _) -> freshCPConstant sym "" ftp - return $ XStruct elts - --- | Get the constant for a given stream id and some offset into the past. This --- should only be called with a strictly negative offset. When this function --- gets called for the first time for a given (streamId, offset) pair, it --- generates a fresh constant and stores it in an internal map. Thereafter, this --- function will just return that constant when called with the same pair. -getStreamConstant :: WB.ExprBuilder t st fs -> CE.Id -> Int -> TransM t (XExpr t) -getStreamConstant sym streamId offset = do - scs <- gets streamConstants - case Map.lookup (streamId, offset) scs of - Just xe -> return xe - Nothing -> do - CS.Stream _ _ _ tp <- getStreamDef streamId - let nm = show streamId ++ "_" ++ show offset - xe <- liftIO $ freshCPConstant sym nm tp - modify (\st -> st { streamConstants = Map.insert (streamId, offset) xe scs }) - return xe - --- | Get the constant for a given external variable and some offset into the --- past. This should only be called with a strictly negative offset. When this --- function gets called for the first time for a given (var, offset) pair, it --- generates a fresh constant and stores it in an internal map. Thereafter, this --- function will just return that constant when called with the same pair. -getExternConstant :: WB.ExprBuilder t st fs - -> CT.Type a - -> CE.Name - -> Int - -> TransM t (XExpr t) -getExternConstant sym tp var offset = do - es <- gets externVars - case Map.lookup (var, offset) es of - Just xe -> return xe - Nothing -> do - xe <- liftIO $ freshCPConstant sym var tp - modify (\st -> st { externVars = Map.insert (var, offset) xe es} ) - return xe - --- | Get the constant for a given external variable at some specific timestep. -getExternConstantAt :: WB.ExprBuilder t st fs - -> CT.Type a - -> CE.Name - -> Int - -> TransM t (XExpr t) -getExternConstantAt sym tp var ix = do - es <- gets externVarsAt - case Map.lookup (var, ix) es of - Just xe -> return xe - Nothing -> do - xe <- liftIO $ freshCPConstant sym var tp - modify (\st -> st { externVarsAt = Map.insert (var, ix) xe es} ) - return xe - --- | Retrieve a stream definition given its id. -getStreamDef :: CE.Id -> TransM t CS.Stream -getStreamDef streamId = fromJust <$> gets (Map.lookup streamId . streams) - --- | Translate an expression into a what4 representation. The int offset keeps --- track of how many timesteps into the past each variable is referring to. --- Initially the value should be zero, but when we translate a stream, the --- offset is recomputed based on the length of that stream's prefix (subtracted) --- and the drop index (added). -translateExpr :: WB.ExprBuilder t st fs - -> Int - -- ^ number of timesteps in the past we are currently looking - -- (must always be <= 0) - -> CE.Expr a - -> TransM t (XExpr t) -translateExpr sym offset e = case e of - CE.Const tp a -> liftIO $ translateConstExpr sym tp a - CE.Drop _tp ix streamId - -- If we are referencing a past value of this stream, just return an - -- unconstrained constant. - | offset + fromIntegral ix < 0 -> - getStreamConstant sym streamId (offset + fromIntegral ix) - -- If we are referencing a current or future value of this stream, we need - -- to translate the stream's expression, using an offset computed based on - -- the current offset (negative or 0), the drop index (positive or 0), and - -- the length of the stream's buffer (subtracted). - | otherwise -> do - CS.Stream _ buf e _ <- getStreamDef streamId - translateExpr sym (offset + fromIntegral ix - length buf) e - CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented" - CE.Var _ _ -> error "translateExpr: Var unimplemented" - CE.ExternVar tp nm _prefix -> getExternConstant sym tp nm offset - CE.Op1 op e -> liftIO . translateOp1 sym op =<< translateExpr sym offset e - CE.Op2 op e1 e2 -> do - xe1 <- translateExpr sym offset e1 - xe2 <- translateExpr sym offset e2 - powFn <- gets pow - logbFn <- gets logb - liftIO $ translateOp2 sym powFn logbFn op xe1 xe2 - CE.Op3 op e1 e2 e3 -> do - xe1 <- translateExpr sym offset e1 - xe2 <- translateExpr sym offset e2 - xe3 <- translateExpr sym offset e3 - liftIO $ translateOp3 sym op xe1 xe2 xe3 - CE.Label _ _ _ -> error "translateExpr: Label unimplemented" - --- | Translate an expression into a what4 representation at a /specific/ --- timestep, rather than "at some indeterminate point in the future." -translateExprAt :: WB.ExprBuilder t st fs - -> Int - -- ^ Index of timestep - -> CE.Expr a - -- ^ stream expression - -> TransM t (XExpr t) -translateExprAt sym k e = do - case e of - CE.Const tp a -> liftIO $ translateConstExpr sym tp a - CE.Drop _tp ix streamId -> do - CS.Stream _ buf e tp <- getStreamDef streamId - if k' < length buf - then liftIO $ translateConstExpr sym tp (buf !! k') - else translateExprAt sym (k' - length buf) e - where - k' = k + fromIntegral ix - CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented" - CE.Var _ _ -> error "translateExpr: Var unimplemented" - CE.ExternVar tp nm _prefix -> getExternConstantAt sym tp nm k - CE.Op1 op e -> liftIO . translateOp1 sym op =<< translateExprAt sym k e - CE.Op2 op e1 e2 -> do - xe1 <- translateExprAt sym k e1 - xe2 <- translateExprAt sym k e2 - powFn <- gets pow - logbFn <- gets logb - liftIO $ translateOp2 sym powFn logbFn op xe1 xe2 - CE.Op3 op e1 e2 e3 -> do - xe1 <- translateExprAt sym k e1 - xe2 <- translateExprAt sym k e2 - xe3 <- translateExprAt sym k e3 - liftIO $ translateOp3 sym op xe1 xe2 xe3 - CE.Label _ _ _ -> error "translateExpr: Label unimplemented" - -type BVOp1 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> IO (WB.BVExpr t w) - -type FPOp1 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp)) - -type RealOp1 t = WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType) - -fieldName :: KnownSymbol s => CT.Field s a -> SymbolRepr s -fieldName _ = knownSymbol - -valueName :: CT.Value a -> Some SymbolRepr -valueName (CT.Value _ f) = Some (fieldName f) - -translateOp1 :: forall t st fs a b . - WB.ExprBuilder t st fs - -> CE.Op1 a b - -> XExpr t - -> IO (XExpr t) -translateOp1 sym op xe = case (op, xe) of - (CE.Not, XBool e) -> XBool <$> WI.notPred sym e - (CE.Not, _) -> panic - (CE.Abs _, xe) -> numOp bvAbs fpAbs xe - where - bvAbs :: BVOp1 w t - bvAbs e = do zero <- WI.bvLit sym knownNat (BV.zero knownNat) - e_neg <- WI.bvSlt sym e zero - neg_e <- WI.bvSub sym zero e - WI.bvIte sym e_neg neg_e e - fpAbs :: FPOp1 fpp t - fpAbs e = do zero <- WI.floatLit sym knownRepr bfPosZero - e_neg <- WI.floatLt sym e zero - neg_e <- WI.floatSub sym fpRM zero e - WI.floatIte sym e_neg neg_e e - (CE.Sign _, xe) -> numOp bvSign fpSign xe - where - bvSign :: BVOp1 w t - bvSign e = do zero <- WI.bvLit sym knownRepr (BV.zero knownNat) - neg_one <- WI.bvLit sym knownNat (BV.mkBV knownNat (-1)) - pos_one <- WI.bvLit sym knownNat (BV.mkBV knownNat 1) - e_zero <- WI.bvEq sym e zero - e_neg <- WI.bvSlt sym e zero - t <- WI.bvIte sym e_neg neg_one pos_one - WI.bvIte sym e_zero zero t - fpSign :: FPOp1 fpp t - fpSign e = do zero <- WI.floatLit sym knownRepr bfPosZero - neg_one <- WI.floatLit sym knownRepr (bfFromDouble (-1.0)) - pos_one <- WI.floatLit sym knownRepr (bfFromDouble 1.0) - e_zero <- WI.floatEq sym e zero - e_neg <- WI.floatLt sym e zero - t <- WI.floatIte sym e_neg neg_one pos_one - WI.floatIte sym e_zero zero t - (CE.Recip _, xe) -> fpOp recip xe - where - recip :: FPOp1 fpp t - recip e = do one <- WI.floatLit sym knownRepr (bfFromDouble 1.0) - WI.floatDiv sym fpRM one e - (CE.Exp _, xe) -> realOp (WI.realExp sym) xe - (CE.Sqrt _, xe) -> fpOp (WI.floatSqrt sym fpRM) xe - (CE.Log _, xe) -> realOp (WI.realLog sym) xe - (CE.Sin _, xe) -> realOp (WI.realSin sym) xe - (CE.Cos _, xe) -> realOp (WI.realCos sym) xe - (CE.Tan _, xe) -> realOp (WI.realTan sym) xe - (CE.Asin _, xe) -> realOp (realRecip <=< WI.realSin sym) xe - (CE.Acos _, xe) -> realOp (realRecip <=< WI.realCos sym) xe - (CE.Atan _, xe) -> realOp (realRecip <=< WI.realTan sym) xe - (CE.Sinh _, xe) -> realOp (WI.realSinh sym) xe - (CE.Cosh _, xe) -> realOp (WI.realCosh sym) xe - (CE.Tanh _, xe) -> realOp (WI.realTanh sym) xe - (CE.Asinh _, xe) -> realOp (realRecip <=< WI.realSinh sym) xe - (CE.Acosh _, xe) -> realOp (realRecip <=< WI.realCosh sym) xe - (CE.Atanh _, xe) -> realOp (realRecip <=< WI.realTanh sym) xe - (CE.BwNot _, xe) -> case xe of - XBool e -> XBool <$> WI.notPred sym e - _ -> bvOp (WI.bvNotBits sym) xe - (CE.Cast _ tp, xe) -> case (xe, tp) of - (XBool e, CT.Bool) -> return $ XBool e - (XBool e, CT.Word8) -> XWord8 <$> WI.predToBV sym e knownNat - (XBool e, CT.Word16) -> XWord16 <$> WI.predToBV sym e knownNat - (XBool e, CT.Word32) -> XWord32 <$> WI.predToBV sym e knownNat - (XBool e, CT.Word64) -> XWord64 <$> WI.predToBV sym e knownNat - (XBool e, CT.Int8) -> XInt8 <$> WI.predToBV sym e knownNat - (XBool e, CT.Int16) -> XInt16 <$> WI.predToBV sym e knownNat - (XBool e, CT.Int32) -> XInt32 <$> WI.predToBV sym e knownNat - (XBool e, CT.Int64) -> XInt64 <$> WI.predToBV sym e knownNat - (XInt8 e, CT.Int8) -> return $ XInt8 e - (XInt8 e, CT.Int16) -> XInt16 <$> WI.bvSext sym knownNat e - (XInt8 e, CT.Int32) -> XInt32 <$> WI.bvSext sym knownNat e - (XInt8 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e - (XInt16 e, CT.Int16) -> return $ XInt16 e - (XInt16 e, CT.Int32) -> XInt32 <$> WI.bvSext sym knownNat e - (XInt16 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e - (XInt32 e, CT.Int32) -> return $ XInt32 e - (XInt32 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e - (XInt64 e, CT.Int64) -> return $ XInt64 e - (XWord8 e, CT.Int16) -> XInt16 <$> WI.bvZext sym knownNat e - (XWord8 e, CT.Int32) -> XInt32 <$> WI.bvZext sym knownNat e - (XWord8 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e - (XWord8 e, CT.Word8) -> return $ XWord8 e - (XWord8 e, CT.Word16) -> XWord16 <$> WI.bvZext sym knownNat e - (XWord8 e, CT.Word32) -> XWord32 <$> WI.bvZext sym knownNat e - (XWord8 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e - (XWord16 e, CT.Int32) -> XInt32 <$> WI.bvZext sym knownNat e - (XWord16 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e - (XWord16 e, CT.Word16) -> return $ XWord16 e - (XWord16 e, CT.Word32) -> XWord32 <$> WI.bvZext sym knownNat e - (XWord16 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e - (XWord32 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e - (XWord32 e, CT.Word32) -> return $ XWord32 e - (XWord32 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e - (XWord64 e, CT.Word64) -> return $ XWord64 e - _ -> panic - (CE.GetField (CT.Struct s) _ftp extractor, XStruct xes) -> do - let fieldNameRepr = fieldName (extractor undefined) - let structFieldNameReprs = valueName <$> CT.toValues s - let mIx = elemIndex (Some fieldNameRepr) structFieldNameReprs - case mIx of - Just ix -> return $ xes !! ix - Nothing -> panic - _ -> panic - where - numOp :: (forall w . BVOp1 w t) - -> (forall fpp . FPOp1 fpp t) - -> XExpr t - -> IO (XExpr t) - numOp bvOp fpOp xe = case xe of - XInt8 e -> XInt8 <$> bvOp e - XInt16 e -> XInt16 <$> bvOp e - XInt32 e -> XInt32 <$> bvOp e - XInt64 e -> XInt64 <$> bvOp e - XWord8 e -> XWord8 <$> bvOp e - XWord16 e -> XWord16 <$> bvOp e - XWord32 e -> XWord32 <$> bvOp e - XWord64 e -> XWord64 <$> bvOp e - XFloat e -> XFloat <$> fpOp e - XDouble e -> XDouble <$> fpOp e - _ -> panic - - bvOp :: (forall w . BVOp1 w t) -> XExpr t -> IO (XExpr t) - bvOp f xe = case xe of - XInt8 e -> XInt8 <$> f e - XInt16 e -> XInt16 <$> f e - XInt32 e -> XInt32 <$> f e - XInt64 e -> XInt64 <$> f e - XWord8 e -> XWord8 <$> f e - XWord16 e -> XWord16 <$> f e - XWord32 e -> XWord32 <$> f e - XWord64 e -> XWord64 <$> f e - _ -> panic - - fpOp :: (forall fpp . FPOp1 fpp t) -> XExpr t -> IO (XExpr t) - fpOp g xe = case xe of - XFloat e -> XFloat <$> g e - XDouble e -> XDouble <$> g e - _ -> panic - - realOp :: RealOp1 t -> XExpr t -> IO (XExpr t) - realOp h xe = fpOp hf xe - where - hf :: (forall fpp . FPOp1 fpp t) - hf e = do re <- WI.floatToReal sym e - hre <- h re - WI.realToFloat sym knownRepr fpRM hre - - realRecip :: RealOp1 t - realRecip e = do one <- WI.realLit sym 1 - WI.realDiv sym one e - -type BVOp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BVExpr t w) - -type FPOp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp)) - -type RealOp2 t = WB.Expr t WT.BaseRealType -> WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType) - -type BoolCmp2 t = WB.BoolExpr t -> WB.BoolExpr t -> IO (WB.BoolExpr t) - -type BVCmp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BoolExpr t) - -type FPCmp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.BoolExpr t) - -translateOp2 :: forall t st fs a b c . - WB.ExprBuilder t st fs - -> (WB.ExprSymFn t - (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) - WT.BaseRealType) - -- ^ Pow function - -> (WB.ExprSymFn t - (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) - WT.BaseRealType) - -- ^ Logb function - -> CE.Op2 a b c - -> XExpr t - -> XExpr t - -> IO (XExpr t) -translateOp2 sym powFn logbFn op xe1 xe2 = case (op, xe1, xe2) of - (CE.And, XBool e1, XBool e2) -> XBool <$> WI.andPred sym e1 e2 - (CE.Or, XBool e1, XBool e2) -> XBool <$> WI.orPred sym e1 e2 - (CE.Add _, xe1, xe2) -> numOp (WI.bvAdd sym) (WI.floatAdd sym fpRM) xe1 xe2 - (CE.Sub _, xe1, xe2) -> numOp (WI.bvSub sym) (WI.floatSub sym fpRM) xe1 xe2 - (CE.Mul _, xe1, xe2) -> numOp (WI.bvMul sym) (WI.floatMul sym fpRM) xe1 xe2 - (CE.Mod _, xe1, xe2) -> bvOp (WI.bvSrem sym) (WI.bvUrem sym) xe1 xe2 - (CE.Div _, xe1, xe2) -> bvOp (WI.bvSdiv sym) (WI.bvUdiv sym) xe1 xe2 - (CE.Fdiv _, xe1, xe2) -> fpOp (WI.floatDiv sym fpRM) xe1 xe2 - (CE.Pow _, xe1, xe2) -> fpOp powFn' xe1 xe2 - where - powFn' :: FPOp2 fpp t - powFn' e1 e2 = do re1 <- WI.floatToReal sym e1 - re2 <- WI.floatToReal sym e2 - let args = (Empty :> re1 :> re2) - rpow <- WI.applySymFn sym powFn args - WI.realToFloat sym knownRepr fpRM rpow - (CE.Logb _, xe1, xe2) -> fpOp logbFn' xe1 xe2 - where - logbFn' :: FPOp2 fpp t - logbFn' e1 e2 = do re1 <- WI.floatToReal sym e1 - re2 <- WI.floatToReal sym e2 - let args = (Empty :> re1 :> re2) - rpow <- WI.applySymFn sym logbFn args - WI.realToFloat sym knownRepr fpRM rpow - (CE.Eq _, xe1, xe2) -> cmp (WI.eqPred sym) (WI.bvEq sym) (WI.floatEq sym) xe1 xe2 - (CE.Ne _, xe1, xe2) -> cmp neqPred bvNeq fpNeq xe1 xe2 - where - neqPred :: BoolCmp2 t - neqPred e1 e2 = do e <- WI.eqPred sym e1 e2 - WI.notPred sym e - bvNeq :: forall w . BVCmp2 w t - bvNeq e1 e2 = do e <- WI.bvEq sym e1 e2 - WI.notPred sym e - fpNeq :: forall fpp . FPCmp2 fpp t - fpNeq e1 e2 = do e <- WI.floatEq sym e1 e2 - WI.notPred sym e - (CE.Le _, xe1, xe2) -> numCmp (WI.bvSle sym) (WI.bvUle sym) (WI.floatLe sym) xe1 xe2 - (CE.Ge _, xe1, xe2) -> numCmp (WI.bvSge sym) (WI.bvUge sym) (WI.floatGe sym) xe1 xe2 - (CE.Lt _, xe1, xe2) -> numCmp (WI.bvSlt sym) (WI.bvUlt sym) (WI.floatLt sym) xe1 xe2 - (CE.Gt _, xe1, xe2) -> numCmp (WI.bvSgt sym) (WI.bvUgt sym) (WI.floatGt sym) xe1 xe2 - (CE.BwAnd _, xe1, xe2) -> bvOp (WI.bvAndBits sym) (WI.bvAndBits sym) xe1 xe2 - (CE.BwOr _, xe1, xe2) -> bvOp (WI.bvOrBits sym) (WI.bvOrBits sym) xe1 xe2 - (CE.BwXor _, xe1, xe2) -> bvOp (WI.bvXorBits sym) (WI.bvXorBits sym) xe1 xe2 - -- Note: For both shift operators, we are interpreting the shifter as an - -- unsigned bitvector regardless of whether it is a word or an int. - (CE.BwShiftL _ _, xe1, xe2) -> do - Just (SomeBVExpr e1 w1 _ ctor1) <- return $ asBVExpr xe1 - Just (SomeBVExpr e2 w2 _ _ ) <- return $ asBVExpr xe2 - e2' <- case testNatCases w1 w2 of - NatCaseLT LeqProof -> WI.bvTrunc sym w1 e2 - NatCaseEQ -> return e2 - NatCaseGT LeqProof -> WI.bvZext sym w1 e2 - ctor1 <$> WI.bvShl sym e1 e2' - (CE.BwShiftR _ _, xe1, xe2) -> do - Just (SomeBVExpr e1 w1 sgn1 ctor1) <- return $ asBVExpr xe1 - Just (SomeBVExpr e2 w2 _ _ ) <- return $ asBVExpr xe2 - e2' <- case testNatCases w1 w2 of - NatCaseLT LeqProof -> WI.bvTrunc sym w1 e2 - NatCaseEQ -> return e2 - NatCaseGT LeqProof -> WI.bvZext sym w1 e2 - ctor1 <$> case sgn1 of - Signed -> WI.bvAshr sym e1 e2' - Unsigned -> WI.bvLshr sym e1 e2' - -- Note: Currently, copilot does not check if array indices are out of bounds, - -- even for constant expressions. The method of translation we are using - -- simply creates a nest of if-then-else expression to check the index - -- expression against all possible indices. If the index expression is known - -- by the solver to be out of bounds (for instance, if it is a constant 5 for - -- an array of 5 elements), then the if-then-else will trivially resolve to - -- true. - (CE.Index _, xe1, xe2) -> do - case (xe1, xe2) of - (XArray xes, XWord32 ix) -> buildIndexExpr sym 0 ix xes - _ -> panic - _ -> panic - where - numOp :: (forall w . BVOp2 w t) - -> (forall fpp . FPOp2 fpp t) - -> XExpr t - -> XExpr t - -> IO (XExpr t) - numOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of - (XInt8 e1, XInt8 e2) -> XInt8 <$> bvOp e1 e2 - (XInt16 e1, XInt16 e2) -> XInt16 <$> bvOp e1 e2 - (XInt32 e1, XInt32 e2)-> XInt32 <$> bvOp e1 e2 - (XInt64 e1, XInt64 e2)-> XInt64 <$> bvOp e1 e2 - (XWord8 e1, XWord8 e2)-> XWord8 <$> bvOp e1 e2 - (XWord16 e1, XWord16 e2)-> XWord16 <$> bvOp e1 e2 - (XWord32 e1, XWord32 e2)-> XWord32 <$> bvOp e1 e2 - (XWord64 e1, XWord64 e2)-> XWord64 <$> bvOp e1 e2 - (XFloat e1, XFloat e2)-> XFloat <$> fpOp e1 e2 - (XDouble e1, XDouble e2)-> XDouble <$> fpOp e1 e2 - _ -> panic - - bvOp :: (forall w . BVOp2 w t) - -> (forall w . BVOp2 w t) - -> XExpr t - -> XExpr t - -> IO (XExpr t) - bvOp opS opU xe1 xe2 = case (xe1, xe2) of - (XInt8 e1, XInt8 e2) -> XInt8 <$> opS e1 e2 - (XInt16 e1, XInt16 e2) -> XInt16 <$> opS e1 e2 - (XInt32 e1, XInt32 e2) -> XInt32 <$> opS e1 e2 - (XInt64 e1, XInt64 e2) -> XInt64 <$> opS e1 e2 - (XWord8 e1, XWord8 e2) -> XWord8 <$> opU e1 e2 - (XWord16 e1, XWord16 e2) -> XWord16 <$> opU e1 e2 - (XWord32 e1, XWord32 e2) -> XWord32 <$> opU e1 e2 - (XWord64 e1, XWord64 e2) -> XWord64 <$> opU e1 e2 - _ -> panic - - fpOp :: (forall fpp . FPOp2 fpp t) - -> XExpr t - -> XExpr t - -> IO (XExpr t) - fpOp op xe1 xe2 = case (xe1, xe2) of - (XFloat e1, XFloat e2) -> XFloat <$> op e1 e2 - (XDouble e1, XDouble e2) -> XDouble <$> op e1 e2 - _ -> panic - - cmp :: BoolCmp2 t - -> (forall w . BVCmp2 w t) - -> (forall fpp . FPCmp2 fpp t) - -> XExpr t - -> XExpr t - -> IO (XExpr t) - cmp boolOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of - (XBool e1, XBool e2) -> XBool <$> boolOp e1 e2 - (XInt8 e1, XInt8 e2) -> XBool <$> bvOp e1 e2 - (XInt16 e1, XInt16 e2) -> XBool <$> bvOp e1 e2 - (XInt32 e1, XInt32 e2)-> XBool <$> bvOp e1 e2 - (XInt64 e1, XInt64 e2)-> XBool <$> bvOp e1 e2 - (XWord8 e1, XWord8 e2)-> XBool <$> bvOp e1 e2 - (XWord16 e1, XWord16 e2)-> XBool <$> bvOp e1 e2 - (XWord32 e1, XWord32 e2)-> XBool <$> bvOp e1 e2 - (XWord64 e1, XWord64 e2)-> XBool <$> bvOp e1 e2 - (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2 - (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2 - _ -> panic - - numCmp :: (forall w . BVCmp2 w t) - -> (forall w . BVCmp2 w t) - -> (forall fpp . FPCmp2 fpp t) - -> XExpr t - -> XExpr t - -> IO (XExpr t) - numCmp bvSOp bvUOp fpOp xe1 xe2 = case (xe1, xe2) of - (XInt8 e1, XInt8 e2) -> XBool <$> bvSOp e1 e2 - (XInt16 e1, XInt16 e2) -> XBool <$> bvSOp e1 e2 - (XInt32 e1, XInt32 e2)-> XBool <$> bvSOp e1 e2 - (XInt64 e1, XInt64 e2)-> XBool <$> bvSOp e1 e2 - (XWord8 e1, XWord8 e2)-> XBool <$> bvUOp e1 e2 - (XWord16 e1, XWord16 e2)-> XBool <$> bvUOp e1 e2 - (XWord32 e1, XWord32 e2)-> XBool <$> bvUOp e1 e2 - (XWord64 e1, XWord64 e2)-> XBool <$> bvUOp e1 e2 - (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2 - (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2 - _ -> panic - - buildIndexExpr :: 1 <= n - => WB.ExprBuilder t st fs - -> Word32 - -- ^ Index - -> WB.Expr t (WT.BaseBVType 32) - -- ^ Index - -> V.Vector n (XExpr t) - -- ^ Elements - -> IO (XExpr t) - buildIndexExpr sym curIx ix xelts = case V.uncons xelts of - (xe, Left Refl) -> return xe - (xe, Right xelts') -> do - LeqProof <- return $ V.nonEmpty xelts' - rstExpr <- buildIndexExpr sym (curIx+1) ix xelts' - curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx) - ixEq <- WI.bvEq sym curIxExpr ix - mkIte sym ixEq xe rstExpr - - mkIte :: WB.ExprBuilder t st fs - -> WB.Expr t WT.BaseBoolType - -> XExpr t - -> XExpr t - -> IO (XExpr t) - mkIte sym pred xe1 xe2 = case (xe1, xe2) of - (XBool e1, XBool e2) -> XBool <$> WI.itePred sym pred e1 e2 - (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym pred e1 e2 - (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym pred e1 e2 - (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym pred e1 e2 - (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym pred e1 e2 - (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym pred e1 e2 - (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym pred e1 e2 - (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym pred e1 e2 - (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym pred e1 e2 - (XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym pred e1 e2 - (XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym pred e1 e2 - (XStruct xes1, XStruct xes2) -> - XStruct <$> zipWithM (mkIte sym pred) xes1 xes2 - (XArray xes1, XArray xes2) -> - case V.length xes1 `testEquality` V.length xes2 of - Just Refl -> XArray <$> V.zipWithM (mkIte sym pred) xes1 xes2 - Nothing -> panic - _ -> panic - -translateOp3 :: forall t st fs a b c d . - WB.ExprBuilder t st fs - -> CE.Op3 a b c d - -> XExpr t - -> XExpr t - -> XExpr t - -> IO (XExpr t) -translateOp3 sym (CE.Mux _) (XBool te) xe1 xe2 = case (xe1, xe2) of - (XBool e1, XBool e2) -> XBool <$> WI.itePred sym te e1 e2 - (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym te e1 e2 - (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym te e1 e2 - (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym te e1 e2 - (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym te e1 e2 - (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym te e1 e2 - (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym te e1 e2 - (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym te e1 e2 - (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym te e1 e2 - (XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym te e1 e2 - (XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym te e1 e2 - _ -> panic -translateOp3 _ _ _ _ _ = panic +-- not proved true, that does not mean it isn't true; the proof may fail because +-- the given property is not inductive. +-- +-- We perform @k@-induction on all the properties in a given specification where +-- @k@ is chosen to be the maximum amount of delay on any of the involved +-- streams. This is a heuristic choice, but often effective. +module Copilot.Theorem.What4 + ( -- * Proving properties about Copilot specifications + prove + , Solver(..) + , SatResult(..) + -- * Bisimulation proofs about @copilot-c99@ code + , computeBisimulationProofBundle + , BisimulationProofBundle(..) + , BisimulationProofState(..) + -- * What4 representations of Copilot expressions + , XExpr(..) + ) where + +import qualified Copilot.Core.Expr as CE +import qualified Copilot.Core.Spec as CS +import qualified Copilot.Core.Type as CT + +import qualified What4.Config as WC +import qualified What4.Expr.Builder as WB +import qualified What4.Expr.GroundEval as WG +import qualified What4.Interface as WI +import qualified What4.InterpretedFloatingPoint as WFP +import qualified What4.Solver as WS +import qualified What4.Solver.DReal as WS + +import Control.Monad.State +import qualified Data.BitVector.Sized as BV +import Data.Foldable (foldrM) +import Data.List (genericLength) +import qualified Data.Map as Map +import Data.Parameterized.NatRepr +import Data.Parameterized.Nonce +import Data.Parameterized.Some +import GHC.Float (castWord32ToFloat, castWord64ToDouble) +import LibBF (BigFloat, bfToDouble, pattern NearEven) +import qualified Panic as Panic + +import Copilot.Theorem.What4.Translate + +-- 'prove' function +-- +-- To prove properties of a spec, we translate them into What4 using the TransM +-- monad (transformer on top of IO), then negate each property and ask a backend +-- solver to produce a model for the negation. + +-- | No builder state needed. +data BuilderState a = EmptyState + +-- | The solvers supported by the what4 backend. +data Solver = CVC4 | DReal | Yices | Z3 + +-- | The 'prove' function returns results of this form for each property in a +-- spec. +data SatResult = Valid | Invalid | Unknown + deriving Show + +type CounterExample = [(String, Some CopilotValue)] + +-- | Attempt to prove all of the properties in a spec via an SMT solver (which +-- must be installed locally on the host). Return an association list mapping +-- the names of each property to the result returned by the solver. +prove :: Solver + -- ^ Solver to use + -> CS.Spec + -- ^ Spec + -> IO [(CE.Name, SatResult)] +prove solver spec = do + -- Setup symbolic backend + Some ng <- newIONonceGenerator + sym <- WB.newExprBuilder WB.FloatIEEERepr EmptyState ng + + -- Solver-specific options + case solver of + CVC4 -> WC.extendConfig WS.cvc4Options (WI.getConfiguration sym) + DReal -> WC.extendConfig WS.drealOptions (WI.getConfiguration sym) + Yices -> WC.extendConfig WS.yicesOptions (WI.getConfiguration sym) + Z3 -> WC.extendConfig WS.z3Options (WI.getConfiguration sym) + + -- Compute the maximum amount of delay for any stream in this spec + let bufLen (CS.Stream _ buf _ _) = genericLength buf + maxBufLen = maximum (0 : (bufLen <$> CS.specStreams spec)) + + -- This process performs k-induction where we use @k = maxBufLen@. + -- The choice for @k@ is heuristic, but often effective. + let proveProperties = forM (CS.specProperties spec) $ \pr -> do + -- State the base cases for k induction. + base_cases <- forM [0 .. maxBufLen - 1] $ \i -> do + xe <- translateExpr sym mempty (CS.propertyExpr pr) (AbsoluteOffset i) + case xe of + XBool p -> return p + _ -> expectedBool "Property" xe + + -- Translate the induction hypothesis for all values up to maxBufLen in + -- the past + ind_hyps <- forM [0 .. maxBufLen-1] $ \i -> do + xe <- translateExpr sym mempty (CS.propertyExpr pr) (RelativeOffset i) + case xe of + XBool hyp -> return hyp + _ -> expectedBool "Property" xe + + -- Translate the predicate for the "current" value + ind_goal <- do + xe <- translateExpr sym + mempty + (CS.propertyExpr pr) + (RelativeOffset maxBufLen) + case xe of + XBool p -> return p + _ -> expectedBool "Property" xe + + -- Compute the predicate (ind_hyps ==> p) + ind_case <- liftIO $ foldrM (WI.impliesPred sym) ind_goal ind_hyps + + -- Compute the conjunction of the base and inductive cases + p <- liftIO $ foldrM (WI.andPred sym) ind_case base_cases + + -- Negate the goals for for SAT search + not_p <- liftIO $ WI.notPred sym p + let clauses = [not_p] + + case solver of + CVC4 -> liftIO $ WS.runCVC4InOverride sym WS.defaultLogData clauses $ \case + WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid) + WS.Unsat _ -> return (CS.propertyName pr, Valid) + WS.Unknown -> return (CS.propertyName pr, Unknown) + DReal -> liftIO $ WS.runDRealInOverride sym WS.defaultLogData clauses $ \case + WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid) + WS.Unsat _ -> return (CS.propertyName pr, Valid) + WS.Unknown -> return (CS.propertyName pr, Unknown) + Yices -> liftIO $ WS.runYicesInOverride sym WS.defaultLogData clauses $ \case + WS.Sat _ge -> return (CS.propertyName pr, Invalid) + WS.Unsat _ -> return (CS.propertyName pr, Valid) + WS.Unknown -> return (CS.propertyName pr, Unknown) + Z3 -> liftIO $ WS.runZ3InOverride sym WS.defaultLogData clauses $ \case + WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid) + WS.Unsat _ -> return (CS.propertyName pr, Valid) + WS.Unknown -> return (CS.propertyName pr, Unknown) + + -- Execute the action and return the results for each property + runTransM spec proveProperties + +-- Bisimulation proofs + +-- | Given a Copilot specification, compute all of the symbolic states necessary +-- to carry out a bisimulation proof that establishes a correspondence between +-- the states of the Copilot stream program and the C code that @copilot-c99@ +-- would generate for that Copilot program. +computeBisimulationProofBundle :: + WFP.IsInterpretedFloatSymExprBuilder sym + => sym + -> [String] + -- ^ Names of properties to assume during verification + -> CS.Spec + -- ^ The input Copilot specification + -> IO (BisimulationProofBundle sym) +computeBisimulationProofBundle sym properties spec = do + iss <- computeInitialStreamState sym spec + runTransM spec $ do + prestate <- computePrestate sym spec + poststate <- computePoststate sym spec + triggers <- computeTriggerState sym spec + assms <- computeAssumptions sym properties spec + externs <- computeExternalInputs sym + sideCnds <- gets sidePreds + return + BisimulationProofBundle + { initialStreamState = iss + , preStreamState = prestate + , postStreamState = poststate + , externalInputs = externs + , triggerState = triggers + , assumptions = assms + , sideConds = sideCnds + } + +-- | A collection of all of the symbolic states necessary to carry out a +-- bisimulation proof. +data BisimulationProofBundle sym = + BisimulationProofBundle + { initialStreamState :: BisimulationProofState sym + -- ^ The state of the global variables at program startup + , preStreamState :: BisimulationProofState sym + -- ^ The stream state prior to invoking the step function + , postStreamState :: BisimulationProofState sym + -- ^ The stream state after invoking the step function + , externalInputs :: [(CE.Name, Some CT.Type, XExpr sym)] + -- ^ A list of external streams, where each tuple contains: + -- + -- 1. The name of the stream + -- + -- 2. The type of the stream + -- + -- 3. The value of the stream represented as a fresh constant + , triggerState :: [(CE.Name, WI.Pred sym, [(Some CT.Type, XExpr sym)])] + -- ^ A list of trigger functions, where each tuple contains: + -- + -- 1. The name of the function + -- + -- 2. A formula representing the guarded condition + -- + -- 3. The arguments to the function, where each argument is represented as + -- a type-value pair + , assumptions :: [WI.Pred sym] + -- ^ User-provided property assumptions + , sideConds :: [WI.Pred sym] + -- ^ Side conditions related to partial operations + } + +-- | The state of a bisimulation proof at a particular step. +newtype BisimulationProofState sym = + BisimulationProofState + { streamState :: [(CE.Id, Some CT.Type, [XExpr sym])] + -- ^ A list of tuples containing: + -- + -- 1. The name of a stream + -- + -- 2. The type of the stream + -- + -- 3. The list of values in the stream description + } + +-- | Compute the initial state of the global variables at the start of a Copilot +-- program. +computeInitialStreamState :: + WFP.IsInterpretedFloatSymExprBuilder sym + => sym + -> CS.Spec + -- ^ The input Copilot specification + -> IO (BisimulationProofState sym) +computeInitialStreamState sym spec = do + xs <- forM (CS.specStreams spec) $ + \CS.Stream { CS.streamId = nm, CS.streamExprType = tp + , CS.streamBuffer = buf } -> + do vs <- mapM (translateConstExpr sym tp) buf + return (nm, Some tp, vs) + return (BisimulationProofState xs) + +-- | Compute the stream state of a Copilot program prior to invoking the step +-- function. +computePrestate :: + WFP.IsInterpretedFloatSymExprBuilder sym + => sym + -> CS.Spec + -- ^ The input Copilot specification + -> TransM sym (BisimulationProofState sym) +computePrestate sym spec = do + xs <- forM (CS.specStreams spec) $ + \CS.Stream { CS.streamId = nm, CS.streamExprType = tp + , CS.streamBuffer = buf } -> + do let buflen = genericLength buf + let idxes = RelativeOffset <$> [0 .. buflen-1] + vs <- mapM (getStreamValue sym nm) idxes + return (nm, Some tp, vs) + return (BisimulationProofState xs) + +-- | Compute ehe stream state of a Copilot program after invoking the step +-- function. +computePoststate :: + WFP.IsInterpretedFloatSymExprBuilder sym + => sym + -> CS.Spec + -- ^ The input Copilot specification + -> TransM sym (BisimulationProofState sym) +computePoststate sym spec = do + xs <- forM (CS.specStreams spec) $ + \CS.Stream { CS.streamId = nm, CS.streamExprType = tp + , CS.streamBuffer = buf } -> + do let buflen = genericLength buf + let idxes = RelativeOffset <$> [1 .. buflen] + vs <- mapM (getStreamValue sym nm) idxes + return (nm, Some tp, vs) + return (BisimulationProofState xs) + +-- | Compute the trigger functions in a Copilot program. +computeTriggerState :: + WFP.IsInterpretedFloatSymExprBuilder sym + => sym + -> CS.Spec + -- ^ The input Copilot specification + -> TransM sym [(CE.Name, WI.Pred sym, [(Some CT.Type, XExpr sym)])] +computeTriggerState sym spec = forM (CS.specTriggers spec) $ + \(CS.Trigger { CS.triggerName = nm, CS.triggerGuard = guard + , CS.triggerArgs = args }) -> + do xguard <- translateExpr sym mempty guard (RelativeOffset 0) + guard' <- + case xguard of + XBool guard' -> return guard' + _ -> expectedBool "Trigger guard" xguard + args' <- mapM computeArg args + return (nm, guard', args') + where + computeArg (CE.UExpr { CE.uExprType = tp, CE.uExprExpr = ex }) = do + v <- translateExpr sym mempty ex (RelativeOffset 0) + return (Some tp, v) + +-- | Compute the values of the external streams in a Copilot program, where each +-- external stream is represented as a fresh constant. +computeExternalInputs :: + WFP.IsInterpretedFloatSymExprBuilder sym + => sym + -> TransM sym [(CE.Name, Some CT.Type, XExpr sym)] +computeExternalInputs sym = do + exts <- Map.toList <$> gets mentionedExternals + forM exts $ \(nm, Some tp) -> do + v <- getExternConstant sym tp nm (RelativeOffset 0) + return (nm, Some tp, v) + +-- | Compute the user-provided property assumptions in a Copilot program. +computeAssumptions :: + forall sym. + WFP.IsInterpretedFloatSymExprBuilder sym + => sym + -> [String] + -- ^ Names of properties to assume during verification + -> CS.Spec + -- ^ The input Copilot specification + -> TransM sym [WI.Pred sym] +computeAssumptions sym properties spec = + concat <$> forM specPropertyExprs computeAssumption + where + bufLen (CS.Stream _ buf _ _) = genericLength buf + maxBufLen = maximum (0 : (bufLen <$> CS.specStreams spec)) + + -- Retrieve the boolean-values Copilot expressions corresponding to the + -- user-provided property assumptions. + specPropertyExprs :: [CE.Expr Bool] + specPropertyExprs = + [ CS.propertyExpr p + | p <- CS.specProperties spec + , elem (CS.propertyName p) properties + ] + + -- Compute all of the what4 predicates corresponding to each user-provided + -- property assumption. + computeAssumption :: CE.Expr Bool -> TransM sym [WI.Pred sym] + computeAssumption e = forM [0 .. maxBufLen] $ \i -> do + xe <- translateExpr sym mempty e (RelativeOffset i) + case xe of + XBool b -> return b + _ -> expectedBool "Property" xe + +-- * Auxiliary functions + +-- | A catch-all 'panic' to use when an 'XExpr' is is expected to uphold the +-- invariant that it is an 'XBool', but the invariant is violated. +expectedBool :: forall m sym a. + (Panic.HasCallStack, MonadIO m, WI.IsExprBuilder sym) + => String + -- ^ What the 'XExpr' represents + -> XExpr sym + -> m a +expectedBool what xe = + panic [what ++ " expected to have boolean result", show xe] + +data CopilotValue a = CopilotValue { cvType :: CT.Type a + , cvVal :: a + } + +valFromExpr :: forall sym t st fm. + ( sym ~ WB.ExprBuilder t st (WB.Flags fm) + , WI.KnownRepr WB.FloatModeRepr fm + ) + => WG.GroundEvalFn t + -> XExpr sym + -> IO (Some CopilotValue) +valFromExpr ge xe = case xe of + XBool e -> Some . CopilotValue CT.Bool <$> WG.groundEval ge e + XInt8 e -> Some . CopilotValue CT.Int8 . fromBV <$> WG.groundEval ge e + XInt16 e -> Some . CopilotValue CT.Int16 . fromBV <$> WG.groundEval ge e + XInt32 e -> Some . CopilotValue CT.Int32 . fromBV <$> WG.groundEval ge e + XInt64 e -> Some . CopilotValue CT.Int64 . fromBV <$> WG.groundEval ge e + XWord8 e -> Some . CopilotValue CT.Word8 . fromBV <$> WG.groundEval ge e + XWord16 e -> Some . CopilotValue CT.Word16 . fromBV <$> WG.groundEval ge e + XWord32 e -> Some . CopilotValue CT.Word32 . fromBV <$> WG.groundEval ge e + XWord64 e -> Some . CopilotValue CT.Word64 . fromBV <$> WG.groundEval ge e + XFloat e -> + Some . CopilotValue CT.Float <$> + iFloatGroundEval WFP.SingleFloatRepr e + (realToFrac . fst . bfToDouble NearEven) + fromRational + (castWord32ToFloat . fromInteger . BV.asUnsigned) + XDouble e -> + Some . CopilotValue CT.Double <$> + iFloatGroundEval WFP.DoubleFloatRepr e + (fst . bfToDouble NearEven) + fromRational + (castWord64ToDouble . fromInteger . BV.asUnsigned) + _ -> error "valFromExpr unhandled case" + where + fromBV :: forall a w . Num a => BV.BV w -> a + fromBV = fromInteger . BV.asUnsigned + + -- Evaluate a (possibly symbolic) floating-point value to a concrete result. + -- Depending on which @what4@ floating-point mode is in use, the result will + -- be passed to one of three different continuation arguments. + iFloatGroundEval :: + forall fi r. + WFP.FloatInfoRepr fi -> + WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi) -> + (BigFloat -> r) -> + -- ^ Continuation to use if the IEEE floating-point mode is in use. + (Rational -> r) -> + -- ^ Continuation to use if the real floating-point mode is in use. + (forall w. BV.BV w -> r) -> + -- ^ Continuation to use if the uninterpreted floating-point mode is in + -- use. + IO r + iFloatGroundEval _ e ieeeK realK uninterpK = + case WI.knownRepr :: WB.FloatModeRepr fm of + WB.FloatIEEERepr -> ieeeK <$> WG.groundEval ge e + WB.FloatRealRepr -> realK <$> WG.groundEval ge e + WB.FloatUninterpretedRepr -> uninterpK <$> WG.groundEval ge e diff --git a/src/Copilot/Theorem/What4/Translate.hs b/src/Copilot/Theorem/What4/Translate.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/What4/Translate.hs @@ -0,0 +1,1375 @@ +{-# 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. + mentionedExternals :: Map.Map CE.Name (Some CT.Type), + -- | Memo table for external variables, indexed by the external stream name + -- and a stream offset. + externVars :: Map.Map (CE.Name, StreamOffset) (XExpr sym), + -- | Memo table for stream values, indexed by the stream 'CE.Id' and offset. + 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. + 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. + sidePreds :: [WI.Pred sym] + } + +newtype TransM sym a = TransM { unTransM :: StateT (TransState sym) IO a } + deriving ( Functor + , Applicative + , Monad + , Fail.MonadFail + , MonadIO + , MonadState (TransState sym) + ) + +-- | Translate a Copilot specification using the given 'TransM' computation. +runTransM :: CS.Spec -> TransM sym a -> IO a +runTransM spec m = do + -- Build up initial translation state + let streamMap = Map.fromList $ + (\stream -> (CS.streamId stream, stream)) <$> CS.specStreams spec + st = TransState + { mentionedExternals = mempty + , externVars = mempty + , streamValues = mempty + , streams = streamMap + , sidePreds = [] + } + + (res, _) <- runStateT (unTransM m) st + return 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 sym localEnv e offset = case e of + CE.Const tp a -> liftIO $ translateConstExpr sym tp a + CE.Drop _tp ix streamId -> getStreamValue sym streamId (addOffset offset ix) + CE.Local _tpa _tpb nm e1 body -> do + ref <- liftIO (newIORef 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 offset' = do + m <- liftIO (readIORef ref) + case Map.lookup offset' m of + -- If we have looked up this value before, return the cached value. + Just x -> return x + -- Otherwise, translate the expression and cache it for subsequent + -- lookups. + Nothing -> + do x <- translateExpr sym localEnv e1 offset' + liftIO (modifyIORef ref (Map.insert offset' x)) + return x + + let localEnv' = Map.insert nm f localEnv + translateExpr sym localEnv' body offset + CE.Var _tp nm -> + case Map.lookup nm localEnv of + Nothing -> panic ["translateExpr: unknown var " ++ show nm] + Just f -> f offset + CE.ExternVar tp nm _prefix -> getExternConstant sym tp nm offset + CE.Op1 op e1 -> do + xe1 <- translateExpr sym localEnv e1 offset + translateOp1 sym e op xe1 + CE.Op2 op e1 e2 -> do + xe1 <- translateExpr sym localEnv e1 offset + xe2 <- translateExpr sym localEnv e2 offset + translateOp2 sym e op xe1 xe2 + CE.Op3 op e1 e2 e3 -> do + xe1 <- translateExpr sym localEnv e1 offset + xe2 <- translateExpr sym localEnv e2 offset + xe3 <- translateExpr sym localEnv e3 offset + translateOp3 sym e op xe1 xe2 xe3 + CE.Label _ _ e1 -> + translateExpr sym localEnv e1 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 sym streamId offset = do + svs <- gets streamValues + case Map.lookup (streamId, offset) svs of + Just xe -> return xe + Nothing -> do + streamDef <- getStreamDef streamId + xe <- computeStreamValue streamDef + modify $ \st -> + st { streamValues = + Map.insert (streamId, offset) xe (streamValues st) } + return xe + where + computeStreamValue + (CS.Stream + { CS.streamId = id, CS.streamBuffer = buf, + CS.streamExpr = ex, CS.streamExprType = tp }) = + let len = genericLength buf in + case offset of + AbsoluteOffset i + | i < 0 -> panic ["Invalid absolute offset " ++ show i ++ + " for stream " ++ show id] + | i < len -> liftIO (translateConstExpr sym tp (genericIndex buf i)) + | otherwise -> translateExpr sym mempty ex (AbsoluteOffset (i - len)) + RelativeOffset i + | i < 0 -> panic ["Invalid relative offset " ++ show i ++ + " for stream " ++ show id] + | i < len -> let nm = "s" ++ show id ++ "_r" ++ show i + in liftIO (freshCPConstant sym nm tp) + | otherwise -> translateExpr sym mempty ex (RelativeOffset (i - 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 sym tp nm offset = do + es <- gets externVars + case Map.lookup (nm, offset) es of + Just xe -> return xe + Nothing -> do + xe <- computeExternConstant + modify $ \st -> + st { externVars = Map.insert (nm, offset) xe (externVars st) + , mentionedExternals = + Map.insert nm (Some tp) (mentionedExternals st) + } + return xe + where + computeExternConstant = + case offset of + AbsoluteOffset i + | i < 0 -> panic ["Invalid absolute offset " ++ show i ++ + " for external stream " ++ nm] + | otherwise -> let nm' = nm ++ "_a" ++ show i + in liftIO (freshCPConstant sym nm' tp) + RelativeOffset i + | i < 0 -> panic ["Invalid relative offset " ++ show i ++ + " for external stream " ++ nm] + | otherwise -> let nm' = nm ++ "_r" ++ show i + in liftIO (freshCPConstant sym nm' 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 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 xe = case xe of + XInt8 e -> Just (SomeBVExpr e knownNat Signed XInt8) + XInt16 e -> Just (SomeBVExpr e knownNat Signed XInt16) + XInt32 e -> Just (SomeBVExpr e knownNat Signed XInt32) + XInt64 e -> Just (SomeBVExpr e knownNat Signed XInt64) + XWord8 e -> Just (SomeBVExpr e knownNat Unsigned XWord8) + XWord16 e -> Just (SomeBVExpr e knownNat Unsigned XWord16) + XWord32 e -> Just (SomeBVExpr e knownNat Unsigned XWord32) + XWord64 e -> Just (SomeBVExpr e knownNat Unsigned XWord64) + _ -> Nothing + +-- | 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 xe makeSidePred = + case asBVExpr xe of + Just (SomeBVExpr e w sgn _) -> do + sidePred <- liftIO $ makeSidePred e w sgn + addSidePred sidePred + Nothing -> 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 xe1 xe2 makeSidePred = + case (asBVExpr xe1, asBVExpr xe2) of + (Just (SomeBVExpr e1 w1 sgn1 _), Just (SomeBVExpr e2 w2 sgn2 _)) + | Just Refl <- testEquality w1 w2 + , sgn1 == sgn2 + -> do sidePred <- liftIO $ makeSidePred e1 e2 w1 sgn1 + addSidePred sidePred + _ -> 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 sym tp a = case tp of + CT.Bool -> case a of + True -> return $ XBool (WI.truePred sym) + False -> return $ XBool (WI.falsePred sym) + CT.Int8 -> XInt8 <$> WI.bvLit sym knownNat (BV.int8 a) + CT.Int16 -> XInt16 <$> WI.bvLit sym knownNat (BV.int16 a) + CT.Int32 -> XInt32 <$> WI.bvLit sym knownNat (BV.int32 a) + CT.Int64 -> XInt64 <$> WI.bvLit sym knownNat (BV.int64 a) + CT.Word8 -> XWord8 <$> WI.bvLit sym knownNat (BV.word8 a) + CT.Word16 -> XWord16 <$> WI.bvLit sym knownNat (BV.word16 a) + CT.Word32 -> XWord32 <$> WI.bvLit sym knownNat (BV.word32 a) + CT.Word64 -> XWord64 <$> WI.bvLit sym knownNat (BV.word64 a) + CT.Float -> XFloat <$> WFP.iFloatLitSingle sym a + CT.Double -> XDouble <$> WFP.iFloatLitDouble sym a + CT.Array tp -> do + elts <- traverse (translateConstExpr sym tp) (CT.arrayelems a) + Some n <- return $ mkNatRepr (genericLength elts) + case isZeroOrGT1 n of + Left Refl -> return XEmptyArray + Right LeqProof -> do + let Just v = V.fromList n elts + return $ XArray v + CT.Struct _ -> do + elts <- forM (CT.toValues a) $ \(CT.Value tp (CT.Field a)) -> + translateConstExpr sym tp a + return $ XStruct elts + +arrayLen :: KnownNat n => CT.Type (CT.Array n t) -> NatRepr n +arrayLen _ = knownNat + +-- | Generate a fresh constant for a given copilot type. This will be called +-- whenever we attempt to get the constant for a given external variable or +-- stream variable, but that variable has not been accessed yet and therefore +-- has no constant allocated. +freshCPConstant :: forall sym a . + WFP.IsInterpretedFloatSymExprBuilder sym + => sym + -> String + -> CT.Type a + -> IO (XExpr sym) +freshCPConstant sym nm tp = case tp of + CT.Bool -> XBool <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Int8 -> XInt8 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Int16 -> XInt16 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Int32 -> XInt32 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Int64 -> XInt64 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Word8 -> XWord8 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Word16 -> XWord16 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Word32 -> XWord32 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Word64 -> XWord64 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Float -> XFloat <$> + WFP.freshFloatConstant sym (WI.safeSymbol nm) WFP.SingleFloatRepr + CT.Double -> XDouble <$> + WFP.freshFloatConstant sym (WI.safeSymbol nm) WFP.DoubleFloatRepr + atp@(CT.Array itp) -> do + let n = arrayLen atp + case isZeroOrGT1 n of + Left Refl -> return XEmptyArray + Right LeqProof -> do + Refl <- return $ minusPlusCancel n (knownNat @1) + elts :: V.Vector n (XExpr t) <- + V.generateM (decNat n) (const (freshCPConstant sym "" itp)) + return $ XArray elts + CT.Struct stp -> do + elts <- forM (CT.toValues stp) $ \(CT.Value ftp _) -> + freshCPConstant sym "" ftp + return $ XStruct elts + +-- | Retrieve a stream definition given its id. +getStreamDef :: CE.Id -> TransM sym CS.Stream +getStreamDef streamId = fromJust <$> gets (Map.lookup streamId . streams) + +-- | Add a side condition originating from an application of a partial function. +addSidePred :: WI.Pred sym -> TransM sym () +addSidePred newPred = modify (\st -> st { sidePreds = newPred : sidePreds 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 _ = knownSymbol + +valueName :: CT.Value a -> Some SymbolRepr +valueName (CT.Value _ f) = Some (fieldName 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 sym origExpr op xe = case (op, xe) of + (CE.Not, XBool e) -> liftIO $ fmap XBool $ WI.notPred sym e + (CE.Not, _) -> panic ["Expected bool", show xe] + (CE.Abs _, xe) -> translateAbs xe + (CE.Sign _, xe) -> translateSign 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 _, xe) -> liftIO $ fpOp recip xe + where + recip :: forall fi . FPOp1 sym fi + recip fiRepr e = do + one <- fpLit fiRepr 1.0 + WFP.iFloatDiv @_ @fi sym fpRM one e + -- The argument should not cause the result to overflow or underlow + (CE.Exp _, xe) -> liftIO $ fpSpecialOp WSF.Exp xe + -- The argument should not be less than -0 + (CE.Sqrt _, xe) -> + liftIO $ + fpOp (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatSqrt @_ @fi sym fpRM) xe + -- The argument should not be negative or zero + (CE.Log _, xe) -> liftIO $ fpSpecialOp WSF.Log xe + -- The argument should not be infinite + (CE.Sin _, xe) -> liftIO $ fpSpecialOp WSF.Sin xe + -- The argument should not be infinite + (CE.Cos _, xe) -> liftIO $ fpSpecialOp WSF.Cos xe + -- The argument should not be infinite, nor should it cause the result to + -- overflow + (CE.Tan _, xe) -> liftIO $ fpSpecialOp WSF.Tan xe + -- The argument should not cause the result to overflow + (CE.Sinh _, xe) -> liftIO $ fpSpecialOp WSF.Sinh xe + -- The argument should not cause the result to overflow + (CE.Cosh _, xe) -> liftIO $ fpSpecialOp WSF.Cosh xe + (CE.Tanh _, xe) -> liftIO $ fpSpecialOp WSF.Tanh xe + -- The argument should not be outside the range [-1, 1] + (CE.Asin _, xe) -> liftIO $ fpSpecialOp WSF.Arcsin xe + -- The argument should not be outside the range [-1, 1] + (CE.Acos _, xe) -> liftIO $ fpSpecialOp WSF.Arccos xe + (CE.Atan _, xe) -> liftIO $ fpSpecialOp WSF.Arctan xe + (CE.Asinh _, xe) -> liftIO $ fpSpecialOp WSF.Arcsinh xe + -- The argument should not be less than 1 + (CE.Acosh _, xe) -> liftIO $ fpSpecialOp WSF.Arccosh xe + -- The argument should not be less than or equal to -1, + -- nor should it be greater than or equal to +1 + (CE.Atanh _, xe) -> liftIO $ fpSpecialOp WSF.Arctanh xe + -- The argument should not cause the result to overflow + (CE.Ceiling _, xe) -> + liftIO $ + fpOp (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatRound @_ @fi sym WI.RTP) xe + -- The argument should not cause the result to overflow + (CE.Floor _, xe) -> + liftIO $ + fpOp (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatRound @_ @fi sym WI.RTN) xe + (CE.BwNot _, xe) -> liftIO $ case xe of + XBool e -> XBool <$> WI.notPred sym e + _ -> bvOp (WI.bvNotBits sym) xe + (CE.Cast _ tp, xe) -> liftIO $ castOp sym origExpr tp xe + (CE.GetField atp _ftp extractor, xe) -> translateGetField atp extractor 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 xe = do + addBVSidePred1 xe $ \e w _ -> do + -- The argument should not be INT_MIN + bvIntMin <- liftIO $ WI.bvLit sym w (BV.minSigned w) + eqIntMin <- liftIO $ WI.bvEq sym e bvIntMin + WI.notPred sym eqIntMin + liftIO $ numOp bvAbs fpAbs xe + where + bvAbs :: BVOp1 sym w + bvAbs e = do + zero <- WI.bvLit sym knownNat (BV.zero knownNat) + e_neg <- WI.bvSlt sym e zero + neg_e <- WI.bvSub sym zero e + WI.bvIte sym e_neg neg_e e + + fpAbs :: forall fi . FPOp1 sym fi + fpAbs _ e = WFP.iFloatAbs @_ @fi sym 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 tp extractor xe = case (tp, xe) of + (CT.Struct s, XStruct xes) -> + case mIx s of + Just ix -> return $ xes !! ix + Nothing -> panic [ "Could not find field " ++ show fieldNameRepr + , show s + ] + _ -> unexpectedValue "get-field operation" + where + fieldNameRepr :: SymbolRepr s + fieldNameRepr = fieldName (extractor undefined) + + structFieldNameReprs :: CT.Struct struct => struct -> [Some SymbolRepr] + structFieldNameReprs s = valueName <$> CT.toValues s + + mIx :: CT.Struct struct => struct -> Maybe Int + mIx s = elemIndex (Some fieldNameRepr) (structFieldNameReprs 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 xe = liftIO $ numOp bvSign fpSign xe + where + bvSign :: BVOp1 sym w + bvSign e = do + zero <- WI.bvLit sym knownRepr (BV.zero knownNat) + neg_one <- WI.bvLit sym knownNat (BV.mkBV knownNat (-1)) + pos_one <- WI.bvLit sym knownNat (BV.mkBV knownNat 1) + e_neg <- WI.bvSlt sym e zero + e_pos <- WI.bvSgt sym e zero + t <- WI.bvIte sym e_neg neg_one e + WI.bvIte sym e_pos pos_one t + + fpSign :: forall fi . FPOp1 sym fi + fpSign fiRepr e = do + zero <- fpLit fiRepr 0.0 + neg_one <- fpLit fiRepr (-1.0) + pos_one <- fpLit fiRepr 1.0 + e_neg <- WFP.iFloatLt @_ @fi sym e zero + e_pos <- WFP.iFloatGt @_ @fi sym e zero + t <- WFP.iFloatIte @_ @fi sym e_neg neg_one e + WFP.iFloatIte @_ @fi sym e_pos pos_one 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 bvOp fpOp xe = case xe of + XInt8 e -> XInt8 <$> bvOp e + XInt16 e -> XInt16 <$> bvOp e + XInt32 e -> XInt32 <$> bvOp e + XInt64 e -> XInt64 <$> bvOp e + XWord8 e -> XWord8 <$> bvOp e + XWord16 e -> XWord16 <$> bvOp e + XWord32 e -> XWord32 <$> bvOp e + XWord64 e -> XWord64 <$> bvOp e + XFloat e -> XFloat <$> fpOp WFP.SingleFloatRepr e + XDouble e -> XDouble <$> fpOp WFP.DoubleFloatRepr e + _ -> unexpectedValue "numOp" + + bvOp :: (forall w . BVOp1 sym w) -> XExpr sym -> IO (XExpr sym) + bvOp f xe = case xe of + XInt8 e -> XInt8 <$> f e + XInt16 e -> XInt16 <$> f e + XInt32 e -> XInt32 <$> f e + XInt64 e -> XInt64 <$> f e + XWord8 e -> XWord8 <$> f e + XWord16 e -> XWord16 <$> f e + XWord32 e -> XWord32 <$> f e + XWord64 e -> XWord64 <$> f e + _ -> unexpectedValue "bvOp" + + fpOp :: (forall fi . FPOp1 sym fi) -> XExpr sym -> IO (XExpr sym) + fpOp g xe = case xe of + XFloat e -> XFloat <$> g WFP.SingleFloatRepr e + XDouble e -> XDouble <$> g WFP.DoubleFloatRepr e + _ -> unexpectedValue "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 fn = fpOp (\fiRepr -> WFP.iFloatSpecialFunction1 sym fiRepr 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 fiRepr fracLit = + case fiRepr of + WFP.SingleFloatRepr -> WFP.iFloatLitSingle sym fracLit + WFP.DoubleFloatRepr -> WFP.iFloatLitDouble sym fracLit + _ -> panic ["Expected single- or double-precision float", show fiRepr] + + -- A catch-all error message to use when translation cannot proceed. + unexpectedValue :: forall m x. + (Panic.HasCallStack, MonadIO m) + => String + -> m x + unexpectedValue op = + panic [ "Unexpected value in " ++ op ++ ": " ++ show (CP.ppExpr origExpr) + , show 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 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of + (CE.And, XBool e1, XBool e2) -> liftIO $ fmap XBool $ WI.andPred sym e1 e2 + (CE.And, _, _) -> unexpectedValues "and operation" + (CE.Or, XBool e1, XBool e2) -> liftIO $ fmap XBool $ WI.orPred sym e1 e2 + (CE.Or, _, _) -> unexpectedValues "or operation" + (CE.Add _, xe1, xe2) -> translateAdd xe1 xe2 + (CE.Sub _, xe1, xe2) -> translateSub xe1 xe2 + (CE.Mul _, xe1, xe2) -> translateMul xe1 xe2 + (CE.Mod _, xe1, xe2) -> do + -- The second argument should not be zero + addBVSidePred1 xe2 $ \e2 _ _ -> WI.bvIsNonzero sym e2 + liftIO $ bvOp (WI.bvSrem sym) (WI.bvUrem sym) xe1 xe2 + (CE.Div _, xe1, xe2) -> do + -- The second argument should not be zero + addBVSidePred1 xe2 $ \e2 _ _ -> WI.bvIsNonzero sym e2 + liftIO $ bvOp (WI.bvSdiv sym) (WI.bvUdiv sym) xe1 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 _, xe1, xe2) -> + liftIO $ + fpOp (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatDiv @_ @fi sym fpRM) + xe1 + 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 _, xe1, xe2) -> liftIO $ fpSpecialOp WSF.Pow xe1 xe2 + -- The second argument should not be negative or zero + (CE.Logb _, xe1, xe2) -> liftIO $ fpOp logbFn xe1 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 fiRepr e1 e2 = do + re1 <- WFP.iFloatSpecialFunction1 sym fiRepr WSF.Log e1 + re2 <- WFP.iFloatSpecialFunction1 sym fiRepr WSF.Log e2 + WFP.iFloatDiv @_ @fi sym fpRM re2 re1 + (CE.Atan2 _, xe1, xe2) -> liftIO $ fpSpecialOp WSF.Arctan2 xe1 xe2 + (CE.Eq _, xe1, xe2) -> + liftIO $ + cmp (WI.eqPred sym) + (WI.bvEq sym) + (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatEq @_ @fi sym) + xe1 + xe2 + (CE.Ne _, xe1, xe2) -> translateNe xe1 xe2 + (CE.Le _, xe1, xe2) -> + liftIO $ + numCmp (WI.bvSle sym) + (WI.bvUle sym) + (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatLe @_ @fi sym) + xe1 + xe2 + (CE.Ge _, xe1, xe2) -> + liftIO $ + numCmp (WI.bvSge sym) + (WI.bvUge sym) + (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatGe @_ @fi sym) + xe1 + xe2 + (CE.Lt _, xe1, xe2) -> + liftIO $ + numCmp (WI.bvSlt sym) + (WI.bvUlt sym) + (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatLt @_ @fi sym) + xe1 + xe2 + (CE.Gt _, xe1, xe2) -> + liftIO $ + numCmp (WI.bvSgt sym) + (WI.bvUgt sym) + (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatGt @_ @fi sym) + xe1 + xe2 + (CE.BwAnd _, xe1, xe2) -> + liftIO $ bvOp (WI.bvAndBits sym) (WI.bvAndBits sym) xe1 xe2 + (CE.BwOr _, xe1, xe2) -> + liftIO $ bvOp (WI.bvOrBits sym) (WI.bvOrBits sym) xe1 xe2 + (CE.BwXor _, xe1, xe2) -> + liftIO $ bvOp (WI.bvXorBits sym) (WI.bvXorBits sym) xe1 xe2 + (CE.BwShiftL _ _, xe1, xe2) -> translateBwShiftL xe1 xe2 + (CE.BwShiftR _ _, xe1, xe2) -> translateBwShiftR xe1 xe2 + (CE.Index _, xe1, xe2) -> translateIndex xe1 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 xe1 xe2 = do + addBVSidePred2 xe1 xe2 $ \e1 e2 _ sgn -> + -- The arguments should not result in signed overflow or underflow + case sgn of + Signed -> do + (wrap, _) <- WI.addSignedOF sym e1 e2 + WI.notPred sym wrap + Unsigned -> pure $ WI.truePred sym + + liftIO $ + numOp (WI.bvAdd sym) + (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatAdd @_ @fi sym fpRM) + xe1 + 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 xe1 xe2 = do + addBVSidePred2 xe1 xe2 $ \e1 e2 _ sgn -> + -- The arguments should not result in signed overflow or underflow + case sgn of + Signed -> do + (wrap, _) <- WI.subSignedOF sym e1 e2 + WI.notPred sym wrap + Unsigned -> pure $ WI.truePred sym + + liftIO $ + numOp (WI.bvSub sym) + (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatSub @_ @fi sym fpRM) + xe1 + 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 xe1 xe2 = do + addBVSidePred2 xe1 xe2 $ \e1 e2 _ sgn -> + -- The arguments should not result in signed overflow or underflow + case sgn of + Signed -> do + (wrap, _) <- WI.mulSignedOF sym e1 e2 + WI.notPred sym wrap + Unsigned -> pure $ WI.truePred sym + + liftIO $ + numOp (WI.bvMul sym) + (\(_ :: WFP.FloatInfoRepr fi) -> WFP.iFloatMul @_ @fi sym fpRM) + xe1 + 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 xe1 xe2 = liftIO $ cmp neqPred bvNeq fpNeq xe1 xe2 + where + neqPred :: BoolCmp2 sym + neqPred e1 e2 = do + e <- WI.eqPred sym e1 e2 + WI.notPred sym e + + bvNeq :: forall w . BVCmp2 sym w + bvNeq e1 e2 = do + e <- WI.bvEq sym e1 e2 + WI.notPred sym e + + fpNeq :: forall fi . FPCmp2 sym fi + fpNeq _ e1 e2 = do + e <- WFP.iFloatEq @_ @fi sym e1 e2 + WI.notPred sym 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 xe1 xe2 = do + -- These partial pattern matches on Just should always succeed because + -- BwShiftL should always have bitvectors as arguments. + Just (SomeBVExpr e1 w1 sgn1 ctor1) <- return $ asBVExpr xe1 + Just (SomeBVExpr e2 w2 _ _ ) <- return $ asBVExpr xe2 + + e2' <- liftIO $ case testNatCases w1 w2 of + NatCaseLT LeqProof -> WI.bvTrunc sym w1 e2 + NatCaseEQ -> return e2 + NatCaseGT LeqProof -> WI.bvZext sym w1 e2 + res <- liftIO $ WI.bvShl sym e1 e2' + + -- The second argument should not be greater than or equal to the bit + -- width + wBV <- liftIO $ WI.bvLit sym w1 $ BV.width w1 + notTooLarge <- liftIO $ WI.bvUlt sym e2' wBV + addSidePred notTooLarge + + case sgn1 of + Unsigned -> do + -- Non-zero bits should not be shifted out + otherDirection <- liftIO $ WI.bvLshr sym res e2' + noWrap <- liftIO $ WI.bvEq sym e1 otherDirection + addSidePred noWrap + Signed -> do + -- Bits that disagree with the sign bit should not be shifted out + otherDirection <- liftIO $ WI.bvAshr sym res e2' + noWrap <- liftIO $ WI.bvEq sym e1 otherDirection + addSidePred noWrap + + return $ ctor1 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 xe1 xe2 = do + -- These partial pattern matches on Just should always succeed because + -- BwShiftL should always have bitvectors as arguments. + Just (SomeBVExpr e1 w1 sgn1 ctor1) <- return $ asBVExpr xe1 + Just (SomeBVExpr e2 w2 _ _ ) <- return $ asBVExpr xe2 + + e2' <- liftIO $ case testNatCases w1 w2 of + NatCaseLT LeqProof -> WI.bvTrunc sym w1 e2 + NatCaseEQ -> return e2 + NatCaseGT LeqProof -> WI.bvZext sym w1 e2 + + -- The second argument should not be greater than or equal to the bit + -- width + wBV <- liftIO $ WI.bvLit sym w1 $ BV.width w1 + notTooLarge <- liftIO $ WI.bvUlt sym e2' wBV + addSidePred notTooLarge + + liftIO $ fmap ctor1 $ case sgn1 of + Signed -> WI.bvAshr sym e1 e2' + Unsigned -> WI.bvLshr sym e1 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 xe1 xe2 = case (xe1, xe2) of + (XArray xes, XWord32 ix) -> do + -- The second argument should not be out of bounds (i.e., greater than + -- or equal to the length of the array) + xesLenBV <- liftIO $ WI.bvLit sym knownNat $ BV.mkBV knownNat + $ toInteger $ V.lengthInt xes + inRange <- liftIO $ WI.bvUlt sym ix xesLenBV + addSidePred inRange + + liftIO $ buildIndexExpr sym ix xes + _ -> unexpectedValues "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 bvOp fpOp xe1 xe2 = case (xe1, xe2) of + (XInt8 e1, XInt8 e2) -> XInt8 <$> bvOp e1 e2 + (XInt16 e1, XInt16 e2) -> XInt16 <$> bvOp e1 e2 + (XInt32 e1, XInt32 e2) -> XInt32 <$> bvOp e1 e2 + (XInt64 e1, XInt64 e2) -> XInt64 <$> bvOp e1 e2 + (XWord8 e1, XWord8 e2) -> XWord8 <$> bvOp e1 e2 + (XWord16 e1, XWord16 e2) -> XWord16 <$> bvOp e1 e2 + (XWord32 e1, XWord32 e2) -> XWord32 <$> bvOp e1 e2 + (XWord64 e1, XWord64 e2) -> XWord64 <$> bvOp e1 e2 + (XFloat e1, XFloat e2) -> XFloat <$> fpOp WFP.SingleFloatRepr e1 e2 + (XDouble e1, XDouble e2) -> XDouble <$> fpOp WFP.DoubleFloatRepr e1 e2 + _ -> unexpectedValues "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 opS opU xe1 xe2 = case (xe1, xe2) of + (XInt8 e1, XInt8 e2) -> XInt8 <$> opS e1 e2 + (XInt16 e1, XInt16 e2) -> XInt16 <$> opS e1 e2 + (XInt32 e1, XInt32 e2) -> XInt32 <$> opS e1 e2 + (XInt64 e1, XInt64 e2) -> XInt64 <$> opS e1 e2 + (XWord8 e1, XWord8 e2) -> XWord8 <$> opU e1 e2 + (XWord16 e1, XWord16 e2) -> XWord16 <$> opU e1 e2 + (XWord32 e1, XWord32 e2) -> XWord32 <$> opU e1 e2 + (XWord64 e1, XWord64 e2) -> XWord64 <$> opU e1 e2 + _ -> unexpectedValues "bvOp" + + fpOp :: (forall fi . FPOp2 sym fi) + -> XExpr sym + -> XExpr sym + -> IO (XExpr sym) + fpOp op xe1 xe2 = case (xe1, xe2) of + (XFloat e1, XFloat e2) -> XFloat <$> op WFP.SingleFloatRepr e1 e2 + (XDouble e1, XDouble e2) -> XDouble <$> op WFP.DoubleFloatRepr e1 e2 + _ -> unexpectedValues "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 fn = fpOp (\fiRepr -> WFP.iFloatSpecialFunction2 sym fiRepr 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 boolOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of + (XBool e1, XBool e2) -> XBool <$> boolOp e1 e2 + (XInt8 e1, XInt8 e2) -> XBool <$> bvOp e1 e2 + (XInt16 e1, XInt16 e2) -> XBool <$> bvOp e1 e2 + (XInt32 e1, XInt32 e2) -> XBool <$> bvOp e1 e2 + (XInt64 e1, XInt64 e2) -> XBool <$> bvOp e1 e2 + (XWord8 e1, XWord8 e2) -> XBool <$> bvOp e1 e2 + (XWord16 e1, XWord16 e2) -> XBool <$> bvOp e1 e2 + (XWord32 e1, XWord32 e2) -> XBool <$> bvOp e1 e2 + (XWord64 e1, XWord64 e2) -> XBool <$> bvOp e1 e2 + (XFloat e1, XFloat e2) -> XBool <$> fpOp WFP.SingleFloatRepr e1 e2 + (XDouble e1, XDouble e2) -> XBool <$> fpOp WFP.DoubleFloatRepr e1 e2 + _ -> unexpectedValues "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 bvSOp bvUOp fpOp xe1 xe2 = case (xe1, xe2) of + (XInt8 e1, XInt8 e2) -> XBool <$> bvSOp e1 e2 + (XInt16 e1, XInt16 e2) -> XBool <$> bvSOp e1 e2 + (XInt32 e1, XInt32 e2) -> XBool <$> bvSOp e1 e2 + (XInt64 e1, XInt64 e2) -> XBool <$> bvSOp e1 e2 + (XWord8 e1, XWord8 e2) -> XBool <$> bvUOp e1 e2 + (XWord16 e1, XWord16 e2) -> XBool <$> bvUOp e1 e2 + (XWord32 e1, XWord32 e2) -> XBool <$> bvUOp e1 e2 + (XWord64 e1, XWord64 e2) -> XBool <$> bvUOp e1 e2 + (XFloat e1, XFloat e2) -> XBool <$> fpOp WFP.SingleFloatRepr e1 e2 + (XDouble e1, XDouble e2) -> XBool <$> fpOp WFP.DoubleFloatRepr e1 e2 + _ -> unexpectedValues "numCmp" + + -- A catch-all error message to use when translation cannot proceed. + unexpectedValues :: forall m x. + (Panic.HasCallStack, MonadIO m) + => String + -> m x + unexpectedValues op = + panic [ "Unexpected values in " ++ op ++ ": " ++ show (CP.ppExpr origExpr) + , show xe1, show 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 sym origExpr op xe1 xe2 xe3 = case (op, xe1, xe2, xe3) of + (CE.Mux _, XBool te, xe1, xe2) -> liftIO $ mkIte sym te xe1 xe2 + (CE.Mux _, _, _, _) -> unexpectedValues "mux operation" + where + unexpectedValues :: forall m x . (Panic.HasCallStack, MonadIO m) + => String -> m x + unexpectedValues op = + panic [ "Unexpected values in " ++ op ++ ":" + , show (CP.ppExpr origExpr), show xe1, show xe2, show 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 sym ix = loop 0 + where + loop :: forall n'. + (1 <= n') + => Word32 + -> V.Vector n' (XExpr sym) + -> IO (XExpr sym) + loop curIx xelts = case V.uncons xelts of + -- Base case, exactly one element left + (xe, Left Refl) -> return xe + -- Recursive case + (xe, Right xelts') -> do + LeqProof <- return $ V.nonEmpty xelts' + rstExpr <- loop (curIx+1) xelts' + curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx) + ixEq <- WI.bvEq sym curIxExpr ix + mkIte sym ixEq xe 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 sym pred xe1 xe2 = case (xe1, xe2) of + (XBool e1, XBool e2) -> XBool <$> WI.itePred sym pred e1 e2 + (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym pred e1 e2 + (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym pred e1 e2 + (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym pred e1 e2 + (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym pred e1 e2 + (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym pred e1 e2 + (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym pred e1 e2 + (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym pred e1 e2 + (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym pred e1 e2 + (XFloat e1, XFloat e2) -> + XFloat <$> WFP.iFloatIte @_ @WFP.SingleFloat sym pred e1 e2 + (XDouble e1, XDouble e2) -> + XDouble <$> WFP.iFloatIte @_ @WFP.DoubleFloat sym pred e1 e2 + (XStruct xes1, XStruct xes2) -> + XStruct <$> zipWithM (mkIte sym pred) xes1 xes2 + (XEmptyArray, XEmptyArray) -> return XEmptyArray + (XArray xes1, XArray xes2) -> + case V.length xes1 `testEquality` V.length xes2 of + Just Refl -> XArray <$> V.zipWithM (mkIte sym pred) xes1 xes2 + Nothing -> panic [ "Array length mismatch in ite" + , show (V.length xes1) + , show (V.length xes2) + ] + _ -> panic ["Unexpected values in ite", show xe1, show 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 sym origExpr tp xe = case (xe, tp) of + -- "safe" casts that cannot lose information + (XBool _, CT.Bool) -> return xe + (XBool e, CT.Word8) -> XWord8 <$> WI.predToBV sym e knownNat + (XBool e, CT.Word16) -> XWord16 <$> WI.predToBV sym e knownNat + (XBool e, CT.Word32) -> XWord32 <$> WI.predToBV sym e knownNat + (XBool e, CT.Word64) -> XWord64 <$> WI.predToBV sym e knownNat + (XBool e, CT.Int8) -> XInt8 <$> WI.predToBV sym e knownNat + (XBool e, CT.Int16) -> XInt16 <$> WI.predToBV sym e knownNat + (XBool e, CT.Int32) -> XInt32 <$> WI.predToBV sym e knownNat + (XBool e, CT.Int64) -> XInt64 <$> WI.predToBV sym e knownNat + + (XInt8 _, CT.Int8) -> return xe + (XInt8 e, CT.Int16) -> XInt16 <$> WI.bvSext sym knownNat e + (XInt8 e, CT.Int32) -> XInt32 <$> WI.bvSext sym knownNat e + (XInt8 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e + (XInt16 _, CT.Int16) -> return xe + (XInt16 e, CT.Int32) -> XInt32 <$> WI.bvSext sym knownNat e + (XInt16 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e + (XInt32 _, CT.Int32) -> return xe + (XInt32 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e + (XInt64 _, CT.Int64) -> return xe + + (XWord8 e, CT.Int16) -> XInt16 <$> WI.bvZext sym knownNat e + (XWord8 e, CT.Int32) -> XInt32 <$> WI.bvZext sym knownNat e + (XWord8 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e + (XWord8 _, CT.Word8) -> return xe + (XWord8 e, CT.Word16) -> XWord16 <$> WI.bvZext sym knownNat e + (XWord8 e, CT.Word32) -> XWord32 <$> WI.bvZext sym knownNat e + (XWord8 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e + (XWord16 e, CT.Int32) -> XInt32 <$> WI.bvZext sym knownNat e + (XWord16 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e + (XWord16 _, CT.Word16) -> return xe + (XWord16 e, CT.Word32) -> XWord32 <$> WI.bvZext sym knownNat e + (XWord16 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e + (XWord32 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e + (XWord32 _, CT.Word32) -> return xe + (XWord32 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e + (XWord64 _, CT.Word64) -> return xe + + -- "unsafe" casts, which may lose information + -- unsigned truncations + (XWord64 e, CT.Word32) -> XWord32 <$> WI.bvTrunc sym knownNat e + (XWord64 e, CT.Word16) -> XWord16 <$> WI.bvTrunc sym knownNat e + (XWord64 e, CT.Word8) -> XWord8 <$> WI.bvTrunc sym knownNat e + (XWord32 e, CT.Word16) -> XWord16 <$> WI.bvTrunc sym knownNat e + (XWord32 e, CT.Word8) -> XWord8 <$> WI.bvTrunc sym knownNat e + (XWord16 e, CT.Word8) -> XWord8 <$> WI.bvTrunc sym knownNat e + + -- signed truncations + (XInt64 e, CT.Int32) -> XInt32 <$> WI.bvTrunc sym knownNat e + (XInt64 e, CT.Int16) -> XInt16 <$> WI.bvTrunc sym knownNat e + (XInt64 e, CT.Int8) -> XInt8 <$> WI.bvTrunc sym knownNat e + (XInt32 e, CT.Int16) -> XInt16 <$> WI.bvTrunc sym knownNat e + (XInt32 e, CT.Int8) -> XInt8 <$> WI.bvTrunc sym knownNat e + (XInt16 e, CT.Int8) -> XInt8 <$> WI.bvTrunc sym knownNat e + + -- signed integer to float + (XInt64 e, CT.Float) -> + XFloat <$> WFP.iSBVToFloat sym WFP.SingleFloatRepr fpRM e + (XInt32 e, CT.Float) -> + XFloat <$> WFP.iSBVToFloat sym WFP.SingleFloatRepr fpRM e + (XInt16 e, CT.Float) -> + XFloat <$> WFP.iSBVToFloat sym WFP.SingleFloatRepr fpRM e + (XInt8 e, CT.Float) -> + XFloat <$> WFP.iSBVToFloat sym WFP.SingleFloatRepr fpRM e + + -- unsigned integer to float + (XWord64 e, CT.Float) -> + XFloat <$> WFP.iBVToFloat sym WFP.SingleFloatRepr fpRM e + (XWord32 e, CT.Float) -> + XFloat <$> WFP.iBVToFloat sym WFP.SingleFloatRepr fpRM e + (XWord16 e, CT.Float) -> + XFloat <$> WFP.iBVToFloat sym WFP.SingleFloatRepr fpRM e + (XWord8 e, CT.Float) -> + XFloat <$> WFP.iBVToFloat sym WFP.SingleFloatRepr fpRM e + + -- signed integer to double + (XInt64 e, CT.Double) -> + XDouble <$> WFP.iSBVToFloat sym WFP.DoubleFloatRepr fpRM e + (XInt32 e, CT.Double) -> + XDouble <$> WFP.iSBVToFloat sym WFP.DoubleFloatRepr fpRM e + (XInt16 e, CT.Double) -> + XDouble <$> WFP.iSBVToFloat sym WFP.DoubleFloatRepr fpRM e + (XInt8 e, CT.Double) -> + XDouble <$> WFP.iSBVToFloat sym WFP.DoubleFloatRepr fpRM e + + -- unsigned integer to double + (XWord64 e, CT.Double) -> + XDouble <$> WFP.iBVToFloat sym WFP.DoubleFloatRepr fpRM e + (XWord32 e, CT.Double) -> + XDouble <$> WFP.iBVToFloat sym WFP.DoubleFloatRepr fpRM e + (XWord16 e, CT.Double) -> + XDouble <$> WFP.iBVToFloat sym WFP.DoubleFloatRepr fpRM e + (XWord8 e, CT.Double) -> + XDouble <$> WFP.iBVToFloat sym WFP.DoubleFloatRepr fpRM e + + -- unsigned to signed conversion + (XWord64 e, CT.Int64) -> return $ XInt64 e + (XWord32 e, CT.Int32) -> return $ XInt32 e + (XWord16 e, CT.Int16) -> return $ XInt16 e + (XWord8 e, CT.Int8) -> return $ XInt8 e + + -- signed to unsigned conversion + (XInt64 e, CT.Word64) -> return $ XWord64 e + (XInt32 e, CT.Word32) -> return $ XWord32 e + (XInt16 e, CT.Word16) -> return $ XWord16 e + (XInt8 e, CT.Word8) -> return $ XWord8 e + + _ -> panic ["Could not compute cast", show (CP.ppExpr origExpr), show 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 (XBool e) = "XBool " ++ show (WI.printSymExpr e) + show (XInt8 e) = "XInt8 " ++ show (WI.printSymExpr e) + show (XInt16 e) = "XInt16 " ++ show (WI.printSymExpr e) + show (XInt32 e) = "XInt32 " ++ show (WI.printSymExpr e) + show (XInt64 e) = "XInt64 " ++ show (WI.printSymExpr e) + show (XWord8 e) = "XWord8 " ++ show (WI.printSymExpr e) + show (XWord16 e) = "XWord16 " ++ show (WI.printSymExpr e) + show (XWord32 e) = "XWord32 " ++ show (WI.printSymExpr e) + show (XWord64 e) = "XWord64 " ++ show (WI.printSymExpr e) + show (XFloat e) = "XFloat " ++ show (WI.printSymExpr e) + show (XDouble e) = "XDouble " ++ show (WI.printSymExpr e) + show XEmptyArray = "[]" + show (XArray vs) = showList (V.toList vs) "" + show (XStruct xs) = "XStruct " ++ showList xs "" + +-- * 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 (Eq, Ord, Show) + +-- | Increment a stream offset by a drop amount. +addOffset :: StreamOffset -> CE.DropIdx -> StreamOffset +addOffset (AbsoluteOffset i) j = AbsoluteOffset (i + toInteger j) +addOffset (RelativeOffset i) j = RelativeOffset (i + toInteger j) + +-- * Auxiliary definitions + +-- | We assume round-near-even throughout, but this variable can be changed if +-- needed. +fpRM :: WI.RoundingMode +fpRM = WI.RNE + +data CopilotWhat4 = CopilotWhat4 + +instance Panic.PanicComponent CopilotWhat4 where + panicComponentName _ = "Copilot/What4 translation" + panicComponentIssues _ = "https://github.com/Copilot-Language/copilot/issues" + + {-# NOINLINE Panic.panicComponentRevision #-} + 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 msg = Panic.panic CopilotWhat4 "Copilot.Theorem.What4" msg