Many things work!

8 files changed, 331 insertions, 53 deletions

diff --git a/Makefile b/Makefile
index 51d9995..00cda6d 100644
--- a/Makefile
+++ b/Makefile
@@ -5,6 +5,7 @@ SRCDIRS=libs,frontend,abstract
 
 SRC= 	main.ml \
 		abstract/constant_domain.ml \
+		abstract/intervals_domain.ml \
 		abstract/environment_domain.ml \
 		abstract/interpret.ml \
 		abstract/nonrelational.ml \
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml
index d142228..44a13fc 100644
--- a/abstract/constant_domain.ml
+++ b/abstract/constant_domain.ml
@@ -9,7 +9,7 @@ module Constants : VALUE_DOMAIN = struct
 	let top = Top
 	let bottom = Bot
 	let const i = Int i
-	let rand i j = if i <> j then Top else Int i
+	let rand i j = if i > j then Bot else if i <> j then Top else Int i
 
 	let subset a b = match a, b with
 		| _, Top -> true
@@ -27,7 +27,7 @@ module Constants : VALUE_DOMAIN = struct
 		| Int a, Int b when a = b -> Int a
 		| _ -> Bot
 	
-	let widen = meet		(* pas besoin d'accélerer la convergence au-delà *)
+	let widen = join		(* pas besoin d'accélerer la convergence au-delà *)
 
 	let neg = function
 		| Int a -> Int (Z.neg a)
@@ -39,13 +39,26 @@ module Constants : VALUE_DOMAIN = struct
 		| _ -> Top
 	let add = b_aux Z.add
 	let sub = b_aux Z.sub
-	let mul = b_aux Z.mul
-	let div = b_aux Z.div
-	let rem = b_aux Z.rem
+	let mul a b = match a, b with
+		| Int x, Int y -> Int (Z.mul x y)
+		| Bot, _ | _, Bot -> Bot
+		| Int x, _ when x = Z.zero -> Int Z.zero
+		| _, Int x when x = Z.zero -> Int (Z.zero)
+		| _ -> Top
+	let div a b = match a, b with
+		| Int x, Int y -> Int (Z.div x y)
+		| Bot, _ | _, Bot -> Bot
+		| Int x, _ when x = Z.zero -> Int Z.zero
+		| _ -> Top
+	let rem a b = match a, b with
+		| Int x, Int y -> Int (Z.rem x y)
+		| Bot, _ | _, Bot -> Bot
+		| Int x, _ when x = Z.zero -> Int Z.zero
+		| _ -> Top
 
 	let leq a b =
 		match a, b with
-		| Int a, Int b when Z.leq a b ->
+		| Int a, Int b ->
 			if Z.leq a b
 				then Int a, Int b
 				else Bot, Bot
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index 254f755..05473aa 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -11,6 +11,7 @@ module type ENVIRONMENT_DOMAIN = sig
 	(* variable management *)
 	val addvar	: t -> id -> t
 	val rmvar	: t -> id -> t
+	val vars	: t -> id list
 
 	(* abstract operation *)
 	val assign	: t -> id -> expr ext -> t		(*    S[id <- expr]     *)
@@ -25,8 +26,7 @@ module type ENVIRONMENT_DOMAIN = sig
 	val subset	: t -> t -> bool
 
 	(* pretty-printing *)
-	val var_str			: t -> id list -> string
-	val all_vars_str	: t -> string
+	val var_str	: t -> id list -> string
 end
 
 
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index fe998a6..79d4d2c 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -7,30 +7,79 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
 	let neg (e, l) =
 		(AST_unary(AST_NOT, (e, l))), l
 
+	let binop op (e, l) e2 =
+		(AST_binary (op, (e,l), e2)), l
+	let m1 (e, l) =
+		binop AST_MINUS (e, l) (AST_int_const("1", l), l)
+	let p1 (e, l) =
+		binop AST_PLUS (e, l) (AST_int_const("1", l), l)
+
 	let rec condition cond env =
 		begin match fst cond with
 		| AST_binary (AST_LESS_EQUAL, e1, e2) ->
 			E.compare env e1 e2
-		| AST_binary (AST_GREATER_EQUAL, e1, e2) ->
-			E.compare env e2 e1
 		| AST_binary (AST_AND, e1, e2) ->
 			E.meet (condition e1 env) (condition e2 env)
 		| AST_binary (AST_OR, e1, e2) ->
 			E.join (condition e1 env) (condition e2 env)
-		(* transformations *)
+
+		(* transformations : remove not *)
+		| AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) ->
+			condition cond env
 		| AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
 			condition
 				(AST_binary(AST_OR, neg e1, neg e2), x) env
 		| AST_unary (AST_NOT, (AST_binary(AST_OR, e1, e2), x)) ->
 			condition
 				(AST_binary(AST_AND, neg e1, neg e2), x) env
-		| _ -> env (* TODO : encode some more transformations *)
+
+		| AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) ->
+			let op2 = match op with
+			| AST_LESS_EQUAL -> AST_GREATER
+			| AST_LESS -> AST_GREATER_EQUAL
+			| AST_GREATER_EQUAL -> AST_LESS
+			| AST_GREATER -> AST_LESS_EQUAL
+			| AST_EQUAL -> AST_NOT_EQUAL
+			| AST_NOT_EQUAL -> AST_EQUAL
+			| _ -> assert false
+			in
+			condition (binop op2 e1 e2) env
+		
+		(* transformations : encode everything with leq *)
+		| AST_binary(AST_LESS, e1, e2) ->
+			condition
+				(binop AST_AND (binop AST_LESS_EQUAL e1 (m1 e2))
+							   (binop AST_LESS_EQUAL (p1 e1) e2))
+				env
+		| AST_binary (AST_GREATER_EQUAL, e1, e2) ->
+			condition
+				(binop AST_LESS_EQUAL e2 e1)
+				env
+		| AST_binary (AST_GREATER, e1, e2) ->
+			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))
+				env
+
+		| _ -> env
 		end
 
 	let rec interp_stmt env stat =
 		begin match fst stat with
 		| AST_block b ->
