Increase flexibility of the decode hook (and simplify it) (#205)

Previously the decoding hook (`ext_post_decode_hook`) allowed models to
override the decoded `ast`. However, this is not sufficient if model
extension changes interpretation of fields. Additionally, the assembly
printing would always print assembly for the "baseline decode" which
resulted in incorrect trace output in the sail-cheri-riscv model.

With the new hook models can implement ext_decode()/ext_decode_compressed()
to return an `ast` and for encodings that are not adjusted fall back to
the default `encdec`/`encdec_compressed`.

3 files changed, 11 insertions, 14 deletions

diff --git a/model/riscv_decode_ext.sail b/model/riscv_decode_ext.sail
index c4b3954..e943ec5 100644
--- a/model/riscv_decode_ext.sail
+++ b/model/riscv_decode_ext.sail
@@ -67,9 +67,12 @@
 /*=======================================================================================*/
 
 /* Extensions may wish to interpose and transform decoded instructions,
- * based on other machine state.  This is supported via a post-decode
- * instruction hook, the default implementation of which is provided below.
+ * based on other machine state. This is supported via decode instruction
+  hooks, the default implementation of which is provided below.
  */
 
-val ext_post_decode_hook : ast -> ast effect {rreg}
-function ext_post_decode_hook(x) = x
+val ext_decode_compressed : bits(16) -> ast effect {rreg}
+function ext_decode_compressed(bv) = encdec_compressed(bv)
+
+val ext_decode : bits(32) -> ast effect {rreg}
+function ext_decode(bv) = encdec(bv)
diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail
index 610508d..267d080 100644
--- a/model/riscv_insts_end.sail
+++ b/model/riscv_insts_end.sail
@@ -101,9 +101,3 @@ val print_insn : ast -> string
 function print_insn insn = assembly(insn)
 
 overload to_str = {print_insn}
-
-val decode : bits(32) -> ast effect {rreg}
-function decode bv = encdec(bv)
-
-val decodeCompressed : bits(16) -> ast effect {rreg}
-function decodeCompressed bv = encdec_compressed(bv)
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 40c0c80..df53fae 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -99,7 +99,7 @@ function step(step_no : int) -> bool = {
           /* non-error cases: */
           F_RVC(h) => {
             instbits = EXTZ(h);
-            let ast = decodeCompressed(h);
+            let ast = ext_decode_compressed(h);
             if   get_config_print_instr()
             then {
               print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast));
@@ -107,7 +107,7 @@ function step(step_no : int) -> bool = {
             /* check for RVC once here instead of every RVC execute clause. */
             if haveRVC() then {
               nextPC = PC + 2;
-              (execute(ext_post_decode_hook(ast)), true)
+              (execute(ast), true)
              } else {
               handle_illegal();
               (RETIRE_FAIL, true)
@@ -115,13 +115,13 @@ function step(step_no : int) -> bool = {
           },
           F_Base(w) => {
             instbits = EXTZ(w);
-            let ast = decode(w);
+            let ast = ext_decode(w);
             if   get_config_print_instr()
             then {
               print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast));
             };
             nextPC = PC + 4;
-            (execute(ext_post_decode_hook(ast)), true)
+            (execute(ast), true)
           }
         }
       }