1 package edu.uci.eecs.specCompiler.codeGenerator;
3 import java.util.ArrayList;
4 import java.util.HashMap;
5 import java.util.HashSet;
7 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
8 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
9 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
10 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
11 import edu.uci.eecs.specCompiler.specExtraction.Construct;
12 import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
13 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
14 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
15 import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
16 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
18 public class SemanticsChecker {
19 public final ArrayList<Construct> constructs;
20 public final HashMap<String, Construct> CPLabel2Construct;
21 public final HashMap<String, Construct> potentialCPLabel2Construct;
22 public final HashMap<String, Construct> interfaceName2Construct;
23 public final HashMap<String, Construct> interfaceName2DefineConstruct;
24 public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
25 public final HashSet<DefineVar> defineVars;
27 public final HashMap<String, Integer> interface2Num;
28 public final HashMap<String, Integer> hbLabel2Num;
29 public final HashMap<String, Integer> commitPointLabel2Num;
31 private HashMap<String, String> options;
32 private HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions;
33 private Construct entryPointConstruct;
35 private int _interfaceNum;
36 private int _hbLabelNum;
37 private int _commitPointNum;
39 public SemanticsChecker(ArrayList<Construct> constructs) {
40 this.constructs = constructs;
41 this.CPLabel2Construct = new HashMap<String, Construct>();
42 this.potentialCPLabel2Construct = new HashMap<String, Construct>();
43 this.interfaceName2Construct = new HashMap<String, Construct>();
44 this.interfaceName2DefineConstruct = new HashMap<String, Construct>();
45 this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
46 this.defineVars = new HashSet<DefineVar>();
47 this.entryPointConstruct = null;
49 this.interface2Num = new HashMap<String, Integer>();
50 this.hbLabel2Num = new HashMap<String, Integer>();
51 // Immediately init the true HB-condition to be 0
52 hbLabel2Num.put("", 0);
54 this.commitPointLabel2Num = new HashMap<String, Integer>();
61 public HashMap<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
62 return this.hbConditions;
65 public String getOption(String key) {
66 return options.get(key);
69 private void checkHBLabelConsistency(ConditionalInterface inst)
70 throws SemanticsCheckerException {
71 String interfaceName = inst.interfaceName, label = inst.hbConditionLabel;
72 if (!interfaceName2Construct.containsKey(interfaceName)) {
73 throw new SemanticsCheckerException(
74 "In global construct, no interface \"" + interfaceName
76 } else if (!label.equals("")) {
77 InterfaceConstruct iConstruct = (InterfaceConstruct) interfaceName2Construct
79 if (!iConstruct.hbConditions.containsKey(label)) {
80 throw new SemanticsCheckerException("Interface "
81 + interfaceName + " doesn't contain HB_codition: "
85 // No HB condition label can duplicate!
86 if (hbLabel2Num.containsKey(label)) {
87 throw new SemanticsCheckerException("Happens-before label: "
88 + label + " duplicates!");
91 // Number the HB-condition label
92 hbLabel2Num.put(label, _hbLabelNum++);
96 private void checkLabelDuplication(Construct construct, String label)
97 throws SemanticsCheckerException {
98 if (potentialCPLabel2Construct.containsKey(label)
99 || CPLabel2Construct.containsKey(label))
100 throw new SemanticsCheckerException("In construct: " + construct
101 + "\"" + label + "\" has duplication.");
104 private void checkOptions() throws SemanticsCheckerException {
105 // FIXME: We don't have any check here
108 private void postCheck() throws SemanticsCheckerException {
109 // This is a C program, must provide the entry point
110 if (getOption("LANG").equals("C") && entryPointConstruct == null) {
111 throw new SemanticsCheckerException(
112 "C program must provide the entry point!");
115 // Check if interface define construct labels are correct
116 for (String name : interfaceName2DefineConstruct.keySet()) {
117 if (!interfaceName2Construct.containsKey(name)) {
118 throw new SemanticsCheckerException(
119 "Label \"" + name + "\" does not have interface declaration!");
124 public void check() throws SemanticsCheckerException {
125 boolean hasGlobalConstruct = false;
126 // First grab the information from the interface
127 for (int i = 0; i < constructs.size(); i++) {
128 Construct inst = constructs.get(i);
129 if (inst instanceof InterfaceConstruct) {
130 InterfaceConstruct iConstruct = (InterfaceConstruct) inst;
131 if (interfaceName2Construct.containsKey(iConstruct.name)) {
132 throw new SemanticsCheckerException("Interface name: "
133 + iConstruct.name + " duplicates!");
135 // Number the interface label
136 interface2Num.put(iConstruct.name, _interfaceNum++);
138 interfaceName2Construct.put(iConstruct.name, constructs.get(i));
139 for (int j = 0; j < iConstruct.action.defineVars.size(); j++) {
140 DefineVar var = iConstruct.action.defineVars.get(j);
141 var.renameVarName("__" + iConstruct.name + "_"
142 + var.varName + "__");
145 for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
146 String label = iConstruct.commitPointSet.get(j);
147 if (!CPLabel2InterfaceConstruct.containsKey(label)) {
148 CPLabel2InterfaceConstruct.put(label,
149 new ArrayList<InterfaceConstruct>());
151 CPLabel2InterfaceConstruct.get(label).add(iConstruct);
157 for (int i = 0; i < constructs.size(); i++) {
158 Construct construct = constructs.get(i);
159 if (construct instanceof GlobalConstruct) {
160 GlobalConstruct theConstruct = (GlobalConstruct) construct;
161 if (!hasGlobalConstruct)
162 hasGlobalConstruct = true;
164 throw new SemanticsCheckerException(
165 "More than one global construct!");
167 // Record the options and check them
168 options = theConstruct.options;
170 // Record the HB conditions and check it
171 hbConditions = theConstruct.hbRelations;
172 for (ConditionalInterface left : hbConditions.keySet()) {
173 HashSet<ConditionalInterface> set = hbConditions.get(left);
174 checkHBLabelConsistency(left);
176 for (ConditionalInterface right : set) {
177 checkHBLabelConsistency(right);
180 } else if (construct instanceof PotentialCPDefineConstruct) {
181 PotentialCPDefineConstruct theConstruct = (PotentialCPDefineConstruct) construct;
182 label = theConstruct.label;
183 checkLabelDuplication(construct, label);
184 // Number the commit_point label
185 commitPointLabel2Num.put(label, _commitPointNum++);
187 potentialCPLabel2Construct.put(label, construct);
188 } else if (construct instanceof CPDefineCheckConstruct) {
189 CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct;
190 label = theConstruct.label;
191 checkLabelDuplication(construct, label);
192 // Number the commit_point label
193 commitPointLabel2Num.put(label, _commitPointNum++);
195 CPLabel2Construct.put(label, construct);
196 } else if (construct instanceof CPDefineConstruct) {
197 CPDefineConstruct theConstruct = (CPDefineConstruct) construct;
198 label = theConstruct.label;
199 checkLabelDuplication(construct, label);
200 // Number the commit_point label
201 commitPointLabel2Num.put(label, _commitPointNum++);
203 CPLabel2Construct.put(label, construct);
204 } else if (construct instanceof EntryPointConstruct) {
205 if (entryPointConstruct != null) {
206 throw new SemanticsCheckerException(
207 "More than one entry point!");
209 entryPointConstruct = construct;
210 } else if (construct instanceof InterfaceDefineConstruct) {
211 InterfaceDefineConstruct theConstruct = (InterfaceDefineConstruct) construct;
212 String name = theConstruct.name;
213 if (interfaceName2DefineConstruct.containsKey(name)) {
214 throw new SemanticsCheckerException(
215 "Interface define label duplicates!");
217 interfaceName2DefineConstruct.put(name, construct);
222 public String toString() {
223 StringBuilder sb = new StringBuilder();
224 if (entryPointConstruct == null) {
225 sb.append("Entry point is not specified!");
227 sb.append("@Entry_point:\n" + entryPointConstruct);
230 sb.append("Interface name 2 Construct:\n");
231 for (String interfaceName : interfaceName2Construct.keySet()) {
232 sb.append(interfaceName + "\t"
233 + interfaceName2Construct.get(interfaceName) + "\n");
236 sb.append("Interface name 2 define construct:\n");
237 for (String interfaceName : interfaceName2DefineConstruct.keySet()) {
238 sb.append(interfaceName + "\t"
239 + interfaceName2DefineConstruct.get(interfaceName) + "\n");
242 sb.append("Potential commit point label 2 Construct:\n");
243 for (String label : potentialCPLabel2Construct.keySet()) {
244 sb.append(label + "\t" + potentialCPLabel2Construct.get(label)
248 sb.append("Commit point label 2 Construct:\n");
249 for (String label : CPLabel2Construct.keySet()) {
250 sb.append(label + "\t" + CPLabel2Construct.get(label) + "\n");
252 return sb.toString();