From 70fd401b67750e8efbd73540e1affa7f65c61c1c Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Mon, 14 Oct 2013 20:00:28 -0700
Subject: [PATCH] ready to generate code

---
 .../codeGenerator/CodeGenerator.java          | 19 +++++
 .../codeGenerator/SemanticsChecker.java       | 84 +++++++++++++++++++
 .../SemanticsCheckerException.java            |  7 ++
 .../specExtraction/SpecExtractor.java         |  4 +
 4 files changed, 114 insertions(+)
 create mode 100644 src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
 create mode 100644 src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
 create mode 100644 src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsCheckerException.java

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
new file mode 100644
index 0000000..faac44c
--- /dev/null
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -0,0 +1,19 @@
+package edu.uci.eecs.specCompiler.codeGenerator;
+
+import java.util.ArrayList;
+
+import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
+
+/**
+ * <p>
+ * This class will generate the annotated C code that can run on the current
+ * model checker.
+ * </p>
+ * 
+ * @author peizhaoo
+ * 
+ */
+public class CodeGenerator {
+	ArrayList<SpecConstruct> _constructs;
+	
+}
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
new file mode 100644
index 0000000..f053ba4
--- /dev/null
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
@@ -0,0 +1,84 @@
+package edu.uci.eecs.specCompiler.codeGenerator;
+
+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.ConditionalInterface;
+import edu.uci.eecs.specCompiler.specExtraction.Construct;
+import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
+
+public class SemanticsChecker {
+	public final ArrayList<SpecConstruct> constructs;
+	public final HashMap<String, SpecConstruct> label2Construct;
+	public final HashMap<String, SpecConstruct> interfaceName2Construct;
+
+	public SemanticsChecker(ArrayList<SpecConstruct> constructs) {
+		this.constructs = constructs;
+		this.label2Construct = new HashMap<String, SpecConstruct>();
+		this.interfaceName2Construct = new HashMap<String, SpecConstruct>();
+	}
+
+	private void checkHBLabelConsistency(String interfaceName, String label)
+			throws SemanticsCheckerException {
+		if (!interfaceName2Construct.containsKey(interfaceName)) {
+			throw new SemanticsCheckerException(
+					"In global construct, no interface \""
+							+ interfaceName + "\"!");
+		} else {
+			InterfaceConstruct iConstruct = (InterfaceConstruct) interfaceName2Construct
+					.get(interfaceName).construct;
+			if (!iConstruct.hbConditions.containsKey(label)) {
+				throw new SemanticsCheckerException("Interface "
+						+ interfaceName
+						+ " doesn't contain HB_codition: " + label
+						+ "!");
+			}
+		}
+	}
+
+	public void check() throws SemanticsCheckerException {
+		boolean hasGlobalConstruct = false;
+		// First grab the information from the interface
+		for (int i = 0; i < constructs.size(); i++) {
+			Construct inst = constructs.get(i).construct;
+			if (inst instanceof InterfaceConstruct) {
+				InterfaceConstruct iConstruct = (InterfaceConstruct) inst;
+				interfaceName2Construct.put(iConstruct.name, constructs.get(i));
+			}
+		}
+
+		for (int i = 0; i < constructs.size(); i++) {
+			SpecConstruct inst = constructs.get(i);
+			Construct construct = inst.construct;
+			if (construct instanceof GlobalConstruct) {
+				GlobalConstruct theConstruct = (GlobalConstruct) construct;
+				if (!hasGlobalConstruct)
+					hasGlobalConstruct = true;
+				else {
+					throw new SemanticsCheckerException(
+							"More than one global construct!");
+				}
+
+				HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions = theConstruct.hbRelations;
+				for (ConditionalInterface left : hbConditions.keySet()) {
+					HashSet<ConditionalInterface> set = hbConditions.get(left);
+					checkHBLabelConsistency(left.interfaceName, left.hbConditionLabel);
+					for (ConditionalInterface right : set) {
+						checkHBLabelConsistency(right.interfaceName, right.hbConditionLabel);
+					}
+				}
+			} else if (construct instanceof PotentialCPDefineConstruct) {
+				PotentialCPDefineConstruct theConstruct = (PotentialCPDefineConstruct) construct;
+				label2Construct.put(theConstruct.label, inst);
+			} else if (construct instanceof CPDefineCheckConstruct) {
+				CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct;
+				label2Construct.put(theConstruct.label, inst);
+			}
+		}
+	}
+}
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsCheckerException.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsCheckerException.java
new file mode 100644
index 0000000..c44da96
--- /dev/null
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsCheckerException.java
@@ -0,0 +1,7 @@
+package edu.uci.eecs.specCompiler.codeGenerator;
+
+public class SemanticsCheckerException extends Exception {
+	public SemanticsCheckerException(String msg) {
+		super(msg);
+	}
+}
\ No newline at end of file
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
index ac6de02..eb4bdb2 100644
--- a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
@@ -179,6 +179,10 @@ public class SpecExtractor {
 		else
 			return line.substring(i, j + 1);
 	}
+	
+	public ArrayList<SpecConstruct> getConstructs() {
+		return this._constructs;
+	}
 
 	public static void main(String[] argvs) {
 		SpecExtractor extractor = new SpecExtractor();
-- 
2.34.1