Zcmp ext

[rez5427]

I noticed #525, but I can't push to pr525.
I've temporarily implemented cm.push, cm.pop, cm.popret, and cm.popretz.
And add test files in riscv-tests riscv-software-src/riscv-tests#592,
This test file need to recompile the compiler see pr.
I run the test files on spike and this sail implementation, nothing wrong with it.
I can't find a better way to do with the assemblly.
This mapping zcmp_assembly_mapping use 200 lines to do this job.
I tried use function in assemblly, not working issue in here.
Tried to seperate {ra}-ish and stack_adj. seems like the rlist can only bind with one mapping.
Maybe sepertate rlist and spimm down below could save some lines.But it can't.

[github-actions]

Test Results

396 tests  ±0   396 ✅ ±0   0s ⏱️ ±0s
  4 suites ±0     0 💤 ±0 
  1 files   ±0     0 ❌ ±0 

Results for commit c192dba. ± Comparison against base commit b590271.

♻️ This comment has been updated with latest results.

[Timmmm]

I didn't check the actual logic at all but the Sail code needs a bit of work so I've added some hints. It's non-exhaustive, but I'll take a second look when it's improved a bit. (Or if we need this extension then I'll finish it myself! :-D)

[Timmmm]

This looks reachable to me. Where's the code that ensures this is unreachable?

[rez5427]

I add the assert in every excute like this, I don't know this is ok or not.

