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