1 | % (c) 2013-2022 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(bmachine_static_checks, [static_check_main_machine/1, extended_static_check_machine/0, | |
6 | toplevel_raw_predicate_sanity_check/4]). | |
7 | ||
8 | :- use_module(probsrc(module_information)). | |
9 | :- module_info(group,typechecker). | |
10 | :- module_info(description,'Static checking of B machines upon construction. Detection of name clashes and uninitalised variables.'). | |
11 | ||
12 | :- use_module(bmachine_structure, [get_section/3]). | |
13 | :- use_module(b_read_write_info, [get_accessed_vars/4]). | |
14 | :- use_module(bsyntaxtree, [get_texpr_expr/2,get_texpr_id/2,get_texpr_ids/2, get_texpr_info/2]). | |
15 | :- use_module(error_manager, [add_warning/3, add_warning/4, add_error/4, add_message/4]). | |
16 | :- use_module(debug, [debug_println/2]). | |
17 | :- use_module(tools, [ajoin/2]). | |
18 | :- use_module(library(lists)). | |
19 | ||
20 | static_check_main_machine(Machine) :- | |
21 | debug_println(19,'Running static machine checks'), | |
22 | initialises_all_variables(Machine), | |
23 | check_name_clashes(Machine). | |
24 | ||
25 | ||
26 | % --------------------------------------------- | |
27 | % check for unnatural invariants and properties | |
28 | % --------------------------------------------- | |
29 | % the priority of the implication is sometimes surprising | |
30 | % a & (x=1) => (y=2) & c --> top-level symbol is the implication ! | |
31 | % the test is done on the raw predicate before ast_cleanup removes potential typing predicates; see tests 106, 107 | |
32 | toplevel_raw_predicate_sanity_check(invariant,MachName,RawPredicate,Infos) :- | |
33 | ? | member(has_variables,Infos), % otherwise it is ok to have just a single disjunt, implication,... |
34 | check_top_level(RawPredicate,MachName,'INVARIANT'), | |
35 | fail. | |
36 | toplevel_raw_predicate_sanity_check(properties,MachName,RawPredicate,Infos) :- | |
37 | member(has_constants,Infos), % otherwise it is ok to have just a single disjunt, implication,... | |
38 | check_top_level(RawPredicate,MachName,'PROPERTIES'), | |
39 | fail. | |
40 | toplevel_raw_predicate_sanity_check(_,_,_,_). | |
41 | ||
42 | % typical error: forget parentheses; if we write P => Q & R --> this is parsed as P => (Q & R) | |
43 | check_top_level(implication(_,B,C),MachName,SECT) :- | |
44 | (composed_predicate(B) ; composed_predicate(C)),!, | |
45 | add_warning(bmachine_static_checks,'Top-level implication (=>) in clause: ',MachName:SECT). | |
46 | check_top_level(disjunct(_,B,C),MachName,SECT) :- | |
47 | (composed_predicate(B) ; composed_predicate(C)),!, | |
48 | add_warning(bmachine_static_checks,'Top-level disjunction (or) in clause: ',MachName:SECT). | |
49 | check_top_level(equivalence(_,B,C),MachName,SECT) :- | |
50 | (composed_predicate(B) ; composed_predicate(C)),!, | |
51 | add_warning(bmachine_static_checks,'Top-level equivalence (<=>) in clause: ',MachName:SECT). | |
52 | ||
53 | % check if a predicate is composed of a binary operator where confusion may arise | |
54 | % with negation and quantification there are explicit parentheses; the user should not be confused | |
55 | composed_predicate(A) :- functor(A,Operator,N), | |
56 | boolean_operator(Operator), | |
57 | % Some binary operators (conjunct, disjunct) can have a varying number of arguments. | |
58 | % See predicates associative_functor/1 and unflatten_assoc/4 in btypechecker. | |
59 | N >= 2. | |
60 | boolean_operator(conjunct). | |
61 | boolean_operator(disjunct). | |
62 | boolean_operator(implication). | |
63 | boolean_operator(equivalence). | |
64 | ||
65 | % --------------------- | |
66 | % Checks is all variables are initialised by the machine | |
67 | % --------------------- | |
68 | initialises_all_variables(Machine) :- | |
69 | get_section(initialisation,Machine,Initialisation), | |
70 | % check wich variables are read / modified by the initialisation | |
71 | get_accessed_vars(Initialisation,[],Modifies,_Reads), | |
72 | get_machine_variables(Machine,SortedAllVars), | |
73 | % check for each variable, if the initialisation modifies it | |
74 | exclude(is_initialised(Modifies),SortedAllVars,Uninitialised), | |
75 | % generate a warning if unitialised is not empty | |
76 | generate_uninitialised_warning(Uninitialised,Initialisation), | |
77 | % now check order of initialisation sequences | |
78 | check_initialisation_order(Initialisation,SortedAllVars,[],_). | |
79 | ||
80 | get_machine_variables(Machine,SortedAllVars) :- | |
81 | % get all variables that should be initialised | |
82 | get_section(abstract_variables,Machine,AbsVars), | |
83 | get_section(concrete_variables,Machine,ConcVars), | |
84 | append(AbsVars,ConcVars,TAllVars), | |
85 | get_texpr_ids(TAllVars,AllVars), | |
86 | sort(AllVars,SortedAllVars). | |
87 | ||
88 | is_initialised(Modifies,Id) :- | |
89 | memberchk(Id,Modifies). | |
90 | ||
91 | generate_uninitialised_warning([],_) :- !. | |
92 | generate_uninitialised_warning(Vars,Initialisation) :- | |
93 | Msg='Machine may not initialise some of its variables: ', | |
94 | add_warning(bmachine_static_checks,Msg,Vars,Initialisation). | |
95 | ||
96 | ||
97 | :- use_module(library(ordsets)). | |
98 | % Check if order of sequential compositions in INITIALISATION is ok | |
99 | % TO DO: add support for if(LIST) and while | |
100 | check_initialisation_order(b(Subst,subst,Info),AllVars,AlreadyInit,OutInit) :- | |
101 | check_initialisation_order2(Subst,Info,AllVars,AlreadyInit,OutInit),!. | |
102 | check_initialisation_order(Subst,AllVars,AlreadyInit,OutInit) :- | |
103 | % print('CHCK '), translate:print_subst(Subst),nl, | |
104 | get_accessed_vars(Subst,[],Modifies,Reads), | |
105 | check_subst_or_pred(Subst,Modifies,Reads,AllVars,AlreadyInit,OutInit). | |
106 | ||
107 | check_subst_or_pred(Subst,Modifies,Reads,AllVars,AlreadyInit,OutInit) :- | |
108 | ord_union(Modifies,AlreadyInit,OutInit), % after Subst we have initialised OutInit | |
109 | % below is already checked by type checker: | |
110 | %ord_subtract(Modifies,AllVars,IllegalAssignments), | |
111 | %(IllegalAssignments=[] -> true | |
112 | % ; add_warning(bmachine_static_checks,'INITIALISATION writes illegal variables: ',IllegalAssignments,Subst)), | |
113 | ord_intersection(Reads,AllVars,ReadFromSameMachine), | |
114 | (atomic_subst(Subst) | |
115 | -> ord_subtract(ReadFromSameMachine,AlreadyInit,IllegalReads) | |
116 | ; ord_subtract(ReadFromSameMachine,OutInit,IllegalReads) % we use OutInit: there could be an if with sequence inside | |
117 | ), | |
118 | (IllegalReads=[] -> true | |
119 | ; add_warning(bmachine_static_checks,'INITIALISATION reads variables which are not yet initialised: ',IllegalReads,Subst)). | |
120 | ||
121 | :- use_module(bsyntaxtree,[find_identifier_uses/3]). | |
122 | check_initialisation_order2(choice([First|T]),Info,AllVars,AlreadyInit,OutInit) :- !, | |
123 | check_initialisation_order(First,AllVars,AlreadyInit,OutInit), % we pick the output of the first choice | |
124 | (T=[] -> true ; check_initialisation_order(b(choice(T),subst,Info),AllVars,AlreadyInit,_)). | |
125 | check_initialisation_order2(parallel([First|T]),Info,AllVars,AlreadyInit,OutInit) :- !, | |
126 | check_initialisation_order(First,AllVars,AlreadyInit,OutInit1), % we pick the output of the first choice | |
127 | (T=[] -> OutInit=OutInit1 | |
128 | ; check_initialisation_order2(parallel(T),Info,AllVars,AlreadyInit,OutInitRest), | |
129 | ord_union(OutInit1,OutInitRest,OutInit) | |
130 | ). | |
131 | check_initialisation_order2(init_parallel(S),Info,AllVars,AlreadyInit,OutInit) :- !, | |
132 | check_initialisation_order(b(parallel(S),subst,Info),AllVars,AlreadyInit,OutInit). | |
133 | check_initialisation_order2(sequence([First|T]),Info,AllVars) --> !, | |
134 | check_initialisation_order(First,AllVars), | |
135 | ({T=[]} -> [] ; check_initialisation_order(b(sequence(T),subst,Info),AllVars)). | |
136 | check_initialisation_order2(any(_Ids,Pred,Subst),_Info,AllVars,AlreadyInit,OutInit) :- !, | |
137 | find_identifier_uses(Pred,[],Reads), | |
138 | check_subst_or_pred(Pred,[],Reads,AllVars,AlreadyInit,_), % check predicate reads are ok | |
139 | check_initialisation_order(Subst,AllVars,AlreadyInit,OutInit). | |
140 | % TO DO: also check if-then-else, while, ... | |
141 | ||
142 | atomic_subst(b(S,_,_)) :- atomic_subst2(S). | |
143 | atomic_subst2(skip). | |
144 | atomic_subst2(assign(_,_)). | |
145 | atomic_subst2(assign_single_id(_,_)). | |
146 | atomic_subst2(becomes_element_of(_,_)). | |
147 | %atomic_subst2(becomes_such(_,_)). % this needs to be dealt with separately, e.g., test 583 p,solved : (p = %i.(i : 1 .. 9|0) & solved = 0) | |
148 | ||
149 | % --------------------- | |
150 | % Checks if an operations parameter or local variable clashes with a variable | |
151 | % --------------------- | |
152 | check_name_clashes(Machine) :- | |
153 | debug_println(10,'Checking for name clashes'), | |
154 | get_all_machine_ids(Machine,SortedAllIds), | |
155 | % for each operation, compare the parameter names with existing vars/constants | |
156 | get_section(operation_bodies,Machine,Operations), | |
157 | maplist(op_name_clashes(SortedAllIds),Operations), | |
158 | get_section(definitions,Machine,Defs), | |
159 | maplist(def_name_clashes(SortedAllIds),Defs). | |
160 | ||
161 | get_all_machine_ids(Machine,SortedAllIds) :- | |
162 | % get all variables and constants that might clash | |
163 | get_section_ids(abstract_variables,Machine,'variable',AbsVars), | |
164 | get_section_ids(concrete_variables,Machine,'variable',ConcVars), | |
165 | get_section_ids(abstract_constants,Machine,'constant',AbsCons), | |
166 | get_section_ids(concrete_constants,Machine,'constant',ConcCons), | |
167 | get_section_ids(deferred_sets,Machine,'set',DefSets), | |
168 | get_section_ids(enumerated_sets,Machine,'set',EnumSets), | |
169 | get_section_ids(enumerated_elements,Machine,'set element',EnumElems), | |
170 | % enumerated b_get_named_machine_set(GlobalSetName,ListOfConstants) + b_get_machine_set(S) | |
171 | append([AbsVars,ConcVars,AbsCons,ConcCons,DefSets,EnumSets,EnumElems],AllIds), | |
172 | keyword_clash(AllIds), | |
173 | sort(AllIds,SortedAllIds). | |
174 | ||
175 | get_section_ids(Section,Machine,Class,ResultList) :- | |
176 | get_section(Section,Machine,Vars), | |
177 | findall(machine_id(ID,Class,Pos,Section), | |
178 | (member(TID,Vars),get_texpr_id(TID,ID),get_texpr_info(TID,Pos)),ResultList). | |
179 | ||
180 | ||
181 | :- use_module(tools_matching,[is_b_keyword/2]). | |
182 | ||
183 | % can be useful for Z, TLA+, Event-B machines: | |
184 | % Clashes may lead to strange type or parse errors in VisB, REPL, ... | |
185 | keyword_clash(AllIds) :- | |
186 | ? | member(machine_id(Name,Class,Pos,Section),AllIds), |
187 | ? | is_b_keyword(Name,_), |
188 | get_descr(Pos,Section,Descr), | |
189 | ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a classical B keyword (may lead to unexpected parse or type errors when entering formulas unless you surround it by backquotes: `',Name,'`).'], Msg), | |
190 | ? | (classical_b_mode |
191 | -> add_message(bmachine_static_checks,Msg,'',Pos) % user probably uses new backquote syntax already | |
192 | ; add_warning(bmachine_static_checks,Msg,'',Pos) | |
193 | ), | |
194 | fail. | |
195 | keyword_clash(_). | |
196 | ||
197 | :- use_module(bsyntaxtree,[map_over_typed_bexpr/2]). | |
198 | :- use_module(external_functions,[is_external_function_name/1]). | |
199 | ||
200 | def_name_clashes(AllIds,definition_decl(Name,DefType,_DefPos,Args,_RawExpr,_Deps)) :- !, | |
201 | (is_external_function_name(Name) | |
202 | -> true % do not check external predicates, functions, subst | |
203 | % they are not written by user and possibly not used and definitions are virtual and not used anyway | |
204 | ; findall(b(identifier(ID),any,[nodeid(IdPos)]), | |
205 | member(identifier(IdPos,ID),Args),ArgIds), % args can sometimes not be identifiers; see test 1711 | |
206 | debug_println(4,checking_def(Name,DefType,Args,ArgIds)), | |
207 | include(clash_warnings('DEFINITION parameter',AllIds,'DEFINITION',Name),ArgIds,_ArgsCausingWarning) | |
208 | % TO DO: check Body; for this we need a map_over_raw_expression to detect local variables introduced ! | |
209 | ). | |
210 | def_name_clashes(_,D) :- print(unknown_def(D)),nl. | |
211 | ||
212 | :- use_module(preferences,[get_preference/2]). | |
213 | op_name_clashes(AllIds,Operation) :- | |
214 | get_texpr_expr(Operation,operation(IdFull,Results,Params,Subst)), | |
215 | %get_texpr_id(IdFull,op(Id)), | |
216 | IdFull = b(identifier(op(Id)),Type,Info), | |
217 | (get_preference(clash_strict_checks,true) | |
218 | -> include(clash_warnings('Operation name',AllIds,operation,Id),[b(identifier(Id),Type,Info)],_NameCausingWarning) % fix PROB-60 | |
219 | ; true), | |
220 | include(clash_warnings('Operation parameter',AllIds,operation,Id),Params,_ParamsCausingWarning), | |
221 | include(clash_warnings('Operation result variable',AllIds,operation,Id),Results,_ResultsCausingWarning), | |
222 | ? | (map_over_typed_bexpr(bmachine_static_checks:check_operation_body_clashes(AllIds,Id),Subst),fail ; true). |
223 | ||
224 | :- public check_operation_body_clashes/3. | |
225 | check_operation_body_clashes(AllIds,Operation,TSubst) :- | |
226 | get_texpr_expr(TSubst,Subst), | |
227 | ? | (local_variable_clash(Subst,TSubst,AllIds,Operation); |
228 | ? | illegal_op_call(Subst,Operation)). |
229 | ||
230 | local_variable_clash(Subst,TSubst,AllIds,Operation) :- | |
231 | ? | introduces_local_variable(Subst,ID), |
232 | clash_local_warnings(AllIds,Operation,ID,TSubst). | |
233 | ||
234 | % check if something like zz(1) <-- Op(a) is used; this is not allowed according to Atelier-B | |
235 | illegal_op_call(operation_call(CalledOperation,Results,_Parameters),Operation) :- | |
236 | ? | member(TID,Results), \+ get_texpr_id(TID,_), |
237 | (get_texpr_id(CalledOperation,op(CalledId)) -> true ; CalledId=CalledOperation), | |
238 | ajoin(['Return value of operation call to ',CalledId,' must be stored in identifier within:'],Msg), | |
239 | add_error(bmachine_static_checks,Msg,Operation,TID). | |
240 | ||
241 | % check for constructs which introduced local variables | |
242 | introduces_local_variable(var(Parameters,_),ID) :- | |
243 | % currently B-interpreter cannot correctly deal with this in the context of operation_call | |
244 | ? | member(TID,Parameters), get_texpr_id(TID,ID). |
245 | ||
246 | :- use_module(probsrc(error_manager),[extract_span_description/2]). | |
247 | % ord_member does not work below because of free variable Class | |
248 | my_ord_member(Name,Class,Descr,[machine_id(Name1,_,_,_)|T]) :- | |
249 | Name @> Name1, !, | |
250 | my_ord_member(Name,Class,Descr,T). | |
251 | my_ord_member(Name,Class,Descr,[machine_id(Name,Class,Pos,Section)|_]) :- | |
252 | get_descr(Pos,Section,Descr). | |
253 | ||
254 | get_descr(Pos,Section,Descr) :- | |
255 | (extract_span_description(Pos,Descr) -> true | |
256 | ; ajoin(['from section ',Section],Descr) ). | |
257 | ||
258 | clash_warnings(Context,AllIds,OpOrDef,OperationId,TName) :- | |
259 | get_texpr_id(TName,Name), | |
260 | my_ord_member(Name,Class,Descr,AllIds), !, | |
261 | ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a ', | |
262 | Context, ' in ',OpOrDef,' "', OperationId,'".'], Msg), | |
263 | add_warning(bmachine_static_checks,Msg,'',TName). | |
264 | ||
265 | clash_local_warnings(AllIds,OperationId,Name,Pos) :- | |
266 | my_ord_member(Name,Class,Descr,AllIds), !, | |
267 | % we could check and see if Name is really visible from this location! | |
268 | % (see public_examples/B/Other/LustreTranslations/UMS_verif/M_UMS_verif.mch) | |
269 | ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a local variable in operation "', OperationId,'".'], Msg), | |
270 | add_warning(bmachine_static_checks,Msg,'',Pos). | |
271 | ||
272 | % TODO: this does not and can not work here: | |
273 | % - Some preconditions are removed (typing only....) during machine simplification | |
274 | % - Needs to be verified during typechecking | |
275 | % --------------------- | |
276 | % Checks if an operations parameter is not typed by a pre condition | |
277 | % --------------------- | |
278 | %parameters_without_pre_condition(Machine) :- | |
279 | % get_section(operation_bodies,Machine,Operations), | |
280 | % maplist(parameters_without_pre_condition_aux,Operations). | |
281 | % | |
282 | %parameters_without_pre_condition_aux(Operation) :-trace, | |
283 | % get_texpr_expr(Operation,operation(IdFull,_Results,Params,Subst)), | |
284 | % get_texpr_id(IdFull,op(Id)), | |
285 | % (Params == [] | |
286 | % -> true % no parameters | |
287 | % ; (get_texpr_expr(Subst,precondition(_,_)) | |
288 | % -> true % parameters and precondition | |
289 | % ; ajoin(['Operation ', Id, ' has parameters but no pre-condition.'], Msg), | |
290 | % add_warning(bmachine_static_checks,Msg) | |
291 | % )). | |
292 | ||
293 | ||
294 | % EXTENDED ADDITIONAL CHECKS | |
295 | % these are run (optionally) after machine is loaded and bmachine pre-calculations have run | |
296 | ||
297 | :- use_module(b_read_write_info,[check_all_variables_written/0]). | |
298 | ||
299 | extended_static_check_machine :- | |
300 | check_all_variables_written, | |
301 | esc_aux. | |
302 | ||
303 | :- use_module(probsrc(bmachine), [b_get_main_filename/1, b_machine_name/1, b_get_machine_header_position/2]). | |
304 | :- use_module(tools,[get_modulename_filename/2, get_filename_extension/2]). | |
305 | :- use_module(bsyntaxtree,[map_over_typed_bexpr_with_names/2]). | |
306 | :- use_module(specfile,[get_specification_description/2, animation_minor_mode/1, classical_b_mode/0]). | |
307 | :- use_module(bmachine). | |
308 | :- use_module(b_machine_hierarchy,[machine_type/2, machine_operations/2]). | |
309 | ||
310 | esc_aux :- | |
311 | b_machine_name(Name), | |
312 | b_get_main_filename(Filename), | |
313 | get_modulename_filename(Filename,ModuleName), | |
314 | Name \= ModuleName, | |
315 | (atom_concat('MAIN_MACHINE_FOR_',RealName,Name) % see dummy_machine_name in bmachine_construction | |
316 | -> RealName \= ModuleName | |
317 | ; is_dummy_machine_name(Name,Filename) | |
318 | -> fail % dummy Rules DSL or Alloy machine name, do not create warning | |
319 | ; true | |
320 | ), | |
321 | (b_get_machine_header_position(Name,Span) -> true | |
322 | ; Span = src_position_with_filename(1,1,1,Filename)), | |
323 | get_specification_description(machine,MCH), | |
324 | ajoin(['Filename ',ModuleName,' does not match name of ', MCH, ': '],Msg), | |
325 | add_warning(bmachine_static_checks,Msg,Name,Span), | |
326 | fail. | |
327 | esc_aux :- debug_println(19,checking_identifiers_for_clashes), | |
328 | full_b_machine(Machine), | |
329 | local_quantified_variable_clashes(Machine), | |
330 | fail. | |
331 | esc_aux :- machine_type(MachName,abstract_machine), | |
332 | machine_operations(MachName,Ops), | |
333 | member(identifier(Span,OpName),Ops), | |
334 | atom_codes(OpName,Codes), member(46,Codes), % "." element of name | |
335 | % Section 7.23, paragraph 2 of Atelier-B handbook: in abstract machine we cannot use renamed operation names | |
336 | ajoin(['Operation name in abstract machine ',MachName,' is composed: '],Msg), | |
337 | add_warning(bmachine_static_checks,Msg,OpName,Span), | |
338 | fail. | |
339 | esc_aux :- debug_println(19,checking_operation_bodies), | |
340 | b_get_machine_operation(ID,_Res,_TParas,Body,_OType,_Pos), | |
341 | check_operation_body(Body,ID), | |
342 | fail. | |
343 | esc_aux :- | |
344 | check_concrete_constants, | |
345 | check_unused_ids. | |
346 | ||
347 | :- use_module(probsrc(tools_strings), [atom_prefix/2]). | |
348 | is_dummy_machine_name(Name,_) :- atom_prefix('__RULES_MACHINE_Main',Name). | |
349 | is_dummy_machine_name(alloytranslation,_) :- animation_minor_mode(alloy). | |
350 | is_dummy_machine_name('DEFINITION_FILE',Filename) :- classical_b_mode, | |
351 | get_filename_extension(Filename,'def'). | |
352 | % when opening .def files; WARNING: sometimes def files use other extensions | |
353 | ||
354 | % TO DO: optionally do these kinds of checks in the REPL | |
355 | local_quantified_variable_clashes(Machine) :- | |
356 | get_all_machine_ids(Machine,SortedAllIds), | |
357 | ? | (get_typed_section(Sec,SecID,Pred), |
358 | debug_println(19,checking_local_quantified_variable_clashes(Sec,SecID)), | |
359 | map_over_typed_bexpr_with_names(bmachine_static_checks:check_introduced_ids(Sec,SecID,SortedAllIds),Pred) | |
360 | ; | |
361 | check_definition_clashes(SortedAllIds) | |
362 | ), | |
363 | fail. | |
364 | local_quantified_variable_clashes(_). | |
365 | ||
366 | :- use_module(bmachine,[b_get_typed_definition/3]). | |
367 | check_definition_clashes(SortedAllIds) :- | |
368 | Scope=[variables], | |
369 | b_get_typed_definition(Name,Scope,TExpr), | |
370 | % TODO: adapt type_check_definitions to return definitions with paras and add paras to list of Ids | |
371 | %print(check(Name,SortedAllIds)),nl, | |
372 | map_over_typed_bexpr_with_names(bmachine_static_checks:check_introduced_ids('DEFINITION',Name,SortedAllIds),TExpr). | |
373 | ||
374 | :- public check_introduced_ids/5. % used in map above | |
375 | check_introduced_ids(Section,SectionID,SortedAllIds,TExpr,TNames) :- | |
376 | \+ ignore_constructor(TExpr), | |
377 | (member(TName,TNames), | |
378 | clash_warnings('local variable',SortedAllIds,Section,SectionID,TName) | |
379 | ; removed_identifier(TExpr,TName), | |
380 | clash_warnings('(removed) local variable',SortedAllIds,Section,SectionID,TName) | |
381 | % TODO: also check duplicate_id_hides info fields ? | |
382 | ). | |
383 | ||
384 | % detect some identifiers that were removed | |
385 | removed_identifier(b(_,_,Infos),TId) :- | |
386 | member(was(WAS),Infos), | |
387 | introduced_ids(WAS,IDs), | |
388 | % this happens in EnumSetClash2.mch | |
389 | member(TId,IDs). | |
390 | ||
391 | introduced_ids(forall(IDs,_,_),IDs). | |
392 | introduced_ids(exists(IDs,_),IDs). % % are there more relevant cases? TODO: use syntaxtraversion | |
393 | ||
394 | % ignore certain constructs, which do not really introduce a new identifier: | |
395 | ignore_constructor(b(recursive_let(_,_),_,_)). | |
396 | ||
397 | ||
398 | get_typed_section(Kind,Name,SubPred) :- | |
399 | b_get_properties_from_machine(P), get_specification_description(properties,PS), | |
400 | get_sub_predicate(PS,P,Kind,Name,SubPred). | |
401 | get_typed_section(Kind,Name,SubPred) :- | |
402 | b_get_invariant_from_machine(P), get_specification_description(invariants,PS), | |
403 | get_sub_predicate(PS,P,Kind,Name,SubPred). | |
404 | get_typed_section(Kind,Name,SubPred) :- | |
405 | get_specification_description(assertions,APS), ajoin(['(dynamic) ',APS],AS), | |
406 | b_get_dynamic_assertions_from_machine(Ps), | |
407 | l_get_sub_predicate(AS,Ps,Kind,Name,SubPred). | |
408 | get_typed_section(Kind,Name,SubPred) :- | |
409 | get_specification_description(assertions,APS), ajoin(['(static) ',APS],AS), | |
410 | b_get_static_assertions_from_machine(Ps), | |
411 | l_get_sub_predicate(AS,Ps,Kind,Name,SubPred). | |
412 | get_typed_section(operation,OpName,P) :- b_get_machine_operation(OpName,_Results,_Parameters,P). | |
413 | % TO DO: add more sections: constraints, DEFINITION bodies | |
414 | ||
415 | ||
416 | :- use_module(bsyntaxtree, [conjunction_to_list/2, get_texpr_label/2]). | |
417 | get_sub_predicate(Clause,Pred,Kind,Name,SubPred) :- | |
418 | conjunction_to_list(Pred,Preds), | |
419 | l_get_sub_predicate(Clause,Preds,Kind,Name,SubPred). | |
420 | l_get_sub_predicate(Clause,Preds,Kind,Name,SubPred) :- | |
421 | member(SubPred,Preds), | |
422 | (get_texpr_label(SubPred,Label) | |
423 | -> Kind = predicate, ajoin([Label,'" in clause "',Clause],Name) | |
424 | ; Kind = clause, Name=Clause). | |
425 | ||
426 | ||
427 | % ------------------------- | |
428 | ||
429 | % check for reading uninitialised variables | |
430 | ||
431 | :- use_module(bmachine, [b_top_level_operation/1, b_top_level_feasible_operation/1]). | |
432 | check_operation_body(Body,OpID) :- b_top_level_operation(OpID), | |
433 | \+ b_top_level_feasible_operation(OpID), | |
434 | add_warning(bmachine_static_checks,'Infeasible body for operation:',OpID,Body), | |
435 | fail. | |
436 | check_operation_body(Body,OpID) :- | |
437 | (map_over_typed_bexpr(bmachine_static_checks:check_operation_body_var(OpID),Body),fail ; true). | |
438 | ||
439 | check_operation_body_var(OpID,b(var(Parameters,Body),subst,_Pos)) :- | |
440 | get_texpr_ids(Parameters,Ps), sort(Ps,Uninitialised), | |
441 | get_accessed_vars(Body,[],_Modifies,Reads), | |
442 | ord_intersection(Uninitialised,Reads,URead), | |
443 | URead \= [], | |
444 | member(TID,Parameters), get_texpr_id(TID,ID), | |
445 | member(ID,URead), | |
446 | ajoin(['Possibly reading uninitialised variable in operation ',OpID,' : '],Msg), | |
447 | add_warning(bmachine_static_checks,Msg,ID,TID). | |
448 | % TO DO: we could pinpoint more precisely where the read occurs | |
449 | ||
450 | % --------------------------- | |
451 | ||
452 | % perform some checks on symbolic values; look for obvious WD errors | |
453 | ||
454 | :- use_module(probsrc(bsyntaxtree),[map_over_typed_bexpr/2]). | |
455 | :- use_module(probsrc(state_space),[is_concrete_constants_state_id/1, visited_expression/2]). | |
456 | :- use_module(probsrc(specfile),[state_corresponds_to_set_up_constants/2]). | |
457 | ||
458 | check_concrete_constants :- is_concrete_constants_state_id(ID),!, | |
459 | check_values_in_state(ID). | |
460 | check_concrete_constants. | |
461 | ||
462 | check_values_in_state(ID) :- debug_format(19,'Checking values in state with id = ~w~n',[ID]), | |
463 | visited_expression(ID,State), | |
464 | state_corresponds_to_set_up_constants(State,EState), | |
465 | member(bind(VarID,Value),EState), | |
466 | check_symbolic_values(Value,VarID), | |
467 | fail. | |
468 | check_values_in_state(_). | |
469 | ||
470 | :- use_module(debug,[debug_println/2, debug_format/3]). | |
471 | :- use_module(error_manager,[add_error/3]). | |
472 | ||
473 | check_symbolic_values(Var,Ctxt) :- var(Var),!, | |
474 | add_error(bmachine_static_checks,'Value is a variable',Ctxt). | |
475 | check_symbolic_values(closure(_,_,Body),Ctxt) :- !, | |
476 | debug_format(19,'Checking symbolic value for ~w~n',[Ctxt]), | |
477 | map_over_typed_bexpr(check_symbolic_value(Ctxt),Body). | |
478 | check_symbolic_values(_,_). | |
479 | ||
480 | check_symbolic_value(Ctxt,b(E,T,I)) :- check_aux(E,T,I,Ctxt). | |
481 | ||
482 | check_aux(function(b(Func,_,_I1),_Arg),_,I2,Ctxt) :- % _I1 sometimes unknown | |
483 | % TO DO: check if Info contains WD flag | |
484 | check_is_partial_function(Func,I2,Ctxt). | |
485 | % TO DO: check sequence operators, ... | |
486 | ||
487 | :- use_module(custom_explicit_sets,[is_not_avl_partial_function/2]). | |
488 | :- use_module(library(avl),[avl_size/2]). | |
489 | :- use_module(probsrc(translate), [translate_bvalue_with_limit/3]). | |
490 | check_is_partial_function(value(Val),Info,Ctxt) :- nonvar(Val), Val=avl_set(AVL), | |
491 | is_not_avl_partial_function(AVL,DuplicateKey),!, | |
492 | avl_size(AVL,Size), | |
493 | translate_bvalue_with_limit(DuplicateKey,80,DKS), | |
494 | ajoin(['Relation of size ', Size, ' is not a function (value for ',Ctxt, '); duplicate key: '],Msg), | |
495 | add_warning(bmachine_static_checks,Msg,DKS,Info). | |
496 | check_is_partial_function(_,_,_). | |
497 | ||
498 | % --------------------- | |
499 | % Checks if some identifiers are not used / are useless | |
500 | % --------------------- | |
501 | ||
502 | :- use_module(bmachine,[b_is_unused_constant/1, get_constant_span/2]). | |
503 | check_unused_ids :- | |
504 | b_is_unused_constant(ID), | |
505 | get_constant_span(ID,Span), | |
506 | % TO DO: check if the constant is used to define other used constants | |
507 | (get_preference(filter_unused_constants,true) | |
508 | -> add_message(bmachine_static_checks,'This constant is not used outside of the PROPERTIES/axioms (and is filtered away because FILTER_UNUSED preference is TRUE): ',ID,Span) | |
509 | ; add_message(bmachine_static_checks,'This constant is not used outside of the PROPERTIES/axioms: ',ID,Span) | |
510 | ), | |
511 | fail. | |
512 | check_unused_ids. |