Add experimental abstract interpreterabstract-interpreter

12 files changed, 895 insertions, 13 deletions

diff --git a/compiler/valacompiler.vala b/compiler/valacompiler.vala
index f271c6f48..51e3245dd 100644
--- a/compiler/valacompiler.vala
+++ b/compiler/valacompiler.vala
@@ -56,6 +56,7 @@ class Vala.Compiler {
 	static bool enable_checking;
 	static bool deprecated;
 	static bool experimental;
+	static bool abstract_interpreter;
 	static bool experimental_non_null;
 	static bool disable_dbus_transformation;
 	static bool disable_warnings;
@@ -109,6 +110,7 @@ class Vala.Compiler {
 		{ "enable-deprecated", 0, 0, OptionArg.NONE, ref deprecated, "Enable deprecated features", null },
 		{ "enable-experimental", 0, 0, OptionArg.NONE, ref experimental, "Enable experimental features", null },
 		{ "disable-warnings", 0, 0, OptionArg.NONE, ref disable_warnings, "Disable warnings", null },
+		{ "enable-abstract-interpreter", 0, 0, OptionArg.NONE, ref abstract_interpreter, "Enable experimental abstract interpreter", null },
 		{ "enable-experimental-non-null", 0, 0, OptionArg.NONE, ref experimental_non_null, "Enable experimental enhancements for non-null types", null },
 		{ "disable-dbus-transformation", 0, 0, OptionArg.NONE, ref disable_dbus_transformation, "Disable transformation of D-Bus member names", null },
 		{ "cc", 0, 0, OptionArg.STRING, ref cc_command, "Use COMMAND as C compiler command", "COMMAND" },
@@ -210,6 +212,7 @@ class Vala.Compiler {
 		context.checking = enable_checking;
 		context.deprecated = deprecated;
 		context.experimental = experimental;
+		context.abstract_interpreter = abstract_interpreter;
 		context.experimental_non_null = experimental_non_null;
 		context.dbus_transformation = !disable_dbus_transformation;
 		context.report.enable_warnings = !disable_warnings;
@@ -416,8 +419,13 @@ class Vala.Compiler {
 			return quit ();
 		}
 
-		var flow_analyzer = new FlowAnalyzer ();
-		flow_analyzer.analyze (context);
+		if (!context.abstract_interpreter) {
+			var flow_analyzer = new FlowAnalyzer ();
+			flow_analyzer.analyze (context);
+		} else {
+			var abstract_interpreter = new AbstractInterpreter ();
+			abstract_interpreter.run (context);
+		}
 
 		if (context.report.get_errors () > 0) {
 			return quit ();
diff --git a/vala/Makefile.am b/vala/Makefile.am
index 7148e44fe..9efbadd88 100644
--- a/vala/Makefile.am
+++ b/vala/Makefile.am
@@ -15,6 +15,7 @@ noinst_LTLIBRARIES = \
 	$(NULL)
 
 libvalacore_la_VALASOURCES = \
+	valaabstractinterpreter.vala \
 	valaaddressofexpression.vala \
 	valaarraycreationexpression.vala \
 	valaarraylengthfield.vala \
diff --git a/vala/valaabstractinterpreter.vala b/vala/valaabstractinterpreter.vala
new file mode 100644
index 000000000..10498f7d3
--- /dev/null
+++ b/vala/valaabstractinterpreter.vala
@@ -0,0 +1,779 @@
+/* valaabstractinterpreter.vala
+ *
+ * Copyright (C) 2009  Jürg Billeter
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Lesser General Public License for more details.
+
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301  USA
+ *
+ * Author:
+ * 	Jürg Billeter <j@bitron.ch>
+ */
+
+public class Vala.AbstractInterpreter : CodeVisitor {
+	CodeContext context;
+
+	State current_state;
+	List<State> loop_init_states;
+	State loop_exit_state;
+	List<State> try_exit_states;
+	List<State> switch_exit_states;
+	List<State> method_exit_states;
+
+	BooleanType true_type;
+	BooleanType false_type;
+
+	abstract class Statement {
+		public abstract bool equal (Statement stmt);
+
+		public virtual Ternary implies (Ternary value, Statement stmt) {
+			return Ternary.UNKNOWN;
+		}
+
+		public abstract string to_string ();
+	}
+
+	class VariableStatement : Statement {
+		public LocalVariable local;
+		public DataType data_type;
+
+		public VariableStatement (LocalVariable local, DataType data_type) {
+			this.local = local;
+			this.data_type = data_type;
+		}
+
+		public override bool equal (Statement stmt) {
+			var var_stmt = stmt as VariableStatement;
+			if (var_stmt == null) {
+				return false;
+			}
+
+			return var_stmt.local == local && var_stmt.data_type.compatible (data_type) && data_type.compatible (var_stmt.data_type);
+		}
+
+		public override Ternary implies (Ternary value, Statement stmt) {
+			var var_stmt = stmt as VariableStatement;
+			if (var_stmt == null) {
+				return Ternary.UNKNOWN;
+			}
+
+			if (var_stmt.local != local) {
+				return Ternary.UNKNOWN;
+			}
+
+			bool maybe_compatible = false;
+
+			if (data_type.compatible (var_stmt.data_type)) {
+				if (value == Ternary.TRUE) {
+					return Ternary.TRUE;
+				} else {
+					maybe_compatible = true;
+				}
+			}
+			if (var_stmt.data_type.compatible (data_type)) {
+				if (value == Ternary.FALSE) {
+					return Ternary.FALSE;
+				} else {
+					maybe_compatible = true;
+				}
+			}
+			if (data_type.data_type is Interface || var_stmt.data_type.data_type is Interface) {
+				// if either type is an interface, it might be compatible
+				maybe_compatible = true;
+			}
+
+			if (!maybe_compatible && value == Ternary.TRUE) {
+				// fully incompatible type
+				return Ternary.FALSE;
+			} else {
+				return Ternary.UNKNOWN;
+			}
+		}
+
+		public override string to_string () {
+			var bool_type = data_type as BooleanType;
+			if (bool_type != null && bool_type.value_set) {
+				return "%s is %s".printf (local.name, bool_type.value.to_string ());
+			} else {
+				return "%s is %s".printf (local.name, data_type.to_string ());
+			}
+		}
+	}
+
+	class ErrorStatement : Statement {
+		public ErrorType? error_type;
+
+		public override bool equal (Statement stmt) {
+			var error_stmt = stmt as ErrorStatement;
+			if (error_stmt == null) {
+				return false;
+			}
+
+			if (error_type == null || error_stmt.error_type == null) {
+				return error_type == error_stmt.error_type;
+			}
+
+			return error_stmt.error_type.compatible (error_type) && error_type.compatible (error_stmt.error_type);
+		}
+
+		public override Ternary implies (Ternary value, Statement stmt) {
+			var error_stmt = stmt as ErrorStatement;
+			if (error_stmt == null) {
+				return Ternary.UNKNOWN;
+			}
+
+			if (error_stmt.error_type == error_type) {
+				return value;
+			}
+
+			if (error_type == null) {
+				// no error
+				if (value == Ternary.TRUE) {
+					return Ternary.FALSE;
+				}
+			}
+			if (error_stmt.error_type == null) {
+				if (value == Ternary.TRUE) {
+					return Ternary.FALSE;
+				}
+			}
+
+			bool maybe_compatible = false;
+
+			if (error_type.compatible (error_stmt.error_type)) {
+				if (value == Ternary.TRUE) {
+					return Ternary.TRUE;
+				} else {
+					maybe_compatible = true;
+				}
+			}
+			if (error_stmt.error_type.compatible (error_type)) {
+				if (value == Ternary.FALSE) {
+					return Ternary.FALSE;
+				} else {
+					maybe_compatible = true;
+				}
+			}
+
+			if (!maybe_compatible && value == Ternary.TRUE) {
+				// fully incompatible type
+				return Ternary.FALSE;
+			} else {
+				return Ternary.UNKNOWN;
+			}
+		}
+
+		public override string to_string () {
+			if (error_type == null) {
+				return "no error";
+			} else {
+				return "error is %s".printf (error_type.to_string ());
+			}
+		}
+	}
+
+	class FalseStatement : Statement {
+		public override bool equal (Statement stmt) {
+			return stmt is FalseStatement;
+		}
+
+		public override Ternary implies (Ternary value, Statement stmt) {
+			if (value == Ternary.TRUE) {
+				return Ternary.TRUE;
+			}
+
+			return Ternary.UNKNOWN;
+		}
+
+		public override string to_string () {
+			return "false";
+		}
+	}
+
+	enum Ternary {
+		UNKNOWN,
+		TRUE,
+		FALSE
+	}
+
+	class State {
+		public List<Statement> statements = new ArrayList<Statement> ();
+
+		int n_valid_states = 1;
+		public char[,] values = new char[4,4];
+
+		public State copy () {
+			var result = new State ();
+			foreach (var statement in statements) {
+				result.statements.add (statement);
+			}
+			result.values = values;
+			result.n_valid_states = n_valid_states;
+			return result;
+		}
+
+		void maybe_resize (int n_states, int n_statements) {
+			bool do_resize = false;
+			int new_n_states = values.length[0];
+			int new_n_statements = values.length[1];
+			while (new_n_states < n_states) {
+				new_n_states *= 2;
+				do_resize = true;
+			}
+			while (new_n_statements < n_statements) {
+				new_n_statements *= 2;
+				do_resize = true;
+			}
+
+			if (do_resize) {
+				var new_values = new char[new_n_states, new_n_statements];
+				for (int i = 0; i < values.length[0]; i++) {
+					for (int j = 0; j < values.length[1]; j++) {
+						new_values[i,j] = values[i,j];
+					}
+				}
+				values = (owned) new_values;
+			}
+		}
+
+		int get_statement (Statement stmt) {
+			int stmt_index = -1;
+			int stmt_i = 0;
+			foreach (var statement in statements) {
+				if (stmt.equal (statement)) {
+					stmt_index = stmt_i;
+					break;
+				}
+				stmt_i++;
+			}
+			return stmt_index;
+		}
+
+		int ensure_statement (Statement stmt) {
+			int stmt_index = get_statement (stmt);
+			if (stmt_index < 0) {
+				// add new statement to array
+				stmt_index = statements.size;
+				statements.add (stmt);
+				maybe_resize (n_valid_states, statements.size);
+				// ensure that entailment is followed
+				for (int stmt_i = 0; stmt_i < stmt_index; stmt_i++) {
+					for (int state = 0; state < n_valid_states; state++) {
+						Ternary t = statements[stmt_i].implies ((Ternary) values[state,stmt_i], stmt);
+						if (t != Ternary.UNKNOWN) {
+							values[state,stmt_index] = t;
+						}
+					}
+				}
+			}
+			return stmt_index;
+		}
+
+		public void unset_variable (LocalVariable local) {
+			for (int i = 0; i < statements.size; i++) {
+				var var_stmt = statements[i] as VariableStatement;
+				if (var_stmt != null && var_stmt.local == local) {
+					// remove statement
+					for (int state = 0; state < n_valid_states; state++) {
+						values[state,i] = values[state,statements.size - 1];
+						values[state,statements.size - 1] = Ternary.UNKNOWN;
+					}
+					statements[i] = statements[statements.size - 1];
+					statements.remove_at (statements.size - 1);
+
+					i--;
+					continue;
+				}
+			}
+		}
+
+		public void assert (List<Statement> disjunction) {
+			if (disjunction.size == 0) {
+				// assert nothing
+				return;
+			}
+
+			// ensure we have all statements of the disjunction in the array
+			int[] stmt_index = new int[disjunction.size];
+			int assert_stmt_index = 0;
+			foreach (var assert_statement in disjunction) {
+				stmt_index[assert_stmt_index] = ensure_statement (assert_statement);;
+				assert_stmt_index++;
+			}
+
+			for (int state = 0; state < n_valid_states; state++) {
+				bool is_true = false;
+				int n_unknown = 0;
+				int[] unknown_index = new int[disjunction.size];
+				for (int i = 0; i < disjunction.size; i++) {
+					Ternary t = (Ternary) values[state,stmt_index[i]];
+					if (t == Ternary.TRUE) {
+						is_true = true;
+						break;
+					} else if (t == Ternary.UNKNOWN) {
+						unknown_index[n_unknown] = i;
+						n_unknown++;
+					}
+				}
+				if (is_true) {
+					// disjunction already true in this state, nothing to do
+					continue;
+				} else {
+					if (n_unknown > 0) {
+						n_valid_states += n_unknown;
+						maybe_resize (n_valid_states, statements.size);
+						for (int j = 0; j < n_unknown; j++) {
+							for (int i = 0; i < statements.size; i++) {
+								Ternary t = (Ternary) values[state,i];
+								Ternary u = disjunction[unknown_index[j]].implies (Ternary.TRUE, statements[i]);
+								if (u != Ternary.UNKNOWN) {
+									t = u;
+								}
+								values[n_valid_states - n_unknown + j,i] = t;
+							}
+							values[n_valid_states - n_unknown + j,stmt_index[unknown_index[j]]] = Ternary.TRUE;
+						}
+					}
+
+					// remove state
+					for (int i = 0; i < statements.size; i++) {
+						values[state,i] = values[n_valid_states - 1,i];
+						values[n_valid_states - 1,i] = Ternary.UNKNOWN;
+					}
+					n_valid_states--;
+
+					state--;
+					continue;
+				}
+			}
+		}
+
+		Ternary check (List<Statement> disjunction) {
+			// true => true
+			int[] conditions11 = {};
+			// false => true
+			int[] conditions01 = {};
+			// true => false
+			int[] conditions10 = {};
+			// false => false
+			int[] conditions00 = {};
+			for (int i = 0; i < statements.size; i++) {
+				foreach (var stmt in disjunction) {
+					if (statements[i].implies (Ternary.TRUE, stmt) == Ternary.TRUE) {
+						conditions11 += i;
+					}
+					if (statements[i].implies (Ternary.FALSE, stmt) == Ternary.TRUE) {
+						conditions01 += i;
+					}
+					if (statements[i].implies (Ternary.TRUE, stmt) == Ternary.FALSE) {
+						conditions10 += i;
+					}
+					if (statements[i].implies (Ternary.FALSE, stmt) == Ternary.FALSE) {
+						conditions00 += i;
+					}
+				}
+			}
+
+			int n_true = 0, n_false = 0, n_unknown = 0;
+			for (int state = 0; state < n_valid_states; state++) {
+				bool is_true = false, is_false = false;
+				foreach (int i in conditions11) {
+					if (values[state,i] == Ternary.TRUE) {
+						is_true = true;
+						break;
+					}
+				}
+				foreach (int i in conditions01) {
+					if (values[state,i] == Ternary.FALSE) {
+						is_true = true;
+						break;
+					}
+				}
+				foreach (int i in conditions10) {
+					if (values[state,i] == Ternary.TRUE) {
+						is_false = true;
+						break;
+					}
+				}
+				foreach (int i in conditions00) {
+					if (values[state,i] == Ternary.FALSE) {
+						is_false = true;
+						break;
+					}
+				}
+				if (is_true) {
+					n_true++;
+				} else if (is_false) {
+					n_false++;
+				} else {
+					n_unknown++;
+				}
+			}
+
+			if (n_false == 0 && n_unknown == 0) {
+				return Ternary.TRUE;
+			} else if (n_true == 0 && n_unknown == 0) {
+				return Ternary.FALSE;
+			} else {
+				return Ternary.UNKNOWN;
+			}
+		}
+
+		public bool is_true (List<Statement> disjunction) {
+			return check (disjunction) == Ternary.TRUE;
+		}
+
+		public bool is_false (List<Statement> disjunction) {
+			return check (disjunction) == Ternary.FALSE;
+		}
+
+		public bool maybe_true (List<Statement> disjunction) {
+			return check (disjunction) != Ternary.FALSE;
+		}
+
+		public bool maybe_false (List<Statement> disjunction) {
+			return check (disjunction) != Ternary.TRUE;
+		}
+
+		public static bool equal (State state1, State state2) {
+			if (state1.statements.size != state2.statements.size) {
+				return false;
+			}
+			int[] mapping = new int[state1.statements.size];
+			for (int i = 0; i < state2.statements.size; i++) {
+				int stmt_index = state1.get_statement (state2.statements[i]);
+				if (stmt_index < 0) {
+					return false;
+				}
+				mapping[stmt_index] = i;
+			}
+			for (int s1 = 0; s1 < state1.n_valid_states; s1++) {
+				bool found = false;
+				for (int s2 = 0; s2 < state2.n_valid_states; s2++) {
+					found = true;
+					for (int i = 0; i < mapping.length; i++) {
+						if (state1.values[s1,i] != state2.values[s2,mapping[i]]) {
+							found = false;
+							break;
+						}
+					}
+					if (found) {
+						break;
+					}
+				}
+				if (!found) {
+					return false;
+				}
+			}
+			for (int s2 = 0; s2 < state2.n_valid_states; s2++) {
+				bool found = false;
+				for (int s1 = 0; s1 < state1.n_valid_states; s1++) {
+					found = true;
+					for (int i = 0; i < mapping.length; i++) {
+						if (state1.values[s1,i] != state2.values[s2,mapping[i]]) {
+							found = false;
+							break;
+						}
+					}
+					if (found) {
+						break;
+					}
+				}
+				if (!found) {
+					return false;
+				}
+			}
+			return true;
+		}
+
+		public static State union (State state1, State state2) {
+			var copy2 = state2.copy ();
+			foreach (var stmt in state1.statements) {
+				copy2.ensure_statement (stmt);
+			}
+
+			var result = state1.copy ();
+			int[] mapping = new int[copy2.statements.size];
+			for (int i = 0; i < copy2.statements.size; i++) {
+				mapping[result.ensure_statement (copy2.statements[i])] = i;
+			}
+			result.n_valid_states += copy2.n_valid_states;
+			result.maybe_resize (result.n_valid_states, result.statements.size);
+			for (int state = 0; state < copy2.n_valid_states; state++) {
+				for (int i = 0; i < result.statements.size; i++) {
+					result.values[state1.n_valid_states + state, i] = copy2.values[state,mapping[i]];
+				}
+			}
+			return result;
+		}
+
+		public void print () {
+			for (int state = 0; state < n_valid_states; state++) {
+				stderr.printf ("\tState %d: ", state);
+				for (int i = 0; i < statements.size; i++) {
+					switch (values[state, i]) {
+					case Ternary.TRUE:
+						stderr.printf ("%s, ", statements[i].to_string ());
+						break;
+					case Ternary.FALSE:
+						stderr.printf ("!(%s), ", statements[i].to_string ());
+						break;
+					default:
+						break;
+					}
+				}
+				stderr.printf ("\n");
+			}
+		}
+	}
+
+	public AbstractInterpreter () {
+	}
+
+	public void run (CodeContext context) {
+		this.context = context;
+
+		true_type = new BooleanType ((Struct) context.root.scope.lookup ("bool"));
+		true_type.value = true;
+		true_type.value_set = true;
+
+		false_type = new BooleanType ((Struct) context.root.scope.lookup ("bool"));
+		false_type.value = false;
+		false_type.value_set = true;
+
+		/* we're only interested in non-pkg source files */
+		var source_files = context.get_source_files ();
+		foreach (SourceFile file in source_files) {
+			if (!file.external_package) {
+				file.accept (this);
+			}
+		}
+	}
+
+	public override void visit_source_file (SourceFile source_file) {
+		source_file.accept_children (this);
+	}
+
+	public override void visit_class (Class cl) {
+		cl.accept_children (this);
+	}
+
+	public override void visit_struct (Struct st) {
+		st.accept_children (this);
+	}
+
+	public override void visit_interface (Interface iface) {
+		iface.accept_children (this);
+	}
+
+	public override void visit_enum (Enum en) {
+		en.accept_children (this);
+	}
+
+	public override void visit_error_domain (ErrorDomain ed) {
+		ed.accept_children (this);
+	}
+
+	List<Statement> create_list (Statement? stmt) {
+		var result = new ArrayList<Statement> ();
+		if (stmt != null) {
+			result.add (stmt);
+		}
+		return result;
+	}
+
+	public override void visit_method (Method m) {
+		if (m.body == null) {
+			return;
+		}
+
+		current_state = new State ();
+
+		// no error has happened when entering the method
+		current_state.assert (create_list (new ErrorStatement ()));
+
+		m.body.accept (this);
+
+		current_state = null;
+	}
+
+	public override void visit_block (Block b) {
+		b.accept_children (this);
+	}
+
+	bool unreachable (CodeNode? node = null) {
+		if (current_state.is_true (create_list (new FalseStatement ()))) {
+			if (node != null) {
+				Report.warning (node.source_reference, "unreachable code");
+			}
+			return true;
+		}
+		return false;
+	}
+
+	public override void visit_declaration_statement (DeclarationStatement stmt) {
+		visit_statement (stmt);
+
+		var local = stmt.declaration as LocalVariable;
+		if (local != null && local.initializer != null) {
+			current_state.assert (create_list (new VariableStatement (local, local.initializer.value_type)));
+		}
+	}
+
+	void visit_statement (Vala.Statement stmt) {
+		if (unreachable (stmt)) {
+			return;
+		}
+
+		var used_variables = new ArrayList<LocalVariable> ();
+		stmt.get_used_variables (used_variables);
+		foreach (var local in used_variables) {
+			if (current_state.maybe_false (create_list (new VariableStatement (local, local.variable_type)))) {
+				Report.error (stmt.source_reference, "use of possibly unassigned local variable `%s'".printf (local.name));
+			}
+		}
+
+		var variables = new ArrayList<LocalVariable> ();
+		var types = new ArrayList<DataType> ();
+		stmt.get_assumptions (variables, types);
+		for (int i = 0; i < variables.size; i++) {
+			if (current_state.maybe_false (create_list (new VariableStatement (variables[i], types[i])))) {
+				Report.error (stmt.source_reference, "cannot convert `%s' from `%s' to `%s'".printf (variables[i].name, variables[i].variable_type.to_string (), types[i].to_string ()));
+			}
+		}
+	}
+
+	public override void visit_expression_statement (ExpressionStatement stmt) {
+		visit_statement (stmt);
+
+		var assign = stmt.expression as Assignment;
+		if (assign != null) {
+			var local = assign.left.symbol_reference as LocalVariable;
+			if (local != null) {
+				current_state.unset_variable (local);
+				current_state.assert (create_list (new VariableStatement (local, assign.right.value_type)));
+			}
+		}
+	}
+
+	public override void visit_if_statement (IfStatement stmt) {
+		visit_statement (stmt);
+
+		var before_state = current_state;
+		State true_state = before_state.copy ();
+		State false_state = before_state.copy ();
+
+		var be = stmt.condition as BinaryExpression;
+		var ue = stmt.condition as UnaryExpression;
+		if (be != null && be.operator == BinaryOperator.INEQUALITY && (be.left is NullLiteral || be.right is NullLiteral)) {
+			var local = be.left.symbol_reference as LocalVariable;
+			if (local == null) {
+				local = be.right.symbol_reference as LocalVariable;
+			}
+			if (local != null) {
+				var non_null_type = local.variable_type.copy ();
+				non_null_type.nullable = false;
+				if (before_state.is_false (create_list (new VariableStatement (local, non_null_type)))) {
+					// unreachable
+					true_state.assert (create_list (new FalseStatement ()));
+				}
+				true_state.assert (create_list (new VariableStatement (local, non_null_type)));
+			}
+		} else if (ue != null && ue.operator == UnaryOperator.LOGICAL_NEGATION) {
+			var local = ue.inner.symbol_reference as LocalVariable;
+			if (local != null) {
+				if (before_state.is_true (create_list (new VariableStatement (local, true_type)))) {
+					// true unreachable
+					true_state.assert (create_list (new FalseStatement ()));
+				} else if (before_state.is_true (create_list (new VariableStatement (local, false_type)))) {
+					// false unreachable
+					false_state.assert (create_list (new FalseStatement ()));
+				}
+				true_state.assert (create_list (new VariableStatement (local, false_type)));
+				false_state.assert (create_list (new VariableStatement (local, true_type)));
+			}
+		}
+
+		/*stderr.printf ("before if state:\n");
+		before_state.print ();
+		stderr.printf ("if true init state:\n");
+		true_state.print ();
+		stderr.printf ("if false init state:\n");
+		false_state.print ();*/
+
+		current_state = true_state;
+		stmt.true_statement.accept (this);
+		true_state = current_state;
+
+		if (stmt.false_statement != null) {
+			current_state = false_state;
+			stmt.false_statement.accept (this);
+			false_state = current_state;
+		}
+
+		current_state = State.union (true_state, false_state);
+
+		/*stderr.printf ("after if state:\n");
+		current_state.print ();*/
+	}
+
+	void add_loop_init_state () {
+		foreach (var state in loop_init_states) {
+			if (State.equal (state, current_state)) {
+				return;
+			}
+		}
+		loop_init_states.add (current_state);
+		/*stderr.printf ("added loop init state %d:", loop_init_states.size - 1);
+		current_state.print ();*/
+	}
+
+	public override void visit_loop (Loop stmt) {
+		visit_statement (stmt);
+
+		loop_init_states = new ArrayList<State> ();
+		loop_init_states.add (current_state);
+
+		loop_exit_state = new State ();
+		// unreachable so far
+		loop_exit_state.assert (create_list (new FalseStatement ()));
+
+		for (int i = 0; i < loop_init_states.size; i++) {
+			current_state = loop_init_states[i].copy ();
+
+			/*stderr.printf ("loop init state %d\n", i);
+			current_state.print ();*/
+
+			stmt.body.accept (this);
+
+			//stderr.printf ("end of loop body\n");
+
+			if (!unreachable ()) {
+				add_loop_init_state ();
+			}
+		}
+
+		current_state = loop_exit_state;
+
+		/*stderr.printf ("loop exit state\n");
+		current_state.print ();*/
+	}
+
+	public override void visit_break_statement (BreakStatement stmt) {
+		// TODO support break in switch statement
+
+		loop_exit_state = State.union (loop_exit_state, current_state);
+		// statements after break unreachable
+		current_state.assert (create_list (new FalseStatement ()));
+	}
+}
diff --git a/vala/valaassignment.vala b/vala/valaassignment.vala
index 0e381fea7..d2547a8fa 100644
--- a/vala/valaassignment.vala
+++ b/vala/valaassignment.vala
@@ -350,9 +350,13 @@ public class Vala.Assignment : Expression {
 				 * i.e. {left|right}.value_type == null, skip type check */
 
 				if (!right.value_type.compatible (left.value_type)) {
-					error = true;
-					Report.error (source_reference, "Assignment: Cannot convert from `%s' to `%s'".printf (right.value_type.to_string (), left.value_type.to_string ()));
-					return false;
+					if (analyzer.context.abstract_interpreter && right.symbol_reference is LocalVariable) {
+						parent_statement.assume ((LocalVariable) right.symbol_reference, left.value_type);
+					} else {
+						error = true;
+						Report.error (source_reference, "Assignment: Cannot convert from `%s' to `%s'".printf (right.value_type.to_string (), left.value_type.to_string ()));
+						return false;
+					}
 				}
 
 				if (!(ma.symbol_reference is Property)) {
diff --git a/vala/valabooleanliteral.vala b/vala/valabooleanliteral.vala
index bf0842fba..d2f469480 100644
--- a/vala/valabooleanliteral.vala
+++ b/vala/valabooleanliteral.vala
@@ -1,6 +1,6 @@
 /* valabooleanliteral.vala
  *
- * Copyright (C) 2006-2008  Jürg Billeter
+ * Copyright (C) 2006-2009  Jürg Billeter
  *
  * This library is free software; you can redistribute it and/or
  * modify it under the terms of the GNU Lesser General Public
@@ -68,7 +68,10 @@ public class Vala.BooleanLiteral : Literal {
 
 		checked = true;
 
-		value_type = analyzer.bool_type;
+		var bool_type = (BooleanType) analyzer.bool_type.copy ();
+		bool_type.value = this.value;
+		bool_type.value_set = true;
+		value_type = bool_type;
 
 		return !error;
 	}
diff --git a/vala/valabooleantype.vala b/vala/valabooleantype.vala
index b224a9359..3f51538e8 100644
--- a/vala/valabooleantype.vala
+++ b/vala/valabooleantype.vala
@@ -26,6 +26,9 @@ using GLib;
  * A boolean type.
  */
 public class Vala.BooleanType : ValueType {
+	public bool value { get; set; }
+	public bool value_set { get; set; }
+
 	public BooleanType (Struct type_symbol) {
 		base (type_symbol);
 	}
@@ -35,6 +38,32 @@ public class Vala.BooleanType : ValueType {
 		result.source_reference = source_reference;
 		result.value_owned = value_owned;
 		result.nullable = nullable;
+		result.value = value;
+		result.value_set = value_set;
 		return result;
 	}
+
+	public override bool compatible (DataType target_type) {
+		if (CodeContext.get ().experimental_non_null && nullable && !target_type.nullable) {
+			return false;
+		}
+
+		if (target_type.get_type_id () == "G_TYPE_VALUE") {
+			// allow implicit conversion to GValue
+			return true;
+		}
+
+		var bool_target_type = target_type as BooleanType;
+		if (bool_target_type != null) {
+			if (!bool_target_type.value_set) {
+				return true;
+			} else if (!value_set) {
+				return false;
+			} else {
+				return (this.value == bool_target_type.value);
+			}
+		}
+
+		return false;
+	}
 }
diff --git a/vala/valacodecontext.vala b/vala/valacodecontext.vala
index cd32378ba..65672cc7b 100644
--- a/vala/valacodecontext.vala
+++ b/vala/valacodecontext.vala
@@ -47,6 +47,11 @@ public class Vala.CodeContext {
 	public bool experimental { get; set; }
 
 	/**
+	 * Enable experimental abstract interpreter.
+	 */
+	public bool abstract_interpreter { get; set; }
+
+	/**
 	 * Enable experimental enhancements for non-null types.
 	 */
 	public bool experimental_non_null { get; set; }
diff --git a/vala/valacodenode.vala b/vala/valacodenode.vala
index f3ae4a4b8..312c76e95 100644
--- a/vala/valacodenode.vala
+++ b/vala/valacodenode.vala
@@ -194,4 +194,29 @@ public abstract class Vala.CodeNode {
 	public static string get_temp_name () {
 		return "." + (++last_temp_nr).to_string ();
 	}
+
+	List<LocalVariable> assumption_variables;
+	List<DataType> assumption_types;
+
+	// we should probably generate AssumeStatement objects instead that can be inserted before the current statement
+	// source reference could be copied from the original expression
+	public void assume (LocalVariable local, DataType type) {
+		if (assumption_variables == null) {
+			assumption_variables = new ArrayList<LocalVariable> ();
+			assumption_types = new ArrayList<DataType> ();
+		}
+		assumption_variables.add (local);
+		assumption_types.add (type);
+	}
+
+	public void get_assumptions (List<LocalVariable> variables, List<DataType> types) {
+		if (assumption_variables != null) {
+			foreach (var local in assumption_variables) {
+				variables.add (local);
+			}
+			foreach (var type in assumption_types) {
+				types.add (type);
+			}
+		}
+	}
 }
diff --git a/vala/valaifstatement.vala b/vala/valaifstatement.vala
index 0804bb466..9656ac18e 100644
--- a/vala/valaifstatement.vala
+++ b/vala/valaifstatement.vala
@@ -139,4 +139,12 @@ public class Vala.IfStatement : CodeNode, Statement {
 
 		return !error;
 	}
+
+	public override void get_defined_variables (Collection<LocalVariable> collection) {
+		condition.get_defined_variables (collection);
+	}
+
+	public override void get_used_variables (Collection<LocalVariable> collection) {
+		condition.get_used_variables (collection);
+	}
 }
diff --git a/vala/valalocalvariable.vala b/vala/valalocalvariable.vala
index 5ef1107fb..8a3cec57f 100644
--- a/vala/valalocalvariable.vala
+++ b/vala/valalocalvariable.vala
@@ -117,6 +117,11 @@ public class Vala.LocalVariable : Variable {
 			variable_type.value_owned = true;
 			variable_type.floating_reference = false;
 
+			var bool_type = variable_type as BooleanType;
+			if (bool_type != null) {
+				bool_type.value_set = false;
+			}
+
 			initializer.target_type = variable_type;
 		}
 
@@ -150,9 +155,13 @@ public class Vala.LocalVariable : Variable {
 			}
 
 			if (!initializer.value_type.compatible (variable_type)) {
-				error = true;
-				Report.error (source_reference, "Assignment: Cannot convert from `%s' to `%s'".printf (initializer.value_type.to_string (), variable_type.to_string ()));
-				return false;
+				if (analyzer.context.abstract_interpreter && initializer.symbol_reference is LocalVariable) {
+					((Statement) parent_node).assume ((LocalVariable) initializer.symbol_reference, variable_type);
+				} else {
+					error = true;
+					Report.error (source_reference, "Assignment: Cannot convert from `%s' to `%s'".printf (initializer.value_type.to_string (), variable_type.to_string ()));
+					return false;
+				}
 			}
 
 			if (initializer.value_type.is_disposable ()) {
diff --git a/vala/valasemanticanalyzer.vala b/vala/valasemanticanalyzer.vala
index e710912c5..55192fb0b 100644
--- a/vala/valasemanticanalyzer.vala
+++ b/vala/valasemanticanalyzer.vala
@@ -507,8 +507,12 @@ public class Vala.SemanticAnalyzer : CodeVisitor {
 		} else if (arg.target_type != null
 		           && (direction == ParameterDirection.IN || direction == ParameterDirection.REF)
 		           && !arg.value_type.compatible (arg.target_type)) {
-			Report.error (arg.source_reference, "Argument %d: Cannot convert from `%s' to `%s'".printf (i + 1, arg.value_type.to_string (), arg.target_type.to_string ()));
-			return false;
+			if (context.abstract_interpreter && arg.symbol_reference is LocalVariable) {
+				arg.parent_statement.assume ((LocalVariable) arg.symbol_reference, arg.target_type);
+			} else {
+				Report.error (arg.source_reference, "Argument %d: Cannot convert from `%s' to `%s'".printf (i + 1, arg.value_type.to_string (), arg.target_type.to_string ()));
+				return false;
+			}
 		} else if (arg.target_type != null
 		           && (direction == ParameterDirection.REF || direction == ParameterDirection.OUT)
 		           && !arg.target_type.compatible (arg.value_type)
diff --git a/vala/valaunaryexpression.vala b/vala/valaunaryexpression.vala
index d2d38ddd5..8a6c9ed35 100644
--- a/vala/valaunaryexpression.vala
+++ b/vala/valaunaryexpression.vala
@@ -178,7 +178,14 @@ public class Vala.UnaryExpression : Expression {
 				return false;
 			}
 
-			value_type = inner.value_type;
+			var bool_type = inner.value_type as BooleanType;
+			if (bool_type.value_set) {
+				bool_type = (BooleanType) bool_type.copy ();
+				bool_type.value = !bool_type.value;
+				value_type = bool_type;
+			} else {
+				value_type = inner.value_type;
+			}
 		} else if (operator == UnaryOperator.BITWISE_COMPLEMENT) {
 			// integer type
 			if (!is_integer_type (inner.value_type) && !(inner.value_type is EnumValueType)) {