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