WIP

lib/ast.ml

@@ -44,6 +44,10 @@ type machine_op =
   | LoadU of regname * regname * reg_or_const
   | StoreU of regname * reg_or_const * reg_or_const
   | PromoteU of regname
+  | EInit of regname * regname
+  | EDeInit of regname * regname
+  | EStoreId of regname * regname
+  | IsUnique of regname * regname
   | Fail
   | Halt
 

lib/encode.ml

@@ -374,8 +374,12 @@ let encode_machine_op (s : machine_op) : Z.t =
       let opc, c_enc = two_const_convert ~$0x33 c1 c2 in
       opc ^! encode_int_int (encode_reg r) c_enc
   | PromoteU r -> ~$0x37 ^! encode_reg r
-  | Fail -> ~$0x38
-  | Halt -> ~$0x39
+  | 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) -> ~$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
 
 let decode_machine_op (i : Z.t) : machine_op =
   (* let dec_perm = *)
@@ -587,10 +591,36 @@ let decode_machine_op (i : Z.t) : machine_op =
     StoreU (r, c1, c2)
   else if (* PromoteU *)
           opc = ~$0x37 && !Parameters.flags.unitialized then PromoteU (decode_reg payload)
+
+  else if (* EInit *)
+          opc = ~$0x38 then
+    let r1_enc, r2_enc = decode_int payload in
+    let r1 = decode_reg r1_enc in
+    let r2 = decode_reg r2_enc in
+    EInit (r1, r2)
+  else if (* EDeInit *)
+          opc = ~$0x3a 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)
+  else if (* EStoreId *)
+          opc = ~$0x3a 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)
+  else if (* IsUnique *)
+          opc = ~$0x3b then
+    let r1_enc, r2_enc = decode_int payload in
+    let r1 = decode_reg r1_enc in
+    let r2 = decode_reg r2_enc in
+    IsUnique (r1, r2)
+
   else if (* Fail *)
-          opc = ~$0x38 then Fail
+          opc = ~$0x3c then Fail
   else if (* Halt *)
-          opc = ~$0x39 then Halt
+          opc = ~$0x3d then Halt
   else
     raise
     @@ DecodeException

lib/ir.ml

@@ -61,6 +61,10 @@ type machine_op =
   | LoadU of regname * regname * reg_or_const
   | StoreU of regname * reg_or_const * reg_or_const
   | PromoteU of regname
+  | EInit of regname * regname
+  | EDeInit of regname * regname
+  | EStoreId of regname * regname
+  | IsUnique of regname * regname
   | Fail
   | Halt
   | Lbl of string
@@ -220,6 +224,10 @@ let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op =
       Ast.StoreU
         (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) -> 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
   | Word w -> raise (WordException w)

lib/lexer.mll

@@ -62,6 +62,9 @@ rule token = parse
 | "load" ['u' 'U'] { LOADU }
 | "store" ['u' 'U'] { STOREU }
 | "promote" ['u' 'U'] { PROMOTEU }
+| "einit" { EINIT }
+| "edeinit" { EDEINIT }
+| "estoreid" { ESTOREID }
 | "fail" { FAIL }
 | "halt" { HALT }
 

lib/machine.ml

@@ -13,10 +13,20 @@ module RegMap = Map.Make (struct
   let compare = compare_regname
 end)
 
+type eid = Z.t
+type e_counter = Z.t
+
+module ETableMap = Map.Make (struct
+  type t = Z.t
+
+  let compare = compare
+end)
+
 type exec_state = Running | Halted | Failed
 type reg_state = word RegMap.t
 type mem_state = word MemMap.t
-type exec_conf = { reg : reg_state; mem : mem_state }
+type e_table = (eid * e_counter) 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 *)
 type mchn = exec_state * exec_conf
@@ -62,8 +72,24 @@ let init_reg_state (stk_addr : Z.t) : reg_state =
 let get_reg (r : regname) ({ reg; _ } : exec_conf) : word = RegMap.find r reg
 let ( @! ) x y = get_reg x y
 
