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 | % )). |