src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java

   1 package edu.uci.eecs.specCompiler.codeGenerator;
   2
   3 import java.io.File;
   4 import java.util.ArrayList;
   5 import java.util.HashMap;
   6 import java.util.HashSet;
   7
   8 import edu.uci.eecs.specCompiler.grammerParser.ParseException;
   9 import edu.uci.eecs.specCompiler.grammerParser.SpecParser;
  10 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
  11 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
  12 import edu.uci.eecs.specCompiler.specExtraction.ClassBeginConstruct;
  13 import edu.uci.eecs.specCompiler.specExtraction.ClassEndConstruct;
  14 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
  15 import edu.uci.eecs.specCompiler.specExtraction.Construct;
  16 import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
  17 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
  18 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
  19 import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
  20 import edu.uci.eecs.specCompiler.specExtraction.ParserUtils;
  21 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
  22 import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
  23 import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
  24
  25 public class SemanticsChecker {
  26         public final HashMap<File, SourceFileInfo> srcFilesInfo;
  27         public final ArrayList<Construct> constructs;
  28         public final HashMap<String, Construct> CPLabel2Construct;
  29         public final HashMap<String, PotentialCPDefineConstruct> potentialCPLabel2Construct;
  30         public final HashMap<String, InterfaceConstruct> interfaceName2Construct;
  31         public final HashMap<String, InterfaceDefineConstruct> interfaceName2DefineConstruct;
  32         public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
  33
  34         public final HashMap<String, Integer> interface2Num;
  35         public final HashMap<String, Integer> hbLabel2Num;
  36         public final HashMap<String, Integer> commitPointLabel2Num;
  37
  38         private HashMap<String, String> options;
  39         private HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions;
  40         private ArrayList<EntryPointConstruct> entryPointConstructs;
  41         private ClassBeginConstruct classBeginConstruct;
  42         private ClassEndConstruct classEndConstruct;
  43         private GlobalConstruct globalConstruct;
  44
  45         private String templateStr;
  46         private String templateFullStr;
  47         private String className;
  48
  49         private int _interfaceNum;
  50         private int _hbLabelNum;
  51         private int _commitPointNum;
  52
  53         public SemanticsChecker(SpecExtractor extractor) {
  54                 this.srcFilesInfo = extractor.srcFilesInfo;
  55                 this.constructs = extractor.getConstructs();
  56                 this.CPLabel2Construct = new HashMap<String, Construct>();
  57                 this.potentialCPLabel2Construct = new HashMap<String, PotentialCPDefineConstruct>();
  58                 this.interfaceName2Construct = new HashMap<String, InterfaceConstruct>();
  59                 this.interfaceName2DefineConstruct = new HashMap<String, InterfaceDefineConstruct>();
  60                 this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
  61                 this.entryPointConstructs = new ArrayList<EntryPointConstruct>();
  62                 this.classBeginConstruct = null;
  63                 this.classEndConstruct = null;
  64
  65                 this.interface2Num = new HashMap<String, Integer>();
  66                 this.hbLabel2Num = new HashMap<String, Integer>();
  67                 // Immediately init the true HB-condition to be 0
  68                 hbLabel2Num.put("", 0);
  69
  70                 this.commitPointLabel2Num = new HashMap<String, Integer>();
  71
  72                 _interfaceNum = 0;
  73                 _hbLabelNum = 0;
  74                 _commitPointNum = 0;
  75
  76                 templateStr = null;
  77                 templateFullStr = null;
  78                 className = null;
  79         }
  80
  81         public ClassBeginConstruct getClassBeginConstruct() {
  82                 return this.classBeginConstruct;
  83         }
  84
  85         public ClassEndConstruct getClassEndConstruct() {
  86                 return this.classEndConstruct;
  87         }
  88
  89         public String getTemplateFullStr() {
  90                 return this.templateFullStr;
  91         }
  92
  93         public String getTemplateStr() {
  94                 return this.templateStr;
  95         }
  96
  97         public String getClassName() {
  98                 return this.className;
  99         }
 100
 101         public GlobalConstruct getGlobalConstruct() {
 102                 return this.globalConstruct;
 103         }
 104
 105         public HashMap<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
 106                 return this.hbConditions;
 107         }
 108
 109         /**
 110          * Check if the conditional interface is in the HB checking list
 111          * @param condInterface
 112          * @return
 113          */
 114         public boolean containsConditionalInterface(ConditionalInterface condInterface) {
 115                 if (hbConditions.containsKey(condInterface))
 116                         return true;
 117                 for (ConditionalInterface key : hbConditions.keySet()) {
 118                         if (hbConditions.get(key).contains(condInterface))
 119                                 return true;
 120                 }
 121                 return false;
 122         }
 123
 124         public String getOption(String key) {
 125                 return options.get(key);
 126         }
 127
 128         private void checkHBLabelConsistency(ConditionalInterface inst)
 129                         throws SemanticsCheckerException {
 130                 String interfaceName = inst.interfaceName, label = inst.hbConditionLabel;
 131                 if (!interfaceName2Construct.containsKey(interfaceName)) {
 132                         throw new SemanticsCheckerException(
 133                                         "In global construct, no interface \"" + interfaceName
 134                                                         + "\"!");
 135                 } else if (!label.equals("")) {
 136                         InterfaceConstruct iConstruct = (InterfaceConstruct) interfaceName2Construct
 137                                         .get(interfaceName);
 138                         if (!iConstruct.hbConditions.containsKey(label)) {
 139                                 throw new SemanticsCheckerException("Interface "
 140                                                 + interfaceName + " doesn't contain HB_codition: "
 141                                                 + label + "!");
 142                         }
 143
 144                         // Number the HB-condition label
 145                         hbLabel2Num.put(label, _hbLabelNum++);
 146                 }
 147         }
 148
 149         private void checkLabelDuplication(Construct construct, String label)
 150                         throws SemanticsCheckerException {
 151                 if (potentialCPLabel2Construct.containsKey(label)
 152                                 || CPLabel2Construct.containsKey(label))
 153                         throw new SemanticsCheckerException("In construct: " + construct
 154                                         + "\"" + label + "\" has duplication.");
 155         }
 156
 157         private void checkOptions() throws SemanticsCheckerException {
 158                 // FIXME: We don't have any check here
 159         }
 160
 161         private void postCheck() throws SemanticsCheckerException {
 162                 // C++ data structure with Class must provide the beginning and ending
 163                 // of its declaration
 164                 if (getOption("Class") != null) {
 165                         if (classBeginConstruct == null || classEndConstruct == null) {
 166                                 throw new SemanticsCheckerException(
 167                                                 "Class must provide the boundary explicitly!");
 168                         }
 169                 }
 170                 // It must provide the entry point
 171                 if (entryPointConstructs.size() == 0) {
 172                         throw new SemanticsCheckerException(
 173                                         "The program must have at least one entry point!");
 174                 }
 175
 176                 // Check if interface define construct labels are correct
 177                 for (String name : interfaceName2DefineConstruct.keySet()) {
 178                         if (!interfaceName2Construct.containsKey(name)) {
 179                                 throw new SemanticsCheckerException("Label \"" + name
 180                                                 + "\" does not have interface declaration!");
 181                         }
 182                 }
 183         }
 184
 185         public void check() throws SemanticsCheckerException {
 186                 boolean hasGlobalConstruct = false;
 187                 // First grab the information from the interface
 188                 for (int i = 0; i < constructs.size(); i++) {
 189                         Construct inst = constructs.get(i);
 190                         if (inst instanceof InterfaceConstruct) {
 191                                 InterfaceConstruct iConstruct = (InterfaceConstruct) inst;
 192                                 if (interfaceName2Construct.containsKey(iConstruct.name)) {
 193                                         throw new SemanticsCheckerException("Interface name: "
 194                                                         + iConstruct.name + " duplicates!");
 195                                 }
 196                                 // Number the interface label
 197                                 interface2Num.put(iConstruct.name, _interfaceNum++);
 198
 199                                 interfaceName2Construct.put(iConstruct.name,
 200                                                 (InterfaceConstruct) constructs.get(i));
 201
 202                                 for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
 203                                         String label = iConstruct.commitPointSet.get(j);
 204                                         if (!CPLabel2InterfaceConstruct.containsKey(label)) {
 205                                                 CPLabel2InterfaceConstruct.put(label,
 206                                                                 new ArrayList<InterfaceConstruct>());
 207                                         }
 208                                         CPLabel2InterfaceConstruct.get(label).add(iConstruct);
 209                                 }
 210                         }
 211                 }
 212
 213                 String label;
 214                 for (int i = 0; i < constructs.size(); i++) {
 215                         Construct construct = constructs.get(i);
 216                         if (construct instanceof GlobalConstruct) {
 217                                 GlobalConstruct theConstruct = (GlobalConstruct) construct;
 218                                 globalConstruct = theConstruct;
 219                                 if (!hasGlobalConstruct)
 220                                         hasGlobalConstruct = true;
 221                                 else {
 222                                         throw new SemanticsCheckerException(
 223                                                         "More than one global construct!");
 224                                 }
 225                                 // Record the options and check them
 226                                 options = theConstruct.options;
 227
 228                                 // Record the HB conditions and check it
 229                                 hbConditions = theConstruct.hbRelations;
 230                                 for (ConditionalInterface left : hbConditions.keySet()) {
 231                                         HashSet<ConditionalInterface> set = hbConditions.get(left);
 232                                         checkHBLabelConsistency(left);
 233
 234                                         for (ConditionalInterface right : set) {
 235                                                 checkHBLabelConsistency(right);
 236                                         }
 237                                 }
 238                         } else if (construct instanceof PotentialCPDefineConstruct) {
 239                                 PotentialCPDefineConstruct theConstruct = (PotentialCPDefineConstruct) construct;
 240                                 label = theConstruct.label;
 241                                 checkLabelDuplication(construct, label);
 242                                 // Number the commit_point label
 243                                 commitPointLabel2Num.put(label, _commitPointNum++);
 244
 245                                 potentialCPLabel2Construct.put(label,
 246                                                 (PotentialCPDefineConstruct) construct);
 247                         } else if (construct instanceof CPDefineCheckConstruct) {
 248                                 CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct;
 249                                 label = theConstruct.label;
 250                                 checkLabelDuplication(construct, label);
 251                                 // Number the commit_point label
 252                                 commitPointLabel2Num.put(label, _commitPointNum++);
 253
 254                                 CPLabel2Construct.put(label, construct);
 255                         } else if (construct instanceof CPDefineConstruct) {
 256                                 CPDefineConstruct theConstruct = (CPDefineConstruct) construct;
 257                                 label = theConstruct.label;
 258                                 checkLabelDuplication(construct, label);
 259                                 // Number the commit_point label
 260                                 commitPointLabel2Num.put(label, _commitPointNum++);
 261
 262                                 CPLabel2Construct.put(label, construct);
 263                         } else if (construct instanceof EntryPointConstruct) {
 264                                 entryPointConstructs.add((EntryPointConstruct) construct);
 265                         } else if (construct instanceof InterfaceDefineConstruct) {
 266                                 InterfaceDefineConstruct theConstruct = (InterfaceDefineConstruct) construct;
 267                                 String name = theConstruct.name;
 268                                 if (interfaceName2DefineConstruct.containsKey(name)) {
 269                                         throw new SemanticsCheckerException(
 270                                                         "Interface define label duplicates!");
 271                                 }
 272                                 interfaceName2DefineConstruct.put(name, theConstruct);
 273                         } else if (construct instanceof ClassBeginConstruct) {
 274                                 classBeginConstruct = (ClassBeginConstruct) construct;
 275                                 ArrayList<String> content = srcFilesInfo.get(classBeginConstruct.file).content;
 276                                 String firstLine = content.get(classBeginConstruct.beginLineNum), secondLine;
 277                                 if (firstLine.startsWith("template")) {
 278                                         secondLine = content.get(classBeginConstruct.beginLineNum + 1);
 279                                         templateFullStr = firstLine;
 280                                         templateStr = ParserUtils.getTemplateStr(firstLine);
 281                                         className = ParserUtils.getClassName(secondLine);
 282                                 } else {
 283                                         className = ParserUtils.getClassName(firstLine);
 284                                 }
 285
 286                         } else if (construct instanceof ClassEndConstruct) {
 287                                 classEndConstruct = (ClassEndConstruct) construct;
 288                                 className = getOption("CLASS");
 289                         }
 290                 }
 291         }
 292
 293         public String toString() {
 294                 StringBuilder sb = new StringBuilder();
 295
 296                 sb.append("Interface name 2 Construct:\n");
 297                 for (String interfaceName : interfaceName2Construct.keySet()) {
 298                         sb.append(interfaceName + "\t"
 299                                         + interfaceName2Construct.get(interfaceName) + "\n");
 300                 }
 301
 302                 sb.append("Interface name 2 define construct:\n");
 303                 for (String interfaceName : interfaceName2DefineConstruct.keySet()) {
 304                         sb.append(interfaceName + "\t"
 305                                         + interfaceName2DefineConstruct.get(interfaceName) + "\n");
 306                 }
 307
 308                 sb.append("Potential commit point label 2 Construct:\n");
 309                 for (String label : potentialCPLabel2Construct.keySet()) {
 310                         sb.append(label + "\t" + potentialCPLabel2Construct.get(label)
 311                                         + "\n");
 312                 }
 313
 314                 sb.append("Commit point label 2 Construct:\n");
 315                 for (String label : CPLabel2Construct.keySet()) {
 316                         sb.append(label + "\t" + CPLabel2Construct.get(label) + "\n");
 317                 }
 318                 return sb.toString();
 319         }
 320 }