1 % Heinrich Heine Universitaet Duesseldorf
2 % (c) 2021-2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(visb_static_check,[static_check_dynamic_update_def_body/1,
6 static_check_attribute_value_expression/2,
7 check_svg_attribute_value/3]).
8
9 :- use_module(probsrc(module_information),[module_info/2]).
10 :- module_info(group,visualization).
11 :- module_info(description,'This module provides static checks for VisB.').
12
13 :- use_module(probsrc(error_manager)).
14 :- use_module(probsrc(bsyntaxtree),[get_info_pos/2, get_texpr_id/2, member_in_conjunction/2]).
15
16 % try and extract potential static values from an update expression for attributes and check values are ok
17 % e.g., look inside IF-THEN-ELSE to check that branches provide valid values
18 static_check_dynamic_update_def_body(TypedExpr) :- \+ get_preference(visb_strict_checking,false),
19 %nl,translate:print_bexpr(TypedExpr),nl,
20 get_potential_value_for_svg_attr(TypedExpr,Attr,CandValue,CandPos),
21 %add_message(visb_lint,Attr,CandValue,CandPos),
22 check_svg_attribute_candidate_value(Attr,CandValue,CandPos),
23 fail.
24 static_check_dynamic_update_def_body(_).
25
26 % check if the typed expressions looks ok for the given attribute
27 static_check_attribute_value_expression(Attr,TExpr) :-
28 get_potential_value(TExpr,unknown,CandidateValue,CandPos),
29 check_svg_attribute_candidate_value(Attr,CandidateValue,CandPos),
30 fail.
31 static_check_attribute_value_expression(_Attr,_TExpr).
32
33 % extract potential values for a SVG attribute
34 get_potential_value_for_svg_attr(b(Expr,_,OuterPos),Attr,CandidateValue,CandPos) :-
35 get_potential_value_for_svg_attr2(Expr,OuterPos,Attr,CandidateValue,CandPos).
36 get_potential_value_for_svg_attr2(rec(Fields),OuterPos,Attr,CandidateValue,CandPos) :- !,
37 member(field(FAttr,RHS),Fields),
38 (FAttr=hovers
39 -> fail % will be checked separately by add_visb_hovers_from_definition
40 % get_potential_value_for_svg_attr(RHS,Attr,CandidateValue,CandPos)
41 ; Attr=FAttr,
42 get_potential_value(RHS,OuterPos,CandidateValue,CandPos)).
43 get_potential_value_for_svg_attr2(comprehension_set([TID],TPred),_OuterPos,Attr,CandidateValue,CandPos) :-
44 % detect Event-B style set comprehension; TODO: generalise this, detect other set comprehensions
45 get_texpr_id(TID,ID),
46 (TPred = b(exists(_,Body),_,_) -> true ; TPred=Body),
47 Equality = b(equal(TID2,RHS),_,_),
48 member_in_conjunction(Equality,Body),
49 !,
50 get_texpr_id(TID2,ID),
51 get_potential_value_for_svg_attr(RHS,Attr,CandidateValue,CandPos).
52 get_potential_value_for_svg_attr2(if_then_else(_,LHS,RHS),_OuterPos,Attr,CandidateValue,CandPos) :- !,
53 (get_potential_value_for_svg_attr(LHS,Attr,CandidateValue,CandPos) ;
54 get_potential_value_for_svg_attr(RHS,Attr,CandidateValue,CandPos)).
55 get_potential_value_for_svg_attr2(couple(LHS,RHS),_OuterPos,Attr,CandidateValue,CandPos) :- !,
56 (get_potential_value_for_svg_attr(LHS,Attr,CandidateValue,CandPos) ;
57 get_potential_value_for_svg_attr(RHS,Attr,CandidateValue,CandPos)).
58 get_potential_value_for_svg_attr2(let_expression(_,_,RHS),_OuterPos,Attr,CandidateValue,CandPos) :- !,
59 % Note: LET are typically already inlined
60 get_potential_value_for_svg_attr(RHS,Attr,CandidateValue,CandPos).
61 %get_potential_value_for_svg_attr2(E,_,_,_,_) :- write(uncovered_expr(E)),nl,fail.
62
63
64 get_potential_value(b(RHS,_,RPos),OuterPos,CandidateValue,CandPos) :-
65 (get_info_pos(RPos,NewPos) -> true ; NewPos=OuterPos),
66 get_potential_value_aux(RHS,NewPos,CandidateValue,CandPos).
67
68 get_potential_value_aux(V,OuterPos,CandidateValue,OuterPos) :- definite_value(V,Val),!,CandidateValue=Val.
69 get_potential_value_aux(if_then_else(_,LHS,RHS),OuterPos,CandidateValue,CandPos) :- !,
70 (get_potential_value(LHS,OuterPos,CandidateValue,CandPos) ;
71 get_potential_value(RHS,OuterPos,CandidateValue,CandPos)).
72 get_potential_value_aux(let_expression(_,_,RHS),OuterPos,CandidateValue,CandPos) :- !,
73 get_potential_value(RHS,OuterPos,CandidateValue,CandPos).
74 get_potential_value_aux(function(LHS,_ARG),OuterPos,CandidateValue,CandPos) :- !,
75 % visualisations often use functions to map objects to colours
76 get_potential_range_value(LHS,OuterPos,CandidateValue,CandPos).
77 %get_potential_value_aux(V,OuterPos,CandidateValue,OuterPos) :- write(uncovered_attribute_value(V)),nl,fail.
78
79 definite_value(string(S),string(S)).
80 definite_value(boolean_true,pred_true).
81 definite_value(boolean_false,pred_false).
82 definite_value(empty_set,[]).
83 definite_value(value(V),V).
84 % TODO: numbers, ...
85
86 % get a potential value from the range of a function:
87 get_potential_range_value(b(RHS,_,RPos),OuterPos,CandidateValue,CandPos) :-
88 (get_info_pos(RPos,NewPos) -> true ; NewPos=OuterPos),
89 get_potential_range_value_aux(RHS,NewPos,CandidateValue,CandPos).
90
91 :- use_module(probsrc(custom_explicit_sets),[try_expand_custom_set_with_catch/3, is_small_specific_custom_set/2]).
92 get_potential_range_value_aux(value(Val),OuterPos,CandidateValue,OuterPos) :- !,
93 is_small_specific_custom_set(Val,100),
94 try_expand_custom_set_with_catch(Val,ExpandedSet,get_potential_range_value),
95 member((_,CandidateValue),ExpandedSet).
96 get_potential_range_value_aux(set_extension(List),OuterPos,CandidateValue,OuterPos) :-
97 member(V,List),definite_range_tvalue(V,Val),!,CandidateValue=Val.
98 get_potential_range_value_aux(overwrite(A,B),OuterPos,CandidateValue,CandPos) :- !,
99 (get_potential_range_value(A,OuterPos,CandidateValue,CandPos)
100 ; get_potential_range_value(B,OuterPos,CandidateValue,CandPos)).
101 get_potential_range_value_aux(cartesian_product(_,B),OuterPos,CandidateValue,CandPos) :- !,
102 get_potential_set_element_value(B,OuterPos,CandidateValue,CandPos).
103 %get_potential_range_value_aux(V,OuterPos,CandidateValue,OuterPos) :- write(uncovered_function(V)),nl,fail.
104 % TODO: overwrite
105
106 definite_range_tvalue(b(couple(_,TRVAL),_,_),Val) :- TRVAL = b(RVAL,_,_), definite_value(RVAL,Val).
107
108 % get a potential value from a set
109 get_potential_set_element_value(b(RHS,_,RPos),OuterPos,CandidateValue,CandPos) :-
110 (get_info_pos(RPos,NewPos) -> true ; NewPos=OuterPos),
111 get_potential_set_element_value_aux(RHS,NewPos,CandidateValue,CandPos).
112
113 get_potential_set_element_value_aux(value(Val),OuterPos,CandidateValue,OuterPos) :- !,
114 is_small_specific_custom_set(Val,100),
115 try_expand_custom_set_with_catch(Val,ExpandedSet,get_potential_range_value),
116 member(CandidateValue,ExpandedSet).
117 get_potential_set_element_value_aux(set_extension(List),OuterPos,CandidateValue,OuterPos) :-
118 member(b(V,_,_),List),definite_value(V,Val),!,CandidateValue=Val.
119
120 % ---------------------
121
122
123 :- use_module(probsrc(tools_matching),[is_svg_attribute_with_fixed_text_values/3,
124 check_svg_attribute_text_alternative/2,
125 fix_svg_attribute_based_on_value/3, svg_attribute_default_value/2,
126 is_svg_color_attribute/1]).
127 :- use_module(probsrc(tools_strings),[ajoin/2,ajoin_with_sep/3]).
128 :- use_module(probsrc(preferences),[get_preference/2]).
129
130 check_svg_attribute_candidate_value(Name,Value,DefPos) :-
131 MsgPrefix = 'Potential value of SVG attribute "',
132 check_svg_attribute_value(Name,Value,DefPos,MsgPrefix).
133
134 check_svg_attribute_value(Name,Value,DefPos) :-
135 MsgPrefix = 'Value of SVG attribute "',
136 check_svg_attribute_value(Name,Value,DefPos,MsgPrefix).
137
138
139
140 check_svg_attribute_value(Name,Value,DefPos,_MsgPrefix) :- Value=string(S),
141 fix_svg_attribute_based_on_value(Name,S,OtherAttrName),
142 ajoin(['You seem to be using the wrong attribute "',Name,
143 '" instead of "',OtherAttrName,'" for the value: '],Msg),
144 add_warning(visb_visualiser,Msg,Value,DefPos),
145 fail. % also show alternative warnings below:
146 check_svg_attribute_value(Name,Value,DefPos,MsgPrefix) :-
147 is_svg_color_attribute(Name),
148 illegal_color(Value),!,
149 (Name=fill,
150 valid_animate_fill_color(Value) % TODO: pass svg_class and check if we have an animation object
151 -> add_debug_message(visb_visualiser,'Value of fill attribute not a colour but final state of animation: ',Value,DefPos)
152 ; valid_tk_color(Value)
153 -> ajoin([MsgPrefix,Name,'" is a TK but not an SVG colour: ' ],Msg),
154 add_warning(visb_visualiser,Msg,Value,DefPos)
155 ; ajoin([MsgPrefix,Name,'" is not a colour: ' ],Msg),
156 add_warning(visb_visualiser,Msg,Value,DefPos)
157 ).
158 check_svg_attribute_value(Name,Value,DefPos,MsgPrefix) :-
159 is_svg_attribute_with_fixed_text_values(Name,List,Alternative),
160 Value=string(S), % Note visb_visualiser calls e.g. b_value_to_text_string,
161 % which converts fd(_,_) values to string, so we only catch somee errors here involving strings
162 % pred_true, pred_false are also accepted for visibility
163 nonmember(S,List),
164 \+ check_svg_attribute_text_alternative(S,Alternative),
165 !,
166 ajoin_with_sep(List,',',Opts),
167 (Alternative = no_alternative
168 -> ajoin([MsgPrefix,Name,'" must be ',Opts,' and not: '],Msg)
169 ; ajoin([MsgPrefix,Name,'" must be ',Opts,'or ',Alternative,' and not: '],Msg)
170 ),
171 add_warning(visb_visualiser,Msg,Value,DefPos),
172 (S = '', svg_attribute_default_value(Name,Default)
173 -> ajoin(['Instead of "" for "',Name,'" you should probably use the default value: '],Msg2),
174 add_warning(visb_visualiser,Msg2,Default,DefPos)
175 ; true
176 ).
177 check_svg_attribute_value(_,_,_,_).
178
179
180 :- use_module(probsrc(b_global_sets),[is_b_global_constant_hash/3]).
181 % now checked by check_attribute_type for updates, we could later check strings, currentcolor is allowed
182 illegal_color(pred_false).
183 illegal_color(pred_true).
184 illegal_color([]).
185 illegal_color(avl_set(_)).
186 illegal_color([_|_]).
187 illegal_color(closure(_,_,_)).
188 illegal_color(term(floating(_))).
189 illegal_color(string(Atom)) :- illegal_color_name(Atom).
190 illegal_color(fd(Nr,GSet)) :- is_b_global_constant_hash(GSet,Nr,Atom), illegal_color_name(Atom).
191
192 :- use_module(probsrc(tools_strings),[is_ascii_id_codes/1]).
193 :- use_module(probsrc(tools_matching),[check_is_svg_color_name/1]).
194 illegal_color_name(Atom) :- atom(Atom),
195 \+ check_is_svg_color_name(Atom),
196 atom_codes(Atom,Codes),
197 is_ascii_id_codes(Codes). % TODO: check other formats like #...., rgb(_,_,_); check if it is a known Tk name
198
199
200 :- use_module(probsrc(preferences),[valid_rgb_color/1]).
201 valid_tk_color(string(Atom)) :- valid_rgb_color(Atom).
202 valid_tk_color(fd(Nr,GSet)) :- is_b_global_constant_hash(GSet,Nr,Atom), valid_rgb_color(Atom).
203
204
205 % the fill attribute for animate, animateTransform, animateMotion, set can be this:
206 valid_animate_fill_color(string(Atom)) :- animate_fill_color_name(Atom).
207 animate_fill_color_name(freeze). % Keep state of last animation frame
208 animate_fill_color_name(remove). % Keep state of first animation frame