[backend] Introduce type substitution to expressions and instructions

Summary: This will allow to replace type vars into concrete types in expressions.

Reviewed By: jvillard, mbouaziz

Differential Revision: D5209276

fbshipit-source-id: c1650f8

infer/src/IR/Sil.re

@@ -1653,7 +1653,9 @@ let equal_ident_exp = [%compare.equal : ident_exp];
 
 type exp_subst = list ident_exp [@@deriving compare];
 
-type subst = [ | `Exp exp_subst] [@@deriving compare];
+type subst = [ | `Exp exp_subst | `Typ Typ.type_subst_t] [@@deriving compare];
+
+type subst_fun = [ | `Exp (Ident.t => Exp.t) | `Typ (Typ.t => Typ.t, Typ.Name.t => Typ.Name.t)];
 
 
 /** Equality for substitutions. */
@@ -1708,7 +1710,8 @@ let sub_empty = `Exp exp_sub_empty;
 let is_sub_empty =
   fun
   | `Exp [] => true
-  | `Exp _ => false;
+  | `Exp _ => false
+  | `Typ sub => Typ.is_type_subst_empty sub;
 
 
 /** Join two substitutions into one.
@@ -1825,12 +1828,26 @@ let sub_fav_add fav (sub: exp_subst) =>
 /** Substitutions do not contain binders */
 let sub_av_add = sub_fav_add;
 
-let rec exp_sub_ids (f: Ident.t => Exp.t) exp =>
+let rec exp_sub_ids (f: subst_fun) exp => {
+  let f_typ x =>
+    switch f {
+    | `Exp _ => x
+    | `Typ (f, _) => f x
+    };
+  let f_tname x =>
+    switch f {
+    | `Exp _ => x
+    | `Typ (_, f) => f x
+    };
   switch (exp: Exp.t) {
   | Var id =>
-    switch (f id) {
+    switch f {
-    | Var id' when Ident.equal id id' => exp
+    | `Exp f_exp =>
-    | exp' => exp'
+      switch (f_exp id) {
+      | Exp.Var id' when Ident.equal id id' => /* it will preserve physical equality when needed */ exp
+      | exp' => exp'
+      }
+    | _ => exp
     }
   | Lvar _ => exp
   | Exn e =>
@@ -1846,10 +1863,11 @@ let rec exp_sub_ids (f: Ident.t => Exp.t) exp =>
         (
           fun ((e, pvar, typ) as captured) => {
             let e' = exp_sub_ids f e;
-            if (phys_equal e' e) {
+            let typ' = f_typ typ;
+            if (phys_equal e' e && phys_equal typ typ') {
               captured
             } else {
-              (e', pvar, typ)
+              (e', pvar, typ')
             }
           }
         )
@@ -1862,17 +1880,29 @@ let rec exp_sub_ids (f: Ident.t => Exp.t) exp =>
   | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _) => exp
   | Cast t e =>
     let e' = exp_sub_ids f e;
-    if (phys_equal e' e) {
+    let t' = f_typ t;
+    if (phys_equal e' e && phys_equal t' t) {
       exp
     } else {
-      Exp.Cast t e'
+      Exp.Cast t' e'
     }
   | UnOp op e typ_opt =>
     let e' = exp_sub_ids f e;
-    if (phys_equal e' e) {
+    let typ_opt' =
+      switch typ_opt {
+      | Some t =>
+        let t' = f_typ t;
+        if (phys_equal t t') {
+          typ_opt
+        } else {
+          Some t'
+        }
+      | None => typ_opt
+      };
+    if (phys_equal e' e && phys_equal typ_opt typ_opt') {
       exp
     } else {
-      Exp.UnOp op e' typ_opt
+      Exp.UnOp op e' typ_opt'
     }
   | BinOp op e1 e2 =>
     let e1' = exp_sub_ids f e1;
@@ -1884,10 +1914,12 @@ let rec exp_sub_ids (f: Ident.t => Exp.t) exp =>
     }
   | Lfield e fld typ =>
     let e' = exp_sub_ids f e;
-    if (phys_equal e' e) {
+    let typ' = f_typ typ;
+    let fld' = Typ.Fieldname.class_name_replace f::f_tname fld;
+    if (phys_equal e' e && phys_equal typ typ' && phys_equal fld fld') {
       exp
     } else {
-      Exp.Lfield e' fld typ
+      Exp.Lfield e' fld' typ'
     }
   | Lindex e1 e2 =>
     let e1' = exp_sub_ids f e1;
@@ -1897,37 +1929,54 @@ let rec exp_sub_ids (f: Ident.t => Exp.t) exp =>
     } else {
       Exp.Lindex e1' e2'
     }
-  | Sizeof ({dynamic_length: Some l} as sizeof_data) =>
+  | Sizeof ({typ, dynamic_length: Some l, subtype} as sizeof_data) =>
     let l' = exp_sub_ids f l;
-    if (phys_equal l' l) {
+    let typ' = f_typ typ;
+    let subtype' = Subtype.sub_type f_tname subtype;
+    if (phys_equal l' l && phys_equal typ typ' && phys_equal subtype subtype') {
       exp
     } else {
-      Exp.Sizeof {...sizeof_data, dynamic_length: Some l'}
+      Exp.Sizeof {...sizeof_data, typ: typ', dynamic_length: Some l', subtype: subtype'}
     }
-  | Sizeof {dynamic_length: None} => exp
+  | Sizeof ({typ, dynamic_length: None, subtype} as sizeof_data) =>
-  };
+    let typ' = f_typ typ;
-
+    let subtype' = Subtype.sub_type f_tname subtype;
-let rec apply_sub subst id =>
+    if (phys_equal typ typ') {
-  switch subst {
+      exp
-  | `Exp [] => Exp.Var id
-  | `Exp [(i, e), ...l] =>
-    if (Ident.equal i id) {
-      e
     } else {
-      apply_sub (`Exp l) id
+      Exp.Sizeof {...sizeof_data, typ: typ', subtype: subtype'}
     }
+  }
+};
+
+let apply_sub subst :subst_fun =>
+  switch subst {
+  | `Exp l =>
+    `Exp (
+      fun id =>
+        switch (List.Assoc.find l equal::Ident.equal id) {
+        | Some x => x
+        | None => Exp.Var id
+        }
+    )
+  | `Typ typ_subst => `Typ (Typ.sub_type typ_subst, Typ.sub_tname typ_subst)
   };
 
 let exp_sub (subst: subst) e => exp_sub_ids (apply_sub subst) e;
 
 
 /** apply [f] to id's in [instr]. if [sub_id_binders] is false, [f] is only applied to bound id's */
-let instr_sub_ids ::sub_id_binders (f: Ident.t => Exp.t) instr => {
+let instr_sub_ids ::sub_id_binders f instr => {
   let sub_id id =>
     switch (exp_sub_ids f (Var id)) {
     | Var id' when not (Ident.equal id id') => id'
     | _ => id
     };
+  let sub_typ x =>
+    switch f {
+    | `Exp _ => x
+    | `Typ (f, _) => f x
+    };
   switch instr {
   | Load id rhs_exp typ loc =>
     let id' =
@@ -1937,18 +1986,20 @@ let instr_sub_ids ::sub_id_binders (f: Ident.t => Exp.t) instr => {
         id
       };
     let rhs_exp' = exp_sub_ids f rhs_exp;
-    if (phys_equal id' id && phys_equal rhs_exp' rhs_exp) {
+    let typ' = sub_typ typ;
+    if (phys_equal id' id && phys_equal rhs_exp' rhs_exp && phys_equal typ typ') {
       instr
     } else {
-      Load id' rhs_exp' typ loc
+      Load id' rhs_exp' typ' loc
     }
   | Store lhs_exp typ rhs_exp loc =>
     let lhs_exp' = exp_sub_ids f lhs_exp;
+    let typ' = sub_typ typ;
     let rhs_exp' = exp_sub_ids f rhs_exp;
-    if (phys_equal lhs_exp' lhs_exp && phys_equal rhs_exp' rhs_exp) {
+    if (phys_equal lhs_exp' lhs_exp && phys_equal typ typ' && phys_equal rhs_exp' rhs_exp) {
       instr
     } else {
-      Store lhs_exp' typ rhs_exp' loc
+      Store lhs_exp' typ' rhs_exp' loc
     }
   | Call ret_id fun_exp actuals call_flags loc =>
     let ret_id' =
@@ -1956,7 +2007,12 @@ let instr_sub_ids ::sub_id_binders (f: Ident.t => Exp.t) instr => {
         switch ret_id {
         | Some (id, typ) =>
           let id' = sub_id id;
-          Ident.equal id id' ? ret_id : Some (id', typ)
+          let typ' = sub_typ typ;
+          if (Ident.equal id id' && phys_equal typ typ') {
+            ret_id
+          } else {
+            Some (id', typ')
+          }
         | None => None
         }
       } else {
@@ -1968,10 +2024,11 @@ let instr_sub_ids ::sub_id_binders (f: Ident.t => Exp.t) instr => {
         (
           fun ((actual, typ) as actual_pair) => {
             let actual' = exp_sub_ids f actual;
-            if (phys_equal actual' actual) {
+            let typ' = sub_typ typ;
+            if (phys_equal actual' actual && phys_equal typ typ') {
               actual_pair
             } else {
-              (actual', typ)
+              (actual', typ')
             }
           }
         )
@@ -1995,9 +2052,27 @@ let instr_sub_ids ::sub_id_binders (f: Ident.t => Exp.t) instr => {
     } else {
       Remove_temps ids' loc
     }
+  | Declare_locals locals loc =>
+    let locals' =
+      IList.map_changed
+        (
+          fun ((name, typ) as local_var) => {
+            let typ' = sub_typ typ;
+            if (phys_equal typ typ') {
+              local_var
+            } else {
+              (name, typ')
+            }
+          }
+        )
+        locals;
+    if (phys_equal locals locals') {
+      instr
+    } else {
+      Declare_locals locals' loc
+    }
   | Nullify _
-  | Abstract _
+  | Abstract _ => instr
-  | Declare_locals _ => instr
   }
 };
 

infer/src/IR/Sil.rei

@@ -670,7 +670,9 @@ let hpara_av_add: fav => hpara => unit;
 /** {2 Substitution} */
 type exp_subst [@@deriving compare];
 
-type subst = [ | `Exp exp_subst] [@@deriving compare];
+type subst = [ | `Exp exp_subst | `Typ Typ.type_subst_t] [@@deriving compare];
+
+type subst_fun = [ | `Exp (Ident.t => Exp.t) | `Typ (Typ.t => Typ.t, Typ.Name.t => Typ.Name.t)];
 
 
 /** Equality for substitutions. */
@@ -790,11 +792,9 @@ let instr_sub: subst => instr => instr;
 
 let hpred_sub: subst => hpred => hpred;
 
-let exp_sub_ids: (Ident.t => Exp.t) => Exp.t => Exp.t;
-
 
 /** apply [f] to id's in [instr]. if [sub_id_binders] is false, [f] is only applied to bound id's */
-let instr_sub_ids: sub_id_binders::bool => (Ident.t => Exp.t) => instr => instr;
+let instr_sub_ids: sub_id_binders::bool => subst_fun => instr => instr;
 
 
 /** {2 Functions for replacing occurrences of expressions.} */

infer/src/IR/Subtype.re

@@ -49,6 +49,20 @@ type result =
 
 let equal_result = [%compare.equal : result];
 
+let sub_type tname_subst st_pair => {
+  let (st, kind) = st_pair;
+  switch st {
+  | Subtypes tnames =>
+    let tnames' = IList.map_changed tname_subst tnames;
+    if (phys_equal tnames tnames') {
+      st_pair
+    } else {
+      (Subtypes tnames', kind)
+    }
+  | Exact => st_pair
+  }
+};
+
 let max_result res1 res2 =>
   if (compare_result res1 res2 <= 0) {
     res2

infer/src/IR/Subtype.rei

@@ -19,6 +19,8 @@ type t [@@deriving compare];
 
 let pp: F.formatter => t => unit;
 
+let sub_type: (Typ.Name.t => Typ.Name.t) => t => t;
+
 let exact: t; /** denotes the current type only */
 
 let subtypes: t; /** denotes the current type and any subtypes */

infer/src/IR/Typ.re

@@ -167,6 +167,12 @@ let mk ::default=? ::quals=? desc :t => {
   mk_aux ::?default ::?quals desc
 };
 
+let merge_quals quals1 quals2 => {
+  is_const: quals1.is_const || quals2.is_const,
+  is_restrict: quals1.is_restrict || quals2.is_restrict,
+  is_volatile: quals1.is_volatile || quals2.is_volatile
+};
+
 let escape pe =>
   if (Pp.equal_print_kind pe.Pp.kind Pp.HTML) {
     Escape.escape_xml
@@ -245,6 +251,67 @@ let to_string typ => {
   F.asprintf "%t" pp
 };
 
+type type_subst_t = list (string, t) [@@deriving compare];
+
+let is_type_subst_empty = List.is_empty;
+
+
+/** Given the template type mapping and the type, substitute tvars within the type. */
+let rec sub_type subst generic_typ :t =>
+  switch generic_typ.desc {
+  | TVar tname =>
+    switch (List.Assoc.find subst equal::String.equal tname) {
+    | Some t =>
+      /* Type qualifiers may come from original type or be part of substitution. Merge them */
+      mk quals::(merge_quals t.quals generic_typ.quals) t.desc
+    | None => generic_typ
+    }
+  | Tarray typ arg1 arg2 =>
+    let typ' = sub_type subst typ;
+    if (phys_equal typ typ') {
+      generic_typ
+    } else {
+      mk default::generic_typ (Tarray typ' arg1 arg2)
+    }
+  | Tptr typ arg =>
+    let typ' = sub_type subst typ;
+    if (phys_equal typ typ') {
+      generic_typ
+    } else {
+      mk default::generic_typ (Tptr typ' arg)
+    }
+  | Tstruct tname =>
+    let tname' = sub_tname subst tname;
+    if (phys_equal tname tname') {
+      generic_typ
+    } else {
+      mk default::generic_typ (Tstruct tname')
+    }
+  | _ => generic_typ
+  }
+and sub_tname subst tname =>
+  switch tname {
+  | CppClass name (Template spec_info) =>
+    let sub_typ_opt typ_opt =>
+      switch typ_opt {
+      | Some typ =>
+        let typ' = sub_type subst typ;
+        if (phys_equal typ typ') {
+          typ_opt
+        } else {
+          Some typ'
+        }
+      | None => typ_opt
+      };
+    let spec_info' = IList.map_changed sub_typ_opt spec_info;
+    if (phys_equal spec_info spec_info') {
+      tname
+    } else {
+      CppClass name (Template spec_info')
+    }
+  | _ => tname
+  };
+
 module Name = {
   type t = name [@@deriving compare];
   let equal = [%compare.equal : t];
@@ -1090,6 +1157,17 @@ module Fieldname = {
     | Java field_name
     | Clang {field_name} => Format.fprintf f "%s" field_name;
   let pp_latex style f fn => Latex.pp_string style f (to_string fn);
+  let class_name_replace fname ::f =>
+    switch fname {
+    | Clang {class_name, field_name} =>
+      let class_name' = f class_name;
+      if (phys_equal class_name class_name') {
+        fname
+      } else {
+        Clang {class_name: class_name', field_name}
+      }
+    | _ => fname
+    };
 
   /** Returns the class part of the fieldname */
   let java_get_class fn => {

infer/src/IR/Typ.rei

@@ -114,6 +114,10 @@ and template_spec_info =
 /** Create Typ.t from given desc. if [default] is passed then use its value to set other fields such as quals */
 let mk: default::t? => quals::type_quals? => desc => t;
 
+
+/** Stores information about type substitution */
+type type_subst_t [@@deriving compare];
+
 module Name: {
 
   /** Named types. */
@@ -186,6 +190,12 @@ let equal_desc: desc => desc => bool;
 
 let equal_quals: type_quals => type_quals => bool;
 
+let sub_type: type_subst_t => t => t;
+
+let sub_tname: type_subst_t => Name.t => Name.t;
+
+let is_type_subst_empty: type_subst_t => bool;
+
 
 /** Sets of types. */
 module Set: Caml.Set.S with type elt = t;
@@ -500,6 +510,7 @@ module Fieldname: {
   /** Convert a field name to a string. */
   let to_string: t => string;
   let to_full_string: t => string;
+  let class_name_replace: t => f::(Name.t => Name.t) => t;
 
   /** Convert a fieldname to a simplified string with at most one-level path. */
   let to_simplified_string: t => string;

infer/src/backend/preanal.ml

@@ -263,7 +263,8 @@ let do_copy_propagation pdesc tenv =
               begin
                 match CopyProp.extract_pre id copy_prop_inv_map with
                 | Some pre when not (CopyPropagation.Domain.is_empty pre) ->
-                    let instr' = Sil.instr_sub_ids ~sub_id_binders:false (id_sub pre) instr in
+                    let instr' =
+                      Sil.instr_sub_ids ~sub_id_binders:false (`Exp (id_sub pre)) instr in
                     instr' :: instrs, changed || not (phys_equal instr' instr)
                 | _ ->
                     instr :: instrs, changed

infer/src/backend/prop.ml

@@ -156,6 +156,8 @@ let pp_sub pe f = function
   | `Exp sub ->
       let pi_sub = List.map ~f:(fun (id, e) -> Sil.Aeq (Var id, e)) (Sil.sub_to_list sub) in
       (Pp.semicolon_seq_oneline pe (Sil.pp_atom pe)) f pi_sub
+  | `Typ _ ->
+      F.fprintf f "Printing typ_subst not implemented."
 
 (** Dump a substitution. *)
 let d_sub (sub: Sil.subst) = L.add_print_action (PTsub, Obj.repr sub)