pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[infer] remove the utility functions to export debug information in LaTeX

Browse Source 
Summary: There is a lot of code to create LaTeX output of the Infer datastructures, but this does not seem to be used anymore.

Reviewed By: jvillard

Differential Revision: D6355686

fbshipit-source-id: 55de8e9
master
Jeremy Dubreil 7 years ago committed by Facebook Github Bot
parent 85ab063983
commit c195e67dfe
25 changed files with 103 additions and 518 deletions
Show Stats Download Patch File Download Diff File

3
infer/src/IR/Binop.ml
Unescape View File

@ -130,8 +130,5 @@ let str pe binop =
" >> " " >> "
| _ -> | _ ->
text binop ) text binop )
| LATEX -> (
match binop with Ge -> " \\geq " | Le -> " \\leq " | _ -> text binop )
| _ -> | _ ->
text binop text binop

3
infer/src/IR/Exp.ml
Unescape View File

@ -232,7 +232,7 @@ let rec pp_ pe pp_t f e =
in in
match (e : t) with match (e : t) with
| Var id -> | Var id ->
Ident.pp pe f id Ident.pp f id
| Const c -> | Const c ->
F.fprintf f "%a" (Const.pp pe) c F.fprintf f "%a" (Const.pp pe) c
| Cast (typ, e) -> | Cast (typ, e) ->
@ -277,4 +277,3 @@ let is_objc_block_closure = function
Typ.Procname.is_objc_block name Typ.Procname.is_objc_block name
| _ -> | _ ->
false false

19
infer/src/IR/Ident.ml
Unescape View File

@ -244,26 +244,11 @@ let to_string id =
(** Pretty print a name. *) (** Pretty print a name. *)
let pp_name f name = F.fprintf f "%s" (name_to_string name) let pp_name f name = F.fprintf f "%s" (name_to_string name)
(** Pretty print a name in latex. *)
let pp_name_latex style f (name: name) = Latex.pp_string style f (name_to_string name)
(** Pretty print an identifier. *) (** Pretty print an identifier. *)
let pp pe f id = let pp f id = F.fprintf f "%s" (to_string id)
match pe.Pp.kind with
| TEXT | HTML ->
F.fprintf f "%s" (to_string id)
| LATEX ->
let base_name = name_to_string id.name in
let style =
if has_kind id KFootprint then Latex.Boldface
else if has_kind id KNormal then Latex.Roman
else Latex.Roman
in
F.fprintf f "%a_{%s}" (Latex.pp_string style) base_name (string_of_int id.stamp)
(** pretty printer for lists of identifiers *) (** pretty printer for lists of identifiers *)
let pp_list pe = Pp.comma_seq (pp pe) let pp_list = Pp.comma_seq pp
(** pretty printer for lists of names *) (** pretty printer for lists of names *)
let pp_name_list = Pp.comma_seq pp_name let pp_name_list = Pp.comma_seq pp_name

7
infer/src/IR/Ident.mli
Unescape View File

@ -135,16 +135,13 @@ val set_stamp : t -> int -> t
val pp_name : Format.formatter -> name -> unit val pp_name : Format.formatter -> name -> unit
(** Pretty print a name. *) (** Pretty print a name. *)
val pp_name_latex : Latex.style -> Format.formatter -> name -> unit val pp : Format.formatter -> t -> unit
(** Pretty print a name in latex. *)
val pp : Pp.env -> Format.formatter -> t -> unit
(** Pretty print an identifier. *) (** Pretty print an identifier. *)
val to_string : t -> string val to_string : t -> string
(** Convert an identifier to a string. *) (** Convert an identifier to a string. *)
val pp_list : Pp.env -> Format.formatter -> t list -> unit val pp_list : Format.formatter -> t list -> unit
(** Pretty print a list of identifiers. *) (** Pretty print a list of identifiers. *)
val pp_name_list : Format.formatter -> name list -> unit val pp_name_list : Format.formatter -> name list -> unit

31
infer/src/IR/Pvar.ml
Unescape View File

@ -86,37 +86,13 @@ let pp_ f pv =
F.fprintf f "old_%a" Mangled.pp name F.fprintf f "old_%a" Mangled.pp name
(** Pretty print a program variable in latex. *)
let pp_latex f pv =
let name = pv.pv_name in
match pv.pv_kind with
| Local_var _ ->
Latex.pp_string Latex.Roman f (Mangled.to_string name)
| Callee_var _ ->
F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name)
(Latex.pp_string Latex.Roman) "callee"
| Abduced_retvar _ ->
F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name)
(Latex.pp_string Latex.Roman) "abducedRetvar"
| Abduced_ref_param _ ->
F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name)
(Latex.pp_string Latex.Roman) "abducedRefParam"
| Global_var _ ->
Latex.pp_string Latex.Boldface f (Mangled.to_string name)
| Seed_var ->
F.fprintf f "%a^{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name)
(Latex.pp_string Latex.Roman) "old"
(** Pretty print a pvar which denotes a value, not an address *) (** Pretty print a pvar which denotes a value, not an address *)
let pp_value pe f pv = let pp_value f pv = pp_ f pv
match pe.Pp.kind with TEXT -> pp_ f pv | HTML -> pp_ f pv | LATEX -> pp_latex f pv
(** Pretty print a program variable. *) (** Pretty print a program variable. *)
let pp pe f pv = let pp pe f pv =
let ampersand = match pe.Pp.kind with TEXT -> "&" | HTML -> "&" | LATEX -> "\\&" in let ampersand = match pe.Pp.kind with TEXT -> "&" | HTML -> "&" in
F.fprintf f "%s%a" ampersand (pp_value pe) pv F.fprintf f "%s%a" ampersand pp_value pv
(** Dump a program variable. *) (** Dump a program variable. *)
@ -291,4 +267,3 @@ let get_initializer_pname {pv_name; pv_kind} =
else Some (Typ.Procname.from_string_c_fun name) else Some (Typ.Procname.from_string_c_fun name)
| _ -> | _ ->
None None

2
infer/src/IR/Pvar.mli
Unescape View File

@ -105,7 +105,7 @@ val pp : Pp.env -> F.formatter -> t -> unit
val pp_list : Pp.env -> F.formatter -> t list -> unit val pp_list : Pp.env -> F.formatter -> t list -> unit
(** Pretty print a list of program variables. *) (** Pretty print a list of program variables. *)
val pp_value : Pp.env -> F.formatter -> t -> unit val pp_value : F.formatter -> t -> unit
(** Pretty print a pvar which denotes a value, not an address *) (** Pretty print a pvar which denotes a value, not an address *)
val pp_translation_unit : F.formatter -> translation_unit -> unit val pp_translation_unit : F.formatter -> translation_unit -> unit

131
infer/src/IR/Sil.ml
Unescape View File

