All tests pass except one !

6 files changed, 165 insertions, 58 deletions

diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index 05473aa..5c00fbd 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -15,7 +15,8 @@ module type ENVIRONMENT_DOMAIN = sig
 
 	(* abstract operation *)
 	val assign	: t -> id -> expr ext -> t		(*    S[id <- expr]     *)
-	val compare : t -> expr ext -> expr ext -> t    (*    S[expr <= expr ?] *)
+	val compare_leq : t -> expr ext -> expr ext -> t    (*    S[expr <= expr ?] *)
+	val compare_eq : t -> expr ext -> expr ext -> t    (*    S[expr = expr ?] *)
 
 	(* set-theoretic operations *)
 	val join 	: t -> t -> t		(* union *)
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))
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 7221df1..8ac6a2a 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -61,31 +61,33 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 	let assign x id expr = strict_apply
 		(fun env -> Env (VarMap.add id (eval env expr) env))
 		x
-	let compare x e1 e2 =
+	let compare f x e1 e2 =
 		strict_apply (fun env -> match fst e1, fst e2 with
 				| AST_identifier(a, _), AST_identifier(b, _) ->
 					let v1, v2 = get_var env a, get_var env b in
-					let v1', v2' = V.leq v1 v2 in
+					let v1', v2' = f v1 v2 in
 					Env (VarMap.add a v1' (VarMap.add b v2' env))
 				| AST_identifier(a, _), _ ->
 					let v1, v2 = get_var env a, eval env e2 in
-					let v1', v2' = V.leq v1 v2 in
+					let v1', v2' = f v1 v2 in
 					if V.bottom = v2'
 						then Bot
 						else Env (VarMap.add a v1' env)
 				| _, AST_identifier(b, _) ->
 					let v1, v2 = eval env e1, get_var env b in
-					let v1', v2' = V.leq v1 v2 in
+					let v1', v2' = f v1 v2 in
 					if V.bottom = v1'
 						then Bot
 						else Env (VarMap.add b v2' env)
 				| _ ->
 					let v1, v2 = eval env e1, eval env e2 in
-					let v1', v2' = V.leq v1 v2 in
+					let v1', v2' = f v1 v2 in
 					if V.bottom = v1' ||V.bottom = v2'
 						then Bot
 						else Env env)
 			x
+    let compare_leq = compare V.leq
+    let compare_eq = compare (fun x y -> let r = V.meet x y in r, r)
 
 	let join a b = match a, b with
 		| Bot, x | x, Bot -> x
diff --git a/abstract/relational_apron.ml b/abstract/relational_apron.ml
index bd078cf..926d2a9 100644
--- a/abstract/relational_apron.ml
+++ b/abstract/relational_apron.ml
@@ -1,3 +1,4 @@
+open Abstract_syntax_tree
 open Apron
 open Util
 open Environment_domain
@@ -11,19 +12,86 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
     (* abstract elements *)
     type t = man Abstract1.t
 
+    (* translation in trees *)
+    let rec texpr_of_expr e =
+        match fst e with
+        | AST_identifier (id, _) -> Texpr1.Var (Var.of_string id)
+        | AST_int_const (s, _) -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_string s))
+        | AST_int_rand ((s, _), (t, _)) ->
+            Texpr1.Cst (Coeff.i_of_mpqf (Mpqf.of_string s) (Mpqf.of_string t))
+        | AST_unary(AST_UNARY_PLUS, e) ->
+            texpr_of_expr e
+        | AST_unary(AST_UNARY_MINUS, e) ->
+            (*
+            (* APRON bug ? Unary negate seems to not work correctly... *)
+            Texpr1.Unop(
+                Texpr1.Neg,
+                (texpr_of_expr e),
+                Texpr1.Int,
+                Texpr1.Zero)
+            *)
+            Texpr1.Binop(
+                Texpr1.Sub,
+                Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")),
+                (texpr_of_expr e),
+                Texpr1.Int,
+                Texpr1.Zero)
+        | AST_binary( op, e1, e2) ->
+            let f = match op with
+            | AST_PLUS -> Texpr1.Add
+            | AST_MINUS -> Texpr1.Sub
+            | AST_MULTIPLY -> Texpr1.Mul
+            | AST_DIVIDE -> Texpr1.Div
+            | AST_MODULO -> Texpr1.Mod
+            | _ -> assert false
+            in
+            Texpr1.Binop
+                (f, (texpr_of_expr e1), (texpr_of_expr e2), Texpr1.Int, Texpr1.Zero)
+        | _ -> assert false
+
     (* implementation *)
     let init = Abstract1.top manager (Environment.make  [||] [||])
     let bottom = Abstract1.bottom manager (Environment.make [||] [||])
     let is_bot = Abstract1.is_bottom manager
 
-    let addvar x id = x (* TODO *)
-    let rmvar x id = x (* TODO *)
+    let addvar x id =
+        let env = Abstract1.env x in
+        let env2 = Environment.add env [| Var.of_string id |] [||] in
+        Abstract1.change_environment manager x env2 false
+    let rmvar x id =
+        let env = Abstract1.env x in
+        let env2 = Environment.remove env [| Var.of_string id |] in
+        Abstract1.change_environment manager x env2 false
     let vars x =
         List.map Var.to_string @@
