Add logical binary operations, and re-encode switcher's entry points

lib/ast.ml

@@ -67,6 +67,10 @@ type machine_op =
   | 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
+  | LAnd of regname * reg_or_const * reg_or_const
+  | LOr of regname * reg_or_const * reg_or_const
+  | LShiftL of regname * reg_or_const * reg_or_const
+  | LShiftR 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

lib/encode.ml

@@ -383,6 +383,22 @@ let encode_machine_op (s : machine_op) : Z.t =
       ~$0x34 ^! encode_int_int (encode_reg r1) (encode_int_int (encode_reg r2) (encode_reg r3))
   | Fail -> ~$0x35
   | Halt -> ~$0x36
+  | LAnd (r, c1, c2) ->
+      (* 0x37, 0x38, 0x39, 0x3a *)
+      let opc, c_enc = two_const_convert ~$0x37 c1 c2 in
+      opc ^! encode_int_int (encode_reg r) c_enc
+  | LOr (r, c1, c2) ->
+      (* 0x3b, 0x3c, 0x3d, 0x3e *)
+      let opc, c_enc = two_const_convert ~$0x3b c1 c2 in
+      opc ^! encode_int_int (encode_reg r) c_enc
+  | LShiftL (r, c1, c2) ->
+      (* 0x3f, 0x40, 0x41, 0x42 *)
+      let opc, c_enc = two_const_convert ~$0x3f c1 c2 in
+      opc ^! encode_int_int (encode_reg r) c_enc
+  | LShiftR (r, c1, c2) ->
+      (* 0x43, 0x44, 0x45, 0x46 *)
+      let opc, c_enc = two_const_convert ~$0x43 c1 c2 in
+      opc ^! encode_int_int (encode_reg r) c_enc
 
 let decode_machine_op (i : Z.t) : machine_op =
   (* let dec_perm = *)
@@ -593,6 +609,38 @@ let decode_machine_op (i : Z.t) : machine_op =
     UnSeal (r1, r2, r3)
   else if (* Fail *) opc = ~$0x35 then Fail
   else if (* Halt *) opc = ~$0x36 then Halt
+  else if (* LAnd *)
+          ~$0x37 <= opc && opc <= ~$0x3a 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 = ~$0x37 || opc = ~$0x38 then Register (decode_reg c1_enc) else Const c1_enc in
+    let c2 = if opc = ~$0x37 || opc = ~$0x39 then Register (decode_reg c2_enc) else Const c2_enc in
+    LAnd (r, c1, c2)
+  else if (* LOr *)
+          ~$0x3b <= opc && opc <= ~$0x3e 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 = ~$0x3b || opc = ~$0x3c then Register (decode_reg c1_enc) else Const c1_enc in
+    let c2 = if opc = ~$0x3b || opc = ~$0x3d then Register (decode_reg c2_enc) else Const c2_enc in
+    LOr (r, c1, c2)
+  else if (* LShiftL *)
+          ~$0x3f <= opc && opc <= ~$0x42 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 = ~$0x3f || opc = ~$0x40 then Register (decode_reg c1_enc) else Const c1_enc in
+    let c2 = if opc = ~$0x3f || opc = ~$0x41 then Register (decode_reg c2_enc) else Const c2_enc in
+    LShiftL (r, c1, c2)
+  else if (* LShiftR *)
+          ~$0x43 <= opc && opc <= ~$0x47 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 = ~$0x43 || opc = ~$0x44 then Register (decode_reg c1_enc) else Const c1_enc in
+    let c2 = if opc = ~$0x43 || opc = ~$0x45 then Register (decode_reg c2_enc) else Const c2_enc in
+    LShiftR (r, c1, c2)
   else
     raise
     @@ DecodeException

lib/ir.ml

@@ -12,6 +12,10 @@ type expr =
   | AddOp of expr * expr
   | SubOp of expr * expr
   | MultOp of expr * expr
+  | LandOp of expr * expr
+  | LorOp of expr * expr
+  | LslOp of expr * expr
+  | LsrOp of expr * expr
 
 type perm = Ast.perm
 type locality = Ast.locality
@@ -51,6 +55,10 @@ type machine_op =
   | 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