@ -262,9 +262,7 @@ let color_pre_wrapper pe f x =
if Config.print_using_diff && pe.Pp.kind <> Pp.TEXT then if Config.print_using_diff && pe.Pp.kind <> Pp.TEXT then
let color = pe.Pp.cmap_norm (Obj.repr x) in let color = pe.Pp.cmap_norm (Obj.repr x) in
if color <> pe.Pp.color then ( if color <> pe.Pp.color then (
( if Pp.equal_print_kind pe.Pp.kind Pp.HTML then Io_infer.Html.pp_start_color Io_infer.Html.pp_start_color f color ;
else Latex.pp_color )
f color ;
if Pp.equal_color color Pp.Red then if Pp.equal_color color Pp.Red then
(* All subexpressions red *) (* All subexpressions red *)
(Pp.{pe with cmap_norm= colormap_red; color= Red}, true) (Pp.{pe with cmap_norm= colormap_red; color= Red}, true)
@ -274,11 +272,7 @@ let color_pre_wrapper pe f x =
(** Close color annotation if changed *) (** Close color annotation if changed *)
let color_post_wrapper changed pe f = let color_post_wrapper changed f = if changed then Io_infer.Html.pp_end_color f ()
if changed then
if Pp.equal_print_kind pe.Pp.kind Pp.HTML then Io_infer.Html.pp_end_color f ()
else Latex.pp_color f pe.Pp.color
(** Print a sequence with difference mode if enabled. *) (** Print a sequence with difference mode if enabled. *)
let pp_seq_diff pp pe0 f = let pp_seq_diff pp pe0 f =
@ -289,10 +283,10 @@ let pp_seq_diff pp pe0 f =
() ()
| [x] -> | [x] ->
let _, changed = color_pre_wrapper pe0 f x in let _, changed = color_pre_wrapper pe0 f x in
F.fprintf f "%a" pp x ; color_post_wrapper changed pe0 f F.fprintf f "%a" pp x ; color_post_wrapper changed f
| x :: l -> | x :: l ->
let _, changed = color_pre_wrapper pe0 f x in let _, changed = color_pre_wrapper pe0 f x in
F.fprintf f "%a" pp x ; color_post_wrapper changed pe0 f ; F.fprintf f ", " ; doit l F.fprintf f "%a" pp x ; color_post_wrapper changed f ; F.fprintf f ", " ; doit l
in in
doit doit
@ -308,9 +302,9 @@ let pp_exp_printenv pe0 f e0 =
e0 e0
in in
if not (Exp.equal e0 e) then if not (Exp.equal e0 e) then
match e with Exp.Lvar pvar -> Pvar.pp_value pe f pvar | _ -> assert false match e with Exp.Lvar pvar -> Pvar.pp_value f pvar | _ -> assert false
else Exp.pp_printenv pe Typ.pp f e ; else Exp.pp_printenv pe Typ.pp f e ;
color_post_wrapper changed pe0 f color_post_wrapper changed f
(** dump an expression. *) (** dump an expression. *)
@ -413,15 +407,14 @@ let pp_instr pe0 f instr =
let pe, changed = color_pre_wrapper pe0 f instr in let pe, changed = color_pre_wrapper pe0 f instr in
( match instr with ( match instr with
| Load (id, e, t, loc) -> | Load (id, e, t, loc) ->
F.fprintf f "%a=*%a:%a [%a]" (Ident.pp pe) id (pp_exp_printenv pe) e (Typ.pp pe) t F.fprintf f "%a=*%a:%a [%a]" Ident.pp id (pp_exp_printenv pe) e (Typ.pp pe) t Location.pp loc
Location.pp loc
| Store (e1, t, e2, loc) -> | Store (e1, t, e2, loc) ->
F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv pe) e1 (Typ.pp pe) t (pp_exp_printenv pe) e2 F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv pe) e1 (Typ.pp pe) t (pp_exp_printenv pe) e2
Location.pp loc Location.pp loc
| Prune (cond, loc, true_branch, _) -> | Prune (cond, loc, true_branch, _) ->
F.fprintf f "PRUNE(%a, %b); [%a]" (pp_exp_printenv 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) -> | Call (ret_id, e, arg_ts, loc, cf) ->
(match ret_id with None -> () | Some (id, _) -> F.fprintf f "%a=" (Ident.pp pe) id) ; (match ret_id with None -> () | Some (id, _) -> F.fprintf f "%a=" Ident.pp id) ;
F.fprintf f "%a(%a)%a [%a]" (pp_exp_printenv pe) e F.fprintf f "%a(%a)%a [%a]" (pp_exp_printenv pe) e
(Pp.comma_seq (pp_exp_typ pe)) (Pp.comma_seq (pp_exp_typ pe))
arg_ts CallFlags.pp cf Location.pp loc arg_ts CallFlags.pp cf Location.pp loc
@ -430,11 +423,11 @@ let pp_instr pe0 f instr =
| Abstract loc -> | Abstract loc ->
F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc
| Remove_temps (temps, loc) -> | Remove_temps (temps, loc) ->
F.fprintf f "REMOVE_TEMPS(%a); [%a]" (Ident.pp_list pe) temps Location.pp loc F.fprintf f "REMOVE_TEMPS(%a); [%a]" Ident.pp_list temps Location.pp loc
| Declare_locals (ptl, loc) -> | Declare_locals (ptl, loc) ->
let pp_typ fmt (pvar, _) = Pvar.pp pe fmt pvar in let pp_typ fmt (pvar, _) = Pvar.pp pe fmt pvar in
F.fprintf f "DECLARE_LOCALS(%a); [%a]" (Pp.comma_seq pp_typ) ptl Location.pp loc ) ; F.fprintf f "DECLARE_LOCALS(%a); [%a]" (Pp.comma_seq pp_typ) ptl Location.pp loc ) ;
color_post_wrapper changed pe0 f color_post_wrapper changed f
let add_with_block_parameters_flag instr = let add_with_block_parameters_flag instr =
@ -470,29 +463,17 @@ let d_instr_list (il: instr list) = L.add_print_action (L.PTinstr_list, Obj.repr
let pp_atom pe0 f a = let pp_atom pe0 f a =
let pe, changed = color_pre_wrapper pe0 f a in let pe, changed = color_pre_wrapper pe0 f a in
( match a with ( match a with
| Aeq (BinOp (op, e1, e2), Const Cint i) when IntLit.isone i -> ( | Aeq (BinOp (op, e1, e2), Const Cint i) when IntLit.isone i ->
match pe.Pp.kind with F.fprintf f "%a" (pp_exp_printenv pe) (Exp.BinOp (op, e1, e2))
| TEXT | HTML -> | Aeq (e1, e2) ->
F.fprintf f "%a" (pp_exp_printenv pe) (Exp.BinOp (op, e1, e2)) F.fprintf f "%a = %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2
| LATEX -> | Aneq (e1, e2) ->
F.fprintf f "%a" (pp_exp_printenv pe) (Exp.BinOp (op, e1, e2)) ) F.fprintf f "%a != %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2
| Aeq (e1, e2) -> (
match pe.Pp.kind with
| TEXT | HTML ->
F.fprintf f "%a = %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2
| LATEX ->
F.fprintf f "%a{=}%a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 )
| Aneq (e1, e2) -> (
match pe.Pp.kind with
| TEXT | HTML ->
F.fprintf f "%a != %a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2
| LATEX ->
F.fprintf f "%a{\\neq}%a" (pp_exp_printenv pe) e1 (pp_exp_printenv pe) e2 )
| Apred (a, es) -> | 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 (pp_exp_printenv pe)) es
| Anpred (a, 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 (pp_exp_printenv pe)) es ) ;
color_post_wrapper changed pe0 f color_post_wrapper changed f
(** dump an atom *) (** dump an atom *)
@ -862,31 +843,23 @@ let rec pp_sexp_env pe0 envo f se =
( match se with ( match se with
| Eexp (e, inst) -> | Eexp (e, inst) ->
F.fprintf f "%a%a" (pp_exp_printenv pe) e (pp_inst_if_trace pe) inst F.fprintf f "%a%a" (pp_exp_printenv pe) e (pp_inst_if_trace pe) inst
| Estruct (fel, inst) -> ( | Estruct (fel, inst) ->
match pe.Pp.kind with let pp_diff f (n, se) = F.fprintf f "%a:%a" Typ.Fieldname.pp n (pp_sexp_env pe envo) se in
| TEXT | HTML -> F.fprintf f "{%a}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) 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
| LATEX ->
let pp_diff f (n, se) =
F.fprintf f "%a:%a" (Typ.Fieldname.pp_latex Latex.Boldface) 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) -> | Earray (len, nel, inst) ->
let pp_diff f (i, se) = 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" (pp_exp_printenv pe) i (pp_sexp_env pe envo) se
in in
F.fprintf f "[%a|%a]%a" (pp_exp_printenv pe) len (pp_seq_diff pp_diff pe) nel F.fprintf f "[%a|%a]%a" (pp_exp_printenv pe) len (pp_seq_diff pp_diff pe) nel
(pp_inst_if_trace pe) inst ) ; (pp_inst_if_trace pe) inst ) ;
color_post_wrapper changed pe0 f color_post_wrapper changed f
(** Pretty print an hpred with an optional predicate env *) (** Pretty print an hpred with an optional predicate env *)
let rec pp_hpred_env pe0 envo f hpred = let rec pp_hpred_env pe0 envo f hpred =
let pe, changed = color_pre_wrapper pe0 f hpred in let pe, changed = color_pre_wrapper pe0 f hpred in
( match hpred with ( match hpred with
| Hpointsto (e, se, te) | Hpointsto (e, se, te) ->
-> (
let pe' = let pe' =
match (e, se) with match (e, se) with
| Lvar pvar, Eexp (Var _, _) when not (Pvar.is_global pvar) -> | Lvar pvar, Eexp (Var _, _) when not (Pvar.is_global pvar) ->
@ -894,49 +867,27 @@ let rec pp_hpred_env pe0 envo f hpred =
| _ -> | _ ->
pe pe
in in
match pe'.Pp.kind with F.fprintf f "%a|->%a:%a" (pp_exp_printenv pe') e (pp_sexp_env pe' envo) se
| TEXT | HTML -> (pp_texp_simple pe') te
F.fprintf f "%a|->%a:%a" (pp_exp_printenv pe') e (pp_sexp_env pe' envo) se | Hlseg (k, hpara, e1, e2, elist) ->
(pp_texp_simple pe') te F.fprintf f "lseg%a(%a,%a,[%a],%a)" pp_lseg_kind k (pp_exp_printenv pe) e1
| LATEX -> (pp_exp_printenv pe) e2
F.fprintf f "%a\\mapsto %a" (pp_exp_printenv pe') e (pp_sexp_env pe' envo) se ) (Pp.comma_seq (pp_exp_printenv pe))
| Hlseg (k, hpara, e1, e2, elist) -> ( elist (pp_hpara_env pe envo) hpara
match pe.Pp.kind with
| TEXT | HTML ->
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))
elist (pp_hpara_env pe envo) hpara
| LATEX ->
F.fprintf f "\\textsf{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))
elist (pp_hpara_env pe envo) hpara )
| Hdllseg (k, hpara_dll, iF, oB, oF, iB, elist) -> | Hdllseg (k, hpara_dll, iF, oB, oF, iB, elist) ->
match pe.Pp.kind with F.fprintf f "dllseg%a(%a,%a,%a,%a,[%a],%a)" pp_lseg_kind k (pp_exp_printenv pe) iF
| TEXT | HTML -> (pp_exp_printenv pe) oB (pp_exp_printenv pe) oF (pp_exp_printenv pe) iB
F.fprintf f "dllseg%a(%a,%a,%a,%a,[%a],%a)" pp_lseg_kind k (pp_exp_printenv pe) iF (Pp.comma_seq (pp_exp_printenv pe))
(pp_exp_printenv pe) oB (pp_exp_printenv pe) oF (pp_exp_printenv pe) iB elist (pp_hpara_dll_env pe envo) hpara_dll ) ;
(Pp.comma_seq (pp_exp_printenv pe)) color_post_wrapper changed f
elist (pp_hpara_dll_env pe envo) hpara_dll
| LATEX ->
F.fprintf f "\\textsf{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))
elist (pp_hpara_dll_env pe envo) hpara_dll ) ;
color_post_wrapper changed pe0 f
and pp_hpara_env pe envo f hpara = and pp_hpara_env pe envo f hpara =
match envo with match envo with
| None -> | None ->
let r, n, svars, evars, b = (hpara.root, hpara.next, hpara.svars, hpara.evars, hpara.body) in let r, n, svars, evars, b = (hpara.root, hpara.next, hpara.svars, hpara.evars, hpara.body) in
F.fprintf f "lam [%a,%a,%a]. exists [%a]. %a" (Ident.pp pe) r (Ident.pp pe) n F.fprintf f "lam [%a,%a,%a]. exists [%a]. %a" Ident.pp r Ident.pp n (Pp.seq Ident.pp) svars
(Pp.seq (Ident.pp pe)) (Pp.seq Ident.pp) evars
svars
(Pp.seq (Ident.pp pe))
evars
(pp_star_seq (pp_hpred_env pe envo)) (pp_star_seq (pp_hpred_env pe envo))
b b
| Some env -> | Some env ->
@ -954,12 +905,8 @@ and pp_hpara_dll_env pe envo f hpara_dll =
, hpara_dll.evars_dll , hpara_dll.evars_dll
, hpara_dll.body_dll ) , hpara_dll.body_dll )
in in
F.fprintf f "lam [%a,%a,%a,%a]. exists [%a]. %a" (Ident.pp pe) iF (Ident.pp pe) oB F.fprintf f "lam [%a,%a,%a,%a]. exists [%a]. %a" Ident.pp iF Ident.pp oB Ident.pp oF
(Ident.pp pe) oF (Pp.seq Ident.pp) svars (Pp.seq Ident.pp) evars
(Pp.seq (Ident.pp pe))
svars
(Pp.seq (Ident.pp pe))
evars
(pp_star_seq (pp_hpred_env pe envo)) (pp_star_seq (pp_hpred_env pe envo))
b b
| Some env -> | Some env ->
@ -1242,7 +1189,7 @@ let fav_from_list l =
let fav_to_list fav = List.rev !fav let fav_to_list fav = List.rev !fav
(** Pretty print a fav. *) (** Pretty print a fav. *)
let pp_fav pe f fav = Pp.seq (Ident.pp pe) f (fav_to_list fav) let pp_fav f fav = Pp.seq Ident.pp f (fav_to_list fav)
(** Copy a [fav]. *) (** Copy a [fav]. *)
let fav_copy fav = ref (List.map ~f:(fun x -> x) !fav) let fav_copy fav = ref (List.map ~f:(fun x -> x) !fav)

