diff --git a/infer/src/IR/DecompiledExp.re b/infer/src/IR/DecompiledExp.re
new file mode 100644
index 000000000..d4e5ac4a9
--- /dev/null
+++ b/infer/src/IR/DecompiledExp.re
@@ -0,0 +1,179 @@
+/*
+ * vim: set ft=rust:
+ * vim: set ft=reason:
+ *
+ * Copyright (c) 2009 - 2013 Monoidics ltd.
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+open! Utils;
+
+
+/** The Smallfoot Intermediate Language: Decompiled Expressions */
+let module L = Logging;
+
+let module F = Format;
+
+
+/** expression representing the result of decompilation */
+type t =
+  | Darray of t t
+  | Dbinop of Binop.t t t
+  | Dconst of Const.t
+  | Dsizeof of Typ.t (option t) Subtype.t
+  | Dderef of t
+  | Dfcall of t (list t) Location.t CallFlags.t
+  | Darrow of t Ident.fieldname
+  | Ddot of t Ident.fieldname
+  | Dpvar of Pvar.t
+  | Dpvaraddr of Pvar.t
+  | Dunop of Unop.t t
+  | Dunknown
+  | Dretcall of t (list t) Location.t CallFlags.t;
+
+
+/** Value paths: identify an occurrence of a value in a symbolic heap
+    each expression represents a path, with Dpvar being the simplest one */
+type vpath = option t;
+
+let java () => !Config.curr_language == Config.Java;
+
+let eradicate_java () => Config.eradicate && java ();
+
+
+/** convert a dexp to a string */
+let rec to_string =
+  fun
+  | Darray de1 de2 => to_string de1 ^ "[" ^ to_string de2 ^ "]"
+  | Dbinop op de1 de2 => "(" ^ to_string de1 ^ Binop.str pe_text op ^ to_string de2 ^ ")"
+  | Dconst (Cfun pn) => Procname.to_simplified_string pn
+  | Dconst c => Const.to_string c
+  | Dderef de => "*" ^ to_string de
+  | Dfcall fun_dexp args _ {cf_virtual: isvirtual} => {
+      let pp_arg fmt de => F.fprintf fmt "%s" (to_string de);
+      let pp_args fmt des =>
+        if (eradicate_java ()) {
+          if (des != []) {
+            F.fprintf fmt "..."
+          }
+        } else {
+          pp_comma_seq pp_arg fmt des
+        };
+      let pp_fun fmt => (
+        fun
+        | Dconst (Cfun pname) => {
+            let s =
+              switch pname {
+              | Procname.Java pname_java => Procname.java_get_method pname_java
+              | _ => Procname.to_string pname
+              };
+            F.fprintf fmt "%s" s
+          }
+        | de => F.fprintf fmt "%s" (to_string de)
+      );
+      let (receiver, args') =
+        switch args {
+        | [Dpvar pv, ...args'] when isvirtual && Pvar.is_this pv => (None, args')
+        | [a, ...args'] when isvirtual => (Some a, args')
+        | _ => (None, args)
+        };
+      let pp fmt () => {
+        let pp_receiver fmt => (
+          fun
+          | None => ()
+          | Some arg => F.fprintf fmt "%a." pp_arg arg
+        );
+        F.fprintf fmt "%a%a(%a)" pp_receiver receiver pp_fun fun_dexp pp_args args'
+      };
+      pp_to_string pp ()
+    }
+  | Darrow (Dpvar pv) f when Pvar.is_this pv =>
+    /* this->fieldname */
+    Ident.fieldname_to_simplified_string f
+  | Darrow de f =>
+    if (Ident.fieldname_is_hidden f) {
+      to_string de
+    } else if (java ()) {
+      to_string de ^ "." ^ Ident.fieldname_to_flat_string f
+    } else {
+      to_string de ^ "->" ^ Ident.fieldname_to_string f
+    }
+  | Ddot (Dpvar _) fe when eradicate_java () =>
+    /* static field access */
+    Ident.fieldname_to_simplified_string fe
+  | Ddot de f =>
+    if (Ident.fieldname_is_hidden f) {
+      "&" ^ to_string de
+    } else if (java ()) {
+      to_string de ^ "." ^ Ident.fieldname_to_flat_string f
+    } else {
+      to_string de ^ "." ^ Ident.fieldname_to_string f
+    }
+  | Dpvar pv => Mangled.to_string (Pvar.get_name pv)
+  | Dpvaraddr pv => {
+      let s =
+        if (eradicate_java ()) {
+          Pvar.get_simplified_name pv
+        } else {
+          Mangled.to_string (Pvar.get_name pv)
+        };
+      let ampersand =
+        if (eradicate_java ()) {
+          ""
+        } else {
+          "&"
+        };
+      ampersand ^ s
+    }
+  | Dunop op de => Unop.str op ^ to_string de
+  | Dsizeof typ _ _ => pp_to_string (Typ.pp_full pe_text) typ
+  | Dunknown => "unknown"
+  | Dretcall de _ _ _ => "returned by " ^ to_string de;
+
+
+/** Pretty print a dexp. */
+let pp fmt de => F.fprintf fmt "%s" (to_string de);
+
+
+/** Pretty print a value path */
+let pp_vpath pe fmt vpath => {
+  let pp fmt =>
+    fun
+    | Some de => pp fmt de
+    | None => ();
+  if (pe.pe_kind === PP_HTML) {
+    F.fprintf
+      fmt
+      " %a{vpath: %a}%a"
+      Io_infer.Html.pp_start_color
+      Orange
+      pp
+      vpath
+      Io_infer.Html.pp_end_color
+      ()
+  } else {
+    F.fprintf fmt "%a" pp vpath
+  }
+};
+
+let rec has_tmp_var =
+  fun
+  | Dpvar pvar
+  | Dpvaraddr pvar => Pvar.is_frontend_tmp pvar
+  | Dderef dexp
+  | Ddot dexp _
+  | Darrow dexp _
+  | Dunop _ dexp
+  | Dsizeof _ (Some dexp) _ => has_tmp_var dexp
+  | Darray dexp1 dexp2
+  | Dbinop _ dexp1 dexp2 => has_tmp_var dexp1 || has_tmp_var dexp2
+  | Dretcall dexp dexp_list _ _
+  | Dfcall dexp dexp_list _ _ => has_tmp_var dexp || IList.exists has_tmp_var dexp_list
+  | Dconst _
+  | Dunknown
+  | Dsizeof _ None _ => false;
diff --git a/infer/src/IR/DecompiledExp.rei b/infer/src/IR/DecompiledExp.rei
new file mode 100644
index 000000000..3d8cf2341
--- /dev/null
+++ b/infer/src/IR/DecompiledExp.rei
@@ -0,0 +1,58 @@
+/*
+ * vim: set ft=rust:
+ * vim: set ft=reason:
+ *
+ * Copyright (c) 2009 - 2013 Monoidics ltd.
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+open! Utils;
+
+
+/** The Smallfoot Intermediate Language: Decompiled Expressions */
+let module L = Logging;
+
+let module F = Format;
+
+
+/** expression representing the result of decompilation */
+type t =
+  | Darray of t t
+  | Dbinop of Binop.t t t
+  | Dconst of Const.t
+  | Dsizeof of Typ.t (option t) Subtype.t
+  | Dderef of t
+  | Dfcall of t (list t) Location.t CallFlags.t
+  | Darrow of t Ident.fieldname
+  | Ddot of t Ident.fieldname
+  | Dpvar of Pvar.t
+  | Dpvaraddr of Pvar.t
+  | Dunop of Unop.t t
+  | Dunknown
+  | Dretcall of t (list t) Location.t CallFlags.t;
+
+
+/** Value paths: identify an occurrence of a value in a symbolic heap
+    each expression represents a path, with Dpvar being the simplest one */
+type vpath = option t;
+
+
+/** convert to a string */
+let to_string: t => string;
+
+
+/** pretty print */
+let pp: F.formatter => t => unit;
+
+
+/** Pretty print a value path */
+let pp_vpath: printenv => F.formatter => vpath => unit;
+
+
+/** return true if [dexp] contains a temporary pvar */
+let has_tmp_var: t => bool;
diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re
index 8e9c0337d..0e2cca0c5 100644
--- a/infer/src/IR/Sil.re
+++ b/infer/src/IR/Sil.re
@@ -75,35 +75,13 @@ type taint_kind =
 type taint_info = {taint_source: Procname.t, taint_kind: taint_kind};
 
 
-/** expression representing the result of decompilation */
-type dexp =
-  | Darray of dexp dexp
-  | Dbinop of Binop.t dexp dexp
-  | Dconst of Const.t
-  | Dsizeof of Typ.t (option dexp) Subtype.t
-  | Dderef of dexp
-  | Dfcall of dexp (list dexp) Location.t CallFlags.t
-  | Darrow of dexp Ident.fieldname
-  | Ddot of dexp Ident.fieldname
-  | Dpvar of Pvar.t
-  | Dpvaraddr of Pvar.t
-  | Dunop of Unop.t dexp
-  | Dunknown
-  | Dretcall of dexp (list dexp) Location.t CallFlags.t;
-
-
-/** Value paths: identify an occurrence of a value in a symbolic heap
-    each expression represents a path, with Dpvar being the simplest one */
-type vpath = option dexp;
-
-
 /** acquire/release action on a resource */
 type res_action = {
   ra_kind: res_act_kind, /** kind of action */
   ra_res: resource, /** kind of resource */
   ra_pname: Procname.t, /** name of the procedure used to acquire/release the resource */
   ra_loc: Location.t, /** location of the acquire/release */
-  ra_vpath: vpath /** vpath of the resource value */
+  ra_vpath: DecompiledExp.vpath /** vpath of the resource value */
 };
 
 
@@ -508,23 +486,6 @@ let attr_is_undef =
   | Aundef _ => true
   | _ => false;
 
-let rec dexp_has_tmp_var =
-  fun
-  | Dpvar pvar
-  | Dpvaraddr pvar => Pvar.is_frontend_tmp pvar
-  | Dderef dexp
-  | Ddot dexp _
-  | Darrow dexp _
-  | Dunop _ dexp
-  | Dsizeof _ (Some dexp) _ => dexp_has_tmp_var dexp
-  | Darray dexp1 dexp2
-  | Dbinop _ dexp1 dexp2 => dexp_has_tmp_var dexp1 || dexp_has_tmp_var dexp2
-  | Dretcall dexp dexp_list _ _
-  | Dfcall dexp dexp_list _ _ => dexp_has_tmp_var dexp || IList.exists dexp_has_tmp_var dexp_list
-  | Dconst _
-  | Dunknown
-  | Dsizeof _ None _ => false;
-
 let attribute_compare (att1: attribute) (att2: attribute) :int =>
   switch (att1, att2) {
   | (Aresource ra1, Aresource ra2) =>
@@ -1015,126 +976,6 @@ let pp_seq_diff pp pe0 f =>
     doit
   };
 
-let java () => !Config.curr_language == Config.Java;
-
-let eradicate_java () => Config.eradicate && java ();
-
-
-/** convert a dexp to a string */
-let rec dexp_to_string =
-  fun
-  | Darray de1 de2 => dexp_to_string de1 ^ "[" ^ dexp_to_string de2 ^ "]"
-  | Dbinop op de1 de2 => "(" ^ dexp_to_string de1 ^ Binop.str pe_text op ^ dexp_to_string de2 ^ ")"
-  | Dconst (Cfun pn) => Procname.to_simplified_string pn
-  | Dconst c => Const.to_string c
-  | Dderef de => "*" ^ dexp_to_string de
-  | Dfcall fun_dexp args _ {cf_virtual: isvirtual} => {
-      let pp_arg fmt de => F.fprintf fmt "%s" (dexp_to_string de);
-      let pp_args fmt des =>
-        if (eradicate_java ()) {
-          if (des != []) {
-            F.fprintf fmt "..."
-          }
-        } else {
-          pp_comma_seq pp_arg fmt des
-        };
-      let pp_fun fmt => (
-        fun
-        | Dconst (Cfun pname) => {
-            let s =
-              switch pname {
-              | Procname.Java pname_java => Procname.java_get_method pname_java
-              | _ => Procname.to_string pname
-              };
-            F.fprintf fmt "%s" s
-          }
-        | de => F.fprintf fmt "%s" (dexp_to_string de)
-      );
-      let (receiver, args') =
-        switch args {
-        | [Dpvar pv, ...args'] when isvirtual && Pvar.is_this pv => (None, args')
-        | [a, ...args'] when isvirtual => (Some a, args')
-        | _ => (None, args)
-        };
-      let pp fmt () => {
-        let pp_receiver fmt => (
-          fun
-          | None => ()
-          | Some arg => F.fprintf fmt "%a." pp_arg arg
-        );
-        F.fprintf fmt "%a%a(%a)" pp_receiver receiver pp_fun fun_dexp pp_args args'
-      };
-      pp_to_string pp ()
-    }
-  | Darrow (Dpvar pv) f when Pvar.is_this pv =>
-    /* this->fieldname */
-    Ident.fieldname_to_simplified_string f
-  | Darrow de f =>
-    if (Ident.fieldname_is_hidden f) {
-      dexp_to_string de
-    } else if (java ()) {
-      dexp_to_string de ^ "." ^ Ident.fieldname_to_flat_string f
-    } else {
-      dexp_to_string de ^ "->" ^ Ident.fieldname_to_string f
-    }
-  | Ddot (Dpvar _) fe when eradicate_java () =>
-    /* static field access */
-    Ident.fieldname_to_simplified_string fe
-  | Ddot de f =>
-    if (Ident.fieldname_is_hidden f) {
-      "&" ^ dexp_to_string de
-    } else if (java ()) {
-      dexp_to_string de ^ "." ^ Ident.fieldname_to_flat_string f
-    } else {
-      dexp_to_string de ^ "." ^ Ident.fieldname_to_string f
-    }
-  | Dpvar pv => Mangled.to_string (Pvar.get_name pv)
-  | Dpvaraddr pv => {
-      let s =
-        if (eradicate_java ()) {
-          Pvar.get_simplified_name pv
-        } else {
-          Mangled.to_string (Pvar.get_name pv)
-        };
-      let ampersand =
-        if (eradicate_java ()) {
-          ""
-        } else {
-          "&"
-        };
-      ampersand ^ s
-    }
-  | Dunop op de => Unop.str op ^ dexp_to_string de
-  | Dsizeof typ _ _ => pp_to_string (Typ.pp_full pe_text) typ
-  | Dunknown => "unknown"
-  | Dretcall de _ _ _ => "returned by " ^ dexp_to_string de;
-
-
-/** Pretty print a dexp. */
-let pp_dexp fmt de => F.fprintf fmt "%s" (dexp_to_string de);
-
-
-/** Pretty print a value path */
-let pp_vpath pe fmt vpath => {
-  let pp fmt =>
-    fun
-    | Some de => pp_dexp fmt de
-    | None => ();
-  if (pe.pe_kind === PP_HTML) {
-    F.fprintf
-      fmt
-      " %a{vpath: %a}%a"
-      Io_infer.Html.pp_start_color
-      Orange
-      pp
-      vpath
-      Io_infer.Html.pp_end_color
-      ()
-  } else {
-    F.fprintf fmt "%a" pp vpath
-  }
-};
-
 
 /** convert the attribute to a string */
 let attribute_to_string pe =>
@@ -1159,7 +1000,7 @@ let attribute_to_string pe =>
         };
       let str_vpath =
         if Config.trace_error {
-          pp_to_string (pp_vpath pe) ra.ra_vpath
+          pp_to_string (DecompiledExp.pp_vpath pe) ra.ra_vpath
         } else {
           ""
         };
diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei
index 2ea625edd..7ff8a8df0 100644
--- a/infer/src/IR/Sil.rei
+++ b/infer/src/IR/Sil.rei
@@ -63,35 +63,13 @@ type taint_kind =
 type taint_info = {taint_source: Procname.t, taint_kind: taint_kind};
 
 
-/** expression representing the result of decompilation */
-type dexp =
-  | Darray of dexp dexp
-  | Dbinop of Binop.t dexp dexp
-  | Dconst of Const.t
-  | Dsizeof of Typ.t (option dexp) Subtype.t
-  | Dderef of dexp
-  | Dfcall of dexp (list dexp) Location.t CallFlags.t
-  | Darrow of dexp Ident.fieldname
-  | Ddot of dexp Ident.fieldname
-  | Dpvar of Pvar.t
-  | Dpvaraddr of Pvar.t
-  | Dunop of Unop.t dexp
-  | Dunknown
-  | Dretcall of dexp (list dexp) Location.t CallFlags.t;
-
-
-/** Value paths: identify an occurrence of a value in a symbolic heap
-    each expression represents a path, with Dpvar being the simplest one */
-type vpath = option dexp;
-
-
 /** acquire/release action on a resource */
 type res_action = {
   ra_kind: res_act_kind, /** kind of action */
   ra_res: resource, /** kind of resource */
   ra_pname: Procname.t, /** name of the procedure used to acquire/release the resource */
   ra_loc: Location.t, /** location of the acquire/release */
-  ra_vpath: vpath /** vpath of the resource value */
+  ra_vpath: DecompiledExp.vpath /** vpath of the resource value */
 };
 
 
@@ -417,10 +395,6 @@ let is_block_pvar: Pvar.t => bool;
     the function raises an exception by calling "assert false". */
 let binop_invert: Binop.t => exp => exp => exp;
 
-
-/** return true if [dexp] contains a temporary pvar */
-let dexp_has_tmp_var: dexp => bool;
-
 let mem_kind_compare: mem_kind => mem_kind => int;
 
 let attribute_compare: attribute => attribute => int;
@@ -533,14 +507,6 @@ let mem_dealloc_pname: mem_kind => Procname.t;
 let attribute_to_string: printenv => attribute => string;
 
 
-/** convert a dexp to a string */
-let dexp_to_string: dexp => string;
-
-
-/** Pretty print a dexp. */
-let pp_dexp: F.formatter => dexp => unit;
-
-
 /** Pretty print an expression. */
 let pp_exp: printenv => F.formatter => exp => unit;
 
@@ -617,10 +583,6 @@ let pp_instr_list: printenv => F.formatter => list instr => unit;
 let d_instr_list: list instr => unit;
 
 
-/** Pretty print a value path */
-let pp_vpath: printenv => F.formatter => vpath => unit;
-
-
 /** Pretty print an atom. */
 let pp_atom: printenv => F.formatter => atom => unit;
 
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index 0e869ca4c..9084c0286 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -1022,7 +1022,7 @@ let cycle_has_weak_or_unretained_or_assign_field cycle =
 
 let check_observer_is_unsubscribed_deallocation prop e =
   let pvar_opt = match Prop.get_resource_attribute prop e with
-    | Some (Sil.Aresource ({Sil.ra_vpath =  Some (Sil.Dpvar pvar) })) -> Some pvar
+    | Some (Sil.Aresource ({Sil.ra_vpath =  Some (DecompiledExp.Dpvar pvar) })) -> Some pvar
     | _ -> None in
   let loc = State.get_loc () in
   match Prop.get_observer_attribute prop e with
diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml
index fdc5a5ba8..1ba036043 100644
--- a/infer/src/backend/buckets.ml
+++ b/infer/src/backend/buckets.ml
@@ -124,7 +124,7 @@ let check_access access_opt de_opt =
   | _ ->
       begin
         match de_opt with
-        | Some (Sil.Dconst _) ->
+        | Some (DecompiledExp.Dconst _) ->
             Some Localise.BucketLevel.b1
         | _ -> None
       end
diff --git a/infer/src/backend/buckets.mli b/infer/src/backend/buckets.mli
index 8bece448e..3adaa8b93 100644
--- a/infer/src/backend/buckets.mli
+++ b/infer/src/backend/buckets.mli
@@ -14,4 +14,5 @@ open! Utils
 
 (** Classify the bucket of an error desc using Location.access and nullable information *)
 val classify_access :
-  Localise.error_desc -> Localise.access option -> Sil.dexp option -> bool -> Localise.error_desc
+  Localise.error_desc -> Localise.access option -> DecompiledExp.t option -> bool ->
+  Localise.error_desc
diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml
index 437106cda..a94b9de9f 100644
--- a/infer/src/backend/errdesc.ml
+++ b/infer/src/backend/errdesc.ml
@@ -14,6 +14,7 @@ open! Utils
 
 module L = Logging
 module F = Format
+module DExp = DecompiledExp
 
 let smart_pointers = [
   ["std"; "shared_ptr"];
@@ -217,7 +218,7 @@ let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option =
 
 (** Find the Letderef instruction used to declare normal variable [id],
     and return the expression dereferenced to initialize [id] *)
-let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp option =
+let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : DExp.t option =
   let is_infer = not (Config.checkers || Config.eradicate) in
   let find_declaration node = function
     | Sil.Letderef (id0, e, _, _) when Ident.equal id id0 ->
@@ -240,7 +241,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
           (L.d_str "find_normal_variable_letderef function call ";
            Sil.d_exp fun_exp; L.d_ln ());
 
-        let fun_dexp = Sil.Dconst (Const.Cfun pname) in
+        let fun_dexp = DExp.Dconst (Const.Cfun pname) in
         let args_dexp =
           let args_dexpo = IList.map (fun (e, _) -> _exp_rv_dexp seen node e) args in
           if IList.exists (fun x -> x = None) args_dexpo
@@ -248,7 +249,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
           else
             let unNone = function Some x -> x | None -> assert false in
             IList.map unNone args_dexpo in
-        Some (Sil.Dretcall (fun_dexp, args_dexp, loc, call_flags))
+        Some (DExp.Dretcall (fun_dexp, args_dexp, loc, call_flags))
     | Sil.Set (Sil.Lvar pvar, _, Sil.Var id0, _)
       when is_infer && Ident.equal id id0 && not (Pvar.is_frontend_tmp pvar) ->
         (* this case is a hack to make bucketing continue to work in the presence of copy
@@ -256,7 +257,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
            n1 = foo(); x = n1; n2 = x; n2.toString(), but copy-propagation will optimize this to:
            n1 = foo(); x = n1; n1.toString(). This case allows us to recognize the association
            between n1 and x. Eradicate/checkers don't use copy-prop, so they don't need this. *)
-        Some (Sil.Dpvar pvar)
+        Some (DExp.Dpvar pvar)
     | _ -> None in
   let res = find_in_node_or_preds node find_declaration in
   if verbose && res == None
@@ -270,7 +271,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
   res
 
 (** describe lvalue [e] as a dexp *)
-and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
+and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : DExp.t option =
   if Sil.ExpSet.mem e _seen then
     (L.d_str "exp_lv_dexp: cycle detected"; Sil.d_exp e; L.d_ln (); None)
   else
@@ -278,17 +279,17 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
     match Prop.exp_normalize_noabs Sil.sub_empty e with
     | Sil.Const c ->
         if verbose then (L.d_str "exp_lv_dexp: constant "; Sil.d_exp e; L.d_ln ());
-        Some (Sil.Dderef (Sil.Dconst c))
+        Some (DExp.Dderef (DExp.Dconst c))
     | Sil.BinOp(Binop.PlusPI, e1, e2) ->
         if verbose then (L.d_str "exp_lv_dexp: (e1 +PI e2) "; Sil.d_exp e; L.d_ln ());
         (match _exp_lv_dexp seen node e1, _exp_rv_dexp seen node e2 with
-         | Some de1, Some de2 -> Some (Sil.Dbinop(Binop.PlusPI, de1, de2))
+         | Some de1, Some de2 -> Some (DExp.Dbinop(Binop.PlusPI, de1, de2))
          | _ -> None)
     | Sil.Var id when Ident.is_normal id ->
         if verbose then (L.d_str "exp_lv_dexp: normal var "; Sil.d_exp e; L.d_ln ());
         (match _find_normal_variable_letderef seen node id with
          | None -> None
-         | Some de -> Some (Sil.Dderef de))
+         | Some de -> Some (DExp.Dderef de))
     | Sil.Lvar pvar ->
         if verbose then (L.d_str "exp_lv_dexp: program var "; Sil.d_exp e; L.d_ln ());
         if Pvar.is_frontend_tmp pvar then
@@ -298,7 +299,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
                 begin
                   match find_struct_by_value_assignment node pvar with
                   | Some (_, pname, loc, call_flags) ->
-                      Some (Sil.Dfcall (Sil.Dconst (Cfun pname), [], loc, call_flags))
+                      Some (DExp.Dfcall (DExp.Dconst (Cfun pname), [], loc, call_flags))
                   | None ->
                       None
                 end
@@ -312,12 +313,12 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
                       else
                         let unNone = function Some x -> x | None -> assert false in
                         let args = IList.map unNone blame_args in
-                        Some (Sil.Dfcall (unNone fun_dexpo, args, loc, call_flags))
+                        Some (DExp.Dfcall (unNone fun_dexpo, args, loc, call_flags))
                   | None ->
                       _exp_rv_dexp seen node' (Sil.Var id)
                 end
           end
-        else Some (Sil.Dpvar pvar)
+        else Some (DExp.Dpvar pvar)
     | Sil.Lfield (Sil.Var id, f, _) when Ident.is_normal id ->
         if verbose then
           begin
@@ -328,7 +329,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
           end;
         (match _find_normal_variable_letderef seen node id with
          | None -> None
-         | Some de -> Some (Sil.Darrow (de, f)))
+         | Some de -> Some (DExp.Darrow (de, f)))
     | Sil.Lfield (e1, f, _) ->
         if verbose then
           begin