-        Array.to_list @@ snd @@ Environment.vars @@ Abstract1.env x
+        Array.to_list @@ fst @@ Environment.vars @@ Abstract1.env x
 
-    let assign x id e = x (* TODO *)
-    let compare x e1 e2 = x (* TODO *)
+    let assign x id e =
+        let expr = Texpr1.of_expr (Abstract1.env x) (texpr_of_expr e) in
+        let x' =
+            Abstract1.assign_texpr manager x
+                (Var.of_string id) expr None
+        in
+        if false then begin
+            Format.eprintf "Assign : ";
+            Abstract1.print Format.err_formatter x;
+            Format.eprintf " ; %s <- " id;
+            Texpr1.print Format.err_formatter expr;
+            Format.eprintf " ; ";
+            Abstract1.print Format.err_formatter x';
+            Format.eprintf "@.";
+        end;
+        x'
+    let compare op x e1 e2 =
+        let env = Abstract1.env x in
+        let expr = Texpr1.Binop
+            (Texpr1.Sub, texpr_of_expr e2, texpr_of_expr e1, Texpr1.Int, Texpr1.Zero) in
+        let cons = Tcons1.make (Texpr1.of_expr env expr) op in
+        let ar = Tcons1.array_make env 1 in
+        Tcons1.array_set ar 0 cons;
+        Abstract1.meet_tcons_array manager x ar
+    let compare_leq = compare Tcons1.SUPEQ
+    let compare_eq = compare Tcons1.EQ
 
     let join = Abstract1.join manager
     let meet = Abstract1.meet manager
@@ -31,7 +99,18 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
 
     let subset = Abstract1.is_leq manager
 
-    let var_str x idl = "" (* TODO *)
+    let var_str x idl = 
+        let prevars = vars x in
+        let rm_vars_l = List.filter (fun id -> not (List.mem id idl)) prevars in
+        (* print_list "prevars" prevars;
+        print_list "idl" idl;
+        print_list "rm_vars_l" rm_vars_l; *)
+        let rm_vars = Array.of_list (List.map Var.of_string rm_vars_l) in
+        let xx = Abstract1.forget_array manager x rm_vars false in
+        let b = Buffer.create 80 in
+        let s = Format.formatter_of_buffer b in
+        Abstract1.print s xx; Format.fprintf s "@?";
+        (Buffer.contents b)
 
 end
 
diff --git a/libs/util.ml b/libs/util.ml
index 68332b6..b1fcdc4 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -9,3 +9,12 @@ let rec fix f s =
     else fix f fs
 
 let (@@) f x = f x
+
+let print_list x l =
+    Format.printf "%s: " x;
+    let rec aux = function
+        | [] -> ()
+        | [a] -> Format.printf "%s" a
+        | p::q -> Format.printf "%s, " p; aux q
+    in
+    Format.printf "["; aux l; Format.printf "]@.";
diff --git a/tests/test.sh b/tests/test.sh
index 443868a..b736fb2 100755
--- a/tests/test.sh
+++ b/tests/test.sh
@@ -1,26 +1,39 @@
 #!/bin/bash
 
+function test_it {
+	if ../analyze $1 $2 > /tmp/analyze_out.txt;
+	then
+		cat /tmp/analyze_out.txt | uniq | tr -d " \\n" > /tmp/analyze_out_2.txt;
+		cat results/$3 | uniq | tr -d " \\n" > /tmp/expected_out_2.txt;
+		if diff -B /tmp/analyze_out_2.txt /tmp/expected_out_2.txt >/dev/null; then
+			echo "OK    $2"
+		else
+			cat /tmp/analyze_out.txt | grep Output > /tmp/analyze_out_3.txt;
+			cat results/$3 | grep Output > /tmp/expected_out_3.txt;
+			if diff -B /tmp/analyze_out_3.txt /tmp/expected_out_3.txt >/dev/null; then
+				echo "(TR)  $2"
+			else
+				echo "FAIL  $2"
+			fi;
+		fi;
+	else
+		echo "TODO  $2"
+	fi;
+}
+
 echo "== CONSTANT ABSTRACT DOMAIN"
 for a in sources/*.c; do
-    if ../analyze --const-interp $a > /tmp/analyze_out.txt;
-        then 
-           if diff -B /tmp/analyze_out.txt results/`basename -s .c $a`.constants.txt > /dev/null
-               then echo "OK    $a"
-               else echo "FAIL  $a"
-            fi
-        else echo "TODO  $a";
-    fi;
+	test_it --const-interp $a `basename $a .c`.constants.txt;
 done;
 
 echo "== INTERVALS ABSTRACT DOMAIN"
 for a in sources/*.c; do
-    if ../analyze --interv-interp $a > /tmp/analyze_out.txt;
-        then 
-           if diff -B /tmp/analyze_out.txt results/`basename -s .c $a`.intervals.txt > /dev/null
-               then echo "OK    $a"
-               else echo "FAIL  $a"
-            fi
-        else echo "TODO  $a";
-    fi;
+	test_it --interv-interp $a `basename $a .c`.intervals.txt;
+done;
+
+
+echo "== RELATIONNAL ABSTRACT DOMAIN"
+for a in sources/*.c; do
+	test_it --rel-interp $a `basename $a .c`.polyhedra.txt;
 done;