From 30b74413a55a0ee701cdb94f148293e663ada3fa Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Wed, 18 Dec 2019 09:32:46 -0800
Subject: [PATCH] [SIL] move some printing stuff to Exp

Summary: Sil.ml contained utility that belong in Exp.ml.

Reviewed By: ngorogiannis

Differential Revision: D19158533

fbshipit-source-id: 364c3f350
---
 infer/src/IR/Exp.ml                     | 48 +++++++++++++
 infer/src/IR/Exp.mli                    | 17 ++++-
 infer/src/IR/Sil.ml                     | 96 ++++++-------------------
 infer/src/IR/Sil.mli                    | 18 -----
 infer/src/backend/errdesc.ml            | 86 +++++++++++-----------
 infer/src/biabduction/Absarray.ml       |  6 +-
 infer/src/biabduction/BuiltinDefn.ml    |  2 +-
 infer/src/biabduction/Dom.ml            | 30 ++++----
 infer/src/biabduction/DotBiabduction.ml | 35 +++++----
 infer/src/biabduction/Match.ml          |  6 +-
 infer/src/biabduction/Prop.ml           |  6 +-
 infer/src/biabduction/Prover.ml         | 16 ++---
 infer/src/biabduction/Rearrange.ml      | 26 +++----
 infer/src/biabduction/SymExec.ml        | 10 +--
 infer/src/biabduction/Tabulation.ml     | 14 ++--
 15 files changed, 204 insertions(+), 212 deletions(-)

diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml
index 3eb12ef5a..5d76a5284 100644
--- a/infer/src/IR/Exp.ml
+++ b/infer/src/IR/Exp.ml
@@ -11,6 +11,7 @@
 open! IStd
 module Hashtbl = Caml.Hashtbl
 module F = Format
+module L = Logging
 
 (* reverse the natural order on Var *)
 type ident_ = Ident.t
@@ -271,6 +272,53 @@ let pp f e = pp_printenv ~print_types:false Pp.text f e
 
 let to_string e = F.asprintf "%a" pp e
 
+let color_wrapper ~f = if Config.print_using_diff then Pp.color_wrapper ~f else f
+
+let pp_diff ?(print_types = false) =
+  color_wrapper ~f:(fun pe f e0 ->
+      let e =
+        match pe.Pp.obj_sub with
+        | Some sub ->
+            (* apply object substitution to expression *) Obj.obj (sub (Obj.repr e0))
+        | None ->
+            e0
+      in
+      if not (equal e0 e) then match e with Lvar pvar -> Pvar.pp_value f pvar | _ -> assert false
+      else pp_printenv ~print_types pe f e )
+
+
+(** dump an expression. *)
+let d_exp (e : t) = L.d_pp_with_pe pp_diff e
+
+(** Pretty print a list of expressions. *)
+let pp_list pe f expl = Pp.seq (pp_diff pe) f expl
+
+(** dump a list of expressions. *)
+let d_list (el : t list) = L.d_pp_with_pe pp_list el
+
+let pp_texp pe f = function
+  | Sizeof {typ; nbytes; dynamic_length; subtype} ->
+      let pp_len f l = Option.iter ~f:(F.fprintf f "[%a]" (pp_diff pe)) l in
+      let pp_size f size = Option.iter ~f:(Int.pp f) size in
+      F.fprintf f "%a%a%a%a" (Typ.pp pe) typ pp_size nbytes pp_len dynamic_length Subtype.pp subtype
+  | e ->
+      pp_diff pe f e
+
+
+(** Pretty print a type with all the details. *)
+let pp_texp_full pe f = function
+  | Sizeof {typ; nbytes; dynamic_length; subtype} ->
+      let pp_len f l = Option.iter ~f:(F.fprintf f "[%a]" (pp_diff pe)) l in
+      let pp_size f size = Option.iter ~f:(Int.pp f) size in
+      F.fprintf f "%a%a%a%a" (Typ.pp_full pe) typ pp_size nbytes pp_len dynamic_length Subtype.pp
+        subtype
+  | e ->
+      pp_diff ~print_types:true pe f e
+
+
+(** Dump a type expression with all the details. *)
+let d_texp_full (te : t) = L.d_pp_with_pe pp_texp_full te
+
 let is_objc_block_closure = function
   | Closure {name} ->
       Typ.Procname.is_objc_block name
diff --git a/infer/src/IR/Exp.mli b/infer/src/IR/Exp.mli
index 4c72e6f90..0e1c2715e 100644
--- a/infer/src/IR/Exp.mli
+++ b/infer/src/IR/Exp.mli
@@ -138,12 +138,27 @@ val rename_pvars : f:(string -> string) -> t -> t
 val fold_captured : f:('a -> t -> 'a) -> t -> 'a -> 'a
 (** Fold over the expressions captured by this expression. *)
 
-val pp_printenv : print_types:bool -> Pp.env -> F.formatter -> t -> unit
+val pp_diff : ?print_types:bool -> Pp.env -> F.formatter -> t -> unit
 
 val pp : F.formatter -> t -> unit
 
 val to_string : t -> string
 
+val d_exp : t -> unit
+(** dump an expression. *)
+
+val pp_texp : Pp.env -> F.formatter -> t -> unit
+(** Pretty print a type. *)
+
+val pp_texp_full : Pp.env -> F.formatter -> t -> unit
+(** Pretty print a type with all the details. *)
+
+val d_texp_full : t -> unit
+(** Dump a type expression with all the details. *)
+
+val d_list : t list -> unit
+(** Dump a list of expressions. *)
+
 val is_objc_block_closure : t -> bool
 
 val zero_of_type : Typ.t -> t option
diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml
index c4a07b9db..885f9ab38 100644
--- a/infer/src/IR/Sil.ml
+++ b/infer/src/IR/Sil.ml
@@ -239,59 +239,12 @@ let pp_seq_diff pp print_env fmt l =
   else Pp.comma_seq ~print_env pp fmt l
 
 
-(** Pretty print an expression. *)
-let pp_exp_printenv ?(print_types = false) =
-  color_wrapper ~f:(fun pe f e0 ->
-      let e =
-        match pe.Pp.obj_sub with
-        | Some sub ->
-            (* apply object substitution to expression *) Obj.obj (sub (Obj.repr e0))
-        | None ->
-            e0
-      in
-      if not (Exp.equal e0 e) then
-        match e with Exp.Lvar pvar -> Pvar.pp_value f pvar | _ -> assert false
-      else Exp.pp_printenv ~print_types pe f e )
-
-
-(** dump an expression. *)
-let d_exp (e : Exp.t) = L.d_pp_with_pe pp_exp_printenv e
-
-(** Pretty print a list of expressions. *)
-let pp_exp_list pe f expl = Pp.seq (pp_exp_printenv pe) f expl
-
-(** dump a list of expressions. *)
-let d_exp_list (el : Exp.t list) = L.d_pp_with_pe pp_exp_list el
-
-let pp_texp pe f = function
-  | Exp.Sizeof {typ; nbytes; dynamic_length; subtype} ->
-      let pp_len f l = Option.iter ~f:(F.fprintf f "[%a]" (pp_exp_printenv pe)) l in
-      let pp_size f size = Option.iter ~f:(Int.pp f) size in
-      F.fprintf f "%a%a%a%a" (Typ.pp pe) typ pp_size nbytes pp_len dynamic_length Subtype.pp subtype
-  | e ->
-      pp_exp_printenv pe f e
-
-
-(** Pretty print a type with all the details. *)
-let pp_texp_full pe f = function
-  | Exp.Sizeof {typ; nbytes; dynamic_length; subtype} ->
-      let pp_len f l = Option.iter ~f:(F.fprintf f "[%a]" (pp_exp_printenv pe)) l in
-      let pp_size f size = Option.iter ~f:(Int.pp f) size in
-      F.fprintf f "%a%a%a%a" (Typ.pp_full pe) typ pp_size nbytes pp_len dynamic_length Subtype.pp
-        subtype
-  | e ->
-      Exp.pp_printenv ~print_types:true pe f e
-
-
-(** Dump a type expression with all the details. *)
-let d_texp_full (te : Exp.t) = L.d_pp_with_pe pp_texp_full te
-
 (** Pretty print an offset *)
 let pp_offset pe f = function
   | Off_fld (fld, _) ->
       Typ.Fieldname.pp f fld
   | Off_index exp ->
