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

   1 package edu.uci.eecs.specCompiler.codeGenerator;
   2
   3 import java.util.ArrayList;
   4 import java.util.HashMap;
   5 import java.util.HashSet;
   6
   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;
  18
  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;
  27
  28         public final HashMap<String, Integer> interface2Num;
  29         public final HashMap<String, Integer> hbLabel2Num;
  30         public final HashMap<String, Integer> commitPointLabel2Num;
  31
  32         private HashMap<String, String> options;
  33         private HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions;
  34         private SpecConstruct entryPointConstruct;
  35
  36         private int _interfaceNum;
  37         private int _hbLabelNum;
  38         private int _commitPointNum;
  39
  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;
  49
  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);
  54
  55                 this.commitPointLabel2Num = new HashMap<String, Integer>();
  56
  57                 _interfaceNum = 0;
  58                 _hbLabelNum = 0;
  59                 _commitPointNum = 0;
  60         }
  61
  62         public HashMap<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
  63                 return this.hbConditions;
  64         }
  65
  66         public String getOption(String key) {
  67                 return options.get(key);
  68         }
  69
  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
  76                                                         + "\"!");
  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: "
  83                                                 + label + "!");
  84                         }
  85
  86                         // No HB condition label can duplicate!
  87                         if (hbLabel2Num.containsKey(label)) {
  88                                 throw new SemanticsCheckerException("Happens-before label: "
  89                                                 + label + " duplicates!");
  90                         }
  91
  92                         // Number the HB-condition label
  93                         hbLabel2Num.put(label, _hbLabelNum++);
  94                 }
  95         }
  96
  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.");
 103         }
 104
 105         private void checkOptions() throws SemanticsCheckerException {
 106                 // FIXME: We don't have any check here
 107         }
 108
 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!");
 114                 }
 115
 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!");
 121                         }
 122                 }
 123         }
 124
 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!");
 135                                 }
 136                                 // Number the interface label
 137                                 interface2Num.put(iConstruct.name, _interfaceNum++);
 138
 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 + "__");
 144                                 }
 145
 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>());
 151                                         }
 152                                         CPLabel2InterfaceConstruct.get(label).add(iConstruct);
 153                                 }
 154                         }
 155                 }
 156
 157                 String label;
 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;
 165                                 else {
 166                                         throw new SemanticsCheckerException(
 167                                                         "More than one global construct!");
 168                                 }
 169                                 // Record the options and check them
 170                                 options = theConstruct.options;
 171
 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);
 177
 178                                         for (ConditionalInterface right : set) {
 179                                                 checkHBLabelConsistency(right);
 180                                         }
 181                                 }
 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++);
 188
 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++);
 196
 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++);
 204
 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!");
 210                                 }
 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!");
 218                                 }
 219                                 interfaceName2DefineConstruct.put(name, inst);
 220                         }
 221                 }
 222         }
 223
 224         public String toString() {
 225                 StringBuilder sb = new StringBuilder();
 226                 if (entryPointConstruct == null) {
 227                         sb.append("Entry point is not specified!");
 228                 } else {
 229                         sb.append("@Entry_point:\n" + entryPointConstruct);
 230                 }
 231
 232                 sb.append("Interface name 2 Construct:\n");
 233                 for (String interfaceName : interfaceName2Construct.keySet()) {
 234                         sb.append(interfaceName + "\t"
 235                                         + interfaceName2Construct.get(interfaceName) + "\n");
 236                 }
 237
 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");
 242                 }
 243
 244                 sb.append("Potential commit point label 2 Construct:\n");
 245                 for (String label : potentialCPLabel2Construct.keySet()) {
 246                         sb.append(label + "\t" + potentialCPLabel2Construct.get(label)
 247                                         + "\n");
 248                 }
 249
 250                 sb.append("Commit point label 2 Construct:\n");
 251                 for (String label : CPLabel2Construct.keySet()) {
 252                         sb.append(label + "\t" + CPLabel2Construct.get(label) + "\n");
 253                 }
 254                 return sb.toString();
 255         }
 256 }