From 0863807f8ff6b98c0d3e82d2cfa8dffdaea759c5 Mon Sep 17 00:00:00 2001 From: June Rousseau Date: Thu, 19 Dec 2024 12:54:03 +0100 Subject: [PATCH] feat(cerisier): update the opsem with new definitions --- lib/ast.ml | 4 +- lib/encode.ml | 18 +++----- lib/interactive_ui.ml | 14 +++--- lib/ir.ml | 11 +++-- lib/machine.ml | 64 +++++++++++--------------- lib/parameters.ml | 6 +-- lib/parser.mly | 4 +- lib/pretty_printer.ml | 4 +- lib/program.ml | 6 +-- tests/test_files/default/pos/enclave.s | 6 +-- tests/tester.ml | 2 +- tests/tests.ml | 8 ++-- 12 files changed, 65 insertions(+), 82 deletions(-) diff --git a/lib/ast.ml b/lib/ast.ml index 0e806f9..25a58ae 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -45,8 +45,8 @@ type machine_op = | StoreU of regname * reg_or_const * reg_or_const | PromoteU of regname | EInit of regname * regname - | EDeInit of regname * regname - | EStoreId of regname * regname * regname + | EDeInit of regname + | EStoreId of regname * regname | IsUnique of regname * regname | Fail | Halt diff --git a/lib/encode.ml b/lib/encode.ml index e7bdf73..02bbe76 100644 --- a/lib/encode.ml +++ b/lib/encode.ml @@ -377,9 +377,9 @@ let encode_machine_op (s : machine_op) : Z.t = opc ^! encode_int_int (encode_reg r) c_enc | PromoteU r -> ~$0x37 ^! encode_reg r | EInit (r1, r2) -> ~$0x38 ^! encode_int_int (encode_reg r1) (encode_reg r2) - | EDeInit (r1, r2) -> ~$0x39 ^! encode_int_int (encode_reg r1) (encode_reg r2) - | EStoreId (r1, r2, r3) -> - ~$0x3a ^! encode_int_int (encode_reg r1) (encode_int_int (encode_reg r2) (encode_reg r3)) + | EDeInit r -> ~$0x39 ^! encode_reg r + | EStoreId (r1, r2) -> + ~$0x3a ^! (encode_int_int (encode_reg r1) (encode_reg r2)) | IsUnique (r1, r2) -> ~$0x3b ^! encode_int_int (encode_reg r1) (encode_reg r2) | Fail -> ~$0x3c | Halt -> ~$0x3d @@ -602,19 +602,13 @@ let decode_machine_op (i : Z.t) : machine_op = let r2 = decode_reg r2_enc in EInit (r1, r2) else if (* EDeInit *) - opc = ~$0x39 then - let r1_enc, r2_enc = decode_int payload in - let r1 = decode_reg r1_enc in - let r2 = decode_reg r2_enc in - EDeInit (r1, r2) + opc = ~$0x39 then EDeInit (decode_reg payload) else if (* EStoreId *) opc = ~$0x3a then - let r1_enc, payload' = decode_int payload in - let r2_enc, r3_enc = decode_int payload' in + let r1_enc, r2_enc = decode_int payload in let r1 = decode_reg r1_enc in let r2 = decode_reg r2_enc in - let r3 = decode_reg r3_enc in - EStoreId (r1, r2, r3) + EStoreId (r1, r2) else if (* IsUnique *) opc = ~$0x3b then let r1_enc, r2_enc = decode_int payload in diff --git a/lib/interactive_ui.ml b/lib/interactive_ui.ml index 445ba2c..0bec705 100644 --- a/lib/interactive_ui.ml +++ b/lib/interactive_ui.ml @@ -210,25 +210,25 @@ module MkUi (Cfg : MachineConfig) : Ui = struct end module ETable_panel = struct - (* : - : - : + (* : + : + : *) let ui width (etbl : Machine.e_table) = let nenclaves = 20. in (* Arbitrary number *) - let eid_width = EC_counter.width + 2 + Identity.width + 2 in - let ncols = max 1 (width / eid_width) in + let tid_width = EC_counter.width + 2 + Identity.width + 2 in + let ncols = max 1 (width / tid_width) in let nregs_per_col = nenclaves /. float ncols |> ceil |> int_of_float in let rec loop fst_col etable = if etable = [] then I.empty else let col, etable = CCList.take_drop nregs_per_col etable in List.fold_left - (fun img (eid, (id, _)) -> + (fun img (tid, id) -> img <-> ((if not fst_col then I.string A.empty " " else I.empty) - <|> EC_counter.ui eid <|> I.string A.empty ": " <|> Identity.ui id)) + <|> EC_counter.ui tid <|> I.string A.empty ": " <|> Identity.ui id)) I.empty col <|> loop false etable in diff --git a/lib/ir.ml b/lib/ir.ml index 06858ad..bdd576c 100644 --- a/lib/ir.ml +++ b/lib/ir.ml @@ -6,6 +6,7 @@ exception ExprException of string type regname = PC | Reg of int let ddc = Reg 0 + let stk = Reg 31 type expr = IntLit of Infinite_z.t | Label of string | AddOp of expr * expr | SubOp of expr * expr @@ -62,8 +63,8 @@ type machine_op = | StoreU of regname * reg_or_const * reg_or_const | PromoteU of regname | EInit of regname * regname - | EDeInit of regname * regname - | EStoreId of regname * regname * regname + | EDeInit of regname + | EStoreId of regname * regname | IsUnique of regname * regname | Fail | Halt @@ -225,9 +226,9 @@ let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op = (translate_regname r, translate_reg_or_const envr c1, translate_reg_or_const envr c2) | PromoteU r -> Ast.PromoteU (translate_regname r) | EInit (r1, r2) -> Ast.EInit (translate_regname r1, translate_regname r2) - | EDeInit (r1, r2) -> Ast.EDeInit (translate_regname r1, translate_regname r2) - | EStoreId (r1, r2, r3) -> - Ast.EStoreId (translate_regname r1, translate_regname r2, translate_regname r3) + | EDeInit r -> Ast.EDeInit (translate_regname r) + | EStoreId (r1, r2) -> + Ast.EStoreId (translate_regname r1, translate_regname r2) | IsUnique (r1, r2) -> Ast.IsUnique (translate_regname r1, translate_regname r2) | Fail -> Ast.Fail | Halt -> Ast.Halt diff --git a/lib/machine.ml b/lib/machine.ml index 39cc158..8f5ddba 100644 --- a/lib/machine.ml +++ b/lib/machine.ml @@ -13,11 +13,12 @@ module RegMap = Map.Make (struct let compare = compare_regname end) -type eid = Z.t +type eidentity = Z.t type e_counter = Z.t +type tindex = Z.t module ETableMap = Map.Make (struct - type t = Z.t + type t = tindex let compare = compare end) @@ -25,7 +26,7 @@ end) type exec_state = Running | Halted | Failed type reg_state = word RegMap.t type mem_state = word MemMap.t -type e_table = (eid * e_counter) ETableMap.t +type e_table = eidentity ETableMap.t type exec_conf = { reg : reg_state; mem : mem_state; etbl : e_table; ec : e_counter } (* using a record to have notation similar to the paper *) @@ -81,15 +82,15 @@ let ( @? ) x y = get_mem x y let upd_mem (addr : Z.t) (w : word) ({ reg; mem; etbl; ec } : exec_conf) : exec_conf = { reg; mem = MemMap.add addr w mem; etbl; ec } -let get_etbl (etbl_idx : Z.t) (conf : exec_conf) : (eid * e_counter) option = - ETableMap.find_opt etbl_idx conf.etbl +let get_etbl (tid : tindex) (conf : exec_conf) : eidentity option = + ETableMap.find_opt tid conf.etbl -let upd_etbl (etbl_idx : Z.t) (identity : eid) (ecounter : e_counter) +let upd_etbl (tid : tindex) (identity : eidentity) ({ reg; mem; etbl; ec } : exec_conf) : exec_conf = - { reg; mem; etbl = ETableMap.add etbl_idx (identity, ecounter) etbl; ec } + { reg; mem; etbl = ETableMap.add tid identity etbl; ec } -let del_etbl (etbl_idx : Z.t) ({ reg; mem; etbl; ec } : exec_conf) : exec_conf = - { reg; mem; etbl = ETableMap.remove etbl_idx etbl; ec } +let del_etbl (tid : tindex) ({ reg; mem; etbl; ec } : exec_conf) : exec_conf = + { reg; mem; etbl = ETableMap.remove tid etbl; ec } let upd_ec (n : e_counter) ({ reg; mem; etbl; _ } : exec_conf) : exec_conf = { reg; mem; etbl; ec = n } @@ -558,9 +559,9 @@ let exec_single (conf : exec_conf) : mchn = | _ -> fail_state) | EInit (rdst, rsrc) -> ( match rsrc @! conf with - | Sealable (Cap (p, _, b, e, _)) when can_read p && is_exec p -> ( + | Sealable (Cap (p, _, b, e, a)) when can_read p && is_exec p -> ( match b @? conf with - | Some (Sealable (Cap (p', _, b', e', _))) when can_read p' && can_write p' -> + | Some (Sealable (Cap (p', _, b', _, _))) when can_read p' && can_write p' -> let isunique_code = sweep_reg conf rsrc in let isunique_data = sweep_addr conf b in if isunique_data then @@ -577,45 +578,36 @@ let exec_single (conf : exec_conf) : mchn = (to_list (MemMap.filter (region_filter b e) conf.mem)) in let code_region = region Z.(b + ~$1) e in - let data_region = region b' e' in - let enclave_region = List.append code_region data_region in - let identity : Z.t = Z.of_int (Hashtbl.hash enclave_region) in + let enclave_region = code_region in + let identity : Z.t = Z.of_int (Hashtbl.hash (b, enclave_region)) in - let conf_etbl' = upd_etbl conf.ec identity conf.ec conf in + let conf_etbl' = upd_etbl conf.ec identity conf in let conf_mem' = upd_mem b' seal_keys conf_etbl' in let conf_ec' = incr_ec conf_mem' in - (* upd_ec Z.(conf.ec + ~$1) conf_mem' in *) - !>(upd_reg rdst (Sealable (Cap (E, Global, b, e, Z.(b + ~$1)))) conf_ec') - else (Failed, upd_reg rdst (I ~$3) conf) - else (Failed, upd_reg rdst (I ~$4) conf) - (* fail_state *) + !>(upd_reg rdst (Sealable (Cap (E, Global, b, e, a))) conf_ec') + else fail_state + else fail_state | _ -> fail_state) | _ -> fail_state) - | EDeInit (rdst, rsrc) -> ( + | EDeInit rsrc -> ( match rsrc @! conf with | Sealable (SealRange ((true, true), Global, b, e, _)) when e = Z.(b + ~$2) -> if Z.is_even b then - let eid = Z.(b / ~$2) in - let res = match get_etbl eid conf with Some _ -> I ~$1 | None -> I ~$0 in - !>(upd_reg rdst res (del_etbl eid conf)) + let tid = Z.(b / ~$2) in + !>(del_etbl tid conf) else fail_state | _ -> fail_state) - | EStoreId (rdst, rsrc1, rsrc2) -> ( - match rsrc1 @! conf with + | EStoreId (rdst, rsrc) -> ( + match rsrc @! conf with | I s -> ( - let eid = + let tid = let open Z in if is_even s then s / of_int 2 else (s - Z.one) / of_int 2 in - match get_etbl eid conf with - | Some (identity, _) -> ( - match rsrc2 @! conf with - | Sealable (Cap (p, _, b, e, a)) - when can_write p && b <= a && Infinite_z.z_leq a e -> - !>(upd_mem a (I identity) (upd_reg rdst (I ~$1) conf)) - (* !> (upd_mem a (I ~$357232418) (upd_reg rdst (I ~$1) conf)) *) - | _ -> fail_state) - | None -> !>(upd_reg rdst (I ~$0) conf)) + match get_etbl tid conf with + | Some identity -> + !>(upd_reg rdst (I identity) conf) + | None -> fail_state) | _ -> fail_state) | IsUnique (rdst, rsrc) -> ( match rsrc @! conf with diff --git a/lib/parameters.ml b/lib/parameters.ml index 65c368f..ca5eb37 100644 --- a/lib/parameters.ml +++ b/lib/parameters.ml @@ -206,7 +206,7 @@ let check_machine_op (i : Ast.machine_op) = | PromoteU _ -> if not !flags.unitialized then instruction_not_supported "PromoteU" | _ -> ()); match i with - | PromoteU r | Jmp r -> check_register r + | PromoteU r | EDeInit r | Jmp r -> check_register r | GetL (r1, r2) | GetB (r1, r2) | GetE (r1, r2) @@ -218,7 +218,7 @@ let check_machine_op (i : Ast.machine_op) = | Invoke (r1, r2) | Jnz (r1, r2) | EInit (r1, r2) - | EDeInit (r1, r2) + | EStoreId (r1, r2) | IsUnique (r1, r2) -> check_register r1; check_register r2 @@ -236,7 +236,7 @@ let check_machine_op (i : Ast.machine_op) = check_register r1; check_zreg zr2; check_zreg zr3 - | EStoreId (r1, r2, r3) | Seal (r1, r2, r3) | UnSeal (r1, r2, r3) -> + | Seal (r1, r2, r3) | UnSeal (r1, r2, r3) -> check_register r1; check_register r2; check_register r3 diff --git a/lib/parser.mly b/lib/parser.mly index 8de5e12..88d59d0 100644 --- a/lib/parser.mly +++ b/lib/parser.mly @@ -53,8 +53,8 @@ main: | STOREU; r = reg; c1 = reg_const; c2 = reg_const; p = main; { StoreU (r, c1, c2) :: p } | PROMOTEU; r = reg; p = main ; { PromoteU r :: p } | EINIT; r1 = reg; r2 = reg; p = main; { EInit (r1, r2) :: p } - | EDEINIT; r1 = reg; r2 = reg; p = main; { EDeInit (r1, r2) :: p } - | ESTOREID; r1 = reg; r2 = reg; r3 = reg ; p = main; { EStoreId (r1, r2, r3) :: p } + | EDEINIT; r1 = reg; p = main; { EDeInit r1 :: p } + | ESTOREID; r1 = reg; r2 = reg ; p = main; { EStoreId (r1, r2) :: p } | ISUNIQUE; r1 = reg; r2 = reg; p = main; { IsUnique (r1, r2) :: p } | FAIL; p = main; { Fail :: p } | HALT; p = main; { Halt :: p } diff --git a/lib/pretty_printer.ml b/lib/pretty_printer.ml index 8f29ee2..9d07533 100644 --- a/lib/pretty_printer.ml +++ b/lib/pretty_printer.ml @@ -101,8 +101,8 @@ let string_of_machine_op (s : machine_op) : string = | StoreU (r, c1, c2) -> "storeU" ^- string_of_rcc r c1 c2 | PromoteU r -> "promoteU" ^- string_of_regname r | EInit (r1, r2) -> "einit" ^- string_of_rr r1 r2 - | EDeInit (r1, r2) -> "edeinit" ^- string_of_rr r1 r2 - | EStoreId (r1, r2, r3) -> "estoreid" ^- string_of_rrr r1 r2 r3 + | EDeInit r -> "edeinit" ^- string_of_regname r + | EStoreId (r1, r2) -> "estoreid" ^- string_of_rr r1 r2 | IsUnique (r1, r2) -> "isunique" ^- string_of_rr r1 r2 | Fail -> "fail" | Halt -> "halt" diff --git a/lib/program.ml b/lib/program.ml index 2ef2740..fe8f92f 100644 --- a/lib/program.ml +++ b/lib/program.ml @@ -26,11 +26,7 @@ let parse_regfile (filename : string) (stk_addr : Z.t) : let init_machine (prog : Ast.t) (init_regs : Ast.word Machine.RegMap.t) : Machine.mchn = let addr_start = Z.(~$0) in - (* TODO lookup the PC *) let init_mems = Machine.init_mem_state addr_start prog in let init_etbl = Machine.ETableMap.empty in - (* let init_etbl = Machine.ETableMap.add Z.zero (Z.of_int (Hashtbl.hash init_mems), Z.zero) init_etbl in *) - (* let init_etbl = Machine.ETableMap.add Z.one (Z.of_int (Hashtbl.hash init_etbl), Z.one) init_etbl in *) - (* let init_etbl = Machine.ETableMap.add (Z.of_int 2) (Z.of_int (Hashtbl.hash init_etbl), (Z.of_int 2)) init_etbl in *) - let init_ec : Machine.eid = Z.zero in + let init_ec : Machine.e_counter = Z.zero in Machine.init init_regs init_mems init_etbl init_ec diff --git a/tests/test_files/default/pos/enclave.s b/tests/test_files/default/pos/enclave.s index 59e2127..af3326f 100644 --- a/tests/test_files/default/pos/enclave.s +++ b/tests/test_files/default/pos/enclave.s @@ -12,6 +12,7 @@ boot: mov r2 (tc_start-boot) mov r3 (tc_data-boot) subseg r1 r2 r3 + lea r1 tc_main restrict r1 (RX, Global) ;; init enclave @@ -20,8 +21,7 @@ boot: lea r31 3 jmp r0 getotype r2 r1 - estoreid r3 r2 r31 - load r3 r31 + estoreid r3 r2 ;; deinit enclave mov r31 pc @@ -55,7 +55,7 @@ tc_deinit: lea r0 (tc_start-tc_deinit) load r1 r0 load r1 r1 - edeinit r1 r1 + edeinit r1 jmp r31 tc_data: #0 diff --git a/tests/tester.ml b/tests/tester.ml index 95e56c2..272c4ef 100644 --- a/tests/tester.ml +++ b/tests/tester.ml @@ -30,7 +30,7 @@ let run_prog (filename : string) : mchn = let init_regs = Machine.init_reg_state stk_addr in let init_mems = Machine.init_mem_state Z.(~$0) parse_res in let init_etbl = Machine.ETableMap.empty in - let init_ec : Machine.eid = Z.zero in + let init_ec : Machine.e_counter = Z.zero in let m = Machine.init init_regs init_mems init_etbl init_ec in run m diff --git a/tests/tests.ml b/tests/tests.ml index d239873..7aefc75 100644 --- a/tests/tests.ml +++ b/tests/tests.ml @@ -74,8 +74,8 @@ let instr_tests = ("promoteu r29", Op (PromoteU (Reg 29))); ("isunique r31 r2", Op (IsUnique (Reg 31, Reg 2))); ("einit r1 r3", Op (EInit (Reg 1, Reg 3))); - ("edeinit r1 r3", Op (EDeInit (Reg 1, Reg 3))); - ("estoreid r1 r3 r4", Op (EStoreId (Reg 1, Reg 3, Reg 4))); + ("edeinit r1", Op (EDeInit (Reg 1))); + ("estoreid r1 r3", Op (EStoreId (Reg 1, Reg 3))); ("fail", Op Fail); ("halt", Op Halt); ] @@ -229,8 +229,8 @@ let test_enc_dec_stm_list = ( LoadU (Reg 31, stk, encode_perm_loc URWLX Directed), "encore-decode LoadU R31 stk URWLX Directed" ); (EInit (Reg 6, Reg 28), "encode-decode EInit R6 R28"); - (EDeInit (Reg 6, Reg 28), "encode-decode EDeInit R6 R28"); - (EStoreId (Reg 6, Reg 28, Reg 9), "encode-decode EStoreId R6 R28 R9"); + (EDeInit (Reg 6), "encode-decode EDeInit R6"); + (EStoreId (Reg 6, Reg 9), "encode-decode EStoreId R6 R9"); (IsUnique (Reg 6, Reg 28), "encode-decode IsUnique R6 R28"); (PromoteU stk, "encore-decode PromoteU stk"); (Fail, "encode-decode Fail");