Bumped sail-riscv and started working around things, but this does no…

…t work yet
CTSRD-CHERI · Apr 18, 2024 · 2f1664d · 2f1664d
1 parent 6e3613a
commit 2f1664d
Show file tree

Hide file tree

Showing 6 changed files with 19 additions and 9 deletions.
diff --git a/Makefile b/Makefile
@@ -19,6 +19,7 @@ CHERI_CAP_RV64_IMPL := cheri_prelude_128.sail
 
 SAIL_XLEN = $(SAIL_$(ARCH)_XLEN)
 SAIL_FLEN = $(SAIL_RISCV_MODEL_DIR)/riscv_flen_D.sail
+SAIL_VLEN = $(SAIL_RISCV_MODEL_DIR)/riscv_vlen.sail
 CHERI_CAP_IMPL = $(CHERI_CAP_$(ARCH)_IMPL)
 
 
@@ -59,7 +60,9 @@ SAIL_SYS_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_sync_exception.sail
 SAIL_SYS_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_next_control.sail
 SAIL_SYS_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_softfloat_interface.sail
 SAIL_SYS_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_fdext_regs.sail
+SAIL_SYS_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_vext_regs.sail
 SAIL_SYS_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_fdext_control.sail
+SAIL_SYS_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_vext_control.sail
 SAIL_SYS_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_csr_ext.sail
 SAIL_SYS_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_sys_control.sail
 SAIL_SYS_SRCS += $(SAIL_CHECK_SRCS)
@@ -72,13 +75,17 @@ SAIL_RV64_VM_SRCS = $(SAIL_RISCV_MODEL_DIR)/riscv_vmem_sv39.sail \
 
 SAIL_VM_SRCS =  $(SAIL_CHERI_MODEL_DIR)/cheri_pte.sail $(SAIL_CHERI_MODEL_DIR)/cheri_ptw.sail \
                 $(SAIL_RISCV_MODEL_DIR)/riscv_vmem_common.sail $(SAIL_RISCV_MODEL_DIR)/riscv_vmem_tlb.sail
-SAIL_VM_SRCS += $(SAIL_$(ARCH)_VM_SRCS)
+SAIL_VM_SRCS += $(SAIL_RISCV_MODEL_DIR)/riscv_vmem_common.sail \
+		$(SAIL_RISCV_MODEL_DIR)/riscv_vmem_pte.sail \
+		$(SAIL_RISCV_MODEL_DIR)/riscv_vmem_ptw.sail \
+		$(SAIL_RISCV_MODEL_DIR)/riscv_vmem_tlb.sail \
+		$(SAIL_RISCV_MODEL_DIR)/riscv_vmem.sail \
 
 # Non-instruction sources
 PRELUDE = $(SAIL_RISCV_MODEL_DIR)/prelude.sail \
-          $(SAIL_RISCV_MODEL_DIR)/prelude_mapping.sail \
           $(SAIL_XLEN) \
           $(SAIL_FLEN) \
+          $(SAIL_VLEN) \
           $(SAIL_CHERI_MODEL_DIR)/cheri_prelude.sail \
           $(SAIL_CHERI_MODEL_DIR)/cheri_types.sail \
           $(SAIL_CHERI_MODEL_DIR)/$(CHERI_CAP_IMPL) \
@@ -88,6 +95,7 @@ PRELUDE = $(SAIL_RISCV_MODEL_DIR)/prelude.sail \
 
 SAIL_REGS_SRCS = $(SAIL_CHERI_MODEL_DIR)/cheri_reg_type.sail \
                  $(SAIL_RISCV_MODEL_DIR)/riscv_freg_type.sail \
+                 $(SAIL_RISCV_MODEL_DIR)/riscv_vreg_type.sail \
                  $(SAIL_RISCV_MODEL_DIR)/riscv_csr_map.sail \
                  $(SAIL_CHERI_MODEL_DIR)/cheri_scr_map.sail \
                  $(SAIL_CHERI_MODEL_DIR)/cheri_vmem_types.sail \

