1		% (c) 2013-2019 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, toplevel_raw_predicate_sanity_check/4]).
6
7		:- use_module(probsrc(module_information)).
8		:- module_info(group,typechecker).
9		:- module_info(description,'Static checking of B machines upon construction. Detection of name clashes and uninitalised variables.').
10
11		:- use_module(bmachine_structure, [get_section/3]).
12		:- use_module(b_read_write_info, [get_accessed_vars/4]).
13		:- use_module(bsyntaxtree, [get_texpr_expr/2,get_texpr_id/2,get_texpr_ids/2]).
14		:- use_module(error_manager, [add_warning/3, add_warning/4, add_error/4]).
15		:- use_module(debug, [debug_println/2]).
16		:- use_module(tools, [ajoin/2]).
17		:- use_module(library(lists)).
18
19		static_check_main_machine(Machine) :-
20		debug_println(19,"Running static machine checks"),
21		initialises_all_variables(Machine),
22		check_name_clashes(Machine).
23
24
25		% ---------------------------------------------
26		% check for unnatural invariants and properties
27		% ---------------------------------------------
28		% the priority of the implication is sometimes surprising
29		% a & (x=1) => (y=2) & c --> top-level symbol is the implication !
30		% the test is done on the raw predicate before ast_cleanup removes potential typing predicates; see tests 106, 107
31		toplevel_raw_predicate_sanity_check(invariant,MachName,RawPredicate,Infos) :-
32	?	member(has_variables,Infos), % otherwise it is ok to have just a single disjunt, implication,...
33		check_top_level(RawPredicate,MachName,'INVARIANT'),
34		fail.
35		toplevel_raw_predicate_sanity_check(properties,MachName,RawPredicate,Infos) :-
36		member(has_constants,Infos), % otherwise it is ok to have just a single disjunt, implication,...
37		check_top_level(RawPredicate,MachName,'PROPERTIES'),
38		fail.
39		toplevel_raw_predicate_sanity_check(_,_,_,_).
40
41		% typical error: forget parentheses; if we write P => Q & R --> this is parsed as P => (Q & R)
42		check_top_level(implication(_,B,C),MachName,SECT) :-
43		(composed_predicate(B) ; composed_predicate(C)),!,
44		add_warning(bmachine_static_checks,'Top-level implication (=>) in clause: ',MachName:SECT).
45		check_top_level(disjunct(_,B,C),MachName,SECT) :-
46		(composed_predicate(B) ; composed_predicate(C)),!,
47		add_warning(bmachine_static_checks,'Top-level disjunction (or) in clause: ',MachName:SECT).
48		check_top_level(equivalence(_,B,C),MachName,SECT) :-
49		(composed_predicate(B) ; composed_predicate(C)),!,
50		add_warning(bmachine_static_checks,'Top-level equivalence (<=>) in clause: ',MachName:SECT).
51
52		% check if a predicate is composed of a binary operator where confusion may arise
53		% with negation and quantification there are explicit parentheses; the user should not be confused
54		composed_predicate(A) :- functor(A,Operator,3),
55		boolean_operator(Operator).
56		boolean_operator(conjunct).
57		boolean_operator(disjunct).
58		boolean_operator(implication).
59		boolean_operator(equivalence).
60
61		% ---------------------
62		% Checks is all variables are initialised by the machine
63		% ---------------------
64		initialises_all_variables(Machine) :-
65		get_section(initialisation,Machine,Initialisation),
66		% check wich variables are read / modified by the initialisation
67		get_accessed_vars(Initialisation,[],Modifies,_Reads),
68		get_machine_variables(Machine,SortedAllVars),
69		% check for each variable, if the initialisation modifies it
70		exclude(is_initialised(Modifies),SortedAllVars,Uninitialised),
71		% generate a warning if unitialised is not empty
72		generate_uninitialised_warning(Uninitialised,Initialisation),
73		% now check order of initialisation sequences
74		check_initialisation_order(Initialisation,SortedAllVars,[],_).
75
76		get_machine_variables(Machine,SortedAllVars) :-
77		% get all variables that should be initialised
78		get_section(abstract_variables,Machine,AbsVars),
79		get_section(concrete_variables,Machine,ConcVars),
80		append(AbsVars,ConcVars,TAllVars),
81		get_texpr_ids(TAllVars,AllVars),
82		sort(AllVars,SortedAllVars).
83
84		is_initialised(Modifies,Id) :-
85		memberchk(Id,Modifies).
86
87		generate_uninitialised_warning([],_) :- !.
88		generate_uninitialised_warning(Vars,Initialisation) :-
89		Msg='Machine may not initialise some of its variables: ',
90		add_warning(bmachine_static_checks,Msg,Vars,Initialisation).
91
92
93		:- use_module(library(ordsets)).
94		% Check if order of sequential compositions in INITIALISATION is ok
95		% TO DO: add support for if(LIST) and while
96		check_initialisation_order(b(Subst,subst,Info),AllVars,AlreadyInit,OutInit) :-
97		check_initialisation_order2(Subst,Info,AllVars,AlreadyInit,OutInit),!.
98		check_initialisation_order(Subst,AllVars,AlreadyInit,OutInit) :-
99		% print('CHCK '), translate:print_subst(Subst),nl,
100		get_accessed_vars(Subst,[],Modifies,Reads),
101		check_subst_or_pred(Subst,Modifies,Reads,AllVars,AlreadyInit,OutInit).
102
103		check_subst_or_pred(Subst,Modifies,Reads,AllVars,AlreadyInit,OutInit) :-
104		ord_union(Modifies,AlreadyInit,OutInit), % after Subst we have initialised OutInit
105		% below is already checked by type checker:
106		%ord_subtract(Modifies,AllVars,IllegalAssignments),
107		%(IllegalAssignments=[] -> true
108		% ; add_warning(bmachine_static_checks,'INITIALISATION writes illegal variables: ',IllegalAssignments,Subst)),
109		ord_intersection(Reads,AllVars,ReadFromSameMachine),
110		(atomic_subst(Subst)
111		-> ord_subtract(ReadFromSameMachine,AlreadyInit,IllegalReads)
112		; ord_subtract(ReadFromSameMachine,OutInit,IllegalReads) % we use OutInit: there could be an if with sequence inside
113		),
114		(IllegalReads=[] -> true
115		; add_warning(bmachine_static_checks,'INITIALISATION reads variables which are not yet initialised: ',IllegalReads,Subst)).
116
117		:- use_module(bsyntaxtree,[find_identifier_uses/3]).
118		check_initialisation_order2(choice([First|T]),Info,AllVars,AlreadyInit,OutInit) :- !,
119		check_initialisation_order(First,AllVars,AlreadyInit,OutInit), % we pick the output of the first choice
120		(T=[] -> true ; check_initialisation_order(b(choice(T),subst,Info),AllVars,AlreadyInit,_)).
121		check_initialisation_order2(parallel([First|T]),Info,AllVars,AlreadyInit,OutInit) :- !,
122		check_initialisation_order(First,AllVars,AlreadyInit,OutInit1), % we pick the output of the first choice
123		(T=[] -> OutInit=OutInit1
124		; check_initialisation_order2(parallel(T),Info,AllVars,AlreadyInit,OutInitRest),
125		ord_union(OutInit1,OutInitRest,OutInit)
126		).
127		check_initialisation_order2(init_parallel(S),Info,AllVars,AlreadyInit,OutInit) :- !,
128		check_initialisation_order(b(parallel(S),subst,Info),AllVars,AlreadyInit,OutInit).
129		check_initialisation_order2(sequence([First|T]),Info,AllVars) --> !,
130		check_initialisation_order(First,AllVars),
131		({T=[]} -> [] ; check_initialisation_order(b(sequence(T),subst,Info),AllVars)).
132		check_initialisation_order2(any(_Ids,Pred,Subst),_Info,AllVars,AlreadyInit,OutInit) :- !,
133		find_identifier_uses(Pred,[],Reads),
134		check_subst_or_pred(Pred,[],Reads,AllVars,AlreadyInit,_), % check predicate reads are ok
135		check_initialisation_order(Subst,AllVars,AlreadyInit,OutInit).
136		% TO DO: also check if-then-else, while, ...
137
138		atomic_subst(b(S,_,_)) :- atomic_subst2(S).
139		atomic_subst2(skip).
140		atomic_subst2(assign(_,_)).
141		atomic_subst2(assign_single_id(_,_)).
142		atomic_subst2(becomes_element_of(_,_)).
143		%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)
144
145		% ---------------------
146		% Checks if an operations parameter or local variable clashes with a variable
147		% ---------------------
148		check_name_clashes(Machine) :-
149		debug_println(10,'Checking for name clashes'),
150		% get all variables and constants that might clash
151		get_section_ids(abstract_variables,Machine,'variable',AbsVars),
152		get_section_ids(concrete_variables,Machine,'variable',ConcVars),
153		get_section_ids(abstract_constants,Machine,'constant',AbsCons),
154		get_section_ids(concrete_constants,Machine,'constant',ConcCons),
155		get_section_ids(deferred_sets,Machine,'set',DefSets),
156		get_section_ids(enumerated_sets,Machine,'set',EnumSets),
157		get_section_ids(enumerated_elements,Machine,'set element',EnumElems),
158		% enumerated b_get_named_machine_set(GlobalSetName,ListOfConstants) + b_get_machine_set(S)
159		append([AbsVars,ConcVars,AbsCons,ConcCons,DefSets,EnumSets,EnumElems],AllIds),
160		sort(AllIds,SortedAllIds),
161		%print(SortedAllIds),nl,nl,
162		% for each operation, compare the parameter names with existing vars/constants
163		get_section(operation_bodies,Machine,Operations),
164		maplist(op_name_clashes(SortedAllIds),Operations),
165		get_section(definitions,Machine,Defs),
166		maplist(def_name_clashes(SortedAllIds),Defs).
167
168		get_section_ids(Section,Machine,Class,ResultList) :-
169		get_section(Section,Machine,Vars),
170		findall(machine_id(ID,Class),(member(TID,Vars),get_texpr_id(TID,ID)),ResultList).
171
172
173		:- use_module(bsyntaxtree,[map_over_typed_bexpr/2]).
174		:- use_module(external_functions,[is_external_function_name/1]).
175
176		def_name_clashes(AllIds,definition_decl(Name,DefType,_DefPos,Args,_RawExpr,_Deps)) :- !,
177		findall(b(identifier(ID),any,[nodeid(IdPos)]),
178		member(identifier(IdPos,ID),Args),ArgIds), % args can sometimes not be identifiers; see test 1711
179		debug_println(4,checking_def(Name,DefType,Args,ArgIds)),
180		% exclude external functions/predicates/...;
181		% EXTERNAL_ declarations do not seem to be included; TO DO: check whether external function actually declared
182	?	(is_external_function_name(Name) -> true
183		; include(clash_warnings('DEFINITION parameter',AllIds,'DEFINITION',Name),ArgIds,_ArgsCausingWarning)
184		% TO DO: check Body; for this we need a map_over_raw_expression to detect local variables introduced !
185		).
186		def_name_clashes(_,D) :- print(unknown_def(D)),nl.
187
188		:- use_module(preferences,[get_preference/2]).
189		op_name_clashes(AllIds,Operation) :-
190		get_texpr_expr(Operation,operation(IdFull,Results,Params,Subst)),
191		%get_texpr_id(IdFull,op(Id)),
192		IdFull = b(identifier(op(Id)),Type,Info),
193		(get_preference(clash_strict_checks,true)
194		-> include(clash_warnings('Operation name',AllIds,operation,Id),[b(identifier(Id),Type,Info)],_NameCausingWarning) % fix PROB-60
195		; true),
196		include(clash_warnings('Operation parameter',AllIds,operation,Id),Params,_ParamsCausingWarning),
197		include(clash_warnings('Operation result variable',AllIds,operation,Id),Results,_ResultsCausingWarning),
198	?	(map_over_typed_bexpr(bmachine_static_checks:check_operation_body(AllIds,Id),Subst),fail ; true).
199
200		:- public check_operation_body/3.
201		check_operation_body(AllIds,Operation,TSubst) :-
202	?	get_texpr_expr(TSubst,Subst),
203	?	(local_variable_clash(Subst,TSubst,AllIds,Operation);
204		illegal_op_call(Subst,Operation)).
205
206		local_variable_clash(Subst,TSubst,AllIds,Operation) :-
207	?	introduces_local_variable(Subst,ID),
208		%print(check(ID,Operation)),nl,
209		clash_local_warnings(AllIds,Operation,ID,TSubst).
210
211		% check if something like zz(1) <-- Op(a) is used; this is not allowed according to Atelier-B
212		illegal_op_call(operation_call(CalledOperation,Results,_Parameters),Operation) :-
213		member(TID,Results), \+ get_texpr_id(TID,_),
214		(get_texpr_id(CalledOperation,op(CalledId)) -> true ; CalledId=CalledOperation),
215		ajoin(['Return value of operation call to ',CalledId,' must be stored in identifier within:'],Msg),
216		add_error(bmachine_static_checks,Msg,Operation,TID).
217
218		% check for constructs which introduced local variables
219		introduces_local_variable(var(Parameters,_),ID) :- % currently B-interpreter cannot correctly deal with this in the context of operation_call
220	?	member(TID,Parameters), get_texpr_id(TID,ID).
221
222		% ord_member does not work below because of free variable Class
223		my_ord_member(Name,Class,[machine_id(Name1,_)|T]) :-
224		Name @> Name1, !,
225		my_ord_member(Name,Class,T).
226		my_ord_member(Name,Class,[machine_id(Name,Class)|_]).
227
228		clash_warnings(Context,AllIds,OpOrDef,OperationId,TName) :-
229		get_texpr_id(TName,Name),
230		my_ord_member(Name,Class,AllIds), !,
231		ajoin([Context, ' "', Name, '" has the same name as a ', Class, ' in ',OpOrDef,' "', OperationId,'".'], Msg),
232		add_warning(bmachine_static_checks,Msg,'',TName).
233
234		clash_local_warnings(AllIds,OperationId,Name,Pos) :-
235		my_ord_member(Name,Class,AllIds), !,
236		ajoin(['Local variable has the same name as a ', Class, ' in operation ', OperationId,': '], Msg),
237		add_warning(bmachine_static_checks,Msg,Name,Pos).
238
239		% TODO: this does not and can not work here:
240		% - Some preconditions are removed (typing only....) during machine simplification
241		% - Needs to be verified during typechecking
242		% ---------------------
243		% Checks if an operations parameter is not typed by a pre condition
244		% ---------------------
245		%parameters_without_pre_condition(Machine) :-
246		% get_section(operation_bodies,Machine,Operations),
247		% maplist(parameters_without_pre_condition_aux,Operations).
248		%
249		%parameters_without_pre_condition_aux(Operation) :-trace,
250		% get_texpr_expr(Operation,operation(IdFull,_Results,Params,Subst)),
251		% get_texpr_id(IdFull,op(Id)),
252		% (Params == []
253		% -> true % no parameters
254		% ; (get_texpr_expr(Subst,precondition(_,_))
255		% -> true % parameters and precondition
256		% ; ajoin(['Operation ', Id, ' has parameters but no pre-condition.'], Msg),
257		% add_warning(bmachine_static_checks,Msg)
258		% )).