New permissions; instructions Jalr+Jmp+Jnz+MoveSR ; new parser/lexer/…

…pp ; adapt tests
logsem · Jun 4, 2024 · 61379e0 · 61379e0
1 parent 4311c88
commit 61379e0
Show file tree

Hide file tree

Showing 27 changed files with 714 additions and 514 deletions.
diff --git a/lib/ast.ml b/lib/ast.ml
@@ -1,9 +1,9 @@
 (* Type definitions for the syntax AST *)
 type regname = PC | Reg of int
 
-let cgp = Reg 0
-let stk = Reg 31
-let sreg = Reg 30
+let cgp = Reg 5
+let stk = Reg 30
+let mtcc = Reg 31
 
 module Perm =
 struct
@@ -16,23 +16,23 @@ struct
   | SR  (* system register access  ---  SR *)
   | DL  (* deep locality           ---  inverse of LG *)
   | DI  (* deep immutability       ---  inverse of LM *)
-  let compare p1 p2 = if (p1 = p2) then 0 else 1
-  let allowed_with (p1 : t) (p2 : t) =
-    match (p1,p2) with
-    (* sentry are not allowed with any other capabilities *)
-    | E,_ -> false
-    (* system access permission only with X *)
-    | SR,X -> true
-    | SR,_ -> false
-
-    (* no write and execute permission at the same time *)
-    | W,X -> false
-    | WL,X -> false
-
-    | _,_ -> true
+  let compare p1 p2 = if (p1 = p2) then 0 else
+      (* Just an order for pretty printing *)
+      let weight p =
+        match p with
+        | E  -> 0
+        | R  -> 1
+        | X  -> 2
+        | W  -> 3
+        | WL -> 4
+        | SR -> 5
+        | DL -> 6
+        | DI -> 7
+      in
+      (weight p2) - (weight p1)
 end
-module PermSet = Set.Make(Perm)
 
+module PermSet = Set.Make(Perm)
 
 type locality = Global | Local
 type wtype = W_I | W_Cap | W_SealRange | W_Sealed
@@ -46,29 +46,39 @@ type sealable =
 type word = I of Z.t | Sealable of sealable | Sealed of Z.t * sealable
 
 type machine_op =
-  | Jmp of regname
-  | Jnz of regname * regname
+  | Jalr of regname * regname (* jump and link return *)
+  | Jmp of reg_or_const (* immediate jump *)
+  | Jnz of regname * reg_or_const (* jump non zero *)
+
+  (* system access registers *)
+  | MoveSR of regname * reg_or_const
+
   | Move of regname * reg_or_const
   | Load of regname * regname
   | Store of regname * reg_or_const
+
   | Add of regname * reg_or_const * reg_or_const
   | Sub of regname * reg_or_const * reg_or_const
   | 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
   | Lt of regname * reg_or_const * reg_or_const
+
   | Lea of regname * reg_or_const
   | Restrict of regname * reg_or_const
   | SubSeg of regname * reg_or_const * reg_or_const
+
   | GetL 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