From e8466e30b587947c60bbba7df22b8b0908c75f26 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Fri, 25 Oct 2013 18:26:52 -0700 Subject: [PATCH] save --- grammer/spec_compiler.jj | 8 +- notes/generated_code_examples.txt | 18 +--- .../codeGenerator/CodeGenerator.java | 2 +- .../codeGenerator/CodeVariables.java | 92 ++++++++++------- .../codeGenerator/SemanticsChecker.java | 98 +++++++++++-------- .../SequentialDefineSubConstruct.java | 11 ++- 6 files changed, 129 insertions(+), 100 deletions(-) diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj index 8e2477d..22fada8 100644 --- a/grammer/spec_compiler.jj +++ b/grammer/spec_compiler.jj @@ -20,6 +20,7 @@ @InitVar: @DefineFunc: ... + @DefineFunc: @Interface_cluster: ... @Happens-before: @@ -747,6 +748,7 @@ GlobalConstruct Global_construct() : SequentialDefineSubConstruct Global_define() : { ArrayList initVar, defineFunc, code; + ArrayList> defineFuncs; ArrayList declareVars; VariableDeclaration declareVar; @@ -755,16 +757,16 @@ SequentialDefineSubConstruct Global_define() : { declareVars = null; initVar = null; - defineFunc = null; + defineFuncs = new ArrayList>(); } ( ((declareVar = TypeParam() ";" { declareVars.add(declareVar); } )*))? ( (code = C_CPP_CODE(null) { initVar = code; } ))? - ( (code = C_CPP_CODE(null) { defineFunc = code; }))? + ( (defineFunc = C_CPP_CODE(null) { defineFuncs.add(defineFunc); }))* { SequentialDefineSubConstruct res = new - SequentialDefineSubConstruct(declareVars, initVar, defineFunc); + SequentialDefineSubConstruct(declareVars, initVar, defineFuncs); //System.out.println(res); return res; } diff --git a/notes/generated_code_examples.txt b/notes/generated_code_examples.txt index ce40580..95e649a 100644 --- a/notes/generated_code_examples.txt +++ b/notes/generated_code_examples.txt @@ -2,14 +2,14 @@ Global Variable Declaration /* Include all the header files that contains the interface declaration */ -#include #inlcude #include #include /* Other necessary header files */ +#include #include -#include +#include /* All other user-defined functions */ ALL_USER_DEFINED_FUNCTIONS @@ -121,8 +121,7 @@ Interface Wrapper #include #include #include -#include -#include +#include TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) { @@ -167,11 +166,8 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) Potential Commit Point -#include -#include -#include -#include #include +#include /* Should add the __ATOMIC_RET__ if necessary */ uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...); @@ -189,10 +185,7 @@ if (POTENTIAL_CP_DEFINE_CONDITION) { Commit Point Define #include -#include #include -#include -#include <_spec_sequential_generated.h> #include /* Should add the __ATOMIC_RET__ if necessary */ @@ -220,10 +213,7 @@ Commit Point Define Check #include -#include #include -#include -#include <_spec_sequential_generated.h> #include /* Should add the __ATOMIC_RET__ if necessary */ diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index 3dbb595..e685bc6 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -54,7 +54,7 @@ public class CodeGenerator { this.codeAdditions = new HashMap>(); - _semantics = new SemanticsChecker(_extractor.getConstructs()); + _semantics = new SemanticsChecker(_extractor); try { _semantics.check(); System.out.println(_semantics); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index 1f7c3a0..e2ae18b 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -1,6 +1,8 @@ package edu.uci.eecs.specCompiler.codeGenerator; import java.util.ArrayList; +import java.util.HashSet; +import java.io.File; import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface; import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct; @@ -9,19 +11,21 @@ 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.SpecExtractor; +import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration; public class CodeVariables { // C++ code or library - public static final String HEADER_THREADS = "threads.h"; + public static final String HEADER_THREADS = ""; + public static final String HEADER_STDINT = ""; public static final String ThreadIDType = "thrd_t"; public static final String GET_THREAD_ID = "thrd_current"; public static final String BOOLEAN = "bool"; public static final String UINT64 = "uint64_t"; // Model checker code - public static final String HEADER_CDSANNOTATE = "cdsannotate.h"; - public static final String HEADER_SPECANNOTATION = "specannotation.h"; - public static final String HEADER_CDSTRACE = "cdstrace.h"; + public static final String HEADER_CDSANNOTATE = ""; + public static final String HEADER_SPECANNOTATION = ""; + public static final String HEADER_CDSTRACE = ""; public static final String CDSAnnotate = "cdsannotate"; public static final String CDSAnnotateType = "SPEC_ANALYSIS"; @@ -45,21 +49,15 @@ public class CodeVariables { public static final String ANNO_POST_CHECK = "anno_post_check"; // Specification variables - 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_INTERFACE_WRAPPER = "__wrapper_"; - public static final String VAR_CALL_SEQUENCE_NUM = "call_sequence_num"; // Specification library + public static final String HEADER_SPEC_LIB = ""; public static final String SPEC_QUEUE = "spec_queue"; public static final String SPEC_STACK = "spec_stack"; public static final String SPEC_DEQUE = "spec_deque"; public static final String SPEC_HASHTABLE = "spec_hashtable"; - public static final String HEADER_SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable.h"; public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable"; - public static final String HEADER_SPEC_TAG = "spec_tag.h"; public static final String SPEC_TAG = "spec_tag"; public static final String SPEC_TAG_CURRENT = "current"; public static final String SPEC_TAG_NEXT = "next"; @@ -81,7 +79,7 @@ public class CodeVariables { } private static String INCLUDE(String header) { - return "#include <" + header + ">"; + return "#include " + header; } private static String DEFINE(String left, String right) { @@ -104,8 +102,8 @@ public class CodeVariables { return structName + "." + field + " = &" + val + ";"; } - private static String DECLARE(String structType, String structName) { - return structType + " " + structName + ";"; + private static String DECLARE(String type, String name) { + return type + " " + name + ";"; } private static String DECLARE_DEFINE(String type, String var, String val) { @@ -116,23 +114,51 @@ public class CodeVariables { return CDSAnnotate + "(" + CDSAnnotateType + ", &" + structName + ");"; } + private static HashSet getAllHeaders(SemanticsChecker semantics) { + HashSet headers = new HashSet(); + for (String interfaceName : semantics.interfaceName2Construct.keySet()) { + File f = semantics.interfaceName2Construct.get(interfaceName).file; + headers.addAll(semantics.srcFilesInfo.get(f).headers); + } + return headers; + } + public static ArrayList generateGlobalVarDeclaration( SemanticsChecker semantics, GlobalConstruct construct) { ArrayList newCode = new ArrayList(); + HashSet allHeaders = getAllHeaders(semantics); - // Header conflicting avoidance macro & headers - newCode.add("/** @file " + HEADER_SPEC_SEQUENTIAL); - newCode.add(" * @brief Automatically generated header file for sequential variables"); - newCode.add(" */"); - newCode.add("#ifndef " + SPEC_SEQUENTIAL_HEADER_MACRO); - newCode.add("#define " + SPEC_SEQUENTIAL_HEADER_MACRO); + // All headers needed by the interface decalration + newCode.add(COMMENT("/* Include all the header files that contains the interface declaration */")); + for (String header : allHeaders) { + newCode.add(INCLUDE(header)); + } newCode.add(""); - newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE)); - newCode.add(INCLUDE(HEADER_SPECANNOTATION)); - newCode.add(INCLUDE(HEADER_SPEC_TAG)); + // Other necessary headers + newCode.add(INCLUDE(HEADER_STDINT)); + newCode.add(INCLUDE(HEADER_CDSANNOTATE)); + newCode.add(INCLUDE(HEADER_SPEC_LIB)); newCode.add(""); + + SequentialDefineSubConstruct code = construct.code; + // User-defined functions + newCode.add(COMMENT("All other user-defined functions")); + ArrayList> defineFuncs = code.defineFuncs; + for (int i = 0; i < defineFuncs.size(); i++) { + newCode.addAll(defineFuncs.get(i)); + newCode.add(""); + } + + // Define necessary info structure + newCode.add(COMMENT("Definition of interface info struct (per interface)")); - + + // User-defined variables + ArrayList varDecls = code.declareVar; + for (int i = 0; i < varDecls.size(); i++) { + VariableDeclaration varDecl = varDecls.get(i); + newCode.add(DECLARE(varDecl.type, varDecl.name)); + } // printCode(newCode); return newCode; @@ -185,27 +211,22 @@ public class CodeVariables { ArrayList newCode = new ArrayList(); // Generate necessary header file (might be redundant but never mind) - // Generate wrapper header - // Wrapper function body - + // Interface begin - + // Call original renamed function - + // HB conditions - - + // Interface end - // End of the wrapper function - -// printCode(newCode); + // printCode(newCode); return newCode; } @@ -219,11 +240,8 @@ public class CodeVariables { newCode.add(COMMENT("Include redundant headers")); newCode.add(INCLUDE(HEADER_THREADS)); newCode.add(INCLUDE(HEADER_CDSTRACE)); - newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE)); - newCode.add(INCLUDE(HEADER_SPEC_SEQUENTIAL)); newCode.add(""); // Some necessary function calls - return newCode; } diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java index 495801b..d09a61c 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java @@ -1,11 +1,14 @@ package edu.uci.eecs.specCompiler.codeGenerator; +import java.io.File; import java.util.ArrayList; import java.util.HashMap; import java.util.HashSet; import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct; import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct; +import edu.uci.eecs.specCompiler.specExtraction.ClassBeginConstruct; +import edu.uci.eecs.specCompiler.specExtraction.ClassEndConstruct; import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface; import edu.uci.eecs.specCompiler.specExtraction.Construct; import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct; @@ -13,43 +16,51 @@ import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct; 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.SourceFileInfo; +import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor; public class SemanticsChecker { + public final HashMap srcFilesInfo; public final ArrayList constructs; public final HashMap CPLabel2Construct; - public final HashMap potentialCPLabel2Construct; - public final HashMap interfaceName2Construct; + public final HashMap potentialCPLabel2Construct; + public final HashMap interfaceName2Construct; public final HashMap interfaceName2DefineConstruct; public final HashMap> CPLabel2InterfaceConstruct; - + public final HashMap interface2Num; public final HashMap hbLabel2Num; public final HashMap commitPointLabel2Num; private HashMap options; private HashMap> hbConditions; - private Construct entryPointConstruct; - + private ArrayList entryPointConstructs; + private ClassBeginConstruct classBeginConstruct; + private ClassEndConstruct classEndConstruct; + private int _interfaceNum; private int _hbLabelNum; - private int _commitPointNum; + private int _commitPointNum; - public SemanticsChecker(ArrayList constructs) { - this.constructs = constructs; + public SemanticsChecker(SpecExtractor extractor) { + this.srcFilesInfo = extractor.srcFilesInfo; + this.constructs = extractor.getConstructs(); this.CPLabel2Construct = new HashMap(); - this.potentialCPLabel2Construct = new HashMap(); - this.interfaceName2Construct = new HashMap(); + this.potentialCPLabel2Construct = new HashMap(); + this.interfaceName2Construct = new HashMap(); this.interfaceName2DefineConstruct = new HashMap(); this.CPLabel2InterfaceConstruct = new HashMap>(); - this.entryPointConstruct = null; - + this.entryPointConstructs = new ArrayList(); + this.classBeginConstruct = null; + this.classEndConstruct = null; + this.interface2Num = new HashMap(); this.hbLabel2Num = new HashMap(); // Immediately init the true HB-condition to be 0 hbLabel2Num.put("", 0); - + this.commitPointLabel2Num = new HashMap(); - + _interfaceNum = 0; _hbLabelNum = 0; _commitPointNum = 0; @@ -78,16 +89,16 @@ public class SemanticsChecker { + interfaceName + " doesn't contain HB_codition: " + 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++); - } + } } private void checkLabelDuplication(Construct construct, String label) @@ -103,17 +114,25 @@ public class SemanticsChecker { } private void postCheck() throws SemanticsCheckerException { - // This is a C program, must provide the entry point - if (getOption("LANG").equals("C") && entryPointConstruct == null) { + // C++ data structure with Class must provide the beginning and ending + // of its declaration + if (getOption("Class") != null) { + if (classBeginConstruct == null || classEndConstruct == null) { + throw new SemanticsCheckerException( + "Class must provide the boundary explicitly!"); + } + } + // It must provide the entry point + if (entryPointConstructs.size() == 0) { throw new SemanticsCheckerException( - "C program must provide the entry point!"); + "The program must have at least one entry point!"); } // Check if interface define construct labels are correct for (String name : interfaceName2DefineConstruct.keySet()) { if (!interfaceName2Construct.containsKey(name)) { - throw new SemanticsCheckerException( - "Label \"" + name + "\" does not have interface declaration!"); + throw new SemanticsCheckerException("Label \"" + name + + "\" does not have interface declaration!"); } } } @@ -131,8 +150,9 @@ public class SemanticsChecker { } // Number the interface label interface2Num.put(iConstruct.name, _interfaceNum++); - - interfaceName2Construct.put(iConstruct.name, constructs.get(i)); + + interfaceName2Construct.put(iConstruct.name, + (InterfaceConstruct) constructs.get(i)); for (int j = 0; j < iConstruct.commitPointSet.size(); j++) { String label = iConstruct.commitPointSet.get(j); @@ -164,7 +184,7 @@ public class SemanticsChecker { for (ConditionalInterface left : hbConditions.keySet()) { HashSet set = hbConditions.get(left); checkHBLabelConsistency(left); - + for (ConditionalInterface right : set) { checkHBLabelConsistency(right); } @@ -175,15 +195,16 @@ public class SemanticsChecker { checkLabelDuplication(construct, label); // Number the commit_point label commitPointLabel2Num.put(label, _commitPointNum++); - - potentialCPLabel2Construct.put(label, construct); + + potentialCPLabel2Construct.put(label, + (PotentialCPDefineConstruct) construct); } else if (construct instanceof CPDefineCheckConstruct) { CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct; label = theConstruct.label; checkLabelDuplication(construct, label); // Number the commit_point label commitPointLabel2Num.put(label, _commitPointNum++); - + CPLabel2Construct.put(label, construct); } else if (construct instanceof CPDefineConstruct) { CPDefineConstruct theConstruct = (CPDefineConstruct) construct; @@ -191,14 +212,10 @@ public class SemanticsChecker { checkLabelDuplication(construct, label); // Number the commit_point label commitPointLabel2Num.put(label, _commitPointNum++); - + CPLabel2Construct.put(label, construct); } else if (construct instanceof EntryPointConstruct) { - if (entryPointConstruct != null) { - throw new SemanticsCheckerException( - "More than one entry point!"); - } - entryPointConstruct = construct; + entryPointConstructs.add((EntryPointConstruct) construct); } else if (construct instanceof InterfaceDefineConstruct) { InterfaceDefineConstruct theConstruct = (InterfaceDefineConstruct) construct; String name = theConstruct.name; @@ -207,24 +224,23 @@ public class SemanticsChecker { "Interface define label duplicates!"); } interfaceName2DefineConstruct.put(name, construct); + } else if (construct instanceof ClassBeginConstruct) { + classBeginConstruct = (ClassBeginConstruct) construct; + } else if (construct instanceof ClassEndConstruct) { + classEndConstruct = (ClassEndConstruct) construct; } } } public String toString() { StringBuilder sb = new StringBuilder(); - if (entryPointConstruct == null) { - sb.append("Entry point is not specified!"); - } else { - sb.append("@Entry_point:\n" + entryPointConstruct); - } - + sb.append("Interface name 2 Construct:\n"); for (String interfaceName : interfaceName2Construct.keySet()) { sb.append(interfaceName + "\t" + interfaceName2Construct.get(interfaceName) + "\n"); } - + sb.append("Interface name 2 define construct:\n"); for (String interfaceName : interfaceName2DefineConstruct.keySet()) { sb.append(interfaceName + "\t" diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java index fb6828e..29080a8 100644 --- a/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java +++ b/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java @@ -3,14 +3,15 @@ package edu.uci.eecs.specCompiler.specExtraction; import java.util.ArrayList; public class SequentialDefineSubConstruct { - public final ArrayList initVar, defineFunc; + public final ArrayList initVar; + public final ArrayList> defineFuncs; public final ArrayList declareVar; public SequentialDefineSubConstruct(ArrayList declareVar, - ArrayList initVar, ArrayList defineFunc) { + ArrayList initVar, ArrayList> defineFuncs) { this.declareVar = declareVar; this.initVar = initVar; - this.defineFunc = defineFunc; + this.defineFuncs = defineFuncs; } public String toString() { @@ -21,7 +22,9 @@ public class SequentialDefineSubConstruct { res.append("@InitVar:\n"); res.append(ParserUtils.array2Str(initVar)); res.append("@DefineFunc:\n"); - res.append(ParserUtils.array2Str(defineFunc)); + for (int i = 0; i < defineFuncs.size(); i++) { + res.append(ParserUtils.array2Str(defineFuncs.get(i)) + "\n"); + } return res.toString(); } } -- 2.34.1