From 5fed80dd976b54a6cbc668497d157ae393816319 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 15 Jun 2020 12:29:04 -0700 Subject: [PATCH] [CCBM] Add trace info (2/3) Summary: This diff adds a prototype of a new checker that collects config checkings between markers. Basically, what the checker is doing is a taint analysis. * Taint source: function calls of "marker start" * Taint sink: function calls of config checking * Taint remove: function calls of "marker end" By the taint analysis, the analysis results will say that which taints can reach to the sink. In other words, which marker ID that has been started can reach to the config checks, before marker's ending. I am separating the diff into three steps: (1/3) Add basic abstract semantics (2/3) Add trace information (3/3) Add reporting with test examples Reviewed By: jvillard Differential Revision: D21998150 fbshipit-source-id: 337a8938a --- .../checkers/ConfigChecksBetweenMarkers.ml | 160 +++++++++++++++--- 1 file changed, 140 insertions(+), 20 deletions(-) diff --git a/infer/src/checkers/ConfigChecksBetweenMarkers.ml b/infer/src/checkers/ConfigChecksBetweenMarkers.ml index c3b2fe190..2e52fe36d 100644 --- a/infer/src/checkers/ConfigChecksBetweenMarkers.ml +++ b/infer/src/checkers/ConfigChecksBetweenMarkers.ml @@ -42,8 +42,63 @@ end module Mem = AbstractDomain.Map (Ident) (ConfigTopLifted) +module Trace = struct + type elem = MarkerStart of IntLit.t | ConfigCheck of ConfigName.t + + type t = + | Empty + | Elem of {kind: elem; location: Location.t; from: t} + | Call of {callee: Procname.t; location: Location.t; from: t; callee_trace: t} + + let pp_elem f = function + | MarkerStart i -> + F.fprintf f "MarkerStart(%a)" IntLit.pp i + | ConfigCheck config -> + F.fprintf f "ConfigCheck(%a)" ConfigName.pp config + + + let rec pp f = function + | Empty -> + F.pp_print_string f "Empty" + | Elem {kind; from} -> + F.fprintf f "Elem(%a,%a)" pp_elem kind pp from + | Call {callee; from; callee_trace} -> + F.fprintf f "Call(%a,%a,%a)" pp from Procname.pp callee pp callee_trace + + + (** [Trace] is additional information, thus which should not affect analysis operation *) + let leq ~lhs:_ ~rhs:_ = true + + let join x _y = x + + let widen ~prev ~next ~num_iters:_ = join prev next + + let marker_start marker = MarkerStart marker + + let config_check config = ConfigCheck config + + let add_elem kind location from = Elem {kind; location; from} + + let add_call callee location ~from ~callee_trace = Call {callee; location; from; callee_trace} + + let singleton kind location = add_elem kind location Empty +end + +module TraceWithNothing = struct + type t = {trace: Trace.t} + + let pp f {trace} = Trace.pp f trace + + let leq ~lhs ~rhs = Trace.leq ~lhs:lhs.trace ~rhs:rhs.trace + + let join x y = {trace= Trace.join x.trace y.trace} + + let widen ~prev ~next ~num_iters = + {trace= Trace.widen ~prev:prev.trace ~next:next.trace ~num_iters} +end + module MarkerSet = struct - include AbstractDomain.FiniteSet (IntLit) + include AbstractDomain.Map (IntLit) (TraceWithNothing) let pp f x = if is_empty x then F.pp_print_string f "{ }" @@ -51,11 +106,36 @@ module MarkerSet = struct F.fprintf f "@[{ " ; let is_first = ref true in iter - (fun marker -> + (fun marker _trace -> if !is_first then is_first := false else F.fprintf f ",@ " ; IntLit.pp f marker ) x ; F.fprintf f " }@]" ) + + + let add_trace new_trace location x = + map (fun {trace} -> {trace= Trace.add_elem new_trace location trace}) x + + + let join_on_call callee_pname ?config_check_trace location ~callee ~caller = + merge + (fun _marker callee_trace caller_trace -> + let add_call {TraceWithNothing.trace= callee_trace} = + let from = + Option.value_map caller_trace ~default:Trace.Empty ~f:(fun {TraceWithNothing.trace} -> + trace ) + in + let trace = Trace.add_call callee_pname location ~from ~callee_trace in + Some {TraceWithNothing.trace} + in + match (callee_trace, config_check_trace) with + | None, None -> + caller_trace + | None, Some config_check_trace -> + add_call {TraceWithNothing.trace= config_check_trace} + | Some callee_trace, _ -> + add_call callee_trace ) + callee caller end module InvMarkerSet = AbstractDomain.InvertedSet (IntLit) @@ -92,8 +172,10 @@ module Context = struct let init = {started_markers= MarkerSet.bottom; ended_markers= InvMarkerSet.top} - let call_marker_start marker {started_markers; ended_markers} = - { started_markers= MarkerSet.add marker started_markers + let call_marker_start marker location {started_markers; ended_markers} = + let trace = Trace.singleton (Trace.marker_start marker) location in + let trace_dom = {TraceWithNothing.trace} in + { started_markers= MarkerSet.add marker trace_dom started_markers ; ended_markers= InvMarkerSet.remove marker ended_markers } @@ -102,23 +184,47 @@ module Context = struct ; ended_markers= InvMarkerSet.add marker ended_markers } - let instantiate_callee ~callee_context ~caller_context = + let call_config_check new_trace location ({started_markers} as context) = + {context with started_markers= MarkerSet.add_trace new_trace location started_markers} + + + let instantiate_callee ~callee_pname ?config_check_trace location ~callee_context ~caller_context + = let started_markers = - MarkerSet.join callee_context.started_markers caller_context.started_markers + MarkerSet.join_on_call callee_pname ?config_check_trace location + ~callee:callee_context.started_markers ~caller:caller_context.started_markers |> InvMarkerSet.fold MarkerSet.remove callee_context.ended_markers in let ended_markers = InvMarkerSet.join caller_context.ended_markers callee_context.ended_markers - |> MarkerSet.fold InvMarkerSet.remove callee_context.started_markers + |> MarkerSet.fold + (fun marker _trace acc -> InvMarkerSet.remove marker acc) + callee_context.started_markers in {started_markers; ended_markers} end +module ContextWithTrace = struct + type t = {context: Context.t; trace: Trace.t} + + let pp f {context; trace= _} = Context.pp f context + + let leq ~lhs ~rhs = Context.leq ~lhs:lhs.context ~rhs:rhs.context + + let join x y = {context= Context.join x.context y.context; trace= Trace.join x.trace y.trace} + + let widen ~prev ~next ~num_iters = + { context= Context.widen ~prev:prev.context ~next:next.context ~num_iters + ; trace= Trace.widen ~prev:prev.trace ~next:next.trace ~num_iters } +end + module ConfigChecks = struct - include AbstractDomain.Map (ConfigWithLocation) (Context) + include AbstractDomain.Map (ConfigWithLocation) (ContextWithTrace) let weak_add k v location m = - update (k, location) (function None -> Some v | Some v' -> Some (Context.join v v')) m + update (k, location) + (function None -> Some v | Some v' -> Some (ContextWithTrace.join v v')) + m end module Summary = struct @@ -162,8 +268,8 @@ module Dom = struct {astate with mem= Mem.add id (NonTop {ConfigName.config_class; config_name}) mem} - let call_marker_start marker ({context} as astate) = - {astate with context= Context.call_marker_start marker context} + let call_marker_start marker location ({context} as astate) = + {astate with context= Context.call_marker_start marker location context} let call_marker_end marker ({context} as astate) = @@ -173,20 +279,34 @@ module Dom = struct let call_config_check id location ({mem; context; config_checks} as astate) = match Mem.find_opt id mem with | Some (NonTop config) -> - {astate with config_checks= ConfigChecks.weak_add config context location config_checks} + let trace_elem = Trace.config_check config in + let context = Context.call_config_check trace_elem location context in + let context_with_trace = + {ContextWithTrace.context; trace= Trace.singleton trace_elem location} + in + { astate with + config_checks= ConfigChecks.weak_add config context_with_trace location config_checks } | _ -> astate - let instantiate_callee + let instantiate_callee ~callee ~callee_summary:{Summary.context= callee_context; config_checks= callee_config_checks} location ({context= caller_context; config_checks= caller_config_checks} as astate) = - let context = Context.instantiate_callee ~callee_context ~caller_context in + let context = + Context.instantiate_callee ~callee_pname:callee location ~callee_context ~caller_context + in let config_checks = ConfigChecks.fold - (fun (config, _) callee_context acc -> - let context = Context.instantiate_callee ~callee_context ~caller_context in - ConfigChecks.weak_add config context location acc ) + (fun (config, _) {context= callee_context; trace= config_check_trace} acc -> + let context = + Context.instantiate_callee ~callee_pname:callee ~config_check_trace location + ~callee_context ~caller_context + in + let trace = + Trace.add_call callee location ~from:Trace.Empty ~callee_trace:config_check_trace + in + ConfigChecks.weak_add config {context; trace} location acc ) callee_config_checks caller_config_checks in {astate with context; config_checks} @@ -208,9 +328,9 @@ module TransferFunctions = struct | Load {id; e= Lfield (Lvar config_class, config_name, _)} when FbGKInteraction.is_config_class config_class -> Dom.load_config id ~config_class ~config_name astate - | Call (_, Const (Cfun callee), _ :: (Const (Cint marker), _) :: _, _, _) + | Call (_, Const (Cfun callee), _ :: (Const (Cint marker), _) :: _, location, _) when FbGKInteraction.is_marker_start tenv callee -> - Dom.call_marker_start marker astate + Dom.call_marker_start marker location astate | Call (_, Const (Cfun callee), _ :: (Const (Cint marker), _) :: _, _, _) when FbGKInteraction.is_marker_end tenv callee -> Dom.call_marker_end marker astate @@ -219,7 +339,7 @@ module TransferFunctions = struct Dom.call_config_check id location astate | Call (_, Const (Cfun callee), _, location, _) -> Option.value_map (get_summary callee) ~default:astate ~f:(fun callee_summary -> - Dom.instantiate_callee ~callee_summary location astate ) + Dom.instantiate_callee ~callee ~callee_summary location astate ) | _ -> astate