@@ -339,7 +340,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
           end;
         (match _exp_lv_dexp seen node e1 with
          | None -> None
-         | Some de -> Some (Sil.Ddot (de, f)))
+         | Some de -> Some (DExp.Ddot (de, f)))
     | Sil.Lindex (e1, e2) ->
         if verbose then
           begin
@@ -353,14 +354,14 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
          | None, _ -> None
          | Some de1, None ->
              (* even if the index is unknown, the array info is useful for bound errors *)
-             Some (Sil.Darray (de1, Sil.Dunknown))
-         | Some de1, Some de2 -> Some (Sil.Darray (de1, de2)))
+             Some (DExp.Darray (de1, DExp.Dunknown))
+         | Some de1, Some de2 -> Some (DExp.Darray (de1, de2)))
     | _ ->
         if verbose then (L.d_str "exp_lv_dexp: no match for  "; Sil.d_exp e; L.d_ln ());
         None
 
 (** describe rvalue [e] as a dexp *)
-and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
+and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : DExp.t option =
   if Sil.ExpSet.mem e _seen then
     (L.d_str "exp_rv_dexp: cycle detected"; Sil.d_exp e; L.d_ln (); None)
   else
@@ -368,12 +369,12 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
     match e with
     | Sil.Const c ->
         if verbose then (L.d_str "exp_rv_dexp: constant "; Sil.d_exp e; L.d_ln ());
