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

Merge pull request #439 from GaloisInc/signed-arith

Browse Source 
Add operations for signed arithmetic, and carry condition testing.
This commit is contained in:
robdockins 2017-08-17 10:27:18 -07:00 committed by GitHub
commit bbcd39d400
19 changed files with 468 additions and 170 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
docs/CryptolPrims.md
View File

@ -16,10 +16,26 @@ Comparisons and Ordering
instance Cmp Bit
// No instance for functions.
instance (Cmp a, fin n) => Cmp [n] a
instance (Cmp a, fin n) => Cmp [n]a
instance (Cmp a, Cmp b) => Cmp (a,b)
instance (Cmp a, Cmp b) => Cmp { x : a, y : b }
Signed Comparisons
---------------------
(<$) : {a} (SignedCmp a) => a -> a -> Bit
(>$) : {a} (SignedCmp a) => a -> a -> Bit
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
// No instance for Bit
// No instance for functions.
instance (fin n, n >= 1) => SignedCmp [n]
instance (SignedCmp a, fin n) => SignedCmp [n]a
// (for [n]a, where a is other than Bit)
instance (SignedCmp a, SignedCmp b) => SignedCmp (a,b)
instance (SignedCmp a, SignedCmp b) => SignedCmp { x : a, y : b }
Arithmetic
----------
@ -30,6 +46,8 @@ Arithmetic
(/) : {a} (Arith a) => a -> a -> a
(%) : {a} (Arith a) => a -> a -> a
(^^) : {a} (Arith a) => a -> a -> a
(/$) : {a} (Arith a) => a -> a -> a
(%$) : {a} (Arith a) => a -> a -> a
// No instance for `Bit`.
instance (fin n) => Arith ( [n] Bit)
@ -53,6 +71,10 @@ Boolean
(^) : a -> a -> a
(~) : a -> a
(==>) : Bit -> Bit -> Bit
(/\) : Bit -> Bit -> Bit
(\/) : Bit -> Bit -> Bit
Sequences
---------
@ -98,6 +120,8 @@ New types:
(<<<) : {n,a,m} (fin n) => [n]a -> [m] -> [n]a
(>>>) : {n,a,m} (fin n) => [n]a -> [m] -> [n]a
// Arithmetic shift only for bitvectors
(>>$) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n]
Random Values
-------------
@ -109,5 +133,6 @@ Debugging
undefined : {a} a
error : {n a} [n][8] -> a
trace : {n, a, b} [n][8] -> a -> b -> b
traceVal : {n, a} [n][8] -> a -> a
trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
traceVal : {n, a} (fin n) => [n][8] -> a -> a

BIN
docs/CryptolPrims.pdf
View File

Binary file not shown.

63
docs/Syntax.md
View File

@ -71,6 +71,7 @@ Bit
Cmp
False
Inf
SignedCmp
True
else
export
@ -92,30 +93,33 @@ where
width
--->
Arith Inf extern inf module then
Bit True fin lg2 newtype type
Cmp else if max pragma where
False export import min property width
Arith Inf export import min property width
Bit SignedCmp extern inf module then
Cmp True fin lg2 newtype type
False else if max pragma where
The following table contains Cryptol's operators and their
associativity with lowest precedence operators first, and highest
precedence last.
Operator Associativity
--------------- -------------
`||` left
`^` left
`&&` left
`->` (types) right
`!=` `==` not associative
`>` `<` `<=` `>=` not associative
`#` right
`>>` `<<` `>>>` `<<<` left
`+` `-` left
`*` `/` `%` left
`^^` right
`!` `!!` `@` `@@` left
(unary) `-` `~` right
Operator Associativity
--------------- -------------
`==>` right
`\/` right
`/\` right
`||` right
`&&` right
`->` (types) right
`!=` `==` not associative
`>` `<` `<=` `>=` `<$` `>$` `<=$` `>=$` not associative
`^` left
`#` right
`>>` `<<` `>>>` `<<<` `>>$` left
`+` `-` left
`*` `/` `%` `/$` `%$` left
`^^` right
`!` `!!` `@` `@@` left
(unary) `-` `~` right
Table: Operator precedences.
@ -159,14 +163,17 @@ The type `Bit` has two inhabitants: `True` and `False`. These values
may be combined using various logical operators, or constructed as
results of comparisons.
Operator Associativity Description
--------------------- ------------- -----------
`||` left Logical or
`^` left Exclusive-or
`&&` left Logical and
`!=` `==` none Not equals, equals
`>` `<` `<=` `>=` none Comparisons
`~` right Logical negation
Operator Associativity Description
--------------------- ------------- -----------
`==>` right Short-cut implication
`\/` right Short-cut or
`/\` right Short-cut and
`||` right Logical or
`&&` right Logical and
`!=` `==` none Not equals, equals
`>` `<` `<=` `>=` `<$` `>$` `<=$` `>=$` none Comparisons
`^` left Exclusive-or
`~` right Logical negation
Table: Bit operations.
@ -276,6 +283,7 @@ Operator Description
`#` Sequence concatenation
`>>` `<<` Shift (right,left)
`>>>` `<<<` Rotate (right,left)
`>>$` Arithmetic right shift (on bitvectors only)
`@` `!` Access elements (front,back)
`@@` `!!` Access sub-sequence (front,back)
`update` `updateEnd` Update the value of a sequence at a location (front,back)
@ -351,4 +359,3 @@ Type Synonym Declarations
=========================
type T a b = [a] b

