From a57daa376a6c15d09ca85738f8c71d867f6fe84f Mon Sep 17 00:00:00 2001 From: Bastien Rousseau Date: Thu, 13 Jun 2024 14:19:30 +0200 Subject: [PATCH] Replace E-perm by reserved sealed otype --- lib/ast.ml | 3 +- lib/encode.ml | 34 +++++++-------- lib/lexer.mll | 1 - lib/lexer_regfile.mll | 1 - lib/machine.ml | 43 +++++++++++++------ lib/parser.mly | 3 +- lib/parser_regfile.mly | 3 +- lib/pretty_printer.ml | 1 - tests/test_files/default/neg/bad_flow1.s | 4 +- tests/test_files/default/neg/bad_flow2.s | 2 +- .../default/neg/lea_perm_not_entry.s | 4 -- tests/test_files/default/pos/jmper_jalr.s | 2 +- tests/test_files/default/pos/seal_unseal.s | 1 + .../test_files/default/pos/sealing_counter.s | 26 +++++------ tests/test_files/default/pos/test1_labels.s | 3 +- tests/tester.ml | 18 ++++---- tests/tests.ml | 12 ------ 17 files changed, 78 insertions(+), 83 deletions(-) delete mode 100644 tests/test_files/default/neg/lea_perm_not_entry.s diff --git a/lib/ast.ml b/lib/ast.ml index 7dca603..f359b2a 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -7,7 +7,6 @@ let mtdc = Reg 31 module Perm = struct type t = - | E (* sentry --- sealed value with otype 1, 2 or 3 *) | R (* read --- LG, MC and LD *) | X (* execute --- EX *) | W (* write --- LM, MC and SD *) @@ -21,7 +20,7 @@ module Perm = struct 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 + match p with R -> 0 | X -> 1 | W -> 2 | WL -> 3 | SR -> 4 | DL -> 5 | DI -> 6 in weight p2 - weight p1 end diff --git a/lib/encode.ml b/lib/encode.ml index edbe1f4..fd5aec4 100644 --- a/lib/encode.ml +++ b/lib/encode.ml @@ -87,14 +87,13 @@ let perm_encoding (p : Perm.t) : Z.t = Z.of_int @@ match p with - | E -> 0b10000000 - | R -> 0b01000000 - | X -> 0b00100000 - | W -> 0b00010000 - | WL -> 0b00001000 - | SR -> 0b00000100 - | DL -> 0b00000010 - | DI -> 0b00000001 + | R -> 0b1000000 + | X -> 0b0100000 + | W -> 0b0010000 + | WL -> 0b0001000 + | SR -> 0b0000100 + | DL -> 0b0000010 + | DI -> 0b0000001 let fperm_encoding (fp : PermSet.t) : Z.t = PermSet.fold (fun p res -> Z.logor (perm_encoding p) res) fp (Z.of_int 0b0) @@ -103,18 +102,17 @@ let perm_decoding (i : Z.t) : Perm.t = let dec_perm_exception _ = raise @@ DecodeException "Error decoding permission: unexpected encoding" in - if Z.(i > of_int 0b11111111) then dec_perm_exception () + if Z.(i > of_int 0b1111111) then dec_perm_exception () else 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 + match (b 6, b 5, b 4, b 3, b 2, b 1, b 0) with + | true, false, false, false, false, false, false -> R + | false, true, false, false, false, false, false -> X + | false, false, true, false, false, false, false -> W + | false, false, false, true, false, false, false -> WL + | false, false, false, false, true, false, false -> SR + | false, false, false, false, false, true, false -> DL + | false, false, false, false, false, false, true -> DI | _ -> dec_perm_exception () let fperm_decoding (i : Z.t) : PermSet.t = diff --git a/lib/lexer.mll b/lib/lexer.mll index 98d3db6..bbfe12a 100644 --- a/lib/lexer.mll +++ b/lib/lexer.mll @@ -81,7 +81,6 @@ rule token = parse (* permissions *) | 'O' { O } -| 'E' { E } | 'R' { R } | 'X' { X } | 'W' { W } diff --git a/lib/lexer_regfile.mll b/lib/lexer_regfile.mll index 6768d6e..304a1bb 100644 --- a/lib/lexer_regfile.mll +++ b/lib/lexer_regfile.mll @@ -54,7 +54,6 @@ rule token = parse (* permissions *) | 'O' { O } -| 'E' { E } | 'R' { R } | 'X' { X } | 'W' { W } diff --git a/lib/machine.ml b/lib/machine.ml index e8c25fd..a2ab966 100644 --- a/lib/machine.ml +++ b/lib/machine.ml @@ -26,6 +26,8 @@ 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 otype_sentry : Z.t = Z.zero + let get_perm (w : Ast.word) : Ast.PermSet.t = match w with | I _ -> Ast.PermSet.empty @@ -34,16 +36,24 @@ let get_perm (w : Ast.word) : Ast.PermSet.t = 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 +let is_sentry (w : Ast.word) : bool = + match w with + | Sealed (ot, Cap (_, _, _, _, _)) -> ot = otype_sentry + | _ -> false + let check_word_derived (w : Ast.word) : unit = + if is_sentry w + then + ( + if is_derived_from (get_perm w) arch_root_executable_perm + then () + else raise (CheckInitFailed w) + ) + else if is_derived_from (get_perm w) arch_root_executable_perm then () else if is_derived_from (get_perm w) arch_root_memory_perm then () else raise (CheckInitFailed w) @@ -165,8 +175,8 @@ let ( !> ) conf = upd_pc conf let upd_pc_perm (w : word) = 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)) + | Sealed ( ot, (Cap (p, g, b, e, a))) when ot = otype_sentry -> + Sealable (Cap (p, g, b, e, a)) | _ -> w let fetch_decode (conf : exec_conf) : machine_op option = @@ -252,9 +262,9 @@ let exec_single (conf : exec_conf) : mchn = | Halt -> (Halted, conf) | Jalr (r_dst, r_src) when (not (r_dst = mtdc)) && not (r_src = mtdc) -> ( match PC @! conf with - | Sealable (Cap (_, g, b, e, a)) -> + | Sealable (Cap (p, 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 + let link_cap = Sealed (otype_sentry, (Cap (p, g, b, e, Z.(a + Z.one)))) in (Running, upd_reg PC new_pc (upd_reg r_dst link_cap conf)) | _ -> fail_state) | Jmp c when not (c = Register mtdc) -> ( @@ -343,7 +353,7 @@ let exec_single (conf : exec_conf) : mchn = let w2 = get_word conf c2 in match (w1, w2) with | I z1, I z2 -> - if b <= z1 && Z.(~$0 <= z2) && Z.zero <= e && not (PermSet.mem E p) then + if b <= z1 && Z.(~$0 <= z2) && Z.zero <= e then let w = Sealable (Cap (p, g, z1, z2, a)) in !>(upd_reg r w conf) else fail_state @@ -364,8 +374,7 @@ let exec_single (conf : exec_conf) : mchn = | Sealable (Cap (p, g, b, e, a)) -> ( let w = get_word conf c in match w with - | I z when not (PermSet.mem E p) -> - !>(upd_reg r (Sealable (Cap (p, g, b, e, Z.(a + z)))) conf) + | I z -> !>(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 @@ -447,11 +456,19 @@ let exec_single (conf : exec_conf) : mchn = | Seal (dst, r1, r2) when (not (dst = mtdc)) && (not (r1 = mtdc)) && not (r2 = mtdc) -> ( match (r1 @! conf, r2 @! conf) with | Sealable (SealRange ((true, _), _, b, e, a)), Sealable sb when b <= a && a < e -> + if a = otype_sentry + then + (match sb with + | Cap (p,_,_,_,_) when PermSet.mem X p -> + !>(upd_reg dst (Sealed (a, sb)) conf) + | _ -> fail_state) + else !>(upd_reg dst (Sealed (a, sb)) conf) | _ -> fail_state) | UnSeal (dst, r1, r2) when (not (dst = mtdc)) && (not (r1 = mtdc)) && not (r2 = mtdc) -> ( match (r1 @! conf, r2 @! conf) with - | Sealable (SealRange ((_, true), _, b, e, a)), Sealed (a', sb) -> + | Sealable (SealRange ((_, true), _, b, e, a)), Sealed (a', sb) + when not (a = otype_sentry) -> if b <= a && a < e && a = a' then !>(upd_reg dst (Sealable sb) conf) else fail_state | _ -> fail_state) | _ -> fail_state) diff --git a/lib/parser.mly b/lib/parser.mly index 81712fc..aec0932 100644 --- a/lib/parser.mly +++ b/lib/parser.mly @@ -10,7 +10,7 @@ %token GETL GETB GETE GETA GETP GETOTYPE GETWTYPE SEAL UNSEAL %token FAIL HALT %token LOCAL GLOBAL -%token O E R X W WL SR DI DL +%token O R X W WL SR DI DL %token SO S U SU %token Int Cap SealRange Sealed %left PLUS MINUS EXPR @@ -110,7 +110,6 @@ locality: | GLOBAL; { Global } perm_enc: - | E; { E: Perm.t } | R; { R: Perm.t } | X; { X: Perm.t } | W; { W: Perm.t } diff --git a/lib/parser_regfile.mly b/lib/parser_regfile.mly index c08d257..9a6c376 100644 --- a/lib/parser_regfile.mly +++ b/lib/parser_regfile.mly @@ -5,7 +5,7 @@ %token MAX_ADDR %token LPAREN RPAREN LSBRK RSBRK LCBRK RCBRK %token PLUS MINUS AFFECT COMMA COLON -%token O E R X W WL SR DI DL +%token O R X W WL SR DI DL %token SO S U SU %token LOCAL GLOBAL %left PLUS MINUS EXPR @@ -54,7 +54,6 @@ seal_perm: | SU; { (true, true) } perm_enc: - | E; { E: Perm.t } | R; { R: Perm.t } | X; { X: Perm.t } | W; { W: Perm.t } diff --git a/lib/pretty_printer.ml b/lib/pretty_printer.ml index 8280948..0d2018b 100644 --- a/lib/pretty_printer.ml +++ b/lib/pretty_printer.ml @@ -17,7 +17,6 @@ let string_of_seal_perm (p : seal_perm) : string = let string_of_perm (p : Perm.t) : string = match p with - | E -> "E" | R -> "R" | X -> "X" | W -> "W" diff --git a/tests/test_files/default/neg/bad_flow1.s b/tests/test_files/default/neg/bad_flow1.s index 30f9104..ff35048 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 ([R W X], GLOBAL) ; FAIL: attempt to flow from E to RWX + seal r1 r0 r1 + unseal r1 r0 r1 ; FAIL: attempt to unseal a sentry halt diff --git a/tests/test_files/default/neg/bad_flow2.s b/tests/test_files/default/neg/bad_flow2.s index 7dbd149..f273587 100644 --- a/tests/test_files/default/neg/bad_flow2.s +++ b/tests/test_files/default/neg/bad_flow2.s @@ -1,4 +1,4 @@ mov r1 pc restrict r1 (O, GLOBAL) - restrict r1 (E, GLOBAL) ; FAIL: attempt to flow from O to E + seal r1 r0 r1 halt diff --git a/tests/test_files/default/neg/lea_perm_not_entry.s b/tests/test_files/default/neg/lea_perm_not_entry.s deleted file mode 100644 index 6bc5fba..0000000 --- a/tests/test_files/default/neg/lea_perm_not_entry.s +++ /dev/null @@ -1,4 +0,0 @@ - mov r1 pc - restrict r1 (E, GLOBAL) - lea r1 15 ; FAIL: attempt to modify the address of a E-capability - halt diff --git a/tests/test_files/default/pos/jmper_jalr.s b/tests/test_files/default/pos/jmper_jalr.s index c033898..84f50bb 100644 --- a/tests/test_files/default/pos/jmper_jalr.s +++ b/tests/test_files/default/pos/jmper_jalr.s @@ -1,6 +1,6 @@ mov r1 pc lea r1 5 - restrict r1 (E, GLOBAL) + seal r1 r0 r1 jalr r0 r1 fail add r2 5 7 diff --git a/tests/test_files/default/pos/seal_unseal.s b/tests/test_files/default/pos/seal_unseal.s index 5b8ebcd..bdc7bb7 100644 --- a/tests/test_files/default/pos/seal_unseal.s +++ b/tests/test_files/default/pos/seal_unseal.s @@ -1,4 +1,5 @@ subseg r0 0 2 + lea r0 1 mov r1 r0 restrict r0 (S, Global) restrict r1 (U, Global) diff --git a/tests/test_files/default/pos/sealing_counter.s b/tests/test_files/default/pos/sealing_counter.s index 04c7a3d..eef9fea 100644 --- a/tests/test_files/default/pos/sealing_counter.s +++ b/tests/test_files/default/pos/sealing_counter.s @@ -15,12 +15,11 @@ init: mov r0 pc ; r0 = (RWX, init, end, init) mov r1 r0 ; r1 = (RWX, init, end, init) lea r1 (data-init) ; r1 = (RWX, init, end, data) - load r1 r1 ; r1 = {0: (RO, counter, counter+1, counter)} + load r1 r1 ; r1 = {1: (RO, counter, counter+1, counter)} ;; prepare the main capability in r0 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) jalr r0 r0 ; jump to main main main: @@ -48,20 +47,23 @@ main: halt data: - #{0: ([R W], Global, counter, counter+1, counter)} + #{1: ([R W], Global, counter, counter+1, counter)} linking_table: - #(E, Global, get, incr, get+1) ; get - #(E, Global, incr, end, incr+2) ; incr + ;; #(E, Global, get, incr, get+1) ; get + ;; #(E, Global, incr, end, incr+2) ; incr + #{0: ([R X], Global, get, incr, get+1)} ; get + #{0: ([R X], Global, incr, end, incr+2)} ; incr counter: - #0 + #1 get: ; check whether the otype matches with the actual value - #[SU, Global, 0, 10, 0] + #[SU, Global, 1, 10, 1] ;; r0 contains callback / r1 = {ot: (RO, counter, counter+1, counter)} mov r2 pc ; r2 = (RX, get, incr, get+1) lea r2 (-1) ; r2 = (RX, get, incr, get) - load r2 r2 ; r2 = #[SU, 0, 10, 0] + load r2 r2 ; r2 = #[SU, 1, 10, 1] getotype r3 r1 ; r3 = ot - lea r2 r3 ; r2 = #[SU, 0, 10, ot] + lea r2 r3 ; r2 = #[SU, 1, 10, ot+1] + lea r2 -1 ; r2 = #[SU, 1, 10, ot] unseal r2 r2 r1 ; r2 = (RO, counter, counter+1, counter) load r2 r2 ; r2 = val_counter sub r3 r2 r3 ; r3 = val_counter - ot @@ -72,17 +74,17 @@ get: ; check whether the otype matches with the actual value jalr r0 r0 ; r2 contains the return value fail ; Case r3 != 0, then fail incr: - #[SU, Global, 0, 10, 0] + #[SU, Global, 1, 10, 1] #([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) - load r3 r2 ; r3 = #[SU, 0, 10, ot] + load r3 r2 ; r3 = #[SU, 1, 10, ot] unseal r1 r3 r1 ; r1 = (RO, counter, counter+1, counter) load r4 r1 ; r4 = val_counter add r4 r4 1 ; r4 = val_counter + 1 store r1 r4 ; stores new counter value - lea r3 1 ; r3 = #[SU, 0, 10, ot+1] + lea r3 1 ; r3 = #[SU, 1, 10, ot+1] lea r2 1 ; r2 = (RX, incr, end, incr+1) load r2 r2 ; r2 = (RW, incr, incr+1, incr) store r2 r3 ; stores new sealrange diff --git a/tests/test_files/default/pos/test1_labels.s b/tests/test_files/default/pos/test1_labels.s index 4cc77d9..72c8d3b 100644 --- a/tests/test_files/default/pos/test1_labels.s +++ b/tests/test_files/default/pos/test1_labels.s @@ -8,7 +8,8 @@ init: 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 + seal r3 r0 r3 ; r3 = {0: (RX, code, end, code)} 9 + ;; 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: diff --git a/tests/tester.ml b/tests/tester.ml index 3b36d0f..df36d91 100644 --- a/tests/tester.ml +++ b/tests/tester.ml @@ -97,8 +97,6 @@ let test_jmper_jalr = 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 = @@ -151,29 +149,29 @@ let test_getwtype = let open Alcotest in let m = run_prog (test_path "pos/get_wtype.s") in [ - test_case "get_otype.s should end in halted state" `Quick (test_state Halted (fst m)); - test_case "get_otype.s should end with r0 containing 0" `Quick + test_case "get_wtype.s should end in halted state" `Quick (test_state Halted (fst m)); + test_case "get_wtype.s should end with r0 containing 0" `Quick (test_const_word Z.zero (get_reg_int_word (Ast.Reg 0) m Z.zero)); - test_case "get_otype.s should end with r1 containing 0" `Quick + test_case "get_wtype.s should end with r1 containing 0" `Quick (test_const_word Z.zero (get_reg_int_word (Ast.Reg 1) m Z.zero)); - test_case "get_otype.s should end with r2 containing 0" `Quick + test_case "get_wtype.s should end with r2 containing 0" `Quick (test_const_word Z.zero (get_reg_int_word (Ast.Reg 2) m Z.zero)); - test_case "get_otype.s should end with r3 containing 0" `Quick + test_case "get_wtype.s should end with r3 containing 0" `Quick (test_const_word Z.zero (get_reg_int_word (Ast.Reg 3) m Z.zero)); ] let test_sealing = let open Alcotest in let m = run_prog (test_path "pos/seal_unseal.s") in - [ test_case "get_otype.s should end in halted state" `Quick (test_state Halted (fst m)) ] + [ test_case "seal_unseal.s should end in halted state" `Quick (test_state Halted (fst m)) ] let test_sealing_counter = let open Alcotest in let m = run_prog (test_path "pos/sealing_counter.s") in [ test_case "sealing_counter.s should end in halted state" `Quick (test_state Halted (fst m)); - test_case "sealing_counter.s should end with r2 containing 3" `Quick - (test_const_word Z.(~$3) (get_reg_int_word (Ast.Reg 2) m Z.zero)); + test_case "sealing_counter.s should end with r2 containing 4" `Quick + (test_const_word Z.(~$4) (get_reg_int_word (Ast.Reg 2) m Z.zero)); ] let () = diff --git a/tests/tests.ml b/tests/tests.ml index 37fed97..8f4df72 100644 --- a/tests/tests.ml +++ b/tests/tests.ml @@ -144,7 +144,6 @@ let test_enc_dec_stm_list = (MoveSR (Reg 7, Register mtdc), "encode-decode MoveSR R7 mtdc"); (Move (PC, Register (Reg 7)), "encode-decode Move PC R7"); (Move (PC, const (-35)), "encode-decode Move PC (-35)"); - (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)"); @@ -155,7 +154,6 @@ let test_enc_dec_stm_list = (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 (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 (PermSet.singleton R) Global), @@ -164,8 +162,6 @@ let test_enc_dec_stm_list = (Add (Reg 5, const 102, const 8128), "encode-decode Add R5 102 8128"); ( 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, @@ -180,8 +176,6 @@ let test_enc_dec_stm_list = (Sub (Reg 5, const 102, const 8128), "encode-decode Sub R5 102 8128"); ( 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, @@ -195,8 +189,6 @@ let test_enc_dec_stm_list = (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 (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, @@ -205,10 +197,8 @@ let test_enc_dec_stm_list = "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 (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 (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), @@ -223,8 +213,6 @@ let test_enc_dec_stm_list = (SubSeg (Reg 5, const 102, const 8128), "encode-decode SubSeg R5 102 8128"); ( 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