Clean up constant check

loonwerks · May 16, 2014 · c0dbc1e · c0dbc1e
1 parent 73ecc2f
commit c0dbc1e
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 32 deletions.
diff --git a/jkind-common/src/jkind/util/CycleFinder.java b/jkind-common/src/jkind/util/CycleFinder.java
@@ -14,7 +14,7 @@ public static List<String> findCycle(Map<String, Set<String>> dependencies) {
 
 	private final Deque<String> callStack = new ArrayDeque<>();
 	private final Map<String, Set<String>> dependencies;
-	
+
 	private CycleFinder(Map<String, Set<String>> dependencies) {
 		this.dependencies = dependencies;
 	}
@@ -29,7 +29,7 @@ private List<String> findCycle() {
 
 		return null;
 	}
-	
+
 	private List<String> findCycle(String curr) {
 		if (callStack.contains(curr)) {
 			callStack.addLast(curr);
@@ -39,14 +39,16 @@ private List<String> findCycle(String curr) {
 			return new ArrayList<>(callStack);
 		}
 
-		callStack.addLast(curr);
-		for (String next : dependencies.get(curr)) {
-			List<String> cycle = findCycle(next);
-			if (cycle != null) {
-				return cycle;
+		if (dependencies.containsKey(curr)) {
+			callStack.addLast(curr);
+			for (String next : dependencies.get(curr)) {
+				List<String> cycle = findCycle(next);
+				if (cycle != null) {
+					return cycle;
+				}
 			}
+			callStack.removeLast();
 		}
-		callStack.removeLast();
 
 		return null;
 	}

diff --git a/jkind/src/jkind/analysis/StaticAnalyzer.java b/jkind/src/jkind/analysis/StaticAnalyzer.java
@@ -36,13 +36,13 @@ private static boolean checkErrors(Program program, Level nonlinear) {
 		result = result && TypesDefined.check(program);
 		result = result && TypeDependencyChecker.check(program);
 		result = result && enumsAndConstantsUnique(program);
-		result = result && constantsConstant(program);
 		result = result && ConstantDependencyChecker.check(program);
 		result = result && nodesUnique(program);
 		result = result && variablesUnique(program);
 		result = result && TypeChecker.check(program);
 		result = result && SubrangesNonempty.check(program);
 		result = result && ArraysNonempty.check(program);
+		result = result && constantsConstant(program);
 		result = result && DivisionChecker.check(program);
 		result = result && NodeDependencyChecker.check(program);
 		result = result && assignmentsSound(program);
@@ -128,18 +128,6 @@ private static boolean enumsAndConstantsUnique(Program program) {
 		return unique;
 	}
 
-	private static boolean constantsConstant(Program program) {
-		boolean constant = true;
-		ConstantAnalyzer constantAnalyzer = new ConstantAnalyzer(program.constants);
-		for (Constant c : program.constants) {
-			if (!c.expr.accept(constantAnalyzer)) {
-				Output.error(c.location, "constant " + c.id + " does not have a constant value");
-				constant = false;
-			}
-		}
-		return constant;
-	}
-
 	private static boolean nodesUnique(Program program) {
 		boolean unique = true;
 		Set<String> seen = new HashSet<>();
@@ -176,6 +164,18 @@ private static boolean variablesUnique(Node node) {
 		return unique;
 	}
 
+	private static boolean constantsConstant(Program program) {
+		boolean constant = true;
+		ConstantAnalyzer constantAnalyzer = new ConstantAnalyzer(program.constants);
+		for (Constant c : program.constants) {
+			if (!c.expr.accept(constantAnalyzer)) {
+				Output.error(c.location, "constant " + c.id + " does not have a constant value");
+				constant = false;
+			}
+		}
+		return constant;
+	}
+
 	private static boolean assignmentsSound(Program program) {
 		boolean sound = true;
 		for (Node node : program.nodes) {

diff --git a/jkind/src/jkind/analysis/TypeChecker.java b/jkind/src/jkind/analysis/TypeChecker.java
@@ -48,7 +48,7 @@
 public class TypeChecker implements ExprVisitor<Type> {
 	private final Map<String, Type> typeTable = new HashMap<>();
 	private final Map<String, Type> constantTable = new HashMap<>();
-	private final Map<String, Expr> constantDefinitionTable = new HashMap<>();
+	private final Map<String, Constant> constantDefinitionTable = new HashMap<>();
 	private final Map<String, EnumType> enumValueTable = new HashMap<>();
 	private final Map<String, Type> variableTable = new HashMap<>();
 	private final Map<String, Node> nodeTable;
@@ -93,18 +93,28 @@ private void populateConstantTable(List<Constant> constants) {
 		// The constantDefinitionTable is used for constants whose type has not
 		// yet been computed
 		for (Constant c : constants) {
-			constantDefinitionTable.put(c.id, c.expr);
+			constantDefinitionTable.put(c.id, c);
 		}
 
 		for (Constant c : constants) {
-			Type actual = c.expr.accept(this);
-			if (c.type == null) {
-				constantTable.put(c.id, actual);
-			} else {
-				Type expected = resolveType(c.type);
-				compareTypeAssignment(c.expr, expected, actual);
-				constantTable.put(c.id, expected);
-			}
+			addConstant(c);
+		}
+	}
+
+	private Type addConstant(Constant c) {
+		if (constantTable.containsKey(c.id)) {
+			return constantTable.get(c.id);
+		}
+
+		Type actual = c.expr.accept(this);
+		if (c.type == null) {
+			constantTable.put(c.id, actual);
+			return actual;
+		} else {
+			Type expected = resolveType(c.type);
+			compareTypeAssignment(c.expr, expected, actual);
+			constantTable.put(c.id, expected);
+			return expected;
 		}
 	}
 
@@ -387,7 +397,7 @@ public Type visit(IdExpr e) {
 		} else if (constantTable.containsKey(e.id)) {
 			return constantTable.get(e.id);
 		} else if (constantDefinitionTable.containsKey(e.id)) {
-			return constantDefinitionTable.get(e.id).accept(this);
+			return addConstant(constantDefinitionTable.get(e.id));
 		} else if (enumValueTable.containsKey(e.id)) {
 			return enumValueTable.get(e.id);
 		} else {