1 | | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
4 | | |
5 | | :- module(b_read_write_info,[get_accessed_vars/4, get_accessed_vars/5, |
6 | | recompute_while_read_write_info/2, |
7 | | get_nondet_modified_vars/3, |
8 | | tcltk_read_write_matrix/1, |
9 | | tcltk_variable_read_write_matrix/2, |
10 | | tcltk_dot_variable_modification_analysis/1, |
11 | | tcltk_get_guards_for_ops/1, |
12 | | tcltk_get_parameter_free_guards_for_ops/1, |
13 | | b_get_read_write/3, |
14 | | b_get_operation_read_guard_vars/4, |
15 | | b_get_read_write_vars/5, |
16 | | b_get_written_variables/1, check_all_variables_written/0, |
17 | | %,b_get_read_may_must_write/7 % currently not used outside |
18 | | |
19 | | get_lhs_assigned_identifier/2 |
20 | | ]). |
21 | | |
22 | | |
23 | | :- use_module(module_information,[module_info/2]). |
24 | | :- module_info(group,typechecker). |
25 | | :- module_info(description,'ProBs type checker and type inference module.'). |
26 | | |
27 | | :- use_module(library(lists)). |
28 | | :- use_module(library(ordsets)). |
29 | | :- use_module(self_check). |
30 | | :- use_module(error_manager). |
31 | | :- use_module(bsyntaxtree). |
32 | | |
33 | | |
34 | | recompute_while_read_write_info(TExpr,NewTExpr) :- |
35 | | (transform_bexpr(b_read_write_info:update_while_info,TExpr,NewTExpr) |
36 | | -> true |
37 | | ; add_internal_error('Call failed: ',transform_bexpr(b_read_write_info:update_while_info,TExpr,NewTExpr)), |
38 | | NewTExpr=TExpr). |
39 | | |
40 | | :- use_module(translate,[print_bexpr/1]). |
41 | | :- public update_while_info/2. |
42 | | update_while_info(b(WHILE,subst,OldInfo),b(WHILE,subst,NewInfo)) :- |
43 | | WHILE = while(_TPred,_TBody,_TInv,TVar), |
44 | | get_accessed_vars(b(WHILE,subst,OldInfo),[],Modifies,Reads), |
45 | | (debug:debug_mode(off) -> true |
46 | | ; nl,print('UPDATING WHILE with VARIANT: '), print_bexpr(TVar),nl, |
47 | | format(' WHILE Reads : ~w~n Modifies : ~w~n',[Reads,Modifies]) |
48 | | ), |
49 | | (delete(OldInfo,reads(OldReads),OI1) -> true ; OldReads=[], OI1=OldInfo), |
50 | | (delete(OI1,modifies(OldModifies),OI2) -> true ; OldModifies=[], OI2=OI1), |
51 | | ((Reads,Modifies)=(OldReads,OldModifies) |
52 | | -> NewInfo=OldInfo |
53 | | ; format('***** different from Reads : ~w~n Modifies : ~w~n',[OldReads,OldModifies]), |
54 | | ord_subtract(Reads,OldReads,NewR), |
55 | | ord_subtract(OldReads,Reads,DelR), |
56 | | format(' added: ~w~n deleted: ~w~n****~n',[NewR,DelR]), |
57 | | NewInfo = [modifies(Modifies),reads(Reads)|OI2] |
58 | | ). |
59 | | |
60 | | % TO DO: also update info for operation call ! |
61 | | |
62 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
63 | | |
64 | | :- use_module(bsyntaxtree,[get_global_identifiers/1]). |
65 | | |
66 | | /* get_accessed_vars/4 computes the variables that are read or written to |
67 | | by a substitution. |
68 | | get_accessed_vars(+Subst,+LocalVars,-Modified,-Reads): |
69 | | Subst is the substitution (as a typed syntax tree) |
70 | | LocalVars is a list of (untyped) ids that are local variables. |
71 | | Local variables are ignored and not included in the list of read or written |
72 | | variables. |
73 | | Modified is the list of (untyped) identifiers that are written by the substitution and |
74 | | Reads is the list of (untyped) identifiers that are read. */ |
75 | | get_accessed_vars(TSubst,LocalVars,Modified,Reads) :- |
76 | | get_accessed_vars(TSubst,LocalVars,Modified,_,Reads). |
77 | | get_accessed_vars(TSubst,LocalVars,Modified,NonDetModified,Reads) :- |
78 | | get_global_identifiers(IS), % TO DO: currently this information is set up only *after* type checking !! |
79 | | % this means the accessed vars will also contain SETS and enumerated set elements ! |
80 | | % either we need to filter them out later, or change the startup / precompilation process |
81 | | list_to_ord_set(LocalVars,SLV), |
82 | | ord_union(IS,SLV,LocalVarsToIgnore), |
83 | | empty_mrinfo(In), |
84 | | get_accessed_vars1(TSubst,LocalVarsToIgnore,In,Out), |
85 | | extract_reads_and_modifies(In,Out,Modified,NonDetModified,Reads). |
86 | | extract_reads_and_modifies(mrinfo(_,_,_),mrinfo(Modified,NonDetModified,Reads), |
87 | | Modified,NonDetModified,Reads). |
88 | | |
89 | | % get variables which are modified non-deterministically; does not traverse operation calls at the moment |
90 | | get_nondet_modified_vars(TSubst,LocalVars,NonDetModified) :- |
91 | | empty_mrinfo(In), |
92 | | list_to_ord_set(LocalVars,SLocalVars), |
93 | | get_accessed_vars1(TSubst,SLocalVars,In,Out), |
94 | | Out=mrinfo(_,NonDetModified,_). |
95 | | |
96 | | is_operation_call(operation_call(Operation,Results,Arguments),Operation,Results,Arguments). |
97 | | is_operation_call(operation_call_in_expr(Operation,Arguments),Operation,[],Arguments). % cannot match, as we are in a substitution context |
98 | | |
99 | | get_accessed_vars1(TSubst,LocalVars,In,Out) :- |
100 | | get_texpr_expr(TSubst,Subst), |
101 | | ( is_operation_call(Subst,Operation,Results,Arguments) -> |
102 | | get_texpr_info(TSubst,Info), |
103 | | def_get_texpr_id(Operation,op(OperationName)), |
104 | | memberchk(modifies(MVars),Info), |
105 | | (memberchk(non_det_modifies(NonDetMVars),Info) -> true ; NonDetMVars=[]), |
106 | | memberchk(reads(RVars),Info), |
107 | | % info fields added in btype2(operation(...) in btypechecker.pl |
108 | | %op_modifies_reads_cache(OperationName,MVarsC,RVarsC) %this is no longer necessary |
109 | | (ground(MVars),ground(RVars) |
110 | | -> true |
111 | | ; add_error(b_read_write_info, 'Cannot obtain modifies/reads info for called operation (probably illegal local call): ',OperationName), |
112 | | % TEST 655 used to reach this branch |
113 | | MVars=[], RVars=[], NonDetMVars=[] |
114 | | % this should only happen when local operation called !?! |
115 | | % or ensure that operations are processed before we reach operation calls |
116 | | % this may be problematic for local operations |
117 | | ), |
118 | | accessed_vars_for_operation_call(MVars,NonDetMVars,RVars,LocalVars,Results,Arguments,In,Out) |
119 | ? | ; get_accessed_vars2(Subst,LocalVars,In,Out) -> |
120 | | true |
121 | | ; Subst = identifier(ID) -> add_error(b_read_write_info,'Identifier not a valid B Operation: ',ID,TSubst),In=Out |
122 | | ; |
123 | | add_internal_error('Could not extract information about accessed variables for substitution', |
124 | | get_accessed_vars2(Subst,LocalVars,In,Out)), |
125 | | %trace, get_accessed_vars2(Subst,LocalVars,In,Out), |
126 | | fail). |
127 | | accessed_vars_for_operation_call(MVars,NonDetMVars,RVars,LocalVars,Results,Arguments) --> |
128 | | add_non_local_modified_vars(MVars,LocalVars), |
129 | | add_non_local_read_vars(RVars,LocalVars), |
130 | | add_modified_vars(Results,LocalVars), |
131 | | add_non_local_non_det_modified_vars(NonDetMVars,LocalVars), |
132 | | add_read_vars_l(Arguments,LocalVars). |
133 | | |
134 | | get_accessed_vars2(skip,_) --> !. |
135 | | get_accessed_vars2(block(Subst),LocalVars) --> get_accessed_vars1(Subst,LocalVars). |
136 | | get_accessed_vars2(init_statement(Subst),LocalVars) --> get_accessed_vars1(Subst,LocalVars). |
137 | | get_accessed_vars2(assertion(A,Subst),R) --> add_read_vars(A,R),get_accessed_vars1(Subst,R). |
138 | | get_accessed_vars2(assign(LHS,E),R) --> %Note: LHS can be nested function application f(a)(b) := |
139 | | {maplist(get_lhs_assigned_identifier,LHS,Ids)}, add_modified_vars(Ids,R), |
140 | | {convlist(get_lhs_read_expression,LHS,LHS_R), append(LHS_R,E,RE)}, add_read_vars_l(RE,R). |
141 | | get_accessed_vars2(assign_single_id(Id,E),R) --> |
142 | | add_read_vars_l([E],R), % Note: LHS is a single Identifier: nothing is ever read there |
143 | | add_modified_vars([Id],R). |
144 | | get_accessed_vars2(precondition(P,Subst),R) -->add_read_vars(P,R),get_accessed_vars1(Subst,R). |
145 | | get_accessed_vars2(assertion(Subst),R) --> get_accessed_vars1(Subst,R). |
146 | ? | get_accessed_vars2(choice(Substs),R) --> get_accessed_vars_for_choice(Substs,R). |
147 | ? | get_accessed_vars2(if(Substs),R) --> get_accessed_vars_for_if(Substs,R). |
148 | ? | get_accessed_vars2(select(Whens,Else),R) --> get_accessed_vars_for_select(Whens,Else,R). |
149 | ? | get_accessed_vars2(select(Whens),R) --> get_accessed_vars_for_select(Whens,none,R). |
150 | ? | get_accessed_vars2(case(Expr,Substs,Else),R) --> get_accessed_vars_for_case(Expr,Substs,Else,R). |
151 | | get_accessed_vars2(case_or(Exprs,Subst),R) --> add_read_vars_l(Exprs,R),get_accessed_vars1(Subst,R). |
152 | | get_accessed_vars2(any(Ids,G,Subst),R) --> get_mrinfo(ModIn,_,_), |
153 | | add_tvars_to_ord_list(R,Ids,L),add_read_vars(G,L), |
154 | | get_accessed_vars1(Subst,L), |
155 | | add_delta_modified_to_non_det_modified(ModIn). % variables modified within an ANY are supposed to be non-det assigned; e.g. ANY x WHERE x:1..2 THEN y:=x END |
156 | | get_accessed_vars2(let(Ids,G,Subst),R) --> |
157 | | add_tvars_to_ord_list(R,Ids,L),add_read_vars(G,L),get_accessed_vars1(Subst,L). |
158 | | get_accessed_vars2(lazy_let_subst(ID,SharedExpr,Subst),R) --> add_tvars_to_ord_list(R,[ID],L), |
159 | | add_read_vars(SharedExpr,L),get_accessed_vars1(Subst,L). |
160 | | get_accessed_vars2(becomes_element_of(Ids,E),R) --> add_non_det_modified_vars(Ids,R),add_read_vars(E,R). |
161 | | get_accessed_vars2(becomes_such(Ids,E),LocalVars0) --> |
162 | | add_non_det_modified_vars(Ids,LocalVars0), |
163 | | {find_read_vars_for_becomes_such(Ids,E,LocalVars0,ReadVars)}, |
164 | | add_read_vars2(ReadVars). |
165 | | %get_accessed_vars2(evb2_becomes_such(Ids,E),R) --> % now translated to becomes_such |
166 | | % add_non_det_modified_vars(Ids,R), add_read_vars(E,R). |
167 | | get_accessed_vars2(sequence(Substs),R) --> get_accessed_vars_sequence(Substs,R). |
168 | | get_accessed_vars2(parallel(Substs),R) --> get_accessed_vars_l(Substs,R). |
169 | | get_accessed_vars2(while(Cond,Subst,Inv,Variant),R) --> |
170 | ? | get_accessed_vars_for_while(Cond,Subst,Inv,Variant,R). |
171 | | get_accessed_vars2(var(Ids,Subst),R) --> add_tvars_to_ord_list(R,Ids,L),get_accessed_vars1(Subst,L). |
172 | | % TODO: we need information about which variables are modified by an external function |
173 | | get_accessed_vars2(external_subst_call(_Name,Exprs),R) --> add_read_vars_l(Exprs,R). |
174 | | get_accessed_vars2(rlevent(_Name,_Section,VariantStatus,Params,Guard,Theorems,Actions,VWitnesses,PWitnesses,Unmod,AbstractEvents),R) --> |
175 | | % the code duplicates the logic in collect_read_vars in bmachine_eventb.pl; TO-DO: merge |
176 | | add_tvars_to_ord_list(R,Params,L), |
177 | | add_read_vars(Guard,L), |
178 | | add_read_vars_l(Theorems,L), |
179 | | add_read_vars_l(Unmod,L), % for unmodifiables we check that whether new values correspond to old values and thus need read accces to the old value in check_if_invalid_vars_are_modified |
180 | | add_variant_status_read_vars(VariantStatus,R), % the parameters should not be used in the Variant |
181 | | add_witness_read_vars_l(VWitnesses,L), |
182 | | add_witness_read_vars_l(PWitnesses,L), |
183 | | get_accessed_vars_l(Actions,L), |
184 | | get_accessed_vars_l(AbstractEvents,L). |
185 | | |
186 | | get_accessed_vars_for_while(Cond,Subst,Inv,Variant,Locals) --> |
187 | | get_accessed_vars_for_while_invariant(Inv,Locals), |
188 | | add_read_vars(Cond,Locals), |
189 | | add_read_vars(Variant,Locals), |
190 | | %get_accessed_vars1(Subst,Locals). |
191 | | % The Substitution may not be executed; just like an IF |
192 | | % e.g. "WHILE P DO x:=1 ... END" may keep (and thus virtually read) the old value of x if P is false initially |
193 | ? | get_accessed_vars_for_if_when(if_with_no_else,[Subst],Locals). |
194 | | get_accessed_vars_for_while_invariant(Inv,Locals,In,Out) :- |
195 | | empty_mrinfo(LI), |
196 | | add_read_vars(Inv,Locals,LI,LO), |
197 | | extract_reads_and_modifies(LI,LO,Modified,_,Reads0), |
198 | | maplist(remove_optional_prime,Reads0,Reads), |
199 | | list_to_ord_set(Reads,SReads), % removing prime can create duplicates |
200 | | add_non_local_read_vars(SReads,Locals,In,Inter), |
201 | | add_non_local_modified_vars(Modified,Locals,Inter,Out). |
202 | | remove_optional_prime(Id,Orig) :- atom_concat(Orig,'$0',Id),!. |
203 | | remove_optional_prime(Id,Id). |
204 | | |
205 | | get_accessed_vars_for_if(ElseIfs,Locals) --> |
206 | | { maplist(split_elseif,ElseIfs,Conds,Subst), |
207 | | (if_has_else_block(Conds) -> HasElse = has_else ; HasElse = if_with_no_else) }, |
208 | | % mark all used variables in the conditions as read |
209 | | add_read_vars_l(Conds,Locals), |
210 | ? | get_accessed_vars_for_if_when(HasElse,Subst,Locals). |
211 | | split_elseif(Expr,Cond,Subst) :- get_texpr_expr(Expr,if_elsif(Cond,Subst)). |
212 | | |
213 | | get_accessed_vars_for_select(Whens,Else,Locals) --> |
214 | | { maplist(split_when,Whens,Conds,Subst1), |
215 | | ( Else = none -> |
216 | | HasElse=select_no_else, Subst = Subst1 |
217 | | ; |
218 | | HasElse=has_else, Subst = [Else|Subst1]) }, |
219 | | % mark all used variables in the conditions as read |
220 | | add_read_vars_l(Conds,Locals), |
221 | ? | get_accessed_vars_for_if_when(HasElse,Subst,Locals). |
222 | | split_when(Expr,Cond,Subst) :- get_texpr_expr(Expr,select_when(Cond,Subst)). |
223 | | |
224 | | |
225 | | % treat substitution body of IF/WHEN/WHILE |
226 | | get_accessed_vars_for_if_when(HasElse,Subst,Locals) --> |
227 | ? | { get_accessed_vars_for_if_when2(HasElse,Subst,Locals,Modified,NonDetModifies,Reads) }, |
228 | | add_read_vars2(Reads), |
229 | | %add_modified_vars2(Modified) |
230 | | ({(HasElse==has_else ; HasElse==if_with_no_else ; Subst = [_,_|_])} |
231 | | -> {my_ord_union(NonDetModifies,Modified,M2)}, |
232 | | add_non_det_modified_vars2(M2) |
233 | | ; add_non_det_modified_vars2(NonDetModifies), |
234 | | add_modified_vars2(Modified) % there is only one branch: Modified variables not also marked as non-det modified |
235 | | ). |
236 | | |
237 | | :- use_module(tools,[maplist5/5]). |
238 | | |
239 | | get_accessed_vars_for_if_when2(has_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome) :- |
240 | ? | maplist5(get_accessed_vars_x(Locals),Subst,Modifies,NonDetModifies,Reads), |
241 | | % We want to calculate those elements that are modified by some (in the union) |
242 | | % but not by all (in the intersection) |
243 | | ord_union(NonDetModifies,NonDetModifiedBySome), |
244 | | ord_union(Modifies,ModifiedBySome), |
245 | | ord_intersection(Modifies,ModifiedByAll), |
246 | | ord_subtract(ModifiedBySome,ModifiedByAll,ModifiedByNotAll), |
247 | | % we add those values that are not modified by all to the set of read variables |
248 | | % because e.g. "IF P THEN x:=1 END" is equivalent to "IF P THEN x:=1 ELSE x:=x END" |
249 | | ord_union([ModifiedByNotAll|Reads],ReadBySome). |
250 | | get_accessed_vars_for_if_when2(select_no_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome) :- |
251 | | % Note "SELECT P THEN x:=1 END" is NOT equivalent to "SELECT P THEN x:=1 ELSE x:=x END" ! |
252 | | % there is no implicit skip, which copies all variables; |
253 | | % as such it can be treated like an if with an exhaustive list of cases |
254 | | % the treatment for computing ModifiedBySome,ReadBySome is identical |
255 | ? | get_accessed_vars_for_if_when2(has_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome). |
256 | | get_accessed_vars_for_if_when2(if_with_no_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome) :- |
257 | | % no else block present, we must assume that each written variable |
258 | | % can also be treated like a read variable, see example in the other condition: |
259 | | % e.g. "IF P THEN x:=1 END" is equivalent to "IF P THEN x:=1 ELSE x:=x END" and thus reads the old value of x |
260 | ? | maplist5(get_accessed_vars_x(Locals),Subst,Modifies,NonDetModifies,Reads), |
261 | | ord_union(NonDetModifies,NonDetModifiedBySome), |
262 | | ord_union(Modifies,ModifiedBySome), |
263 | | ord_union([ModifiedBySome|Reads],ReadBySome). |
264 | | |
265 | | get_accessed_vars_for_choice(Substs,Locals,In,mrinfo(ModOut,NDOut2,Read)) :- |
266 | ? | get_accessed_vars_for_if_when(has_else,Substs,Locals,In,Out), |
267 | | In = mrinfo(ModIn,_,_), |
268 | | Out = mrinfo(ModOut,NDOut,Read), % these three fields will be all variables |
269 | | % mark all assignments as non-deterministically chosen: |
270 | | add_modified_to_non_det_modified(ModIn,ModOut,NDOut,NDOut2). |
271 | | |
272 | | add_modified_to_non_det_modified(ModIn,ModOut,NDOut,NDOut2) :- |
273 | | ord_subtract(ModOut,ModIn,Delta), % these variables were detected as written |
274 | | ord_union(Delta,NDOut,NDOut2). |
275 | | |
276 | | |
277 | | % get the modifies/read info for use in a DCG context: |
278 | | get_mrinfo(Modified,NonDetModified,InRead,I,I) :- |
279 | | (var(I) -> add_internal_error('Unbound mrinfo env:',I) ; true), |
280 | | I = mrinfo(Modified,NonDetModified,InRead), |
281 | | (var(Modified) -> add_internal_error('Illegal mrinfo env:',I) ; true). |
282 | | |
283 | | %portray_mrinfo(Msg,I,I) :- I=mrinfo(Modified,NonDetModified,Read),!, |
284 | | % format('~w : modified=~w (non-det:~w), read=~w~n',[Msg,Modified,NonDetModified,Read]). |
285 | | %portray_mrinfo(Msg,I,I) :- format(user_error,'*** ~w ~w~n',[Msg,I]). |
286 | | |
287 | | % create an initial modifies/reads info environment for the DCGs |
288 | | empty_mrinfo(mrinfo([],[],[])). |
289 | | |
290 | | my_ord_union(Vars,S,Res) :- \+ is_ordset(Vars),!, |
291 | | add_internal_error('Not sorted (first argument): ',my_ord_union(Vars,S,Res)), |
292 | | list_to_ord_set(Vars,SV), ord_union(SV,S,Res). |
293 | | my_ord_union(Vars,S,Res) :- \+ is_ordset(S),!, |
294 | | add_internal_error('Not sorted (second argument): ',my_ord_union(Vars,S,Res)), |
295 | | list_to_ord_set(S,SS), ord_union(Vars,SS,Res). |
296 | | my_ord_union(Vars,S,Res) :- ord_union(Vars,S,Res). |
297 | | |
298 | | |
299 | | |
300 | | add_delta_modified_to_non_det_modified(ModIn,mrinfo(ModOut,NonDet,Read),mrinfo(ModOut,NonDet2,Read)) :- |
301 | | add_modified_to_non_det_modified(ModIn,ModOut,NonDet,NonDet2). |
302 | | |
303 | | get_accessed_vars_for_case(Expr,Eithers,Else,Locals) --> |
304 | | % we can treat a case statement analogously to an IF-THEN-ELSE statement |
305 | | % where an ELSE is present |
306 | | % additionally, we have to add all expressions to the read set |
307 | | add_read_vars(Expr,Locals), |
308 | | { maplist(split_case_or,Eithers,ExprsList,Substs), append(ExprsList,Exprs) }, |
309 | | add_read_vars_l(Exprs,Locals), |
310 | ? | get_accessed_vars_for_if_when(has_else,[Else|Substs],Locals). |
311 | | split_case_or(CaseOr,Exprs,Subst) :- get_texpr_expr(CaseOr,case_or(Exprs,Subst)). |
312 | | |
313 | | % just the same as get_accessed_vars, but with different order of parameters |
314 | | % to allow call with maplist |
315 | | get_accessed_vars_x(Locals,Subst,Modifies,NonDetModifies,Reads) :- |
316 | | get_accessed_vars(Subst,Locals,Modifies,NonDetModifies,Reads). |
317 | | |
318 | | if_has_else_block(Conds) :- |
319 | | last(Conds,Cond),is_truth(Cond). |
320 | | |
321 | | % add ids of unsorted list of typed identifiers to sorted list of ids: |
322 | | add_tvars_to_ord_list(SortedVars,TIds,NewVars,X,X) :- |
323 | | get_texpr_ids(TIds,Ids), |
324 | | list_to_ord_set(Ids,SIds), |
325 | | my_ord_union(SortedVars,SIds,NewVars). |
326 | | %append(Vars,Ids,NewVars). |
327 | | |
328 | | add_read_vars_l([],_LocalVars) --> !. |
329 | | add_read_vars_l([Expr|Rest],LocalVars) --> !, |
330 | | add_read_vars(Expr,LocalVars), |
331 | | add_read_vars_l(Rest,LocalVars). |
332 | | add_read_vars_l(E,LV) --> !, {add_internal_error('Not a list: ',add_read_vars_l(E,LV,_,_))}. |
333 | | |
334 | | add_variant_status_read_vars(b(Status,status,_Info),LocalVars) --> |
335 | | % TO DO: if member(convergence_proved,Info) should we add the vars? |
336 | | add_variant_status_aux(Status,LocalVars). |
337 | | |
338 | | add_variant_status_aux(convergent(VariantExpr),LocalVars) --> !, |
339 | | add_read_vars(VariantExpr,LocalVars). |
340 | | add_variant_status_aux(anticipated(VariantExpr),LocalVars) --> !, |
341 | | add_read_vars(VariantExpr,LocalVars). |
342 | | add_variant_status_aux(ordinary,_) --> !, []. |
343 | | add_variant_status_aux(Status,_) --> {add_warning(b_read_write_info,'Unrecognised VARIANT status: ',Status)}. |
344 | | |
345 | | add_witness_read_vars_l([],_LocalVars) --> !. |
346 | | add_witness_read_vars_l([Expr|Rest],LocalVars) --> |
347 | | add_witness_read_vars(Expr,LocalVars), !, |
348 | | add_witness_read_vars_l(Rest,LocalVars). |
349 | | add_witness_read_vars_l(E,LV) --> !, {add_internal_error('Not a witness list: ',add_witness_read_vars_l(E,LV,_,_))}. |
350 | | |
351 | | % extract modified identifier from LHS of assign: |
352 | | get_lhs_assigned_identifier(b(function(LHS,_),_,_),Res) :- !, get_lhs_assigned_identifier(LHS,Res). |
353 | | get_lhs_assigned_identifier(b(record_field(LHS,_),_,_),Res) :- !, % something like xx'field := yy (cf test 2032) |
354 | | get_lhs_assigned_identifier(LHS,Res). |
355 | | get_lhs_assigned_identifier(ID,ID) :- |
356 | | (ID= b(identifier(_),_,_) -> true ; add_warning(b_read_write_info,'Unrecognized LHS of assignment: ',ID,ID)). |
357 | | |
358 | | % extract part of LHS of assign which reads information: |
359 | | get_lhs_read_expression(b(function(LHS,Read1),T,I),Res) :- !, |
360 | | Res = b(function(LHS,Read1),T,I). |
361 | | get_lhs_read_expression(b(record_field(LHS,Read1),T,I),Res) :- !, |
362 | | Res = b(record_field(LHS,Read1),T,I). % TO DO: check if LHS has more than one field? but could be nested |
363 | | % old version which for f(a) := b only marked a as read in LHS f(a); now we also mark f |
364 | | % indeed f(a) := b is equivalent to f := f <+ {a|->b} ; so the old value of f is implicitly read (important for ltsmin symbolic model checking) |
365 | | % similarly r'x := b also reads the old value of r (if r has more than one field) |
366 | | %get_lhs_read_expression(b(function(LHS,Read1),_,_),Res) :- !, |
367 | | % (get_lhs_read_expression(LHS,Read2) -> create_couple(Read1,Read2,Res) |
368 | | % ; Res = Read1). |
369 | | |
370 | | add_witness_read_vars(b(witness(ID,Predicate),witness,_),LocalVars) --> !, |
371 | | % a parameter witness talks about a parameter no longer there: it is not really read here, but the predicate is used to set the any local parameter in another context |
372 | | % a variable witness alks about a variable non-deterministically assigned in the abstraction; we also pretend it is not read here (but assigned somewhere else) |
373 | | add_tvars_to_ord_list(LocalVars,[ID],LocalVars2), % we add ID to local variables not read "really" read here |
374 | | %{print(witness_add_read_vars(ID)),nl}, |
375 | | add_read_vars(Predicate,LocalVars2). |
376 | | |
377 | | add_read_vars(Expression,LocalVars) --> |
378 | | {find_identifier_uses(Expression,LocalVars,ReadVars)}, % TOOD: here we can have operation_call_in_expr with non-ground reads info! |
379 | | add_read_vars2(ReadVars). |
380 | | add_read_vars2(SVars,mrinfo(Modified,NonDetModified,InRead), |
381 | | mrinfo(Modified,NonDetModified,OutRead)) :- my_ord_union(SVars,InRead,OutRead). |
382 | | |
383 | | |
384 | | |
385 | | add_non_local_read_vars(ReadVars,LocalVars) --> |
386 | | {ord_subtract(ReadVars,LocalVars,AddVars)}, |
387 | | add_read_vars2(AddVars). |
388 | | add_non_local_modified_vars(WriteVars,LocalVars) --> |
389 | | {ord_subtract(WriteVars,LocalVars,AddVars)}, |
390 | | add_modified_vars2(AddVars). |
391 | | |
392 | | add_modified_vars(Ids,LocalVars) --> |
393 | | {filter_result_vars(Ids,LocalVars,ModifiedVars)}, |
394 | | add_modified_vars2(ModifiedVars). |
395 | | add_modified_vars2(Vars,In,Res) :- |
396 | | (var(Vars) |
397 | | -> add_internal_error('Modified Vars variable: ',add_modified_vars2(Vars,In,Res)) |
398 | | ; true), |
399 | | In = mrinfo(InModified,NonDetModified,Read), |
400 | | Res = mrinfo(OutModified,NonDetModified,Read), |
401 | | list_to_ord_set(Vars,SVars), |
402 | | my_ord_union(SVars,InModified,OutModified). |
403 | | |
404 | | |
405 | | add_non_local_non_det_modified_vars(WriteVars,LocalVars) --> |
406 | | {ord_subtract(WriteVars,LocalVars,AddVars)}, |
407 | | add_non_det_modified_vars2(AddVars). |
408 | | |
409 | | add_non_det_modified_vars(Ids,LocalVars) --> |
410 | | {filter_result_vars(Ids,LocalVars,ModifiedVars)}, |
411 | | {list_to_ord_set(ModifiedVars,SModifiedVars)}, |
412 | | add_non_det_modified_vars2(SModifiedVars). |
413 | | add_non_det_modified_vars2(Vars,In,Res) :- |
414 | | (var(Vars) |
415 | | -> add_internal_error('Modified Vars variable: ',add_non_det_modified_vars2(Vars,In,Res)) |
416 | | ; true), |
417 | | In = mrinfo(InModified,InNonDetModified,Read), |
418 | | Res = mrinfo(OutModified,OutNonDetModified,Read), |
419 | | my_ord_union(Vars,InModified,OutModified), |
420 | | my_ord_union(Vars,InNonDetModified,OutNonDetModified). |
421 | | |
422 | | |
423 | | :- use_module(tools,[remove_all/3]). |
424 | | filter_result_vars(Ids,LocalVars,ModifiedVars) :- |
425 | | % extract_changed_id might fail if the user entered |
426 | | % a wrong LHS of an assignment. This should lead to an |
427 | | % type error, handled by the assign type checking rule. |
428 | | convlist(extract_changed_id,Ids,Names), |
429 | | remove_all(Names,LocalVars,ModifiedVars). |
430 | | extract_changed_id(Id,Name) :- |
431 | | get_texpr_id(Id,Name),!. |
432 | | extract_changed_id(FuncOrRec,Name) :- |
433 | | get_texpr_expr(FuncOrRec,Expr), |
434 | | get_nested_modified_expr(Expr,TId), |
435 | | !, |
436 | | extract_changed_id(TId,Name). % we can have nested function calls f(x)(y) := z or nested records f(x)'field := z |
437 | | % nested records are currently not allowed in the btypechecker though (id_or_function_or_rec) |
438 | | extract_changed_id(X,Name) :- |
439 | | add_internal_error('Could not extract changed id: ',extract_changed_id(X,Name)),fail. |
440 | | |
441 | | get_nested_modified_expr(function(TId,_),TId). |
442 | | get_nested_modified_expr(record_field(TId,_Field),TId). |
443 | | |
444 | | get_accessed_vars_l([],_) --> []. |
445 | | get_accessed_vars_l([S|Rest],LovalVars) --> |
446 | | get_accessed_vars1(S,LovalVars), |
447 | | get_accessed_vars_l(Rest,LovalVars). |
448 | | |
449 | | % get accessed vars for a sequence (sequential composition) |
450 | | get_accessed_vars_sequence([],_) --> []. |
451 | | get_accessed_vars_sequence([S|Rest],LocalVars) --> %portray_mrinfo(seq(S)), |
452 | | % TO DO: we could always compute must_write information in get_accessed_vars, rather than re-traversing here: |
453 | | {Rest \= [], extract_must_write(S,not_nested,WIds),my_ord_union(WIds,LocalVars,LocalVars2)},!, |
454 | | % not_nested: do not look at nested operation calls: they may not be precompiled; and we cannot read them from here anyway? ; relevant tests: 1601, 1782, 1870 |
455 | | % treat case x := 0 ; y := x+1 --> x is read after completely written |
456 | | % careful, we can have: f(1) := 0; y := f(2) ! |
457 | | % we can also have: x:=x+1 ; y := x --> here x is read |
458 | | % Note: we need the must_write information to be sure that x cannot be read after S; may_write is not enough |
459 | | get_accessed_vars1(S,LocalVars), |
460 | | % in rest any read, write to LocalVars2 will not be registered; |
461 | | % only problem is that we could have something like x:=0 ; x::{1,2} and we would not register x as NonDetModifies |
462 | | % NonDetModifies is only used in animation interface to show additional virtual parameters for operations |
463 | | % it is thus not critical |
464 | | get_accessed_vars_sequence(Rest,LocalVars2). |
465 | | get_accessed_vars_sequence([S|Rest],LocalVars) --> |
466 | | get_accessed_vars1(S,LocalVars), |
467 | | get_accessed_vars_sequence(Rest,LocalVars). |
468 | | |
469 | | % now handled in find_identifier_uses |
470 | | %:- use_module(tools,[number_suffix/3]). |
471 | | %:- assert_must_succeed(( b_read_write_info:append_primed_vars([b(identifier(x),integer,[])],[],R), R = ['x$0'])). |
472 | | %append_primed_vars(TIds,R,L) :- |
473 | | % maplist(add_dollar_zero,TIds,Primed), |
474 | | % append(Primed,R,L). |
475 | | %:- assert_must_succeed(( b_read_write_info:add_dollar_zero(b(identifier(x),integer,[]),R), R = 'x$0')). |
476 | | %add_dollar_zero(TId,P) :- |
477 | | % get_texpr_id(TId,Id), |
478 | | % number_suffix(Id,0,P). |
479 | | |
480 | | :- use_module(tools_lists,[ord_member_nonvar_chk/2]). |
481 | | % remap reads of ID$0 to reads of ID |
482 | | remap_primed_ids([],_,_,[]). |
483 | | remap_primed_ids([ID0|T],SRenameList,LocalVars0,[ID|RT]) :- |
484 | | (ord_member_nonvar_chk(rename(ID0,ID),SRenameList) |
485 | | -> ord_nonmember(ID,LocalVars0) % only keep if not a local variable |
486 | | ; ID=ID0 |
487 | | ), |
488 | | !, |
489 | | remap_primed_ids(T,SRenameList,LocalVars0,RT). |
490 | | remap_primed_ids([_|T],SRenameList,LocalVars0,RT) :- |
491 | | remap_primed_ids(T,SRenameList,LocalVars0,RT). |
492 | | |
493 | | % compute read variables for becomes_such; remapping reads of ID$0 to ID |
494 | | find_read_vars_for_becomes_such(TIds,Body,LocalVars0,BMSuchReadVars) :- |
495 | | add_tvars_to_ord_list(LocalVars0,TIds,LocalVars1,_,_), % ignore reading new values; this does not correspond to reading a value in the current state |
496 | | % all Ids are already marked as accessed, any reference to Id$0 is a read of the old value; do not add Id$0 to the accessed variables |
497 | | get_texpr_ids(TIds,Names), |
498 | | maplist(add_dollar_zero,Names,RenameList), |
499 | | list_to_ord_set(RenameList,SRenameList), |
500 | | find_identifier_uses(Body,LocalVars1,ReadVars), |
501 | | remap_primed_ids(ReadVars,SRenameList,LocalVars0,BMSuchReadVars). |
502 | | |
503 | | :- use_module(tools,[number_suffix/3]). % $0 |
504 | | add_dollar_zero(Id,rename(P,Id)) :- |
505 | | number_suffix(Id,0,P). |
506 | | |
507 | | |
508 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
509 | | |
510 | | % READ-WRITE-INFO for OPERATIONS |
511 | | |
512 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
513 | | |
514 | | |
515 | | :- use_module(bmachine,[b_get_operation_normalized_read_write_info/3, b_get_machine_operation/4, |
516 | | b_is_operation_name/1, |
517 | | b_get_machine_variables/1, b_get_machine_constants/1, b_is_variable/1]). |
518 | | |
519 | | b_get_read_write(O,R,W) :- |
520 | | if(b_get_operation_normalized_read_write_info(O,R,W),true, |
521 | | (R,W)=('$all','$all')). % it used to be that in Event-B no read information was stored; all calls to b_get_operation_normalized_read_write_info failed; has been fixed |
522 | | |
523 | | b_get_machine_operation_with_local_paras(OpName,AllLocalParas,Body) :- |
524 | | b_get_machine_operation(OpName,Results,Parameters,Body), |
525 | | append(Parameters,Results,TP), |
526 | | get_texpr_ids(TP,TPIds), |
527 | | list_to_ord_set(TPIds,AllLocalParas). |
528 | | |
529 | | /* We distinguish between read variables in the guard and read variables in the event statement */ |
530 | | b_get_read_write_guard_action(Operation,ReadGuard,ReadAction,Read,Write) :- |
531 | | b_get_read_write(Operation,Read,Write), |
532 | | b_get_operation_read_guard_vars(Operation,false,ReadGuard,_Precise), |
533 | | b_get_machine_operation_with_local_paras(Operation,LocalParas,Body), |
534 | | get_texpr_expr(Body,RLEVENT), |
535 | | (RLEVENT = rlevent(_Name,_Section,_Stat,_Parameters,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_AbsEvents) -> |
536 | | % special code to deal with *all* guards/actions (also in abstractions) + not extract guards from actions |
537 | | % TO DO: maybe move this to get_guard/get_action (see below) ; or maybe provide parameter to choose |
538 | | % in some circumstances (Deadlock checking) it is sufficient to look at lowest refinement level |
539 | | % for LTSMin,... : we need info from all refinement levels and from theorems |
540 | | % TO DO: look at _Unmod |
541 | | findall(A1,(get_full_eventb_action(RLEVENT,AA),member(A1,AA)),A) |
542 | | ; get_action(Operation,A) -> true |
543 | | ; add_error(b_get_read_write_guard_action,'Could not get action for operation: ',Operation), fail |
544 | | ), |
545 | | (is_list(A) % in case of Event-B events the action block is a list of assignments |
546 | | -> find_identifier_uses_l(A,LocalParas,RActionVars) % TO DO: use get_accessed_vars ? |
547 | | ; get_accessed_vars(A,LocalParas,_,RActionVars) |
548 | | ), |
549 | | list_to_ord_set(RActionVars,RActionVars1), |
550 | | rw_ord_intersection(RActionVars1,Read,ReadAction). |
551 | | |
552 | | :- dynamic b_get_operation_read_guard_vars_cache/4. |
553 | | reset_b_read_write_info :- retractall(b_get_operation_read_guard_vars_cache(_,_,_,_)). |
554 | | |
555 | | :- use_module(eventhandling,[register_event_listener/3]). |
556 | | :- register_event_listener(reset_specification,reset_b_read_write_info, |
557 | | 'Reset Read-Write Operation Cache.'). |
558 | | :- register_event_listener(reset_prob,reset_b_read_write_info, |
559 | | 'Reset Read-Write Operation Cache.'). |
560 | | |
561 | | |
562 | | % if JustVariables is true we return just the variables |
563 | | b_get_operation_read_guard_vars(Operation,JustVariables,VarsResult,VarsPrecise) :- |
564 | | (var(Operation) -> b_is_operation_name(Operation) ; true), |
565 | | b_get_operation_read_guard_vars2(Operation,JustVariables,VarsResult,VarsPrecise). |
566 | | % this gets the variables/identifiers read in the guard of an operation |
567 | | % Note: this part will include parts of the guard that depend on the parameters |
568 | | b_get_operation_read_guard_vars2(Operation,JustVariables,VarsResult,VarsPrecise) :- |
569 | | b_get_operation_read_guard_vars_cache(Operation,JustVariables,R,P),!, |
570 | | VarsResult=R, VarsPrecise=P. |
571 | | b_get_operation_read_guard_vars2(Operation,JustVariables,VarsResult,VarsPrecise) :- |
572 | | b_get_machine_operation_with_local_paras(Operation,Paras,_), |
573 | | get_operation_guard(Operation,G,Precise), |
574 | | % RGuardVars can comprise also local variables by operations with parameters |
575 | | find_identifier_uses(G,Paras,RGuardVars), |
576 | | list_to_ord_set(RGuardVars,ReadGuard), |
577 | | (JustVariables=false |
578 | | -> Result = ReadGuard |
579 | | ; b_get_machine_variables(TVars),get_texpr_ids(TVars,Vars), |
580 | | list_to_ord_set(Vars,Variables), |
581 | | ord_intersection(ReadGuard,Variables,Result) |
582 | | ), |
583 | | assertz(b_get_operation_read_guard_vars_cache(Operation,JustVariables,Result,Precise)), |
584 | | VarsResult=Result, VarsPrecise=Precise. |
585 | | |
586 | | |
587 | | % show full guards |
588 | | tcltk_get_guards_for_ops(list(Res)) :- |
589 | | findall([Name,' GUARD ',GS, 'PRECISE', Precise], |
590 | | (get_operation_guard(Name,G,Precise), |
591 | | translate:translate_bexpression(G,GS)), Res). |
592 | | |
593 | | % show guards which do not depend on parameters and the rest (the Action) |
594 | | tcltk_get_parameter_free_guards_for_ops(list(Res)) :- |
595 | | findall([Name,' LTSMIN-GUARD ',GS, 'ACTION ',AS], |
596 | | (get_operation_propositional_guards(Name,Guards,A),conjunct_predicates(Guards,G), |
597 | | translate:translate_bexpression(G,GS), |
598 | | translate:translate_substitution(A,AS)), Res). |
599 | | |
600 | | get_operation_guard(Operation,G,Precise) :- |
601 | | b_get_machine_operation(Operation,_RR,_P,TBody), |
602 | | get_texpr_expr(TBody,Body), |
603 | | get_operation_guard_aux(Body,Operation,G,Precise). |
604 | | |
605 | | :- use_module(probsrc(b_state_model_check), [get_guard_and_precision/3]). |
606 | | get_operation_guard_aux(RLEVENT,_,G,Precision) :- |
607 | | RLEVENT = rlevent(_Name,_Section,_Status,_Parameters,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_AbsEvents), |
608 | | !, |
609 | | Precision = precise, % computation in Event-B is always precise, no while loops or sequences |
610 | | findall(G1,get_full_eventb_guard(RLEVENT,G1),Gs), |
611 | | conjunct_predicates(Gs,G). |
612 | | get_operation_guard_aux(_,Operation,G,Precise) :- get_guard_and_precision(Operation,G,Precise). |
613 | | |
614 | | |
615 | | % TO DO: we should move this code to b_state_model_check/predicate_debugger:get_operation_enabling_condition2 ? |
616 | | get_full_eventb_guard(rlevent(_Name,_Section,VariantStatus,_Parameters,Grd,Thms,_Act,_VWit,_PWit,_Unmod,AbsEvents),G) :- |
617 | | (G=Grd |
618 | | ; member(G,Thms) % this is relevant for LTS Min; but not for normal enabling analysis; |
619 | | % Note guard theorems are fully checked by interpreter |
620 | | ; b_operation_guards:get_variant_pred(VariantStatus,G) |
621 | | ; member(b(E,_,_),AbsEvents),get_full_eventb_guard(E,G)). |
622 | | get_full_eventb_action(rlevent(_Name,_Section,_Stat,_Parameters,_Grd,_Thm,Act,_VWit,_PWit,_Unmod,AbsEvents),A) :- |
623 | | (A=Act ; member(b(E,_,_),AbsEvents),get_full_eventb_action(E,A)). |
624 | | |
625 | | |
626 | | % Note: this is the LTSMin meaning of action (for LTSMin a guard depending on the parameter is part of the action) |
627 | | % Action will also contain parts of the guard that depend on parameters ! |
628 | | % This is important for independence |
629 | | % Example: CopyYY2XX(p) = PRE v>1 & p = yy THEN xx := p END --> Guard is #p.(p=yy) --> v>1 ; LTS Min Action is PRE p=yy THEN x := yy END; |
630 | | get_action(OpName,Action) :- get_operation_propositional_guards(OpName,_,Action). |
631 | | |
632 | | |
633 | | % we need just the variables that are read by the operation (constants will not be considered) |
634 | | b_get_read_write_vars(Operation,ReadGuardV,ReadActionV,ReadV,Write) :- |
635 | | b_get_read_write_vars_and_consts(false,Operation,ReadGuardV,ReadActionV,ReadV,Write). |
636 | | b_get_read_write_vars_and_consts(IncludeConstants,Operation,ReadGuardV,ReadActionV,ReadV,Write) :- |
637 | | b_get_read_write_guard_action(Operation,ReadGuard,ReadAction,Read,Write), |
638 | | b_get_machine_variables(TVars), |
639 | | (IncludeConstants==true |
640 | | -> b_get_machine_constants(TConsts), append(TConsts,TVars,TCV) % should we include get_global_identifiers ? |
641 | | ; TCV = TVars), |
642 | | get_texpr_ids(TCV,Vars), |
643 | | list_to_ord_set(Vars,Variables), |
644 | | ord_intersection(ReadGuard,Variables,ReadGuardV), |
645 | | ord_intersection(ReadAction,Variables,ReadActionV), |
646 | | ord_intersection(Read,Variables,ReadV). |
647 | | |
648 | | |
649 | | % ----------------------------------------------- |
650 | | % compute MAY/MUST write information (for LTSMin) |
651 | | % ----------------------------------------------- |
652 | | |
653 | | :- use_module(bsyntaxtree, [get_texpr_id/2, def_get_texpr_ids/2, is_truth/1, def_get_texpr_id/2]). |
654 | | |
655 | | % get read/write with may/must write info |
656 | | b_get_read_may_must_write(Operation,MustWriteV,MayWriteV) :- |
657 | | b_get_machine_operation(Operation,ReturnVars,_P,Body), |
658 | | b_get_read_write(Operation,_,WriteV), |
659 | | (is_eventb_event(Body) -> MayWriteV = [], |
660 | | WriteV = MustWriteV % in Event-B there are no conditions on the actions |
661 | | ; extract_must_write(Body,nested,MustWriteV1) -> |
662 | | % remove return values: they are not global variables written to |
663 | | def_get_texpr_ids(ReturnVars,RV),list_to_ord_set(RV,SRV), |
664 | | ord_subtract(MustWriteV1,SRV,MustWriteV), |
665 | | ord_subtract(WriteV,MustWriteV,MayWriteV) |
666 | | ; add_internal_error('Extraction of Must-Write failed: ',extract_must_write(Body,nested,_)), |
667 | | MustWriteV=[], MayWriteV=WriteV). |
668 | | /* |
669 | | b_get_read_may_must_write(Operation,ReadGuardV,ReadActionV,ReadV,MustWriteV,MayWriteV,WriteV) :- |
670 | | b_get_read_write_vars_and_consts(true,Operation,ReadGuardV,ReadActionV,ReadV,WriteV), |
671 | | b_get_machine_operation(Operation,ReturnVars,_P,Body), |
672 | | (is_eventb_event(Body) -> MayWriteV = [], MustWriteV=WriteV % in Event-B there are no conditions on the actions |
673 | | ; extract_must_write(Body,nested,MustWriteV1) -> |
674 | | % remove return values: they are not global variables written to |
675 | | def_get_texpr_ids(ReturnVars,RV),list_to_ord_set(RV,SRV), |
676 | | ord_subtract(MustWriteV1,SRV,MustWriteV), |
677 | | ord_subtract(WriteV,MustWriteV,MayWriteV) |
678 | | ; add_internal_error('Extraction of Must-Write failed: ',extract_must_write(Body,_)), |
679 | | MustWriteV=[], MayWriteV=WriteV). |
680 | | */ |
681 | | is_eventb_event(b(E,_,_)) :- |
682 | | E = rlevent(_Name,_Section,_Status,_Params,_Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents). |
683 | | |
684 | | % compute the variables that must be written by an operation if it is enabled |
685 | ? | extract_must_write(b(Sub,_,_),Nested,MV) :- extract_must_write_aux(Sub,Nested,MV),!. |
686 | | extract_must_write(O,N,MV) :- add_internal_error('Call failed: ',extract_must_write(O,N,MV)),MV=[]. |
687 | | |
688 | | |
689 | | %extract_must_write_aux(P,V) :- functor(P,F,N), print(ex_aux(F,N)),nl,fail. |
690 | | extract_must_write_aux(assign(LHS,_),_,V) :- maplist(get_id,LHS,Vars), list_to_ord_set(Vars,V). |
691 | | extract_must_write_aux(assign_single_id(TID,_),_,[ID]) :- get_id(TID,ID). |
692 | | extract_must_write_aux(becomes_such(LHS,_),_,V) :- maplist(get_id,LHS,Vars), list_to_ord_set(Vars,V). |
693 | | extract_must_write_aux(becomes_element_of(LHS,_),_,V) :- maplist(get_id,LHS,Vars), list_to_ord_set(Vars,V). |
694 | | extract_must_write_aux(precondition(_,TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV). |
695 | | extract_must_write_aux(assertion(_,TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV). |
696 | | extract_must_write_aux(any(_,_,TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV). |
697 | | extract_must_write_aux(let(_,_,TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV). |
698 | | extract_must_write_aux(lazy_let_subst(_,_,TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV). |
699 | | extract_must_write_aux(block(TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV). |
700 | | extract_must_write_aux(choice([A]),Nested,MV) :- !, extract_must_write(A,Nested,MV). |
701 | | extract_must_write_aux(choice([A|T]),Nested,MV) :- |
702 | | extract_must_write(A,Nested,MV1), extract_must_write_aux(choice(T),Nested,MV2), ord_intersection(MV1,MV2,MV). |
703 | | extract_must_write_aux(if([I]),Nested,MV) :- !, get_texpr_expr(I,if_elsif(Cond,TBody)), |
704 | | (is_truth(Cond) -> extract_must_write(TBody,Nested,MV) ; MV=[]). % we have ELSE skip and then write nothing |
705 | | extract_must_write_aux(if([I|T]),Nested,MV) :- get_texpr_expr(I,if_elsif(_,TBody)), |
706 | | extract_must_write(TBody,Nested,MV1), extract_must_write_aux(if(T),Nested,MV2), ord_intersection(MV1,MV2,MV). |
707 | | extract_must_write_aux(select([SW]),Nested,MV) :- !, |
708 | | get_texpr_expr(SW,select_when(_,TBody)),extract_must_write(TBody,Nested,MV). |
709 | | extract_must_write_aux(select([SW|T]),Nested,MV) :- |
710 | | get_texpr_expr(SW,select_when(_,TBody)), extract_must_write(TBody,Nested,MV1), |
711 | | extract_must_write_aux(select(T),Nested,MV2),ord_intersection(MV1,MV2,MV). |
712 | | extract_must_write_aux(select(T,Else),Nested,MV) :- |
713 | | extract_must_write(Else,Nested,MV1), |
714 | | extract_must_write_aux(select(T),Nested,MV2),ord_intersection(MV1,MV2,MV). |
715 | | extract_must_write_aux(case(_,[],Else),Nested,MV) :- extract_must_write(Else,Nested,MV). |
716 | | extract_must_write_aux(case(E,[C|T],Else),Nested,MV) :- |
717 | | get_texpr_expr(C,case_or(_,TBody)), |
718 | | extract_must_write(TBody,Nested,MV1), |
719 | | extract_must_write_aux(case(E,T,Else),Nested,MV2),ord_intersection(MV1,MV2,MV). |
720 | | extract_must_write_aux(parallel([A]),Nested,MV) :- !, extract_must_write(A,Nested,MV). |
721 | | extract_must_write_aux(parallel([A|T]),Nested,MV) :- |
722 | | extract_must_write(A,Nested,MV1), extract_must_write_aux(parallel(T),Nested,MV2), ord_union(MV1,MV2,MV). |
723 | | extract_must_write_aux(sequence(S),Nested,MV) :- !, extract_must_write_aux(parallel(S),Nested,MV). |
724 | | extract_must_write_aux(skip,_,[]). |
725 | | extract_must_write_aux(external_subst_call(_,_),_,[]). % assume there is no guarantee that something is written |
726 | | extract_must_write_aux(while(_,_,_,_),_,[]). % in case the condition is false, the loop is not entered |
727 | | extract_must_write_aux(var(Parameters,TBody),Nested,MV) :- |
728 | | def_get_texpr_ids(Parameters,IDs), |
729 | | list_to_ord_set(IDs,MV2), |
730 | | extract_must_write(TBody,Nested,MV1), |
731 | | ord_subtract(MV1,MV2,MV). |
732 | | extract_must_write_aux(operation_call(TOperation,Results,_),Nested,MustWriteV) :- |
733 | | maplist(get_id,Results,Vars), list_to_ord_set(Vars,WrittenResults), |
734 | | (Nested=not_nested -> MustWriteV=WrittenResults |
735 | | ; def_get_texpr_id(TOperation,op(Operation)), |
736 | | b_get_read_may_must_write(Operation,MustWriteVInner,_), %and ideally cache values |
737 | | ord_union(WrittenResults,MustWriteVInner,MustWriteV) |
738 | | ). |
739 | | extract_must_write_aux(Other,_,[]) :- |
740 | | add_message('Uncovered substitution for must_write computation: ',Other). |
741 | | |
742 | | get_id(b(function(A,_),_,_),ID) :- !, get_id(A,ID). |
743 | | get_id(TID,ID) :- get_texpr_id(TID,ID). |
744 | | |
745 | | % mainly used for LTS Min (uses LTSMin's definition of Action and (parameter-free) Guard): |
746 | | tcltk_read_write_matrix(list([list(['Operation','ReadsGuard','ReadsAction','MustWrite','MayWrite'])|Result])) :- |
747 | | findall(list([Operation,RG,RA,MustW,MayW]),b_get_read_may_must_write_for_ltsmin(Operation,RG,RA,MustW,MayW),Result). |
748 | | |
749 | | :- use_module(bsyntaxtree,[get_global_identifiers/1]). |
750 | | % obtains the read and written variables (constants, SETS and enumerated elements not included) |
751 | | % seperates the operations into parameter-independent guards and the rest, the Action |
752 | | :- use_module(b_operation_guards,[get_operation_propositional_guards/3]). |
753 | | :- use_module(probsrc(bmachine),[b_get_machine_operation_for_animation/6]). |
754 | | :- use_module(bmachine,[b_top_level_operation/1]). |
755 | | |
756 | | |
757 | | get_operation(Operation,Results,Paras) :- |
758 | | b_top_level_operation(Operation), |
759 | | b_get_machine_operation_for_animation(Operation,Results,Paras,_TB,_OT,true). |
760 | | |
761 | | b_get_read_may_must_write_for_ltsmin(Operation,ReadsGuard,ReadsAction,MustW,MayW) :- |
762 | | get_operation(Operation,Results,Paras), |
763 | | % LTSmin needs the constants in the read matrices; |
764 | | % if they are not included, it will transfer the uninitialised constants from the root state |
765 | | %b_get_machine_constants(TConsts), append(Paras,TConsts,TP), |
766 | | append(Results, Paras, ResultsAndParas), |
767 | | get_texpr_ids(ResultsAndParas,TPIds), |
768 | | get_global_identifiers(Global), |
769 | | append(TPIds,Global,PIDs),list_to_ord_set(PIDs,VarsToIgnore), % the VarsToIgnore should not be included in the matrix |
770 | | b_get_read_may_must_write(Operation,MustW,MayW), % we ignore the info about guards and actions: LTS Min has another definition of what a guard is than b_get_read_may_must_write |
771 | | get_operation_propositional_guards(Operation,Guards,RestBody), % obtain LTSMin guards, which are independent of the parameters |
772 | | get_accessed_vars(RestBody,VarsToIgnore,_Modified,ReadsAction), % this computes the ReadsAction the LTSMin way |
773 | | %format('READS ACTION for ~w ~n ~w~n',[Operation,ReadsAction]), |
774 | | conjunct_predicates(Guards,G), |
775 | | find_identifier_uses(G,VarsToIgnore,ReadsGuard). |
776 | | % (op_has_parameters(Operation) |
777 | | % -> ReadsAction = FullReads % guards on parameters may be projected away; leading to implicit reads in actions |
778 | | % % TO DO: convert operations into normal form; until this is done: simply return full reads |
779 | | % ; ReadsAction = RA). |
780 | | |
781 | | %op_has_parameters(OpName) :- |
782 | | % b_get_machine_operation_for_animation(OpName,_Results,Paras,_TB,_OT,true), |
783 | | % Paras = [_|_]. |
784 | | |
785 | | |
786 | | rw_ord_intersection('$all',B,R) :- !,R=B. |
787 | | rw_ord_intersection(A,'$all',R) :- !,R=A. |
788 | | rw_ord_intersection(A,B,R) :- ord_intersection(A,B,R). |
789 | | |
790 | | |
791 | | % compute the variables that are written by at least one operation: |
792 | | b_get_written_variables(WrittenVariables) :- |
793 | | findall(Var, |
794 | | (b_top_level_operation(Operation), |
795 | | %get_operation(Operation,_Results,_Paras), |
796 | | b_get_read_write(Operation,_,WriteV), |
797 | | member(Var,WriteV) |
798 | | ),Vars), |
799 | | sort(Vars,WrittenVariables). |
800 | | |
801 | | written_by_not_top_level_operation(Variable,Operation) :- |
802 | | b_get_read_write(Operation,_,WriteV), |
803 | | \+ b_top_level_operation(Operation), |
804 | | member(Variable,WriteV). |
805 | | |
806 | | % compute the variables that are read by at least one operation: |
807 | | b_get_read_variables(ReadVariables) :- |
808 | | findall(Var, |
809 | | (b_top_level_operation(Operation), |
810 | | b_get_read_write(Operation,ReadV,_), |
811 | | member(Var,ReadV), |
812 | | b_is_variable(Var) |
813 | | ),Vars), |
814 | | sort(Vars,ReadVariables). |
815 | | % compute the variables that are read by at least one operation: |
816 | | b_get_read_guard_variables(ReadVariables) :- |
817 | | findall(Var, |
818 | | (b_top_level_operation(Operation), |
819 | | b_get_operation_read_guard_vars(Operation,true,ReadV,_), |
820 | | member(Var,ReadV), |
821 | | b_is_variable(Var) |
822 | | ),Vars), |
823 | | sort(Vars,ReadVariables). |
824 | | |
825 | | % cannot be run in bmachine_static_checks as operations are not yet precompiled |
826 | | check_all_variables_written :- |
827 | | b_get_written_variables(WrittenVariables), |
828 | | b_get_machine_variables(TVars), |
829 | | member(TVar,TVars), |
830 | | get_texpr_id(TVar,Var), |
831 | | \+ ord_member(Var,WrittenVariables), |
832 | | (written_by_not_top_level_operation(Var,Op2) |
833 | | -> ajoin(['Variable is written by no top-level operation (but is written by ',Op2,'): '],Msg), |
834 | | add_warning(check_all_variables_written,Msg,Var,TVar) |
835 | | ; add_warning(check_all_variables_written,'Variable is written by no operation (consider defining it as a constant): ',Var,TVar) |
836 | | ), |
837 | | fail. |
838 | | check_all_variables_written. |
839 | | |
840 | | % compute a matrix which shows for variables who reads and modifies them: |
841 | | tcltk_variable_read_write_matrix(Warn,list([list(['Variable','Read by','Written by'])|Result])) :- |
842 | | findall(list([Variable,Reads,Writes]), |
843 | | get_read_write_ops_for_variable(Variable,Reads,Writes),Result), |
844 | | (Warn=no_check -> true ; check_all_variables_written). |
845 | | |
846 | | get_read_write_ops_for_variable(Var,ReadOps,WriteOps) :- |
847 | | b_get_machine_variables(TVars), member(TVar,TVars), get_texpr_id(TVar,Var), |
848 | | findall(Op,(b_top_level_operation(Op),b_get_read_write(Op,Reads,_),ord_member(Var,Reads)),ReadOps), |
849 | | findall(Op,(b_top_level_operation(Op),b_get_read_write(Op,_,Writes),ord_member(Var,Writes)),WriteOps). |
850 | | |
851 | | |
852 | | % -------------------- READ/WRITE VARIABLE ANALYSIS GRAPH ------------------------- |
853 | | |
854 | | :- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/3]). |
855 | | tcltk_dot_variable_modification_analysis(File) :- |
856 | | gen_dot_graph(File,var_op_node_predicate,var_mod_pred). |
857 | | |
858 | | |
859 | | :- use_module(tools_strings,[ajoin/2]). |
860 | | :- use_module(preferences,[get_preference/2]). |
861 | | var_op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :- |
862 | | b_get_written_variables(WrittenVariables), |
863 | | b_get_read_variables(ReadVariables), |
864 | | b_get_read_guard_variables(ReadGrdVariables), |
865 | | SubGraph=none, |
866 | | Color='RoyalBlue4', |
867 | | b_is_variable(NodeID), |
868 | | (ord_member(NodeID,ReadGrdVariables) |
869 | | -> Style=none |
870 | | ; get_preference(dot_var_mod_hide_only_written,false), |
871 | | Style=dotted |
872 | | ), |
873 | | (\+ ord_member(NodeID,WrittenVariables) |
874 | | -> Shape=invtrapezium, ajoin([NodeID,'\\n (NOT WRITTEN)'],NodeDesc) |
875 | | ; \+ ord_member(NodeID,ReadVariables) |
876 | | -> Shape=trapezium, ajoin([NodeID,'\\n (NOT READ)'],NodeDesc) |
877 | | ; Shape=box, NodeDesc=NodeID |
878 | | ). |
879 | | var_op_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color) :- |
880 | | b_top_level_operation(NodeID), |
881 | | %b_get_read_write(NodeID,_,Writes), dif(Writes,[]), % do not show query operations |
882 | | SubGraph=none, Shape=rect, Style='filled,rounded', |
883 | | NodeDesc=NodeID, Color=gray90. |
884 | | |
885 | | |
886 | | :- use_module(translate,[translate_bexpression_with_limit/3]). |
887 | | var_mod_pred(OpNodeID,Label,SuccID,Color,Style) :- Color=red4, Style=solid, % writes variable |
888 | | b_get_read_guard_variables(ReadVariables), |
889 | | b_get_read_may_must_write(OpNodeID,MustWrite,_), |
890 | | member(SuccID,MustWrite), |
891 | | (get_preference(dot_var_mod_hide_only_written,true) |
892 | | -> ord_member(SuccID,ReadVariables) ; true), |
893 | | (get_assignment_value(OpNodeID,SuccID,Val) |
894 | | -> translate_bexpression_with_limit(Val,30,VS), |
895 | | ajoin([':= \\n',VS],Label) |
896 | | ; Label = writes). |
897 | | var_mod_pred(OpNodeID,Label,SuccID,Color,Style) :- Color=goldenrod, Label='may write',Style=dotted, |
898 | | b_get_read_guard_variables(ReadVariables), |
899 | | b_get_read_may_must_write(OpNodeID,_,MayWrite), |
900 | | member(SuccID,MayWrite), |
901 | | (get_preference(dot_var_mod_hide_only_written,true) |
902 | | -> ord_member(SuccID,ReadVariables) ; true). |
903 | | var_mod_pred(NodeID,Label,SuccOpID,Color,Style) :- Color=azure4, Style=solid, % reads variable |
904 | | %b_get_read_write(SuccOpID,Reads,_), |
905 | | %b_get_read_may_must_write_for_ltsmin(SuccOpID,ReadsGuard,_,_,_), |
906 | | b_get_operation_read_guard_vars(SuccOpID,true,ReadsGuard,_), |
907 | | member(NodeID,ReadsGuard), |
908 | | (get_decisive_predicate_from_guard(SuccOpID,NodeID,_Pred,Op,Val) |
909 | | -> translate_bexpression_with_limit(Val,30,VS), |
910 | | ajoin([Op,'\\n',VS],Label) |
911 | | ; Label = reads). |
912 | | var_mod_pred(NodeID,Label,SuccOpID,Color,Style) :- Color=azure3, Style=solid, Label = reads_body, |
913 | | b_get_read_variables(ReadVariables), |
914 | | b_get_read_write(SuccOpID,ReadV,_), |
915 | | b_get_operation_read_guard_vars(SuccOpID,true,ReadsGuard,_), |
916 | | member(NodeID,ReadV), nonmember(NodeID,ReadsGuard), member(NodeID,ReadVariables). |
917 | | |
918 | | % try to find relevant, decisive checks from guard |
919 | | get_decisive_predicate_from_guard(Operation,Variable,TPred,Op,TVal) :- |
920 | | get_operation_guard(Operation,G,_), |
921 | | member_in_conjunction(TPred,G), |
922 | | get_texpr_expr(TPred,Pred), |
923 | | is_decisive(Pred,Variable,Op,TVal). |
924 | | |
925 | | is_decisive(equal(TID,VAL),Variable,'=',VAL) :- get_texpr_id(TID,Variable), simple_val(VAL). |
926 | | is_decisive(equal(VAL,TID),Variable,'=',VAL) :- get_texpr_id(TID,Variable), simple_val(VAL). |
927 | | % TO DO: other checks ? not_equal, greater, ... |
928 | | simple_val(b(V,_,_)) :- simple_val2(V). |
929 | | simple_val2(empty_set). |
930 | | simple_val2(empty_sequence). |
931 | | simple_val2(boolean_true). |
932 | | simple_val2(boolean_false). |
933 | | simple_val2(integer(_)). |
934 | | simple_val2(string(_)). |
935 | | simple_val2(max_int). |
936 | | simple_val2(min_int). |
937 | | simple_val2(value(_)). |
938 | | |
939 | | get_assignment_value(Operation,Variable,Val) :- |
940 | | get_action(Operation,TAction), |
941 | | get_texpr_expr(TAction,Action), |
942 | | get_assign_val(Action,Variable,Val). |
943 | | |
944 | | get_assign_val(assign_single_id(TID,Val),ID,Val) :- |
945 | | get_texpr_id(TID,ID),!, |
946 | | (simple_val(Val) -> true ; simple_modification(Val,ID)). |
947 | | get_assign_val(any(_,_,TBody),Var,Val) :- get_texpr_expr(TBody,Body), get_assign_val(Body,Var,Val). |
948 | | get_assign_val(select([b(select_when(_,TBody),_,_)]),Var,Val) :- |
949 | | get_texpr_expr(TBody,Body), get_assign_val(Body,Var,Val). |
950 | | get_assign_val(parallel(Bodies),Var,Val) :- member(TBody,Bodies), |
951 | | get_texpr_expr(TBody,Body), get_assign_val(Body,Var,Val). |
952 | | % TO DO: sequence, ... |
953 | | |
954 | | simple_modification(TExpr,Var) :- get_texpr_expr(TExpr,Expr), |
955 | | simple_modification_aux(Expr,Var). |
956 | | simple_modification_aux(add(A,B),Var) :- simple_binop(A,B,Var). |
957 | | simple_modification_aux(minus(A,B),Var) :- simple_binop(A,B,Var). |
958 | | simple_modification_aux(multiplication(A,B),Var) :- simple_binop(A,B,Var). |
959 | | |
960 | | simple_binop(TID,Val,Var) :- get_texpr_id(TID,Var), simple_val(Val). |
961 | | simple_binop(Val,TID,Var) :- get_texpr_id(TID,Var), simple_val(Val). |
962 | | |