Support for sealing

* Quick compilation fix

* Simplification of the encoding for the permissions

* Merge branch 'main' into directed-caps

* Refactoring encoding

* Merge branch 'main' into directed-caps: normalization

* Merge branch 'directed-caps' into bastien/compiler

lib/ast.ml

@@ -2,9 +2,12 @@
 type regname = PC | STK | Reg of int
 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 wtype = W_I | W_Cap | W_SealRange | W_Sealed
+type seal_perm = bool * bool
+type reg_or_const = Register of regname | Const of Z.t
+type sealable = Cap of perm * locality * Z.t * Z.t * Z.t
+              | SealRange of seal_perm * locality* Z.t * Z.t * Z.t
+type word = I of Z.t | Sealable of sealable | Sealed of Z.t * sealable
 type machine_op
   =
   | Jmp of regname
@@ -21,12 +24,15 @@ type machine_op
   | Lea of regname * reg_or_const
   | Restrict of regname * reg_or_const
   | SubSeg of regname * reg_or_const * reg_or_const
-  | IsPtr of regname * regname
   | GetL of regname * regname
-  | GetP of regname * regname
   | GetB of regname * regname
   | GetE of regname * regname
   | GetA of regname * regname
+  | GetP of regname * regname
+  | GetOType of regname * regname
+  | GetWType of regname * regname
+  | Seal of regname * regname * regname
+  | UnSeal of regname * regname * regname
   | LoadU of regname * regname * reg_or_const
   | StoreU of regname * reg_or_const * reg_or_const
   | PromoteU of regname
@@ -48,4 +54,4 @@ let compare_regname (r1 : regname) (r2: regname) : int =
   | Reg _, PC -> 1
   | Reg i, Reg j -> Int.compare i j
 
-let const n = CP (Const (Z.of_int n))
+let const n = Const (Z.of_int n)

lib/call.ml

