Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix disassembly problems #456

Merged
merged 2 commits into from
May 23, 2024
Merged

fix disassembly problems #456

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
13c24db
Change immediates to be signed in assembly
KotorinMinami May 9, 2024
f6e1f25
fix format problem and prevent different name
KotorinMinami May 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
141 changes: 141 additions & 0 deletions model/hex_bits_signed.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,141 @@
/*==========================================================================*/
/* Sail */
/* */
/* Sail and the Sail architecture models here, comprising all files and */
/* directories except the ASL-derived Sail code in the aarch64 directory, */
/* are subject to the BSD two-clause licence below. */
/* */
/* The ASL derived parts of the ARMv8.3 specification in */
/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */
/* */
/* Copyright (c) 2013-2021 */
/* Kathyrn Gray */
/* Shaked Flur */
/* Stephen Kell */
/* Gabriel Kerneis */
/* Robert Norton-Wright */
/* Christopher Pulte */
/* Peter Sewell */
/* Alasdair Armstrong */
/* Brian Campbell */
/* Thomas Bauereiss */
/* Anthony Fox */
/* Jon French */
/* Dominic Mulligan */
/* Stephen Kell */
/* Mark Wassell */
/* Alastair Reid (Arm Ltd) */
/* */
/* All rights reserved. */
/* */
/* This work was partially supported by EPSRC grant EP/K008528/1 <a */
/* href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous */
/* Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA */
/* KTF funding, and donations from Arm. This project has received */
/* funding from the European Research Council (ERC) under the European */
/* Union’s Horizon 2020 research and innovation programme (grant */
/* agreement No 789108, ELVER). */
/* */
/* This software was developed by SRI International and the University of */
/* Cambridge Computer Laboratory (Department of Computer Science and */
/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */
/* and FA8750-10-C-0237 ("CTSRD"). */
/* */
/* Redistribution and use in source and binary forms, with or without */
/* modification, are permitted provided that the following conditions */
/* are met: */
/* 1. Redistributions of source code must retain the above copyright */
/* notice, this list of conditions and the following disclaimer. */
/* 2. Redistributions in binary form must reproduce the above copyright */
/* notice, this list of conditions and the following disclaimer in */
/* the documentation and/or other materials provided with the */
/* distribution. */
/* */
/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */
/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */
/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */
/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */
/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */
/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */
/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */
/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */
/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */
/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */
/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */
/* SUCH DAMAGE. */
/*==========================================================================*/

$ifndef _HEX_BITS_SIGNED
$define _HEX_BITS_SIGNED

$include <vector.sail>
$include <string.sail>