+  | LAnd of regname * reg_or_const * reg_or_const
+  | LOr of regname * reg_or_const * reg_or_const
+  | LShiftL of regname * reg_or_const * reg_or_const
+  | LShiftR 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
@@ -80,15 +88,24 @@ let rec compute_env (i : int) (prog : t) (envr : env) : env =
   | _ :: p -> compute_env (i + 1) p envr
 
 let rec eval_expr (envr : env) (e : expr) : Z.t =
+  let binop_eval (binop : Z.t -> Z.t -> Z.t) ( e1 : expr ) ( e2 : expr ) : Z.t =
+    binop (eval_expr envr e1) (eval_expr envr e2)
+  in
+  let lshiftl (z1 : Z.t) (z2 : Z.t) : Z.t = Z.of_int ((Z.to_int z1) lsl (Z.to_int z2)) in
+  let lshiftr (z1 : Z.t) (z2 : Z.t) : Z.t = Z.of_int ((Z.to_int z1) lsr (Z.to_int z2)) in
   match e with
   | IntLit i -> i
   | Label s -> (
       match List.find_opt (fun p -> fst p = s) envr with
       | Some (_, i) -> Z.of_int i
       | None -> raise (UnknownLabelException s))
-  | AddOp (e1, e2) -> Z.(eval_expr envr e1 + eval_expr envr e2)
-  | SubOp (e1, e2) -> Z.(eval_expr envr e1 - eval_expr envr e2)
-  | MultOp (e1, e2) -> Z.(eval_expr envr e1 * eval_expr envr e2)
+  | AddOp (e1, e2) -> binop_eval Z.(+) e1 e2
+  | SubOp (e1, e2) -> binop_eval Z.(-) e1 e2
+  | MultOp (e1, e2) -> binop_eval Z.( * ) e1 e2
+  | LandOp (e1, e2) -> binop_eval Z.(land) e1 e2
+  | LorOp (e1, e2) -> binop_eval Z.(lor) e1 e2
+  | LslOp (e1, e2) -> binop_eval lshiftl e1 e2
+  | LsrOp (e1, e2) -> binop_eval lshiftr e1 e2
 
 let translate_perm (p : perm) : Ast.perm = p
 let translate_locality (g : locality) : Ast.locality = g
@@ -152,6 +169,14 @@ let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op =
       Ast.Rem (translate_regname r, translate_reg_or_const envr c1, translate_reg_or_const envr c2)
   | Div (r, c1, c2) ->
       Ast.Div (translate_regname r, translate_reg_or_const envr c1, translate_reg_or_const envr c2)
+  | LAnd (r, c1, c2) ->
+      Ast.LAnd (translate_regname r, translate_reg_or_const envr c1, translate_reg_or_const envr c2)
+  | LOr (r, c1, c2) ->
+      Ast.LOr (translate_regname r, translate_reg_or_const envr c1, translate_reg_or_const envr c2)
+  | LShiftL (r, c1, c2) ->
+      Ast.LShiftL (translate_regname r, translate_reg_or_const envr c1, translate_reg_or_const envr c2)
+  | LShiftR (r, c1, c2) ->
+      Ast.LShiftR (translate_regname r, translate_reg_or_const envr c1, translate_reg_or_const envr c2)
   | Lt (r, c1, c2) ->
       Ast.Lt (translate_regname r, translate_reg_or_const envr c1, translate_reg_or_const envr c2)
   | Lea (r, c) -> Ast.Lea (translate_regname r, translate_reg_or_const envr c)

lib/irreg.ml

@@ -8,6 +8,10 @@ type expr =
   | AddOp of expr * expr
   | SubOp of expr * expr
   | MultOp of expr * expr
+  | LandOp of expr * expr
+  | LorOp of expr * expr
+  | LslOp of expr * expr
+  | LsrOp of expr * expr
   | MaxAddr
 
 type perm = Ast.perm
@@ -24,12 +28,27 @@ type sregfile_t = (Ast.sregname * word) list
 type t = regfile_t * sregfile_t
 
 let rec eval_expr (e : expr) (max_addr : Z.t) : Z.t =
