diff --git a/src/Cryptol/Backend/SeqMap.hs b/src/Cryptol/Backend/SeqMap.hs index 115e7ff39..167e3c90d 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 f59e844c1..dbef2d688 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 = @@ -532,27 +534,18 @@ 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 #-} 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) @@ -572,19 +565,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 idx_segs <- enumerateIndexSegments sym idx - bitmapWordVal sym n =<< barrelShifter sym (iteBit sym) shiftOp (Nat n) bs0 n 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 #-} @@ -651,17 +633,24 @@ 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 = - 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 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.