From 19da59cf198cc6e2ca03e9f7283285b8ab6b08e2 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 4 May 2017 10:49:09 -0700 Subject: [PATCH] [hil] functor for easily creating HIL analyses Summary: Last step for converting thread-safety and quandary to HIL. Push the logic for managing the id map and converting the instructions into a functor. This way, client analyses can simply write HIL transfer functions and call the functor. Reviewed By: jberdine Differential Revision: D4989987 fbshipit-source-id: 485169e --- infer/src/checkers/AbstractInterpreter.ml | 8 +- infer/src/checkers/AbstractInterpreter.mli | 6 +- infer/src/checkers/LowerHil.ml | 42 ++ infer/src/checkers/LowerHil.mli | 24 + infer/src/checkers/ThreadSafety.ml | 556 ++++++++++----------- infer/src/checkers/ThreadSafetyDomain.ml | 21 +- infer/src/checkers/ThreadSafetyDomain.mli | 6 +- infer/src/checkers/transferFunctions.ml | 26 +- infer/src/checkers/transferFunctions.mli | 21 +- infer/src/quandary/TaintAnalysis.ml | 358 ++++++------- infer/src/unit/TaintTests.ml | 7 +- infer/src/unit/analyzerTester.ml | 3 +- 12 files changed, 534 insertions(+), 544 deletions(-) create mode 100644 infer/src/checkers/LowerHil.ml create mode 100644 infer/src/checkers/LowerHil.mli diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml index 562b875b2..40c1a83e2 100644 --- a/infer/src/checkers/AbstractInterpreter.ml +++ b/infer/src/checkers/AbstractInterpreter.ml @@ -14,7 +14,7 @@ module L = Logging type 'a state = { pre: 'a; post: 'a; visit_count: int; } module type S = sig - module TransferFunctions : TransferFunctions.S + module TransferFunctions : TransferFunctions.SIL module InvariantMap : Caml.Map.S with type key = TransferFunctions.CFG.id @@ -44,7 +44,7 @@ end module MakeNoCFG (Scheduler : Scheduler.S) - (TransferFunctions : TransferFunctions.S with module CFG = Scheduler.CFG) = struct + (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) = struct module CFG = Scheduler.CFG module InvariantMap = ProcCfg.NodeIdMap (CFG) @@ -167,8 +167,8 @@ module Interprocedural (Summ : Summary.S) = struct end -module MakeWithScheduler (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.Make) = +module MakeWithScheduler (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.MakeSIL) = MakeNoCFG (S (C)) (T (C)) -module Make (C : ProcCfg.S) (T : TransferFunctions.Make) = +module Make (C : ProcCfg.S) (T : TransferFunctions.MakeSIL) = MakeWithScheduler (C) (Scheduler.ReversePostorder) (T) diff --git a/infer/src/checkers/AbstractInterpreter.mli b/infer/src/checkers/AbstractInterpreter.mli index af5d11e04..e64404ffb 100644 --- a/infer/src/checkers/AbstractInterpreter.mli +++ b/infer/src/checkers/AbstractInterpreter.mli @@ -13,7 +13,7 @@ type 'a state = { pre: 'a; post: 'a; visit_count: int; } (** type of an intraprocedural abstract interpreter *) module type S = sig - module TransferFunctions : TransferFunctions.S + module TransferFunctions : TransferFunctions.SIL module InvariantMap : Caml.Map.S with type key = TransferFunctions.CFG.id @@ -52,14 +52,14 @@ end (** create an intraprocedural abstract interpreter from a scheduler and transfer functions *) module MakeNoCFG (Scheduler : Scheduler.S) - (TransferFunctions : TransferFunctions.S with module CFG = Scheduler.CFG) : + (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) : S with module TransferFunctions = TransferFunctions (** create an intraprocedural abstract interpreter from a CFG and functors for creating a scheduler/ transfer functions from a CFG *) module Make (CFG : ProcCfg.S) - (MakeTransferFunctions : TransferFunctions.Make) : + (MakeTransferFunctions : TransferFunctions.MakeSIL) : S with module TransferFunctions = MakeTransferFunctions(CFG) (** create an interprocedural abstract interpreter given logic for handling summaries *) diff --git a/infer/src/checkers/LowerHil.ml b/infer/src/checkers/LowerHil.ml new file mode 100644 index 000000000..991228e8f --- /dev/null +++ b/infer/src/checkers/LowerHil.ml @@ -0,0 +1,42 @@ +(* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd + +module Make (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) = struct + module TransferFunctions = MakeTransferFunctions (CFG) + module CFG = TransferFunctions.CFG + module Domain = AbstractDomain.Pair (TransferFunctions.Domain) (IdAccessPathMapDomain) + type extras = TransferFunctions.extras + + let exec_instr ((actual_state, id_map) as astate) extras node instr = + let f_resolve_id id = + try Some (IdAccessPathMapDomain.find id id_map) + with Not_found -> None in + match HilInstr.of_sil ~f_resolve_id instr with + | Bind (id, access_path) -> + let id_map' = IdAccessPathMapDomain.add id access_path id_map in + if phys_equal id_map id_map' + then astate + else actual_state, id_map' + | Unbind ids -> + let id_map' = + List.fold + ~f:(fun acc id -> IdAccessPathMapDomain.remove id acc) ~init:id_map ids in + if phys_equal id_map id_map' + then astate + else actual_state, id_map' + | Instr hil_instr -> + let actual_state' = TransferFunctions.exec_instr actual_state extras node hil_instr in + if phys_equal actual_state actual_state' + then astate + else actual_state', id_map + | Ignore -> + astate +end diff --git a/infer/src/checkers/LowerHil.mli b/infer/src/checkers/LowerHil.mli new file mode 100644 index 000000000..7e2ae4254 --- /dev/null +++ b/infer/src/checkers/LowerHil.mli @@ -0,0 +1,24 @@ +(* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd + +(** Functor for turning HIL transfer functions into SIL transfer functions *) +module Make (MakeTransferFunctions : TransferFunctions.MakeHIL) (CFG : ProcCfg.S) : sig + module TransferFunctions : module type of (MakeTransferFunctions (CFG)) + + module CFG : module type of TransferFunctions.CFG + + module Domain : + module type of AbstractDomain.Pair (TransferFunctions.Domain) (IdAccessPathMapDomain) + + type extras = TransferFunctions.extras + + val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate +end diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index db03494fd..014b0338c 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -384,295 +384,283 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> false - let exec_instr (astate : Domain.astate) ({ ProcData.extras; tenv; pdesc; } as proc_data) _ instr = + let add_reads exps loc accesses locks attribute_map proc_data = + List.fold + ~f:(fun acc exp -> add_access exp loc Read acc locks attribute_map proc_data) + exps + ~init:accesses + + let exec_instr + (astate : Domain.astate) + ({ ProcData.extras; tenv; pdesc; } as proc_data) + _ + (instr : HilInstr.t) = let open Domain in - let add_reads exps loc accesses locks attribute_map proc_data = - List.fold - ~f:(fun acc exp -> add_access exp loc Read acc locks attribute_map proc_data) - exps - ~init:accesses in - let exec_instr_ = function - | HilInstr.Call (Some ret_base, Direct procname, actuals, _, loc) - when acquires_ownership procname tenv -> - let accesses = - add_reads actuals loc astate.accesses astate.locks astate.attribute_map proc_data in - let attribute_map = - AttributeMapDomain.add_attribute - (ret_base, []) Attribute.unconditionally_owned astate.attribute_map in - { astate with accesses; attribute_map; } - - | HilInstr.Call (ret_opt, Direct callee_pname, actuals, call_flags, loc) -> - let accesses = - add_reads actuals loc astate.accesses astate.locks astate.attribute_map proc_data in - let astate = { astate with accesses; } in - let astate_callee = - (* assuming that modeled procedures do not have useful summaries *) - if is_thread_utils_method "assertMainThread" callee_pname - then - { astate with threads = true; } - else - match get_lock_model callee_pname with - | Lock -> - { astate with locks = true; } - | Unlock -> - { astate with locks = false; } - | LockedIfTrue -> - begin - match ret_opt with - | Some ret_access_path -> - let attribute_map = - AttributeMapDomain.add_attribute - (ret_access_path, []) - (Choice Choice.LockHeld) - astate.attribute_map in - { astate with attribute_map; } - | None -> - failwithf - "Procedure %a specified as returning boolean, but returns nothing" - Typ.Procname.pp callee_pname - end - | NoEffect -> - match get_summary pdesc callee_pname actuals loc tenv with - | Some (callee_threads, callee_locks, callee_accesses, return_attributes) -> - let update_caller_accesses pre callee_accesses caller_accesses = - let combined_accesses = - PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc) - |> PathDomain.join (AccessDomain.get_accesses pre caller_accesses) in - AccessDomain.add pre combined_accesses caller_accesses in - let locks = callee_locks || astate.locks in - let threads = callee_threads || astate.threads in - let unprotected = is_unprotected locks pdesc in - (* add [ownership_accesses] to the [accesses_acc] with a protected pre if - [exp] is owned, and an appropriate unprotected pre otherwise *) - let add_ownership_access ownership_accesses actual_exp accesses_acc = - match actual_exp with - | HilExp.Constant _ -> - (* the actual is a constant, so it's owned in the caller. *) - accesses_acc - | HilExp.AccessPath actual_access_path -> - if is_owned actual_access_path astate.attribute_map - then - (* the actual passed to the current callee is owned. drop all the - conditional accesses for that actual, since they're all safe *) - accesses_acc - else - let pre = - if unprotected - then - let base = fst actual_access_path in - match FormalMap.get_formal_index base extras with - | Some formal_index -> - (* the actual passed to the current callee is rooted in a - formal *) - AccessPrecondition.Unprotected (Some formal_index) - | None -> - match - AttributeMapDomain.get_conditional_ownership_index - actual_access_path - astate.attribute_map - with - | Some formal_index -> - (* access path conditionally owned if [formal_index] is - owned *) - AccessPrecondition.Unprotected (Some formal_index) - | None -> - (* access path not rooted in a formal and not - conditionally owned *) - AccessPrecondition.unprotected - else - (* access protected by held lock *) - AccessPrecondition.Protected in - update_caller_accesses pre ownership_accesses accesses_acc - | _ -> - (* couldn't find access path, don't know if it's owned *) - update_caller_accesses - AccessPrecondition.unprotected ownership_accesses accesses_acc in - let accesses = - let update_accesses pre callee_accesses accesses_acc = match pre with - | AccessPrecondition.Protected -> - update_caller_accesses pre callee_accesses accesses_acc - | AccessPrecondition.Unprotected None -> - let pre' = - if unprotected - then pre - else AccessPrecondition.Protected in - update_caller_accesses pre' callee_accesses accesses_acc - | AccessPrecondition.Unprotected (Some index) -> - add_ownership_access - callee_accesses (List.nth_exn actuals index) accesses_acc in - AccessDomain.fold update_accesses callee_accesses astate.accesses in + match instr with + | Call (Some ret_base, Direct procname, actuals, _, loc) + when acquires_ownership procname tenv -> + let accesses = + add_reads actuals loc astate.accesses astate.locks astate.attribute_map proc_data in + let attribute_map = + AttributeMapDomain.add_attribute + (ret_base, []) Attribute.unconditionally_owned astate.attribute_map in + { astate with accesses; attribute_map; } + + | Call (ret_opt, Direct callee_pname, actuals, call_flags, loc) -> + let accesses = + add_reads actuals loc astate.accesses astate.locks astate.attribute_map proc_data in + let astate = { astate with accesses; } in + let astate_callee = + (* assuming that modeled procedures do not have useful summaries *) + if is_thread_utils_method "assertMainThread" callee_pname + then + { astate with threads = true; } + else + match get_lock_model callee_pname with + | Lock -> + { astate with locks = true; } + | Unlock -> + { astate with locks = false; } + | LockedIfTrue -> + begin + match ret_opt with + | Some ret_access_path -> let attribute_map = - propagate_return_attributes - ret_opt - return_attributes - actuals - astate.attribute_map - extras in - { astate with locks; threads; accesses; attribute_map; } + AttributeMapDomain.add_attribute + (ret_access_path, []) + (Choice Choice.LockHeld) + astate.attribute_map in + { astate with attribute_map; } | None -> - let should_assume_returns_ownership (call_flags : CallFlags.t) actuals = - (* assume non-interface methods with no summary and no parameters return - ownership *) - not (call_flags.cf_interface) && List.is_empty actuals in - if is_box callee_pname - then - match ret_opt, actuals with - | Some ret, HilExp.AccessPath actual_ap :: _ - when AttributeMapDomain.has_attribute - actual_ap Functional astate.attribute_map -> - (* TODO: check for constants, which are functional? *) - let attribute_map = - AttributeMapDomain.add_attribute - (ret, []) - Functional - astate.attribute_map in - { astate with attribute_map; } - | _ -> - astate - else if should_assume_returns_ownership call_flags actuals - then - match ret_opt with - | Some ret -> - let attribute_map = - AttributeMapDomain.add_attribute - (ret, []) - Attribute.unconditionally_owned - astate.attribute_map in - { astate with attribute_map; } - | None -> - astate - else - astate in - begin - match ret_opt with - | Some (_, { Typ.desc=Typ.Tint ILong | Tfloat FDouble }) -> - (* writes to longs and doubles are not guaranteed to be atomic in Java, so don't - bother tracking whether a returned long or float value is functional *) - astate_callee - | Some ret -> - let add_if_annotated predicate attribute attribute_map = - if PatternMatch.override_exists predicate tenv callee_pname - then - AttributeMapDomain.add_attribute (ret, []) attribute attribute_map - else - attribute_map in - let attribute_map = - add_if_annotated is_functional Functional astate_callee.attribute_map - |> add_if_annotated - (has_return_annot Annotations.ia_is_returns_ownership) - Domain.Attribute.unconditionally_owned in - { astate_callee with attribute_map; } - | _ -> - astate_callee - end + failwithf + "Procedure %a specified as returning boolean, but returns nothing" + Typ.Procname.pp callee_pname + end + | NoEffect -> + match get_summary pdesc callee_pname actuals loc tenv with + | Some (callee_threads, callee_locks, callee_accesses, return_attributes) -> + let update_caller_accesses pre callee_accesses caller_accesses = + let combined_accesses = + PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc) + |> PathDomain.join (AccessDomain.get_accesses pre caller_accesses) in + AccessDomain.add pre combined_accesses caller_accesses in + let locks = callee_locks || astate.locks in + let threads = callee_threads || astate.threads in + let unprotected = is_unprotected locks pdesc in + (* add [ownership_accesses] to the [accesses_acc] with a protected pre if + [exp] is owned, and an appropriate unprotected pre otherwise *) + let add_ownership_access ownership_accesses actual_exp accesses_acc = + match actual_exp with + | HilExp.Constant _ -> + (* the actual is a constant, so it's owned in the caller. *) + accesses_acc + | HilExp.AccessPath actual_access_path -> + if is_owned actual_access_path astate.attribute_map + then + (* the actual passed to the current callee is owned. drop all the + conditional accesses for that actual, since they're all safe *) + accesses_acc + else + let pre = + if unprotected + then + let base = fst actual_access_path in + match FormalMap.get_formal_index base extras with + | Some formal_index -> + (* the actual passed to the current callee is rooted in a + formal *) + AccessPrecondition.Unprotected (Some formal_index) + | None -> + match + AttributeMapDomain.get_conditional_ownership_index + actual_access_path + astate.attribute_map + with + | Some formal_index -> + (* access path conditionally owned if [formal_index] is + owned *) + AccessPrecondition.Unprotected (Some formal_index) + | None -> + (* access path not rooted in a formal and not + conditionally owned *) + AccessPrecondition.unprotected + else + (* access protected by held lock *) + AccessPrecondition.Protected in + update_caller_accesses pre ownership_accesses accesses_acc + | _ -> + (* couldn't find access path, don't know if it's owned *) + update_caller_accesses + AccessPrecondition.unprotected ownership_accesses accesses_acc in + let accesses = + let update_accesses pre callee_accesses accesses_acc = match pre with + | AccessPrecondition.Protected -> + update_caller_accesses pre callee_accesses accesses_acc + | AccessPrecondition.Unprotected None -> + let pre' = + if unprotected + then pre + else AccessPrecondition.Protected in + update_caller_accesses pre' callee_accesses accesses_acc + | AccessPrecondition.Unprotected (Some index) -> + add_ownership_access + callee_accesses (List.nth_exn actuals index) accesses_acc in + AccessDomain.fold update_accesses callee_accesses astate.accesses in + let attribute_map = + propagate_return_attributes + ret_opt + return_attributes + actuals + astate.attribute_map + extras in + { locks; threads; accesses; attribute_map; } + | None -> + let should_assume_returns_ownership (call_flags : CallFlags.t) actuals = + (* assume non-interface methods with no summary and no parameters return + ownership *) + not (call_flags.cf_interface) && List.is_empty actuals in + if is_box callee_pname + then + match ret_opt, actuals with + | Some ret, HilExp.AccessPath actual_ap :: _ + when AttributeMapDomain.has_attribute + actual_ap Functional astate.attribute_map -> + (* TODO: check for constants, which are functional? *) + let attribute_map = + AttributeMapDomain.add_attribute + (ret, []) + Functional + astate.attribute_map in + { astate with attribute_map; } + | _ -> + astate + else if should_assume_returns_ownership call_flags actuals + then + match ret_opt with + | Some ret -> + let attribute_map = + AttributeMapDomain.add_attribute + (ret, []) + Attribute.unconditionally_owned + astate.attribute_map in + { astate with attribute_map; } + | None -> + astate + else + astate in + begin + match ret_opt with + | Some (_, { Typ.desc=Typ.Tint ILong | Tfloat FDouble }) -> + (* writes to longs and doubles are not guaranteed to be atomic in Java, so don't + bother tracking whether a returned long or float value is functional *) + astate_callee + | Some ret -> + let add_if_annotated predicate attribute attribute_map = + if PatternMatch.override_exists predicate tenv callee_pname + then + AttributeMapDomain.add_attribute (ret, []) attribute attribute_map + else + attribute_map in + let attribute_map = + add_if_annotated is_functional Functional astate_callee.attribute_map + |> add_if_annotated + (has_return_annot Annotations.ia_is_returns_ownership) + Domain.Attribute.unconditionally_owned in + { astate_callee with attribute_map; } + | _ -> + astate_callee + end - | HilInstr.Write (lhs_access_path, rhs_exp, loc) -> - let rhs_accesses = + | Write (lhs_access_path, rhs_exp, loc) -> + let rhs_accesses = + add_access + rhs_exp loc Read astate.accesses astate.locks astate.attribute_map proc_data in + let rhs_access_paths = HilExp.get_access_paths rhs_exp in + let is_functional = + not (List.is_empty rhs_access_paths) && + List.for_all + ~f:(fun access_path -> + AttributeMapDomain.has_attribute access_path Functional astate.attribute_map) + rhs_access_paths in + let accesses = + if is_functional + then + (* we want to forget about writes to @Functional fields altogether, otherwise we'll + report spurious read/write races *) + rhs_accesses + else add_access - rhs_exp loc Read astate.accesses astate.locks astate.attribute_map proc_data in - let rhs_access_paths = HilExp.get_access_paths rhs_exp in - let is_functional = - not (List.is_empty rhs_access_paths) && - List.for_all - ~f:(fun access_path -> - AttributeMapDomain.has_attribute access_path Functional astate.attribute_map) - rhs_access_paths in - let accesses = - if is_functional - then - (* we want to forget about writes to @Functional fields altogether, otherwise we'll - report spurious read/write races *) + (AccessPath lhs_access_path) + loc + Write rhs_accesses - else - add_access - (AccessPath lhs_access_path) - loc - Write - rhs_accesses - astate.locks - astate.attribute_map - proc_data in - let attribute_map = - propagate_attributes - lhs_access_path (HilExp.get_access_paths rhs_exp) astate.attribute_map extras in - { astate with accesses; attribute_map; } - - | HilInstr.Assume (assume_exp, _, _, loc) -> - let rec eval_binop op var e1 e2 = - match eval_bexp var e1, eval_bexp var e2 with - | Some b1, Some b2 -> Some (op b1 b2) - | _ -> None - (* return Some bool_value if the given boolean expression evaluates to bool_value when - [var] is set to true. return None if it has free variables that stop us from - evaluating it *) - and eval_bexp var = function - | HilExp.AccessPath ap when AccessPath.Raw.equal ap var -> - Some true - | HilExp.Constant c -> - Some (not (Const.iszero_int_float c)) - | HilExp.UnaryOperator (Unop.LNot, e, _) -> - let b_opt = eval_bexp var e in - Option.map ~f:not b_opt - | HilExp.BinaryOperator (Binop.LAnd, e1, e2) -> - eval_binop (&&) var e1 e2 - | HilExp.BinaryOperator (Binop.LOr, e1, e2) -> - eval_binop (||) var e1 e2 - | HilExp.BinaryOperator (Binop.Eq, e1, e2) -> - eval_binop Bool.equal var e1 e2 - | HilExp.BinaryOperator (Binop.Ne, e1, e2) -> - eval_binop (<>) var e1 e2 - | _ -> - (* non-boolean expression; can't evaluate it *) - None in - let add_choice bool_value acc = function - | Choice.LockHeld -> - let locks = bool_value in - { acc with locks; } - | Choice.OnMainThread -> - let threads = bool_value in - { acc with threads; } in - - let accesses = - add_access - assume_exp loc Read astate.accesses astate.locks astate.attribute_map proc_data in - let astate' = - match HilExp.get_access_paths assume_exp with - | [access_path] -> - let choices = AttributeMapDomain.get_choices access_path astate.attribute_map in - begin - match eval_bexp access_path assume_exp with - | Some bool_value -> - (* prune (prune_exp) can only evaluate to true if the choice is [bool_value]. - add the constraint that the the choice must be [bool_value] to the state *) - List.fold ~f:(add_choice bool_value) ~init:astate choices - | None -> - astate - end - | _ -> - astate in - { astate' with accesses; } - | (HilInstr.Call (_, Indirect _, _, _, _) as hil_instr) -> - failwithf "Unexpected indirect call instruction %a" HilInstr.pp hil_instr in - - let f_resolve_id id = - try Some (IdAccessPathMapDomain.find id astate.id_map) - with Not_found -> None in - match HilInstr.of_sil ~f_resolve_id instr with - | Bind (id, access_path) -> - let id_map = IdAccessPathMapDomain.add id access_path astate.id_map in - { astate with id_map; } - | Unbind ids -> - let id_map = - List.fold - ~f:(fun acc id -> IdAccessPathMapDomain.remove id acc) ~init:astate.id_map ids in - { astate with id_map; } - | Instr hil_instr -> - exec_instr_ hil_instr - | Ignore -> - astate + astate.locks + astate.attribute_map + proc_data in + let attribute_map = + propagate_attributes + lhs_access_path (HilExp.get_access_paths rhs_exp) astate.attribute_map extras in + { astate with accesses; attribute_map; } + + | Assume (assume_exp, _, _, loc) -> + let rec eval_binop op var e1 e2 = + match eval_bexp var e1, eval_bexp var e2 with + | Some b1, Some b2 -> Some (op b1 b2) + | _ -> None + (* return Some bool_value if the given boolean expression evaluates to bool_value when + [var] is set to true. return None if it has free variables that stop us from + evaluating it *) + and eval_bexp var = function + | HilExp.AccessPath ap when AccessPath.Raw.equal ap var -> + Some true + | HilExp.Constant c -> + Some (not (Const.iszero_int_float c)) + | HilExp.UnaryOperator (Unop.LNot, e, _) -> + let b_opt = eval_bexp var e in + Option.map ~f:not b_opt + | HilExp.BinaryOperator (Binop.LAnd, e1, e2) -> + eval_binop (&&) var e1 e2 + | HilExp.BinaryOperator (Binop.LOr, e1, e2) -> + eval_binop (||) var e1 e2 + | HilExp.BinaryOperator (Binop.Eq, e1, e2) -> + eval_binop Bool.equal var e1 e2 + | HilExp.BinaryOperator (Binop.Ne, e1, e2) -> + eval_binop (<>) var e1 e2 + | _ -> + (* non-boolean expression; can't evaluate it *) + None in + let add_choice bool_value acc = function + | Choice.LockHeld -> + let locks = bool_value in + { acc with locks; } + | Choice.OnMainThread -> + let threads = bool_value in + { acc with threads; } in + + let accesses = + add_access + assume_exp loc Read astate.accesses astate.locks astate.attribute_map proc_data in + let astate' = + match HilExp.get_access_paths assume_exp with + | [access_path] -> + let choices = AttributeMapDomain.get_choices access_path astate.attribute_map in + begin + match eval_bexp access_path assume_exp with + | Some bool_value -> + (* prune (prune_exp) can only evaluate to true if the choice is [bool_value]. + add the constraint that the the choice must be [bool_value] to the state *) + List.fold ~f:(add_choice bool_value) ~init:astate choices + | None -> + astate + end + | _ -> + astate in + { astate' with accesses; } + | Call (_, Indirect _, _, _, _) -> + failwithf "Unexpected indirect call instruction %a" HilInstr.pp instr end -module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions) +module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (LowerHil.Make(TransferFunctions)) module Interprocedural = AbstractInterpreter.Interprocedural (Summary) @@ -810,12 +798,12 @@ let analyze_procedure callback = ~f:add_owned_formal owned_formals ~init:ThreadSafetyDomain.empty.attribute_map in - { ThreadSafetyDomain.empty with attribute_map; threads; } + { ThreadSafetyDomain.empty with attribute_map; threads; }, IdAccessPathMapDomain.empty else - { ThreadSafetyDomain.empty with threads; } in + { ThreadSafetyDomain.empty with threads; }, IdAccessPathMapDomain.empty in match Analyzer.compute_post proc_data ~initial with - | Some { threads; locks; accesses; attribute_map; } -> + | Some ({ threads; locks; accesses; attribute_map; }, _) -> let return_var_ap = AccessPath.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc)) diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index a12185399..02c4b66d8 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -201,20 +201,18 @@ type astate = threads: ThreadsDomain.astate; locks : LocksDomain.astate; accesses : AccessDomain.astate; - id_map : IdAccessPathMapDomain.astate; attribute_map : AttributeMapDomain.astate; } -type summary = ThreadsDomain.astate * LocksDomain.astate - * AccessDomain.astate * AttributeSetDomain.astate +type summary = + ThreadsDomain.astate * LocksDomain.astate * AccessDomain.astate * AttributeSetDomain.astate let empty = let threads = false in let locks = false in let accesses = AccessDomain.empty in - let id_map = IdAccessPathMapDomain.empty in let attribute_map = AccessPath.RawMap.empty in - { threads; locks; accesses; id_map; attribute_map; } + { threads; locks; accesses; attribute_map; } let (<=) ~lhs ~rhs = if phys_equal lhs rhs @@ -223,7 +221,6 @@ let (<=) ~lhs ~rhs = ThreadsDomain.(<=) ~lhs:lhs.threads ~rhs:rhs.threads && LocksDomain.(<=) ~lhs:lhs.locks ~rhs:rhs.locks && AccessDomain.(<=) ~lhs:lhs.accesses ~rhs:rhs.accesses && - IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map && AttributeMapDomain.(<=) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map let join astate1 astate2 = @@ -234,9 +231,8 @@ let join astate1 astate2 = let threads = ThreadsDomain.join astate1.threads astate2.threads in let locks = LocksDomain.join astate1.locks astate2.locks in let accesses = AccessDomain.join astate1.accesses astate2.accesses in - let id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in - { threads; locks; accesses; id_map; attribute_map; } + { threads; locks; accesses; attribute_map; } let widen ~prev ~next ~num_iters = if phys_equal prev next @@ -246,10 +242,9 @@ let widen ~prev ~next ~num_iters = let threads = ThreadsDomain.widen ~prev:prev.threads ~next:next.threads ~num_iters in let locks = LocksDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in let accesses = AccessDomain.widen ~prev:prev.accesses ~next:next.accesses ~num_iters in - let id_map = IdAccessPathMapDomain.widen ~prev:prev.id_map ~next:next.id_map ~num_iters in let attribute_map = AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters in - { threads; locks; accesses; id_map; attribute_map; } + { threads; locks; accesses; attribute_map; } let pp_summary fmt (threads, locks, accesses, return_attributes) = F.fprintf @@ -260,13 +255,11 @@ let pp_summary fmt (threads, locks, accesses, return_attributes) = AccessDomain.pp accesses AttributeSetDomain.pp return_attributes -let pp fmt { threads; locks; accesses; id_map; attribute_map; } = +let pp fmt { threads; locks; accesses; attribute_map; } = F.fprintf fmt - "Threads: %a Locks: %a Accesses %a Id Map: %a Attribute Map:\ - %a" + "Threads: %a Locks: %a Accesses: %a Attribute Map: %a" ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses - IdAccessPathMapDomain.pp id_map AttributeMapDomain.pp attribute_map diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 3f765c4f1..6b8c90bdb 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -125,16 +125,14 @@ type astate = (** boolean that is true if a lock must currently be held *) accesses : AccessDomain.astate; (** read and writes accesses performed without ownership permissions *) - id_map : IdAccessPathMapDomain.astate; - (** map used to decompile temporary variables into access paths *) attribute_map : AttributeMapDomain.astate; (** map of access paths to attributes such as owned, functional, ... *) } (** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of the attributes associated with the return value *) -type summary = ThreadsDomain.astate * LocksDomain.astate - * AccessDomain.astate * AttributeSetDomain.astate +type summary = + ThreadsDomain.astate * LocksDomain.astate * AccessDomain.astate * AttributeSetDomain.astate include AbstractDomain.WithBottom with type astate := astate diff --git a/infer/src/checkers/transferFunctions.ml b/infer/src/checkers/transferFunctions.ml index e79d392ca..f0b8393bf 100644 --- a/infer/src/checkers/transferFunctions.ml +++ b/infer/src/checkers/transferFunctions.ml @@ -9,22 +9,28 @@ open! IStd -(** Transfer functions that push abstract states across instructions. A typical client should - implement the Make signature to allow the transfer functions to be used with any kind of CFG. *) - module type S = sig module CFG : ProcCfg.S - - (** abstract domain whose state we propagate *) module Domain : AbstractDomain.S - (** read-only extra state (results of previous analyses, globals, etc.) *) type extras + type instr + + val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> instr -> Domain.astate +end + +module type SIL = sig + include (S with type instr := Sil.instr) +end + +module type HIL = sig + include (S with type instr := HilInstr.t) +end - (** {A} instr {A'}. [node] is the node of the current instruction *) - val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate +module type MakeSIL = functor (C : ProcCfg.S) -> sig + include (SIL with module CFG = C) end -module type Make = functor (C : ProcCfg.S) -> sig - include (S with module CFG = C) +module type MakeHIL = functor (C : ProcCfg.S) -> sig + include (HIL with module CFG = C) end diff --git a/infer/src/checkers/transferFunctions.mli b/infer/src/checkers/transferFunctions.mli index e79d392ca..f1ca11d30 100644 --- a/infer/src/checkers/transferFunctions.mli +++ b/infer/src/checkers/transferFunctions.mli @@ -21,10 +21,25 @@ module type S = sig (** read-only extra state (results of previous analyses, globals, etc.) *) type extras + (** type of the instructions the transfer functions operate on *) + type instr + (** {A} instr {A'}. [node] is the node of the current instruction *) - val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate + val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> instr -> Domain.astate +end + +module type SIL = sig + include (S with type instr := Sil.instr) +end + +module type HIL = sig + include (S with type instr := HilInstr.t) +end + +module type MakeSIL = functor (C : ProcCfg.S) -> sig + include (SIL with module CFG = C) end -module type Make = functor (C : ProcCfg.S) -> sig - include (S with module CFG = C) +module type MakeHIL = functor (C : ProcCfg.S) -> sig + include (HIL with module CFG = C) end diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 06704d4a9..233423fa7 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -29,45 +29,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct summary.payload.quandary end) - module Domain = struct - type astate = - { - access_tree : TaintDomain.astate; (* mapping of access paths to trace sets *) - id_map : IdMapDomain.astate; (* mapping of id's to access paths for normalization *) - } - - let empty = - let access_tree = TaintDomain.empty in - let id_map = IdMapDomain.empty in - { access_tree; id_map; } - - let (<=) ~lhs ~rhs = - if phys_equal lhs rhs - then true - else - TaintDomain.(<=) ~lhs:lhs.access_tree ~rhs:rhs.access_tree && - IdMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map - - let join astate1 astate2 = - if phys_equal astate1 astate2 - then astate1 - else - let access_tree = TaintDomain.join astate1.access_tree astate2.access_tree in - let id_map = IdMapDomain.join astate1.id_map astate2.id_map in - { access_tree; id_map; } - - let widen ~prev ~next ~num_iters = - if phys_equal prev next - then prev - else - let access_tree = - TaintDomain.widen ~prev:prev.access_tree ~next:next.access_tree ~num_iters in - let id_map = IdMapDomain.widen ~prev:prev.id_map ~next:next.id_map ~num_iters in - { access_tree; id_map; } - - let pp fmt { access_tree; id_map; } = - F.fprintf fmt "(%a, %a)" TaintDomain.pp access_tree IdMapDomain.pp id_map - end + module Domain = TaintDomain let is_global (var, _) = match var with | Var.ProgramVar pvar -> Pvar.is_global pvar @@ -94,10 +56,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct type extras = FormalMap.t - let resolve_id id_map id = - try Some (IdMapDomain.find id id_map) - with Not_found -> None - (* get the node associated with [access_path] in [access_tree] *) let access_path_get_node access_path access_tree (proc_data : FormalMap.t ProcData.t) = match TaintDomain.get_node access_path access_tree with @@ -131,13 +89,6 @@ module Make (TaintSpecification : TaintSpec.S) = struct else AccessPath.Exact raw_access_path in access_path_get_node access_path access_tree proc_data - (* get the node associated with [exp] in [access_tree] *) - let exp_get_node ?(abstracted=false) exp typ { Domain.access_tree; id_map; } proc_data = - let f_resolve_id = resolve_id id_map in - match AccessPath.of_lhs_exp exp typ ~f_resolve_id with - | Some raw_access_path -> exp_get_node_ ~abstracted raw_access_path access_tree proc_data - | None -> None - (* get the node associated with [exp] in [access_tree] *) let hil_exp_get_node ?(abstracted=false) (exp : HilExp.t) access_tree proc_data = match exp with @@ -195,7 +146,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct List.iter ~f:report_error (TraceDomain.get_reportable_paths ~cur_site trace ~trace_of_pname) - let add_sinks sinks actuals ({ Domain.access_tree; } as astate) proc_data callee_site = + let add_sinks sinks actuals access_tree proc_data callee_site = (* add [sink] to the trace associated with the [formal_index]th actual *) let add_sink_to_actual access_tree_acc (sink_param : TraceDomain.Sink.parameter) = match List.nth_exn actuals sink_param.index with @@ -226,17 +177,15 @@ module Make (TaintSpecification : TaintSpec.S) = struct end | _ -> access_tree_acc in - let access_tree' = List.fold ~f:add_sink_to_actual ~init:access_tree sinks in - { astate with Domain.access_tree = access_tree'; } + List.fold ~f:add_sink_to_actual ~init:access_tree sinks let apply_summary ret_opt (actuals : HilExp.t list) summary - (astate_in : Domain.astate) + caller_access_tree (proc_data : FormalMap.t ProcData.t) callee_site = - let caller_access_tree = astate_in.access_tree in let get_caller_ap formal_ap = let apply_return ret_ap = match ret_opt with @@ -309,173 +258,148 @@ module Make (TaintSpecification : TaintSpec.S) = struct ignore (instantiate_and_report callee_trace TraceDomain.empty access_tree_acc); access_tree_acc in - let access_tree = - TaintDomain.trace_fold - add_to_caller_tree - (TaintSpecification.of_summary_access_tree summary) - caller_access_tree in - { astate_in with access_tree; } - - let exec_hil_instr (astate : Domain.astate) (proc_data : FormalMap.t ProcData.t) instr = - let exec_instr_ (instr : HilInstr.t) = match instr with - | Write (((Var.ProgramVar pvar, _), []), HilExp.Exception _, _) when Pvar.is_return pvar -> - (* the Java frontend translates `throw Exception` as `return Exception`, which is a bit + TaintDomain.trace_fold + add_to_caller_tree + (TaintSpecification.of_summary_access_tree summary) + caller_access_tree + + let exec_instr + (astate : Domain.astate) (proc_data : FormalMap.t ProcData.t) _ (instr : HilInstr.t) = + match instr with + | Write (((Var.ProgramVar pvar, _), []), HilExp.Exception _, _) when Pvar.is_return pvar -> + (* the Java frontend translates `throw Exception` as `return Exception`, which is a bit wonky. this translation causes problems for us in computing a summary when an exception is "returned" from a void function. skip code like this for now, fix via t14159157 later *) - astate - - | Write (((Var.ProgramVar pvar, _), []), rhs_exp, _) - when Pvar.is_return pvar && HilExp.is_null_literal rhs_exp && - Typ.equal_desc Tvoid (Procdesc.get_ret_type proc_data.pdesc).desc -> - (* similar to the case above; the Java frontend translates "return no exception" as - `return null` in a void function *) - astate - - | Write (lhs_access_path, rhs_exp, _) -> - let access_tree = - let rhs_node = - Option.value - (hil_exp_get_node rhs_exp astate.access_tree proc_data) - ~default:TaintDomain.empty_node in - TaintDomain.add_node (AccessPath.Exact lhs_access_path) rhs_node astate.access_tree in - { astate with access_tree; } - - | Call (ret_opt, Direct called_pname, actuals, call_flags, callee_loc) -> - let handle_unknown_call callee_pname access_tree = - let is_variadic = match callee_pname with - | Typ.Procname.Java pname -> - begin - match List.rev (Typ.Procname.java_get_parameters pname) with - | (_, "java.lang.Object[]") :: _ -> true - | _ -> false - end - | _ -> false in - let should_taint_typ typ = is_variadic || TaintSpecification.is_taintable_type typ in - let exp_join_traces trace_acc exp = - match hil_exp_get_node ~abstracted:true exp access_tree proc_data with - | Some (trace, _) -> TraceDomain.join trace trace_acc - | None -> trace_acc in - let propagate_to_access_path access_path actuals access_tree = - let initial_trace = - access_path_get_trace access_path access_tree proc_data in - let trace_with_propagation = - List.fold ~f:exp_join_traces ~init:initial_trace actuals in - let filtered_sources = - TraceDomain.Sources.filter (fun source -> - match TraceDomain.Source.get_footprint_access_path source with - | Some access_path -> - Option.exists - (AccessPath.Raw.get_typ (AccessPath.extract access_path) proc_data.tenv) - ~f:should_taint_typ - | None -> - true) - (TraceDomain.sources trace_with_propagation) in - if TraceDomain.Sources.is_empty filtered_sources - then - access_tree - else - let trace' = TraceDomain.update_sources trace_with_propagation filtered_sources in - TaintDomain.add_trace access_path trace' access_tree in - let handle_unknown_call_ astate_acc propagation = - match propagation, actuals, ret_opt with - | _, [], _ -> - astate_acc - | TaintSpec.Propagate_to_return, actuals, Some ret_ap -> - propagate_to_access_path (AccessPath.Exact (ret_ap, [])) actuals astate_acc - | TaintSpec.Propagate_to_receiver, - AccessPath receiver_ap :: (_ :: _ as other_actuals), - _ -> - propagate_to_access_path (AccessPath.Exact receiver_ap) other_actuals astate_acc - | _ -> - astate_acc in - - let propagations = - TaintSpecification.handle_unknown_call - callee_pname - (Option.map ~f:snd ret_opt) - actuals - proc_data.tenv in - List.fold ~f:handle_unknown_call_ ~init:access_tree propagations in - - let analyze_call astate_acc callee_pname = - let call_site = CallSite.make callee_pname callee_loc in - - let sinks = TraceDomain.Sink.get call_site actuals proc_data.ProcData.tenv in - let astate_with_sink = match sinks with - | [] -> astate - | sinks -> add_sinks sinks actuals astate proc_data call_site in - - let source = TraceDomain.Source.get call_site proc_data.tenv in - let astate_with_source = - match source, ret_opt with - | Some source, Some ret_exp -> - let access_tree = add_source source ret_exp astate_with_sink.access_tree in - { astate_with_sink with access_tree; } - | Some _, None -> - L.err - "Warning: %a is marked as a source, but has no return value" - Typ.Procname.pp callee_pname; - astate_with_sink - | None, _ -> - astate_with_sink in - - let astate_with_summary = - if sinks <> [] || Option.is_some source - then - (* don't use a summary for a procedure that is a direct source or sink *) - astate_with_source - else - match Summary.read_summary proc_data.pdesc callee_pname with - | Some summary -> - apply_summary ret_opt actuals summary astate_with_source proc_data call_site - | None -> - let access_tree = - handle_unknown_call callee_pname astate_with_source.access_tree in - { astate with access_tree; } in - Domain.join astate_acc astate_with_summary in - - (* highly polymorphic call sites stress reactive mode too much by using too much memory. - here, we choose an arbitrary call limit that allows us to finish the analysis in - practice. this is obviously unsound; will try to remove in the future. *) - let max_calls = 3 in - let targets = - if List.length call_flags.cf_targets <= max_calls + astate + + | Write (((Var.ProgramVar pvar, _), []), rhs_exp, _) + when Pvar.is_return pvar && HilExp.is_null_literal rhs_exp && + Typ.equal_desc Tvoid (Procdesc.get_ret_type proc_data.pdesc).desc -> + (* similar to the case above; the Java frontend translates "return no exception" as + `return null` in a void function *) + astate + + | Write (lhs_access_path, rhs_exp, _) -> + let rhs_node = + Option.value + (hil_exp_get_node rhs_exp astate proc_data) + ~default:TaintDomain.empty_node in + TaintDomain.add_node (AccessPath.Exact lhs_access_path) rhs_node astate + + | Call (ret_opt, Direct called_pname, actuals, call_flags, callee_loc) -> + let handle_unknown_call callee_pname access_tree = + let is_variadic = match callee_pname with + | Typ.Procname.Java pname -> + begin + match List.rev (Typ.Procname.java_get_parameters pname) with + | (_, "java.lang.Object[]") :: _ -> true + | _ -> false + end + | _ -> false in + let should_taint_typ typ = is_variadic || TaintSpecification.is_taintable_type typ in + let exp_join_traces trace_acc exp = + match hil_exp_get_node ~abstracted:true exp access_tree proc_data with + | Some (trace, _) -> TraceDomain.join trace trace_acc + | None -> trace_acc in + let propagate_to_access_path access_path actuals access_tree = + let initial_trace = + access_path_get_trace access_path access_tree proc_data in + let trace_with_propagation = + List.fold ~f:exp_join_traces ~init:initial_trace actuals in + let filtered_sources = + TraceDomain.Sources.filter (fun source -> + match TraceDomain.Source.get_footprint_access_path source with + | Some access_path -> + Option.exists + (AccessPath.Raw.get_typ (AccessPath.extract access_path) proc_data.tenv) + ~f:should_taint_typ + | None -> + true) + (TraceDomain.sources trace_with_propagation) in + if TraceDomain.Sources.is_empty filtered_sources then - called_pname :: call_flags.cf_targets + access_tree else - begin - L.out - "Skipping highly polymorphic call site for %a@." Typ.Procname.pp called_pname; - [called_pname] - end in - (* for each possible target of the call, apply the summary. join all results together *) - List.fold ~f:analyze_call ~init:Domain.empty targets - | _ -> - astate in - - let f_resolve_id id = - try Some (IdAccessPathMapDomain.find id astate.id_map) - with Not_found -> None in - match HilInstr.of_sil ~f_resolve_id instr with - | Bind (id, access_path) -> - let id_map = IdAccessPathMapDomain.add id access_path astate.id_map in - { astate with id_map; } - | Unbind ids -> - let id_map = - List.fold - ~f:(fun acc id -> IdAccessPathMapDomain.remove id acc) ~init:astate.id_map ids in - { astate with id_map; } - | Instr hil_instr -> - exec_instr_ hil_instr - | Ignore -> + let trace' = TraceDomain.update_sources trace_with_propagation filtered_sources in + TaintDomain.add_trace access_path trace' access_tree in + let handle_unknown_call_ astate_acc propagation = + match propagation, actuals, ret_opt with + | _, [], _ -> + astate_acc + | TaintSpec.Propagate_to_return, actuals, Some ret_ap -> + propagate_to_access_path (AccessPath.Exact (ret_ap, [])) actuals astate_acc + | TaintSpec.Propagate_to_receiver, + AccessPath receiver_ap :: (_ :: _ as other_actuals), + _ -> + propagate_to_access_path (AccessPath.Exact receiver_ap) other_actuals astate_acc + | _ -> + astate_acc in + + let propagations = + TaintSpecification.handle_unknown_call + callee_pname + (Option.map ~f:snd ret_opt) + actuals + proc_data.tenv in + List.fold ~f:handle_unknown_call_ ~init:access_tree propagations in + + let analyze_call astate_acc callee_pname = + let call_site = CallSite.make callee_pname callee_loc in + + let sinks = TraceDomain.Sink.get call_site actuals proc_data.ProcData.tenv in + let astate_with_sink = match sinks with + | [] -> astate + | sinks -> add_sinks sinks actuals astate proc_data call_site in + + let source = TraceDomain.Source.get call_site proc_data.tenv in + let astate_with_source = + match source, ret_opt with + | Some source, Some ret_exp -> + add_source source ret_exp astate_with_sink + | Some _, None -> + L.err + "Warning: %a is marked as a source, but has no return value" + Typ.Procname.pp callee_pname; + astate_with_sink + | None, _ -> + astate_with_sink in + + let astate_with_summary = + if sinks <> [] || Option.is_some source + then + (* don't use a summary for a procedure that is a direct source or sink *) + astate_with_source + else + match Summary.read_summary proc_data.pdesc callee_pname with + | Some summary -> + apply_summary ret_opt actuals summary astate_with_source proc_data call_site + | None -> + handle_unknown_call callee_pname astate_with_source in + Domain.join astate_acc astate_with_summary in + + (* highly polymorphic call sites stress reactive mode too much by using too much memory. + here, we choose an arbitrary call limit that allows us to finish the analysis in + practice. this is obviously unsound; will try to remove in the future. *) + let max_calls = 3 in + let targets = + if List.length call_flags.cf_targets <= max_calls + then + called_pname :: call_flags.cf_targets + else + begin + L.out + "Skipping highly polymorphic call site for %a@." Typ.Procname.pp called_pname; + [called_pname] + end in + (* for each possible target of the call, apply the summary. join all results together *) + List.fold ~f:analyze_call ~init:Domain.empty targets + | _ -> astate - - let exec_instr (astate : Domain.astate) (proc_data : FormalMap.t ProcData.t) _ instr = - exec_hil_instr astate proc_data instr end - module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) + module Analyzer = + AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.Make(TransferFunctions)) let make_summary formal_map access_tree = (* if a trace has footprint sources, attach them to the appropriate footprint var *) @@ -565,9 +489,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct acc) ~init:TaintDomain.empty (TraceDomain.Source.get_tainted_formals pdesc tenv) in - if TaintDomain.BaseMap.is_empty access_tree - then Domain.empty - else { Domain.empty with Domain.access_tree; } in + access_tree, IdAccessPathMapDomain.empty in let compute_post (proc_data : FormalMap.t ProcData.t) = if not (Procdesc.did_preanalysis proc_data.pdesc) @@ -578,7 +500,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct end; let initial = make_initial proc_data.pdesc in match Analyzer.compute_post proc_data ~initial with - | Some { access_tree; } -> + | Some (access_tree, _) -> Some (make_summary proc_data.extras access_tree) | None -> if Procdesc.Node.get_succs (Procdesc.get_start_node proc_data.pdesc) <> [] diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 4da7d3eca..61590fd76 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -49,7 +49,8 @@ module MockTaintAnalysis = TaintAnalysis.Make(struct let is_taintable_type _ = true end) -module TestInterpreter = AnalyzerTester.Make (ProcCfg.Normal) (MockTaintAnalysis.TransferFunctions) +module TestInterpreter = + AnalyzerTester.Make (ProcCfg.Normal) (LowerHil.Make (MockTaintAnalysis.TransferFunctions)) let tests = let open OUnit2 in @@ -89,7 +90,7 @@ let tests = if not (MockTrace.is_empty t) then (ap, t) :: acc else acc) - astate.MockTaintAnalysis.Domain.access_tree + (fst astate) [] in PrettyPrintable.pp_collection ~pp_item fmt (List.rev trace_assocs) in let assign_to_source ret_str = @@ -225,5 +226,5 @@ let tests = ] |> TestInterpreter.create_tests ~pp_opt:pp_sparse FormalMap.empty - ~initial:MockTaintAnalysis.Domain.empty in + ~initial:(MockTaintAnalysis.Domain.empty, IdAccessPathMapDomain.empty) in "taint_test_suite">:::test_list diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 95bc2cfbb..55d439a6e 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -158,7 +158,8 @@ module StructuredSil = struct call_unknown None arg_strs end -module Make (CFG : ProcCfg.S with type node = Procdesc.Node.t) (T : TransferFunctions.Make) = struct +module Make + (CFG : ProcCfg.S with type node = Procdesc.Node.t) (T : TransferFunctions.MakeSIL) = struct open StructuredSil