From d9c5f3639af2eaa7a35b7242c846f657b875657c Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Sun, 20 Oct 2013 09:17:26 -0700 Subject: [PATCH] more changes --- notes/generated_code_examples.txt | 71 ++++---- .../codeGenerator/CodeGenerator.java | 2 +- .../codeGenerator/CodeVariables.java | 155 +++++++++++++++++- 3 files changed, 186 insertions(+), 42 deletions(-) diff --git a/notes/generated_code_examples.txt b/notes/generated_code_examples.txt index aa0b388..5dc22b7 100644 --- a/notes/generated_code_examples.txt +++ b/notes/generated_code_examples.txt @@ -4,58 +4,55 @@ Global Variable Declaration /* 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 #include -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 -#include - -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 */ @@ -123,14 +120,14 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) } -****** Example4: ****** +****** Example3: ****** Potential Commit Point #include #include #include #include -#include +#include <_sepc_sequential_genenrated.h> thrd_t __tid = thrd_current(); uint64_t __ATOMIC_RET__ = get_prev_value(tid); @@ -147,14 +144,14 @@ if (POTENTIAL_CP_DEFINE_CONDITION) { cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define); } -****** Example5: ****** +****** Example4: ****** Commit Point Define #include #include #include #include -#include +#include <_spec_sequential_generated.h> thrd_t __tid = thrd_current(); int interface_num = get(&__sequential.interface, tid); @@ -213,7 +210,7 @@ switch (interface_num) { } -***** Example6: ****** +***** Example5: ****** Commit Point Define Check @@ -221,7 +218,7 @@ Commit Point Define Check #include #include #include -#include +#include <_spec_sequential_generated.h> thrd_t __tid = thrd_current(); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index d051906..c69473a 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -99,7 +99,7 @@ public class CodeGenerator { ArrayList newCode = new ArrayList(); // Generate all sequential variables into a struct - newCode.add("struct " + CodeVariables.SPEC_STRUCT + " {\n"); + newCode.add("struct " + CodeVariables.SPEC_SEQUENTIAL_STRUCT + " {\n"); // Generate the code in global construct first SequentialDefineSubConstruct globalCode = construct.code; diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index e0a41fa..4ee3e3d 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -3,6 +3,10 @@ package edu.uci.eecs.specCompiler.codeGenerator; 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 @@ -33,8 +37,11 @@ public class CodeVariables { 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"; @@ -47,6 +54,7 @@ public class CodeVariables { 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"; @@ -55,6 +63,144 @@ public class CodeVariables { 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 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 code) { + for (int i = 0; i < code.size(); i++) { + System.out.println(code.get(i)); + } + } + + public static ArrayList generateGlobalVarDeclaration( + SemanticsChecker semantics, GlobalConstruct construct) { + ArrayList newCode = new ArrayList(); + + // 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 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 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 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 generateHBInitAnnotation( SemanticsChecker semantics) { ArrayList newCode = new ArrayList(); @@ -79,8 +225,9 @@ public class CodeVariables { + interfaceNumAfter + ";"); newCode.add(structVarName + "." + "hb_condition_num_after" + " = " + hbLabelNumAfter + ";"); - - newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &" + structVarName + ");"); + + newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &" + + structVarName + ");"); } } return newCode; -- 2.34.1