[HIL] Fix ExitScope

Reviewed By: jvillard

Differential Revision: D13399373

fbshipit-source-id: 9fa20fb41

infer/src/IR/HilExp.ml

@@ -293,6 +293,39 @@ module AccessExpression = struct
   let of_pvar pvar typ = address_of (base (base_of_pvar pvar typ))
 
   let of_id id typ = base (base_of_id id typ)
+
+  let rec fold_vars ae ~init ~f =
+    match ae with
+    | Base (var, _typ) ->
+        f init var
+    | FieldOffset (ae, _) | AddressOf ae | Dereference ae ->
+        fold_vars ae ~init ~f
+    | ArrayOffset (ae, _typ, exp_opt) ->
+        let init = fold_vars ae ~init ~f in
+        fold_vars_exp_opt exp_opt ~init ~f
+
+
+  and fold_vars_exp_opt exp_opt ~init ~f =
+    Option.fold exp_opt ~init ~f:(fun init ae -> fold_vars_exp ae ~init ~f)
+
+
+  and fold_vars_exp exp ~init ~f =
+    match exp with
+    | AccessExpression ae ->
+        fold_vars ae ~init ~f
+    | UnaryOperator (_, exp, _) | Exception exp | Cast (_, exp) ->
+        fold_vars_exp exp ~init ~f
+    | BinaryOperator (_, exp1, exp2) ->
+        let init = fold_vars_exp exp1 ~init ~f in
+        fold_vars_exp exp2 ~init ~f
+    | Closure (_, capt) ->
+        List.fold capt ~init ~f:(fun init ((var, _typ), exp) ->
+            let init = f init var in
+            fold_vars_exp exp ~init ~f )
+    | Constant _ ->
+        init
+    | Sizeof (_, exp_opt) ->
+        fold_vars_exp_opt exp_opt ~init ~f
 end
 
 let rec get_typ tenv = function

infer/src/IR/HilExp.mli

@@ -80,6 +80,8 @@ module AccessExpression : sig
     | AddressOf of access_expression
     | Dereference of access_expression
   [@@deriving compare]
+
+  val fold_vars : (t, Var.t, 'accum) Container.fold
 end
 
 val pp : F.formatter -> t -> unit

infer/src/absint/AbstractDomain.ml

@@ -396,6 +396,44 @@ module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S
     inter prev next ~f:(fun prev next -> ValueDomain.widen ~prev ~next ~num_iters)
 end
 
+module FiniteMultiMap
+    (Key : PrettyPrintable.PrintableOrderedType)
+    (Value : PrettyPrintable.PrintableOrderedType) =
+struct
+  module S = FiniteSet (Value)
+  module M = Map (Key) (S)
+
+  type t = M.t
+
+  let empty = M.empty
+
+  let is_empty = M.is_empty
+
+  let ( <= ) = M.( <= )
+
+  let join = M.join
+
+  let widen = M.widen
+
+  let pp = M.pp
+
+  let add k v m =
+    M.update k (function None -> Some (S.singleton v) | Some s -> Some (S.add v s)) m
+
+
+  let mem k m = M.mem k m
+
+  let remove k v m =
+    M.update k
+      (function
+        | None ->
+            None
+        | Some s ->
+            let s' = S.remove v s in
+            if S.is_empty s' then None else Some s')
+      m
+end
+
 module BooleanAnd = struct
   type t = bool
 

infer/src/absint/AbstractDomain.mli

@@ -146,6 +146,18 @@ end
 module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) :
   InvertedMapS with type key = Key.t and type value = ValueDomain.t
 