-        Some (Sil.Dconst c)
+        Some (DExp.Dconst c)
     | Sil.Lvar pv ->
         if verbose then (L.d_str "exp_rv_dexp: program var "; Sil.d_exp e; L.d_ln ());
         if Pvar.is_frontend_tmp pv
         then _exp_lv_dexp _seen (* avoid spurious cycle detection *) node e
-        else Some (Sil.Dpvaraddr pv)
+        else Some (DExp.Dpvaraddr pv)
     | Sil.Var id when Ident.is_normal id ->
         if verbose then (L.d_str "exp_rv_dexp: normal var "; Sil.d_exp e; L.d_ln ());
         _find_normal_variable_letderef seen node id
@@ -387,7 +388,7 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
           end;
         (match _exp_rv_dexp seen node e1 with
          | None -> None
-         | Some de -> Some (Sil.Ddot(de, f)))
+         | Some de -> Some (DExp.Ddot(de, f)))
     | Sil.Lindex (e1, e2) ->
         if verbose then
           begin
@@ -399,23 +400,23 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
           end;
         (match _exp_rv_dexp seen node e1, _exp_rv_dexp seen node e2 with
          | None, _ | _, None -> None
-         | Some de1, Some de2 -> Some (Sil.Darray(de1, de2)))
+         | Some de1, Some de2 -> Some (DExp.Darray(de1, de2)))
     | Sil.BinOp (op, e1, e2) ->
         if verbose then (L.d_str "exp_rv_dexp: BinOp "; Sil.d_exp e; L.d_ln ());
         (match _exp_rv_dexp seen node e1, _exp_rv_dexp seen node e2 with
          | None, _ | _, None -> None
-         | Some de1, Some de2 -> Some (Sil.Dbinop (op, de1, de2)))
+         | Some de1, Some de2 -> Some (DExp.Dbinop (op, de1, de2)))
     | Sil.UnOp (op, e1, _) ->
         if verbose then (L.d_str "exp_rv_dexp: UnOp "; Sil.d_exp e; L.d_ln ());
         (match _exp_rv_dexp seen node e1 with
          | None -> None
-         | Some de1 -> Some (Sil.Dunop (op, de1)))
+         | Some de1 -> Some (DExp.Dunop (op, de1)))
     | Sil.Cast (_, e1) ->
         if verbose then (L.d_str "exp_rv_dexp: Cast "; Sil.d_exp e; L.d_ln ());
         _exp_rv_dexp seen node e1
     | Sil.Sizeof (typ, len, sub) ->
         if verbose then (L.d_str "exp_rv_dexp: type "; Sil.d_exp e; L.d_ln ());
