Sail's pattern matching checking for overlaps & exhaustiveness

[martinberger]

I have a question about Sail's semantics of pattern matching. Regarding overlapping checks, currently Sail 0.13 accepts:

val overlap : bits(5) -> string                                                                                                                 
function overlap(r) = {                                                                                                                         
  match (r) {                                                                                                                                   
    0b00000 => "zero",                                                                                                                          
    0b00000 => "hello",                                                                                                                 
    _ => "t6"                                                                                                                             
  }                                                                                                                                             
}                                                                                                                                               

without any warnings, despite the unreachable middle pattern. Regarding checks for exhaustiveness patterns, Sail accepts

val f2 :  bits(5) -> string                                                                                                                     
function f2(r) = {                                                                                                                              
  match (r) {                                                                                                                                   
    0b00000 => "zero",                                                                                                                          
    0b11111 => "t6"                                                                                                                             
  }                                                                                                                                             
}                                                                                                                                               

without warning, but both of:

val f3 :  bits(5) -> string                                                                                                                     
function f3(r) = {                                                                                                                              
  match (r) {                                                                                                                                   
    0b11111 => "t6"                                                                                                                             
  }                                                                                                                                             
}                                                                                                                                               

val f4 :  bits(5) -> string                                                                                                                     
function f4(r) = {                                                                                                                              
  match (r) {                                                                                                                                   
    0b00000 => "zero"                                                                                                                           
  }                                                                                                                                             
}                                                                                                                                               

do generate "Possible incomplete pattern match" warnings (as they should). It seems to be a bit inconsistent to warn about 31 missing patterns but not 30.

I understand that both, exhaustiveness and overlapping patterns, cannot be computed at compile time due to pattern guards. Nevertheless, I think it would be highly useful in practise to get suitable warnings, at least for the cases where no (complex) guards are used. The Ocaml / Rust / Scala compilers, for example, do this, and would have caught (the respective versions of) both problems above.

Given how difficult it is for humans to handle long bit patterns, and given the importance of single bits in processors, I think it would be highly useful to have warnings about this. Are there any plans in this direction?

[Alasdair]

I've implemented a new pattern completeness checker, that should address some of these issues:

https://github.com/rems-project/sail/commit/fe545b7f1fd1b6622abf4b1f7c33ff3e6ce6ba48

f2 now gives the warning:

Warning: Incomplete pattern match statement at [pattern_completeness.sail]:55:2-7
55 |  match (r) {                                                                                                                                   
   |  ^---^
   | 
The following expression is unmatched: 0b00001

I'll leave this issue open because I know there are some incomplete patterns it won't detect, but I've tried to make sure it doesn't generate false positives for the time being, which the previous code could do in some cases.

[martinberger]

I've implemented a new pattern completeness checker,

Great, thanks. Just to double-check, this addresses incompleteness only, not overlapping patterns?

[Alasdair]

Currently yes, although I might be able to detect overlapping patterns by modifying the code a bit as well

[martinberger]

Overlapping bit-string patterns are a real source of bugs, so I think this would be useful.

[xiak95]

val foo : forall 'n, 'n == 0 | 'n == 2 . (int('n)) -> bits(64)
function foo(n) = {
  match n { 
         0 => sail_zeros(64),
         2 => sail_ones(64)
  }
}

Hi, I would imagine that this match case should not generate incomplete warning as n is limited to either 0 or 2 , however it does, how can I make SAIL stop generating such warning ?

[Alasdair]

Currently the only way is to use a wildcard pattern for the final match.

The new pattern match completeness checker already uses Z3 for checking bitvector pattern completeness, so in theory I could extend it to check integer patterns as well. Right now the completeness checking doesn't look at the context in the match statement occurs, and just looks at the match statement itself (I also can't inspect guards, a limitation shared by most pattern completeness checking in other languages). If I added context-sensitive checking for integer patterns you could construct rather complex mixed integer-bitvector constraints, so I don't know how well it would work in practice.

[Alasdair]

Are you using the version of Sail on opam or the latest commit from git? I've recently re-written the pattern completeness checker, I don't think it will give a warning for your example with the latest git version but I'm not at a computer that can check that right now.

[Alasdair]

One final thing worth noting is you may get slightly cleaner theorem prover definitions (both Coq and Isabelle) from Sail if your patterns are 'obviously' complete, i.e. even if Sail could tell that 0 and 2 are the only possible numeric values from the surrounding constraints the completeness checker in Coq would probably not be able to, so if there is no wildcard-pattern we sometimes have to add a redundant unreachable match arm when generating theorem-prover definitions just to keep Coq and Isabelle happy.

[xiak95]

I am using the version from opam, I will try with latest version from git and let you know.

[xiak95]

Yes, the warning went away with latest version from git, so the new completeness checker does not check integers ?