Compare commits
2 commits
f477edb789
...
1fbdff1ec6
Author | SHA1 | Date | |
---|---|---|---|
|
1fbdff1ec6 | ||
|
041d492986 |
6 changed files with 47 additions and 20 deletions
15
analyzer.ml
15
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 fb = SignIterator.iterate cfg in
|
||||
Format.printf "@[<v 0>Failed asserts :@ %a@]" pp_asserts (ArcSet.inter fa fb) end
|
||||
let f = match !Options.domain with
|
||||
| "signs" -> SignIterator.iterate cfg
|
||||
| "constants" -> ConstIterator.iterate cfg
|
||||
| _ -> ConstIterator.iterate cfg in
|
||||
Format.printf "@[<v 0>Failed asserts :@ %a@]" pp_asserts f end
|
||||
|
||||
|
||||
(* parses arguments to get filename *)
|
||||
|
|
|
@ -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
|
||||
|
|
18
examples/sign/functions.c
Normal file
18
examples/sign/functions.c
Normal file
|
@ -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);
|
||||
}
|
||||
|
|
@ -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"
|
||||
|
|
|
@ -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 _ = 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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue