diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/run_embed.ml | 202 |
1 files changed, 0 insertions, 202 deletions
diff --git a/mips/run_embed.ml b/mips/run_embed.ml index 62f5bb09..8b752f03 100644 --- a/mips/run_embed.ml +++ b/mips/run_embed.ml @@ -88,208 +88,6 @@ let add_mem byte addr mem = begin (*printf "MEM [%s] <- %x\n" (big_int_to_hex addr) byte;*) mem := Mem.add addr byte !mem end -(* -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_paddr in - load_memory_segment' bytes addr mem - -let rec load_memory_segments segments = - begin match segments with - | [] -> () - | segment::segments' -> - let (x,w,r) = segment.Elf_interpreted_segment.elf64_segment_flags in - begin - load_memory_segment segment mips_mem; - load_memory_segments segments' - end - end - -let initial_system_state_of_elf_file name = - - (* call ELF analyser on file *) - match Sail_interface.populate_and_obtain_global_symbol_init_info name with - | Error.Fail s -> failwith ("populate_and_obtain_global_symbol_init_info: " ^ s) - | Error.Success - (_, (elf_epi: Sail_interface.executable_process_image), - (symbol_map: Elf_file.global_symbol_init_info)) - -> - let (segments, e_entry, e_machine) = - begin match elf_epi with - | ELF_Class_32 _ -> failwith "cannot handle ELF_Class_32" - | ELF_Class_64 (segments,e_entry,e_machine) -> - (* remove all the auto generated segments (they contain only 0s) *) - let segments = - Lem_list.mapMaybe - (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None) - segments - in - (segments,e_entry,e_machine) - end - in - (* construct program memory and start address *) - begin - load_memory_segments segments; - (* - debugf "prog_mem\n"; - Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) !prog_mem; - debugf "data_mem\n"; - Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) !data_mem; - *) - let (isa_defs, isa_memory_access, isa_externs, isa_model, model_reg_d, startaddr, - initial_stack_data, initial_register_abi_data, register_data_all) = - match Nat_big_num.to_int e_machine with - | 8 (* EM_MIPS *) -> - let startaddr = - let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in - match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with - | Error.Fail s -> failwith "Failed computing entry point" - | Error.Success s -> s - in - let (initial_stack_data, initial_register_abi_data) = - initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in - - (Mips.defs, - (Mips_extras.read_memory_functions, - Mips_extras.memory_writes, - Mips_extras.memory_eas, - Mips_extras.memory_vals, - Mips_extras.barrier_functions), - [], - MIPS, - D_decreasing, - startaddr, - initial_stack_data, - initial_register_abi_data, - mips_register_data_all) - - | _ -> failwith (Printf.sprintf "Sail sequential interpreter can't handle the e_machine value %s, only EM_MIPS is supported." (Nat_big_num.to_string e_machine)) - in - - (* pull the object symbols from the symbol table *) - let symbol_table : (string * Nat_big_num.num * int * word8 list (*their bytes*)) list = - let rec convert_symbol_table symbol_map = - begin match symbol_map with - | [] -> [] - | ((name: string), - ((typ: Nat_big_num.num), - (size: Nat_big_num.num (*number of bytes*)), - (address: Nat_big_num.num), - (mb: Byte_sequence.byte_sequence option (*present iff type=stt_object*)), - (binding: Nat_big_num.num))) - (* (mb: Byte_sequence_wrapper.t option (*present iff type=stt_object*)) )) *) - ::symbol_map' -> - if Nat_big_num.equal typ Elf_symbol_table.stt_object && not (Nat_big_num.equal size (Nat_big_num.of_int 0)) - then - (, - (* an object symbol - map *) - (*Printf.printf "*** size %d ***\n" (Nat_big_num.to_int size);*) - let bytes = - (match mb with - | None -> raise (Failure "this cannot happen") - | Some (Sequence bytes) -> - List.map (fun (c:char) -> Char.code c) bytes) in - (name, address, List.length bytes, bytes):: convert_symbol_table symbol_map' - ) - else - (* not an object symbol or of zero size - ignore *) - convert_symbol_table symbol_map' - end - in - (List.map (fun (n,a,bs) -> (n,a,List.length bs,bs)) initial_stack_data) @ convert_symbol_table symbol_map - in - - (* invert the symbol table to use for pp *) - let symbol_table_pp : ((Sail_impl_base.address * int) * string) list = - (* map symbol to (bindings, footprint), - if a symbol appears more then onece keep the one with higher - precedence (stb_global > stb_weak > stb_local) *) - let map = - List.fold_left - (fun map (name, (typ, size, address, mb, binding)) -> - if String.length name <> 0 && - (if String.length name = 1 then Char.code (String.get name 0) <> 0 else true) && - not (Nat_big_num.equal address (Nat_big_num.of_int 0)) - then - try - let (binding', _) = StringMap.find name map in - if Nat_big_num.equal binding' Elf_symbol_table.stb_local || - Nat_big_num.equal binding Elf_symbol_table.stb_global - then - StringMap.add name (binding, - (Sail_impl_base.address_of_integer address, Nat_big_num.to_int size)) map - else map - with Not_found -> - StringMap.add name (binding, - (Sail_impl_base.address_of_integer address, Nat_big_num.to_int size)) map - - else map - ) - StringMap.empty - symbol_map - in - - List.map (fun (name, (binding, fp)) -> (fp, name)) (StringMap.bindings map) - in - - - (* Now we examine the rest of the data memory, - removing the footprint of the symbols and chunking it into aligned chunks *) - - let rec remove_symbols_from_data_memory data_mem symbols = - match symbols with - | [] -> data_mem - | (name,address,size,bs)::symbols' -> - let data_mem' = - Mem.filter - (fun a v -> - not (Nat_big_num.greater_equal a address && - Nat_big_num.less a (Nat_big_num.add (Nat_big_num.of_int (List.length bs)) address))) - data_mem in - remove_symbols_from_data_memory data_mem' symbols' in - - let trimmed_data_memory : (Nat_big_num.num * memory_byte) list = - Mem.bindings (remove_symbols_from_data_memory !data_mem symbol_table) in - - (* make sure that's ordered increasingly.... *) - let trimmed_data_memory = - List.sort (fun (a,b) (a',b') -> Nat_big_num.compare a a') trimmed_data_memory in - - let aligned a n = (* a mod n = 0 *) - let n_big = Nat_big_num.of_int n in - Nat_big_num.equal (Nat_big_num.modulus a n_big) ((Nat_big_num.of_int 0)) in - - let isplus a' a n = (* a' = a+n *) - Nat_big_num.equal a' (Nat_big_num.add (Nat_big_num.of_int n) a) in - - - let initial_register_state = - fun rbn -> - try - List.assoc rbn initial_register_abi_data - with - Not_found -> - (register_state_zero register_data_all) rbn - in - - begin - (initial_reg_file register_data_all initial_register_state); - - (* construct initial system state *) - let initial_system_state = - (isa_defs, - isa_memory_access, - isa_externs, - isa_model, - model_reg_d, - startaddr, - (Sail_impl_base.address_of_integer startaddr)) - in - - (initial_system_state, symbol_table_pp) - end - end - *) let max_cut_off = ref false let max_instr = ref 0 |