[backend] move expression pretty-printing into exp module

Reviewed By: jberdine

Differential Revision: D4059909

fbshipit-source-id: b382cb1
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent 47c623ff51
commit 355ab92130

@ -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;

@ -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;

@ -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

@ -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;

@ -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;

@ -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.

@ -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
| [] -> ()

@ -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

@ -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

@ -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

@ -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)]

@ -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

@ -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 ->

@ -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) ->

@ -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
*)

@ -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

@ -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

@ -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

@ -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

@ -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

@ -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' =

@ -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

@ -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

@ -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)

Loading…
Cancel
Save