+  let binop_eval (binop : Z.t -> Z.t -> Z.t) ( e1 : expr ) ( e2 : expr ) : Z.t =
+    binop (eval_expr e1 max_addr) (eval_expr e2 max_addr)
+  in
+  let lshiftl (z1 : Z.t) (z2 : Z.t) : Z.t =
+    print_string (Z.to_string z1 ^ "\n");
+    print_newline;
+    print_string (Z.to_string z2 ^ "\n");
+    print_newline;
+    print_string (Z.to_string (Z.of_int ((Z.to_int z1) lsl (Z.to_int z2))) ^ "\n");
+    Z.of_int ((Z.to_int z1) lsl (Z.to_int z2)) in
+  let lshiftr (z1 : Z.t) (z2 : Z.t) : Z.t = Z.of_int ((Z.to_int z1) lsr (Z.to_int z2)) in
   match e with
   | IntLit i -> i
   | MaxAddr -> max_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)
-  | MultOp (e1, e2) -> Z.(eval_expr e1 max_addr * eval_expr e2 max_addr)
+  | AddOp (e1, e2) -> binop_eval Z.(+) e1 e2
+  | SubOp (e1, e2) -> binop_eval Z.(-) e1 e2
+  | MultOp (e1, e2) -> binop_eval Z.( * ) e1 e2
+  | LandOp (e1, e2) -> binop_eval Z.(land) e1 e2
+  | LorOp (e1, e2) -> binop_eval Z.(lor) e1 e2
+  | LslOp (e1, e2) -> binop_eval lshiftl e1 e2
+  | LsrOp (e1, e2) -> binop_eval lshiftr e1 e2
 
 let translate_perm (p : perm) : Ast.perm = p
 let translate_locality (g : locality) : Ast.locality = g

lib/lexer.mll

@@ -82,6 +82,10 @@ rule token = parse
 | "rem" { REM }
 | "div" { DIV }
 | "lt" { LT }
+| "land" { LAND }
+| "lor" { LOR }
+| "lshiftl" { LSHIFTL }
+| "lshiftr" { LSHIFTR }
 | "lea" { LEA }
 | "restrict" { RESTRICT }
 | "subseg" { SUBSEG }
@@ -111,6 +115,10 @@ rule token = parse
 | ',' { COMMA }
 | ':' { COLON }
 | '#' { SHARP }
+| "&&" { LANDOP }
+| "||" { LOROP }
+| "<<" { LSL }
+| ">>" { LSR }
 
 (* locality *)
 | "LOCAL"    | "Local" { LOCAL }

lib/lexer_regfile.mll

@@ -85,6 +85,10 @@ rule token = parse
 | ',' { COMMA }
 | ':' { COLON }
 | ":=" { AFFECT }
+| "&&" { LANDOP }
+| "||" { LOROP }
+| "<<" { LSL }
+| ">>" { LSR }
 
 (* locality *)
 | "LOCAL"    | "Local" { LOCAL }

lib/machine.ml

@@ -298,6 +298,9 @@ let load_word (p : perm) (w : word) : word =
 let authorised_access_system_register (conf : exec_conf) : bool =
   match PC @! conf with Sealable (Cap ((XSR, _, _, _), _, _, _, _)) -> true | _ -> false
 
+let lshiftl (z1 : Z.t) (z2 : Z.t) : Z.t = Z.of_int ((Z.to_int z1) lsl (Z.to_int z2))
+let lshiftr (z1 : Z.t) (z2 : Z.t) : Z.t = Z.of_int ((Z.to_int z1) lsr (Z.to_int z2))
+
 (* NOTE Although we've already check that not supported instructions / capabilities *)
 (*  are not in the initial machine, we still need to make sure that *)
 (*  the user does not encode not supported instructions *)
@@ -466,6 +469,22 @@ let exec_single (conf : exec_conf) : mchn =
             | 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)