function clause execute (CM_POPRETZ(rlist, spimm)) = {
  assert(rlist >=_u 0b0100);

[Timmmm]

The Sail model shouldn't trigger an assert()or internal_error for any code that can actually execute. In this case your decoder lets you decode an instruction with any rlist value, so executing an instruction with rlist = 0b0000 will crash the model.

What would a real implementation do in that case?

[rez5427]

Add cm.mvsa01and cm.mva01s instructions

[Timmmm]

Ok in fairness this was pretty difficult and uses some advanced Sail features, but you can cut this down a lot. Here's my attempt. It also supports the x1, ... syntax.

I haven't tested it but I think it's quite a bit shorter (especially since you'll want to reuse rlist_stack_adj_base in the actual code), and easier to understand.

mapping zcmp_assembly_rlist : bits(4) <-> string = {
  0x4 <-> "ra",
  0x5 <-> "ra" ^ sep() ^ "s0",
  0x6 <-> "ra" ^ sep() ^ "s0-s1",
  0x7 <-> "ra" ^ sep() ^ "s0-s2",
  0x8 <-> "ra" ^ sep() ^ "s0-s3",
  0x9 <-> "ra" ^ sep() ^ "s0-s4",
  0xa <-> "ra" ^ sep() ^ "s0-s5",
  0xb <-> "ra" ^ sep() ^ "s0-s6",
  0xc <-> "ra" ^ sep() ^ "s0-s7",
  0xd <-> "ra" ^ sep() ^ "s0-s8",
  0xe <-> "ra" ^ sep() ^ "s0-s9",
  // To include s10, s11 must also be included.
  0xf <-> "ra" ^ sep() ^ "s0-s11",

  // Using X names instead of ABI names.
  0x4 <-> "x1",
  0x5 <-> "x1" ^ sep() ^ "x8",
  0x6 <-> "x1" ^ sep() ^ "x8-x9",
  0x7 <-> "x1" ^ sep() ^ "x8-x9" ^ sep() ^ "x18",
  0x8 <-> "x1" ^ sep() ^ "x8-x9" ^ sep() ^ "x18-x19",
  0x9 <-> "x1" ^ sep() ^ "x8-x9" ^ sep() ^ "x18-x20",
  0xa <-> "x1" ^ sep() ^ "x8-x9" ^ sep() ^ "x18-x21",
  0xb <-> "x1" ^ sep() ^ "x8-x9" ^ sep() ^ "x18-x22",
  0xc <-> "x1" ^ sep() ^ "x8-x9" ^ sep() ^ "x18-x23",
  0xd <-> "x1" ^ sep() ^ "x8-x9" ^ sep() ^ "x18-x24",
  0xe <-> "x1" ^ sep() ^ "x8-x9" ^ sep() ^ "x18-x25",
  0xf <-> "x1" ^ sep() ^ "x8-x9" ^ sep() ^ "x18-x27",
}

mapping negative_sign : bool <-> string = {
  false <-> "",
  true <-> "-",
}

// Note for the integer types we deal in 16s, so a value of 1 here means 16 bytes.
type stack_adj = range(1, if xlen == 32 then 7 else 10)
type stack_adj_base = range(1, if xlen == 32 then 4 else 7)

mapping stack_adj_str : string <-> stack_adj = {
  "16" <-> 1,
  "32" <-> 2,
  "48" <-> 3,
  "64" <-> 4,
  "80" <-> 5,
  "96" <-> 6,
  "112" <-> 7,
  "128" if xlen == 64 <-> 8  if xlen == 64,
  "144" if xlen == 64 <-> 9  if xlen == 64,
  "160" if xlen == 64 <-> 10 if xlen == 64,
}

mapping rlist_stack_adj_base_rv32 : bits(4) <-> range(1, 4) = {
  0x4 <-> 1,
  0x5 <-> 1,
  0x6 <-> 1,
  0x7 <-> 1,
  0x8 <-> 2,
  0x9 <-> 2,
  0xa <-> 2,
  0xb <-> 2,
  0xc <-> 3,
  0xd <-> 3,
  0xe <-> 3,
  0xf <-> 4,
}

mapping rlist_stack_adj_base_rv64 : bits(4) <-> range(1, 7) = {
  0x4 <-> 1,
  0x5 <-> 1,
  0x6 <-> 2,
  0x7 <-> 2,
  0x8 <-> 3,
  0x9 <-> 3,
  0xa <-> 4,
  0xb <-> 4,
  0xc <-> 5,
  0xd <-> 5,
  0xe <-> 6,
  0xf <-> 7,
}

mapping rlist_stack_adj_base : bits(4) <-> stack_adj_base = {
  s if xlen == 32 <-> rlist_stack_adj_base_rv32(s) if xlen == 32,
  s if xlen == 64 <-> rlist_stack_adj_base_rv64(s) if xlen == 64,
}

mapping zcmp_assembly_mapping_stack_adj : (bits(4), stack_adj, bool) <-> string = {
  (rlist, stack_adj, is_negative) <-> "{" ^ spc() ^ "ra" ^ sep() ^ "{" ^ spc() ^ zcmp_assembly_rlist(rlist) ^ spc() ^ "}" ^ sep() ^ negative_sign(is_negative) ^ stack_adj_str(stack_adj),
}

mapping zcmp_assembly_mapping : (bits(4), bits(2), bool) <-> string = {
  forwards (rlist, spimm54, is_negative) => {
    let stack_adj = rlist_stack_adj_base(rlist) + unsigned(spimm54);
    zcmp_assembly_mapping_stack_adj(rlist, stack_adj, is_negative)
  },
  backwards str => {
    let (rlist, stack_adj, is_negative) = zcmp_assembly_mapping_stack_adj(str);
    let stack_adj_offset = stack_adj - rlist_stack_adj_base(rlist);
    let spimm54 = to_bits(2, stack_adj_offset);
    // to_bits is not well typed so double check this.
    assert(unsigned(spimm54) == stack_adj_offset);
    (rlist, spimm54, is_negative)
  },
}

[rez5427]

WOW

[rez5427]

emmmm.... I temporarily write a double direction function like this

val zcmp_assembly_mapping : (bits(4), bits(2), bool) <-> string

function zcmp_assembly_mapping_forwards (rlist, spimm, is_negative) = {
  var stack_adj : int = undefined;
  stack_adj = get_stack_adj_base(rlist) + unsigned(spimm);

  "{" ^ zcmp_assembly_rlist(rlist) ^ ", " ^ BitStr(to_bits(xlen, stack_adj)) ^ ", " ^ negative_sign(is_negative) ^ "}"
}

function zcmp_assembly_mapping_forwards_matches (rlist, spimm54, is_negative) = true

function zcmp_assembly_mapping_backwards(str_input) = {
  var str = str_input;
  var rlist : bits(4) = undefined;
  var spimm54 : bits(2) = undefined;
  var is_negative : bool = false;

  if string_take(str, 7) == "cm.push" then {
    is_negative = true;
    str = string_drop(str, 9);
    
  } else if string_take(str, 6) == "cm.pop" then {
    is_negative = false;
    str = string_drop(str, 8);
  } else if string_take(str, 9) == "cm.popret" then {
    is_negative = false;
    str = string_drop(str, 11);
  } else {
    is_negative = false;
    str = string_drop(str, 12);
  };

  if string_take(str, 3) == "ra," then {
    if string_take(str, 5) == "ra, s0" then {
      rlist = zcmp_assembly_rlist(string_take(str, 5));
      str = string_drop(str, 9);
    } else {
      if string_take(str, 10) == "ra, s0-s11" then {
        rlist = zcmp_assembly_rlist(string_take(str, 10));
        str = string_drop(str, 13);
      } else {
        rlist = zcmp_assembly_rlist(string_take(str, 9));
        str = string_drop(str, 12);
      }
    }
  } else {
    rlist = zcmp_assembly_rlist(string_take(str, 2));
    str = string_drop(str, 5);
  };

  if string_take(str, 1) == "-" then {
    str = string_drop(str, 1);
  };

  var stack_adj_offset : int = 0;

  foreach (i from string_length(str) downto 1) {
    let temp_val : int = match string_take(str, 1) {
      "0" => 0,
      "1" => 1,
      "2" => 2,
      "3" => 3,
      "4" => 4,
      "5" => 5,
      "6" => 6,
      "7" => 7,
      "8" => 8,
      "9" => 9
    };
    stack_adj_offset = stack_adj_offset + temp_val;
    stack_adj_offset = stack_adj_offset * 10;
  };

  spimm54 = to_bits(2, (stack_adj_offset - get_stack_adj_base(rlist)) / 16);

  (rlist, spimm54, is_negative)
}

function zcmp_assembly_mapping_backwards_matches (str) = true

And it shows

Type error:
Tuple mapping-pattern and tuple type have different length

This Type error doesn't show where the error is in the code...
I don't know what to do now....

[Timmmm]

Yeah I occasionally see errors with no source location. Quite annoying! If you push that code and open a bug report on the Sail compiler @Alasdair is very good about fixing them.

I would guess the function types are wrong or something? They look correct to me though.

[Alasdair]

Suspect this issue with locations might be the same one as fixed in rems-project/sail@3611e46

But yes, please do report any errors without location information as bugs to Sail! If you ever decide to write a compiler I highly suggest encoding terms with location info and terms without location info as separate types in the implementation language, and avoid an 'unknown' location no matter how convenient it is.

[rez5427]

I checked spike's logic, spike use a default 0 as the stack_adj_base.

function get_stack_adj_base(rlist : bits(4)) -> int = {
  if(xlen == 32) then
    match rlist[3 .. 2] {
      0b01 => 16,
      0b10 => 32,
      0b11 => if rlist == 0b1111 then 64 else 48,
      _    => 0,
    }
  else {
    match rlist[3 .. 1] {
      0b010 => 16,
      0b011 => 32,
      0b100 => 48,
      0b101 => 64,
      0b110 => 80,
      0b111 => if rlist == 0b1111 then 112 else 96,
      _     => 0,
    }
  }
}

Here is the code in spike.

 uint64_t zcmp_stack_adjustment(int xlen) {
    reg_t stack_adj_base = 0;
    switch (rvc_rlist()) {
    case 15:
      stack_adj_base += 16;
    case 14:
      if (xlen == 64)
        stack_adj_base += 16;
    case 13:
    case 12:
      stack_adj_base += 16;
    case 11:
    case 10:
      if (xlen == 64)
        stack_adj_base += 16;
    case 9:
    case 8:
      stack_adj_base += 16;
    case 7:
    case 6:
      if (xlen == 64)
        stack_adj_base += 16;
    case 5:
    case 4:
      stack_adj_base += 16;
      break;
    }

    return stack_adj_base + rvc_spimm();
  }

And when it comes a rlist which not valid in spec, it shows a string "unsupport rlist".

struct : public arg_t {
  std::string to_string(insn_t insn) const {
    int rlist = insn.rvc_rlist();
    if (rlist >= 4) {
      switch(rlist) {
        case 4: return "{ra}";
        case 5: return "{ra, s0}";
        case 15: return "{ra, s0-s11}";
        default: return "{ra, s0-s" + std::to_string(rlist - 5)+'}';
      }
    } else {
      return "unsupport rlist";
    }
  }
} rvcm_pushpop_rlist;

I did the same logic in the sail

mapping zcmp_assembly_mapping : (bits(4), bits(2), bool) <-> string = {
  forwards (rlist, spimm54, is_negative) => {
    var stack_adj : int = undefined;
    let stack_adj_base = get_stack_adj_base(rlist);
    stack_adj = get_stack_adj_base(rlist) + unsigned(spimm54) * 16;

    if stack_adj_base == 0 then {
      "unsupport rlist" ^ sep() ^ negative_sign(is_negative) ^ dec_str(stack_adj)
    } else {
      "{" ^ zcmp_assembly_rlist(rlist) ^ "}" ^ sep() ^ negative_sign(is_negative) ^ dec_str(stack_adj)
    }
  },

Not sure this is ok or not.

[rez5427]

And it left only one warning, I checked sail it only have a parse_hex,which convert a hex string to int.
Should I add a parse_dec in sail to get rid of this warning?

Warning: Incomplete pattern match statement at model/riscv_insts_zcmp.sail:108.27-32:
108 |      let temp_val : int = match string_take(str, 1) {
    |                           ^---^
    | 
The following expression is unmatched: "??"