Skip to content

Commit

Permalink
Change encoding permission set -> tuple ; extract sregs ; movsr -> re…
Browse files Browse the repository at this point in the history 
…adsr/writesr
  • Loading branch information
@JuneRousseau
JuneRousseau committed Feb 9, 2025
1 parent 667ab3d commit d1e2b56
Show file tree
Hide file tree
Showing 31 changed files with 664 additions and 505 deletions.
44 changes: 16 additions & 28 deletions lib/ast.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
(* Type definitions for the syntax AST *)
type regname = PC | Reg of int
type sregname = MTDC

(* https://github.com/CHERIoT-Platform/llvm-project/blob/f39e8860b29668f986b11d29fa953c96a25373f1/llvm/lib/Target/RISCV/RISCVRegisterInfo.td#L138 *)
let cnull = Reg 0
let cra = Reg 1 (* link register *)
let csp = Reg 2 (* compartment stack register *)
let cgp = Reg 3 (* global data register *)
Expand All @@ -12,6 +14,7 @@ let ct2 = Reg 7
let ct3 = Reg 28
let ct4 = Reg 29
let ct5 = Reg 30
let ct6 = Reg 31
let cs0 = Reg 8 (* temporary registers ? *)
let cs1 = Reg 9
let cs2 = Reg 18
Expand All @@ -33,39 +36,18 @@ let ca5 = Reg 15
let ca6 = Reg 16
let ca7 = Reg 17

(* Instead of a new regname, we use r31 as mtdc, and r0 as ct6 *)
let mtdc = Reg 31
let ct6 = Reg 0

module Perm = struct
type t =
| R (* read --- LG, MC and LD *)
| X (* execute --- EX *)
| W (* write --- LM, MC and SD *)
| WL (* write local --- SL *)
| SR (* system register access --- SR *)
| DL (* deep locality --- inverse of LG *)
| DI (* deep immutability --- inverse of LM *)

let compare p1 p2 =
if p1 = p2 then 0
else
(* Just an order for pretty printing *)
let weight p =
match p with R -> 0 | X -> 1 | W -> 2 | WL -> 3 | SR -> 4 | DL -> 5 | DI -> 6
in
weight p2 - weight p1
end

module PermSet = Set.Make (Perm)

type rxperm = Orx | R | X | XSR
type wperm = Ow | W | WL
type dlperm = DL | LG
type droperm = DRO | LM
type perm = rxperm * wperm * dlperm * droperm
type locality = Global | Local
type wtype = W_I | W_Cap | W_SealRange | W_Sealed
type seal_perm = bool * bool
type reg_or_const = Register of regname | Const of Z.t

type sealable =
| Cap of PermSet.t * locality * Z.t * Z.t * Z.t
| Cap of perm * locality * Z.t * Z.t * Z.t
| SealRange of seal_perm * locality * Z.t * Z.t * Z.t

type word = I of Z.t | Sealable of sealable | Sealed of Z.t * sealable
Expand All @@ -75,7 +57,8 @@ type machine_op =
| Jmp of reg_or_const (* immediate jump *)
| Jnz of regname * reg_or_const (* jump non zero *)
(* system access registers *)
| MoveSR of regname * reg_or_const
| ReadSR of regname * sregname
| WriteSR of sregname * regname
| Move of regname * reg_or_const
| Load of regname * regname
| Store of regname * reg_or_const
Expand Down Expand Up @@ -103,11 +86,16 @@ type machine_op =
type statement = Op of machine_op | Word of word (* TODO: PseudoOp and LabelDefs *)
type t = statement list

let null_perm = (Orx, Ow, DL, DRO)

let compare_regname (r1 : regname) (r2 : regname) : int =
match (r1, r2) with
| PC, PC -> 0
| PC, Reg _ -> -1
| Reg _, PC -> 1
| Reg i, Reg j -> Int.compare i j

let compare_sregname (sr1 : sregname) (sr2 : sregname) : int =
match (sr1, sr2) with MTDC, MTDC -> 0

let const n = Const (Z.of_int n)
143 changes: 75 additions & 68 deletions lib/encode.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,61 +83,60 @@ let decode_locality (i : Z.t) : locality =
let dec_type, dec_i = decode_const i in
if dec_type != _LOCALITY_ENC then dec_loc_exception () else locality_decoding dec_i

let perm_encoding (p : Perm.t) : Z.t =
Z.of_int
@@
match p with
| R -> 0b1000000
| X -> 0b0100000
| W -> 0b0010000
| WL -> 0b0001000
| SR -> 0b0000100
| DL -> 0b0000010
| DI -> 0b0000001

let fperm_encoding (fp : PermSet.t) : Z.t =
PermSet.fold (fun p res -> Z.logor (perm_encoding p) res) fp (Z.of_int 0b0)

let perm_decoding (i : Z.t) : Perm.t =
let rxperm_encoding (rx : rxperm) : Z.t =
Z.of_int @@ match rx with Orx -> 0b00 | R -> 0b01 | X -> 0b10 | XSR -> 0b11

let wperm_encoding (w : wperm) : Z.t =
Z.of_int @@ match w with Ow -> 0b00 | W -> 0b01 | WL -> 0b10

let dlperm_encoding (dl : dlperm) : Z.t = Z.of_int @@ match dl with DL -> 0b0 | LG -> 0b1
let droperm_encoding (dro : droperm) : Z.t = Z.of_int @@ match dro with DRO -> 0b0 | LM -> 0b1

let perm_encoding (p : perm) : Z.t =
let open Z in
let rx, w, dl, dro = p in
let enc_dro = droperm_encoding dro lsl 0 in
(* size of DRO_ENCODING *)
let enc_dl = dlperm_encoding dl lsl 1 in
(* size of DL_ENCODING *)
let enc_w = wperm_encoding w lsl 2 in
(* size of W_ENCODING *)
let enc_rx = rxperm_encoding rx lsl 4 in
enc_rx lor enc_w lor enc_dl lor enc_dro

let perm_decoding (i : Z.t) : perm =
let dec_perm_exception _ =
raise @@ DecodeException "Error decoding permission: unexpected encoding"
in
if Z.(i > of_int 0b1111111) then dec_perm_exception ()
if Z.(i > of_int 0b111111) then dec_perm_exception ()
else
let b k = Z.testbit i k in
match (b 6, b 5, b 4, b 3, b 2, b 1, b 0) with
| true, false, false, false, false, false, false -> R
| false, true, false, false, false, false, false -> X
| false, false, true, false, false, false, false -> W
| false, false, false, true, false, false, false -> WL
| false, false, false, false, true, false, false -> SR
| false, false, false, false, false, true, false -> DL
| false, false, false, false, false, false, true -> DI
| _ -> dec_perm_exception ()

let fperm_decoding (i : Z.t) : PermSet.t =
let dec_perm_exception _ =
raise @@ DecodeException "Error decoding permission: unexpected encoding"
in
if Z.(i > of_int 0b11111111) then dec_perm_exception ()
else
let perm_mask =
List.map Z.of_int
[ 0b10000000; 0b01000000; 0b00100000; 0b00010000; 0b00001000; 0b00000010; 0b00000001 ]
let rx =
match (b 5, b 4) with
| false, false -> Orx
| false, true -> R
| true, false -> X
| true, true -> XSR
in
let w =
match (b 3, b 2) with
| false, false -> Ow
| false, true -> W
| true, false -> WL
| true, true -> dec_perm_exception ()
in
let masked = List.map (fun mask -> Z.logand mask i) perm_mask in
let filtered = List.filter (fun r -> not (r = Z.zero)) masked in
let decoded = List.map perm_decoding filtered in
PermSet.of_list decoded
let dl = match b 1 with false -> DL | true -> LG in
let dro = match b 0 with false -> DRO | true -> LM in
(rx, w, dl, dro)

let encode_perm (p : PermSet.t) : Z.t = encode_const _PERM_ENC (fperm_encoding p)
let encode_perm (p : perm) : Z.t = encode_const _PERM_ENC (perm_encoding p)

let decode_perm (i : Z.t) : PermSet.t =
let decode_perm (i : Z.t) : perm =
let dec_perm_exception _ =
raise @@ DecodeException "Error decoding permission: does not recognize a permission"
in
let dec_type, dec_i = decode_const i in
if dec_type != _PERM_ENC then dec_perm_exception () else fperm_decoding dec_i
if dec_type != _PERM_ENC then dec_perm_exception () else perm_decoding dec_i

(** Sealing Permission *)

Expand Down Expand Up @@ -169,29 +168,29 @@ let decode_seal_perm (i : Z.t) : seal_perm =
if dec_type != _SEAL_PERM_ENC then decode_perm_exception () else seal_perm_decoding dec_i

(** Permission-locality encoding *)
let perm_loc_pair_encoding (p : PermSet.t) (g : locality) : Z.t =
let size_perm = 8 in
let perm_loc_pair_encoding (p : perm) (g : locality) : Z.t =
let size_perm = 6 in
let open Z in
let encoded_g = locality_encoding g lsl size_perm in
let encoded_p = fperm_encoding p in
let encoded_p = perm_encoding p in
encoded_g lor encoded_p

let encode_perm_loc_pair (p : PermSet.t) (g : locality) : Z.t =
let encode_perm_loc_pair (p : perm) (g : locality) : Z.t =
encode_const _PERM_LOC_ENC (perm_loc_pair_encoding p g)

let perm_loc_pair_decoding (i : Z.t) : PermSet.t * locality =
let size_perm = 8 in
let perm_loc_pair_decoding (i : Z.t) : perm * locality =
let size_perm = 6 in
let dec_perm_loc_exception _ =
raise @@ DecodeException "Error decoding permission-locality pair: unexpected encoding"
in
let open Z in
if i > of_int 0b1111111111 then dec_perm_loc_exception ()
if i > of_int 0b11111111 then dec_perm_loc_exception ()
else
let encoded_g = (i land of_int 0b1100000000) asr size_perm in
let encoded_p = i land of_int 0b0011111111 in
(fperm_decoding encoded_p, locality_decoding encoded_g)
let encoded_g = (i land of_int 0b11000000) asr size_perm in
let encoded_p = i land of_int 0b00111111 in
(perm_decoding encoded_p, locality_decoding encoded_g)

let decode_perm_loc_pair (i : Z.t) : PermSet.t * locality =
let decode_perm_loc_pair (i : Z.t) : perm * locality =
let dec_perm_loc_exception _ =
raise
@@ DecodeException
Expand Down Expand Up @@ -236,6 +235,11 @@ let decode_seal_perm_loc_pair (i : Z.t) : seal_perm * locality =

let encode_reg (r : regname) : Z.t = match r with PC -> Z.zero | Reg i -> Z.succ @@ Z.of_int i
let decode_reg (i : Z.t) : regname = if i = Z.zero then PC else Reg (Z.to_int @@ Z.pred i)
let encode_sreg (sr : sregname) : Z.t = match sr with MTDC -> Z.zero

let decode_sreg (i : Z.t) : sregname =
if i = Z.zero then MTDC
else raise @@ DecodeException "Error decoding system register: unknown sregister"

let rec split_int (i : Z.t) : Z.t * Z.t =
let open Z in
Expand Down Expand Up @@ -313,10 +317,12 @@ let encode_machine_op (s : machine_op) : Z.t =
| Jalr (r1, r2) ->
(* 0x04 *)
~$0x04 ^! encode_int_int (encode_reg r1) (encode_reg r2)
| MoveSR (r, c) ->
(* 0x05, 0x06 *)
let opc, c_enc = const_convert ~$0x05 c in
opc ^! encode_int_int (encode_reg r) c_enc
| ReadSR (r, sr) ->
(* 0x05 *)
~$0x05 ^! encode_int_int (encode_reg r) (encode_sreg sr)
| WriteSR (sr, r) ->
(* 0x06 *)
~$0x06 ^! encode_int_int (encode_sreg sr) (encode_reg r)
| Move (r, c) ->
(* 0x07, 0x08 *)
let opc, c_enc = const_convert ~$0x07 c in
Expand Down Expand Up @@ -409,17 +415,18 @@ let decode_machine_op (i : Z.t) : machine_op =
let r1 = decode_reg r1_enc in
let r2 = decode_reg r2_enc in
Jalr (r1, r2)
else if (* MoveSR *)
opc = ~$0x05 (* register register *) then
let r_enc, c_enc = decode_int payload in
let r1 = decode_reg r_enc in
let r2 = Register (decode_reg c_enc) in
MoveSR (r1, r2)
else if opc = ~$0x06 (* register const *) then
let r_enc, c_enc = decode_int payload in
else if (* ReadSR *)
opc = ~$0x05 (* register sregister *) then
let r_enc, sr_enc = decode_int payload in
let r = decode_reg r_enc in
let c = Const c_enc in
MoveSR (r, c)
let sr = decode_sreg sr_enc in
ReadSR (r, sr)
else if (* WriteSR *)
opc = ~$0x06 (* sregister register *) then
let sr_enc, r_enc = decode_int payload in
let sr = decode_sreg sr_enc in
let r = decode_reg r_enc in
WriteSR (sr, r)
else if (* Move *)
opc = ~$0x07 (* register register *) then
let r_enc, c_enc = decode_int payload in
Expand Down
43 changes: 38 additions & 5 deletions lib/interactive_ui.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,10 @@ end

module MkUi (Cfg : MachineConfig) : Ui = struct
module Perm = struct
let width = 12
let width = 15

let ui ?(attr = A.empty) (p : Ast.PermSet.t) =
I.hsnap ~align:`Left width (I.string attr (Pretty_printer.string_of_fperm p))
let ui ?(attr = A.empty) (p : Ast.perm) =
I.hsnap ~align:`Left width (I.string attr (Pretty_printer.string_of_perm p))
end

module Locality = struct
Expand Down Expand Up @@ -160,6 +160,14 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
I.hsnap ~align:`Right width (I.string A.empty (Pretty_printer.string_of_regname r))
end

module SRegname = struct
(* pc or rNN or mtdc *)
let width = 4

let ui (sr : Ast.sregname) =
I.hsnap ~align:`Right width (I.string A.empty (Pretty_printer.string_of_sregname sr))
end

module Regs_panel = struct
(* <reg>: <word> <reg>: <word> <reg>: <word>
<reg>: <word> <reg>: <word>
Expand All @@ -183,6 +191,29 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
loop true (Machine.RegMap.to_seq regs |> List.of_seq) |> I.hsnap ~align:`Left width
end

module SRegs_panel = struct
(* <reg>: <word> <reg>: <word> <reg>: <word>
<reg>: <word> <reg>: <word>
*)
let ui width (sregs : Machine.sreg_state) =
let sreg_width = SRegname.width + 2 + Word.width + 2 in
let ncols = max 1 (width / sreg_width) in
let nsregs_per_col = 1. (* nsregs *) /. float ncols |> ceil |> int_of_float in
let rec loop fst_col sregs =
if sregs = [] then I.empty
else
let col, sregs = CCList.take_drop nsregs_per_col sregs in
List.fold_left
(fun img (r, w) ->
img
<-> ((if not fst_col then I.string A.empty " " else I.empty)
<|> SRegname.ui r <|> I.string A.empty ": " <|> Word.ui w Left))
I.empty col
<|> loop false sregs
in
loop true (Machine.SRegMap.to_seq sregs |> List.of_seq) |> I.hsnap ~align:`Left width
end

module Instr = struct
let ui (i : Ast.machine_op) = I.string A.(fg green) (Pretty_printer.string_of_machine_op i)
end
Expand Down Expand Up @@ -330,11 +361,13 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
history =
let term_width, term_height = Term.size term in
let reg = (snd m).Machine.reg in
let sreg = (snd m).Machine.sreg in
let mem = (snd m).Machine.mem in
let regs_img = Regs_panel.ui term_width reg in
let sregs_img = SRegs_panel.ui term_width sreg in
let mem_img, panel_start, panel_stk =
Program_panel.ui ~upd_prog:update_prog ~upd_stk:update_stk ~show_stack
(term_height - 1 - I.height regs_img)
(term_height - 1 - I.height regs_img - I.height sregs_img)
term_width mem (Machine.RegMap.find Ast.PC reg) (Machine.RegMap.find Ast.csp reg)
!prog_panel_start !stk_panel_start
in
Expand All @@ -344,7 +377,7 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
I.hsnap ~align:`Right term_width
(I.string A.empty "machine state: " <|> Exec_state.ui (fst m))
in
let img = regs_img <-> mach_state_img <-> mem_img in
let img = regs_img <-> sregs_img <-> mach_state_img <-> mem_img in
Term.image term img;
(* watch for a relevant event *)
let rec process_events () =
Expand Down
Loading

0 comments on commit d1e2b56

Please sign in to comment.