-        Some (Sil.Dsizeof (typ, Option.map_default (_exp_rv_dexp seen node) None len, sub))
+        Some (DExp.Dsizeof (typ, Option.map_default (_exp_rv_dexp seen node) None len, sub))
     | _ ->
         if verbose then (L.d_str "exp_rv_dexp: no match for  "; Sil.d_exp e; L.d_ln ());
         None
@@ -507,8 +508,8 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
         Some desc_string
       end
     else match vpath with
-      | Some de when not (Sil.dexp_has_tmp_var de) ->
-          Some (Sil.dexp_to_string de)
+      | Some de when not (DExp.has_tmp_var de) ->
+          Some (DExp.to_string de)
       | _ -> None in
   let res_action_opt, resource_opt, vpath = match alloc_att_opt with
     | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Racquire } as ra)) ->
@@ -541,7 +542,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
           (L.d_str "explain_leak: current instruction is Nullify for pvar ";
            Pvar.d pvar; L.d_ln ());
         (match exp_lv_dexp (State.get_node ()) (Sil.Lvar pvar) with
-         | Some de when not (Sil.dexp_has_tmp_var de)-> Some (Sil.dexp_to_string de)
+         | Some de when not (DExp.has_tmp_var de)-> Some (DExp.to_string de)
          | _ -> None)
     | Some (Sil.Abstract _) ->
         if verbose then (L.d_str "explain_leak: current instruction is Abstract"; L.d_ln ());