-			List.fold_left interp_stmt env b
+			(* remember to remove vars that have gone out of scope at the end *)
+			let prevars = E.vars env in
+			let env2 = List.fold_left interp_stmt env b in
+			let postvars = E.vars env2 in
+			let rmvars = List.filter (fun x -> not (List.mem x prevars)) postvars in
+			List.fold_left E.rmvar env2 rmvars
 		| AST_assign ((id, _), exp) ->
 			E.assign env id exp
 		| AST_if (cond, tb, None) ->
@@ -38,27 +87,57 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
 				(interp_stmt (condition cond env) tb)
 				(condition (neg cond) env)
 		| AST_if (cond, tb, Some eb) ->
-			E.join
-				(interp_stmt (condition cond env) tb)
-				(interp_stmt (condition (neg cond) env) eb)
-		| AST_while (cond, (body, _)) ->
-			(* TODO *)
-			env
+			let e1 = (interp_stmt (condition cond env) tb) in
+			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
-		| AST_assert (cond, l) ->
+		| AST_assert cond ->
 			if not
-				(E.is_bot (condition (neg (cond, l)) env))
+				(E.is_bot (condition (neg cond) env))
 			then begin
-				print_string (Abstract_syntax_printer.string_of_extent l);
-				print_string ": ERROR: assertion failure\n"
+				Format.printf "%s: ERROR: assertion failure@."
+					(Abstract_syntax_printer.string_of_extent (snd stat));
 			end;
-			condition (cond, l) env
+			condition cond env
 		| AST_print items ->
-			print_string (Abstract_syntax_printer.string_of_extent (snd stat));
-			print_string ": ";
-			print_string (E.var_str env (List.map fst items));
-			print_string "\n";
+			Format.printf "%s: %s@."
+				(Abstract_syntax_printer.string_of_extent (snd stat))
+				(E.var_str env (List.map fst items));
 			env
+		| AST_local ((ty, _), vars) ->
+			List.fold_left
+				(fun env ((id, _), init) ->
+					let env2 = E.addvar env id in
+					match init with
+					| Some e -> E.assign env2 id e
+					| None -> env2)
+				env
+				vars
 		| _ -> assert false (* not implemented *)
 		end
 	
@@ -70,7 +149,6 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
 			E.init
 			(fst prog)
 		in
