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

Conflicts:
	src/Makefile

3 files changed, 21 insertions, 12 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 400bbd8e..df5413ae 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -686,9 +686,13 @@ let library_functions direction = [
   ("bitwise_rightshift", shift_op_vec ">>");
   ("bitwise_rotate", shift_op_vec "<<<");
   ("modulo", arith_op_no0 (mod));
+  ("mod_signed", arith_op_no0 hardware_mod);
   ("mod_vec", arith_op_vec_no0 hardware_mod "mod" Unsigned 1);
   ("mod_vec_range", arith_op_vec_range_no0 hardware_mod "mod" Unsigned 1);
+  ("mod_signed_vec", arith_op_vec_no0 hardware_mod "mod" Signed 1);
+  ("mod_signed_vec_range", arith_op_vec_range_no0 hardware_mod "mod" Signed 1);
   ("quot", arith_op_no0 hardware_quot);
+  ("quot_signed", arith_op_no0 hardware_quot);
   ("quot_vec", arith_op_vec_no0 hardware_quot "quot" Unsigned 1);
   ("quot_overflow_vec", arith_op_overflow_vec_no0 hardware_quot "quot" Unsigned 1);
   ("quot_vec_signed", arith_op_vec_no0 hardware_quot "quot" Signed 1);
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 3703940a..a9a44dfe 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -285,7 +285,7 @@ let doc_exp, doc_let =
   and star_exp env add_red ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id (
       "*" | "/"
-    | "div" | "quot" | "rem" | "mod" | "quot_s"
+    | "div" | "quot" | "rem" | "mod" | "quot_s" | "mod_s" 
     | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) ->
       doc_op (doc_id op) (star_exp env add_red l) (starstar_exp env add_red r)
   | _ -> starstar_exp env add_red expr
@@ -410,7 +410,7 @@ let doc_exp, doc_let =
     | ">>" | ">>>" | "<<" | "<<<"
     | "+" | "+_s" | "-" | "-_s" 
     | "*" | "/"
-    | "div" | "quot" | "quot_s" | "rem" | "mod"
+    | "div" | "quot" | "quot_s" | "rem" | "mod" | "mod_s" 
     | "*_s" | "*_si" | "*_u" | "*_ui"
     | "**"), _))
     , _) ->
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 () ;;