@@ -563,7 +564,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
           (L.d_str "explain_leak: current instruction Set for ";
            Sil.d_exp lexp; L.d_ln ());
         (match exp_lv_dexp node lexp with
-         | Some dexp when not (Sil.dexp_has_tmp_var dexp) -> Some (Sil.dexp_to_string dexp)
+         | Some dexp when not (DExp.has_tmp_var dexp) -> Some (DExp.to_string dexp)
          | _ -> None)
     | Some instr ->
         if verbose
@@ -586,7 +587,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
 
 (** find the dexp, if any, where the given value is stored
     also return the type of the value if found *)
-let vpath_find prop _exp : Sil.dexp option * Typ.t option =
+let vpath_find prop _exp : DExp.t option * Typ.t option =
   if verbose then (L.d_str "in vpath_find exp:"; Sil.d_exp _exp; L.d_ln ());
   let rec find sigma_acc sigma_todo exp =
     let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = match se with
@@ -604,11 +605,11 @@ let vpath_find prop _exp : Sil.dexp option * Typ.t option =
                         Some t
                       with Not_found -> None)
                  | _ -> None in
-               res := Some (Sil.Ddot (Sil.Dpvar pv, f)), typo
+               res := Some (DExp.Ddot (DExp.Dpvar pv, f)), typo
            | Sil.Var id ->
                (match find [] sigma' (Sil.Var id) with
                 | None, _ -> ()
-                | Some de, typo -> res := Some (Sil.Darrow (de, f)), typo)
+                | Some de, typo -> res := Some (DExp.Darrow (de, f)), typo)
            | lexp ->
                if verbose
                then
@@ -623,11 +624,11 @@ let vpath_find prop _exp : Sil.dexp option * Typ.t option =
                let typo = match texp with
                  | Sil.Sizeof (typ, _, _) -> Some typ
                  | _ -> None in
-               Some (Sil.Dpvar pv), typo
+               Some (DExp.Dpvar pv), typo
            | Sil.Var id ->
                (match find [] sigma' (Sil.Var id) with
                 | None, typo -> None, typo
-                | Some de, typo -> Some (Sil.Dderef de), typo)
+                | Some de, typo -> Some (DExp.Dderef de), typo)
            | lexp ->
                if verbose
                then
@@ -665,7 +666,8 @@ let vpath_find prop _exp : Sil.dexp option * Typ.t option =
   if verbose then begin
     match res with
     | None, _ -> L.d_str "vpath_find: cannot find "; Sil.d_exp _exp; L.d_ln ()
-    | Some de, typo -> L.d_str "vpath_find: found "; L.d_str (Sil.dexp_to_string de); L.d_str " : ";
+    | Some de, typo ->
+        L.d_str "vpath_find: found "; L.d_str (DExp.to_string de); L.d_str " : ";
         match typo with
         | None -> L.d_str " No type"
         | Some typ -> Typ.d_full typ;
@@ -706,10 +708,10 @@ let explain_dexp_access prop dexp is_nullable =
     | (e1, se):: esel' ->
         if Sil.exp_equal e1 e then Some se
         else lookup_esel esel' e in
-  let rec lookup : Sil.dexp -> Sil.strexp option = function
-    | Sil.Dconst c ->
+  let rec lookup : DExp.t -> Sil.strexp option = function
+    | DExp.Dconst c ->
         Some (Sil.Eexp (Sil.Const c, Sil.inst_none))
-    | Sil.Darray (de1, de2) ->
+    | DExp.Darray (de1, de2) ->
         (match lookup de1, lookup de2 with
          | None, _ | _, None -> None
          | Some Sil.Earray (_, esel, _), Some Sil.Eexp (e, _) ->
@@ -720,23 +722,23 @@ let explain_dexp_access prop dexp is_nullable =
                (L.d_str "lookup: case not matched on Darray ";
                 Sil.d_sexp se1; L.d_str " "; Sil.d_sexp se2; L.d_ln());
              None)
