1 % (c) 2012-17 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(kodkod_integer_recalc,[integer_recalc/2, integer_recalc/3]).
6
7 :- use_module('../module_information',[module_info/2]).
8 :- module_info(group,kodkod).
9 :- module_info(description,'This module provides functionality to adapt the outcome of the interval analysis to the needs of the Kodkod translation.').
10
11 :- use_module(library(lists)).
12
13 :- use_module(probsrc(self_check)).
14
15 :- use_module(probsrc(bsyntaxtree),[create_texpr/4,syntaxtransformation/5,get_texpr_info/2]).
16 :- use_module(kodkodsrc(interval_calc)).
17 :- use_module(probsrc(inf_arith)).
18
19 :- use_module(predicate_analysis,[max_type_cardinality/2]).
20
21 % re-calculate integer expressions
22 % The predicate analysis computes the possible integer intervals of expressions
23 % for valid solutions. E.g. for the predicate "x:1..100 & y:2..88 & x+y = x*y"
24 % it finds out that "x*y" lies in the range of "2..200" because the expresssion
25 % equals "x+y" which lies obviously in "3..188".
26 % But if we use that information as a basis for Kodkod's bitwidth, we can receive
27 % invalid solutions because of an integer overflow on the right side.
28 % E.g. Kodkod may choose a bitwidth that allows 511 as the maximum integer, then
29 % it can find the solution x=28 & y=20 because x*y = 560 which leads to an
30 % (unnoticed) overflow such that x*y = x*y mod 512 = 560 mod 512 = 48 = x+y
31 %
32 % To prevent this behaviour, we use the interval of basic integer expressions
33 % (variables, integers, cardinality) to re-calc the possible interval of
34 % integer expressions
35
36 :- assert_must_succeed((
37 create_texpr(identifier(x),integer,[analysis([interval:irange(1,100)])],X),
38 create_texpr(identifier(y),integer,[analysis([interval:irange(2,88)])],Y),
39 create_texpr(multiplication(X,Y),integer,[other,analysis([interval:irange(3,188)])],M),
40 integer_recalc(M,N),
41 ground(N), % make sure no variables are in the result
42 get_texpr_info(N,NInfo),
43 memberchk(other,NInfo), % the old information must still be there
44 memberchk(analysis([A]),NInfo),
45 A = interval:irange(2,8800) % the updated interval information should reflect the multiplication
46 )).
47
48 integer_recalc(TExpr,NTExpr) :-
49 integer_recalc(TExpr,unknown_atoms(_),NTExpr).
50
51 % integer_recalc(+TExpr,+IntAtoms,-NTExpr):
52 % IntAtoms is atoms(Range) if the range of the integer atoms is known (none or irange(A,B)),
53 % otherwise unknown_atoms(Flag) and Flag is set to true if the cardinality or sum of an
54 % integer set would need this range (see kodkod2:extract_used_types)
55 integer_recalc(TExpr,IntAtoms,NTExpr) :-
56 create_texpr(Expr,Type,Info,TExpr),
57 create_texpr(NExpr,Type,NInfo,NTExpr),
58 syntaxtransformation(Expr,Subs,_,NSubs,NExpr),
59 maplist(integer_recalc_aux(IntAtoms),Subs,NSubs),
60 (integer_recalc2(NExpr,IntAtoms,Interval) -> safe_add_interval_info(Interval,Info,NInfo) ; Info=NInfo).
61 integer_recalc_aux(IntAtoms,TExpr,NTExpr) :- integer_recalc(TExpr,IntAtoms,NTExpr).
62
63 integer_recalc2(card(S),IntAtoms,irange(MinCard,MaxCard)) :- !,
64 % TODO[DP,2016-04-20]: This is a very pessimistic approach:
65 % The cardinality is maximally as high as the type allows
66 % Maybe an alternative approach would be to add a second infered information to each node,
67 % the "guaranteed" integer interval which is independent of overflows. E.g. "card({a,b,c}) : 1..3"
68 get_texpr_set_type(S,Type),
69 % print(recalc(Type,S)),nl,
70 ( extract_min_max_card(S,Type,C1,C2) -> (MinCard,MaxCard)=(C1,C2),
71 debug_println(9,extract_max_card_for_kodkod(C1,C2))
72 ; max_type_cardinality(Type,MaxCard) -> MinCard=0
73 % for sets containing integers: Kodkod can choose any subset of the integer atoms
74 ; IntAtoms = atoms(AtomRange), nr_of_atoms(AtomRange,NrAtoms),
75 max_card_with_integer_atoms(Type,NrAtoms,MaxCard) -> MinCard=0
76 ; IntAtoms = unknown_atoms(true) -> MinCard=0, MaxCard=0 % preliminary, recomputed when the atoms are known
77 %; Card=64 % TO DO allow user to provide a custom upper bound ???
78 ; MinCard=0, MaxCard = inf).
79 integer_recalc2(general_sum(_,_,_),IntAtoms,Interval) :- !,
80 % SIGMA is translated to Kodkod's sum over a set of integer atoms (see kodkod_translate);
81 % the interval of the analysis is not sufficient to prevent overflows, e.g.,
82 % for s <: 0..20 & card(s) = 4 & SIGMA(z).(z:s|z) = 3 Kodkod finds s = {14,15,18,20}
83 % (the sum 67 overflows to 3 with 7 bits)
84 ( IntAtoms = atoms(AtomRange) -> sum_of_atoms_range(AtomRange,Interval)
85 ; IntAtoms = unknown_atoms(true), Interval = irange(0,0)). % preliminary
86 integer_recalc2(Expr,_,Interval) :- integer_recalc2(Expr,Interval).
87
88 % probkodkod always creates the atoms min(A,0)..max(B,0), see kodkod_process:extract_int_types
89 nr_of_atoms(none,0).
90 nr_of_atoms(irange(A,B),N) :- N is max(B,0)-min(A,0)+1.
91
92 % the minimal and maximal sum of a subset of the atoms A..B
93 sum_of_atoms_range(none,irange(0,0)).
94 sum_of_atoms_range(irange(A,B),irange(Min,Max)) :-
95 NegMax is min(B,-1), sum_interval(A,NegMax,Min),
96 PosMin is max(A,1), sum_interval(PosMin,B,Max).
97 sum_interval(A,B,0) :- A > B, !.
98 sum_interval(A,B,S) :- S is (A+B)*(B-A+1)//2.
99
100 :- use_module(probsrc(bsyntaxtree),[get_texpr_set_type/2]).
101 :- use_module(probsrc(debug),[debug_println/2]).
102
103 integer_recalc2(value(IV),irange(I,I)) :- nonvar(IV), IV=int(I), number(I).
104 integer_recalc2(integer(I),irange(I,I)).
105 integer_recalc2(add(A,B),C) :-
106 get_interval_info(A,AI), get_interval_info(B,BI),
107 interval_addition(AI,BI,C).
108 integer_recalc2(minus(A,B),C) :-
109 get_interval_info(A,AI), get_interval_info(B,BI),
110 interval_subtraction(AI,BI,C).
111 integer_recalc2(unary_minus(A),C) :-
112 get_interval_info(A,AI),
113 interval_negation(AI,C).
114 integer_recalc2(multiplication(A,B),C) :-
115 get_interval_info(A,AI), get_interval_info(B,BI),
116 interval_multiplication(AI,BI,C).
117 integer_recalc2(div(A,B),C) :-
118 get_interval_info(A,AI), get_interval_info(B,BI),
119 AI=irange(Am,AMNr),BI=irange(Bm,_BM),
120 ( number(Bm), Bm>=0 ->
121 % the result lies between A and 0, e.g., 5/10 = 0 for A:5..10
122 (number(Am), Am > 0 -> Cm = 0 ; Cm = Am),
123 (number(AMNr), AMNr < 0 -> CM = 0 ; CM = AMNr),
124 C = irange(Cm,CM)
125 ; number(Am),number(AMNr) ->
126 M is max(abs(Am),abs(AMNr)), MinM is -M,
127 C = irange(MinM,M)
128 ;
129 C = irange(-inf,inf)).
130 integer_recalc2(floored_div(A,B),C) :-
131 % the Kodkod translation computes A - (((A mod B) + B) mod B), see kodkod_translate;
132 % the interval must also cover these intermediate values to avoid an overflow
133 get_interval_info(A,irange(Am,AM)), get_interval_info(B,irange(Bm,BM)),
134 ( number(Am),number(AM),number(Bm),number(BM) ->
135 MA is max(abs(Am),abs(AM)), MB is max(abs(Bm),abs(BM)),
136 M is max(MA+MB,2*MB), MinM is -M,
137 C = irange(MinM,M)
138 ;
139 C = irange(-inf,inf)).
140 integer_recalc2(modulo(_A,B),irange(0,M)) :-
141 get_interval_info(B,irange(_Bm,BM)),
142 M infis BM-1.
143 % TO DO: use definitely_not_empty_and_finite from b_ast_cleanup for MinCard ?
144
145 :- use_module(library(lists),[maplist/3]).
146 extract_min_max_card(b(E,_,_),Type,MinCard,MaxCard) :- extract_min_max_card2(E,MinCard,MaxCardE),
147 ((max_type_cardinality(Type,CType), number(CType), CType < MaxCardE)
148 -> MaxCard = CType
149 ; MaxCard = MaxCardE).
150 extract_min_max_card2(comprehension_set(IDs,_), 0, Card) :-
151 maplist(extract_max_card_id,IDs,Cards),
152 simple_mul_list(Cards,1,Card).
153 extract_min_max_card2(set_extension(L), MinCard, MaxCard) :- length(L,MaxCard),
154 (MaxCard>0 -> MinCard=1 ; MinCard=0). % should always be 1
155 extract_min_max_card2(sequence_extension(L), MinCard, MaxCard) :- length(L,MaxCard),
156 (MaxCard>0 -> MinCard=1 ; MinCard=0). % should always be 1
157 extract_min_max_card2(empty_set,0,0).
158 extract_min_max_card2(empty_sequence,0,0).
159 % integer_set(_) ?
160 % TO DO: check with Daniel if ok
161 % I think this is ok as the comprehension set will be computed separately and will lead a value between 0 and Card, if extract_max_card_id succeeds; no overflow should ever occur here
162
163 extract_max_card_id(b(identifier(_),_,Info),MaxCard) :-
164 member(analysis(I),Info),
165 member(interval:irange(A,B),I), % should we support other analysis infos ??
166 number(A),number(B),
167 !,
168 MaxCard is B+1-A.
169 extract_max_card_id(b(_,Type,_),MaxCard) :- % use max card of type; maybe other identifiers have restricted cardinality
170 max_type_cardinality(Type,MaxCard), number(MaxCard).
171
172
173 max_card_with_integer_atoms(integer,NrAtoms,NrAtoms) :- !.
174 max_card_with_integer_atoms(couple(A,B),NrAtoms,Card) :- !,
175 max_card_with_integer_atoms(A,NrAtoms,CardA),
176 max_card_with_integer_atoms(B,NrAtoms,CardB),
177 Card is CardA * CardB.
178 max_card_with_integer_atoms(set(T),NrAtoms,Card) :- !,
179 max_card_with_integer_atoms(T,NrAtoms,C1),
180 catch( Card is ceiling(2 ** C1), error(_,_), fail).
181 max_card_with_integer_atoms(seq(T),NrAtoms,Card) :- !,
182 max_card_with_integer_atoms(set(couple(integer,T)),NrAtoms,Card).
183 max_card_with_integer_atoms(T,_,Card) :- max_type_cardinality(T,Card).
184
185 simple_mul_list([],A,A).
186 simple_mul_list([H|T],Acc,R) :- NA is Acc*H, simple_mul_list(T,NA,R).
187
188 % b(identifier(p),integer,[analysis([possible_values:irange(0,16),interval:irange(1,16)]),nodeid(pos(4360,1,383,8,383,8))])
189
190 get_interval_info(TExpr,I) :-
191 get_texpr_info(TExpr,Info),
192 memberchk(analysis(An),Info),
193 memberchk(interval:I,An).
194
195 safe_add_interval_info(Interval,Info,[analysis([interval:Interval|AnRest])|InfoRest]) :-
196 selectchk(analysis(A),Info,InfoRest),!,
197 (selectchk(interval:_,A,AnRest) -> true ; AnRest=A).
198 safe_add_interval_info(Interval,Info,[analysis([interval:Interval])|Info]).