map = spec_hashtable<TypeK, TypeV*>();
id_map = spec_hashtable<TypeK, TypeV*>();
tag = Tag();
- @DefineFunc:
static bool equals_val(TypeV *ptr1, TypeV *ptr2) {
// ...
}
@Commit_point_set: Read_Val_Point1 | Read_Val_Point2 | Read_Val_Point3
@ID: __sequential.getKeyTag(key)
@Action:
- @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
+ TypeV *_Old_Val = __sequential.map.get(key)
@Post_check:
__sequential.equals_val(_Old_Val, __RET__)
@End
@ID: __sequential.getKeyTag(key)
@Action:
# Remember this old value at checking point
- @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
- @Code: __sequential.map.put(key, &val);
+ TypeV *_Old_Val = __sequential.map.get(key)
+ __sequential.map.put(key, &val);
@Post_check:
__sequential.equals_val(__RET__, _Old_Val)
@End
COND_PutIfAbsentSucc :: __RET__ == NULL
@ID: __sequential.getKeyTag(key)
@Action:
- @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
- @Code:
+ TypeV *_Old_Val = __sequential.map.get(key)
if (__COND_SAT__)
__sequential.map.put(key, &value);
@Post_check:
@Commit_point_set: Write_Val_Point
@ID: __sequential.getKeyTag(key)
@Action:
- @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
- @Code: __sequential.map.put(key, NULL);
+ TypeV *_Old_Val = __sequential.map.get(key)
+ __sequential.map.put(key, NULL);
@Post_check:
__sequential.equals_val(__RET__, _Old_Val)
@End
COND_RemoveIfMatchSucc :: __RET__ == true
@ID: __sequential.getKeyTag(key)
@Action:
- @Code:
if (__COND_SAY__)
__sequential.map.put(key, NULL);
@Post_check:
Write_Val_Point
@ID: __sequential.getKeyTag(key)
@Action:
- @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
+ TypeV *_Old_Val = __sequential.map.get(key)
@Post_check:
__sequential.equals_val(__RET__, _Old_Val)
@End
COND_ReplaceIfMatchSucc :: __RET__ == true
@ID: __sequential.getKeyTag(key)
@Action:
- @Code:
if (__COND_SAY__)
__sequential.map.put(key, &newval);
@Post_check:
@InitVar:
writer_lock_acquired = false;
reader_lock_cnt = 0;
- @DefineFunc:
@Happens_before:
# Since commit_point_set has no ID attached, A -> B means that for any B,
# the previous A happens before B.
@Commit_point_set:
Read_Lock_Success_1 | Read_Lock_Success_2
@Check:
- !__sequential.writer_lock_acquired
+ !writer_lock_acquired
@Action:
- @Code:
- __sequential.reader_lock_cnt++;
+ reader_lock_cnt++;
@End
*/
static inline void read_lock(rwlock_t *rw)
@Commit_point_set:
Write_Lock_Success_1 | Write_Lock_Success_2
@Check:
- !__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
+ !writer_lock_acquired && reader_lock_cnt == 0
@Action:
- @Code:
- __sequential.writer_lock_acquired = true;
+ writer_lock_acquired = true;
@End
*/
static inline void write_lock(rwlock_t *rw)
@Commit_point_set:
Read_Trylock_Point
@Condition:
- __sequential.writer_lock_acquired == false
+ writer_lock_acquired == false
@HB_condition:
HB_Read_Trylock_Succ :: __RET__ == 1
@Action:
- @Code:
- if (__COND_SAY__)
- __sequential.reader_lock_cnt++;
+ if (__COND_SAT__)
+ reader_lock_cnt++;
@Post_check:
- __COND_SAY__ ? __RET__ == 1 : __RET__ == 0
+ __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
@End
*/
static inline int read_trylock(rwlock_t *rw)
@Commit_point_set:
Write_Trylock_Point
@Condition:
- !__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
+ !writer_lock_acquired && reader_lock_cnt == 0
@HB_condition:
HB_Write_Trylock_Succ :: __RET__ == 1
@Action:
- @Code:
- if (__COND_SAY__)
- __sequential.writer_lock_acquired = true;
+ if (__COND_SAT__)
+ writer_lock_acquired = true;
@Post_check:
- __COND_SAY__ ? __RET__ == 1 : __RET__ == 0
+ __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
@End
*/
static inline int write_trylock(rwlock_t *rw)
@Interface: Read_Unlock
@Commit_point_set: Read_Unlock_Point
@Check:
- __sequential.reader_lock_cnt > 0 && !__sequential.writer_lock_acquired
+ reader_lock_cnt > 0 && !writer_lock_acquired
@Action:
- @Code:
reader_lock_cnt--;
@End
*/
@Check:
reader_lock_cnt == 0 && writer_lock_acquired
@Action:
- @Code:
- __sequential.writer_lock_acquired = false;
+ writer_lock_acquired = false;
@End
*/
-void enqueue(queue_t *q, unsigned int val)
+/**
+@Begin
+ @Options:
+ LANG = C;
+ CLASS = cliffc_hashtable;
+ @Global_define:
+ @DeclareVar:
+ spec_hashtable<TypeK, TypeV*> map;
+ spec_hashtable<TypeK, Tag> id_map;
+ Tag tag;
+ @InitVar:
+ map = spec_hashtable<TypeK, TypeV*>();
+ id_map = spec_hashtable<TypeK, TypeV*>();
+ tag = Tag();
+ @DefineFunc:
+ static bool equals_val(TypeV *ptr1, TypeV *ptr2) {
+ // ...
+ }
+
+ # Update the tag for the current key slot if the corresponding tag
+ # is NULL, otherwise just return that tag. It will update the next
+ # available tag too if it requires a new tag for that key slot.
+ static Tag getKeyTag(TypeK &key) {
+ if (id_map.get(key) == NULL) {
+ Tag cur_tag = tag.current();
+ id_map.put(key, cur_tag);
+ tag.next();
+ return cur_tag;
+ } else {
+ return id_map.get(key);
+ }
+ }
+
+ @Interface_cluster:
+ Read_interface = {
+ Get,
+ PutIfAbsent,
+ RemoveAny,
+ RemoveIfMatch,
+ ReplaceAny,
+ ReplaceIfMatch
+ }
+
+ Write_interface = {
+ Put,
+ PutIfAbsent(COND_PutIfAbsentSucc),
+ RemoveAny,
+ RemoveIfMatch(COND_RemoveIfMatchSucc),
+ ReplaceAny,
+ ReplaceIfMatch(COND_ReplaceIfMatchSucc)
+ }
+ @Happens_before:
+ Write_interface -> Read_interface
+ @End
+ */
public static String stringArray2String(ArrayList<String> content) {
StringBuilder sb = new StringBuilder();
+ if (content.size() == 1)
+ return content.get(0);
for (int i = 0; i < content.size(); i++) {
sb.append(content.get(i) + "\n");
}
<UNSIGNED: "unsigned">
|
<TEMPLATE: "template">
+|
+ <INLINE: "inline">
+|
+ <STATIC: "static">
|
<#DIGIT: ["0"-"9"]>
|
{
System.out.println(func);
}
-
}
}
{
(str = <IDENTIFIER>.image {res = str;})
- ("<" str = <IDENTIFIER>.image { res = res + "<" + str; }
- ("," str = <IDENTIFIER>.image { res = res + ", " + str; })* ">"
+ ("<" str = Type() { res = res + "<" + str; }
+ ("," str = Type() { res = res + ", " + str; })* ">"
{ res = res + ">"; }
)?
{
ArrayList<VariableDeclaration> args;
}
{
+ (<STATIC> | <INLINE>)*
ret = Type()
funcName = ParseQualifiedName()
args = FormalParamList()
(
t = <CONST> | t = <STRUCT> | t = <CLASS> | t = <UNSIGNED> |
(t = <TEMPLATE> { inTemplate = true; })|
+ t = <STATIC> | t = <INLINE> |
(t = <INCLUDE>
{
header = t.image;
(t = <DEFINE> { newLine = true; } )
)
{
- text = text + " " + t.image;
+ if (text.equals("")) {
+ text = t.image;
+ } else {
+ text = text + " " + t.image;
+ }
if (newLine) {
content.add(text);
text = "";
newLine = false;
+ inTemplate = false;
}
}
)+
{
hbConditionLabel = "";
}
- interfaceName = <IDENTIFIER>.image (<OPEN_BRACKET> hbConditionLabel =
- <IDENTIFIER>.image <CLOSE_BRACKET>)?
+ interfaceName = <IDENTIFIER>.image (<OPEN_PAREN> hbConditionLabel =
+ <IDENTIFIER>.image <CLOSE_PAREN>)?
{
return new ConditionalInterface(interfaceName, hbConditionLabel);
}
}
{
(clusterName= <IDENTIFIER>.image)
- <EQUALS> <OPEN_PAREN>
+ <EQUALS> <OPEN_BRACE>
(condInterface = Conditional_interface()
{ inst.addInterface2Cluster(clusterName, condInterface); }
)
(<COMMA> condInterface = Conditional_interface()
{ inst.addInterface2Cluster(clusterName, condInterface); }
)*
- <CLOSE_PAREN>
+ <CLOSE_BRACE>
}
void Interface_clusters(GlobalConstruct inst) :
(<CONDITION> (content = C_CPP_CODE(null) { condition = stringArray2String(content); }))?
(
<HB_CONDITION>
- (hbLabel = <IDENTIFIER>.image)
+ (hbLabel = <IDENTIFIER>.image) <DOUBLECOLON>
(content = C_CPP_CODE(null) { hbCondition = stringArray2String(content); })
{
if (hbConditions.containsKey(hbLabel)) {
package edu.uci.eecs.specCompiler.codeGenerator;
import java.util.ArrayList;
+import java.util.Comparator;
public class CodeAddition {
- public static class CodeAdditionComparator<CodeAddition> {
-
- }
+ public static Comparator<CodeAddition> lineNumComparator = new Comparator<CodeAddition>() {
+ public int compare(CodeAddition addition1, CodeAddition addition2) {
+ return addition1.lineNum - addition2.lineNum;
+ }
+ };
public final int lineNum;
public final ArrayList<String> newCode;
import java.io.FileReader;
import java.io.IOException;
import java.util.ArrayList;
+import java.util.Collections;
import java.util.HashMap;
import java.util.Iterator;
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.ParserUtils;
import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
codeAdditions.get(construct.file).add(addition);
}
+ private ArrayList<String> insertAnnotation2Src(
+ ArrayList<CodeAddition> additions, ArrayList<String> content) {
+ int totalSize = content.size();
+ for (int i = 0; i < additions.size(); i++) {
+ totalSize += additions.size();
+ }
+ ArrayList<String> newContent = new ArrayList<String>(totalSize);
+ int curSrcLine = 0;
+ for (int i = 0; i < additions.size(); i++) {
+ CodeAddition addition = additions.get(i);
+ if (curSrcLine < addition.lineNum) {
+ newContent.addAll(content.subList(curSrcLine, addition.lineNum - 1));
+ curSrcLine = addition.lineNum;
+ }
+ newContent.addAll(addition.newCode);
+ }
+ return newContent;
+ }
+
public void generateCode() {
for (int i = 0; i < _semantics.constructs.size(); i++) {
Construct construct = _semantics.constructs.get(i);
CPDefine2Code((CPDefineConstruct) construct);
} else if (construct instanceof CPDefineCheckConstruct) {
CPDefineCheck2Code((CPDefineCheckConstruct) construct);
+ } else if (construct instanceof EntryPointConstruct) {
+ EntryPoint2Code((EntryPointConstruct) construct);
}
}
+ // Sort code additions
+ for (File file : codeAdditions.keySet()) {
+ ArrayList<CodeAddition> additions = codeAdditions.get(file);
+ if (additions.size() == 0) // Simply do nothing, already written
+ // once
+ continue;
+ ArrayList<String> content = _semantics.srcFilesInfo.get(file).content;
+ Collections.sort(additions, CodeAddition.lineNumComparator);
+ // Insert generated annotation to the source files
+ ArrayList<String> newContent = insertAnnotation2Src(additions,
+ content);
+ // Write it back to file
+ ParserUtils.write2File(file, newContent);
+ }
+
}
public static void main(String[] argvs) {
String homeDir = Environment.HOME_DIRECTORY;
File[] srcFiles = {
- // new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"),
- new File(homeDir
- + "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), };
-// new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
-// new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
+ new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+// new File(homeDir
+// + "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), };
+ // new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+ // new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
CodeGenerator gen = new CodeGenerator(srcFiles);
gen.generateCode();
}
public class CodeVariables {
// C++ code or library
+ public static final String HEADER_STDLIB = "<stdlib.h>";
public static final String HEADER_THREADS = "<threads.h>";
public static final String HEADER_STDINT = "<stdint.h>";
public static final String ThreadIDType = "thrd_t";
}
private static ArrayList<String> DEFINE_INFO_STRUCT(String interfaceName,
- FunctionHeader funcDecl) {
+ FunctionHeader header) {
ArrayList<String> code = new ArrayList<String>();
code.add("typedef struct " + interfaceName + "_info {");
- code.add(DECLARE(funcDecl.returnType, MACRO_RETURN));
- for (int i = 0; i < funcDecl.args.size(); i++) {
- code.add(DECLARE(funcDecl.args.get(i)));
+ if (!header.returnType.equals("void")) {
+ code.add(DECLARE(header.returnType, MACRO_RETURN));
+ }
+ for (int i = 0; i < header.args.size(); i++) {
+ code.add(DECLARE(header.args.get(i)));
}
code.add("} " + interfaceName + "_info {");
return code;
code.add("static bool " + interfaceName + "_check_action(void *info, "
+ IDType + " " + MACRO_ID + ") {");
code.add(DECLARE("bool", "check_passed"));
- String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
- code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
- BRACE(infoStructType) + "info"));
- code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
- GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
- for (int i = 0; i < header.args.size(); i++) {
- String type = header.args.get(i).type, var = header.args.get(i).name;
- code.add((DECLARE_DEFINE(type, var,
- GET_FIELD_BY_PTR(infoStructName, var))));
+ // Read info struct
+ if (!header.returnType.equals("void") || header.args.size() != 0) {
+ String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
+ code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
+ BRACE(infoStructType) + "info"));
+ if (!header.returnType.equals("void")) {
+ code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
+ GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
+ }
+ for (int i = 0; i < header.args.size(); i++) {
+ String type = header.args.get(i).type, var = header.args.get(i).name;
+ code.add((DECLARE_DEFINE(type, var,
+ GET_FIELD_BY_PTR(infoStructName, var))));
+ }
+ code.add("");
}
- code.add("");
// __COND_SAT
if (!construct.condition.equals("")) {
code.add(DECLARE_DEFINE("bool", MACRO_COND, construct.condition));
.get(interfaceName);
FunctionHeader funcHeader = getFunctionHeader(semantics, iConstruct);
// Define necessary info structure
- newCode.add(COMMENT("Definition of interface info struct: "
- + interfaceName));
- newCode.addAll(DEFINE_INFO_STRUCT(interfaceName, funcHeader));
- newCode.add(COMMENT("End of info struct definition: "
- + interfaceName));
- newCode.add("");
+ if (!funcHeader.returnType.equals("void") || funcHeader.args.size() > 0) {
+ newCode.add(COMMENT("Definition of interface info struct: "
+ + interfaceName));
+ newCode.addAll(DEFINE_INFO_STRUCT(interfaceName, funcHeader));
+ newCode.add(COMMENT("End of info struct definition: "
+ + interfaceName));
+ newCode.add("");
+ }
// Define ID function
newCode.add(COMMENT("ID function of interface: " + interfaceName));
ArrayList<String> newCode = new ArrayList<String>();
String interfaceName = construct.name;
// Generate necessary header file (might be redundant but never mind)
+ newCode.add(INCLUDE(HEADER_STDLIB));
newCode.add(INCLUDE(HEADER_THREADS));
newCode.add(INCLUDE(HEADER_CDSANNOTATE));
newCode.add(INCLUDE(HEADER_SPECANNOTATION));
newCode.add(ASSIGN_PTR(structName, "annotation", structName));
newCode.add(ANNOTATE(anno));
// Call original renamed function
- newCode.add(DECLARE_DEFINE(header.returnType, MACRO_RETURN,
- header.getRenamedCall(SPEC_INTERFACE_WRAPPER)));
+ if (header.returnType.equals("void")) {
+ newCode.add(header.getRenamedCall(SPEC_INTERFACE_WRAPPER));
+ } else {
+ newCode.add(DECLARE_DEFINE(header.returnType, MACRO_RETURN,
+ header.getRenamedCall(SPEC_INTERFACE_WRAPPER)));
+ }
// HB conditions
for (String label : construct.hbConditions.keySet()) {
String condition = construct.hbConditions.get(label);
- String hbCondNum = Integer.toString(semantics.interface2Num
+ String hbCondNum = Integer.toString(semantics.hbLabel2Num
.get(label));
newCode.add("if " + BRACE(condition) + " {");
structName = "hb_condition";
newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_HB_CONDITION));
newCode.add(ASSIGN_PTR(anno, "annotation", structName));
newCode.add(ANNOTATE(anno));
+ newCode.add("}");
+ newCode.add("");
}
// Interface end
- String infoStructType = interfaceName + "_info", infoName = "info";
- newCode.add(DECLARE_DEFINE(infoStructType, infoName,
- BRACE(infoStructType + "*") + " malloc(sizeof("
- + infoStructType + "))"));
- newCode.add(ASSIGN_TO_PTR(infoName, MACRO_RETURN, MACRO_RETURN));
- for (int i = 0; i < header.args.size(); i++) {
- String argName = header.args.get(i).name;
- newCode.add(ASSIGN_TO_PTR(infoName, argName, argName));
+ String infoStructType = null, infoName = null;
+ if (!header.returnType.equals("void") || header.args.size() > 0) {
+ infoStructType = interfaceName + "_info";
+ infoName = "info";
+ newCode.add(DECLARE_DEFINE(infoStructType, infoName,
+ BRACE(infoStructType + "*") + " malloc(sizeof("
+ + infoStructType + "))"));
+ if (!header.returnType.equals("void")) {
+ newCode.add(ASSIGN_TO_PTR(infoName, MACRO_RETURN, MACRO_RETURN));
+ }
+ for (int i = 0; i < header.args.size(); i++) {
+ String argName = header.args.get(i).name;
+ newCode.add(ASSIGN_TO_PTR(infoName, argName, argName));
+ }
+ } else {
+ infoName = "NULL";
}
structName = "interface_end";
anno = "annoation_interface_end";
+ label + "!");
}
- // No HB condition label can duplicate!
- if (hbLabel2Num.containsKey(label)) {
- throw new SemanticsCheckerException("Happens-before label: "
- + label + " duplicates!");
- }
-
// Number the HB-condition label
hbLabel2Num.put(label, _hbLabelNum++);
}
package edu.uci.eecs.specCompiler.specExtraction;
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.FileWriter;
+import java.io.IOException;
import java.util.ArrayList;
+import edu.uci.eecs.specCompiler.codeGenerator.Environment;
import edu.uci.eecs.specCompiler.codeGenerator.SemanticsChecker;
import edu.uci.eecs.specCompiler.grammerParser.ParseException;
import edu.uci.eecs.specCompiler.grammerParser.SpecParser;
}
return templateStr;
}
+
+ public static void write2File(File file, ArrayList<String> content) {
+ String newFileName = Environment.GENERATED_FILE_DIR + "/" + file.getName();
+ File newFile = new File(newFileName);
+ newFile.getParentFile().mkdirs();
+ if (!newFile.exists()) {
+ try {
+ newFile.createNewFile();
+ } catch (IOException e) {
+ e.printStackTrace();
+ }
+ }
+ try {
+ BufferedWriter bw = new BufferedWriter(new FileWriter(newFile));
+ for (int i = 0; i < content.size(); i++) {
+ bw.write(content.get(i) + "\n");
+ }
+ bw.flush();
+ } catch (IOException e) {
+ e.printStackTrace();
+ }
+ }
}
SourceFileInfo another = (SourceFileInfo) o;
return another.file.equals(file);
}
-
- public void write2File() {
- String newFileName = Environment.GENERATED_FILE_DIR + "/" + file.getName();
- File newFile = new File(newFileName);
- newFile.getParentFile().mkdirs();
- if (!newFile.exists()) {
- try {
- newFile.createNewFile();
- } catch (IOException e) {
- e.printStackTrace();
- }
- }
- try {
- BufferedWriter bw = new BufferedWriter(new FileWriter(newFile));
- for (int i = 0; i < content.size(); i++) {
- bw.write(content.get(i) + "\n");
- }
- bw.flush();
- } catch (IOException e) {
- e.printStackTrace();
- }
- }
}
SourceFileInfo srcFileInfo;
try {
srcFileInfo = SpecParser.ParseFile(file);
- srcFileInfo.write2File();
+ ParserUtils.write2File(srcFileInfo.file, srcFileInfo.content);
srcFilesInfo.put(file, srcFileInfo);
} catch (ParseException e) {
e.printStackTrace();
#include <stdlib.h>
#include <stdint.h>
+typedef struct A {
+
+} A;
+
int main() {
uint64_t i64 = (uint64_t) NULL;
- if (i64)
- printf("True\n");
+ A *a = (A*) malloc (sizeof(A));
+ printf("%d\n", sizeof(A));
+ printf("%d\n", a);
return 1;
}