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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
|
open Big_int
type 'a return = { return : 'b . 'a -> 'b }
let with_return (type t) (f : _ -> t) =
let module M =
struct exception Return of t end
in
let return = { return = (fun x -> raise (M.Return x)); } in
try f return with M.Return x -> x
type bit = B0 | B1
let and_bit = function
| B1, B1 -> B1
| _, _ -> B0
let or_bit = function
| B0, B0 -> B0
| _, _ -> B1
let and_vec (xs, ys) =
assert (List.length xs = List.length ys);
List.map2 (fun x y -> and_bit (x, y)) xs ys
let and_bool (b1, b2) = b1 && b2
let or_vec (xs, ys) =
assert (List.length xs = List.length ys);
List.map2 (fun x y -> or_bit (x, y)) xs ys
let or_bool (b1, b2) = b1 || b2
let undefined_bit () =
if Random.bool () then B0 else B1
let undefined_bool () = Random.bool ()
let rec undefined_vector (start_index, len, item) =
if eq_big_int len zero_big_int
then []
else item :: undefined_vector (start_index, sub_big_int len unit_big_int, item)
let undefined_string () = ""
let undefined_unit () = ()
let undefined_int () =
big_int_of_int (Random.int 0xFFFF)
let internal_pick list =
List.nth list (Random.int (List.length list))
let eq_int (n, m) = eq_big_int n m
let eq_string (str1, str2) = String.compare str1 str2 = 0
let concat_string (str1, str2) = str1 ^ str2
let rec drop n xs =
match n, xs with
| 0, xs -> xs
| n, [] -> []
| n, (x :: xs) -> drop (n -1) xs
let rec take n xs =
match n, xs with
| 0, xs -> []
| n, (x :: xs) -> x :: take (n - 1) xs
| n, [] -> []
let subrange (list, n, m) =
let n = int_of_big_int n in
let m = int_of_big_int m in
List.rev (take (n - (m - 1)) (drop m (List.rev list)))
let eq_list (xs, ys) = List.for_all2 (fun x y -> x == y) xs ys
let access (xs, n) = List.nth (List.rev xs) (int_of_big_int n)
let append (xs, ys) = xs @ ys
let update (xs, n, x) =
let n = int_of_big_int n in
take n xs @ [x] @ drop (n + 1) xs
let update_subrange (xs, n, m, ys) =
let n = int_of_big_int n in
let m = int_of_big_int m in
assert false
let length xs = big_int_of_int (List.length xs)
let big_int_of_bit = function
| B0 -> zero_big_int
| B1 -> unit_big_int
let uint xs =
let uint_bit x (n, pos) =
add_big_int n (mult_big_int (power_int_positive_int 2 pos) (big_int_of_bit x)), pos + 1
in
fst (List.fold_right uint_bit xs (zero_big_int, 0))
let sint = function
| [] -> zero_big_int
| [msb] -> minus_big_int (big_int_of_bit msb)
| msb :: xs ->
let msb_pos = List.length xs in
let complement =
minus_big_int (mult_big_int (power_int_positive_int 2 msb_pos) (big_int_of_bit msb))
in
add_big_int complement (uint xs)
let add (x, y) = add_big_int x y
let sub (x, y) = sub_big_int x y
let mult (x, y) = mult_big_int x y
let quotient (x, y) = fst (quomod_big_int x y)
let modulus (x, y) = snd (quomod_big_int x y)
let add_bit_with_carry (x, y, carry) =
match x, y, carry with
| B0, B0, B0 -> B0, B0
| B0, B1, B0 -> B1, B0
| B1, B0, B0 -> B1, B0
| B1, B1, B0 -> B0, B1
| B0, B0, B1 -> B1, B0
| B0, B1, B1 -> B0, B1
| B1, B0, B1 -> B0, B1
| B1, B1, B1 -> B1, B1
let not_bit = function
| B0 -> B1
| B1 -> B0
let not_vec xs = List.map not_bit xs
let add_vec_carry (xs, ys) =
assert (List.length xs = List.length ys);
let (carry, result) =
List.fold_right2 (fun x y (c, result) -> let (z, c) = add_bit_with_carry (x, y, c) in (c, z :: result)) xs ys (B0, [])
in
carry, result
let add_vec (xs, ys) = snd (add_vec_carry (xs, ys))
let rec replicate_bits (bits, n) =
if eq_big_int n zero_big_int
then []
else bits @ replicate_bits (bits, sub_big_int n unit_big_int)
let identity x = x
let get_slice_int (n, m, o) = assert false
let hex_slice (str, n, m) = assert false
let putchar n = print_endline (string_of_big_int n)
let write_ram (addr_size, data_size, hex_ram, addr, data) =
assert false
let read_ram (addr_size, data_size, hex_ram, addr) =
assert false
(* FIXME: Casts can't be externed *)
let zcast_unit_vec x = [x]
let shl_int (n, m) = assert false
let shr_int (n, m) = assert false
|
