feat(cerisier): update the opsem with new definitions

logsem · Dec 19, 2024 · 0863807 · 0863807
1 parent ff40d14
commit 0863807
Show file tree

Hide file tree

Showing 12 changed files with 65 additions and 82 deletions.
diff --git 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
@@ -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
@@ -210,25 +210,25 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
   end
 
   module ETable_panel = struct
-    (* <eid>: <identity>
-       <eid>: <identity>
-       <eid>: <identity>
+    (* <tid>: <identity>
+       <tid>: <identity>
+       <tid>: <identity>
     *)
     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
@@ -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
@@ -13,19 +13,20 @@ 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)
 
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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");