src/edu/uci/eecs/specExtraction/SpecNaming.java

   1 package edu.uci.eecs.specExtraction;
   2
   3 import java.util.ArrayList;
   4 import java.util.Collections;
   5 import java.util.HashSet;
   6
   7 /**
   8  * <p>
   9  * This class contains most of the constant strings that we will be using
  10  * throughout the whole annotation extraction and code generation process.
  11  * </p>
  12  *
  13  * @author Peizhao Ou
  14  *
  15  */
  16 public class SpecNaming {
  17
  18         // Specification annotation naming
  19
  20         // Global construct
  21         public static final String DeclareState = "DeclareState";
  22         public static final String InitalState = "Initial";
  23         public static final String CopyState = "Copy";
  24         public static final String ClearState = "Clear";
  25         public static final String FinalState = "Final";
  26         public static final String PrintState = "Print";
  27         public static final String Commutativity = "Commutativity";
  28
  29         // Define construct
  30         public static final String Define = "Define";
  31
  32         // Interface construct
  33         public static final String Interface = "Interface";
  34         public static final String Transition = "Transition";
  35         public static final String PreCondition = "PreCondition";
  36         public static final String JustifyingPrecondition = "JustifyingPrecondition";
  37         public static final String SideEffect = "SideEffect";
  38         public static final String JustifyingPostcondition = "JustifyingPostcondition";
  39         public static final String PostCondition = "PostCondition";
  40         public static final String PrintValue = "Print";
  41
  42         public static final String PrintStateType = "PRINT_STATE";
  43         public static final String PrintValueType = "PRINT_VALUE";
  44         public static final String TransitionType = "TRANSITION";
  45         public static final String PreConditionType = "PRE_CONDITION";
  46         public static final String JustifyingPreconditionType = "JUSTIFYING_PRECONDITION";
  47         public static final String SideEffectType = "SIDE_EFFECT";
  48         public static final String JustifyingPostconditionType = "JUSTIFYING_POSTCONDITION";
  49         public static final String PostConditionType = "POST_CONDITION";
  50
  51         // Ordering point construct
  52         public static final String OPDefine = "OPDefine";
  53         public static final String PotentialOP = "PotentialOP";
  54         public static final String OPCheck = "OPCheck";
  55         public static final String OPClear = "OPClear";
  56         public static final String OPClearDefine = "OPClearDefine";
  57         // Entry construct
  58         public static final String Entry = "Entry";
  59
  60         // Generated header file name
  61         public static final String CDSSpecGeneratedName = "cdsspec-generated";
  62         public static final String CDSSpecGeneratedHeader = "\""
  63                         + CDSSpecGeneratedName + ".h\"";
  64         // Generated hedaer file comment
  65         public static final String CDSSpecGeneratedHeaderComment = "This is a header file auto-generated by CDSSpec compiler; together, CDSSpec\n"
  66                         + "compiler should have generated the accompanying implementation file that\n"
  67                         + "implements the some functions declared in this file. In order to instrument\n"
  68                         + "your benchmark for CDSSpec checker to check, you should include this header\n"
  69                         + "file in every file you use an CDSSpec annotation. Note that it should be\n"
  70                         + "placed in the end of all other header files. Currently we require a C++\n"
  71                         + "compiler that supports C++11.";
  72
  73         // Generated CPP file name
  74         public static final String CDSSpecGeneratedCPP = "cdsspec-generated.cc";
  75         // Generated CPP file comment
  76         public static final String CDSSpecGeneratedCPPComment = "This is an implementation file auto-generated by CDSSpec compiler to\n"
  77                         + "instrument your benchmark for CDSSpec checker to check. Currently we require\n"
  78                         + "a C++ compiler that supports C++11.";
  79
  80         // Pre-included header files
  81         public static final HashSet<String> includedHeaders;
  82         public static final ArrayList<String> includedHeadersList;
  83
  84         public static final String ATOMIC = "<atomic>";
  85         public static final String THREADS = "<threads.h>";
  86         public static final String STDATOMIC = "<stdatomic.h>";
  87         public static final String STDLIB = "<stdlib.h>";
  88         public static final String STDIO = "<stdio.h>";
  89
  90         public static final String MODELTYPES = "<modeltypes.h>";
  91         public static final String CDSANNOTATE = "<cdsannotate.h>";
  92         public static final String MYMEMORY = "\"mymemory.h\"";
  93         public static final String MODELASSERT = "\"model-assert.h\"";
  94         public static final String LIBRACE = "\"librace.h\"";
  95         public static final String SPECANNOTATION = "\"specannotation.h\"";
  96         public static final String SPEC_COMMON = "\"spec_common.h\"";
  97         public static final String CDSSPEC = "\"cdsspec.h\"";
  98         public static final String METHODCALL = "\"methodcall.h\"";
  99
 100         // Header files to include in the cdsspec-generated.h
 101         public static final String SPECANNOTATION_API = "\"specannotation-api.h\"";
 102
 103         // Header files to include in the cdsspec-generated.cc
 104         // <cdsannotate.h>
 105         // "spec_common.h"
 106         // "methodcall.h"
 107         // "cdsspec.h"
 108         // "specannotation.h"
 109
 110         static {
 111                 // Initialize the header set and list
 112                 includedHeaders = new HashSet<String>();
 113                 includedHeadersList = new ArrayList<String>();
 114
 115                 // Add each header to the set
 116                 includedHeadersList.add(ATOMIC);
 117                 includedHeadersList.add(THREADS);
 118                 includedHeadersList.add(STDATOMIC);
 119                 includedHeadersList.add(STDLIB);
 120                 includedHeadersList.add(STDIO);
 121
 122                 includedHeadersList.add(MODELTYPES);
 123                 includedHeadersList.add(CDSANNOTATE);
 124                 includedHeadersList.add(MYMEMORY);
 125                 includedHeadersList.add(MODELASSERT);
 126                 includedHeadersList.add(LIBRACE);
 127                 includedHeadersList.add(SPECANNOTATION);
 128                 includedHeadersList.add(SPEC_COMMON);
 129                 includedHeadersList.add(METHODCALL);
 130                 includedHeadersList.add(CDSSPEC);
 131
 132                 // Add files to list
 133                 for (String header : includedHeadersList) {
 134                         includedHeaders.add(header);
 135                 }
 136         }
 137
 138         public static boolean isPreIncludedHeader(String header) {
 139                 return includedHeaders.contains(header)
 140                                 || header.equals(CDSSpecGeneratedHeader);
 141         }
 142
 143         // Some CDSSpec keywords and function names
 144         public static final String NewSize = "NEW_SIZE";
 145         public static final String New = "NEW";
 146         // Some CDSSpec types
 147         public static final String CString = "CSTR";
 148         public static final String EmptyCString = "_EMPTY";
 149         public static final String NullFunc = "NULL_FUNC";
 150
 151         public static final String StateStruct = "StateStruct";
 152         public static final String Method = "Method";
 153         public static final String MethodValueField = "value";
 154         public static final String CommutativityRule = "CommutativityRule";
 155         public static final String StateFunctions = "StateFunctions";
 156         public static final String NamedFunction = "NamedFunction";
 157
 158         public static final String SPEC_ANALYSIS = "SPEC_ANALYSIS";
 159         // Spec annotations
 160         public static final String AnnoInit = "AnnoInit";
 161         public static final String AnnoTypeInit = "INIT";
 162         public static final String AnnoInterfaceInfo = "AnnoInterfaceInfo";
 163         public static final String CAnnoInterfaceInfo = "CAnnoInterfaceInfo";
 164         public static final String SpecAnnotation = "SpecAnnotation";
 165
 166         // Some CDSSpec state functions
 167         public static final String InitialFunc = "_Initial";
 168         public static final String CopyFunc = "_Copy";
 169         public static final String FinalFunc = "_Final";
 170         public static final String PrintStateFunc = "_PrintState";
 171
 172         // Functions for instrumenting annotation
 173         public static final String CreateInitAnnoFunc = "_createInitAnnotation";
 174         public static final String CreateInterfaceBeginAnnoFunc = "_createInterfaceBeginAnnotation";
 175         public static final String SetInterfaceBeginAnnoValueFunc = "_setInterfaceBeginAnnotationValue";
 176         public static final String CreateInterfaceEndAnnoFunc = "_createInterfaceEndAnnotation";
 177         public static final String CreateOPDefineAnnoFunc = "_createOPDefineAnnotation";
 178         public static final String CreateOPDefineUnattachedFunc = "_createOPDefineUnattached";
 179         public static final String CreateOPClearDefineUnattachedFunc = "_createOPClearDefineUnattached";
 180         public static final String CreatePotentialOPAnnoFunc = "_createPotentialOPAnnotation";
 181         public static final String CreateOPCheckAnnoFunc = "_createOPCheckAnnotation";
 182         public static final String CreateOPClearAnnoFunc = "_createOPClearAnnotation";
 183         public static final String CreateOPClearDefineAnnoFunc = "_createOPClearDefineAnnotation";
 184
 185         // Other CDSSpec functions
 186         public static final String AddInterfaceFunctions = "addInterfaceFunctions";
 187         public static final String CDSAnnotateFunc = "cdsannotate";
 188         public static final String PRINT = "PRINT";
 189         public static final String PrintContainer = "printContainer";
 190         public static final String PrintMap = "printMap";
 191
 192         // Special instances
 193         public static final String Method1 = "_M";
 194         public static final String Method2 = "_exec";
 195         public static final String StateInst = "state";
 196         public static final String OldStateInst = "OLD";
 197         public static final String NewStateInst = "NEW";
 198         // Specification types and macros
 199         public static final String C_RET = "C_RET";
 200         public static final String S_RET = "S_RET";
 201         public static final String InterfaceValueInst = "__value";
 202
 203         // The fake ordering point operation
 204         public static final String FakeOP = "_FAKE_OP_";
 205
 206         // The wrapper prefix that we want to attach to the function name
 207         public static final String WrapperPrefix = "Wrapper";
 208
 209         public static final String CommutativityRuleInst = "commuteRules";
 210         public static final String CommutativityRuleSizeInst = "CommuteRuleSize";
 211         public static final String StateFunctionsInst = "stateFuncs";
 212         public static final String AnnoInitInst = "init";
 213         public static final String AnnoInterfaceInfoInst = "info";
 214
 215         public static String AppendStr(String original) {
 216                 return "_" + original + "_str";
 217         }
 218
 219         public static String CheckCommutativity(int ruleNum) {
 220                 return "_checkCommutativity" + ruleNum;
 221         }
 222
 223 }