All tests pass except one !

1 files changed, 33 insertions, 30 deletions

diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index 79d4d2c..5f03775 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -14,10 +14,15 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
 	let p1 (e, l) =
 		binop AST_PLUS (e, l) (AST_int_const("1", l), l)
 
+    let bottom_with_vars =
+        List.fold_left E.addvar E.bottom
+
 	let rec condition cond env =
 		begin match fst cond with
 		| AST_binary (AST_LESS_EQUAL, e1, e2) ->
-			E.compare env e1 e2
+			E.compare_leq env e1 e2
+		| AST_binary (AST_EQUAL, e1, e2) ->
+            E.compare_eq env e1 e2
 		| AST_binary (AST_AND, e1, e2) ->
 			E.meet (condition e1 env) (condition e2 env)
 		| AST_binary (AST_OR, e1, e2) ->
@@ -59,10 +64,6 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
 			condition
 				(binop AST_LESS e2 e1)
 				env
-		| AST_binary (AST_EQUAL, e1, e2) ->
-			condition
-				(binop AST_AND (binop AST_LESS_EQUAL e1 e2) (binop AST_LESS_EQUAL e2 e1))
-				env
 		| AST_binary (AST_NOT_EQUAL, e1, e2) ->
 			condition
 				(binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
@@ -91,31 +92,33 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
 			let e2 = (interp_stmt (condition (neg cond) env) eb) in
 			E.join e1 e2
 		| AST_while (cond, body) ->
-			let unroll_count = 3 in
-			let rec iter n i x =
-				(* Format.printf "(iter %d) i:%s x:%s @." n (E.var_str i (E.vars i))
-								(E.var_str x (E.vars x)); *)
-				let out_state = condition (neg cond) i in
-				let next_step = interp_stmt (condition cond i) body in
-				(* Format.printf ". next step: %s@." (E.var_str next_step (E.vars next_step)); *)
-				if n < unroll_count then
-					E.join
-						out_state
-						(iter (n+1) next_step x)
-				else
-					let env2 =
-						E.widen
-							i
-							next_step
-					in
-						if env2 = i
-							then env2
-							else E.join
-								out_state
-								(iter (n+1) env2 x)
-			in
-			condition (neg cond) (iter 0 env env)
-		| AST_HALT -> E.bottom
+            (* loop unrolling *)
+            let rec unroll u = function
+                | 0 -> u, bottom_with_vars (E.vars env)
+                | n ->
+                     let prev_u, u_prev_u = unroll u (n-1) in
+                     interp_stmt (condition cond prev_u) body,
+                     E.join u_prev_u (condition (neg cond) prev_u)
+            in
+            let env, u_u = unroll env 3 in
+            (* widening *)
+            let widen_delay = 3 in
+            let fsharp i =
+                let next_step = interp_stmt (condition cond i) body in
+                E.join env next_step
+            in
+            let rec iter n i =
+                let i' =
+                    (if n < widen_delay then E.join else E.widen)
+                        i
+                        (fsharp i)
+                in
+                if i = i' then i else iter (n+1) i'
+            in
+            let x = iter 0 env in
+            let y = fix fsharp x in     (* decreasing iteration *)
+            E.join (condition (neg cond) y) u_u
+		| AST_HALT -> bottom_with_vars (E.vars env)
 		| AST_assert cond ->
 			if not
 				(E.is_bot (condition (neg cond) env))