Generating instruction footprints for different privilege modes.

[neeluk7]

Hello,

I am wondering if it's possible to generate footprints for each instruction that are specific to different privilege modes?

Particularly for RISC-V, I tried to set the cur_privilege to Supervisor in the config. Here's what the trace looked like:

(trace
(assume-reg |monomorphize_reads| nil false)
(assume-reg |monomorphize_writes| nil false)
(assume-reg |cur_privilege| nil |Supervisor|)
(assume-reg |misa| nil ( struct (|bits| #x0000000000000000)))
(assume-reg |mstatus| nil ( struct (|bits| #x0000000000000000)))
(assume-reg |mcountinhibit| nil ( struct (|bits| #x00000000)))
(assume-reg |tlb| nil (|None| ( unit)))
(assume-reg |satp| nil #x0000000000000000)
(define-enum |Privilege| 3 (|User| |Supervisor| |Machine|)) ; 0:0 - 0:0
(define-enum |Architecture| 3 (|RV32| |RV64| |RV128|)) ; 0:0 - 0:0
(define-enum |PmpAddrMatchType| 4 (|OFF| |TOR| |NA4| |NAPOT|)) ; 0:0 - 0:0
(cycle)
(read-reg |cur_privilege| nil |Machine|)
(read-reg |cur_privilege| nil |Machine|)
(declare-const v442 (_ BitVec 64)) ; model/riscv_insts_base.sail 652:16 - 652:64
(read-reg |PC| nil v442)
(read-reg |cur_privilege| nil |Machine|)
(read-reg |mstatus| ((_ field |bits|)) (_ struct (|bits| #x0000000a00000000)))
(read-reg |mstatus| nil (_ struct (|bits| #x0000000a00000000)))
(read-reg |mstatus| nil (_ struct (|bits| #x0000000a00000000)))
(write-reg |mstatus| nil (_ struct (|bits| #x0000000a00000000)))
(read-reg |mstatus| ((_ field |bits|)) (_ struct (|bits| #x0000000a00000000)))
(read-reg |mstatus| nil (_ struct (|bits| #x0000000a00000000)))
(write-reg |mstatus| nil (_ struct (|bits| #x0000000a00000080)))
(read-reg |mstatus| nil (_ struct (|bits| #x0000000a00000080)))
(write-reg |cur_privilege| nil |User|)
(read-reg |mstatus| ((_ field |bits|)) (_ struct (|bits| #x0000000a00000080)))
(read-reg |misa| nil (_ struct (|bits| #x8000000000141105)))
(read-reg |mstatus| nil (_ struct (|bits| #x0000000a00000080)))
(write-reg |mstatus| nil (_ struct (|bits| #x0000000a00000080)))
(read-reg |cur_privilege| nil |User|)
(read-reg |mstatus| ((_ field |bits|)) (_ struct (|bits| #x0000000a00000080)))
(read-reg |mstatus| nil (_ struct (|bits| #x0000000a00000080)))
(write-reg |mstatus| nil (_ struct (|bits| #x0000000a00000080)))
(read-reg |mepc| nil #x0000000000000000)
(read-reg |misa| nil (_ struct (|bits| #x8000000000141105)))
(branch-address #x0000000000000000)
(write-reg |nextPC| nil #x0000000000000000)
(define-enum |Retired| 2 (|RETIRE_SUCCESS| |RETIRE_FAIL|)) ; 0:0 - 0:0)

Even though I can see the assume-reg cur_privilege with value Supervisor, eventually it says "define-enum" and sets that to Machine, so when cur_privilege is read after the (cycle) event, it's set to Machine and not Supervisor.

I haven't deep dived into the code to see what's causing this yet, it would be great if you can point me to that.

What I want to achieve is for instance, an instruction like "mret" should trap if executed by Supervisor mode.
Similarly, a "csrw mstatus, " should also trap if executed by Supervisor mode. Is this possible to observe in the footprints generated by Isla?