+module FiniteMultiMap
+    (Key : PrettyPrintable.PrintableOrderedType)
+    (Value : PrettyPrintable.PrintableOrderedType) : sig
+  include WithBottom
+
+  val add : Key.t -> Value.t -> t -> t
+
+  val mem : Key.t -> t -> bool
+
+  val remove : Key.t -> Value.t -> t -> t
+end
+
 (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
 
 include

infer/src/absint/LowerHil.ml

@@ -15,24 +15,14 @@ module DefaultConfig : HilConfig = struct
   let include_array_indexes = false
 end
 
-let update_id_map hil_translation id_map =
-  match (hil_translation : HilInstr.translation) with
-  | Bind (id, access_path) ->
-      IdAccessPathMapDomain.add id access_path id_map
-  | Instr (ExitScope vars) ->
-      List.fold ~f:(fun acc var -> IdAccessPathMapDomain.remove var acc) ~init:id_map vars
-  | Instr _ | Ignore ->
-      id_map
-
-
 (** HIL adds a map from temporary variables to access paths to each domain *)
 module MakeHILDomain (Domain : AbstractDomain.S) = struct
-  include AbstractDomain.Pair (Domain) (IdAccessPathMapDomain)
+  include AbstractDomain.Pair (Domain) (Bindings)
 
   (** hides HIL implementation details *)
   let pp fmt (astate, id_map) =
     if Config.debug_level_analysis >= 3 then
-      Format.fprintf fmt "Id map: @[<h>%a@]@\n" IdAccessPathMapDomain.pp id_map ;
+      Format.fprintf fmt "Bindings: @[<h>%a@]@\n" Bindings.pp id_map ;
     Domain.pp fmt astate
 end
 
@@ -50,7 +40,7 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
     && match ConcurrencyModels.get_lock_effect pname actuals with Unlock _ -> true | _ -> false
 
 
-  let exec_instr_actual extras id_map node hil_instr actual_state =
+  let exec_instr_actual extras bindings node hil_instr actual_state =
     match (hil_instr : HilInstr.t) with
     | Call (_, Direct callee_pname, actuals, _, loc) as hil_instr
       when is_java_unlock callee_pname actuals ->
@@ -58,36 +48,52 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
            temporaries introduced in our translation of try/synchronized in Java. to ensure this,
            "dump" all of the temporaries out of the id map, then execute the unlock instruction. *)
         let actual_state' =
