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]).