+ private static String ANNOTATE(SemanticsChecker semantics, String structName) {
+ return CDSAnnotate + "(" + CDSAnnotateType + ", " + structName + ");";
+ }
+
+ private static ArrayList<String> DEFINE_INFO_STRUCT(String interfaceName,
+ FunctionHeader header) {
+ ArrayList<String> code = new ArrayList<String>();
+ code.add("typedef struct " + interfaceName + "_info {");
+ if (!header.returnType.equals("void")) {
+ code.add(DECLARE(header.returnType, MACRO_RETURN));
+ }
+ for (int i = 0; i < header.args.size(); i++) {
+ code.add(DECLARE(header.args.get(i)));
+ }
+ code.add("} " + interfaceName + "_info;");
+ return code;
+ }
+
+ private static ArrayList<String> DEFINE_ID_FUNC(
+ InterfaceConstruct construct, FunctionHeader header) {
+ String interfaceName = construct.name;
+ ArrayList<String> code = new ArrayList<String>();
+ String idCode = construct.idCode;
+ code.add("inline static " + IDType + " " + interfaceName + "_id("
+ + "void *info, " + ThreadIDType + " " + MACRO_THREAD_ID + ") {");
+
+ // Read info struct
+ if (!header.returnType.equals("void") || header.args.size() != 0) {
+ String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
+ code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
+ BRACE(infoStructType + "*") + "info"));
+ if (!header.returnType.equals("void")) {
+ code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
+ GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
+ }
+ for (int i = 0; i < header.args.size(); i++) {
+ String type = header.args.get(i).type, var = header.args.get(i).name;
+ code.add((DECLARE_DEFINE(type, var,
+ GET_FIELD_BY_PTR(infoStructName, var))));
+ }
+ code.add("");
+ }
+
+ if (!idCode.equals("")) {
+ code.add(DECLARE_DEFINE(IDType, MACRO_ID, idCode));
+ } else {
+ code.add(DECLARE_DEFINE(IDType, MACRO_ID, DEFAULT_ID));
+ }
+ code.add("return " + MACRO_ID + ";");
+ code.add("}");
+ return code;
+ }
+
+ private static ArrayList<String> DEFINE_CHECK_ACTION_FUNC(
+ InterfaceConstruct construct, FunctionHeader header) {
+ String interfaceName = construct.name;
+ ArrayList<String> code = new ArrayList<String>();
+ code.add("inline static bool " + interfaceName
+ + "_check_action(void *info, " + IDType + " " + MACRO_ID + ", "
+ + ThreadIDType + " " + MACRO_THREAD_ID + ") {");
+ code.add(DECLARE("bool", "check_passed"));
+ // Read info struct
+ if (!header.returnType.equals("void") || header.args.size() != 0) {
+ String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
+ code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
+ BRACE(infoStructType + "*") + "info"));
+ if (!header.returnType.equals("void")) {
+ code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
+ GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
+ }
+ for (int i = 0; i < header.args.size(); i++) {
+ String type = header.args.get(i).type, var = header.args.get(i).name;
+ code.add((DECLARE_DEFINE(type, var,
+ GET_FIELD_BY_PTR(infoStructName, var))));
+ }
+ code.add("");
+ }
+ // __COND_SAT
+ if (!construct.condition.equals("")) {
+ code.add(DECLARE_DEFINE("bool", MACRO_COND, construct.condition));
+ }
+ // Check
+ if (!construct.check.equals("")) {
+ code.add(ASSIGN("check_passed", construct.check));
+ code.add("if (!check_passed) return false;");
+ }
+ // Action
+ if (construct.action.size() > 0) {
+ code.addAll(construct.action);
+ }
+ // Post_check
+ if (!construct.postCheck.equals("")) {
+ code.add(ASSIGN("check_passed", construct.postCheck));
+ code.add("if (!check_passed) return false;");
+ }
+ // Post_action
+ if (construct.postAction.size() > 0) {
+ code.addAll(construct.postAction);
+ }
+ // Return true finally
+ code.add("return true;");
+
+ code.add("}");
+
+ return code;
+ }
+
+ public 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);
+ }
+ headers.add(HEADER_STDLIB);
+ headers.add(HEADER_STDINT);
+ headers.add(HEADER_MODELMEMORY);
+ headers.add(HEADER_MODELTYPES);
+ headers.add(HEADER_SPEC_LIB);
+ headers.add(HEADER_STDINT);
+ headers.add(HEADER_CDSANNOTATE);
+ // headers.add(HEADER_COMMON);
+ headers.add(HEADER_SPECANNOTATION);
+ return headers;
+ }
+
+ private static void makeFunctionStatic(ArrayList<String> funcDefine) {
+ String headLine = funcDefine.get(0);
+ headLine = "inline static " + headLine;
+ funcDefine.set(0, headLine);
+ }
+
+ private static String makeVariablesStatic(VariableDeclaration varDecl) {
+ String res = "static " + varDecl.type + " " + varDecl.name + ";";
+ return res;
+ }
+
+ private static FunctionHeader getFunctionHeader(SemanticsChecker semantics,
+ Construct construct) {
+ ArrayList<String> content = semantics.srcFilesInfo.get(construct.file).content;
+ String headerLine = content.get(construct.beginLineNum), templateLine = null;
+ if (headerLine.startsWith("template")) {
+ templateLine = headerLine;
+ headerLine = content.get(construct.beginLineNum + 1);
+ }
+ headerLine = headerLine.substring(0, headerLine.indexOf(')') + 1);
+ try {
+ FunctionHeader header = SpecParser.parseFuncHeader(headerLine);
+ if (templateLine != null) {
+ ArrayList<VariableDeclaration> templateArgs = SpecParser
+ .getTemplateArg(templateLine);
+ header.setTemplateList(templateArgs);
+ }
+ return header;
+ } catch (ParseException e) {
+ e.printStackTrace();
+ }
+ return null;