diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile | 2 | ||||
| -rwxr-xr-x | src/test/hello6 | bin | 0 -> 1470 bytes | |||
| -rw-r--r-- | src/test/run_power.ml | 16 |
3 files changed, 13 insertions, 5 deletions
diff --git a/src/Makefile b/src/Makefile index cc651e21..93cad76c 100644 --- a/src/Makefile +++ b/src/Makefile @@ -30,7 +30,7 @@ power: sail interpreter cd _build/elf_model ;\ $(LEM) -ocaml -only_changed_output missing_pervasives.lem show.lem endianness.lem bitstring.lem elf_types.lem elf_interpreted_segment.lem elf_header.lem elf_file1.lem elf_program_header_table.lem elf_executable_file2.lem elf_section_header_table.lem elf_executable_file3.lem string_table.lem elf_executable_file4.lem elf_executable_file5.lem sail_interface.lem main.lem ;\ ocamlfind ocamlopt -package bitstring.syntax -package batteries -package uint -package bitstring -syntax camlp4o -I $(LEMLIB) nat_num.cmx lem.cmx lem_function.cmx lem_list.cmx -linkpkg missing_pervasives.ml show.ml endianness.ml error.ml ml_bindings.ml bitstring_local.ml elf_types.ml elf_header.ml elf_file1.ml elf_program_header_table.ml elf_executable_file2.ml string_table.ml elf_section_header_table.ml elf_executable_file3.ml elf_executable_file4.ml elf_interpreted_segment.ml elf_executable_file5.ml sail_interface.ml main.ml ;\ - ocamlfind ocamlopt -package batteries -package uint -package bitstring -I $(LEMLIB) -a -o elf_extract.cmxa nat_num.cmx lem.cmx lem_function.cmx lem_list.cmx missing_pervasives.cmx show.cmx endianness.cmx error.cmx ml_bindings.cmx bitstring_local.cmx elf_types.cmx elf_header.cmx elf_file1.cmx elf_program_header_table.cmx elf_executable_file2.cmx + ocamlfind ocamlopt -package batteries -package uint -package bitstring -I $(LEMLIB) -a -o elf_extract.cmxa missing_pervasives.cmx show.cmx endianness.cmx error.cmx ml_bindings.cmx bitstring_local.cmx elf_types.cmx elf_header.cmx elf_file1.cmx elf_program_header_table.cmx elf_executable_file2.cmx string_table.cmx elf_section_header_table.cmx elf_executable_file3.cmx elf_executable_file4.cmx elf_interpreted_segment.cmx elf_executable_file5.cmx sail_interface.cmx cd _build/test ;\ ../../sail.native -lem_ast power.sail ;\ $(LEM) -ocaml -only_changed_output -lib ../lem_interp/ power.lem;\ diff --git a/src/test/hello6 b/src/test/hello6 Binary files differnew file mode 100755 index 00000000..4eb7db0a --- /dev/null +++ b/src/test/hello6 diff --git a/src/test/run_power.ml b/src/test/run_power.ml index be11ce4d..57f8ce2e 100644 --- a/src/test/run_power.ml +++ b/src/test/run_power.ml @@ -63,6 +63,10 @@ let load_section ic (offset,size,addr) = done ;; +let load_memory (bits,addr) = + let (Error.Success(bitsnum,_)) = Ml_bindings.read_unsigned_char Endianness.default_endianness bits in + add_mem (Uint32.to_int bitsnum) (Big_int.big_int_of_int addr) + (* use zero as a sentinel --- it might prevent a minimal loop from * working in principle, but won't happen in practice *) let lr_init_value = Big_int.zero_big_int @@ -133,15 +137,19 @@ let run () = exit 1; end; if !eager_eval then Run_interp_model.debug := true; - let ic = open_in_bin !file in +(* let ic = open_in_bin !file in if !sections = [] then begin sections := [(0, in_channel_length ic, Big_int.zero_big_int)]; end; - let total_size = List.fold_left (fun n (_,s,_) -> n+s) 0 !sections in + let total_size = List.fold_left (fun n (_,s,_) -> n+s) 0 !sections in*) + let (locations,start_address) = populate !file in + mainaddr := Printf.sprintf "0x%x" start_address; + let total_size = 8 * (List.length locations) in eprintf "Loading binary into memory (%d bytes)... %!" total_size; - let t = time_it (List.iter (load_section ic)) !sections in +(* let t = time_it (List.iter (load_section ic)) !sections in*) + let t = time_it (List.iter load_memory) locations in eprintf "done. (%f seconds)\n%!" t; - close_in ic; +(* close_in ic;*) let reg = init_reg () in (* entry point: unit -> unit fde *) let funk_name = "fde" in |