blob: 4f9e0fe3e25545ee16bd4d6bff84e34ddac705c7 (
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
131
|
open import Pervasives_extra
open import Sail_impl_base
open import Sail_values
open import Sail_operators_bitlists
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)))
val uint : list bitU -> integer
let uint = unsigned
val sint : list bitU -> integer
let sint = signed
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 bits = bits_of_int (hi + 1) n in
get_bits false bits hi lo
val get_slice_int : integer -> integer -> integer -> list bitU
let get_slice_int len n lo = of_bits (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 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)
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
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
val hex_slice : string -> integer -> integer -> list bitU
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
val undefined_vector : forall 'a. integer -> 'a -> list 'a
let undefined_vector len u = repeat [u] len
val undefined_bitvector : integer -> list bitU
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)
|
