Skip to content

Adds support for what4 1.1 #218

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
benjaminselfridge wants to merge 1 commit into from
Closed

Adds support for what4 1.1 #218

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion lib/copilot-theorem/copilot-theorem.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down
32 changes: 18 additions & 14 deletions lib/copilot-theorem/src/Copilot/Theorem/What4.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
}
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down