Allow CR_multi singletons in addition to CR_one

[NicolasVanPhan]

The example code below :

mapping ap_m_encdec : bits(cap_AP_M_width) <-> option((ArchPerms, ExecutionMode)) = {
  execution_mode_encdec(M) @ bool_bits(ASR) @ bool_bits(X) @ bool_bits(R) @ bool_bits(W) @ bool_bits(C)
    if (not(ASR) | X) & (not(C) | (R | W)) & (M == execution_mode_encdec(0b0) | X) <->
  Some(struct{R, W, C, X, ASR}, M)
    if (not(ASR) | X) & (not(C) | (R | W)) & (M == execution_mode_encdec(0b0) | X),

  forwards _ => None()
}

Gives the following error :

Internal error: Unreachable code (at "src/sail_sv_backend/jib_sv.ml" line 973):
sail-cheri-riscv/src/cheri_prelude_128.sail:71.8-16:
71 |    if (not(ASR) | X) & (not(C) | (R | W)) & (M == execution_mode_encdec(0b0) | X) <->
   |        ^------^
   | Multiple return generator primitive found
   | 
   | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62   | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml", line 219, characters 34-61
   | Called from Jib_sv.Make.svir_instr in file "src/sail_sv_backend/jib_sv.ml", line 973, characters 21-96
   | Called from Libsail__Smt_gen.mapM in file "src/lib/smt_gen.ml", line 119, characters 15-18
   | Called from Libsail__Smt_gen.mapM in file "src/lib/smt_gen.ml", line 120, characters 16-25
   | Called from Libsail__Smt_gen.bind in file "src/lib/smt_gen.ml", line 104, characters 15-30
   | Called from Libsail__Smt_gen.bind in file "src/lib/smt_gen.ml", line 103, characters 14-17
   | Called from Libsail__Smt_gen.bind in file "src/lib/smt_gen.ml", line 104, characters 15-30
   | Called from Libsail__Smt_gen.bind in file "src/lib/smt_gen.ml", line 103, characters 14-17
   | 
   | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues

The error comes from the following source in the Sail compiler :

https://github.com/NicolasVanPhan/sail/blob/release-0.18/src/sail_sv_backend/jib_sv.ml#L967

Additional debug printing of the AST reveals the creturn is a CR_Multi with only 1 return element in the list

// Pseudo-code pretty-print
I_funcall
  ( creturn = CR_Multi [ "zz4414/2" ]  // list of 1 element
  , preserve_name  = false
  , arg = "zz4395/2"
  , (id = "not", _)
  ...
  )

I guess we want to allow all CR_ values as long as they contain 1 and only 1 return element, unless mistaken. That is why this MR allows CR_Multi elements (in addition to `CR_One1) if and only if they contain exactly 1 element.

With the current MR, the above code snippet compiles successfully.

[Alasdair]

I think maybe we should be maintaining the invariant that CR_multi always has at least two l-expressions, so it might be better to figure out why this is being produced in the first place.

[NicolasVanPhan]

I think maybe we should be maintaining the invariant that CR_multi always has at least two l-expressions, so it might be better to figure out why this is being produced in the first place.

Oh okay I understand, I thought CR_Multi was a more general-purpose variant to CR_One accepting 0 1 or more arguments. I'll try to investigate where this CR_Multi singleton comes from, then.

In the longer run, should we enforce this invariant through typing ? (i.e. | CR_Multi of 'a * 'a * 'a list) to make sure there are at least two 'a ? Or would it be too cumbersome ?

[NicolasVanPhan]

I didn't manage to reproduce the error on the latest sail2 branch. It only appeared on origin/release.0.18. I couldn't dig into the very root cause but the problem seems to be gone on the latest branch, so I think we can close this one.