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
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
|
open import Pervasives
open import Interp
open import Interp_ast
import Assert_extra Maybe_extra (* For failwith for error reporting while debugging; and for fromJust when we know it's not Nothing *)
open import Num
open import List
open import Word
open import Bool
let ignore_sail x = V_lit (L_aux L_unit Unknown) ;;
let compose f g x = f (V_tuple [g x]) ;;
let zeroi = integerFromNat 0
let onei = integerFromNat 1
let twoi = integerFromNat 2
let rec sparse_walker update ni processed_length length ls df =
if processed_length = length
then []
else match ls with
| [] -> replicate (natFromInteger (length - processed_length)) df
| (i,v)::ls ->
if ni = i
then v::(sparse_walker update (update ni) (processed_length + 1) length ls df)
else df::(sparse_walker update (update ni) (processed_length + 1) length ((i,v)::ls) df)
end
let rec fill_in_sparse v = match v with
| V_vector_sparse first length inc ls df ->
V_vector first inc (sparse_walker (if inc then (fun (x: integer) -> x + onei) else (fun (x: integer) -> x - onei)) first zeroi length ls df)
| V_track v r -> taint (fill_in_sparse v) r
end
let is_one v = match v with
| V_lit (L_aux b lb) -> V_lit (L_aux (if b = L_one then L_true else L_false) lb)
| V_track (V_lit (L_aux b lb)) r -> V_track (V_lit (L_aux (if b = L_one then L_true else L_false) lb)) r
| V_unknown -> V_unknown
end ;;
let rec lt_range (V_tuple[v1;v2]) = match (v1,v2) with
| (V_lit (L_aux (L_num l1) lr),V_lit (L_aux (L_num l2) ll)) ->
if l1 < l2
then V_lit (L_aux L_one Unknown)
else V_lit (L_aux L_zero Unknown)
| (V_track v1 r1, V_track v2 r2) ->
taint (lt_range (V_tuple [v1;v2])) (r1++r2)
| (V_track v1 r1, v2) ->
taint (lt_range (V_tuple [v1;v2])) r1
| (v1,V_track v2 r2) ->
taint (lt_range (V_tuple [v1;v2])) r2
| (V_unknown,_) -> V_unknown
| (_,V_unknown) -> V_unknown
end ;;
let bit_to_bool b = match b with
| V_lit (L_aux L_zero _) -> false
| V_track (V_lit (L_aux L_zero _)) _ -> false
| V_lit (L_aux L_one _) -> true
| V_track (V_lit (L_aux L_one _)) _ -> true
end ;;
let bool_to_bit b = match b with
false -> V_lit (L_aux L_zero Unknown)
| true -> V_lit (L_aux L_one Unknown)
end ;;
let bitwise_not v =
match v with
| V_vector idx inc v ->
let apply x = bool_to_bit(not (bit_to_bool x)) in
V_vector idx inc (List.map apply v)
| V_track (V_vector idx inc v) r ->
let apply x = bool_to_bit(not (bit_to_bool x)) in
V_track (V_vector idx inc (List.map apply v)) r
end ;;
let bitwise_not_bit v =
let lit_not (L_aux l loc) = match l with
| L_zero -> (V_lit (L_aux L_one loc))
| L_one -> (V_lit (L_aux L_zero loc)) end in
match v with
| V_lit lit -> lit_not lit
| V_track (V_lit lit) r -> V_track (lit_not lit) r
end;;
let bitwise_binop_bit op (V_tuple [x; y]) = match (x,y) with
| (V_track x rx,V_track y ry) ->
V_track (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) (rx ++ ry)
| (V_track x rx,y) ->
V_track (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) rx
| (x,V_track y ry) ->
V_track (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) ry
| _ -> bool_to_bit (op (bit_to_bool x) (bit_to_bool y))
end ;;
let bitwise_binop op (V_tuple [v1;v2]) =
match (v1,v2) with
| (V_vector idx inc v, V_vector idx' inc' v') ->
(* typechecker ensures inc = inc', idx = idx' and length v = length v' *)
let apply (x, y) = bool_to_bit(op (bit_to_bool x) (bit_to_bool y)) in
V_vector idx inc (List.map apply (List.zip v v'))
end ;;
(* BitSeq expects LSB first.
* By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
* hence MSB first.
* http://en.wikipedia.org/wiki/Bit_numbering *)
let to_num signed (V_vector idx inc l) =
(* Word library in Lem expects bitseq with LSB first *)
(*TODO: Kathy think more
We thought a reverse was needed due to above comments only in inc case.
However, we seem to be interpresting bit vectors such that reverse is always needed
and despite numbering MSB is on the left.
*)
let l = (*if inc then reverse l else l*) reverse l in
(* Make sure the last bit is a zero to force unsigned numbers *)
let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);;
(*TODO As with above, consider the reverse here in both cases, where we're again always interpreting with the MSB on the left *)
let to_vec_inc (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
V_vector 0 true (map bool_to_bit (reverse l)) ;;
let to_vec_dec (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
V_vector (len - 1) false (map bool_to_bit (reverse l)) ;;
let to_vec ord len n =
if ord
then to_vec_inc (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
else to_vec_dec (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
;;
let exts len ((V_vector _ inc _) as v) =
to_vec inc len (to_num true v)
;;
let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
(* XXX interpret vectors as unsigned numbers for equality *)
let eq_vec_range (V_tuple [v; r]) = eq (V_tuple [to_num false v; r]) ;;
let eq_range_vec (V_tuple [r; v]) = eq (V_tuple [r; to_num false v]) ;;
let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
| L_one -> L_zero
| L_zero -> L_one end) la) ;;
let neq = compose neg eq ;;
let arith_op op (V_tuple args) = match args with
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
| [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx)
end ;;
let arith_op_vec op (V_tuple args) = match args with
| [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
let (l1',l2') = (to_num false l1,to_num false l2) in
let n = arith_op op (V_tuple [l1';l2']) in
to_vec ord (List.length cs) n
end ;;
let arith_op_range_vec op (V_tuple args) = match args with
| [n; (V_vector _ ord cs as l2)] ->
arith_op_vec op (V_tuple [(to_vec ord (List.length cs) n);l2])
end ;;
let arith_op_vec_range op (V_tuple args) = match args with
| [(V_vector _ ord cs as l1);n] ->
arith_op_vec op (V_tuple [l1;(to_vec ord (List.length cs) n)])
end ;;
let arith_op_range_vec_range op (V_tuple args) = match args with
| [n;(V_vector _ ord _ as l2)] ->
arith_op op (V_tuple [n;(to_num ord l2)])
end ;;
let arith_op_vec_range_range op (V_tuple args) = match args with
| [(V_vector _ ord _ as l1);n] ->
arith_op op (V_tuple [(to_num ord l1);n])
end ;;
let compare_op op (V_tuple args) = match args with
| [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] ->
if (op x y)
then V_lit(L_aux L_one lx)
else V_lit(L_aux L_zero lx)
end ;;
let compare_op_vec op (V_tuple args) = match args with
| [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
let (l1',l2') = (to_num true l1, to_num true l2) in
compare_op op (V_tuple[l1';l2'])
end ;;
let rec vec_concat (V_tuple args) = match args with
| [V_vector n d l; V_vector n' d' l'] ->
(* XXX d = d' ? droping n' ? *)
V_vector n d (l ++ l')
| [V_lit l; x] -> vec_concat (V_tuple [litV_to_vec l true; x]) (*TODO, get the correct order*)
| [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l true]) (*TODO, get the correct order*)
end ;;
let function_map = [
("ignore", ignore_sail);
("add", arith_op (+));
("add_vec", arith_op_vec (+));
("add_vec_range", arith_op_vec_range (+));
("add_vec_range_range", arith_op_vec_range_range (+));
("add_range_vec", arith_op_range_vec (+));
("add_range_vec_range", arith_op_range_vec_range (+));
("minus", arith_op (-));
("minus_vec", arith_op_vec (-));
("mod", arith_op (mod));
("mod_vec", arith_op_vec (mod));
("mod_vec_range", arith_op_vec_range (mod));
("eq", eq);
("eq_vec_range", eq_vec_range);
("eq_range_vec", eq_range_vec);
("neq", neq);
("vec_concat", vec_concat);
("is_one", is_one);
("to_num_inc", to_num false);
("to_num_dec", to_num false);
("EXTS", exts 64);
("to_vec_inc", to_vec_inc);
("to_vec_dec", to_vec_dec);
("bitwise_not", bitwise_not);
("bitwise_not_bit", bitwise_not_bit);
("bitwise_and", bitwise_binop (&&));
("bitwise_or", bitwise_binop (||));
("bitwise_xor", bitwise_binop xor);
("bitwise_and_bit", bitwise_binop_bit (&&));
("bitwise_or_bit", bitwise_binop_bit (||));
("bitwise_xor_bit", bitwise_binop_bit xor);
("lt", compare_op (<));
("gt", compare_op (>));
("lt_vec", compare_op_vec (<));
("gt_vec", compare_op_vec (>));
] ;;
let eval_external name v = match List.lookup name function_map with
| Just f -> f v
| Nothing -> Assert_extra.failwith ("missing library function " ^ name)
end
|
