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;
17 import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
19 public class SemanticsChecker {
20 public final ArrayList<SpecConstruct> constructs;
21 public final HashMap<String, SpecConstruct> CPLabel2Construct;
22 public final HashMap<String, SpecConstruct> potentialCPLabel2Construct;
23 public final HashMap<String, SpecConstruct> interfaceName2Construct;
24 public final HashMap<String, SpecConstruct> interfaceName2DefineConstruct;
25 public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
26 public final HashSet<DefineVar> defineVars;
28 public final HashMap<String, Integer> interface2Num;
29 public final HashMap<String, Integer> hbLabel2Num;
30 public final HashMap<String, Integer> commitPointLabel2Num;
32 private HashMap<String, String> options;
33 private HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions;
34 private SpecConstruct entryPointConstruct;
36 private int _interfaceNum;
37 private int _hbLabelNum;
38 private int _commitPointNum;
40 public SemanticsChecker(ArrayList<SpecConstruct> constructs) {
41 this.constructs = constructs;
42 this.CPLabel2Construct = new HashMap<String, SpecConstruct>();
43 this.potentialCPLabel2Construct = new HashMap<String, SpecConstruct>();
44 this.interfaceName2Construct = new HashMap<String, SpecConstruct>();
45 this.interfaceName2DefineConstruct = new HashMap<String, SpecConstruct>();
46 this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
47 this.defineVars = new HashSet<DefineVar>();
48 this.entryPointConstruct = null;
50 this.interface2Num = new HashMap<String, Integer>();
51 this.hbLabel2Num = new HashMap<String, Integer>();
52 // Immediately init the true HB-condition to be 0
53 hbLabel2Num.put("", 0);
55 this.commitPointLabel2Num = new HashMap<String, Integer>();
62 public HashMap<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
63 return this.hbConditions;
66 public String getOption(String key) {
67 return options.get(key);
70 private void checkHBLabelConsistency(ConditionalInterface inst)
71 throws SemanticsCheckerException {
72 String interfaceName = inst.interfaceName, label = inst.hbConditionLabel;
73 if (!interfaceName2Construct.containsKey(interfaceName)) {
74 throw new SemanticsCheckerException(
75 "In global construct, no interface \"" + interfaceName
77 } else if (!label.equals("")) {
78 InterfaceConstruct iConstruct = (InterfaceConstruct) interfaceName2Construct
79 .get(interfaceName).construct;
80 if (!iConstruct.hbConditions.containsKey(label)) {
81 throw new SemanticsCheckerException("Interface "
82 + interfaceName + " doesn't contain HB_codition: "
86 // No HB condition label can duplicate!
87 if (hbLabel2Num.containsKey(label)) {
88 throw new SemanticsCheckerException("Happens-before label: "
89 + label + " duplicates!");
92 // Number the HB-condition label
93 hbLabel2Num.put(label, _hbLabelNum++);
97 private void checkLabelDuplication(Construct construct, String label)
98 throws SemanticsCheckerException {
99 if (potentialCPLabel2Construct.containsKey(label)
100 || CPLabel2Construct.containsKey(label))
101 throw new SemanticsCheckerException("In construct: " + construct
102 + "\"" + label + "\" has duplication.");
105 private void checkOptions() throws SemanticsCheckerException {
106 // FIXME: We don't have any check here
109 private void postCheck() throws SemanticsCheckerException {
110 // This is a C program, must provide the entry point
111 if (getOption("LANG").equals("C") && entryPointConstruct == null) {
112 throw new SemanticsCheckerException(
113 "C program must provide the entry point!");
116 // Check if interface define construct labels are correct
117 for (String name : interfaceName2DefineConstruct.keySet()) {
118 if (!interfaceName2Construct.containsKey(name)) {
119 throw new SemanticsCheckerException(
120 "Label \"" + name + "\" does not have interface declaration!");
125 public void check() throws SemanticsCheckerException {
126 boolean hasGlobalConstruct = false;
127 // First grab the information from the interface
128 for (int i = 0; i < constructs.size(); i++) {
129 Construct inst = constructs.get(i).construct;
130 if (inst instanceof InterfaceConstruct) {
131 InterfaceConstruct iConstruct = (InterfaceConstruct) inst;
132 if (interfaceName2Construct.containsKey(iConstruct.name)) {
133 throw new SemanticsCheckerException("Interface name: "
134 + iConstruct.name + " duplicates!");
136 // Number the interface label
137 interface2Num.put(iConstruct.name, _interfaceNum++);
139 interfaceName2Construct.put(iConstruct.name, constructs.get(i));
140 for (int j = 0; j < iConstruct.action.defineVars.size(); j++) {
141 DefineVar var = iConstruct.action.defineVars.get(j);
142 var.renameVarName("__" + iConstruct.name + "_"
143 + var.varName + "__");
146 for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
147 String label = iConstruct.commitPointSet.get(j);
148 if (!CPLabel2InterfaceConstruct.containsKey(label)) {
149 CPLabel2InterfaceConstruct.put(label,
150 new ArrayList<InterfaceConstruct>());
152 CPLabel2InterfaceConstruct.get(label).add(iConstruct);
158 for (int i = 0; i < constructs.size(); i++) {
159 SpecConstruct inst = constructs.get(i);
160 Construct construct = inst.construct;
161 if (construct instanceof GlobalConstruct) {
162 GlobalConstruct theConstruct = (GlobalConstruct) construct;
163 if (!hasGlobalConstruct)
164 hasGlobalConstruct = true;
166 throw new SemanticsCheckerException(
167 "More than one global construct!");
169 // Record the options and check them
170 options = theConstruct.options;
172 // Record the HB conditions and check it
173 hbConditions = theConstruct.hbRelations;
174 for (ConditionalInterface left : hbConditions.keySet()) {
175 HashSet<ConditionalInterface> set = hbConditions.get(left);
176 checkHBLabelConsistency(left);
178 for (ConditionalInterface right : set) {
179 checkHBLabelConsistency(right);
182 } else if (construct instanceof PotentialCPDefineConstruct) {
183 PotentialCPDefineConstruct theConstruct = (PotentialCPDefineConstruct) construct;
184 label = theConstruct.label;
185 checkLabelDuplication(construct, label);
186 // Number the commit_point label
187 commitPointLabel2Num.put(label, _commitPointNum++);
189 potentialCPLabel2Construct.put(label, inst);
190 } else if (construct instanceof CPDefineCheckConstruct) {
191 CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct;
192 label = theConstruct.label;
193 checkLabelDuplication(construct, label);
194 // Number the commit_point label
195 commitPointLabel2Num.put(label, _commitPointNum++);
197 CPLabel2Construct.put(label, inst);
198 } else if (construct instanceof CPDefineConstruct) {
199 CPDefineConstruct theConstruct = (CPDefineConstruct) construct;
200 label = theConstruct.label;
201 checkLabelDuplication(construct, label);
202 // Number the commit_point label
203 commitPointLabel2Num.put(label, _commitPointNum++);
205 CPLabel2Construct.put(label, inst);
206 } else if (construct instanceof EntryPointConstruct) {
207 if (entryPointConstruct != null) {
208 throw new SemanticsCheckerException(
209 "More than one entry point!");
211 entryPointConstruct = inst;
212 } else if (construct instanceof InterfaceDefineConstruct) {
213 InterfaceDefineConstruct theConstruct = (InterfaceDefineConstruct) construct;
214 String name = theConstruct.name;
215 if (interfaceName2DefineConstruct.containsKey(name)) {
216 throw new SemanticsCheckerException(
217 "Interface define label duplicates!");
219 interfaceName2DefineConstruct.put(name, inst);
224 public String toString() {
225 StringBuilder sb = new StringBuilder();
226 if (entryPointConstruct == null) {
227 sb.append("Entry point is not specified!");
229 sb.append("@Entry_point:\n" + entryPointConstruct);
232 sb.append("Interface name 2 Construct:\n");
233 for (String interfaceName : interfaceName2Construct.keySet()) {
234 sb.append(interfaceName + "\t"
235 + interfaceName2Construct.get(interfaceName) + "\n");
238 sb.append("Interface name 2 define construct:\n");
239 for (String interfaceName : interfaceName2DefineConstruct.keySet()) {
240 sb.append(interfaceName + "\t"
241 + interfaceName2DefineConstruct.get(interfaceName) + "\n");
244 sb.append("Potential commit point label 2 Construct:\n");
245 for (String label : potentialCPLabel2Construct.keySet()) {
246 sb.append(label + "\t" + potentialCPLabel2Construct.get(label)
250 sb.append("Commit point label 2 Construct:\n");
251 for (String label : CPLabel2Construct.keySet()) {
252 sb.append(label + "\t" + CPLabel2Construct.get(label) + "\n");
254 return sb.toString();