[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

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} =
+  let call_marker_start marker location {started_markers; ended_markers} =
-    { started_markers= MarkerSet.add marker started_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) =
+  let call_marker_start marker location ({context} as astate) =
-    {astate with context= Context.call_marker_start marker context}
+    {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 ->
+        (fun (config, _) {context= callee_context; trace= config_check_trace} acc ->
-          let context = Context.instantiate_callee ~callee_context ~caller_context in
+          let context =
-          ConfigChecks.weak_add config context location acc )
+            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