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