From a68b835d51da9f7f549b8df36f320614e442c540 Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Wed, 2 Aug 2017 16:39:07 -0700 Subject: [PATCH] Add operations for signed arithmetic, and carry condition testing. --- lib/Cryptol.cry | 79 +++++++++++++++++++++++++++++++++-- src/Cryptol/Prims/Eval.hs | 75 +++++++++++++++++++++++++++++++++ src/Cryptol/Symbolic/Prims.hs | 42 ++++++++++++++++++- 3 files changed, 192 insertions(+), 4 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 8513a4e5..2d740fc1 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -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 diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs index 12bbfce0..34d8a563 100644 --- a/src/Cryptol/Prims/Eval.hs +++ b/src/Cryptol/Prims/Eval.hs @@ -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 diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs index 2fccbda0..0f19dcda 100644 --- a/src/Cryptol/Symbolic/Prims.hs +++ b/src/Cryptol/Symbolic/Prims.hs @@ -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,