-			print_string "Output: ";
-			print_string (E.all_vars_str result);
-			print_string "\n"
+			Format.printf "Output: %s@."
+				(E.var_str result (E.vars result))
 end
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
new file mode 100644
index 0000000..98f4daf
--- /dev/null
+++ b/abstract/intervals_domain.ml
@@ -0,0 +1,122 @@
+open Value_domain
+
+module Intervals : VALUE_DOMAIN = struct
+  type bound = Int of Z.t | PInf | MInf
+
+  type t = Itv of bound * bound | Bot
+
+  (* utilities *)
+  let bound_leq a b =   (* a <= b ? *)
+    match a, b with
+    | MInf, _ | _, PInf -> true
+    | Int a, Int b -> Z.leq a b
+    | x, y -> x = y
+
+  let bound_add a b =
+    match a, b with
+    | MInf, Int a | Int a, MInf -> MInf
+    | PInf, Int a | Int a, PInf -> PInf
+    | MInf, MInf -> MInf
+    | PInf, PInf -> PInf
+    | Int a, Int b -> Int (Z.add a b)
+    | _ -> assert false
+  let bound_mul a b =
+    match a, b with
+    | PInf, Int(x) | Int(x), PInf ->
+      if x > Z.zero then PInf
+      else if x < Z.zero then MInf
+      else Int Z.zero
+    | MInf, Int(x) | Int(x), MInf ->
+      if x < Z.zero then PInf
+      else if x > Z.zero then MInf
+      else Int Z.zero
+    | Int(x), Int(y) -> Int(Z.mul x y)
+    | MInf, PInf | PInf, MInf -> MInf
+    | MInf, MInf | PInf, PInf -> PInf
+
+  let bound_min a b = match a, b with
+    | MInf, _ | _, MInf -> MInf
+    | Int a, Int b -> Int (min a b)
+    | Int a, PInf -> Int a
+    | PInf, Int a -> Int a
+    | PInf, PInf -> PInf
+  let bound_max a b = match a, b with
+    | PInf, _ | _, PInf -> PInf
+    | Int a, Int b -> Int (max a b)
+    | Int a, MInf | MInf, Int a -> Int a
+    | MInf, MInf -> MInf
+
+  let bound_neg = function
+    | PInf -> MInf
+    | MInf -> PInf
+    | Int i -> Int (Z.neg i)
+
+  (* implementation *)
+  let top = Itv(MInf, PInf)
+  let bottom = Bot
+  let const i = Itv(Int i, Int i)
+  let rand i j =
+    if Z.leq i j then Itv(Int i, Int j) else Bot
+
+  let subset a b = match a, b with
+    | Bot, _ -> true
+    | _, Bot -> false
+    | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
+
+  let join a b = match a, b with
+    | Bot, x | x, Bot -> x
+    | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)
+
+  let meet a b = match a, b with
+    | Bot, x | x, Bot -> Bot
+    | Itv(a, b), Itv(c, d) ->
+      let u, v = bound_max a c, bound_min b d in
+      if bound_leq u v
+        then Itv(u, v)
+        else Bot
+
+  let widen a b = match a, b with
+    | x, Bot | Bot, x -> x
+    | Itv(a, b), Itv(c, d) ->
+      Itv(
+        (if not (bound_leq a c) then MInf else a),
+        (if not (bound_leq d b) then PInf else b))
+
+  let neg = function
+    | Bot -> Bot
+    | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
+  let add a b = match a, b with
+    | Bot, _ | _, Bot -> Bot
+    | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
+  let sub a b = match a, b with
+    | Bot, _ | _, Bot -> Bot
+    | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
+  let mul a b = match a, b with
+    | Bot, _ | _, Bot -> Bot
+    | Itv(a, b), Itv(c, d) ->
+        Itv(
+          (bound_min (bound_min (bound_mul a c) (bound_mul a d))
+                     (bound_min (bound_mul b c) (bound_mul b d))),
+          (bound_max (bound_max (bound_mul a c) (bound_mul a d))
+                     (bound_max (bound_mul b c) (bound_mul b d))))
+      
+
+  let div a b = top (* TODO *)
+  let rem a b = top (* TODO *)
+
+  let leq a b = match a, b with
+    | Bot, _ | _, Bot -> Bot, Bot
+    | Itv(a, b), Itv(c, d) ->
+      if not (bound_leq a d)
+        then Bot, Bot
+        else Itv(a, bound_min b d), Itv(bound_max a c, d)
+
+  let bound_str = function
+    | MInf -> "-oo"
+    | PInf -> "+oo"
+    | Int i -> Z.to_string i
+  let to_string = function
+    | Bot -> "bot"
+    | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
+
+end
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index d4118da..7221df1 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -66,16 +66,25 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 				| 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
-					Env (VarMap.add a v1' (VarMap.add b v1' env))
-				| AST_identifier(a, _), AST_int_const(s, _) ->
-					let v1, v2 = get_var env a, V.const (Z.of_string s) in
-					let v1', _ = V.leq v1 v2 in
-					Env (VarMap.add a v1' env)
-				| AST_int_const(s, _), AST_identifier(b, _) ->
-					let v1, v2 = V.const (Z.of_string s), get_var env b in
-					let _, v2' = V.leq v1 v2 in
-					Env (VarMap.add b v2' env)
-				| _ -> Env env)
+					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
+					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
+					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
+					if V.bottom = v1' ||V.bottom = v2'
+						then Bot
+						else Env env)
 			x
 
 	let join a b = match a, b with
