/* Include the header files first
** This declaration will be written into a header file
*/
-/* @file CDSName.h */
+/* @file _spec_sequential_generated.h */
/* @brief automatically generated file */
-#ifndef _CDSNAME_H
-#define _CDSNAME_H
+#ifndef __SPEC_SEQUENTIAL_GENERATED_H
+#define __SPEC_SEQUENTIAL_GENERATED_H
#include <specannotation.h>
#include <spec_private_hashtable.h>
-typedef struct Sequential
-{
- spec_private_hashtabel cond;
- spec_private_hashtabel id;
- spec_private_hashtabel interface;
- spec_private_hashtabel interface_call_sequence;
+/* Beginning of struct Sequential */
+typedef struct Sequential {
+ spec_private_hashtable cond;
+ spec_private_hashtable id;
+ spec_private_hashtable interface;
+ spec_private_hashtable interface_call_sequence;
/* DefineVar unfolded here */
spec_private_hashtable Put__Old_Val;
- /* Other user-defined variables */
+ /* Beginning of other user-defined variables */
bool lock_acquired;
int reader_lock_cnt;
-} Sequential;
+ /* End of other user-defined variables */
+
+} Sequential; /* End of struct Sequential */
+/* Instance of the struct */
Sequential __sequential;
+/* Define function for sequential code initialization */
+void __sequential_init() {
+ /* Init internal variables */
+ init(&__sequential.cond);
+ init(&__sequential.id);
+ init(&__sequential.interface);
+ init(&__sequential.interface_call_sequence);
+ /* Init DefineVars */
+ init(&__sequential.Put__Old_Val);
+ /* Init user-defined variables */
+ lock_acquired = false;
+ reader_lock_cnt = 0;
+}
+
/* All other user-defined functions */
ALL_USER_DEFINED_FUNCTIONS
-
#endif
****** Example2: ******
-Global Variable Initialization (Entry Point Unfolding)
-
-#include <spec_private_hashtable.h>
-#include <CDSName.h>
-
-init(&__sequential.condition);
-init(&__sequential.id);
-init(&__sequential.interface);
-init(&__sequential.interface_call_sequence);
-/* DefineVar initialized here */
-init(&Put__Old_Val);
-
-/* User-define variables */
-lock_acquired = false;
-reader_lock_cnt = 0;
-
-
-
-****** Example3: ******
Interface Wrapper
/* Include the header files first */
}
-****** Example4: ******
+****** Example3: ******
Potential Commit Point
#include <threads.h>
#include <cdstrace.h>
#include <cdsannotate.h>
#include <spec_private_hashtable.h>
-#include <CDSName.h>
+#include <_sepc_sequential_genenrated.h>
thrd_t __tid = thrd_current();
uint64_t __ATOMIC_RET__ = get_prev_value(tid);
cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
}
-****** Example5: ******
+****** Example4: ******
Commit Point Define
#include <threads.h>
#include <cdstrace.h>
#include <cdsannotate.h>
#include <spec_private_hashtable.h>
-#include <CDSName.h>
+#include <_spec_sequential_generated.h>
thrd_t __tid = thrd_current();
int interface_num = get(&__sequential.interface, tid);
}
-***** Example6: ******
+***** Example5: ******
Commit Point Define Check
#include <cdstrace.h>
#include <cdsannotate.h>
#include <spec_private_hashtable.h>
-#include <CDSName.h>
+#include <_spec_sequential_generated.h>
thrd_t __tid = thrd_current();
import java.util.ArrayList;
import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
+import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
public class CodeVariables {
// C++ code or library
public static final String ANNO_POST_CHECK = "anno_post_check";
// Specification variables
- public static final String SPEC_STRUCT = "Sequential";
- public static final String SPEC_INSTANCE = "__sequential";
+ public static final String SPEC_SEQUENTIAL_HEADER = "_spec_sequential.h";
+ public static final String SPEC_SEQUENTIAL_HEADER_MACRO = SPEC_SEQUENTIAL_HEADER
+ .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_QUEUE = "spec_queue";
public static final String SPEC_STACK = "spec_stack";
public static final String SPEC_HASHTABLE = "spec_hashtable";
+ public static final String SPEC_PRIVATE_HASHTABLE_HEADER = "spec_private_hashtable.h";
public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
public static final String SPEC_TAG = "spec_tag";
public static final String MACRO_COND = "__COND_SAT__";
public static final String MACRO_RETURN = "__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++;
+ }
+ }
+
+ private static void printCode(ArrayList<String> code) {
+ for (int i = 0; i < code.size(); i++) {
+ System.out.println(code.get(i));
+ }
+ }
+
+ public static ArrayList<String> generateGlobalVarDeclaration(
+ SemanticsChecker semantics, GlobalConstruct construct) {
+ ArrayList<String> newCode = new ArrayList<String>();
+
+ // Header conflicting avoidance macro & headers
+ newCode.add("/** @file " + SPEC_SEQUENTIAL_HEADER);
+ 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);
+ newCode.add("#include " + "<" + SPEC_PRIVATE_HASHTABLE_HEADER + ">");
+ newCode.add("#include " + "<" + HEADER_SPECANNOTATION + ">");
+
+ // Generate all sequential variables into a struct
+ newCode.add("/* Beginning of struct " + SPEC_SEQUENTIAL_STRUCT + " */");
+ newCode.add("typedef struct " + SPEC_SEQUENTIAL_STRUCT + " {");
+ newCode.add("/* Condition of interface */");
+ newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_CONDITION + ";");
+ newCode.add("/* ID of interface */");
+ newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_ID + ";");
+ newCode.add("/* Current interface call */");
+ newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_INTERFACE + ";");
+ newCode.add("/* Current interface call sequence */");
+ newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_INTERFACE_CALL_SEQUENCE
+ + ";");
+ newCode.add("");
+ // DefineVar declaration
+ for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
+ InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
+ .get(interfaceName).construct;
+ ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
+ newCode.add("/* DefineVar in " + interfaceName + " */");
+ for (int i = 0; i < defineVars.size(); i++) {
+ DefineVar var = defineVars.get(i);
+ newCode.add(SPEC_PRIVATE_HASHTABLE + " " + var.getNewVarName()
+ + ";");
+ }
+ newCode.add("");
+ }
+ // Generate user-defined variable declaration
+ newCode.add("/* Beginnint of other user-defined variables */");
+ SequentialDefineSubConstruct globalCode = construct.code;
+ breakCodeLines(newCode, globalCode.declareVar);
+ newCode.add("/* End of other user-defined variables */");
+ // End of struct Sequential
+ newCode.add("} " + SPEC_SEQUENTIAL_STRUCT + "; /* End of struct "
+ + SPEC_SEQUENTIAL_STRUCT + " */");
+
+ // Generate
+
+ // Generate code from the DefineVar, __COND_SAT__ and __ID__
+ // The hashtable in the contract can only contains pointers or integers
+ // __COND_SAT__
+ newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_CONDITION
+ + ";");
+ // __ID__
+ newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_ID + ";");
+ // DefineVars
+ for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
+ InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
+ .get(interfaceName).construct;
+ ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
+ for (int i = 0; i < defineVars.size(); i++) {
+ DefineVar var = defineVars.get(i);
+ newCode.add(CodeVariables.SPEC_HASHTABLE + var.getNewVarName()
+ + ";");
+ }
+ }
+ // __interface
+ newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE
+ + ";");
+ // __interface_call_sequence
+ newCode.add(CodeVariables.SPEC_HASHTABLE
+ + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ";");
+ // Interface call sequence varaiable
+ newCode.add(CodeVariables.SPEC_TAG + " "
+ + CodeVariables.INTERFACE_CALL_SEQUENCE + ";");
+ // End of the struct
+ newCode.add("}");
+
+ // FIXME: Constructor should be modified and put in the right place
+ // Generate constructor (the place to initialize everything!)
+ breakCodeLines(newCode, globalCode.initVar);
+ // __COND_SAT__
+ newCode.add("init_table(&" + CodeVariables.SPEC_CONDITION + ");");
+ // __ID__
+ newCode.add("init_table(&" + CodeVariables.SPEC_ID + ");");
+ // DefineVars
+ for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
+ InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
+ .get(interfaceName).construct;
+ ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
+ for (int i = 0; i < defineVars.size(); i++) {
+ DefineVar var = defineVars.get(i);
+ newCode.add("init_table(&" + var.getNewVarName() + ");");
+ }
+ }
+ // __interface
+ newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE + ");");
+ // __interface_call_sequence
+ newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE
+ + ");");
+
+ // Pass the happens-before relationship check here
+ newCode.addAll(CodeVariables.generateHBInitAnnotation(semantics));
+
+ newCode.add("\n");
+
+ // Generate the sequential functions
+ breakCodeLines(newCode, globalCode.defineFunc);
+
+ // The end
+ newCode.add("#endif " + SPEC_SEQUENTIAL_HEADER_MACRO + "\t/* End of "
+ + SPEC_SEQUENTIAL_HEADER + " */");
+
+ printCode(newCode);
+ return newCode;
+ }
+
public static ArrayList<String> generateHBInitAnnotation(
SemanticsChecker semantics) {
ArrayList<String> newCode = new ArrayList<String>();
+ interfaceNumAfter + ";");
newCode.add(structVarName + "." + "hb_condition_num_after"
+ " = " + hbLabelNumAfter + ";");
-
- newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &" + structVarName + ");");
+
+ newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &"
+ + structVarName + ");");
}
}
return newCode;
projects / cdsspec-compiler.git / commitdiff