blob: c9ea84e24e399f038c382248cd5a63347bcffcdf (
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
126
127
128
129
130
|
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 prerr_endline : string -> unit
let prerr_endline _ = ()
declare ocaml target_rep function prerr_endline = `prerr_endline`
val print_int : string -> integer -> unit
let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
val putchar : integer -> unit
let putchar _ = ()
declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
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 = bit_list_of_int n in
let len_n = max (hi + 1) (integerFromNat (List.length bs)) in
let ext_bs = exts_bits len_n bs in
maybe_failwith (signed (update_subrange_list false ext_bs hi lo (bits_of 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)
let write_ram addrsize size hexRAM address value =
write_mem_ea Write_plain address size >>
write_mem_val value >>= fun _ ->
return ()
let read_ram addrsize size hexRAM address =
read_mem Read_plain address size
|
