GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 01:13:34 +03:00
Code Issues Projects Releases Wiki Activity

Update for SBV 5.7

Browse Source 
Conflicts:
	cryptol.cabal
	src/Cryptol/Symbolic.hs
	src/Cryptol/Symbolic/Prims.hs
This commit is contained in:
Thomas M. DuBuisson 2015-12-10 12:38:26 -08:00 committed by Adam C. Foltzer
parent 579ccc96a0
commit 1c36537d78
4 changed files with 13 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cryptol.cabal
View File

@ -57,7 +57,7 @@ library
process >= 1.2,
QuickCheck >= 2.7,
random >= 1.0.1,
sbv >= 5.3 && < 5.4,
sbv >= 5.7,
smtLib >= 1.0.7,
syb >= 0.4,
text >= 1.1,

3
src/Cryptol/Symbolic.hs
View File

@ -415,7 +415,8 @@ evalSel sel v =
_ -> panic "Cryptol.Symbolic.evalSel" [ "Record selector applied to non-record" ]
ListSel n _ -> case v of
VWord s -> VBit (SBV.svTestBit s n)
VWord s -> VBit (SBV.svTestBit s i)
where i = SBV.intSizeOf s - 1 - n
_ -> fromSeq v !! n -- 0-based indexing
-- Declarations ----------------------------------------------------------------

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

@ -25,9 +25,8 @@ import Cryptol.Utils.Panic
import qualified Data.SBV.Dynamic as SBV
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif
import Prelude ()
import Prelude.Compat
traverseSnd :: Functor f => (a -> f b) -> (t, a) -> f (t, b)
traverseSnd f (x, y) = (,) x <$> f y
@ -317,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
@ -342,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
@ -425,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
@ -434,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 -------------------------------------------------------------------------

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

@ -92,7 +92,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 +104,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 ----------------------------------------------------------------------