From 61379e0d973f4a504b42e510b6322044a0e42b3b Mon Sep 17 00:00:00 2001 From: Bastien Rousseau Date: Tue, 4 Jun 2024 16:14:15 +0200 Subject: [PATCH] New permissions; instructions Jalr+Jmp+Jnz+MoveSR ; new parser/lexer/pp ; adapt tests --- lib/ast.ml | 50 ++- lib/encode.ml | 385 +++++++++++------- lib/interactive_ui.ml | 6 +- lib/ir.ml | 67 +-- lib/irreg.ml | 67 ++- lib/lexer.mll | 17 +- lib/lexer_regfile.mll | 16 +- lib/machine.ml | 194 +++++---- lib/parameters.ml | 20 +- lib/parser.mly | 47 ++- lib/parser_regfile.mly | 30 +- lib/pretty_printer.ml | 36 +- lib/program.ml | 4 +- src/interpreter.ml | 4 +- tests/test_files/default/neg/bad_flow1.s | 2 +- tests/test_files/default/neg/bad_flow3.s | 2 +- tests/test_files/default/neg/bad_flow_WL.s | 6 +- .../default/neg/bad_flow_locality.s | 6 +- tests/test_files/default/pos/jmper.s | 4 +- tests/test_files/default/pos/jmper_jalr.s | 7 + tests/test_files/default/pos/mov_test.s | 11 + .../test_files/default/pos/sealing_counter.s | 47 +-- tests/test_files/default/pos/test1.s | 27 -- tests/test_files/default/pos/test1_labels.s | 47 ++- .../default/pos/test_locality_flow.s | 6 +- tests/tester.ml | 29 +- tests/tests.ml | 91 +++-- 27 files changed, 714 insertions(+), 514 deletions(-) create mode 100644 tests/test_files/default/pos/jmper_jalr.s delete mode 100644 tests/test_files/default/pos/test1.s diff --git a/lib/ast.ml b/lib/ast.ml index c1fee41..899f519 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -1,9 +1,9 @@ (* Type definitions for the syntax AST *) type regname = PC | Reg of int -let cgp = Reg 0 -let stk = Reg 31 -let sreg = Reg 30 +let cgp = Reg 5 +let stk = Reg 30 +let mtcc = Reg 31 module Perm = struct @@ -16,23 +16,23 @@ struct | 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 1 - let allowed_with (p1 : t) (p2 : t) = - match (p1,p2) with - (* sentry are not allowed with any other capabilities *) - | E,_ -> false - (* system access permission only with X *) - | SR,X -> true - | SR,_ -> false - - (* no write and execute permission at the same time *) - | W,X -> false - | WL,X -> false - - | _,_ -> true + let compare p1 p2 = if (p1 = p2) then 0 else + (* Just an order for pretty printing *) + let weight p = + match p with + | E -> 0 + | R -> 1 + | X -> 2 + | W -> 3 + | WL -> 4 + | SR -> 5 + | DL -> 6 + | DI -> 7 + in + (weight p2) - (weight p1) end -module PermSet = Set.Make(Perm) +module PermSet = Set.Make(Perm) type locality = Global | Local type wtype = W_I | W_Cap | W_SealRange | W_Sealed @@ -46,20 +46,28 @@ type sealable = type word = I of Z.t | Sealable of sealable | Sealed of Z.t * sealable type machine_op = - | Jmp of regname - | Jnz of regname * regname + | Jalr of regname * regname (* jump and link return *) + | 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 + | Move of regname * reg_or_const | Load of regname * regname | Store of regname * reg_or_const + | Add of regname * reg_or_const * reg_or_const | Sub of regname * reg_or_const * reg_or_const | Mul of regname * reg_or_const * reg_or_const | Rem of regname * reg_or_const * reg_or_const | Div of regname * reg_or_const * reg_or_const | Lt of regname * reg_or_const * reg_or_const + | Lea of regname * reg_or_const | Restrict of regname * reg_or_const | SubSeg of regname * reg_or_const * reg_or_const + | GetL of regname * regname | GetB of regname * regname | GetE of regname * regname @@ -67,8 +75,10 @@ type machine_op = | GetP of regname * regname | GetOType of regname * regname | GetWType of regname * regname + | Seal of regname * regname * regname | UnSeal of regname * regname * regname + | Fail | Halt diff --git a/lib/encode.ml b/lib/encode.ml index b9e7524..90fae32 100644 --- a/lib/encode.ml +++ b/lib/encode.ml @@ -88,49 +88,73 @@ 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) : Z.t = +let perm_encoding (p : Perm.t) : Z.t = Z.of_int @@ match p with - | O -> 0b00000 - | E -> 0b00001 - | RO -> 0b00100 - | RX -> 0b00101 - | RW -> 0b00110 - | RWX -> 0b00111 - | RWL -> 0b01110 - | RWLX -> 0b01111 - -let perm_decoding (i : Z.t) : perm = + | E -> 0b10000000 + | R -> 0b01000000 + | X -> 0b00100000 + | W -> 0b00010000 + | WL -> 0b00001000 + | SR -> 0b00000100 + | DL -> 0b00000010 + | DI -> 0b00000001 + +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 dec_perm_exception _ = raise @@ DecodeException "Error decoding permission: unexpected encoding" in - let b0 = Z.testbit i 0 in - let b1 = Z.testbit i 1 in - let b2 = Z.testbit i 2 in - let b3 = Z.testbit i 3 in - let b4 = Z.testbit i 4 in - if Z.(i > of_int 0b11111) then dec_perm_exception () + if Z.(i > of_int 0b11111111) then dec_perm_exception () else - match (b4, b3, b2, b1, b0) with - | false, false, false, false, false -> O - | false, false, false, false, true -> E - | false, false, true, false, false -> RO - | false, false, true, false, true -> RX - | false, false, true, true, false -> RW - | false, false, true, true, true -> RWX - | false, true, true, true, false -> RWL - | false, true, true, true, true -> RWLX + let b k = Z.testbit i k in + match (b 7, b 6, b 5, b 4, b 3, b 2, b 1, b 0) with + | true, false, false, false, false, false, false, false -> E + | false, true, false, false, false, false, false, false -> R + | false, false, true, false, false, false, false, false -> X + | false, false, false, true, false, false, false, false -> W + | false, false, false, false, true, false, false, false -> WL + | false, false, false, false, false, true, false, false -> SR + | false, false, false, false, false, false, true, false -> DL + | false, false, false, false, false, false, false, true -> DI | _ -> dec_perm_exception () -let encode_perm (p : perm) : Z.t = encode_const _PERM_ENC (perm_encoding p) +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] + 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 encode_perm (p : PermSet.t) : Z.t = encode_const _PERM_ENC (fperm_encoding p) -let decode_perm (i : Z.t) : perm = +let decode_perm (i : Z.t) : PermSet.t = 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 perm_decoding dec_i + if dec_type != _PERM_ENC then dec_perm_exception () else fperm_decoding dec_i (** Sealing Permission *) @@ -162,29 +186,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 : perm) (g : locality) : Z.t = - let size_perm = 5 in +let perm_loc_pair_encoding (p : PermSet.t) (g : locality) : Z.t = + let size_perm = 8 in let open Z in let encoded_g = locality_encoding g lsl size_perm in - let encoded_p = perm_encoding p in + let encoded_p = fperm_encoding p in encoded_g lor encoded_p -let encode_perm_loc_pair (p : perm) (g : locality) : Z.t = +let encode_perm_loc_pair (p : PermSet.t) (g : locality) : Z.t = encode_const _PERM_LOC_ENC (perm_loc_pair_encoding p g) -let perm_loc_pair_decoding (i : Z.t) : perm * locality = - let size_perm = 5 in +let perm_loc_pair_decoding (i : Z.t) : PermSet.t * locality = + let size_perm = 8 in let dec_perm_loc_exception _ = raise @@ DecodeException "Error decoding permission-locality pair: unexpected encoding" in let open Z in - if i > of_int 0b1111111 then dec_perm_loc_exception () + if i > of_int 0b1111111111 then dec_perm_loc_exception () else - let encoded_g = (i land of_int 0b1100000) asr size_perm in - let encoded_p = i land of_int 0b0011111 in - (perm_decoding encoded_p, locality_decoding encoded_g) + 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 decode_perm_loc_pair (i : Z.t) : perm * locality = +let decode_perm_loc_pair (i : Z.t) : PermSet.t * locality = let dec_perm_loc_exception _ = raise @@ DecodeException @@ -295,66 +319,85 @@ let encode_machine_op (s : machine_op) : Z.t = (opc2, encode_int_int c1_enc c2_enc) in match s with - | Jmp r -> ~$0x00 ^! encode_reg r - | Jnz (r1, r2) -> ~$0x01 ^! encode_int_int (encode_reg r1) (encode_reg r2) + | Jmp c -> + (* 0x00, 0x01 *) + let opc, c_enc = const_convert ~$0x00 c in + opc ^! c_enc + | Jnz (r, c) -> + (* 0x02, 0x03 *) + let opc, c_enc = const_convert ~$0x02 c in + opc ^! encode_int_int (encode_reg r) c_enc + | 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 + | Move (r, c) -> - (* 0x02, 0x03 *) - let opc, c_enc = const_convert ~$0x02 c in + (* 0x07, 0x08 *) + let opc, c_enc = const_convert ~$0x07 c in opc ^! encode_int_int (encode_reg r) c_enc - | Load (r1, r2) -> ~$0x04 ^! encode_int_int (encode_reg r1) (encode_reg r2) + | Load (r1, r2) -> + (* 0x09 *) + ~$0x09 ^! encode_int_int (encode_reg r1) (encode_reg r2) | Store (r, c) -> - (* 0x05, 0x06 *) - let opc, c_enc = const_convert ~$0x05 c in + (* 0x0a, 0x0b *) + let opc, c_enc = const_convert ~$0x0a c in opc ^! encode_int_int (encode_reg r) c_enc | Add (r, c1, c2) -> - (* 0x07, 0x08, 0x09, 0x0a *) - let opc, c_enc = two_const_convert ~$0x07 c1 c2 in + (* 0x0c, 0x0d, 0x0e, 0x0f *) + let opc, c_enc = two_const_convert ~$0x0c c1 c2 in opc ^! encode_int_int (encode_reg r) c_enc | Sub (r, c1, c2) -> - (* 0x0b, 0x0c, 0x0d, 0x0e *) - let opc, c_enc = two_const_convert ~$0x0b c1 c2 in + (* 0x10, 0x11, 0x12, 0x13 *) + let opc, c_enc = two_const_convert ~$0x10 c1 c2 in opc ^! encode_int_int (encode_reg r) c_enc | Mul (r, c1, c2) -> - (* 0x0f, 0x10, 0x11, 0x12 *) - let opc, c_enc = two_const_convert ~$0x0f c1 c2 in + (* 0x14, 0x15, 0x16, 0x17 *) + let opc, c_enc = two_const_convert ~$0x14 c1 c2 in opc ^! encode_int_int (encode_reg r) c_enc | Rem (r, c1, c2) -> - (* 0x13, 0x14, 0x15, 0x16 *) - let opc, c_enc = two_const_convert ~$0x13 c1 c2 in + (* 0x18, 0x19, 0x1a, 0x1b *) + let opc, c_enc = two_const_convert ~$0x18 c1 c2 in opc ^! encode_int_int (encode_reg r) c_enc | Div (r, c1, c2) -> - (* 0x17, 0x18, 0x19, 0x1a *) - let opc, c_enc = two_const_convert ~$0x17 c1 c2 in + (* 0x1c, 0x1d, 0x1e, 0x1f *) + let opc, c_enc = two_const_convert ~$0x1c c1 c2 in opc ^! encode_int_int (encode_reg r) c_enc | Lt (r, c1, c2) -> - (* 0x1b, 0x1c, 0x1d, 0x1e *) - let opc, c_enc = two_const_convert ~$0x1b c1 c2 in + (* 0x20, 0x21, 0x22, 0x23 *) + let opc, c_enc = two_const_convert ~$0x20 c1 c2 in opc ^! encode_int_int (encode_reg r) c_enc | Lea (r, c) -> - (* 0x1f, 0x20 *) - let opc, c_enc = const_convert ~$0x1f c in + (* 0x24, 0x25 *) + let opc, c_enc = const_convert ~$0x24 c in opc ^! encode_int_int (encode_reg r) c_enc | Restrict (r, c) -> - (* 0x21, 0x22 *) - let opc, c_enc = const_convert ~$0x21 c in + (* 0x26, 0x27 *) + let opc, c_enc = const_convert ~$0x26 c in opc ^! encode_int_int (encode_reg r) c_enc | SubSeg (r, c1, c2) -> - (* 0x23, 0x24, 0x25, 0x26 *) - let opc, c_enc = two_const_convert ~$0x23 c1 c2 in + (* 0x28, 0x29, 0x2a, 0x2b *) + let opc, c_enc = two_const_convert ~$0x28 c1 c2 in opc ^! encode_int_int (encode_reg r) c_enc - | GetL (r1, r2) -> ~$0x27 ^! encode_int_int (encode_reg r1) (encode_reg r2) - | GetB (r1, r2) -> ~$0x28 ^! encode_int_int (encode_reg r1) (encode_reg r2) - | GetE (r1, r2) -> ~$0x29 ^! encode_int_int (encode_reg r1) (encode_reg r2) - | GetA (r1, r2) -> ~$0x2a ^! encode_int_int (encode_reg r1) (encode_reg r2) - | GetP (r1, r2) -> ~$0x2b ^! encode_int_int (encode_reg r1) (encode_reg r2) - | GetOType (r1, r2) -> ~$0x2c ^! encode_int_int (encode_reg r1) (encode_reg r2) - | GetWType (r1, r2) -> ~$0x2d ^! encode_int_int (encode_reg r1) (encode_reg r2) + | GetL (r1, r2) -> ~$0x2c ^! encode_int_int (encode_reg r1) (encode_reg r2) + | GetB (r1, r2) -> ~$0x2d ^! encode_int_int (encode_reg r1) (encode_reg r2) + | GetE (r1, r2) -> ~$0x2e ^! encode_int_int (encode_reg r1) (encode_reg r2) + | GetA (r1, r2) -> ~$0x2f ^! encode_int_int (encode_reg r1) (encode_reg r2) + | GetP (r1, r2) -> ~$0x30 ^! encode_int_int (encode_reg r1) (encode_reg r2) + | GetOType (r1, r2) -> + ~$0x31 ^! encode_int_int (encode_reg r1) (encode_reg r2) + | GetWType (r1, r2) -> + ~$0x32 ^! encode_int_int (encode_reg r1) (encode_reg r2) | Seal (r1, r2, r3) -> - ~$0x2e ^! encode_int_int (encode_reg r1) (encode_int_int (encode_reg r2) (encode_reg r3)) + ~$0x33 ^! encode_int_int (encode_reg r1) (encode_int_int (encode_reg r2) (encode_reg r3)) | UnSeal (r1, r2, r3) -> - ~$0x2f ^! encode_int_int (encode_reg r1) (encode_int_int (encode_reg r2) (encode_reg r3)) - | Fail -> ~$0x30 - | Halt -> ~$0x31 + ~$0x34 ^! encode_int_int (encode_reg r1) (encode_int_int (encode_reg r2) (encode_reg r3)) + | Fail -> ~$0x35 + | Halt -> ~$0x36 let decode_machine_op (i : Z.t) : machine_op = (* let dec_perm = *) @@ -362,182 +405,236 @@ let decode_machine_op (i : Z.t) : machine_op = (* in *) let opc = Z.extract i 0 8 in let payload = Z.(i asr 8) in + (* Jmp *) - if opc = ~$0x00 then Jmp (decode_reg payload) - else if (* Jnz *) - opc = ~$0x01 then + if opc = ~$0x00 (* register register *) then + let r = Register (decode_reg payload) in + Jmp r + else if opc = ~$0x01 (* register const *) then + let r = Const payload in + Jmp r + + (* Jnz *) + else if opc = ~$0x02 then let r1_enc, r2_enc = decode_int payload in let r1 = decode_reg r1_enc in - let r2 = decode_reg r2_enc in + let r2 = Register (decode_reg r2_enc) in Jnz (r1, r2) - else if (* Move *) - opc = ~$0x02 (* register register *) then + else if opc = ~$0x03 then + let r1_enc, c_enc = decode_int payload in + let r1 = decode_reg r1_enc in + let c = Const c_enc in + Jnz (r1, c) + + (* Jalr *) + else if opc = ~$0x04 then + let r1_enc, r2_enc = decode_int payload in + let r1 = decode_reg r1_enc in + let r2 = decode_reg r2_enc in + Jalr (r1, r2) + + (* MoveSR *) + else if 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 + let r = decode_reg r_enc in + let c = Const c_enc in + MoveSR (r, c) + + (* Move *) + else if opc = ~$0x07 (* 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 Move (r1, r2) - else if opc = ~$0x03 (* register const *) then + else if opc = ~$0x08 (* register const *) then let r_enc, c_enc = decode_int payload in let r = decode_reg r_enc in let c = Const c_enc in Move (r, c) - else if (* Load *) - opc = ~$0x04 then + + (* Load *) + else if opc = ~$0x09 then let r1_enc, r2_enc = decode_int payload in let r1 = decode_reg r1_enc in let r2 = decode_reg r2_enc in Load (r1, r2) - else if (* Store *) - opc = ~$0x05 (* register register *) then + + (* Store *) + else if opc = ~$0x0a (* 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 Store (r1, r2) - else if opc = ~$0x06 (* register const *) then + else if opc = ~$0x0b (* register const *) then let r_enc, c_enc = decode_int payload in let r = decode_reg r_enc in let c = Const c_enc in Store (r, c) - else if (* Add *) - ~$0x07 <= opc && opc <= ~$0x0a then + + (* Add *) + else if ~$0x0c <= opc && opc <= ~$0x0f then let r_enc, payload' = decode_int payload in let c1_enc, c2_enc = decode_int payload' in let r = decode_reg r_enc in - let c1 = if opc = ~$0x07 || opc = ~$0x08 then Register (decode_reg c1_enc) else Const c1_enc in - let c2 = if opc = ~$0x07 || opc = ~$0x09 then Register (decode_reg c2_enc) else Const c2_enc in + let c1 = if opc = ~$0x0c || opc = ~$0x0d then Register (decode_reg c1_enc) else Const c1_enc in + let c2 = if opc = ~$0x0c || opc = ~$0x0e then Register (decode_reg c2_enc) else Const c2_enc in Add (r, c1, c2) - else if (* Sub *) - ~$0x0b <= opc && opc <= ~$0x0e then + + (* Sub *) + else if ~$0x10 <= opc && opc <= ~$0x13 then let r_enc, payload' = decode_int payload in let c1_enc, c2_enc = decode_int payload' in let r = decode_reg r_enc in - let c1 = if opc = ~$0x0b || opc = ~$0x0c then Register (decode_reg c1_enc) else Const c1_enc in - let c2 = if opc = ~$0x0b || opc = ~$0x0d then Register (decode_reg c2_enc) else Const c2_enc in + let c1 = if opc = ~$0x10 || opc = ~$0x11 then Register (decode_reg c1_enc) else Const c1_enc in + let c2 = if opc = ~$0x10 || opc = ~$0x12 then Register (decode_reg c2_enc) else Const c2_enc in Sub (r, c1, c2) - else if (* Mul *) - ~$0x0f <= opc && opc <= ~$0x12 then + + (* Mul *) + else if ~$0x14 <= opc && opc <= ~$0x17 then let r_enc, payload' = decode_int payload in let c1_enc, c2_enc = decode_int payload' in let r = decode_reg r_enc in - let c1 = if opc = ~$0x0f || opc = ~$0x10 then Register (decode_reg c1_enc) else Const c1_enc in - let c2 = if opc = ~$0x0f || opc = ~$0x11 then Register (decode_reg c2_enc) else Const c2_enc in + let c1 = if opc = ~$0x14 || opc = ~$0x15 then Register (decode_reg c1_enc) else Const c1_enc in + let c2 = if opc = ~$0x14 || opc = ~$0x16 then Register (decode_reg c2_enc) else Const c2_enc in Mul (r, c1, c2) - else if (* Rem *) - ~$0x13 <= opc && opc <= ~$0x16 then + + (* Rem *) + else if ~$0x18 <= opc && opc <= ~$0x1b then let r_enc, payload' = decode_int payload in let c1_enc, c2_enc = decode_int payload' in let r = decode_reg r_enc in - let c1 = if opc = ~$0x13 || opc = ~$0x14 then Register (decode_reg c1_enc) else Const c1_enc in - let c2 = if opc = ~$0x13 || opc = ~$0x15 then Register (decode_reg c2_enc) else Const c2_enc in + let c1 = if opc = ~$0x18 || opc = ~$0x19 then Register (decode_reg c1_enc) else Const c1_enc in + let c2 = if opc = ~$0x18 || opc = ~$0x1a then Register (decode_reg c2_enc) else Const c2_enc in Rem (r, c1, c2) - else if (* Div *) - ~$0x17 <= opc && opc <= ~$0x1a then + + (* Div *) + else if ~$0x1c <= opc && opc <= ~$0x1f then let r_enc, payload' = decode_int payload in let c1_enc, c2_enc = decode_int payload' in let r = decode_reg r_enc in - let c1 = if opc = ~$0x17 || opc = ~$0x18 then Register (decode_reg c1_enc) else Const c1_enc in - let c2 = if opc = ~$0x17 || opc = ~$0x19 then Register (decode_reg c2_enc) else Const c2_enc in + let c1 = if opc = ~$0x1c || opc = ~$0x1d then Register (decode_reg c1_enc) else Const c1_enc in + let c2 = if opc = ~$0x1c || opc = ~$0x1e then Register (decode_reg c2_enc) else Const c2_enc in Div (r, c1, c2) - else if (* Lt *) - ~$0x1b <= opc && opc <= ~$0x1e then + + (* Lt *) + else if ~$0x20 <= opc && opc <= ~$0x23 then let r_enc, payload' = decode_int payload in let c1_enc, c2_enc = decode_int payload' in let r = decode_reg r_enc in - let c1 = if opc = ~$0x1b || opc = ~$0x1c then Register (decode_reg c1_enc) else Const c1_enc in - let c2 = if opc = ~$0x1b || opc = ~$0x1d then Register (decode_reg c2_enc) else Const c2_enc in + let c1 = if opc = ~$0x20 || opc = ~$0x21 then Register (decode_reg c1_enc) else Const c1_enc in + let c2 = if opc = ~$0x20 || opc = ~$0x22 then Register (decode_reg c2_enc) else Const c2_enc in Lt (r, c1, c2) - else if (* Lea *) - opc = ~$0x1f (* register register *) then + + (* Lea *) + else if opc = ~$0x24 (* 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 Lea (r1, r2) - else if opc = ~$0x20 (* register const *) then + else if opc = ~$0x25 (* register const *) then let r_enc, c_enc = decode_int payload in let r = decode_reg r_enc in let c = Const c_enc in Lea (r, c) - else if (* Restrict *) - opc = ~$0x21 (* register register *) then + + (* Restrict *) + else if opc = ~$0x26 (* 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 Restrict (r1, r2) - else if opc = ~$0x22 (* register const *) then + else if opc = ~$0x27 (* register const *) then let r_enc, c_enc = decode_int payload in let r = decode_reg r_enc in let c = Const c_enc in Restrict (r, c) - else if (* Subseg *) - ~$0x23 <= opc && opc <= ~$0x26 then + + (* Subseg *) + else if ~$0x28 <= opc && opc <= ~$0x2b then let r_enc, payload' = decode_int payload in let c1_enc, c2_enc = decode_int payload' in let r = decode_reg r_enc in - let c1 = if opc = ~$0x23 || opc = ~$0x24 then Register (decode_reg c1_enc) else Const c1_enc in - let c2 = if opc = ~$0x23 || opc = ~$0x25 then Register (decode_reg c2_enc) else Const c2_enc in + let c1 = if opc = ~$0x28 || opc = ~$0x29 then Register (decode_reg c1_enc) else Const c1_enc in + let c2 = if opc = ~$0x28 || opc = ~$0x2a then Register (decode_reg c2_enc) else Const c2_enc in SubSeg (r, c1, c2) - else if (* GetL *) - opc = ~$0x27 then + + (* GetL *) + else if opc = ~$0x2c then let r1_enc, r2_enc = decode_int payload in let r1 = decode_reg r1_enc in let r2 = decode_reg r2_enc in GetL (r1, r2) - else if (* GetB *) - opc = ~$0x28 then + + (* GetB *) + else if opc = ~$0x2d then let r1_enc, r2_enc = decode_int payload in let r1 = decode_reg r1_enc in let r2 = decode_reg r2_enc in GetB (r1, r2) - else if (* GetE *) - opc = ~$0x29 then + + (* GetE *) + else if opc = ~$0x2e then let r1_enc, r2_enc = decode_int payload in let r1 = decode_reg r1_enc in let r2 = decode_reg r2_enc in GetE (r1, r2) - else if (* GetA *) - opc = ~$0x2a then + + (* GetA *) + else if opc = ~$0x2f then let r1_enc, r2_enc = decode_int payload in let r1 = decode_reg r1_enc in let r2 = decode_reg r2_enc in GetA (r1, r2) - else if (* GetP *) - opc = ~$0x2b then + + (* GetP *) + else if opc = ~$0x30 then let r1_enc, r2_enc = decode_int payload in let r1 = decode_reg r1_enc in let r2 = decode_reg r2_enc in GetP (r1, r2) - else if (* GetOType *) - opc = ~$0x2c then + + (* GetOType *) + else if opc = ~$0x31 then let r1_enc, r2_enc = decode_int payload in let r1 = decode_reg r1_enc in let r2 = decode_reg r2_enc in GetOType (r1, r2) - else if (* GetWType *) - opc = ~$0x2d then + + (* GetWType *) + else if opc = ~$0x32 then let r1_enc, r2_enc = decode_int payload in let r1 = decode_reg r1_enc in let r2 = decode_reg r2_enc in GetWType (r1, r2) - else if (* Seal *) - opc = ~$0x2e then + + (* Seal *) + else if opc = ~$0x33 then let r1_enc, payload' = decode_int payload in let r2_enc, r3_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 Seal (r1, r2, r3) - else if (* UnSeal *) - opc = ~$0x2f then + + (* UnSeal *) + else if opc = ~$0x34 then let r1_enc, payload' = decode_int payload in let r2_enc, r3_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 UnSeal (r1, r2, r3) - else if (* Fail *) - opc = ~$0x30 then Fail - else if (* Halt *) - opc = ~$0x31 then Halt + + (* Fail *) + else if opc = ~$0x35 then Fail + + (* Halt *) + else if opc = ~$0x36 then Halt else raise @@ DecodeException diff --git a/lib/interactive_ui.ml b/lib/interactive_ui.ml index 720f429..bb6e983 100644 --- a/lib/interactive_ui.ml +++ b/lib/interactive_ui.ml @@ -15,10 +15,10 @@ end module MkUi (Cfg : MachineConfig) : Ui = struct module Perm = struct - let width = 5 + let width = 12 - let ui ?(attr = A.empty) (p : Ast.perm) = - I.hsnap ~align:`Left width (I.string attr (Pretty_printer.string_of_perm p)) + let ui ?(attr = A.empty) (p : Ast.PermSet.t) = + I.hsnap ~align:`Left width (I.string attr (Pretty_printer.string_of_fperm p)) end module Locality = struct diff --git a/lib/ir.ml b/lib/ir.ml index d0a1259..0f191e6 100644 --- a/lib/ir.ml +++ b/lib/ir.ml @@ -3,16 +3,17 @@ exception UnknownLabelException of string exception ExprException of string -type regname = PC | Reg of int +type regname = Ast.regname -let cgp = Reg 0 -let stk = Reg 31 +let cgp = Ast.Reg 5 +let stk = Ast.Reg 30 +let mtcc = Ast.Reg 31 type expr = IntLit of Z.t | Label of string | AddOp of expr * expr | SubOp of expr * expr -type perm = O | E | RO | RX | RW | RWX | RWL | RWLX -type locality = Global | Local -type seal_perm = bool * bool -type wtype = W_I | W_Cap | W_SealRange | W_Sealed +type perm = Ast.PermSet.t +type locality = Ast.locality +type seal_perm = Ast.seal_perm +type wtype = Ast.wtype type const_encoded = | ConstExpr of expr @@ -34,8 +35,12 @@ type word = I of expr | Sealable of sealable | Sealed of expr * sealable exception WordException of word type machine_op = - | Jmp of regname - | Jnz of regname * regname + | Jalr of regname * regname + | Jmp of reg_or_const + | Jnz of regname * reg_or_const + + | MoveSR of regname * reg_or_const + | Move of regname * reg_or_const | Load of regname * regname | Store of regname * reg_or_const @@ -48,6 +53,7 @@ type machine_op = | Lea of regname * reg_or_const | Restrict of regname * reg_or_const | SubSeg of regname * reg_or_const * reg_or_const + | GetL of regname * regname | GetB of regname * regname | GetE of regname * regname @@ -55,10 +61,13 @@ type machine_op = | GetP of regname * regname | GetOType of regname * regname | GetWType of regname * regname + | Seal of regname * regname * regname | UnSeal of regname * regname * regname + | Fail | Halt + | Lbl of string | Word of word @@ -82,28 +91,13 @@ let rec eval_expr (envr : env) (e : expr) : Z.t = | AddOp (e1, e2) -> Z.(eval_expr envr e1 + eval_expr envr e2) | SubOp (e1, e2) -> Z.(eval_expr envr e1 - eval_expr envr e2) -let translate_perm (p : perm) : Ast.perm = - match p with - | O -> Ast.O - | E -> Ast.E - | RO -> Ast.RO - | RX -> Ast.RX - | RW -> Ast.RW - | RWX -> Ast.RWX - | RWL -> Ast.RWL - | RWLX -> Ast.RWLX - -let translate_locality (g : locality) : Ast.locality = - match g with Local -> Ast.Local | Global -> Ast.Global - -let translate_wt (wt : wtype) : Ast.wtype = - match wt with - | W_I -> Ast.W_I - | W_Cap -> Ast.W_Cap - | W_SealRange -> Ast.W_SealRange - | W_Sealed -> Ast.W_Sealed - -let translate_regname (r : regname) : Ast.regname = match r with PC -> Ast.PC | Reg i -> Ast.Reg i +let translate_perm (p : perm) : Ast.PermSet.t = p + +let translate_locality (g : locality) : Ast.locality = g + +let translate_wt (wt : wtype) : Ast.wtype = wt + +let translate_regname (r : regname) : Ast.regname = r let translate_reg_or_const (envr : env) (roc : reg_or_const) : Ast.reg_or_const = match roc with @@ -143,8 +137,12 @@ let translate_word (envr : env) (w : word) : Ast.statement = let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op = match instr with - | Jmp r -> Ast.Jmp (translate_regname r) - | Jnz (r1, r2) -> Ast.Jnz (translate_regname r1, translate_regname r2) + | Jalr (r1,r2) -> Ast.Jalr (translate_regname r1, translate_regname r2) + | Jmp r -> Ast.Jmp (translate_reg_or_const envr r) + | Jnz (r1, r2) -> Ast.Jnz (translate_regname r1, translate_reg_or_const envr r2) + + | MoveSR (r, c) -> Ast.MoveSR (translate_regname r, translate_reg_or_const envr c) + | Move (r, c) -> Ast.Move (translate_regname r, translate_reg_or_const envr c) | Load (r1, r2) -> Ast.Load (translate_regname r1, translate_regname r2) | Store (r, c) -> Ast.Store (translate_regname r, translate_reg_or_const envr c) @@ -165,6 +163,7 @@ let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op = | SubSeg (r, c1, c2) -> Ast.SubSeg (translate_regname r, translate_reg_or_const envr c1, translate_reg_or_const envr c2) + | GetL (r1, r2) -> Ast.GetL (translate_regname r1, translate_regname r2) | GetB (r1, r2) -> Ast.GetB (translate_regname r1, translate_regname r2) | GetE (r1, r2) -> Ast.GetE (translate_regname r1, translate_regname r2) @@ -172,11 +171,13 @@ let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op = | GetP (r1, r2) -> Ast.GetP (translate_regname r1, translate_regname r2) | GetOType (r1, r2) -> Ast.GetOType (translate_regname r1, translate_regname r2) | GetWType (r1, r2) -> Ast.GetWType (translate_regname r1, translate_regname r2) + | Seal (r1, r2, r3) -> Ast.Seal (translate_regname r1, translate_regname r2, translate_regname r3) | UnSeal (r1, r2, r3) -> Ast.UnSeal (translate_regname r1, translate_regname r2, translate_regname r3) | Fail -> Ast.Fail | Halt -> Ast.Halt + | Word w -> raise (WordException w) | Lbl s -> raise (UnknownLabelException s) diff --git a/lib/irreg.ml b/lib/irreg.ml index 619db55..b9e17ab 100644 --- a/lib/irreg.ml +++ b/lib/irreg.ml @@ -2,18 +2,17 @@ exception ExprException of string -type regname = PC | STK | CGP | Reg of int +type regname = PC | STK | CGP | MTCC | Reg of int type expr = | IntLit of Z.t | AddOp of expr * expr | SubOp of expr * expr | MaxAddr - | StkAddr -type perm = O | E | RO | RX | RW | RWX | RWL | RWLX -type locality = Global | Local -type seal_perm = bool * bool +type perm = Ast.PermSet.t +type locality = Ast.locality +type seal_perm = Ast.seal_perm type sealable = | WCap of perm * locality * expr * expr * expr @@ -22,62 +21,56 @@ type sealable = type word = WI of expr | WSealable of sealable | WSealed of expr * sealable type t = (regname * word) list -let rec eval_expr (e : expr) (max_addr : Z.t) (stk_addr : Z.t) : Z.t = +let rec eval_expr (e : expr) (max_addr : Z.t) : Z.t = match e with | IntLit i -> i | MaxAddr -> max_addr - | StkAddr -> stk_addr - | AddOp (e1, e2) -> Z.(eval_expr e1 max_addr stk_addr + eval_expr e2 max_addr stk_addr) - | SubOp (e1, e2) -> Z.(eval_expr e1 max_addr stk_addr - eval_expr e2 max_addr stk_addr) + | AddOp (e1, e2) -> Z.(eval_expr e1 max_addr + eval_expr e2 max_addr ) + | SubOp (e1, e2) -> Z.(eval_expr e1 max_addr - eval_expr e2 max_addr ) -let translate_perm (p : perm) : Ast.perm = - match p with - | O -> Ast.O - | E -> Ast.E - | RO -> Ast.RO - | RX -> Ast.RX - | RW -> Ast.RW - | RWX -> Ast.RWX - | RWL -> Ast.RWL - | RWLX -> Ast.RWLX +let translate_perm (p : perm) : Ast.PermSet.t = p -let translate_locality (g : locality) : Ast.locality = - match g with Local -> Ast.Local | Global -> Ast.Global +let translate_locality (g : locality) : Ast.locality = g let translate_regname (r : regname) : Ast.regname = - match r with PC -> Ast.PC | CGP -> Ast.cgp | STK -> Ast.stk | Reg i -> Ast.Reg i + match r with + | PC -> Ast.PC + | CGP -> Ast.cgp + | STK -> Ast.stk + | MTCC -> Ast.mtcc + | Reg i -> Ast.Reg i -let translate_sealable (sb : sealable) (max_addr : Z.t) (stk_addr : Z.t) : Ast.sealable = +let translate_sealable (sb : sealable) (max_addr : Z.t) : Ast.sealable = match sb with | WCap (p, g, b, e, a) -> let g = translate_locality g in let p = translate_perm p in - let b = eval_expr b max_addr stk_addr in - let e = eval_expr e max_addr stk_addr in - let a = eval_expr a max_addr stk_addr in + let b = eval_expr b max_addr in + let e = eval_expr e max_addr in + let a = eval_expr a max_addr in Cap (p, g, b, e, a) | WSealRange (p, g, b, e, a) -> let g = translate_locality g in - let b = eval_expr b max_addr stk_addr in - let e = eval_expr e max_addr stk_addr in - let a = eval_expr a max_addr stk_addr in + let b = eval_expr b max_addr in + let e = eval_expr e max_addr in + let a = eval_expr a max_addr in SealRange (p, g, b, e, a) -let translate_word (w : word) (max_addr : Z.t) (stk_addr : Z.t) : Ast.word = +let translate_word (w : word) (max_addr : Z.t) : Ast.word = match w with | WI e -> - let z = eval_expr e max_addr stk_addr in + let z = eval_expr e max_addr in Ast.I z - | WSealable sb -> Ast.Sealable (translate_sealable sb max_addr stk_addr) + | WSealable sb -> Ast.Sealable (translate_sealable sb max_addr) | WSealed (o, sb) -> - let ot = eval_expr o max_addr stk_addr in - Ast.Sealed (ot, translate_sealable sb max_addr stk_addr) + let ot = eval_expr o max_addr in + Ast.Sealed (ot, translate_sealable sb max_addr) -let rec translate_regfile (regfile : t) (max_addr : Z.t) (stk_addr : Z.t) : +let rec translate_regfile (regfile : t) (max_addr : Z.t) : Ast.word Machine.RegMap.t = let init_regfile = Machine.RegMap.empty in match regfile with | [] -> init_regfile | (r, w) :: rf -> - let nrf = translate_regfile rf max_addr stk_addr in - Machine.RegMap.add (translate_regname r) (translate_word w max_addr stk_addr) nrf + let nrf = translate_regfile rf max_addr in + Machine.RegMap.add (translate_regname r) (translate_word w max_addr) nrf diff --git a/lib/lexer.mll b/lib/lexer.mll index c385c68..30e0d6f 100644 --- a/lib/lexer.mll +++ b/lib/lexer.mll @@ -12,7 +12,6 @@ let digit = ['0'-'9'] let hex = (digit | ['a'-'f'] | ['A'-'F']) let reg_num = ((digit) | ('1' digit) | ('2' digit) | "30" | "31") -let perm = ('O' | 'E' | "RO" | "RW" | "RWX") let locality = ("LOCAL" | "GLOBAL" | "Local" | "Global") let letter = ['a'-'z' 'A'-'Z'] let label = ('_' | letter) (letter | '_' | digit)* @@ -29,12 +28,15 @@ rule token = parse | ['p' 'P'] ['c' 'C'] { PC } | ['s' 'S'] ['t' 'T'] ['k' 'K'] { STK } | ['c' 'C'] ['g' 'G'] ['p' 'P'] { CGP } +| ['m' 'M'] ['t' 'T'] ['c' 'C'] ['c' 'C'] { MTCC } | ['r' 'R'] (reg_num as n) { try REG (int_of_string n) with Failure _ -> error lexbuf ("Invalid register id '" ^ n ^ "'.")} (* machine_op *) +| "jalr" { JALR } | "jmp" { JMP } | "jnz" { JNZ } +| "movSR" { MOVESR } | "mov" { MOVE } | "load" { LOAD } | "store" { STORE } @@ -80,12 +82,13 @@ rule token = parse (* permissions *) | 'O' { O } | 'E' { E } -| "RO" { RO } -| "RX" { RX } -| "RW" { RW } -| "RWX" { RWX } -| "RWL" { RWL } -| "RWLX" { RWLX } +| 'R' { R } +| 'X' { X } +| 'W' { W } +| "WL" { WL } +| "SR" { SR } +| "DL" { DL } +| "DI" { DI } | "SO" { SO } | 'S' { S } | 'U' { U } diff --git a/lib/lexer_regfile.mll b/lib/lexer_regfile.mll index 66cba37..981de4c 100644 --- a/lib/lexer_regfile.mll +++ b/lib/lexer_regfile.mll @@ -29,11 +29,11 @@ rule token = parse | ['p' 'P'] ['c' 'C'] { PC } | ['s' 'S'] ['t' 'T'] ['k' 'K'] { STK } | ['c' 'C'] ['g' 'G'] ['p' 'P'] { CGP } +| ['m' 'M'] ['t' 'T'] ['c' 'C'] ['c' 'C'] { MTCC } | ['r' 'R'] (reg_num as n) { try REG (int_of_string n) with Failure _ -> error lexbuf ("Invalid register id '" ^ n ^ "'.")} (* addresses *) | "MAX_ADDR" { MAX_ADDR } -| "STK_ADDR" { STK_ADDR } (* single-character tokens *) | '(' { LPAREN } @@ -47,6 +47,7 @@ rule token = parse | ',' { COMMA } | ':' { COLON } | ":=" { AFFECT } +| '_' { UNDERSCORE } (* locality *) | "LOCAL" | "Local" { LOCAL } @@ -55,12 +56,13 @@ rule token = parse (* permissions *) | 'O' { O } | 'E' { E } -| "RO" { RO } -| "RX" { RX } -| "RW" { RW } -| "RWX" { RWX } -| "RWL" { RWL } -| "RWLX" { RWLX } +| 'R' { R } +| 'X' { X } +| 'W' { W } +| "WL" { WL } +| "SR" { SR } +| "DL" { DL } +| "DI" { DI } | "SO" { SO } | 'S' { S } | 'U' { U } diff --git a/lib/machine.ml b/lib/machine.ml index 6793357..3e143d9 100644 --- a/lib/machine.ml +++ b/lib/machine.ml @@ -1,5 +1,5 @@ open Ast -open Parameters +(* open Parameters *) let ( ~$ ) = Z.( ~$ ) @@ -18,39 +18,59 @@ type reg_state = word RegMap.t type mem_state = word MemMap.t type exec_conf = { reg : reg_state; mem : mem_state } +(* Architectural roots *) +(* - memory root, LD_LG_LM_MC_SD_SL --> R_W_WL *) +let arch_root_memory_perm = PermSet.of_list [R;W;WL] +(* - executable root, EX_LD_LG_LM_MC_SR --> R_X_SR *) +let arch_root_executable_perm = PermSet.of_list [R;X;SR] + +let is_derived_from (p_dst : PermSet.t) (p_src : PermSet.t) = + if (PermSet.equal p_dst p_src) (* p <= p *) + then true + else if PermSet.mem E p_dst (* E <= RX *) + then + (PermSet.equal (PermSet.of_list [E]) p_dst) + && (PermSet.mem R p_src) && (PermSet.mem X p_src) + && (not (PermSet.mem DL p_src)) && (not (PermSet.mem DI p_src)) + else (* p_dst ⊆ p_src, except that we can add DI or DL *) + (PermSet.subset (PermSet.remove DL (PermSet.remove DI p_dst)) p_src) + (* using a record to have notation similar to the paper *) type mchn = exec_state * exec_conf -let init_reg_state (stk_addr : Z.t) : reg_state = +let init_reg_state : reg_state = let start_heap_addr = ~$0 in - let max_heap_addr = !Parameters.flags.max_addr in - let max_stk_addr = !Parameters.flags.max_addr in + let max_heap_addr = Parameters.get_max_addr () in + let start_otype = ~$0 in + let max_otype = Parameters.get_max_otype () in let l = - let seal_reg = 1 in - let n = 31 - seal_reg in - List.init n (fun i -> (Reg (i + seal_reg), I Z.zero)) + let n = 30 in + List.init n (fun i -> (Reg (i + 1), I Z.zero)) in - let stk_init = - let stk_locality = Local in - let stk_perm = RWLX in - [ (stk, Sealable (Cap (stk_perm, stk_locality, stk_addr, max_stk_addr, stk_addr))) ] + let root_exec = + Sealable (Cap (arch_root_executable_perm, Global, start_heap_addr, max_heap_addr, start_heap_addr)) in - - (* The PC register starts with full permission over the entire "heap" segment *) - let pc_init = - [ (PC, Sealable (Cap (RWX, Global, start_heap_addr, max_heap_addr, start_heap_addr))) ] + let root_mem = + Sealable (Cap (arch_root_memory_perm, Global, start_heap_addr, max_heap_addr, start_heap_addr)) + in + let root_sealing = + Sealable (SealRange ((true, true), Global, start_otype, max_otype, start_otype)) in - let pc_sealing = - [ - ( Reg 0, - Sealable (SealRange ((true, true), Global, start_heap_addr, stk_addr, start_heap_addr)) ); - ] + (* The PC register starts with full exec permission over the entire "heap" segment *) + let pc_init = [ (PC, root_exec) ] in + (* The CGP register starts with full mem permission over the entire "heap" segment *) + let cgp_init = [ (cgp, root_mem) ] in + (* The R0 register starts with full sealing permission over the entire otypes region *) + let sealing_init = + let sealing_reg = Reg 0 in + [( sealing_reg, root_sealing);] in + (* The stk register starts with full permission over the entire "stack" segment *) - let seq = List.to_seq (pc_init @ pc_sealing @ l @ stk_init) in + let seq = List.to_seq (pc_init @ l @ sealing_init @ cgp_init) in RegMap.of_seq seq let get_reg (r : regname) ({ reg; _ } : exec_conf) : word = RegMap.find r reg @@ -106,7 +126,11 @@ let upd_pc (conf : exec_conf) : mchn = let ( !> ) conf = upd_pc conf let upd_pc_perm (w : word) = - match w with Sealable (Cap (E, g, b, e, a)) -> Sealable (Cap (RX, g, b, e, a)) | _ -> w + match w with + | Sealable (Cap (p, g, b, e, a)) + when (PermSet.equal p (PermSet.singleton E)) -> + Sealable (Cap (PermSet.of_list [R;X], g, b, e, a)) + | _ -> w let fetch_decode (conf : exec_conf) : machine_op option = match PC @! conf with @@ -117,40 +141,33 @@ let fetch_decode (conf : exec_conf) : machine_op option = | _ -> None) | _ -> None + +let is_WLperm (p : PermSet.t) : bool = (PermSet.mem WL p) && (PermSet.mem W p) +let is_exec (p : PermSet.t) : bool = (PermSet.mem R p) && (PermSet.mem X p) +let can_write (p : PermSet.t) : bool = (PermSet.mem W p) +let can_read (p : PermSet.t) : bool = (PermSet.mem R p) + let is_pc_valid (conf : exec_conf) : bool = match PC @! conf with - | Sealable (Cap ((RX | RWX | RWLX), _, b, e, a)) -> + | Sealable (Cap (p, _, b, e, a)) + when (is_exec p) -> if b <= a && a < e then Option.is_some @@ a @? conf else false | _ -> false -let perm_flowsto (p1 : perm) (p2 : perm) : bool = - match p1 with - | O -> true - | E -> ( match p2 with E | RX | RWX | RWLX -> true | _ -> false) - | RX -> ( match p2 with RX | RWX | RWLX -> true | _ -> false) - | RWX -> ( match p2 with RWX | RWLX -> true | _ -> false) - | RWLX -> ( match p2 with RWLX -> true | _ -> false) - | RO -> ( match p2 with E | O -> false | _ -> true) - | RW -> ( match p2 with RW | RWX | RWL | RWLX -> true | _ -> false) - | RWL -> ( match p2 with RWL | RWLX -> true | _ -> false) +let perm_flowsto (p1 : PermSet.t) (p2 : PermSet.t) : bool = + is_derived_from p1 p2 let locality_flowsto (g1 : locality) (g2 : locality) : bool = match g1 with | Local -> true | Global -> ( match g2 with Global -> true | _ -> false) -let is_WLperm (p : perm) : bool = match p with RWL | RWLX -> true | _ -> false -let is_exec (p : perm) : bool = match p with RX | RWX | RWLX -> true | _ -> false - let sealperm_flowsto (p1 : seal_perm) (p2 : seal_perm) : bool = let p_flows p p' = match (p, p') with false, _ -> true | true, true -> true | _, _ -> false in let s1, u1 = p1 in let s2, u2 = p2 in p_flows s1 s2 && p_flows u1 u2 -let can_write (p : perm) : bool = match p with RW | RWX | RWL | RWLX -> true | _ -> false -let can_read (p : perm) : bool = match p with RO | RX | RW | RWX | RWL | RWLX -> true | _ -> false - let get_wtype (w : word) : wtype = match w with | I _ -> W_I @@ -176,10 +193,44 @@ let exec_single (conf : exec_conf) : mchn = match instr with | Fail -> (Failed, conf) | Halt -> (Halted, conf) - | Move (r, c) -> + + | Jalr (r_dst, r_src) when (not (r_dst = mtcc) && not (r_src = mtcc)) -> + begin + match (PC @! conf) with + | Sealable (Cap (_,g,b,e,a)) -> + let new_pc = upd_pc_perm (r_src @! conf) in + let link_cap = Sealable (Cap (PermSet.singleton E,g,b,e,Z.(a+Z.one))) in + (Running, upd_reg PC new_pc (upd_reg r_dst link_cap conf)) + | _ -> fail_state + end + | Jmp c when (not (c = Register mtcc)) -> + begin + match get_word conf c,(PC @! conf) with + | I imm, Sealable (Cap (p,g,b,e,a)) -> + let new_pc = Sealable (Cap (p,g,b,e,Z.(a+imm))) in + (Running, upd_reg PC new_pc conf) + | _ -> fail_state + end + | Jnz (r_src, c) when (not (r_src = mtcc) && not (c = Register mtcc)) -> ( + match r_src @! conf with + | I i when Z.(equal i zero) -> !>conf + | _ -> + begin + match get_word conf c, PC @! conf with + | I imm, Sealable (Cap (p,g,b,e,a)) -> + let new_pc = Sealable (Cap (p,g,b,e,Z.(a+imm))) in + (Running, upd_reg PC new_pc conf) + | _,_ -> fail_state + end) + + | MoveSR (r, c) when (r = mtcc && not (c = Register mtcc))-> let w = get_word conf c in !>(upd_reg r w conf) - | Load (r1, r2) -> ( + + | Move (r, c) when (not (r = mtcc) && not (c = Register mtcc)) -> + let w = get_word conf c in + !>(upd_reg r w conf) + | Load (r1, r2) when (not (r1 = mtcc) && not (r2 = mtcc)) -> ( match r2 @! conf with | Sealable (Cap (p, _, b, e, a)) -> if can_read p then @@ -188,7 +239,7 @@ let exec_single (conf : exec_conf) : mchn = | _ -> fail_state else fail_state | _ -> fail_state) - | Store (r, c) -> ( + | Store (r, c) when (not (r = mtcc) && not (c = Register mtcc)) -> ( let w = get_word conf c in match r @! conf with | Sealable (Cap (p, _, b, e, a)) when b <= a && a < e -> @@ -201,16 +252,7 @@ let exec_single (conf : exec_conf) : mchn = | _ -> !>(upd_mem a w conf) else fail_state | _ -> fail_state) - | Jmp r -> - let new_pc = upd_pc_perm (r @! conf) in - (Running, upd_reg PC new_pc conf) - | Jnz (r1, r2) -> ( - match r2 @! conf with - | I i when Z.(equal i zero) -> !>conf - | _ -> - let new_pc = upd_pc_perm (r1 @! conf) in - (Running, upd_reg PC new_pc conf)) - | Restrict (r, c) -> ( + | Restrict (r, c) when (not (r = mtcc) && not (c = Register mtcc)) -> ( match r @! conf with | Sealable (Cap (p, g, b, e, a)) -> ( match get_word conf c with @@ -241,20 +283,16 @@ let exec_single (conf : exec_conf) : mchn = else fail_state) | _ -> fail_state) | _ -> fail_state) - | SubSeg (r, c1, c2) -> ( + | SubSeg (r, c1, c2) when (not (r = mtcc) && not (c1 = Register mtcc) && not (c2 = Register mtcc)) -> ( match r @! conf with | Sealable (Cap (p, g, b, e, a)) -> ( let w1 = get_word conf c1 in let w2 = get_word conf c2 in match (w1, w2) with | I z1, I z2 -> - if b <= z1 && Z.(~$0 <= z2) && Z.zero <= e && p <> E then + if b <= z1 && Z.(~$0 <= z2) && Z.zero <= e && (not (PermSet.mem E p)) then let w = Sealable (Cap (p, g, z1, z2, a)) in !>(upd_reg r w conf) - (* Special case: SubSeg (p,g,b,+∞,a) z1 (-1) , ie. the upper-bound is still infinity *) - (* else if b <= z1 && Z.(z2 == ~$(-1)) && Infinite_z.eq Inf e && p <> E then *) - (* let w = Sealable (Cap (p, g, z1, Inf, a)) in *) - (* !>(upd_reg r w conf) *) else fail_state | _ -> fail_state) | Sealable (SealRange (p, g, b, e, a)) -> ( @@ -268,12 +306,12 @@ let exec_single (conf : exec_conf) : mchn = else fail_state | _ -> fail_state) | _ -> fail_state) - | Lea (r, c) -> ( + | Lea (r, c) when (not (r = mtcc) && not (c = Register mtcc)) -> ( match r @! conf with | Sealable (Cap (p, g, b, e, a)) -> ( let w = get_word conf c in match w with - | I z when p <> E -> !>(upd_reg r (Sealable (Cap (p, g, b, e, Z.(a + z)))) conf) + | I z when (not (PermSet.mem E p)) -> !>(upd_reg r (Sealable (Cap (p, g, b, e, Z.(a + z)))) conf) | _ -> fail_state) | Sealable (SealRange (p, g, b, e, a)) -> ( let w = get_word conf c in @@ -281,82 +319,86 @@ let exec_single (conf : exec_conf) : mchn = | I z -> !>(upd_reg r (Sealable (SealRange (p, g, b, e, Z.(a + z)))) conf) | _ -> fail_state) | _ -> fail_state) - | Add (r, c1, c2) -> ( + + | Add (r, c1, c2) when (not (r = mtcc) && not (c1 = Register mtcc) && not (c2 = Register mtcc)) -> ( let w1 = get_word conf c1 in let w2 = get_word conf c2 in match (w1, w2) with I z1, I z2 -> !>(upd_reg r (I Z.(z1 + z2)) conf) | _ -> fail_state) - | Sub (r, c1, c2) -> ( + | Sub (r, c1, c2) when (not (r = mtcc) && not (c1 = Register mtcc) && not (c2 = Register mtcc)) -> ( let w1 = get_word conf c1 in let w2 = get_word conf c2 in match (w1, w2) with I z1, I z2 -> !>(upd_reg r (I Z.(z1 - z2)) conf) | _ -> fail_state) - | Mul (r, c1, c2) -> ( + | Mul (r, c1, c2) when (not (r = mtcc) && not (c1 = Register mtcc) && not (c2 = Register mtcc)) -> ( let w1 = get_word conf c1 in let w2 = get_word conf c2 in match (w1, w2) with I z1, I z2 -> !>(upd_reg r (I Z.(z1 * z2)) conf) | _ -> fail_state) - | Rem (r, c1, c2) -> ( + | Rem (r, c1, c2) when (not (r = mtcc) && not (c1 = Register mtcc) && not (c2 = Register mtcc)) -> ( let w1 = get_word conf c1 in let w2 = get_word conf c2 in match (w1, w2) with | I z1, I z2 when z2 != Z.zero -> !>(upd_reg r (I Z.(z1 mod z2)) conf) | _ -> fail_state) - | Div (r, c1, c2) -> ( + | Div (r, c1, c2) when (not (r = mtcc) && not (c1 = Register mtcc) && not (c2 = Register mtcc)) -> ( let w1 = get_word conf c1 in let w2 = get_word conf c2 in match (w1, w2) with | I z1, I z2 when z2 != Z.zero -> !>(upd_reg r (I Z.(z1 / z2)) conf) | _ -> fail_state) - | Lt (r, c1, c2) -> ( + | Lt (r, c1, c2) when (not (r = mtcc) && not (c1 = Register mtcc) && not (c2 = Register mtcc)) -> ( let w1 = get_word conf c1 in let w2 = get_word conf c2 in match (w1, w2) with | I z1, I z2 when Z.(lt z1 z2) -> !>(upd_reg r (I Z.one) conf) | I _, I _ -> !>(upd_reg r (I Z.zero) conf) | _ -> fail_state) - | GetL (r1, r2) -> ( + + | GetL (r1, r2) when (not (r1 = mtcc) && not (r2 = mtcc)) -> ( match r2 @! conf with | Sealable sb | Sealed (_, sb) -> let g = get_locality_sealable sb in !>(upd_reg r1 (I (Encode.encode_locality g)) conf) | _ -> fail_state) - | GetB (r1, r2) -> ( + | GetB (r1, r2) when (not (r1 = mtcc) && not (r2 = mtcc)) -> ( match r2 @! conf with | Sealable (SealRange (_, _, b, _, _)) | Sealable (Cap (_, _, b, _, _)) -> !>(upd_reg r1 (I b) conf) | _ -> fail_state) - | GetE (r1, r2) -> ( + | GetE (r1, r2) when (not (r1 = mtcc) && not (r2 = mtcc)) -> ( match r2 @! conf with | Sealable (SealRange (_, _, _, e, _)) -> !>(upd_reg r1 (I e) conf) | Sealable (Cap (_, _, _, e, _)) -> !>(upd_reg r1 (I e) conf) | _ -> fail_state) - | GetA (r1, r2) -> ( + | GetA (r1, r2) when (not (r1 = mtcc) && not (r2 = mtcc)) -> ( match r2 @! conf with | Sealable (SealRange (_, _, _, _, a)) | Sealable (Cap (_, _, _, _, a)) -> !>(upd_reg r1 (I a) conf) | _ -> fail_state) - | GetP (r1, r2) -> ( + | GetP (r1, r2) when (not (r1 = mtcc) && not (r2 = mtcc)) -> ( match r2 @! conf with | Sealable (Cap (p, _, _, _, _)) -> !>(upd_reg r1 (I (Encode.encode_perm p)) conf) | Sealable (SealRange (p, _, _, _, _)) -> !>(upd_reg r1 (I (Encode.encode_seal_perm p)) conf) | _ -> fail_state) - | GetOType (r1, r2) -> ( + | GetOType (r1, r2) when (not (r1 = mtcc) && not (r2 = mtcc)) -> ( match r2 @! conf with | Sealed (o, _) -> !>(upd_reg r1 (I o) conf) | _ -> !>(upd_reg r1 (I ~$(-1)) conf)) - | GetWType (r1, r2) -> + | GetWType (r1, r2) when (not (r1 = mtcc) && not (r2 = mtcc)) -> let wtype_enc = Encode.encode_wtype (get_wtype (r2 @! conf)) in !>(upd_reg r1 (I wtype_enc) conf) - | Seal (dst, r1, r2) -> ( + + | Seal (dst, r1, r2) when (not (dst = mtcc) && not (r1 = mtcc) && not (r2 = mtcc)) -> ( match (r1 @! conf, r2 @! conf) with | Sealable (SealRange ((true, _), _, b, e, a)), Sealable sb when b <= a && a < e -> !>(upd_reg dst (Sealed (a, sb)) conf) | _ -> fail_state) - | UnSeal (dst, r1, r2) -> ( + | UnSeal (dst, r1, r2) when (not (dst = mtcc) && not (r1 = mtcc) && not (r2 = mtcc)) -> ( match (r1 @! conf, r2 @! conf) with | Sealable (SealRange ((_, true), _, b, e, a)), Sealed (a', sb) -> if b <= a && a < e && a = a' then !>(upd_reg dst (Sealable sb) conf) else fail_state - | _ -> fail_state)) + | _ -> fail_state) + | _ -> fail_state ) else fail_state let step (m : mchn) : mchn option = diff --git a/lib/parameters.ml b/lib/parameters.ml index e06ac73..b670149 100644 --- a/lib/parameters.ml +++ b/lib/parameters.ml @@ -1,26 +1,31 @@ type machineFlags = { version : string; (* Name of the version of Cerise *) - max_addr : Z.t; (* Maximum memory address (can be infinite) *) + max_addr : Z.t; (* Maximum memory address *) + max_otype : Z.t; (* Maximum otype *) } let max_addr = Z.of_int (Int32.to_int Int32.max_int / 4096) (* (2^31 - 1) / 2^12 *) +let max_otype = Z.of_int (Int32.to_int Int32.max_int / 4096) (* (2^31 - 1) / 2^12 *) let vanilla_cerise : machineFlags = { version = "vanilla-cerise"; max_addr = max_addr; + max_otype = max_otype; } let full_cerise : machineFlags = { version = "cerise"; max_addr = max_addr; + max_otype = max_otype; } let griotte : machineFlags = { version = "griotte"; max_addr = max_addr; + max_otype = Z.of_int 15; } let default : machineFlags = griotte @@ -31,8 +36,19 @@ exception MalformedConfiguration of string let set_max_addr a = flags := { + version = !flags.version; max_addr = a; - version = !flags.version + max_otype = !flags.max_otype; } let get_max_addr () : Z.t = !flags.max_addr + +let set_max_otype o = + flags := + { + version = !flags.version; + max_otype = o; + max_addr = !flags.max_addr; + } + +let get_max_otype () : Z.t = !flags.max_otype diff --git a/lib/parser.mly b/lib/parser.mly index 0b91469..436ce4e 100644 --- a/lib/parser.mly +++ b/lib/parser.mly @@ -1,30 +1,36 @@ %token EOF -%token PC STK CGP +%token PC STK CGP MTCC %token REG %token INT %token LABELDEF %token LABEL %token LPAREN RPAREN LSBRK RSBRK LCBRK RCBRK %token PLUS MINUS COMMA SHARP COLON -%token JMP JNZ MOVE LOAD STORE ADD SUB MUL REM DIV LT LEA RESTRICT SUBSEG +%token JALR JMP JNZ MOVESR MOVE LOAD STORE ADD SUB MUL REM DIV LT LEA RESTRICT SUBSEG %token GETL GETB GETE GETA GETP GETOTYPE GETWTYPE SEAL UNSEAL %token FAIL HALT %token LOCAL GLOBAL -%token O E RO RX RW RWX RWL RWLX +%token O E R X W WL SR DI DL %token SO S U SU %token Int Cap SealRange Sealed %left PLUS MINUS EXPR %left UMINUS %start main +%{ open! Ast %} %{ open! Ir %} %% main: | EOF; { ([]: Ir.t) } - | JMP; r = reg; p = main; { Jmp r :: p } - | JNZ; r1 = reg; r2 = reg; p = main; { Jnz (r1, r2) :: p } + + | JALR; r1 = reg; r2 = reg; p = main; { Jalr (r1,r2) :: p } + | JMP; c = reg_const; p = main; { Jmp c :: p } + | JNZ; r = reg; c = reg_const; p = main; { Jnz (r, c) :: p } + + | MOVESR; r = reg; c = reg_const; p = main; { MoveSR (r, c) :: p } + | MOVE; r = reg; c = reg_const; p = main; { Move (r, c) :: p } | LOAD; r1 = reg; r2 = reg; p = main; { Load (r1, r2) :: p } | STORE; r = reg; c = reg_const; p = main; { Store (r, c) :: p } @@ -37,6 +43,7 @@ main: | LEA; r = reg; c = reg_const; p = main; { Lea (r, c) :: p } | RESTRICT; r = reg; c = reg_const; p = main; { Restrict (r, c) :: p } | SUBSEG; r = reg; c1 = reg_const; c2 = reg_const; p = main; { SubSeg (r, c1, c2) :: p } + | GETL; r1 = reg; r2 = reg; p = main; { GetL (r1, r2) :: p } | GETB; r1 = reg; r2 = reg; p = main; { GetB (r1, r2) :: p } | GETE; r1 = reg; r2 = reg; p = main; { GetE (r1, r2) :: p } @@ -44,10 +51,13 @@ main: | GETP; r1 = reg; r2 = reg; p = main; { GetP (r1, r2) :: p } | GETOTYPE; r1 = reg; r2 = reg; p = main; { GetOType (r1, r2) :: p } | GETWTYPE; r1 = reg; r2 = reg; p = main; { GetWType (r1, r2) :: p } + | SEAL; r1 = reg; r2 = reg; r3 = reg; p = main; { Seal (r1, r2, r3) :: p } | UNSEAL; r1 = reg; r2 = reg; r3 = reg; p = main; { UnSeal (r1, r2, r3) :: p } + | FAIL; p = main; { Fail :: p } | HALT; p = main; { Halt :: p } + | lbl = LABELDEF; p = main; { Lbl lbl :: p } | SHARP ; w = word_def; p = main { Word w :: p } @@ -70,6 +80,7 @@ reg: | PC; { PC } | STK; { stk } | CGP; { cgp } + | MTCC; { mtcc } | i = REG; { Reg i } reg_const: @@ -92,21 +103,29 @@ wtype: | Int ; { W_I } | Cap ; { W_Cap } | SealRange ; { W_SealRange } - | Sealed ; { W_Sealed } + | Sealed ; { Ast.W_Sealed } locality: | LOCAL; { Local } | GLOBAL; { Global } +perm_enc: + | E; { E: Perm.t } + | R; { R: Perm.t } + | X; { X: Perm.t } + | W; { W: Perm.t } + | WL; { WL: Perm.t } + | SR; { SR: Perm.t } + | DL; { DL: Perm.t } + | DI; { DI: Perm.t } + perm: - | O; { O } - | E; { E } - | RO; { RO } - | RX; { RX } - | RW; { RW } - | RWX; { RWX } - | RWL; { RWL } - | RWLX; { RWLX } + | O; { PermSet.empty } + | p = perm_enc; { PermSet.singleton p } + | LSBRK; p = perm_list ; RSBRK ; { p } +perm_list: + | p = perm_enc; { PermSet.singleton p } + | p = perm_enc ; tl = perm_list { PermSet.add p tl } expr: | LPAREN; e = expr; RPAREN { e } diff --git a/lib/parser_regfile.mly b/lib/parser_regfile.mly index bc390aa..5f2ddec 100644 --- a/lib/parser_regfile.mly +++ b/lib/parser_regfile.mly @@ -1,17 +1,18 @@ %token EOF -%token PC CGP STK +%token PC CGP STK MTCC %token REG %token INT -%token MAX_ADDR STK_ADDR +%token MAX_ADDR %token LPAREN RPAREN LSBRK RSBRK LCBRK RCBRK -%token PLUS MINUS AFFECT COMMA COLON -%token O E RO RX RW RWX RWL RWLX +%token PLUS MINUS AFFECT COMMA COLON UNDERSCORE +%token O E R X W WL SR DI DL %token SO S U SU %token LOCAL GLOBAL %left PLUS MINUS EXPR %left UMINUS %start main +%{ open! Ast %} %{ open! Irreg %} %% @@ -24,6 +25,7 @@ reg: | PC; { PC } | CGP; { CGP } | STK; { STK } + | MTCC; { MTCC } | i = REG; { Reg i } word: @@ -52,19 +54,21 @@ seal_perm: | SU; { (true, true) } perm: - | O; { O } - | E; { E } - | RO; { RO } - | RX; { RX } - | RW; { RW } - | RWX; { RWX } - | RWL; { RWL } - | RWLX; { RWLX } + | O; { PermSet.empty } + | p = perm_enc; UNDERSCORE ; np = perm ; { PermSet.add p np } +perm_enc: + | E; { E: Perm.t } + | R; { R: Perm.t } + | X; { X: Perm.t } + | W; { W: Perm.t } + | WL; { WL: Perm.t } + | SR; { SR: Perm.t } + | DL; { DL: Perm.t } + | DI; { DI: Perm.t } expr: | LPAREN; e = expr; RPAREN { e } | MAX_ADDR { MaxAddr } - | STK_ADDR { StkAddr } | e1 = expr; PLUS; e2 = expr { AddOp (e1,e2) } | e1 = expr; MINUS; e2 = expr { SubOp (e1,e2) } | MINUS; e = expr %prec UMINUS { SubOp (IntLit (Z.of_int 0),e) } diff --git a/lib/pretty_printer.ml b/lib/pretty_printer.ml index de29d44..6f2cb4d 100644 --- a/lib/pretty_printer.ml +++ b/lib/pretty_printer.ml @@ -14,16 +14,24 @@ let string_of_regname (r : regname) : string = let string_of_seal_perm (p : seal_perm) : string = match p with false, false -> "SO" | true, false -> "S" | false, true -> "U" | true, true -> "SU" -let string_of_perm (p : perm) : string = +let string_of_perm (p : Perm.t) : string = match p with - | O -> "O" | E -> "E" - | RO -> "RO" - | RX -> "RX" - | RW -> "RW" - | RWX -> "RWX" - | RWL -> "RWL" - | RWLX -> "RWLX" + | R -> "R" + | X -> "X" + | W -> "W" + | WL -> "WL" + | SR -> "SR" + | DL -> "DL" + | DI -> "DI" + +let string_of_fperm (fp : PermSet.t) : string = + if fp = PermSet.empty + then "O" + else + let l = List.sort Perm.compare (PermSet.fold (fun p l -> p::l) fp []) in + let s = List.fold_left (fun str p -> (string_of_perm p) ^ "_" ^ str) "" l in + String.sub s 0 (String.length s - 1) let string_of_locality (g : locality) : string = match g with Local -> "Local" | Global -> "Global" @@ -42,7 +50,7 @@ let string_of_reg_or_const_restrict (c : reg_or_const) : string = try if dec_type = Encode._PERM_LOC_ENC then let p, g = Encode.perm_loc_pair_decoding dec_z in - "(" ^ string_of_perm p ^ "," ^- string_of_locality g ^ ")" + "(" ^ string_of_fperm p ^ "," ^- string_of_locality g ^ ")" else if dec_type = Encode._SEAL_LOC_ENC then let p, g = Encode.seal_perm_loc_pair_decoding dec_z in "(" ^ string_of_seal_perm p ^ "," ^- string_of_locality g ^ ")" @@ -65,8 +73,10 @@ let string_of_machine_op (s : machine_op) : string = (* string_of_regname r1 ^- string_of_regname r2 ^- string_of_reg_or_const c *) in match s with - | Jmp r -> "jmp" ^- string_of_regname r - | Jnz (r1, r2) -> "jnz" ^- string_of_rr r1 r2 + | Jalr (r1, r2) -> "jalr" ^- string_of_rr r1 r2 + | Jmp c -> "jmp" ^- string_of_reg_or_const c + | Jnz (r, c) -> "jnz" ^- string_of_rc r c + | MoveSR (r, c) -> "movSR" ^- string_of_rc r c | Move (r, c) -> "mov" ^- string_of_rc r c | Load (r1, r2) -> "load" ^- string_of_rr r1 r2 | Store (r, c) -> "store" ^- string_of_rc r c @@ -96,7 +106,7 @@ let string_of_machine_op (s : machine_op) : string = let string_of_sealable (sb : sealable) : string = match sb with | Cap (p, g, b, e, a) -> - Printf.sprintf "Cap (%s, %s, %s, %s, %s)" (string_of_perm p) (string_of_locality g) + Printf.sprintf "Cap (%s, %s, %s, %s, %s)" (string_of_fperm p) (string_of_locality g) (Z.to_string b) (Z.to_string e) (Z.to_string a) | SealRange (p, g, b, e, a) -> Printf.sprintf "SRange [%s, %s, %s, %s, %s]" (string_of_seal_perm p) (string_of_locality g) @@ -111,7 +121,7 @@ let string_of_word (w : word) : string = let string_of_ast_sealable (sb : Ast.sealable) : string = match sb with | Ast.Cap (p, g, b, e, a) -> - Printf.sprintf "Cap (%s, %s, %s, %s, %s)" (string_of_perm p) (string_of_locality g) + Printf.sprintf "Cap (%s, %s, %s, %s, %s)" (string_of_fperm p) (string_of_locality g) (Z.to_string b) (Z.to_string e) (Z.to_string a) | Ast.SealRange (p, g, b, e, a) -> Printf.sprintf "SRange [%s, %s, %s, %s, %s]" (string_of_seal_perm p) (string_of_locality g) diff --git a/lib/program.ml b/lib/program.ml index 6fa9147..e5b7787 100644 --- a/lib/program.ml +++ b/lib/program.ml @@ -9,13 +9,13 @@ let parse_prog (filename : string) : (Ast.t, string) Result.t = close_in input; Result.Error "Parsing Failed" -let parse_regfile (filename : string) (stk_addr : Z.t) : +let parse_regfile (filename : string) : (Ast.word Machine.RegMap.t, string) Result.t = let input = open_in filename in try let filebuf = Lexing.from_channel input in let parse_res = Irreg.translate_regfile @@ Parser_regfile.main Lexer_regfile.token filebuf in - let parse_regfile = parse_res !Parameters.flags.max_addr stk_addr in + let parse_regfile = parse_res (Parameters.get_max_addr ()) in close_in input; Result.Ok parse_regfile with Failure _ -> diff --git a/src/interpreter.ml b/src/interpreter.ml index 3bc24de..44d912c 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -18,10 +18,10 @@ let () = (* Parse initial register file *) let regfile = - let init_regfile = Machine.init_reg_state stk_addr in + let init_regfile = Machine.init_reg_state in if regfile_name = "" then init_regfile else - match Program.parse_regfile regfile_name stk_addr with + match Program.parse_regfile regfile_name with | Ok regs -> (Machine.RegMap.fold (fun r w rf -> Machine.RegMap.add r w rf) regs) init_regfile | Error msg -> Printf.eprintf "Regfile parse error: %s\n" msg; diff --git a/tests/test_files/default/neg/bad_flow1.s b/tests/test_files/default/neg/bad_flow1.s index 371eb94..30f9104 100644 --- a/tests/test_files/default/neg/bad_flow1.s +++ b/tests/test_files/default/neg/bad_flow1.s @@ -1,4 +1,4 @@ mov r1 pc restrict r1 (E, GLOBAL) - restrict r1 (RWX, GLOBAL) ; FAIL: attempt to flow from E to RWX + restrict r1 ([R W X], GLOBAL) ; FAIL: attempt to flow from E to RWX halt diff --git a/tests/test_files/default/neg/bad_flow3.s b/tests/test_files/default/neg/bad_flow3.s index baf6bad..6ee5c10 100644 --- a/tests/test_files/default/neg/bad_flow3.s +++ b/tests/test_files/default/neg/bad_flow3.s @@ -1,2 +1,2 @@ - restrict r0 (RO, GLOBAL) ; FAIL: attempt to restrict a SealRange with a Regular permission + restrict r0 (R, GLOBAL) ; FAIL: attempt to restrict a SealRange with a Regular permission halt diff --git a/tests/test_files/default/neg/bad_flow_WL.s b/tests/test_files/default/neg/bad_flow_WL.s index 7738cba..0dc8a45 100644 --- a/tests/test_files/default/neg/bad_flow_WL.s +++ b/tests/test_files/default/neg/bad_flow_WL.s @@ -1,4 +1,4 @@ - mov r1 pc - restrict r1 (RW, GLOBAL) - restrict r1 (RWL, GLOBAL) + mov r1 cgp + restrict r1 ([R W], GLOBAL) + restrict r1 ([R W WL], GLOBAL) halt diff --git a/tests/test_files/default/neg/bad_flow_locality.s b/tests/test_files/default/neg/bad_flow_locality.s index 8c8aec3..06a8040 100644 --- a/tests/test_files/default/neg/bad_flow_locality.s +++ b/tests/test_files/default/neg/bad_flow_locality.s @@ -1,5 +1,5 @@ - mov r1 pc + mov r1 cgp ;; Cannot restrict Local to Global - restrict r1 (RWX, LOCAL) - restrict r1 (RWX, GLOBAL) + restrict r1 ([R W], LOCAL) + restrict r1 ([R W], GLOBAL) halt diff --git a/tests/test_files/default/pos/jmper.s b/tests/test_files/default/pos/jmper.s index f19994d..f41a0e9 100644 --- a/tests/test_files/default/pos/jmper.s +++ b/tests/test_files/default/pos/jmper.s @@ -1,6 +1,4 @@ - mov r1 pc - lea r1 5 - restrict r1 (E, GLOBAL) + mov r1 2 jmp r1 fail add r2 5 7 diff --git a/tests/test_files/default/pos/jmper_jalr.s b/tests/test_files/default/pos/jmper_jalr.s new file mode 100644 index 0000000..c033898 --- /dev/null +++ b/tests/test_files/default/pos/jmper_jalr.s @@ -0,0 +1,7 @@ + mov r1 pc + lea r1 5 + restrict r1 (E, GLOBAL) + jalr r0 r1 + fail + add r2 5 7 + halt diff --git a/tests/test_files/default/pos/mov_test.s b/tests/test_files/default/pos/mov_test.s index 7e3ea60..c1079e0 100644 --- a/tests/test_files/default/pos/mov_test.s +++ b/tests/test_files/default/pos/mov_test.s @@ -1,3 +1,14 @@ mov r2 28 mov r5 -30 + mov r30 O + mov r30 R + mov r30 X + mov r30 W + mov r30 WL + mov r30 SR + mov r30 DL + mov r30 DI + mov r30 [ R X ] + mov r30 [ R W WL SR ] + mov r30 Local halt diff --git a/tests/test_files/default/pos/sealing_counter.s b/tests/test_files/default/pos/sealing_counter.s index 567f209..04c7a3d 100644 --- a/tests/test_files/default/pos/sealing_counter.s +++ b/tests/test_files/default/pos/sealing_counter.s @@ -21,45 +21,34 @@ init: lea r0 (main+1-init) ; r0 = (RWX, init, end, main+1) subseg r0 main data ; r0 = (RWX, main, data, main+1) restrict r0 (E, Global) ; r0 = (E, main, data, main+1) - jmp r0 ; jump to main main + jalr r0 r0 ; jump to main main main: ;; r0 = pc / r1 = {0: (RO, counter, counter+1, counter)} - #(RO, Global, linking_table, end, linking_table) + #(R, Global, linking_table, end, linking_table) ;; prepare the sentry for get and incr in r30 and r31 mov r0 pc lea r0 (-1) ; r0 = (RX, main, data, main+1) - load r31 r0 ; r30 = (RO, linking_table, end, linking_table) - load r30 r31 ; r30 = #(E, get, incr, get+1) - lea r31 1 - load r31 r31 ; r31 = #(E, incr, end, incr+1) + load r29 r0 ; r30 = (RO, linking_table, end, linking_table) + load r30 r29 ; r30 = #(E, get, incr, get+1) + lea r29 1 + load r29 r29 ; r29 = #(E, incr, end, incr+1) ;; call get - mov r0 pc - lea r0 3 ; r0 = callback - jmp r30 ; call get + jalr r0 r30 ; call get ;; call incr 3 times - mov r0 pc - lea r0 3 ; r0 = callback - jmp r31 ; call incr - mov r0 pc - lea r0 3 ; r0 = callback - jmp r31 ; call incr - mov r0 pc - lea r0 3 ; r0 = callback - jmp r31 ; call incr - mov r0 pc + jalr r0 r29 ; call incr + jalr r0 r29 ; call incr + jalr r0 r29 ; call incr ;; call get - mov r0 pc - lea r0 3 ; r0 = callback - jmp r30 ; call get + jalr r0 r30 ; call incr halt data: - #{0: (RW, Global, counter, counter+1, counter)} + #{0: ([R W], Global, counter, counter+1, counter)} linking_table: #(E, Global, get, incr, get+1) ; get #(E, Global, incr, end, incr+2) ; incr @@ -76,15 +65,15 @@ get: ; check whether the otype matches with the actual value unseal r2 r2 r1 ; r2 = (RO, counter, counter+1, counter) load r2 r2 ; r2 = val_counter sub r3 r2 r3 ; r3 = val_counter - ot - mov r2 pc - lea r2 5 ; prepare jump to the fail instruction - jnz r2 r3 ; if r3 != 0, then fail, else return + ;; mov r2 pc + ;; lea r2 5 ; prepare jump to the fail instruction + jnz r3 3 ; if r3 != 0, then fail, else return getotype r2 r1 ; Case r3 = 0, then get_value and jmp to callback - jmp r0 ; r2 contains the return value + jalr r0 r0 ; r2 contains the return value fail ; Case r3 != 0, then fail incr: #[SU, Global, 0, 10, 0] - #(RW, Global, incr, incr+1, incr) + #([R W], Global, incr, incr+1, incr) ;; r0 contains callback / r1 = {ot: (RO, counter, counter+1, counter)} mov r2 pc ; r2 = (RX, incr, end, incr+2) lea r2 (-2) ; r2 = (RX, incr, end, incr) @@ -101,5 +90,5 @@ incr: mov r2 0 mov r3 0 mov r4 0 - jmp r0 + jalr r0 r0 end: diff --git a/tests/test_files/default/pos/test1.s b/tests/test_files/default/pos/test1.s deleted file mode 100644 index a959f84..0000000 --- a/tests/test_files/default/pos/test1.s +++ /dev/null @@ -1,27 +0,0 @@ - ;; Init - mov r1 pc ; r1 = (RWX, init, end, init) 0 - lea r1 20 ; r1 = (RWX, init, end, data) 1 - mov r2 r1 ; r2 = (RWX, init, end, data) 2 - lea r2 1 ; r2 = (RWX, init, end, data+1) 3 - store r2 2 ; mem[data+1] <- 2 4 - store r1 r2 ; mem[data] <- (RWX, init, end, data+1) 5 - lea r1 (-9) ; r1 = (RWX, init, end, code) 6 - subseg r1 11 21 ; r1 = (RWX, code, end, code) 7 - restrict r1 (E, LOCAL) ; r1 = (E, code, end, code) 8 - mov r2 0 ; r2 = 0 9 - jmp r1 ; jump to unknown code: we only give it access 10 - - ;; Code - mov r1 pc ; r1 = (RX, code, end, code) 11 - lea r1 9 ; r1 = (RX, code, end, data) 12 - load r1 r1 ; r1 = (RWX, init, end, data+1) 13 - load r2 r1 ; r2 = 14 - add r2 r2 1 ; r2 = +1 15 - store r1 r2 ; mem[data+1] <- +1 16 - load r0 r1 ; r0 = mem[data+1] 17 - mov r1 0 ; r1 = 0 18 - halt ; return to unknown code 19 - - ;; Data - mov r5 r5 ; 20 - mov r5 0 ; 21 diff --git a/tests/test_files/default/pos/test1_labels.s b/tests/test_files/default/pos/test1_labels.s index aaa69e5..4cc77d9 100644 --- a/tests/test_files/default/pos/test1_labels.s +++ b/tests/test_files/default/pos/test1_labels.s @@ -1,29 +1,32 @@ init: - mov r1 pc ; r1 = (RWX, init, end, init) 0 - lea r1 (data-init) ; r1 = (RWX, init, end, data) 1 - mov r2 r1 ; r2 = (RWX, init, end, data) 2 - lea r2 1 ; r2 = (RWX, init, end, data+1) 3 - store r2 2 ; mem[data+1] <- 2 4 - store r1 r2 ; mem[data] <- (RWX, init, end, data+1) 5 - lea r1 (code-data) ; r1 = (RWX, init, end, code) 6 - subseg r1 code end ; r1 = (RWX, code, end, code) 7 - restrict r1 (E, GLOBAL) ; r1 = (E, code, end, code) 8 - mov r2 0 ; r2 = 0 9 - jmp r1 ; jump to unknown code: we only give it access 10 + mov r3 pc ; r3 = (RX, init, end, init) 0 + mov r1 cgp ; r1 = (RWL, init, end, init) 1 + lea r1 (data-init) ; r1 = (RWL, init, end, data) 2 + mov r2 r1 ; r2 = (RWL, init, end, data) 3 + lea r2 1 ; r2 = (RWL, init, end, data+1) 4 + store r2 2 ; mem[data+1] <- 2 5 + store r1 r2 ; mem[data] <- (RWL, init, end, data+1) 6 + lea r3 (code-init) ; r3 = (RX, init, end, code) 7 + subseg r3 code end ; r3 = (RX, code, end, code) 8 + restrict r3 (E, GLOBAL) ; r3 = (E, code, end, code) 9 + mov r2 0 ; r2 = 0 10 + mov r1 0 ; r1 = 0 11 + jalr r2 r3 ; jump to unknown code: + ; we only give it access 12 code: - mov r1 pc ; r1 = (RX, code, end, code) 11 - lea r1 (data-code) ; r1 = (RX, code, end, data) 12 - load r1 r1 ; r1 = (RWX, init, end, data+1) 13 - load r2 r1 ; r2 = 14 - add r2 r2 1 ; r2 = +1 15 - store r1 r2 ; mem[data+1] <- +1 16 - load r0 r1 ; r0 = mem[data+1] 17 - mov r1 0 ; r1 = 0 18 - halt ; return to unknown code 19 + mov r1 pc ; r1 = (RX, code, end, code) 13 + lea r1 (data-code) ; r1 = (RX, code, end, data) 14 + load r1 r1 ; r1 = (RWX, init, end, data+1) 15 + load r2 r1 ; r2 = 16 + add r2 r2 1 ; r2 = +1 17 + store r1 r2 ; mem[data+1] <- +1 18 + load r0 r1 ; r0 = mem[data+1] 19 + mov r1 0 ; r1 = 0 20 + halt ; return to unknown code 21 data: - mov r5 r5 ; 20 - mov r5 0 ; 21 + mov r5 r5 ; 22 + mov r5 0 ; 23 end: diff --git a/tests/test_files/default/pos/test_locality_flow.s b/tests/test_files/default/pos/test_locality_flow.s index 8edb57a..5f65e84 100644 --- a/tests/test_files/default/pos/test_locality_flow.s +++ b/tests/test_files/default/pos/test_locality_flow.s @@ -1,9 +1,9 @@ code: mov r0 pc ; r0 Global - restrict r0 (RWX, GLOBAL) ; Global can be restricted to global - restrict r0 (RWX, LOCAL) ; Global can be restricted to local - restrict r0 (RWX, LOCAL) ; Local can be restricted to local + restrict r0 ([R X SR], GLOBAL) ; Global can be restricted to global + restrict r0 ([R X SR], LOCAL) ; Global can be restricted to local + restrict r0 ([R X SR], LOCAL) ; Local can be restricted to local halt data: diff --git a/tests/tester.ml b/tests/tester.ml index cbe06e3..74e2e7f 100644 --- a/tests/tester.ml +++ b/tests/tester.ml @@ -14,7 +14,7 @@ let state_tst = (fun a b -> a = b) let perm_tst = - Alcotest.testable (Fmt.of_to_string @@ Pretty_printer.string_of_perm) (fun a b -> a = b) + Alcotest.testable (Fmt.of_to_string @@ Pretty_printer.string_of_fperm) (fun a b -> PermSet.equal a b) (* TODO I should add a try/catch in case of parsing failure *) (* TODO also test multiple flags configurations *) @@ -26,8 +26,7 @@ let run_prog (filename : string) : mchn = let _ = Parameters.flags := Parameters.griotte in - let stk_addr = Z.(Parameters.get_max_addr () / ~$2) in - let init_regs = Machine.init_reg_state stk_addr in + let init_regs = Machine.init_reg_state in let init_mems = Machine.init_mem_state Z.(~$0) parse_res in let m = Machine.init init_regs init_mems in @@ -40,7 +39,7 @@ let test_perm expected actual _ = Alcotest.(check perm_tst) "Permission match" e let get_reg_int_word (r : Ast.regname) (m : mchn) (d : Z.t) = match r @! snd m with I z -> z | _ -> d -let get_reg_cap_perm (r : regname) (m : mchn) (d : perm) = +let get_reg_cap_perm (r : regname) (m : mchn) (d : PermSet.t) = match r @! snd m with Sealable (Cap (p, _, _, _, _)) -> p | _ -> d let test_path s = "../../../tests/test_files/default/" ^ s @@ -68,8 +67,8 @@ let test_mov_test = let r5_res = match Reg 5 @! snd m with I z -> z | _ -> Z.zero in [ test_case "mov_test.s should end in halted state" `Quick (test_state Halted (fst m)); - test_case "mov_test.s PC should point to address 2" `Quick (fun _ -> - check int "Ints match" 2 (Z.to_int pc_a)); + test_case "mov_test.s PC should point to address 13" `Quick (fun _ -> + check int "Ints match" 13 (Z.to_int pc_a)); test_case "mov_test.s R2 should contain 28" `Quick (test_const_word Z.(~$28) r2_res); test_case "mov_test.s R5 should contain -30" `Quick (test_const_word Z.(~$(-30)) r5_res); ] @@ -81,8 +80,17 @@ let test_jmper = test_case "jmper.s should end in halted state" `Quick (test_state Halted (fst m)); test_case "jmper.s should end with r2 containing 12" `Quick (test_const_word Z.(~$12) (get_reg_int_word (Ast.Reg 2) m Z.zero)); - test_case "jmper.s should contain E permission in r1" `Quick - (test_perm E (get_reg_cap_perm (Reg 1) m O)); + ] + +let test_jmper_jalr = + let open Alcotest in + let m = run_prog (test_path "pos/jmper_jalr.s") in + [ + test_case "jmper_jalr.s should end in halted state" `Quick (test_state Halted (fst m)); + test_case "jmper_jalr.s should end with r2 containing 12" `Quick + (test_const_word Z.(~$12) (get_reg_int_word (Ast.Reg 2) m Z.zero)); + test_case "jmper_jalr.s should contain E permission in r1" `Quick + (test_perm (PermSet.singleton E) (get_reg_cap_perm (Reg 1) m PermSet.empty)); ] let test_locality_flow = @@ -140,8 +148,9 @@ let () = [ ( "Pos", test_mov_test - @ test_jmper @ test_locality_flow - @ test_getotype @ test_getwtype @ test_sealing @ test_sealing_counter + @ test_jmper @ test_jmper_jalr @ test_locality_flow + @ test_getotype @ test_getwtype @ test_sealing + @ test_sealing_counter ); ("Neg", test_negatives); ] diff --git a/tests/tests.ml b/tests/tests.ml index aa3ae88..3dd487d 100644 --- a/tests/tests.ml +++ b/tests/tests.ml @@ -34,18 +34,22 @@ let encode_seal_loc p g = Const (Encode.encode_seal_perm_loc_pair p g) (* TODO add test cases for mul/rem/div *) let instr_tests = [ - ("jmp pc", Op (Jmp PC)); - ("jmp r0", Op (Jmp (Reg 0))); - ("jnz r1 r2", Op (Jnz (Reg 1, Reg 2))); + ("jmp r0", Op (Jmp (Register (Reg 0)))); + ("jmp 2", Op (Jmp (Const (Z.of_int 2)))); + ("jnz r1 r2", Op (Jnz (Reg 1, (Register (Reg 2))))); + ("jnz r1 5", Op (Jnz (Reg 1, Const (Z.of_int 5)))); + ("jalr r13 r2", Op (Jalr (Reg 13, Reg 2))); ("mov pc 25", Op (Move (PC, const 25))); ("mov r3 -25", Op (Move (Reg 3, const (-25)))); ("mov r30 stk", Op (Move (Reg 30, Register stk))); - ("mov r30 RW", Op (Move (Reg 30, encode_perm RW))); + ("mov r30 [R W]", Op (Move (Reg 30, encode_perm (PermSet.of_list [R;W])))); ("mov r30 U", Op (Move (Reg 30, encode_seal_perm (false, true)))); ("mov r3 Sealed", Op (Move (Reg 3, encode_wtype W_Sealed))); ("mov r13 SealRange", Op (Move (Reg 13, encode_wtype W_SealRange))); ("mov r23 Cap", Op (Move (Reg 23, encode_wtype W_Cap))); ("mov r30 Int", Op (Move (Reg 30, encode_wtype W_I))); + ("movSR r31 0", Op (MoveSR (Reg 31, Const Z.zero))); + ("movSR r31 r24", Op (MoveSR (Reg 31, Register (Reg 24)))); ("load r4 r5", Op (Load (Reg 4, Reg 5))); ("store r6 r7", Op (Store (Reg 6, Register (Reg 7)))); ("add r8 (10-15) (-37)", Op (Add (Reg 8, const (-5), const (-37)))); @@ -53,8 +57,9 @@ let instr_tests = ("sub r8 r8 Global", Op (Sub (Reg 8, Register (Reg 8), encode_locality Global))); ("lt r10 496 8128 ; perfect numbers are cool!", Op (Lt (Reg 10, const 496, const 8128))); ("lea r11 r12", Op (Lea (Reg 11, Register (Reg 12)))); - ("restrict r13 (RX, Global)", Op (Restrict (Reg 13, encode_perm_loc RX Global))); - ("restrict r13 (RWL, LOCAL)", Op (Restrict (Reg 13, encode_perm_loc RWL Local))); + ("restrict r13 ([R X], Global)", Op (Restrict (Reg 13, encode_perm_loc (PermSet.of_list [R;X]) Global))); + ("restrict r13 ([R WL DL], LOCAL)", Op (Restrict (Reg 13, encode_perm_loc (PermSet.of_list [R;WL;DL]) Local))); + ("restrict r13 (O, Local)", Op (Restrict (Reg 13, encode_perm_loc PermSet.empty Local))); ("restrict r14 (S, GLOBAL)", Op (Restrict (Reg 14, encode_seal_loc (true, false) Global))); ("subseg r15 pc r16", Op (SubSeg (Reg 15, Register PC, Register (Reg 16)))); ("getl r21 r17", Op (GetL (Reg 21, Reg 17))); @@ -127,69 +132,76 @@ let make_enc_dec_stm_tests (stm, test_name) = (* TODO add test cases for mul/rem/div *) let test_enc_dec_stm_list = [ - (Jmp PC, "encode-decode Jmp PC"); - (Jmp (Reg 28), "encode-decode Jmp R28"); - (Jnz (Reg 6, Reg 28), "encode-decode Jnz R6 R28"); + (Jmp (Register PC), "encode-decode Jmp PC"); + (Jmp (Register (Reg 28)), "encode-decode Jmp R28"); + (Jmp (Const Z.one), "encode-decode Jmp 1"); + (Jnz (Reg 6, (Register (Reg 28))), "encode-decode Jnz R6 R28"); + (Jnz (Reg 6, (Const Z.one)), "encode-decode Jnz R6 1"); + (Jalr (Reg 6, (Reg 22)), "encode-decode Jalr R6 R22"); + (MoveSR (mtcc, Const (Z.of_int 42)), "encode-decode MoveSR mtcc 42"); + (MoveSR (Reg 7, Register mtcc), "encode-decode MoveSR R7 mtcc"); (Move (PC, Register (Reg 7)), "encode-decode Move PC R7"); (Move (PC, const (-35)), "encode-decode Move PC (-35)"); - (Move (PC, encode_perm_loc E Global), "encode-decode Move PC (E, Global)"); + (Move (PC, encode_perm_loc (PermSet.singleton E) Global), "encode-decode Move PC (E, Global)"); + (Move (Reg 30, encode_perm_loc (PermSet.of_list [R;X]) Global), "encode-decode Move R30 (RX, Global)"); (Move (PC, encode_seal_loc (false, true) Local), "encode-decode Move PC (U,Local)"); (Move (PC, encode_wtype W_Cap), "encode-decode Move PC Cap"); - (Move (PC, encode_perm RWX), "encode-decode Move PC RWX"); + (Move (PC, encode_perm (PermSet.of_list [R;W;DI])), "encode-decode Move PC R_W_DI"); (Move (PC, encode_seal_perm (true, false)), "encode-decode Move PC U"); (Move (Reg 0, Register stk), "encode-decode Move R0 stk"); (Load (Reg 9, PC), "encode-decode Load R9 PC"); (Store (PC, Register (Reg 7)), "encode-decode Store PC R7"); (Store (PC, const (-35)), "encode-decode Store PC (-35)"); - (Store (PC, encode_perm_loc E Global), "encode-decode Store PC (E, Global)"); + (Store (PC, encode_perm_loc (PermSet.singleton E) Global), "encode-decode Store PC (E, Global)"); (Add (Reg 5, Register (Reg 6), Register PC), "encode-decode Add R5 R6 PC"); (Add (Reg 5, Register (Reg 6), const 8128), "encode-decode Add R5 R6 8128"); - ( Add (Reg 5, Register (Reg 6), encode_perm_loc RO Global), + ( Add (Reg 5, Register (Reg 6), encode_perm_loc (PermSet.singleton R) Global), "encode-decode Add R5 R6 (RO, Global)" ); (Add (Reg 5, const (-549), Register PC), "encode-decode Add R5 (-549) PC"); (Add (Reg 5, const 102, const 8128), "encode-decode Add R5 102 8128"); - (Add (Reg 5, const 83, encode_perm_loc RO Global), "encode-decode Add R5 83 (RO, Global)"); - (Add (Reg 5, encode_perm_loc E Global, Register PC), "encode-decode Add R5 E PC"); - (Add (Reg 5, encode_perm_loc O Global, const 8128), "encode-decode Add R5 O 8128"); - ( Add (Reg 5, encode_perm_loc RWX Global, encode_perm_loc RO Global), - "encode-decode Add R5 RWX (RO, Global)" ); + (Add (Reg 5, const 83, encode_perm_loc (PermSet.singleton R) Global), "encode-decode Add R5 83 (RO, Global)"); + (Add (Reg 5, encode_perm_loc (PermSet.singleton E) Global, Register PC), "encode-decode Add R5 E PC"); + (Add (Reg 5, encode_perm_loc PermSet.empty Global, const 8128), "encode-decode Add R5 O 8128"); + ( Add (Reg 5, encode_perm_loc (PermSet.of_list [R;W]) Global, encode_perm_loc (PermSet.singleton R) Global), + "encode-decode Add R5 RW (RO, Global)" ); (Sub (Reg 5, Register (Reg 6), Register PC), "encode-decode Sub R5 R6 PC"); (Sub (Reg 5, Register (Reg 6), const 8128), "encode-decode Sub R5 R6 8128"); - (Sub (Reg 5, Register (Reg 6), encode_perm_loc RO Global), "encode-decode Sub R5 R6 RO"); + (Sub (Reg 5, Register (Reg 6), encode_perm_loc (PermSet.singleton R) Global), "encode-decode Sub R5 R6 RO"); (Sub (Reg 5, const (-549), Register PC), "encode-decode Sub R5 (-549) PC"); (Sub (Reg 5, const 102, const 8128), "encode-decode Sub R5 102 8128"); - (Sub (Reg 5, const 83, encode_perm_loc RO Global), "encode-decode Sub R5 83 RO"); - (Sub (Reg 5, encode_perm_loc E Global, Register PC), "encode-decode Sub R5 E PC"); - (Sub (Reg 5, encode_perm_loc O Global, const 8128), "encode-decode Sub R5 O 8128"); - ( Sub (Reg 5, encode_perm_loc RWX Global, encode_perm_loc RO Global), - "encode-decode Sub R5 RWX RO" ); + (Sub (Reg 5, const 83, encode_perm_loc (PermSet.singleton R) Global), "encode-decode Sub R5 83 RO"); + (Sub (Reg 5, encode_perm_loc (PermSet.singleton E) Global, Register PC), "encode-decode Sub R5 E PC"); + (Sub (Reg 5, encode_perm_loc PermSet.empty Global, const 8128), "encode-decode Sub R5 O 8128"); + ( Sub (Reg 5, encode_perm_loc (PermSet.of_list [R;W]) Global, encode_perm_loc (PermSet.singleton R) Global), + "encode-decode Sub R5 RW RO" ); (Lt (Reg 5, Register (Reg 6), Register PC), "encode-decode Lt R5 R6 PC"); (Lt (Reg 5, Register (Reg 6), const 8128), "encode-decode Lt R5 R6 8128"); - (Lt (Reg 5, Register (Reg 6), encode_perm_loc RO Global), "encode-decode Lt R5 R6 RO"); + (Lt (Reg 5, Register (Reg 6), encode_perm_loc (PermSet.singleton R) Global), "encode-decode Lt R5 R6 RO"); (Lt (Reg 5, const (-549), Register PC), "encode-decode Lt R5 (-549) PC"); (Lt (Reg 5, const 102, const 8128), "encode-decode Lt R5 102 8128"); - (Lt (Reg 5, const 83, encode_perm_loc RO Global), "encode-decode Lt R5 83 RO"); - (Lt (Reg 5, encode_perm_loc E Global, Register PC), "encode-decode Lt R5 E PC"); - (Lt (Reg 5, encode_perm_loc O Global, const 8128), "encode-decode Lt R5 O 8128"); - (Lt (Reg 5, encode_perm_loc RWX Global, encode_perm_loc RO Global), "encode-decode Lt R5 RWX RO"); + (Lt (Reg 5, const 83, encode_perm_loc (PermSet.singleton R) Global), "encode-decode Lt R5 83 RO"); + (Lt (Reg 5, encode_perm_loc (PermSet.singleton E) Global, Register PC), "encode-decode Lt R5 E PC"); + (Lt (Reg 5, encode_perm_loc PermSet.empty Global, const 8128), "encode-decode Lt R5 O 8128"); + (Lt (Reg 5, encode_perm_loc (PermSet.of_list [R;W]) Global, encode_perm_loc (PermSet.singleton R) Global), "encode-decode Lt R5 RW RO"); (Lea (PC, Register (Reg 7)), "encode-decode Lea PC R7"); (Lea (PC, const (-35)), "encode-decode Lea PC (-35)"); - (Lea (PC, encode_perm_loc E Global), "encode-decode Lea PC E"); + (Lea (PC, encode_perm_loc (PermSet.singleton E) Global), "encode-decode Lea PC E"); (Restrict (PC, Register (Reg 7)), "encode-decode Restrict PC R7"); (Restrict (PC, const (-35)), "encode-decode Restrict PC (-35)"); - (Restrict (PC, encode_perm_loc E Global), "encode-decode Restrict PC E"); - (Restrict (Reg 30, encode_perm_loc RWL Global), "encode-decode Restrict R30 RWL Global"); - (Restrict (Reg 30, encode_perm_loc RWL Local), "encode-decode Restrict R30 RWL Local"); + (Restrict (PC, encode_perm_loc (PermSet.singleton E) Global), "encode-decode Restrict PC E"); + (Restrict (Reg 30, encode_perm_loc (PermSet.of_list [R;W;WL]) Global), "encode-decode Restrict R30 RWL Global"); + (Restrict (Reg 30, encode_perm_loc (PermSet.of_list [X;R]) Local), "encode-decode Restrict R30 RX Local"); + (Restrict (Reg 30, encode_perm_loc (PermSet.of_list [X;R]) Local), "encode-decode Restrict R30 RX Local"); (SubSeg (Reg 5, Register (Reg 6), Register PC), "encode-decode SubSeg R5 R6 PC"); (SubSeg (Reg 5, Register (Reg 6), const 8128), "encode-decode SubSeg R5 R6 8128"); - (SubSeg (Reg 5, Register (Reg 6), encode_perm_loc RO Global), "encode-decode SubSeg R5 R6 RO"); + (SubSeg (Reg 5, Register (Reg 6), encode_perm_loc (PermSet.singleton R) Global), "encode-decode SubSeg R5 R6 RO"); (SubSeg (Reg 5, const (-549), Register PC), "encode-decode SubSeg R5 (-549) PC"); (SubSeg (Reg 5, const 102, const 8128), "encode-decode SubSeg R5 102 8128"); - (SubSeg (Reg 5, const 83, encode_perm_loc RO Global), "encode-decode SubSeg R5 83 RO"); - (SubSeg (Reg 5, encode_perm_loc E Global, Register PC), "encode-decode SubSeg R5 E PC"); - (SubSeg (Reg 5, encode_perm_loc O Global, const 8128), "encode-decode SubSeg R5 O 8128"); - ( SubSeg (Reg 5, encode_perm_loc RWX Global, encode_perm_loc RO Global), - "encode-decode SubSeg R5 RWX RO" ); + (SubSeg (Reg 5, const 83, encode_perm_loc (PermSet.singleton R) Global), "encode-decode SubSeg R5 83 RO"); + (SubSeg (Reg 5, encode_perm_loc (PermSet.singleton E) Global, Register PC), "encode-decode SubSeg R5 E PC"); + (SubSeg (Reg 5, encode_perm_loc PermSet.empty Global, const 8128), "encode-decode SubSeg R5 O 8128"); + ( SubSeg (Reg 5, encode_perm_loc (PermSet.of_list [R;W]) Global, encode_perm_loc (PermSet.singleton R) Global), + "encode-decode SubSeg R5 RW RO" ); (GetB (Reg 6, Reg 31), "encode-decode GetB R6 R31"); (GetE (Reg 7, Reg 30), "encode-decode GetE R7 R30"); (GetA (Reg 8, Reg 29), "encode-decode GetA R8 R29"); @@ -219,3 +231,4 @@ let () = :: List.map test_encode_decode_int_bulk test_int_pair_list ); ("Encode/Decode Statement", List.map make_enc_dec_stm_tests test_enc_dec_stm_list); ] + ;