fix mips build by copying across run_with_elf_cheri.ml and removing cheri parts.

1 files changed, 126 insertions, 78 deletions

diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 302f9eb2..ee9dfcc6 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -30,7 +30,9 @@ let add_mem byte addr mem =
   assert(byte >= 0 && byte < 256);
   (*Printf.printf "add_mem %s: 0x%02x\n" (Uint64.to_string_hex (Uint64.of_string (Nat_big_num.to_string addr))) byte;*)
   let mem_byte = memory_byte_of_int byte in
-  mem := Mem.add addr mem_byte !mem
+  let zero_byte = memory_byte_of_int 0 in
+  mem := Mem.add addr mem_byte !mem;
+  tag_mem := Mem.add addr zero_byte !tag_mem
 
 let get_reg reg name =
   let reg_content = Reg.find name reg in reg_content
@@ -447,6 +449,7 @@ let initial_stack_and_reg_data_of_AAarch64_elf_file e_entry all_data_memory =
 
 let mips_register_data_all =  [
   (*Pseudo registers*)
+  ("PC", (D_decreasing, 64, 63));
   ("branchPending", (D_decreasing, 1, 0));
   ("inBranchDelay", (D_decreasing, 1, 0));
   ("delayedPC", (D_decreasing, 64, 63));
@@ -863,6 +866,40 @@ let set_next_instruction_address model =
 
 let add1 = Nat_big_num.add (Nat_big_num.of_int 1)
 
+let get_addr_trans_regs _ =
+  Some([
+    (Interp_interface.Reg0("PC", 63, 64, Interp_interface.D_decreasing),    Reg.find "PC" !reg);
+    (Interp_interface.Reg0("CP0Status", 31, 32, Interp_interface.D_decreasing), Reg.find "CP0Status" !reg);
+    (Interp_interface.Reg0("inBranchDelay", 0, 1, Interp_interface.D_decreasing), Reg.find "inBranchDelay" !reg);
+  ])
+
+let get_opcode pc_a =
+  List.map (fun b -> match b with
+  | Some b -> b
+  | None -> failwith "A byte in opcode contained unknown or undef")
+    (List.map byte_of_memory_byte
+       ([Mem.find pc_a !prog_mem;
+         Mem.find (add1 pc_a) !prog_mem;
+         Mem.find (add1 (add1 pc_a)) !prog_mem;
+         Mem.find (add1 (add1 (add1 pc_a))) !prog_mem]))
+
+let rec write_events = function
+  | [] -> ()
+  | e::events ->
+    (match e with
+     | E_write_reg (Reg0(id,_,_,_), value) -> reg := Reg.add id value !reg
+     | E_write_reg ((Reg_slice(id,_,_,range) as reg_n),value) 
+     | E_write_reg ((Reg_field(id,_,_,_,range) as reg_n),value)->
+       let old_val = Reg.find id !reg in
+       let new_val = fupdate_slice reg_n old_val value range in
+       reg := Reg.add id new_val !reg
+     | E_write_reg((Reg_f_slice(id,_,_,_,range,mini_range) as reg_n),value) ->
+       let old_val = Reg.find id !reg in
+       let new_val = fupdate_slice reg_n old_val value (combine_slices range mini_range) in
+       reg := Reg.add id new_val !reg
+     | _ -> failwith "Only register write events expected");
+    write_events events
+
 let fetch_instruction_opcode_and_update_ia model addr_trans =
   match model with
   | PPC ->
@@ -871,14 +908,7 @@ let fetch_instruction_opcode_and_update_ia model addr_trans =
     (match cia_addr with
      | Some cia_addr ->
        let cia_a = integer_of_address cia_addr in
-       let opcode = List.map (fun b -> match b with
-           | Some b -> b
-           | None -> failwith "A byte in opcode contained unknown or undef")
-           (List.map byte_of_memory_byte
-              [Mem.find cia_a !prog_mem;
-               Mem.find (add1 cia_a) !prog_mem;
-               Mem.find (add1 (add1 cia_a)) !prog_mem;
-               Mem.find (add1 (add1 (add1 cia_a))) !prog_mem]) in
+       let opcode = (get_opcode cia_a) in
        begin
          reg := Reg.add "CIA" (Reg.find "NIA" !reg) !reg;
          Opcode opcode
@@ -890,38 +920,39 @@ let fetch_instruction_opcode_and_update_ia model addr_trans =
     (match pc_addr with
      | Some pc_addr ->
        let pc_a = integer_of_address pc_addr in
-       let opcode =  List.map (fun b -> match b with
-           | Some b -> b
-           | None -> failwith "A byte in opcode contained unknown or undef")
-           (List.map byte_of_memory_byte
-              ([Mem.find pc_a !prog_mem;
-                Mem.find (add1 pc_a) !prog_mem;
-                Mem.find (add1 (add1 pc_a)) !prog_mem;
-                Mem.find (add1 (add1 (add1 pc_a))) !prog_mem])) in
-       Opcode opcode       
+       let opcode = (get_opcode pc_a) in
+       Opcode opcode
      | None -> failwith "_PC address contains unknown or undefined")
   | MIPS -> 
+    begin
     let nextPC  = Reg.find "nextPC" !reg in
     let pc_addr = address_of_register_value nextPC in
+    (*let unused = interactf "PC: %s\n" (Printing_functions.register_value_to_string nextPC) in*)
     (match pc_addr with
     | Some pc_addr ->
-      let pc_a = match addr_trans None pc_addr with
-        | Some a, _ -> integer_of_address a
-        | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i))
-        | _ -> failwith "Neither an address or a code on translate address" in
-      let opcode = List.map (fun b -> match b with
-        | Some b -> b
-        | None -> failwith "A byte in opcode contained unknown or undef")
-        (List.map byte_of_memory_byte
-           (([Mem.find pc_a !prog_mem;
-                Mem.find (add1 pc_a) !prog_mem;
-                Mem.find (add1 (add1 pc_a)) !prog_mem;
-                Mem.find (add1 (add1 (add1 pc_a))) !prog_mem]))) in
+      let pc_a = match addr_trans (get_addr_trans_regs ()) pc_addr with
+        | Some a, Some events -> write_events (List.rev events); integer_of_address a
+        | Some a, None -> integer_of_address a
+        | None, Some events ->
+          write_events (List.rev events);
+          let nextPC  = Reg.find "nextPC" !reg in
+          let pc_addr = address_of_register_value nextPC in
+          (match pc_addr with
+           | Some pc_addr ->
+             (match addr_trans (get_addr_trans_regs ()) pc_addr with
+              | Some a, Some events -> write_events (List.rev events); integer_of_address a
+              | Some a, None -> integer_of_address a
+              | None, _ -> failwith "Address translation failed twice")
+           | None -> failwith "no nextPc address")
+        | _ -> failwith "No address and no events from translate address"
+      in
+      let opcode = (get_opcode pc_a) in
       begin
-        reg := Reg.add "PC" nextPC !reg;
+        reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg;
         Opcode opcode
       end
      | None -> errorf "nextPC contains unknown or undefined"; exit 1)
