Question about array slicing

[martinberger]

Using Sail 0.17.1: in the following program the construction of tmp1 and tmp2 causes an error, regardless of whether the default Order is inc or dec.

  $include <prelude.sail>
  //default Order inc                                                                                                                                                                     
  default Order dec

  function main() -> unit = {
     let v : bits(8) = [bitzero, bitzero, bitone, bitzero, bitzero, bitzero, bitone, bitzero];
     let tmp1 = v[2 .. 1]; // ERROR                                                                                                                                                      
     let tmp2 : bits(2) = v[2 .. 1]; // ERROR                                                                                                                                             
     let tmp3 = v[1 .. 2]; // Fine                                                                                                                                                       
     let tmp4 : bits(2) = v[1 .. 2]; // Fine                                                                                                                                             
     ()
  }

Why? The specification says "The indexes are always supplied with the index closest to the MSB being given first" , see https://alasdair.github.io/#_accessing_and_updating_vectors. So the construction of tmp1 and tmp2 should be fine.

[Alasdair]

It should be v[2 .. 1] with decreasing order and v[1 .. 2] with increasing. If v[2 .. 1] is not working with default Order dec then something is quite wrong.

[martinberger]

Agreed. I get

  sail -c error.sail
  Type error:
  error.sail:7.15-24:
  7 |   let tmp1  = v[2 .. 1]; // ERROR
    |               ^-------^
    | No overloading for vector_subrange, tried:
    | * subrange_bits
    |    Could not resolve quantifiers for subrange_bits
    |    * (0 <= 2 & (2 <= 1 & 1 < 8))

but I don't know why. Order dec vs inc makes no difference to this error message.

[Alasdair]

I'm on a train right now, so I'll have to take a look myself later. That is the error I would expect with that line and default Order inc. With your file default Order dec should give almost the same error, but just pointing at the tmp3 line.

[bauereiss]

The position of the default Order declaration seems to be significant. If I move it before the $include, I get the expected errors.

[Alasdair]

Yes, I think I this might be a duplicate of https://github.com/rems-project/sail/issues/382

[martinberger]

I've just swapped the default Order statement with the $include and now I get the expected behaviour.

This is surprising behaviour. (I also tried with bitvectors where I stated the order in the bitvector type declaration and got similar issues.) I think the error message should be different. Alternatively, the manual should state that thedefault Order statement should come before all $include.

[Alasdair]

Yes, I plan on fixing this before the next release the only question is whether to make it an error or make it work by scanning all the definitions for the order before anything else

[Alasdair]

Should be fixed by #444