Let user choose domain

analyzer.ml

@@ -7,15 +7,8 @@
   Ecole normale supérieure, Paris, France / CNRS / INRIA
 *)
 
-(*
-  Simple driver: parses the file given as argument and prints it back.
-
-  You should modify this file to call your functions instead!
-*)
-
 
 open Iterator 
-open Cfg
 
 (* parse filename *)
 let doit filename = begin
@@ -24,9 +17,11 @@ let doit filename = begin
   if !Options.verbose then
     Format.printf "%a" Cfg_printer.print_cfg cfg;
   Cfg_printer.output_dot !Options.cfg_out cfg;
-  let fa = ConstIterator.iterate cfg in
+  let f = match !Options.domain with
-  let fb = SignIterator.iterate cfg in 
+	| "signs" -> SignIterator.iterate cfg
-  Format.printf "@[<v 0>Failed asserts :@ %a@]" pp_asserts (ArcSet.inter fa fb) end
+	| "constants" -> ConstIterator.iterate cfg
+	| _ -> ConstIterator.iterate cfg in
+  Format.printf "@[<v 0>Failed asserts :@ %a@]" pp_asserts f  end
 
 
 (* parses arguments to get filename *)

domains/sign.ml

@@ -38,15 +38,24 @@ module Signs : NAKED_VALUE_DOMAIN = struct
 		| AST_NOT_EQUAL -> raise NeedTop
 		| AST_LESS | AST_LESS_EQUAL -> if a == P || a == Z then P else raise NeedTop
 		| AST_GREATER | AST_GREATER_EQUAL -> if a == N || a == Z then N else raise NeedTop
-	let compare a b op = match op with
+	let rec compare a b op = match op with
 		| AST_EQUAL 	-> if a <> b then Z, Z else a, b
 		| AST_NOT_EQUAL -> if a == b && a == Z then raise Absurd else a, b
-		| AST_LESS | AST_LESS_EQUAL -> if b == N || b == Z then
+		| AST_LESS_EQUAL -> (match b with
-						(match a with | P -> Z | Z -> Z | N -> N), b
+					| Z -> (match a with | P -> Z | Z -> Z | N -> N), b
-						else a, b (*if b is P then we learn nothing*)
+					| N -> (match a with
-		| AST_GREATER | AST_GREATER_EQUAL -> if a == N || a == Z then
+						| P -> Z,Z
-							a, (match b with | P -> Z | Z -> Z | N -> N)
+						| N -> N,N
-						     else a,b
+						| Z -> Z,Z)
+					| P -> a,b)
+		| AST_LESS -> (match b with
+				| Z -> (match a with | P -> raise Absurd | Z -> raise Absurd | N -> N), b
+				| N -> (match a with
+					| P -> raise Absurd
+					| N -> N,N
+					| Z -> raise Absurd)
+				| P -> a,b)
+		| AST_GREATER_EQUAL | AST_GREATER -> let b',a' = compare b a (reverse op) in a', b'
 
 	let meet x y = match x,y with
 			|P, N | N, P -> raise Absurd

examples/sign/functions.c

@@ -0,0 +1,18 @@
+
+int abs(int x) {
+	if(x < 0) {
+		return -x;
+	} else {
+		return x;
+	}
+}
+
+void main() {
+	int x = rand(0,10);
+	int y = abs(x);
+	assert(y >= 0);
+	x = rand(-10, 10);
+	y = abs(x);
+	assert(y >= 0);
+}
+

frontend/options.ml

@@ -30,7 +30,7 @@ let args = [
   "--dot-out", Set_string cfg_out,
     " Print the cfg in this file (default is cfg.dot)";
   "--domain", Set_string domain,
-    " Select the abstract domain (constants/interval)";
+    " Select the abstract domain (constants/interval/signs)";
 ] |> align
 
 let usage = "usage: ./analyzer.exe [options] filename.c"

iterator/iterator.ml

@@ -34,6 +34,7 @@ module Iterator (D : DOMAIN) = struct
 				func_state := NodeMap.add n (D.join s (node_abst n)) !func_state in
 
 			let rec iterate n = begin
+				(*Format.printf "@[<h 0> Handling node %i@]@ " n.node_id;*)
 				func_dirty := NodeSet.remove n !func_dirty;
 				let curr_abst = node_abst n in
 				let l = List.filter (fun x -> Node.equal x.arc_src n) cfg.cfg_arcs in begin
@@ -70,8 +71,11 @@ module Iterator (D : DOMAIN) = struct
 					func_args = [];
 					func_ret = None;
 					func_calls = []} D.init in
-			let x = List.hd cfg.cfg_funcs in (* we are ASSUMING main() is function 0*)
+			let rec do_main l = match l with
-			let _ = do_fun x init_st in
+				| x::_ when x.func_name = "main" -> do_fun x init_st
+				| _::q -> do_main q
+				| [] -> failwith "function main() not found" in
+			let _ = do_main cfg.cfg_funcs in
 			Format.printf "@]";
 			!failed_asserts
 		end

scripts/test.sh

@@ -265,6 +265,7 @@ treat_examples "constant" "Constants operations (I)" "--domain interval" ""
 treat_examples "interval" "Interval operations" "--domain interval" ""
 treat_examples "constant_loop" "Constants loops (I)" "--domain interval" ""
 treat_examples "interval_loop" "Interval loops" "--domain interval" ""
+treat_examples "sign" "Sign and misc." "--domain signs" ""
 echo "</table>"                                   >> $index_html
 echo "</body>"                                    >> $index_html
 echo "</html>"                                    >> $index_html