1 package edu.uci.eecs.specExtraction;
3 import java.util.ArrayList;
4 import java.util.Collections;
5 import java.util.HashSet;
9 * This class contains most of the constant strings that we will be using
10 * throughout the whole annotation extraction and code generation process.
16 public class SpecNaming {
18 // Specification annotation naming
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";
30 public static final String Define = "Define";
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";
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";
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";
58 public static final String Entry = "Entry";
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.";
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.";
80 // Pre-included header files
81 public static final HashSet<String> includedHeaders;
82 public static final ArrayList<String> includedHeadersList;
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>";
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\"";
100 // Header files to include in the cdsspec-generated.h
101 public static final String SPECANNOTATION_API = "\"specannotation-api.h\"";
103 // Header files to include in the cdsspec-generated.cc
108 // "specannotation.h"
111 // Initialize the header set and list
112 includedHeaders = new HashSet<String>();
113 includedHeadersList = new ArrayList<String>();
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);
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);
133 for (String header : includedHeadersList) {
134 includedHeaders.add(header);
138 public static boolean isPreIncludedHeader(String header) {
139 return includedHeaders.contains(header)
140 || header.equals(CDSSpecGeneratedHeader);
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";
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";
158 public static final String SPEC_ANALYSIS = "SPEC_ANALYSIS";
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";
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";
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";
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";
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";
203 // The fake ordering point operation
204 public static final String FakeOP = "_FAKE_OP_";
206 // The wrapper prefix that we want to attach to the function name
207 public static final String WrapperPrefix = "Wrapper";
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";
215 public static String AppendStr(String original) {
216 return "_" + original + "_str";
219 public static String CheckCommutativity(int ruleNum) {
220 return "_checkCommutativity" + ruleNum;