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