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