-    | Sil.Darrow ((Sil.Dpvaraddr pvar), f) ->
-        (match lookup (Sil.Dpvaraddr pvar) with
+    | DExp.Darrow ((DExp.Dpvaraddr pvar), f) ->
+        (match lookup (DExp.Dpvaraddr pvar) with
          | None -> None
          | Some Sil.Estruct (fsel, _) ->
              lookup_fld fsel f
          | Some _ ->
              if verbose then (L.d_str "lookup: case not matched on Darrow "; L.d_ln ());
              None)
-    | Sil.Darrow (de1, f) ->
-        (match lookup (Sil.Dderef de1) with
+    | DExp.Darrow (de1, f) ->
+        (match lookup (DExp.Dderef de1) with
          | None -> None
          | Some Sil.Estruct (fsel, _) ->
              lookup_fld fsel f
          | Some _ ->
              if verbose then (L.d_str "lookup: case not matched on Darrow "; L.d_ln ());
              None)
-    | Sil.Ddot (de1, f) ->
+    | DExp.Ddot (de1, f) ->
         (match lookup de1 with
          | None -> None
          | Some Sil.Estruct (fsel, _) ->
@@ -746,38 +748,38 @@ let explain_dexp_access prop dexp is_nullable =
          | Some _ ->
              if verbose then (L.d_str "lookup: case not matched on Ddot "; L.d_ln ());
              None)
-    | Sil.Dpvar pvar ->
+    | DExp.Dpvar pvar ->
         if verbose then (L.d_str "lookup: found Dpvar "; L.d_ln ());
         (find_ptsto (Sil.Lvar pvar))
-    | Sil.Dderef de ->
+    | DExp.Dderef de ->
         (match lookup de with
          | None -> None
          | Some (Sil.Eexp (e, _)) -> find_ptsto e
          | Some _ -> None)
-    | (Sil.Dbinop(Binop.PlusPI, Sil.Dpvar _, Sil.Dconst _) as de) ->
-        if verbose then (L.d_strln ("lookup: case )pvar + constant) " ^ Sil.dexp_to_string de));
+    | (DExp.Dbinop(Binop.PlusPI, DExp.Dpvar _, DExp.Dconst _) as de) ->
+        if verbose then (L.d_strln ("lookup: case )pvar + constant) " ^ DExp.to_string de));
         None
-    | Sil.Dfcall (Sil.Dconst c, _, loc, _) ->
+    | DExp.Dfcall (DExp.Dconst c, _, loc, _) ->
         if verbose then (L.d_strln "lookup: found Dfcall ");
         (match c with
          | Const.Cfun _ -> (* Treat function as an update *)
              Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_call loc.Location.line))
          | _ -> None)
-    | Sil.Dretcall (Sil.Dconst (Const.Cfun pname as c ) , _, loc, _ )
+    | DExp.Dretcall (DExp.Dconst (Const.Cfun pname as c ) , _, loc, _ )
       when method_of_pointer_wrapper pname ->
         if verbose then (L.d_strln "lookup: found Dretcall ");
         Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_pointer_wrapper_call loc.Location.line))
-    | Sil.Dpvaraddr pvar ->
-        (L.d_strln ("lookup: found Dvaraddr " ^ Sil.dexp_to_string (Sil.Dpvaraddr pvar)));
+    | DExp.Dpvaraddr pvar ->
+        (L.d_strln ("lookup: found Dvaraddr " ^ DExp.to_string (DExp.Dpvaraddr pvar)));
         find_ptsto (Sil.Lvar pvar)
     | de ->
-        if verbose then (L.d_strln ("lookup: unknown case not matched " ^ Sil.dexp_to_string de));
+        if verbose then (L.d_strln ("lookup: unknown case not matched " ^ DExp.to_string de));
         None in
   let access_opt = match sexpo_to_inst (lookup dexp) with
     | None ->
         if verbose
         then
-          (L.d_strln ("explain_dexp_access: cannot find inst of " ^ Sil.dexp_to_string dexp));
+          (L.d_strln ("explain_dexp_access: cannot find inst of " ^ DExp.to_string dexp));
         None
     | Some (Sil.Iupdate (_, ncf, n, _)) ->
         Some (Localise.Last_assigned (n, ncf))
@@ -801,15 +803,17 @@ let explain_dexp_access prop dexp is_nullable =
 let explain_dereference_access outermost_array is_nullable _de_opt prop =
   let de_opt =
     let rec remove_outermost_array_access = function (* remove outermost array access from [de] *)
-      | Sil.Dbinop(Binop.PlusPI, de1, _) -> (* remove pointer arithmetic before array access *)
+      | DExp.Dbinop(Binop.PlusPI, de1, _) ->
+          (* remove pointer arithmetic before array access *)
           remove_outermost_array_access de1
-      | Sil.Darray(Sil.Dderef de1, _) -> (* array access is a deref already: remove both *)
+      | DExp.Darray(DExp.Dderef de1, _) ->
+          (* array access is a deref already: remove both *)
           de1
-      | Sil.Darray(de1, _) -> (* remove array access *)
+      | DExp.Darray(de1, _) -> (* remove array access *)
           de1
-      | Sil.Dderef de -> (* remove implicit array access *)
+      | DExp.Dderef de -> (* remove implicit array access *)
           de
-      | Sil.Ddot (de, _) -> (* remove field access before array access *)
+      | DExp.Ddot (de, _) -> (* remove field access before array access *)
           remove_outermost_array_access de
       | de -> de in
     match _de_opt with
@@ -817,12 +821,12 @@ let explain_dereference_access outermost_array is_nullable _de_opt prop =
     | Some de ->
         Some (if outermost_array then remove_outermost_array_access de else de) in
   let value_str = match de_opt with
-    | Some (Sil.Darrow ((Sil.Dpvaraddr pvar), f) as de) ->
+    | Some (DExp.Darrow ((DExp.Dpvaraddr pvar), f) as de) ->
         if is_special_field smart_pointers None f then
-          Sil.dexp_to_string (Sil.Dpvaraddr pvar)
-        else Sil.dexp_to_string de
+          DExp.to_string (DExp.Dpvaraddr pvar)
+        else DExp.to_string de
     | Some de ->
-        Sil.dexp_to_string de
+        DExp.to_string de
     | None -> "" in
   let access_opt = match de_opt with
     | Some de -> explain_dexp_access prop de is_nullable
@@ -846,20 +850,20 @@ let create_dereference_desc
   let desc =
     if !Config.curr_language = Config.Clang && not is_premature_nil then
       match de_opt with
-      | Some (Sil.Dpvar pvar)
-      | Some (Sil.Dpvaraddr pvar) ->
+      | Some (DExp.Dpvar pvar)
+      | Some (DExp.Dpvaraddr pvar) ->
           (match Prop.get_objc_null_attribute prop (Sil.Lvar pvar) with
            | Some (Sil.Aobjc_null (v,fs)) ->
                let e = IList.fold_left (fun e f -> Sil.Lfield (e, f, Typ.Tvoid)) (Sil.Lvar v) fs in
                Localise.parameter_field_not_null_checked_desc desc e
            | _ ->
                desc)
-      | Some (Sil.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ ))
+      | Some (DExp.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ ))
         when is_vector_method pname ->
-          Localise.desc_empty_vector_access (Some pname) (Sil.dexp_to_string this_dexp) loc
-      | Some (Sil.Darrow (dexp, fieldname))
+          Localise.desc_empty_vector_access (Some pname) (DExp.to_string this_dexp) loc
+      | Some (DExp.Darrow (dexp, fieldname))
         when is_special_field [vector_class] (Some "beginPtr") fieldname ->
-          Localise.desc_empty_vector_access None (Sil.dexp_to_string dexp) loc
+          Localise.desc_empty_vector_access None (DExp.to_string dexp) loc
       | _ -> desc
     else desc in
   if use_buckets then Buckets.classify_access desc access_opt' de_opt is_nullable
@@ -974,10 +978,10 @@ let dexp_apply_pvar_off dexp pvar_off =
   let rec add_ddot de = function
     | [] -> de
     | f:: fl ->