diff --git a/sail-riscv b/sail-riscv
diff --git a/src/cheri_addr_checks.sail b/src/cheri_addr_checks.sail
@@ -211,7 +211,7 @@ function ext_data_get_addr(base_reg : regidx, offset : xlenbits, acc : AccessTyp
     Ext_DataAddr_Error(CapEx_PermitLoadViolation, auth_idx)
   else if not(have_rqd_store_perm) then
     Ext_DataAddr_Error(CapEx_PermitStoreViolation, auth_idx)
-  else if not(inCapBounds(auth_val, newAddr, word_width_bytes(width))) then
+  else if not(inCapBounds(auth_val, newAddr, size_bytes(width))) then
     Ext_DataAddr_Error(CapEx_LengthViolation, auth_idx)
   else
     Ext_DataAddr_OK(newAddr)

diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail
@@ -1174,7 +1174,7 @@ function clause execute(JALR_PCC(rd, rs1)) = {
 
 val handle_load_data_via_cap : (regidx, capreg_idx, Capability, xlenbits, bool, word_width) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function handle_load_data_via_cap(rd, auth_idx, auth_val, vaddrBits, is_unsigned, width) = {
-  let size = word_width_bytes(width);
+  let size = size_bytes(width);
   let aq : bool = false;
   let rl : bool = false;
   if not(auth_val.tag) then {
@@ -1439,7 +1439,7 @@ function check_res_misaligned(vaddr : xlenbits, width : word_width) -> bool =
 
 val handle_loadres_data_via_cap : (regidx, capreg_idx, Capability, xlenbits, word_width) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function handle_loadres_data_via_cap(rd, auth_idx, auth_val, vaddrBits, width) = {
-  let size = word_width_bytes(width);
+  let size = size_bytes(width);
   let aq : bool = false;
   let rl : bool = false;
   let is_unsigned = false;
@@ -1578,7 +1578,7 @@ function clause execute (LoadResCapMode(cd, rs1_cs1, aq, rl)) = {
 
 val handle_store_data_via_cap : (regidx, capreg_idx, Capability, xlenbits, word_width) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function handle_store_data_via_cap(rs2, auth_idx, auth_val, vaddrBits, width) = {
-  let size = word_width_bytes(width);
+  let size = size_bytes(width);
   let aq : bool = false;
   let rl : bool = false;
   if not(auth_val.tag) then {
@@ -1832,7 +1832,7 @@ function clause execute StoreCapImm(cs2, rs1_cs1, imm) = {
 
 val handle_store_cond_data_via_cap : (regidx, capreg_idx, Capability, xlenbits, word_width) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function handle_store_cond_data_via_cap(rs2, auth_idx, auth_val, vaddrBits, width) = {
-  let size = word_width_bytes(width);
+  let size = size_bytes(width);
   let aq : bool = true; /* cheri-specific aq/rl */
   let rl : bool = true;
   if not(auth_val.tag) then {

diff --git a/src/cheri_prelude.sail b/src/cheri_prelude.sail
@@ -70,8 +70,10 @@ function MAX(n) = pow2(n) - 1
 
 val not = {coq:"negb", _:"not"} : bool -> bool
 
+/*
 val bool_to_bit : bool -> bit
 function bool_to_bit x = if x then bitone else bitzero
+*/
 
 /*
  * We use a single feature flag controlling DDC/PCC relocation.

diff --git a/src/cheri_regs.sail b/src/cheri_regs.sail
@@ -143,7 +143,7 @@ function wC (r, v) = {
   if (r != 0) then {
      rvfi_wX(r, v.address);
      if get_config_print_reg() then
-       print_reg("x" ^ string_of_int(r) ^ " <- " ^ RegStr(v));
+       print_reg("x" ^ dec_str(r) ^ " <- " ^ RegStr(v));
   }
 }