From 92dcbdc2021968689c8da5fc3c1f21790a0f72a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 21 May 2020 09:41:16 -0700 Subject: [PATCH] [control] Fix dangling node Summary: Consider the below program, ``` const int gvar = 0; enum { cvar = gvar + 1, }; bool dangling_cvar(int x) { for (int i = 0; i < cvar; i++){ } } ``` In the prune node, we don't have `cvar` but its inlined version, i.e. we have ` i < n$2 + 1` and the variable `n$2` is defined not in predecessor nodes to the prune node (as normally one would expect) but in a separate dangling node (see the {F236910156}) : ``` 6: BinaryOperatorStmt:Add n$2=*&#GB$gvar:int [line 38, column 10] ``` When computing the control var of this loop, previously we gave up and simply raised an error. With this diff, let's handle this case by looking inside this dangling node. Reviewed By: skcho Differential Revision: D21525569 fbshipit-source-id: bd4371493 --- infer/src/IR/Procdesc.ml | 2 ++ infer/src/IR/Procdesc.mli | 3 +++ infer/src/checkers/control.ml | 42 +++++++++++++++++++++--------- infer/src/checkers/control.mli | 3 ++- infer/src/checkers/loop_control.ml | 10 ++++--- 5 files changed, 43 insertions(+), 17 deletions(-) diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 08755ff07..e0a148e1b 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -191,6 +191,8 @@ module Node = struct (** Get the predecessors of the node *) let get_preds node = node.preds + let is_dangling node = List.is_empty (get_preds node) && List.is_empty (get_succs node) + (** Get siblings *) let get_siblings node = get_preds node diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 5d5a0d544..b03e887ab 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -162,6 +162,9 @@ module Node : sig val get_wto_index : t -> int + val is_dangling : t -> bool + (** Returns true if the node is dangling, i.e. no successors and predecessors *) + val hash : t -> int (** Hash function for nodes *) diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index 9cae77b76..205f7fd94 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -49,7 +49,8 @@ module LoopHeadToGuardNodes = Procdesc.NodeMap type loop_control_maps = { exit_map: LoopHeads.t ExitNodeToLoopHeads.t - ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t } + ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t + ; nodes: Procdesc.Node.t list Lazy.t } (* forward transfer function for control dependencies *) module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct @@ -75,7 +76,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct None - let get_vars_in_exp exp prune_node loop_head = + let get_vars_in_exp nodes exp prune_node loop_head = let program_control_vars = Exp.program_vars exp |> Sequence.fold ~init:ControlDepSet.empty ~f:(fun acc pvar -> @@ -88,15 +89,32 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct with | Some deps -> ControlDepSet.union deps acc - | None -> - L.internal_error - "Failed to get the definition of the control variable %a in exp %a \n" Ident.pp id - Exp.pp exp ; - acc ) + | None -> ( + (* the variables in the prone node do not appear in + predecessor nodes. This could happen if the variable + is defined in a dangling node due to a frontend + issue (when reading from a global variable). In that + case, we find that node among all the nodes of the + cfg and pick up the control variables. *) + let all_nodes = force nodes in + match + List.find_map all_nodes ~f:(fun node -> + if Procdesc.Node.is_dangling node then + let instrs = Procdesc.Node.get_instrs node in + Instrs.find_map instrs ~f:(find_vars_in_decl id loop_head prune_node) + else None ) + with + | Some deps -> + ControlDepSet.union deps acc + | None -> + L.internal_error + "Failed to get the definition of the control variable %a in exp %a \n" Ident.pp + id Exp.pp exp ; + acc ) ) (* extract vars from the prune instructions in the node *) - let get_control_vars loop_nodes loop_head = + let get_control_vars nodes loop_nodes loop_head = GuardNodes.fold (fun prune_node acc -> let instrs = Procdesc.Node.get_instrs prune_node in @@ -104,7 +122,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct ~f:(fun astate instr -> match instr with | Sil.Prune (exp, _, _, _) -> - Domain.union (get_vars_in_exp exp prune_node loop_head) astate + Domain.union (get_vars_in_exp nodes exp prune_node loop_head) astate | _ -> (* prune nodes include other instructions like REMOVE_TEMPS or loads *) astate ) @@ -117,12 +135,12 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct along with the loop header that CV is originating from - a loop exit node, remove control variables of its guard nodes This is correct because the CVs are only going to be temporaries. *) - let exec_instr astate {exit_map; loop_head_to_guard_nodes} (node : CFG.Node.t) _ = + let exec_instr astate {exit_map; nodes; loop_head_to_guard_nodes} (node : CFG.Node.t) _ = let node = CFG.Node.underlying_node node in let astate' = match LoopHeadToGuardNodes.find_opt node loop_head_to_guard_nodes with | Some loop_nodes -> - Domain.union astate (get_control_vars loop_nodes node) + Domain.union astate (get_control_vars nodes loop_nodes node) | _ -> astate in @@ -137,7 +155,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct L.(debug Analysis Medium) "@\n>>>Exit node %a, Loop head %a, guard nodes=%a @\n\n" Procdesc.Node.pp node Procdesc.Node.pp loop_head GuardNodes.pp guard_nodes ; - get_control_vars guard_nodes loop_head |> Domain.diff astate_acc + get_control_vars nodes guard_nodes loop_head |> Domain.diff astate_acc | _ -> (* Every loop head must have a guard node *) assert false ) diff --git a/infer/src/checkers/control.mli b/infer/src/checkers/control.mli index dc7df0fdb..4bb0df3b0 100644 --- a/infer/src/checkers/control.mli +++ b/infer/src/checkers/control.mli @@ -24,7 +24,8 @@ type invariant_map type loop_control_maps = { exit_map: LoopHeads.t ExitNodeToLoopHeads.t - ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t } + ; loop_head_to_guard_nodes: GuardNodes.t LoopHeadToGuardNodes.t + ; nodes: Procdesc.Node.t list Lazy.t } val compute_invariant_map : Procdesc.t -> loop_control_maps -> invariant_map diff --git a/infer/src/checkers/loop_control.ml b/infer/src/checkers/loop_control.ml index f0870d5a8..3f62650d2 100644 --- a/infer/src/checkers/loop_control.ml +++ b/infer/src/checkers/loop_control.ml @@ -120,7 +120,8 @@ let get_loop_head_to_source_nodes cfg = set (i.e. target of the back edges) loop_head_to_guard_map : loop_head -> guard_nodes and guard_nodes contains the nodes that may affect the looping behavior, i.e. occur in the guard of the loop conditional. *) -let get_control_maps loop_head_to_source_nodes_map = +let get_control_maps pdesc loop_head_to_source_nodes_map = + let nodes = lazy (Procdesc.get_nodes pdesc) in Procdesc.NodeMap.fold (fun loop_head source_list (Control.{exit_map; loop_head_to_guard_nodes}, loop_head_to_loop_nodes) -> @@ -166,15 +167,16 @@ let get_control_maps loop_head_to_source_nodes_map = loop_head_to_loop_nodes in let open Control in - ( {exit_map= exit_map'; loop_head_to_guard_nodes= loop_head_to_guard_nodes'} + ( {exit_map= exit_map'; loop_head_to_guard_nodes= loop_head_to_guard_nodes'; nodes} , loop_head_to_loop_nodes' ) ) loop_head_to_source_nodes_map ( Control. { exit_map= Control.ExitNodeToLoopHeads.empty - ; loop_head_to_guard_nodes= Control.LoopHeadToGuardNodes.empty } + ; loop_head_to_guard_nodes= Control.LoopHeadToGuardNodes.empty + ; nodes } , LoopInvariant.LoopHeadToLoopNodes.empty ) let get_loop_control_maps cfg = let loop_head_to_source_nodes_map = get_loop_head_to_source_nodes cfg in - get_control_maps loop_head_to_source_nodes_map + get_control_maps cfg loop_head_to_source_nodes_map