diff --git a/analyzer.ml b/analyzer.ml index 18b6ad9..b6b0cd9 100644 --- a/analyzer.ml +++ b/analyzer.ml @@ -18,11 +18,11 @@ let doit filename = begin Format.printf "%a" Cfg_printer.print_cfg cfg; Cfg_printer.output_dot !Options.cfg_out cfg; let f = match !Options.domain with - | "signs" -> SignIterator.iterate cfg - | "interval" -> IntervalIterator.iterate cfg - | "constants" -> ConstIterator.iterate cfg - | "congruence" -> CongIterator.iterate cfg - | "product" -> RPIterator.iterate cfg + | "signs" -> if !Options.disjunction then SignDisjIterator.iterate cfg else SignIterator.iterate cfg + | "interval" -> if !Options.disjunction then IntervalDisjIterator.iterate cfg else IntervalIterator.iterate cfg + | "constants" -> if !Options.disjunction then ConstDisjIterator.iterate cfg else ConstIterator.iterate cfg + | "congruence" ->if !Options.disjunction then CongDisjIterator.iterate cfg else CongIterator.iterate cfg + | "product" -> if !Options.disjunction then RPDisjIterator.iterate cfg else RPIterator.iterate cfg | _ -> failwith "No valid iterator specified" in Format.printf "@[Failed asserts :@ %a@]" pp_asserts f end diff --git a/domains/congruence.ml b/domains/congruence.ml index 638e585..87bbadc 100644 --- a/domains/congruence.ml +++ b/domains/congruence.ml @@ -136,7 +136,7 @@ module Congruence (*: NAKED_VALUE_DOMAIN*) = struct else (z1', z2') | AST_DIVIDE -> (meet z1 (binary r z2 AST_MULTIPLY), meet z2 (binary z1 r AST_DIVIDE)) - | AST_MODULO -> (z1, z2) + | AST_MODULO -> (z1, z2) (* If z2 is a constant this is somewhat doable with the Chinese Remainder Theorem *) let widen = join let narrow = meet diff --git a/domains/naked.ml b/domains/naked.ml index 93469a9..43a8b0f 100644 --- a/domains/naked.ml +++ b/domains/naked.ml @@ -104,7 +104,7 @@ struct | Top -> x, y | Bot -> (match op with | AST_DIVIDE | AST_MODULO -> x, (try (V (N.const Z.zero) )with NeedTop->Top) - | _ -> x, y (* This can only happen if one of x or y was already Bot *) + | _ -> Bot, Bot (* Propagate absurdity *) ) | V r' -> (match x, y with | Bot, _| _, Bot -> x,y diff --git a/examples/disjunction/disjunction.c b/examples/disjunction/disjunction.c new file mode 100644 index 0000000..b1a64a0 --- /dev/null +++ b/examples/disjunction/disjunction.c @@ -0,0 +1,10 @@ +void main() { + int x = rand(-10, 10); + if(brand) { + x *= 2; + } else { + x *= 3; + } + + assert(x%3 == 0 || x%2 == 0); +} diff --git a/frontend/cfg.ml b/frontend/cfg.ml index 7b8861c..bc13b57 100644 --- a/frontend/cfg.ml +++ b/frontend/cfg.ml @@ -181,6 +181,7 @@ and node = mutable node_in: arc list; (* arcs with this node as destination *) mutable widen_target : bool; (* is node a candidate for widening : either head of structured loop or destination of goto in goto-made loop that doesn't have any widen-target *) + mutable branch_node : bool (* is node source of a branch *) } and arc = @@ -188,6 +189,7 @@ and arc = arc_src: node; (* source node *) arc_dst: node; (* destination node *) arc_inst: inst; (* instruction *) + arc_parity: bool; (* true for positive branch, false for negative branch *) } diff --git a/frontend/options.ml b/frontend/options.ml index 7b20b11..7ab3dda 100644 --- a/frontend/options.ml +++ b/frontend/options.ml @@ -18,7 +18,7 @@ open Arg (* Flags *) let verbose = ref false - +let disjunction = ref true (* string arguments *) let file = ref "" let cfg_out = ref "cfg.dot" @@ -30,7 +30,9 @@ 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/signs)"; + " Select the abstract domain (constants/interval/signs/congruence/product)"; + "-fno-disjunction", Clear disjunction, + " Disable disjunctive path analysis" ] |> align let usage = "usage: ./analyzer.exe [options] filename.c" diff --git a/frontend/tree_to_cfg.ml b/frontend/tree_to_cfg.ml index 84ba344..19ec75c 100644 --- a/frontend/tree_to_cfg.ml +++ b/frontend/tree_to_cfg.ml @@ -36,13 +36,14 @@ let node_counter = ref 0 let nodes = ref [] (* create a new node, with a fresh identifier and accumulate into nodes *) -let create_node ?(widen_target) (pos:position) = +let create_node ?(widen_target) ?(branch) (pos:position) = incr node_counter; let node = { node_id = !node_counter; node_pos = pos; node_in = []; node_out = []; + branch_node = (match branch with | None -> false | Some b -> b); widen_target = match widen_target with | None -> false | Some b -> b; } in @@ -54,13 +55,14 @@ let arcs = ref [] let arc_counter = ref 0 (* create a new arc and accumulate it into arcs *) -let add_arc (src:node) (dst:node) (inst:inst) = +let add_arc ?(parity) (src:node) (dst:node) (inst:inst) = incr arc_counter; let arc = { arc_id = !arc_counter; arc_src = src; arc_dst = dst; arc_inst = inst; + arc_parity = match parity with | None -> false | Some b -> b; } in src.node_out <- arc::src.node_out; @@ -419,11 +421,12 @@ let rec stat (env:env) (entry:node) (exit:node) (s:stat) : env = let env1, before, e = bool_expr env expr in (* entry --[before]--> entry1 *) let entry1 = append_inst entry before in + entry1.branch_node <- true; let node_t, node_f = create_node (fst x1), create_node (fst x2) in (* entry1 --[expr]--> node_t_t *) - add_arc entry1 node_t (CFG_guard e); + add_arc ~parity:true entry1 node_t (CFG_guard e); (* entry1 --[!expr] --> node_f *) - add_arc entry1 node_f (CFG_guard (CFG_bool_unary (AST_NOT, e))); + add_arc ~parity:false entry1 node_f (CFG_guard (CFG_bool_unary (AST_NOT, e))); (* node_t --[s1]--> exit *) let env2 = stat env1 node_t exit s1 in (* node_f --[s2] --> exit *) @@ -438,11 +441,12 @@ let rec stat (env:env) (entry:node) (exit:node) (s:stat) : env = let env1, before, e = bool_expr env expr in (* entry --[before]--> entry1 *) let entry1 = append_inst entry before in + entry1.branch_node <- true; let node_t = create_node (fst x1) in (* entry1 --[expr]--> node_t *) - add_arc entry1 node_t (CFG_guard e); + add_arc ~parity:true entry1 node_t (CFG_guard e); (* entry1 --[!expr]--> exit *) - add_arc entry1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e))); + add_arc ~parity:false entry1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e))); (* node_t --[s1]--> exit *) stat env1 node_t exit s1 @@ -456,11 +460,12 @@ let rec stat (env:env) (entry:node) (exit:node) (s:stat) : env = let env1, before, e = bool_expr env expr in (* entry --[before]--> entry1 *) let entry1 = append_inst entry before in + entry1.branch_node <- true; let node_t = create_node ~widen_target:true (fst x1) in (* entry1 --[expr]--> node_t *) - add_arc entry1 node_t (CFG_guard e); + add_arc ~parity:true entry1 node_t (CFG_guard e); (* entry1 --[!expr]--> node_f *) - add_arc entry1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e))); + add_arc ~parity:false entry1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e))); (* node_t --[s1]--> entry *) let env2 = stat { env1 with env_break = Some exit; } node_t entry s1 in { env2 with env_break = env1.env_break; } @@ -487,9 +492,10 @@ let rec stat (env:env) (entry:node) (exit:node) (s:stat) : env = | Some (expr,_) -> bool_expr env1 expr in let head1 = append_inst head before in + head1.branch_node <- true; let node_t = create_node ~widen_target:true (fst x1) in - add_arc head1 node_t (CFG_guard e); - add_arc head1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e))); + add_arc ~parity:true head1 node_t (CFG_guard e); + add_arc ~parity:false head1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e))); (* increment *) (* tail --[incr]--> head *) let env3, tail = diff --git a/iterator/iterable.ml b/iterator/iterable.ml new file mode 100644 index 0000000..9a4a389 --- /dev/null +++ b/iterator/iterable.ml @@ -0,0 +1,107 @@ + +open Cfg +open Domain + +module type ITERABLE = sig + type t (*type of a node abst*) + val bottom : t + val init : t + + val do_compute : arc -> t (*source*) -> (arc -> unit) -> (func -> t -> t) -> t (*to accumulate*) + val accumulate : arc -> t (*source*) -> t (*old dst*) -> t*bool (*dst*) +end + +module SimpleIterable (D : DOMAIN) : ITERABLE = struct + type t = D.t + + let bottom = D.bottom + let init = D.init + + let do_compute a src cb_fail cb_fun = match a.arc_inst with + | CFG_skip _ -> src + | CFG_assign (v, iexpr) -> D.assign src v iexpr + | CFG_guard bexpr -> D.guard src bexpr + | CFG_assert (bexpr, _) -> (let s = D.guard src (CFG_bool_unary (AST_NOT, bexpr)) in + if D.is_bottom s then ( + Format.printf "State %a is disjoint with %a@ " D.print src Cfg_printer.print_bool_expr (rm_negations (CFG_bool_unary (AST_NOT, bexpr))); + src) else ( + Format.printf "Failure of assert on %a@ " D.print s; + cb_fail a; + (D.guard src bexpr))) + | CFG_call f -> cb_fun f src + + + let accumulate a dst_old dst_toacc = + if D.subset dst_toacc dst_old then (dst_old, false) else ( + let accfun = if a.arc_dst.widen_target then D.widen else D.join in + let str = if a.arc_dst.widen_target then "widen" else "join" in + Format.printf "@[[%i -> %i] Got node %i state %a %s %a " a.arc_src.node_id a.arc_dst.node_id a.arc_dst.node_id + D.print dst_old + str + D.print dst_toacc; + let r = accfun dst_old dst_toacc in + Format.printf "= %a@]@ " D.print r; r,true) +end + + +module SCR = struct (*Sparse Conditional Record*) + type t = (int*bool) list (*list must be sorted!!*) + let compare v1 v2 = match v1, v2 with + | [], [] -> 0 + | _, [] -> 1 + | [], _ -> -1 + | (i,_)::_, (i',_)::_ when i < i' -> 1 (* v1 > v2 *) + | (i,_)::_, (i',_)::_ when i > i' -> -1 + | (_,w)::q, (_,w')::q' -> if (compare w w') <> 0 then compare w w' else + compare q q' +end + +module SCRMap = Map.Make(SCR) + +module DisjunctiveIterable (D : DOMAIN) : ITERABLE = struct + (* invariant : dans tout parcours de l'arbre, le int est croissant *) + type t = D.t SCRMap.t + + let bottom = SCRMap.empty + let init = SCRMap.singleton [] D.init + + let do_compute a src cb_fail cb_fun = match a.arc_inst with + | CFG_skip _ -> src + | CFG_assign (v, iexpr) -> SCRMap.map (fun d -> D.assign d v iexpr) src + | CFG_guard bexpr -> SCRMap.map (fun d -> D.guard d bexpr) src + | CFG_assert (bexpr, _) -> let b = SCRMap.fold (fun _ d acc -> match D.is_bottom (D.guard d (CFG_bool_unary(AST_NOT, bexpr))) with + | true -> acc + | false -> Some d) src None in + (match b with + | None -> src + | Some d -> Format.printf "Failure of assert : cannot rule out state %a@ " D.print d; + cb_fail a; SCRMap.map (fun d -> D.guard d bexpr) src) + | CFG_call f -> cb_fun f src + + let rec tag_key a key = match key with + | [] -> [a.arc_src.node_id, a.arc_parity] + | (ci, x)::q when ci < a.arc_src.node_id -> (ci, x)::(tag_key a q) + | (ci, _)::_ when ci > a.arc_src.node_id -> (a.arc_src.node_id, a.arc_parity)::key + | (ci, _)::q -> (ci, a.arc_parity)::q + + let accumulate a dst_old dst_toacc = + Format.printf "[%i -> %i] accumulating...@ " a.arc_src.node_id a.arc_dst.node_id; + let tounion = if a.arc_src.branch_node then + let ml = SCRMap.to_list dst_toacc in + let modlist = (List.map (fun (key,d) -> (tag_key a key, d)) ml) in + SCRMap.of_list modlist + else dst_toacc in + let acctor = if a.arc_dst.widen_target then D.widen else D.join in + let flag = ref false in + let ns = SCRMap.merge (fun _ d d' -> match d,d' with + | None, None -> None + | Some d, None -> Some d (*just preserving old state*) + | None, Some d -> (flag := true; Format.printf "Unreached branch took !@ "; Some d) + | Some d, Some d' -> (if D.subset d' d then (Some d) else + (flag := true; Some (acctor d d')))) dst_old tounion in + ns, !flag + (* + If we are on the arc of a conditional, change the keys of dst_old accordingly. + Then, union the maps (with the appropriate accfun) ! + *) +end diff --git a/iterator/iterator.ml b/iterator/iterator.ml index 381fe69..e66f417 100644 --- a/iterator/iterator.ml +++ b/iterator/iterator.ml @@ -8,15 +8,15 @@ *) open Cfg -open Domain - +open Iterable let pp_asserts out a = ArcSet.iter (fun arc -> match arc.arc_inst with | CFG_assert (b, ext) -> Format.fprintf out "%a@ " Errors.pp_err (AssertFalse, ext, b) | _ -> failwith "Failed on non-assert") a -module Iterator (D : DOMAIN) = struct + +module Iterator (I : ITERABLE) = struct (*let pp_nodes out (s,nodelist) = List.iter (fun node -> (Format.fprintf out "<%i>: %a@ " node.node_id D.print (node_abst node s))) nodelist @@ -24,50 +24,30 @@ module Iterator (D : DOMAIN) = struct let iterate cfg = let failed_asserts = ref ArcSet.empty in - let rec do_fun (f : func) (ctx : D.t) = (*returns an abstraction of the result of exec*) + let rec do_fun (f : func) (ctx : I.t) = (*returns an abstraction of the result of exec*) let func_state = ref NodeMap.empty in (*avoid losing precision between function calls*) let func_dirty = ref NodeSet.empty in begin func_state := NodeMap.add f.func_entry ctx (!func_state); - let node_abst n = try( NodeMap.find n !func_state )with Not_found -> D.bottom in - let update_node n s = - let acctor = if (n.widen_target) then D.widen else D.join in - func_state := NodeMap.add n (acctor (node_abst n) s) !func_state in - + let node_abst n = try( NodeMap.find n !func_state )with Not_found -> I.bottom 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 - List.iter (fun arc -> let s = do_inst curr_abst arc in - if D.subset s (node_abst arc.arc_dst) then () - else (let str = if arc.arc_dst.widen_target then "widen" else "join" in - Format.printf "@[[%i -> %i] Got node %i state %a %s %a " n.node_id arc.arc_dst.node_id arc.arc_dst.node_id - D.print (node_abst arc.arc_dst) - str - D.print s; - update_node arc.arc_dst s; - Format.printf "= %a@]@ " D.print (node_abst arc.arc_dst); - func_dirty := NodeSet.add arc.arc_dst !func_dirty)) l; + List.iter (fun arc -> + let nv = I.do_compute arc curr_abst + (fun a -> failed_asserts := ArcSet.add a !failed_asserts) + do_fun in + let s,b = I.accumulate arc (node_abst arc.arc_dst) nv in + func_state := NodeMap.add arc.arc_dst s !func_state; + if b then func_dirty := NodeSet.add arc.arc_dst !func_dirty;) n.node_out; if NodeSet.is_empty !func_dirty then () else iterate (NodeSet.choose !func_dirty) - end end in + end in iterate f.func_entry; node_abst f.func_exit; end - and do_inst state arc = (* Returns a D.t describing the state we end up in after following the arc. May be bottom*) - match arc.arc_inst with - | CFG_skip _-> state - | CFG_assign (v, iexpr) -> (D.assign state v iexpr) - | CFG_guard bexpr -> D.guard state bexpr - | CFG_assert (bexpr, _) -> (let s = D.guard state (CFG_bool_unary (AST_NOT, bexpr)) in - if D.is_bottom s then ( - Format.printf "State %a is disjoint with %a@ " D.print state Cfg_printer.print_bool_expr (rm_negations (CFG_bool_unary (AST_NOT, bexpr))); - state) else ( - Format.printf "Failure of guard on %a@ " D.print s; - failed_asserts := ArcSet.add arc !failed_asserts; - (D.guard state bexpr))) - | CFG_call f -> do_fun f state in begin Format.printf "@["; @@ -77,7 +57,7 @@ module Iterator (D : DOMAIN) = struct func_exit = cfg.cfg_init_exit; func_args = []; func_ret = None; - func_calls = []} D.init in + func_calls = []} I.init in let rec do_main l = match l with | x::_ when x.func_name = "main" -> do_fun x init_st | _::q -> do_main q @@ -123,28 +103,15 @@ module IntervalxCongr : CROSS_REDUCTION = struct end -module ConstIterator = Iterator(NonRelational(AddTopBot(Constants))) -module SignIterator = Iterator(NonRelational(AddTopBot(Signs))) -module IntervalIterator = Iterator(NonRelational(AddTopBot(Interval))) -module CongIterator = Iterator(NonRelational(AddTopBot(Congruence))) -module RPIterator = Iterator(NonRelational(ReducedProduct(IntervalxCongr))) -(* -let iterate cfg = - let () = Random.self_init () in - let iter_arc arc: unit = - match arc.arc_inst with - | CFG_assert (b, ext) -> - Format.printf "%a@ " Errors.pp_err (AssertFalse, ext, b) - | _ -> () in -(* let iter_arc arc: unit = - match arc.arc_inst with - | CFG_assert (b, ext) -> - Format.printf "%a@ " Errors.pp_err (AssertFalse, ext, b) - | _ -> () in - let iter_node node: unit = - Format.printf "<%i>: ⊤@ " node.node_id in - List.iter iter_arc cfg.cfg_arcs; - Format.printf "Node Values:@ @["; - List.iter iter_node cfg.cfg_nodes; - Format.printf "@]"*) -*) +module ConstIterator = Iterator(SimpleIterable(NonRelational(AddTopBot(Constants)))) +module SignIterator = Iterator(SimpleIterable(NonRelational(AddTopBot(Signs)))) +module IntervalIterator = Iterator(SimpleIterable(NonRelational(AddTopBot(Interval)))) +module CongIterator = Iterator(SimpleIterable(NonRelational(AddTopBot(Congruence)))) +module RPIterator = Iterator(SimpleIterable(NonRelational(ReducedProduct(IntervalxCongr)))) + +module ConstDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Constants)))) +module SignDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Signs)))) +module IntervalDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Interval)))) +module CongDisjIterator = Iterator(DisjunctiveIterable(NonRelational(AddTopBot(Congruence)))) +module RPDisjIterator = Iterator(DisjunctiveIterable(NonRelational(ReducedProduct(IntervalxCongr)))) + diff --git a/scripts/test.sh b/scripts/test.sh index 6bafb4f..61909de 100755 --- a/scripts/test.sh +++ b/scripts/test.sh @@ -270,6 +270,8 @@ 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" "" +treat_examples "congruence" "Congruence operations" "--domain congruence" "" +treat_examples "disjunction" "Disjunctive analysis" "--domain congruence" "" echo "" >> $index_html echo "" >> $index_html echo "" >> $index_html