-        add_ddot (Sil.Ddot (de, f)) fl in
+        add_ddot (DExp.Ddot (de, f)) fl in
   match pvar_off with
   | Fpvar -> dexp
-  | Fstruct (f:: fl) -> add_ddot (Sil.Darrow (dexp, f)) fl
+  | Fstruct (f:: fl) -> add_ddot (DExp.Darrow (dexp, f)) fl
   | Fstruct [] -> dexp (* case should not happen *)
 
 (** Produce a description of the nth parameter of the function call, if the current instruction
@@ -1061,12 +1065,12 @@ let explain_dereference_as_caller_expression
 (** explain a class cast exception *)
 let explain_class_cast_exception pname_opt typ1 typ2 exp node loc =
   let exp_str_opt = match exp_rv_dexp node exp with
-    | Some dexp -> Some (Sil.dexp_to_string dexp)
+    | Some dexp -> Some (DExp.to_string dexp)
     | None -> None in
   match exp_rv_dexp node typ1, exp_rv_dexp node typ2 with
   | Some de1, Some de2 ->
-      let typ_str1 = Sil.dexp_to_string de1 in
-      let typ_str2 = Sil.dexp_to_string de2 in
+      let typ_str1 = DExp.to_string de1 in
+      let typ_str2 = DExp.to_string de2 in
       Localise.desc_class_cast_exception pname_opt typ_str1 typ_str2 exp_str_opt loc
   | _ -> Localise.no_desc
 
@@ -1074,7 +1078,7 @@ let explain_class_cast_exception pname_opt typ1 typ2 exp node loc =
 let explain_divide_by_zero exp node loc =
   match exp_rv_dexp node exp with
   | Some de ->
-      let exp_str = Sil.dexp_to_string de in
+      let exp_str = DExp.to_string de in
       Localise.desc_divide_by_zero exp_str loc
   | None -> Localise.no_desc
 
@@ -1099,8 +1103,8 @@ let explain_tainted_value_reaching_sensitive_function
         begin
           match find_with_exp prop e with
           | Some (pvar, pvar_off) ->
-              let dexp = dexp_apply_pvar_off (Sil.Dpvar pvar) pvar_off in
-              Sil.dexp_to_string dexp
+              let dexp = dexp_apply_pvar_off (DExp.Dpvar pvar) pvar_off in
+              DExp.to_string dexp
           | None -> Sil.exp_to_string e
         end in
   Localise.desc_tainted_value_reaching_sensitive_function
@@ -1130,25 +1134,25 @@ let explain_condition_is_assignment loc =
 let explain_condition_always_true_false i cond node loc =
   let cond_str_opt = match exp_rv_dexp node cond with
     | Some de ->
-        Some (Sil.dexp_to_string de)
+        Some (DExp.to_string de)
     | None -> None in
   Localise.desc_condition_always_true_false i cond_str_opt loc
 
 (** explain the escape of a stack variable address from its scope *)
 let explain_stack_variable_address_escape loc pvar addr_dexp_opt =
   let addr_dexp_str = match addr_dexp_opt with
-    | Some (Sil.Dpvar pv)
+    | Some (DExp.Dpvar pv)
       when Pvar.is_local pv &&
            Mangled.equal (Pvar.get_name pv) Ident.name_return ->
         Some "the caller via a return"
-    | Some dexp -> Some (Sil.dexp_to_string dexp)
+    | Some dexp -> Some (DExp.to_string dexp)
     | None -> None in
   Localise.desc_stack_variable_address_escape (Pvar.to_string pvar) addr_dexp_str loc
 
 (** explain unary minus applied to unsigned expression *)
 let explain_unary_minus_applied_to_unsigned_expression exp typ node loc =
   let exp_str_opt = match exp_rv_dexp node exp with
-    | Some de -> Some (Sil.dexp_to_string de)
+    | Some de -> Some (DExp.to_string de)
     | None -> None in
   let typ_str =
     let pp fmt () = Typ.pp_full pe_text fmt typ in
@@ -1159,7 +1163,7 @@ let explain_unary_minus_applied_to_unsigned_expression exp typ node loc =
 let explain_null_test_after_dereference exp node line loc =
   match exp_rv_dexp node exp with
   | Some de ->
-      let expr_str = Sil.dexp_to_string de in
+      let expr_str = DExp.to_string de in
       Localise.desc_null_test_after_dereference expr_str line loc
   | None -> Localise.no_desc
 
diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli
index 92359ec6d..d77fad5a0 100644
--- a/infer/src/backend/errdesc.mli
+++ b/infer/src/backend/errdesc.mli
@@ -14,7 +14,7 @@ open! Utils
 
 (** find the dexp, if any, where the given value is stored
     also return the type of the value if found *)
-val vpath_find : 'a Prop.t -> Sil.exp -> Sil.vpath * Typ.t option
+val vpath_find : 'a Prop.t -> Sil.exp -> DecompiledExp.vpath * Typ.t option
 
 (** Return true if [id] is assigned to a program variable which is then nullified *)
 val id_is_assigned_then_dead : Cfg.Node.t -> Ident.t -> bool
@@ -38,7 +38,7 @@ val find_ident_assignment : Cfg.Node.t -> Ident.t -> (Cfg.Node.t * Sil.exp) opti
 val find_boolean_assignment : Cfg.Node.t -> Pvar.t -> bool -> Cfg.Node.t option
 
 (** describe rvalue [e] as a dexp *)
-val exp_rv_dexp : Cfg.Node.t -> Sil.exp -> Sil.dexp option
+val exp_rv_dexp : Cfg.Node.t -> Sil.exp -> DecompiledExp.t option
 
 (** Produce a description of a persistent reference to an Android Context *)
 val explain_context_leak : Procname.t -> Typ.t -> Ident.fieldname ->
@@ -94,7 +94,7 @@ val explain_condition_always_true_false :
 
 (** explain the escape of a stack variable address from its scope *)
 val explain_stack_variable_address_escape :
-  Location.t -> Pvar.t -> Sil.dexp option -> Localise.error_desc
+  Location.t -> Pvar.t -> DecompiledExp.t option -> Localise.error_desc
 
 (** explain frontend warning *)
 val explain_frontend_warning : string -> string -> Location.t -> Localise.error_desc
diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml
index 96ea401fe..7c5916fb5 100644
--- a/infer/src/backend/localise.ml
+++ b/infer/src/backend/localise.ml
@@ -469,7 +469,7 @@ let desc_custom_error loc : error_desc =
 
 let desc_bad_pointer_comparison dexp_opt loc : error_desc =
   let dexp_str = match dexp_opt with
-    | Some dexp -> (Sil.dexp_to_string dexp) ^ " "
+    | Some dexp -> (DecompiledExp.to_string dexp) ^ " "
     | None -> "" in
   let line_info = at_line (Tags.create ()) loc in
   let check_msg =
diff --git a/infer/src/backend/localise.mli b/infer/src/backend/localise.mli
index 8d94985b8..f47c88577 100644
--- a/infer/src/backend/localise.mli
+++ b/infer/src/backend/localise.mli
@@ -227,7 +227,7 @@ val desc_fragment_retains_view :
 (* Create human-readable error description for assertion failures *)
 val desc_custom_error : Location.t -> error_desc
 
-val desc_bad_pointer_comparison : Sil.dexp option -> Location.t -> error_desc
+val desc_bad_pointer_comparison : DecompiledExp.t option -> Location.t -> error_desc
 (** kind of precondition not met *)
 type pnm_kind =
   | Pnm_bounds
diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml
index 1ef9c65dc..acec4139d 100644
--- a/infer/src/checkers/checkers.ml
+++ b/infer/src/checkers/checkers.ml
@@ -548,7 +548,7 @@ let callback_print_c_method_calls { Callbacks.proc_desc; proc_name } =
     | Sil.Call (_, Sil.Const (Const.Cfun pn), (e, _):: _, loc, _)
       when Procname.is_c_method pn ->
         let receiver = match Errdesc.exp_rv_dexp node e with
-          | Some de -> Sil.dexp_to_string de
+          | Some de -> DecompiledExp.to_string de
           | None -> "?" in
         let description =
           Printf.sprintf "['%s' %s]" receiver (Procname.to_string pn) in
diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml
index 68a1cb3c5..1083172bf 100644
--- a/infer/src/eradicate/eradicateChecks.ml
+++ b/infer/src/eradicate/eradicateChecks.ml
@@ -57,7 +57,7 @@ let report_error =
 
 let explain_expr node e =
   match Errdesc.exp_rv_dexp node e with
-  | Some de -> Some (Sil.dexp_to_string de)
+  | Some de -> Some (DecompiledExp.to_string de)
   | None -> None
 
 (** Classify a procedure. *)
diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml
index 55458ad22..ebd32c13f 100644
--- a/infer/src/eradicate/typeCheck.ml
+++ b/infer/src/eradicate/typeCheck.ml
@@ -11,6 +11,7 @@ open! Utils
 
 module L = Logging
 module F = Format
+module DExp = DecompiledExp
 
 (** Module for type checking. *)
 
@@ -91,21 +92,21 @@ module ComplexExpressions = struct
         raise Not_handled in
 
       match dexp with
-      | Sil.Darray (de1, de2) ->
+      | DExp.Darray (de1, de2) ->
           dexp_to_string de1 ^ "[" ^ dexp_to_string de2 ^ "]"
-      | Sil.Darrow (de, f)
-      | Sil.Ddot (de, f) ->
+      | DExp.Darrow (de, f)
+      | DExp.Ddot (de, f) ->
           dexp_to_string de ^ "." ^ Ident.fieldname_to_string f
-      | Sil.Dbinop (op, de1, de2) ->
+      | DExp.Dbinop (op, de1, de2) ->
           "(" ^ dexp_to_string de1 ^ (Binop.str pe_text op) ^ dexp_to_string de2 ^ ")"
-      | Sil.Dconst (Const.Cfun pn) ->
+      | DExp.Dconst (Const.Cfun pn) ->
           Procname.to_unique_id pn
-      | Sil.Dconst c ->
+      | DExp.Dconst c ->
           pp_to_string (Const.pp pe_text) c
-      | Sil.Dderef de ->
+      | DExp.Dderef de ->
           dexp_to_string de
-      | Sil.Dfcall (fun_dexp, args, _, { CallFlags.cf_virtual = isvirtual })
-      | Sil.Dretcall (fun_dexp, args, _, { CallFlags.cf_virtual = isvirtual })
+      | DExp.Dfcall (fun_dexp, args, _, { CallFlags.cf_virtual = isvirtual })
+      | DExp.Dretcall (fun_dexp, args, _, { CallFlags.cf_virtual = isvirtual })
         when functions_idempotent () ->
           let pp_arg fmt de = F.fprintf fmt "%s" (dexp_to_string de) in
           let pp_args fmt des = (pp_comma_seq) pp_arg fmt des in
@@ -113,20 +114,20 @@ module ComplexExpressions = struct
             let virt = if isvirtual then "V" else "" in
             F.fprintf fmt "%a(%a)%s" pp_arg fun_dexp pp_args args virt in
           pp_to_string pp ()
-      | Sil.Dfcall _
-      | Sil.Dretcall _ ->
+      | DExp.Dfcall _
+      | DExp.Dretcall _ ->
           case_not_handled ()
-      | Sil.Dpvar pv
-      | Sil.Dpvaraddr pv when not (Pvar.is_frontend_tmp pv) ->
+      | DExp.Dpvar pv
+      | DExp.Dpvaraddr pv when not (Pvar.is_frontend_tmp pv) ->
           Pvar.to_string pv
-      | Sil.Dpvar _
-      | Sil.Dpvaraddr _ (* front-end variable -- this should not happen) *) ->
+      | DExp.Dpvar _
+      | DExp.Dpvaraddr _ (* front-end variable -- this should not happen) *) ->
           case_not_handled ()
