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