Merge pull request #1192 from GaloisInc/issue1191

Fix for issue 1191

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 -} ->

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

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))

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)

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.