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

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

Hide file tree

Showing 28 changed files with 684 additions and 604 deletions.
diff --git a/lib/ast.ml b/lib/ast.ml
@@ -1,53 +1,50 @@
 (* 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
+module Perm = struct
   type t =
-  | E   (* sentry                  ---  sealed value with otype 1, 2 or 3 *)
-  | R   (* read                    ---  LG, MC and LD *)
-  | X   (* execute                 ---  EX *)
-  | W   (* write                   ---  LM, MC and SD *)
-  | WL  (* write local             ---  SL *)
-  | 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
+    | E (* sentry                  ---  sealed value with otype 1, 2 or 3 *)
+    | R (* read                    ---  LG, MC and LD *)
+    | X (* execute                 ---  EX *)
+    | W (* write                   ---  LM, MC and SD *)
+    | WL (* write local             ---  SL *)
+    | SR (* system register access  ---  SR *)
+    | DL (* deep locality           ---  inverse of LG *)
+    | DI (* deep immutability       ---  inverse of LM *)
 
-    (* 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
 type seal_perm = bool * bool
 type reg_or_const = Register of regname | Const of Z.t
 
 type sealable =
-  | Cap of (PermSet.t) * locality * Z.t * Z.t * Z.t
+  | Cap of PermSet.t * 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
-  | 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

diff --git a/lib/cli_parser.ml b/lib/cli_parser.ml
@@ -5,9 +5,7 @@ type cli_mode = Interactive_mode | Interpreter_mode
 (** Initialize the Cerise version and returns
     (mode, program_filename, register_filename, size_mem) *)
 let parse_arguments () : cli_mode * string * string =
-  let usage_msg =
-    "interpreter [-I] [--interactive] [--version version] [--mem-size size] <file>"
-  in
+  let usage_msg = "interpreter [-I] [--interactive] [--version version] [--mem-size size] <file>" in
   let interactive_option = ref false in
   let version_option = ref "default" in
   let mem_size_option = ref "" in
@@ -19,9 +17,7 @@ let parse_arguments () : cli_mode * string * string =
     [
       ("--interactive", Arg.Set interactive_option, "Interactive mode of the interpreter");
       ("-I", Arg.Set interactive_option, "Interactive mode of the interpreter");
-      ( "--version",
-        Arg.Set_string version_option,
-        "Version Cerise: default" );
+      ("--version", Arg.Set_string version_option, "Version Cerise: default");
       ("--mem-size", Arg.Set_string mem_size_option, "Size of the memory, integer");
       ("--regfile", Arg.Set_string regfile_name_option, "Initial state of the registers");
     ]
@@ -34,10 +30,7 @@ let parse_arguments () : cli_mode * string * string =
   let _ =
     match !version_option with
     | "default" -> Parameters.flags := Parameters.full_cerise
-    | _ ->
-        raise
-        @@ Arg.Help
-             "The --version option requires one of the following values: default"
+    | _ -> raise @@ Arg.Help "The --version option requires one of the following values: default"
   in
 
   let _ =