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