Merge branch 'main' into directed-caps

logsem · Aug 3, 2023 · 93982ec · 93982ec
2 parents a40994e + f094632
commit 93982ec
Show file tree

Hide file tree

Showing 46 changed files with 1,243 additions and 739 deletions.
diff --git a/lib/ast.ml b/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)
diff --git a/lib/call.ml b/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 (Ir.encode_const [] (Perm (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));