GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-05 15:07:12 +03:00
Code Issues Projects Releases Wiki Activity

Add operations for signed arithmetic, and carry condition testing.

Browse Source
This commit is contained in:
Robert Dockins 2017-08-02 16:39:07 -07:00
parent 08b334fce5
commit a68b835d51
3 changed files with 192 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

79
lib/Cryptol.cry
View File

@ -16,12 +16,12 @@ infixr 15 /\
infixr 20 ||
infixr 25 &&
infix 30 ==, ===, !=, !==
infix 40 >, >=, <, <=
infix 40 >, >=, <, <=, $<, $>, $<=, $>=
infixl 50 ^
infixr 60 #
infixl 70 <<, <<<, >>, >>>
infixl 70 <<, <<<, >>, >>>, $>>
infixl 80 +, -
infixl 90 *, /, %
infixl 90 *, /, %, $/, $%
infixr 95 ^^
infixl 100 @, @@, !, !!
@ -104,21 +104,29 @@ primitive complement : {a} a -> a
/**
* Less-than. Only works on comparable arguments.
*
* Bitvectors are compared using unsigned arithmetic.
*/
primitive (<) : {a} (Cmp a) => a -> a -> Bit
/**
* Greater-than of two comparable arguments.
*
* Bitvectors are compared using unsigned arithmetic.
*/
primitive (>) : {a} (Cmp a) => a -> a -> Bit
/**
* Less-than or equal of two comparable arguments.
*
* Bitvectors are compared using unsigned arithmetic.
*/
primitive (<=) : {a} (Cmp a) => a -> a -> Bit
/**
* Greater-than or equal of two comparable arguments.
*
* Bitvectors are compared using unsigned arithmetic.
*/
primitive (>=) : {a} (Cmp a) => a -> a -> Bit
@ -146,16 +154,71 @@ f !== g = \x -> f x != g x
/**
* Returns the smaller of two comparable arguments.
* Bitvectors are compared using unsigned arithmetic.
*/
min : {a} (Cmp a) => a -> a -> a
min x y = if x < y then x else y
/**
* Returns the greater of two comparable arguments.
* Bitvectors are compared using unsigned arithmetic.
*/
max : {a} (Cmp a) => a -> a -> a
max x y = if x > y then x else y
/**
* 2's complement signed less-than on bitvectors.
*/
primitive ($<) : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
/**
* 2's complement signed greater-than on bitvectors.
*/
($>) : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
x $> y = y $< x
/**
* 2's complement signed less-than-or-equal on bitvectors.
*/
($<=) : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
x $<= y = ~(y $< x)
/**
* 2's complement signed greater-than-or-equal on bitvectors.
*/
($>=) : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
x $>= y = ~(x $< y)
/**
* 2's complement signed division on bitvectors.
*/
primitive ($/) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
/**
* 2's complement signed modulus on bitvectors.
*/
primitive ($%) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
/**
* Unsigned carry. Returns true if the unsigned addition of the given
* bitvector arguments would result in an unsigned overflow.
*/
primitive carry : {n} (fin n) => [n] -> [n] -> Bit
/**
* Signed carry. Returns true if the 2's complement signed addition of the
* given bitvector arguments would result in a signed overflow.
*/
primitive scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
/**
* Signed borrow. Returns true if the 2's complement signed subtraction of the
* given bitvector arguments would result in a signed overflow.
*/
sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
sborrow x y = scarry x (negate y)
/**
* Short-cutting boolean conjuction function.
* If the first argument is False, the second argument
@ -225,6 +288,16 @@ primitive (<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
*/
primitive (>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
/**
* 2's complement signed (arithmetic) right shift. The first argument
* is the sequence to shift (considered as a signed value),
* the second argument is the number of positions to shift
* by (considered as an unsigned value).
*/
primitive ($>>) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n]
primitive (#) : {front, back, a} (fin front) => [front]a -> [back]a
-> [front + back] a

75
src/Cryptol/Prims/Eval.hs
View File

@ -84,6 +84,14 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
binary (cmpOrder "==" (\o -> o == EQ)))
, ("!=" , {-# SCC "Prelude::(!=)" #-}
binary (cmpOrder "!=" (\o -> o /= EQ)))
, ("$<" , {-# SCC "Prelude::($<)" #-}
liftSigned bvSlt)
, ("$/" , {-# SCC "Prelude::($/)" #-}
liftSigned bvSdiv)
, ("$%" , {-# SCC "Prelude::($%)" #-}
liftSigned bvSrem)
, ("$>>" , {-# SCC "Prelude::($>>)" #-}
liftWord bvSshr)
, ("&&" , {-# SCC "Prelude::(&&)" #-}
binary (logicBinary (.&.) (binBV (.&.))))
, ("||" , {-# SCC "Prelude::(||)" #-}
@ -103,6 +111,10 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
, ("True" , VBit True)
, ("False" , VBit False)
, ("carry" , {-# SCC "Prelude::carry" #-}
carryV)
, ("scarry" , {-# SCC "Prelude::scarry" #-}
scarryV)
, ("demote" , {-# SCC "Prelude::demote" #-}
ecDemoteV)
@ -522,6 +534,69 @@ funCmp op =
cmpOrder "funCmp" op b fl fr
-- Signed arithmetic -----------------------------------------------------------
-- | Lifted operation on finite bitsequences. Used
-- for signed comparisons and arithemtic.
liftWord :: BitWord b w
=> (w -> w -> Eval (GenValue b w))
-> GenValue b w
liftWord op =
nlam $ \_n ->
wlam $ \w1 -> return $
wlam $ \w2 -> op w1 w2
liftSigned :: (Integer -> Integer -> Integer -> Eval Value)
-> Value
liftSigned op = liftWord f
where
f (BV i x) (BV j y)
| i == j = op i sx sy
| otherwise = evalPanic "liftSigned" ["Attempt to compute with words of different sizes"]
where sx = if testBit x (fromIntegral (i-1)) then negate x else x
sy = if testBit y (fromIntegral (j-1)) then negate y else y
bvSlt :: Integer -> Integer -> Integer -> Eval Value
bvSlt _sz x y = return . VBit $! (x < y)
bvSdiv :: Integer -> Integer -> Integer -> Eval Value
bvSdiv _ _ 0 = divideByZero
bvSdiv sz x y = return . VWord sz . ready . WordVal $ mkBv sz (x `quot` y)
bvSrem :: Integer -> Integer -> Integer -> Eval Value
bvSrem _ _ 0 = divideByZero
bvSrem sz x y = return . VWord sz . ready . WordVal $ mkBv sz (x `rem` y)
bvSshr :: BV -> BV -> Eval Value
bvSshr (BV i x) y = return . VWord i . ready $ WordVal z
where sx = if testBit x (fromIntegral (i-1)) then negate x else x
z = mkBv i (sx `shiftR` (fromInteger (bvVal y)))
-- | Signed carry bit.
scarryV :: Value
scarryV =
nlam $ \_n ->
wlam $ \(BV i x) -> return $
wlam $ \(BV j y) ->
if i == j
then let z = x + y
xsign = testBit x (fromInteger i - 1)
ysign = testBit y (fromInteger i - 1)
zsign = testBit z (fromInteger i - 1)
sc = (xsign == ysign) && (xsign /= zsign)
in return $ VBit sc
else evalPanic "scarryV" ["Attempted to compute with words of different sizes"]
-- | Unsigned carry bit.
carryV :: Value
carryV =
nlam $ \_n ->
wlam $ \(BV i x) -> return $
wlam $ \(BV j y) ->
if i == j
then return . VBit $! testBit (x + y) (fromInteger i)
else evalPanic "carryV" ["Attempted to compute with words of different sizes"]
-- Logic -----------------------------------------------------------------------
zeroV :: forall b w

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

@ -38,7 +38,7 @@ import Cryptol.Prims.Eval (binary, unary, arithUnary,
reverseV, infFromV, infFromThenV,
fromThenV, fromToV, fromThenToV,
transposeV, indexPrimOne, indexPrimMany,
ecDemoteV, updatePrim, randomV)
ecDemoteV, updatePrim, randomV, liftWord)
import Cryptol.Symbolic.Value
import Cryptol.TypeCheck.AST (Decl(..))
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
@ -92,6 +92,10 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
, (">=" , binary (cmpBinary cmpGtEq cmpGtEq SBV.svTrue))
, ("==" , binary (cmpBinary cmpEq cmpEq SBV.svTrue))
, ("!=" , binary (cmpBinary cmpNotEq cmpNotEq SBV.svFalse))
, ("$<" , liftWord swordSlt)
, ("$/" , liftWord swordSdiv)
, ("$%" , liftWord swordSrem)
, ("$>>" , liftWord swordSshr)
, ("&&" , binary (logicBinary SBV.svAnd SBV.svAnd))
, ("||" , binary (logicBinary SBV.svOr SBV.svOr))
, ("^" , binary (logicBinary SBV.svXOr SBV.svXOr))
@ -122,6 +126,9 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
Inf -> evalPanic "cannot rotate infinite sequence" []
Nat n -> Just ((i+n-shft) `mod` n)))
, ("carry" , liftWord carry)
, ("scarry" , liftWord scarry)
, ("#" , -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d
nlam $ \ front ->
nlam $ \ back ->
@ -519,6 +526,39 @@ cmpBinary :: (SBool -> SBool -> Eval SBool -> Eval SBool)
-> SBool -> Binary SBool SWord
cmpBinary fb fw b _ty v1 v2 = VBit <$> cmpValue fb fw v1 v2 (return b)
-- Signed arithmetic -----------------------------------------------------------
swordSlt :: SWord -> SWord -> Eval Value
swordSlt x y = return $ VBit lt
where lt = SBV.svLessThan (SBV.svSign x) (SBV.svSign y)
swordSshr :: SWord -> SWord -> Eval Value
swordSshr x y = return . VWord (toInteger (SBV.intSizeOf x)) . ready . WordVal $ z
where z = SBV.svShiftRight (SBV.svSign x) y
swordSdiv :: SWord -> SWord -> Eval Value
swordSdiv x y = return . VWord (toInteger (SBV.intSizeOf x)) . ready . WordVal $ z
where z = SBV.svQuot (SBV.svSign x) (SBV.svSign y)
swordSrem :: SWord -> SWord -> Eval Value
swordSrem x y = return . VWord (toInteger (SBV.intSizeOf x)) . ready . WordVal $ z
where z = SBV.svRem (SBV.svSign x) (SBV.svSign y)
carry :: SWord -> SWord -> Eval Value
carry x y = return $ VBit c
where
c = SBV.svLessThan (SBV.svPlus x y) x
scarry :: SWord -> SWord -> Eval Value
scarry x y = return $ VBit sc
where
n = SBV.intSizeOf x
z = SBV.svPlus (SBV.svSign x) (SBV.svSign y)
xsign = SBV.svTestBit x (n-1)
ysign = SBV.svTestBit y (n-1)
zsign = SBV.svTestBit z (n-1)
sc = SBV.svAnd (SBV.svEqual xsign ysign) (SBV.svNotEqual xsign zsign)
-- Polynomials -----------------------------------------------------------------
-- TODO: Data.SBV.BitVectors.Polynomials should export ites, addPoly,