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