pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[AI] refactor html debug and add convergence messages

Browse Source 
Summary:
Open fewer sessions by wrapping AI operations together in the same HTML
node session. This allows us to also print more stuff, such as whether
the current loop computation has converged.

Reviewed By: skcho

Differential Revision: D14568274

fbshipit-source-id: d47110cf4
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent 3b5ef0b31b
commit 2f09a38e24
3 changed files with 66 additions and 45 deletions
Show Stats Download Patch File Download Diff File

103
infer/src/absint/AbstractInterpreter.ml
Unescape View File

@ -98,17 +98,14 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
(** extract the precondition of node [n] from [inv_map] *)
let extract_pre node_id inv_map = extract_state node_id inv_map |> Option.map ~f:State.pre
let debug_absint_operation op node =
let pp_name fmt =
TransferFunctions.pp_session_name node fmt ;
let debug_absint_operation op =
let pp_op fmt op =
match op with
| `Join _ ->
F.pp_print_string fmt " JOIN"
F.pp_print_string fmt "JOIN"
| `Widen (num_iters, _) ->
F.fprintf fmt " WIDEN(num_iters= %d)" num_iters
F.fprintf fmt "WIDEN(num_iters= %d)" num_iters
in
let underlying_node = Node.underlying_node node in
NodePrinter.start_session ~pp_name underlying_node ;
let left, right, result = match op with `Join lrr | `Widen (_, lrr) -> lrr in
let pp_right f =
if phys_equal right left then F.pp_print_string f "= LEFT" else Domain.pp f right
@ -118,8 +115,8 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
else if phys_equal result right then F.pp_print_string f "= RIGHT"
else Domain.pp f result
in
L.d_printfln_escaped "LEFT: %a@\nRIGHT: %t@\nRESULT: %t@." Domain.pp left pp_right pp_result ;
NodePrinter.finish_session underlying_node
L.d_printfln_escaped "%a@\n@\nLEFT: %a@\nRIGHT: %t@\nRESULT: %t@." pp_op op Domain.pp left
pp_right pp_result
(** reference to log errors only at the innermost recursive call *)
@ -154,10 +151,6 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
let exec_instrs ~pp_instr proc_data node node_id ~visit_count pre inv_map =
let instrs = CFG.instrs node in
if Config.write_html then
NodePrinter.start_session
~pp_name:(TransferFunctions.pp_session_name node)
(Node.underlying_node node) ;
let post =
if Config.write_html then L.d_printfln_escaped "PRE STATE:@\n@[%a@]@\n" Domain.pp pre ;
let compute_post pre instr =
@ -181,7 +174,6 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
compute_post pre Sil.skip_instr
else Container.fold_result ~fold:Instrs.fold ~init:pre instrs ~f:compute_post
in
if Config.write_html then NodePrinter.finish_session (Node.underlying_node node) ;
match post with
| Ok astate_post ->
InvariantMap.add node_id {State.pre; post= astate_post; visit_count} inv_map
@ -203,36 +195,51 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
let inv_map' = exec_instrs ~pp_instr proc_data node node_id ~visit_count pre inv_map in
(inv_map', DidNotReachFixPoint)
in
if InvariantMap.mem node_id inv_map then
let old_state = InvariantMap.find node_id inv_map in
let new_pre =
if is_loop_head && not is_narrowing then (
let num_iters = (old_state.State.visit_count :> int) in
let prev = old_state.State.pre in
let next = astate_pre in
let res = Domain.widen ~prev ~next ~num_iters in
if Config.write_html then
debug_absint_operation (`Widen (num_iters, (prev, next, res))) node ;
res )
else astate_pre
in
if
if is_narrowing then
(old_state.State.visit_count :> int) > Config.max_narrows
|| Domain.( <= ) ~lhs:old_state.State.pre ~rhs:new_pre
else Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre
then (inv_map, ReachedFixPoint)
else if is_narrowing && not (Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre) then (
L.(debug Analysis Verbose)
"Terminate narrowing because old and new states are not comparable at %a:%a@."
Typ.Procname.pp (Procdesc.get_proc_name pdesc) Node.pp_id node_id ;
(inv_map, ReachedFixPoint) )
let inv_map, converged =
if InvariantMap.mem node_id inv_map then
let old_state = InvariantMap.find node_id inv_map in
let new_pre =
if is_loop_head && not is_narrowing then (
let num_iters = (old_state.State.visit_count :> int) in
let prev = old_state.State.pre in
let next = astate_pre in
let res = Domain.widen ~prev ~next ~num_iters in
if Config.write_html then
debug_absint_operation (`Widen (num_iters, (prev, next, res))) ;
res )
else astate_pre
in
if
if is_narrowing then
(old_state.State.visit_count :> int) > Config.max_narrows
|| Domain.( <= ) ~lhs:old_state.State.pre ~rhs:new_pre
else Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre
then (inv_map, ReachedFixPoint)
else if is_narrowing && not (Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre) then (
L.(debug Analysis Verbose)
"Terminate narrowing because old and new states are not comparable at %a:%a@."
Typ.Procname.pp (Procdesc.get_proc_name pdesc) Node.pp_id node_id ;
(inv_map, ReachedFixPoint) )
else
let visit_count' = VisitCount.succ ~pdesc old_state.State.visit_count in
update_inv_map new_pre ~visit_count:visit_count'
else
let visit_count' = VisitCount.succ ~pdesc old_state.State.visit_count in
update_inv_map new_pre ~visit_count:visit_count'
else
(* first time visiting this node *)
update_inv_map astate_pre ~visit_count:VisitCount.first_time
(* first time visiting this node *)
update_inv_map astate_pre ~visit_count:VisitCount.first_time
in
( match converged with
| ReachedFixPoint ->
L.d_printfln "Fixpoint reached.@."
| DidNotReachFixPoint ->
() ) ;
(inv_map, converged)
(* shadowed for HTML debug *)
let exec_node ~pp_instr proc_data node ~is_loop_head ~is_narrowing astate_pre inv_map =
NodePrinter.with_session ~pp_name:(TransferFunctions.pp_session_name node)
(Node.underlying_node node) ~f:(fun () ->
exec_node ~pp_instr proc_data node ~is_loop_head ~is_narrowing astate_pre inv_map )
let compute_pre cfg node inv_map =
@ -247,11 +254,17 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
some_post
| Some joined_post ->
let res = Domain.join joined_post post in
if Config.write_html then
debug_absint_operation (`Join (joined_post, post, res)) node ;
if Config.write_html then debug_absint_operation (`Join (joined_post, post, res)) ;
Some res ) )
(* shadowed for HTML debug *)
let compute_pre cfg node inv_map =
NodePrinter.with_session (Node.underlying_node node)
~pp_name:(TransferFunctions.pp_session_name node) ~f:(fun () -> compute_pre cfg node inv_map
)
(** compute and return an invariant map for [pdesc] *)
let make_exec_pdesc ~exec_cfg_internal ({ProcData.pdesc} as proc_data) ~do_narrowing ~initial =
exec_cfg_internal ~pp_instr:pp_sil_instr (CFG.from_pdesc pdesc) proc_data ~do_narrowing

4
infer/src/absint/NodePrinter.ml
Unescape View File

@ -29,3 +29,7 @@ let start_session ~pp_name node =
let finish_session node = if Config.write_html then Printer.node_finish_session node
let with_session ~pp_name node ~f =
start_session ~pp_name node ;
Utils.try_finally_swallow_timeout ~f ~finally:(fun () -> finish_session node)

4
infer/src/absint/NodePrinter.mli
Unescape View File

@ -14,3 +14,7 @@ val start_session : pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> uni
val finish_session : Procdesc.Node.t -> unit
(** To be called after analyzing a node *)
val with_session : pp_name:(Format.formatter -> unit) -> Procdesc.Node.t -> f:(unit -> 'a) -> 'a
(** Wraps [f] between [start_session] and [finish_session]. Will swallow timeouts so do *not* use
from within biabduction *)

Write Preview
Loading…
Cancel
Save