4
infer/src/IR/Sil.mli
Unescape View File

@ -289,7 +289,7 @@ val hpred_get_lhs : hpred -> Exp.t
val color_pre_wrapper : Pp.env -> F.formatter -> 'a -> Pp.env * bool val color_pre_wrapper : Pp.env -> F.formatter -> 'a -> Pp.env * bool
(** Begin change color if using diff printing, return updated printenv and change status *) (** Begin change color if using diff printing, return updated printenv and change status *)
val color_post_wrapper : bool -> Pp.env -> F.formatter -> unit val color_post_wrapper : bool -> F.formatter -> unit
(** Close color annotation if changed *) (** Close color annotation if changed *)
val pp_exp_printenv : Pp.env -> F.formatter -> Exp.t -> unit val pp_exp_printenv : Pp.env -> F.formatter -> Exp.t -> unit
@ -476,7 +476,7 @@ val fav_duplicates : bool ref
(** flag to indicate whether fav's are stored in duplicate form. (** flag to indicate whether fav's are stored in duplicate form.
Only to be used with fav_to_list *) Only to be used with fav_to_list *)
val pp_fav : Pp.env -> F.formatter -> fav -> unit val pp_fav : F.formatter -> fav -> unit
(** Pretty print a fav. *) (** Pretty print a fav. *)
val fav_new : unit -> fav val fav_new : unit -> fav

2
infer/src/IR/Typ.ml
Unescape View File

@ -1279,8 +1279,6 @@ module Fieldname = struct
Format.fprintf f "%s" field_name Format.fprintf f "%s" field_name
let pp_latex style f fn = Latex.pp_string style f (to_string fn)
let class_name_replace fname ~f = let class_name_replace fname ~f =
match fname with match fname with
| Clang {class_name; field_name} -> | Clang {class_name; field_name} ->

3
infer/src/IR/Typ.mli
Unescape View File

@ -589,9 +589,6 @@ module Fieldname : sig
val pp : Format.formatter -> t -> unit val pp : Format.formatter -> t -> unit
(** Pretty print a field name. *) (** Pretty print a field name. *)
val pp_latex : Latex.style -> Format.formatter -> t -> unit
(** Pretty print a field name in latex. *)
val java_get_class : t -> string val java_get_class : t -> string
(** The class part of the fieldname *) (** The class part of the fieldname *)

7
infer/src/absint/Var.ml
Unescape View File

