1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(**************************************************************************)
(* Sail *)
(* *)
(* Copyright (c) 2013-2017 *)
(* Kathyrn Gray *)
(* Shaked Flur *)
(* Stephen Kell *)
(* Gabriel Kerneis *)
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
(* Alasdair Armstrong *)
(* *)
(* All rights reserved. *)
(* *)
(* This software was developed by the University of Cambridge Computer *)
(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
(* *)
(* Redistribution and use in source and binary forms, with or without *)
(* modification, are permitted provided that the following conditions *)
(* are met: *)
(* 1. Redistributions of source code must retain the above copyright *)
(* notice, this list of conditions and the following disclaimer. *)
(* 2. Redistributions in binary form must reproduce the above copyright *)
(* notice, this list of conditions and the following disclaimer in *)
(* the documentation and/or other materials provided with the *)
(* distribution. *)
(* *)
(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
(* SUCH DAMAGE. *)
(**************************************************************************)
open Big_int
let opt_file_arguments = ref ([] : string list)
let opt_elf_threads = ref 1
let opt_elf_entry = ref zero_big_int
let options = Arg.align []
let usage_msg = "Sail OCaml RTS options:"
let () =
Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg
type word8 = int
let escape_char c =
if int_of_char c <= 31 then '.'
else if int_of_char c >= 127 then '.'
else c
let hex_line bs =
let hex_char i c =
(if i mod 2 == 0 && i <> 0 then " " else "") ^ Printf.sprintf "%02x" (int_of_char c)
in
String.concat "" (List.mapi hex_char bs) ^ " " ^ String.concat "" (List.map (fun c -> Printf.sprintf "%c" (escape_char c)) bs)
let rec break n = function
| [] -> []
| (_ :: _ as xs) -> [Lem_list.take n xs] @ break n (Lem_list.drop n xs)
let print_segment seg =
let (Byte_sequence.Sequence bs) = seg.Elf_interpreted_segment.elf64_segment_body in
prerr_endline "0011 2233 4455 6677 8899 aabb ccdd eeff 0123456789abcdef";
List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 bs)
let read name =
let info = Sail_interface.populate_and_obtain_global_symbol_init_info name in
prerr_endline "Elf read:";
let (elf_file, elf_epi, symbol_map) =
begin match info with
| Error.Fail s -> failwith (Printf.sprintf "populate_and_obtain_global_symbol_init_info: %s" s)
| Error.Success ((elf_file: Elf_file.elf_file),
(elf_epi: Sail_interface.executable_process_image),
(symbol_map: Elf_file.global_symbol_init_info))
->
prerr_endline (Sail_interface.string_of_executable_process_image elf_epi);
(elf_file, elf_epi, symbol_map)
end
in
prerr_endline "\nElf segments:";
let (segments, e_entry, e_machine) =
begin match elf_epi, elf_file with
| (Sail_interface.ELF_Class_32 _, _) -> failwith "cannot handle ELF_Class_32"
| (_, Elf_file.ELF_File_32 _) -> failwith "cannot handle ELF_File_32"
| (Sail_interface.ELF_Class_64 (segments, e_entry, e_machine), Elf_file.ELF_File_64 f1) ->
(* 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, big_int_of_string (Nat_big_num.to_string e_entry),e_machine)
end
in
(segments, e_entry)
let load_segment seg =
let open Elf_interpreted_segment in
let (Byte_sequence.Sequence bs) = seg.elf64_segment_body in
let paddr = big_int_of_string (Nat_big_num.to_string (seg.elf64_segment_paddr)) in
let base = big_int_of_string (Nat_big_num.to_string (seg.elf64_segment_base)) in
let offset = big_int_of_string (Nat_big_num.to_string (seg.elf64_segment_offset)) in
prerr_endline "\nLoading Segment";
prerr_endline ("Segment offset: " ^ string_of_big_int offset);
prerr_endline ("Segment base address: " ^ string_of_big_int base);
prerr_endline ("Segment physical address: " ^ string_of_big_int paddr);
print_segment seg;
List.iteri (fun i byte -> Sail_lib.wram (add_big_int paddr (big_int_of_int i)) byte) (List.map int_of_char bs)
let load_elf () =
match !opt_file_arguments with
| (name :: _) ->
let segments, e_entry = read name in
opt_elf_entry := e_entry;
List.iter load_segment segments
| [] -> ()
(* The sail model can access this by externing a unit -> int function
as Elf_loader.elf_entry. *)
let elf_entry () = !opt_elf_entry
|
