Merge branch 'master' of bitbucket.org:Peter_Sewell/l2

Conflicts:
	src/Makefile

1 files changed, 15 insertions, 10 deletions

diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 9d0af83d..c971550d 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -46,7 +46,7 @@ let rec load_memory_segment' (bytes,addr) mem =
 
 let rec load_memory_segment (segment: Elf_interpreted_segment.elf64_interpreted_segment) mem =
   let (Byte_sequence.Sequence bytes) = segment.Elf_interpreted_segment.elf64_segment_body in
-  let addr = segment.Elf_interpreted_segment.elf64_segment_base in
+  let addr = segment.Elf_interpreted_segment.elf64_segment_paddr in
   load_memory_segment' (bytes,addr) mem
 
 
@@ -447,7 +447,7 @@ let initial_stack_and_reg_data_of_AAarch64_elf_file e_entry all_data_memory =
 let mips_register_data_all =  [
   (*Pseudo registers*)
   ("branchPending", (D_decreasing, 1, 0));
-  ("exceptionSignalled", (D_decreasing, 1, 0));
+  ("inBranchDelay", (D_decreasing, 1, 0));
   ("delayedPC", (D_decreasing, 64, 63));
   ("nextPC", (D_decreasing, 64, 63));
   (* General purpose registers *)
@@ -490,6 +490,8 @@ let mips_register_data_all =  [
   ("CP0Status", (D_decreasing, 32, 31));
   ("CP0Cause", (D_decreasing, 32, 31));
   ("CP0EPC", (D_decreasing, 64, 63));
+  ("CP0LLAddr", (D_decreasing, 64, 63));
+  ("CP0LLBit", (D_decreasing, 1, 0));
 ]
 
 let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory =
@@ -860,7 +862,7 @@ let set_next_instruction_address model =
 
 let add1 = Nat_big_num.add (Nat_big_num.of_int 1)
 
-let fetch_instruction_opcode_and_update_ia model =
+let fetch_instruction_opcode_and_update_ia model addr_trans =
   match model with
   | PPC ->
     let cia = Reg.find "CIA" !reg in
@@ -902,7 +904,10 @@ let fetch_instruction_opcode_and_update_ia model =
     let pc_addr = address_of_register_value nextPC in
     (match pc_addr with
     | Some pc_addr ->
-      let pc_a = integer_of_address pc_addr in
+      let pc_a = match addr_trans 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")
@@ -924,7 +929,7 @@ let get_pc_address = function
   | AArch64 -> Reg.find "_PC" !reg
         
 
-let rec fde_loop count context model mode track_dependencies opcode =
+let rec fde_loop count context model mode track_dependencies opcode 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
@@ -956,8 +961,8 @@ let rec fde_loop count context model mode track_dependencies opcode =
         | true, mode, track_dependencies, (my_reg, my_mem) ->
           reg := my_reg;
           prog_mem := my_mem;
-          let opcode = fetch_instruction_opcode_and_update_ia model in
-          fde_loop (count + 1) context model (Some mode) (ref track_dependencies) opcode
+          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
   end
   
@@ -982,8 +987,8 @@ let run () =
           endian mode, and translate function name 
   *)
   let addr_trans = translate_address context E_big_endian "TranslateAddress" in
-  let startaddr,startaddr_internal = match addr_trans startaddr_internal with
-    | Some a, _ -> integer_of_address a, a
+  let startaddr = match addr_trans startaddr_internal 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
@@ -999,7 +1004,7 @@ let run () =
   
   (* 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) () in
+  let t = time_it (fun () -> fde_loop 0 context isa_model (Some Run) (ref false) initial_opcode addr_trans) () in
   resultf "Execution time for file %s: %f seconds\n" name t;;
 
 run () ;;