@ -29,12 +29,7 @@ let is_return = function ProgramVar pvar -> Pvar.is_return pvar | LogicalVar _ -
let is_footprint = function ProgramVar _ -> false | LogicalVar id -> Ident.is_footprint id let is_footprint = function ProgramVar _ -> false | LogicalVar id -> Ident.is_footprint id
let pp fmt = function let pp fmt = function ProgramVar pv -> Pvar.pp Pp.text fmt pv | LogicalVar id -> Ident.pp fmt id
| ProgramVar pv ->
Pvar.pp Pp.text fmt pv
| LogicalVar id ->
Ident.pp Pp.text fmt id
module Map = PrettyPrintable.MakePPMap (struct module Map = PrettyPrintable.MakePPMap (struct
type nonrec t = t type nonrec t = t

145
infer/src/backend/InferPrint.ml
Unescape View File

@ -32,14 +32,6 @@ let load_specfiles () =
specs_files_in_dir result_specs_dir specs_files_in_dir result_specs_dir
(** Create and initialize latex file *)
let begin_latex_file fmt =
let author = "Infer " ^ Version.versionString in
let title = "Report on Analysis Results" in
let table_of_contents = true in
Latex.pp_begin fmt (author, title, table_of_contents)
let error_desc_to_csv_string error_desc = let error_desc_to_csv_string error_desc =
let pp fmt = F.fprintf fmt "%a" Localise.pp_error_desc error_desc in let pp fmt = F.fprintf fmt "%a" Localise.pp_error_desc error_desc in
Escape.escape_csv (F.asprintf "%t" pp) Escape.escape_csv (F.asprintf "%t" pp)
@ -684,55 +676,6 @@ module Report = struct
let pp_stats fmt stats = Stats.pp fmt stats let pp_stats fmt stats = Stats.pp fmt stats
end end
module Summary = struct
let pp_summary_out summary =
let proc_name = Specs.get_proc_name summary in
if CLOpt.equal_command Config.command CLOpt.Report && not Config.quiet then
L.result "Procedure: %a@\n%a@." Typ.Procname.pp proc_name Specs.pp_summary_text summary
(** Write proc summary to latex file *)
let write_summary_latex fmt summary =
let proc_name = Specs.get_proc_name summary in
Latex.pp_section fmt
("Analysis of function " ^ Latex.convert_string (Typ.Procname.to_string proc_name)) ;
F.fprintf fmt "@[<v>%a@]" (Specs.pp_summary_latex Black) summary
let pp_summary_xml summary fname =
if Config.xml_specs then
let base = DB.chop_extension (DB.filename_from_string fname) in
let xml_file = DB.filename_add_suffix base ".xml" in
let specs = Specs.get_specs_from_payload summary in
if not (DB.file_exists xml_file)
|| DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time xml_file
then
let xml_out = Utils.create_outfile (DB.filename_to_string xml_file) in
Utils.do_outf xml_out (fun outf ->
Dotty.print_specs_xml (Specs.get_signature summary) specs (Specs.get_loc summary)
outf.fmt ;
Utils.close_outf outf )
let print_summary_dot_svg summary fname =
if Config.svg then
let base = DB.chop_extension (DB.filename_from_string fname) in
let specs = Specs.get_specs_from_payload summary in
let dot_file = DB.filename_add_suffix base ".dot" in
let svg_file = DB.filename_add_suffix base ".svg" in
if not (DB.file_exists dot_file)
|| DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time dot_file
then Dotty.pp_speclist_dotty_file base specs ;
if not (DB.file_exists svg_file)
|| DB.file_modified_time dot_file > DB.file_modified_time svg_file
then
ignore
(Sys.command
( "dot -Tsvg \"" ^ DB.filename_to_string dot_file ^ "\" >\""
^ DB.filename_to_string svg_file ^ "\"" ))
end
(** Categorize the preconditions of specs and print stats *) (** Categorize the preconditions of specs and print stats *)
module PreconditionStats = struct module PreconditionStats = struct
let nr_nopres = ref 0 let nr_nopres = ref 0
@ -811,9 +754,9 @@ let error_filter filters proc_name file error_desc error_name =
&& filters.Inferconfig.error_filter error_name && filters.Inferconfig.proc_filter proc_name && filters.Inferconfig.error_filter error_name && filters.Inferconfig.proc_filter proc_name
type report_kind = Issues | Procs | Stats | Calls | Summary [@@deriving compare] type report_kind = Issues | Procs | Stats | Calls [@@deriving compare]
type bug_format_kind = Json | Csv | Tests | Text | Latex [@@deriving compare] type bug_format_kind = Json | Csv | Tests | Text [@@deriving compare]
let pp_issue_in_format (format_kind, (outf: Utils.outfile)) error_filter let pp_issue_in_format (format_kind, (outf: Utils.outfile)) error_filter
{Issue.proc_name; proc_location; err_key; err_data} = {Issue.proc_name; proc_location; err_key; err_data} =
@ -822,8 +765,6 @@ let pp_issue_in_format (format_kind, (outf: Utils.outfile)) error_filter
IssuesCsv.pp_issue outf.fmt error_filter proc_name (Some proc_location) err_key err_data IssuesCsv.pp_issue outf.fmt error_filter proc_name (Some proc_location) err_key err_data
| Json -> | Json ->
IssuesJson.pp_issue outf.fmt error_filter proc_name (Some proc_location) err_key err_data IssuesJson.pp_issue outf.fmt error_filter proc_name (Some proc_location) err_key err_data
| Latex ->
L.(die InternalError) "Printing issues in latex is not implemented"
| Tests -> | Tests ->
L.(die InternalError) "Print issues as tests is not implemented" L.(die InternalError) "Print issues as tests is not implemented"
| Text -> | Text ->
@ -840,40 +781,30 @@ let pp_issues_in_format (format_kind, (outf: Utils.outfile)) =
L.(die InternalError) "Print issues as tests is not implemented" L.(die InternalError) "Print issues as tests is not implemented"
| Text -> | Text ->
IssuesTxt.pp_issues_of_error_log outf.fmt IssuesTxt.pp_issues_of_error_log outf.fmt
| Latex ->
L.(die InternalError) "Printing issues in latex is not implemented"
let pp_procs_in_format (format_kind, (outf: Utils.outfile)) = let pp_procs_in_format (format_kind, (outf: Utils.outfile)) =
match format_kind with match format_kind with
| Csv -> | Csv ->
ProcsCsv.pp_summary outf.fmt ProcsCsv.pp_summary outf.fmt
| Json | Latex | Tests | Text -> | Json | Tests | Text ->
L.(die InternalError) "Printing procs in json/latex/tests/text is not implemented" L.(die InternalError) "Printing procs in json/tests/text is not implemented"
let pp_calls_in_format (format_kind, (outf: Utils.outfile)) = let pp_calls_in_format (format_kind, (outf: Utils.outfile)) =
match format_kind with match format_kind with
| Csv -> | Csv ->
CallsCsv.pp_calls outf.fmt CallsCsv.pp_calls outf.fmt
| Json | Tests | Text | Latex -> | Json | Tests | Text ->
L.(die InternalError) "Printing calls in json/tests/text/latex is not implemented" L.(die InternalError) "Printing calls in json/tests/text is not implemented"
let pp_stats_in_format (format_kind, _) = let pp_stats_in_format (format_kind, _) =
match format_kind with match format_kind with
| Csv -> | Csv ->
Stats.process_summary Stats.process_summary
| Json | Tests | Text | Latex -> | Json | Tests | Text ->
L.(die InternalError) "Printing stats in json/tests/text/latex is not implemented" L.(die InternalError) "Printing stats in json/tests/text is not implemented"
let pp_summary_in_format (format_kind, (outf: Utils.outfile)) =
match format_kind with
| Latex ->
Summary.write_summary_latex outf.fmt
| Json | Csv | Tests | Text ->
L.(die InternalError) "Printing summary in json/csv/tests/text is not implemented"
let pp_issues_of_error_log error_filter linereader proc_loc_opt procname err_log bug_format_list = let pp_issues_of_error_log error_filter linereader proc_loc_opt procname err_log bug_format_list =
@ -916,19 +847,8 @@ let pp_stats error_filter linereader summary stats stats_format_list =
List.iter ~f:pp_stats_in_format stats_format_list List.iter ~f:pp_stats_in_format stats_format_list
let pp_summary summary fname summary_format_list = let pp_summary_by_report_kind formats_by_report_kind summary error_filter linereader stats file
let pp_summary_in_format format = issues_acc =
let pp_summary = pp_summary_in_format format in
pp_summary summary
in
List.iter ~f:pp_summary_in_format summary_format_list ;
Summary.pp_summary_out summary ;
Summary.pp_summary_xml summary fname ;
Summary.print_summary_dot_svg summary fname
let pp_summary_by_report_kind formats_by_report_kind summary fname error_filter linereader stats
file issues_acc =
let pp_summary_by_report_kind (report_kind, format_list) = let pp_summary_by_report_kind (report_kind, format_list) =
match (report_kind, format_list) with match (report_kind, format_list) with
| Procs, _ :: _ -> | Procs, _ :: _ ->
@ -937,8 +857,6 @@ let pp_summary_by_report_kind formats_by_report_kind summary fname error_filter
pp_stats (error_filter file) linereader summary stats format_list pp_stats (error_filter file) linereader summary stats format_list
| Calls, _ :: _ -> | Calls, _ :: _ ->
pp_calls summary format_list pp_calls summary format_list
| Summary, _ ->
pp_summary summary fname format_list
| _ -> | _ ->
() ()
in in
@ -960,8 +878,6 @@ let pp_json_report_by_report_kind formats_by_report_kind fname =
L.(die InternalError) "Printing issues from json does not support json output" L.(die InternalError) "Printing issues from json does not support json output"
| Csv -> | Csv ->
L.(die InternalError) "Printing issues from json does not support csv output" L.(die InternalError) "Printing issues from json does not support csv output"
| Latex ->
L.(die InternalError) "Printing issues from json does not support latex output"
in in
List.iter ~f:pp_json_issue format_list List.iter ~f:pp_json_issue format_list
in in
@ -999,15 +915,15 @@ let pp_lint_issues filters formats_by_report_kind linereader procname error_log
(** Process a summary *) (** Process a summary *)
let process_summary filters formats_by_report_kind linereader stats fname summary issues_acc = let process_summary filters formats_by_report_kind linereader stats summary issues_acc =
let file = (Specs.get_loc summary).Location.file in let file = (Specs.get_loc summary).Location.file in
let proc_name = Specs.get_proc_name summary in let proc_name = Specs.get_proc_name summary in
let error_filter = error_filter filters proc_name in let error_filter = error_filter filters proc_name in
let pp_simple_saved = !Config.pp_simple in let pp_simple_saved = !Config.pp_simple in
Config.pp_simple := true ; Config.pp_simple := true ;
let issues_acc' = let issues_acc' =
pp_summary_by_report_kind formats_by_report_kind summary fname error_filter linereader stats pp_summary_by_report_kind formats_by_report_kind summary error_filter linereader stats file
file issues_acc issues_acc
in in
if Config.precondition_stats then PreconditionStats.do_summary proc_name summary ; if Config.precondition_stats then PreconditionStats.do_summary proc_name summary ;
Config.pp_simple := pp_simple_saved ; Config.pp_simple := pp_simple_saved ;
@ -1135,11 +1051,6 @@ let init_stats_format_list () =
csv_format csv_format
let init_summary_format_list () =
let latex_format = Option.value_map ~f:(mk_format Latex) ~default:[] Config.latex in
latex_format
let init_files format_list_by_kind = let init_files format_list_by_kind =
let init_files_of_report_kind (report_kind, format_list) = let init_files_of_report_kind (report_kind, format_list) =
let init_files_of_format (format_kind, (outfile: Utils.outfile)) = let init_files_of_format (format_kind, (outfile: Utils.outfile)) =
@ -1152,9 +1063,7 @@ let init_files format_list_by_kind =
Report.pp_header outfile.fmt () Report.pp_header outfile.fmt ()
| Json, Issues -> | Json, Issues ->
IssuesJson.pp_json_open outfile.fmt () IssuesJson.pp_json_open outfile.fmt ()
| Latex, Summary -> | (Csv | Json | Tests | Text), _ ->
begin_latex_file outfile.fmt
| (Csv | Json | Latex | Tests | Text), _ ->
() ()
in in
List.iter ~f:init_files_of_format format_list List.iter ~f:init_files_of_format format_list
@ -1162,7 +1071,7 @@ let init_files format_list_by_kind =
List.iter ~f:init_files_of_report_kind format_list_by_kind List.iter ~f:init_files_of_report_kind format_list_by_kind
let finalize_and_close_files format_list_by_kind stats pdflatex = let finalize_and_close_files format_list_by_kind stats =
let close_files_of_report_kind (report_kind, format_list) = let close_files_of_report_kind (report_kind, format_list) =
let close_files_of_format (format_kind, (outfile: Utils.outfile)) = let close_files_of_format (format_kind, (outfile: Utils.outfile)) =
( match (format_kind, report_kind) with ( match (format_kind, report_kind) with
@ -1170,18 +1079,9 @@ let finalize_and_close_files format_list_by_kind stats pdflatex =
F.fprintf outfile.fmt "%a@?" Report.pp_stats stats F.fprintf outfile.fmt "%a@?" Report.pp_stats stats
| Json, Issues -> | Json, Issues ->
IssuesJson.pp_json_close outfile.fmt () IssuesJson.pp_json_close outfile.fmt ()
| Latex, Summary -> | (Csv | Tests | Text | Json), _ ->
Latex.pp_end outfile.fmt ()
| (Csv | Latex | Tests | Text | Json), _ ->
() ) ; () ) ;
Utils.close_outf outfile ; Utils.close_outf outfile
(* bug_format_kind report_kind *)
if [%compare.equal : bug_format_kind * report_kind]
(format_kind, report_kind) (Latex, Summary)
then (
pdflatex outfile.fname ;
let pdf_name = Filename.chop_extension outfile.fname ^ ".pdf" in
ignore (Sys.command ("open " ^ pdf_name)) )
in in
List.iter ~f:close_files_of_format format_list ; List.iter ~f:close_files_of_format format_list ;
() ()
@ -1190,16 +1090,14 @@ let finalize_and_close_files format_list_by_kind stats pdflatex =
let pp_summary_and_issues formats_by_report_kind issue_formats = let pp_summary_and_issues formats_by_report_kind issue_formats =
let pdflatex fname = ignore (Sys.command ("pdflatex " ^ fname)) in
let stats = Stats.create () in let stats = Stats.create () in
let linereader = Printer.LineReader.create () in let linereader = Printer.LineReader.create () in
let filters = Inferconfig.create_filters Config.analyzer in let filters = Inferconfig.create_filters Config.analyzer in
let iterate_summaries = AnalysisResults.get_summary_iterator () in let iterate_summaries = AnalysisResults.get_summary_iterator () in
let all_issues = ref [] in let all_issues = ref [] in
iterate_summaries (fun (filename, summary) -> iterate_summaries (fun (_, summary) ->
all_issues all_issues
:= process_summary filters formats_by_report_kind linereader stats filename summary := process_summary filters formats_by_report_kind linereader stats summary !all_issues ) ;
!all_issues ) ;
List.iter List.iter
~f:(fun ({Issue.proc_name} as issue) -> ~f:(fun ({Issue.proc_name} as issue) ->
let error_filter = error_filter filters proc_name in let error_filter = error_filter filters proc_name in
@ -1212,7 +1110,7 @@ let pp_summary_and_issues formats_by_report_kind issue_formats =
Typ.Procname.Map.iter Typ.Procname.Map.iter
(pp_lint_issues filters formats_by_report_kind linereader) (pp_lint_issues filters formats_by_report_kind linereader)
!LintIssues.errLogMap ; !LintIssues.errLogMap ;
finalize_and_close_files formats_by_report_kind stats pdflatex finalize_and_close_files formats_by_report_kind stats
let main ~report_csv ~report_json = let main ~report_csv ~report_json =
@ -1221,8 +1119,7 @@ let main ~report_csv ~report_json =
[ (Issues, issue_formats) [ (Issues, issue_formats)
; (Procs, init_procs_format_list ()) ; (Procs, init_procs_format_list ())
; (Calls, init_calls_format_list ()) ; (Calls, init_calls_format_list ())
; (Stats, init_stats_format_list ()) ; (Stats, init_stats_format_list ()) ]
; (Summary, init_summary_format_list ()) ]
in in
if Config.developer_mode then register_perf_stats_report () ; if Config.developer_mode then register_perf_stats_report () ;
init_files formats_by_report_kind ; init_files formats_by_report_kind ;

3
infer/src/backend/dotty.ml
Unescape View File

@ -135,7 +135,7 @@ let rec strexp_to_string pe coo f se =
| Sil.Eexp (Exp.Lvar pvar, _) -> | Sil.Eexp (Exp.Lvar pvar, _) ->
F.fprintf f "%a" (Pvar.pp pe) pvar F.fprintf f "%a" (Pvar.pp pe) pvar
| Sil.Eexp (Exp.Var id, _) -> | Sil.Eexp (Exp.Var id, _) ->
if !print_full_prop then F.fprintf f "%a" (Ident.pp pe) id else () if !print_full_prop then F.fprintf f "%a" Ident.pp id else ()
| Sil.Eexp (e, _) -> | Sil.Eexp (e, _) ->
if !print_full_prop then F.fprintf f "%a" (Sil.pp_exp_printenv pe) e else F.fprintf f "_" if !print_full_prop then F.fprintf f "%a" (Sil.pp_exp_printenv pe) e else F.fprintf f "_"
| Sil.Estruct (ls, _) -> | Sil.Estruct (ls, _) ->
@ -1715,4 +1715,3 @@ let print_specs_xml signature specs loc fmt =
[xml_signature; xml_specifications] [xml_signature; xml_specifications]
in in
Io_infer.Xml.pp_document true fmt proc_summary Io_infer.Xml.pp_document true fmt proc_summary

3
infer/src/backend/errdesc.ml
Unescape View File

@ -571,7 +571,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
let hpred_typ_opt = find_hpred_typ hpred in let hpred_typ_opt = find_hpred_typ hpred in
let value_str_from_pvars_vpath pvars vpath = let value_str_from_pvars_vpath pvars vpath =
if pvars <> [] then if pvars <> [] then
let pp = Pp.seq (Pvar.pp_value Pp.text) in let pp = Pp.seq Pvar.pp_value in
let desc_string = F.asprintf "%a" pp pvars in let desc_string = F.asprintf "%a" pp pvars in
Some desc_string Some desc_string
else else
@ -1331,4 +1331,3 @@ let explain_null_test_after_dereference tenv exp node line loc =
let warning_err loc fmt_string = let warning_err loc fmt_string =
L.(debug Analysis Medium) ("%a: Warning: " ^^ fmt_string) Location.pp loc L.(debug Analysis Medium) ("%a: Warning: " ^^ fmt_string) Location.pp loc

70
infer/src/backend/prop.ml
Unescape View File

@ -123,8 +123,7 @@ let pp_texp_simple pe =
let pp_hpred_stackvar pe0 f (hpred: Sil.hpred) = let pp_hpred_stackvar pe0 f (hpred: Sil.hpred) =
let pe, changed = Sil.color_pre_wrapper pe0 f hpred in let pe, changed = Sil.color_pre_wrapper pe0 f hpred in
( match hpred with ( match hpred with
| Hpointsto (Exp.Lvar pvar, se, te) | Hpointsto (Exp.Lvar pvar, se, te) ->
-> (
let pe' = let pe' =
match se with match se with
| Eexp (Exp.Var _, _) when not (Pvar.is_global pvar) -> | Eexp (Exp.Var _, _) when not (Pvar.is_global pvar) ->
@ -132,15 +131,10 @@ let pp_hpred_stackvar pe0 f (hpred: Sil.hpred) =
| _ -> | _ ->
pe pe
in in
match pe'.kind with F.fprintf f "%a = %a:%a" Pvar.pp_value pvar (Sil.pp_sexp pe') se (pp_texp_simple pe') te
| TEXT | HTML ->
F.fprintf f "%a = %a:%a" (Pvar.pp_value pe') pvar (Sil.pp_sexp pe') se
(pp_texp_simple pe') te
| LATEX ->
F.fprintf f "%a{=}%a" (Pvar.pp_value pe') pvar (Sil.pp_sexp pe') se )
| Hpointsto _ | Hlseg _ | Hdllseg _ -> | Hpointsto _ | Hlseg _ | Hdllseg _ ->
assert false (* should not happen *) ) ; assert false (* should not happen *) ) ;
Sil.color_post_wrapper changed pe0 f Sil.color_post_wrapper changed f
(** Pretty print a substitution. *) (** Pretty print a substitution. *)
@ -158,12 +152,8 @@ let d_sub (sub: Sil.subst) = L.add_print_action (PTsub, Obj.repr sub)
let pp_sub_entry pe0 f entry = let pp_sub_entry pe0 f entry =
let pe, changed = Sil.color_pre_wrapper pe0 f entry in let pe, changed = Sil.color_pre_wrapper pe0 f entry in
let x, e = entry in let x, e = entry in
( match pe.kind with F.fprintf f "%a = %a" Ident.pp x (Sil.pp_exp_printenv pe) e ;
| TEXT | HTML -> Sil.color_post_wrapper changed f
F.fprintf f "%a = %a" (Ident.pp pe) x (Sil.pp_exp_printenv pe) e
| LATEX ->
F.fprintf f "%a{=}%a" (Ident.pp pe) x (Sil.pp_exp_printenv pe) e ) ;
Sil.color_post_wrapper changed pe0 f
(** Pretty print a substitution as a list of (ident,exp) pairs *) (** Pretty print a substitution as a list of (ident,exp) pairs *)
@ -204,14 +194,7 @@ let pp_sigma_simple pe env fmt sigma =
if sg <> [] then if sg <> [] then
Format.fprintf fmt "%a" (Pp.semicolon_seq ~print_env:pe (pp_hpred_stackvar pe)) sg Format.fprintf fmt "%a" (Pp.semicolon_seq ~print_env:pe (pp_hpred_stackvar pe)) sg
in in
let pp_nl fmt doit = let pp_nl fmt doit = if doit then Format.fprintf fmt " ;@\n" in
if doit then
match pe.Pp.kind with
| TEXT | HTML ->
Format.fprintf fmt " ;@\n"
| LATEX ->
Format.fprintf fmt " ; \\\\@\n"
in
let pp_nonstack fmt = Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)) fmt in let pp_nonstack fmt = Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)) fmt in
if sigma_stack <> [] || sigma_nonstack <> [] then if sigma_stack <> [] || sigma_nonstack <> [] then
Format.fprintf fmt "%a%a%a" pp_stack sigma_stack pp_nl Format.fprintf fmt "%a%a%a" pp_stack sigma_stack pp_nl
@ -260,43 +243,26 @@ let get_pure_extended p =
(** Print existential quantification *) (** Print existential quantification *)
let pp_evars pe f evars = let pp_evars f evars =
if evars <> [] then if evars <> [] then F.fprintf f "exists [%a]. " (Pp.comma_seq Ident.pp) evars
match pe.Pp.kind with
| TEXT | HTML ->
F.fprintf f "exists [%a]. " (Pp.comma_seq (Ident.pp pe)) evars
| LATEX ->
F.fprintf f "\\exists %a. " (Pp.comma_seq (Ident.pp pe)) evars
(** Print an hpara in simple mode *) (** Print an hpara in simple mode *)
let pp_hpara_simple pe_ env n f pred = let pp_hpara_simple pe_ env n f pred =
let pe = Pp.reset_obj_sub pe_ in let pe = Pp.reset_obj_sub pe_ in
(* no free vars: disable object substitution *) (* no free vars: disable object substitution *)
match pe.kind with F.fprintf f "P%d = %a%a" n pp_evars pred.Sil.evars
| TEXT | HTML -> (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)))
F.fprintf f "P%d = %a%a" n (pp_evars pe) pred.Sil.evars pred.Sil.body
(Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)))
pred.Sil.body
| LATEX ->
F.fprintf f "P_{%d} = %a%a\\\\" n (pp_evars pe) pred.Sil.evars
(Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)))
pred.Sil.body
(** Print an hpara_dll in simple mode *) (** Print an hpara_dll in simple mode *)
let pp_hpara_dll_simple pe_ env n f pred = let pp_hpara_dll_simple pe_ env n f pred =
let pe = Pp.reset_obj_sub pe_ in let pe = Pp.reset_obj_sub pe_ in
(* no free vars: disable object substitution *) (* no free vars: disable object substitution *)
match pe.kind with F.fprintf f "P%d = %a%a" n pp_evars pred.Sil.evars_dll
| TEXT | HTML -> (Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)))
F.fprintf f "P%d = %a%a" n (pp_evars pe) pred.Sil.evars_dll pred.Sil.body_dll
(Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)))
pred.Sil.body_dll
| LATEX ->
F.fprintf f "P_{%d} = %a%a" n (pp_evars pe) pred.Sil.evars_dll
(Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred_env pe (Some env)))
pred.Sil.body_dll
(** Create an environment mapping (ident) expressions to the program variables containing them *) (** Create an environment mapping (ident) expressions to the program variables containing them *)
@ -341,7 +307,6 @@ let prop_pred_env prop =
(** Pretty print a proposition. *) (** Pretty print a proposition. *)
let pp_prop pe0 f prop = let pp_prop pe0 f prop =
let pe = prop_update_obj_sub pe0 prop in let pe = prop_update_obj_sub pe0 prop in
let latex = Pp.equal_print_kind pe.Pp.kind Pp.LATEX in
let do_print f () = let do_print f () =
let subl = Sil.sub_to_list prop.sub in let subl = Sil.sub_to_list prop.sub in
(* since prop diff is based on physical equality, we need to extract the sub verbatim *) (* since prop diff is based on physical equality, we need to extract the sub verbatim *)
@ -350,7 +315,7 @@ let pp_prop pe0 f prop =
if subl <> [] then F.fprintf f "%a ;@\n" (pp_subl pe) subl ; if subl <> [] then F.fprintf f "%a ;@\n" (pp_subl pe) subl ;
if pi <> [] then F.fprintf f "%a ;@\n" (pp_pi pe) pi if pi <> [] then F.fprintf f "%a ;@\n" (pp_pi pe) pi
in in
if !Config.pp_simple || latex then if !Config.pp_simple then
let env = prop_pred_env prop in let env = prop_pred_env prop in
let iter_f n hpara = F.fprintf f "@,@[<h>%a@]" (pp_hpara_simple pe env n) hpara in let iter_f n hpara = F.fprintf f "@,@[<h>%a@]" (pp_hpara_simple pe env n) hpara in
let iter_f_dll n hpara_dll = let iter_f_dll n hpara_dll =
@ -358,9 +323,6 @@ let pp_prop pe0 f prop =
in in
let pp_predicates _ () = let pp_predicates _ () =
if Sil.Predicates.is_empty env then () if Sil.Predicates.is_empty env then ()
else if latex then (
F.fprintf f "@\n\\\\\\textsf{where }" ;
Sil.Predicates.iter env iter_f iter_f_dll )
else ( else (
F.fprintf f "@,where" ; F.fprintf f "@,where" ;
Sil.Predicates.iter env iter_f iter_f_dll ) Sil.Predicates.iter env iter_f iter_f_dll )
@ -2517,7 +2479,7 @@ let prop_iter_make_id_primed tenv id iter =
| Aeq (Var id1, e1) when Sil.ident_in_exp id1 e1 -> | Aeq (Var id1, e1) when Sil.ident_in_exp id1 e1 ->
L.internal_error "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n" ; L.internal_error "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n" ;
L.internal_error "Broken Assumption: id notin e for all (id,e) in sub@\n" ; L.internal_error "Broken Assumption: id notin e for all (id,e) in sub@\n" ;
L.internal_error "(id,e) : (%a,%a)@\n" (Ident.pp Pp.text) id1 Exp.pp e1 ; L.internal_error "(id,e) : (%a,%a)@\n" Ident.pp id1 Exp.pp e1 ;
L.internal_error "PROP : %a@\n@." (pp_prop Pp.text) (prop_iter_to_prop tenv iter) ; L.internal_error "PROP : %a@\n@." (pp_prop Pp.text) (prop_iter_to_prop tenv iter) ;
assert false assert false
| Aeq (Var id1, e1) when Ident.equal pid id1 -> | Aeq (Var id1, e1) when Ident.equal pid id1 ->

