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