+        | LAnd (r, c1, c2) -> (
+            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 land z2)) conf) | _ -> fail_state)
+        | LOr (r, c1, c2) -> (
+            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 lor z2)) conf) | _ -> fail_state)
+        | LShiftL (r, c1, c2) -> (
+            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 (lshiftl z1 z2)) conf) | _ -> fail_state)
+        | LShiftR (r, c1, c2) -> (
+            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 (lshiftr z1 z2)) conf) | _ -> fail_state)
         | GetL (r1, r2) -> (
             match r2 @! conf with
             | Sealable sb | Sealed (_, sb) ->

lib/parser.mly

@@ -8,15 +8,16 @@
 %token <string> LABELDEF
 %token <string> LABEL
 %token LPAREN RPAREN LSBRK RSBRK LCBRK RCBRK
-%token PLUS MINUS MULT COMMA SHARP COLON
+%token PLUS MINUS MULT COMMA SHARP COLON LANDOP LOROP LSL LSR
 %token JALR JMP JNZ READSR WRITESR MOVE LOAD STORE ADD SUB MUL REM DIV LT LEA RESTRICT SUBSEG
+%token LAND LOR LSHIFTL LSHIFTR
 %token GETL GETB GETE GETA GETP GETOTYPE GETWTYPE SEAL UNSEAL
 %token FAIL HALT
 %token LOCAL GLOBAL
 %token O Orx R X XSR Ow W WL DL LG DRO LM
 %token SO S U SU
 %token Int Cap SealRange Sealed
-%left PLUS MINUS MULT EXPR
+%left PLUS MINUS MULT EXPR LANDOP LOROP LSL LSR
 %left UMINUS
 
 %start <Ir.t> main
@@ -44,6 +45,10 @@ main:
   | REM; r = reg; c1 = reg_const; c2 = reg_const; p = main; { Rem (r, c1, c2) :: p }
   | DIV; r = reg; c1 = reg_const; c2 = reg_const; p = main; { Div (r, c1, c2) :: p }
   | LT; r = reg; c1 = reg_const; c2 = reg_const; p = main; { Lt (r, c1, c2) :: p }
+  | LAND; r = reg; c1 = reg_const; c2 = reg_const; p = main; { LAnd (r, c1, c2) :: p }
+  | LOR; r = reg; c1 = reg_const; c2 = reg_const; p = main; { LOr (r, c1, c2) :: p }
+  | LSHIFTL; r = reg; c1 = reg_const; c2 = reg_const; p = main; { LShiftL (r, c1, c2) :: p }
+  | LSHIFTR; r = reg; c1 = reg_const; c2 = reg_const; p = main; { LShiftR (r, c1, c2) :: p }
   | 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 }
@@ -177,6 +182,10 @@ expr:
   | e1 = expr; PLUS; e2 = expr { AddOp (e1,e2) }
   | e1 = expr; MINUS; e2 = expr { SubOp (e1,e2) }
   | e1 = expr; MULT; e2 = expr { MultOp (e1,e2) }
+  | e1 = expr; LANDOP; e2 = expr { LandOp (e1,e2) }
+  | e1 = expr; LOROP; e2 = expr { LorOp (e1,e2) }
+  | e1 = expr; LSL; e2 = expr { LslOp (e1,e2) }
+  | e1 = expr; LSR; e2 = expr { LsrOp (e1,e2) }
   | MINUS; e = expr %prec UMINUS { SubOp (IntLit (Z.of_int 0),e) }
   | i = INT { IntLit (Z.of_int i) }
   | lbl = LABEL { Label lbl }

lib/parser_regfile.mly

@@ -7,11 +7,11 @@
 %token <int> INT
 %token MAX_ADDR
 %token LPAREN RPAREN LSBRK RSBRK LCBRK RCBRK
-%token PLUS MINUS MULT AFFECT COMMA COLON
+%token PLUS MINUS MULT AFFECT COMMA COLON LANDOP LOROP LSL LSR
 %token O Orx R X XSR Ow W WL DL LG DRO LM
 %token SO S U SU
 %token LOCAL GLOBAL
-%left PLUS MINUS MULT EXPR
+%left PLUS MINUS MULT EXPR LANDOP LOROP LSL LSR
 %left UMINUS
 
 %start <Irreg.t> main
@@ -122,6 +122,10 @@ expr:
   | e1 = expr; PLUS; e2 = expr { AddOp (e1,e2) }
   | e1 = expr; MINUS; e2 = expr { SubOp (e1,e2) }
   | e1 = expr; MULT; e2 = expr { MultOp (e1,e2) }