val parse_hex_bits_signed : forall 'n, 'n > 0. (int('n), string) -> bits('n)
val valid_hex_bits_signed : forall 'n, 'n > 0. (int('n), string) -> bool

val hex_bits_signed: forall 'n, 'n > 0. bits('n) <-> (int('n), string)
Timmmm marked this conversation as resolved.
Show resolved Hide resolved

function hex_bits_signed_forwards(bv) = {
if signed(bv) < 0
then (length(bv), concat_str("-", hex_str(unsigned(not_vec(bv) + 1))))
else (length(bv), hex_str(unsigned(bv)))
}
function hex_bits_signed_forwards_matches(bv) = true

function parse_hex_bits_signed(n, str) = {
if string_take(str, 1) == "-"
then {
let str_ = string_drop(str, 1);
Timmmm marked this conversation as resolved.
Show resolved Hide resolved
let bv = parse_hex_bits(n, str_);
not_vec(bv) + 1
}
else parse_hex_bits(n, str)
}

function valid_hex_bits_signed(n, str) = {
if string_take(str, 1) == "-"
then valid_hex_bits(n, string_drop(str, 1))
else valid_hex_bits(n, str)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's not true? An N-bit signed value is only valid if it's an N-1-bit signed value or it's exactly -(1 << N). This would, for example, allow parsing 0xff as a signed 8-bit value.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This function is designed to ensure the validity when converting from a string back to an integer. It should correspond to the hex_bits_signed_forwards function.
When using the hex_bits_signed_forwards function to convert a signed numerical value to a string, it will convert negative numbers to their absolute values and then convert them to strings. Additionally, a negative sign is added at the beginning of the result. This validation is specifically tied to this function. When calling this function, it should be ensured that the input parameter is a string converted from hex_bits_signed_forwards and that the number of bits matches.
I believe that in other SAIL files, the calls to this function meet these requirements, as other ASTs only invoke it when the value at this location should be interpreted as a signed number, as mentioned in the issue #21 .
I believe these modifications only make the output of the SAIL simulator more user-friendly and accurate, and they should not cause any other issues.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I know what this function is for. I'm saying it's buggy, because it accepts more inputs than it should.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I understand then, so I should no matter what, check if the bleedin' string passed in is either a non-negative number or a minus followed by a positive number, ain't it? Just let me have a think on the best way to go about it...

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good spot, though I think the behaviour here is the same as the existing unsigned one:

function hex_bits_backwards(n, str) = parse_hex_bits(n, str)
function hex_bits_backwards_matches(n, str) = valid_hex_bits(n, str)

void parse_hex_bits(lbits *res, const mpz_t n, const_sail_string hex)
{
  if (strncmp(hex, "0x", 2) != 0) {
    goto failure;
  }

  mpz_t value;
  mpz_init(value);
  if (mpz_set_str(value, hex + 2, 16) == 0) {
    res->len = mpz_get_ui(n);
    mpz_set(*res->bits, value);
    mpz_clear(value);
    return;
  }
  mpz_clear(value);

  // On failure, we return a zero bitvector of the correct width
failure:
  res->len = mpz_get_ui(n);
  mpz_set_ui(*res->bits, 0);
}

bool valid_hex_bits(const mpz_t n, const_sail_string hex) {
  if (strncmp(hex, "0x", 2) != 0) {
    return false;
  }

  for (int i = 2; i < strlen(hex); i++) {
    char c = hex[i];
    if (!((c >= '0' && c <= '9') || (c >= 'a' && c <= 'f') || (c >= 'A' && c <= 'F'))) {
      return false;
    }
  }

  return true;
}

If you do let foo : bits(8) = hex_bits_16("0xFFFF"); it will set res->len to 8 but res->bits to 0xFFFF. IIRC I think that's ok from lbits point of view - you're allowed to have "extra bits"; they're just truncated. Don't quote me on that though, it's been a while since I read sail.c.

Obviously that isn't ideal though. It probably makes sense for valid_hex_bits to actually do something with n. You only need to check the total length and the first non-zero digit so it shouldn't be too hard.

Seeing as that code needs changes I wonder if it makes more sense to just add signed support at the same time in sail.c.

On the other hand, given that it's an existing bug maybe it shouldn't block this? @Alasdair any thoughts?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See: rems-project/sail#538

Note that the potential for anything to actually go wrong here is very slim, because we statically check that the string parsing part of the mapping has no semantic effect on the model - which means it never get executed, and therefore the actual behavior of the primitive in the Sail library is mostly irrelevant.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Alasdair So, if I understand correctly, you're saying that I just need to keep the solution from my last commit? And this buggy problem will be resolved in the new version release of Sail? Does that mean I can revert the commit and the code will move on to the next review? If that's the case, thank you for your help and clarification. Otherwise, could you please provide me with some further advice?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we statically check that the string parsing part of the mapping has no semantic effect on the model

That's really interesting - can you explain more how/where that works? Presumably this check can be disabled otherwise you can't actually use the reverse mapping?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@KotorinMinami yes, that seems right

@Timmmm Internally we keep track of what side effects expressions have, and anything with a string append pattern gets specially marked. It would be good to expand this check, because model checkers in EDA tools don't typically have good support for SystemVerilog strings, so if you want to do any kind of model checking with the Sail spec you need to ensure that the semantics doesn't rely on logic involving strings (which would be somewhat tasteless in an ISA spec anyway). Right now this does mean there is no practical way to use the 'string -> ast' side of the mapping , other than as part of the documentation generation flow.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@jrtc27 @Alasdair Could you please spare some time to move on to the next review ?

}

function hex_bits_signed_backwards(n, str) = parse_hex_bits_signed(n, str)
function hex_bits_signed_backwards_matches(n, str) = valid_hex_bits_signed(n, str)

mapping hex_bits_signed_1 : bits(1) <-> string = { hex_bits_signed(1, s) <-> s }
mapping hex_bits_signed_2 : bits(2) <-> string = { hex_bits_signed(2, s) <-> s }
mapping hex_bits_signed_3 : bits(3) <-> string = { hex_bits_signed(3, s) <-> s }
mapping hex_bits_signed_4 : bits(4) <-> string = { hex_bits_signed(4, s) <-> s }
mapping hex_bits_signed_5 : bits(5) <-> string = { hex_bits_signed(5, s) <-> s }
mapping hex_bits_signed_6 : bits(6) <-> string = { hex_bits_signed(6, s) <-> s }
mapping hex_bits_signed_7 : bits(7) <-> string = { hex_bits_signed(7, s) <-> s }
mapping hex_bits_signed_8 : bits(8) <-> string = { hex_bits_signed(8, s) <-> s }
mapping hex_bits_signed_9 : bits(9) <-> string = { hex_bits_signed(9, s) <-> s }

mapping hex_bits_signed_10 : bits(10) <-> string = { hex_bits_signed(10, s) <-> s }
mapping hex_bits_signed_11 : bits(11) <-> string = { hex_bits_signed(11, s) <-> s }
mapping hex_bits_signed_12 : bits(12) <-> string = { hex_bits_signed(12, s) <-> s }
mapping hex_bits_signed_13 : bits(13) <-> string = { hex_bits_signed(13, s) <-> s }
mapping hex_bits_signed_14 : bits(14) <-> string = { hex_bits_signed(14, s) <-> s }
mapping hex_bits_signed_15 : bits(15) <-> string = { hex_bits_signed(15, s) <-> s }
mapping hex_bits_signed_16 : bits(16) <-> string = { hex_bits_signed(16, s) <-> s }
mapping hex_bits_signed_17 : bits(17) <-> string = { hex_bits_signed(17, s) <-> s }
mapping hex_bits_signed_18 : bits(18) <-> string = { hex_bits_signed(18, s) <-> s }
mapping hex_bits_signed_19 : bits(19) <-> string = { hex_bits_signed(19, s) <-> s }

mapping hex_bits_signed_20 : bits(20) <-> string = { hex_bits_signed(20, s) <-> s }
mapping hex_bits_signed_21 : bits(21) <-> string = { hex_bits_signed(21, s) <-> s }
mapping hex_bits_signed_22 : bits(22) <-> string = { hex_bits_signed(22, s) <-> s }
mapping hex_bits_signed_23 : bits(23) <-> string = { hex_bits_signed(23, s) <-> s }
mapping hex_bits_signed_24 : bits(24) <-> string = { hex_bits_signed(24, s) <-> s }
mapping hex_bits_signed_25 : bits(25) <-> string = { hex_bits_signed(25, s) <-> s }
mapping hex_bits_signed_26 : bits(26) <-> string = { hex_bits_signed(26, s) <-> s }
mapping hex_bits_signed_27 : bits(27) <-> string = { hex_bits_signed(27, s) <-> s }
mapping hex_bits_signed_28 : bits(28) <-> string = { hex_bits_signed(28, s) <-> s }
mapping hex_bits_signed_29 : bits(29) <-> string = { hex_bits_signed(29, s) <-> s }

mapping hex_bits_signed_30 : bits(30) <-> string = { hex_bits_signed(30, s) <-> s }
mapping hex_bits_signed_31 : bits(31) <-> string = { hex_bits_signed(31, s) <-> s }
mapping hex_bits_signed_32 : bits(32) <-> string = { hex_bits_signed(32, s) <-> s }

$endif _HEX_BITS_SIGNED
1 change: 1 addition & 0 deletions model/prelude.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ $include <vector_dec.sail>
$include <regfp.sail>
$include <generic_equality.sail>
$include "hex_bits.sail"
$include "hex_bits_signed.sail"


val not_bit : bit -> bit
Expand Down
16 changes: 8 additions & 8 deletions model/riscv_insts_base.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ mapping utype_mnemonic : uop <-> string = {
}

mapping clause assembly = UTYPE(imm, rd, op)
<-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm)
<-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_20(imm)

/* ****************************************************************** */
union clause ast = RISCV_JAL : (bits(21), regidx)
Expand Down Expand Up @@ -83,7 +83,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
/* TODO: handle 2-byte-alignment in mappings */

mapping clause assembly = RISCV_JAL(imm, rd)
<-> "jal" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_21(imm)
<-> "jal" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_21(imm)

/* ****************************************************************** */
union clause ast = RISCV_JALR : (bits(12), regidx, regidx)
Expand All @@ -92,7 +92,7 @@ mapping clause encdec = RISCV_JALR(imm, rs1, rd)
<-> imm @ rs1 @ 0b000 @ rd @ 0b1100111

mapping clause assembly = RISCV_JALR(imm, rs1, rd)
<-> "jalr" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_12(imm) ^ "(" ^ reg_name(rs1) ^ ")"
<-> "jalr" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_12(imm) ^ "(" ^ reg_name(rs1) ^ ")"

/* see riscv_jalr_seq.sail or riscv_jalr_rmem.sail for the execute clause. */

Expand Down Expand Up @@ -153,7 +153,7 @@ mapping btype_mnemonic : bop <-> string = {
}

mapping clause assembly = BTYPE(imm, rs2, rs1, op)
<-> btype_mnemonic(op) ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_13(imm)
<-> btype_mnemonic(op) ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_signed_13(imm)

/* ****************************************************************** */
union clause ast = ITYPE : (bits(12), regidx, regidx, iop)
Expand Down Expand Up @@ -195,7 +195,7 @@ mapping itype_mnemonic : iop <-> string = {
}

mapping clause assembly = ITYPE(imm, rs1, rd, op)
<-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
<-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_signed_12(imm)

/* ****************************************************************** */
union clause ast = SHIFTIOP : (bits(6), regidx, regidx, sop)
Expand Down Expand Up @@ -368,7 +368,7 @@ mapping maybe_u = {
}

mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl)
<-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_12(imm) ^ "(" ^ reg_name(rs1) ^ ")"
<-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_12(imm) ^ "(" ^ reg_name(rs1) ^ ")"

