Support for plain values (expressions and capabilities) in assembly file

lib/ast.ml

@@ -4,6 +4,7 @@ type perm = O | E | RO | RX | RW | RWX | RWL | RWLX | URW | URWL | URWX | URWLX
 type locality = Global | Local | Directed
 type const_perm = Const of Z.t | Perm of perm * locality
 type reg_or_const = Register of regname | CP of const_perm (* TODO: separate into two types *)
+type word = I of Z.t | Cap of perm * locality * Z.t * Z.t * Z.t
 type machine_op
   =
   | Nop
@@ -29,7 +30,7 @@ type machine_op
   | PromoteU of regname
   | Fail
   | Halt
-type statement = machine_op (* TODO: PseudoOp and LabelDefs *)
+type statement = Op of machine_op | Word of word (* TODO: PseudoOp and LabelDefs *)
 
 type t = statement list
 

lib/call.ml

@@ -14,45 +14,45 @@ let all_registers : regname list =
 
 let rstk : regname = (Reg 0)
 
-let rec rclear (regs : regname list) : (statement list) =
+let rec rclear (regs : regname list) : (machine_op list) =
   match regs with
   | [] -> []
   | r::regs' -> (Move (r, const 0))::(rclear regs')
 
-let rclear_inv (regs : regname list) : statement list =
+let rclear_inv (regs : regname list) : machine_op list =
   (rclear (List.filter (fun r -> not (in_list r regs)) all_registers))
 
 let reg_diff (regs : regname list) : regname list=
   (List.filter (fun r -> not (in_list r regs)) all_registers)
 
 let push_instrs ps = List.map (fun p -> StoreU (rstk, const 0, p)) ps
 let pop_instrs r =
-  [Encode.encode_statement (LoadU (r,rstk, const (-1)));
-  Encode.encode_statement (Lea (rstk, const (-1)))]
+  [Encode.encode_machine_op (LoadU (r,rstk, const (-1)));
+  Encode.encode_machine_op (Lea (rstk, const (-1)))]
 
 let push_env =
   push_instrs (List.map (fun r -> Register r) (reg_diff [PC;rstk]))
 
 let pop_env =
   List.fold_left (fun b r -> (pop_instrs r) @ b) [] (reg_diff [PC;rstk])
 
-let call_prologue (rargs : regname list) : (statement list) =
+let call_prologue (rargs : regname list) : (machine_op list) =
   push_instrs [const 0]@
   push_env@
   push_instrs [Register rstk]@
   push_instrs
