From bf243886bb78d8e446162ea3ff2b40d74db229ba Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Mon, 10 May 2021 20:26:30 -0700 Subject: [PATCH] Adds support for what4 1.1 This commit makes the changes required to the what4 translation for what4-1.1 compatibility. There were two significant changes that affected Copilot.Theorem.What4. The first was the type of ExprSymFn changed trivially; it no longer requires (Expr t) as an argument. The second was that concrete floating point operations are now implemented, and the libBF library is used for that, so several types changed from raw bitvectors to libBF floats. --- lib/copilot-theorem/copilot-theorem.cabal | 3 +- .../src/Copilot/Theorem/What4.hs | 32 +++++++++++-------- 2 files changed, 20 insertions(+), 15 deletions(-) diff --git a/lib/copilot-theorem/copilot-theorem.cabal b/lib/copilot-theorem/copilot-theorem.cabal index 667df1248..05017db57 100644 --- a/lib/copilot-theorem/copilot-theorem.cabal +++ b/lib/copilot-theorem/copilot-theorem.cabal @@ -60,6 +60,7 @@ library , data-default >= 0.7 && < 0.8 , directory >= 1.3 && < 1.4 , filepath >= 1.4.2 && < 1.5 + , libBF >= 0.6.2 && < 0.7 , mtl >= 2.0 && < 2.3 , panic >= 0.4.0 && < 0.5 , parsec >= 2.0 && < 3.2 @@ -69,7 +70,7 @@ library , random >= 1.1 && < 1.2 , transformers >= 0.5 && < 0.6 , xml >= 1.3 && < 1.4 - , what4 >= 1.0 && < 1.2 + , what4 >= 1.1 && < 1.2 , copilot-core >= 3.2.1 && < 3.3 diff --git a/lib/copilot-theorem/src/Copilot/Theorem/What4.hs b/lib/copilot-theorem/src/Copilot/Theorem/What4.hs index ec5018c44..7607d2438 100644 --- a/lib/copilot-theorem/src/Copilot/Theorem/What4.hs +++ b/lib/copilot-theorem/src/Copilot/Theorem/What4.hs @@ -5,6 +5,7 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} @@ -90,7 +91,10 @@ import Data.Parameterized.Some import Data.Parameterized.SymbolRepr import qualified Data.Parameterized.Vector as V import Data.Word -import GHC.Float (castWord32ToFloat, castWord64ToDouble) +import LibBF ( bfToDouble + , bfFromDouble + , bfPosZero + , pattern NearEven ) import GHC.TypeNats (KnownNat) import qualified Panic as Panic @@ -215,11 +219,11 @@ data TransState t = TransState { -- stateful value. streams :: Map.Map CE.Id CS.Stream, -- | Binary power operator, represented as an uninterpreted function. - pow :: WB.ExprSymFn t (WB.Expr t) + pow :: WB.ExprSymFn t (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) WT.BaseRealType, -- | Binary logarithm operator, represented as an uninterpreted function. - logb :: WB.ExprSymFn t (WB.Expr t) + logb :: WB.ExprSymFn t (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) WT.BaseRealType } @@ -295,9 +299,9 @@ valFromExpr ge xe = case xe of XWord32 e -> Some . CopilotValue CT.Word32 . fromBV <$> WG.groundEval ge e XWord64 e -> Some . CopilotValue CT.Word64 . fromBV <$> WG.groundEval ge e XFloat e -> - Some . CopilotValue CT.Float . castWord32ToFloat . fromBV <$> WG.groundEval ge e + Some . CopilotValue CT.Float . realToFrac . fst . bfToDouble NearEven <$> WG.groundEval ge e XDouble e -> - Some . CopilotValue CT.Double . castWord64ToDouble . fromBV <$> WG.groundEval ge 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 @@ -351,8 +355,8 @@ translateConstExpr sym tp a = case tp of CT.Word16 -> XWord16 <$> WI.bvLit sym knownNat (BV.word16 a) CT.Word32 -> XWord32 <$> WI.bvLit sym knownNat (BV.word32 a) CT.Word64 -> XWord64 <$> WI.bvLit sym knownNat (BV.word64 a) - CT.Float -> XFloat <$> WI.floatLit sym knownRepr (toRational a) - CT.Double -> XDouble <$> WI.floatLit sym knownRepr (toRational a) + CT.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) @@ -560,7 +564,7 @@ translateOp1 sym op xe = case (op, xe) of neg_e <- WI.bvSub sym zero e WI.bvIte sym e_neg neg_e e fpAbs :: FPOp1 fpp t - fpAbs e = do zero <- WI.floatLit sym knownRepr 0 + 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 @@ -574,16 +578,16 @@ translateOp1 sym op xe = case (op, xe) of t <- WI.bvIte sym e_neg neg_one pos_one WI.bvIte sym e_zero zero t fpSign :: FPOp1 fpp t - fpSign e = do zero <- WI.floatLit sym knownRepr 0 - neg_one <- WI.floatLit sym knownRepr (-1) - pos_one <- WI.floatLit sym knownRepr 1 + 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 1 + 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 @@ -708,11 +712,11 @@ type FPCmp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFlo translateOp2 :: forall t st fs a b c . WB.ExprBuilder t st fs - -> (WB.ExprSymFn t (WB.Expr t) + -> (WB.ExprSymFn t (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) WT.BaseRealType) -- ^ Pow function - -> (WB.ExprSymFn t (WB.Expr t) + -> (WB.ExprSymFn t (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) WT.BaseRealType) -- ^ Logb function