-      | Sil.Dunop (op, de) ->
+      | DExp.Dunop (op, de) ->
           Unop.str op ^ dexp_to_string de
-      | Sil.Dsizeof _ ->
+      | DExp.Dsizeof _ ->
           case_not_handled ()
-      | Sil.Dunknown ->
+      | DExp.Dunknown ->
           case_not_handled () in
 
     match map_dexp (Errdesc.exp_rv_dexp node' exp) with
@@ -770,11 +771,11 @@ let typecheck_instr
               | Some dexp_key, Procname.Java callee_pname_java ->
                   let pname_get =
                     Procname.Java (pname_get_from_pname_put callee_pname_java) in
-                  let dexp_get = Sil.Dconst (Const.Cfun pname_get) in
-                  let dexp_map = Sil.Dpvar pv_map in
+                  let dexp_get = DExp.Dconst (Const.Cfun pname_get) in
+                  let dexp_map = DExp.Dpvar pv_map in
                   let args = [dexp_map; dexp_key] in
                   let call_flags = { CallFlags.default with CallFlags.cf_virtual = true } in
-                  Some (Sil.Dretcall (dexp_get, args, loc, call_flags))
+                  Some (DExp.Dretcall (dexp_get, args, loc, call_flags))
               | _ -> None in
             begin
               match ComplexExpressions.exp_to_string_map_dexp
@@ -903,16 +904,15 @@ let typecheck_instr
         let handle_containsKey e =
           let map_dexp = function
             | Some
-                (Sil.Dretcall
-                   (Sil.Dconst
-                      (Const.Cfun (Procname.Java pname_java)), args, loc, call_flags)) ->
+                (DExp.Dretcall
+                   (DExp.Dconst (Const.Cfun (Procname.Java pname_java)), args, loc, call_flags)) ->
                 let pname_java' =
                   let object_t = (Some "java.lang", "Object") in
                   Procname.java_replace_return_type
                     (Procname.java_replace_method pname_java "get")
                     object_t in
-                let fun_dexp = Sil.Dconst (Const.Cfun (Procname.Java pname_java')) in
-                Some (Sil.Dretcall (fun_dexp, args, loc, call_flags))
+                let fun_dexp = DExp.Dconst (Const.Cfun (Procname.Java pname_java')) in
+                Some (DExp.Dretcall (fun_dexp, args, loc, call_flags))
             | _ -> None in
           begin
             match ComplexExpressions.exp_to_string_map_dexp map_dexp node' e with