114 lines
4.1 KiB
OCaml
114 lines
4.1 KiB
OCaml
(*
|
||
Cours "Sémantique et Application à la Vérification de programmes"
|
||
|
||
Antoine Miné 2015
|
||
Marc Chevalier 2018
|
||
Josselin Giet 2021
|
||
Ecole normale supérieure, Paris, France / CNRS / INRIA
|
||
*)
|
||
|
||
open Cfg
|
||
open Domain
|
||
|
||
|
||
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
|
||
|
||
(*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
|
||
*)
|
||
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 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 =
|
||
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
|
||
List.iter (fun arc -> let s = do_inst curr_abst arc in
|
||
if D.subset s (node_abst arc.arc_dst) then ()
|
||
else (Format.printf "@[<h 0>[%i -> %i] Got node %i state %a join %a " n.node_id arc.arc_dst.node_id arc.arc_dst.node_id
|
||
D.print (node_abst arc.arc_dst) 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;
|
||
if NodeSet.is_empty !func_dirty then () else
|
||
iterate (NodeSet.choose !func_dirty)
|
||
end 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 "@[<v 0>";
|
||
let init_st = do_fun {func_id = -1; func_name = "_init";
|
||
func_pos = Lexing.dummy_pos, Lexing.dummy_pos;
|
||
func_entry = cfg.cfg_init_entry;
|
||
func_exit = cfg.cfg_init_exit;
|
||
func_args = [];
|
||
func_ret = None;
|
||
func_calls = []} D.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
|
||
| [] -> failwith "function main() not found" in
|
||
let _ = do_main cfg.cfg_funcs in
|
||
Format.printf "@]";
|
||
!failed_asserts
|
||
end
|
||
end
|
||
|
||
open Interval
|
||
open Sign
|
||
open Constant
|
||
open Naked
|
||
open Value_domain
|
||
module ConstIterator = Iterator(NonRelational(AddTopBot(Constants)))
|
||
module SignIterator = Iterator(NonRelational(AddTopBot(Signs)))
|
||
module IntervalIterator = Iterator(NonRelational(AddTopBot(Interval)))
|
||
(*
|
||
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:@ @[<v 0>";
|
||
List.iter iter_node cfg.cfg_nodes;
|
||
Format.printf "@]"*)
|
||
*)
|