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]). | |
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(probsrc(interval_calc)). | |
17 | :- use_module(probsrc(inf_arith)). | |
18 | ||
19 | :- use_module(probsrc(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 | create_texpr(Expr,Type,Info,TExpr), | |
50 | create_texpr(NExpr,Type,NInfo,NTExpr), | |
51 | syntaxtransformation(Expr,Subs,_,NSubs,NExpr), | |
52 | maplist(integer_recalc,Subs,NSubs), | |
53 | ( integer_recalc2(NExpr,Interval) -> | |
54 | safe_add_interval_info(Interval,Info,NInfo) | |
55 | ; otherwise -> | |
56 | Info=NInfo). | |
57 | ||
58 | :- use_module(probsrc(bsyntaxtree),[get_texpr_set_type/2]). | |
59 | :- use_module(probsrc(debug),[debug_println/2]). | |
60 | ||
61 | integer_recalc2(value(IV),irange(I,I)) :- nonvar(IV), IV=int(I), number(I). | |
62 | integer_recalc2(integer(I),irange(I,I)). | |
63 | integer_recalc2(add(A,B),C) :- | |
64 | get_interval_info(A,AI), get_interval_info(B,BI), | |
65 | interval_addition(AI,BI,C). | |
66 | integer_recalc2(minus(A,B),C) :- | |
67 | get_interval_info(A,AI), get_interval_info(B,BI), | |
68 | interval_subtraction(AI,BI,C). | |
69 | integer_recalc2(unary_minus(A),C) :- | |
70 | get_interval_info(A,AI), | |
71 | interval_negation(AI,C). | |
72 | integer_recalc2(multiplication(A,B),C) :- | |
73 | get_interval_info(A,AI), get_interval_info(B,BI), | |
74 | interval_multiplication(AI,BI,C). | |
75 | integer_recalc2(division(A,B),C) :- | |
76 | get_interval_info(A,AI), get_interval_info(B,BI), | |
77 | AI=irange(Am,AM),BI=irange(Bm,_BM), | |
78 | ( number(Bm), Bm>=0 -> C = AI | |
79 | ; number(Am),number(AM) -> | |
80 | M is max(abs(Am),abs(AM)), | |
81 | C = irange(-M,M) | |
82 | ; otherwise -> | |
83 | C = irange(-inf,inf)). | |
84 | integer_recalc2(modulo(_A,B),irange(0,M)) :- | |
85 | get_interval_info(B,irange(_Bm,BM)), | |
86 | M infis BM-1. | |
87 | integer_recalc2(card(S),irange(MinCard,MaxCard)) :- | |
88 | % TODO[DP,2016-04-20]: This is a very pessimistic approach: | |
89 | % The cardinality is maximally as high as the type allows | |
90 | % Maybe an alternative approach would be to add a second infered information to each node, | |
91 | % the "guaranteed" integer interval which is independent of overflows. E.g. "card({a,b,c}) : 1..3" | |
92 | get_texpr_set_type(S,Type), | |
93 | % print(recalc(Type,S)),nl, | |
94 | ( extract_min_max_card(S,Type,C1,C2) -> (MinCard,MaxCard)=(C1,C2), | |
95 | debug_println(9,extract_max_card_for_kodkod(C1,C2)) | |
96 | ; max_type_cardinality(Type,MaxCard) -> MinCard=0 | |
97 | %; otherwise -> Card=64 % TO DO allow user to provide a custom upper bound ??? | |
98 | ; otherwise -> MinCard=0, MaxCard = inf). | |
99 | ||
100 | % TO DO: use definitely_not_empty_and_finite from b_ast_cleanup for MinCard ? | |
101 | ||
102 | :- use_module(library(lists),[maplist/3]). | |
103 | extract_min_max_card(b(E,_,_),Type,MinCard,MaxCard) :- extract_min_max_card2(E,MinCard,MaxCardE), | |
104 | ((max_type_cardinality(Type,CType), number(CType), CType < MaxCardE) | |
105 | -> MaxCard = CType | |
106 | ; MaxCard = MaxCardE). | |
107 | extract_min_max_card2(comprehension_set(IDs,_), 0, Card) :- | |
108 | maplist(extract_max_card_id,IDs,Cards), | |
109 | simple_mul_list(Cards,1,Card). | |
110 | extract_min_max_card2(set_extension(L), MinCard, MaxCard) :- length(L,MaxCard), | |
111 | (MaxCard>0 -> MinCard=1 ; MinCard=0). % should always be 1 | |
112 | extract_min_max_card2(sequence_extension(L), MinCard, MaxCard) :- length(L,MaxCard), | |
113 | (MaxCard>0 -> MinCard=1 ; MinCard=0). % should always be 1 | |
114 | extract_min_max_card2(empty_set,0,0). | |
115 | extract_min_max_card2(empty_sequence,0,0). | |
116 | % integer_set(_) ? | |
117 | % TO DO: check with Daniel if ok | |
118 | % 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 | |
119 | ||
120 | extract_max_card_id(b(identifier(_),_,Info),MaxCard) :- | |
121 | member(analysis(I),Info), | |
122 | member(interval:irange(A,B),I), % should we support other analysis infos ?? | |
123 | number(A),number(B), | |
124 | !, | |
125 | MaxCard is B+1-A. | |
126 | extract_max_card_id(b(_,Type,_),MaxCard) :- % use max card of type; maybe other identifiers have restricted cardinality | |
127 | max_type_cardinality(Type,MaxCard), number(MaxCard). | |
128 | ||
129 | ||
130 | simple_mul_list([],A,A). | |
131 | simple_mul_list([H|T],Acc,R) :- NA is Acc*H, simple_mul_list(T,NA,R). | |
132 | ||
133 | % b(identifier(p),integer,[analysis([possible_values:irange(0,16),interval:irange(1,16)]),nodeid(pos(4360,1,383,8,383,8))]) | |
134 | ||
135 | get_interval_info(TExpr,I) :- | |
136 | get_texpr_info(TExpr,Info), | |
137 | memberchk(analysis(An),Info), | |
138 | memberchk(interval:I,An). | |
139 | ||
140 | safe_add_interval_info(Interval,Info,[analysis([interval:Interval|AnRest])|InfoRest]) :- | |
141 | selectchk(analysis(A),Info,InfoRest),!, | |
142 | ( selectchk(interval:_,A,AnRest) -> true | |
143 | ; otherwise -> AnRest=A). | |
144 | safe_add_interval_info(Interval,Info,[analysis([interval:Interval])|Info]). |