blob: 1e91dd314ea2f0a444f3fc7b95997369e4302db3 (
plain)
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
|
open import Pervasives_extra
open import Sail2_instr_kinds
open import Sail2_values
open import Sail2_operators_mwords
open import Sail2_prompt_monad
open import Sail2_prompt
type ty512
instance (Size ty512) let size = 512 end
declare isabelle target_rep type ty512 = `512`
declare hol target_rep type ty512 = `512`
type ty1024
instance (Size ty1024) let size = 1024 end
declare isabelle target_rep type ty1024 = `1024`
declare hol target_rep type ty1024 = `1024`
type ty2048
instance (Size ty2048) let size = 2048 end
declare isabelle target_rep type ty2048 = `2048`
declare hol target_rep type ty2048 = `2048`
let hexchar_to_bool_list c =
if c = #'0' then Just ([false;false;false;false])
else if c = #'1' then Just ([false;false;false;true ])
else if c = #'2' then Just ([false;false;true; false])
else if c = #'3' then Just ([false;false;true; true ])
else if c = #'4' then Just ([false;true; false;false])
else if c = #'5' then Just ([false;true; false;true ])
else if c = #'6' then Just ([false;true; true; false])
else if c = #'7' then Just ([false;true; true; true ])
else if c = #'8' then Just ([true; false;false;false])
else if c = #'9' then Just ([true; false;false;true ])
else if c = #'A' then Just ([true; false;true; false])
else if c = #'a' then Just ([true; false;true; false])
else if c = #'B' then Just ([true; false;true; true ])
else if c = #'b' then Just ([true; false;true; true ])
else if c = #'C' then Just ([true; true; false;false])
else if c = #'c' then Just ([true; true; false;false])
else if c = #'D' then Just ([true; true; false;true ])
else if c = #'d' then Just ([true; true; false;true ])
else if c = #'E' then Just ([true; true; true; false])
else if c = #'e' then Just ([true; true; true; false])
else if c = #'F' then Just ([true; true; true; true ])
else if c = #'f' then Just ([true; true; true; true ])
else Nothing
let hexstring_to_bools s =
match (toCharList s) with
| z :: x :: hs ->
let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
Maybe.map List.concat (just_list (List.map hexchar_to_bool_list str))
| _ -> Nothing
end
val hex_slice : forall 'rv 'n 'e. Size 'n => string -> integer -> integer -> monad 'rv (mword 'n) 'e
let hex_slice v len lo =
maybe_fail "hex_slice" (hexstring_to_bools v) >>= fun bs ->
let hi = len + lo - 1 in
let bs = ext_list false (len + lo) bs in
return (of_bools (subrange_list false bs hi lo))
val BigEndianReverse : forall 'rv 'n 'e. Size 'n => mword 'n -> monad 'rv (mword 'n) 'e
let BigEndianReverse w = return (reverse_endianness w)
let internal_pick vs = return (head vs)
(* Use constants for undefined values for now *)
let undefined_string () = return ""
let undefined_unit () = return ()
let undefined_int () = return (0:ii)
val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e
let undefined_vector len u = return (repeat [u] len)
val undefined_bitvector : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e
let undefined_bitvector len = return (of_bools (repeat [false] len))
val undefined_bits : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e
let undefined_bits = undefined_bitvector
let undefined_bit () = return B0
let undefined_real () = return (realFromFrac 0 1)
let undefined_range i j = return i
let undefined_atom i = return i
let undefined_nat () = return (0:ii)
val write_ram : forall 'rv 'a 'b 'c 'e. Size 'b, Size 'c =>
integer -> integer -> mword 'a -> mword 'b -> mword 'c -> monad 'rv unit 'e
let write_ram addrsize size hexRAM address value =
write_mem_ea Write_plain address size >>
write_mem_val value >>= fun _ ->
return ()
val read_ram : forall 'rv 'a 'b 'c 'e. Size 'b, Size 'c =>
integer -> integer -> mword 'a -> mword 'b -> monad 'rv (mword 'c) 'e
let read_ram addrsize size hexRAM address =
(*let _ = prerr_endline ("Reading " ^ (stringFromInteger size) ^ " bytes from address " ^ (stringFromInteger (unsigned address))) in*)
read_mem Read_plain address size
val elf_entry : unit -> integer
let elf_entry () = 0
declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry`
|
