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 |