15
infer/src/backend/propgraph.ml
Unescape View File

@ -287,12 +287,10 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist =
| TEXT -> | TEXT ->
F.fprintf f "%s %d of %d:@\n%a" s n num (Prop.pp_prop pe) x F.fprintf f "%s %d of %d:@\n%a" s n num (Prop.pp_prop pe) x
| HTML -> | HTML ->
F.fprintf f "%s %d of %d:@\n%a@\n" s n num (Prop.pp_prop pe) x F.fprintf f "%s %d of %d:@\n%a@\n" s n num (Prop.pp_prop pe) x )
| LATEX -> | _x :: l ->
F.fprintf f "@[%a@]@\n" (Prop.pp_prop pe) x ) let pe = update_pe_diff _x in
| x_ :: l -> let x = add_base_stack _x in
let pe = update_pe_diff x_ in
let x = add_base_stack x_ in
match pe.kind with match pe.kind with
| TEXT -> | TEXT ->
F.fprintf f "%s %d of %d:@\n%a@\n%a" s n num (Prop.pp_prop pe) x F.fprintf f "%s %d of %d:@\n%a@\n%a" s n num (Prop.pp_prop pe) x
@ -302,10 +300,6 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist =
F.fprintf f "%s %d of %d:@\n%a@\n%a" s n num (Prop.pp_prop pe) x F.fprintf f "%s %d of %d:@\n%a@\n%a" s n num (Prop.pp_prop pe) x
(pp_seq_newline (n + 1)) (pp_seq_newline (n + 1))
l l
| LATEX ->
F.fprintf f "@[%a@]\\\\@\n\\bigvee\\\\@\n%a" (Prop.pp_prop pe) x
(pp_seq_newline (n + 1))
l
in in
pp_seq_newline 1 f plist pp_seq_newline 1 f plist
@ -313,4 +307,3 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist =
(** dump a propset *) (** dump a propset *)
let d_proplist (p: 'a Prop.t) (pl: 'b Prop.t list) = let d_proplist (p: 'a Prop.t) (pl: 'b Prop.t list) =
L.add_print_action (L.PTproplist, Obj.repr (p, pl)) L.add_print_action (L.PTproplist, Obj.repr (p, pl))

