1		% (c) 2013-2024 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,
6		extended_static_check_machine/0, extended_static_check_machine/1,
7		find_constant_expressions_in_operations/1, find_constant_expressions_in_operations/2,
8		toplevel_raw_predicate_sanity_check/4]).
9
10		:- use_module(probsrc(module_information)).
11		:- module_info(group,typechecker).
12		:- module_info(description,'Static checking of B machines upon construction. Detection of name clashes and uninitalised variables.').
13
14		:- use_module(bmachine_structure, [get_section/3]).
15		:- use_module(b_read_write_info, [get_accessed_vars/4]).
16		:- use_module(bsyntaxtree, [get_texpr_expr/2,get_texpr_id/2,get_texpr_ids/2, get_texpr_info/2]).
17		:- use_module(error_manager, [add_warning/3, add_warning/4, add_error/4, add_message/4]).
18		:- use_module(debug, [debug_println/2]).
19		:- use_module(tools, [ajoin/2]).
20		:- use_module(library(lists)).
21
22		static_check_main_machine(Machine) :-
23		debug_println(19,'Running static machine checks'),
24		initialises_all_variables(Machine),
25		check_name_clashes(Machine).
26
27
28		% ---------------------------------------------
29		% check for unnatural invariants and properties
30		% ---------------------------------------------
31		% the priority of the implication is sometimes surprising
32		% a & (x=1) => (y=2) & c --> top-level symbol is the implication !
33		% the test is done on the raw predicate before ast_cleanup removes potential typing predicates; see tests 106, 107
34		toplevel_raw_predicate_sanity_check(invariant,MachName,RawPredicate,Infos) :-
35		member(has_variables,Infos), % otherwise it is ok to have just a single disjunt, implication,...
36		check_top_level(RawPredicate,MachName,'INVARIANT'),
37		fail.
38		toplevel_raw_predicate_sanity_check(properties,MachName,RawPredicate,Infos) :-
39		member(has_constants,Infos), % otherwise it is ok to have just a single disjunt, implication,...
40		check_top_level(RawPredicate,MachName,'PROPERTIES'),
41		fail.
42		toplevel_raw_predicate_sanity_check(_,_,_,_).
43
44		% typical error: forget parentheses; if we write P => Q & R --> this is parsed as P => (Q & R)
45		check_top_level(implication(_,B,C),MachName,SECT) :-
46		(composed_predicate(B) ; composed_predicate(C)),!,
47		add_warning(bmachine_static_checks,'Top-level implication (=>) in clause: ',MachName:SECT).
48		check_top_level(disjunct(_,B,C),MachName,SECT) :-
49		(composed_predicate(B) ; composed_predicate(C)),!,
50		add_warning(bmachine_static_checks,'Top-level disjunction (or) in clause: ',MachName:SECT).
51		check_top_level(equivalence(_,B,C),MachName,SECT) :-
52		(composed_predicate(B) ; composed_predicate(C)),!,
53		add_warning(bmachine_static_checks,'Top-level equivalence (<=>) in clause: ',MachName:SECT).
54
55		% check if a predicate is composed of a binary operator where confusion may arise
56		% with negation and quantification there are explicit parentheses; the user should not be confused
57		composed_predicate(A) :- functor(A,Operator,N),
58		boolean_operator(Operator),
59		% Some binary operators (conjunct, disjunct) can have a varying number of arguments.
60		% See predicates associative_functor/1 and unflatten_assoc/4 in btypechecker.
61		N >= 2.
62		boolean_operator(conjunct).
63		boolean_operator(disjunct).
64		boolean_operator(implication).
65		boolean_operator(equivalence).
66
67		% ---------------------
68		% Checks is all variables are initialised by the machine
69		% ---------------------
70		initialises_all_variables(Machine) :-
71		get_section(initialisation,Machine,Initialisation),
72		% check wich variables are read / modified by the initialisation
73		get_accessed_vars(Initialisation,[],Modifies,_Reads),
74		get_machine_variables(Machine,SortedAllVars),
75		% check for each variable, if the initialisation modifies it
76		exclude(is_initialised(Modifies),SortedAllVars,Uninitialised),
77		% generate a warning if unitialised is not empty
78		generate_uninitialised_warning(Uninitialised,Initialisation),
79		% now check order of initialisation sequences
80		check_initialisation_order(Initialisation,SortedAllVars,[],_).
81
82		get_machine_variables(Machine,SortedAllVars) :-
83		% get all variables that should be initialised
84		get_section(abstract_variables,Machine,AbsVars),
85		get_section(concrete_variables,Machine,ConcVars),
86		append(AbsVars,ConcVars,TAllVars),
87		get_texpr_ids(TAllVars,AllVars),
88		sort(AllVars,SortedAllVars).
89
90		is_initialised(Modifies,Id) :-
91		memberchk(Id,Modifies).
92
93		generate_uninitialised_warning([],_) :- !.
94		generate_uninitialised_warning(Vars,Initialisation) :-
95		Msg='Machine may not initialise some of its variables: ',
96		add_warning(bmachine_static_checks,Msg,Vars,Initialisation).
97
98
99		:- use_module(library(ordsets)).
100		% Check if order of sequential compositions in INITIALISATION is ok
101		% TO DO: add support for if(LIST) and while
102		check_initialisation_order(b(Subst,subst,Info),AllVars,AlreadyInit,OutInit) :-
103		check_initialisation_order2(Subst,Info,AllVars,AlreadyInit,OutInit),!.
104		check_initialisation_order(Subst,AllVars,AlreadyInit,OutInit) :-
105		% print('CHCK '), translate:print_subst(Subst),nl,
106		get_accessed_vars(Subst,[],Modifies,Reads),
107		check_subst_or_pred(Subst,Modifies,Reads,AllVars,AlreadyInit,OutInit).
108
109		check_subst_or_pred(Subst,Modifies,Reads,AllVars,AlreadyInit,OutInit) :-
110		ord_union(Modifies,AlreadyInit,OutInit), % after Subst we have initialised OutInit
111		% below is already checked by type checker:
112		%ord_subtract(Modifies,AllVars,IllegalAssignments),
113		%(IllegalAssignments=[] -> true
114		% ; add_warning(bmachine_static_checks,'INITIALISATION writes illegal variables: ',IllegalAssignments,Subst)),
115		ord_intersection(Reads,AllVars,ReadFromSameMachine),
116		(atomic_subst(Subst)
117		-> ord_subtract(ReadFromSameMachine,AlreadyInit,IllegalReads)
118		; ord_subtract(ReadFromSameMachine,OutInit,IllegalReads) % we use OutInit: there could be an if with sequence inside
119		),
120		(IllegalReads=[] -> true
121		; add_warning(bmachine_static_checks,'INITIALISATION reads variables which are not yet initialised: ',IllegalReads,Subst)).
122
123		:- use_module(bsyntaxtree,[find_identifier_uses/3]).
124		check_initialisation_order2(choice([First|T]),Info,AllVars,AlreadyInit,OutInit) :- !,
125		check_initialisation_order(First,AllVars,AlreadyInit,OutInit), % we pick the output of the first choice
126		(T=[] -> true ; check_initialisation_order(b(choice(T),subst,Info),AllVars,AlreadyInit,_)).
127		check_initialisation_order2(parallel([First|T]),Info,AllVars,AlreadyInit,OutInit) :- !,
128		check_initialisation_order(First,AllVars,AlreadyInit,OutInit1), % we pick the output of the first choice
129		(T=[] -> OutInit=OutInit1
130		; check_initialisation_order2(parallel(T),Info,AllVars,AlreadyInit,OutInitRest),
131		ord_union(OutInit1,OutInitRest,OutInit)
132		).
133		check_initialisation_order2(init_parallel(S),Info,AllVars,AlreadyInit,OutInit) :- !,
134		check_initialisation_order(b(parallel(S),subst,Info),AllVars,AlreadyInit,OutInit).
135		check_initialisation_order2(sequence([First|T]),Info,AllVars) --> !,
136		check_initialisation_order(First,AllVars),
137		({T=[]} -> [] ; check_initialisation_order(b(sequence(T),subst,Info),AllVars)).
138		check_initialisation_order2(any(_Ids,Pred,Subst),_Info,AllVars,AlreadyInit,OutInit) :- !,
139		find_identifier_uses(Pred,[],Reads),
140		check_subst_or_pred(Pred,[],Reads,AllVars,AlreadyInit,_), % check predicate reads are ok
141		check_initialisation_order(Subst,AllVars,AlreadyInit,OutInit).
142		% TO DO: also check if-then-else, while, ...
143
144		atomic_subst(b(S,_,_)) :- atomic_subst2(S).
145		atomic_subst2(skip).
146		atomic_subst2(assign(_,_)).
147		atomic_subst2(assign_single_id(_,_)).
148		atomic_subst2(becomes_element_of(_,_)).
149		%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)
150
151		% ---------------------
152		% Checks if an operations parameter or local variable clashes with a variable
153		% ---------------------
154		check_name_clashes(Machine) :-
155		debug_println(10,'Checking for name clashes'),
156		get_all_machine_ids(Machine,SortedAllIds),
157		% for each operation, compare the parameter names with existing vars/constants
158		get_section(operation_bodies,Machine,Operations),
159		maplist(op_name_clashes(SortedAllIds),Operations),
160		get_section(definitions,Machine,Defs),
161		maplist(def_name_clashes(SortedAllIds),Defs).
162
163		get_all_machine_ids(Machine,SortedAllIds) :-
164		% get all variables and constants that might clash
165		get_section_ids(abstract_variables,Machine,'variable',AbsVars),
166		get_section_ids(concrete_variables,Machine,'variable',ConcVars),
167		get_section_ids(abstract_constants,Machine,'constant',AbsCons),
168		get_section_ids(concrete_constants,Machine,'constant',ConcCons),
169		get_section_ids(deferred_sets,Machine,'set',DefSets),
170		get_section_ids(enumerated_sets,Machine,'set',EnumSets),
171		get_section_ids(enumerated_elements,Machine,'set element',EnumElems),
172		% enumerated b_get_named_machine_set(GlobalSetName,ListOfConstants) + b_get_machine_set(S)
173		append([AbsVars,ConcVars,AbsCons,ConcCons,DefSets,EnumSets,EnumElems],AllIds),
174		keyword_clash(AllIds),
175		sort(AllIds,SortedAllIds).
176
177		get_section_ids(Section,Machine,Class,ResultList) :-
178		get_section(Section,Machine,Vars),
179		findall(machine_id(ID,Class,Pos,Section),
180		(member(TID,Vars),get_texpr_id(TID,ID),get_texpr_info(TID,Pos)),ResultList).
181
182
183		:- use_module(tools_matching,[is_b_keyword/2]).
184
185		% can be useful for Z, TLA+, Event-B machines:
186		% Clashes may lead to strange type or parse errors in VisB, REPL, ...
187		keyword_clash(AllIds) :-
188	?	member(machine_id(Name,Class,Pos,Section),AllIds),
189		is_b_keyword(Name,_),
190		get_descr(Pos,Section,Descr),
191		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),
192		(classical_b_mode
193		-> add_message(bmachine_static_checks,Msg,'',Pos) % user probably uses new backquote syntax already
194		; add_warning(bmachine_static_checks,Msg,'',Pos)
195		),
196		fail.
197		keyword_clash(_).
198
199		:- use_module(bsyntaxtree,[map_over_typed_bexpr/2]).
200		:- use_module(external_functions,[is_external_function_name/1]).
201
202		def_name_clashes(AllIds,definition_decl(Name,DefType,_DefPos,Args,_RawExpr,_Deps)) :- !,
203		(is_external_function_name(Name)
204		-> true % do not check external predicates, functions, subst
205		% they are not written by user and possibly not used and definitions are virtual and not used anyway
206		; findall(b(identifier(ID),any,[nodeid(IdPos)]),
207		member(identifier(IdPos,ID),Args),ArgIds), % args can sometimes not be identifiers; see test 1711
208		debug_println(4,checking_def(Name,DefType,Args,ArgIds)),
209		include(clash_warnings('DEFINITION parameter',AllIds,'DEFINITION',Name),ArgIds,_ArgsCausingWarning)
210		% TO DO: check Body; for this we need a map_over_raw_expression to detect local variables introduced !
211		).
212		def_name_clashes(_,D) :- print(unknown_def(D)),nl.
213
214		:- use_module(preferences,[get_preference/2]).
215		op_name_clashes(AllIds,Operation) :-
216		get_texpr_expr(Operation,operation(IdFull,Results,Params,Subst)),
217		%get_texpr_id(IdFull,op(Id)),
218		IdFull = b(identifier(op(Id)),Type,Info),
219		(get_preference(clash_strict_checks,true)
220		-> include(clash_warnings('Operation name',AllIds,operation,Id),[b(identifier(Id),Type,Info)],_NameCausingWarning) % fix PROB-60
221		; true),
222		include(clash_warnings('Operation parameter',AllIds,operation,Id),Params,_ParamsCausingWarning),
223		include(clash_warnings('Operation result variable',AllIds,operation,Id),Results,_ResultsCausingWarning),
224		(map_over_typed_bexpr(bmachine_static_checks:check_operation_body_clashes(AllIds,Id),Subst),fail ; true).
225
226		:- public check_operation_body_clashes/3.
227		check_operation_body_clashes(AllIds,Operation,TSubst) :-
228		get_texpr_expr(TSubst,Subst),
229		(local_variable_clash(Subst,TSubst,AllIds,Operation);
230		illegal_op_call(Subst,Operation)).
231
232		local_variable_clash(Subst,TSubst,AllIds,Operation) :-
233		introduces_local_variable(Subst,ID),
234		clash_local_warnings(AllIds,Operation,ID,TSubst).
235
236		% check if something like zz(1) <-- Op(a) is used; this is not allowed according to Atelier-B
237		illegal_op_call(operation_call(CalledOperation,Results,_Parameters),Operation) :-
238		member(TID,Results), \+ get_texpr_id(TID,_),
239		(get_texpr_id(CalledOperation,op(CalledId)) -> true ; CalledId=CalledOperation),
240		ajoin(['Return value of operation call to ',CalledId,' must be stored in identifier within:'],Msg),
241		add_error(bmachine_static_checks,Msg,Operation,TID).
242
243		% check for constructs which introduced local variables
244		introduces_local_variable(var(Parameters,_),ID) :-
245		% currently B-interpreter cannot correctly deal with this in the context of operation_call
246		member(TID,Parameters), get_texpr_id(TID,ID).
247
248		:- use_module(probsrc(error_manager),[extract_span_description/2]).
249		% ord_member does not work below because of free variable Class
250		my_ord_member(Name,Class,Descr,[machine_id(Name1,_,_,_)|T]) :-
251		Name @> Name1, !,
252		my_ord_member(Name,Class,Descr,T).
253		my_ord_member(Name,Class,Descr,[machine_id(Name,Class,Pos,Section)|_]) :-
254		get_descr(Pos,Section,Descr).
255
256		get_descr(Pos,Section,Descr) :-
257		(extract_span_description(Pos,Descr) -> true
258		; ajoin(['from section ',Section],Descr) ).
259
260		clash_warnings(Context,AllIds,OpOrDef,OperationId,TName) :-
261		get_texpr_id(TName,Name),
262		my_ord_member(Name,Class,Descr,AllIds), !,
263		ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a ',
264		Context, ' in ',OpOrDef,' "', OperationId,'".'], Msg),
265		add_warning(bmachine_static_checks,Msg,'',TName).
266
267		clash_local_warnings(AllIds,OperationId,Name,Pos) :-
268		my_ord_member(Name,Class,Descr,AllIds), !,
269		% we could check and see if Name is really visible from this location!
270		% (see public_examples/B/Other/LustreTranslations/UMS_verif/M_UMS_verif.mch)
271		ajoin(['The ', Class, ' "', Name, '" (', Descr,') has the same name as a local variable in operation "', OperationId,'".'], Msg),
272		add_warning(bmachine_static_checks,Msg,'',Pos).
273
274		% TODO: this does not and can not work here:
275		% - Some preconditions are removed (typing only....) during machine simplification
276		% - Needs to be verified during typechecking
277		% ---------------------
278		% Checks if an operations parameter is not typed by a pre condition
279		% ---------------------
280		%parameters_without_pre_condition(Machine) :-
281		% get_section(operation_bodies,Machine,Operations),
282		% maplist(parameters_without_pre_condition_aux,Operations).
283		%
284		%parameters_without_pre_condition_aux(Operation) :-trace,
285		% get_texpr_expr(Operation,operation(IdFull,_Results,Params,Subst)),
286		% get_texpr_id(IdFull,op(Id)),
287		% (Params == []
288		% -> true % no parameters
289		% ; (get_texpr_expr(Subst,precondition(_,_))
290		% -> true % parameters and precondition
291		% ; ajoin(['Operation ', Id, ' has parameters but no pre-condition.'], Msg),
292		% add_warning(bmachine_static_checks,Msg)
293		% )).
294
295
296		% EXTENDED ADDITIONAL CHECKS
297		% these are run (optionally) after machine is loaded and bmachine pre-calculations have run
298
299		:- use_module(b_read_write_info,[check_all_variables_written/0]).
300
301		extended_static_check_machine :-
302		extended_static_check_machine(_).
303		extended_static_check_machine(Check) :-
304		reset_static_check,
305		esc_step(Check).
306
307		:- use_module(probsrc(bmachine), [b_get_main_filename/1, b_machine_name/1, b_get_machine_header_position/2]).
308		:- use_module(tools,[get_modulename_filename/2, get_filename_extension/2]).
309		:- use_module(bsyntaxtree,[map_over_typed_bexpr_with_names/2]).
310		:- use_module(specfile,[get_specification_description/2, animation_minor_mode/1, classical_b_mode/0]).
311		:- use_module(bmachine).
312		:- use_module(b_machine_hierarchy,[machine_type/2, machine_operations/2]).
313
314		esc_step(variables) :-
315		check_all_variables_written,
316		fail.
317		esc_step(machine_name) :-
318		b_machine_name(Name),
319		b_get_main_filename(Filename),
320		get_modulename_filename(Filename,ModuleName),
321		Name \= ModuleName,
322		(atom_concat('MAIN_MACHINE_FOR_',RealName,Name) % see dummy_machine_name in bmachine_construction
323		-> RealName \= ModuleName
324		; is_dummy_machine_name(Name,Filename)
325		-> fail % dummy Rules DSL or Alloy machine name, do not create warning
326		; true
327		),
328		(b_get_machine_header_position(Name,Span) -> true
329		; Span = src_position_with_filename(1,1,1,Filename)),
330		get_specification_description(machine,MCH),
331		ajoin(['Filename ',ModuleName,' does not match name of ', MCH, ': '],Msg),
332		add_warning(bmachine_static_checks,Msg,Name,Span),
333		fail.
334		esc_step(variables) :- debug_println(19,checking_identifiers_for_clashes),
335		full_b_machine(Machine),
336		local_quantified_variable_clashes(Machine),
337		fail.
338		esc_step(operations) :- machine_type(MachName,abstract_machine),
339		machine_operations(MachName,Ops),
340		member(identifier(Span,OpName),Ops),
341		atom_codes(OpName,Codes), member(46,Codes), % "." element of name
342		% Section 7.23, paragraph 2 of Atelier-B handbook: in abstract machine we cannot use renamed operation names
343		ajoin(['Operation name in abstract machine ',MachName,' is composed: '],Msg),
344		add_warning(bmachine_static_checks,Msg,OpName,Span),
345		fail.
346		esc_step(operations) :- debug_println(19,checking_operation_bodies),
347		b_get_machine_operation(ID,_Res,_TParas,Body,_OType,_Pos),
348		check_operation_body(Body,ID),
349		fail.
350		esc_step(operations) :- portray_constant_expr_summary, fail.
351		esc_step(constants) :-
352		check_concrete_constants, % check concrete_constants(.) states
353		fail.
354		esc_step(unused_ids) :-
355		check_unused_ids,
356		fail.
357		esc_step(_).
358
359		:- use_module(probsrc(tools_strings), [atom_prefix/2]).
360		is_dummy_machine_name(Name,_) :- atom_prefix('__RULES_MACHINE_Main',Name).
361		is_dummy_machine_name(alloytranslation,_) :- animation_minor_mode(alloy).
362		is_dummy_machine_name('DEFINITION_FILE',Filename) :- classical_b_mode,
363		get_filename_extension(Filename,'def').
364		% when opening .def files; WARNING: sometimes def files use other extensions
365
366		% TO DO: optionally do these kinds of checks in the REPL
367		local_quantified_variable_clashes(Machine) :-
368		get_all_machine_ids(Machine,SortedAllIds),
369		(get_typed_section(Sec,SecID,Pred),
370		debug_println(19,checking_local_quantified_variable_clashes(Sec,SecID)),
371		map_over_typed_bexpr_with_names(bmachine_static_checks:check_introduced_ids(Sec,SecID,SortedAllIds),Pred)
372		;
373		check_definition_clashes(SortedAllIds)
374		),
375		fail.
376		local_quantified_variable_clashes(_).
377
378		:- use_module(bmachine,[b_get_typed_definition/3]).
379		check_definition_clashes(SortedAllIds) :-
380		Scope=[variables],
381		b_get_typed_definition(Name,Scope,TExpr),
382		% TODO: adapt type_check_definitions to return definitions with paras and add paras to list of Ids
383		%print(check(Name,SortedAllIds)),nl,
384		map_over_typed_bexpr_with_names(bmachine_static_checks:check_introduced_ids('DEFINITION',Name,SortedAllIds),TExpr).
385
386		:- public check_introduced_ids/5. % used in map above
387		check_introduced_ids(Section,SectionID,SortedAllIds,TExpr,TNames) :-
388		\+ ignore_constructor(TExpr),
389		(member(TName,TNames),
390		clash_warnings('local variable',SortedAllIds,Section,SectionID,TName)
391		; removed_identifier(TExpr,TName),
392		clash_warnings('(removed) local variable',SortedAllIds,Section,SectionID,TName)
393		% TODO: also check duplicate_id_hides info fields ?
394		).
395
396		% detect some identifiers that were removed
397		removed_identifier(b(_,_,Infos),TId) :-
398		member(was(WAS),Infos),
399		introduced_ids(WAS,IDs),
400		% this happens in EnumSetClash2.mch
401		member(TId,IDs).
402
403		introduced_ids(forall(IDs,_,_),IDs).
404		introduced_ids(exists(IDs,_),IDs). % % are there more relevant cases? TODO: use syntaxtraversion
405
406		% ignore certain constructs, which do not really introduce a new identifier:
407		ignore_constructor(b(recursive_let(_,_),_,_)).
408
409
410		get_typed_section(Kind,Name,SubPred) :-
411		b_get_properties_from_machine(P), get_specification_description(properties,PS),
412		get_sub_predicate(PS,P,Kind,Name,SubPred).
413		get_typed_section(Kind,Name,SubPred) :-
414		b_get_invariant_from_machine(P), get_specification_description(invariants,PS),
415		get_sub_predicate(PS,P,Kind,Name,SubPred).
416		get_typed_section(Kind,Name,SubPred) :-
417		get_specification_description(assertions,APS), ajoin(['(dynamic) ',APS],AS),
418		b_get_dynamic_assertions_from_machine(Ps),
419		l_get_sub_predicate(AS,Ps,Kind,Name,SubPred).
420		get_typed_section(Kind,Name,SubPred) :-
421		get_specification_description(assertions,APS), ajoin(['(static) ',APS],AS),
422		b_get_static_assertions_from_machine(Ps),
423		l_get_sub_predicate(AS,Ps,Kind,Name,SubPred).
424		get_typed_section(operation,OpName,P) :- b_get_machine_operation(OpName,_Results,_Parameters,P).
425		% TO DO: add more sections: constraints, DEFINITION bodies
426
427
428		:- use_module(bsyntaxtree, [conjunction_to_list/2, get_texpr_label/2]).
429		get_sub_predicate(Clause,Pred,Kind,Name,SubPred) :-
430		conjunction_to_list(Pred,Preds),
431		l_get_sub_predicate(Clause,Preds,Kind,Name,SubPred).
432		l_get_sub_predicate(Clause,Preds,Kind,Name,SubPred) :-
433		member(SubPred,Preds),
434		(get_texpr_label(SubPred,Label)
435		-> Kind = predicate, ajoin([Label,'" in clause "',Clause],Name)
436		; Kind = clause, Name=Clause).
437
438
439		% -------------------------
440
441		% check for reading uninitialised variables
442
443		:- use_module(bmachine, [b_top_level_operation/1, b_top_level_feasible_operation/1, b_is_constant/1]).
444		check_operation_body(Body,OpID) :- b_top_level_operation(OpID),
445		\+ b_top_level_feasible_operation(OpID),
446		add_warning(bmachine_static_checks,'Infeasible body for operation:',OpID,Body),
447		fail.
448		check_operation_body(Body,OpID) :-
449		map_over_typed_bexpr(bmachine_static_checks:check_operation_body_var(OpID),Body),
450		fail.
451		check_operation_body(Body,OpID) :-
452		check_for_constant_expressions(Body,OpID,[],_,_).
453
454		check_operation_body_var(OpID,b(var(Parameters,Body),subst,_Pos)) :-
455		get_texpr_ids(Parameters,Ps), sort(Ps,Uninitialised),
456		get_accessed_vars(Body,[],_Modifies,Reads),
457		ord_intersection(Uninitialised,Reads,URead),
458		URead \= [],
459		member(TID,Parameters), get_texpr_id(TID,ID),
460		member(ID,URead),
461		ajoin(['Possibly reading uninitialised variable in operation ',OpID,' : '],Msg),
462		add_warning(bmachine_static_checks,Msg,ID,TID).
463		% TO DO: we could pinpoint more precisely where the read occurs
464
465		% locate potentially expensive fully constant expressions (depending only on B constants)
466		% which are in a dynamic context (operations) and which may be recomputed many times
467		% the b_compiler will quite often pre-compile those, but not always (e.g., for relational composition involving infinite functions or when we have WD conditions)
468		:- use_module(error_manager,[get_tk_table_position_info/2]).
469		:- use_module(translate,[translate_bexpression_with_limit/3]).
470		find_constant_expressions_in_operations(List) :-
471		find_constant_expressions_in_operations(create_messages,List).
472
473		find_constant_expressions_in_operations(MsgOrWarn,_) :-
474		reset_static_check,
475		assert(store_expr(MsgOrWarn)),
476		b_get_machine_operation(OpID,_Res,_TParas,Body,_OType,_Pos),
477		check_for_constant_expressions(Body,OpID,[],_,_),
478		fail.
479		find_constant_expressions_in_operations(_,list([Header|List])) :-
480		Header = ['Operation', 'Occurence', 'Expr', 'LocalIds', 'Source'],
481		portray_constant_expr_summary,
482		findall(list([OpID,Count,ES,LocalIds,Src]),
483		(const_expr(OpID,Count,BExpr,LocalIds),
484		translate_bexpression_with_limit(BExpr,100,ES),
485		get_tk_table_position_info(BExpr,Src)), List),
486		reset_static_check.
487
488		:- use_module(bsyntaxtree,[syntaxtraversion/6]).
489		check_for_constant_expressions(BExpr,OpID,LocalIds,IsConstant,IsExpensive) :-
490		syntaxtraversion(BExpr,Expr,Type,_Infos,Subs,TNames),
491		(get_texpr_ids(TNames,QuantifiedNewIds), list_to_ord_set(QuantifiedNewIds,SQuantifiedNewIds)
492		-> ord_union(LocalIds,SQuantifiedNewIds,NewLocalIds)
493		; write(err(TNames)),nl, NewLocalIds = LocalIds),
494		l_check_for_const(Subs,OpID,NewLocalIds,SQuantifiedNewIds,AreAllConstant,IsExpensive1,ExpensiveList),
495		%translate:print_bexpr_or_subst(BExpr),nl, write(cst(AreAllConstant,IsExpensive1,LocalIds)),nl,nl,
496		(AreAllConstant=is_constant,
497		is_constant_expression(Expr,LocalIds,IsExpensive2)
498		-> IsConstant = is_constant,
499		combine_expensive(IsExpensive1,IsExpensive2,IsExpensive),
500		(pred_or_subst(Type) % we may traverse the boundary of expressions to pred/subst: print expressions
501		-> maplist(add_const_expr_msg(OpID,LocalIds),ExpensiveList)
502		; true)
503		; IsConstant = not_constant, IsExpensive=not_expensive,
504		maplist(add_const_expr_msg(OpID,LocalIds),ExpensiveList)
505		).
506
507
508		:- use_module(probsrc(b_interpreter_check),[norm_check/2]).
509		:- use_module(probsrc(hashing),[my_term_hash/2]).
510		:- use_module(probsrc(tools), [ajoin_with_sep/3]).
511		add_const_expr_msg(OpID,LocalIds,BExpr) :-
512		(LocalIds=[] -> debug:debug_mode(on) ; true), % decide whether to show outer-level constant expressions
513		register_constant_expression(BExpr,OpID,LocalIds,Count,MsgOrWarn),
514		(LocalIds = [] -> LMsg=[': ']
515		; length(LocalIds,Len),
516		(Len =< 3
517		-> ajoin_with_sep(LocalIds,',',LIDS),
518		LMsg = [' inside quantification (',LIDS,'): ']
519		; prefix_length(LocalIds,Prefix,2),
520		last(LocalIds,LastId),
521		ajoin_with_sep(Prefix,',',LIDS),
522		LMsg = [' inside quantification (',Len,' ids: ',LIDS,',...,',LastId,'): ']
523		)
524		),
525		(Count > 1
526		-> ajoin(['Repeated constant expression in operation ',OpID,
527		' (occurence nr. ',Count,', consider lifting it out)'|LMsg],Msg)
528		; ajoin(['Non-trivial constant expression in operation ',OpID,' (consider lifting it out)'|LMsg],Msg)
529		),
530		(MsgOrWarn=create_messages
531		-> add_message(b_machine_static_checks,Msg,BExpr,BExpr)
532		; add_warning(b_machine_static_checks,Msg,BExpr,BExpr)).
533
534		:- dynamic store_expr/1, const_expr_hash_count/2, const_expr/4.
535		reset_static_check :- retractall(const_expr_hash_count(_,_)),
536		retractall(const_expr(_,_,_,_)), retractall(store_expr(_)).
537		register_constant_expression(BExpr,OpID,LocalIds,Count,MsgOrWarn) :-
538		norm_check(BExpr,Norm), my_term_hash(Norm,Hash),
539		(retract(const_expr_hash_count(Hash,C)) -> Count is C+1 ; Count=1),
540		assert(const_expr_hash_count(Hash,Count)),
541		(store_expr(MsgOrWarn) -> assert(const_expr(OpID,Count,BExpr,LocalIds)) ; MsgOrWarn=message).
542
543		portray_constant_expr_summary :-
544		findall(Count,const_expr_hash_count(_,Count),LC),
545		length(LC,Len),
546		format('Constant expressions found: ~w~n',[Len]),
547		sumlist(LC,Total),
548		format('Total # of occurrences: ~w~n',[Total]).
549
550
551		l_check_for_const([],_OpID,_,_,is_constant,not_expensive,[]).
552		l_check_for_const([H|T],OpID,LocalIds,NewQuantLocalIds,AreAllConstant,IsExpensive,ExpResList) :-
553		check_for_constant_expressions(H,OpID,LocalIds,IsConstant,IsExpensive0),
554		project_is_expensive(IsExpensive0,NewQuantLocalIds,IsExpensive1), % project on NewIds introduced at top-level
555		(IsConstant=is_constant
556		-> (IsExpensive1=is_expensive, is_expression(H) % currently we only look for constant expressions
557		-> ExpResList = [H|TR] % add to list for add_const_expr_msg
558		; ExpResList=TR),
559		l_check_for_const(T,OpID,LocalIds,NewQuantLocalIds,AreAllConstant,IsExpensive2,TR),
560		combine_expensive(IsExpensive1,IsExpensive2,IsExpensive)
561		; AreAllConstant=not_constant, IsExpensive=not_expensive,
562		l_check_for_const(T,OpID,LocalIds,NewQuantLocalIds,_,_,ExpResList)).
563
564		is_expression(b(_,T,_)) :- \+ pred_or_subst(T).
565
566		pred_or_subst(pred).
567		pred_or_subst(subst).
568
569		% operators on abstract expensive/local_id domain:
570		combine_expensive(not_expensive,IsExpensive2,IsExpensive) :- !, IsExpensive=IsExpensive2.
571		combine_expensive(is_expensive,depends_on_local_ids(Ids,_),Res) :- !,
572		Res=depends_on_local_ids(Ids,is_expensive).
573		combine_expensive(is_expensive,_,IsExpensive) :- !, IsExpensive=is_expensive.
574		combine_expensive(depends_on_local_ids(Ids1,IE1),depends_on_local_ids(Ids2,IE2),Res) :- !,
575		combine_expensive(IE1,IE2,IE),
576		ord_union(Ids1,Ids2,Ids), Res=depends_on_local_ids(Ids,IE).
577		combine_expensive(depends_on_local_ids(Ids,IE1),IE2,Res) :- !,
578		combine_expensive(IE1,IE2,IE),
579		Res=depends_on_local_ids(Ids,IE).
580		combine_expensive(A,B,C) :- write(combine_expensive_uncovered(A,B,C)),nl,nl,C=A.
581
582		% project is_expensive domain value after leaving SQuantifiedNewIds
583		project_is_expensive(depends_on_local_ids(LocalIds,IE),SQuantifiedNewIds,Res) :- !,
584		ord_subtract(LocalIds,SQuantifiedNewIds,NewLocalIds),
585		(NewLocalIds = [] -> Res = IE % is_expensive/not_expensive
586		; Res= depends_on_local_ids(NewLocalIds,IE)).
587		project_is_expensive(IE,_,IE).
588
589		:- use_module(probsrc(b_global_sets),[lookup_global_constant/2]).
590		% check if based on top-level the expression is constant, assuming all args are constant
591		is_constant_expression(identifier(ID),LocalIds,Kind) :- !,
592		(ord_member(ID,LocalIds) -> Kind = depends_on_local_ids([ID],not_expensive)
593		; b_is_constant(ID) -> Kind = not_expensive
594		; b_get_machine_set(ID) -> Kind = not_expensive
595		; lookup_global_constant(ID,_) -> Kind = not_expensive). % enumerated set element
596		is_constant_expression(Expr,_,IsExpensive) :- is_constant_expression(Expr,IsExpensive).
597
598		is_constant_expression(value(_),not_expensive).
599		% literals:
600		is_constant_expression(max_int,not_expensive).
601		is_constant_expression(min_int,not_expensive).
602		is_constant_expression(boolean_false,not_expensive).
603		is_constant_expression(boolean_true,not_expensive).
604		is_constant_expression(empty_set,not_expensive).
605		is_constant_expression(empty_sequence,not_expensive).
606		is_constant_expression(integer(_),not_expensive).
607		is_constant_expression(real(_),not_expensive).
608		is_constant_expression(string(_),not_expensive).
609
610		is_constant_expression(bool_set,not_expensive).
611		is_constant_expression(freetype_set(_),not_expensive).
612		is_constant_expression(real_set,not_expensive).
613		is_constant_expression(string_set,not_expensive).
614		is_constant_expression(typeset,not_expensive).
615		is_constant_expression(integer_set(_),not_expensive).
616		% simple arithmetic:
617		is_constant_expression(unary_minus(_),not_expensive).
618		is_constant_expression(add(_,_),not_expensive).
619		is_constant_expression(minus(_,_),not_expensive).
620		is_constant_expression(multiplication(_,_),not_expensive).
621		% just constructing values:
622		is_constant_expression(couple(_,_),not_expensive).
623		is_constant_expression(record_field(_,_),not_expensive).
624		is_constant_expression(rec(_),not_expensive).
625		is_constant_expression(set_extension(_),not_expensive).
626		is_constant_expression(sequence_extension(_),not_expensive).
627		is_constant_expression(interval(_,_),not_expensive).
628		% simple deconstructing
629		is_constant_expression(first_of_pair(_),not_expensive).
630		is_constant_expression(second_of_pair(_),not_expensive).
631		is_constant_expression(record_field(_,_),not_expensive).
632		% just typing
633		% TODO: return typing instead of not_expensive as result and check context used later
634		is_constant_expression(pow_subset(_),not_expensive).
635		is_constant_expression(fin_subset(_),not_expensive).
636		is_constant_expression(pow1_subset(_),not_expensive).
637		is_constant_expression(fin1_subset(_),not_expensive).
638		is_constant_expression(seq(_),not_expensive).
639		is_constant_expression(seq1(_),not_expensive).
640		is_constant_expression(iseq(_),not_expensive).
641		is_constant_expression(iseq1(_),not_expensive).
642		is_constant_expression(cartesian_product(_,_),not_expensive).
643		is_constant_expression(mult_or_cart(_,_),not_expensive).
644		is_constant_expression(relations(_,_),not_expensive).
645		is_constant_expression(relations(_,_),not_expensive).
646		is_constant_expression(struct(_),not_expensive).
647		% TO DO: card : trivial if avl_set; maybe we should do this after constants_analysis
648		% TODO: detect some external function calls as not constant: RANDOM, ...
649
650		%is_constant_expression(domain(_),not_expensive). % is not expensive for symbolic lambas, and reasonable for avl_set
651		is_constant_expression(composition(_,_),is_expensive).
652		is_constant_expression(image(_,_),is_expensive).
653		is_constant_expression(iteration(_,_),is_expensive).
654		is_constant_expression(concat(_,_),is_expensive).
655		is_constant_expression(reflexive_closure(_),is_expensive).
656		is_constant_expression(closure(_),is_expensive).
657		is_constant_expression(union(_,_),is_expensive).
658		is_constant_expression(intersection(_,_),is_expensive).
659
660		is_constant_expression(_,is_expensive).
661
662		% ---------------------------
663
664		% perform some checks on symbolic values; look for obvious WD errors
665
666		:- use_module(probsrc(bsyntaxtree),[map_over_typed_bexpr/2]).
667		:- use_module(probsrc(state_space),[is_concrete_constants_state_id/1, visited_expression/2]).
668		:- use_module(probsrc(specfile),[state_corresponds_to_set_up_constants/2]).
669
670		check_concrete_constants :- is_concrete_constants_state_id(ID),!,
671		check_values_in_state(ID).
672		check_concrete_constants.
673
674		check_values_in_state(ID) :- debug_format(19,'Checking values in state with id = ~w~n',[ID]),
675		visited_expression(ID,State),
676		state_corresponds_to_set_up_constants(State,EState),
677		member(bind(VarID,Value),EState),
678		check_symbolic_values(Value,VarID),
679		fail.
680		check_values_in_state(_).
681
682		:- use_module(debug,[debug_println/2, debug_format/3]).
683		:- use_module(error_manager,[add_error/3]).
684
685		check_symbolic_values(Var,Ctxt) :- var(Var),!,
686		add_error(bmachine_static_checks,'Value is a variable',Ctxt).
687		check_symbolic_values(closure(_,_,Body),Ctxt) :- !,
688		debug_format(19,'Checking symbolic value for ~w~n',[Ctxt]),
689		map_over_typed_bexpr(check_symbolic_value(Ctxt),Body).
690		check_symbolic_values(_,_).
691
692		check_symbolic_value(Ctxt,b(E,T,I)) :- check_aux(E,T,I,Ctxt).
693
694		check_aux(function(b(Func,_,_I1),_Arg),_,I2,Ctxt) :- % _I1 sometimes unknown
695		% TO DO: check if Info contains WD flag
696		check_is_partial_function(Func,I2,Ctxt).
697		% TO DO: check sequence operators, ...
698
699		:- use_module(custom_explicit_sets,[is_not_avl_partial_function/2]).
700		:- use_module(library(avl),[avl_size/2]).
701		:- use_module(probsrc(translate), [translate_bvalue_with_limit/3]).
702		check_is_partial_function(value(Val),Info,Ctxt) :- nonvar(Val), Val=avl_set(AVL),
703		is_not_avl_partial_function(AVL,DuplicateKey),!,
704		avl_size(AVL,Size),
705		translate_bvalue_with_limit(DuplicateKey,80,DKS),
706		ajoin(['Relation of size ', Size, ' is not a function (value for ',Ctxt, '); duplicate key: '],Msg),
707		add_warning(bmachine_static_checks,Msg,DKS,Info).
708		check_is_partial_function(_,_,_).
709
710		% ---------------------
711		% Checks if some identifiers are not used / are useless
712		% ---------------------
713
714		:- use_module(bmachine,[b_is_unused_constant/1, get_constant_span/2]).
715		check_unused_ids :-
716		b_is_unused_constant(ID),
717		get_constant_span(ID,Span),
718		% TO DO: check if the constant is used to define other used constants
719		(get_preference(filter_unused_constants,true)
720		-> 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)
721		; add_message(bmachine_static_checks,'This constant is not used outside of the PROPERTIES/axioms: ',ID,Span)
722		),
723		fail.
724		check_unused_ids.