GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-16 17:30:27 +03:00
Code Issues Projects Releases Wiki Activity

update to bv-sized branch of what4

Browse Source
This commit is contained in:
Ben Selfridge 2020-05-06 13:01:57 -07:00 committed by robdockins
parent 3de1e95808
commit 22d98c72b8
8 changed files with 13 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
cabal.GHC-8.4.4.config
View File

@ -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,

3
cabal.GHC-8.6.5.config
View File

@ -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,

3
cabal.GHC-8.8.3.config
View File

@ -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,

1
cabal.project
View File

@ -4,3 +4,4 @@ packages:
optional-packages:
dependencies/what4/what4

1
cryptol.cabal
View File

@ -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,

2
dependencies/what4 vendored

@ -1 +1 @@
Subproject commit 3a12e48f9e066ce99d7c29c16f067235abbfec31
Subproject commit 213b23099c1778c02ffd59554976fcb4891630d2

3
src/Cryptol/Eval/What4.hs
View File

@ -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

3
src/Cryptol/Symbolic/What4.hs
View File

@ -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')))