From 45a94756dec1364837f3b4b116a33894813f8325 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Thu, 18 Feb 2016 02:17:40 -0800 Subject: [PATCH] edits --- benchmark/linuxrwlocks/linuxrwlocks.c | 31 +++--------------- .../uci/eecs/codeGenerator/CodeGenerator.java | 2 +- .../codeGenerator/CodeGeneratorUtils.java | 7 ++++ .../uci/eecs/codeGenerator/Environment.java | 1 + .../eecs/specExtraction/GlobalConstruct.java | 2 +- .../eecs/specExtraction/SpecExtractor.java | 16 ++++++++++ .../uci/eecs/specExtraction/SpecUtils.java | 32 +++++++++++++------ 7 files changed, 53 insertions(+), 38 deletions(-) diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c index 1f7059f..03a292b 100644 --- a/benchmark/linuxrwlocks/linuxrwlocks.c +++ b/benchmark/linuxrwlocks/linuxrwlocks.c @@ -47,31 +47,11 @@ typedef union { auxiliary check since it is an extra rule for how the interfaces should called. */ -/** - @Begin - @Options: - LANG = C; - @Global_define: - @DeclareVar: - bool writer_lock_acquired; - int reader_lock_cnt; - @InitVar: - writer_lock_acquired = false; - reader_lock_cnt = 0; - @Happens_before: - # Since commit_point_set has no ID attached, A -> B means that for any B, - # the previous A happens before B. - #Read_Unlock -> Read_Lock - Read_Unlock -> Write_Lock - Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ) - #Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ) - - Write_Unlock -> Write_Lock - Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ) - - Write_Unlock -> Read_Lock - Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ) - +/** @DeclareState: + bool writer_lock_acquired; + int reader_lock_cnt; + @Initial: writer_lock_acquired = false; + reader_lock_cnt = 0; @Commutativity: Read_Lock <-> Read_Lock: true @Commutativity: Read_Lock <-> Read_Unlock: true @Commutativity: Read_Lock <-> Read_Trylock: true @@ -89,7 +69,6 @@ typedef union { @Commutativity: Write_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__ @Commutativity: Write_Trylock <-> Write_Unlock: !_Method1.__RET__ @Commutativity: Write_Trylock <-> Write_Lock: !_Method1.__RET__ - @End */ static inline int read_can_lock(rwlock_t *lock) diff --git a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java index 3d6b224..b3f1c61 100644 --- a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java @@ -306,7 +306,7 @@ public class CodeGenerator { } static public void main(String[] args) { - String[] dirNames = { Environment.REGISTER }; + String[] dirNames = { Environment.REGISTER, Environment.MS_QUEUE, Environment.LINUXRWLOCKS, Environment.MCS_LOCK }; for (int i = 0; i < dirNames.length; i++) { String dirName = dirNames[i]; diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java index abcb45c..005397e 100644 --- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java +++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java @@ -155,11 +155,18 @@ public class CodeGeneratorUtils { code.addLine(""); // Users included headers + // FIXME: We don't add user-defined headers, but as a workaround we only add forward class. code.addLine(ShortComment("User included headers go here")); for (String header : headerFiles) { code.addLine(IncludeHeader(header)); } code.addLine(""); + +// code.addLine(ShortComment("Forward declaration goes here")); +// for (String type : extractor.forwardClass) { +// code.addLine("class " + type + ";"); +// } +// code.addLine(""); code.addLine("using namespace std;"); code.addLine(""); diff --git a/src/edu/uci/eecs/codeGenerator/Environment.java b/src/edu/uci/eecs/codeGenerator/Environment.java index d11545d..f323ca7 100644 --- a/src/edu/uci/eecs/codeGenerator/Environment.java +++ b/src/edu/uci/eecs/codeGenerator/Environment.java @@ -23,5 +23,6 @@ public class Environment { public final static String REGISTER = "register"; public final static String MS_QUEUE = "ms-queue"; public final static String LINUXRWLOCKS = "linuxrwlocks"; + public final static String MCS_LOCK = "mcs-lock"; } diff --git a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java index 8c6848a..f49911b 100644 --- a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java +++ b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java @@ -66,7 +66,7 @@ public class GlobalConstruct extends Construct { if (type.equals("int") || type.equals("unsigned") || type.equals("unsigned int") || type.equals("int unsigned") || type.equals("double") - || type.equals("double")) { + || type.equals("double") || type.equals("bool")) { // NEW->x = OLD->x; code.addLine(SpecNaming.NewStateInst + "->" + name + " = " + SpecNaming.OldStateInst + "->" + name + ";"); diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java index 0e470e0..a7b4fe5 100644 --- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java +++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java @@ -37,6 +37,9 @@ public class SpecExtractor { public final HashMap entryMap; public final HashSet headerFiles; + + // In the generated header file, we need to forward the user-defined + public final HashSet forwardClass; private GlobalConstruct globalConstruct; @@ -46,6 +49,7 @@ public class SpecExtractor { OPLabelSet = new HashSet(); entryMap = new HashMap(); headerFiles = new HashSet(); + forwardClass = new HashSet(); globalConstruct = null; } @@ -410,6 +414,18 @@ public class SpecExtractor { line = lineReader.readLine(); lineNum = lineReader.getLineNumber(); construct.processFunctionDeclaration(line); + + // Record those user-defined struct + // RET + String returnType = construct.getFunctionHeader().returnType; + if (SpecUtils.isUserDefinedStruct(returnType)) + forwardClass.add(SpecUtils.getPlainType(returnType)); + // Arguments + for (VariableDeclaration decl : construct.getFunctionHeader().args) { + if (SpecUtils.isUserDefinedStruct(decl.type)) + forwardClass.add(SpecUtils.getPlainType(decl.type)); + } + } catch (IOException e) { errMsg = "Spec error in file \"" + file.getName() diff --git a/src/edu/uci/eecs/specExtraction/SpecUtils.java b/src/edu/uci/eecs/specExtraction/SpecUtils.java index a9ed016..869b9ff 100644 --- a/src/edu/uci/eecs/specExtraction/SpecUtils.java +++ b/src/edu/uci/eecs/specExtraction/SpecUtils.java @@ -123,8 +123,7 @@ public class SpecUtils { * annotations or the beginning line of the next primitive * @throws WrongAnnotationException */ - public static Primitive extractPrimitive(File file, int beginLineNum, - ArrayList annotations, IntObj curIdx) + public static Primitive extractPrimitive(File file, int beginLineNum, ArrayList annotations, IntObj curIdx) throws WrongAnnotationException { if (curIdx.getVal() == annotations.size()) // The current index points // to the end @@ -147,9 +146,8 @@ public class SpecUtils { } // Assert that we must have found one primitive if (primitive == null) { - WrongAnnotationException - .err(file, curLineNum, - "Something is wrong! We must have found one primitve here!\n"); + WrongAnnotationException.err(file, curLineNum, + "Something is wrong! We must have found one primitve here!\n"); } // Process the current "primitive" @@ -163,9 +161,8 @@ public class SpecUtils { primitive.addLine(trimmedCode); } } else { - WrongAnnotationException - .err(file, curLineNum, - "The state annotation should have correct primitive syntax (sub-annotations)"); + WrongAnnotationException.err(file, curLineNum, + "The state annotation should have correct primitive syntax (sub-annotations)"); } // Deal with other normal line. E.g. y = 1; @@ -187,8 +184,7 @@ public class SpecUtils { if (primitive.contents.size() == 0) { // The content of the primitive is // empty - WrongAnnotationException.warning(file, curLineNum, "Primitive " - + primitive.name + " is empty."); + WrongAnnotationException.warning(file, curLineNum, "Primitive " + primitive.name + " is empty."); } return primitive; } @@ -228,4 +224,20 @@ public class SpecUtils { return null; } } + + public static boolean isUserDefinedStruct(String type) { + // FIXME: We only consider the type is either a one-level pointer or a + // struct + String bareType = trimSpace(type.replace('*', ' ')); + return !bareType.equals("int") && !bareType.matches("unsigned\\s+int") && !bareType.equals("unsigned") + && !bareType.equals("bool") && !bareType.equals("double") && !bareType.equals("float") + && !bareType.equals("void"); + } + + public static String getPlainType(String type) { + // FIXME: We only consider the type is either a one-level pointer or a + // struct + String bareType = trimSpace(type.replace('*', ' ')); + return bareType; + } } -- 2.34.1