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