chore(fmt): Apply ocamlformat

logsem · Jan 19, 2024 · ea4e6a1 · ea4e6a1
1 parent 9ef8fc2
commit ea4e6a1
Show file tree

Hide file tree

Showing 24 changed files with 1,954 additions and 2,609 deletions.
diff --git a/.ocamlformat b/.ocamlformat
@@ -0,0 +1,3 @@
+profile = default
+version = 0.26.0
+margin = 100
diff --git a/lib/ast.ml b/lib/ast.ml
@@ -1,17 +1,22 @@
 (* Type definitions for the syntax AST *)
 type regname = PC | Reg of int
+
 let ddc = Reg 0
 let stk = Reg 31
+
 type perm = O | E | RO | RX | RW | RWX | RWL | RWLX | URW | URWL | URWX | URWLX
 type locality = Global | Local | Directed
 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 * Infinite_z.t * Z.t
-              | SealRange of seal_perm * locality* Z.t * Z.t * Z.t
+
+type sealable =
+  | Cap of perm * locality * Z.t * Infinite_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
-  =
+
+type machine_op =
   | Jmp of regname
   | Jnz of regname * regname
   | Invoke of regname * regname
@@ -45,8 +50,8 @@ type machine_op
 type statement = Op of machine_op | Word of word (* TODO: PseudoOp and LabelDefs *)
 type t = statement list
 
-let compare_regname (r1 : regname) (r2: regname) : int =
-  match r1, r2 with
+let compare_regname (r1 : regname) (r2 : regname) : int =
+  match (r1, r2) with
   | PC, PC -> 0
   | PC, Reg _ -> -1
   | Reg _, PC -> 1

diff --git a/lib/call.ml b/lib/call.ml
@@ -3,67 +3,62 @@ open Ast
 (** Calling convention from
  https://github.com/logsem/cerise-stack-monotone/blob/master/theories/overlay/call.v *)
 
-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
-  | Some _ -> true
+let const n = Const (Z.of_int n)
 
-let all_registers : regname list =
-  [PC; stk] @ List.init 32 (fun i -> Reg i)
+let in_list (e : 'a) (l : 'a list) : bool =
+  match List.find_opt (fun x -> x = e) l with None -> false | Some _ -> true
 
-let rstk : regname = (Reg 0)
+let all_registers : regname list = [ PC; stk ] @ List.init 32 (fun i -> Reg i)
+let rstk : regname = Reg 0
 
-let rec rclear (regs : regname list) : (machine_op list) =
-  match regs with
-  | [] -> []
-  | r::regs' -> (Move (r, const 0))::(rclear regs')
+let rec rclear (regs : regname list) : machine_op list =
+  match regs with [] -> [] | r :: regs' -> Move (r, const 0) :: rclear regs'
 
 let rclear_inv (regs : regname list) : machine_op list =
-  (rclear (List.filter (fun r -> not (in_list r regs)) all_registers))
+  rclear (List.filter (fun r -> not (in_list r regs)) all_registers)
 
-let reg_diff (regs : regname list) : regname list=
-  (List.filter (fun r -> not (in_list r regs)) all_registers)
+let reg_diff (regs : regname list) : regname list =
+  List.filter (fun r -> not (in_list r regs)) all_registers
 
 let push_instrs ps = List.map (fun p -> StoreU (rstk, const 0, p)) ps
-let pop_instrs r =
-  [Encode.encode_machine_op (LoadU (r,rstk, const (-1)));
-  Encode.encode_machine_op (Lea (rstk, const (-1)))]
 
-let push_env =
-  push_instrs (List.map (fun r -> Register r) (reg_diff [PC;rstk]))
+let pop_instrs r =
+  [
+    Encode.encode_machine_op (LoadU (r, rstk, const (-1)));
+    Encode.encode_machine_op (Lea (rstk, const (-1)));
+  ]
 
-let pop_env =
-  List.fold_left (fun b r -> (pop_instrs r) @ b) [] (reg_diff [PC;rstk])
+let push_env = push_instrs (List.map (fun r -> Register r) (reg_diff [ PC; rstk ]))
+let pop_env = List.fold_left (fun b r -> pop_instrs r @ b) [] (reg_diff [ PC; rstk ])
 
