-Class<int>* //A::B<sfd, _sdf>::id(const char * ch_ptr, int a)
-//template < TypeK k, TypeV v>
+#include <threads.h>
+#include <stdlib.h>
+#include "librace.h"
+#include "model-assert.h"
+
+#include "my_queue.h"
+
+#define relaxed memory_order_relaxed
+#define release memory_order_release
+#define acquire memory_order_acquire
+
+#define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */
+#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */
+
+#define POISON_IDX 0x666
+
+static unsigned int (*free_lists)[MAX_FREELIST];
+
+/* Search this thread's free list for a "new" node */
+static unsigned int new_node()
+{
+ int i;
+ int t = get_thread_num();
+ for (i = 0; i < MAX_FREELIST; i++) {
+ unsigned int node = load_32(&free_lists[t][i]);
+ if (node) {
+ store_32(&free_lists[t][i], 0);
+ return node;
+ }
+ }
+ /* free_list is empty? */
+ MODEL_ASSERT(0);
+ return 0;
+}
+
+/* Place this node index back on this thread's free list */
+static void reclaim(unsigned int node)
+{
+ int i;
+ int t = get_thread_num();
+
+ /* Don't reclaim NULL node */
+ MODEL_ASSERT(node);
+
+ for (i = 0; i < MAX_FREELIST; i++) {
+ /* Should never race with our own thread here */
+ unsigned int idx = load_32(&free_lists[t][i]);
+
+ /* Found empty spot in free list */
+ if (idx == 0) {
+ store_32(&free_lists[t][i], node);
+ return;
+ }
+ }
+ /* free list is full? */
+ MODEL_ASSERT(0);
+}
+
+void init_queue(queue_t *q, int num_threads)
+{
+ /**
+ @Begin
+ @Entry_point
+ @End
+ */
+
+ int i, j;
+
+ /* Initialize each thread's free list with INITIAL_FREE pointers */
+ /* The actual nodes are initialized with poison indexes */
+ free_lists = malloc(num_threads * sizeof(*free_lists));
+ for (i = 0; i < num_threads; i++) {
+ for (j = 0; j < INITIAL_FREE; j++) {
+ free_lists[i][j] = 2 + i * MAX_FREELIST + j;
+ atomic_init(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
+ }
+ }
+
+ /* initialize queue */
+ atomic_init(&q->head, MAKE_POINTER(1, 0));
+ atomic_init(&q->tail, MAKE_POINTER(1, 0));
+ atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
+}
+
+/**
+ @Begin
+ @Interface_define: Enqueue
+ @End
+*/
+void enqueue(queue_t *q, unsigned int val)
+{
+ int success = 0;
+ unsigned int node;
+ pointer tail;
+ pointer next;
+ pointer tmp;
+
+ node = new_node();
+ store_32(&q->nodes[node].value, val);
+ tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
+ set_ptr(&tmp, 0); // NULL
+ atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
+
+ while (!success) {
+ tail = atomic_load_explicit(&q->tail, acquire);
+ next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
+ if (tail == atomic_load_explicit(&q->tail, relaxed)) {
+
+ /* Check for uninitialized 'next' */
+ MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+ if (get_ptr(next) == 0) { // == NULL
+ pointer value = MAKE_POINTER(node, get_count(next) + 1);
+ success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
+ &next, value, release, release);
+ }
+ if (!success) {
+ unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
+ pointer value = MAKE_POINTER(ptr,
+ get_count(tail) + 1);
+ int commit_success = 0;
+ commit_success = atomic_compare_exchange_strong_explicit(&q->tail,
+ &tail, value, release, release);
+ /**
+ @Begin
+ @Commit_point_define_check: __ATOMIC_RET__ == true
+ @Label: Enqueue_Success_Point
+ @End
+ */
+ thrd_yield();
+ }
+ }
+ }
+ atomic_compare_exchange_strong_explicit(&q->tail,
+ &tail,
+ MAKE_POINTER(node, get_count(tail) + 1),
+ release, release);
+}
+
+
+/**
+ @Begin
+ @Interface_define: Dequeue
+ @End
+*/
+unsigned int dequeue(queue_t *q)
+{
+ unsigned int value;
+ int success = 0;
+ pointer head;
+ pointer tail;
+ pointer next;
+
+ while (!success) {
+ head = atomic_load_explicit(&q->head, acquire);
+ tail = atomic_load_explicit(&q->tail, relaxed);
+ next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
+ if (atomic_load_explicit(&q->head, relaxed) == head) {
+ if (get_ptr(head) == get_ptr(tail)) {
+
+ /* Check for uninitialized 'next' */
+ MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+ if (get_ptr(next) == 0) { // NULL
+ return 0; // NULL
+ }
+ atomic_compare_exchange_strong_explicit(&q->tail,
+ &tail,
+ MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
+ release, release);
+ thrd_yield();
+ } else {
+ value = load_32(&q->nodes[get_ptr(next)].value);
+ success = atomic_compare_exchange_strong_explicit(&q->head,
+ &head,
+ MAKE_POINTER(get_ptr(next), get_count(head) + 1),
+ release, release);
+ /**
+ @Begin
+ @Commit_point_define_check: __ATOMIC_RET__ == true
+ @Label: Dequeue_Success_Point
+ @End
+ */
+ if (!success)
+ thrd_yield();
+ }
+ }
+ }
+ reclaim(get_ptr(head));
+ return value;
+}
@Check: (Optional)
...
@Action: (Optional)
- # Type here must be a pointer
- @DefineVar: Type var1 = SomeExpression (Optional)
- @Code (Optional)
...
@Post_action: (Optional)
@Post_check: (Optional)
import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
-import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
import edu.uci.eecs.specCompiler.specExtraction.ClassBeginConstruct;
import edu.uci.eecs.specCompiler.specExtraction.ClassEndConstruct;
import edu.uci.eecs.specCompiler.specExtraction.FunctionHeader;
+import edu.uci.eecs.specCompiler.specExtraction.QualifiedName;
+import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
+import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
public class SpecParser {
private static ArrayList<String> _content;
public static void main(String[] argvs)
throws ParseException, TokenMgrError {
try {
- String line = "int* A::B<sfd, _sdf>::id(const char * ch_ptr, int a)";
- System.out.println(parseFuncHeader(line));
-
File f = new File("./grammer/spec.txt");
FileInputStream fis = new FileInputStream(f);
SpecParser parser = new SpecParser(fis);
- /**
+
ArrayList<String> content = new ArrayList<String>();
ArrayList<Construct> constructs = new ArrayList<Construct>();
- parser.Parse(f, content, constructs);
+ ArrayList<String> headers = new ArrayList<String>();
+ parser.Parse(f, content, constructs, headers);
for (int i = 0; i < content.size(); i++) {
System.out.println(content.get(i));
}
- */
- parser.Test();
+
+ for (int i = 0; i < constructs.size(); i++) {
+ System.out.println(constructs.get(i));
+ }
+
+ //parser.Test();
System.out.println("Parsing finished!");
} catch (FileNotFoundException e) {
e.printStackTrace();
}
}
- public static void ParseFile(File f, ArrayList<String> content, ArrayList<Construct> constructs)
+ public static SourceFileInfo ParseFile(File f)
throws ParseException, TokenMgrError {
try {
InputStream input = new FileInputStream(f);
SpecParser parser = new SpecParser(input);
- parser.Parse(f, content, constructs);
+ ArrayList<String> content = new ArrayList<String>(),
+ headers = new ArrayList<String>();
+ ArrayList<Construct> constructs = new ArrayList<Construct>();
+ parser.Parse(f, content, constructs, headers);
+ return new SourceFileInfo(f, content, headers, constructs);
} catch (FileNotFoundException e) {
e.printStackTrace();
}
+ return null;
}
public static ArrayList<String> getTemplateArg(String line)
<CHECK: "@Check:">
|
<ACTION: "@Action:">
-|
- <DEFINEVAR: "@DefineVar:">
|
<CODE: "@Code:">
|
<HB_SYMBOL: "->">
|
<COMMA: ",">
-
|
/* C/C++ only token*/
<DOT: ".">
{
String type;
String str;
+ QualifiedName name;
}
{
{ type = ""; }
)?
(((str = <STRUCT>.image | str = <CLASS>.image) { type = type + " " + str; })?
(
- str = QualifiedName() {
+ name = ParseQualifiedName() {
if (!type.equals(""))
- type = type + " " + str;
+ type = type + " " + name.fullName;
else
- type = str;
- })
- (
- str = ParameterizedName() {
- if (!type.equals(""))
- type = type + " " + str;
- else
- type = str;
+ type = name.fullName;
})
)
((str = "const".image {
}
void Test() :
-{}
{
- Type()
- //FuncDecl()
+ String str;
+ FunctionHeader func;
+}
+{
+ /*
+ str = Type()
+ {
+ System.out.println(str);
+ }
+ */
+ func = FuncDecl()
+ {
+ System.out.println(func);
+ }
}
String ParameterizedName() :
FunctionHeader FuncDecl() :
{
- String ret, qualifiedName, bareName;
- ArrayList<String> args;
+ String ret;
+ QualifiedName funcName;
+ ArrayList<VariableDeclaration> args;
}
{
ret = Type()
- qualifiedName = QualifiedName()
- bareName = <IDENTIFIER>.image
+ funcName = ParseQualifiedName()
args = FormalParamList()
{
- FunctionHeader res = new FunctionHeader(ret, qualifiedName, bareName, args);
+ FunctionHeader res = new FunctionHeader(ret, funcName, args);
//System.out.println(res);
return res;
}
}
-String QualifiedName() :
+QualifiedName ParseQualifiedName() :
{
String qualifiedName, str;
}
{
{ qualifiedName = ""; }
- (LOOKAHEAD(2) (str = ParameterizedName() { qualifiedName = qualifiedName +
- str + "::"; } <DOUBLECOLON> ))*
+ (str = ParameterizedName() { qualifiedName = qualifiedName + str; } )
+ ( <DOUBLECOLON> (str = ParameterizedName() { qualifiedName = qualifiedName +
+ "::" + str; } ))*
{
- return qualifiedName;
+ QualifiedName res = new QualifiedName(qualifiedName);
+ //System.out.println(res);
+ return res;
}
}
}
}
-ArrayList<String> FormalParamList() :
+ArrayList<VariableDeclaration > FormalParamList() :
{
- ArrayList<String> typeParams;
+ ArrayList<VariableDeclaration > typeParams;
+ VariableDeclaration varDecl;
}
{
{
- typeParams = new ArrayList<String>();
+ typeParams = new ArrayList<VariableDeclaration >();
}
"("
- (TypeParam(typeParams) (<COMMA> TypeParam(typeParams))*)?
+ ((varDecl = TypeParam() {typeParams.add(varDecl);})
+ ((<COMMA> varDecl = TypeParam() {typeParams.add(varDecl);}))*)?
")"
{
return typeParams;
}
}
-void TypeParam(ArrayList<String> typeParams) :
+VariableDeclaration TypeParam() :
{
String type, param;
}
{
(type = Type()) (param = <IDENTIFIER>.image)
{
- typeParams.add(type);
- typeParams.add(param);
+ return new VariableDeclaration(type, param);
}
}
-ArrayList<String> C_CPP_CODE() :
+ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
{
String text;
Token t;
boolean newLine = false;
boolean inTemplate = false;
ArrayList<String> content;
+ String header;
}
{
{
(
t = <CONST> | t = <STRUCT> | t = <CLASS> |
(t = <TEMPLATE> { inTemplate = true; })|
- t = <IDENTIFIER> | t = <POUND> |
+ (header = <INCLUDE>.image {
+ if (headers != null) {
+ headers.add(header.substring(header.lastIndexOf(' ') + 1));
+ }
+ })
+ | t = <IDENTIFIER> | t = <POUND> |
(t = <OPEN_BRACE> { newLine = true; } ) |
(t = <CLOSE_BRACE> { newLine = true; } ) |
t = <EQUALS> | t = <OPEN_PAREN> | t = <CLOSE_PAREN> |
(t = <SEMI_COLON> { newLine = true; } )
| t = <STRING_LITERAL> | t = <CHARACTER_LITERAL> |
t = <INTEGER_LITERAL> | t = <FLOATING_POINT_LITERAL> |
- (t = <INCLUDE> { newLine = true; } ) |
(t = <DEFINE> { newLine = true; } )
)
{
}
-void Parse(File f, ArrayList<String> content, ArrayList<Construct> constructs) :
+void Parse(File f, ArrayList<String> content, ArrayList<Construct> constructs, ArrayList<String> headers) :
{
Construct inst;
ArrayList<String> code;
_constructs = constructs;
}
((inst = ParseSpec() { _constructs.add(inst); }) |
- ((code = C_CPP_CODE()) { _content.addAll(code); })
+ ((code = C_CPP_CODE(headers)) { _content.addAll(code); })
)* <EOF>
}
SequentialDefineSubConstruct Global_define() :
{
- String declareVar, initVar, defineFunc;
- ArrayList<String> code;
+ ArrayList<String> initVar, defineFunc, code;
+ ArrayList<VariableDeclaration> declareVars;
+ VariableDeclaration declareVar;
+
}
{
{
- declareVar = "";
- initVar = "";
- defineFunc = "";
+ declareVars = null;
+ initVar = null;
+ defineFunc = null;
}
<GLOBAL_DEFINE>
- (<DECLARE_VAR> (code = C_CPP_CODE() { declareVar = stringArray2String(code); } ))?
- (<INIT_VAR> (code = C_CPP_CODE() { initVar = stringArray2String(code); } ))?
- (<DEFINE_FUNC> (code = C_CPP_CODE() { defineFunc = stringArray2String(code); }))?
+ (<DECLARE_VAR> ((declareVar = TypeParam() ";" {
+ declareVars.add(declareVar); } )*))?
+ (<INIT_VAR> (code = C_CPP_CODE(null) { initVar = code; } ))?
+ (<DEFINE_FUNC> (code = C_CPP_CODE(null) { defineFunc = code; }))?
{
- SequentialDefineSubConstruct res = new SequentialDefineSubConstruct(declareVar, initVar, defineFunc);
+ SequentialDefineSubConstruct res = new
+ SequentialDefineSubConstruct(declareVars, initVar, defineFunc);
//System.out.println(res);
return res;
}
InterfaceConstruct Interface() :
{
InterfaceConstruct res;
- String interfaceName, condition, idCode, check, postAction,
+ String interfaceName, condition, idCode, check,
postCheck, commitPoint, hbLabel, hbCondition;
- ActionSubConstruct action;
ArrayList<String> commitPointSet;
+ ArrayList<String> action, postAction;
HashMap<String, String> hbConditions;
ArrayList<String> content;
}
condition = "";
idCode = "";
check = "";
- postAction = "";
postCheck = "";
commitPointSet = new ArrayList<String>();
hbConditions = new HashMap<String, String>();
+
+ action = null;
+ postAction = null;
}
<BEGIN>
<INTERFACE> (interfaceName = <IDENTIFIER>.image)
}
)*
- (<CONDITION> (content = C_CPP_CODE() { condition = stringArray2String(content); }))?
+ (<CONDITION> (content = C_CPP_CODE(null) { condition = stringArray2String(content); }))?
(
<HB_CONDITION>
(hbLabel = <IDENTIFIER>.image)
- (content = C_CPP_CODE() { hbCondition = stringArray2String(content); })
+ (content = C_CPP_CODE(null) { hbCondition = stringArray2String(content); })
{
if (hbConditions.containsKey(hbLabel)) {
throw new ParseException(interfaceName + " has" +
hbConditions.put(hbLabel, hbCondition);
}
)*
- (<ID> (content = C_CPP_CODE() { idCode = stringArray2String(content); }))?
- (<CHECK> (content = C_CPP_CODE() { check = stringArray2String(content); }))?
- (action = Action())?
- (<POST_ACTION> (content = C_CPP_CODE() { postAction = stringArray2String(content); }))?
- (<POST_CHECK> (content = C_CPP_CODE() { postCheck = stringArray2String(content); }))?
+ (<ID> (content = C_CPP_CODE(null) { idCode = stringArray2String(content); }))?
+ (<CHECK> (content = C_CPP_CODE(null) { check = stringArray2String(content); }))?
+ (<ACTION> action = C_CPP_CODE(null))?
+ (<POST_ACTION> (postAction = C_CPP_CODE(null) ))?
+ (<POST_CHECK> (content = C_CPP_CODE(null) { postCheck = stringArray2String(content); }))?
<END>
{
res = new InterfaceConstruct(_file, _content.size(), interfaceName, commitPointSet, condition,
}
}
-ActionSubConstruct Action() :
-{
- String type, name, expr, defineVarStr, code;
- ArrayList<DefineVar> defineVars;
- ArrayList<String> content;
-}
-{
- {
- defineVars = new ArrayList<DefineVar>();
- code = "";
- }
- <ACTION>
- (
- (
- (<DEFINEVAR> (content = C_CPP_CODE() { defineVarStr = stringArray2String(content); })
- {
- int eqIdx = defineVarStr.indexOf('=');
- int typeEnd = defineVarStr.lastIndexOf(' ', eqIdx - 2);
- type = defineVarStr.substring(0, typeEnd);
- name = defineVarStr.substring(typeEnd + 1, eqIdx - 1);
- expr = defineVarStr.substring(eqIdx + 2);
- DefineVar defineVar = new DefineVar(type, name, expr);
- defineVars.add(defineVar);
- })* (<CODE> (content = C_CPP_CODE() { code = stringArray2String(content); }))? )
- )
-
- {
- ActionSubConstruct res = new ActionSubConstruct(defineVars, code);
- return res;
- }
-}
PotentialCPDefineConstruct Potential_commit_point_define() :
{
{ res = null; }
<BEGIN>
- <POTENTIAL_COMMIT_POINT_DEFINE> (content = C_CPP_CODE() { condition = stringArray2String(content); })
+ <POTENTIAL_COMMIT_POINT_DEFINE> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
<LABEL> (label = <IDENTIFIER>.image)
<END>
{
{ res = null; }
<BEGIN>
- <COMMIT_POINT_DEFINE> (content = C_CPP_CODE() { condition = stringArray2String(content); })
+ <COMMIT_POINT_DEFINE> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
<POTENTIAL_COMMIT_POINT_LABEL> (potentialCPLabel = <IDENTIFIER>.image)
<LABEL> (label = <IDENTIFIER>.image)
<END>
{ res = null; }
<BEGIN>
- <COMMIT_POINT_DEFINE_CHECK> (content = C_CPP_CODE() { condition = stringArray2String(content); })
+ <COMMIT_POINT_DEFINE_CHECK> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
<LABEL> (label = <IDENTIFIER>.image)
<END>
{
****** Example1: ******
Global Variable Declaration
-
/* Include all the header files that contains the interface declaration */
#include <iostream>
#inlcude <atomic>
// Action
PUT_ACTION
- /* DefineVars */
- TypeV *_Old_Val = DefineVarExpr;
-
// Post_check
check_passed = PUT_POST_CHECK_EXPRESSION;
if (!check_passed)
hb_init0.annotation = &hbConditionInit0;
cdsannotate(SPEC_ANALYSIS, &hb_init0);
}
+/* End of Global construct generation in class */
-#endif /* End of
+/* The following static field declaration is necessary for class */
+template <typename T>
+bool CLASS<T>::lock_acquired;
+
+template <typename T>
+int CLASS<T>::reader_lock_cnt;
+/* End of static field definition */
****** Example2: ******
TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
{
- thrd_t tid = thrd_current();
- uint64_t call_sequence_num = current(&__sequential.global_call_sequence);
- next(&__sequential.global_call_sequence);
- put(&__sequential.interface_call_sequence, tid, call_sequence_num);
-
// Interface begins
- anno_interface_boundary interface_boundary;
- interface_boundary.interface_num = 0; // Interface number
- interface_boundary.call_sequence_num = call_sequence_num;
+ anno_interface_begin interface_begin;
+ interface_begin.interface_num = 0; // Interface number
spec_annotation annotation_interface_begin;
annotation_interface_begin.type = INTERFACE_BEGIN;
- annotation_interface_begin.annotation = &interface_boundary;
+ annotation_interface_begin.annotation = &interface_begin;
cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
anno_hb_condition hb_condition1;
hb_condition1.interface_num = 0; // Interface number
hb_condition1.hb_condition_num = 1; // HB condition number
- hb_condition1.id = __ID__;
- hb_condition1.call_sequence_num = call_sequence_num;
spec_annotation annotation_hb_condition;
annotation_hb_condition.type = HB_CONDITION;
annotation_hb_condition.annotation = &hb_condition;
cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
- // And more (if any)
}
+ // And more (if any)
// Interface ends
spec_annotation annotation_interface_end;
+ INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info));
+ info->__RET__ = __RET__;
+ info->arg1 = arg1;
+ info->arg2 = arg2;
+ anno_interface_end interface_end;
+ interface_end.interface_num = 0; // Interface number
+ interface_end.info = info; // Info
annotation_interface_end.type = INTERFACE_END;
- annotation_interface_end.annotation = &interface_boundary;
+ annotation_interface_end.annotation = &interface_end;
cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
}
****** Example3: ******
Potential Commit Point
+
#include <threads.h>
#include <cdstrace.h>
#include <cdsannotate.h>
#include <spec_private_hashtable.h>
-#include <_sepc_sequential_genenrated.h>
+#include <stdint.h>
-// FIXME
-/* Define MACRO */
-#define CAS (__ATOMIC_RET__ = CAS)
-#define LOAD (__ATOMIC_RET__ = LOAD)
-#define RMW (__ATOMIC_RET__ = RMW)
+/* Should add the __ATOMIC_RET__ if necessary */
+uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
-thrd_t tid = thrd_current();
if (POTENTIAL_CP_DEFINE_CONDITION) {
- uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
-
anno_potential_cp_define potential_cp_define;
- potential_cp_define.interface_num = get(&__sequential.interface, tid);
potential_cp_define.label_num = 1; // Commit point label number
- potential_cp_define.call_sequence_num = call_sequence_num;
spec_annotation annotation_potential_cp_define;
annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
annotation_potential_cp_define.annotation = &potential_cp_define;
cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
}
-/* Undefine MACRO */
-#undef CAS
-#undef LOAD
-#undef RMW
****** Example4: ******
Commit Point Define
#include <cdsannotate.h>
#include <spec_private_hashtable.h>
#include <_spec_sequential_generated.h>
+#include <stdint.h>
+
+/* Should add the __ATOMIC_RET__ if necessary */
+uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
-thrd_t __tid = thrd_current();
-int interface_num = get(&__sequential.interface, tid);
/* For all the interface check at this commit point (if there is multiple
* checks here) */
-/* Need to compute the relationship between labels before hand */
-switch (interface_num) {
- case 0:
- // Commit point 3 <=> potentialCP 4
- if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
- if (INTERFACE0_CHECK_CONDITION) {
- check_passed = true;
- }
- /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
- * pointer) */
- /* Unfold all if there are multiple DefineVars */
- Type res0 = Expr;
- put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
- // And more...
-
- /* Compute id; If not defined, assign the default ID */
- int id = INTERFACE0_ID_EXPRESSION;
- put(__sequential.id, tid, id);
-
- /* Execute actions if there's any */
- #define _Old_Val res0;
- INTERFACE0_ACTION; // Unfolded right in place
- #undef _Old_Val
- // And more...
-
- anno_cp_define cp_define;
- uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
- bool check_passed = false;
- cp_define.check_passed = check_passed;
- cp_define.interface_num = interface_num;
- cp_define.label_num = 3;
- cp_define.call_sequence_num = call_sequence_num;
- spec_annotation annotation_cp_define;
- annotation_cp_define.type = CP_DEFINE;
- annotation_cp_define.annotation = &cp_define;
- cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
- }
- break;
- case 1:
- // Commit point 5 <=> potentialCP 6
- if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
- if (INTERFACE1_CHECK_CONDITION) {
- check_passed = true;
- }
- // ...
- // Same as the above case
- }
- break;
- default:
- break;
+// Commit point 3 <=> potentialCP 4
+if (COMMIT_POINT3_CONDITION) {
+ anno_cp_define cp_define;
+ cp_define.label_num = 3;
+ cp_define.potential_cp_label_num = 1;
+ spec_annotation annotation_cp_define;
+ annotation_cp_define.type = CP_DEFINE;
+ annotation_cp_define.annotation = &cp_define;
+ cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
+}
+// More if there are any
+
}
#include <cdsannotate.h>
#include <spec_private_hashtable.h>
#include <_spec_sequential_generated.h>
+#include <stdint.h>
+
+/* Should add the __ATOMIC_RET__ if necessary */
+uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
-thrd_t __tid = thrd_current();
-int interface_num = get(&__sequential.interface, tid);
/* For all the interface check at this commit point (if there is multiple
* checks here) */
-/* Need to compute the relationship between labels before hand */
-switch (interface_num) {
- case 0:
- if (COMMIT_POINT3_CONDITION) {
- if (INTERFACE0_CHECK_CONDITION) {
- check_passed = true;
- }
- /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
- * pointer) */
- /* Unfold all if there are multiple DefineVars */
- Type res0 = Expr;
- put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
- // And more...
-
- /* Compute id; If not defined, assign the default ID */
- int id = INTERFACE0_ID_EXPRESSION;
- put(__sequential.id, tid, id);
-
- /* Execute actions if there's any */
- #define _Old_Val res0;
- INTERFACE0_ACTION; // Unfolded right in place
- #undef _Old_Val
- // And more...
-
- anno_cp_define cp_define;
- uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
- bool check_passed = false;
- cp_define.check_passed = check_passed;
- cp_define.interface_num = interface_num;
- cp_define.label_num = 3;
- cp_define.call_sequence_num = call_sequence_num;
- spec_annotation annotation_cp_define;
- annotation_cp_define.type = CP_DEFINE;
- annotation_cp_define.annotation = &cp_define;
- cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
- }
- break;
- case 1:
- if (COMMIT_POINT5_CONDITION) {
- if (INTERFACE1_CHECK_CONDITION) {
- check_passed = true;
- }
- // ...
- // Same as the above case
- }
- break;
- default:
- break;
+if (COMMIT_POINT3_CONDITION) {
+ anno_cp_define cp_define;
+ uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
+ bool check_passed = false;
+ cp_define.check_passed = check_passed;
+ cp_define.interface_num = interface_num;
+ cp_define.label_num = 3;
+ cp_define.call_sequence_num = call_sequence_num;
+ spec_annotation annotation_cp_define;
+ annotation_cp_define.type = CP_DEFINE;
+ annotation_cp_define.annotation = &cp_define;
+ cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
+}
+// More if there are any
+
}
import java.util.HashMap;
import java.util.Iterator;
-import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
import edu.uci.eecs.specCompiler.specExtraction.IDExtractor;
import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
/**
private File[] srcFiles;
- private HashMap<File, ArrayList<String>> contents;
+ private HashMap<File, SourceFileInfo> srcFilesInfo;
private HashMap<File, ArrayList<CodeAddition>> codeAdditions;
_extractor = new SpecExtractor();
_extractor.extract(srcFiles);
- this.contents = _extractor.contents;
+ this.srcFilesInfo = _extractor.srcFilesInfo;
this.globalContent = null;
this.codeAdditions = new HashMap<File, ArrayList<CodeAddition>>();
- _semantics = new SemanticsChecker(_extractor.constructs);
+ _semantics = new SemanticsChecker(_extractor.getConstructs());
try {
_semantics.check();
System.out.println(_semantics);
}
}
- private ArrayList<String> readSrcFile(File f) throws IOException {
- BufferedReader bf = new BufferedReader(new FileReader(f));
- ArrayList<String> content = new ArrayList<String>();
- String curLine;
- while ((curLine = bf.readLine()) != null) {
- content.add(curLine);
- }
- return content;
- }
-
/**
* <p>
* Generate all the global code, including the "@DefineVar" in each
// Mainly rename and wrap the interface
private void interface2Code(InterfaceConstruct construct)
throws InterfaceWrongFormatException {
- int lineNum = construct.begin + 1;
+ int lineNum = construct.beginLineNum;
+ String funcName = "";
// Rename the interface name
- File file = inst.file;
- String funcDecl = inst.interfaceDeclBody;
+
// Rename the function declaration
- String funcName = renameInterface(inst);
+
// Also rename the function definition if it's separated from the
// declaration
- SpecConstruct definition = _semantics.interfaceName2DefineConstruct
+ InterfaceDefineConstruct definition = (InterfaceDefineConstruct) _semantics.interfaceName2DefineConstruct
.get(construct.name);
if (definition != null) {
String funcDefintionName = renameInterface(definition);
// Generate new wrapper
ArrayList<String> newCode = CodeVariables.generateInterfaceWrapper(
- _semantics, inst);
+ _semantics, construct);
// Add it to the codeAdditions
CodeAddition addition = new CodeAddition(lineNum, newCode);
- if (!codeAdditions.containsKey(inst.file)) {
- codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
+ if (!codeAdditions.containsKey(construct.file)) {
+ codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
}
- codeAdditions.get(inst.file).add(addition);
+ codeAdditions.get(construct.file).add(addition);
}
// Returns the function name that has been renamed and replace the old line
- private String renameInterface(Construct inst)
+ private String renameInterface(Construct construct)
throws InterfaceWrongFormatException {
- String funcDecl = inst.interfaceDeclBody;
- ArrayList<String> content = contents.get(inst.file);
+ String funcDecl = "";
+ ArrayList<String> content = srcFilesInfo.get(construct.file).content;
// Depending on "(" to find the function name, so it doesn't matter if
// there's any template
int lineNumOfID = idExtractor.lineNumOfID();
// Be careful: lineNum - 1 -> index of content array
- content.set(inst.endLineNum + lineNumOfID, newLine);
+ content.set(construct.beginLineNum - 1, newLine);
return funcName;
}
import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
public class CodeVariables {
public static final String HEADER_CDSTRACE = "cdstrace.h";
public static final String CDSAnnotate = "cdsannotate";
public static final String CDSAnnotateType = "SPEC_ANALYSIS";
- public static final String GET_PREV_ATOMIC_VAL = "get_prev_value";
public static final String SPEC_ANNO_TYPE = "spec_anno_type";
public static final String SPEC_ANNO_TYPE_HB_INIT = "HB_INIT";
public static final String SPEC_ANNO_TYPE_INTERFACE_BEGIN = "INTERFACE_BEGIN";
- public static final String SPEC_ANNO_TYPE_POST_CHECK = "POST_CHECK";
public static final String SPEC_ANNO_TYPE_HB_CONDITION = "HB_CONDITION";
public static final String SPEC_ANNO_TYPE_INTERFACE_END = "INTERFACE_END";
public static final String SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE = "POTENTIAL_CP_DEFINE";
public static final String HEADER_SPEC_SEQUENTIAL = "_spec_sequential.h";
public static final String SPEC_SEQUENTIAL_HEADER_MACRO = HEADER_SPEC_SEQUENTIAL
.replace('.', '_').toUpperCase();
- public static final String SPEC_SEQUENTIAL_STRUCT = "Sequential";
- public static final String SPEC_SEQUENTIAL_INSTANCE = "__sequential";
-
- public static final String SPEC_CONDITION = "condition";
- public static final String SPEC_ID = "id";
- public static final String SPEC_INTERFACE = "interface";
- public static final String SPEC_INTERFACE_CALL_SEQUENCE = "interface_call_sequence";
- public static final String SPEC_GLOBAL_CALL_SEQUENCE = "global_call_sequence";
public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
-
- public static final String VAR_ThreadID = "tid";
public static final String VAR_CALL_SEQUENCE_NUM = "call_sequence_num";
// Specification library
public static final String MACRO_RETURN = "__RET__";
public static final String MACRO_ATOMIC_RETURN = "__ATOMIC_RET__";
- // Break the code (String) into multiple lines and add it to newCode
- private static void breakCodeLines(ArrayList<String> newCode, String code) {
- int begin = 0, end = 0;
- while (end < code.length()) {
- if (code.charAt(end) == '\n') {
- String line = code.substring(begin, end);
- newCode.add(line);
- begin = end + 1;
- }
- end++;
- }
- }
-
public static void printCode(ArrayList<String> code) {
for (int i = 0; i < code.size(); i++) {
System.out.println(code.get(i));
}
}
- public static String getFuncName(String funcDecl) {
- int beginIdx = funcDecl.indexOf('(');
- IDExtractor idExtractor = new IDExtractor(funcDecl, beginIdx);
- return idExtractor.getPrevID();
- }
-
- public static String getFuncReturnType(String funcDecl) {
- int beginIdx = funcDecl.indexOf('(');
- IDExtractor idExtractor = new IDExtractor(funcDecl, beginIdx);
- idExtractor.getPrevID();
- int idLineBegin = idExtractor.lineBeginIdxOfID(), idBegin = idExtractor
- .getIDBeginIdx();
- String type = funcDecl.substring(idLineBegin, idBegin);
- return SpecExtractor.trimSpace(type);
- }
-
- public static ArrayList<String> getFuncArgs(String funcDecl) {
- ArrayList<String> args = new ArrayList<String>();
- int beginIdx = funcDecl.indexOf('('), endIdx = funcDecl.indexOf(')');
- IDExtractor idExtractor = new IDExtractor(funcDecl, endIdx);
- String arg = idExtractor.getPrevID();
- // Void argument
- if (arg == null || idExtractor.getIDBeginIdx() < beginIdx) {
- return args;
- } else {
- args.add(arg);
- }
-
- do {
- endIdx = funcDecl.lastIndexOf(',', endIdx);
- if (endIdx == -1) {
- return args;
- }
- idExtractor.reset(endIdx);
- args.add(idExtractor.getPrevID());
- } while (true);
- }
-
private static String COMMENT(String comment) {
return "/* " + comment + " */";
}
- private static String GET(String var) {
- return "get(&" + VAR(var) + ", " + VAR_ThreadID + ")";
- }
-
- private static String PUT(String var, String tid, String val) {
- return "put(&" + VAR(var) + ", " + tid + ", " + val + ");";
- }
-
- private static String INIT(String var) {
- return "init(&" + VAR(var) + ");";
- }
-
private static String INCLUDE(String header) {
return "#include <" + header + ">";
}
return "#undef " + macro;
}
- private static String VAR(String var) {
- return SPEC_SEQUENTIAL_INSTANCE + "." + var;
- }
-
private static String BRACE(String val) {
return "(" + val + ")";
}
- private static String VAR_PTR(String var) {
- return "&" + SPEC_SEQUENTIAL_INSTANCE + "." + var;
- }
-
private static String ASSIGN(String structName, String field, String val) {
return structName + "." + field + " = " + val + ";";
}
newCode.add(INCLUDE(HEADER_SPECANNOTATION));
newCode.add(INCLUDE(HEADER_SPEC_TAG));
newCode.add("");
-
- // Generate all sequential variables into a struct
- newCode.add(COMMENT("Beginning of struct " + SPEC_SEQUENTIAL_STRUCT));
- newCode.add("typedef struct " + SPEC_SEQUENTIAL_STRUCT + " {");
- newCode.add(COMMENT("Condition"));
- newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, SPEC_CONDITION));
- newCode.add(COMMENT("ID"));
- newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, SPEC_ID));
- newCode.add(COMMENT("Current interface call"));
- newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE, SPEC_INTERFACE));
- newCode.add(COMMENT("Current interface call sequence"));
- newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE,
- SPEC_INTERFACE_CALL_SEQUENCE));
- newCode.add(COMMENT("Global interface call sequence number"));
- newCode.add(DECLARE(SPEC_TAG, SPEC_GLOBAL_CALL_SEQUENCE));
- newCode.add("");
- // DefineVar declaration
- for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
- InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
- .get(interfaceName);
- ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
- if (defineVars.size() > 0) {
- newCode.add(COMMENT("DefineVar in " + interfaceName));
- for (int i = 0; i < defineVars.size(); i++) {
- DefineVar var = defineVars.get(i);
- newCode.add(DECLARE(SPEC_PRIVATE_HASHTABLE,
- var.getNewVarName()));
- }
- }
- newCode.add("");
- }
- // Generate user-defined variable declaration
- newCode.add(COMMENT("Beginnint of other user-defined variables"));
- SequentialDefineSubConstruct globalCode = construct.code;
- breakCodeLines(newCode, globalCode.declareVar);
- newCode.add(COMMENT("End of other user-defined variables"));
- // End of struct Sequential
- newCode.add("} " + SPEC_SEQUENTIAL_STRUCT + "; "
- + COMMENT("End of struct " + SPEC_SEQUENTIAL_STRUCT));
-
- // Generate definition of the sequential struct
- newCode.add("");
- newCode.add(COMMENT("Instance of the struct"));
- newCode.add(DECLARE(SPEC_SEQUENTIAL_STRUCT, SPEC_SEQUENTIAL_INSTANCE));
-
- newCode.add("");
- newCode.add(COMMENT("Define function for sequential code initialization"));
- newCode.add("void " + SPEC_SEQUENTIAL_INSTANCE + "_init() {");
- // Internal variables
- newCode.add(COMMENT("Init internal variables"));
- newCode.add(INIT(SPEC_CONDITION));
- newCode.add(INIT(SPEC_ID));
- newCode.add(INIT(SPEC_INTERFACE));
- newCode.add(INIT(SPEC_INTERFACE_CALL_SEQUENCE));
- newCode.add(INIT(SPEC_GLOBAL_CALL_SEQUENCE));
- // Init DefineVars
- newCode.add(COMMENT("Init DefineVars"));
- for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
- InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
- .get(interfaceName);
- ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
- if (defineVars.size() > 0) {
- newCode.add(COMMENT("DefineVar in " + interfaceName));
- for (int i = 0; i < defineVars.size(); i++) {
- DefineVar var = defineVars.get(i);
- newCode.add(INIT(var.getNewVarName()));
- }
- }
- }
- // Init user-defined variables
- newCode.add(COMMENT("Init user-defined variables"));
- breakCodeLines(newCode, globalCode.initVar);
- // Pass the HB initialization
- newCode.add(COMMENT("Pass the happens-before initialization here"));
- newCode.addAll(CodeVariables.generateHBInitAnnotation(semantics));
- // End of init the function
- newCode.add("} " + COMMENT("End of init function"));
-
- // Generate the user-defined sequential functions
- newCode.add("");
- newCode.add(COMMENT("All other user-defined functions"));
- breakCodeLines(newCode, globalCode.defineFunc);
-
- // The end
- newCode.add("");
- newCode.add("#endif " + SPEC_SEQUENTIAL_HEADER_MACRO + "\t"
- + COMMENT("End of " + HEADER_SPEC_SEQUENTIAL));
+
+
// printCode(newCode);
return newCode;
public static ArrayList<String> generateInterfaceWrapper(
SemanticsChecker semantics, InterfaceConstruct construct) {
ArrayList<String> newCode = new ArrayList<String>();
- String funcDecl = construct.interfaceDeclBody.substring(0,
- construct.interfaceDeclBody.indexOf(')') + 1);
- String returnType = getFuncReturnType(funcDecl), funcName = getFuncName(funcDecl), renamedFuncName = SPEC_INTERFACE_WRAPPER
- + funcName;
- ArrayList<String> args = getFuncArgs(funcDecl);
// Generate necessary header file (might be redundant but never mind)
- newCode.add(COMMENT("Automatically generated code for interface: "
- + construct.name));
- newCode.add(COMMENT("Include redundant headers"));
- newCode.add(INCLUDE(HEADER_THREADS));
- newCode.add(INCLUDE(HEADER_CDSANNOTATE));
- newCode.add(INCLUDE(HEADER_SPECANNOTATION));
- newCode.add(INCLUDE(HEADER_SPEC_TAG));
- newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE));
- newCode.add("");
+
// Generate wrapper header
- newCode.add(COMMENT("Wrapper for " + SPEC_INTERFACE_WRAPPER + funcName));
- breakCodeLines(newCode, funcDecl);
- newCode.add("{");
+
// Wrapper function body
- newCode.add(DECLARE_DEFINE(ThreadIDType, VAR_ThreadID, GET_THREAD_ID
- + BRACE("")));
- newCode.add(DECLARE_DEFINE(UINT64, VAR_CALL_SEQUENCE_NUM,
- SPEC_TAG_CURRENT + BRACE(VAR_PTR(SPEC_GLOBAL_CALL_SEQUENCE))));
- newCode.add(SPEC_TAG_NEXT + BRACE(VAR_PTR(SPEC_GLOBAL_CALL_SEQUENCE)));
- newCode.add(PUT(SPEC_INTERFACE_CALL_SEQUENCE, VAR_ThreadID,
- VAR_CALL_SEQUENCE_NUM));
+
// Interface begin
- newCode.add("");
- newCode.add(COMMENT("Interface begin"));
- String interfaceName = construct.name;
- String annoStruct = "interface_boundary", interfaceNum = Integer
- .toString(semantics.interface2Num.get(interfaceName));
- newCode.add(DECLARE(ANNO_INTERFACE_BOUNDARY, annoStruct));
- newCode.add(ASSIGN(annoStruct, "interface_num", interfaceNum));
- newCode.add(ASSIGN(annoStruct, "call_sequence_num",
- VAR_CALL_SEQUENCE_NUM));
- String anno = "annotation_interface_begin";
- newCode.add(DECLARE(SPEC_ANNOTATION, anno));
- newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
- SPEC_ANNO_TYPE_INTERFACE_BEGIN));
- newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
- newCode.add(ANNOTATE(anno));
+
// Call original renamed function
- String funcCall = renamedFuncName + "(";
- if (args.size() == 0) {
- funcCall = funcCall + ")";
- } else {
- funcCall = funcCall + args.get(0);
- for (int i = 1; i < args.size(); i++) {
- funcCall = funcCall + ", " + args.get(i);
- }
- funcCall = funcCall + ")";
- }
- newCode.add(DECLARE_DEFINE(returnType, MACRO_RETURN, funcCall));
- newCode.add(DECLARE_DEFINE("int", MACRO_COND, GET(SPEC_CONDITION)));
- newCode.add(DECLARE_DEFINE(UINT64, MACRO_ID, GET(SPEC_ID)));
- // Post check & action
- newCode.add("");
- newCode.add(COMMENT("Post_check action, define macros for all DefineVars"));
- // Define all DefineVar macro
- ArrayList<DefineVar> defineVars = construct.action.defineVars;
- for (int i = 0; i < defineVars.size(); i++) {
- DefineVar var = defineVars.get(i);
- newCode.add(DEFINE(var.varName, BRACE(GET(interfaceName + "_"
- + var.varName))));
- }
- // Post check
- newCode.add(DECLARE_DEFINE("bool", "post_check_passed",
- construct.postCheck));
- annoStruct = "post_check";
- newCode.add(DECLARE(ANNO_POST_CHECK, annoStruct));
- newCode.add(ASSIGN(annoStruct, "check_passed", "post_check_passed"));
- newCode.add(ASSIGN(annoStruct, "interface_num", interfaceNum));
- newCode.add(ASSIGN(annoStruct, "call_sequence_num",
- VAR_CALL_SEQUENCE_NUM));
- anno = "annotation_post_check";
- newCode.add(DECLARE(SPEC_ANNOTATION, anno));
- newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
- SPEC_ANNO_TYPE_POST_CHECK));
- newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
- newCode.add(ANNOTATE(anno));
- // Post action if any
- breakCodeLines(newCode, construct.postAction);
- // Undefine all DefineVar macro
- for (int i = 0; i < defineVars.size(); i++) {
- DefineVar var = defineVars.get(i);
- newCode.add(UNDEFINE(var.varName));
- }
+
// HB conditions
- newCode.add("");
- for (String label : construct.hbConditions.keySet()) {
- String hbCondition = construct.hbConditions.get(label);
- newCode.add(COMMENT("Happens-before condition for " + label
- + " ::= " + hbCondition));
- newCode.add("if " + BRACE(hbCondition) + " {");
- String hbNum = Integer.toString(semantics.hbLabel2Num.get(label));
- annoStruct = "hb_condition" + hbNum;
- newCode.add(DECLARE(ANNO_HB_CONDITION, annoStruct));
- newCode.add(ASSIGN(annoStruct, "interface_num", interfaceNum));
- newCode.add(ASSIGN(annoStruct, "hb_condition_num", hbNum));
- newCode.add(ASSIGN(annoStruct, "id", MACRO_ID));
- newCode.add(ASSIGN(annoStruct, "call_sequence_num",
- VAR_CALL_SEQUENCE_NUM));
- anno = "annotation_hb_condition";
- newCode.add(DECLARE(SPEC_ANNOTATION, anno));
- newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
- SPEC_ANNO_TYPE_HB_CONDITION));
- newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
- ANNOTATE(anno);
- newCode.add("} " + COMMENT("End of HB condition " + label));
- newCode.add("");
- }
+
+
// Interface end
- annoStruct = "interface_boundary";
- anno = "annotation_interface_end";
- newCode.add(DECLARE(SPEC_ANNOTATION, anno));
- newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
- SPEC_ANNO_TYPE_INTERFACE_END));
- newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
- newCode.add(ANNOTATE(anno));
+
// End of the wrapper function
- newCode.add("} "
- + COMMENT("End of automatically generated code for interface wrapper"));
+
- printCode(newCode);
+// printCode(newCode);
return newCode;
}
newCode.add(INCLUDE(HEADER_SPEC_SEQUENTIAL));
newCode.add("");
// Some necessary function calls
- newCode.add(DECLARE_DEFINE(ThreadIDType, VAR_ThreadID, GET_THREAD_ID
- + BRACE("")));
- newCode.add(DECLARE_DEFINE(UINT64, MACRO_ATOMIC_RETURN,
- GET_PREV_ATOMIC_VAL + BRACE(VAR_ThreadID)));
- newCode.add("if " + BRACE(construct.condition) + " {");
- newCode.add(DECLARE_DEFINE(UINT64, VAR_CALL_SEQUENCE_NUM,
- GET(SPEC_INTERFACE_CALL_SEQUENCE)));
- String annoStruct = "potential_cp_define";
- newCode.add(DECLARE(ANNO_POTENTIAL_CP_DEFINE, annoStruct));
- newCode.add(ASSIGN(annoStruct, "interface_num", GET(SPEC_INTERFACE)));
- String labelNum = Integer.toString(semantics.commitPointLabel2Num
- .get(construct.label));
- newCode.add(ASSIGN(annoStruct, "label_num", labelNum));
- newCode.add(ASSIGN(annoStruct, "call_sequence_num",
- VAR_CALL_SEQUENCE_NUM));
- String anno = "annotation_potential_cp_define";
- newCode.add(DECLARE(SPEC_ANNOTATION, anno));
- newCode.add(ASSIGN(anno, SPEC_ANNOTATION_FIELD_TYPE,
- SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE));
- newCode.add(ASSIGN_PTR(anno, SPEC_ANNOTATION_FIELD_ANNO, annoStruct));
- ANNOTATE(anno);
-
- newCode.add("} "
- + COMMENT("End of automatically generated code for potential commit point"));
+
return newCode;
}
import java.util.HashMap;
import java.util.HashSet;
-import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
public final HashMap<String, Construct> interfaceName2Construct;
public final HashMap<String, Construct> interfaceName2DefineConstruct;
public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
- public final HashSet<DefineVar> defineVars;
public final HashMap<String, Integer> interface2Num;
public final HashMap<String, Integer> hbLabel2Num;
this.interfaceName2Construct = new HashMap<String, Construct>();
this.interfaceName2DefineConstruct = new HashMap<String, Construct>();
this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
- this.defineVars = new HashSet<DefineVar>();
this.entryPointConstruct = null;
this.interface2Num = new HashMap<String, Integer>();
interface2Num.put(iConstruct.name, _interfaceNum++);
interfaceName2Construct.put(iConstruct.name, constructs.get(i));
- for (int j = 0; j < iConstruct.action.defineVars.size(); j++) {
- DefineVar var = iConstruct.action.defineVars.get(j);
- var.renameVarName("__" + iConstruct.name + "_"
- + var.varName + "__");
- }
for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
String label = iConstruct.commitPointSet.get(j);
+++ /dev/null
-package edu.uci.eecs.specCompiler.specExtraction;
-
-import java.util.ArrayList;
-
-public class ActionSubConstruct {
- public static class DefineVar {
- public final String varType;
- public final String varName;
- public final String varExpr;
- private String newVarName;
-
- public DefineVar(String varType, String varName, String varExpr) {
- this.varType = varType;
- this.varName = varName;
- this.varExpr = varExpr;
- this.newVarName = null;
- }
-
- public void renameVarName(String newName) {
- this.newVarName = newName;
- }
-
- public String getNewVarName() {
- return this.newVarName;
- }
-
- public String toString() {
- if (newVarName == null)
- return varType + " " + varName + " = " + varExpr;
- else
- return varType + " " + varName + "(" + newVarName + ")" + " = "
- + varExpr;
- }
- }
-
- public final ArrayList<DefineVar> defineVars;
- public final String code;
-
- public ActionSubConstruct(ArrayList<DefineVar> defineVars, String code) {
- this.code = code;
- this.defineVars = defineVars;
- }
-
- public void addDefineVar(DefineVar defineVar) {
- defineVars.add(defineVar);
- }
-
- public String toString() {
- StringBuilder sb = new StringBuilder();
- sb.append("@Action:\n");
- for (DefineVar defineVar : defineVars) {
- sb.append("\t@DefineVar: " + defineVar + "\n");
- }
- sb.append("\t@Code: " + code);
- return sb.toString();
- }
-}
abstract public class Construct {
public final File file;
public final int beginLineNum;
- public final String interfaceDeclBody;
public Construct(File file, int beginLineNum) {
this.file = file;
this.beginLineNum = beginLineNum;
- this.interfaceDeclBody = "";
- }
-
- public Construct(File file, int beginLineNum, String interfaceDeclBody) {
- this.file = file;
- this.beginLineNum = beginLineNum;
- this.interfaceDeclBody = interfaceDeclBody;
}
}
public class FunctionHeader {
public final String returnType;
- public final String qualifiedName;
- public final String bareFuncName;
- public final ArrayList<String> args;
+ public final QualifiedName qualifiedName;
+ public final ArrayList<VariableDeclaration> args;
- public FunctionHeader(String returnType, String qualifiedName,
- String bareFuncName, ArrayList<String> args) {
+ public FunctionHeader(String returnType, QualifiedName qualifiedName,
+ ArrayList<VariableDeclaration> args) {
this.returnType = returnType;
this.qualifiedName = qualifiedName;
- this.bareFuncName = bareFuncName;
this.args = args;
}
public String toString() {
- return "Ret: " + returnType + "\n" + qualifiedName + "\t"
- + bareFuncName + "\n" + args;
+ return "Ret: " + returnType + "\n" + qualifiedName + "\n" + args;
}
}
public final HashMap<String, String> hbConditions;
public final String idCode;
public final String check;
- public final ActionSubConstruct action;
- public final String postAction;
+ public final ArrayList<String> action;
+ public final ArrayList<String> postAction;
public final String postCheck;
public InterfaceConstruct(File file, int beginLineNum, String name,
ArrayList<String> commitPointSet, String condition,
HashMap<String, String> hbConditions, String idCode, String check,
- ActionSubConstruct action, String postAction, String postCheck) {
+ ArrayList<String> action, ArrayList<String> postAction, String postCheck) {
super(file, beginLineNum);
this.name = name;
this.commitPointSet = commitPointSet;
sb.append("@ID: ");
sb.append(idCode + "\n");
sb.append("@Check: " + check + "\n");
- sb.append(action + "\n");
+ sb.append(ParserUtils.array2Str(action));
sb.append("@Post_action:\n");
- sb.append(postAction + "\n");
+ sb.append(ParserUtils.array2Str(postAction));
sb.append("@Post_check: " + postCheck + "\n");
return sb.toString();
import java.util.ArrayList;
-import edu.uci.eecs.specCompiler.codeGenerator.InterfaceWrongFormatException;
-
public class ParserUtils {
public static String trimSpace(String line) {
int i, j;
else
return line.substring(i, j + 1);
}
+
+ public static String array2Str(ArrayList code) {
+ StringBuilder sb = new StringBuilder();
+ for (int i = 0; i < code.size(); i++) {
+ sb.append(code.get(i) + "\n");
+ }
+ return sb.toString();
+ }
}
--- /dev/null
+package edu.uci.eecs.specCompiler.specExtraction;
+
+public class QualifiedName {
+ public final String fullName;
+ public final String bareName;
+
+ public QualifiedName(String fullName) {
+ this.fullName = fullName;
+ this.bareName = getBareName();
+ }
+
+ private String getBareName() {
+ int beginIdx, endIdx;
+ beginIdx = fullName.lastIndexOf(':');
+ if (beginIdx == -1)
+ return fullName;
+ else
+ return fullName.substring(beginIdx + 1);
+ }
+
+ public String toString() {
+ return fullName + "\n" + bareName;
+ }
+}
package edu.uci.eecs.specCompiler.specExtraction;
+import java.util.ArrayList;
+
public class SequentialDefineSubConstruct {
- public final String declareVar;
- public final String initVar;
- public final String defineFunc;
-
- public SequentialDefineSubConstruct(String declareVar, String initVar, String defineFunc) {
+ public final ArrayList<String> initVar, defineFunc;
+ public final ArrayList<VariableDeclaration> declareVar;
+
+ public SequentialDefineSubConstruct(ArrayList<VariableDeclaration> declareVar,
+ ArrayList<String> initVar, ArrayList<String> defineFunc) {
this.declareVar = declareVar;
this.initVar = initVar;
this.defineFunc = defineFunc;
}
-
+
public String toString() {
StringBuffer res = new StringBuffer();
res.append("@Sequential_define:\n");
- res.append("\t@DeclareVar:\n");
- res.append(declareVar);
- res.append("\t@InitVar:\n");
- res.append(initVar);
- res.append("\t@DefineFunc:\n");
- res.append(defineFunc);
+ res.append("@DeclareVar:\n");
+ res.append(ParserUtils.array2Str(declareVar));
+ res.append("@InitVar:\n");
+ res.append(ParserUtils.array2Str(initVar));
+ res.append("@DefineFunc:\n");
+ res.append(ParserUtils.array2Str(defineFunc));
return res.toString();
}
}
--- /dev/null
+package edu.uci.eecs.specCompiler.specExtraction;
+
+import java.io.File;
+import java.util.ArrayList;
+
+public class SourceFileInfo {
+ public final File file;
+ public final ArrayList<String> content;
+ public final ArrayList<String> headers;
+ public final ArrayList<Construct> constructs;
+
+ public SourceFileInfo(File file, ArrayList<String> content,
+ ArrayList<String> headers, ArrayList<Construct> constructs) {
+ this.file = file;
+ this.content = content;
+ this.headers = headers;
+ this.constructs = constructs;
+ }
+
+ public boolean equals(Object o) {
+ if (!(o instanceof SourceFileInfo))
+ return false;
+ SourceFileInfo another = (SourceFileInfo) o;
+ return another.file.equals(file);
+ }
+}
import java.io.LineNumberReader;
import java.util.ArrayList;
import java.util.HashMap;
+import java.util.HashSet;
import edu.uci.eecs.specCompiler.grammerParser.ParseException;
import edu.uci.eecs.specCompiler.grammerParser.SpecParser;
*
*/
public class SpecExtractor {
- public final ArrayList<Construct> constructs;
-
- public final HashMap<File, ArrayList<String>> contents;
-
+ public final HashMap<File, SourceFileInfo> srcFilesInfo;
public SpecExtractor() {
- constructs = new ArrayList<Construct>();
- contents = new HashMap<File, ArrayList<String>>();
+ srcFilesInfo = new HashMap<File, SourceFileInfo>();
+ }
+
+ public ArrayList<Construct> getConstructs() {
+ ArrayList<Construct> constructs = new ArrayList<Construct>();
+ for (File f : srcFilesInfo.keySet()) {
+ constructs.addAll(srcFilesInfo.get(f).constructs);
+ }
+ return constructs;
}
/**
}
public void extract(File file) {
- if (contents.containsKey(file))
+ if (srcFilesInfo.containsKey(file))
return;
- ArrayList<String> content = new ArrayList<String>();
- ArrayList<Construct> localConstructs = new ArrayList<Construct>();
+ SourceFileInfo srcFileInfo;
try {
- SpecParser.ParseFile(file, content, localConstructs);
- contents.put(file, content);
- constructs.addAll(localConstructs);
+ srcFileInfo = SpecParser.ParseFile(file);
+ srcFilesInfo.put(file, srcFileInfo);
} catch (ParseException e) {
e.printStackTrace();
} catch (TokenMgrError e) {
--- /dev/null
+package edu.uci.eecs.specCompiler.specExtraction;
+
+public class VariableDeclaration {
+ public String type;
+ public String name;
+
+ public VariableDeclaration(String type, String name) {
+ this.type = type;
+ this.name = name;
+ }
+
+ public String toString() {
+ return type + " " + name;
+ }
+}
--- /dev/null
+# include <stdio.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+int main() {
+ uint64_t i64 = (uint64_t) NULL;
+ if (i64)
+ printf("True\n");
+ return 1;
+}
+++ /dev/null
-#include <stdio.h>
-#include <stdlib.h>
-//#include "test.h"
-
-typedef void (*action_t)();
-
-void bar() {
- printf("In bar\n");
-}
-
-template <typename T, action_t val, int b>
-class Class {
- public:
- static T arr;
- struct A {
- int &a;
- };
-
- static void action() {
- printf("%d\n", arr);
- }
-
- action_t getFuncPtr() {
- foo();
- action();
- return &Class::action;
- }
-
- static void foo() {
-
- }
-
- static void init() {
- action_t inst1 = &foo;
- int a = (1, 2);
- }
-
- Class() {
- //ar = T((int)val);
- (*val)();
- //foo();
- }
-};
-
-#include "test.h"
-
-int main() {
- Class<int> c;
- action_t f_ptr = c.getFuncPtr();
- //cc.getFuncPtr();
- return 1;
-}
-
#ifndef _TEST_H
#define _TEST_H
-template <typename T, action_t a, int b>
-T Class<T, a, b>::arr;
#endif
projects / cdsspec-compiler.git / commitdiff