@@ -3,7 +3,7 @@ open Ast
 (** Calling convention from
  https://github.com/logsem/cerise-stack-monotone/blob/master/theories/overlay/call.v *)
 
-let const n = CP (Const (Z.of_int n))
+let const n = (Const (Z.of_int n))
 let in_list (e :'a) (l : 'a list) : bool =
   match (List.find_opt (fun x -> x = e) l) with
   | None -> false
@@ -41,23 +41,24 @@ let call_prologue (rargs : regname list) : (machine_op list) =
   push_env@
   push_instrs [Register rstk]@
   push_instrs
-    ((List.map (fun i -> CP (Const (Encode.encode_machine_op i)))
+    ((List.map (fun i -> (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_machine_op (LoadU (PC, rstk, const (-1))))))])@
+     @ List.map (fun i -> (Const i)) pop_env
+     @ [(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) : machine_op list =
+  let e_directed_perm = Const (Encode.encode_perm_loc_pair E Directed) in
   call_prologue rargs @
   [ Move (Reg 30, Register rstk);
     PromoteU (Reg 30);
     Lea (Reg 30, const (-66));
-    Restrict (Reg 30, CP (Perm (E, Directed)));
+    Restrict (Reg 30, e_directed_perm);
     GetA (Reg 31, rstk);
     GetB (Reg 29, rstk);
     SubSeg (rstk, Register (Reg 31), Register (Reg 31));

lib/compiler.ml

@@ -0,0 +1,71 @@
+open Convert
+open Extract
+
+let rec pp_of_instrs l =
+  match l with
+  | [] -> Printf.printf ""
+  | i::l' ->
+    Printf.printf "%s\n%!" (Pretty_printer.string_of_machine_op (Convert.translate_instr i));
+  pp_of_instrs l'
+
+let pp_sealable (sb : Ast.sealable) =
+  match sb with
+  | Cap (p, g, b, e, a) ->
+    Printf.sprintf "(%s, %s, %s, %s, %s)" (Pretty_printer.string_of_perm p)
+      (Pretty_printer.string_of_locality g)
+      (Big_int_Z.string_of_big_int b)
+      (Big_int_Z.string_of_big_int e)
+      (Big_int_Z.string_of_big_int a)
+  | SealRange (p, g, b, e, a) ->
+    Printf.sprintf "[%s, %s, %s, %s, %s]" (Pretty_printer.string_of_seal_perm p)
+      (Pretty_printer.string_of_locality g)
+      (Big_int_Z.string_of_big_int b)
+      (Big_int_Z.string_of_big_int e)
+      (Big_int_Z.string_of_big_int a)
+
+let pp_word_reg (w : Ast.word)
+  = match w with
+  | I z -> Printf.sprintf "%s" (Big_int_Z.string_of_big_int z)
+  | Sealable sb -> pp_sealable sb
+  | Sealed (ot, sb) -> Printf.sprintf "{%s: %s}" (Big_int_Z.string_of_big_int ot) (pp_sealable sb)
+
+let pp_word_asm (w : Ast.word)
+  = match w with
+  | I z -> (Pretty_printer.string_of_machine_op (Convert.translate_instr (Convert.machine_param.decodeInstr z)))
+  | Sealable sb -> Printf.sprintf "#%s" (pp_sealable sb)
+  | Sealed (ot, sb) -> Printf.sprintf "#{%s: %s}" (Big_int_Z.string_of_big_int ot) (pp_sealable sb)
+
+let pp_regname (r : Extract.regName) =
+  match r with
+  | PC -> "PC"
+  | STK -> "stk"
+  | R n -> Printf.sprintf "r%s" (Big_int_Z.string_of_big_int n)
+
+let machine_compile
+    ?(addr_max = (Int32.to_int Int32.max_int)/4096 )
+    ?(start_stack = Big_int_Z.big_int_of_int (addr_max/2) )
+    ?(end_stack = Big_int_Z.big_int_of_int addr_max)
+    program
+  : (regName * Ast.word) list * (addr * Ast.word) list
+  =
+  let (regs, compiled_prog) = program Convert.machine_param start_stack end_stack in
+  let prog =
+    List.map
+      (fun w -> (fst w, Convert.translate_word (snd w)))
+      compiled_prog
+  in
+  let regs =
+    List.map
+      (fun w -> (fst w, Convert.translate_word (snd w)))
+      regs
+  in
+  (regs, prog)
+
+let output_machine regfile_output_name asm_output_name regs prog  =
+  let oc = open_out regfile_output_name in
+  List.iter (fun w -> Printf.fprintf oc "%s := %s\n" (pp_regname (fst w))
+                (pp_word_reg (snd w))) regs;
+  close_out oc;
+  let oc = open_out asm_output_name in
+  List.iter (fun w -> Printf.fprintf oc "%s\n" (pp_word_asm (snd w))) prog;
+  close_out oc

lib/convert.ml

@@ -21,6 +21,13 @@ let translate_locality (g : locality) : Ast.locality =
   | Global -> Ast.Global
   | Directed -> Ast.Directed
 
+let translate_wtype (wt : word) : Ast.wtype =
+  match wt with
+  | WInt _ -> Ast.W_I
+  | WSealable (SCap _) -> Ast.W_Cap
+  | WSealable (SSealRange _) -> Ast.W_SealRange
+  | WSealed _ -> Ast.W_Sealed
+
 let translate_regname (r : regName) : Ast.regname =
   match r with
   | PC -> Ast.PC
@@ -30,7 +37,7 @@ let translate_regname (r : regName) : Ast.regname =
 let translate_sum (s : (Big_int_Z.big_int, regName) sum) : Ast.reg_or_const =
 match s with
 | Inr r -> Ast.Register (translate_regname r)
-| Inl z -> Ast.CP (Const z)
+| Inl z -> Ast.Const z
 
 let translate_instr (i : cerise_instruction) : Ast.machine_op =
   match i with
@@ -57,7 +64,7 @@ let translate_instr (i : cerise_instruction) : Ast.machine_op =
   | Div (r, c1, c2) -> Ast.Div (translate_regname r,
                                 translate_sum c1,
                                 translate_sum c2)
-  | Lt (r, c1, c2) -> Ast.Lt (translate_regname r,
+  | Lt0 (r, c1, c2) -> Ast.Lt (translate_regname r,
                               translate_sum c1,
                               translate_sum c2)
   | Lea (r, c) -> Ast.Lea (translate_regname r, translate_sum c)
@@ -66,12 +73,16 @@ let translate_instr (i : cerise_instruction) : Ast.machine_op =
   | Subseg (r, c1, c2) -> Ast.SubSeg (translate_regname r,
                                       translate_sum c1,
                                       translate_sum c2)
-  | IsPtr (r1, r2) -> Ast.IsPtr (translate_regname r1, translate_regname r2)
   | GetL (r1, r2) -> Ast.GetL (translate_regname r1, translate_regname r2)
-  | GetP (r1, r2) -> Ast.GetP (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)
   | GetA (r1, r2) -> Ast.GetA (translate_regname r1, translate_regname r2)
+  | GetP (r1, r2) -> Ast.GetP (translate_regname r1, translate_regname r2)
+  | GetWType (r1, r2) -> Ast.GetWType (translate_regname r1, translate_regname r2)
+  | GetOType (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)
+
   | LoadU (r1, r2, c) -> Ast.LoadU (translate_regname r1,
                                     translate_regname r2,
                                     translate_sum c)
@@ -91,12 +102,14 @@ let tr_reg (r : Ast.regname) : regName =
 let tr_sum (c : Ast.reg_or_const) : (Big_int_Z.big_int, regName) sum =
   match c with
   | Register r -> Inr (tr_reg r)
-  | CP cp ->
-    match cp with
-    | Const n -> Inl n
-    | Perm (p,g)->
-      let n = Encode.encode_perm_pair p g in
-      Inl n
+  | Const z -> Inl z
+    (* TODO might require to use decode/encode from Ir *)
+    (* Ir.decode *)
+    (* match cp with *)
+    (* | Const n -> Inl n *)
+    (* | Perm (p,g)-> *)
+    (*   let n = Encode.encode_perm_pair p g in *)
+    (*   Inl n *)
 
 let tr_machine_op (s : Ast.machine_op) : cerise_instruction =
   match s with
@@ -110,16 +123,19 @@ let tr_machine_op (s : Ast.machine_op) : cerise_instruction =
   | Ast.Mul (r, c1, c2) -> Mul (tr_reg r, tr_sum c1, tr_sum c2)
   | Ast.Rem (r, c1, c2) -> Rem (tr_reg r, tr_sum c1, tr_sum c2)
   | Ast.Div (r, c1, c2) -> Div (tr_reg r, tr_sum c1, tr_sum c2)
-  | Ast.Lt (r, c1, c2) -> Lt (tr_reg r, tr_sum c1, tr_sum c2)
+  | Ast.Lt (r, c1, c2) -> Lt0 (tr_reg r, tr_sum c1, tr_sum c2)
   | Ast.Lea (r, c) -> Lea (tr_reg r, tr_sum c)
   | Ast.Restrict (r, c) -> Restrict (tr_reg r, tr_sum c)
   | Ast.SubSeg (r, c1, c2) -> Subseg (tr_reg r, tr_sum c1, tr_sum c2)
-  | Ast.IsPtr (r1, r2) -> IsPtr (tr_reg r1, tr_reg r2)
   | Ast.GetL (r1, r2) -> GetL (tr_reg r1, tr_reg r2)
-  | Ast.GetP (r1, r2) -> GetP (tr_reg r1, tr_reg r2)
   | Ast.GetB (r1, r2) -> GetB (tr_reg r1, tr_reg r2)
   | Ast.GetE (r1, r2) -> GetE (tr_reg r1, tr_reg r2)
   | Ast.GetA (r1, r2) -> GetA (tr_reg r1, tr_reg r2)
+  | Ast.GetP (r1, r2) -> GetP (tr_reg r1, tr_reg r2)
+  | Ast.GetOType (r1, r2) -> GetOType (tr_reg r1, tr_reg r2)
+  | Ast.GetWType (r1, r2) -> GetWType (tr_reg r1, tr_reg r2)
+  | Ast.Seal (r1, r2, r3) -> Seal (tr_reg r1, tr_reg r2, tr_reg r3)
+  | Ast.UnSeal (r1, r2, r3) -> UnSeal (tr_reg r1, tr_reg r2, tr_reg r3)
   | Ast.LoadU (r1, r2, c) -> LoadU (tr_reg r1, tr_reg r2, tr_sum c)
   | Ast.StoreU (r, c1, c2) -> StoreU (tr_reg r, tr_sum c1, tr_sum c2)
   | Ast.PromoteU r -> PromoteU (tr_reg r)
@@ -147,6 +163,13 @@ let tr_loc (g : Ast.locality) : locality =
   | Ast.Global -> Global
   | Ast.Directed -> Directed
 
+let tr_wtype (wt : Ast.wtype) : word =
+  match wt with
+  | Ast.W_I -> wt_int
+  | Ast.W_Cap -> wt_cap
+  | Ast.W_SealRange -> wt_sealrange
+  | Ast.W_Sealed -> wt_sealed
+
 let encode_label_name (l : Big_int_Z.big_int list) : Big_int_Z.big_int =
   let rec encode_label_name' (l : Big_int_Z.big_int list)
     : Big_int_Z.big_int =
@@ -214,17 +237,27 @@ let machine_param = {
   encodeInstr = (function i -> Encode.encode_machine_op (translate_instr i));
   encodePerm = (function p -> Encode.encode_perm (translate_perm p));
   encodeLoc = (function g -> Encode.encode_locality (translate_locality g));
-  decodePermPair = (function z ->
-      let (p,g) = Encode.decode_perm_pair z in
-      (tr_perm p, tr_loc g));
-  encodePermPair = (function p ->
-    let (p,g) = p in Encode.encode_perm_pair (translate_perm p) (translate_locality g))
+
+  decodePermPair = (function z -> let (p,g) = Encode.decode_perm_loc_pair z in (tr_perm p, tr_loc g));
+  encodePermPair = (function p -> let (p,g) = p in Encode.encode_perm_loc_pair (translate_perm p) (translate_locality g));
+
+  decodeSealPermPair = (function z -> let (p,g) = Encode.decode_seal_perm_loc_pair z in (p, tr_loc g));
+  encodeSealPermPair = (function p -> let (p,g) = p in Encode.encode_seal_perm_loc_pair p (translate_locality g));
+
+  encodeSealPerms = (function p -> Encode.encode_seal_perm p);
+  decodeSealPerms = (function p -> Encode.decode_seal_perm p);
+  encodeWordType = (function wt -> Encode.encode_wtype (translate_wtype wt));
+  decodeWordType = (function wt -> tr_wtype (Encode.decode_wtype wt));
 }
 
-let translate_word (w : (Big_int_Z.big_int, (((Extract.perm * Extract.locality) * Big_int_Z.big_int) * Big_int_Z.big_int
-                    ) * Big_int_Z.big_int) Extract.sum)
-  = match w with
-  | Inl z -> Ast.I z
-  | Inr ((((p,l),b),e),a) -> Ast.Cap (translate_perm p, translate_locality l,b,e,a)
+let translate_sealable (sb : Extract.sealable) =
+  match sb with
+  | SCap ((p,l), b, e, a) -> Ast.Cap (translate_perm p, translate_locality l, b, e, a)
+  | SSealRange ((p,l), b, e, a) -> Ast.SealRange (p, translate_locality l, b, e, a)
+
 
-(* (Convert.translate_instr (Convert.driver.decodeInstr z)) *)
+let translate_word (w : Extract.word) =
+  match w with
+  | WInt z -> Ast.I z
+  | WSealable sb -> Ast.Sealable (translate_sealable sb)
+  | WSealed (ot, sb) -> Ast.Sealed (ot, translate_sealable sb)