From 0707bdcd33f276daca206755b17e9f82d0a1cff2 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 5 May 2021 15:52:48 -0700 Subject: [PATCH 1/5] Fix #1191 The barrel shifter was being called with the wrong width; the length of the sequence to be shifted was passed instead of the number of bits in the index word. --- src/Cryptol/Backend/WordValue.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/Backend/WordValue.hs b/src/Cryptol/Backend/WordValue.hs index f59e844c1..c32967abe 100644 --- a/src/Cryptol/Backend/WordValue.hs +++ b/src/Cryptol/Backend/WordValue.hs @@ -576,8 +576,9 @@ shiftWordByWord sym wop reindex x idx = WordVal (wordAsLit sym -> Just (_,j)) -> bitmapWordVal sym n =<< shiftOp bs0 j _ -> - do idx_segs <- enumerateIndexSegments sym idx - bitmapWordVal sym n =<< barrelShifter sym (iteBit sym) shiftOp (Nat n) bs0 n idx_segs + do let idx_w = wordValueSize sym idx + idx_segs <- enumerateIndexSegments sym idx + bitmapWordVal sym n =<< barrelShifter sym (iteBit sym) shiftOp (Nat n) bs0 idx_w idx_segs where shiftOp vs shft = From 6497daede672e912e4aba1e54ab20e817cf397d9 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 5 May 2021 17:07:22 -0700 Subject: [PATCH 2/5] Dispatch to `shiftSeqByInteger` and `shiftSeqByWord` in the `BitmapVal` cases of `shiftWordByInteger` and `shiftWordByWord`. --- src/Cryptol/Backend/WordValue.hs | 42 +++++++++----------------------- 1 file changed, 12 insertions(+), 30 deletions(-) diff --git a/src/Cryptol/Backend/WordValue.hs b/src/Cryptol/Backend/WordValue.hs index c32967abe..c0073fc43 100644 --- a/src/Cryptol/Backend/WordValue.hs +++ b/src/Cryptol/Backend/WordValue.hs @@ -532,19 +532,8 @@ shiftWordByInteger sym wop reindex x idx = isReady sym packed >>= \case Just w -> shiftWordByInteger sym wop reindex (WordVal w) idx Nothing -> - case integerAsLit sym idx of - Just j -> bitmapWordVal sym n =<< shiftOp bs0 j - Nothing -> - do (numbits, idx_bits) <- enumerateIntBits' sym n idx - bitmapWordVal sym n =<< - barrelShifter sym (iteBit sym) shiftOp (Nat n) bs0 numbits (map BitIndexSegment idx_bits) - - where - shiftOp vs shft = - pure $ indexSeqMap $ \i -> - case reindex i shft of - Nothing -> pure $ bitLit sym False - Just i' -> lookupSeqMap vs i' + bitmapWordVal sym n =<< + shiftSeqByInteger sym (iteBit sym) reindex (pure (bitLit sym False)) (Nat n) bs0 idx {-# INLINE shiftWordByWord #-} @@ -572,20 +561,8 @@ shiftWordByWord sym wop reindex x idx = isReady sym packed >>= \case Just w -> shiftWordByWord sym wop reindex (WordVal w) idx Nothing -> - case idx of - WordVal (wordAsLit sym -> Just (_,j)) -> - bitmapWordVal sym n =<< shiftOp bs0 j - _ -> - do let idx_w = wordValueSize sym idx - idx_segs <- enumerateIndexSegments sym idx - bitmapWordVal sym n =<< barrelShifter sym (iteBit sym) shiftOp (Nat n) bs0 idx_w idx_segs - - where - shiftOp vs shft = - pure $ indexSeqMap $ \i -> - case reindex i shft of - Nothing -> pure $ bitLit sym False - Just i' -> lookupSeqMap vs i' + bitmapWordVal sym n =<< + shiftSeqByWord sym (iteBit sym) reindex (pure (bitLit sym False)) (Nat n) bs0 idx {-# INLINE updateWordByWord #-} @@ -660,9 +637,14 @@ shiftSeqByWord :: WordValue sym -> SEval sym (SeqMap sym a) shiftSeqByWord sym merge reindex zro sz xs idx = - do idx_segs <- enumerateIndexSegments sym idx - barrelShifter sym merge shiftOp sz xs (wordValueSize sym idx) idx_segs - where + wordValAsLit sym idx >>= \case + Just j -> shiftOp xs j + Nothing -> + do idx_segs <- enumerateIndexSegments sym idx + barrelShifter sym merge shiftOp sz xs idx_bits idx_segs + where + idx_bits = wordValueSize sym idx + shiftOp vs shft = pure $ indexSeqMap $ \i -> case reindex i shft of From a0816576cf7382a72d37aac355c809d6c2449342 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 5 May 2021 17:38:59 -0700 Subject: [PATCH 3/5] A bit more documentation --- src/Cryptol/Backend/SeqMap.hs | 14 ++++++++------ src/Cryptol/Backend/WordValue.hs | 30 ++++++++++++++++++------------ 2 files changed, 26 insertions(+), 18 deletions(-) diff --git a/src/Cryptol/Backend/SeqMap.hs b/src/Cryptol/Backend/SeqMap.hs index 115e7ff39..d6b031caf 100644 --- a/src/Cryptol/Backend/SeqMap.hs +++ b/src/Cryptol/Backend/SeqMap.hs @@ -221,13 +221,14 @@ mergeSeqMap sym f c x y = {-# INLINE shiftSeqByInteger #-} shiftSeqByInteger :: Backend sym => sym -> - (SBit sym -> a -> a -> SEval sym a) -> + (SBit sym -> a -> a -> SEval sym a) + {- ^ if/then/else operation of values -} -> (Integer -> Integer -> Maybe Integer) {- ^ reindexing operation -} -> - SEval sym a -> - Nat' -> - SeqMap sym a -> - SInteger sym -> + SEval sym a {- ^ zero value -} -> + Nat' {- ^ size of the sequence -} -> + SeqMap sym a {- ^ sequence to shift -} -> + SInteger sym {- ^ shift amount, assumed to be in range [0,len) -} -> SEval sym (SeqMap sym a) shiftSeqByInteger sym merge reindex zro m xs idx | Just j <- integerAsLit sym idx = shiftOp xs j @@ -259,7 +260,8 @@ data IndexSegment sym #-} barrelShifter :: Backend sym => sym -> - (SBit sym -> a -> a -> SEval sym a) -> + (SBit sym -> a -> a -> SEval sym a) + {- ^ if/then/else operation of values -} -> (SeqMap sym a -> Integer -> SEval sym (SeqMap sym a)) {- ^ concrete shifting operation -} -> Nat' {- ^ Size of the map being shifted -} -> diff --git a/src/Cryptol/Backend/WordValue.hs b/src/Cryptol/Backend/WordValue.hs index c0073fc43..b0570e213 100644 --- a/src/Cryptol/Backend/WordValue.hs +++ b/src/Cryptol/Backend/WordValue.hs @@ -509,10 +509,12 @@ unwindThunks m = shiftWordByInteger :: Backend sym => sym -> - (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> - (Integer -> Integer -> Maybe Integer) -> - WordValue sym -> - SInteger sym -> + (SWord sym -> SWord sym -> SEval sym (SWord sym)) + {- ^ operation on word values -} -> + (Integer -> Integer -> Maybe Integer) + {- ^ reindexing operation -} -> + WordValue sym {- ^ word value to shift -} -> + SInteger sym {- ^ shift amount, assumed to be in range [0,len) -} -> SEval sym (WordValue sym) shiftWordByInteger sym wop reindex x idx = @@ -540,8 +542,10 @@ shiftWordByInteger sym wop reindex x idx = shiftWordByWord :: Backend sym => sym -> - (SWord sym -> SWord sym -> SEval sym (SWord sym)) -> - (Integer -> Integer -> Maybe Integer) -> + (SWord sym -> SWord sym -> SEval sym (SWord sym)) + {- ^ operation on word values -} -> + (Integer -> Integer -> Maybe Integer) + {- ^ reindexing operation -} -> WordValue sym {- ^ value to shift -} -> WordValue sym {- ^ amount to shift -} -> SEval sym (WordValue sym) @@ -629,12 +633,14 @@ updateWordByWord sym dir w0 idx bitval = shiftSeqByWord :: Backend sym => sym -> - (SBit sym -> a -> a -> SEval sym a) -> - (Integer -> Integer -> Maybe Integer) -> - SEval sym a -> - Nat' -> - SeqMap sym a -> - WordValue sym -> + (SBit sym -> a -> a -> SEval sym a) + {- ^ if/then/else operation of values -} -> + (Integer -> Integer -> Maybe Integer) + {- ^ reindexing operation -} -> + SEval sym a {- ^ zero value -} -> + Nat' {- ^ size of the sequence -} -> + SeqMap sym a {- ^ sequence to shift -} -> + WordValue sym {- ^ shift amount -} -> SEval sym (SeqMap sym a) shiftSeqByWord sym merge reindex zro sz xs idx = wordValAsLit sym idx >>= \case From a05b4eda7fb74ef7e63797c836978a8f7bb23908 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 5 May 2021 17:43:32 -0700 Subject: [PATCH 4/5] Add test case for issue 1191 --- tests/issues/issue1191.cry | 20 ++++++++++++++++++++ tests/issues/issue1191.icry | 12 ++++++++++++ tests/issues/issue1191.icry.stdout | 11 +++++++++++ 3 files changed, 43 insertions(+) create mode 100644 tests/issues/issue1191.cry create mode 100644 tests/issues/issue1191.icry create mode 100644 tests/issues/issue1191.icry.stdout diff --git a/tests/issues/issue1191.cry b/tests/issues/issue1191.cry new file mode 100644 index 000000000..04a55e990 --- /dev/null +++ b/tests/issues/issue1191.cry @@ -0,0 +1,20 @@ +xs : [32] +xs = 0xdeadbeef + +f : [32] -> [32] +f zs = zs <<< ( [True,False,False]:[3] ) + +q0 = f xs +q1 = f (rnf (xs @@ [0..31])) +q2 = f (xs @@ [0..31]) + + +ys : [1][32] +ys = [ 0xdeadbeef ] + +g : [1][32] -> [32] +g zs = (zs@0) <<< ( [True,False,False]:[3] ) + +r0 = g ys +r1 = g (split (rnf (join ys))) +r2 = g (split (join ys)) diff --git a/tests/issues/issue1191.icry b/tests/issues/issue1191.icry new file mode 100644 index 000000000..3d2b8cb0d --- /dev/null +++ b/tests/issues/issue1191.icry @@ -0,0 +1,12 @@ +:l issue1191.cry + +q0 +q1 +q2 + +r0 +r1 +r2 + +:prove (q0 == q1 /\ q1 == q2) +:prove (r0 == r1 /\ r1 == r2) diff --git a/tests/issues/issue1191.icry.stdout b/tests/issues/issue1191.icry.stdout new file mode 100644 index 000000000..c22d89ac2 --- /dev/null +++ b/tests/issues/issue1191.icry.stdout @@ -0,0 +1,11 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +0xeadbeefd +0xeadbeefd +0xeadbeefd +0xeadbeefd +0xeadbeefd +0xeadbeefd +Q.E.D. +Q.E.D. From 69e768952757d65ab5bd1755080a2eaa6b72b75a Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 5 May 2021 17:46:17 -0700 Subject: [PATCH 5/5] Fix slightly incorrect documentation --- src/Cryptol/Backend/SeqMap.hs | 2 +- src/Cryptol/Backend/WordValue.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Cryptol/Backend/SeqMap.hs b/src/Cryptol/Backend/SeqMap.hs index d6b031caf..167e3c90d 100644 --- a/src/Cryptol/Backend/SeqMap.hs +++ b/src/Cryptol/Backend/SeqMap.hs @@ -228,7 +228,7 @@ shiftSeqByInteger :: Backend sym => SEval sym a {- ^ zero value -} -> Nat' {- ^ size of the sequence -} -> SeqMap sym a {- ^ sequence to shift -} -> - SInteger sym {- ^ shift amount, assumed to be in range [0,len) -} -> + SInteger sym {- ^ shift amount, assumed to be in range [0,len] -} -> SEval sym (SeqMap sym a) shiftSeqByInteger sym merge reindex zro m xs idx | Just j <- integerAsLit sym idx = shiftOp xs j diff --git a/src/Cryptol/Backend/WordValue.hs b/src/Cryptol/Backend/WordValue.hs index b0570e213..dbef2d688 100644 --- a/src/Cryptol/Backend/WordValue.hs +++ b/src/Cryptol/Backend/WordValue.hs @@ -514,7 +514,7 @@ shiftWordByInteger :: (Integer -> Integer -> Maybe Integer) {- ^ reindexing operation -} -> WordValue sym {- ^ word value to shift -} -> - SInteger sym {- ^ shift amount, assumed to be in range [0,len) -} -> + SInteger sym {- ^ shift amount, assumed to be in range [0,len] -} -> SEval sym (WordValue sym) shiftWordByInteger sym wop reindex x idx =