Detecting overlapping mapping clauses

[Timmmm]

Suppose you're writing an ISA and you accidentally make two instruction encodings overlap, e.g:

type regidx  = bits(5)

scattered union ast

union clause ast = INSTRUCTION_A : (regidx, bits(12))
union clause ast = INSTRUCTION_B : (regidx, regidx)

val encdec : ast <-> bits(32)
scattered mapping encdec

mapping clause encdec = INSTRUCTION_A(rs1, offset)
  <-> offset @ rs1 @ 0b100 @ 0b00000 @ 0b0001001

mapping clause encdec = INSTRUCTION_B(rs1, rs2)
  <-> 0b000000000000 @ rs2 @ 0b100 @ rs1 @ 0b0001001

val decode : bits(32) -> ast
function decode(bv) = encdec(bv)

As far as I can tell, Sail will happily compile this and it will just be a case of "first one wins" in the if-elseif... chain.

It would be nice to be able to automatically detect issues like this. Is there a way to automatically check if all clauses of a mapping are fully disjoint?

If not, it doesn't seem like it would be that hard to do with an SMT solver. Can you give any hints as to how you would go about doing that? I.e. can Sail output SMT code for mappings?

Thanks!

[Alasdair]

We don't have a way to do this out of the box.

You could use the Sail SMT generation in the following way: for the function decode : bits(32) -> ast you would construct a function for each function clause decode_clause_N : bits(32) -> bits(W) returning either 1 or 0 depending on whether the clause applies, where W is a bitvector wide enough to encode the maximum clause number N. Then you would ask the SMT solver for a bitvector such that (bvadd (encode_clause_0 ... encode_clause_N)) is greater than 1, which would give you an opcode that matches multiple clauses.

[Timmmm]

Thanks that makes sense. Where would you add that code? It seems like the mappings are already gone by the time you get to Jib (by realize_mapdef?) so I guess I would maybe add something in realize_mapdef to generate the decode_clause_N functions?

[Alasdair]

For the encdec mapping you'll get a function encdec_forwards and encdec_backwards, so I would work with those. I think all the work would end up happening in the sail_smt_backend.

[Timmmm]

I had a look at the SMT backend but to be honest I couldn't follow the code at all. :-/ Fortunately I realised in this case the actual search space is only 30 bits so I can just go through all of them (takes about 30 mins on my laptop with 7 threads). That has the advantage of listing all conflicts easily instead of just finding an arbitrary one.

To do it I hacked the C backend which I can just about follow to check for multiple matches in all foo_matches() functions (hackily detected by their bool return type). Then I just call encdec_backwards_matches() in a loop.

I don't think that's a good general solution because - as far as I understand it - match is supposed to allow multiple matches, whereas mapping shouldn't (I guess? the manual doesn't say) but internally they are both lowered to E_Match or something so there is no way to distinguish them at codegen time.

I wonder if it would be worth adding a unique match feature which checks for multiple matches at runtime (or compile time if possible?). Then you could map mapping to that instead.

Anyway I'll close this so you don't have another open bug. :-) Thanks for the help!