blob: ab67f50640f7256234bda72d1906edb34159f83e (
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
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
|
open import Pervasives_extra
open import Sail_instr_kinds
open import Sail_values
open import Sail_operators_bitlists
open import Prompt_monad
open import Prompt
type ty512
instance (Size ty512) let size = 512 end
declare isabelle target_rep type ty512 = `512`
type ty1024
instance (Size ty1024) let size = 1024 end
declare isabelle target_rep type ty1024 = `1024`
type ty2048
instance (Size ty2048) let size = 2048 end
declare isabelle target_rep type ty2048 = `2048`
val slice : list bitU -> integer -> integer -> list bitU
let slice v lo len =
subrange_vec_dec v (lo + len - 1) lo
val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
update_subrange_vec_dec out (n + slice_len - 1) n v
let get_slice_int_bl len n lo =
(* TODO: Is this the intended behaviour? *)
let hi = lo + len - 1 in
let bs = bools_of_int (hi + 1) n in
subrange_list false bs hi lo
val get_slice_int : integer -> integer -> integer -> list bitU
let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
val set_slice_int : integer -> integer -> integer -> list bitU -> integer
let set_slice_int len n lo v =
let hi = lo + len - 1 in
let bs = bits_of_int (hi + 1) n in
maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo v))
(*let ext_slice signed v i j =
let len = length v in
let bits = get_bits false (bits_of v) i j in
of_bits (if signed then exts_bits len bits else extz_bits len bits)
val exts_slice : list bitU -> integer -> integer -> list bitU
let exts_slice v i j = ext_slice true v i j
val extz_slice : list bitU -> integer -> integer -> list bitU
let extz_slice v i j = ext_slice false v i j*)
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 'e. string -> integer -> integer -> monad 'rv (list bitU) 'e
let hex_slice v len lo =
match hexstring_to_bools v with
| Just 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))
| Nothing -> Fail "hex_slice"
end
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 'e. integer -> monad 'rv (list bitU) 'e
let undefined_bitvector len = return (of_bools (repeat [false] len))
val undefined_bits : forall 'rv 'e. integer -> monad 'rv (list bitU) '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 'e.
integer -> integer -> list bitU -> list bitU -> list bitU -> 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 'e.
integer -> integer -> list bitU -> list bitU -> monad 'rv (list bitU) 'e
let read_ram addrsize size hexRAM address =
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`
|
