Skip to content

Commit

Permalink
Make fromTo and friends return VWord when appropriate (#1436)
Browse files Browse the repository at this point in the history
Previous, `fromTo` and related functions would always return a `VSeq`. If the
type happened to be a `Bit`, this would violate the internal invariant that
sequences of `Bit`s are always represented with `VWord`s, leading to the panics
observed in #1435. This patch fixes the issue by using the `mkSeq` smart
constructor, which chooses between `VWord` and `VSeq` depending on the sequence
type.

Fixes #1435.
  • Loading branch information
RyanGlScott authored Sep 17, 2022
1 parent 6fd1a11 commit 4367eee
Show file tree
Hide file tree
Showing 4 changed files with 56 additions and 16 deletions.
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
32 changes: 16 additions & 16 deletions src/Cryptol/Eval/Generic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 #-}
Expand All @@ -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 #-}
Expand All @@ -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 ]@
Expand All @@ -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 ]@
Expand All @@ -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 #-}
Expand All @@ -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 ]@
Expand All @@ -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
Expand Down
9 changes: 9 additions & 0 deletions tests/issues/issue1435.icry
Original file line number Diff line number Diff line change
@@ -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
28 changes: 28 additions & 0 deletions tests/issues/issue1435.icry.stdout
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 4367eee

Please sign in to comment.