diff --git a/domains/sign.ml b/domains/sign.ml index fbf271c..6330d8b 100644 --- a/domains/sign.ml +++ b/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 - (match a with | P -> Z | Z -> Z | N -> N), b - else a, b (*if b is P then we learn nothing*) - | AST_GREATER | AST_GREATER_EQUAL -> if a == N || a == Z then - a, (match b with | P -> Z | Z -> Z | N -> N) - else a,b + | AST_LESS_EQUAL -> (match b with + | Z -> (match a with | P -> Z | Z -> Z | N -> N), b + | N -> (match a with + | P -> Z,Z + | N -> N,N + | 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 diff --git a/examples/sign/functions.c b/examples/sign/functions.c new file mode 100644 index 0000000..a672441 --- /dev/null +++ b/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); +} + diff --git a/frontend/options.ml b/frontend/options.ml index 9c21226..7b20b11 100644 --- a/frontend/options.ml +++ b/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" diff --git a/iterator/iterator.ml b/iterator/iterator.ml index 0dae579..4210e54 100644 --- a/iterator/iterator.ml +++ b/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 "@[ 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 _ = do_fun x init_st in + let rec do_main l = match l with + | 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 diff --git a/scripts/test.sh b/scripts/test.sh index 89b8a50..1f8ca8d 100755 --- a/scripts/test.sh +++ b/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 "" >> $index_html echo "" >> $index_html echo "" >> $index_html