From 00d79ec8397c55be0ebb2516267bed88a16d9a5e Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 26 Apr 2018 09:23:51 -0700 Subject: [PATCH] Simplify abstract interpreter Summary: Now that we have a proper InstrNode, we can kill `instr_ids`! Of course: Depends on D7608526 Reviewed By: sblackshear Differential Revision: D7618124 fbshipit-source-id: b3609cd --- infer/src/absint/AbstractInterpreter.ml | 30 ++++++++----------------- infer/src/absint/ProcCfg.ml | 21 ----------------- infer/src/absint/ProcCfg.mli | 6 ----- infer/src/unit/schedulerTests.ml | 2 -- 4 files changed, 9 insertions(+), 50 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 6f2ad91a2..da61d4be8 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -63,33 +63,23 @@ struct let exec_node node astate_pre work_queue inv_map ({ProcData.pdesc} as proc_data) ~debug = let node_id = CFG.id node in - let update_inv_map pre visit_count = - let compute_post (pre, inv_map) (instr, id_opt) = - let post = TransferFunctions.exec_instr pre proc_data node instr in - match id_opt with - | Some id -> - (post, InvariantMap.add id {pre; post; visit_count} inv_map) - | None -> - (post, inv_map) - in + let update_inv_map pre ~visit_count = + let compute_post pre instr = TransferFunctions.exec_instr pre proc_data node instr in (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *) - let instr_ids = match CFG.instr_ids node with [] -> [(Sil.skip_instr, None)] | l -> l in + let instrs = match CFG.instrs node with [] -> [Sil.skip_instr] | l -> l in if debug then NodePrinter.start_session ~pp_name:(TransferFunctions.pp_session_name node) (CFG.underlying_node node) ; - let astate_post, inv_map_post = List.fold ~f:compute_post ~init:(pre, inv_map) instr_ids in + let astate_post = List.fold ~f:compute_post ~init:pre instrs in if debug then ( - let instrs = List.map ~f:fst instr_ids in L.d_strln (Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." Domain.pp pre (Sil.pp_instr_list Pp.(html Green)) instrs Domain.pp astate_post) ; NodePrinter.finish_session (CFG.underlying_node node) ) ; - let inv_map'' = - InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map_post - in - (inv_map'', Scheduler.schedule_succs work_queue node) + let inv_map' = InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map in + (inv_map', Scheduler.schedule_succs work_queue node) in if InvariantMap.mem node_id inv_map then ( let old_state = InvariantMap.find node_id inv_map in @@ -106,11 +96,9 @@ struct "Exceeded max widening threshold %d while analyzing %a. Please check your widening \ operator or increase the threshold" Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ; - update_inv_map widened_pre visit_count' ) - else - (* first time visiting this node *) - let visit_count = 1 in - update_inv_map astate_pre visit_count + update_inv_map widened_pre ~visit_count:visit_count' ) + else (* first time visiting this node *) + update_inv_map astate_pre ~visit_count:1 let rec exec_worklist cfg work_queue inv_map proc_data ~debug = diff --git a/infer/src/absint/ProcCfg.ml b/infer/src/absint/ProcCfg.ml index 31338b4f3..29cb0c609 100644 --- a/infer/src/absint/ProcCfg.ml +++ b/infer/src/absint/ProcCfg.ml @@ -114,12 +114,6 @@ module type S = sig val instrs : node -> Sil.instr list (** get the instructions from a node *) - val instr_ids : node -> (Sil.instr * id option) list - (** explode a block into its instructions and an optional id for the instruction. the purpose of - this is to specify a policy for fine-grained storage of invariants by the abstract - interpreter. the interpreter will forget invariants at program points where the id is None, - and remember them otherwise *) - val succs : t -> node -> node list val preds : t -> node -> node list @@ -160,8 +154,6 @@ module Normal = struct let instrs = Procdesc.Node.get_instrs - let instr_ids n = List.map ~f:(fun i -> (i, None)) (instrs n) - let normal_succs _ n = Procdesc.Node.get_succs n let normal_preds _ n = Procdesc.Node.get_preds n @@ -223,8 +215,6 @@ module Exceptional = struct let instrs = Procdesc.Node.get_instrs - let instr_ids n = List.map ~f:(fun i -> (i, None)) (instrs n) - let nodes (t, _) = Procdesc.get_nodes t let normal_succs _ n = Procdesc.Node.get_succs n @@ -272,8 +262,6 @@ module Backward (Base : S) = struct let instrs n = List.rev (Base.instrs n) - let instr_ids n = List.rev (Base.instr_ids n) - let succs = Base.preds let preds = Base.succs @@ -311,15 +299,6 @@ struct match Base.instrs node with [] -> [] | instrs -> [List.nth_exn instrs index] - let instr_ids (node, index) = - match Base.instr_ids node with - | [] -> - [] - | instr_ids -> - let instr, id_opt = List.nth_exn instr_ids index in - [(instr, Option.map id_opt ~f:(fun base_id -> (base_id, index)))] - - let first_of_node node = (node, 0) let last_of_node node = (node, max 0 (List.length (Base.instrs node) - 1)) diff --git a/infer/src/absint/ProcCfg.mli b/infer/src/absint/ProcCfg.mli index 07d9712df..bca572c29 100644 --- a/infer/src/absint/ProcCfg.mli +++ b/infer/src/absint/ProcCfg.mli @@ -49,12 +49,6 @@ module type S = sig val instrs : node -> Sil.instr list (** get the instructions from a node *) - val instr_ids : node -> (Sil.instr * id option) list - (** explode a block into its instructions and an optional id for the instruction. the purpose of - this is to specify a policy for fine-grained storage of invariants by the abstract - interpreter. the interpreter will forget invariants at program points where the id is None, - and remember them otherwise *) - val succs : t -> node -> node list (** all succcessors (normal and exceptional) *) diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index a743f40f5..ccf628565 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/infer/src/unit/schedulerTests.ml @@ -18,8 +18,6 @@ module MockNode = struct let instrs _ = [] - let instr_ids _ = [] - let hash = Hashtbl.hash let to_instr_nodes _ = assert false