diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 4 | ||||
| -rw-r--r-- | src/lem_interp/pretty_interp.ml | 4 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 25 |
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 () ;; |