24
infer/src/backend/specs.ml
Unescape View File

@ -430,13 +430,6 @@ let pp_spec pe num_opt fmt spec =
pre Io_infer.Html.pp_end_color () ; pre Io_infer.Html.pp_end_color () ;
F.fprintf fmt "%a" (Propgraph.pp_proplist pe_post "POST" (pre, true)) post_list ; F.fprintf fmt "%a" (Propgraph.pp_proplist pe_post "POST" (pre, true)) post_list ;
F.fprintf fmt "----------------------------------------------------------------" F.fprintf fmt "----------------------------------------------------------------"
| LATEX ->
F.fprintf fmt "\\textbf{\\large Requires}\\\\@\n@[%a%a%a@]\\\\@\n" Latex.pp_color Pp.Blue
(Prop.pp_prop (Pp.latex Blue))
pre Latex.pp_color pe.Pp.color ;
F.fprintf fmt "\\textbf{\\large Ensures}\\\\@\n@[%a@]"
(Propgraph.pp_proplist pe_post "POST" (pre, true))
post_list
(** Dump a spec *) (** Dump a spec *)
@ -458,13 +451,6 @@ let pp_specs pe fmt specs =
incr cnt ; incr cnt ;
F.fprintf fmt "%a<br>@\n" (pp_spec pe (Some (!cnt, total))) spec) F.fprintf fmt "%a<br>@\n" (pp_spec pe (Some (!cnt, total))) spec)
specs specs
| LATEX ->
List.iter
~f:(fun spec ->
incr cnt ;
F.fprintf fmt "\\subsection*{Spec %d of %d}@\n\\(%a\\)@\n" !cnt total (pp_spec pe None)
spec)
specs
let describe_phase summary = let describe_phase summary =
@ -541,16 +527,6 @@ let pp_summary_text fmt summary =
summary.payload summary.payload
let pp_summary_latex color fmt summary =
let pe = Pp.latex color in
F.fprintf fmt "\\begin{verbatim}@\n" ;
pp_summary_no_stats_specs fmt summary ;
F.fprintf fmt "%a@\n" pp_errlog (get_err_log summary) ;
F.fprintf fmt "%a@\n" pp_stats summary.stats ;
F.fprintf fmt "\\end{verbatim}@\n" ;
F.fprintf fmt "%a@\n" (pp_specs pe) (get_specs_from_payload summary)
let pp_summary_html source color fmt summary = let pp_summary_html source color fmt summary =
let pe = Pp.html color in let pe = Pp.html color in
Io_infer.Html.pp_start_color fmt Black ; Io_infer.Html.pp_start_color fmt Black ;

