What4 panic - bvSliceLE

[weaversa]

Cryptol> :s prover=w4-yices
Cryptol> :safe \a -> sortBy (\c1 c2 -> c2 != ' ') (split`{8} a)

What4 exception:
You have encountered a bug in What4's implementation.
*** Please create an issue at https://github.com/GaloisInc/what4/issues

%< --------------------------------------------------- 
  Revision:  UNKNOWN
  Branch:    UNKNOWN
  Location:  bvSliceLE
  Message:   invalid arguments to slice: -8 8 from vector of length 64
CallStack (from HasCallStack):
  panic, called at src/What4/Panic.hs:17:9 in what4-1.3-bfc7256e61a16a19b2a7e616b2f312207ac52dd905f463dea20337459d487211:What4.Panic
  panic, called at src/What4/SWord.hs:360:5 in what4-1.3-bfc7256e61a16a19b2a7e616b2f312207ac52dd905f463dea20337459d487211:What4.SWord
%< ---------------------------------------------------

[RyanGlScott]

Interesting. I can reproduce this using Cryptol 2.13.0 but not 2.12.0.

[RyanGlScott]

Ah, but that's simply because the implementation of sortBy changed in Cryptol 2.13.0. If I create a standalone file with the modern implementation of sortBy:

sortBy' : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a
sortBy' le ((xs : [n/2]a) # (ys : [n/^2]a)) = take zs.0
  where
    xs' = if `(n/2)  == 1 then xs else sortBy' le xs
    ys' = if `(n/^2) == 1 then ys else sortBy' le ys
    zs  = [ if i == `(n/2)        then (ys'@j, i  , j+1)
             | j == `(n/^2)       then (xs'@i, i+1, j  )
             | le (xs'@i) (ys'@j) then (xs'@i, i+1, j  )
            else                       (ys'@j, i  , j+1)
          | (_, i, j) <- [ (undefined, 0, 0) ] # zs
          ]

Then I can reproduce the panic using either Cryptol 2.12.0 or 2.13.0:

$ ~/Software/cryptol-2.12.0/bin/cryptol Bug.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.12.0
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Main
Main> :s prover=w4-yices
Main> :safe \a -> sortBy' (\c1 c2 -> c2 != ' ') (split`{8} a)

What4 exception:
You have encountered a bug in What4's implementation.
*** Please create an issue at https://github.com/GaloisInc/what4/issues

%< --------------------------------------------------- 
  Revision:  cb240cdd31c864b298f181c0dac660e2f4e32aa5
  Branch:    master (uncommited files present)
  Location:  bvSliceLE
  Message:   invalid arguments to slice: -8 8 from vector of length 64
CallStack (from HasCallStack):
  panic, called at src/What4/Panic.hs:17:9 in what4-1.2.1-0e36dce815ba6a943ccd671db5fe64d701778a802305688be36c2457edf079a9:What4.Panic
  panic, called at src/What4/SWord.hs:360:5 in what4-1.2.1-0e36dce815ba6a943ccd671db5fe64d701778a802305688be36c2457edf079a9:What4.SWord
%< ---------------------------------------------------

[RyanGlScott]

A slightly smaller example that doesn't require sortBy:

$ ~/Software/cryptol-2.13.0/bin/cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.13.0
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :s prover=sbv-yices
Cryptol> :safe \(a : [64]) (i : Integer) -> (split`{8} a)@(max 0 (min i 7))
Safe
(Total Elapsed Time: 0.002s, using "Yices")
Cryptol> :set prover=w4-yices
Cryptol> :safe \(a : [64]) (i : Integer) -> (split`{8} a)@(max 0 (min i 7))

What4 exception:
You have encountered a bug in What4's implementation.
*** Please create an issue at https://github.com/GaloisInc/what4/issues

%< --------------------------------------------------- 
  Revision:  8cca24568ad499f06032c2e4eaa7dfd4c542efb6
  Branch:    master (uncommited files present)
  Location:  bvSliceLE
  Message:   invalid arguments to slice: -8 8 from vector of length 64
CallStack (from HasCallStack):
  panic, called at src/What4/Panic.hs:17:9 in what4-1.3-ff3aee1f97aca88324f966c041e5f99ea48c545ca23bc80745e4da673528a840:What4.Panic
  panic, called at src/What4/SWord.hs:360:5 in what4-1.3-ff3aee1f97aca88324f966c041e5f99ea48c545ca23bc80745e4da673528a840:What4.SWord
%< ---------------------------------------------------

[benjaminselfridge]

I'm going to take a look at this real quick...

[benjaminselfridge]

This tells me that the max 0 (min i 7) is not working properly; it seems to be allowing i == -1. Still investigating.

[benjaminselfridge]

I'm not sure what's going on here; it's clearly got something to do with the translation of max 0 (min i 7) to what4.

[RyanGlScott]

I think I see what is going on here. This is a Cryptol bug, not a What4 one, so I've moved the issue accordingly.

The issue arises due to a bug in the way the (@) function handles symbolic indices in the What4 backend. In particular, this code:

cryptol/src/Cryptol/Eval/What4.hs

Lines 512 to 515 in 8cca245

	| (lo, Just hi) <- bounds
	= case foldr f Nothing [lo .. hi] of
	Nothing -> raiseError sym (InvalidIndex Nothing)
	Just m -> m

Will construct a mux of all possible indices from lo to hi. The value of hi ultimately comes from maxIdx here:

cryptol/src/Cryptol/Eval/What4.hs

Lines 538 to 547 in 8cca245

	-- Maximum possible in-bounds index given `Z m`
	-- type information and the length
	-- of the sequence. If the sequences is infinite and the
	-- integer is unbounded, there isn't much we can do.
	maxIdx =
	case (mblen, ix) of
	(Nat n, TVIntMod m) -> Just (min (toInteger n) (toInteger m))
	(Nat n, _) -> Just n
	(_ , TVIntMod m) -> Just m
	_ -> Nothing

The implementation of maxIdx has an off-by-one error, however. The value n represents the type variable in the type of (@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a. In the \(a : [64]) (i : Integer) -> (split`{8} a)@(max 0 (min i 7)) example above, n equals 8. But 8 is not a valid index into a list of length 8! The only valid indices are 0 through 7, but this code will construct a mux with all of the indices from 0 to 8 instead. This confuses the code that implements split, which ultimately results in the negative offset seen in the panic message.

Note that this bug does not occur if the type of i is changed from an Integer to a bitvector. This is because there is a separate case for (@) with bitvector indices, and that case constructs maxIdx correctly by subtracting 1 from n:

cryptol/src/Cryptol/Eval/What4.hs

Lines 577 to 582 in 8cca245

	-- maximum possible in-bounds index given the bitwidth
	-- of the index value and the length of the sequence
	maxIdx =
	case mblen of
	Nat n | n < 2^w -> n-1
	_ -> 2^w - 1

The SBV backend also subtracts 1 from n in a similar fashion. As a result, a fix for this issue is to do the same in the Integer-index case for (@) in the What4 backend:

diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs
index 0e6bc98f..bedd7139 100644
--- a/src/Cryptol/Eval/What4.hs
+++ b/src/Cryptol/Eval/What4.hs
@@ -541,9 +541,9 @@ indexFront_int sym mblen _a xs ix idx
     -- integer is unbounded, there isn't much we can do.
     maxIdx =
       case (mblen, ix) of
-        (Nat n, TVIntMod m)  -> Just (min (toInteger n) (toInteger m))
-        (Nat n, _)           -> Just n
-        (_    , TVIntMod m)  -> Just m
+        (Nat n, TVIntMod m)  -> Just (min (toInteger n) (toInteger m) - 1)
+        (Nat n, _)           -> Just (n - 1)
+        (_    , TVIntMod m)  -> Just (m - 1)
         _                    -> Nothing
 indexFront_segs ::
   W4.IsSymExprBuilder sym =>

(Curiously, there are also special cases for when the index is Z m, but since Z m isn't an instance of Integral, I'm not sure if it's even possible to reach those special cases.)

[robdockins]

Nice find @RyanGlScott, I'm sure that code is my fault. I think the Z n case is a leftover from the design period when we were deciding if it should be a member of integral or not. We can probably remove it.

On the other side of the bound, are we always guaranteed to call these functions with n > 0, or do we need to check for that explicitly?

[RyanGlScott]

On the other side of the bound, are we always guaranteed to call these functions with n > 0, or do we need to check for that explicitly?

I believe that by the time that indexFront_int function (where the code in #1359 (comment) lives) is invoked, we've already called assertIndexInBounds (here). That function should complain if n is 0, if I'm reading its code correctly. One piece of evidence to support this claim is :safe \(x : [0]) (i : Integer) -> (split`{2} x)@i throws a proper error message with a counterexample rather than panicking.