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