fixing handling of aliasing for frontend tmp vars

Reviewed By: cristianoc

Differential Revision: D3824558

fbshipit-source-id: 624df00

infer/src/checkers/IdAccessPathMapDomain.ml

@@ -10,11 +10,8 @@
 open! Utils
 
 (** mapping of ids to raw access paths. useful for id-normalizing access paths *)
-module IdMap = PrettyPrintable.MakePPMap(struct
-    type t = Ident.t
-    let compare = Ident.compare
-    let pp_key = (Ident.pp pe_text)
-  end)
+
+module IdMap = Var.Map
 
 type astate = AccessPath.raw IdMap.t
 

infer/src/checkers/accessPath.ml

@@ -79,16 +79,22 @@ let of_pvar pvar typ =
 let of_id id typ =
   base_of_id id typ, []
 
-let of_exp exp typ ~(f_resolve_id : Ident.t -> raw option) =
+let of_exp exp typ ~(f_resolve_id : Var.t -> raw option) =
   (* [typ] is the type of the last element of the access path (e.g., typeof(g) for x.f.g) *)
   let rec of_exp_ exp typ accesses =
     match exp with
     | Exp.Var id ->
         begin
-          match f_resolve_id id with
+          match f_resolve_id (Var.of_id id) with
           | Some (base, base_accesses) -> Some (base, base_accesses @ accesses)
           | None -> Some (base_of_id id typ, accesses)
         end
+    | Exp.Lvar pvar when Pvar.is_frontend_tmp pvar ->
+        begin
+          match f_resolve_id (Var.of_pvar pvar) with
+          | Some (base, base_accesses) -> Some (base, base_accesses @ accesses)
+          | None -> Some (base_of_pvar pvar typ, accesses)
+        end
     | Exp.Lvar pvar ->
         Some (base_of_pvar pvar typ, accesses)
     | Exp.Lfield (root_exp, fld, root_exp_typ) ->

infer/src/checkers/accessPath.mli

@@ -48,7 +48,7 @@ val of_pvar : Pvar.t -> Typ.t -> raw
 val of_id : Ident.t -> Typ.t -> raw
 
 (** convert [exp] to a raw access path, resolving identifiers using [f_resolve_id] *)
-val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Ident.t -> raw option) -> raw option
+val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> raw option) -> raw option
 
 (** append new accesses to an existing access path; e.g., `append_access x.f [g, h]` produces
     `x.f.g.h` *)

infer/src/quandary/TaintAnalysis.ml

@@ -151,7 +151,9 @@ module Make (TraceDomain : Trace.S) = struct
       let f_resolve_id = resolve_id id_map in
       match instr with
       | Sil.Load (lhs_id, rhs_exp, rhs_typ, _) ->
-          analyze_id_assignment lhs_id rhs_exp rhs_typ astate
+          analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ astate
+      | Sil.Store (Exp.Lvar lhs_pvar, lhs_typ, rhs_exp, _) when Pvar.is_frontend_tmp lhs_pvar ->
+          analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ astate
       | Sil.Store (lhs_exp, lhs_typ, rhs_exp, loc) ->
           let lhs_access_path =
             match AccessPath.of_exp lhs_exp lhs_typ ~f_resolve_id with
@@ -173,10 +175,10 @@ module Make (TraceDomain : Trace.S) = struct
             match rhs_exp with
             | Exp.Var rhs_id ->
                 let existing_accesses =
-                  try snd (IdMapDomain.find rhs_id astate'.Domain.id_map)
+                  try snd (IdMapDomain.find (Var.of_id rhs_id) astate'.Domain.id_map)
                   with Not_found -> [] in
                 let lhs_ap' = AccessPath.append lhs_access_path existing_accesses in
-                let id_map' = IdMapDomain.add rhs_id lhs_ap' astate'.Domain.id_map in
+                let id_map' = IdMapDomain.add (Var.of_id rhs_id) lhs_ap' astate'.Domain.id_map in
                 { astate' with Domain.id_map = id_map'; }
             | _ ->
                 astate'
@@ -187,7 +189,7 @@ module Make (TraceDomain : Trace.S) = struct
           then
             match args with
             | (cast_target, cast_typ) :: _ ->
-                analyze_id_assignment ret_id cast_target cast_typ astate
+                analyze_id_assignment (Var.of_id ret_id) cast_target cast_typ astate
             | _ ->
                 failwithf
                   "Unexpected cast %a in procedure %a at line %a"

infer/tests/codetoanalyze/java/quandary/Fields.java

@@ -51,6 +51,18 @@ public class Fields {
     InferTaint.inferSensitiveSink(src);
   }
 
+  void viaNestedFieldBad1(Obj obj) {
+    obj.g.f = InferTaint.inferSecretSource();
+    InferTaint.inferSensitiveSink(obj.g.f);
+  }
+
+  void viaNestedFieldBad2() {
+    Obj obj = new Obj();
+    obj.g = new Obj();
+    obj.g.f = InferTaint.inferSecretSource();
+    InferTaint.inferSensitiveSink(obj.g.f);
+  }
+
   /** should not report on these tests */
 
   void viaFieldOk1(Obj obj) {
@@ -109,20 +121,7 @@ public class Fields {
 
   /** an ideal analysis would report on these tests, but we currently do not */
 
-  // need to handle aliasing to get these examples
-  // in the first few cases, this is due to intermediate pvar's introduced by Infer's translation
-
-  void FN_viaNestedFieldBad1(Obj obj) {
-    obj.g.f = InferTaint.inferSecretSource();
-    InferTaint.inferSensitiveSink(obj.g.f);
-  }
-
-  void FN_viaNestedFieldBad2() {
-    Obj obj = new Obj();
-    obj.g = new Obj();
-    obj.g.f = InferTaint.inferSecretSource();
-    InferTaint.inferSensitiveSink(obj.g.f);
-  }
+  // need to soundly handle aliasing to get these examples
 
   void FN_aliasBad1() {
     Obj obj1 = new Obj();
@@ -131,7 +130,7 @@ public class Fields {
     InferTaint.inferSensitiveSink(obj1.f);
   }
 
-  void FN_AliasBad2(Obj obj) {
+  void FN_aliasBad2(Obj obj) {
     Obj x = obj.g;
     x.f = InferTaint.inferSecretSource();
     InferTaint.inferSensitiveSink(obj.g.f);

infer/tests/codetoanalyze/java/quandary/issues.exp

@@ -21,5 +21,7 @@ Fields.java:33: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.infer
 Fields.java:38: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 37]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 38]) via {  }
 Fields.java:44: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 43]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 44]) via {  }
 Fields.java:51: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 49]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 51]) via {  }
+Fields.java:56: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 55]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 56]) via {  }
+Fields.java:63: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 62]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 63]) via {  }
 LoggingPrivateData.java:18: ERROR: QUANDARY_TAINT_ERROR Error: SharedPreferences(String SharedPreferences.getString(String,String) at [line 18]) -> Logging(int Log.d(String,String) at [line 18]) via {  }
 LoggingPrivateData.java:22: ERROR: QUANDARY_TAINT_ERROR Error: SharedPreferences(String SharedPreferences.getString(String,String) at [line 22]) -> Logging(int Log.d(String,String) at [line 22]) via {  }