-let upd_reg (r : regname) (w : word) ({ reg; mem } : exec_conf) : exec_conf =
-  { reg = RegMap.add r w reg; mem }
+let upd_reg (r : regname) (w : word) ({ reg; mem; etbl; ec } : exec_conf) : exec_conf =
+  { reg = RegMap.add r w reg; mem ; etbl ; ec}
+
+let get_mem (addr : Z.t) (conf : exec_conf) : word option = MemMap.find_opt addr conf.mem
+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 upd_etbl (etbl_idx : Z.t) (identity : eid) (ecounter : e_counter) ({ reg; mem ; etbl ; ec } : exec_conf) : exec_conf =
+  { reg; mem ; etbl = ETableMap.add etbl_idx (identity, ecounter) etbl ; ec }
+
+let upd_ec (n : e_counter) ({ reg; mem ; etbl ; _ } : exec_conf) : exec_conf =
+  { reg; mem ; etbl ; ec = n }
+
 
 let init_mem_state (addr_start : Z.t) (prog : t) : mem_state =
   let zeroed_mem =
@@ -92,14 +118,8 @@ let init_mem_state (addr_start : Z.t) (prog : t) : mem_state =
   in
   MemMap.add_seq enc_prog zeroed_mem
 
-let get_mem (addr : Z.t) (conf : exec_conf) : word option = MemMap.find_opt addr conf.mem
-let ( @? ) x y = get_mem x y
-
-let upd_mem (addr : Z.t) (w : word) ({ reg; mem } : exec_conf) : exec_conf =
-  { reg; mem = MemMap.add addr w mem }
-
-let init (initial_regs : word RegMap.t) (initial_mems : word MemMap.t) =
-  (Running, { reg = initial_regs; mem = initial_mems })
+let init (initial_regs : reg_state) (initial_mems : mem_state) (initial_etbl : e_table) (initial_ec : e_counter) =
+  (Running, { reg = initial_regs; mem = initial_mems ; etbl = initial_etbl ; ec = initial_ec })
 
 let get_word (conf : exec_conf) (roc : reg_or_const) : word =
   match roc with Register r -> get_reg r conf | Const i -> I i
@@ -185,6 +205,42 @@ let get_locality_sealable (s : sealable) =
 let is_sealrange (sb : sealable) = match sb with SealRange _ -> true | _ -> false
 let is_cap (sb : sealable) = match sb with Cap _ -> true | _ -> false
 
+let get_scap (w : word) : sealable option =
+  match w with
+  | Sealable (Cap (p,l,b,e,a)) -> Some (Cap (p,l,b,e,a))
+  | Sealed (_, (Cap (p,l,b,e,a))) -> Some (Cap (p,l,b,e,a))
+  | _ -> None
+
+let overlap_word (w1 : word) (w2 : word) : bool =
+  match get_scap w1, get_scap w2 with
+  | Some (Cap (_,_,b1,e1,_)), Some (Cap (_,_,b2,e2,_)) ->
+      if (b1 < b2)
+      then (Infinite_z.z_leq b2 (Infinite_z.sub_z e1 Z.one))
+      else (Infinite_z.z_leq b1 (Infinite_z.sub_z e2 Z.one))
+  | _,_ -> false
+
+let all_registers : regname list = [ PC; stk ] @ List.init 32 (fun i -> Reg i)
+
+(* sweep all the register, excluding the register src *)
+let sweep_registers_reg (conf : exec_conf) (src : regname) =
+  let w = get_reg src conf in
+  List.fold_left
+      (fun res w' -> res && overlap_word w w')
+
+
+
+
+
+let sweep_reg (conf : exec_conf) (src : regname) : bool =
+  let unique_mem = sweep_memory_reg conf src in
+  let unique_reg = sweep_registers_reg conf src in
+  unique_mem && unique_reg
+
+let sweep_addr (conf : exec_conf) (src : addr) : bool =
+  let unique_mem = sweep_memory_mem conf src in
+  let unique_reg = sweep_registers_mem conf src in
+  unique_mem && unique_reg
+
 (* NOTE Although we've already check that not supported instructions / capabilities *)
 (*  are not in the initial machine, we still need to make sure that *)
 (*  the user does not encode not supported instructions *)
@@ -486,7 +542,12 @@ let exec_single (conf : exec_conf) : mchn =
                     let e' = Infinite_z.min_z e a in
                     !>(upd_reg r (Sealable (Cap (p', g, b, e', a))) conf)
                 | _ -> fail_state)
