From 596d8338eef9dd73627b09e64de666264ce151d2 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 15 Apr 2016 08:51:00 -0700 Subject: [PATCH] dealing with exceptional control-flow in abstract interpreter Reviewed By: cristianoc Differential Revision: D3178139 fb-gh-sync-id: e1f9364 fbshipit-source-id: e1f9364 --- infer/src/checkers/abstractInterpreter.ml | 70 ++++++++++++++-------- infer/src/checkers/scheduler.ml | 2 - infer/src/unit/abstractInterpreterTests.ml | 50 ++++++++++++++-- 3 files changed, 90 insertions(+), 32 deletions(-) diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index 198eea6e9..9a5211d1e 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -20,10 +20,30 @@ module Make module S = Sched (C) module M = ProcCfg.NodeIdMap (C) - type state = { post: A.astate; visit_count: int; } + type state = { pre: A.astate; post: A.astate; visit_count: int; } (* invariant map from node id -> abstract state representing postcondition for node id *) type inv_map = state M.t + (** extract the state of node [n] from [inv_map] *) + let extract_state node_id inv_map = + try + Some (M.find node_id inv_map) + with Not_found -> + L.err "Warning: No state found for node %a" C.pp_node_id node_id; + None + + (** extract the postcondition of node [n] from [inv_map] *) + let extract_post node_id inv_map = + match extract_state node_id inv_map with + | Some state -> Some state.post + | None -> None + + (** extract the precondition of node [n] from [inv_map] *) + let extract_pre node_id inv_map = + match extract_state node_id inv_map with + | Some state -> Some state.pre + | None -> None + let exec_node node astate_pre work_queue inv_map proc_data = let exec_instrs astate_acc instr = if A.is_bottom astate_acc @@ -51,36 +71,43 @@ module Make A.pp astate_post A.pp old_state.post A.pp widened_post; let inv_map' = let visit_count = old_state.visit_count + 1 in - M.add node_id { post=widened_post; visit_count; } inv_map in + M.add node_id { pre=astate_pre; post=widened_post; visit_count; } inv_map in inv_map', S.schedule_succs work_queue node end else (* first time visiting this node *) let inv_map' = let visit_count = 0 in - M.add node_id { post=astate_post; visit_count; } inv_map in + M.add node_id { pre=astate_pre; post=astate_post; visit_count; } inv_map in inv_map', S.schedule_succs work_queue node - let rec exec_worklist work_queue inv_map proc_data = + let rec exec_worklist cfg work_queue inv_map proc_data = + let compute_pre node inv_map = + (* if the [pred] -> [node] transition was normal, use post([pred]) *) + let extract_post_ pred = extract_post (C.node_id pred) inv_map in + let normal_posts = IList.map extract_post_ (C.normal_preds cfg node) in + (* if the [pred] -> [node] transition was exceptional, use pre([pred]) *) + let extract_pre_f acc pred = extract_pre (C.node_id pred) inv_map :: acc in + let all_posts = IList.fold_left extract_pre_f normal_posts (C.exceptional_preds cfg node) in + match IList.flatten_options all_posts with + | post :: posts -> Some (IList.fold_left A.join post posts) + | [] -> None in match S.pop work_queue with | Some (_, [], work_queue') -> - exec_worklist work_queue' inv_map proc_data - | Some (node, visited_pred :: visited_preds, work_queue') -> - let get_post pred_id = - (M.find pred_id inv_map).post in - (* compute the precondition for node by joining post of all visited preds *) - let join_pred_posts astate_acc pred_id = - A.join (get_post pred_id) astate_acc in - let astate_pre = IList.fold_left join_pred_posts (get_post visited_pred) visited_preds in - let inv_map', work_queue'' = exec_node node astate_pre work_queue' inv_map proc_data in - exec_worklist work_queue'' inv_map' proc_data - | None -> inv_map + exec_worklist cfg work_queue' inv_map proc_data + | Some (node, _, work_queue') -> + let inv_map_post, work_queue_post = match compute_pre node inv_map with + | Some astate_pre -> exec_node node astate_pre work_queue' inv_map proc_data + | None -> inv_map, work_queue' in + exec_worklist cfg work_queue_post inv_map_post proc_data + | None -> + inv_map (* compute and return an invariant map for [cfg] *) let exec_cfg cfg proc_data = let start_node = C.start_node cfg in let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty proc_data in - exec_worklist work_queue' inv_map' proc_data + exec_worklist cfg work_queue' inv_map' proc_data (* compute and return an invariant map for [pdesc] *) let exec_pdesc ({ ProcData.pdesc; } as proc_data) = @@ -91,16 +118,7 @@ module Make let compute_post ({ ProcData.pdesc; } as proc_data) = let cfg = C.from_pdesc pdesc in let inv_map = exec_cfg cfg proc_data in - try - let end_state = M.find (C.node_id (C.exit_node cfg)) inv_map in - Some (end_state.post) - with Not_found -> - (* TODO: this happens when we get a malformed CFG due to a frontend failure. can eliminate in - the future once we fix the frontends. *) - L.err - "Warning: No postcondition found for exit node of %a" - Procname.pp (Cfg.Procdesc.get_proc_name pdesc); - None + extract_post (C.node_id (C.exit_node cfg)) inv_map module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct diff --git a/infer/src/checkers/scheduler.ml b/infer/src/checkers/scheduler.ml index 73e302d97..2278eb864 100644 --- a/infer/src/checkers/scheduler.ml +++ b/infer/src/checkers/scheduler.ml @@ -57,7 +57,6 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct let visited_preds' = IdSet.add node_id t.visited_preds in let priority' = compute_priority cfg t.node visited_preds' in { t with visited_preds = visited_preds'; priority = priority'; } - end type t = { worklist : WorkUnit.t M.t; cfg : C.t; } @@ -100,5 +99,4 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct with Not_found -> None let empty cfg = { worklist = M.empty; cfg; } - end diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index d1e43714a..230ed69a6 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -56,16 +56,22 @@ module PathCountTransferFunctions = struct end -module TestInterpreter = AnalyzerTester.Make +module NormalTestInterpreter = AnalyzerTester.Make (ProcCfg.Normal) (Scheduler.ReversePostorder) (PathCountDomain) (PathCountTransferFunctions) +module ExceptionalTestInterpreter = AnalyzerTester.Make + (ProcCfg.Exceptional) + (Scheduler.ReversePostorder) + (PathCountDomain) + (PathCountTransferFunctions) + let tests = let open OUnit2 in let open AnalyzerTester.StructuredSil in - let test_list = [ + let normal_test_list = [ "straightline", [ invariant "1"; @@ -176,5 +182,41 @@ let tests = ); invariant "1" ]; - ] |> TestInterpreter.create_tests in - "analyzer_tests_suite">:::test_list + ] |> NormalTestInterpreter.create_tests in + let exceptional_test_list = [ + "try1", + [ + Try ( + [ + invariant "1"; + ], + [ + invariant "1"; (* catch block should be visited *) + ], + [ + invariant "2"; (* could come from try or catch block *) + ] + ); + invariant "2" + ]; + "try1", + [ + Try ( + [ + (* note: each instruction in try block is treated as potentially-excepting... *) + (* point 1 *) + invariant "1"; (* point 2 *) + invariant "1"; (* point 3 *) + ], + [ + (* ... so |paths through catch block| shoud be |number of instructions in try block| *) + invariant "2"; (* point 4 *) + ], + [ + invariant "3"; (* could arrive here via (1, 2, 3), (1, 4), or (2, 4) *) + ] + ); + invariant "3" + ]; + ] |> ExceptionalTestInterpreter.create_tests in + "analyzer_tests_suite">:::(normal_test_list @ exceptional_test_list)