From 4309870e7b4d968187ff5da57e5db5a59fd41866 Mon Sep 17 00:00:00 2001 From: June Rousseau Date: Fri, 1 Nov 2024 17:21:04 +0100 Subject: [PATCH] WIP --- lib/ast.ml | 4 ++ lib/encode.ml | 38 +++++++++++++++++-- lib/ir.ml | 8 ++++ lib/lexer.mll | 3 ++ lib/machine.ml | 85 +++++++++++++++++++++++++++++++++++++------ lib/parameters.ml | 6 ++- lib/parser.mly | 4 ++ lib/pretty_printer.ml | 4 ++ lib/program.ml | 4 +- tests/tester.ml | 4 +- 10 files changed, 141 insertions(+), 19 deletions(-) diff --git a/lib/ast.ml b/lib/ast.ml index 2e5d377..1ffdf71 100644 --- a/lib/ast.ml +++ b/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 diff --git a/lib/encode.ml b/lib/encode.ml index bd120f2..1e38157 100644 --- a/lib/encode.ml +++ b/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 diff --git a/lib/ir.ml b/lib/ir.ml index 11d4d78..5c42786 100644 --- a/lib/ir.ml +++ b/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) diff --git a/lib/lexer.mll b/lib/lexer.mll index 2079a13..575d65a 100644 --- a/lib/lexer.mll +++ b/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 } diff --git a/lib/machine.ml b/lib/machine.ml index 3304677..37e73d2 100644 --- a/lib/machine.ml +++ b/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 = diff --git a/lib/parameters.ml b/lib/parameters.ml index 4801bd8..9a5f1c5 100644 --- a/lib/parameters.ml +++ b/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) -> diff --git a/lib/parser.mly b/lib/parser.mly index e363618..51fac81 100644 --- a/lib/parser.mly +++ b/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 } diff --git a/lib/pretty_printer.ml b/lib/pretty_printer.ml index ca926a2..c668a87 100644 --- a/lib/pretty_printer.ml +++ b/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" diff --git a/lib/program.ml b/lib/program.ml index c3c5b47..b52f0d6 100644 --- a/lib/program.ml +++ b/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 diff --git a/tests/tester.ml b/tests/tester.ml index a3e6b74..8b8c42c 100644 --- a/tests/tester.ml +++ b/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