1 % (c) 2009-2010 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(interval, []).
6
7 :- use_module(probsrc(b_global_sets)).
8
9 :- use_module(probsrc(module_information)).
10 :- module_info(group,plugin_absint).
11 :- module_info(description,'Integer interval analysis for the experimental abstract interpretation plugin. This domain abstracts integers by intervals and sets by the cardinality.').
12 :- module_info(revision,'$Rev$').
13 :- module_info(lastchanged,'$LastChangedDate$').
14
15 % ------------
16 % GLB and LUB
17 % ------------
18 :- public glb/1, lub/1.
19 glb(interval_glb).
20 lub(lub).
21
22 % ---------
23 % Mappings
24 % ---------
25 :- public map_alpha/2, map_unary_operator/2, map_binary_operator/2, map_nary_operator/2, map_binary_test_operator/2.
26 map_alpha(alpha,alpha).
27
28 map_unary_operator(card,acard).
29 map_unary_operator(domain,adomain).
30 map_unary_operator(range,arange).
31
32 map_binary_operator(add,aadd).
33 map_binary_operator(div,adiv).
34 map_binary_operator(intersection,aintersection).
35 map_binary_operator(interval,ainterval).
36 map_binary_operator(minus,aminus).
37 map_binary_operator(multiplication,amultiplication).
38 map_binary_operator(set_subtraction,aset_subtraction).
39 map_binary_operator(union,aunion).
40
41
42 map_nary_operator(set_extension,aset_extension).
43
44 map_binary_test_operator(equal,aequal).
45 map_binary_test_operator(greater,agreater).
46 map_binary_test_operator(less,aless).
47 map_binary_test_operator(less_equal,aless_equal).
48 map_binary_test_operator(member,amember).
49 map_binary_test_operator(not_equal,anot_equal).
50 map_binary_test_operator(not_member,anot_member).
51
52 % ------------------
53 % Alpha transitions
54 % ------------------
55
56 :- public alpha/4.
57 % based on types: Initial values
58 alpha(boolean,_Type,_Infos,boolean) :- !.
59 alpha(boolean_true,_Type,_Infos,boolean_true) :- !.
60 alpha(boolean_false,_Type,_Infos,boolean_false) :- !.
61
62 alpha(global(X),_Type,_Infos,global(X)) :- !.
63
64 alpha(string,_Type,_Infos,string) :- !.
65
66 alpha(integer,_Type,_Infos,integer([MinInt,MaxInt])) :- !,
67 preferences:get_preference(minint,MinInt),
68 preferences:get_preference(maxint,MaxInt).
69
70 alpha(couple(X,Y),_Type,_Infos,couple(AbsX,AbsY)) :- !,
71 alpha(X,X,[],AbsX), alpha(Y,Y,[],AbsY).
72
73 alpha(set(_X),Type,Infos,Abs) :- !,
74 alpha(empty_set,Type,Infos,Abs).
75
76 % based on expressions
77 alpha(integer(X),_Type,_Infos,integer([X,X])) :- !.
78
79 alpha(empty_set,set(SetOfType),_Infos,set(AbsType,[0,0],MaxCard)) :- !,
80 alpha(SetOfType,SetOfType,[],AbsType),
81 max_cardinality(SetOfType,MaxCard).
82
83 % ------------------
84 % LUB
85 % ------------------
86
87 :- public lub/3.
88 lub(X,X,X).
89
90 lub(integer([CurMinA,CurMaxA]),
91 integer([CurMinB,CurMaxB]),
92 integer([CurMinC,CurMaxC])) :-
93 CurMinC is min(CurMinA,CurMinB), CurMaxC is max(CurMaxA,CurMaxB).
94
95 % ------------------
96 % Abstract Operations
97 % ------------------
98
99 :- public acard/2.
100 acard(set(_Contents,[CurMinCard,CurMaxCard],_MaxCard), integer([CurMinCard,CurMaxCard])).
101
102 :- public adomain/2, arange/2.
103 adomain(SV1,set(Value,[CurMinCard,CurMaxCard],MaxCard)) :-
104 !, SV1 = set(couple(Value,_X),[SetCurMinCard,SetCurMaxCard],_SetMaxCard),
105 max_cardinality(Value,MaxCard),
106 CurMinCard = SetCurMinCard, CurMaxCard is min(SetCurMaxCard,MaxCard).
107
108 arange(SV1,set(Value,[CurMinCard,CurMaxCard],MaxCard)) :-
109 !, SV1 = set(couple(_X,Value),[SetCurMinCard,SetCurMaxCard],_SetMaxCard),
110 max_cardinality(Value,MaxCard),
111 CurMinCard = SetCurMinCard, CurMaxCard is min(SetCurMaxCard,MaxCard).
112
113 :- public aadd/3.
114 aadd(integer([MinA,MaxA]),integer([MinB,MaxB]),integer([MinC,MaxC])) :-
115 MinCT is MinA + MinB, MaxCT is MaxA + MaxB,
116 bound_ints(MinCT,MaxCT,MinC,MaxC).
117
118 :- public aminus/3.
119 aminus(integer([MinA,MaxA]),integer([MinB,MaxB]),integer([MinC,MaxC])) :-
120 MinCT is MinA - MaxB, MaxCT is MaxA - MinB,
121 bound_ints(MinCT,MaxCT,MinC,MaxC).
122
123 :- public amultiplication/3.
124 amultiplication(integer([MinA,MaxA]),integer([MinB,MaxB]),integer([MinC,MaxC])) :-
125 multi_min([MinA * MinB, MaxA * MaxB, MinA * MaxB, MaxA * MinB], MinCT),
126 multi_max([MinA * MinB, MaxA * MaxB, MinA * MaxB, MaxA * MinB], MaxCT),
127 bound_ints(MinCT,MaxCT,MinC,MaxC).
128
129 :- public adiv/3.
130 adiv(integer([MinA,MaxA]),integer([MinB,MaxB]),integer([MinCR,MaxCR])) :-
131 % todo: div by zero
132 (MaxB \= 0 -> MinC is MinA/MaxB ; MinC is MinA),
133 (MinB \= 0 -> MaxC is MaxA/MinB ; MaxC is MaxA),
134 MinCR is floor(MinC), MaxCR is floor(MaxC).
135
136 aunion(set(X,[CurMinCardX,CurMaxCardX],MaxCardX), set(Y,[CurMinCardY,CurMaxCardY],MaxCardY),Out) :-
137 lub(X,Y,Z), CurMinCardZ is max(CurMinCardX,CurMinCardY),
138 % if the type did not change, maxcard still applies
139 (X=Y -> MaxCardZ = MaxCardX ; MaxCardZ is MaxCardX + MaxCardY),
140 CurMaxCardZ is min(MaxCardZ,CurMaxCardX + CurMaxCardY),
141 Out = set(Z,[CurMinCardZ,CurMaxCardZ],MaxCardZ).
142
143 :- public aintersection/3.
144 aintersection(set(X,[CurMinCardX,CurMaxCardX],MaxCardX), set(Y,[_CurMinCardY,CurMaxCardY],_MaxCardY),Out) :-
145 lub(X,Y,Z), CurMinCardZ is max(0,CurMinCardX-CurMaxCardY),
146 CurMaxCardZ is CurMaxCardX, MaxCardZ is MaxCardX,
147 Out = set(Z,[CurMinCardZ,CurMaxCardZ],MaxCardZ).
148
149 :- public aset_subtraction/3.
150 aset_subtraction(set(X,[CurMinCardX,CurMaxCardX],MaxCardX), set(_Y,[_CurMinCardY,CurMaxCardY],_MaxCardY),Out) :-
151 CurMinCardZ is max(0,CurMinCardX - CurMaxCardY),
152 Out = set(X,[CurMinCardZ,CurMaxCardX],MaxCardX).
153
154 :- public aset_extension/2.
155 aset_extension([AbsVal|AbsVals],Set) :-
156 aset_extension(set(AbsVal,[1,1],1),AbsVals,Set).
157 aset_extension(SetIn,[],SetIn).
158 aset_extension(SetIn,[AbsVal|AbsVals],SetOut) :-
159 aunion(SetIn,set(AbsVal,[1,1],1),UpdatedSet),
160 aset_extension(UpdatedSet,AbsVals,SetOut).
161
162 :- public ainterval/3.
163 ainterval(Int1,Int2,set(Int3,[MaxCard,MaxCard],[MaxCard])) :-
164 lub(Int1,Int2,Int3), max_cardinality(Int3,MaxCard).
165
166 % ------------------
167 % Tests
168 % ------------------
169
170 :- public aequal/5.
171 aequal(A,A,A,A,true).
172 aequal(integer([MinA,MaxA]),integer([MinB,MaxB]),integer([MinA,MaxA]),integer([MinB,MaxB]),false) :-
173 (MaxA < MinB ; MaxB < MinA), !.
174 aequal(integer([MinA,MaxA]),integer([MinB,MaxB]),integer([MinOut,MaxOut]),integer([MinOut,MaxOut]),true) :-
175 MinOut is max(MinA,MinB), MaxOut is min(MaxA,MaxB).
176
177 aequal(set(Type,[0,0],MaxCard),set(Type,[0,0],MaxCard),set(Type,[0,0],MaxCard),set(Type,[0,0],MaxCard),true).
178
179 :- public anot_equal/5.
180 anot_equal(E1,S1,E2,S2,Res) :-
181 aequal(E1,S1,E2,S2,Res2),
182 Res2 = true -> Res = false ; Res = true.
183
184 :- public agreater/5.
185 agreater(A,B,C,D,Res) :- aless(B,A,D,C,Res).
186
187 aless(integer([MinA,MaxA]),integer([MinB,MaxB]),integer([MinA,MaxA]),integer([MinB,MaxB]),true) :-
188 MaxA < MinB.
189 aless(integer([MinA,_MaxA]),integer([MinB,MaxB]),integer([MinA,MaxAOut]),integer([MinB,MaxB]),true) :-
190 MaxAOut is MinB - 1, MaxAOut > MinA.
191 aless(integer([MinA,MaxA]),integer([_MinB,MaxB]),integer([MinA,MaxA]),integer([MinBOut,MaxB]),true) :-
192 MinBOut is MaxA + 1, MinBOut < MaxB.
193
194 :- public aless_equal/5.
195 aless_equal(A,B,C,D,E) :- aless(A,B,C,D,E) ; aequal(A,B,C,D,E).
196
197 amember(integer(X),set(integer(Y),[CurMinCard,CurMaxCard],MaxCard),integer(X),set(integer(Y),[CurMinCard,CurMaxCard],MaxCard),true) :-
198 CurMinCard > 0, lub(integer(X),integer(Y),integer(Y)).
199 amember(Elem,set(Type,[CurMinCard,CurMaxCard],MaxCard),Elem,set(Type,[CurMinCard,CurMaxCard],MaxCard),true) :-
200 CurMinCard > 0.
201 amember(Elem,set(Type,[CurMinCard,CurMaxCard],MaxCard),Elem,set(Type,[CurMinCard,CurMaxCard],MaxCard),false) :-
202 CurMinCard = 0.
203
204 :- public anot_member/5.
205 anot_member(E1,S1,E2,S2,Res) :-
206 amember(E1,S1,E2,S2,Res2),
207 Res2 = true -> Res = false ; Res = true.
208
209
210 % ------------------
211 % Helpers
212 % ------------------
213
214 multi_min([A,B],Min) :- !,
215 Min is min(A,B).
216 multi_min([H|T], Min) :-
217 multi_min(T,Min2),
218 Min is min(H,Min2).
219
220 multi_max([A,B],Max) :- !,
221 Max is max(A,B).
222 multi_max([H|T], Max) :-
223 multi_max(T,Max2),
224 Max is max(H,Max2).
225
226 bound_ints(MinC,MaxC,MinCOut,MaxCOut) :-
227 bound_by_min_int(MinC,MinC2), bound_by_max_int(MinC2,MinCOut),
228 bound_by_min_int(MaxC,MaxC2), bound_by_max_int(MaxC2,MaxCOut).
229
230 bound_by_min_int(MinCandidate,Min) :-
231 preferences:get_preference(minint,MinInt),
232 (MinInt > MinCandidate -> Min = MinInt ; Min = MinCandidate).
233
234 bound_by_max_int(MaxCandidate,Max) :-
235 preferences:get_preference(maxint,MaxInt),
236 (MaxInt < MaxCandidate -> Max = MaxInt ; Max = MaxCandidate).
237
238 max_cardinality(integer([A,B]), Card) :-
239 !, Card is B - A + 1.
240 max_cardinality(integer,Card) :-
241 !, preferences:get_preference(minint,MinInt),
242 preferences:get_preference(maxint,MaxInt),
243 Card is MaxInt - MinInt + 1.
244 max_cardinality(couple(X,Y),Card) :-
245 !, max_cardinality(X,CardX),
246 max_cardinality(Y, CardY),
247 Card is CardX * CardY.
248 max_cardinality(global(X),Card) :-
249 b_global_set_cardinality(X,Card).
250 max_cardinality(boolean,2).