diff --git a/CHANGES.md b/CHANGES.md index cc41ad935..d56d22c09 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -28,6 +28,9 @@ * Fix a bug in the What4 backend that could cause applications of `(@)` with symbolic `Integer` indices to become out of bounds (#1359). +* Fix a bug that caused finite bitvector enumerations to panic when used in + combination with `(#)` (e.g., `[0..1] # 0`). + # 2.13.0 ## Language changes diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index 204658b91..461c4bc22 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -1452,12 +1452,12 @@ fromToV sym = PNumPoly \first -> PNumPoly \lst -> PTyPoly \ty -> - PVal + PPrim let !f = mkLit sym ty in case (first, lst) of (Nat first', Nat lst') -> let len = 1 + (lst' - first') - in VSeq len $ indexSeqMap $ \i -> f (first' + i) + in mkSeq sym (Nat len) ty $ indexSeqMap $ \i -> f (first' + i) _ -> evalPanic "fromToV" ["invalid arguments"] {-# INLINE fromThenToV #-} @@ -1469,12 +1469,12 @@ fromThenToV sym = PNumPoly \lst -> PTyPoly \ty -> PNumPoly \len -> - PVal + PPrim let !f = mkLit sym ty in case (first, next, lst, len) of (Nat first', Nat next', Nat _lst', Nat len') -> let diff = next' - first' - in VSeq len' $ indexSeqMap $ \i -> f (first' + i*diff) + in mkSeq sym (Nat len') ty $ indexSeqMap $ \i -> f (first' + i*diff) _ -> evalPanic "fromThenToV" ["invalid arguments"] {-# INLINE fromToLessThanV #-} @@ -1484,12 +1484,12 @@ fromToLessThanV sym = PFinPoly \first -> PNumPoly \bound -> PTyPoly \ty -> - PVal + PPrim let !f = mkLit sym ty ss = indexSeqMap $ \i -> f (first + i) in case bound of - Inf -> VStream ss - Nat bound' -> VSeq (bound' - first) ss + Inf -> return $ VStream ss + Nat bound' -> mkSeq sym (Nat (bound' - first)) ty ss {-# INLINE fromToByV #-} -- @[ 0 .. 10 by 2 ]@ @@ -1499,10 +1499,10 @@ fromToByV sym = PFinPoly \lst -> PFinPoly \stride -> PTyPoly \ty -> - PVal + PPrim let !f = mkLit sym ty ss = indexSeqMap $ \i -> f (first + i*stride) - in VSeq (1 + ((lst - first) `div` stride)) ss + in mkSeq sym (Nat (1 + ((lst - first) `div` stride))) ty ss {-# INLINE fromToByLessThanV #-} -- @[ 0 .. <10 by 2 ]@ @@ -1512,12 +1512,12 @@ fromToByLessThanV sym = PNumPoly \bound -> PFinPoly \stride -> PTyPoly \ty -> - PVal + PPrim let !f = mkLit sym ty ss = indexSeqMap $ \i -> f (first + i*stride) in case bound of - Inf -> VStream ss - Nat bound' -> VSeq ((bound' - first + stride - 1) `div` stride) ss + Inf -> return $ VStream ss + Nat bound' -> mkSeq sym (Nat ((bound' - first + stride - 1) `div` stride)) ty ss {-# INLINE fromToDownByV #-} @@ -1528,10 +1528,10 @@ fromToDownByV sym = PFinPoly \lst -> PFinPoly \stride -> PTyPoly \ty -> - PVal + PPrim let !f = mkLit sym ty ss = indexSeqMap $ \i -> f (first - i*stride) - in VSeq (1 + ((first - lst) `div` stride)) ss + in mkSeq sym (Nat (1 + ((first - lst) `div` stride))) ty ss {-# INLINE fromToDownByGreaterThanV #-} -- @[ 10 .. >0 down by 2 ]@ @@ -1541,10 +1541,10 @@ fromToDownByGreaterThanV sym = PFinPoly \bound -> PFinPoly \stride -> PTyPoly \ty -> - PVal + PPrim let !f = mkLit sym ty ss = indexSeqMap $ \i -> f (first - i*stride) - in VSeq ((first - bound + stride - 1) `div` stride) ss + in mkSeq sym (Nat ((first - bound + stride - 1) `div` stride)) ty ss {-# INLINE infFromV #-} infFromV :: Backend sym => sym -> Prim sym diff --git a/tests/issues/issue1435.icry b/tests/issues/issue1435.icry new file mode 100644 index 000000000..59c006fb1 --- /dev/null +++ b/tests/issues/issue1435.icry @@ -0,0 +1,9 @@ +[0..0] # 0 +[0..1] # 0 +0 # [0..0] +[0,1..1] # 0 +[0..<2] # 0 +[0..0 by 2] # 0 +[0..<2 by 2] # 0 +[0..0 down by 2] # 0 +[1..>0 down by 2] # 0 diff --git a/tests/issues/issue1435.icry.stdout b/tests/issues/issue1435.icry.stdout new file mode 100644 index 000000000..8fce9f918 --- /dev/null +++ b/tests/issues/issue1435.icry.stdout @@ -0,0 +1,28 @@ +Loading module Cryptol +Showing a specific instance of polymorphic result: + * Using '0' for type argument 'back' of '(Cryptol::#)' +0x0 +Showing a specific instance of polymorphic result: + * Using '0' for type argument 'back' of '(Cryptol::#)' +0x1 +Showing a specific instance of polymorphic result: + * Using '0' for type argument 'front' of '(Cryptol::#)' +0x0 +Showing a specific instance of polymorphic result: + * Using '0' for type argument 'back' of '(Cryptol::#)' +0x1 +Showing a specific instance of polymorphic result: + * Using '0' for type argument 'back' of '(Cryptol::#)' +0x1 +Showing a specific instance of polymorphic result: + * Using '0' for type argument 'back' of '(Cryptol::#)' +0x0 +Showing a specific instance of polymorphic result: + * Using '0' for type argument 'back' of '(Cryptol::#)' +0x0 +Showing a specific instance of polymorphic result: + * Using '0' for type argument 'back' of '(Cryptol::#)' +0x0 +Showing a specific instance of polymorphic result: + * Using '0' for type argument 'back' of '(Cryptol::#)' +0x1