1		% (c) 2009-2022 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(static_enabling_analysis,[
6		%static_activation_dependent/2,
7		static_cannot_enable/2,
8		vars_ord_intersect/2
9		]).
10
11		:- use_module(probsrc(module_information),[module_info/2]).
12		:- module_info(group,cbc).
13		:- module_info(description,'This module computes static enabling infos for B operations, without using the constraint solver.').
14
15		:- use_module(probsrc(debug), [debug_format/3]).
16		:- use_module(probsrc(bmachine),[b_top_level_operation/1]).
17		:- use_module(probsrc(b_read_write_info),
18		[b_get_read_write/3, b_get_operation_read_guard_vars/4]).
19
20		% -------------------- BINARY STATIC ANALYSIS -------------------------
21
22		% certain static analyses used by CBC Test case generation
23
24		% check if OpName1 can influence the truth value of the guard of OpName2 by looking at read/write info
25		%static_activation_dependent(OpName1,OpName2) :- static_activation_dependence(OpName1,OpName2,dependent).
26
27		% true when OpName1 cannot enable a previously disabled OpName2
28		static_cannot_enable(OpName1,OpName2) :-
29		static_activation_dependence(OpName1,OpName2,Res),
30		Res \= dependent. % activation_independent or independent
31
32		:- dynamic static_activation_dependence_cache/3.
33		static_activation_dependence(OpName1,OpName2,Res) :-
34		static_activation_dependence_cache(OpName1,OpName2,Cached),!,
35		Res=Cached.
36		static_activation_dependence(OpName1,OpName2,Res) :-
37		b_top_level_operation(OpName1),
38		b_get_read_write(OpName1,_,Writes1),
39		b_top_level_operation(OpName2),
40		b_get_operation_read_guard_vars(OpName2,true,GuardReads2,Precise),
41		(vars_ord_intersect(Writes1,GuardReads2)
42		-> Cached = dependent % OpName1 could enable or disable OpName2
43		; %print(indep(OpName1,Writes1,OpName2,GuardReads2)),nl,
44		b_get_read_write(OpName2,Reads2,_Writes2),
45		(vars_ord_intersect(Writes1,Reads2)
46		-> (Precise==precise
47		-> Cached = activation_independent % OpName1 cannot enable or disable OpName2, but can influence effect
48		; Cached = dependent % Computation of GuardReads2 was not precise (while loops, ... in operation)
49		)
50		; Cached = independent % but order could still matter; for this we would need to look at Writes2
51		)
52		),
53		debug_format(19,'Computed static dependence ~w -> ~w : ~w~n',[OpName1,OpName2,Cached]),
54		assertz(static_activation_dependence_cache(OpName1,OpName2,Cached)),
55		Res=Cached.
56
57
58		:- use_module(library(ordsets),[ord_intersect/2]).
59		% a version of ord_intersect(ion) which deals with the '$all' term
60		vars_ord_intersect('$all',_) :- !.
61		vars_ord_intersect(_,'$all') :- !.
62		vars_ord_intersect(A,B) :- ord_intersect(A,B).
63
64
65
66		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
67		:- register_event_listener(specification_initialised,reset_static_enabling_analysis,
68		'Initialise module static_enabling analysis.').
69
70		reset_static_enabling_analysis :-
71		retractall(static_activation_dependence_cache(_,_,_)).
72