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