/* ****************************************************************** */
union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool)
Expand Down Expand Up @@ -421,7 +421,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
}

mapping clause assembly = STORE(imm, rs2, rs1, size, aq, rl)
<-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
<-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_signed_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"

/* ****************************************************************** */
union clause ast = ADDIW : (bits(12), regidx, regidx)
Expand All @@ -439,7 +439,7 @@ function clause execute (ADDIW(imm, rs1, rd)) = {

mapping clause assembly = ADDIW(imm, rs1, rd)
if sizeof(xlen) == 64
<-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
<-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_signed_12(imm)
if sizeof(xlen) == 64

/* ****************************************************************** */
Expand Down
20 changes: 10 additions & 10 deletions model/riscv_insts_cext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ function clause execute (C_ADDI(nzi, rsd)) = {

mapping clause assembly = C_ADDI(nzi, rsd)
if nzi != 0b000000 & rsd != zreg
<-> "c.addi" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(nzi)
<-> "c.addi" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_signed_6(nzi)
if nzi != 0b000000 & rsd != zreg

/* ****************************************************************** */
Expand All @@ -147,7 +147,7 @@ function clause execute (C_JAL(imm)) =

mapping clause assembly = C_JAL(imm)
if sizeof(xlen) == 32
<-> "c.jal" ^ spc() ^ hex_bits_12(imm @ 0b0)
<-> "c.jal" ^ spc() ^ hex_bits_signed_12(imm @ 0b0)
if sizeof(xlen) == 32

/* ****************************************************************** */
Expand All @@ -163,7 +163,7 @@ function clause execute (C_ADDIW(imm, rsd)) =

mapping clause assembly = C_ADDIW(imm, rsd)
if sizeof(xlen) == 64
<-> "c.addiw" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(imm)
<-> "c.addiw" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_signed_6(imm)
if sizeof(xlen) == 64

/* ****************************************************************** */
Expand All @@ -181,7 +181,7 @@ function clause execute (C_LI(imm, rd)) = {

mapping clause assembly = C_LI(imm, rd)
if rd != zreg
<-> "c.li" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(imm)
<-> "c.li" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_6(imm)
if rd != zreg

/* ****************************************************************** */
Expand All @@ -199,7 +199,7 @@ function clause execute (C_ADDI16SP(imm)) = {

mapping clause assembly = C_ADDI16SP(imm)
if imm != 0b000000
<-> "c.addi16sp" ^ spc() ^ hex_bits_6(imm)
<-> "c.addi16sp" ^ spc() ^ hex_bits_signed_6(imm)
if imm != 0b000000

/* ****************************************************************** */
Expand All @@ -217,7 +217,7 @@ function clause execute (C_LUI(imm, rd)) = {

mapping clause assembly = C_LUI(imm, rd)
if rd != zreg & rd != sp & imm != 0b000000
<-> "c.lui" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(imm)
<-> "c.lui" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_signed_6(imm)
if rd != zreg & rd != sp & imm != 0b000000

/* ****************************************************************** */
Expand Down Expand Up @@ -268,7 +268,7 @@ function clause execute (C_ANDI(imm, rsd)) = {
}

mapping clause assembly = C_ANDI(imm, rsd)
<-> "c.andi" ^ spc() ^ creg_name(rsd) ^ sep() ^ hex_bits_6(imm)
<-> "c.andi" ^ spc() ^ creg_name(rsd) ^ sep() ^ hex_bits_signed_6(imm)

/* ****************************************************************** */
union clause ast = C_SUB : (cregidx, cregidx)
Expand Down Expand Up @@ -378,7 +378,7 @@ function clause execute (C_J(imm)) =
execute(RISCV_JAL(sign_extend(imm @ 0b0), zreg))

mapping clause assembly = C_J(imm)
<-> "c.j" ^ spc() ^ hex_bits_11(imm)
<-> "c.j" ^ spc() ^ hex_bits_signed_11(imm)

/* ****************************************************************** */
union clause ast = C_BEQZ : (bits(8), cregidx)
Expand All @@ -390,7 +390,7 @@ function clause execute (C_BEQZ(imm, rs)) =
execute(BTYPE(sign_extend(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BEQ))

mapping clause assembly = C_BEQZ(imm, rs)
<-> "c.beqz" ^ spc() ^ creg_name(rs) ^ sep() ^ hex_bits_8(imm)
<-> "c.beqz" ^ spc() ^ creg_name(rs) ^ sep() ^ hex_bits_signed_8(imm)

/* ****************************************************************** */
union clause ast = C_BNEZ : (bits(8), cregidx)
Expand All @@ -402,7 +402,7 @@ function clause execute (C_BNEZ(imm, rs)) =
execute(BTYPE(sign_extend(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BNE))

mapping clause assembly = C_BNEZ(imm, rs)
<-> "c.bnez" ^ spc() ^ creg_name(rs) ^ sep() ^ hex_bits_8(imm)
<-> "c.bnez" ^ spc() ^ creg_name(rs) ^ sep() ^ hex_bits_signed_8(imm)

/* ****************************************************************** */
union clause ast = C_SLLI : (bits(6), regidx)
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_fext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -344,7 +344,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
mapping clause assembly = LOAD_FP(imm, rs1, rd, width)
<-> "fl" ^ size_mnemonic(width)
^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ hex_bits_12(imm)
^ sep() ^ hex_bits_signed_12(imm)
^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"

/* ****************************************************************** */
Expand Down Expand Up @@ -419,7 +419,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
mapping clause assembly = STORE_FP(imm, rs2, rs1, width)
<-> "fs" ^ size_mnemonic(width)
^ spc() ^ freg_name(rs2)
^ sep() ^ hex_bits_12(imm)
^ sep() ^ hex_bits_signed_12(imm)
^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"

/* ****************************************************************** */
Expand Down