Skip to content

Commit

Permalink
Fix decode of CHERI instructions following upstream change to decode …
Browse files Browse the repository at this point in the history
…hook.

riscv/sail-riscv#205 changed the way decode hooks used to override existing RISC-V instructions work.
This commit imports changes from upstream to adapt to the change. Relevant commit:
CTSRD-CHERI/sail-cheri-riscv@d760e53
  • Loading branch information
ronorton committed Feb 13, 2024
1 parent 4da8c3f commit ab7d014
Show file tree
Hide file tree
Showing 6 changed files with 450 additions and 89 deletions.
11 changes: 6 additions & 5 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,10 @@ SAIL_DEFAULT_INST = $(SAIL_RISCV_MODEL_DIR)/riscv_insts_base.sail \
$(SAIL_RISCV_MODEL_DIR)/riscv_insts_cext.sail \
$(SAIL_RISCV_MODEL_DIR)/riscv_insts_mext.sail \
$(SAIL_RISCV_MODEL_DIR)/riscv_insts_zicsr.sail \
$(SAIL_CHERI_MODEL_DIR)/cheri_insts.sail
$(SAIL_CHERI_MODEL_DIR)/cheri_insts_begin.sail \
$(SAIL_CHERI_MODEL_DIR)/cheri_insts.sail \
$(SAIL_CHERI_MODEL_DIR)/cheri_insts_cext.sail \
$(SAIL_CHERI_MODEL_DIR)/cheri_insts_end.sail
# $(SAIL_FD_INST) \
# $(SAIL_RISCV_MODEL_DIR)/riscv_insts_aext.sail
SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) $(SAIL_RISCV_MODEL_DIR)/riscv_jalr_seq.sail
Expand Down Expand Up @@ -110,14 +113,12 @@ SAIL_ARCH_RVFI_SRCS = \

SAIL_STEP_SRCS = $(SAIL_RISCV_MODEL_DIR)/riscv_step_common.sail \
$(SAIL_CHERI_MODEL_DIR)/cheri_step_ext.sail \
$(SAIL_RISCV_MODEL_DIR)/riscv_decode_ext.sail \
$(SAIL_CHERI_MODEL_DIR)/cheri_decode_ext.sail \
$(SAIL_RISCV_MODEL_DIR)/riscv_fetch.sail \
$(SAIL_RISCV_MODEL_DIR)/riscv_step.sail

RVFI_STEP_SRCS = $(SAIL_RISCV_MODEL_DIR)/riscv_step_common.sail \
$(SAIL_CHERI_MODEL_DIR)/cheri_step_rvfi.sail \
$(SAIL_RISCV_MODEL_DIR)/riscv_decode_ext.sail \
$(SAIL_CHERI_MODEL_DIR)/cheri_decode_ext.sail \
$(SAIL_RISCV_MODEL_DIR)/riscv_fetch_rvfi.sail \
$(SAIL_RISCV_MODEL_DIR)/riscv_step.sail
Expand Down Expand Up @@ -152,14 +153,14 @@ SAIL:=$(SAIL_DIR)/sail
export SAIL_DIR
else
# Use sail from opam package
SAIL_DIR=$(shell opam config var sail:share)
SAIL_DIR=$(shell opam var sail:share)
SAIL:=sail
endif
SAIL_LIB_DIR:=$(SAIL_DIR)/lib
export SAIL_LIB_DIR
SAIL_SRC_DIR:=$(SAIL_DIR)/src

LEM_DIR?=$(shell opam config var lem:share)
LEM_DIR?=$(shell opam var lem:share)
export LEM_DIR
#Coq BBV library hopefully checked out in directory above us
BBV_DIR?=../bbv
Expand Down
25 changes: 12 additions & 13 deletions src/cheri_decode_ext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -60,19 +60,18 @@
/* SUCH DAMAGE. */
/*=======================================================================================*/

function ext_decode_compressed(bv : bits(16)) -> ast = {
match(encdec_compressed_capmode(bv)) {
/* Use the default decoding for non-capmode encodings. */
NOT_C_CAPMODE(_) => encdec_compressed(bv),
C_CAPMODE_AST => C_CAPMODE_AST
}
}