+    end
   |  _ -> assert false
 
 let get_pc_address = function
@@ -930,42 +961,73 @@ let get_pc_address = function
   | AArch64 -> Reg.find "_PC" !reg
         
 
-let rec fde_loop count context model mode track_dependencies opcode addr_trans =
+let option_int_of_reg str =
+  option_int_of_option_integer (integer_of_register_value (Reg.find str !reg))
+
+let rec fde_loop count context model mode track_dependencies addr_trans =
   if !max_cut_off && count = !max_instr
   then resultf "\nEnding evaluation due to reaching cut off point of %d instructions\n" count
   else begin
-    interactf "\n**** instruction %d from address %s ****\n"
-      count (Printing_functions.register_value_to_string (get_pc_address model));
     if !break_point && count = !break_instr then begin break_point := false; eager_eval := false end;
-    let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with
-      | Instr(instruction,istate) ->
-        interactf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction);
-        (instruction,istate)
-      | Decode_error d ->
-        (match d with
-         | Interp_interface.Unsupported_instruction_error instr ->
-           errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instr)
-         | Interp_interface.Not_an_instruction_error op ->
-           (match op with
-            | Opcode bytes ->
-              errorf "\n**** Encountered non-decodeable opcode: %s ****\n" (Printing_functions.byte_list_to_string bytes))
-         | Internal_error s -> errorf "\n**** Internal error on decode: %s ****\n" s);
-        exit 1
-    in
-    if stop_condition_met model instruction
-    then resultf "\nSUCCESS program terminated after %d instructions\n" count
-    else
-      begin
-        set_next_instruction_address model;
-        match Run_interp_model.run  istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with
-        | false, _,_, _ -> errorf "FAILURE\n"; exit 1
-        | true, mode, track_dependencies, (my_reg, my_mem, my_tags) ->
-          reg := my_reg;
-          prog_mem := my_mem;
-          tag_mem := my_tags;
-          let opcode = fetch_instruction_opcode_and_update_ia model addr_trans in
-          fde_loop (count + 1) context model (Some mode) (ref track_dependencies) opcode addr_trans
-      end
+    let pc_regval = get_pc_address model in
+    interactf "\n**** instruction %d from address %s ****\n"
+      count (Printing_functions.register_value_to_string pc_regval);
+    let pc_addr  = address_of_register_value pc_regval in
+    let pc_val = match pc_addr with
+      | Some v -> v
+      | None   -> failwith "pc contains undef or unknown" in
+    let m_paddr_int = match addr_trans (get_addr_trans_regs ()) pc_val with
+      | Some a, Some events -> write_events (List.rev events); Some (integer_of_address a)
+      | Some a, None        -> Some (integer_of_address a)
+      | None, Some events   -> write_events (List.rev events); None
+      | None, None          -> failwith "address translation failed and no writes" in
+    match m_paddr_int with
+      | Some pc ->
+          let inBranchDelay = option_int_of_reg "inBranchDelay" in
+          (match inBranchDelay with
+          | Some 0 -> 
+            let npc_addr = add_address_nat pc_val 4 in
+            let npc_reg = register_value_of_address npc_addr Interp_interface.D_decreasing in
+            reg := Reg.add "nextPC" npc_reg !reg;
+          | Some 1 ->
+            reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg;
+          | None   -> failwith "invalid value of inBranchDelay");
+          let opcode = Opcode (get_opcode pc) in
+          let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with
+            | Instr(instruction,istate) ->
+              interactf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction);
+              (instruction,istate)
+            | Decode_error d ->
+              (match d with
+              | Interp_interface.Unsupported_instruction_error instr ->
+                errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instr)
+              | Interp_interface.Not_an_instruction_error op ->
+                (match op with
+                | Opcode bytes ->
+                  errorf "\n**** Encountered non-decodeable opcode: %s ****\n" (Printing_functions.byte_list_to_string bytes))
+              | Internal_error s -> errorf "\n**** Internal error on decode: %s ****\n" s); exit 1
+          in
+          if stop_condition_met model instruction
+          then resultf "\nSUCCESS program terminated after %d instructions\n" count
+          else
+            begin
+              match Run_interp_model.run  istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with
+              | false, _,_, _ -> errorf "FAILURE\n"; exit 1
+              | true, mode, track_dependencies, (my_reg, my_mem, my_tags) ->
+                reg := my_reg;
+                prog_mem := my_mem;
+                tag_mem := my_tags;
+                reg := Reg.add "inBranchDelay" (Reg.find "branchPending" !reg) !reg;
+                reg := Reg.add "branchPending" (register_value_of_integer 1 0 Interp_interface.D_decreasing Nat_big_num.zero) !reg;
+                reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg;
+                fde_loop (count + 1) context model (Some mode) (ref track_dependencies) addr_trans
+            end
+      | None -> begin
+      reg := Reg.add "inBranchDelay" (Reg.find "branchPending" !reg) !reg;
+      reg := Reg.add "branchPending" (register_value_of_integer 1 0 Interp_interface.D_decreasing Nat_big_num.zero) !reg;
+      reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg;
+      fde_loop (count + 1) context model mode track_dependencies addr_trans
+    end
   end
   
 let run () =