@@ -106,7 +115,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 	(* pretty-printing *)
 	let var_str env vars =
 		match env with
-		| Bot -> "bot"
+		| Bot -> "bottom"
 		| Env env ->
 			let v = List.fold_left
 				(fun s id ->
@@ -118,8 +127,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 			in
 				"[ " ^ v ^ " ]"
 	
-	let all_vars_str env =
-		match env with
-		| Bot -> "bot"
-		| Env map -> var_str env (List.map fst (VarMap.bindings map))
+	let vars env = match env with
+		| Bot -> []
+		| Env env -> List.map fst (VarMap.bindings env)
 end
diff --git a/main.ml b/main.ml
index e09ac0e..8f33d2d 100644
--- a/main.ml
+++ b/main.ml
@@ -13,19 +13,49 @@
 
 open Abstract_syntax_tree
 
-module Env_dom = Nonrelational.NonRelational(Constant_domain.Constants)
-module Interp = Interpret.Make(Env_dom)
+module Env_dom_const = Nonrelational.NonRelational(Constant_domain.Constants)
+module Interp_const = Interpret.Make(Env_dom_const)
+
+module Env_dom_interv = Nonrelational.NonRelational(Intervals_domain.Intervals)
+module Interp_interv = Interpret.Make(Env_dom_interv)
+
+(* option parsing *)
+let dump = ref false
+let const_interp = ref false
+let interv_interp = ref false
+let poly_interp = ref false
+let get_interp () =
+  if !interv_interp
+      then Interp_interv.interpret
+      else Interp_const.interpret
+
+let ifile = ref ""
+let set_var v s = v := s
+
+let usage = "usage: analyzer [options] file.c"
+
+let options = [
+  "--dump", Arg.Set dump, "Dump program source.";
+  "--const-interp",  Arg.Set const_interp, "Use constant lattice interpreter.";
+  "--interv-interp", Arg.Set interv_interp, "Use interval lattice interpreter.";
+  "--poly-interp", Arg.Set poly_interp, "Use polyhedra lattice interpreter.";
+]
 
 (* parse and print filename *)
 let doit filename =
   let prog = File_parser.parse_file filename in
-  Abstract_syntax_printer.print_prog Format.std_formatter prog;
-  Interp.interpret prog
+  if !dump then Abstract_syntax_printer.print_prog Format.std_formatter prog;
+  (get_interp ()) prog
 
 (* parses arguments to get filename *)
 let main () =
-  match Array.to_list Sys.argv with
-  | _::filename::_ -> doit filename
-  | _ -> invalid_arg "no source file specified"
+  Arg.parse options (set_var ifile) usage;
+
+  if !ifile = "" then begin
+    Format.eprintf "No input file...@.";
+    exit 1
+  end;
+
+  doit !ifile
 
 let _ = main ()
diff --git a/tests/test.sh b/tests/test.sh
new file mode 100755
index 0000000..443868a
--- /dev/null
+++ b/tests/test.sh
@@ -0,0 +1,26 @@
+#!/bin/bash
+
+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;
+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;
+done;
+