-    ((List.map (fun i -> CP (Const (Encode.encode_statement i)))
+    ((List.map (fun i -> CP (Const (Encode.encode_machine_op i)))
         [ Move (Reg 31, Register PC);
           Lea (Reg 31, const (-1));
           Load (rstk, Reg 31)])
      @ List.map (fun i -> CP (Const i)) pop_env
-     @ [CP (Const ((Encode.encode_statement (LoadU (PC, rstk, const (-1))))))])@
+     @ [CP (Const ((Encode.encode_machine_op (LoadU (PC, rstk, const (-1))))))])@
   [Move (Reg 31, Register PC);
    Lea (Reg 31, const (41+List.length rargs));
    StoreU (rstk, const (-99), Register (Reg 1))
   ]
 
-let scall (r : regname) (rargs : regname list) : statement list =
+let scall (r : regname) (rargs : regname list) : machine_op list =
   call_prologue rargs @
   [ Move (Reg 30, Register rstk);
     PromoteU (Reg 30);

lib/encode.ml

@@ -154,7 +154,7 @@ let decode_int (i : Z.t) : Z.t * Z.t =
 
 let (~$) = Z.(~$)
 
-let encode_statement (s : statement): Z.t =
+let encode_machine_op (s : machine_op): Z.t =
   let (^!) opcode args = Z.(opcode + (args lsl 8)) in
   let const_convert opcode c = begin
     match c with
@@ -228,7 +228,7 @@ let encode_statement (s : statement): Z.t =
   (* TODO I would prefer to have Nop encoded as 0 *)
   | Nop -> ~$0x48
 
-let decode_statement (i : Z.t) : statement =
+let decode_machine_op (i : Z.t) : machine_op =
   let dec_perm =
     fun c_enc -> let (p,g) = (decode_perm_pair c_enc) in Perm (p,g)
   in

lib/interactive_ui.ml

@@ -167,7 +167,7 @@ module MkUi (Cfg: MachineConfig) : Ui = struct
 
   module Instr = struct
     let ui (i: Ast.machine_op) =
-      I.string A.(fg green) (Pretty_printer.string_of_statement i)
+      I.string A.(fg green) (Pretty_printer.string_of_machine_op i)
   end
 
   module Program_panel = struct
@@ -195,7 +195,7 @@ module MkUi (Cfg: MachineConfig) : Ui = struct
     let img_instr in_range a w =
       (match w with
        | Machine.I z when in_range a <> `No ->
-         begin match Encode.decode_statement z with
+         begin match Encode.decode_machine_op z with
            | i -> Instr.ui i
            | exception Encode.DecodeException _ -> I.string A.(fg green) "???"
          end

lib/ir.ml

@@ -13,6 +13,9 @@ type perm = O | E | RO | RX | RW | RWX | RWL | RWLX | URW | URWL | URWX | URWLX
 type locality = Global | Local | Directed
 type const_perm = Const of expr | Perm of perm * locality
 type reg_or_const = Register of regname | CP of const_perm (* TODO: separate into two types *)
+type word = I of expr | Cap of perm * locality * expr * expr * expr
+exception WordException of word
+
 type machine_op
   =
   | Nop
@@ -39,6 +42,7 @@ type machine_op
   | Fail
   | Halt
   | Lbl of string
+  | Word of word
 type statement = machine_op (* TODO: PseudoOp and LabelDefs *)
 
 type t = statement list
@@ -98,6 +102,18 @@ let translate_reg_or_const (envr : env) (roc : reg_or_const) : Ast.reg_or_const
   | Register r -> Ast.Register (translate_regname r)
   | CP cp -> Ast.CP (translate_const_perm envr cp)
 
+let translate_word (envr : env) (w : word) : Ast.statement =
+  match w with
+  | I e -> Ast.Word (Ast.I (eval_expr envr e))
+  | Cap (p,l,b,e,a) ->
+    Ast.Word (Ast.Cap
+                ((translate_perm p),
+                 (translate_locality l),
+                 (eval_expr envr b),
+                 (eval_expr envr e),
+                 (eval_expr envr a)
+                ))
+
 let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op =
   match instr with
   | Jmp r -> Ast.Jmp (translate_regname r)
@@ -139,13 +155,15 @@ let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op =
   | Fail -> Ast.Fail
   | Halt -> Ast.Halt
   | Nop -> Ast.Nop
+  | Word w -> raise (WordException w)
   | Lbl s -> raise (UnknownLabelException s)
 
 let rec translate_prog_aux (envr : env) (prog : t) : Ast.t =
   match prog with
   | [] -> []
   | (Lbl _) :: p -> translate_prog_aux envr p
-  | instr :: p -> (translate_instr envr instr) :: (translate_prog_aux envr p)
+  | (Word w) :: p -> translate_word envr w :: (translate_prog_aux envr p)
+  | instr :: p -> (Op (translate_instr envr instr)) :: (translate_prog_aux envr p)
 
 let translate_prog (prog : t) : Ast.t =
   let envr = compute_env 0 prog [] in

lib/lexer.mll

@@ -61,6 +61,8 @@ rule token = parse
 | ')' { RPAREN }
 | '+' { PLUS }
 | '-' { MINUS }
+| ',' { COMMA }
+| '#' { SHARP }
 
 (* locality *)
 | "LOCAL"    | "Local" { LOCAL }

lib/machine.ml

@@ -45,7 +45,13 @@ let init_mem_state (addr_max : int) (prog : t) : mem_state =
     loop 0 MemMap.empty
   in
   let enc_prog =
-    List.to_seq @@ List.mapi (fun i x -> i, I (Encode.encode_statement x)) prog in
+    List.to_seq @@ List.mapi
+      (fun i x -> i,
+                  match x with
+                  | Op op -> I (Encode.encode_machine_op op)
+                  | Word (Ast.I z) -> I z
+                  | Word (Ast.Cap (p,g,b,e,a)) -> Cap (p, g, Z.to_int b, Z.to_int e, Z.to_int a))
+      prog in
   MemMap.add_seq enc_prog zeroed_mem
 
 let get_mem (addr : int) (conf : exec_conf) : word option = MemMap.find_opt addr conf.mem
@@ -76,19 +82,18 @@ let upd_pc_perm (w : word) =
   | Cap (E, g, b, e, a) -> Cap (RX, g, b, e, a)
   | _ -> w
 
-let fetch_decode (conf : exec_conf) : statement option =
+let fetch_decode (conf : exec_conf) : machine_op option =
   match PC @! conf with
   | I _ -> None
   | Cap (_, _, _, _, addr) ->
     match get_mem addr conf with
     | Some (I enc) ->
-      (try Some (Encode.decode_statement enc)
+      (try Some (Encode.decode_machine_op enc)
         with Encode.DecodeException _ -> None)
     | _ -> None
 
 let is_pc_valid (conf : exec_conf) : bool =
-  match PC @! conf with
-  | Cap ((RX|RWX|RWLX), _, b, e, a) -> begin
+  match PC @! conf with | Cap ((RX|RWX|RWLX), _, b, e, a) -> begin
       if b <= a && a < e
       then Option.is_some @@ a @? conf
       else false

lib/parser.mly

@@ -5,7 +5,7 @@
 %token <string> LABELDEF
 %token <string> LABEL
 %token LPAREN RPAREN
-%token PLUS MINUS
+%token PLUS MINUS COMMA SHARP
 %token NOP JMP JNZ MOVE LOAD STORE ADD SUB LT LEA RESTRICT SUBSEG ISPTR
 %token GETL GETP GETB GETE GETA FAIL HALT LOADU STOREU PROMOTEU
 %token O E RO RX RW RWX RWL RWLX URW URWX URWL URWLX
@@ -45,6 +45,11 @@ main:
   | FAIL; p = main; { Fail :: p }
   | HALT; p = main; { Halt :: p }
   | lbl = LABELDEF; p = main; { Lbl lbl :: p }
+  | SHARP ; cap = cap_def; p = main; { Word cap :: p }
+  | SHARP ; z = expr; p = main; { Word (I z) :: p }
+
+cap_def:
+  | LPAREN; p = perm; COMMA; g = locality; COMMA; b = expr; COMMA; e = expr; COMMA; a = expr; RPAREN; { Cap (p, g, b, e, a) }
 
 reg:
   | PC; { PC }

lib/pretty_printer.ml

@@ -36,7 +36,7 @@ let string_of_reg_or_const (c: reg_or_const) : string =
   | CP (Const c) -> (Z.to_string c)
   | CP (Perm (p,g)) -> "(" ^- string_of_perm p ^- "," ^- string_of_locality g  ^- ")"
 
-let string_of_statement (s: statement): string =
+let string_of_machine_op (s: machine_op): string =
   let string_of_rr r1 r2 =
     string_of_regname r1 ^- string_of_regname r2
   and string_of_rc r c =
@@ -76,6 +76,19 @@ let string_of_word (w : word) : string =
     Printf.sprintf "Cap (%s, %s, %d, %d, %d)" (string_of_perm p) (string_of_locality g) b e a
   | I z -> Z.to_string z
 
+let string_of_ast_word (w : Ast.word) : string =
+  match w with
+  | Ast.Cap (p, g, b, e, a) ->
+    Printf.sprintf "Cap (%s, %s, %s, %s, %s)" (string_of_perm p)
+      (string_of_locality g)
+      (Z.to_string b) (Z.to_string e) (Z.to_string a)
+  | Ast.I z -> Z.to_string z
+
+let string_of_statement (s : statement) : string =
+  match s with
+  | Op op -> string_of_machine_op op
+  | Ast.Word w -> string_of_ast_word w
+
 let string_of_reg_word (r : regname) (w : word) : string =
   Printf.sprintf "| %s : %s |" (string_of_regname r) (string_of_word w)
 

lib/scall_dcap.ml

@@ -8,19 +8,19 @@ let in_list (e :'a) (l : 'a list) : bool =
 let all_registers : regname list =
   [PC; STK] @ List.init 32 (fun i -> Reg i)
 
-let rec rclear (regs : regname list) : (statement list) =
+let rec rclear (regs : regname list) : (machine_op list) =
   match regs with
   | [] -> []
   | r::regs' -> (Move (r, const 0))::(rclear regs')
 
 let reg_diff (regs : regname list) : regname list=
   (List.filter (fun r -> not (in_list r regs)) all_registers)
 
-let rclear_inv (regs : regname list) : statement list =
+let rclear_inv (regs : regname list) : machine_op list =
   (rclear (reg_diff regs))
 
 
-let mclearU : statement list =
+let mclearU : machine_op list =
   let mclear_off_end = 9 in
   let mclear_off_iter = 2 in
   [
@@ -105,12 +105,12 @@ let prepstack r minsize paramsize =
   ]
 
 
-let scall_prologue radv params : (statement list) =
-  let w1 = Encode.encode_statement (Move (Reg 1, Register PC)) in
-  let w2 = Encode.encode_statement (Lea (Reg 1, const 6)) in
-  let w3 = Encode.encode_statement (Load (STK, Reg 1)) in
-  let w4a = Encode.encode_statement (Sub (Reg 1, const 0, const 1)) in
-  let w4b = Encode.encode_statement (LoadU (PC, STK, Register (Reg 1))) in
+let scall_prologue radv params : (machine_op list) =
+  let w1 = Encode.encode_machine_op (Move (Reg 1, Register PC)) in
+  let w2 = Encode.encode_machine_op (Lea (Reg 1, const 6)) in
+  let w3 = Encode.encode_machine_op (Load (STK, Reg 1)) in
+  let w4a = Encode.encode_machine_op (Sub (Reg 1, const 0, const 1)) in
+  let w4b = Encode.encode_machine_op (LoadU (PC, STK, Register (Reg 1))) in
   let epilogue_b =
   [
     (* Push activation record *)

lib/scall_ucap.ml

@@ -8,15 +8,15 @@ let in_list (e :'a) (l : 'a list) : bool =
 let all_registers : regname list =
   [PC; STK] @ List.init 32 (fun i -> Reg i)
 
-let rec rclear (regs : regname list) : (statement list) =
+let rec rclear (regs : regname list) : (machine_op list) =
   match regs with
   | [] -> []
   | r::regs' -> (Move (r,const 0))::(rclear regs')
 
-let rclear_inv (regs : regname list) : statement list =
+let rclear_inv (regs : regname list) : machine_op list =
   (rclear (List.filter (fun r -> not (in_list r regs)) all_registers))
 
-let mclearU : statement list =
+let mclearU : machine_op list =
   let mclear_off_end = 9 in
   let mclear_off_iter = 2 in
   [
@@ -100,12 +100,12 @@ let prepstack r minsize =
   ]
 
 
-let epilogue_scall radv : (statement list) =
-  let w1 = Encode.encode_statement (Move (Reg 1, Register PC)) in
-  let w2 = Encode.encode_statement (Lea (Reg 1, const 6)) in
-  let w3 = Encode.encode_statement (Load (STK, Reg 1)) in
-  let w4a = Encode.encode_statement (Sub (Reg 1, const 0, const 1)) in
-  let w4b = Encode.encode_statement (LoadU (PC, STK, Register (Reg 1))) in
+let epilogue_scall radv : (machine_op list) =
+  let w1 = Encode.encode_machine_op (Move (Reg 1, Register PC)) in
+  let w2 = Encode.encode_machine_op (Lea (Reg 1, const 6)) in
+  let w3 = Encode.encode_machine_op (Load (STK, Reg 1)) in
+  let w4a = Encode.encode_machine_op (Sub (Reg 1, const 0, const 1)) in
+  let w4b = Encode.encode_machine_op (LoadU (PC, STK, Register (Reg 1))) in
   let epilogue_b =
   [
     (* Push activation record *)

src/awkward_dcaps.ml

@@ -4,7 +4,10 @@ open Scall_dcap
 let () =
   let radv = (Ast.Reg 28) in
   let renv = (Ast.Reg 30) in
-  let prog = awkward_example radv @ adv_instr @ ret_instr in
+  let prog =
+    List.map (fun i -> Ast.Op i)
+      (awkward_example radv @ adv_instr @ ret_instr)
+  in
 
   (* let addr_max = List.length prog in *)
   (* let addr_max = (Int32.to_int Int32.max_int)/4096 in *)

src/awkward_ucaps.ml

@@ -4,7 +4,10 @@ open Scall_ucap
 let () =
   let radv = (Ast.Reg 28) in
   let renv = (Ast.Reg 30) in
-  let prog = awkward_example radv @ adv_instr @ ret_instr in
+  let prog =
+    List.map (fun i -> Ast.Op i)
+      (awkward_example radv @ adv_instr @ ret_instr)
+  in
 
   (* let addr_max = List.length prog in *)
   (* let addr_max = (Int32.to_int Int32.max_int)/4096 in *)