@@ -989,24 +1051,10 @@ let run () =
           endian mode, and translate function name 
   *)
   let addr_trans = translate_address context E_big_endian "TranslateAddress" in
-  let startaddr = match addr_trans None startaddr_internal with
-    | Some a, events -> integer_of_address a
-    | None, events -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i))
-    | _ -> failwith "Neither an address or a code on translate address"
-  in
-  let initial_opcode = Opcode (List.map (fun b -> match b with
-      | Some b -> b
-      | None -> errorf "A byte in opcode contained unknown or undef"; exit 1)
-      (List.map byte_of_memory_byte
-         [Mem.find startaddr !prog_mem;
-          Mem.find (add1 startaddr) !prog_mem;
-          Mem.find (add1 (add1 startaddr)) !prog_mem;
-          Mem.find (add1 (add1 (add1 startaddr))) !prog_mem])) in
   reg := Reg.add "PC" (register_value_of_address startaddr_internal model_reg_d ) !reg;
-  
   (* entry point: unit -> unit fde *)
   let name = Filename.basename !file in
-  let t = time_it (fun () -> fde_loop 0 context isa_model (Some Run) (ref false) initial_opcode addr_trans) () in
+  let t = time_it (fun () -> fde_loop 0 context isa_model (Some Run) (ref false)  addr_trans) () in
   resultf "Execution time for file %s: %f seconds\n" name t;;
 
 run () ;;