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