From 22d98c72b8cbf93f57b54b3a339580d617851058 Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Wed, 6 May 2020 13:01:57 -0700 Subject: [PATCH] update to bv-sized branch of what4 --- cabal.GHC-8.4.4.config | 3 ++- cabal.GHC-8.6.5.config | 3 ++- cabal.GHC-8.8.3.config | 3 ++- cabal.project | 1 + cryptol.cabal | 1 + dependencies/what4 | 2 +- src/Cryptol/Eval/What4.hs | 3 ++- src/Cryptol/Symbolic/What4.hs | 3 ++- 8 files changed, 13 insertions(+), 6 deletions(-) diff --git a/cabal.GHC-8.4.4.config b/cabal.GHC-8.4.4.config index 606f3c4c..5563b175 100644 --- a/cabal.GHC-8.4.4.config +++ b/cabal.GHC-8.4.4.config @@ -37,6 +37,7 @@ constraints: any.Cabal ==2.2.0.1, any.blaze-builder ==0.4.1.0, any.blaze-html ==0.9.1.2, any.blaze-markup ==0.8.2.5, + any.bv-sized ==1.0.0, any.bytestring ==0.10.8.2, any.bytestring-builder ==0.10.8.2.0, bytestring-builder +bytestring_has_builder, @@ -137,7 +138,7 @@ constraints: any.Cabal ==2.2.0.1, any.optparse-applicative ==0.15.1.0, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, - any.parameterized-utils ==2.0.2, + any.parameterized-utils ==2.1.0, parameterized-utils +unsafe-operations, any.parsec ==3.1.13.0, any.parser-combinators ==1.2.1, diff --git a/cabal.GHC-8.6.5.config b/cabal.GHC-8.6.5.config index 1ae7275e..96e2e11f 100644 --- a/cabal.GHC-8.6.5.config +++ b/cabal.GHC-8.6.5.config @@ -37,6 +37,7 @@ constraints: any.Cabal ==2.4.0.1, any.blaze-builder ==0.4.1.0, any.blaze-html ==0.9.1.2, any.blaze-markup ==0.8.2.5, + any.bv-sized ==1.0.0, any.bytestring ==0.10.8.2, any.bytestring-builder ==0.10.8.2.0, bytestring-builder +bytestring_has_builder, @@ -138,7 +139,7 @@ constraints: any.Cabal ==2.4.0.1, any.optparse-applicative ==0.15.1.0, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, - any.parameterized-utils ==2.0.2, + any.parameterized-utils ==2.1.0, parameterized-utils +unsafe-operations, any.parsec ==3.1.13.0, any.parser-combinators ==1.2.1, diff --git a/cabal.GHC-8.8.3.config b/cabal.GHC-8.8.3.config index 9feaa40b..8563b993 100644 --- a/cabal.GHC-8.8.3.config +++ b/cabal.GHC-8.8.3.config @@ -37,6 +37,7 @@ constraints: any.Cabal ==3.0.1.0, any.blaze-builder ==0.4.1.0, any.blaze-html ==0.9.1.2, any.blaze-markup ==0.8.2.5, + any.bv-sized ==1.0.0, any.bytestring ==0.10.10.0, any.bytestring-builder ==0.10.8.2.0, bytestring-builder +bytestring_has_builder, @@ -138,7 +139,7 @@ constraints: any.Cabal ==3.0.1.0, any.optparse-applicative ==0.15.1.0, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, - any.parameterized-utils ==2.0.2, + any.parameterized-utils ==2.1.0, parameterized-utils +unsafe-operations, any.parsec ==3.1.14.0, any.parser-combinators ==1.2.1, diff --git a/cabal.project b/cabal.project index 8e43e3e1..59b7dffd 100644 --- a/cabal.project +++ b/cabal.project @@ -4,3 +4,4 @@ packages: optional-packages: dependencies/what4/what4 + diff --git a/cryptol.cabal b/cryptol.cabal index aed0ae5e..a2026664 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -44,6 +44,7 @@ library Haskell2010 Build-depends: base >= 4.8 && < 5, base-compat >= 0.6 && < 0.12, + bv-sized >= 1.0 && < 1.1, bytestring >= 0.10, array >= 0.4, containers >= 0.5, diff --git a/dependencies/what4 b/dependencies/what4 index 3a12e48f..213b2309 160000 --- a/dependencies/what4 +++ b/dependencies/what4 @@ -1 +1 @@ -Subproject commit 3a12e48f9e066ce99d7c29c16f067235abbfec31 +Subproject commit 213b23099c1778c02ffd59554976fcb4891630d2 diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs index 9faa7353..571a37f8 100644 --- a/src/Cryptol/Eval/What4.hs +++ b/src/Cryptol/Eval/What4.hs @@ -28,6 +28,7 @@ import qualified Control.Exception as X import Control.Monad (foldM, join) import Control.Monad.IO.Class import Data.Bits (bit, shiftR, shiftL, testBit) +import qualified Data.BitVector.Sized as BV import Data.List import qualified Data.Map as Map import Data.Parameterized.NatRepr @@ -157,7 +158,7 @@ instance W4.IsExprBuilder sym => Backend (What4 sym) where | Just (Some w) <- someNat intw = case isPosNat w of Nothing -> pure $ SW.ZBV - Just LeqProof -> SW.DBV <$> liftIO (W4.bvLit sym w i) + Just LeqProof -> SW.DBV <$> liftIO (W4.bvLit sym w (BV.mkBV w i)) | otherwise = panic "what4: wordLit" ["invalid bit width:", show intw ] wordAsLit _ v diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs index 4e7d1e0e..4bbe60ac 100644 --- a/src/Cryptol/Symbolic/What4.hs +++ b/src/Cryptol/Symbolic/What4.hs @@ -58,6 +58,7 @@ import qualified What4.SWord as SW import What4.Solver import qualified What4.Solver.Adapter as W4 +import qualified Data.BitVector.Sized as BV import Data.Parameterized.Nonce @@ -398,7 +399,7 @@ varToConcreteValue evalFn v = pure (Eval.VWord 0 (pure (Eval.WordVal (Concrete.mkBv 0 0)))) VarWord (SW.DBV x) -> do let w = W4.intValue (W4.bvWidth x) - Eval.VWord w . pure . Eval.WordVal . Concrete.mkBv w <$> W4.groundEval evalFn x + Eval.VWord w . pure . Eval.WordVal . Concrete.mkBv w . BV.asUnsigned <$> W4.groundEval evalFn x VarFinSeq n vs -> do vs' <- mapM (varToConcreteValue evalFn) vs pure (Eval.VSeq (toInteger n) (Eval.finiteSeqMap Concrete.Concrete (map pure vs')))