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