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