3
infer/src/backend/specs.mli
Unescape View File

@ -221,9 +221,6 @@ val pp_specs : Pp.env -> Format.formatter -> Prop.normal spec list -> unit
val pp_summary_html : SourceFile.t -> Pp.color -> Format.formatter -> summary -> unit val pp_summary_html : SourceFile.t -> Pp.color -> Format.formatter -> summary -> unit
(** Print the summary in html format *) (** Print the summary in html format *)
val pp_summary_latex : Pp.color -> Format.formatter -> summary -> unit
(** Print the summary in latext format *)
val pp_summary_text : Format.formatter -> summary -> unit val pp_summary_text : Format.formatter -> summary -> unit
(** Print the summary in text format *) (** Print the summary in text format *)

7
infer/src/base/Config.ml
Unescape View File

@ -1425,11 +1425,6 @@ and join_cond =
|} |}
and latex =
CLOpt.mk_path_opt ~deprecated:["latex"] ~long:"latex" ~meta:"file"
"Write a latex report of the analysis results to a file"
and log_file = and log_file =
CLOpt.mk_string ~deprecated:["out_file"; "-out-file"] ~long:"log-file" ~meta:"file" CLOpt.mk_string ~deprecated:["out_file"; "-out-file"] ~long:"log-file" ~meta:"file"
~default:"logs" "Specify the file to use for logging" ~default:"logs" "Specify the file to use for logging"
@ -2472,8 +2467,6 @@ and jobs = !jobs
and join_cond = !join_cond and join_cond = !join_cond
and latex = !latex
and linter = !linter and linter = !linter
and linters = and linters =

2
infer/src/base/Config.mli
Unescape View File

@ -497,8 +497,6 @@ val join_cond : int
val keep_going : bool val keep_going : bool
val latex : string option
val linter : string option val linter : string option
val linters : bool val linters : bool

72
infer/src/base/Latex.ml
Unescape View File