-let call_prologue (rargs : regname list) : (machine_op list) =
-  push_instrs [const 0]@
-  push_env@
-  push_instrs [Register rstk]@
-  push_instrs
-    ((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 -> (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 call_prologue (rargs : regname list) : machine_op list =
+  push_instrs [ const 0 ]
+  @ push_env @ push_instrs [ Register rstk ]
+  @ push_instrs
+      (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 -> 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, e_directed_perm);
-    GetA (Reg 31, rstk);
-    GetB (Reg 29, rstk);
-    SubSeg (rstk, Register (Reg 31), Register (Reg 31));
-  ]@
-  push_instrs [Register (Reg 30)]@
-  push_instrs (List.map (fun x -> Register x) rargs)@
-  rclear (reg_diff [PC;rstk])@
-  [Jmp r]
+  call_prologue rargs
+  @ [
+      Move (Reg 30, Register rstk);
+      PromoteU (Reg 30);
+      Lea (Reg 30, const (-66));
+      Restrict (Reg 30, e_directed_perm);
+      GetA (Reg 31, rstk);
+      GetB (Reg 29, rstk);
+      SubSeg (rstk, Register (Reg 31), Register (Reg 31));
+    ]
+  @ push_instrs [ Register (Reg 30) ]
+  @ push_instrs (List.map (fun x -> Register x) rargs)
+  @ rclear (reg_diff [ PC; rstk ])
+  @ [ Jmp r ]
diff --git a/lib/cli_parser.ml b/lib/cli_parser.ml
@@ -4,10 +4,10 @@ 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 parse_arguments () : cli_mode * string * string =
   let usage_msg =
-    "interpreter [-I] [--interactive] [--version version] [--locality locality] [--sealing | --no-sealing]  [--stack | --no-stack] [--uperms | --no-uperms] [--mem-size size] <file>"
+    "interpreter [-I] [--interactive] [--version version] [--locality locality] [--sealing | \
+     --no-sealing]  [--stack | --no-stack] [--uperms | --no-uperms] [--mem-size size] <file>"
   in
   let interactive_option = ref false in
   let version_option = ref "default" in
@@ -27,56 +27,64 @@ 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, vanilla, ucerise, mcerise, seal_cerise, custom");
+      ( "--version",
+        Arg.Set_string version_option,
+        "Version Cerise: default, vanilla, ucerise, mcerise, seal_cerise, custom" );
       ("--sealing", Arg.Set sealing_option, "Enable the seals");
       ("--no-sealing", Arg.Set no_sealing_option, "Disable the seals");
       ("--stack", Arg.Set stack_option, "Enable the stack");
       ("--no-stack", Arg.Set no_stack_option, "Disable the stack");
       ("--uperms", Arg.Set uperms_option, "Enable the U-permission");
       ("--no-uperms", Arg.Set no_uperms_option, "Disable the U-permission");
-      ("--locality", Arg.Set_string locality_option, "Choose the minimum locality: Global, Local, Directed");
+      ( "--locality",
+        Arg.Set_string locality_option,
+        "Choose the minimum locality: Global, Local, Directed" );
       ("--mem-size", Arg.Set_string mem_size_option, "Size of the memory, Inf or integer");
       ("--regfile", Arg.Set_string regfile_name_option, "Initial state of the registers");
-    ] in
+    ]
+  in
   Arg.parse speclist anon_fun usage_msg;
 
   let mode = if !interactive_option then Interactive_mode else Interpreter_mode in
 
   (* Construct the configuration *)
   let _ =
     match !version_option with
-    | "default" -> (Parameters.flags := Parameters.full_cerise)
-    | "vanilla" -> (Parameters.flags := Parameters.vanilla_cerise)
-    | "ucerise" -> (Parameters.flags := Parameters.stack_cerise)
-    | "mcerise" -> (Parameters.flags := Parameters.mcerise)
-    | "seal_cerise" -> (Parameters.flags := Parameters.sealing_cerise)
-    | "custom" -> (Parameters.flags := Parameters.custom_cerise)
-    | _ -> raise @@ Arg.Help
-        "The --version option requires one of the following values: default, vanilla, ucerise, mcerise, custom"
+    | "default" -> Parameters.flags := Parameters.full_cerise
+    | "vanilla" -> Parameters.flags := Parameters.vanilla_cerise
+    | "ucerise" -> Parameters.flags := Parameters.stack_cerise
+    | "mcerise" -> Parameters.flags := Parameters.mcerise
+    | "seal_cerise" -> Parameters.flags := Parameters.sealing_cerise
+    | "custom" -> Parameters.flags := Parameters.custom_cerise
+    | _ ->
+        raise
+        @@ Arg.Help
+             "The --version option requires one of the following values: default, vanilla, \
+              ucerise, mcerise, custom"
   in
 
   let _ =