BIN
docs/Syntax.pdf
View File

Binary file not shown.

92
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,84 @@ 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.
*/
primitive (<$) : {a} (SignedCmp a) => a -> a -> Bit
/**
* 2's complement signed greater-than.
*/
(>$) : {a} (SignedCmp a) => a -> a -> Bit
x >$ y = y <$ x
/**
* 2's complement signed less-than-or-equal.
*/
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
x <=$ y = ~(y <$ x)
/**
* 2's complement signed greater-than-or-equal.
*/
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
x >=$ y = ~(x <$ y)
/**
* 2's complement signed division. Division rounds toward 0.
*/
primitive (/$) : {a} (Arith a) => a -> a -> a
/**
* 2's complement signed remainder. Division rounds toward 0.
*/
primitive (%$) : {a} (Arith a) => a -> a -> a
/**
* 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 = ( x <$ (x-y) ) ^ y@0
/**
* Zero extension of a bitvector.
*/
zext : {n, m} (fin m, m >= n) => [n] -> [m]
zext x = zero # x
/**
* Sign extension of a bitvector.
*/
sext : {n, m} (fin m, m >= n, n >= 1) => [n] -> [m]
sext x = newbits # x
where newbits = if x@0 then ~zero else zero
/**
* Short-cutting boolean conjuction function.
* If the first argument is False, the second argument
@ -225,6 +301,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

11
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -491,11 +491,12 @@ instance Rename TParam where
instance Rename Prop where
rename p = case p of
CFin t -> CFin <$> rename t
CEqual l r -> CEqual <$> rename l <*> rename r
CGeq l r -> CGeq <$> rename l <*> rename r
CArith t -> CArith <$> rename t
CCmp t -> CCmp <$> rename t
CFin t -> CFin <$> rename t
CEqual l r -> CEqual <$> rename l <*> rename r
CGeq l r -> CGeq <$> rename l <*> rename r
CArith t -> CArith <$> rename t
CCmp t -> CCmp <$> rename t
CSignedCmp t -> CSignedCmp <$> rename t
CLocated p' r -> withLoc r
$ CLocated <$> rename p' <*> pure r

4
src/Cryptol/Parser/AST.hs
View File

@ -374,6 +374,7 @@ data Prop n = CFin (Type n) -- ^ @ fin x @
| CGeq (Type n) (Type n) -- ^ @ x >= 10 @
| CArith (Type n) -- ^ @ Arith a @
| CCmp (Type n) -- ^ @ Cmp a @
| CSignedCmp (Type n) -- ^ @ SignedCmp a @
| CLocated (Prop n) Range -- ^ Location information
| CType (Type n) -- ^ After parsing
deriving (Eq, Show, Generic, NFData, Functor)
@ -824,6 +825,7 @@ instance PPName name => PP (Prop name) where
CFin t -> text "fin" <+> ppPrec 4 t
CArith t -> text "Arith" <+> ppPrec 4 t
CCmp t -> text "Cmp" <+> ppPrec 4 t
CSignedCmp t -> text "SignedCmp" <+> ppPrec 4 t
CEqual t1 t2 -> ppPrec 2 t1 <+> text "==" <+> ppPrec 2 t2
CGeq t1 t2 -> ppPrec 2 t1 <+> text ">=" <+> ppPrec 2 t2
CLocated c _ -> ppPrec n c
@ -981,6 +983,6 @@ instance NoPos (Prop name) where
CFin x -> CFin (noPos x)
CArith x -> CArith (noPos x)
CCmp x -> CCmp (noPos x)
CSignedCmp x -> CSignedCmp (noPos x)
CLocated c _ -> noPos c
CType t -> CType (noPos t)

1
src/Cryptol/Parser/LexerUtils.hs
View File

@ -361,6 +361,7 @@ data TokenW = BlockComment | LineComment | Space | DocStr
data TokenKW = KW_Arith
| KW_Bit
| KW_Cmp
| KW_SignedCmp
| KW_else
| KW_Eq
| KW_extern

1
src/Cryptol/Parser/Names.hs
View File

@ -263,6 +263,7 @@ tnamesC prop =
CGeq t1 t2 -> Set.union (tnamesT t1) (tnamesT t2)
CArith t -> tnamesT t
CCmp t -> tnamesT t
CSignedCmp t -> tnamesT t
CLocated p _ -> tnamesC p
CType t -> tnamesT t

18
src/Cryptol/Parser/ParserUtils.hs
View File

@ -428,14 +428,16 @@ mkProp ty =
-- these can be translated right away
prefixProp r f xs
| i == arithIdent, [x] <- xs = return [CLocated (CArith x) r]
| i == finIdent, [x] <- xs = return [CLocated (CFin x) r]
| i == cmpIdent, [x] <- xs = return [CLocated (CCmp x) r]
| otherwise = errorMessage r "Invalid constraint"
| i == arithIdent, [x] <- xs = return [CLocated (CArith x) r]
| i == finIdent, [x] <- xs = return [CLocated (CFin x) r]
| i == cmpIdent, [x] <- xs = return [CLocated (CCmp x) r]
| i == signedCmpIdent, [x] <- xs = return [CLocated (CSignedCmp x) r]
| otherwise = errorMessage r "Invalid constraint"
where
i = getIdent f
arithIdent, finIdent, cmpIdent :: Ident
arithIdent = mkIdent (S.pack "Arith")
finIdent = mkIdent (S.pack "fin")
cmpIdent = mkIdent (S.pack "Cmp")
arithIdent, finIdent, cmpIdent, signedCmpIdent :: Ident
arithIdent = mkIdent (S.pack "Arith")
finIdent = mkIdent (S.pack "fin")
cmpIdent = mkIdent (S.pack "Cmp")
signedCmpIdent = mkIdent (S.pack "SignedCmp")

217
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::(<$)" #-}
binary (signedCmpOrder "<$" (\o -> o == LT)))
, ("/$" , {-# SCC "Prelude::(/$)" #-}
binary (arithBinary (liftSigned bvSdiv)))
, ("%$" , {-# SCC "Prelude::(%$)" #-}
binary (arithBinary (liftSigned bvSrem)))
, (">>$" , {-# SCC "Prelude::(>>$)" #-}
sshrV)
, ("&&" , {-# 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)
@ -323,13 +335,18 @@ unary f = tlam $ \ ty ->
-- Arith -----------------------------------------------------------------------
-- | Turn a normal binop on Integers into one that can also deal with a bitsize.
-- However, if the bitvector size is 0, always return the 0
-- bitvector.
liftBinArith :: (Integer -> Integer -> Integer) -> BinArith BV
liftBinArith _ 0 _ _ = ready $ mkBv 0 0
liftBinArith op w (BV _ x) (BV _ y) = ready $ mkBv w $ op x y
-- | Turn a normal binop on Integers into one that can also deal with a bitsize.
-- Generate a thunk that throws a divide by 0 error when forced if the second
-- argument is 0.
-- argument is 0. However, if the bitvector size is 0, always return the 0
-- bitvector.
liftDivArith :: (Integer -> Integer -> Integer) -> BinArith BV
liftDivArith _ 0 _ _ = ready $ mkBv 0 0
liftDivArith _ _ _ (BV _ 0) = divideByZero
liftDivArith op w (BV _ x) (BV _ y) = ready $ mkBv w $ op x y
@ -447,80 +464,148 @@ lg2 i = case genLog i 2 of
-- Cmp -------------------------------------------------------------------------
-- | Lexicographic ordering on two values.
lexCompare :: String -> TValue -> Value -> Value -> Eval Ordering
lexCompare nm ty l r = case ty of
TVBit ->
return $ compare (fromVBit l) (fromVBit r)
TVSeq _ TVBit ->
compare <$> (fromWord "compareLeft" l) <*> (fromWord "compareRight" r)
TVSeq w e ->
join (zipLexCompare nm (repeat e) <$>
(enumerateSeqMap w <$> fromSeq "lexCompare left" l) <*>
(enumerateSeqMap w <$> fromSeq "lexCompare right" r))
-- tuples
TVTuple etys ->
zipLexCompare nm etys (fromVTuple l) (fromVTuple r)
-- records
TVRec fields ->
let tys = map snd (sortBy (comparing fst) fields)
ls = map snd (sortBy (comparing fst) (fromVRecord l))
rs = map snd (sortBy (comparing fst) (fromVRecord r))
in zipLexCompare nm tys ls rs
_ -> evalPanic "lexCompare" ["invalid type"]
-- XXX the lists are expected to be of the same length, as this should only be
-- used with values that come from type-correct expressions.
zipLexCompare :: String -> [TValue] -> [Eval Value] -> [Eval Value] -> Eval Ordering
zipLexCompare nm tys ls rs = foldr choose (return EQ) (zipWith3 lexCompare' tys ls rs)
cmpValue :: BitWord b w
=> (b -> b -> Eval a -> Eval a)
-> (w -> w -> Eval a -> Eval a)
-> (GenValue b w -> GenValue b w -> Eval a -> Eval a)
cmpValue fb fw = cmp
where
lexCompare' t l r = join (lexCompare nm t <$> l <*> r)
cmp v1 v2 k =
case (v1, v2) of
(VRecord fs1, VRecord fs2) -> let vals = map snd . sortBy (comparing fst)
in cmpValues (vals fs1) (vals fs2) k
(VTuple vs1 , VTuple vs2 ) -> cmpValues vs1 vs2 k
(VBit b1 , VBit b2 ) -> fb b1 b2 k
(VWord _ w1 , VWord _ w2 ) -> join (fw <$> (asWordVal =<< w1)
<*> (asWordVal =<< w2)
<*> return k)
(VSeq n vs1 , VSeq _ vs2 ) -> cmpValues (enumerateSeqMap n vs1)
(enumerateSeqMap n vs2) k
(VStream {} , VStream {} ) -> panic "Cryptol.Prims.Value.cmpValue"
[ "Infinite streams are not comparable" ]
(VFun {} , VFun {} ) -> panic "Cryptol.Prims.Value.cmpValue"
[ "Functions are not comparable" ]
(VPoly {} , VPoly {} ) -> panic "Cryptol.Prims.Value.cmpValue"
[ "Polymorphic values are not comparable" ]
(_ , _ ) -> panic "Cryptol.Prims.Value.cmpValue"
[ "type mismatch" ]
choose c acc = c >>= \c' -> case c' of
EQ -> acc
_ -> return c'
cmpValues (x1 : xs1) (x2 : xs2) k = do
x1' <- x1
x2' <- x2
cmp x1' x2' (cmpValues xs1 xs2 k)
cmpValues _ _ k = k
lexCompare :: Value -> Value -> Eval Ordering
lexCompare a b = cmpValue op opw a b (return EQ)
where
opw :: BV -> BV -> Eval Ordering -> Eval Ordering
opw x y k = op (bvVal x) (bvVal y) k
op :: Ord a => a -> a -> Eval Ordering -> Eval Ordering
op x y k = case compare x y of
EQ -> k
cmp -> return cmp
signedLexCompare :: Value -> Value -> Eval Ordering
signedLexCompare a b = cmpValue opb opw a b (return EQ)
where
opb :: Bool -> Bool -> Eval Ordering -> Eval Ordering
opb _x _y _k = panic "signedLexCompare"
["Attempted to perform signed comparisons on bare Bit type"]
opw :: BV -> BV -> Eval Ordering -> Eval Ordering
opw x y k = case compare (signedBV x) (signedBV y) of
EQ -> k
cmp -> return cmp
-- | Process two elements based on their lexicographic ordering.
cmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV
cmpOrder nm op ty l r = VBit . op <$> lexCompare nm ty l r
cmpOrder _nm op _ty l r = VBit . op <$> lexCompare l r
withOrder :: String -> (Ordering -> TValue -> Value -> Value -> Value) -> Binary Bool BV
withOrder nm choose ty l r =
do ord <- lexCompare nm ty l r
return $ choose ord ty l r
maxV :: Ordering -> TValue -> Value -> Value -> Value
maxV o _ l r = case o of
LT -> r
_ -> l
minV :: Ordering -> TValue -> Value -> Value -> Value
minV o _ l r = case o of
GT -> r
_ -> l
-- | Process two elements based on their lexicographic ordering, using signed comparisons
signedCmpOrder :: String -> (Ordering -> Bool) -> Binary Bool BV
signedCmpOrder _nm op _ty l r = VBit . op <$> signedLexCompare l r
funCmp :: (Ordering -> Bool) -> Value
funCmp op =
tlam $ \ _a ->
tlam $ \ b ->
lam $ \ l -> return $
lam $ \ r -> return $
lam $ \ x -> do
l' <- l
r' <- r
x' <- x
fl <- fromVFun l' (ready x')
fr <- fromVFun r' (ready x')
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 BV)
-> BinArith BV
liftSigned _ 0 = \_ _ -> return $ mkBv 0 0
liftSigned op size = f
where
f (BV i x) (BV j y)
| i == j && size == i = op size sx sy
| otherwise = evalPanic "liftSigned" ["Attempt to compute with words of different sizes"]
where sx = signedValue i x
sy = signedValue j y
signedBV :: BV -> Integer
signedBV (BV i x) = signedValue i x
signedValue :: Integer -> Integer -> Integer
signedValue i x = if testBit x (fromIntegral (i-1)) then x - (1 `shiftL` (fromIntegral i)) else x
bvSlt :: Integer -> Integer -> Integer -> Eval Value
bvSlt _sz x y = return . VBit $! (x < y)
bvSdiv :: Integer -> Integer -> Integer -> Eval BV
bvSdiv _ _ 0 = divideByZero
bvSdiv sz x y = return $! mkBv sz (x `quot` y)
bvSrem :: Integer -> Integer -> Integer -> Eval BV
bvSrem _ _ 0 = divideByZero
bvSrem sz x y = return $! mkBv sz (x `rem` y)
sshrV :: Value
sshrV =
nlam $ \_n ->
nlam $ \_k ->
wlam $ \(BV i x) -> return $
wlam $ \y ->
let signx = testBit x (fromIntegral (i-1))
amt = fromInteger (bvVal y)
negv = (((-1) `shiftL` amt) .|. x) `shiftR` amt
posv = x `shiftR` amt
in return . VWord i . ready . WordVal . mkBv i $! if signx then negv else posv
-- | 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 -----------------------------------------------------------------------

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

@ -20,8 +20,7 @@ module Cryptol.Symbolic.Prims where
import Control.Monad (unless)
import Data.Bits
import Data.List (genericTake, sortBy)
import Data.Ord (comparing)
import Data.List (genericTake)
import qualified Data.Sequence as Seq
import Cryptol.Eval.Monad (Eval(..), ready, invalidIndex, cryUserError)
@ -38,7 +37,8 @@ import Cryptol.Prims.Eval (binary, unary, arithUnary,
reverseV, infFromV, infFromThenV,
fromThenV, fromToV, fromThenToV,
transposeV, indexPrimOne, indexPrimMany,
ecDemoteV, updatePrim, randomV)
ecDemoteV, updatePrim, randomV, liftWord,
cmpValue)
import Cryptol.Symbolic.Value
import Cryptol.TypeCheck.AST (Decl(..))
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
@ -92,6 +92,11 @@ 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))
, ("<$" , let boolFail = evalPanic "<$" ["Attempted signed comparison on bare Bit values"]
in binary (cmpBinary boolFail cmpSignedLt SBV.svFalse))
, ("/$" , binary (arithBinary (liftBinArith signedQuot)))
, ("%$" , binary (arithBinary (liftBinArith signedRem)))
, (">>$" , sshrV)
, ("&&" , binary (logicBinary SBV.svAnd SBV.svAnd))
, ("||" , binary (logicBinary SBV.svOr SBV.svOr))
, ("^" , binary (logicBinary SBV.svXOr SBV.svXOr))
@ -122,6 +127,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 ->
@ -469,43 +477,17 @@ sLg2 _w x = ready $ go 0
-- Cmp -------------------------------------------------------------------------
cmpValue :: (SBool -> SBool -> Eval a -> Eval a)
-> (SWord -> SWord -> Eval a -> Eval a)
-> (Value -> Value -> Eval a -> Eval a)
cmpValue fb fw = cmp
where
cmp v1 v2 k =
case (v1, v2) of
(VRecord fs1, VRecord fs2) -> let vals = map snd . sortBy (comparing fst)
in cmpValues (vals fs1) (vals fs2) k
(VTuple vs1 , VTuple vs2 ) -> cmpValues vs1 vs2 k
(VBit b1 , VBit b2 ) -> fb b1 b2 k
(VWord _ w1 , VWord _ w2 ) -> join (fw <$> (asWordVal =<< w1)
<*> (asWordVal =<< w2)
<*> return k)
(VSeq n vs1 , VSeq _ vs2 ) -> cmpValues (enumerateSeqMap n vs1)
(enumerateSeqMap n vs2) k
(VStream {} , VStream {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
[ "Infinite streams are not comparable" ]
(VFun {} , VFun {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
[ "Functions are not comparable" ]
(VPoly {} , VPoly {} ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
[ "Polymorphic values are not comparable" ]
(_ , _ ) -> panic "Cryptol.Symbolic.Prims.cmpValue"
[ "type mismatch" ]
cmpValues (x1 : xs1) (x2 : xs2) k = do
x1' <- x1
x2' <- x2
cmp x1' x2' (cmpValues xs1 xs2 k)
cmpValues _ _ k = k
cmpEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpEq x y k = SBV.svAnd (SBV.svEqual x y) <$> k
cmpNotEq :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpNotEq x y k = SBV.svOr (SBV.svNotEqual x y) <$> k
cmpSignedLt :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpSignedLt x y k = SBV.svOr (SBV.svLessThan sx sy) <$> (cmpEq sx sy k)
where sx = SBV.svSign x
sy = SBV.svSign y
cmpLt, cmpGt :: SWord -> SWord -> Eval SBool -> Eval SBool
cmpLt x y k = SBV.svOr (SBV.svLessThan x y) <$> (cmpEq x y k)
cmpGt x y k = SBV.svOr (SBV.svGreaterThan x y) <$> (cmpEq x y k)
@ -519,6 +501,44 @@ 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 -----------------------------------------------------------
signedQuot :: SWord -> SWord -> SWord
signedQuot x y = SBV.svUnsign (SBV.svQuot (SBV.svSign x) (SBV.svSign y))
signedRem :: SWord -> SWord -> SWord
signedRem x y = SBV.svUnsign (SBV.svRem (SBV.svSign x) (SBV.svSign y))
sshrV :: Value
sshrV =
nlam $ \_n ->
nlam $ \_k ->
wlam $ \x -> return $
wlam $ \y ->
case SBV.svAsInteger y of
Just i ->
let z = SBV.svUnsign (SBV.svShr (SBV.svSign x) (fromInteger i))
in return . VWord (toInteger (SBV.intSizeOf x)) . ready . WordVal $ z
Nothing ->
let z = SBV.svUnsign (SBV.svShiftRight (SBV.svSign x) y)
in return . VWord (toInteger (SBV.intSizeOf x)) . ready . WordVal $ z
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,

1
src/Cryptol/TypeCheck/Kind.hs
View File

@ -317,6 +317,7 @@ checkProp prop =
P.CGeq t1 t2 -> tcon (PC PGeq) [t1,t2] (Just KProp)
P.CArith t1 -> tcon (PC PArith) [t1] (Just KProp)
P.CCmp t1 -> tcon (PC PCmp) [t1] (Just KProp)
P.CSignedCmp t1 -> tcon (PC PSignedCmp) [t1] (Just KProp)
P.CLocated p r1 -> kInRange r1 (checkProp p)
P.CType _ -> panic "checkProp" [ "Unexpected CType", show prop ]

3
src/Cryptol/TypeCheck/SimpleSolver.hs
View File

@ -7,7 +7,7 @@ import Cryptol.TypeCheck.Type hiding
import Cryptol.TypeCheck.Solver.Types
import Cryptol.TypeCheck.Solver.Numeric.Fin(cryIsFinType)
import Cryptol.TypeCheck.Solver.Numeric(cryIsEqual, cryIsNotEqual, cryIsGeq)
import Cryptol.TypeCheck.Solver.Class(solveArithInst,solveCmpInst)
import Cryptol.TypeCheck.Solver.Class(solveArithInst,solveCmpInst, solveSignedCmpInst)
import Cryptol.Utils.Debug(ppTrace)
import Cryptol.TypeCheck.PP
@ -38,6 +38,7 @@ simplifyStep ctxt prop =
TCon (PC PArith) [ty] -> solveArithInst ty
TCon (PC PCmp) [ty] -> solveCmpInst ty
TCon (PC PSignedCmp) [ty] -> solveSignedCmpInst ty
TCon (PC PFin) [ty] -> cryIsFinType ctxt ty

42
src/Cryptol/TypeCheck/Solver/Class.hs
View File

@ -13,6 +13,7 @@ module Cryptol.TypeCheck.Solver.Class
( classStep
, solveArithInst
, solveCmpInst
, solveSignedCmpInst
, expandProp
) where
@ -94,6 +95,47 @@ solveCmpInst ty = case tNoUser ty of
_ -> Unsolved
-- | Solve a SignedCmp constraint for a sequence. The type passed here is the
-- element type of the sequence.
solveSignedCmpSeq :: Type -> Type -> Solved
solveSignedCmpSeq n ty = case tNoUser ty of
-- (fin n, n >=1 ) => SignedCmp [n]Bit
TCon (TC TCBit) [] -> SolvedIf [ pFin n, n >== tNum (1 :: Integer) ]
-- variables are not solvable.
TVar {} -> Unsolved
-- (fin n, SignedCmp ty) => SignedCmp [n]ty, when ty != Bit
_ -> SolvedIf [ pFin n, pSignedCmp ty ]
-- | Solve SignedCmp constraints.
solveSignedCmpInst :: Type -> Solved
solveSignedCmpInst ty = case tNoUser ty of
-- SignedCmp Error -> fails
TCon (TError _ e) _ -> Unsolvable e
-- SignedCmp Bit
TCon (TC TCBit) [] -> Unsolvable $ TCErrorMessage "Signed comparisons may not be performed on bits"
-- SignedCmp for sequences
TCon (TC TCSeq) [n,a] -> solveSignedCmpSeq n a
-- (SignedCmp a, SignedCmp b) => SignedCmp (a,b)
TCon (TC (TCTuple _)) es -> SolvedIf (map pSignedCmp es)
-- SignedCmp (a -> b) fails
TCon (TC TCFun) [_,_] ->
Unsolvable $ TCErrorMessage "Signed comparisons may not be performed on functions."
-- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b }
TRec fs -> SolvedIf [ pSignedCmp e | (_,e) <- fs ]
_ -> Unsolved
-- | Add propositions that are implied by the given one.
-- The result contains the orignal proposition, and maybe some more.
expandProp :: Prop -> [Prop]

48
src/Cryptol/TypeCheck/Type.hs
View File

@ -99,6 +99,7 @@ data PC = PEqual -- ^ @_ == _@
| PHas Selector -- ^ @Has sel type field@ does not appear in schemas
| PArith -- ^ @Arith _@
| PCmp -- ^ @Cmp _@
| PSignedCmp -- ^ @SignedCmp _@
| PAnd -- ^ This is useful when simplifying things in place
| PTrue -- ^ Ditto
@ -182,15 +183,16 @@ instance HasKind TC where
instance HasKind PC where
kindOf pc =
case pc of
PEqual -> KNum :-> KNum :-> KProp
PNeq -> KNum :-> KNum :-> KProp
PGeq -> KNum :-> KNum :-> KProp
PFin -> KNum :-> KProp
PHas _ -> KType :-> KType :-> KProp
PArith -> KType :-> KProp
PCmp -> KType :-> KProp
PAnd -> KProp :-> KProp :-> KProp
PTrue -> KProp
PEqual -> KNum :-> KNum :-> KProp
PNeq -> KNum :-> KNum :-> KProp
PGeq -> KNum :-> KNum :-> KProp
PFin -> KNum :-> KProp
PHas _ -> KType :-> KType :-> KProp
PArith -> KType :-> KProp
PCmp -> KType :-> KProp
PSignedCmp -> KType :-> KProp
PAnd -> KProp :-> KProp :-> KProp
PTrue -> KProp
instance HasKind TFun where
kindOf tfun =
@ -406,6 +408,11 @@ pIsCmp ty = case tNoUser ty of
TCon (PC PCmp) [t1] -> Just t1
_ -> Nothing
pIsSignedCmp :: Prop -> Maybe Type
pIsSignedCmp ty = case tNoUser ty of
TCon (PC PSignedCmp) [t1] -> Just t1
_ -> Nothing
pIsTrue :: Prop -> Bool
pIsTrue ty = case tNoUser ty of
TCon (PC PTrue) _ -> True
@ -549,6 +556,9 @@ pArith t = TCon (PC PArith) [t]
pCmp :: Type -> Prop
pCmp t = TCon (PC PCmp) [t]
pSignedCmp :: Type -> Prop
pSignedCmp t = TCon (PC PSignedCmp) [t]
-- | Make a greater-than-or-equal-to constraint.
(>==) :: Type -> Type -> Prop
x >== y = TCon (PC PGeq) [x,y]
@ -715,6 +725,7 @@ instance PP (WithNames Type) where
(PArith, [t1]) -> pp pc <+> go 4 t1
(PCmp, [t1]) -> pp pc <+> go 4 t1
(PSignedCmp, [t1]) -> pp pc <+> go 4 t1
(_, _) -> pp pc <+> fsep (map (go 4) ts)
@ -773,15 +784,16 @@ instance PP TCErrorMessage where
instance PP PC where
ppPrec _ x =
case x of
PEqual -> text "(==)"
PNeq -> text "(/=)"
PGeq -> text "(>=)"
PFin -> text "fin"
PHas sel -> parens (ppSelector sel)
PArith -> text "Arith"
PCmp -> text "Cmp"
PTrue -> text "True"
PAnd -> text "(&&)"
PEqual -> text "(==)"
PNeq -> text "(/=)"
PGeq -> text "(>=)"
PFin -> text "fin"
PHas sel -> parens (ppSelector sel)
PArith -> text "Arith"
PCmp -> text "Cmp"
PSignedCmp -> text "SignedCmp"
PTrue -> text "True"
PAnd -> text "(&&)"
instance PP TC where
ppPrec _ x =

12
tests/issues/issue226.icry.stdout
View File

@ -19,22 +19,29 @@ Symbols
(#) : {front, back,
a} (fin front) => [front]a -> [back]a -> [front + back]a
(%) : {a} (Arith a) => a -> a -> a
(%$) : {a} (Arith a) => a -> a -> a
(&&) : {a} a -> a -> a
(*) : {a} (Arith a) => a -> a -> a
(+) : {a} (Arith a) => a -> a -> a
(-) : {a} (Arith a) => a -> a -> a
(/) : {a} (Arith a) => a -> a -> a
(/$) : {a} (Arith a) => a -> a -> a
(/\) : Bit -> Bit -> Bit
(<) : {a} (Cmp a) => a -> a -> Bit
(<$) : {a} (SignedCmp a) => a -> a -> Bit
(<<) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
(<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
(<=) : {a} (Cmp a) => a -> a -> Bit
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
(==) : {a} (Cmp a) => a -> a -> Bit
(===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
(==>) : Bit -> Bit -> Bit
(>) : {a} (Cmp a) => a -> a -> Bit
(>$) : {a} (SignedCmp a) => a -> a -> Bit
(>=) : {a} (Cmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
(>>) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
(>>$) : {n, k} (fin n, n >= 1, fin k) => [n] -> [k] -> [n]
(>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
(@) : {a, b, c} (fin c) => [a]b -> [c] -> b
(@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
@ -43,6 +50,7 @@ Symbols
(\/) : Bit -> Bit -> Bit
(^) : {a} a -> a -> a
(^^) : {a} (Arith a) => a -> a -> a
carry : {n} (fin n) => [n] -> [n] -> Bit
complement : {a} a -> a
demote : {val, bits} (fin val, fin bits,
bits >= width val) => [bits]
@ -76,6 +84,9 @@ Symbols
(a + b)]
random : {a} [256] -> a
reverse : {a, b} (fin a) => [a]b -> [a]b
sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
sext : {n, m} (fin m, m >= n, n >= 1) => [n] -> [m]
split : {parts, each, a} (fin each) => [parts *
each]a -> [parts][each]a
splitAt : {front, back, a} (fin front) => [front +
@ -96,5 +107,6 @@ Symbols
width : {bits, len, elem} (fin len, fin bits,
bits >= width len) => [len]elem -> [bits]
zero : {a} a
zext : {n, m} (fin m, m >= n) => [n] -> [m]
(||) : {a} a -> a -> a

2
tests/issues/issue290v2.icry.stdout
View File

@ -4,7 +4,7 @@ Loading module Main
[error] at ./issue290v2.cry:2:1--2:19:
Unsolved constraints:
a`283 == 1
a`356 == 1
arising from
checking a pattern: type of 1st argument of Main::minMax
at ./issue290v2.cry:2:8--2:11

4
tests/mono-binds/test04.icry.stdout
View File

@ -25,8 +25,8 @@ Loading module test04
[error] at ./test04.cry:3:19--3:21:
Type mismatch:
Expected type: ()
Inferred type: [?l11]
Inferred type: [?g14]
where
?l11 is type parameter 'bits'
?g14 is type parameter 'bits'
of literal or demoted expression
at ./test04.cry:3:19--3:21