@InitVar:
@DefineFunc:
...
+ @DefineFunc:
@Interface_cluster:
...
@Happens-before:
SequentialDefineSubConstruct Global_define() :
{
ArrayList<String> initVar, defineFunc, code;
+ ArrayList<ArrayList<String>> defineFuncs;
ArrayList<VariableDeclaration> declareVars;
VariableDeclaration declareVar;
{
declareVars = null;
initVar = null;
- defineFunc = null;
+ defineFuncs = new ArrayList<ArrayList<String>>();
}
<GLOBAL_DEFINE>
(<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; }))?
+ (<DEFINE_FUNC> (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;
}
Global Variable Declaration
/* Include all the header files that contains the interface declaration */
-#include <iostream>
#inlcude <atomic>
#include <memory>
#include <assert.h>
/* Other necessary header files */
+#include <stdint.h>
#include <specannotation.h>
-#include <spec_tag.h>
+#include <spec_lib.h>
/* All other user-defined functions */
ALL_USER_DEFINED_FUNCTIONS
#include <threads.h>
#include <cdsannotate.h>
#include <specannotation.h>
-#include <spec_tag.h>
-#include <spec_private_hashtable.h>
+#include <spec_lib.h>
TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
{
Potential Commit Point
-#include <threads.h>
-#include <cdstrace.h>
-#include <cdsannotate.h>
-#include <spec_private_hashtable.h>
#include <stdint.h>
+#include <cdsannotate.h>
/* Should add the __ATOMIC_RET__ if necessary */
uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
Commit Point Define
#include <threads.h>
-#include <cdstrace.h>
#include <cdsannotate.h>
-#include <spec_private_hashtable.h>
-#include <_spec_sequential_generated.h>
#include <stdint.h>
/* Should add the __ATOMIC_RET__ if necessary */
#include <threads.h>
-#include <cdstrace.h>
#include <cdsannotate.h>
-#include <spec_private_hashtable.h>
-#include <_spec_sequential_generated.h>
#include <stdint.h>
/* Should add the __ATOMIC_RET__ if necessary */
this.codeAdditions = new HashMap<File, ArrayList<CodeAddition>>();
- _semantics = new SemanticsChecker(_extractor.getConstructs());
+ _semantics = new SemanticsChecker(_extractor);
try {
_semantics.check();
System.out.println(_semantics);
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;
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 = "<threads.h>";
+ public static final String HEADER_STDINT = "<stdint.h>";
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 = "<cdsannotate.h>";
+ public static final String HEADER_SPECANNOTATION = "<specannotation.h>";
+ 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 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 = "<spec_lib.h>";
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";
}
private static String INCLUDE(String header) {
- return "#include <" + header + ">";
+ return "#include " + header;
}
private static String DEFINE(String left, String right) {
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) {
return CDSAnnotate + "(" + CDSAnnotateType + ", &" + structName + ");";
}
+ private static HashSet<String> getAllHeaders(SemanticsChecker semantics) {
+ HashSet<String> headers = new HashSet<String>();
+ 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<String> generateGlobalVarDeclaration(
SemanticsChecker semantics, GlobalConstruct construct) {
ArrayList<String> newCode = new ArrayList<String>();
+ HashSet<String> 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<ArrayList<String>> 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<VariableDeclaration> 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;
ArrayList<String> newCode = new ArrayList<String>();
// 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;
}
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;
}
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;
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<File, SourceFileInfo> srcFilesInfo;
public final ArrayList<Construct> constructs;
public final HashMap<String, Construct> CPLabel2Construct;
- public final HashMap<String, Construct> potentialCPLabel2Construct;
- public final HashMap<String, Construct> interfaceName2Construct;
+ public final HashMap<String, PotentialCPDefineConstruct> potentialCPLabel2Construct;
+ public final HashMap<String, InterfaceConstruct> interfaceName2Construct;
public final HashMap<String, Construct> interfaceName2DefineConstruct;
public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
-
+
public final HashMap<String, Integer> interface2Num;
public final HashMap<String, Integer> hbLabel2Num;
public final HashMap<String, Integer> commitPointLabel2Num;
private HashMap<String, String> options;
private HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions;
- private Construct entryPointConstruct;
-
+ private ArrayList<EntryPointConstruct> entryPointConstructs;
+ private ClassBeginConstruct classBeginConstruct;
+ private ClassEndConstruct classEndConstruct;
+
private int _interfaceNum;
private int _hbLabelNum;
- private int _commitPointNum;
+ private int _commitPointNum;
- public SemanticsChecker(ArrayList<Construct> constructs) {
- this.constructs = constructs;
+ public SemanticsChecker(SpecExtractor extractor) {
+ this.srcFilesInfo = extractor.srcFilesInfo;
+ this.constructs = extractor.getConstructs();
this.CPLabel2Construct = new HashMap<String, Construct>();
- this.potentialCPLabel2Construct = new HashMap<String, Construct>();
- this.interfaceName2Construct = new HashMap<String, Construct>();
+ this.potentialCPLabel2Construct = new HashMap<String, PotentialCPDefineConstruct>();
+ this.interfaceName2Construct = new HashMap<String, InterfaceConstruct>();
this.interfaceName2DefineConstruct = new HashMap<String, Construct>();
this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
- this.entryPointConstruct = null;
-
+ this.entryPointConstructs = new ArrayList<EntryPointConstruct>();
+ this.classBeginConstruct = null;
+ this.classEndConstruct = null;
+
this.interface2Num = new HashMap<String, Integer>();
this.hbLabel2Num = new HashMap<String, Integer>();
// Immediately init the true HB-condition to be 0
hbLabel2Num.put("", 0);
-
+
this.commitPointLabel2Num = new HashMap<String, Integer>();
-
+
_interfaceNum = 0;
_hbLabelNum = 0;
_commitPointNum = 0;
+ 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)
}
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!");
}
}
}
}
// 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);
for (ConditionalInterface left : hbConditions.keySet()) {
HashSet<ConditionalInterface> set = hbConditions.get(left);
checkHBLabelConsistency(left);
-
+
for (ConditionalInterface right : set) {
checkHBLabelConsistency(right);
}
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;
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;
"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"
import java.util.ArrayList;
public class SequentialDefineSubConstruct {
- public final ArrayList<String> initVar, defineFunc;
+ public final ArrayList<String> initVar;
+ public final ArrayList<ArrayList<String>> defineFuncs;
public final ArrayList<VariableDeclaration> declareVar;
public SequentialDefineSubConstruct(ArrayList<VariableDeclaration> declareVar,
- ArrayList<String> initVar, ArrayList<String> defineFunc) {
+ ArrayList<String> initVar, ArrayList<ArrayList<String>> defineFuncs) {
this.declareVar = declareVar;
this.initVar = initVar;
- this.defineFunc = defineFunc;
+ this.defineFuncs = defineFuncs;
}
public String toString() {
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();
}
}
projects / cdsspec-compiler.git / commitdiff