function ext_post_decode_hook(x) : ast -> ast = {
match(x) {
UTYPE(imm, 0b0 @ cd : bits(4), RISCV_AUIPC) => AUIPCC(imm, 0b0 @ cd),
RISCV_JAL(imm, cd) => CJAL(imm, cd),
RISCV_JALR(imm, cs1, cd) => CJALR(imm, cs1, cd),
C_JAL(imm) => CJAL(sign_extend(imm @ 0b0), ra),
C_JALR(rs1) => CJALR(zero_extend(0b0), rs1, ra),
C_J(imm) => CJAL(sign_extend(imm @ 0b0), zreg),
C_JR(rs1) => CJALR(zero_extend(0b0), rs1, zreg),
C_MV(rd, 0b1 @ rs2 : bits(4)) => CMove(rd, 0b0 @ rs2),
C_ADDI4SPN(rdc, nzimm) => CIncAddrImmediate(creg2reg_idx(rdc), sp, zero_extend(nzimm @ 0b00)),
C_ADDI16SP(imm) => CIncAddrImmediate(sp, sp, sign_extend(imm @ 0x0)),
OTHERS => OTHERS
function ext_decode(bv : bits(32)) -> ast = {
match(encdec_capmode(bv)) {
/* Use the default decoding for non-capmode encodings. */
NOT_CAPMODE(_) => encdec(bv),
CAPMODE_AST => CAPMODE_AST
}
}
89 changes: 18 additions & 71 deletions src/cheri_insts.sail
Original file line number Diff line number Diff line change
Expand Up @@ -958,74 +958,21 @@ mapping clause encdec = StoreCapImm(cs2, rs1, off7 @ off5) <-> off7 : bits(7) @
mapping clause assembly = LoadCapImm(cd, rs1, offset) <-> "lc" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ hex_bits_12(offset) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
mapping clause assembly = StoreCapImm(cs2, rs1, offset) <-> "sc" ^ spc() ^ cap_reg_name(cs2) ^ sep() ^ hex_bits_12(offset) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"

/* ****************************************************************** */
/* Use encoding for C.LDSP (RV64) / C.FLWSP (RV32) for CLCSP */

union clause ast = C_CLCSP : (bits(6), regidx)

mapping clause encdec_compressed = C_CLCSP(ui86 @ ui5 @ ui43, rd)
if rd != zreg
<-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
if rd != zreg

function clause execute (C_CLCSP(uimm, rd)) = {
let imm : bits(12) = zero_extend(uimm @ 0b000);
execute(LoadCapImm(rd, sp, imm))
}

mapping clause assembly = C_CLCSP(uimm, rd)
if rd != zreg
<-> "c.clcsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm)
if rd != zreg

/* ****************************************************************** */
/* Use encoding for C.SDSP (RV64) / C.FSWSP (RV32) for CSCSP */

union clause ast = C_CSCSP : (bits(6), regidx)

mapping clause encdec_compressed = C_CSCSP(ui86 @ ui53, rs2)
<-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10

function clause execute (C_CSCSP(uimm, rs2)) = {
let imm : bits(12) = zero_extend(uimm @ 0b000);
execute(StoreCapImm(rs2, sp, imm))
}

mapping clause assembly = C_CSCSP(uimm, rs2)
<-> "c.cscsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_6(uimm)

/* ****************************************************************** */
/* The encoding for C.LD (RV64) and C.FLW (RV32) is used for C.CLC */

union clause ast = C_CLC : (bits(5), cregidx, cregidx)

mapping clause encdec_compressed = C_CLC(ui76 @ ui53, rs1, rd)
<-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00

function clause execute (C_CLC(uimm, rsc, rdc)) = {
let imm : bits(12) = zero_extend(uimm @ 0b000);
let rd = creg2reg_idx(rdc);
let rs = creg2reg_idx(rsc);
execute(LoadCapImm(rd, rs, imm))
}

mapping clause assembly = C_CLC(uimm, rsc, rdc)
<-> "c.clc" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_8(uimm @ 0b000)

/* ****************************************************************** */
/* The encoding for C.SD (RV64) and C.FSW (RV32) is used for C.CSC */

union clause ast = C_CSC : (bits(5), cregidx, cregidx)

mapping clause encdec_compressed = C_CSC(ui76 @ ui53, rs1, rs2)
<-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00

function clause execute (C_CSC(uimm, rsc1, rsc2)) = {
let imm : bits(12) = zero_extend(uimm @ 0b000);
let rs1 = creg2reg_idx(rsc1);
let rs2 = creg2reg_idx(rsc2);
execute(StoreCapImm(rs2, rs1, imm))
}

mapping clause assembly = C_CSC(uimm, rsc1, rsc2)
<-> "c.csc" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_8(uimm @ 0b000)
/*
* Encoding/assembly mappings for instructions that overlap existing RISC-V
* encodings. This does not include loads/stores since they are not decoded
* differently, but instead use hooks for semantic differences. CHERIoT
* only supports cap mode see these always have priority over the RISC-V
* ones.
*/
mapping clause encdec_capmode = AUIPCC(imm, cd) <-> imm @ cd @ 0b0010111
mapping clause assembly = AUIPCC(imm, cd)
<-> "auipcc" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ hex_bits_20(imm)
mapping clause encdec_capmode = CJALR(imm, cs1, cd) <-> imm @ cs1 @ 0b000 @ cd @ 0b1100111
mapping clause assembly = CJALR(imm, cs1, cd)
<-> "cjalr" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ hex_bits_12(imm)
/* See `mapping clause encdec = RISCV_JAL` for why we have to use this syntax */
mapping clause encdec_capmode = CJAL(imm_19 @ imm_7_0 @ imm_8 @ imm_18_13 @ imm_12_9 @ 0b0, cd)
<-> imm_19 : bits(1) @ imm_18_13 : bits(6) @ imm_12_9 : bits(4) @ imm_8 : bits(1) @ imm_7_0 : bits(8) @ cd @ 0b1101111
mapping clause assembly = CJAL(imm, cd)
<-> "cjal" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ hex_bits_21(imm)
71 changes: 71 additions & 0 deletions src/cheri_insts_begin.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
/*=======================================================================================*/
/* CHERI RISCV Sail Model */
/* */
/* This CHERI Sail RISC-V architecture model here, comprising all files and */
/* directories except for the snapshots of the Lem and Sail libraries in the */
/* prover_snapshots directory (which include copies of their licenses), is subject */
/* to the BSD two-clause licence below. */
/* */
/* Copyright (c) 2017-2021 */
/* Alasdair Armstrong */
/* Thomas Bauereiss */
/* Brian Campbell */
/* Jessica Clarke */
/* Nathaniel Wesley Filardo (contributions prior to July 2020, thereafter Microsoft) */
/* Alexandre Joannou */
/* Microsoft */
/* Prashanth Mundkur */
/* Robert Norton-Wright (contributions prior to March 2020, thereafter Microsoft) */
/* Alexander Richardson */
/* Peter Rugg */
/* Peter Sewell */
/* */
/* All rights reserved. */
/* */
/* This software was developed by SRI International and the University of */
/* Cambridge Computer Laboratory (Department of Computer Science and */
/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */
/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */
/* SSITH research programme. */
/* */
/* This software was developed within the Rigorous Engineering of */
/* Mainstream Systems (REMS) project, partly funded by EPSRC grant */
/* EP/K008528/1, at the Universities of Cambridge and Edinburgh. */
/* */
/* This project has received funding from the European Research Council */
/* (ERC) under the European Union’s Horizon 2020 research and innovation */
/* programme (grant agreement 789108, ELVER). */
/* */
/* 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. */
/*=======================================================================================*/

/*
* We add a separate capability-mode encdec clause to handle encodings that overlap
* with baseline RISC-V encodings.
*/
val encdec_capmode : ast <-> bits(32) effect {rreg}
scattered mapping encdec_capmode

val encdec_compressed_capmode : ast <-> bits(16) effect {rreg}
scattered mapping encdec_compressed_capmode
Loading

0 comments on commit ab7d014

Please sign in to comment.