Fixed inteferes bug, improved precision of other analysis to allow
[repair.git] / Repair / RepairCompiler / MCC / IR / ModelRuleDependence.java
1 package MCC.IR;
2 import MCC.State;
3 import java.util.*;
4
5 class ModelRuleDependence {
6     State state;
7     HashSet nodes;
8     HashMap ruletonode, nodetorule;
9     // Stores references to negated edges
10     HashSet negatededges;
11     GraphNode.SCC scc;
12     HashMap sccCache;
13
14     private final int NODEPENDENCY=0;
15     private final int NORMDEPENDENCY=1;
16     private final int NEGDEPENDENCY=2;
17     
18     private ModelRuleDependence(State state) {
19         this.state=state;
20         this.nodes=new HashSet();
21         this.ruletonode=new HashMap();
22         this.nodetorule=new HashMap();
23         this.negatededges=new HashSet();
24         this.sccCache=new HashMap();
25     }
26     
27     public static ModelRuleDependence doAnalysis(State state) {
28         ModelRuleDependence mrd=new ModelRuleDependence(state);
29         mrd.generateNodes();
30         mrd.generateEdges();
31         mrd.scc=GraphNode.DFS.computeSCC(mrd.nodes);
32         if (mrd.checkForNegatedDependences())
33             throw new Error("Negated Dependence");
34         return mrd;
35     }
36
37     public int numSCC() {
38         return scc.numSCC();
39     }
40
41     /** Gives strongly connected components in reverse topological
42      * order */
43     public Set getSCC(int i) {
44         Integer in=new Integer(i);
45         if (sccCache.containsKey(in))
46             return (Set) sccCache.get(in);
47         Set nodescc=scc.getSCC(i);
48         HashSet rulescc=new HashSet();
49         for (Iterator nodeit=nodescc.iterator();nodeit.hasNext();) {
50             GraphNode gn=(GraphNode) nodeit.next();
51             Rule r=(Rule)nodetorule.get(gn);
52             rulescc.add(r);
53         }
54         sccCache.put(in,rulescc);
55         return rulescc;
56     }
57
58     public boolean hasCycle(Rule r) {
59         return hasCycle(getComponent(r));
60     }
61
62     public boolean hasCycle(int i) {
63         return scc.hasCycle(i);
64     }
65
66     public int getComponent(Rule r) {
67         return scc.getComponent((GraphNode)ruletonode.get(r));
68     }
69
70     /** Returns true if there are any negated dependence cycles, false
71      * otherwise. */
72     private boolean checkForNegatedDependences() {
73         for(Iterator it=negatededges.iterator();it.hasNext();) {
74             GraphNode.Edge e=(GraphNode.Edge)it.next();
75             int scc1=scc.getComponent(e.getSource());
76             int scc2=scc.getComponent(e.getTarget());
77             if (scc1==scc2)
78                 return true;
79         }
80         return false;
81     }
82
83     /** Build mapping between nodes and rules */
84     private void generateNodes() {
85         for(int i=0;i<state.vRules.size();i++) {
86             GraphNode gn=new GraphNode("Rule"+i);
87             ruletonode.put(state.vRules.get(i),gn);
88             nodetorule.put(gn,state.vRules.get(i));
89             nodes.add(gn);
90         }
91     }
92     
93     /** Generate edges between rule nodes */
94     private void generateEdges() {
95         for(int i=0;i<state.vRules.size();i++) {
96             for(int j=0;j<state.vRules.size();j++) {
97                 Rule r1=(Rule)state.vRules.get(i);
98                 Rule r2=(Rule)state.vRules.get(j);
99                 generateEdge(r1,r2);
100             }
101         }
102     }
103
104     private void generateEdge(Rule r1,Rule r2) {
105         Descriptor d=(Descriptor) r1.getInclusion().getTargetDescriptors().iterator().next();
106         int dep=checkBody(d,r2.getDNFGuardExpr());
107         if (dep==NODEPENDENCY) {
108             SetDescriptor bsd=null;
109             if (d instanceof SetDescriptor) {
110                 SetInclusion si=(SetInclusion)r1.getInclusion();
111                 if (si.getExpr() instanceof VarExpr) {
112                     VarDescriptor vd=((VarExpr)si.getExpr()).getVar();
113                     bsd=vd.getSet();
114                 }
115             }
116             dep=checkQuantifiers(bsd,d,r2);
117         }
118         if (dep==NODEPENDENCY)
119             return;
120         GraphNode gn1=(GraphNode) ruletonode.get(r1);
121         GraphNode gn2=(GraphNode) ruletonode.get(r2);
122         GraphNode.Edge edge=new GraphNode.Edge("dependency",gn2);
123         gn1.addEdge(edge);
124         if (dep==NEGDEPENDENCY)
125             negatededges.add(edge);
126     }
127
128     private int checkBody(Descriptor d, DNFRule drule) {
129         boolean dependency=false;
130         for(int i=0;i<drule.size();i++) {
131             RuleConjunction rconj=drule.get(i);
132             for(int j=0;j<rconj.size();j++){ 
133                 DNFExpr dexpr=rconj.get(j);
134                 Expr e=dexpr.getExpr();
135                 if (e.usesDescriptor(d)) {
136                     boolean negated=dexpr.getNegation();
137                     if (negated)
138                         return NEGDEPENDENCY;
139                     else
140                         dependency=true;
141                 }
142             }
143         }
144         if (dependency)
145             return NORMDEPENDENCY;
146         else 
147             return NODEPENDENCY;
148     }
149
150     private int checkQuantifiers(SetDescriptor bsd, Descriptor d, Quantifiers qs) {
151         for (int i=0;i<qs.numQuantifiers();i++) {
152             Quantifier q=qs.getQuantifier(i);
153             if (q instanceof SetQuantifier&&
154                 d instanceof SetDescriptor) {
155                 SetQuantifier sq=(SetQuantifier)q;
156                 SetDescriptor sd=(SetDescriptor)d;
157                 if (sq.getSet().isSubset(sd)&&
158                     ((bsd==null)||!bsd.isSubset(sq.getSet())))
159                     return NORMDEPENDENCY;
160             } else if (q.getRequiredDescriptors().contains(d))
161                 return NORMDEPENDENCY;
162         }
163         return NODEPENDENCY;
164     }
165 }