blob: a9e2e9e3ba7ba41af46fd3b57d1f832da7d8cdac (
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
|
open import Pervasives_extra
open import Sail_impl_base
open import Sail_values
open import Sail_operators
open import State
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)))
let inline uint = unsigned
let inline sint = signed
let slice v lo len =
subrange_vec_dec v (lo + len - 1) lo
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 bits = bits_of_int (hi + 1) n in
get_bits false bits hi lo
let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
let set_slice_int len n lo v =
let hi = lo + len - 1 in
let bits = bitlist_of_int n in
let len_n = max (hi + 1) (integerFromNat (List.length bits)) in
let ext_bits = exts_bits len_n bits in
signed (set_bits false ext_bits 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)
let exts_slice v i j = ext_slice true v i j
let extz_slice v i j = ext_slice false v i j
val shr_int : ii -> ii -> ii
let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
val shl_int : integer -> integer -> integer
let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
let hexchar_to_bitlist c =
if c = #'0' then [B0;B0;B0;B0]
else if c = #'1' then [B0;B0;B0;B1]
else if c = #'2' then [B0;B0;B1;B0]
else if c = #'3' then [B0;B0;B1;B1]
else if c = #'4' then [B0;B1;B0;B0]
else if c = #'5' then [B0;B1;B0;B1]
else if c = #'6' then [B0;B1;B1;B0]
else if c = #'7' then [B0;B1;B1;B1]
else if c = #'8' then [B1;B0;B0;B0]
else if c = #'9' then [B1;B0;B0;B1]
else if c = #'A' then [B1;B0;B1;B0]
else if c = #'a' then [B1;B0;B1;B0]
else if c = #'B' then [B1;B0;B1;B1]
else if c = #'b' then [B1;B0;B1;B1]
else if c = #'C' then [B1;B1;B0;B0]
else if c = #'c' then [B1;B1;B0;B0]
else if c = #'D' then [B1;B1;B0;B1]
else if c = #'d' then [B1;B1;B0;B1]
else if c = #'E' then [B1;B1;B1;B0]
else if c = #'e' then [B1;B1;B1;B0]
else if c = #'F' then [B1;B1;B1;B1]
else if c = #'f' then [B1;B1;B1;B1]
else failwith "hexchar_to_bitlist given unrecognized character"
let hexstring_to_bits s =
match (toCharList s) with
| z :: x :: hs ->
let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
List.concat (List.map hexchar_to_bitlist str)
| _ -> failwith "hexstring_to_bits called with unexpected string"
end
let hex_slice v len lo =
let hi = len + lo - 1 in
let bits = extz_bits (len + lo) (hexstring_to_bits v) in
of_bits (get_bits false bits hi lo)
let internal_pick vs = head vs
let undefined_string () = ""
let undefined_unit () = ()
let undefined_int () = (0:ii)
let undefined_bool () = false
let undefined_vector len u = repeat [u] len
let undefined_bitvector len = duplicate B0 len
let undefined_bits len = undefined_bitvector len
let undefined_bit () = B0
let undefined_real () = realFromFrac 0 1
let undefined_range i j = i
let undefined_atom i = i
let undefined_nat () = (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 =
(*let _ = prerr_endline ("Reading " ^ (stringFromInteger size) ^ " bytes from address " ^ (stringFromInteger (unsigned address))) in*)
(*read_mem false Read_plain address size*)
undefined_bitvector (8 * size)
|
