Compare commits

...

2 commits

Author SHA1 Message Date
Granahir2
1fbdff1ec6 Let user choose domain 2024-06-01 19:35:36 +02:00
Granahir2
041d492986 Fixed up signs, less naive func support 2024-06-01 19:29:10 +02:00
6 changed files with 47 additions and 20 deletions

View file

@ -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 *)

View file

@ -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
View 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);
}

View file

@ -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"

View file

@ -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

View file

@ -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