From 3c86a2266e77a59dc5f0f489d5a4d0e436d10af3 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Fri, 11 Aug 2023 16:01:37 +0100 Subject: [PATCH 1/5] Remove duplicate xor_vec This is already provided by Sail. --- model/prelude.sail | 2 -- 1 file changed, 2 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index 5ff8a1213..9a7aace8c 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -138,8 +138,6 @@ function string_of_bit(b: bit) -> string = overload BitStr = {string_of_bits, string_of_bit} -val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int overload operator ^ = {xor_vec, int_power, concat_str} From 53c3802695acc4d1ba3e36d32b9429796e8cd34f Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Fri, 11 Aug 2023 16:03:14 +0100 Subject: [PATCH 2/5] Remove redundant _ match case --- model/riscv_sys_control.sail | 1 - 1 file changed, 1 deletion(-) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index d057ad6c0..b8540538c 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -205,7 +205,6 @@ function check_seed_CSR (csr : csreg, p : Privilege, isWrite : bool) -> bool = { Machine => true, Supervisor => false, /* TODO: base this on mseccfg */ User => false, /* TODO: base this on mseccfg */ - _ => false } } } From 05bf331198e5d71aeb91e02229ed6ea925c3d6e9 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 15 Aug 2023 14:00:16 +0100 Subject: [PATCH 3/5] Add z3_problems to .gitignore This file seems to be created on every build. --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 224b1595b..0079a6798 100644 --- a/.gitignore +++ b/.gitignore @@ -6,3 +6,4 @@ _build/ _sbuild/ *.o *.a +/z3_problems From f18739b553f81e2cf20df6d8a1b545e8f5eb5261 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Wed, 16 Aug 2023 15:10:08 +0100 Subject: [PATCH 4/5] Fix some stray tabs --- model/riscv_vmem_sv39.sail | 4 ++-- model/riscv_vmem_sv48.sail | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 12f1eafcc..5bc5a187e 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -111,7 +111,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { } } else { /* leaf PTE */ match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) { - PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { + PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { /* print("walk39: pte permission check failure"); */ PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, @@ -232,7 +232,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = TR_Failure(PTW_PTE_Update(), ext_ptw) } else { w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); - w_pte : SV39_PTE = update_Ext(w_pte, ext); + w_pte : SV39_PTE = update_Ext(w_pte, ext); match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { MemValue(_) => { add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 601ed0f17..26a8a3b6a 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -115,7 +115,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { /* print("walk48: pte permission check failure"); */ PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, - PTE_Check_Success(ext_ptw) => { + PTE_Check_Success(ext_ptw) => { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1; @@ -196,7 +196,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = TR_Failure(PTW_PTE_Update(), ext_ptw) } else { w_pte : SV48_PTE = update_BITS(pte, pbits.bits()); - w_pte : SV48_PTE = update_Ext(w_pte, ext); + w_pte : SV48_PTE = update_Ext(w_pte, ext); match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { MemValue(_) => { add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global); From 14335e33832bb13c3ebd6efe55adfc3693a3ced8 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Thu, 17 Aug 2023 12:12:11 +0100 Subject: [PATCH 5/5] Remove redundant type annotations on w_pte & add explicit `var`. These are given on the previous line already. Sail does not let you change the type of a variable like Rust does. The `var` ensures this definitely refers to a local rather than global variable. --- model/riscv_vmem_sv32.sail | 2 +- model/riscv_vmem_sv39.sail | 4 ++-- model/riscv_vmem_sv48.sail | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index e0f5bc985..e8365c323 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -237,7 +237,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) } else { - w_pte : SV32_PTE = update_BITS(pte, pbits.bits()); + var w_pte : SV32_PTE = update_BITS(pte, pbits.bits()); /* ext is unused since there are no reserved bits for extensions */ match mem_write_value_priv(to_phys_addr(pteAddr), 4, w_pte.bits(), Supervisor, false, false, false) { MemValue(_) => { diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 5bc5a187e..384b6ece3 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -231,8 +231,8 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) } else { - w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); - w_pte : SV39_PTE = update_Ext(w_pte, ext); + var w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); + w_pte = update_Ext(w_pte, ext); match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { MemValue(_) => { add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 26a8a3b6a..729a70177 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -195,8 +195,8 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) } else { - w_pte : SV48_PTE = update_BITS(pte, pbits.bits()); - w_pte : SV48_PTE = update_Ext(w_pte, ext); + var w_pte : SV48_PTE = update_BITS(pte, pbits.bits()); + w_pte = update_Ext(w_pte, ext); match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { MemValue(_) => { add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global);