-    match !stack_option, !no_stack_option with
-    | (false, false) -> ()
-    | (true, false) -> Parameters.set_stack true
-    | (false, true) -> Parameters.set_stack false
-    | (true, true) -> raise @@ Arg.Help "Option --stack and --no-stack cannot be used together."
+    match (!stack_option, !no_stack_option) with
+    | false, false -> ()
+    | true, false -> Parameters.set_stack true
+    | false, true -> Parameters.set_stack false
+    | true, true -> raise @@ Arg.Help "Option --stack and --no-stack cannot be used together."
   in
 
   let _ =
-    match !sealing_option, !no_sealing_option with
-    | (false, false) -> ()
-    | (true, false) -> Parameters.set_sealing true
-    | (false, true) -> Parameters.set_sealing false
-    | (true, true) -> raise @@ Arg.Help "Option --sealing and --no-sealing cannot be used together."
+    match (!sealing_option, !no_sealing_option) with
+    | false, false -> ()
+    | true, false -> Parameters.set_sealing true
+    | false, true -> Parameters.set_sealing false
+    | true, true -> raise @@ Arg.Help "Option --sealing and --no-sealing cannot be used together."
   in
 
   let _ =
-    match !uperms_option, !no_uperms_option with
-    | (false, false) -> ()
-    | (true, false) -> Parameters.set_uperms true
-    | (false, true) -> Parameters.set_uperms false
-    | (true, true) -> raise @@ Arg.Help "Option --uperms and --no-uperms cannot be used together."
+    match (!uperms_option, !no_uperms_option) with
+    | false, false -> ()
+    | true, false -> Parameters.set_uperms true
+    | false, true -> Parameters.set_uperms false
+    | true, true -> raise @@ Arg.Help "Option --uperms and --no-uperms cannot be used together."
   in
 
   let _ =
@@ -85,27 +93,30 @@ let parse_arguments () : (cli_mode * string * string)
     | "Directed" -> Parameters.set_locality Directed
     | "Local" -> Parameters.set_locality Local
     | "Global" -> Parameters.set_locality Global
-    | _ -> raise @@ Arg.Help "The --locality option requires one of the following values: Global, Local or Directed"
+    | _ ->
+        raise
+        @@ Arg.Help
+             "The --locality option requires one of the following values: Global, Local or Directed"
   in
 
   let _ =
-      match !mem_size_option with
-       | "inf"
-       | "Inf" -> Parameters.set_max_addr Infinite_z.Inf
-       | "" -> ()
-       | s ->
-         let n = (Z.of_string s) in
-         if Z.(n < ~$0)
-         then (Printf.eprintf "Size of memory must be positive (%s)" s; exit 1)
-         else Parameters.set_max_addr (Infinite_z.Int n)
+    match !mem_size_option with
+    | "inf" | "Inf" -> Parameters.set_max_addr Infinite_z.Inf
+    | "" -> ()
+    | s ->
+        let n = Z.of_string s in
+        if Z.(n < ~$0) then (
+          Printf.eprintf "Size of memory must be positive (%s)" s;
+          exit 1)
+        else Parameters.set_max_addr (Infinite_z.Int n)
   in
 
   let filename_prog =
     match !input_files with
-    | [filename] -> filename
+    | [ filename ] -> filename
     | _ ->
-      Printf.eprintf "%s\n" usage_msg;
-      exit 1
+        Printf.eprintf "%s\n" usage_msg;
+        exit 1
   in
 
   (mode, filename_prog, !regfile_name_option)
diff --git a/lib/dune b/lib/dune
@@ -1,6 +1,8 @@
 (library
- (name        libinterp)
+ (name libinterp)
  (libraries containers notty notty.unix zarith))
 
 (ocamllex lexer lexer_regfile)
-(menhir (modules parser parser_regfile) )
+
+(menhir
+ (modules parser parser_regfile))