remove unsed code for elf file loading in run_embed.

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