From 7786a0bfe4a49eab3dbeacc5815b4ddd26a014d0 Mon Sep 17 00:00:00 2001
From: Bastien Rousseau <bastien.rousseau@cs.au.dk>
Date: Thu, 6 Jun 2024 10:35:58 +0200
Subject: [PATCH] add sanity check initial machine configuration

---
 lib/machine.ml     | 36 ++++++++++++++++++++++++++++++++++++
 lib/program.ml     | 12 ++++++++----
 src/interpreter.ml | 13 +++++++++++--
 3 files changed, 55 insertions(+), 6 deletions(-)

diff --git a/lib/machine.ml b/lib/machine.ml
index 7a9a1f8..f09474c 100644
--- a/lib/machine.ml
+++ b/lib/machine.ml
@@ -4,6 +4,7 @@ open Ast
 let ( ~$ ) = Z.( ~$ )
 
 exception NotYetImplemented
+exception CheckInitFailed of Ast.word
 
 module MemMap = Map.Make (Z)
 
@@ -25,6 +26,12 @@ let arch_root_memory_perm = PermSet.of_list [ R; W; WL ]
 (* - executable root, EX_LD_LG_LM_MC_SR --> R_X_SR *)
 let arch_root_executable_perm = PermSet.of_list [ R; X; SR ]
 
+let get_perm (w : Ast.word) : Ast.PermSet.t =
+  match w with
+  | I _ -> Ast.PermSet.empty
+  | Sealable (Cap (p, _, _, _, _)) | Sealed (_, Cap (p, _, _, _, _)) -> p
+  | _ -> Ast.PermSet.empty
+
 let is_derived_from (p_dst : PermSet.t) (p_src : PermSet.t) =
   if PermSet.equal p_dst p_src (* p <= p *) then true
   else if PermSet.mem E p_dst (* E <= RX *) then
@@ -36,9 +43,38 @@ let is_derived_from (p_dst : PermSet.t) (p_src : PermSet.t) =
     (* p_dst ⊆ p_src, except that we can add DI or DL *)
     PermSet.subset (PermSet.remove DL (PermSet.remove DI p_dst)) p_src
 
+let check_word_derived (w : Ast.word) : unit =
+  if is_derived_from (get_perm w) arch_root_executable_perm then ()
+  else if is_derived_from (get_perm w) arch_root_memory_perm then ()
+  else raise (CheckInitFailed w)
+
+let check_init_regfile (reg : Ast.word RegMap.t) : unit =
+  RegMap.iter (fun _ w -> check_word_derived w) reg
+
+let check_init_memory (mem : Ast.word MemMap.t) : unit =
+  MemMap.iter (fun _ w -> check_word_derived w) mem
+
 (* using a record to have notation similar to the paper *)
 type mchn = exec_state * exec_conf
 
+let check_init_config (m : mchn) : unit =
+  check_init_regfile (snd m).reg;
+  check_init_memory (snd m).mem
+
+let init_reg_state_zeros : reg_state =
+  let l =
+    let n = 30 in
+    List.init n (fun i -> (Reg (i + 1), I Z.zero))
+  in
+  let pc_init = [ (PC, I Z.zero) ] in
+  let cgp_init = [ (cgp, I Z.zero) ] in
+  let sealing_init =
+    let sealing_reg = Reg 0 in
+    [ (sealing_reg, I Z.zero) ]
+  in
+  let seq = List.to_seq (pc_init @ l @ sealing_init @ cgp_init) in
+  RegMap.of_seq seq
+
 let init_reg_state : reg_state =
   let start_heap_addr = ~$0 in
   let max_heap_addr = Parameters.get_max_addr () in
diff --git a/lib/program.ml b/lib/program.ml
index b461782..910882f 100644
--- a/lib/program.ml
+++ b/lib/program.ml
@@ -1,3 +1,5 @@
+open Machine
+
 let parse_prog (filename : string) : (Ast.t, string) Result.t =
   let input = open_in filename in
   try
@@ -9,7 +11,7 @@ let parse_prog (filename : string) : (Ast.t, string) Result.t =
     close_in input;
     Result.Error "Parsing Failed"
 
-let parse_regfile (filename : string) : (Ast.word Machine.RegMap.t, string) Result.t =
+let parse_regfile (filename : string) : (Ast.word RegMap.t, string) Result.t =
   let input = open_in filename in
   try
     let filebuf = Lexing.from_channel input in
@@ -21,8 +23,10 @@ let parse_regfile (filename : string) : (Ast.word Machine.RegMap.t, string) Resu
     close_in input;
     Result.Error "Parsing Failed"
 
-let init_machine (prog : Ast.t) (init_regs : Ast.word Machine.RegMap.t) : Machine.mchn =
+let init_machine (prog : Ast.t) (init_regs : Ast.word RegMap.t) : mchn =
   let addr_start = Z.(~$0) in
   (* TODO lookup the PC *)
-  let init_mems = Machine.init_mem_state addr_start prog in
-  Machine.init init_regs init_mems
+  let init_mems = init_mem_state addr_start prog in
+  let init_config = init init_regs init_mems in
+  check_init_config init_config;
+  init_config
diff --git a/src/interpreter.ml b/src/interpreter.ml
index ddf8ce4..d20cc7f 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -20,12 +20,21 @@ let () =
     if regfile_name = "" then init_regfile
     else
       match Program.parse_regfile regfile_name with
-      | Ok regs -> (Machine.RegMap.fold (fun r w rf -> Machine.RegMap.add r w rf) regs) init_regfile
+      | Ok regs ->
+          (Machine.RegMap.fold (fun r w rf -> Machine.RegMap.add r w rf) regs)
+            Machine.init_reg_state_zeros
       | Error msg ->
           Printf.eprintf "Regfile parse error: %s\n" msg;
           exit 1
   in
-  let m_init = Program.init_machine prog regfile in
+  let m_init =
+    try Program.init_machine prog regfile
+    with Machine.CheckInitFailed w ->
+      failwith
+        ("The word "
+        ^ Pretty_printer.string_of_ast_word w
+        ^ " is not derived from an architectural root.")
+  in
 
   match mode with
   | Cli_parser.Interactive_mode ->