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
|
open Ast
open Util
open Big_int
open Type_internal
type typ = Type_internal.t
(*Query a spec for its default order if one is provided. Assumes Inc if not *)
let get_default_order_sp (DT_aux(spec,_)) =
match spec with
| DT_order (Ord_aux(o,_)) ->
(match o with
| Ord_inc -> Some {order = Oinc}
| Ord_dec -> Some { order = Odec}
| _ -> Some {order = Oinc})
| _ -> None
let get_default_order_def = function
| DEF_default def_spec -> get_default_order_sp def_spec
| _ -> None
let rec default_order (Defs defs) =
match defs with
| [] -> { order = Oinc } (*When no order is specified, we assume that it's inc*)
| def::defs ->
match get_default_order_def def with
| None -> default_order (Defs defs)
| Some o -> o
(*Is within range*)
let check_in_range (candidate : big_int) (range : typ) : bool =
match range.t with
| Tapp("range", [TA_nexp min; TA_nexp max]) | Tabbrev(_,{t=Tapp("range", [TA_nexp min; TA_nexp max])}) ->
let min,max =
match min.nexp,max.nexp with
| (Nconst min, Nconst max)
| (Nconst min, N2n(_, Some max))
| (N2n(_, Some min), Nconst max)
| (N2n(_, Some min), N2n(_, Some max))
-> min, max
| (Nneg n, Nconst max) | (Nneg n, N2n(_, Some max))->
(match n.nexp with
| Nconst abs_min | N2n(_,Some abs_min) ->
(minus_big_int abs_min), max
| _ -> assert false (*Put a better error message here*))
| (Nconst min,Nneg n) | (N2n(_, Some min), Nneg n) ->
(match n.nexp with
| Nconst abs_max | N2n(_,Some abs_max) ->
min, (minus_big_int abs_max)
| _ -> assert false (*Put a better error message here*))
| (Nneg nmin, Nneg nmax) ->
((match nmin.nexp with
| Nconst abs_min | N2n(_,Some abs_min) -> (minus_big_int abs_min)
| _ -> assert false (*Put a better error message here*)),
(match nmax.nexp with
| Nconst abs_max | N2n(_,Some abs_max) -> (minus_big_int abs_max)
| _ -> assert false (*Put a better error message here*)))
| _ -> assert false
in le_big_int min candidate && le_big_int candidate max
| _ -> assert false
(*Rmove me when switch to zarith*)
let rec power_big_int b n =
if eq_big_int n zero_big_int
then unit_big_int
else mult_big_int b (power_big_int b (sub_big_int n unit_big_int))
let unpower_of_2 b =
let two = big_int_of_int 2 in
let four = big_int_of_int 4 in
let eight = big_int_of_int 8 in
let sixteen = big_int_of_int 16 in
let thirty_two = big_int_of_int 32 in
let sixty_four = big_int_of_int 64 in
let onetwentyeight = big_int_of_int 128 in
let twofiftysix = big_int_of_int 256 in
let fivetwelve = big_int_of_int 512 in
let oneotwentyfour = big_int_of_int 1024 in
let to_the_sixteen = big_int_of_int 65536 in
let to_the_thirtytwo = big_int_of_string "4294967296" in
let to_the_sixtyfour = big_int_of_string "18446744073709551616" in
let ck i = eq_big_int b i in
if ck unit_big_int then zero_big_int
else if ck two then unit_big_int
else if ck four then two
else if ck eight then big_int_of_int 3
else if ck sixteen then four
else if ck thirty_two then big_int_of_int 5
else if ck sixty_four then big_int_of_int 6
else if ck onetwentyeight then big_int_of_int 7
else if ck twofiftysix then eight
else if ck fivetwelve then big_int_of_int 9
else if ck oneotwentyfour then big_int_of_int 10
else if ck to_the_sixteen then sixteen
else if ck to_the_thirtytwo then thirty_two
else if ck to_the_sixtyfour then sixty_four
else let rec unpower b power =
if eq_big_int b unit_big_int
then power
else (unpower (div_big_int b two) (succ_big_int power)) in
unpower b zero_big_int
let is_within_range candidate range constraints =
let candidate_actual = match candidate.t with
| Tabbrev(_,t) -> t
| _ -> candidate in
match candidate_actual.t with
| Tapp("atom", [TA_nexp n]) ->
(match n.nexp with
| Nconst i | N2n(_,Some i) -> if check_in_range i range then Yes else No
| _ -> Maybe)
| Tapp("range", [TA_nexp bot; TA_nexp top]) ->
(match bot.nexp,top.nexp with
| Nconst b, Nconst t | Nconst b, N2n(_,Some t) | N2n(_, Some b), Nconst t | N2n(_,Some b), N2n(_, Some t) ->
let at_least_in = check_in_range b range in
let at_most_in = check_in_range t range in
if at_least_in && at_most_in
then Yes
else if at_least_in || at_most_in
then Maybe
else No
| _ -> Maybe)
| Tapp("vector", [_; TA_nexp size ; _; _]) ->
(match size.nexp with
| Nconst i | N2n(_, Some i) ->
if check_in_range (power_big_int (big_int_of_int 2) i) range
then Yes
else No
| _ -> Maybe)
| _ -> Maybe
let is_within_machine64 candidate constraints = is_within_range candidate int64_t constraints
|
