search

katamaran-project / sail-minimal-caps

Other
0 stars 0 forks source link

execute(CJALR) #1

Open fvogels opened 10 months ago

fvogels commented 10 months ago 
function clause execute(CJALR(cd, cs, imm)) = {
  // [...]
  let imm = sail_zero_extend(imm, integer_size);
  let c' = updatePCPerm({c with cap_cursor = c.cap_cursor + imm});
  // [...]
}

imm gets zero-extended, but shouldn't this be sign-extended? From the corresponding CHERI RISC-V Sail code:

function clause execute(CJALR(imm, cs1, cd)) = {
  let cs1_val = C(cs1);
  let off : xlenbits = sign_extend(imm);    // <--
  let newPC = [cs1_val.address + off with 0 = bitzero]; /* clear bit zero as for RISCV JALR */
  // [...]

Also note that the lsb is set to 0.

capt-hb commented 10 months ago

Yes, it should indeed be sign-extended. These (and maybe other uncovered) bugs are remnants of the "bi-translation" of MinimalCaps (which was initially written directly in microSail). Note that these bugs are only part of the Sail spec of MinimalCaps. The microSail implementation doesn't use bitvectors yet (nor has it any kind of alignment restrictions).