GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-28 02:15:31 +03:00
Code Issues Projects Releases Wiki Activity

Update for SBV 5.6

Browse Source
This commit is contained in:
Thomas M. DuBuisson 2015-12-10 12:38:26 -08:00
parent 3afdae127a
commit 1ffc086ed4
4 changed files with 15 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cryptol.cabal
View File

@ -60,7 +60,7 @@ library
process >= 1.2,
QuickCheck >= 2.7,
random >= 1.0.1,
sbv >= 5.5,
sbv >= 5.6,
smtLib >= 1.0.7,
simple-smt >= 0.6.0,
syb >= 0.4,

3
src/Cryptol/Symbolic.hs
View File

@ -19,6 +19,7 @@ import Data.List (transpose, intercalate)
import qualified Data.Map as Map
import qualified Control.Exception as X
import Data.SBV (intSizeOf)
import qualified Data.SBV.Dynamic as SBV
import qualified Cryptol.ModuleSystem as M hiding (getPrimMap)
@ -404,7 +405,7 @@ evalSel sel v =
ListSel n _ -> case v of
VWord s -> VBit (SBV.svTestBit s i)
where i = SBV.svBitSize s - 1 - n
where i = intSizeOf s - 1 - n
_ -> fromSeq v !! n -- 0-based indexing
-- Declarations ----------------------------------------------------------------

17
src/Cryptol/Symbolic/Prims.hs
View File

@ -24,6 +24,7 @@ import Cryptol.Utils.Panic
import Cryptol.ModuleSystem.Name (asPrim)
import Cryptol.Utils.Ident (Ident,mkIdent)
import qualified Data.SBV as SBV
import qualified Data.SBV.Dynamic as SBV
import qualified Data.Map as Map
import qualified Data.Text as T
@ -286,9 +287,9 @@ atV def vs i =
case foldr weave vs bits of
[] -> def
y : _ -> y
VWord x -> foldr f def (zip [0 .. 2 ^ SBV.svBitSize x - 1] vs)
VWord x -> foldr f def (zip [0 .. 2 ^ SBV.intSizeOf x - 1] vs)
where
k = SBV.svKind x
k = SBV.kindOf x
f (n, v) y = iteValue (SBV.svEqual x (SBV.svInteger k n)) v y
_ -> evalPanic "Cryptol.Symbolic.Prims.selectV" ["Invalid index argument"]
where
@ -315,7 +316,7 @@ nthV err v n =
case v of
VStream xs -> nth err xs (fromInteger n)
VSeq _ xs -> nth err xs (fromInteger n)
VWord x -> let i = SBV.svBitSize x - 1 - fromInteger n
VWord x -> let i = SBV.intSizeOf x - 1 - fromInteger n
in if i < 0 then err else
VBit (SBV.svTestBit x i)
_ -> err
@ -340,13 +341,13 @@ dropV n xs =
case xs of
VSeq b xs' -> VSeq b (genericDrop n xs')
VStream xs' -> VStream (genericDrop n xs')
VWord w -> VWord $ SBV.svExtract (SBV.svBitSize w - 1 - fromInteger n) 0 w
VWord w -> VWord $ SBV.svExtract (SBV.intSizeOf w - 1 - fromInteger n) 0 w
_ -> panic "Cryptol.Symbolic.Prims.dropV" [ "non-droppable value" ]
takeV :: Integer -> Value -> Value
takeV n xs =
case xs of
VWord w -> VWord $ SBV.svExtract (SBV.svBitSize w - 1) (SBV.svBitSize w - fromInteger n) w
VWord w -> VWord $ SBV.svExtract (SBV.intSizeOf w - 1) (SBV.intSizeOf w - fromInteger n) w
VSeq b xs' -> VSeq b (genericTake n xs')
VStream xs' -> VSeq b (genericTake n xs')
where b = case xs' of VBit _ : _ -> True
@ -423,7 +424,7 @@ arithUnary op = loop . toTypeVal
sExp :: SWord -> SWord -> SWord
sExp x y = go (reverse (unpackWord y)) -- bits in little-endian order
where go [] = literalSWord (SBV.svBitSize x) 1
where go [] = literalSWord (SBV.intSizeOf x) 1
go (b : bs) = SBV.svIte b (SBV.svTimes x s) s
where a = go bs
s = SBV.svTimes a a
@ -432,8 +433,8 @@ sExp x y = go (reverse (unpackWord y)) -- bits in little-endian order
sLg2 :: SWord -> SWord
sLg2 x = go 0
where
lit n = literalSWord (SBV.svBitSize x) n
go i | i < SBV.svBitSize x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1))
lit n = literalSWord (SBV.intSizeOf x) n
go i | i < SBV.intSizeOf x = SBV.svIte (SBV.svLessEq x (lit (2^i))) (lit (toInteger i)) (go (i + 1))
| otherwise = lit (toInteger i)
-- Cmp -------------------------------------------------------------------------

5
src/Cryptol/Symbolic/Value.hs
View File

@ -29,6 +29,7 @@ module Cryptol.Symbolic.Value
import Data.List (foldl')
import Data.SBV (HasKind(..))
import Data.SBV.Dynamic
import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit,
@ -92,7 +93,7 @@ mergeValue f c v1 v2 =
[ "mergeValue: incompatible values" ]
where
mergeBit b1 b2 = svSymbolicMerge KBool f c b1 b2
mergeWord w1 w2 = svSymbolicMerge (svKind w1) f c w1 w2
mergeWord w1 w2 = svSymbolicMerge (kindOf w1) f c w1 w2
mergeField (n1, x1) (n2, x2)
| n1 == n2 = (n1, mergeValue f c x1 x2)
| otherwise = panic "Cryptol.Symbolic.Value"
@ -104,7 +105,7 @@ mergeValue f c v1 v2 =
instance BitWord SBool SWord where
packWord bs = fromBitsLE (reverse bs)
unpackWord x = [ svTestBit x i | i <- reverse [0 .. svBitSize x - 1] ]
unpackWord x = [ svTestBit x i | i <- reverse [0 .. intSizeOf x - 1] ]
-- Errors ----------------------------------------------------------------------