From 355ab92130f73b7eef4ce2d2dc13cbd9f3b60649 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 25 Oct 2016 08:50:16 -0700 Subject: [PATCH] [backend] move expression pretty-printing into exp module Reviewed By: jberdine Differential Revision: D4059909 fbshipit-source-id: b382cb1 --- infer/src/IR/Exp.re | 42 +++++++ infer/src/IR/Exp.rei | 7 ++ infer/src/IR/Localise.ml | 2 +- infer/src/IR/Sil.re | 144 ++++++++++------------ infer/src/IR/Sil.rei | 6 +- infer/src/backend/abs.ml | 8 +- infer/src/backend/dotty.ml | 62 +++++----- infer/src/backend/errdesc.ml | 4 +- infer/src/backend/interproc.ml | 2 +- infer/src/backend/match.ml | 4 +- infer/src/backend/modelBuiltins.ml | 2 +- infer/src/backend/printer.ml | 2 +- infer/src/backend/prop.ml | 20 +-- infer/src/backend/prover.ml | 4 +- infer/src/backend/rearrange.ml | 13 +- infer/src/backend/tabulation.ml | 2 +- infer/src/checkers/checkers.ml | 6 +- infer/src/checkers/constantPropagation.ml | 2 +- infer/src/clang/cTrans.ml | 6 +- infer/src/eradicate/typeState.ml | 2 +- infer/src/quandary/TaintAnalysis.ml | 2 +- infer/src/unit/accessPathTests.ml | 2 +- infer/src/unit/analyzerTester.ml | 4 +- infer/tests/repl/infer_batch_script.ml | 2 +- 24 files changed, 185 insertions(+), 165 deletions(-) diff --git a/infer/src/IR/Exp.re b/infer/src/IR/Exp.re index 3c215c668..ef5f42748 100644 --- a/infer/src/IR/Exp.re +++ b/infer/src/IR/Exp.re @@ -313,3 +313,45 @@ let get_vars exp => { }; get_vars_ exp ([], []) }; + + +/** Pretty print an expression. */ +let rec pp_ pe pp_t f e => { + let pp_exp = pp_ pe pp_t; + let print_binop_stm_output e1 op e2 => + switch (op: Binop.t) { + | Eq + | Ne + | PlusA + | Mult => F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe op) pp_exp e1 + | Lt => F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Gt) pp_exp e1 + | Gt => F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Lt) pp_exp e1 + | Le => F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Ge) pp_exp e1 + | Ge => F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Le) pp_exp e1 + | _ => F.fprintf f "(%a %s %a)" pp_exp e1 (Binop.str pe op) pp_exp e2 + }; + switch (e: t) { + | Var id => (Ident.pp pe) f id + | Const c => F.fprintf f "%a" (Const.pp pe) c + | Cast typ e => F.fprintf f "(%a)%a" pp_t typ pp_exp e + | UnOp op e _ => F.fprintf f "%s%a" (Unop.str op) pp_exp e + | BinOp op (Const c) e2 when Config.smt_output => print_binop_stm_output (Const c) op e2 + | BinOp op e1 e2 => F.fprintf f "(%a %s %a)" pp_exp e1 (Binop.str pe op) pp_exp e2 + | Exn e => F.fprintf f "EXN %a" pp_exp e + | Closure {name, captured_vars} => + let id_exps = IList.map (fun (id_exp, _, _) => id_exp) captured_vars; + F.fprintf f "(%a)" (pp_comma_seq pp_exp) [Const (Cfun name), ...id_exps] + | Lvar pv => Pvar.pp pe f pv + | Lfield e fld _ => F.fprintf f "%a.%a" pp_exp e Ident.pp_fieldname fld + | Lindex e1 e2 => F.fprintf f "%a[%a]" pp_exp e1 pp_exp e2 + | Sizeof t l s => + let pp_len f l => Option.map_default (F.fprintf f "[%a]" pp_exp) () l; + F.fprintf f "sizeof(%a%a%a)" pp_t t pp_len l Subtype.pp s + } +}; + +let pp_printenv pe pp_typ f e => pp_ pe (pp_typ pe) f e; + +let pp f e => pp_printenv pe_text Typ.pp f e; + +let to_string e => F.asprintf "%a" pp e; diff --git a/infer/src/IR/Exp.rei b/infer/src/IR/Exp.rei index d847cd8db..baf5bae5b 100644 --- a/infer/src/IR/Exp.rei +++ b/infer/src/IR/Exp.rei @@ -154,3 +154,10 @@ let lt: t => t => t; /** Extract the ids and pvars from an expression */ let get_vars: t => (list Ident.t, list Pvar.t); + +let pp_printenv: + printenv => (printenv => F.formatter => Typ.t => unit) => F.formatter => t => unit; + +let pp: F.formatter => t => unit; + +let to_string: t => string; diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index 64a5f18d5..8262a36e8 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -772,7 +772,7 @@ let desc_retain_cycle cycle loc cycle_dotty = str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") a block capturing "^(Ident.fieldname_to_string f)^"; "; ct:=!ct +1; | Sil.Eexp(Exp.Lvar pvar as e, _) -> - let e_str = Sil.exp_to_string e in + let e_str = Exp.to_string e in let e_str = if Pvar.is_seed pvar then remove_old e_str else e_str in diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 351c12344..396acdd4e 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -532,7 +532,7 @@ let pp_seq_diff pp pe0 f => /** Pretty print an expression. */ -let rec _pp_exp pe0 pp_t f e0 => { +let pp_exp_printenv pe0 f e0 => { let (pe, changed) = color_pre_wrapper pe0 f e0; let e = switch pe.pe_obj_sub { @@ -545,54 +545,18 @@ let rec _pp_exp pe0 pp_t f e0 => { | _ => assert false } } else { - let pp_exp = _pp_exp pe pp_t; - let print_binop_stm_output e1 op e2 => - switch (op: Binop.t) { - | Eq - | Ne - | PlusA - | Mult => F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe op) pp_exp e1 - | Lt => F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Gt) pp_exp e1 - | Gt => F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Lt) pp_exp e1 - | Le => F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Ge) pp_exp e1 - | Ge => F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Le) pp_exp e1 - | _ => F.fprintf f "(%a %s %a)" pp_exp e1 (Binop.str pe op) pp_exp e2 - }; - switch (e: Exp.t) { - | Var id => (Ident.pp pe) f id - | Const c => F.fprintf f "%a" (Const.pp pe) c - | Cast typ e => F.fprintf f "(%a)%a" pp_t typ pp_exp e - | UnOp op e _ => F.fprintf f "%s%a" (Unop.str op) pp_exp e - | BinOp op (Const c) e2 when Config.smt_output => print_binop_stm_output (Exp.Const c) op e2 - | BinOp op e1 e2 => F.fprintf f "(%a %s %a)" pp_exp e1 (Binop.str pe op) pp_exp e2 - | Exn e => F.fprintf f "EXN %a" pp_exp e - | Closure {name, captured_vars} => - let id_exps = IList.map (fun (id_exp, _, _) => id_exp) captured_vars; - F.fprintf f "(%a)" (pp_comma_seq pp_exp) [Exp.Const (Cfun name), ...id_exps] - | Lvar pv => Pvar.pp pe f pv - | Lfield e fld _ => F.fprintf f "%a.%a" pp_exp e Ident.pp_fieldname fld - | Lindex e1 e2 => F.fprintf f "%a[%a]" pp_exp e1 pp_exp e2 - | Sizeof t l s => - let pp_len f l => Option.map_default (F.fprintf f "[%a]" pp_exp) () l; - F.fprintf f "sizeof(%a%a%a)" pp_t t pp_len l Subtype.pp s - } + Exp.pp_printenv pe Typ.pp f e }; color_post_wrapper changed pe0 f }; -let pp_exp pe f e => _pp_exp pe (Typ.pp pe) f e; - - -/** Convert an expression to a string */ -let exp_to_string e => pp_to_string (pp_exp pe_text) e; - /** dump an expression. */ let d_exp (e: Exp.t) => L.add_print_action (L.PTexp, Obj.repr e); /** Pretty print a list of expressions. */ -let pp_exp_list pe f expl => (pp_seq (pp_exp pe)) f expl; +let pp_exp_list pe f expl => (pp_seq (pp_exp_printenv pe)) f expl; /** dump a list of expressions. */ @@ -601,20 +565,20 @@ let d_exp_list (el: list Exp.t) => L.add_print_action (L.PTexp_list, Obj.repr el let pp_texp pe f => fun | Exp.Sizeof t l s => { - let pp_len f l => Option.map_default (F.fprintf f "[%a]" (pp_exp pe)) () l; + let pp_len f l => Option.map_default (F.fprintf f "[%a]" (pp_exp_printenv pe)) () l; F.fprintf f "%a%a%a" (Typ.pp pe) t pp_len l Subtype.pp s } - | e => (pp_exp pe) f e; + | e => (pp_exp_printenv pe) f e; /** Pretty print a type with all the details. */ let pp_texp_full pe f => fun | Exp.Sizeof t l s => { - let pp_len f l => Option.map_default (F.fprintf f "[%a]" (pp_exp pe)) () l; + let pp_len f l => Option.map_default (F.fprintf f "[%a]" (pp_exp_printenv pe)) () l; F.fprintf f "%a%a%a" (Typ.pp_full pe) t pp_len l Subtype.pp s } - | e => (_pp_exp pe) (Typ.pp_full pe) f e; + | e => Exp.pp_printenv pe Typ.pp_full f e; /** Dump a type expression with all the details. */ @@ -625,7 +589,7 @@ let d_texp_full (te: Exp.t) => L.add_print_action (L.PTtexp_full, Obj.repr te); let pp_offset pe f => fun | Off_fld fld _ => F.fprintf f "%a" Ident.pp_fieldname fld - | Off_index exp => F.fprintf f "%a" (pp_exp pe) exp; + | Off_index exp => F.fprintf f "%a" (pp_exp_printenv pe) exp; /** Convert an offset to a string */ @@ -647,7 +611,7 @@ let rec pp_offset_list pe f => /** Dump a list of offsets */ let d_offset_list (offl: list offset) => L.add_print_action (L.PToff_list, Obj.repr offl); -let pp_exp_typ pe f (e, t) => F.fprintf f "%a:%a" (pp_exp pe) e (Typ.pp pe) t; +let pp_exp_typ pe f (e, t) => F.fprintf f "%a:%a" (pp_exp_printenv pe) e (Typ.pp pe) t; /** Get the location of the instruction */ @@ -681,11 +645,22 @@ let pp_instr pe0 f instr => { let (pe, changed) = color_pre_wrapper pe0 f instr; switch instr { | Load id e t loc => - F.fprintf f "%a=*%a:%a %a" (Ident.pp pe) id (pp_exp pe) e (Typ.pp pe) t Location.pp loc + F.fprintf + f "%a=*%a:%a %a" (Ident.pp pe) id (pp_exp_printenv pe) e (Typ.pp pe) t Location.pp loc | Store e1 t e2 loc => - F.fprintf f "*%a:%a=%a %a" (pp_exp pe) e1 (Typ.pp pe) t (pp_exp pe) e2 Location.pp loc + F.fprintf + f + "*%a:%a=%a %a" + (pp_exp_printenv pe) + e1 + (Typ.pp pe) + t + (pp_exp_printenv pe) + e2 + Location.pp + loc | Prune cond loc true_branch _ => - F.fprintf f "PRUNE(%a, %b); %a" (pp_exp pe) cond true_branch Location.pp loc + F.fprintf f "PRUNE(%a, %b); %a" (pp_exp_printenv pe) cond true_branch Location.pp loc | Call ret_id e arg_ts loc cf => switch ret_id { | None => () @@ -694,7 +669,7 @@ let pp_instr pe0 f instr => { F.fprintf f "%a(%a)%a %a" - (pp_exp pe) + (pp_exp_printenv pe) e (pp_comma_seq (pp_exp_typ pe)) arg_ts @@ -739,23 +714,25 @@ let pp_atom pe0 f a => { | Aeq (BinOp op e1 e2) (Const (Cint i)) when IntLit.isone i => switch pe.pe_kind { | PP_TEXT - | PP_HTML => F.fprintf f "%a" (pp_exp pe) (Exp.BinOp op e1 e2) - | PP_LATEX => F.fprintf f "%a" (pp_exp pe) (Exp.BinOp op e1 e2) + | PP_HTML => F.fprintf f "%a" (pp_exp_printenv pe) (Exp.BinOp op e1 e2) + | PP_LATEX => F.fprintf f "%a" (pp_exp_printenv pe) (Exp.BinOp op e1 e2) } | Aeq e1 e2 => switch pe.pe_kind { | PP_TEXT - | PP_HTML => F.fprintf f "%a = %a" (pp_exp pe) e1 (pp_exp pe) e2 - | PP_LATEX => F.fprintf f "%a{=}%a" (pp_exp pe) e1 (pp_exp pe) e2 + | PP_HTML => F.fprintf f "%a = %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 + | PP_LATEX => F.fprintf f "%a{=}%a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 } | Aneq e1 e2 => switch pe.pe_kind { | PP_TEXT - | PP_HTML => F.fprintf f "%a != %a" (pp_exp pe) e1 (pp_exp pe) e2 - | PP_LATEX => F.fprintf f "%a{\\neq}%a" (pp_exp pe) e1 (pp_exp pe) e2 + | PP_HTML => F.fprintf f "%a != %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 + | PP_LATEX => F.fprintf f "%a{\\neq}%a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 } - | Apred a es => F.fprintf f "%s(%a)" (PredSymb.to_string pe a) (pp_comma_seq (pp_exp pe)) es - | Anpred a es => F.fprintf f "!%s(%a)" (PredSymb.to_string pe a) (pp_comma_seq (pp_exp pe)) es + | Apred a es => + F.fprintf f "%s(%a)" (PredSymb.to_string pe a) (pp_comma_seq (pp_exp_printenv pe)) es + | Anpred a es => + F.fprintf f "!%s(%a)" (PredSymb.to_string pe a) (pp_comma_seq (pp_exp_printenv pe)) es }; color_post_wrapper changed pe0 f }; @@ -1106,7 +1083,7 @@ let pp_inst_if_trace pe f inst => let rec pp_sexp_env pe0 envo f se => { let (pe, changed) = color_pre_wrapper pe0 f se; switch se { - | Eexp e inst => F.fprintf f "%a%a" (pp_exp pe) e (pp_inst_if_trace pe) inst + | Eexp e inst => F.fprintf f "%a%a" (pp_exp_printenv pe) e (pp_inst_if_trace pe) inst | Estruct fel inst => switch pe.pe_kind { | PP_TEXT @@ -1119,8 +1096,16 @@ let rec pp_sexp_env pe0 envo f se => { 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 pe) i (pp_sexp_env pe envo) se; - F.fprintf f "[%a|%a]%a" (pp_exp pe) len (pp_seq_diff pp_diff pe) nel (pp_inst_if_trace pe) inst + let pp_diff f (i, se) => F.fprintf f "%a:%a" (pp_exp_printenv pe) i (pp_sexp_env pe envo) se; + F.fprintf + f + "[%a|%a]%a" + (pp_exp_printenv pe) + len + (pp_seq_diff pp_diff pe) + nel + (pp_inst_if_trace pe) + inst }; color_post_wrapper changed pe0 f }; @@ -1140,8 +1125,9 @@ let rec pp_hpred_env pe0 envo f hpred => { switch pe'.pe_kind { | PP_TEXT | PP_HTML => - F.fprintf f "%a|->%a:%a" (pp_exp pe') e (pp_sexp_env pe' envo) se (pp_texp_simple pe') te - | PP_LATEX => F.fprintf f "%a\\mapsto %a" (pp_exp pe') e (pp_sexp_env pe' envo) se + F.fprintf + f "%a|->%a:%a" (pp_exp_printenv pe') e (pp_sexp_env pe' envo) se (pp_texp_simple pe') te + | PP_LATEX => F.fprintf f "%a\\mapsto %a" (pp_exp_printenv pe') e (pp_sexp_env pe' envo) se } | Hlseg k hpara e1 e2 elist => switch pe.pe_kind { @@ -1152,11 +1138,11 @@ let rec pp_hpred_env pe0 envo f hpred => { "lseg%a(%a,%a,[%a],%a)" pp_lseg_kind k - (pp_exp pe) + (pp_exp_printenv pe) e1 - (pp_exp pe) + (pp_exp_printenv pe) e2 - (pp_comma_seq (pp_exp pe)) + (pp_comma_seq (pp_exp_printenv pe)) elist (pp_hpara_env pe envo) hpara @@ -1166,11 +1152,11 @@ let rec pp_hpred_env pe0 envo f hpred => { "\\textsf{lseg}_{%a}(%a,%a,[%a],%a)" pp_lseg_kind k - (pp_exp pe) + (pp_exp_printenv pe) e1 - (pp_exp pe) + (pp_exp_printenv pe) e2 - (pp_comma_seq (pp_exp pe)) + (pp_comma_seq (pp_exp_printenv pe)) elist (pp_hpara_env pe envo) hpara @@ -1184,15 +1170,15 @@ let rec pp_hpred_env pe0 envo f hpred => { "dllseg%a(%a,%a,%a,%a,[%a],%a)" pp_lseg_kind k - (pp_exp pe) + (pp_exp_printenv pe) iF - (pp_exp pe) + (pp_exp_printenv pe) oB - (pp_exp pe) + (pp_exp_printenv pe) oF - (pp_exp pe) + (pp_exp_printenv pe) iB - (pp_comma_seq (pp_exp pe)) + (pp_comma_seq (pp_exp_printenv pe)) elist (pp_hpara_dll_env pe envo) hpara_dll @@ -1202,15 +1188,15 @@ let rec pp_hpred_env pe0 envo f hpred => { "\\textsf{dllseg}_{%a}(%a,%a,%a,%a,[%a],%a)" pp_lseg_kind k - (pp_exp pe) + (pp_exp_printenv pe) iF - (pp_exp pe) + (pp_exp_printenv pe) oB - (pp_exp pe) + (pp_exp_printenv pe) oF - (pp_exp pe) + (pp_exp_printenv pe) iB - (pp_comma_seq (pp_exp pe)) + (pp_comma_seq (pp_exp_printenv pe)) elist (pp_hpara_dll_env pe envo) hpara_dll @@ -1713,7 +1699,7 @@ let array_clean_new_index footprint_part new_idx => { if (footprint_part && fav_exists fav (fun id => not (Ident.is_footprint id))) { L.d_warning ( "Array index " ^ - exp_to_string new_idx ^ " has non-footprint vars: replaced by fresh footprint var" + Exp.to_string new_idx ^ " has non-footprint vars: replaced by fresh footprint var" ); L.d_ln (); let id = Ident.create_fresh Ident.kfootprint; diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index 13fb4ff16..acd1ae3eb 100644 --- a/infer/src/IR/Sil.rei +++ b/infer/src/IR/Sil.rei @@ -317,17 +317,13 @@ let color_post_wrapper: bool => printenv => F.formatter => unit; /** Pretty print an expression. */ -let pp_exp: printenv => F.formatter => Exp.t => unit; +let pp_exp_printenv: printenv => F.formatter => Exp.t => unit; /** Pretty print an expression with type. */ let pp_exp_typ: printenv => F.formatter => (Exp.t, Typ.t) => unit; -/** Convert an expression to a string */ -let exp_to_string: Exp.t => string; - - /** dump an expression. */ let d_exp: Exp.t => unit; diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 3269ad08a..512662e9a 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -422,7 +422,7 @@ let typ_get_recursive_flds tenv typ_exp = match Tenv.lookup tenv name with | Some { fields } -> IList.map fst3 (IList.filter (filter typ) fields) | None -> - L.err "@.typ_get_recursive: unexpected type expr: %a@." (Sil.pp_exp pe_text) typ_exp; + L.err "@.typ_get_recursive: unexpected type expr: %a@." Exp.pp typ_exp; [] (* ToDo: assert false *) ) | Tint _ | Tvoid | Tfun _ | Tptr _ | Tfloat _ | Tarray _ -> [] @@ -430,7 +430,7 @@ let typ_get_recursive_flds tenv typ_exp = | Exp.Var _ -> [] (* type of |-> not known yet *) | Exp.Const _ -> [] | _ -> - L.err "@.typ_get_recursive: unexpected type expr: %a@." (Sil.pp_exp pe_text) typ_exp; + L.err "@.typ_get_recursive: unexpected type expr: %a@." Exp.pp typ_exp; assert false let discover_para_roots tenv p root1 next1 root2 next2 : Sil.hpara option = @@ -893,8 +893,8 @@ let get_cycle root prop = IList.iter (fun ((e, t), f, e') -> match e, e' with | Sil.Eexp (e, _), Sil.Eexp (e', _) -> - L.d_str ("("^(Sil.exp_to_string e)^": "^(Typ.to_string t)^", " - ^(Ident.fieldname_to_string f)^", "^(Sil.exp_to_string e')^")") + L.d_str ("("^(Exp.to_string e)^": "^(Typ.to_string t)^", " + ^(Ident.fieldname_to_string f)^", "^(Exp.to_string e')^")") | _ -> ()) cyc; L.d_strln "") in (* Perform a dfs of a graph stopping when e_root is reached. diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 771f2ede7..36448c724 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -135,10 +135,10 @@ let rec strexp_to_string pe coo f se = else () | Sil.Eexp (e, _) -> if !print_full_prop then - F.fprintf f "%a" (Sil.pp_exp pe) e + F.fprintf f "%a" (Sil.pp_exp_printenv pe) e else F.fprintf 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 pe) e (get_contents pe coo) idx + | Sil.Earray(e, idx, _) -> F.fprintf f " ARRAY[%a] | { %a } " (Sil.pp_exp_printenv pe) e (get_contents pe coo) idx and struct_to_dotty_str pe coo f ls : unit = match ls with @@ -149,19 +149,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', _) -> - F.fprintf f "%a" (Sil.pp_exp pe) e' + F.fprintf f "%a" (Sil.pp_exp_printenv pe) 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 pe) e' + F.fprintf f "(ARRAY Size: %a) | { }" (Sil.pp_exp_printenv pe) e' | Sil.Earray(e', ((idx, a):: linner), _) -> - F.fprintf f "(ARRAY Size: %a) | { %a: %a | %a }" (Sil.pp_exp pe) e' (Sil.pp_exp pe) idx + 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 and get_contents_single pe coo f (e, se) = - let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in + 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 pe) e (get_contents_sexp pe coo) se + e_no_special_char (Sil.pp_exp_printenv pe) e (get_contents_sexp pe coo) se and get_contents pe coo f = function | [] -> () @@ -415,7 +415,7 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle = | [node] | [Dotpointsto _ ; node] | [node; Dotpointsto _] -> let n = get_coordinate_id node in if IList.mem Exp.equal e !struct_exp_nodes then begin - let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in + let e_no_special_char = strip_special_chars (Exp.to_string e) in let link_kind = if (in_cycle cycle (fn, se)) && (not !print_full_prop) then LinkRetainCycle else LinkStructToStruct in @@ -439,22 +439,22 @@ let rec compute_target_array_elements dotnodes list_elements p f lambda = | Sil.Eexp (e, _) -> if is_nil e p then begin let n'= make_nil_node lambda in - [(LinkArrayToExp, Sil.exp_to_string idx, n',"")] + [(LinkArrayToExp, Exp.to_string idx, n',"")] end else let nodes_e = select_nodes_exp_lambda dotnodes e lambda in (match nodes_e with | [] -> (match box_dangling e with | None -> [] - | Some n' -> [(LinkArrayToExp, Sil.exp_to_string idx, n',"")] + | Some n' -> [(LinkArrayToExp, Exp.to_string idx, n',"")] ) | [node] | [Dotpointsto _ ; node] | [node; Dotpointsto _] -> let n = get_coordinate_id node in if IList.mem Exp.equal e !struct_exp_nodes then begin - let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in - [(LinkArrayToStruct, Sil.exp_to_string idx, n, e_no_special_char)] + let e_no_special_char = strip_special_chars (Exp.to_string e) in + [(LinkArrayToStruct, Exp.to_string idx, n, e_no_special_char)] end else - [(LinkArrayToExp, Sil.exp_to_string idx, n,"")] + [(LinkArrayToExp, Exp.to_string idx, n,"")] | _ -> (* by construction there must be at most 2 nodes for an expression*) L.out "@\n Too many nodes! Error! @\n@.@."; assert false ) @@ -496,7 +496,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle = let ff n = IList.map (fun (k, lab_src, m, lab_trg) -> mk_link k (mk_coordinate (n + 1) lambda) (strip_special_chars lab_src) (mk_coordinate m lambda) (strip_special_chars lab_trg)) target_list in let links_from_elements = IList.flatten (IList.map ff (n:: nl)) in - let trg_label = strip_special_chars (Sil.exp_to_string e) in + let trg_label = strip_special_chars (Exp.to_string e) in let lnk = mk_link (LinkToArray) (mk_coordinate n lambda) "" (mk_coordinate (n + 1) lambda) trg_label in lnk :: links_from_elements @ dotty_mk_set_links dotnodes sigma' p f cycle in match sigma with @@ -521,7 +521,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle = let nl'= IList.filter (fun id -> address_struct_id != id) nl in let links_from_fields = IList.flatten (IList.map ff nl') in let lnk_from_address_struct = if !print_full_prop then - let trg_label = strip_special_chars (Sil.exp_to_string e) in + let trg_label = strip_special_chars (Exp.to_string e) in [mk_link (LinkExpToStruct) (mk_coordinate address_struct_id lambda) "" (mk_coordinate (address_struct_id + 1) lambda) trg_label] else [] in @@ -662,7 +662,7 @@ let filter_useless_spec_dollar_box (nodes: dotty_node list) (links: link list) = | Dotpointsto _ -> let e = get_node_exp node in if is_spec_variable e then begin - (*L.out "@\n Found a spec expression = %s @.@." (Sil.exp_to_string e); *) + (*L.out "@\n Found a spec expression = %s @.@." (Exp.to_string e); *) let links_from_node = boxes_pointed_by node links in let links_to_node = boxes_pointing_at node links in (* L.out "@\n Size of links_from=%i links_to=%i @.@." (IList.length links_from_node) (IList.length links_to_node); *) @@ -683,16 +683,16 @@ let rec print_struct f pe e te l coo c = (match Str.split_delim (Str.regexp_string Config.anonymous_block_prefix) str_t with | [_; _] -> "BLOCK object" | _ -> str_t) - | _ -> Sil.exp_to_string te in + | _ -> Exp.to_string te in let n = coo.id in let lambda = coo.lambda in - let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in + let e_no_special_char = strip_special_chars (Exp.to_string e) in F.fprintf f "subgraph structs_%iL%i {\n" n lambda ; if !print_full_prop then F.fprintf f " node [shape=record]; \n struct%iL%i \ [label=\"{<%s%iL%i> STRUCT: %a } | %a\" ] fontcolor=%s\n" - n lambda e_no_special_char n lambda (Sil.pp_exp pe) e (struct_to_dotty_str pe coo) l c + n lambda e_no_special_char n lambda (Sil.pp_exp_printenv pe) e (struct_to_dotty_str pe coo) l c else F.fprintf f " node [shape=record]; \n struct%iL%i \ @@ -703,9 +703,9 @@ let rec print_struct f pe e te l coo c = and print_array f pe e1 e2 l coo c = let n = coo.id in let lambda = coo.lambda in - let e_no_special_char = strip_special_chars (Sil.exp_to_string e1) in + let e_no_special_char = strip_special_chars (Exp.to_string e1) in F.fprintf f "subgraph structs_%iL%i {\n" n lambda ; - F.fprintf f " node [shape=record]; \n struct%iL%i [label=\"{<%s%iL%i> ARRAY| SIZE: %a } | %a\" ] fontcolor=%s\n" n lambda e_no_special_char n lambda (Sil.pp_exp pe) e2 (get_contents pe coo) l c; + F.fprintf f " node [shape=record]; \n struct%iL%i [label=\"{<%s%iL%i> ARRAY| SIZE: %a } | %a\" ] fontcolor=%s\n" n lambda e_no_special_char n lambda (Sil.pp_exp_printenv pe) e2 (get_contents pe coo) l c; F.fprintf f "}\n" and print_sll f pe nesting k e1 coo = @@ -718,7 +718,7 @@ and print_sll f pe nesting k e1 coo = | Sil.Lseg_NE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white]; label=\"list NE\";" n' lambda (*pp_nesting nesting*) | Sil.Lseg_PE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white]; label=\"list PE\";" n' lambda (*pp_nesting nesting *) end; - F.fprintf f "state%iL%i [label=\"%a\"]\n" n lambda (Sil.pp_exp pe) e1; + F.fprintf f "state%iL%i [label=\"%a\"]\n" n lambda (Sil.pp_exp_printenv 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 ; @@ -739,13 +739,13 @@ and print_dll f pe nesting k e1 e4 coo = | Sil.Lseg_NE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white]; label=\"doubly-linked list NE\";" n' lambda (*pp_nesting nesting *) | Sil.Lseg_PE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white]; label=\"doubly-linked list PE\";" n' lambda (*pp_nesting nesting *) end; - F.fprintf f "state%iL%i [label=\"%a\"]\n" n lambda (Sil.pp_exp pe) e1; + F.fprintf f "state%iL%i [label=\"%a\"]\n" n lambda (Sil.pp_exp_printenv 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 pe) e4; + F.fprintf f "state%iL%i [label=\"%a\"]\n" (n + 1) lambda (Sil.pp_exp_printenv 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; @@ -757,9 +757,9 @@ and dotty_pp_state f pe cycle dotnode = let n = coo.id in 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 pe) e c + 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 pe) e c in + F.fprintf f "state%iL%i [label=\"%a\" fontcolor=%s]\n" n lambda (Sil.pp_exp_printenv pe) e c in match dotnode with | Dotnil coo when !print_full_prop -> F.fprintf f "state%iL%i [label=\"NIL \", color=green, style=filled]\n" coo.id coo.lambda @@ -786,10 +786,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: "; - IList.iter (fun e -> L.out " %a " (Sil.pp_exp pe) e) !fields_structs; + IList.iter (fun e -> L.out " %a " (Sil.pp_exp_printenv pe) e) !fields_structs; L.out "@\n@."; L.out "@\n@\n Computed exp structs nodes: "; - IList.iter (fun e -> L.out " %a " (Sil.pp_exp pe) e) !struct_exp_nodes; + IList.iter (fun e -> L.out " %a " (Sil.pp_exp_printenv pe) e) !struct_exp_nodes; L.out "@\n@."; *) let sigma_lambda = IList.map (fun hp -> (hp,!lambda_counter)) sigma in let nodes = (dotty_mk_node pe) sigma_lambda in @@ -1106,7 +1106,7 @@ let set_dangling_nodes = ref [] (* convert an exp into a string which is xml friendly, ie. special character are replaced by*) (* the proper xml way to visualize them*) let exp_to_xml_string e = - pp_to_string (Sil.pp_exp (pe_html Black)) e + pp_to_string (Sil.pp_exp_printenv (pe_html Black)) e (* convert an atom into an xml-friendly string without special characters *) let atom_to_xml_string a = @@ -1415,9 +1415,9 @@ let exp_is_neq_zero e = let rec get_contents_range_single pe coo f range_se = let (e1, e2), se = range_se in - let e1_no_special_char = strip_special_chars (Sil.exp_to_string e1) in + let e1_no_special_char = strip_special_chars (Exp.to_string e1) in F.fprintf f "{ <%s> [%a,%a] : %a }" - e1_no_special_char (Sil.pp_exp pe) e1 (Sil.pp_exp pe) e2 (get_contents_sexp pe coo) se + e1_no_special_char (Sil.pp_exp_printenv pe) e1 (Sil.pp_exp_printenv pe) e2 (get_contents_sexp pe coo) se and get_contents_range pe coo f = function | [] -> () diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index f8eec7e18..ab01bed42 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -64,7 +64,7 @@ let explain_deallocate_stack_var pvar ra = let explain_deallocate_constant_string s ra = let const_str = let pp fmt () = - Sil.pp_exp pe_text fmt (Exp.Const (Const.Cstr s)) in + Exp.pp fmt (Exp.Const (Const.Cstr s)) in pp_to_string pp () in Localise.desc_deallocate_static_memory const_str ra.PredSymb.ra_pname ra.PredSymb.ra_loc @@ -1079,7 +1079,7 @@ let explain_tainted_value_reaching_sensitive_function | Some (pvar, pvar_off) -> let dexp = dexp_apply_pvar_off (DExp.Dpvar pvar) pvar_off in DExp.to_string dexp - | None -> Sil.exp_to_string e + | None -> Exp.to_string e end in Localise.desc_tainted_value_reaching_sensitive_function taint_kind diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 4aa89466f..3e8a987b8 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -406,7 +406,7 @@ let check_assignement_guard node = when (Ident.equal e1 e2) -> if verbose then - L.d_strln ("Found " ^ (Sil.exp_to_string e') ^ " as prune var"); + L.d_strln ("Found " ^ (Exp.to_string e') ^ " as prune var"); [e'] | _ -> [] in let prune_vars = IList.flatten(IList.map (fun n -> prune_var n) succs) in diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml index 6fbb2a82d..0f4c09922 100644 --- a/infer/src/backend/match.ml +++ b/infer/src/backend/match.ml @@ -144,8 +144,8 @@ and isel_match isel1 sub vars isel2 = if (not sanity_check) then begin let pe = pe_text in L.out "@[.... Sanity Check Failure while Matching Index-Strexps ....@."; - L.out "@[<4> IDX1: %a, STREXP1: %a@." (Sil.pp_exp pe) idx1 (Sil.pp_sexp pe) se1'; - L.out "@[<4> IDX2: %a, STREXP2: %a@\n@." (Sil.pp_exp pe) idx2 (Sil.pp_sexp pe) se2'; + L.out "@[<4> IDX1: %a, STREXP1: %a@." (Sil.pp_exp_printenv pe) idx1 (Sil.pp_sexp pe) se1'; + L.out "@[<4> IDX2: %a, STREXP2: %a@\n@." (Sil.pp_exp_printenv pe) idx2 (Sil.pp_sexp pe) se2'; assert false end else if Exp.equal idx1 idx2 then begin diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 321bd6633..b16a296b1 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -130,7 +130,7 @@ let execute___print_value { Builtin.tenv; pdesc; prop_; path; args; } let pname = Cfg.Procdesc.get_proc_name pdesc in let do_arg (lexp, _) = let n_lexp, _ = check_arith_norm_exp tenv pname lexp prop_ in - L.err "%a " (Sil.pp_exp pe_text) n_lexp in + L.err "%a " Exp.pp n_lexp in IList.iter do_arg args; L.err "@."; [(prop_, path)] diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index c47845cc4..3e9337870 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -184,7 +184,7 @@ let force_delayed_print fmt = for _ = 1 to n do F.fprintf fmt "@]" done | (L.PTexp, e) -> let (e: Exp.t) = Obj.obj e in - Sil.pp_exp pe_default fmt e + Sil.pp_exp_printenv pe_default fmt e | (L.PTexp_list, el) -> let (el: Exp.t list) = Obj.obj el in Sil.pp_exp_list pe_default fmt el diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 1e1b48c4e..590b1966e 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -195,9 +195,9 @@ let pp_sub_entry pe0 f entry = begin match pe.pe_kind with | PP_TEXT | PP_HTML -> - F.fprintf f "%a = %a" (Ident.pp pe) x (Sil.pp_exp pe) e + F.fprintf f "%a = %a" (Ident.pp pe) x (Sil.pp_exp_printenv pe) e | PP_LATEX -> - F.fprintf f "%a{=}%a" (Ident.pp pe) x (Sil.pp_exp pe) e + F.fprintf f "%a{=}%a" (Ident.pp pe) x (Sil.pp_exp_printenv pe) e end; Sil.color_post_wrapper changed pe0 f @@ -1498,13 +1498,13 @@ module Normalize = struct (fun (a : Sil.atom) -> match a with | Aneq (Const (Cint n), e) | Aneq (e, Const (Cint n)) -> - (not (IList.exists - (fun (e', n') -> Exp.equal e e' && IntLit.lt n' n) - le_list_tightened)) && - (not (IList.exists - (fun (n', e') -> Exp.equal e e' && IntLit.leq n n') - lt_list_tightened)) - | _ -> true) + (not (IList.exists + (fun (e', n') -> Exp.equal e e' && IntLit.lt n' n) + le_list_tightened)) && + (not (IList.exists + (fun (n', e') -> Exp.equal e e' && IntLit.leq n n') + lt_list_tightened)) + | _ -> true) nonineq_list in (ineq_list', nonineq_list') @@ -2368,7 +2368,7 @@ let prop_iter_make_id_primed tenv id iter = | Aeq (Var id1, e1) when Sil.ident_in_exp id1 e1 -> L.out "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n"; L.out "Broken Assumption: id notin e for all (id,e) in sub@\n"; - L.out "(id,e) : (%a,%a)@\n" (Ident.pp pe_text) id1 (Sil.pp_exp pe_text) e1; + L.out "(id,e) : (%a,%a)@\n" (Ident.pp pe_text) id1 Exp.pp e1; L.out "PROP : %a@\n@." (pp_prop pe_text) (prop_iter_to_prop tenv iter); assert false | Aeq (Var id1, e1) when Ident.equal pid id1 -> diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 9f121b97f..47c6c34d3 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1236,9 +1236,9 @@ let path_to_id path = | Exp.Lindex (e, ind) -> (match f e with | None -> None - | Some s -> Some (s ^ "_" ^ (Sil.exp_to_string ind))) + | Some s -> Some (s ^ "_" ^ (Exp.to_string ind))) | Exp.Lvar _ -> - Some (Sil.exp_to_string path) + Some (Exp.to_string path) | Exp.Const (Const.Cstr s) -> Some ("_const_str_" ^ s) | Exp.Const (Const.Cclass c) -> diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 572c1315f..c69616bae 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -422,7 +422,7 @@ let mk_ptsto_exp_footprint if not (Config.angelic_execution && !Config.footprint) then begin if Config.developer_mode then - L.err "!!!! Footprint Error, Bad Root : %a !!!! @\n" (Sil.pp_exp pe_text) lexp; + L.err "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp; let deref_str = Localise.deref_str_dangling None in let err_desc = Errdesc.explain_dereference tenv deref_str orig_prop (State.get_loc ()) in @@ -1408,14 +1408,3 @@ let rearrange ?(report_deref_errors=true) pdesc tenv lexp typ prop loc raise (Exceptions.Symexec_memory_error __POS__) end | Some iter -> iter_rearrange pname tenv nlexp typ prop' iter inst - -(* -let pp_off fmt off = - IList.iter (fun n -> match n with - | Sil.Off_fld (f, t) -> F.fprintf fmt "%a " Ident.pp_fieldname f - | Sil.Off_index e -> F.fprintf fmt "%a " (Sil.pp_exp pe_text) e) off - -let sort_ftl ftl = - let compare (f1, _) (f2, _) = Ident.fieldname_compare f1 f2 in - IList.sort compare ftl -*) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 49d5ed8ee..7196a43da 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -838,7 +838,7 @@ let check_taint_on_variadic_function tenv callee_pname caller_pname actual_param let actual_params' = n_tail actual_params tp_abs in L.d_str "Paramters to be checked: [ "; IList.iter(fun (e,_) -> - L.d_str (" " ^ (Sil.exp_to_string e) ^ " "); + L.d_str (" " ^ (Exp.to_string e) ^ " "); match Attribute.get_taint tenv calling_prop e with | Some (Apred (Ataint taint_info, _)) -> report_taint_error e taint_info callee_pname caller_pname calling_prop diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index e678fa564..a75f5c081 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -357,10 +357,10 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } = let handle_check_of_formal e = let repeated = Exp.Set.mem e !checks_to_formals in - if repeated && !verbose then L.stdout "Repeated Null Check of Formal: %a@." (Sil.pp_exp pe_text) e + if repeated && !verbose then L.stdout "Repeated Null Check of Formal: %a@." Exp.pp e else begin checks_to_formals := Exp.Set.add e !checks_to_formals; - if !verbose then L.stdout "Null Check of Formal: %a@." (Sil.pp_exp pe_text) e + if !verbose then L.stdout "Null Check of Formal: %a@." Exp.pp e end in let summary_checks_of_formals () = @@ -394,7 +394,7 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } = (Procname.java_get_class_name pname_java) (Procname.java_get_method pname_java) (Sil.pp_instr pe_text) instr - (Sil.pp_exp pe_text) arg1 + Exp.pp arg1 | _ -> ()) | _ -> () in diff --git a/infer/src/checkers/constantPropagation.ml b/infer/src/checkers/constantPropagation.ml index 5be05afb2..fd2b83754 100644 --- a/infer/src/checkers/constantPropagation.ml +++ b/infer/src/checkers/constantPropagation.ml @@ -30,7 +30,7 @@ module ConstantFlow = Dataflow.MakeDF(struct type t = (Const.t option) ConstantMap.t let pp fmt constants = - let pp_key fmt = Sil.pp_exp pe_text fmt in + let pp_key fmt = Exp.pp fmt in let print_kv k = function | Some v -> Format.fprintf fmt " %a -> %a@." pp_key k (Const.pp pe_text) v | _ -> Format.fprintf fmt " %a -> None@." pp_key k in diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index f40b647be..fd38911ab 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -893,12 +893,12 @@ struct { CallFlags.default with CallFlags.cf_is_objc_block = is_call_to_block; } in create_call_instr trans_state function_type sil_fe act_params sil_loc call_flags ~is_objc_method:false in - let nname = "Call "^(Sil.exp_to_string sil_fe) in + let nname = "Call "^(Exp.to_string sil_fe) in let all_res_trans = result_trans_subexprs @ [res_trans_call] in let res_trans_to_parent = PriorityNode.compute_results_to_parent trans_state_pri sil_loc nname si all_res_trans in let add_cg_edge callee_pname = - Cg.add_edge context.CContext.cg procname callee_pname + Cg.add_edge context.CContext.cg procname callee_pname in Option.may add_cg_edge callee_pname_opt; { res_trans_to_parent with exps = res_trans_call.exps } @@ -936,7 +936,7 @@ struct } in let res_trans_call = create_call_instr trans_state_pri function_type sil_method actual_params sil_loc call_flags ~is_objc_method:false in - let nname = "Call " ^ (Sil.exp_to_string sil_method) in + let nname = "Call " ^ (Exp.to_string sil_method) in let all_res_trans = result_trans_subexprs @ [res_trans_call; extra_res_trans] in let result_trans_to_parent = PriorityNode.compute_results_to_parent trans_state_pri sil_loc nname si all_res_trans in diff --git a/infer/src/eradicate/typeState.ml b/infer/src/eradicate/typeState.ml index e3bc04fcc..f49f91732 100644 --- a/infer/src/eradicate/typeState.ml +++ b/infer/src/eradicate/typeState.ml @@ -66,7 +66,7 @@ let pp ext fmt typestate = let pp_locs fmt locs = F.fprintf fmt " [%a]" (pp_seq pp_loc) locs in let pp_one exp (typ, ta, locs) = F.fprintf fmt " %a -> [%s] %s %a%a@\n" - (Sil.pp_exp pe_text) exp + Exp.pp exp (TypeOrigin.to_string (TypeAnnotation.get_origin ta)) (TypeAnnotation.to_string ta) (Typ.pp_full pe_text) typ pp_locs locs in diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index b902aff59..ec96d642b 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -275,7 +275,7 @@ module Make (TaintSpec : TaintSpec.S) = struct | None -> failwithf "Assignment to unexpected lhs expression %a in proc %a at loc %a" - (Sil.pp_exp pe_text) lhs_exp + Exp.pp lhs_exp Procname.pp (Cfg.Procdesc.get_proc_name (proc_data.pdesc)) Location.pp loc in let astate' = diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml index b9c31f3c5..bc0d6a033 100644 --- a/infer/src/unit/accessPathTests.ml +++ b/infer/src/unit/accessPathTests.ml @@ -87,7 +87,7 @@ let tests = fmt "Expected to make access path %a from expression %a, but got %a" AccessPath.pp_raw expected_ap - (Sil.pp_exp pe_text) exp + Exp.pp exp AccessPath.pp_raw actual_ap in assert_equal ~cmp:AccessPath.raw_equal ~pp_diff actual_ap expected_ap in diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 862a54c05..1d267127b 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -35,11 +35,11 @@ module StructuredSil = struct | If (exp, then_instrs, else_instrs) -> (* TODO (t10287763): indent bodies of if/while *) F.fprintf fmt "if (%a) {@.%a@.} else {@.%a@.}" - (Sil.pp_exp pe_text) exp + Exp.pp exp pp_structured_instr_list then_instrs pp_structured_instr_list else_instrs | While (exp, instrs) -> - F.fprintf fmt "while (%a) {@.%a@.}" (Sil.pp_exp pe_text) exp pp_structured_instr_list instrs + F.fprintf fmt "while (%a) {@.%a@.}" Exp.pp exp pp_structured_instr_list instrs | Try (try_, catch, finally) -> F.fprintf fmt diff --git a/infer/tests/repl/infer_batch_script.ml b/infer/tests/repl/infer_batch_script.ml index 5ba8262ac..921b127b1 100644 --- a/infer/tests/repl/infer_batch_script.ml +++ b/infer/tests/repl/infer_batch_script.ml @@ -17,6 +17,6 @@ let _ = Ident.create_fresh Ident.knormal in let ident = Ident.create_fresh Ident.knormal in let e = Exp.Var ident in -print_endline (Sil.exp_to_string e); +print_endline (Exp.to_string e); (* pass --flavors flag to change the value *) print_endline (string_of_bool Config.flavors)