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