+  | e1 = expr; LANDOP; e2 = expr { LandOp (e1,e2) }
+  | e1 = expr; LOROP; e2 = expr { LorOp (e1,e2) }
+  | e1 = expr; LSL; e2 = expr { LslOp (e1,e2) }
+  | e1 = expr; LSR; e2 = expr { LsrOp (e1,e2) }
   | MINUS; e = expr %prec UMINUS { SubOp (IntLit (Z.of_int 0),e) }
   | i = INT { IntLit (Z.of_int i) }
 

lib/pretty_printer.ml

@@ -83,6 +83,10 @@ let string_of_machine_op (s : machine_op) : string =
   | Mul (r, c1, c2) -> "mul" ^- string_of_rcc r c1 c2
   | Rem (r, c1, c2) -> "rem" ^- string_of_rcc r c1 c2
   | Div (r, c1, c2) -> "div" ^- string_of_rcc r c1 c2
+  | LAnd (r, c1, c2) -> "land" ^- string_of_rcc r c1 c2
+  | LOr (r, c1, c2) -> "lor" ^- string_of_rcc r c1 c2
+  | LShiftL (r, c1, c2) -> "lshiftl" ^- string_of_rcc r c1 c2
+  | LShiftR (r, c1, c2) -> "lshiftr" ^- string_of_rcc r c1 c2
   | Lt (r, c1, c2) -> "lt" ^- string_of_rcc r c1 c2
   | Lea (r, c) -> "lea" ^- string_of_rc r c
   (* NOTE Restrict is a special case, because we know that we are supposed to restrict with a

tests/test_files/case_studies/mutually_distrustful.s

@@ -109,24 +109,25 @@ C_data_end:
 ;; export table compartment A -> does not export any entry points
 A_ext:
     #([X Ow LG LM], Global, A, A_end, A)                 ; PCC
-    #([R W LG LM], Global, A_data, A_data_end, A_data)  ; CGP
+    #([R W LG LM], Global, A_data, A_data_end, A_data)   ; CGP
 A_ext_end:
 
 ;; export table compartment B -> exports B_f
 B_ext:
     #([X Ow LG LM], Global, B, B_end, B)                 ; PCC
-    #([R W LG LM], Global, B_data, B_data_end, B_data)  ; CGP
-B_ext_f: #(10 * (B_f - B) + 1)                    ; offset_f
-B_ext_h: #(10 * (B_f - B) + 0)                    ; offset_h
+    #([R W LG LM], Global, B_data, B_data_end, B_data)   ; CGP
+B_ext_f: #(((B_f - B) << 3) || 1)                         ; offset_f
+B_ext_h: #(((B_h - B) << 3) || 0)                         ; offset_h
 B_ext_end:
 
 ;; export table compartment C -> exports C_g
 C_ext:
     #([X Ow LG LM], Global, C, C_end, C)                 ; PCC
-    #([R W LG LM], Global, C_data, C_data_end, C_data)  ; CGP
-C_ext_g: #(10 * (C_g - C) + 0)                    ; offset_g
+    #([R W LG LM], Global, C_data, C_data_end, C_data)   ; CGP
+C_ext_g: #(((C_g - C) << 3) || 0)                         ; offset_g
 C_ext_end:
 
+
 ;; Concatenate this file at the end of any example that require the switcher
 switcher:
     #[SU, Global, 9, 10, 9]
@@ -174,9 +175,8 @@ switcher_zero_stk_end_pre:
     load cs0 cs0
     unseal ct1 cs0 ct1
     load cs0 ct1
-    rem ct2 cs0 10
-    sub cs0 cs0 ct2
-    div cs0 cs0 10
+    land ct2 cs0 7
+    lshiftr cs0 cs0 3
     getb cgp ct1
     geta cs1 ct1
     sub cs1 cgp cs1

tests/test_files/switcher/switcher.s

@@ -46,9 +46,8 @@ switcher_zero_stk_end_pre:
     load cs0 cs0
     unseal ct1 cs0 ct1
     load cs0 ct1
-    rem ct2 cs0 10
-    sub cs0 cs0 ct2
-    div cs0 cs0 10
+    land ct2 cs0 7
+    lshiftr cs0 cs0 3
     getb cgp ct1
     geta cs1 ct1
     sub cs1 cgp cs1