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