From 2f09a38e24f363f54abb3a4250a6be64eb49bee2 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 27 Mar 2019 10:22:14 -0700 Subject: [PATCH] [AI] refactor html debug and add convergence messages 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 --- infer/src/absint/AbstractInterpreter.ml | 103 +++++++++++++----------- infer/src/absint/NodePrinter.ml | 4 + infer/src/absint/NodePrinter.mli | 4 + 3 files changed, 66 insertions(+), 45 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 0235f84a1..f0fe411ae 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -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 diff --git a/infer/src/absint/NodePrinter.ml b/infer/src/absint/NodePrinter.ml index 3deee6371..01adc5cd5 100644 --- a/infer/src/absint/NodePrinter.ml +++ b/infer/src/absint/NodePrinter.ml @@ -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) diff --git a/infer/src/absint/NodePrinter.mli b/infer/src/absint/NodePrinter.mli index db90c9d9d..cf03d4d4d 100644 --- a/infer/src/absint/NodePrinter.mli +++ b/infer/src/absint/NodePrinter.mli @@ -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 *)