@ -1,72 +0,0 @@
(*
* Copyright (c) 2009 - 2013 Monoidics ltd.
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! IStd
module F = Format
(** Produce output in latex *)
type style = Boldface | Roman | Italics
(** Convert a string to a latex-friendly format *)
let convert_string s =
if String.contains s '_' then
let cnt = ref 0 in
let s' = ref "" in
let f c =
if Char.equal c '_' then s' := !s' ^ "\\_" else s' := !s' ^ Char.escaped s.[!cnt] ;
incr cnt
in
String.iter ~f s ; !s'
else s
(** Print a string in the given style, after converting it into latex-friendly format *)
let pp_string style f s =
let converted = convert_string s in
match style with
| Boldface ->
F.fprintf f "\\textbf{%s}" converted
| Roman ->
F.fprintf f "\\textrm{%s}" converted
| Italics ->
F.fprintf f "\\textit{%s}" converted
let color_to_string (c: Pp.color) =
match c with
| Black ->
"black"
| Blue ->
"blue"
| Green ->
"green"
| Orange ->
"orange"
| Red ->
"red"
(** Print color command *)
let pp_color f color = F.fprintf f "\\color{%s}" (color_to_string color)
(** Prelude for a latex file with the given author and title *)
let pp_begin f (author, title, table_of_contents) =
let pp_toc f () = if table_of_contents then F.fprintf f "\\tableofcontents@\n" else () in
F.fprintf f
"\\documentclass{article}@\n\\usepackage{hyperref}@\n\\usepackage{color}@\n\\author{%s}@\n\\title{%s}@\n\\begin{document}@\n\\maketitle@\n%a"
author title pp_toc ()
(** Epilogue for a latex file *)
let pp_end f () = F.fprintf f "\\end{document}@\n"
(** Section with the given title *)
let pp_section f title = F.fprintf f "\\section{%s}@\n" title

31
infer/src/base/Latex.mli
Unescape View File

@ -1,31 +0,0 @@
(*
* Copyright (c) 2009 - 2013 Monoidics ltd.
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! IStd
type style = Boldface | Roman | Italics
val convert_string : string -> string
(** Convert a string to a latex-friendly format *)
val pp_string : style -> Format.formatter -> string -> unit
(** Print a string in the given style, after converting it into latex-friendly format *)
val pp_color : Format.formatter -> Pp.color -> unit
(** Print color command *)
val pp_begin : Format.formatter -> string * string * bool -> unit
(** Prelude for a latex file with the given author and title and table of contents flag *)
val pp_end : Format.formatter -> unit -> unit
(** Epilogue for a latex file *)
val pp_section : Format.formatter -> string -> unit
(** Section with the given title *)

21
infer/src/base/Pp.ml
Unescape View File

@ -18,7 +18,7 @@ module CLOpt = CommandLineOption
type simple_kind = SIM_DEFAULT | SIM_WITH_TYP type simple_kind = SIM_DEFAULT | SIM_WITH_TYP
(** Kind of printing *) (** Kind of printing *)
type print_kind = TEXT | LATEX | HTML [@@deriving compare] type print_kind = TEXT | HTML [@@deriving compare]
let equal_print_kind = [%compare.equal : print_kind] let equal_print_kind = [%compare.equal : print_kind]
@ -66,17 +66,6 @@ let html color =
kind= HTML; cmap_norm= colormap_from_color color; cmap_foot= colormap_from_color color; color } kind= HTML; cmap_norm= colormap_from_color color; cmap_foot= colormap_from_color color; color }
(** Default latex print environment *)
let latex color =
{ opt= SIM_DEFAULT
; kind= LATEX
; break_lines= false
; cmap_norm= colormap_from_color color
; cmap_foot= colormap_from_color color
; color
; obj_sub= None }
(** Extend the normal colormap for the given object with the given color *) (** Extend the normal colormap for the given object with the given color *)
let extend_colormap pe (x: Obj.t) (c: color) = let extend_colormap pe (x: Obj.t) (c: color) =
let colormap (y: Obj.t) = if phys_equal x y then c else pe.cmap_norm y in let colormap (y: Obj.t) = if phys_equal x y then c else pe.cmap_norm y in
@ -110,16 +99,14 @@ let color_string = function
"color_red" "color_red"
let seq ?(print_env= text) ?sep:(sep_text = " ") ?(sep_html= sep_text) ?(sep_latex= sep_text) pp = let seq ?(print_env= text) ?sep:(sep_text = " ") ?(sep_html= sep_text) pp =
let rec aux f = function let rec aux f = function
| [] -> | [] ->
() ()
| [x] -> | [x] ->
F.fprintf f "%a" pp x F.fprintf f "%a" pp x
| x :: l -> | x :: l ->
let sep = let sep = match print_env.kind with TEXT -> sep_text | HTML -> sep_html in
match print_env.kind with TEXT -> sep_text | HTML -> sep_html | LATEX -> sep_latex
in
if print_env.break_lines then F.fprintf f "%a%s@ %a" pp x sep aux l if print_env.break_lines then F.fprintf f "%a%s@ %a" pp x sep aux l
else F.fprintf f "%a%s%a" pp x sep aux l else F.fprintf f "%a%s%a" pp x sep aux l
in in
@ -130,7 +117,7 @@ let comma_seq ?print_env pp f l = seq ?print_env ~sep:"," pp f l
let semicolon_seq ?print_env pp f l = seq ?print_env ~sep:";" pp f l let semicolon_seq ?print_env pp f l = seq ?print_env ~sep:";" pp f l
let or_seq ?print_env pp f = seq ?print_env ~sep:" ||" ~sep_html:" &or;" ~sep_latex:" \\vee" pp f let or_seq ?print_env pp f = seq ?print_env ~sep:" ||" ~sep_html:" &or;" pp f
(** Print the current time and date in a format similar to the "date" command *) (** Print the current time and date in a format similar to the "date" command *)
let current_time f () = let current_time f () =

11
infer/src/base/Pp.mli
Unescape View File

@ -25,7 +25,7 @@ type colormap = Obj.t -> color
type simple_kind = SIM_DEFAULT | SIM_WITH_TYP type simple_kind = SIM_DEFAULT | SIM_WITH_TYP
(** Kind of printing *) (** Kind of printing *)
type print_kind = TEXT | LATEX | HTML [@@deriving compare] type print_kind = TEXT | HTML [@@deriving compare]
val equal_print_kind : print_kind -> print_kind -> bool val equal_print_kind : print_kind -> print_kind -> bool
@ -62,9 +62,6 @@ val text : env
val html : color -> env val html : color -> env
(** Default html print environment *) (** Default html print environment *)
val latex : color -> env
(** Default latex print environment *)
val color_string : color -> string val color_string : color -> string
(** string representation of colors *) (** string representation of colors *)
@ -76,10 +73,10 @@ val cli_args : F.formatter -> string list -> unit
(** pretty print command line arguments, expanding argument files to print their contents *) (** pretty print command line arguments, expanding argument files to print their contents *)
val seq : val seq :
?print_env:env -> ?sep:string -> ?sep_html:string -> ?sep_latex:string ?print_env:env -> ?sep:string -> ?sep_html:string -> (F.formatter -> 'a -> unit) -> F.formatter
-> (F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit -> 'a list -> unit
(** Pretty print a sequence with [sep] followed by a space between each element. By default, (** Pretty print a sequence with [sep] followed by a space between each element. By default,
[print_env] is [text], [sep] is "", and [sep_html] and [sep_latex] set to [sep]. *) [print_env] is [text], [sep] is "", and [sep_html] set to [sep]. *)
val comma_seq : ?print_env:env -> (F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit val comma_seq : ?print_env:env -> (F.formatter -> 'a -> unit) -> F.formatter -> 'a list -> unit
(** Pretty print a comma-separated sequence. *) (** Pretty print a comma-separated sequence. *)

2
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -424,7 +424,7 @@ module AliasMap = struct
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
fun fmt x -> fun fmt x ->
let pp_sep fmt () = F.fprintf fmt ", @," in let pp_sep fmt () = F.fprintf fmt ", @," in
let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k AliasTarget.pp v in let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Ident.pp k AliasTarget.pp v in
(* F.fprintf fmt "@[<v 0>Logical Variables :@,"; *) (* F.fprintf fmt "@[<v 0>Logical Variables :@,"; *)
F.fprintf fmt "@[<hov 2>{ @," ; F.fprintf fmt "@[<hov 2>{ @," ;
F.pp_print_list ~pp_sep pp1 fmt (M.bindings x) ; F.pp_print_list ~pp_sep pp1 fmt (M.bindings x) ;

Write Preview
Loading…
Cancel
Save