Uninformative error message `SMT solver returned unexpected status 1`

[martinberger]

The following function fails to compile, and terminates with the uninformative error message SMT solver returned unexpected status 1 using Sail 0.17 (sail @ opam-v2.1.5).

type regno ('n : Int), 0 <= 'n < 32 = int('n)

function f() -> unit = {
   foreach (reg from 0 to 31) { let _ : regno(reg) = reg; }
}

Likewise with this variant:

val g : forall 'n, 0 <= 'n < 32. regno('n) -> unit
function g(reg) = {
   let _ : regno(reg) = reg
}

I can understand why this program is rejected (despite there being enough constraints to make the programs work) since the type checker is looking for a singleton kind as argument for regno(.), but it would be nice to have a more informative error message.

[bacam]

The error it should be reporting is that reg in regno(reg) isn't a type variable. Unfortunately we expand type synonyms before checking whether the arguments are well-formed, so reg leaks into the SMT problem without being bound. @Alasdair Maybe we don't need to expand type synonyms in Type_env.wf_typ?

Your examples can be made to work by using regno('loop_reg) instead. I'm not sure if we should document that, or introduce some foreach ('reg ... syntax analogous to let 'reg = ... instead.

[martinberger]

That's interesting. My use case is where I have an enum (which will be a processor state) and with each element of the enum I have an irregular list (or vector) of registers.

enum Zc with as_bits -> nat = {                                                                      
   Zc1 => 7,                                                                                         
   Zc2 => 666,                                                                                       
   ...,                                                                                              
   Zc17 => 5                                                                                         
}                                                                                                    

function active_regs(version : Zc) -> list(regno) = {                                                
   match version {                                                                                   
      Zc1 => [| sp |]                                                                                
      Zc2 => [| sp, ra, s0, s1, s2, s4, s5 |]                                                                        
      ...,                                                                                           
      Zc17 => [| s1, s5, s8 |]                                                                               
   }                                                                                                 
}

Then, in some execute clauses, I need to iterate over the list or vector, depending on the processor state given by the enum. Something like this:

function clause execute ... = {                                                                      
   let zc = active_Zc_version()                                                                      
   foreach (reg in active_regs(zc)) {                                                                
      ...                                                                                            
      reg = f(as_bits(zc))                                                                           
      ...                                                                                            
      RETIRE_SUCCESS                                                                                 
   }                                                                                                 
}

If I could get the type-system to check these irregular lists of registers, then there would be more type-safety. But it's not necessary. I am currently doing all this without using fancy types. It's fine.