-          IdAccessPathMapDomain.fold
-            (fun id access_expr astate_acc ->
+          Bindings.fold bindings ~init:actual_state ~f:(fun id access_expr astate_acc ->
               let lhs_access_path = HilExp.AccessExpression.base (id, Typ.mk Typ.Tvoid) in
               let dummy_assign =
                 HilInstr.Assign (lhs_access_path, HilExp.AccessExpression access_expr, loc)
               in
               TransferFunctions.exec_instr astate_acc extras node dummy_assign )
-            id_map actual_state
         in
-        ( TransferFunctions.exec_instr actual_state' extras node hil_instr
-        , IdAccessPathMapDomain.empty )
+        (TransferFunctions.exec_instr actual_state' extras node hil_instr, Bindings.empty)
     | hil_instr ->
-        (TransferFunctions.exec_instr actual_state extras node hil_instr, id_map)
+        (TransferFunctions.exec_instr actual_state extras node hil_instr, bindings)
 
 
-  let exec_instr ((actual_state, id_map) as astate) extras node instr =
-    let f_resolve_id id = IdAccessPathMapDomain.find_opt id id_map in
+  let append_bindings = IList.append_no_duplicates ~cmp:Var.compare |> Staged.unstage
+
+  let hil_instr_of_sil bindings instr =
     let hil_translation =
+      let f_resolve_id = Bindings.resolve bindings in
       HilInstr.of_sil ~include_array_indexes:HilConfig.include_array_indexes ~f_resolve_id instr
     in
-    let actual_state', id_map' =
-      match hil_translation with
-      | Instr hil_instr ->
-          exec_instr_actual extras id_map node hil_instr actual_state
-      | Bind _ | Ignore ->
-          (actual_state, id_map)
+    match hil_translation with
+    | Ignore ->
+        (None, bindings)
+    | Bind (id, access_path) ->
+        (None, Bindings.add id access_path bindings)
+    | Instr (ExitScope vars) ->
+        let bindings, vars =
+          List.fold vars ~init:(bindings, []) ~f:(fun (bindings, vars) var ->
+              let bindings, vars' = Bindings.exit_scope var bindings in
+              (bindings, append_bindings vars vars') )
+        in
+        let instr = if List.is_empty vars then None else Some (HilInstr.ExitScope vars) in
+        (instr, bindings)
+    | Instr instr ->
+        (Some instr, bindings)
+
+
+  let exec_instr ((actual_state, bindings) as astate) extras node instr =
+    let actual_state', bindings' =
+      match hil_instr_of_sil bindings instr with
+      | None, bindings ->
+          (actual_state, bindings)
+      | Some hil_instr, bindings ->
+          exec_instr_actual extras bindings node hil_instr actual_state
     in
-    let id_map' = update_id_map hil_translation id_map' in
-    if phys_equal id_map id_map' && phys_equal actual_state actual_state' then astate
-    else (actual_state', id_map')
+    if phys_equal bindings bindings' && phys_equal actual_state actual_state' then astate
+    else (actual_state', bindings')
 end
 
 module type S = sig
@@ -106,22 +112,19 @@ module MakeAbstractInterpreterWithConfig
   S
   with type domain = TransferFunctions.Domain.t
    and module Interpreter = MakeAbstractInterpreter(Make(TransferFunctions)(HilConfig)) = struct
-  module Interpreter = MakeAbstractInterpreter (Make (TransferFunctions) (HilConfig))
+  module LowerHilInterpreter = Make (TransferFunctions) (HilConfig)
+  module Interpreter = MakeAbstractInterpreter (LowerHilInterpreter)
 
   type domain = TransferFunctions.Domain.t
 
   let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial =
     Preanal.do_preanalysis pdesc tenv ;
-    let initial' = (initial, IdAccessPathMapDomain.empty) in
-    let pp_instr (_, id_map) instr =
-      let f_resolve_id id = IdAccessPathMapDomain.find_opt id id_map in
-      let hil_translation =
-        HilInstr.of_sil ~include_array_indexes:HilConfig.include_array_indexes ~f_resolve_id instr
-      in
-      match hil_translation with
-      | Instr hil_instr ->
+    let initial' = (initial, Bindings.empty) in
+    let pp_instr (_, bindings) instr =
+      match LowerHilInterpreter.hil_instr_of_sil bindings instr with
+      | Some hil_instr, _ ->
           Some (fun f -> Format.fprintf f "@[<h>%a@];@;" HilInstr.pp hil_instr)
-      | Bind _ | Ignore ->
+      | None, _ ->
           None
     in
     Interpreter.compute_post ~pp_instr proc_data ~initial:initial' |> Option.map ~f:fst

infer/src/absint/LowerHil.mli

@@ -25,8 +25,7 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
      and module Node.IdMap = TransferFunctions.CFG.Node.IdMap
      and module Node.IdSet = TransferFunctions.CFG.Node.IdSet
 
-  module Domain :
-      module type of AbstractDomain.Pair (TransferFunctions.Domain) (IdAccessPathMapDomain)
+  module Domain : module type of AbstractDomain.Pair (TransferFunctions.Domain) (Bindings)
 
   type extras = TransferFunctions.extras
 

infer/src/checkers/Bindings.ml

@@ -0,0 +1,83 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+module F = Format
+module L = Logging
+module Dead = AbstractDomain.InvertedSet (Var)
+module Reverse = AbstractDomain.FiniteMultiMap (Var) (Var)
+
+type t =
+  { resolve: IdAccessPathMapDomain.t
+  ; reverse: Reverse.t
+        (** there is a [x -> y] mapping in reverse for each variable [y] appearing in [resolve x] *)
+  ; dead: Dead.t }
+
+let empty = {resolve= IdAccessPathMapDomain.empty; reverse= Reverse.empty; dead= Dead.empty}
+
+let add id ap {resolve; reverse; dead} =
+  let resolve = IdAccessPathMapDomain.add id ap resolve in
+  let reverse =
+    HilExp.AccessExpression.fold_vars ap ~init:reverse ~f:(fun acc var_in_ap ->
+        Reverse.add var_in_ap id acc )
+  in
+  let dead = Dead.remove id dead in
+  {resolve; reverse; dead}
+
+
+let exit_scope id bindings =
+  let {resolve; reverse; dead} = bindings in
+  match (Reverse.mem id reverse, IdAccessPathMapDomain.find_opt id resolve) with
+  | true, None ->
+      let dead = Dead.add id dead in
+      ({resolve; reverse; dead}, [])
+  | true, Some _ ->
+      L.(die InternalError) "Variable appearing on both sides of bindings"
+  | false, None ->
+      (bindings, [id])
+  | false, Some ap ->
+      let resolve = IdAccessPathMapDomain.remove id resolve in
+      let reverse, vars, dead =
+        HilExp.AccessExpression.fold_vars ap ~init:(reverse, [], dead)
+          ~f:(fun (reverse, vars, dead) var_in_ap ->
+            let reverse = Reverse.remove var_in_ap id reverse in
+            if (not (Reverse.mem var_in_ap reverse)) && Dead.mem var_in_ap dead then
+              (reverse, var_in_ap :: vars, Dead.remove var_in_ap dead)
+            else (reverse, vars, dead) )
+      in
+      ({resolve; reverse; dead}, vars)
+
+
+let resolve {resolve} id = IdAccessPathMapDomain.find_opt id resolve
+
+let fold {resolve} ~init ~f = IdAccessPathMapDomain.fold f resolve init
+
+let pp f {resolve; reverse; dead} =
+  F.fprintf f "{@[<v1> resolve=@[<hv>%a@];@;reverse=@[<hv>%a@];@;dead=@[<hv>%a@];@]}"
+    IdAccessPathMapDomain.pp resolve Reverse.pp reverse Dead.pp dead
+
+
+let ( <= ) ~lhs ~rhs = IdAccessPathMapDomain.( <= ) ~lhs:lhs.resolve ~rhs:rhs.resolve
+
+let join bindings1 bindings2 =
+  if phys_equal bindings1 bindings2 then bindings1
+  else
+    let {resolve= resolve1; reverse= reverse1; dead= dead1} = bindings1 in
+    let {resolve= resolve2; reverse= reverse2; dead= dead2} = bindings2 in
+    { resolve= IdAccessPathMapDomain.join resolve1 resolve2
+    ; reverse= Reverse.join reverse1 reverse2
+    ; dead= Dead.join dead1 dead2 }
+
+
+let widen ~prev ~next ~num_iters =
+  if phys_equal prev next then prev
+  else
+    let {resolve= resolve1; reverse= reverse1; dead= dead1} = prev in
+    let {resolve= resolve2; reverse= reverse2; dead= dead2} = next in
+    { resolve= IdAccessPathMapDomain.widen ~prev:resolve1 ~next:resolve2 ~num_iters
+    ; reverse= Reverse.widen ~prev:reverse1 ~next:reverse2 ~num_iters
+    ; dead= Dead.widen ~prev:dead1 ~next:dead2 ~num_iters }

infer/src/checkers/Bindings.mli

@@ -0,0 +1,21 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+include AbstractDomain.S
+
+val empty : t
+
+val add : Var.t -> HilExp.AccessExpression.t -> t -> t
+
+val exit_scope : Var.t -> t -> t * Var.t list
+(** returns the new bindings as well as a list of variables that became dead *)
+
+val resolve : t -> Var.t -> HilExp.AccessExpression.t option
+
+val fold : t -> init:'accum -> f:(Var.t -> HilExp.AccessExpression.t -> 'accum -> 'accum) -> 'accum

infer/src/unit/TaintTests.ml

@@ -157,6 +157,6 @@ let tests =
       , [assign_to_non_source "ret_id"; call_sink "ret_id"; assert_empty] ) ]
     |> TestInterpreter.create_tests ~pp_opt:pp_sparse
          {formal_map= FormalMap.empty; summary= Summary.dummy}
-         ~initial:(MockTaintAnalysis.Domain.empty, IdAccessPathMapDomain.empty)
+         ~initial:(MockTaintAnalysis.Domain.empty, Bindings.empty)
   in
   "taint_test_suite" >::: test_list