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
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
|
open Big_int_Z
(* only expected to be 0, 1, 2; 2 represents undef *)
type vbit = Vone | Vzero | Vundef
type number = Big_int_Z.big_int
type value =
| Vvector of vbit array * int * bool
| VvectorR of value array * int * bool
| Vregister of vbit array ref * int * bool * (string * (int * int)) list
| Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*)
let to_bool = function
| Vzero -> false
| Vone -> true
| Vundef -> assert false
let get_barray = function
| Vvector(a,_,_) -> a
| Vregister(a,_,_,_) -> !a
| _ -> assert false
let get_varray = function
| VvectorR(a,_,_) -> a
| _ -> assert false
let get_ord = function
| Vvector(_,_,o) | Vregister(_,_,o,_) | VvectorR(_,_,o) -> o
| _ -> assert false
let get_start = function
| Vvector(_,s,o) | Vregister(_,s,o,_) | VvectorR(_,s,o) -> s
| _ -> assert false
let length = function
| Vvector(array,_,_) -> big_int_of_int (Array.length array)
| Vregister(array,_,_,_) -> big_int_of_int (Array.length !array)
| VvectorR(array,_,_) -> big_int_of_int (Array.length array)
| _ -> assert false
let read_register = function
| Vregister(a,start,inc,_) -> Vvector(!a,start,inc)
| v -> v
let vector_access v n = match v with
| VvectorR(array,start,is_inc) ->
if is_inc
then (array.(n-start))
else (array.(start-n))
| _ -> assert false
let bit_vector_access v n = match v with
| Vvector(array,start,is_inc) ->
if is_inc
then array.(n-start)
else array.(start-n)
| Vregister(array,start,is_inc,_) ->
if is_inc
then !array.(n-start)
else !array.(start-n)
| _ -> assert false
let vector_subrange v n m =
let builder array length offset default =
let new_array = Array.make length default in
begin
for x = 0 to length-1
do new_array.(x) <- array.(x+offset)
done;
new_array
end
in
match v with
| VvectorR(array,start,is_inc) ->
let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
VvectorR(builder array length offset (VvectorR([||], 0, is_inc)),n,is_inc)
| Vvector(array,start,is_inc) ->
let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
Vvector(builder array length offset Vzero,n,is_inc)
| Vregister(array,start,is_inc,fields) ->
let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
Vvector(builder !array length offset Vzero,n,is_inc)
| _ -> v
let get_register_field_vec reg field =
match reg with
| Vregister(_,_,_,fields) ->
(match List.assoc field fields with
| (i,j) ->
if i = j
then Vbit Vundef
else vector_subrange reg i j)
| _ -> Vbit Vundef
let get_register_field_bit reg field =
match reg with
| Vregister(_,_,_,fields) ->
(match List.assoc field fields with
| (i,j) ->
if i = j
then bit_vector_access reg i
else Vundef)
| _ -> Vundef
let set_register register value = match register,value with
| Vregister(a,_,_,_), Vregister(new_v,_,_,_) ->
a := !new_v
| Vregister(a,_,_,_), Vvector(new_v,_,_) ->
a := new_v
| _ -> ()
let set_vector_subrange_vec v n m new_v =
let walker array length offset new_values =
begin
for x = 0 to length-1
do array.(x+offset) <- new_values.(x)
done;
end
in
match v with
| VvectorR(array,start,is_inc) ->
let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
walker array length offset new_v
| _ -> ()
let set_vector_subrange_bit v n m new_v =
let walker array length offset new_values =
begin
for x = 0 to length-1
do array.(x+offset) <- new_values.(x)
done;
end
in
match v,new_v with
| Vvector(array,start,is_inc),Vvector(new_v,_,_) ->
let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
walker array length offset new_v
| Vregister(array,start,is_inc,fields),Vvector(new_v,_,_) ->
let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
walker !array length offset new_v
| _ -> ()
let set_register_field_v reg field new_v =
match reg with
| Vregister(array,start,dir,fields) ->
(match List.assoc field fields with
| (i,j) ->
if i = j
then ()
else set_vector_subrange_bit reg i j new_v)
| _ -> ()
let set_register_field_bit reg field new_v =
match reg with
| Vregister(array,start,dir,fields) ->
(match List.assoc field fields with
| (i,j) ->
if i = j
then !array.(if dir then i - start else start - i) <- new_v
else ())
| _ -> ()
let set_two_reg r1 r2 vec =
let size = int_of_big_int (length r1) in
let dir = get_ord r1 in
let start = get_start vec in
let vsize = int_of_big_int (length vec) in
let r1_v = vector_subrange vec start ((if dir then size - start else start - size) - 1) in
let r2_v = vector_subrange vec (if dir then size - start else start - size)
(if dir then vsize - start else start - vsize) in
begin set_register r1 r1_v; set_register r2 r2_v end
let make_indexed_v entries default start size dir =
let default_value = match default with
| None -> Vbit Vundef
| Some v -> v in
let array = Array.make size default_value in
begin
List.iter (fun (i,v) -> array.(if dir then start - i else i - start) <- v) entries;
VvectorR(array, start, dir)
end
let make_indexed_bitv entries default start size dir =
let default_value = match default with
| None -> Vundef
| Some v -> v in
let array = Array.make size default_value in
begin
List.iter (fun (i,v) -> array.(if dir then start - i else i - start) <- v) entries;
Vvector(array, start, dir)
end
let vector_concat l r =
match l,r with
| Vvector(arrayl,start,ord), Vvector(arrayr,_,_) ->
Vvector(Array.append arrayl arrayr, start, ord)
| Vvector(arrayl,start,ord), Vregister(arrayr,_,_,_) ->
Vvector(Array.append arrayl !arrayr, start,ord)
| Vregister(arrayl,start,ord,_), Vvector(arrayr,_,_) ->
Vvector(Array.append !arrayl arrayr, start, ord)
| Vregister(arrayl,start,ord,_), Vregister(arrayr,_,_,_) ->
Vvector(Array.append !arrayl !arrayr,start,ord)
| VvectorR(arrayl,start,ord),VvectorR(arrayr,_,_) ->
VvectorR(Array.append arrayl arrayr, start,ord)
| _ -> Vbit Vundef
let has_undef = function
| Vvector(array,_,_) ->
let rec foreach i =
if i <= Array.length array
then
if array.(i) = Vundef then true
else foreach (i+1)
else false in
foreach 0
| Vregister(array,_,_,_) ->
let array = !array in
let rec foreach i =
if i <= Array.length array
then
if array.(i) = Vundef then true
else foreach (i+1)
else false in
foreach 0
| _ -> false
let most_significant = function
| Vvector(array,_,_) -> array.(0)
| Vregister(array,_,_,_) -> !array.(0)
| _ -> assert false
let bitwise_not_bit = function
| Vone -> Vzero
| Vzero -> Vone
| _ -> Vundef
let bitwise_not = function
| Vvector(array,s,d)-> Vvector( Array.map bitwise_not_bit array,s,d)
| Vregister(array,s,d,_) -> Vvector( Array.map bitwise_not_bit !array,s,d)
| _ -> assert false
let bool_to_bit b = if b then Vone else Vzero
let bitwise_binop_bit op (l,r) =
match l,r with
| Vundef,_ | _,Vundef -> Vundef (*Do we want to do this or to respect | of One and & of Zero rules?*)
| Vone,Vone -> bool_to_bit (op true true)
| Vone,Vzero -> bool_to_bit (op true false)
| Vzero,Vone -> bool_to_bit (op false true)
| Vzero,Vzero -> bool_to_bit (op false false)
let bitwise_and_bit = bitwise_binop_bit (&&)
let bitwise_or_bit = bitwise_binop_bit (||)
let bitwise_xor_bit = bitwise_binop_bit (fun x y -> (1 = (if x then 1 else 0) lxor (if y then 0 else 1)))
let bitwise_binop op (l,r) =
let bop l arrayl arrayr =
let array = Array.make l Vzero in
begin
for i = 0 to l do
array.(i) <- bitwise_binop_bit op (arrayl.(i), arrayr.(i))
done;
array
end in
match l,r with
| Vvector(arrayl, start, dir), Vvector(arrayr,_,_) ->
Vvector(bop (Array.length arrayl) arrayl arrayr, start,dir)
| Vvector(arrayl, start, dir), Vregister(arrayr,_,_,_) ->
Vvector(bop (Array.length arrayl) arrayl !arrayr, start, dir)
| Vregister(arrayl, start,dir,_), Vvector(arrayr,_,_) ->
Vvector(bop (Array.length arrayr) !arrayl arrayr, start,dir)
| Vregister(arrayl, start, dir, _), Vregister(arrayr,_,_,_) ->
Vvector(bop (Array.length !arrayl) !arrayl !arrayr, start,dir)
| _ -> Vbit Vundef
let bitwise_and = bitwise_binop (&&)
let bitwise_or = bitwise_binop (||)
let bitwise_xor = bitwise_binop (fun x y -> (1 = (if x then 1 else 0) lxor (if y then 0 else 1)))
let unsigned = function
| (Vvector(array,_,_) as v) ->
if has_undef v
then assert false
else
let acc = ref zero_big_int in
begin for i = (Array.length array) - 1 downto 0 do
match array.(i) with
| Vone -> acc := add_big_int !acc (power_int_positive_int 2 i)
| _ -> ()
done;
!acc
end
| (Vregister(array,_,_,_) as v)->
let array = !array in
if has_undef v
then assert false
else
let acc = ref zero_big_int in
begin for i = (Array.length array) - 1 downto 0 do
match array.(i) with
| Vone -> acc := add_big_int !acc (power_int_positive_int 2 i)
| _ -> ()
done;
!acc
end
| _ -> assert false
let signed v =
match most_significant v with
| Vone -> minus_big_int(add_int_big_int 1 (unsigned (bitwise_not v)))
| Vzero -> unsigned v
| _ -> assert false
let to_num sign = if sign then signed else unsigned
let two_big_int = big_int_of_int 2
let max_64u = pred_big_int (power_big two_big_int (big_int_of_int 64))
let max_64 = pred_big_int (power_big two_big_int (big_int_of_int 63))
let min_64 = minus_big_int (power_big two_big_int (big_int_of_int 63))
let max_32u = big_int_of_int 4294967295
let max_32 = big_int_of_int 2147483647
let min_32 = big_int_of_int (-2147483648)
let max_8 = big_int_of_int 127
let min_8 = big_int_of_int (-128)
let max_5 = big_int_of_int 31
let min_5 = big_int_of_int (-32)
let get_max_representable_in sign n =
if (n = 64) then match sign with | true -> max_64 | false -> max_64u
else if (n=32) then match sign with | true -> max_32 | false -> max_32u
else if (n=8) then max_8
else if (n=5) then max_5
else match sign with | true -> power_big two_big_int (pred_big_int (big_int_of_int n))
| false -> power_big two_big_int (big_int_of_int n)
let get_min_representable_in _ n =
if (n = 64) then min_64
else if (n=32) then min_32
else if (n=8) then min_8
else if (n=5) then min_5
else minus_big_int (power_big two_big_int (big_int_of_int n))
let rec divide_by_2 array i n =
if i < 0 || eq_big_int n zero_big_int
then array
else let (quo,modu) = quomod_big_int n two_big_int in
if eq_big_int modu unit_big_int
then begin array.(i) <- Vone; divide_by_2 array (i-1) quo end
else divide_by_2 array (i-1) quo
let rec add_one_bit array co i =
if i < 0
then array
else match array.(i),co with
| Vzero,false -> array.(i) <- Vone; array
| Vzero,true -> array.(i) <- Vone; add_one_bit array true (i-1)
| Vone, false -> array.(i) <- Vzero; add_one_bit array true (i-1)
| Vone, true -> add_one_bit array true (i-1)
| Vundef,_ -> assert false
let to_vec ord len n =
let len = int_of_big_int len in
let array = Array.make len Vzero in
let start = if ord then 0 else len-1 in
if eq_big_int n zero_big_int
then Vvector(array, start, ord)
else if gt_big_int n zero_big_int
then Vvector(divide_by_2 array (len -1) n, start, ord)
else
let abs_n = abs_big_int n in
let abs_array = divide_by_2 array (len-1) abs_n in
let v_abs = bitwise_not (Vvector(abs_array,start,ord)) in
match v_abs with
| Vvector(array,start,ord) -> Vvector(add_one_bit array false (len-1),start,ord)
| _ -> assert false
let to_vec_inc (len,n) = to_vec true len n
let to_vec_dec (len,n) = to_vec false len n
let to_vec_undef ord len =
let len = int_of_big_int len in
let array = Array.make len Vundef in
let start = if ord then 0 else len-1 in
Vvector(array, start, ord)
let to_vec_inc_undef len = to_vec_undef true len
let to_vec_dec_undef len = to_vec_undef false len
let arith_op op (l,r) = op l r
let add = arith_op add_big_int
let add_signed = arith_op add_big_int
let minus = arith_op sub_big_int
let multiply = arith_op mult_big_int
let modulo = arith_op mod_big_int
let quot = arith_op div_big_int
let power = arith_op power_big
let arith_op_vec op sign size (l,r) =
let ord = get_ord l in
let (l',r') = to_num sign l, to_num sign r in
let n = arith_op op (l',r') in
to_vec ord (mult_big_int size (length l)) n
let add_vec = arith_op_vec add_big_int false unit_big_int
let add_vec_signed = arith_op_vec add_big_int true unit_big_int
let minus_vec = arith_op_vec sub_big_int false unit_big_int
let multiply_vec = arith_op_vec mult_big_int false two_big_int
let multiply_vec_signed = arith_op_vec mult_big_int true two_big_int
let arith_op_vec_range op sign size (l,r) =
let ord = get_ord l in
arith_op_vec op sign size (l, to_vec ord (length l) r)
let add_vec_range = arith_op_vec_range add_big_int false unit_big_int
let add_vec_range_signed = arith_op_vec_range add_big_int true unit_big_int
let minus_vec_range = arith_op_vec_range sub_big_int false unit_big_int
let mult_vec_range = arith_op_vec_range mult_big_int false two_big_int
let mult_vec_range_signed = arith_op_vec_range mult_big_int true two_big_int
let arith_op_range_vec op sign size (l,r) =
let ord = get_ord r in
arith_op_vec op sign size ((to_vec ord (length r) l), r)
let add_range_vec = arith_op_range_vec add_big_int false unit_big_int
let add_range_vec_signed = arith_op_range_vec add_big_int true unit_big_int
let minus_range_vec = arith_op_range_vec sub_big_int false unit_big_int
let mult_range_vec = arith_op_range_vec mult_big_int false two_big_int
let mult_range_vec_signed = arith_op_range_vec mult_big_int true two_big_int
let arith_op_range_vec_range op sign (l,r) = arith_op op (l, to_num sign r)
let add_range_vec_range = arith_op_range_vec_range add_big_int false
let add_range_vec_range_signed = arith_op_range_vec_range add_big_int true
let minus_range_vec_range = arith_op_range_vec_range sub_big_int false
let arith_op_vec_range_range op sign (l,r) = arith_op op (to_num sign l,r)
let add_vec_range_range = arith_op_vec_range_range add_big_int false
let add_vec_range_range_signed = arith_op_vec_range_range add_big_int true
let minus_vec_range_range = arith_op_vec_range_range sub_big_int false
let arith_op_vec_vec_range op sign (l,r) =
let (l',r') = (to_num sign l,to_num sign r) in
arith_op op (l',r')
let add_vec_vec_range = arith_op_vec_vec_range add_big_int false
let add_vec_vec_range_signed = arith_op_vec_vec_range add_big_int true
let arith_op_vec_bit op sign size (l,r) =
let ord = get_ord l in
let l' = to_num sign l in
let n = arith_op op (l', match r with | Vone -> unit_big_int | _ -> zero_big_int) in
to_vec ord (mult_big_int (length l) size) n
let add_vec_bit = arith_op_vec_bit add_big_int false unit_big_int
let add_vec_bit_signed = arith_op_vec_bit add_big_int true unit_big_int
let minus_vec_bit = arith_op_vec_bit sub_big_int true unit_big_int
let rec arith_op_overflow_vec op sign size (l,r) =
let ord = get_ord l in
let len = length l in
let act_size = mult_big_int len size in
let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
let n = arith_op op (l_sign,r_sign) in
let n_unsign = arith_op op (l_unsign,r_unsign) in
let correct_size_num = to_vec ord act_size n in
let one_more_size_u = to_vec ord (succ_big_int act_size) n_unsign in
let overflow = if (le_big_int n (get_max_representable_in sign (int_of_big_int len))) &&
(ge_big_int n (get_min_representable_in sign (int_of_big_int len)))
then Vzero
else Vone in
let c_out = most_significant one_more_size_u in
(correct_size_num,overflow,c_out)
let add_overflow_vec = arith_op_overflow_vec add_big_int false unit_big_int
let add_overflow_vec_signed = arith_op_overflow_vec add_big_int true unit_big_int
let minus_overflow_vec = arith_op_overflow_vec sub_big_int false unit_big_int
let minus_overflow_vec_signed = arith_op_overflow_vec sub_big_int true unit_big_int
let mult_overflow_vec = arith_op_overflow_vec mult_big_int false two_big_int
let mult_overflow_vec_signed = arith_op_overflow_vec mult_big_int true two_big_int
let rec arith_op_overflow_vec_bit op sign size (l,r_bit) =
let ord = get_ord l in
let act_size = mult_big_int (length l) size in
let l' = to_num sign l in
let l_u = to_num false l in
let (n,nu,changed) = match r_bit with
| Vone -> (arith_op op (l',unit_big_int), arith_op op (l_u,unit_big_int), true)
| Vzero -> (l',l_u,false)
| _ -> assert false
in
let correct_size_num = to_vec ord act_size n in
let one_larger = to_vec ord (succ_big_int act_size) nu in
let overflow =
if changed
then if (le_big_int n (get_max_representable_in sign (int_of_big_int act_size))) &&
(ge_big_int n (get_min_representable_in sign (int_of_big_int act_size)))
then Vzero
else Vone
else Vone in
(correct_size_num,overflow,most_significant one_larger)
let add_overflow_vec_bit_signed = arith_op_overflow_vec_bit add_big_int true unit_big_int
let minus_overflow_vec_bit = arith_op_overflow_vec_bit sub_big_int false unit_big_int
let minus_overflow_vec_bit_signed = arith_op_overflow_vec_bit sub_big_int true unit_big_int
let shift_op_vec op (l,r) =
match l with
| Vvector(_,start,ord) | Vregister(_,start,ord,_) ->
let array = match l with | Vvector(array,_,_) -> array | Vregister(array,_,_,_) -> !array | _ -> assert false in
let len = Array.length array in
let n = int_of_big_int r in
(match op with
| "<<" ->
let right_vec = Vvector(Array.make n Vzero,0,true) in
let left_vec = vector_subrange l n (if ord then len + start else start - len) in
vector_concat left_vec right_vec
| ">>" ->
let right_vec = vector_subrange l start n in
let left_vec = Vvector(Array.make n Vzero,0,true) in
vector_concat left_vec right_vec
| "<<<" ->
let left_vec = vector_subrange l n (if ord then len + start else start - len) in
let right_vec = vector_subrange l start n in
vector_concat left_vec right_vec
| _ -> assert false)
| _ -> assert false
let bitwise_leftshift = shift_op_vec "<<"
let bitwise_rightshift = shift_op_vec ">>"
let bitwise_rotate = shift_op_vec "<<<"
let rec arith_op_no0 op (l,r) =
if eq_big_int r zero_big_int
then None
else Some (op l r)
let modulo = arith_op_no0 mod_big_int
let quot = arith_op_no0 div_big_int
let rec arith_op_vec_no0 op sign size (l,r) =
let ord = get_ord l in
let act_size = int_of_big_int (mult_big_int (length l) size) in
let (l',r') = (to_num sign l,to_num sign r) in
let n = arith_op_no0 op (l',r') in
let representable,n' =
match n with
| Some n' ->
((le_big_int n' (get_max_representable_in sign act_size)) &&
(ge_big_int n' (get_min_representable_in sign act_size))), n'
| _ -> false,zero_big_int in
if representable
then to_vec ord (big_int_of_int act_size) n'
else
match l with
| Vvector(_, start, _) | Vregister(_, start, _, _) ->
Vvector((Array.make act_size Vundef), start, ord)
| _ -> assert false
let mod_vec = arith_op_vec_no0 mod_big_int false unit_big_int
let quot_vec = arith_op_vec_no0 div_big_int false unit_big_int
let quot_vec_signed = arith_op_vec_no0 div_big_int true unit_big_int
let arith_op_overflow_no0_vec op sign size (l,r) =
let ord = get_ord l in
let rep_size = mult_big_int (length r) size in
let act_size = mult_big_int (length l) size in
let (l',r') = ((to_num sign l),(to_num sign r)) in
let (l_u,r_u) = (to_num false l,to_num false r) in
let n = arith_op_no0 op (l',r') in
let n_u = arith_op_no0 op (l_u,r_u) in
let representable,n',n_u' =
match n, n_u with
| Some n',Some n_u' ->
((le_big_int n' (get_max_representable_in sign (int_of_big_int rep_size))) &&
(ge_big_int n' (get_min_representable_in sign (int_of_big_int rep_size))), n', n_u')
| _ -> true,zero_big_int,zero_big_int in
let (correct_size_num,one_more) =
if representable then
(to_vec ord act_size n',to_vec ord (succ_big_int act_size) n_u')
else match l with
| Vvector(_, start, _) | Vregister(_, start, _, _) ->
Vvector((Array.make (int_of_big_int act_size) Vundef), start, ord),
Vvector((Array.make ((int_of_big_int act_size) + 1) Vundef), start, ord)
| _ -> assert false in
let overflow = if representable then Vzero else Vone in
(correct_size_num,overflow,most_significant one_more)
let quot_overflow_vec = arith_op_overflow_no0_vec div_big_int false unit_big_int
let quot_overflow_vec_signed = arith_op_overflow_no0_vec div_big_int true unit_big_int
let arith_op_vec_range_no0 op sign size (l,r) =
let ord = get_ord l in
arith_op_vec_no0 op sign size (l,(to_vec ord (length l) r))
let mod_vec_range = arith_op_vec_range_no0 mod_big_int false unit_big_int
(*Need to have a default top level direction reference I think*)
let duplicate (bit,length) =
Vvector((Array.make (int_of_big_int length) bit), 0, true)
let compare_op op (l,r) =
if (op l r)
then Vone
else Vzero
let lt = compare_op lt_big_int
let gt = compare_op gt_big_int
let lteq = compare_op le_big_int
let gteq = compare_op ge_big_int
let compare_op_vec op sign (l,r) =
let (l',r') = (to_num sign l, to_num sign r) in
compare_op op (l',r')
let lt_vec = compare_op_vec lt_big_int true
let gt_vec = compare_op_vec gt_big_int true
let lteq_vec = compare_op_vec le_big_int true
let gteq_vec = compare_op_vec ge_big_int true
let lt_vec_signed = compare_op_vec lt_big_int true
let gt_vec_signed = compare_op_vec gt_big_int true
let lteq_vec_signed = compare_op_vec le_big_int true
let gteq_vec_signed = compare_op_vec ge_big_int true
let lt_vec_unsigned = compare_op_vec lt_big_int false
let gt_vec_unsigned = compare_op_vec gt_big_int false
let lteq_vec_unsigned = compare_op_vec le_big_int false
let gteq_vec_unsigned = compare_op_vec ge_big_int false
let compare_op_vec_range op sign (l,r) =
compare_op op ((to_num sign l),r)
let lt_vec_range = compare_op_vec_range lt_big_int true
let gt_vec_range = compare_op_vec_range gt_big_int true
let lteq_vec_range = compare_op_vec_range le_big_int true
let gteq_vec_range = compare_op_vec_range ge_big_int true
let compare_op_range_vec op sign (l,r) =
compare_op op (l, (to_num sign r))
let lt_range_vec = compare_op_range_vec lt_big_int true
let gt_range_vec = compare_op_range_vec gt_big_int true
let lteq_range_vec = compare_op_range_vec le_big_int true
let gteq_range_vec = compare_op_range_vec ge_big_int true
let eq (l,r) = if l == r then Vone else Vzero
let eq_vec_range (l,r) = eq (to_num false l,r)
let eq_range_vec (l,r) = eq (l, to_num false r)
let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
let neq (l,r) = bitwise_not_bit (eq (l,r))
let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec(l,r))
|