Date: Thursday, February 4, 2021 @ 20:05:36 Author: felixonmars Revision: 845511
upgpkg: cryptol 2.10.0-59: rebuild with libBF 0.6 Added: cryptol/trunk/libbf-0.6.patch Modified: cryptol/trunk/PKGBUILD -----------------+ PKGBUILD | 9 ++- libbf-0.6.patch | 156 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 162 insertions(+), 3 deletions(-) Modified: PKGBUILD =================================================================== --- PKGBUILD 2021-02-04 19:50:28 UTC (rev 845510) +++ PKGBUILD 2021-02-04 20:05:36 UTC (rev 845511) @@ -2,7 +2,7 @@ pkgname=cryptol pkgver=2.10.0 -pkgrel=58 +pkgrel=59 pkgdesc="The Language of Cryptography" url="https://www.cryptol.net"; license=("BSD") @@ -15,12 +15,15 @@ 'haskell-transformers-base' 'haskell-what4' 'haskell-ansi-terminal' 'haskell-blaze-html') makedepends=('ghc' 'alex' 'happy') source=("$pkgname-$pkgver.tar.gz::https://github.com/GaloisInc/cryptol/archive/$pkgver.tar.gz"; - sbv-8.8.patch) + sbv-8.8.patch + libbf-0.6.patch) sha512sums=('efb5f048a23de2040716d210b3d59071744d97989920266206590320585850a84de989851ed94687995874d74a3e6986d2e735e636aaa9f70f8949604ab62904' - 'da4ac99c538a935eed9efd98dd6c57f24ad12d8effe328a814661ed02395445d28c8b4f43b48492171dc0bd65c6568fe7641de94e32765d51ab208a38f09d2d2') + 'da4ac99c538a935eed9efd98dd6c57f24ad12d8effe328a814661ed02395445d28c8b4f43b48492171dc0bd65c6568fe7641de94e32765d51ab208a38f09d2d2' + 'b26cef81b4412b7d655376ee01a67bb531b69b2a134b08d6ee592618dee87bc70f8f1acb38db42d5b49f0e70934670f3118e07887958a262924faf469d41eb47') prepare() { patch -d $pkgname-$pkgver -p1 < sbv-8.8.patch + patch -d $pkgname-$pkgver -p1 < libbf-0.6.patch } build() { Added: libbf-0.6.patch =================================================================== --- libbf-0.6.patch (rev 0) +++ libbf-0.6.patch 2021-02-04 20:05:36 UTC (rev 845511) @@ -0,0 +1,156 @@ +From 78855e796720cf6b96f4ccc9435d871b9474f05c Mon Sep 17 00:00:00 2001 +From: Rob Dockins <[email protected]> +Date: Thu, 28 Jan 2021 15:24:15 -0800 +Subject: [PATCH] Update to use `libBF` version 0.6, which has some bugfixes + and additional operations. + +--- + cryptol.cabal | 2 +- + src/Cryptol/Backend/Concrete.hs | 4 +- + src/Cryptol/Backend/FloatHelpers.hs | 86 +---------------------------- + 3 files changed, 5 insertions(+), 87 deletions(-) + +diff --git a/cryptol.cabal b/cryptol.cabal +index a737c0d3..dfd30a26 100644 +--- a/cryptol.cabal ++++ b/cryptol.cabal +@@ -57,7 +57,7 @@ library + GraphSCC >= 1.0.4, + heredoc >= 0.2, + integer-gmp >= 1.0 && < 1.1, +- libBF >= 0.5.1, ++ libBF >= 0.6 && < 0.7, + MemoTrie >= 0.6 && < 0.7, + monad-control >= 1.0, + monadLib >= 3.7.2, +diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs +index 129c9a11..cb043b17 100644 +--- a/src/Cryptol/Backend/Concrete.hs ++++ b/src/Cryptol/Backend/Concrete.hs +@@ -338,11 +338,11 @@ instance Backend Concrete where + fpDiv = fpBinArith FP.bfDiv + fpNeg _ x = pure x { FP.bfValue = FP.bfNeg (FP.bfValue x) } + fpFromInteger sym e p r x = +- do opts <- FP.fpOpts e p <$> fpRoundMode sym r ++ do r' <- fpRoundMode sym r + pure FP.BF { FP.bfExpWidth = e + , FP.bfPrecWidth = p + , FP.bfValue = FP.fpCheckStatus $ +- FP.bfRoundInt opts (FP.bfFromInteger x) ++ FP.bfRoundInt r' (FP.bfFromInteger x) + } + fpToInteger = fpCvtToInteger + +diff --git a/src/Cryptol/Backend/FloatHelpers.hs b/src/Cryptol/Backend/FloatHelpers.hs +index 07c5113f..a622b668 100644 +--- a/src/Cryptol/Backend/FloatHelpers.hs ++++ b/src/Cryptol/Backend/FloatHelpers.hs +@@ -3,8 +3,6 @@ + module Cryptol.Backend.FloatHelpers where + + import Data.Ratio(numerator,denominator) +-import Data.Int(Int64) +-import Data.Bits(testBit,setBit,shiftL,shiftR,(.&.),(.|.)) + import LibBF + + import Cryptol.Utils.PP +@@ -150,97 +148,17 @@ floatToInteger fun r fp = + ["Unexpected rounding mode", show r] + + +- +- + floatFromBits :: + Integer {- ^ Exponent width -} -> + Integer {- ^ Precision widht -} -> + Integer {- ^ Raw bits -} -> + BF +-floatFromBits e p bv = BF { bfValue = floatFromBits' e p bv ++floatFromBits e p bv = BF { bfValue = bfFromBits (fpOpts e p NearEven) bv + , bfExpWidth = e, bfPrecWidth = p } + + +- +--- | Make a float using "raw" bits. +-floatFromBits' :: +- Integer {- ^ Exponent width -} -> +- Integer {- ^ Precision widht -} -> +- Integer {- ^ Raw bits -} -> +- BigFloat +- +-floatFromBits' e p bits +- | expoBiased == 0 && mant == 0 = -- zero +- if isNeg then bfNegZero else bfPosZero +- +- | expoBiased == eMask && mant == 0 = -- infinity +- if isNeg then bfNegInf else bfPosInf +- +- | expoBiased == eMask = bfNaN -- NaN +- +- | expoBiased == 0 = -- Subnormal +- case bfMul2Exp opts (bfFromInteger mant) (expoVal + 1) of +- (num,Ok) -> if isNeg then bfNeg num else num +- (_,s) -> panic "floatFromBits" [ "Unexpected status: " ++ show s ] +- +- | otherwise = -- Normal +- case bfMul2Exp opts (bfFromInteger mantVal) expoVal of +- (num,Ok) -> if isNeg then bfNeg num else num +- (_,s) -> panic "floatFromBits" [ "Unexpected status: " ++ show s ] +- +- where +- opts = expBits e' <> precBits (p' + 1) <> allowSubnormal +- +- e' = fromInteger e :: Int +- p' = fromInteger p - 1 :: Int +- eMask = (1 `shiftL` e') - 1 :: Int64 +- pMask = (1 `shiftL` p') - 1 :: Integer +- +- isNeg = testBit bits (e' + p') +- +- mant = pMask .&. bits :: Integer +- mantVal = mant `setBit` p' :: Integer +- -- accounts for the implicit 1 bit +- +- expoBiased = eMask .&. fromInteger (bits `shiftR` p') :: Int64 +- bias = eMask `shiftR` 1 :: Int64 +- expoVal = expoBiased - bias - fromIntegral p' :: Int64 +- +- + -- | Turn a float into raw bits. + -- @NaN@ is represented as a positive "quiet" @NaN@ + -- (most significant bit in the significand is set, the rest of it is 0) + floatToBits :: Integer -> Integer -> BigFloat -> Integer +-floatToBits e p bf = (isNeg `shiftL` (e' + p')) +- .|. (expBiased `shiftL` p') +- .|. (mant `shiftL` 0) +- where +- e' = fromInteger e :: Int +- p' = fromInteger p - 1 :: Int +- +- eMask = (1 `shiftL` e') - 1 :: Integer +- pMask = (1 `shiftL` p') - 1 :: Integer +- +- (isNeg, expBiased, mant) = +- case bfToRep bf of +- BFNaN -> (0, eMask, 1 `shiftL` (p' - 1)) +- BFRep s num -> (sign, be, ma) +- where +- sign = case s of +- Neg -> 1 +- Pos -> 0 +- +- (be,ma) = +- case num of +- Zero -> (0,0) +- Num i ev +- | ex == 0 -> (0, i `shiftL` (p' - m -1)) +- | otherwise -> (ex, (i `shiftL` (p' - m)) .&. pMask) +- where +- m = msb 0 i - 1 +- bias = eMask `shiftR` 1 +- ex = toInteger ev + bias + toInteger m +- +- Inf -> (eMask,0) +- +- msb !n j = if j == 0 then n else msb (n+1) (j `shiftR` 1) ++floatToBits e p bf = bfToBits (fpOpts e p NearEven) bf
