Sealing (#1)

* Add support for sealing

* Fixing parser + display style for interactive

* GetOType and GetWType instructions

* Modification of the internal model for permission: every kind of permission/word type is a constant that is encoded at parsing-time.

* Test cases for sealing + fixing/cleaning tests

* Non-trivial test case using sealing (sealing_counter)

lib/ast.ml

@@ -1,9 +1,11 @@
 (* Type definitions for the syntax AST *)
 type regname = PC | Reg of int
 type perm = O | E | RO | RX | RW | RWX
-type const_perm = Const of Z.t | Perm of perm
-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 * 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 * Z.t * Z.t * Z.t | SealRange of seal_perm * 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
   | Jnz of regname * regname
@@ -19,11 +21,14 @@ 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
-  | 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
   | Fail
   | Halt
 
@@ -37,4 +42,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)