-      (pp_exp_printenv pe) f exp
+      (Exp.pp_diff pe) f exp
 
 
 (** Pretty print a list of offsets *)
@@ -307,7 +260,7 @@ let rec pp_offset_list pe f = function
 (** Dump a list of offsets *)
 let d_offset_list (offl : offset list) = L.d_pp_with_pe pp_offset_list offl
 
-let pp_exp_typ pe f (e, t) = F.fprintf f "%a:%a" (pp_exp_printenv pe) e (Typ.pp pe) t
+let pp_exp_typ pe f (e, t) = F.fprintf f "%a:%a" (Exp.pp_diff pe) e (Typ.pp pe) t
 
 let location_of_instr_metadata = function
   | Abstract loc | ExitScope (_, loc) | Nullify (_, loc) | VariableLifetimeBegins (_, _, loc) ->
@@ -391,17 +344,17 @@ let pp_instr ~print_types pe0 f instr =
   color_wrapper pe0 f instr ~f:(fun pe f instr ->
       match instr with
       | Load {id; e; root_typ; typ; loc} ->
-          F.fprintf f "%a=*%a:%a%t [%a]" Ident.pp id (pp_exp_printenv ~print_types pe) e
-            (pp_typ pe0) typ (pp_root ~typ ~root_typ) Location.pp loc
+          F.fprintf f "%a=*%a:%a%t [%a]" Ident.pp id (Exp.pp_diff ~print_types pe) e (pp_typ pe0)
+            typ (pp_root ~typ ~root_typ) Location.pp loc
       | Store {e1; root_typ; typ; e2; loc} ->
-          F.fprintf f "*%a:%a%t=%a [%a]" (pp_exp_printenv ~print_types pe) e1 (pp_typ pe0) root_typ
-            (pp_root ~typ ~root_typ) (pp_exp_printenv ~print_types pe) e2 Location.pp loc
+          F.fprintf f "*%a:%a%t=%a [%a]" (Exp.pp_diff ~print_types pe) e1 (pp_typ pe0) root_typ
+            (pp_root ~typ ~root_typ) (Exp.pp_diff ~print_types pe) e2 Location.pp loc
       | Prune (cond, loc, true_branch, _) ->
-          F.fprintf f "PRUNE(%a, %b); [%a]" (pp_exp_printenv ~print_types pe) cond true_branch
+          F.fprintf f "PRUNE(%a, %b); [%a]" (Exp.pp_diff ~print_types pe) cond true_branch
             Location.pp loc
       | Call ((id, _), e, arg_ts, loc, cf) ->
           F.fprintf f "%a=" Ident.pp id ;
-          F.fprintf f "%a(%a)%a [%a]" (pp_exp_printenv ~print_types pe) e
+          F.fprintf f "%a(%a)%a [%a]" (Exp.pp_diff ~print_types pe) e
             (Pp.comma_seq (pp_exp_typ pe))
             arg_ts CallFlags.pp cf Location.pp loc
       | Metadata metadata ->
@@ -433,15 +386,15 @@ let pp_atom =
   color_wrapper ~f:(fun pe f a ->
       match a with
       | Aeq (BinOp (op, e1, e2), Const (Cint i)) when IntLit.isone i ->
-          (pp_exp_printenv pe) f (Exp.BinOp (op, e1, e2))
+          (Exp.pp_diff pe) f (Exp.BinOp (op, e1, e2))
       | Aeq (e1, e2) ->
-          F.fprintf f "%a = %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2
+          F.fprintf f "%a = %a" (Exp.pp_diff pe) e1 (Exp.pp_diff pe) e2
       | Aneq (e1, e2) ->
-          F.fprintf f "%a != %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2
+          F.fprintf f "%a != %a" (Exp.pp_diff pe) e1 (Exp.pp_diff pe) e2
       | Apred (a, es) ->
-          F.fprintf f "%s(%a)" (PredSymb.to_string pe a) (Pp.comma_seq (pp_exp_printenv pe)) es
+          F.fprintf f "%s(%a)" (PredSymb.to_string pe a) (Pp.comma_seq (Exp.pp_diff pe)) es
       | Anpred (a, es) ->
-          F.fprintf f "!%s(%a)" (PredSymb.to_string pe a) (Pp.comma_seq (pp_exp_printenv pe)) es )
+          F.fprintf f "!%s(%a)" (PredSymb.to_string pe a) (Pp.comma_seq (Exp.pp_diff pe)) es )
 
 
 (** dump an atom *)
@@ -585,7 +538,7 @@ end = struct
 end
 
 let pp_texp_simple pe =
-  match pe.Pp.opt with SIM_DEFAULT -> pp_texp pe | SIM_WITH_TYP -> pp_texp_full pe
+  match pe.Pp.opt with SIM_DEFAULT -> Exp.pp_texp pe | SIM_WITH_TYP -> Exp.pp_texp_full pe
 
 
 let inst_actual_precondition = Iactual_precondition
@@ -787,15 +740,13 @@ let rec pp_sexp_env pe0 envo f se =
   color_wrapper pe0 f se ~f:(fun pe f se ->
       match se with
       | Eexp (e, inst) ->
-          F.fprintf f "%a%a" (pp_exp_printenv pe) e (pp_inst_if_trace pe) inst
+          F.fprintf f "%a%a" (Exp.pp_diff pe) e (pp_inst_if_trace pe) inst
       | Estruct (fel, inst) ->
           let pp_diff f (n, se) = F.fprintf f "%a:%a" Typ.Fieldname.pp n (pp_sexp_env pe envo) se in
           F.fprintf f "{%a}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst
       | Earray (len, nel, inst) ->
-          let pp_diff f (i, se) =
-            F.fprintf f "%a:%a" (pp_exp_printenv pe) i (pp_sexp_env pe envo) se
-          in
-          F.fprintf f "[%a|%a]%a" (pp_exp_printenv pe) len (pp_seq_diff pp_diff pe) nel
+          let pp_diff f (i, se) = F.fprintf f "%a:%a" (Exp.pp_diff pe) i (pp_sexp_env pe envo) se in
+          F.fprintf f "[%a|%a]%a" (Exp.pp_diff pe) len (pp_seq_diff pp_diff pe) nel
             (pp_inst_if_trace pe) inst )
 
 
@@ -811,17 +762,16 @@ let rec pp_hpred_env pe0 envo f hpred =
             | _ ->
                 pe
           in
-          F.fprintf f "%a|->%a:%a" (pp_exp_printenv pe') e (pp_sexp_env pe' envo) se
+          F.fprintf f "%a|->%a:%a" (Exp.pp_diff pe') e (pp_sexp_env pe' envo) se
             (pp_texp_simple pe') te
       | Hlseg (k, hpara, e1, e2, elist) ->
-          F.fprintf f "lseg%a(%a,%a,[%a],%a)" pp_lseg_kind k (pp_exp_printenv pe) e1
-            (pp_exp_printenv pe) e2
-            (Pp.comma_seq (pp_exp_printenv pe))
+          F.fprintf f "lseg%a(%a,%a,[%a],%a)" pp_lseg_kind k (Exp.pp_diff pe) e1 (Exp.pp_diff pe) e2
+            (Pp.comma_seq (Exp.pp_diff pe))
             elist (pp_hpara_env pe envo) hpara
       | Hdllseg (k, hpara_dll, iF, oB, oF, iB, elist) ->
-          F.fprintf f "dllseg%a(%a,%a,%a,%a,[%a],%a)" pp_lseg_kind k (pp_exp_printenv pe) iF
-            (pp_exp_printenv pe) oB (pp_exp_printenv pe) oF (pp_exp_printenv pe) iB
-            (Pp.comma_seq (pp_exp_printenv pe))
+          F.fprintf f "dllseg%a(%a,%a,%a,%a,[%a],%a)" pp_lseg_kind k (Exp.pp_diff pe) iF
+            (Exp.pp_diff pe) oB (Exp.pp_diff pe) oF (Exp.pp_diff pe) iB
+            (Pp.comma_seq (Exp.pp_diff pe))
             elist (pp_hpara_dll_env pe envo) hpara_dll )
 
 
diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli
index e29cf2219..baebd5e7e 100644
--- a/infer/src/IR/Sil.mli
+++ b/infer/src/IR/Sil.mli
@@ -259,24 +259,6 @@ val add_with_block_parameters_flag : instr -> instr
 
 (** {2 Pretty Printing} *)
 
-val pp_exp_printenv : ?print_types:bool -> Pp.env -> F.formatter -> Exp.t -> unit
-(** Pretty print an expression. *)
-
-val d_exp : Exp.t -> unit
-(** dump an expression. *)
-
-val pp_texp : Pp.env -> F.formatter -> Exp.t -> unit
-(** Pretty print a type. *)
-
-val pp_texp_full : Pp.env -> F.formatter -> Exp.t -> unit
-(** Pretty print a type with all the details. *)
-
-val d_texp_full : Exp.t -> unit
-(** Dump a type expression with all the details. *)
-
-val d_exp_list : Exp.t list -> unit
-(** Dump a list of expressions. *)
-
 val pp_offset : Pp.env -> F.formatter -> offset -> unit
 
 val d_offset_list : offset list -> unit
diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml
index a897f1a12..df403ab3d 100644
--- a/infer/src/backend/errdesc.ml
+++ b/infer/src/backend/errdesc.ml
@@ -162,21 +162,21 @@ let rec find_normal_variable_load_ tenv (seen : Exp.Set.t) node id : DExp.t opti
     | Sil.Load {id= id0; e} when Ident.equal id id0 ->
         if verbose then (
           L.d_str "find_normal_variable_load defining " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         exp_lv_dexp_ tenv seen node e
     | Sil.Call ((id0, _), Exp.Const (Const.Cfun pn), (e, _) :: _, _, _)
       when Ident.equal id id0 && Typ.Procname.equal pn (Typ.Procname.from_string_c_fun "__cast") ->
         if verbose then (
           L.d_str "find_normal_variable_load cast on " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         exp_rv_dexp_ tenv seen node e
     | Sil.Call ((id0, _), (Exp.Const (Const.Cfun pname) as fun_exp), args, loc, call_flags)
       when Ident.equal id id0 ->
         if verbose then (
           L.d_str "find_normal_variable_load function call " ;
-          Sil.d_exp fun_exp ;
+          Exp.d_exp fun_exp ;
           L.d_ln () ) ;
         let fun_dexp = DExp.Dconst (Const.Cfun pname) in
         let args_dexp =
@@ -209,19 +209,19 @@ let rec find_normal_variable_load_ tenv (seen : Exp.Set.t) node id : DExp.t opti
 and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
   if Exp.Set.mem e seen_ then (
     L.d_str "exp_lv_dexp: cycle detected" ;
-    Sil.d_exp e ;
+    Exp.d_exp e ;
     L.d_ln () ;
     None )
   else
     let seen = Exp.Set.add e seen_ in
     match Prop.exp_normalize_noabs tenv Sil.sub_empty e with
     | Exp.Const c ->
-        if verbose then (L.d_str "exp_lv_dexp: constant " ; Sil.d_exp e ; L.d_ln ()) ;
+        if verbose then (L.d_str "exp_lv_dexp: constant " ; Exp.d_exp e ; L.d_ln ()) ;
         Some (DExp.Dderef (DExp.Dconst c))
     | Exp.BinOp (Binop.PlusPI, e1, e2) -> (
         if verbose then (
           L.d_str "exp_lv_dexp: (e1 +PI e2) " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         match (exp_lv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with
         | Some de1, Some de2 ->
@@ -231,7 +231,7 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
     | Exp.Var id when Ident.is_normal id -> (
         if verbose then (
           L.d_str "exp_lv_dexp: normal var " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         match find_normal_variable_load_ tenv seen node id with
         | None ->
@@ -241,7 +241,7 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
     | Exp.Lvar pvar ->
         if verbose then (
           L.d_str "exp_lv_dexp: program var " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         if Pvar.is_frontend_tmp pvar then
           match find_program_variable_assignment node pvar with
@@ -267,7 +267,7 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
     | Exp.Lfield (Exp.Var id, f, _) when Ident.is_normal id -> (
         if verbose then (
           L.d_str "exp_lv_dexp: Lfield with var " ;
-          Sil.d_exp (Exp.Var id) ;
+          Exp.d_exp (Exp.Var id) ;
           L.d_printfln " %a" Typ.Fieldname.pp f ) ;
         match find_normal_variable_load_ tenv seen node id with
         | None ->
@@ -277,7 +277,7 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
     | Exp.Lfield (e1, f, _) -> (
         if verbose then (
           L.d_str "exp_lv_dexp: Lfield " ;
-          Sil.d_exp e1 ;
+          Exp.d_exp e1 ;
           L.d_printfln " %a" Typ.Fieldname.pp f ) ;
         match exp_lv_dexp_ tenv seen node e1 with
         | None ->
@@ -286,7 +286,7 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
             Some (DExp.Ddot (de, f)) )
     | Exp.Lindex (e1, e2) -> (
         if verbose then (
-          L.d_str "exp_lv_dexp: Lindex " ; Sil.d_exp e1 ; L.d_str " " ; Sil.d_exp e2 ; L.d_ln () ) ;
+          L.d_str "exp_lv_dexp: Lindex " ; Exp.d_exp e1 ; L.d_str " " ; Exp.d_exp e2 ; L.d_ln () ) ;
         match (exp_lv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with
         | None, _ ->
             None
@@ -298,7 +298,7 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
     | _ ->
         if verbose then (
           L.d_str "exp_lv_dexp: no match for  " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         None
 
@@ -307,19 +307,19 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
 and exp_rv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
   if Exp.Set.mem e seen_ then (
     L.d_str "exp_rv_dexp: cycle detected" ;
-    Sil.d_exp e ;
+    Exp.d_exp e ;
     L.d_ln () ;
     None )
   else
     let seen = Exp.Set.add e seen_ in
     match e with
     | Exp.Const c ->
-        if verbose then (L.d_str "exp_rv_dexp: constant " ; Sil.d_exp e ; L.d_ln ()) ;
+        if verbose then (L.d_str "exp_rv_dexp: constant " ; Exp.d_exp e ; L.d_ln ()) ;
         Some (DExp.Dconst c)
     | Exp.Lvar pv ->
         if verbose then (
           L.d_str "exp_rv_dexp: program var " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         if Pvar.is_frontend_tmp pv then
           exp_lv_dexp_ tenv seen_ (* avoid spurious cycle detection *) node e
@@ -327,13 +327,13 @@ and exp_rv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
     | Exp.Var id when Ident.is_normal id ->
         if verbose then (
           L.d_str "exp_rv_dexp: normal var " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         find_normal_variable_load_ tenv seen node id
     | Exp.Lfield (e1, f, _) -> (
         if verbose then (
           L.d_str "exp_rv_dexp: Lfield " ;
-          Sil.d_exp e1 ;
+          Exp.d_exp e1 ;
           L.d_printfln " %a" Typ.Fieldname.pp f ) ;
         match exp_rv_dexp_ tenv seen node e1 with
         | None ->
@@ -342,37 +342,37 @@ and exp_rv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
             Some (DExp.Ddot (de, f)) )
     | Exp.Lindex (e1, e2) -> (
         if verbose then (
-          L.d_str "exp_rv_dexp: Lindex " ; Sil.d_exp e1 ; L.d_str " " ; Sil.d_exp e2 ; L.d_ln () ) ;
+          L.d_str "exp_rv_dexp: Lindex " ; Exp.d_exp e1 ; L.d_str " " ; Exp.d_exp e2 ; L.d_ln () ) ;
         match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with
         | None, _ | _, None ->
             None
         | Some de1, Some de2 ->
             Some (DExp.Darray (de1, de2)) )
     | Exp.BinOp (op, e1, e2) -> (
-        if verbose then (L.d_str "exp_rv_dexp: BinOp " ; Sil.d_exp e ; L.d_ln ()) ;
+        if verbose then (L.d_str "exp_rv_dexp: BinOp " ; Exp.d_exp e ; L.d_ln ()) ;
         match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with
         | None, _ | _, None ->
             None
         | Some de1, Some de2 ->
             Some (DExp.Dbinop (op, de1, de2)) )
     | Exp.UnOp (op, e1, _) -> (
-        if verbose then (L.d_str "exp_rv_dexp: UnOp " ; Sil.d_exp e ; L.d_ln ()) ;
+        if verbose then (L.d_str "exp_rv_dexp: UnOp " ; Exp.d_exp e ; L.d_ln ()) ;
         match exp_rv_dexp_ tenv seen node e1 with
         | None ->
             None
         | Some de1 ->
             Some (DExp.Dunop (op, de1)) )
     | Exp.Cast (_, e1) ->
-        if verbose then (L.d_str "exp_rv_dexp: Cast " ; Sil.d_exp e ; L.d_ln ()) ;
+        if verbose then (L.d_str "exp_rv_dexp: Cast " ; Exp.d_exp e ; L.d_ln ()) ;
         exp_rv_dexp_ tenv seen node e1
     | Exp.Sizeof {typ; dynamic_length; subtype} ->
-        if verbose then (L.d_str "exp_rv_dexp: type " ; Sil.d_exp e ; L.d_ln ()) ;
+        if verbose then (L.d_str "exp_rv_dexp: type " ; Exp.d_exp e ; L.d_ln ()) ;
         Some
           (DExp.Dsizeof (typ, Option.bind dynamic_length ~f:(exp_rv_dexp_ tenv seen node), subtype))
     | _ ->
         if verbose then (
           L.d_str "exp_rv_dexp: no match for  " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         None
 
@@ -429,7 +429,7 @@ let leak_from_list_abstraction hpred prop =
       Sil.Predicates.iter env (check_hpara texp) (check_hpara_dll texp) ;
       if !found then (
         L.d_str "leak_from_list_abstraction of predicate of type " ;
-        Sil.d_texp_full texp ;
+        Exp.d_texp_full texp ;
         L.d_ln () ) ;
       !found
   | None ->
@@ -534,7 +534,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
     | Some (Sil.Store {e1= lexp}) when is_none vpath -> (
         if verbose then (
           L.d_str "explain_leak: current instruction Set for " ;
-          Sil.d_exp lexp ;
+          Exp.d_exp lexp ;
           L.d_ln () ) ;
         match exp_lv_dexp tenv node lexp with
         | Some dexp when not (DExp.has_tmp_var dexp) ->
@@ -567,7 +567,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 tenv 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 ()) ;
+  if verbose then (L.d_str "in vpath_find exp:" ; Exp.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
@@ -597,7 +597,7 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
           | lexp ->
               if verbose then (
                 L.d_str "vpath_find do_fse: no match on Eexp " ;
-                Sil.d_exp lexp ;
+                Exp.d_exp lexp ;
                 L.d_ln () ) )
       | _ ->
           ()
@@ -619,7 +619,7 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
           | lexp ->
               if verbose then (
                 L.d_str "vpath_find do_sexp: no match on Eexp " ;
-                Sil.d_exp lexp ;
+                Exp.d_exp lexp ;
                 L.d_ln () ) ;
               (None, None) )
       | Sil.Estruct (fsel, _) ->
@@ -664,7 +664,7 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
     match res with
     | None, _ ->
         L.d_str "vpath_find: cannot find " ;
-        Sil.d_exp exp_ ;
+        Exp.d_exp exp_ ;
         L.d_ln ()
     | Some de, typo -> (
         L.d_printf "vpath_find: found %a :" DExp.pp de ;
@@ -725,7 +725,7 @@ let explain_dexp_access prop dexp is_nullable =
     | [] ->
         if verbose then (
           L.d_str "lookup_esel: can't find index " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         None
     | (e1, se) :: esel' ->
@@ -886,50 +886,50 @@ let rec find_outermost_dereference tenv node e =
   | Exp.Const _ ->
       if verbose then (
         L.d_str "find_outermost_dereference: constant " ;
-        Sil.d_exp e ;
+        Exp.d_exp e ;
         L.d_ln () ) ;
       exp_lv_dexp tenv node e
   | Exp.Var id when Ident.is_normal id ->
       (* look up the normal variable declaration *)
       if verbose then (
         L.d_str "find_outermost_dereference: normal var " ;
-        Sil.d_exp e ;
+        Exp.d_exp e ;
         L.d_ln () ) ;
       find_normal_variable_load tenv node id
   | Exp.Lfield (e', _, _) ->
       if verbose then (
         L.d_str "find_outermost_dereference: Lfield " ;
-        Sil.d_exp e ;
+        Exp.d_exp e ;
         L.d_ln () ) ;
       find_outermost_dereference tenv node e'
   | Exp.Lindex (e', _) ->
       if verbose then (
         L.d_str "find_outermost_dereference: Lindex " ;
-        Sil.d_exp e ;
+        Exp.d_exp e ;
         L.d_ln () ) ;
       find_outermost_dereference tenv node e'
   | Exp.Lvar _ ->
       if verbose then (
         L.d_str "find_outermost_dereference: Lvar " ;
-        Sil.d_exp e ;
+        Exp.d_exp e ;
         L.d_ln () ) ;
       exp_lv_dexp tenv node e
   | Exp.BinOp (Binop.PlusPI, Exp.Lvar _, _) ->
       if verbose then (
         L.d_str "find_outermost_dereference: Lvar+index " ;
-        Sil.d_exp e ;
+        Exp.d_exp e ;
         L.d_ln () ) ;
       exp_lv_dexp tenv node e
   | Exp.Cast (_, e') ->
       if verbose then (
         L.d_str "find_outermost_dereference: cast " ;
-        Sil.d_exp e ;
+        Exp.d_exp e ;
         L.d_ln () ) ;
       find_outermost_dereference tenv node e'
   | _ ->
       if verbose then (
         L.d_str "find_outermost_dereference: no match for " ;
-        Sil.d_exp e ;
+        Exp.d_exp e ;
         L.d_ln () ) ;
       None
 
@@ -946,13 +946,13 @@ let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = fa
     | Some (Sil.Store {e1= e}) ->
         if verbose then (
           L.d_str "explain_dereference Sil.Store " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         Some e
     | Some (Sil.Load {e}) ->
         if verbose then (
           L.d_str "explain_dereference Binop.Leteref " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         Some e
     | Some (Sil.Call (_, Exp.Const (Const.Cfun fn), [(e, _)], _, _))
@@ -960,13 +960,13 @@ let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = fa
              [BuiltinDecl.free; BuiltinDecl.__delete; BuiltinDecl.__delete_array] ->
         if verbose then (
           L.d_str "explain_dereference Sil.Call " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         Some e
     | Some (Sil.Call (_, (Exp.Var _ as e), _, _, _)) ->
         if verbose then (
           L.d_str "explain_dereference Sil.Call " ;
-          Sil.d_exp e ;
+          Exp.d_exp e ;
           L.d_ln () ) ;
         Some e
     | _ ->
@@ -1106,7 +1106,7 @@ let explain_dereference_as_caller_expression proc_name tenv ?(use_buckets = fals
   | None ->
       if verbose then (
         L.d_str "explain_dereference_as_caller_expression " ;
-        Sil.d_exp exp ;
+        Exp.d_exp exp ;
         L.d_strln ": cannot explain None" ) ;
       Localise.no_desc
 
diff --git a/infer/src/biabduction/Absarray.ml b/infer/src/biabduction/Absarray.ml
index 804c1c89f..5d07ce8a3 100644
--- a/infer/src/biabduction/Absarray.ml
+++ b/infer/src/biabduction/Absarray.ml
@@ -522,7 +522,7 @@ let strexp_do_abstract tenv footprint_part p ((path, se_in, _) : StrexpMatch.str
     (p3, changed2 || changed3)
   in
   let prune_and_blur_indices =
-    prune_and_blur Sil.d_exp_list (keep_only_indices tenv) (blur_array_indices tenv)
+    prune_and_blur Exp.d_list (keep_only_indices tenv) (blur_array_indices tenv)
   in
   let partition_abstract should_keep abstract ksel default_keys =
     let keep_ksel, remove_ksel = List.partition_tf ~f:should_keep ksel in
@@ -565,7 +565,7 @@ let strexp_do_abstract tenv footprint_part p ((path, se_in, _) : StrexpMatch.str
           false
     in
     let abstract = prune_and_blur_indices path in
-    filter_abstract Sil.d_exp_list should_keep abstract esel []
+    filter_abstract Exp.d_list should_keep abstract esel []
   in
   let do_reexecution () =
     match se_in with Sil.Earray (_, esel, _) -> do_array_reexecution esel | _ -> assert false
@@ -655,7 +655,7 @@ let remove_redundant_elements tenv prop =
   let filter_redundant_e_se fp_part (e, se) =
     let remove () =
       L.d_strln "kill_redundant: removing " ;
-      Sil.d_exp e ;
+      Exp.d_exp e ;
       L.d_str " " ;
       Sil.d_sexp se ;
       L.d_ln () ;
diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml
index 9705b1c6f..63ac1d524 100644
--- a/infer/src/biabduction/BuiltinDefn.ml
+++ b/infer/src/biabduction/BuiltinDefn.ml
@@ -654,7 +654,7 @@ let execute_pthread_create ({Builtin.tenv; summary; prop_; path; args; exe_env}
       match pname with
       | None ->
           L.d_str "pthread_create: unknown function " ;
-          Sil.d_exp routine_name ;
+          Exp.d_exp routine_name ;
           L.d_strln ", skipping call." ;
           [(prop_, path)]
       | Some pname -> (
diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml
index 06643fa31..5dbf60c08 100644
--- a/infer/src/biabduction/Dom.ml
+++ b/infer/src/biabduction/Dom.ml
@@ -244,9 +244,9 @@ module CheckJoinPre : InfoLossCheckerSig = struct
           let r = List.exists ~f:(fun e' -> not (Dangling.check side_op e')) es in
           if r then (
             L.d_str ".... Dangling Check (dang e:" ;
-            Sil.d_exp e ;
+            Exp.d_exp e ;
             L.d_str ") (? es:" ;
-            Sil.d_exp_list es ;
+            Exp.d_list es ;
             L.d_strln ") ...." ;
             L.d_ln () ) ;
           r )
@@ -254,9 +254,9 @@ module CheckJoinPre : InfoLossCheckerSig = struct
           let r = List.exists ~f:(Dangling.check side_op) es in
           if r then (
             L.d_str ".... Dangling Check (notdang e:" ;
-            Sil.d_exp e ;
+            Exp.d_exp e ;
             L.d_str ") (? es:" ;
-            Sil.d_exp_list es ;
+            Exp.d_list es ;
             L.d_strln ") ...." ;
             L.d_ln () ) ;
           r
@@ -568,7 +568,7 @@ end = struct
             List.map ~f:(fun (e1, e2, _) -> select side_op e1 e2) assoc
         | _ ->
             L.d_str "no pattern match in check lost_little e: " ;
-            Sil.d_exp e ;
+            Exp.d_exp e ;
             L.d_ln () ;
             raise Sil.JoinFail
       in
@@ -750,7 +750,7 @@ end = struct
 
   let get_other_atoms tenv side atom_in =
     let build_other_atoms construct side e =
-      if Config.trace_join then (L.d_str "build_other_atoms: " ; Sil.d_exp e ; L.d_ln ()) ;
+      if Config.trace_join then (L.d_str "build_other_atoms: " ; Exp.d_exp e ; L.d_ln ()) ;
       let others1 = get_others_direct_or_induced side e in
       let others2 = match others1 with None -> get_others_deep side e | Some _ -> others1 in
       match others2 with
@@ -968,7 +968,7 @@ let const_partial_join c1 c2 =
 
 
 let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
-  (* L.d_str "exp_partial_join "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
+  (* L.d_str "exp_partial_join "; Exp.d_exp e1; L.d_str " "; Exp.d_exp e2; L.d_ln (); *)
   match (e1, e2) with
   | Exp.Var id1, Exp.Var id2 ->
       ident_partial_join id1 id2
@@ -1039,9 +1039,9 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
         ; subtype= Subtype.join st1 st2 }
   | _ ->
       L.d_str "exp_partial_join no match " ;
-      Sil.d_exp e1 ;
+      Exp.d_exp e1 ;
       L.d_str " " ;
-      Sil.d_exp e2 ;
+      Exp.d_exp e2 ;
       L.d_ln () ;
       raise Sil.JoinFail
 
@@ -1525,11 +1525,11 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop
     if Config.trace_join then (
       L.d_strln ".... sigma_partial_join' ...." ;
       L.d_str "TODO: " ;
-      Sil.d_exp e1 ;
+      Exp.d_exp e1 ;
       L.d_str "," ;
-      Sil.d_exp e2 ;
+      Exp.d_exp e2 ;
       L.d_str "," ;
-      Sil.d_exp e ;
+      Exp.d_exp e ;
       L.d_ln () ;
       L.d_strln "SIGMA1 =" ;
       Prop.d_sigma sigma1_in ;
@@ -1628,11 +1628,11 @@ let rec sigma_partial_meet' tenv (sigma_acc : Prop.sigma) (sigma1_in : Prop.sigm
     let e1, e2, e = todo_curr in
     L.d_strln ".... sigma_partial_meet' ...." ;
     L.d_str "TODO: " ;
-    Sil.d_exp e1 ;
+    Exp.d_exp e1 ;
     L.d_str "," ;
-    Sil.d_exp e2 ;
+    Exp.d_exp e2 ;
     L.d_str "," ;
-    Sil.d_exp e ;
+    Exp.d_exp e ;
     L.d_ln () ;
     L.d_str "PROP1=" ;
     Prop.d_sigma sigma1_in ;
diff --git a/infer/src/biabduction/DotBiabduction.ml b/infer/src/biabduction/DotBiabduction.ml
index 9ecdb1f6a..8cdfe2611 100644
--- a/infer/src/biabduction/DotBiabduction.ml
+++ b/infer/src/biabduction/DotBiabduction.ml
@@ -132,11 +132,11 @@ let rec strexp_to_string pe coo f se =
   | Sil.Eexp (Exp.Var id, _) ->
       if !print_full_prop then Ident.pp f id else ()
   | Sil.Eexp (e, _) ->
-      if !print_full_prop then (Sil.pp_exp_printenv pe) f e else F.pp_print_char f '_'
+      if !print_full_prop then (Exp.pp_diff pe) f e else F.pp_print_char f '_'
   | Sil.Estruct (ls, _) ->
       F.fprintf f " STRUCT | { %a } " (struct_to_dotty_str pe coo) ls
   | Sil.Earray (e, idx, _) ->
-      F.fprintf f " ARRAY[%a] | { %a } " (Sil.pp_exp_printenv pe) e (get_contents pe coo) idx
+      F.fprintf f " ARRAY[%a] | { %a } " (Exp.pp_diff pe) e (get_contents pe coo) idx
 
 
 and struct_to_dotty_str pe coo f ls : unit =
@@ -154,20 +154,19 @@ and struct_to_dotty_str pe coo f ls : unit =
 and get_contents_sexp pe coo f se =
   match se with
   | Sil.Eexp (e', _) ->
-      (Sil.pp_exp_printenv pe) f e'
+      (Exp.pp_diff pe) f e'
   | Sil.Estruct (se', _) ->
       F.fprintf f "| { %a }" (struct_to_dotty_str pe coo) se'
   | Sil.Earray (e', [], _) ->
-      F.fprintf f "(ARRAY Size: %a) | { }" (Sil.pp_exp_printenv pe) e'
+      F.fprintf f "(ARRAY Size: %a) | { }" (Exp.pp_diff pe) e'
   | Sil.Earray (e', (idx, a) :: linner, _) ->
-      F.fprintf f "(ARRAY Size: %a) | { %a: %a | %a }" (Sil.pp_exp_printenv pe) e'
-        (Sil.pp_exp_printenv pe) idx (strexp_to_string pe coo) a (get_contents pe coo) linner
+      F.fprintf f "(ARRAY Size: %a) | { %a: %a | %a }" (Exp.pp_diff pe) e' (Exp.pp_diff pe) idx
+        (strexp_to_string pe coo) a (get_contents pe coo) linner
 
 
 and get_contents_single pe coo f (e, se) =
   let e_no_special_char = strip_special_chars (Exp.to_string e) in
-  F.fprintf f "{ <%s> %a : %a }" e_no_special_char (Sil.pp_exp_printenv pe) e
-    (get_contents_sexp pe coo) se
+  F.fprintf f "{ <%s> %a : %a }" e_no_special_char (Exp.pp_diff pe) e (get_contents_sexp pe coo) se
 
 
 and get_contents pe coo f = function
@@ -832,7 +831,7 @@ let rec print_struct f pe e te l coo c =
   if !print_full_prop then
     F.fprintf f
       " node [%s]; @\n struct%iL%i [label=\"{<%s%iL%i> STRUCT: %a } | %a\" ] fontcolor=%s@\n"
-      "shape=record" n lambda e_no_special_char n lambda (Sil.pp_exp_printenv pe) e
+      "shape=record" n lambda e_no_special_char n lambda (Exp.pp_diff pe) e
       (struct_to_dotty_str pe coo) l c
   else
     F.fprintf f
@@ -848,8 +847,7 @@ and print_array f pe e1 e2 l coo c =
   F.fprintf f "subgraph structs_%iL%i {@\n" n lambda ;
   F.fprintf f
     " node [%s]; @\n struct%iL%i [label=\"{<%s%iL%i> ARRAY| SIZE: %a } | %a\" ] fontcolor=%s@\n"
-    "shape=record" n lambda e_no_special_char n lambda (Sil.pp_exp_printenv pe) e2
-    (get_contents pe coo) l c ;
+    "shape=record" n lambda e_no_special_char n lambda (Exp.pp_diff pe) e2 (get_contents pe coo) l c ;
   F.fprintf f "}@\n"
 
 
@@ -866,7 +864,7 @@ and print_sll f pe nesting k e1 coo =
       F.fprintf f
         "subgraph cluster_%iL%i { %s node [style=filled,color=white];   label=\"list PE\";" n'
         lambda "style=filled; color=lightgrey;" ) ;
-  F.fprintf f "state%iL%i [label=\"%a\"]@\n" n lambda (Sil.pp_exp_printenv pe) e1 ;
+  F.fprintf f "state%iL%i [label=\"%a\"]@\n" n lambda (Exp.pp_diff pe) e1 ;
   let n' = !dotty_state_count in
   incr dotty_state_count ;
   F.fprintf f "state%iL%i [label=\"... \" style=filled color=lightgrey] @\n" n' lambda ;
@@ -892,13 +890,13 @@ and print_dll f pe nesting k e1 e4 coo =
   | Sil.Lseg_PE ->
       F.fprintf f "subgraph cluster_%iL%i { %s node [style=filled,color=white];  label=\"%s\";" n'
         lambda "style=filled; color=lightgrey;" "doubly-linked list PE" ) ;
-  F.fprintf f "state%iL%i [label=\"%a\"]@\n" n lambda (Sil.pp_exp_printenv pe) e1 ;
+  F.fprintf f "state%iL%i [label=\"%a\"]@\n" n lambda (Exp.pp_diff pe) e1 ;
   let n' = !dotty_state_count in
   incr dotty_state_count ;
   F.fprintf f "state%iL%i [label=\"... \" style=filled color=lightgrey] @\n" n' lambda ;
   F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]@\n" n lambda n' lambda ;
   F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]@\n" n' lambda n lambda ;
-  F.fprintf f "state%iL%i [label=\"%a\"]@\n" (n + 1) lambda (Sil.pp_exp_printenv pe) e4 ;
+  F.fprintf f "state%iL%i [label=\"%a\"]@\n" (n + 1) lambda (Exp.pp_diff pe) e4 ;
   F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]@\n" (n + 1) lambda n' lambda ;
   F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]}@\n" n' lambda (n + 1) lambda ;
   incr lambda_counter ;
@@ -914,9 +912,8 @@ and dotty_pp_state f pe cycle dotnode =
     let lambda = coo.lambda in
     if is_dangling then
       F.fprintf f "state%iL%i [label=\"%a \", color=red, style=dashed, fontcolor=%s]@\n" n lambda
-        (Sil.pp_exp_printenv pe) e c
-    else
-      F.fprintf f "state%iL%i [label=\"%a\" fontcolor=%s]@\n" n lambda (Sil.pp_exp_printenv pe) e c
+        (Exp.pp_diff pe) e c
+    else F.fprintf f "state%iL%i [label=\"%a\" fontcolor=%s]@\n" n lambda (Exp.pp_diff pe) e c
   in
   match dotnode with
   | Dotnil coo when !print_full_prop ->
@@ -948,10 +945,10 @@ and build_visual_graph f pe p cycle =
   compute_fields_struct sigma ;
   compute_struct_exp_nodes sigma ;
   (* L.out "@\n@\n Computed fields structs: ";
-     List.iter ~f:(fun e -> L.out " %a " (Sil.pp_exp_printenv pe) e) !fields_structs;
+     List.iter ~f:(fun e -> L.out " %a " (Exp.pp_diff pe) e) !fields_structs;
      L.out "@\n@.";
      L.out "@\n@\n Computed exp structs nodes: ";
-     List.iter ~f:(fun e -> L.out " %a " (Sil.pp_exp_printenv pe) e) !struct_exp_nodes;
+     List.iter ~f:(fun e -> L.out " %a " (Exp.pp_diff pe) e) !struct_exp_nodes;
      L.out "@\n@."; *)
   let sigma_lambda = List.map ~f:(fun hp -> (hp, !lambda_counter)) sigma in
   let nodes = dotty_mk_node pe sigma_lambda in
diff --git a/infer/src/biabduction/Match.ml b/infer/src/biabduction/Match.ml
index faa432d57..bb0d84ffa 100644
--- a/infer/src/biabduction/Match.ml
+++ b/infer/src/biabduction/Match.ml
@@ -153,9 +153,9 @@ and isel_match isel1 sub vars isel2 =
       if not sanity_check then (
         let pe = Pp.text in
         L.internal_error "@[.... Sanity Check Failure while Matching Index-Strexps ....@\n" ;
-        L.internal_error "@[<4>    IDX1: %a, STREXP1: %a@\n" (Sil.pp_exp_printenv pe) idx1
-          (Sil.pp_sexp pe) se1' ;
-        L.internal_error "@[<4>    IDX2: %a, STREXP2: %a@\n@." (Sil.pp_exp_printenv pe) idx2
+        L.internal_error "@[<4>    IDX1: %a, STREXP1: %a@\n" (Exp.pp_diff pe) idx1 (Sil.pp_sexp pe)
+          se1' ;
+        L.internal_error "@[<4>    IDX2: %a, STREXP2: %a@\n@." (Exp.pp_diff pe) idx2
           (Sil.pp_sexp pe) se2' ;
         assert false )
       else if Exp.equal idx1 idx2 then
diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml
index d7772848f..18b6ce0c2 100644
--- a/infer/src/biabduction/Prop.ml
+++ b/infer/src/biabduction/Prop.ml
@@ -108,7 +108,7 @@ let compare_prop p1 p2 = compare (fun _ _ -> 0) p1 p2
 (** {1 Functions for Pretty Printing} *)
 
 let pp_texp_simple pe =
-  match pe.Pp.opt with SIM_DEFAULT -> Sil.pp_texp pe | SIM_WITH_TYP -> Sil.pp_texp_full pe
+  match pe.Pp.opt with SIM_DEFAULT -> Exp.pp_texp pe | SIM_WITH_TYP -> Exp.pp_texp_full pe
 
 
 (** Pretty print a pointsto representing a stack variable as an equality *)
@@ -141,7 +141,7 @@ let d_sub (sub : Sil.subst) = L.d_pp_with_pe pp_sub sub
 let pp_sub_entry =
   Pp.color_wrapper ~f:(fun pe f entry ->
       let x, e = entry in
-      F.fprintf f "%a = %a" Ident.pp x (Sil.pp_exp_printenv pe) e )
+      F.fprintf f "%a = %a" Ident.pp x (Exp.pp_diff pe) e )
 
 
 (** Pretty print a substitution as a list of (ident,exp) pairs *)
@@ -1358,7 +1358,7 @@ module Normalize = struct
       | Var _ ->
           Estruct ([], inst)
       | te ->
-          L.internal_error "trying to create ptsto with type: %a@." (Sil.pp_texp_full Pp.text) te ;
+          L.internal_error "trying to create ptsto with type: %a@." (Exp.pp_texp_full Pp.text) te ;
           assert false
     in
     let strexp : Sil.strexp =
diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml
index b809e728a..b6425decd 100644
--- a/infer/src/biabduction/Prover.ml
+++ b/infer/src/biabduction/Prover.ml
@@ -1064,7 +1064,7 @@ exception MISSING_EXC of string
 type check = Bounds_check | Class_cast_check of Exp.t * Exp.t * Exp.t
 
 let d_typings typings =
-  let d_elem (exp, texp) = Sil.d_exp exp ; L.d_str ": " ; Sil.d_texp_full texp ; L.d_str " " in
+  let d_elem (exp, texp) = Exp.d_exp exp ; L.d_str ": " ; Exp.d_texp_full texp ; L.d_str " " in
   List.iter ~f:d_elem typings
 
 
@@ -1279,7 +1279,7 @@ end = struct
       | EXC_FALSE_HPRED hpred ->
           L.d_str " on " ; Sil.d_hpred hpred
       | EXC_FALSE_EXPS (e1, e2) ->
-          L.d_str " on " ; Sil.d_exp e1 ; L.d_str "," ; Sil.d_exp e2
+          L.d_str " on " ; Exp.d_exp e1 ; L.d_str "," ; Exp.d_exp e2
       | EXC_FALSE_SEXPS (se1, se2) ->
           L.d_str " on " ; Sil.d_sexp se1 ; L.d_str "," ; Sil.d_sexp se2
       | EXC_FALSE_ATOM a ->
@@ -1333,9 +1333,9 @@ let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
   in
   let rec do_imply subs e1 e2 : subst2 =
     L.d_str "do_imply " ;
-    Sil.d_exp e1 ;
+    Exp.d_exp e1 ;
     L.d_str " " ;
-    Sil.d_exp e2 ;
+    Exp.d_exp e2 ;
     L.d_ln () ;
     match (e1, e2) with
     | Exp.Var v1, Exp.Var v2 ->
@@ -1450,7 +1450,7 @@ let path_to_id path =
         None
     | _ ->
         L.d_str "path_to_id undefined on " ;
-        Sil.d_exp path ;
+        Exp.d_exp path ;
         L.d_ln () ;
         assert false
     (* None *)
@@ -1631,8 +1631,8 @@ and sexp_imply_nolhs tenv source calc_missing (subs : subst2) se2 typ2 =
       match e2 with
       | Exp.Var v2 when Ident.is_primed v2 ->
           let v2' = path_to_id source in
-          (* L.d_str "called path_to_id on "; Sil.d_exp e2; *)
-          (* L.d_str " returns "; Sil.d_exp (Exp.Var v2'); L.d_ln (); *)
+          (* L.d_str "called path_to_id on "; Exp.d_exp e2; *)
+          (* L.d_str " returns "; Exp.d_exp (Exp.Var v2'); L.d_ln (); *)
           let sub2' = extend_sub (snd subs) v2 (Exp.Var v2') in
           (fst subs, sub2')
       | Exp.Var _ ->
@@ -2490,7 +2490,7 @@ let check_array_bounds tenv (sub1, sub2) prop =
         let len1 = Sil.exp_sub sub1 len1_ in
         let len2 = Sil.exp_sub sub2 len2_ in
         (* L.d_strln ~color:Orange "check_bound ";
-           Sil.d_exp len1; L.d_str " "; Sil.d_exp len2; L.d_ln(); *)
+           Exp.d_exp len1; L.d_str " "; Exp.d_exp len2; L.d_ln(); *)
         let indices_to_check =
           [Exp.BinOp (Binop.PlusA None, len2, Exp.minus_one)]
           (* only check len *)
diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml
index 9072dfd93..c25cd1bc9 100644
--- a/infer/src/biabduction/Rearrange.ml
+++ b/infer/src/biabduction/Rearrange.ml
@@ -73,7 +73,7 @@ let check_bad_index tenv pname p len index loc =
 (** Perform bounds checking *)
 let bounds_check tenv pname prop len e =
   if Config.trace_rearrange then (
-    L.d_str "Bounds check index:" ; Sil.d_exp e ; L.d_str " len: " ; Sil.d_exp len ; L.d_ln () ) ;
+    L.d_str "Bounds check index:" ; Exp.d_exp e ; L.d_str " len: " ; Exp.d_exp len ; L.d_ln () ) ;
   check_bad_index tenv pname prop len e
 
 
@@ -526,7 +526,7 @@ let prop_iter_check_fields_ptsto_shallow tenv iter lexp =
 let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
   if Config.trace_rearrange then (
     L.d_str "entering prop_iter_extend_ptsto lexp: " ;
-    Sil.d_exp lexp ;
+    Exp.d_exp lexp ;
     L.d_ln () ) ;
   let offset = Sil.exp_get_offsets lexp in
   let max_stamp = Prop.prop_iter_max_stamp iter in
@@ -574,11 +574,11 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
     if Config.trace_rearrange then (
       L.d_strln "entering do_extend" ;
       L.d_str "e: " ;
-      Sil.d_exp e ;
+      Exp.d_exp e ;
       L.d_str " se : " ;
       Sil.d_sexp se ;
       L.d_str " te: " ;
-      Sil.d_texp_full te ;
+      Exp.d_texp_full te ;
       L.d_ln () ;
       L.d_ln () ) ;
     let extend_kind =
@@ -623,7 +623,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
                 List.map ~f:(fun (atoms, hpred') -> (atoms, hpred' :: sigma_rest)) atoms_hpred_list
             | _ ->
                 L.d_warning "Cannot extend " ;
-                Sil.d_exp lexp ;
+                Exp.d_exp lexp ;
                 L.d_strln " in" ;
                 Prop.d_prop (Prop.prop_iter_to_prop tenv iter) ;
                 L.d_ln () ;
@@ -644,7 +644,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
     in
     let res_prop_list = List.map ~f:(Prop.prop_iter_to_prop tenv) res_iter_list in
     L.d_str "in prop_iter_extend_ptsto lexp: " ;
-    Sil.d_exp lexp ;
+    Exp.d_exp lexp ;
     L.d_ln () ;
     L.d_strln "prop before:" ;
     let prop_before = Prop.prop_iter_to_prop tenv iter in
@@ -1034,7 +1034,7 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst =
   if Config.trace_rearrange then (
     L.d_strln "entering prop_iter_add_hpred_footprint" ;
     L.d_str "lexp: " ;
-    Sil.d_exp lexp ;
+    Exp.d_exp lexp ;
     L.d_ln () ;
     L.d_str "typ:" ;
     Typ.d_full typ ;
@@ -1063,7 +1063,7 @@ let rearrange_arith tenv lexp prop =
   if Config.trace_rearrange then (
     L.d_strln "entering rearrange_arith" ;
     L.d_str "lexp: " ;
-    Sil.d_exp lexp ;
+    Exp.d_exp lexp ;
     L.d_ln () ;
     L.d_str "prop: " ;
     L.d_ln () ;
@@ -1080,7 +1080,7 @@ let rearrange_arith tenv lexp prop =
 let pp_rearrangement_error message prop lexp =
   L.d_printfln ".... Rearrangement Error .... %s" message ;
   L.d_str "Exp:" ;
-  Sil.d_exp lexp ;
+  Exp.d_exp lexp ;
   L.d_ln () ;
   L.d_str "Prop:" ;
   L.d_ln () ;
@@ -1095,7 +1095,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
     L.d_increase_indent () ;
     L.d_strln "entering iter_rearrange_ptsto" ;
     L.d_str "lexp: " ;
-    Sil.d_exp lexp ;
+    Exp.d_exp lexp ;
     L.d_ln () ;
     L.d_strln "prop:" ;
     Prop.d_prop orig_prop ;
@@ -1332,7 +1332,7 @@ let check_type_size tenv pname prop texp off typ_from_instr =
         in
         Reporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
   | None ->
-      L.d_str "texp: " ; Sil.d_texp_full texp ; L.d_ln ()
+      L.d_str "texp: " ; Exp.d_texp_full texp ; L.d_ln ()
 
 
 (** Exposes lexp |->- from iter. In case that it is not possible to
@@ -1372,7 +1372,7 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst :
     L.d_increase_indent () ;
     L.d_strln "entering iter_rearrange" ;
     L.d_str "lexp: " ;
-    Sil.d_exp lexp ;
+    Exp.d_exp lexp ;
     L.d_ln () ;
     L.d_str "typ: " ;
     Typ.d_full typ ;
@@ -1721,7 +1721,7 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc :
   let inst = Sil.inst_rearrange (not ptr_tested_for_zero) loc (State.get_path_pos ()) in
   L.d_strln ".... Rearrangement Start ...." ;
   L.d_str "Exp: " ;
-  Sil.d_exp nlexp ;
+  Exp.d_exp nlexp ;
   L.d_ln () ;
   L.d_strln "Prop:" ;
   Prop.d_prop prop ;
diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml
index 26222c9bd..7d9b4d9a4 100644
--- a/infer/src/biabduction/SymExec.ml
+++ b/infer/src/biabduction/SymExec.ml
@@ -150,7 +150,7 @@ let rec apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, strexp, ty
       | None ->
           (* return a nondeterministic value if the index is not found after rearrangement *)
           L.d_str "apply_offlist: index " ;
-          Sil.d_exp idx ;
+          Exp.d_exp idx ;
           L.d_strln " not materialized -- returning nondeterministic value" ;
           let res_e' = Exp.Var (Ident.create_fresh Ident.kprimed) in
           (res_e', strexp, typ, None) )
@@ -1466,7 +1466,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
       then Rearrange.check_call_to_objc_block_error tenv current_pdesc prop_r fun_exp loc ;
       Rearrange.check_dereference_error tenv current_pdesc prop_r fun_exp loc ;
       L.d_str "Unknown function pointer " ;
-      Sil.d_exp fun_exp ;
+      Exp.d_exp fun_exp ;
       L.d_strln ", returning undefined value." ;
       let callee_pname = Typ.Procname.from_string_c_fun "__function_pointer__" in
       unknown_or_scan_call ~is_scan:false ~reason:"unresolved function pointer" (snd ret_id_typ)
@@ -1619,7 +1619,7 @@ and add_constraints_on_actuals_by_ref tenv caller_pdesc prop actuals_by_ref call
           let is_const = List.mem ~equal:Int.equal attrs.ProcAttributes.const_formals i in
           if is_const then (
             L.d_printf "Not havocing const argument number %d: " i ;
-            Sil.d_exp e ;
+            Exp.d_exp e ;
             L.d_ln () ) ;
           not is_const
       | None ->
@@ -1862,7 +1862,7 @@ and proc_call ?dynamic_dispatch exe_env callee_summary
         L.d_warning "likely use of variable-arguments function, or function prototype missing" ;
         L.d_ln () ;
         L.d_str "actual parameters: " ;
-        Sil.d_exp_list (List.map ~f:fst actual_pars) ;
+        Exp.d_list (List.map ~f:fst actual_pars) ;
         L.d_ln () ;
         L.d_str "formal parameters: " ;
         Typ.d_list formal_types ;
@@ -1872,7 +1872,7 @@ and proc_call ?dynamic_dispatch exe_env callee_summary
         L.d_printfln "**** ERROR: Procedure %a mismatch in the number of parameters ****"
           Typ.Procname.pp callee_pname ;
         L.d_str "actual parameters: " ;
-        Sil.d_exp_list (List.map ~f:fst actual_pars) ;
+        Exp.d_list (List.map ~f:fst actual_pars) ;
         L.d_ln () ;
         L.d_str "formal parameters: " ;
         Typ.d_list formal_types ;
diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml
index 00e3a8e26..3bc82c4c1 100644
--- a/infer/src/biabduction/Tabulation.ml
+++ b/infer/src/biabduction/Tabulation.ml
@@ -247,22 +247,22 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_
           List.map ~f:(fun id -> Exp.Var id) (Ident.HashQueue.keys fav_actual_pre)
         in
         L.d_str "fav_actual_pre: " ;
-        Sil.d_exp_list vars_actual_pre ;
+        Exp.d_list vars_actual_pre ;
         L.d_ln () ;
         L.d_str "Dom(Sub1): " ;
-        Sil.d_exp_list (List.map ~f:(fun id -> Exp.Var id) dom1) ;
+        Exp.d_list (List.map ~f:(fun id -> Exp.Var id) dom1) ;
         L.d_ln () ;
         L.d_str "Ran(Sub1): " ;
-        Sil.d_exp_list rng1 ;
+        Exp.d_list rng1 ;
         L.d_ln () ;
         L.d_str "Dom(Sub2): " ;
-        Sil.d_exp_list (List.map ~f:(fun id -> Exp.Var id) dom2) ;
+        Exp.d_list (List.map ~f:(fun id -> Exp.Var id) dom2) ;
         L.d_ln () ;
         L.d_str "Ran(Sub2): " ;
-        Sil.d_exp_list rng2 ;
+        Exp.d_list rng2 ;
         L.d_ln () ;
         L.d_str "Don't know about id: " ;
-        Sil.d_exp (Exp.Var id) ;
+        Exp.d_exp (Exp.Var id) ;
         L.d_ln () ;
         assert false
     in
@@ -372,7 +372,7 @@ let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre fo
       Prop.d_prop spec_pre ;
       L.d_ln () ;
       L.d_str "exp " ;
-      Sil.d_exp e ;
+      Exp.d_exp e ;
       L.d_printfln " desc: %a" Localise.pp_error_desc error_desc ;
       error_desc
     in