-            | _ -> fail_state))
+            | _ -> fail_state)
+        | EInit (_, _) -> fail_state
+        | EDeInit (_, _) -> fail_state
+        | EStoreId (_, _) -> fail_state
+        | IsUnique (_, _) -> fail_state
+    )
   else fail_state
 
 let step (m : mchn) : mchn option =

lib/parameters.ml

@@ -216,7 +216,11 @@ let check_machine_op (i : Ast.machine_op) =
   | GetWType (r1, r2)
   | Load (r1, r2)
   | Invoke (r1, r2)
-  | Jnz (r1, r2) ->
+  | Jnz (r1, r2)
+  | EInit (r1, r2)
+  | EDeInit (r1, r2)
+  | EStoreId (r1, r2)
+  | IsUnique (r1, r2) ->
       check_register r1;
       check_register r2
   | Lea (r1, zr2) | Restrict (r1, zr2) | Store (r1, zr2) | Move (r1, zr2) ->

lib/parser.mly

@@ -10,6 +10,7 @@
 %token JMP JNZ MOVE LOAD STORE ADD SUB MUL REM DIV LT LEA RESTRICT SUBSEG
 %token GETL GETB GETE GETA GETP GETOTYPE GETWTYPE SEAL UNSEAL INVOKE
 %token LOADU STOREU PROMOTEU FAIL HALT
+%token EINIT EDEINIT ESTOREID
 %token LOCAL GLOBAL DIRECTED
 %token O E RO RX RW RWX RWL RWLX URW URWX URWL URWLX
 %token SO S U SU
@@ -51,6 +52,9 @@ main:
   | LOADU; r1 = reg; r2 = reg; c = reg_const; p = main; { LoadU (r1, r2, c) :: p }
   | 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; p = main; { EStoreId (r1, r2) :: p }
   | FAIL; p = main; { Fail :: p }
   | HALT; p = main; { Halt :: p }
   | lbl = LABELDEF; p = main; { Lbl lbl :: p }

lib/pretty_printer.ml

@@ -98,6 +98,10 @@ let string_of_machine_op (s : machine_op) : string =
   | LoadU (r1, r2, c) -> "loadU" ^- string_of_rrc r1 r2 c
   | 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) -> "EStoreId" ^- string_of_rr r1 r2
+  | IsUnique (r1, r2) -> "IsUnique" ^- string_of_rr r1 r2
   | Fail -> "fail"
   | Halt -> "halt"
 

lib/program.ml

@@ -28,4 +28,6 @@ let init_machine (prog : Ast.t) (init_regs : Ast.word Machine.RegMap.t) : Machin
   let addr_start = Z.(~$0) in
   (* TODO lookup the PC *)
   let init_mems = Machine.init_mem_state addr_start prog in
-  Machine.init init_regs init_mems
+  let init_etbl = Machine.ETableMap.empty in
+  let init_ec : Machine.eid = Z.zero in
+  Machine.init init_regs init_mems init_etbl init_ec

tests/tester.ml

@@ -29,7 +29,9 @@ let run_prog (filename : string) : mchn =
   let stk_addr = Z.(Parameters.get_max_addr () / ~$2) in
   let init_regs = Machine.init_reg_state stk_addr in
   let init_mems = Machine.init_mem_state Z.(~$0) parse_res in
-  let m = Machine.init init_regs init_mems in
+  let init_etbl = Machine.ETableMap.empty in
+  let init_ec : Machine.eid = Z.zero in
+  let m = Machine.init init_regs init_mems init_etbl init_ec in
 
   run m