[ocamlformat] Upgrade base and ocamlformat

Summary:
Upgrade ocamlformat to 0.3, and (necessarily) base to v0.10.0.

- Fix accumulated mis-formatting
- Update opam.lock to unbreak clean build
- Update to base v0.10.0
- Update opam.lock for base
- Update offline opam repo
- Everyone should already have removed their ocamlformat pin
- ocamlformat 0.3 supports output to stdout natively
- bump version of ocamlformat

Reviewed By: jeremydubreil

Differential Revision: D6636741

fbshipit-source-id: 41a56a8
master
Josh Berdine 7 years ago committed by Facebook Github Bot
parent 7032bca1d5
commit 63439ecc02

@ -1,3 +1,3 @@
margin 100 margin 100
sparse true sparse true
version v0.2 version 0.3

@ -600,7 +600,6 @@ endif
devsetup: Makefile.autoconf devsetup: Makefile.autoconf
$(QUIET)[ $(OPAM) != "no" ] || (echo 'No `opam` found, aborting setup.' >&2; exit 1) $(QUIET)[ $(OPAM) != "no" ] || (echo 'No `opam` found, aborting setup.' >&2; exit 1)
$(QUIET)$(call silent_on_success,installing $(OPAM_DEV_DEPS),\ $(QUIET)$(call silent_on_success,installing $(OPAM_DEV_DEPS),\
OPAMSWITCH=$(OPAMSWITCH); $(OPAM) pin remove --yes ocamlformat; \
OPAMSWITCH=$(OPAMSWITCH); $(OPAM) install --yes --no-checksum user-setup $(OPAM_DEV_DEPS)) OPAMSWITCH=$(OPAMSWITCH); $(OPAM) install --yes --no-checksum user-setup $(OPAM_DEV_DEPS))
$(QUIET)echo '$(TERM_INFO)*** Running `opam config setup -a`$(TERM_RESET)' >&2 $(QUIET)echo '$(TERM_INFO)*** Running `opam config setup -a`$(TERM_RESET)' >&2
$(QUIET)OPAMSWITCH=$(OPAMSWITCH); $(OPAM) config --yes setup -a $(QUIET)OPAMSWITCH=$(OPAMSWITCH); $(OPAM) config --yes setup -a

@ -202,7 +202,6 @@ module Raw = struct
let is_prefix ((base1, path1) as ap1) ((base2, path2) as ap2) = let is_prefix ((base1, path1) as ap1) ((base2, path2) as ap2) =
if phys_equal ap1 ap2 then true else equal_base base1 base2 && is_prefix_path path1 path2 if phys_equal ap1 ap2 then true else equal_base base1 base2 && is_prefix_path path1 path2
end end
module Abs = struct module Abs = struct
@ -256,7 +255,6 @@ module Abs = struct
Raw.pp fmt access_path Raw.pp fmt access_path
| Abstracted access_path -> | Abstracted access_path ->
F.fprintf fmt "%a*" Raw.pp access_path F.fprintf fmt "%a*" Raw.pp access_path
end end
include Raw include Raw

@ -132,4 +132,3 @@ let find_file_capturing_procedure pname =
`Source `Source
in in
(source_file, origin) ) (source_file, origin) )

@ -37,4 +37,3 @@ let default =
; cf_is_objc_block= false ; cf_is_objc_block= false
; cf_with_block_parameters= false ; cf_with_block_parameters= false
; cf_targets= [] } ; cf_targets= [] }

@ -46,7 +46,7 @@ let iter_all_nodes ?(sorted= false) f cfg =
(fun _ pdesc desc_nodes -> (fun _ pdesc desc_nodes ->
List.fold List.fold
~f:(fun desc_nodes node -> (pdesc, node) :: desc_nodes) ~f:(fun desc_nodes node -> (pdesc, node) :: desc_nodes)
~init:desc_nodes (Procdesc.get_nodes pdesc)) ~init:desc_nodes (Procdesc.get_nodes pdesc) )
cfg [] cfg []
|> List.sort ~cmp:[%compare : Procdesc.t * Procdesc.Node.t] |> List.sort ~cmp:[%compare : Procdesc.t * Procdesc.Node.t]
|> List.iter ~f:(fun (d, n) -> f d n) |> List.iter ~f:(fun (d, n) -> f d n)
@ -248,7 +248,7 @@ let mark_unchanged_pdescs cfg_new cfg_old =
~equal:(fun i1 i2 -> ~equal:(fun i1 i2 ->
let n, exp_map' = Sil.compare_structural_instr i1 i2 !exp_map in let n, exp_map' = Sil.compare_structural_instr i1 i2 !exp_map in
exp_map := exp_map' ; exp_map := exp_map' ;
Int.equal n 0) Int.equal n 0 )
instrs1 instrs2 instrs1 instrs2
in in
Int.equal (compare_id n1 n2) 0 Int.equal (compare_id n1 n2) 0
@ -443,7 +443,7 @@ let specialize_types callee_pdesc resolved_pname args =
(* Replace the type of the parameter by the type of the argument *) (* Replace the type of the parameter by the type of the argument *)
((param_name, arg_typ) :: params, Mangled.Map.add param_name typename subts) ((param_name, arg_typ) :: params, Mangled.Map.add param_name typename subts)
| _ -> | _ ->
((param_name, param_typ) :: params, subts)) ((param_name, param_typ) :: params, subts) )
~init:([], Mangled.Map.empty) callee_attributes.formals args ~init:([], Mangled.Map.empty) callee_attributes.formals args
in in
let resolved_attributes = let resolved_attributes =
@ -561,7 +561,7 @@ let specialize_with_block_args callee_pdesc pname_with_block_args block_args =
~f:(fun (_, var, typ) -> ~f:(fun (_, var, typ) ->
(* Here we create fresh names for the new formals, based on the names of the captured (* Here we create fresh names for the new formals, based on the names of the captured
variables annotated with the name of the caller method *) variables annotated with the name of the caller method *)
(Pvar.get_name_of_local_with_procname var, typ)) (Pvar.get_name_of_local_with_procname var, typ) )
cl.captured_vars cl.captured_vars
in in
Mangled.Map.add param_name (cl.name, formals_from_captured) subts Mangled.Map.add param_name (cl.name, formals_from_captured) subts
@ -631,4 +631,3 @@ let pp_proc_signatures fmt cfg =
let exists_for_source_file source = let exists_for_source_file source =
(* simplistic implementation that allocates the cfg as this is only used for reactive capture for now *) (* simplistic implementation that allocates the cfg as this is only used for reactive capture for now *)
load source |> Option.is_some load source |> Option.is_some

@ -323,7 +323,7 @@ let pp_graph_dotty (g: t) fmt =
List.iter List.iter
~f:(fun nc -> ~f:(fun nc ->
F.fprintf fmt "%a [shape=box,label=%a,color=%s,shape=%s]@\n" pp_node nc pp_node_label nc F.fprintf fmt "%a [shape=box,label=%a,color=%s,shape=%s]@\n" pp_node nc pp_node_label nc
"red" (get_shape nc)) "red" (get_shape nc) )
nodes_with_calls ; nodes_with_calls ;
List.iter ~f:(fun (s, d) -> F.fprintf fmt "%a -> %a@\n" pp_node s pp_node d) (get_edges g) ; List.iter ~f:(fun (s, d) -> F.fprintf fmt "%a -> %a@\n" pp_node s pp_node d) (get_edges g) ;
F.fprintf fmt "}@." F.fprintf fmt "}@."
@ -337,4 +337,3 @@ let save_call_graph_dotty source (g: t) =
let outc = Out_channel.create (DB.filename_to_string fname_dot) in let outc = Out_channel.create (DB.filename_to_string fname_dot) in
let fmt = F.formatter_of_out_channel outc in let fmt = F.formatter_of_out_channel outc in
pp_graph_dotty g fmt ; Out_channel.close outc pp_graph_dotty g fmt ; Out_channel.close outc

@ -70,4 +70,3 @@ let isminusone_int_float = function
true true
| _ -> | _ ->
false false

@ -137,4 +137,3 @@ let rec has_tmp_var = function
has_tmp_var dexp || List.exists ~f:has_tmp_var dexp_list has_tmp_var dexp || List.exists ~f:has_tmp_var dexp_list
| Dconst _ | Dunknown | Dsizeof (_, None, _) -> | Dconst _ | Dunknown | Dsizeof (_, None, _) ->
false false

@ -65,7 +65,7 @@ let compute_local_exception_line loc_trace =
snd (List_.fold_until ~init:(`Continue (None, None)) ~f:compute_local_exception_line loc_trace) snd (List_.fold_until ~init:(`Continue (None, None)) ~f:compute_local_exception_line loc_trace)
type node_id_key = {node_id: int; node_key: Digest.t} type node_id_key = {node_id: int; node_key: Caml.Digest.t}
type err_key = type err_key =
{ err_kind: Exceptions.err_kind { err_kind: Exceptions.err_kind
@ -113,7 +113,6 @@ module ErrLogHash = struct
(key1.err_kind, key1.in_footprint, key1.err_name) (key1.err_kind, key1.in_footprint, key1.err_name)
(key2.err_kind, key2.in_footprint, key2.err_name) (key2.err_kind, key2.in_footprint, key2.err_name)
&& Localise.error_desc_equal key1.err_desc key2.err_desc && Localise.error_desc_equal key1.err_desc key2.err_desc
end end
include Hashtbl.Make (Key) include Hashtbl.Make (Key)
@ -147,12 +146,14 @@ let fold (f: err_key -> err_data -> 'a -> 'a) t acc =
(fun err_key set acc -> ErrDataSet.fold (fun err_data acc -> f err_key err_data acc) set acc) (fun err_key set acc -> ErrDataSet.fold (fun err_data acc -> f err_key err_data acc) set acc)
t acc t acc
(** Return the number of elements in the error log which satisfy [filter] *) (** Return the number of elements in the error log which satisfy [filter] *)
let size filter (err_log: t) = let size filter (err_log: t) =
let count = ref 0 in let count = ref 0 in
ErrLogHash.iter ErrLogHash.iter
(fun key err_datas -> (fun key err_datas ->
if filter key.err_kind key.in_footprint then count := !count + ErrDataSet.cardinal err_datas) if filter key.err_kind key.in_footprint then count := !count + ErrDataSet.cardinal err_datas
)
err_log ; err_log ;
!count !count
@ -324,7 +325,7 @@ module Err_table = struct
let count_err (err_name: IssueType.t) n = let count_err (err_name: IssueType.t) n =
let err_string = err_name.IssueType.unique_id in let err_string = err_name.IssueType.unique_id in
let count = try String.Map.find_exn !err_name_map err_string with Not_found -> 0 in let count = try String.Map.find_exn !err_name_map err_string with Not_found -> 0 in
err_name_map := String.Map.add ~key:err_string ~data:(count + n) !err_name_map err_name_map := String.Map.set ~key:err_string ~data:(count + n) !err_name_map
in in
let count key err_datas = let count key err_datas =
if Exceptions.equal_err_kind ekind key.err_kind && key.in_footprint then if Exceptions.equal_err_kind ekind key.err_kind && key.in_footprint then
@ -378,7 +379,7 @@ module Err_table = struct
List.iter List.iter
~f:(fun (err_name, desc) -> ~f:(fun (err_name, desc) ->
Exceptions.pp_err ~node_key:err_data.node_id_key.node_key err_data.loc ekind err_name Exceptions.pp_err ~node_key:err_data.node_id_key.node_key err_data.loc ekind err_name
desc err_data.loc_in_ml_source fmt ()) desc err_data.loc_in_ml_source fmt () )
err_names err_names
in in
F.fprintf fmt "@.Detailed errors during footprint phase:@." ; F.fprintf fmt "@.Detailed errors during footprint phase:@." ;
@ -397,7 +398,6 @@ module Err_table = struct
LocMap.iter LocMap.iter
(fun nslm err_names -> F.fprintf fmt "%a" (pp Exceptions.Kwarning nslm) err_names) (fun nslm err_names -> F.fprintf fmt "%a" (pp Exceptions.Kwarning nslm) err_names)
!map_warn_re !map_warn_re
end end
type err_table = Err_table.t type err_table = Err_table.t

@ -36,7 +36,7 @@ val compute_local_exception_line : loc_trace -> int option
This extra information adds value to the report itself, and may avoid This extra information adds value to the report itself, and may avoid
digging into the trace to understand the cause of the report. *) digging into the trace to understand the cause of the report. *)
type node_id_key = private {node_id: int; node_key: Digest.t} type node_id_key = private {node_id: int; node_key: Caml.Digest.t}
type err_key = private type err_key = private
{ err_kind: Exceptions.err_kind { err_kind: Exceptions.err_kind
@ -93,7 +93,7 @@ val update : t -> t -> unit
(** Update an old error log with a new one *) (** Update an old error log with a new one *)
val log_issue : val log_issue :
Exceptions.err_kind -> t -> Location.t -> int * Digest.t -> int -> loc_trace Exceptions.err_kind -> t -> Location.t -> int * Caml.Digest.t -> int -> loc_trace
-> ?linters_def_file:string -> ?doc_url:string -> ?access:string -> exn -> unit -> ?linters_def_file:string -> ?doc_url:string -> ?access:string -> exn -> unit
(** {2 Functions for manipulating per-file error tables} *) (** {2 Functions for manipulating per-file error tables} *)

@ -686,7 +686,7 @@ let print_key = false
(** pretty print an error *) (** pretty print an error *)
let pp_err ~node_key loc ekind ex_name desc ml_loc_opt fmt () = let pp_err ~node_key loc ekind ex_name desc ml_loc_opt fmt () =
let kind = err_kind_string (if equal_err_kind ekind Kinfo then Kwarning else ekind) in let kind = err_kind_string (if equal_err_kind ekind Kinfo then Kwarning else ekind) in
let pp_key fmt k = if print_key then F.fprintf fmt " key: %s " (Digest.to_hex k) else () in let pp_key fmt k = if print_key then F.fprintf fmt " key: %s " (Caml.Digest.to_hex k) else () in
F.fprintf fmt "%a:%d: %s: %a %a%a%a@\n" SourceFile.pp loc.Location.file loc.Location.line kind F.fprintf fmt "%a:%d: %s: %a %a%a%a@\n" SourceFile.pp loc.Location.file loc.Location.line kind
IssueType.pp ex_name Localise.pp_error_desc desc pp_key node_key L.pp_ml_loc_opt ml_loc_opt IssueType.pp ex_name Localise.pp_error_desc desc pp_key node_key L.pp_ml_loc_opt ml_loc_opt

@ -158,7 +158,7 @@ val print_exception_html : string -> exn -> unit
(** print a description of the exception to the html output *) (** print a description of the exception to the html output *)
val pp_err : val pp_err :
node_key:Digest.t -> Location.t -> err_kind -> IssueType.t -> Localise.error_desc node_key:Caml.Digest.t -> Location.t -> err_kind -> IssueType.t -> Localise.error_desc
-> Logging.ml_loc option -> Format.formatter -> unit -> unit -> Logging.ml_loc option -> Format.formatter -> unit -> unit
(** pretty print an error *) (** pretty print an error *)

@ -179,7 +179,6 @@ let rec eval_arithmetic_binop op e1 e2 =
| _ -> | _ ->
None None
and eval = function and eval = function
| Constant c -> | Constant c ->
Some c Some c
@ -196,4 +195,3 @@ and eval = function
| _ -> | _ ->
(* TODO: handle bitshifting cases, port eval_binop from RacerD.ml *) (* TODO: handle bitshifting cases, port eval_binop from RacerD.ml *)
None None

@ -127,4 +127,3 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =
| Declare_locals _ -> | Declare_locals _ ->
(* these don't seem useful for most analyses. can translate them later if we want to *) (* these don't seem useful for most analyses. can translate them later if we want to *)
Ignore Ignore

@ -39,7 +39,6 @@ module Name = struct
spec spec
| FromString s -> | FromString s ->
s s
end end
type name = Name.t [@@deriving compare] type name = Name.t [@@deriving compare]
@ -159,7 +158,6 @@ module NameGenerator = struct
let new_stamp = max curr_stamp stamp in let new_stamp = max curr_stamp stamp in
NameHash.replace !name_map name new_stamp NameHash.replace !name_map name new_stamp
with Not_found -> NameHash.add !name_map name stamp with Not_found -> NameHash.add !name_map name stamp
end end
(** Name used for the return variable *) (** Name used for the return variable *)

@ -203,7 +203,6 @@ td.rowname { text-align:right; font-weight:bold; color:#444444; padding-right:2e
~pos:(Some pos) ~path:path_to_node fmt ~pos:(Some pos) ~path:path_to_node fmt
(node_name ^ "#" ^ pos) ; (node_name ^ "#" ^ pos) ;
F.fprintf fmt "(%a)" (pp_line_link source path_to_root) linenum F.fprintf fmt "(%a)" (pp_line_link source path_to_root) linenum
end end
(* =============== END of module Html =============== *) (* =============== END of module Html =============== *)
@ -341,7 +340,6 @@ module Xml = struct
if on_several_lines then pp_prelude fmt ; if on_several_lines then pp_prelude fmt ;
pp_node newline "" fmt node ; pp_node newline "" fmt node ;
if on_several_lines then pp fmt "@." if on_several_lines then pp fmt "@."
end end
(* =============== END of module Xml =============== *) (* =============== END of module Xml =============== *)

@ -53,10 +53,9 @@ let load_issues_to_errlog_map dir =
| None, Some issues2 -> | None, Some issues2 ->
Some issues2 Some issues2
| None, None -> | None, None ->
None) None )
!errLogMap map !errLogMap map
| None -> | None ->
() ()
in in
match children_opt with Some children -> Array.iter ~f:load_issues_to_map children | None -> () match children_opt with Some children -> Array.iter ~f:load_issues_to_map children | None -> ()

@ -114,9 +114,8 @@ module Tags = struct
in in
List.filter_map List.filter_map
~f:(fun (tag, value) -> ~f:(fun (tag, value) ->
if String.Set.mem line_tags tag then Some (int_of_string value) else None) if String.Set.mem line_tags tag then Some (int_of_string value) else None )
tags tags
end end
type error_desc = type error_desc =
@ -607,14 +606,16 @@ let dereference_string proc_name deref_str value_str access_opt loc =
let annotation_name = nullable_annotation_name proc_name in let annotation_name = nullable_annotation_name proc_name in
match (Tags.get !tags Tags.nullable_src, Tags.get !tags Tags.weak_captured_var_src) with match (Tags.get !tags Tags.nullable_src, Tags.get !tags Tags.weak_captured_var_src) with
| Some nullable_src, _ -> | Some nullable_src, _ ->
if String.equal nullable_src value_str then "is annotated with " ^ annotation_name if String.equal nullable_src value_str then
^ " and is dereferenced without a null check" "is annotated with " ^ annotation_name ^ " and is dereferenced without a null check"
else "is indirectly marked " ^ annotation_name ^ " (source: " else
"is indirectly marked " ^ annotation_name ^ " (source: "
^ MF.monospaced_to_string nullable_src ^ ") and is dereferenced without a null check" ^ MF.monospaced_to_string nullable_src ^ ") and is dereferenced without a null check"
| None, Some weak_var_str -> | None, Some weak_var_str ->
if String.equal weak_var_str value_str then if String.equal weak_var_str value_str then
"is a weak pointer captured in the block and is dereferenced without a null check" "is a weak pointer captured in the block and is dereferenced without a null check"
else "is equal to the variable " ^ MF.monospaced_to_string weak_var_str else
"is equal to the variable " ^ MF.monospaced_to_string weak_var_str
^ ", a weak pointer captured in the block, and is dereferenced without a null check" ^ ", a weak pointer captured in the block, and is dereferenced without a null check"
| None, None -> | None, None ->
deref_str.problem_str deref_str.problem_str
@ -690,8 +691,8 @@ let desc_allocation_mismatch alloc dealloc =
Tags.update tags tag_line (string_of_int loc.Location.line) ; Tags.update tags tag_line (string_of_int loc.Location.line) ;
let by_call = let by_call =
if Typ.Procname.equal primitive_pname called_pname then "" if Typ.Procname.equal primitive_pname called_pname then ""
else " by call to " else
^ MF.monospaced_to_string (Typ.Procname.to_simplified_string called_pname) " by call to " ^ MF.monospaced_to_string (Typ.Procname.to_simplified_string called_pname)
in in
"using " ^ MF.monospaced_to_string (Typ.Procname.to_simplified_string primitive_pname) "using " ^ MF.monospaced_to_string (Typ.Procname.to_simplified_string primitive_pname)
^ by_call ^ " " ^ at_line (Tags.create ()) (* ignore the tag *) loc ^ by_call ^ " " ^ at_line (Tags.create ()) (* ignore the tag *) loc

@ -42,4 +42,3 @@ let pp_file_pos f (loc: t) =
let fname = SourceFile.to_string loc.file in let fname = SourceFile.to_string loc.file in
let pos = to_string loc in let pos = to_string loc in
F.fprintf f "%s:%s" fname pos F.fprintf f "%s:%s" fname pos

@ -201,11 +201,9 @@ module Core_foundation_model = struct
let is_core_lib_create typ funct = let is_core_lib_create typ funct =
is_core_lib_type typ is_core_lib_type typ
&& (String.is_substring ~substring:create funct || String.is_substring ~substring:copy funct) && (String.is_substring ~substring:create funct || String.is_substring ~substring:copy funct)
end end
let is_core_lib_type typ = Core_foundation_model.is_core_lib_type typ let is_core_lib_type typ = Core_foundation_model.is_core_lib_type typ
let is_malloc_model return_type pname = let is_malloc_model return_type pname =
Core_foundation_model.is_core_lib_create return_type (Typ.Procname.to_string pname) Core_foundation_model.is_core_lib_create return_type (Typ.Procname.to_string pname)

@ -251,7 +251,6 @@ module Node = struct
in in
let pp fmt = F.fprintf fmt "%s@\n%a@?" str (pp_instrs pe None ~sub_instrs:true) node in let pp fmt = F.fprintf fmt "%s@\n%a@?" str (pp_instrs pe None ~sub_instrs:true) node in
F.asprintf "%t" pp F.asprintf "%t" pp
end end
(* =============== END of module Node =============== *) (* =============== END of module Node =============== *)
@ -593,4 +592,3 @@ let has_modify_in_block_attr procdesc pvar =
ProcAttributes.var_attribute_equal attr ProcAttributes.Modify_in_block ) ProcAttributes.var_attribute_equal attr ProcAttributes.Modify_in_block )
in in
List.exists ~f:pvar_local_matches (get_locals procdesc) List.exists ~f:pvar_local_matches (get_locals procdesc)

@ -754,7 +754,6 @@ module Procname = struct
let ( $!--> ) args_matcher f = let ( $!--> ) args_matcher f =
args_matcher $* exact_args_or_retry wrong_args_internal_error $*--> f args_matcher $* exact_args_or_retry wrong_args_internal_error $*--> f
end end
module TypName = struct module TypName = struct

@ -52,6 +52,7 @@ let compare_modulo_this x y =
else if String.equal "this" (Mangled.to_string x.pv_name) then 0 else if String.equal "this" (Mangled.to_string x.pv_name) then 0
else compare_pvar_kind x.pv_kind y.pv_kind else compare_pvar_kind x.pv_kind y.pv_kind
let equal = [%compare.equal : t] let equal = [%compare.equal : t]
let pp_translation_unit fmt = function let pp_translation_unit fmt = function

@ -73,8 +73,9 @@ module Match = struct
let qualifiers_list_matcher ?prefix quals_list = let qualifiers_list_matcher ?prefix quals_list =
( if List.is_empty quals_list then "a^" (* regexp that does not match anything *) ( if List.is_empty quals_list then "a^" (* regexp that does not match anything *)
else List.rev_map ~f:(regexp_string_of_qualifiers ?prefix) quals_list else
|> String.concat ~sep:"\\|" ) List.rev_map ~f:(regexp_string_of_qualifiers ?prefix) quals_list |> String.concat ~sep:"\\|"
)
|> Str.regexp |> Str.regexp
@ -100,5 +101,4 @@ module Match = struct
instantiations *) instantiations *)
let normalized_qualifiers = strip_template_args quals in let normalized_qualifiers = strip_template_args quals in
Str.string_match matcher (to_separated_string ~sep:matching_separator normalized_qualifiers) 0 Str.string_match matcher (to_separated_string ~sep:matching_separator normalized_qualifiers) 0
end end

@ -619,7 +619,6 @@ end = struct
| [] -> | [] ->
() ()
done done
end end
let pp_texp_simple pe = let pp_texp_simple pe =
@ -1402,7 +1401,7 @@ let sub_no_duplicated_ids sub = not (List.contains_dup ~compare:compare_ident_ex
For all (id1, e1), (id2, e2) in the input list, For all (id1, e1), (id2, e2) in the input list,
if id1 = id2, then e1 = e2. *) if id1 = id2, then e1 = e2. *)
let exp_subst_of_list sub = let exp_subst_of_list sub =
let sub' = List.dedup ~compare:compare_ident_exp sub in let sub' = List.dedup_and_sort ~compare:compare_ident_exp sub in
assert (sub_no_duplicated_ids sub') ; assert (sub_no_duplicated_ids sub') ;
sub' sub'
@ -1410,7 +1409,7 @@ let exp_subst_of_list sub =
let subst_of_list sub = `Exp (exp_subst_of_list sub) let subst_of_list sub = `Exp (exp_subst_of_list sub)
(** like exp_subst_of_list, but allow duplicate ids and only keep the first occurrence *) (** like exp_subst_of_list, but allow duplicate ids and only keep the first occurrence *)
let exp_subst_of_list_duplicates sub = List.dedup ~compare:compare_ident_exp_ids sub let exp_subst_of_list_duplicates sub = List.dedup_and_sort ~compare:compare_ident_exp_ids sub
(** Convert a subst to a list of pairs. *) (** Convert a subst to a list of pairs. *)
let sub_to_list sub = sub let sub_to_list sub = sub
@ -1535,7 +1534,7 @@ let rec exp_sub_ids (f: subst_fun) exp =
(fun ((e, pvar, typ) as captured) -> (fun ((e, pvar, typ) as captured) ->
let e' = exp_sub_ids f e in let e' = exp_sub_ids f e in
let typ' = f_typ typ in let typ' = f_typ typ in
if phys_equal e' e && phys_equal typ typ' then captured else (e', pvar, typ')) if phys_equal e' e && phys_equal typ typ' then captured else (e', pvar, typ') )
c.captured_vars c.captured_vars
in in
if phys_equal captured_vars c.captured_vars then exp else Exp.Closure {c with captured_vars} if phys_equal captured_vars c.captured_vars then exp else Exp.Closure {c with captured_vars}
@ -1588,7 +1587,7 @@ let apply_sub subst : subst_fun =
| `Exp l -> | `Exp l ->
`Exp `Exp
(fun id -> (fun id ->
match List.Assoc.find l ~equal:Ident.equal id with Some x -> x | None -> Exp.Var id) match List.Assoc.find l ~equal:Ident.equal id with Some x -> x | None -> Exp.Var id )
| `Typ typ_subst -> | `Typ typ_subst ->
`Typ (Typ.sub_type typ_subst, Typ.sub_tname typ_subst) `Typ (Typ.sub_type typ_subst, Typ.sub_tname typ_subst)
@ -1634,7 +1633,7 @@ let instr_sub_ids ~sub_id_binders f instr =
let actual' = exp_sub_ids f actual in let actual' = exp_sub_ids f actual in
let typ' = sub_typ typ in let typ' = sub_typ typ in
if phys_equal actual' actual && phys_equal typ typ' then actual_pair if phys_equal actual' actual && phys_equal typ typ' then actual_pair
else (actual', typ')) else (actual', typ') )
actuals actuals
in in
if phys_equal ret_id' ret_id && phys_equal fun_exp' fun_exp && phys_equal actuals' actuals if phys_equal ret_id' ret_id && phys_equal fun_exp' fun_exp && phys_equal actuals' actuals
@ -1651,7 +1650,7 @@ let instr_sub_ids ~sub_id_binders f instr =
IList.map_changed IList.map_changed
(fun ((name, typ) as local_var) -> (fun ((name, typ) as local_var) ->
let typ' = sub_typ typ in let typ' = sub_typ typ in
if phys_equal typ typ' then local_var else (name, typ')) if phys_equal typ typ' then local_var else (name, typ') )
locals locals
in in
if phys_equal locals locals' then instr else Declare_locals (locals', loc) if phys_equal locals locals' then instr else Declare_locals (locals', loc)
@ -1738,7 +1737,7 @@ let compare_structural_instr instr1 instr2 exp_map =
else else
List.fold2_exn List.fold2_exn
~f:(fun (n, exp_map) id1 id2 -> ~f:(fun (n, exp_map) id1 id2 ->
if n <> 0 then (n, exp_map) else exp_compare_structural (Var id1) (Var id2) exp_map) if n <> 0 then (n, exp_map) else exp_compare_structural (Var id1) (Var id2) exp_map )
~init:(0, exp_map) ids1 ids2 ~init:(0, exp_map) ids1 ids2
in in
match (instr1, instr2) with match (instr1, instr2) with
@ -1768,7 +1767,7 @@ let compare_structural_instr instr1 instr2 exp_map =
else else
List.fold2_exn List.fold2_exn
~f:(fun (n, exp_map) arg1 arg2 -> ~f:(fun (n, exp_map) arg1 arg2 ->
if n <> 0 then (n, exp_map) else exp_typ_compare_structural arg1 arg2 exp_map) if n <> 0 then (n, exp_map) else exp_typ_compare_structural arg1 arg2 exp_map )
~init:(0, exp_map) args1 args2 ~init:(0, exp_map) args1 args2
in in
let n, exp_map = id_typ_opt_compare_structural ret_id1 ret_id2 exp_map in let n, exp_map = id_typ_opt_compare_structural ret_id1 ret_id2 exp_map in
@ -1794,7 +1793,7 @@ let compare_structural_instr instr1 instr2 exp_map =
if n <> 0 then (n, exp_map) if n <> 0 then (n, exp_map)
else else
let n, exp_map = exp_compare_structural (Lvar pv1) (Lvar pv2) exp_map in let n, exp_map = exp_compare_structural (Lvar pv1) (Lvar pv2) exp_map in
if n <> 0 then (n, exp_map) else (Typ.compare t1 t2, exp_map)) if n <> 0 then (n, exp_map) else (Typ.compare t1 t2, exp_map) )
~init:(0, exp_map) ptl1 ptl2 ~init:(0, exp_map) ptl1 ptl2
| _ -> | _ ->
(compare_instr instr1 instr2, exp_map) (compare_instr instr1 instr2, exp_map)

@ -298,4 +298,3 @@ let case_analysis_basic tenv (c1, st) (c2, (_, flag2)) =
let case_analysis tenv (c1, st1) (c2, st2) = let case_analysis tenv (c1, st1) (c2, st2) =
if Config.subtype_multirange then get_subtypes tenv (c1, st1) (c2, st2) if Config.subtype_multirange then get_subtypes tenv (c1, st1) (c2, st2)
else case_analysis_basic tenv (c1, st1) (c2, st2) else case_analysis_basic tenv (c1, st1) (c2, st2)

@ -31,7 +31,7 @@ let pp fmt (tenv: t) =
TypenameHash.iter TypenameHash.iter
(fun name typ -> (fun name typ ->
Format.fprintf fmt "@[<6>NAME: %s@." (Typ.Name.to_string name) ; Format.fprintf fmt "@[<6>NAME: %s@." (Typ.Name.to_string name) ;
Format.fprintf fmt "@[<6>TYPE: %a@." (Typ.Struct.pp Pp.text name) typ) Format.fprintf fmt "@[<6>TYPE: %a@." (Typ.Struct.pp Pp.text name) typ )
tenv tenv
@ -128,8 +128,8 @@ let global_tenv : t option ref = ref None
(** Load a type environment from a file *) (** Load a type environment from a file *)
let load_from_file (filename: DB.filename) : t option = let load_from_file (filename: DB.filename) : t option =
if DB.equal_filename filename DB.global_tenv_fname then ( if DB.equal_filename filename DB.global_tenv_fname then (
if is_none !global_tenv then global_tenv if is_none !global_tenv then
:= Serialization.read_from_file tenv_serializer DB.global_tenv_fname ; global_tenv := Serialization.read_from_file tenv_serializer DB.global_tenv_fname ;
!global_tenv ) !global_tenv )
else Serialization.read_from_file tenv_serializer filename else Serialization.read_from_file tenv_serializer filename
@ -157,4 +157,3 @@ let language_is tenv lang =
Config.equal_language lang Java Config.equal_language lang Java
| exception Found _ -> | exception Found _ ->
Config.equal_language lang Clang Config.equal_language lang Clang

@ -816,8 +816,8 @@ module Procname = struct
| Simple -> | Simple ->
(* methodname(...) or without ... if there are no parameters *) (* methodname(...) or without ... if there are no parameters *)
let cls_prefix = let cls_prefix =
if withclass then java_type_to_string_verbosity (split_typename j.class_name) verbosity if withclass then
^ "." java_type_to_string_verbosity (split_typename j.class_name) verbosity ^ "."
else "" else ""
in in
let params = match j.parameters with [] -> "" | _ -> "..." in let params = match j.parameters with [] -> "" | _ -> "..." in
@ -1186,7 +1186,6 @@ module Procname = struct
let serialize pname = let serialize pname =
let default () = Sqlite3.Data.TEXT (to_filename pname) in let default () = Sqlite3.Data.TEXT (to_filename pname) in
Base.Hashtbl.find_or_add pname_to_key pname ~default Base.Hashtbl.find_or_add pname_to_key pname ~default
end end
(** given two template arguments, try to generate mapping from generic ones to concrete ones. *) (** given two template arguments, try to generate mapping from generic ones to concrete ones. *)
@ -1242,7 +1241,6 @@ module Procname = struct
|> extract_mapping |> extract_mapping
| _ -> | _ ->
None None
end end
(** Return the return type of [pname_java]. *) (** Return the return type of [pname_java]. *)
@ -1352,7 +1350,6 @@ module Fieldname = struct
String.is_prefix ~prefix:"val$" (to_flat_string field_name) String.is_prefix ~prefix:"val$" (to_flat_string field_name)
| Clang _ -> | Clang _ ->
false false
end end
end end
@ -1439,11 +1436,10 @@ module Struct = struct
| Some {fields; statics} -> | Some {fields; statics} ->
List.find_map List.find_map
~f:(fun (f, t, a) -> ~f:(fun (f, t, a) ->
match Fieldname.equal f fn with true -> Some (t, a) | false -> None) match Fieldname.equal f fn with true -> Some (t, a) | false -> None )
(fields @ statics) (fields @ statics)
| None -> | None ->
None ) None )
| _ -> | _ ->
None None
end end

@ -640,5 +640,4 @@ module Struct : sig
val get_field_type_and_annotation : val get_field_type_and_annotation :
lookup:lookup -> Fieldname.t -> typ -> (typ * Annot.Item.t) option lookup:lookup -> Fieldname.t -> typ -> (typ * Annot.Item.t) option
(** Return the type of the field [fn] and its annotation, None if [typ] has no field named [fn] *) (** Return the type of the field [fn] and its annotation, None if [typ] has no field named [fn] *)
end end

@ -137,8 +137,8 @@ module Pair (Domain1 : S) (Domain2 : S) = struct
let ( <= ) ~lhs ~rhs = let ( <= ) ~lhs ~rhs =
if phys_equal lhs rhs then true if phys_equal lhs rhs then true
else Domain1.( <= ) ~lhs:(fst lhs) ~rhs:(fst rhs) else
&& Domain2.( <= ) ~lhs:(snd lhs) ~rhs:(snd rhs) Domain1.( <= ) ~lhs:(fst lhs) ~rhs:(fst rhs) && Domain2.( <= ) ~lhs:(snd lhs) ~rhs:(snd rhs)
let join astate1 astate2 = let join astate1 astate2 =
@ -192,7 +192,7 @@ module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = stru
else else
M.for_all M.for_all
(fun k lhs_v -> (fun k lhs_v ->
try ValueDomain.( <= ) ~lhs:lhs_v ~rhs:(M.find k rhs) with Not_found -> false) try ValueDomain.( <= ) ~lhs:lhs_v ~rhs:(M.find k rhs) with Not_found -> false )
lhs lhs
@ -207,7 +207,7 @@ module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = stru
| Some v, _ | _, Some v -> | Some v, _ | _, Some v ->
Some v Some v
| None, None -> | None, None ->
None) None )
astate1 astate2 astate1 astate2
@ -222,7 +222,7 @@ module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = stru
| Some v, _ | _, Some v -> | Some v, _ | _, Some v ->
Some v Some v
| None, None -> | None, None ->
None) None )
prev next prev next
@ -251,7 +251,7 @@ module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S
| Some v1, Some v2 -> | Some v1, Some v2 ->
Some (ValueDomain.join v1 v2) Some (ValueDomain.join v1 v2)
| _ -> | _ ->
None) None )
astate1 astate2 astate1 astate2
@ -264,7 +264,7 @@ module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S
| Some v1, Some v2 -> | Some v1, Some v2 ->
Some (ValueDomain.widen ~prev:v1 ~next:v2 ~num_iters) Some (ValueDomain.widen ~prev:v1 ~next:v2 ~num_iters)
| _ -> | _ ->
None) None )
prev next prev next

@ -162,7 +162,6 @@ struct
let cfg = CFG.from_pdesc pdesc in let cfg = CFG.from_pdesc pdesc in
let inv_map = exec_cfg cfg proc_data ~initial ~debug in let inv_map = exec_cfg cfg proc_data ~initial ~debug in
extract_post (CFG.id (CFG.exit_node cfg)) inv_map extract_post (CFG.id (CFG.exit_node cfg)) inv_map
end end
module MakeWithScheduler (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.MakeSIL) = module MakeWithScheduler (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.MakeSIL) =

@ -28,7 +28,6 @@ module PP = struct
in in
F.fprintf fmt "%a:%d@\n" SourceFile.pp loc.Location.file loc.Location.line ; F.fprintf fmt "%a:%d@\n" SourceFile.pp loc.Location.file loc.Location.line ;
for n = loc.Location.line - nbefore to loc.Location.line + nafter do printline n done for n = loc.Location.line - nbefore to loc.Location.line + nafter do printline n done
end end
(* PP *) (* PP *)
@ -109,5 +108,4 @@ module ST = struct
(Typ.Procname.to_string proc_name) ; (Typ.Procname.to_string proc_name) ;
L.progress "%s@." description ; L.progress "%s@." description ;
Reporting.log_error_deprecated proc_name ~loc ~ltr:trace exn ) Reporting.log_error_deprecated proc_name ~loc ~ltr:trace exn )
end end

@ -20,7 +20,7 @@ let make pdesc =
List.mapi List.mapi
~f:(fun index (name, typ) -> ~f:(fun index (name, typ) ->
let pvar = Pvar.mk name pname in let pvar = Pvar.mk name pname in
(AccessPath.base_of_pvar pvar typ, index)) (AccessPath.base_of_pvar pvar typ, index) )
attrs.ProcAttributes.formals attrs.ProcAttributes.formals
in in
List.fold List.fold

@ -72,7 +72,7 @@ struct
let dummy_assign = let dummy_assign =
HilInstr.Assign (lhs_access_path, HilExp.AccessPath access_path, loc) HilInstr.Assign (lhs_access_path, HilExp.AccessPath access_path, loc)
in in
TransferFunctions.exec_instr astate_acc extras node dummy_assign) TransferFunctions.exec_instr astate_acc extras node dummy_assign )
id_map actual_state id_map actual_state
in in
let actual_state'' = TransferFunctions.exec_instr actual_state' extras node hil_instr in let actual_state'' = TransferFunctions.exec_instr actual_state' extras node hil_instr in
@ -84,7 +84,6 @@ struct
if phys_equal actual_state actual_state' then astate else (actual_state', id_map) if phys_equal actual_state actual_state' then astate else (actual_state', id_map)
| Ignore -> | Ignore ->
astate astate
end end
module MakeAbstractInterpreterWithConfig module MakeAbstractInterpreterWithConfig
@ -98,7 +97,6 @@ struct
Preanal.do_preanalysis pdesc tenv ; Preanal.do_preanalysis pdesc tenv ;
let initial' = (initial, IdAccessPathMapDomain.empty) in let initial' = (initial, IdAccessPathMapDomain.empty) in
Option.map ~f:fst (Interpreter.compute_post ~debug:false proc_data ~initial:initial') Option.map ~f:fst (Interpreter.compute_post ~debug:false proc_data ~initial:initial')
end end
module MakeAbstractInterpreter = MakeAbstractInterpreterWithConfig (DefaultConfig) module MakeAbstractInterpreter = MakeAbstractInterpreterWithConfig (DefaultConfig)

@ -431,4 +431,3 @@ let rec find_superclasses_with_attributes check tenv tname =
if check struct_typ.annots then tname :: result_from_supers else result_from_supers if check struct_typ.annots then tname :: result_from_supers else result_from_supers
| _ -> | _ ->
[] []

@ -84,7 +84,6 @@ module InstrNode = struct
Procdesc.Node.pp_id fmt id Procdesc.Node.pp_id fmt id
| Instr_index i -> | Instr_index i ->
F.fprintf fmt "(%a: %d)" Procdesc.Node.pp_id id i F.fprintf fmt "(%a: %d)" Procdesc.Node.pp_id id i
end end
module type S = sig module type S = sig
@ -287,9 +286,8 @@ struct
List.mapi List.mapi
~f:(fun i instr -> ~f:(fun i instr ->
let id = (Procdesc.Node.get_id t, Instr_index i) in let id = (Procdesc.Node.get_id t, Instr_index i) in
(instr, Some id)) (instr, Some id) )
(instrs t) (instrs t)
end end
module NodeIdMap (CFG : S) = Caml.Map.Make (struct module NodeIdMap (CFG : S) = Caml.Map.Make (struct

@ -70,7 +70,6 @@ module ReversePostorder (CFG : ProcCfg.S) = struct
let visited_preds' = IdSet.add node_id t.visited_preds in let visited_preds' = IdSet.add node_id t.visited_preds in
let priority' = compute_priority cfg t.node visited_preds' in let priority' = compute_priority cfg t.node visited_preds' in
{t with visited_preds= visited_preds'; priority= priority'} {t with visited_preds= visited_preds'; priority= priority'}
end end
type t = {worklist: WorkUnit.t M.t; cfg: CFG.t} type t = {worklist: WorkUnit.t M.t; cfg: CFG.t}
@ -104,7 +103,7 @@ module ReversePostorder (CFG : ProcCfg.S) = struct
M.fold M.fold
(fun id work (lowest_id, lowest_priority) -> (fun id work (lowest_id, lowest_priority) ->
let priority = WorkUnit.priority work in let priority = WorkUnit.priority work in
if priority < lowest_priority then (id, priority) else (lowest_id, lowest_priority)) if priority < lowest_priority then (id, priority) else (lowest_id, lowest_priority) )
t.worklist (init_id, init_priority) t.worklist (init_id, init_priority)
in in
let max_priority_work = M.find max_priority_id t.worklist in let max_priority_work = M.find max_priority_id t.worklist in

@ -36,5 +36,4 @@ module Make (P : Payload) : S with type payload = P.payload = struct
None None
| Some summary -> | Some summary ->
P.read_payload summary P.read_payload summary
end end

@ -38,8 +38,7 @@ let add_or_replace_check_changed tenv check_attribute_change prop atom =
let _, nexp = List.hd_exn pairs in let _, nexp = List.hd_exn pairs in
(* len exps0 > 0 by match *) (* len exps0 > 0 by match *)
let atom_map = function let atom_map = function
| Sil.Apred (att, exp :: _) | (Sil.Apred (att, exp :: _) | Anpred (att, exp :: _))
| Anpred (att, exp :: _)
when Exp.equal nexp exp && attributes_in_same_category att att0 -> when Exp.equal nexp exp && attributes_in_same_category att att0 ->
check_attribute_change att att0 ; atom check_attribute_change att att0 ; atom
| atom' -> | atom' ->
@ -268,8 +267,8 @@ let find_arithmetic_problem tenv proc_node_session prop exp =
| Exp.UnOp (_, e, _) -> | Exp.UnOp (_, e, _) ->
walk e walk e
| Exp.BinOp (op, e1, e2) -> | Exp.BinOp (op, e1, e2) ->
if Binop.equal op Binop.Div || Binop.equal op Binop.Mod then exps_divided if Binop.equal op Binop.Div || Binop.equal op Binop.Mod then
:= e2 :: !exps_divided ; exps_divided := e2 :: !exps_divided ;
walk e1 ; walk e1 ;
walk e2 walk e2
| Exp.Exn _ -> | Exp.Exn _ ->
@ -394,10 +393,10 @@ let find_equal_formal_path tenv e prop =
| None -> | None ->
None ) None )
| _ -> | _ ->
None) None )
fields ~init:None fields ~init:None
| _ -> | _ ->
None) None )
prop.Prop.sigma ~init:None prop.Prop.sigma ~init:None
in in
match find_in_sigma e [] with match find_in_sigma e [] with
@ -409,4 +408,3 @@ let find_equal_formal_path tenv e prop =
Some vfs Some vfs
| _ -> | _ ->
None None

@ -397,6 +397,7 @@ let execute___set_mem_attribute {Builtin.tenv; pdesc; prop_; path; ret_id; args;
| _ -> | _ ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
let set_attr tenv pdesc prop path exp attr = let set_attr tenv pdesc prop path exp attr =
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
let n_lexp, prop = check_arith_norm_exp tenv pname exp prop in let n_lexp, prop = check_arith_norm_exp tenv pname exp prop in
@ -521,7 +522,7 @@ let execute_free mk ?(mark_as_freed= true) {Builtin.pdesc; instr; tenv; prop_; p
~f:(fun p -> ~f:(fun p ->
execute_free_nonzero_ mk ~mark_as_freed pdesc tenv instr p execute_free_nonzero_ mk ~mark_as_freed pdesc tenv instr p
(Prop.exp_normalize_prop tenv p lexp) (Prop.exp_normalize_prop tenv p lexp)
typ loc) typ loc )
prop_nonzero prop_nonzero
in in
List.map ~f:(fun p -> (p, path)) plist List.map ~f:(fun p -> (p, path)) plist

@ -134,4 +134,3 @@ let to_files {introduced; fixed; preexisting} destdir =
Out_channel.write_all (destdir ^/ "fixed.json") ~data:(Jsonbug_j.string_of_report fixed) ; Out_channel.write_all (destdir ^/ "fixed.json") ~data:(Jsonbug_j.string_of_report fixed) ;
Out_channel.write_all (destdir ^/ "preexisting.json") Out_channel.write_all (destdir ^/ "preexisting.json")
~data:(Jsonbug_j.string_of_report preexisting) ~data:(Jsonbug_j.string_of_report preexisting)

@ -123,7 +123,7 @@ let skip_duplicated_types_on_filenames renamings (diff: Differential.t) : Differ
String.compare f1 f2 String.compare f1 f2
in in
let cmp ((issue1, _) as issue_with_previous_file1) ((issue2, _) as issue_with_previous_file2) = let cmp ((issue1, _) as issue_with_previous_file1) ((issue2, _) as issue_with_previous_file2) =
[%compare : Digest.t * string * issue_file_with_renaming] [%compare : Caml.Digest.t * string * issue_file_with_renaming]
(issue1.Jsonbug_t.key, issue1.Jsonbug_t.bug_type, issue_with_previous_file1) (issue1.Jsonbug_t.key, issue1.Jsonbug_t.bug_type, issue_with_previous_file1)
(issue2.Jsonbug_t.key, issue2.Jsonbug_t.bug_type, issue_with_previous_file2) (issue2.Jsonbug_t.key, issue2.Jsonbug_t.bug_type, issue_with_previous_file2)
in in
@ -180,7 +180,7 @@ let value_of_qualifier_tag qts tag =
type file_extension = string [@@deriving compare] type file_extension = string [@@deriving compare]
type weak_hash = string * string * string * Digest.t * string option [@@deriving compare] type weak_hash = string * string * string * Caml.Digest.t * string option [@@deriving compare]
let skip_anonymous_class_renamings (diff: Differential.t) : Differential.t = let skip_anonymous_class_renamings (diff: Differential.t) : Differential.t =
(* (*

@ -22,7 +22,7 @@ let analyze_exe_env_tasks cluster exe_env : Tasks.t =
[ (fun () -> [ (fun () ->
let call_graph = Exe_env.get_cg exe_env in let call_graph = Exe_env.get_cg exe_env in
Callbacks.iterate_callbacks call_graph exe_env ; Callbacks.iterate_callbacks call_graph exe_env ;
if Config.write_html then Printer.write_all_html_files cluster) ] if Config.write_html then Printer.write_all_html_files cluster ) ]
(** Create tasks to analyze a cluster *) (** Create tasks to analyze a cluster *)
@ -85,7 +85,7 @@ let cluster_should_be_analyzed ~changed_files cluster =
SourceFile.Set.fold SourceFile.Set.fold
(fun source_file source_dir_set -> (fun source_file source_dir_set ->
let source_dir = DB.source_dir_from_source_file source_file in let source_dir = DB.source_dir_from_source_file source_file in
String.Set.add source_dir_set (DB.source_dir_to_string source_dir)) String.Set.add source_dir_set (DB.source_dir_to_string source_dir) )
changed_files String.Set.empty changed_files String.Set.empty
in in
Option.map ~f:source_dirs_to_analyze changed_files Option.map ~f:source_dirs_to_analyze changed_files
@ -134,8 +134,8 @@ let main ~changed_files ~makefile =
in in
let n_clusters_to_analyze = List.length clusters_to_analyze in let n_clusters_to_analyze = List.length clusters_to_analyze in
L.progress "Found %d%s source file%s to analyze in %s@." n_clusters_to_analyze L.progress "Found %d%s source file%s to analyze in %s@." n_clusters_to_analyze
( if Config.reactive_mode || Option.is_some changed_files then " (out of " ( if Config.reactive_mode || Option.is_some changed_files then
^ string_of_int (List.length all_clusters) ^ ")" " (out of " ^ string_of_int (List.length all_clusters) ^ ")"
else "" ) else "" )
(if Int.equal n_clusters_to_analyze 1 then "" else "s") (if Int.equal n_clusters_to_analyze 1 then "" else "s")
Config.results_dir ; Config.results_dir ;

@ -56,7 +56,7 @@ let compute_hash (kind: string) (type_str: string) (proc_name: Typ.Procname.t) (
in in
Utils.better_hash Utils.better_hash
(kind, type_str, hashable_procedure_name, base_filename, location_independent_qualifier) (kind, type_str, hashable_procedure_name, base_filename, location_independent_qualifier)
|> Digest.to_hex |> Caml.Digest.to_hex
let exception_value = "exception" let exception_value = "exception"
@ -143,7 +143,7 @@ let summary_values summary =
; verr= ; verr=
Errlog.size Errlog.size
(fun ekind in_footprint -> (fun ekind in_footprint ->
Exceptions.equal_err_kind ekind Exceptions.Kerror && in_footprint) Exceptions.equal_err_kind ekind Exceptions.Kerror && in_footprint )
err_log err_log
; vflags= attributes.ProcAttributes.proc_flags ; vflags= attributes.ProcAttributes.proc_flags
; vfile= SourceFile.to_string attributes.ProcAttributes.loc.Location.file ; vfile= SourceFile.to_string attributes.ProcAttributes.loc.Location.file
@ -177,7 +177,6 @@ module ProcsCsv = struct
pp "%d," sv.vline ; pp "%d," sv.vline ;
pp "\"%s\"," (Escape.escape_csv sv.vsignature) ; pp "\"%s\"," (Escape.escape_csv sv.vsignature) ;
pp "%s@\n" sv.vproof_trace pp "%s@\n" sv.vproof_trace
end end
let should_report (issue_kind: Exceptions.err_kind) issue_type error_desc eclass = let should_report (issue_kind: Exceptions.err_kind) issue_type error_desc eclass =
@ -290,7 +289,7 @@ module IssuesJson = struct
; procedure_start_line ; procedure_start_line
; file ; file
; bug_trace= loc_trace_to_jsonbug_record err_data.loc_trace key.err_kind ; bug_trace= loc_trace_to_jsonbug_record err_data.loc_trace key.err_kind
; key= err_data.node_id_key.node_key |> Digest.to_hex ; key= err_data.node_id_key.node_key |> Caml.Digest.to_hex
; qualifier_tags= Localise.Tags.tag_value_records_of_tags key.err_desc.tags ; qualifier_tags= Localise.Tags.tag_value_records_of_tags key.err_desc.tags
; hash= compute_hash kind bug_type procname file qualifier ; hash= compute_hash kind bug_type procname file qualifier
; dotty= error_desc_to_dotty_string key.err_desc ; dotty= error_desc_to_dotty_string key.err_desc
@ -309,7 +308,6 @@ module IssuesJson = struct
(** Write bug report in JSON format *) (** Write bug report in JSON format *)
let pp_issues_of_error_log fmt error_filter _ proc_loc_opt procname err_log = let pp_issues_of_error_log fmt error_filter _ proc_loc_opt procname err_log =
Errlog.iter (pp_issue fmt error_filter procname proc_loc_opt) err_log Errlog.iter (pp_issue fmt error_filter procname proc_loc_opt) err_log
end end
let pp_custom_of_report fmt report fields = let pp_custom_of_report fmt report fields =
@ -352,9 +350,9 @@ let pp_custom_of_report fmt report fields =
| `Issue_field_bug_trace -> | `Issue_field_bug_trace ->
pp_trace fmt issue.bug_trace (comma_separator index) pp_trace fmt issue.bug_trace (comma_separator index)
| `Issue_field_key -> | `Issue_field_key ->
Format.fprintf fmt "%s%s" (comma_separator index) (Digest.to_hex issue.key) Format.fprintf fmt "%s%s" (comma_separator index) (Caml.Digest.to_hex issue.key)
| `Issue_field_hash -> | `Issue_field_hash ->
Format.fprintf fmt "%s%s" (comma_separator index) (Digest.to_hex issue.hash) Format.fprintf fmt "%s%s" (comma_separator index) (Caml.Digest.to_hex issue.hash)
| `Issue_field_line_offset -> | `Issue_field_line_offset ->
Format.fprintf fmt "%s%d" (comma_separator index) Format.fprintf fmt "%s%d" (comma_separator index)
(issue.line - issue.procedure_start_line) (issue.line - issue.procedure_start_line)
@ -371,7 +369,7 @@ let pp_custom_of_report fmt report fields =
let tests_jsonbug_compare bug1 bug2 = let tests_jsonbug_compare bug1 bug2 =
let open Jsonbug_t in let open Jsonbug_t in
[%compare : string * string * int * string * Digest.t] [%compare : string * string * int * string * Caml.Digest.t]
(bug1.file, bug1.procedure, bug1.line - bug1.procedure_start_line, bug1.bug_type, bug1.hash) (bug1.file, bug1.procedure, bug1.line - bug1.procedure_start_line, bug1.bug_type, bug1.hash)
(bug2.file, bug2.procedure, bug2.line - bug2.procedure_start_line, bug2.bug_type, bug2.hash) (bug2.file, bug2.procedure, bug2.line - bug2.procedure_start_line, bug2.bug_type, bug2.hash)
@ -395,7 +393,6 @@ module IssuesTxt = struct
(** Write bug report in text format *) (** Write bug report in text format *)
let pp_issues_of_error_log fmt error_filter _ proc_loc_opt _ err_log = let pp_issues_of_error_log fmt error_filter _ proc_loc_opt _ err_log =
Errlog.iter (pp_issue fmt error_filter proc_loc_opt) err_log Errlog.iter (pp_issue fmt error_filter proc_loc_opt) err_log
end end
let pp_text_of_report fmt report = let pp_text_of_report fmt report =
@ -423,7 +420,6 @@ module CallsCsv = struct
pp "%a@\n" Specs.CallStats.pp_trace trace pp "%a@\n" Specs.CallStats.pp_trace trace
in in
Specs.CallStats.iter do_call stats.Specs.call_stats Specs.CallStats.iter do_call stats.Specs.call_stats
end end
module Stats = struct module Stats = struct
@ -559,7 +555,6 @@ module Stats = struct
F.fprintf fmt "@\n -------------------@\n" ; F.fprintf fmt "@\n -------------------@\n" ;
F.fprintf fmt "@\nDetailed Errors@\n@\n" ; F.fprintf fmt "@\nDetailed Errors@\n@\n" ;
List.iter ~f:(fun s -> F.fprintf fmt "%s@\n" s) (List.rev stats.saved_errors) List.iter ~f:(fun s -> F.fprintf fmt "%s@\n" s) (List.rev stats.saved_errors)
end end
module Report = struct module Report = struct
@ -605,7 +600,6 @@ module PreconditionStats = struct
L.result "Procedures with empty precondition: %d@." !nr_empty ; L.result "Procedures with empty precondition: %d@." !nr_empty ;
L.result "Procedures with only allocation conditions: %d@." !nr_onlyallocation ; L.result "Procedures with only allocation conditions: %d@." !nr_onlyallocation ;
L.result "Procedures with data constraints: %d@." !nr_dataconstraints L.result "Procedures with data constraints: %d@." !nr_dataconstraints
end end
(* Wrapper of an issue that compares all parts except the procname *) (* Wrapper of an issue that compares all parts except the procname *)
@ -631,13 +625,12 @@ module Issue = struct
identical warning on the same line. Accomplish this by sorting without regard to procname, then identical warning on the same line. Accomplish this by sorting without regard to procname, then
de-duplicating. *) de-duplicating. *)
let sort_filter_issues issues = let sort_filter_issues issues =
let issues' = List.dedup ~compare issues in let issues' = List.dedup_and_sort ~compare issues in
( if Config.developer_mode then ( if Config.developer_mode then
let num_pruned_issues = List.length issues - List.length issues' in let num_pruned_issues = List.length issues - List.length issues' in
if num_pruned_issues > 0 then if num_pruned_issues > 0 then
L.user_warning "Note: pruned %d duplicate issues@\n" num_pruned_issues ) ; L.user_warning "Note: pruned %d duplicate issues@\n" num_pruned_issues ) ;
issues' issues'
end end
let error_filter filters proc_name file error_desc error_name = let error_filter filters proc_name file error_desc error_name =
@ -842,7 +835,7 @@ module AnalysisResults = struct
List.iter List.iter
~f:(fun arg -> ~f:(fun arg ->
if not (Filename.check_suffix arg Config.specs_files_suffix) && arg <> "." then if not (Filename.check_suffix arg Config.specs_files_suffix) && arg <> "." then
print_usage_exit ("file " ^ arg ^ ": arguments must be .specs files")) print_usage_exit ("file " ^ arg ^ ": arguments must be .specs files") )
Config.anon_args ; Config.anon_args ;
if Config.test_filtering then ( Inferconfig.test () ; L.exit 0 ) ; if Config.test_filtering then ( Inferconfig.test () ; L.exit 0 ) ;
if List.is_empty Config.anon_args then load_specfiles () else List.rev Config.anon_args ) if List.is_empty Config.anon_args then load_specfiles () else List.rev Config.anon_args )
@ -918,7 +911,6 @@ module AnalysisResults = struct
iterator_of_summary_list r iterator_of_summary_list r
| None -> | None ->
L.(die UserError) "Error: cannot open analysis results file %s@." fname L.(die UserError) "Error: cannot open analysis results file %s@." fname
end end
let register_perf_stats_report () = let register_perf_stats_report () =
@ -1004,7 +996,7 @@ let pp_summary_and_issues formats_by_report_kind issue_formats =
let error_filter = error_filter filters proc_name in let error_filter = error_filter filters proc_name in
List.iter List.iter
~f:(fun issue_format -> pp_issue_in_format issue_format error_filter issue) ~f:(fun issue_format -> pp_issue_in_format issue_format error_filter issue)
issue_formats) issue_formats )
(Issue.sort_filter_issues !all_issues) ; (Issue.sort_filter_issues !all_issues) ;
if Config.precondition_stats then PreconditionStats.pp_stats () ; if Config.precondition_stats then PreconditionStats.pp_stats () ;
LintIssues.load_issues_to_errlog_map Config.lint_issues_dir_name ; LintIssues.load_issues_to_errlog_map Config.lint_issues_dir_name ;

@ -59,4 +59,3 @@ let try_capture (attributes: ProcAttributes.t) : ProcAttributes.t option =
Caveat: it's possible that procedure will be captured in some other unrelated file Caveat: it's possible that procedure will be captured in some other unrelated file
later - infer may ignore it then. *) later - infer may ignore it then. *)
Attributes.load_defined attributes.proc_name Attributes.load_defined attributes.proc_name

@ -153,4 +153,3 @@ let register_report_at_exit =
String.Table.set registered_files ~key:file ~data:() ; String.Table.set registered_files ~key:file ~data:() ;
if not Config.buck_cache_mode then if not Config.buck_cache_mode then
Epilogues.register ~f:(report_at_exit file) ("stats reporting in " ^ file) ) Epilogues.register ~f:(report_at_exit file) ("stats reporting in " ^ file) )

@ -121,7 +121,7 @@ let remove_abduced_retvars tenv p =
if Pvar.is_abduced pvar then (pvar :: abduceds, normal_pvars) if Pvar.is_abduced pvar then (pvar :: abduceds, normal_pvars)
else (abduceds, pvar :: normal_pvars) else (abduceds, pvar :: normal_pvars)
| _ -> | _ ->
pvars) pvars )
~init:([], []) p.Prop.sigma ~init:([], []) p.Prop.sigma
in in
let _, p' = Attribute.deallocate_stack_vars tenv p abduceds in let _, p' = Attribute.deallocate_stack_vars tenv p abduceds in
@ -189,4 +189,3 @@ let remove_seed_vars tenv (prop: 'a Prop.t) : Prop.normal Prop.t =
let sigma = prop.sigma in let sigma = prop.sigma in
let sigma' = List.filter ~f:hpred_not_seed sigma in let sigma' = List.filter ~f:hpred_not_seed sigma in
Prop.normalize tenv (Prop.set prop ~sigma:sigma') Prop.normalize tenv (Prop.set prop ~sigma:sigma')

@ -182,4 +182,3 @@ let report_cycle tenv hpred original_prop =
Some (exn_retain_cycle tenv prop hpred cycle) Some (exn_retain_cycle tenv prop hpred cycle)
| _ -> | _ ->
None None

@ -84,7 +84,7 @@ let collect_all_stats_files () =
let targets_files = let targets_files =
List.map List.map
~f:(fun (t, p) -> ~f:(fun (t, p) ->
(t, find_stats_files_in_dir (concatenate_paths buck_out_parent p))) (t, find_stats_files_in_dir (concatenate_paths buck_out_parent p)) )
r r
in in
Ok (Buck_out targets_files) Ok (Buck_out targets_files)
@ -179,4 +179,3 @@ let generate_files () =
write_to_json_file_opt write_to_json_file_opt
(Filename.concat aggregated_reporting_stats_dir aggregated_stats_filename) (Filename.concat aggregated_reporting_stats_dir aggregated_stats_filename)
j.reporting_json_data j.reporting_json_data

@ -67,5 +67,4 @@ module Runner = struct
let complete runner = let complete runner =
ProcessPool.wait_all runner.pool ; ProcessPool.wait_all runner.pool ;
Queue.iter ~f:(fun f -> f ()) runner.all_continuations Queue.iter ~f:(fun f -> f ()) runner.all_continuations
end end

@ -889,7 +889,7 @@ let abstract_pure_part tenv p ~(from_abstract_footprint: bool) =
| Sil.Aneq (Var _, _) | Sil.Apred (_, (Var _) :: _) | Anpred (_, (Var _) :: _) -> | Sil.Aneq (Var _, _) | Sil.Apred (_, (Var _) :: _) | Anpred (_, (Var _) :: _) ->
a :: pi a :: pi
| Sil.Aeq _ | Aneq _ | Apred _ | Anpred _ -> | Sil.Aeq _ | Aneq _ | Apred _ | Anpred _ ->
pi) pi )
~init:[] pi_filtered ~init:[] pi_filtered
in in
List.rev new_pure List.rev new_pure
@ -926,7 +926,7 @@ let abstract_gc tenv p =
let no_fav_e1 = Sil.fav_is_empty fav_e1 in let no_fav_e1 = Sil.fav_is_empty fav_e1 in
let no_fav_e2 = Sil.fav_is_empty fav_e2 in let no_fav_e2 = Sil.fav_is_empty fav_e2 in
(no_fav_e1 || intersect_e1 ()) && (no_fav_e2 || intersect_e2 ()) (no_fav_e1 || intersect_e1 ()) && (no_fav_e2 || intersect_e2 ())
| Sil.Apred _ | Anpred _ as a -> | (Sil.Apred _ | Anpred _) as a ->
let fav_a = Sil.atom_fav a in let fav_a = Sil.atom_fav a in
Sil.fav_is_empty fav_a Sil.fav_is_empty fav_a
|| IList.intersect Ident.compare (Sil.fav_to_list fav_a) (Sil.fav_to_list fav_p_without_pi) || IList.intersect Ident.compare (Sil.fav_to_list fav_a) (Sil.fav_to_list fav_p_without_pi)
@ -1111,8 +1111,7 @@ let check_junk ?original_prop pname tenv prop =
in in
let ml_bucket_opt = let ml_bucket_opt =
match resource with match resource with
| PredSymb.Rmemory PredSymb.Mnew | (PredSymb.Rmemory PredSymb.Mnew | PredSymb.Rmemory PredSymb.Mnew_array)
| PredSymb.Rmemory PredSymb.Mnew_array
when Config.curr_language_is Config.Clang -> when Config.curr_language_is Config.Clang ->
Mleak_buckets.should_raise_cpp_leak Mleak_buckets.should_raise_cpp_leak
| _ -> | _ ->
@ -1137,9 +1136,7 @@ let check_junk ?original_prop pname tenv prop =
(false, exn) (false, exn)
| None -> | None ->
(true, exn_leak) ) (true, exn_leak) )
| Some _, Rmemory Mobjc | (Some _, Rmemory Mobjc | Some _, Rmemory Mnew | Some _, Rmemory Mnew_array)
| Some _, Rmemory Mnew
| Some _, Rmemory Mnew_array
when Config.curr_language_is Config.Clang -> when Config.curr_language_is Config.Clang ->
(is_none ml_bucket_opt, exn_leak) (is_none ml_bucket_opt, exn_leak)
| Some _, Rmemory _ -> | Some _, Rmemory _ ->
@ -1327,5 +1324,4 @@ let lifted_abstract pname tenv pset =
let abstracted_pset = Propset.map_option tenv f pset in let abstracted_pset = Propset.map_option tenv f pset in
abstracted_pset abstracted_pset
(***************** End of Main Abstraction Functions *****************) (***************** End of Main Abstraction Functions *****************)

@ -109,7 +109,7 @@ end = struct
let fsel' = let fsel' =
List.map List.map
~f:(fun (f'', se'') -> ~f:(fun (f'', se'') ->
if Typ.Fieldname.equal f'' fld then (fld, se_mod) else (f'', se'')) if Typ.Fieldname.equal f'' fld then (fld, se_mod) else (f'', se'') )
fsel fsel
in in
Sil.Estruct (fsel', inst) Sil.Estruct (fsel', inst)
@ -286,7 +286,6 @@ end = struct
in in
let hpred' = hpred_replace_strexp tenv footprint_part hpred syn_offs update in let hpred' = hpred_replace_strexp tenv footprint_part hpred syn_offs update in
replace_hpred (sigma, hpred, syn_offs) hpred' replace_hpred (sigma, hpred, syn_offs) hpred'
end end
(** This function renames expressions in [p]. The renaming is, roughly (** This function renames expressions in [p]. The renaming is, roughly
@ -305,8 +304,8 @@ let prop_replace_path_index tenv (p: Prop.exposed Prop.t) (path: StrexpMatch.pat
let new_e_path_index = let new_e_path_index =
Prop.exp_normalize_prop tenv p (Exp.Lindex (e_path, new_index)) Prop.exp_normalize_prop tenv p (Exp.Lindex (e_path, new_index))
in in
(old_e_path_index, new_e_path_index) :: acc_inner) (old_e_path_index, new_e_path_index) :: acc_inner )
~init:acc_outer map) ~init:acc_outer map )
~init:[] elist_path ~init:[] elist_path
in in
let expmap_fun e' = let expmap_fun e' =
@ -605,7 +604,7 @@ let check_after_array_abstraction tenv prop =
List.iter List.iter
~f:(fun (f, se) -> ~f:(fun (f, se) ->
let typ_f = Typ.Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f typ in let typ_f = Typ.Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f typ in
check_se root (offs @ [Sil.Off_fld (f, typ)]) typ_f se) check_se root (offs @ [Sil.Off_fld (f, typ)]) typ_f se )
fsel fsel
in in
let check_hpred = function let check_hpred = function
@ -690,4 +689,3 @@ let remove_redundant_elements tenv prop =
let prop' = Prop.set prop ~sigma:sigma' ~sigma_fp:sigma_fp' in let prop' = Prop.set prop ~sigma:sigma' ~sigma_fp:sigma_fp' in
Prop.normalize tenv prop' Prop.normalize tenv prop'
else prop else prop

@ -70,4 +70,3 @@ let pp_registered fmt () =
let print_and_exit () = let print_and_exit () =
pp_registered Format.std_formatter () ; pp_registered Format.std_formatter () ;
L.exit 0 L.exit 0

@ -65,7 +65,7 @@ let iterate_procedure_callbacks get_proc_desc exe_env summary proc_desc =
~f:(fun summary (language, resolved, proc_callback) -> ~f:(fun summary (language, resolved, proc_callback) ->
if Config.equal_language language procedure_language && (resolved || not is_specialized) then if Config.equal_language language procedure_language && (resolved || not is_specialized) then
proc_callback {get_proc_desc; get_procs_in_file; tenv; summary; proc_desc} proc_callback {get_proc_desc; get_procs_in_file; tenv; summary; proc_desc}
else summary) else summary )
!procedure_callbacks !procedure_callbacks
@ -82,7 +82,7 @@ let iterate_cluster_callbacks all_procs exe_env get_proc_desc =
in in
List.iter List.iter
~f:(fun (language_opt, cluster_callback) -> ~f:(fun (language_opt, cluster_callback) ->
if language_matches language_opt then cluster_callback environment) if language_matches language_opt then cluster_callback environment )
!cluster_callbacks !cluster_callbacks

@ -49,4 +49,3 @@ let pp_cluster fmt (nr, cluster) =
(* touch the target of the rule to let `make` know that the job has been done *) (* touch the target of the rule to let `make` know that the job has been done *)
F.fprintf fmt "\t%@touch $%@@\n" ; F.fprintf fmt "\t%@touch $%@@\n" ;
F.fprintf fmt "@\n" F.fprintf fmt "@\n"

@ -49,4 +49,3 @@ let create_cluster_makefile (clusters: Cluster.t list) (fname: string) =
List.iteri ~f:do_cluster clusters ; List.iteri ~f:do_cluster clusters ;
pp_epilog fmt () ; pp_epilog fmt () ;
Out_channel.close outc Out_channel.close outc

@ -53,7 +53,7 @@ let stitch_summaries stacktrace_file summary_files out_file =
let summary_map = let summary_map =
List.fold List.fold
~f:(fun acc stacktree -> ~f:(fun acc stacktree ->
String.Map.add ~key:(frame_id_of_summary stacktree) ~data:stacktree acc) String.Map.set ~key:(frame_id_of_summary stacktree) ~data:stacktree acc )
~init:String.Map.empty summaries ~init:String.Map.empty summaries
in in
let expand_stack_frame frame = let expand_stack_frame frame =
@ -76,7 +76,7 @@ let collect_all_summaries root_summaries_dir stacktrace_file stacktraces_dir =
if Sys.is_directory path <> `Yes && Filename.check_suffix path "json" if Sys.is_directory path <> `Yes && Filename.check_suffix path "json"
&& String.is_suffix ~suffix:"crashcontext" (Filename.dirname path) && String.is_suffix ~suffix:"crashcontext" (Filename.dirname path)
then path :: summaries then path :: summaries
else summaries) else summaries )
[] root_summaries_dir [] root_summaries_dir
in in
let pair_for_stacktrace_file = let pair_for_stacktrace_file =

@ -181,7 +181,6 @@ end = struct
let set = lookup_const' const_tbl r in let set = lookup_const' const_tbl r in
List.for_all ~f:(fun v' -> Exp.equal (find' tbl v') r) vars' List.for_all ~f:(fun v' -> Exp.equal (find' tbl v') r) vars'
&& List.for_all ~f:(fun c -> Exp.Set.mem c set) nonvars && List.for_all ~f:(fun c -> Exp.Set.mem c set) nonvars
end end
(** {2 Modules for checking whether join or meet loses too much info} *) (** {2 Modules for checking whether join or meet loses too much info} *)
@ -234,7 +233,6 @@ end = struct
not (Exp.Set.mem e lexps) not (Exp.Set.mem e lexps)
| _ -> | _ ->
false false
end end
module CheckJoinPre : InfoLossCheckerSig = struct module CheckJoinPre : InfoLossCheckerSig = struct
@ -356,7 +354,6 @@ end = struct
CheckJoinPre.add side e1 e2 CheckJoinPre.add side e1 e2
| JoinState.Post -> | JoinState.Post ->
CheckJoinPost.add side e1 e2 CheckJoinPost.add side e1 e2
end end
module CheckMeet : InfoLossCheckerSig = struct module CheckMeet : InfoLossCheckerSig = struct
@ -452,7 +449,6 @@ end = struct
let res = !tbl in let res = !tbl in
tbl := [] ; tbl := [] ;
res res
end end
(** {2 Module for introducing fresh variables} *) (** {2 Module for introducing fresh variables} *)
@ -553,7 +549,6 @@ end = struct
acc acc
in in
List.fold ~f:f_ineqs ~init:eqs t_minimal List.fold ~f:f_ineqs ~init:eqs t_minimal
end end
(** {2 Modules for renaming} *) (** {2 Modules for renaming} *)
@ -868,7 +863,6 @@ end = struct
in in
let entry = (e1, e2, e) in let entry = (e1, e2, e) in
push entry ; Todo.push entry ; e push entry ; Todo.push entry ; e
end end
(** {2 Functions for constructing fresh sil data types} *) (** {2 Functions for constructing fresh sil data types} *)
@ -1643,7 +1637,7 @@ let sigma_partial_join tenv mode (sigma1: Prop.sigma) (sigma2: Prop.sigma)
SymOp.try_finally SymOp.try_finally
~f:(fun () -> ~f:(fun () ->
if Rename.check lost_little then (s1, s2, s3) if Rename.check lost_little then (s1, s2, s3)
else ( L.d_strln "failed Rename.check" ; raise Sil.JoinFail )) else ( L.d_strln "failed Rename.check" ; raise Sil.JoinFail ) )
~finally:CheckJoin.final ~finally:CheckJoin.final
@ -1897,8 +1891,9 @@ let prop_partial_meet tenv p1 p2 =
FreshVarExp.init () ; FreshVarExp.init () ;
Todo.init () ; Todo.init () ;
try try
SymOp.try_finally ~f:(fun () -> Some (eprop_partial_meet tenv p1 p2)) ~finally:(fun () -> SymOp.try_finally
Rename.final () ; FreshVarExp.final () ; Todo.final () ) ~f:(fun () -> Some (eprop_partial_meet tenv p1 p2))
~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ())
with Sil.JoinFail -> None with Sil.JoinFail -> None
@ -2011,7 +2006,8 @@ let prop_partial_join pname tenv mode p1 p2 =
Todo.reset rename_footprint ; Todo.reset rename_footprint ;
let res = eprop_partial_join' tenv mode (Prop.expose p1') (Prop.expose p2') in let res = eprop_partial_join' tenv mode (Prop.expose p1') (Prop.expose p2') in
if !Config.footprint then JoinState.set_footprint false ; if !Config.footprint then JoinState.set_footprint false ;
Some res) ~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final () ) Some res )
~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ())
with Sil.JoinFail -> None ) with Sil.JoinFail -> None )
| Some _ -> | Some _ ->
res_by_implication_only res_by_implication_only
@ -2022,8 +2018,9 @@ let eprop_partial_join tenv mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed P
Rename.init () ; Rename.init () ;
FreshVarExp.init () ; FreshVarExp.init () ;
Todo.init () ; Todo.init () ;
SymOp.try_finally ~f:(fun () -> eprop_partial_join' tenv mode ep1 ep2) ~finally:(fun () -> SymOp.try_finally
Rename.final () ; FreshVarExp.final () ; Todo.final () ) ~f:(fun () -> eprop_partial_join' tenv mode ep1 ep2)
~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ())
(** {2 Join and Meet for Propset} *) (** {2 Join and Meet for Propset} *)
@ -2232,4 +2229,3 @@ let propset_meet_generate_pre tenv pset =
let plist_old = Propset.to_proplist pset in let plist_old = Propset.to_proplist pset in
let plist_new = Propset.to_proplist pset_new in let plist_new = Propset.to_proplist pset_new in
plist_new @ plist_old plist_new @ plist_old

@ -111,10 +111,11 @@ let print_stack_info = ref false
(* replace a dollar sign in a name with a D. We need this because dotty get confused if there is*) (* replace a dollar sign in a name with a D. We need this because dotty get confused if there is*)
(* a dollar sign i a label*) (* a dollar sign i a label*)
let strip_special_chars b = let strip_special_chars b =
let b = Bytes.of_string b in
let replace st c c' = let replace st c c' =
if String.contains st c then if Bytes.contains st c then
let idx = String.index_exn st c in let idx = String.index_exn (Bytes.to_string st) c in
try st.[idx] <- c' ; st with Invalid_argument _ -> try Bytes.set st idx c' ; st with Invalid_argument _ ->
L.internal_error "@\n@\nstrip_special_chars: Invalid argument!@\n@." ; L.internal_error "@\n@\nstrip_special_chars: Invalid argument!@\n@." ;
assert false assert false
else st else st
@ -127,7 +128,7 @@ let strip_special_chars b =
let s5 = replace s4 ')' 'B' in let s5 = replace s4 ')' 'B' in
let s6 = replace s5 '+' 'P' in let s6 = replace s5 '+' 'P' in
let s7 = replace s6 '-' 'M' in let s7 = replace s6 '-' 'M' in
s7 Bytes.to_string s7
let rec strexp_to_string pe coo f se = let rec strexp_to_string pe coo f se =
@ -302,7 +303,7 @@ let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list
| Dotdllseg (_, e', _, _, _, _, _, _) -> | Dotdllseg (_, e', _, _, _, _, _, _) ->
Exp.equal e e' Exp.equal e e'
| _ -> | _ ->
false) false )
allocated_nodes allocated_nodes
| _ -> | _ ->
false false
@ -592,7 +593,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
mk_link k mk_link k
(mk_coordinate (n + 1) lambda) (mk_coordinate (n + 1) lambda)
(strip_special_chars lab_src) (mk_coordinate m lambda) (strip_special_chars lab_src) (mk_coordinate m lambda)
(strip_special_chars lab_trg)) (strip_special_chars lab_trg) )
target_list target_list
in in
let links_from_elements = List.concat_map ~f:ff (n :: nl) in let links_from_elements = List.concat_map ~f:ff (n :: nl) in
@ -619,7 +620,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
let ff n = let ff n =
List.map List.map
~f:(fun (k, lab_src, m, lab_trg) -> ~f:(fun (k, lab_src, m, lab_trg) ->
mk_link k (mk_coordinate n lambda) lab_src (mk_coordinate m lambda) lab_trg) mk_link k (mk_coordinate n lambda) lab_src (mk_coordinate m lambda) lab_trg )
target_list target_list
in in
let nodes_e = select_nodes_exp_lambda dotnodes e lambda in let nodes_e = select_nodes_exp_lambda dotnodes e lambda in
@ -654,7 +655,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
List.map List.map
~f:(fun (k, m, lab_target) -> ~f:(fun (k, m, lab_target) ->
mk_link k (mk_coordinate n lambda) "" (mk_coordinate m lambda) mk_link k (mk_coordinate n lambda) "" (mk_coordinate m lambda)
(strip_special_chars lab_target)) (strip_special_chars lab_target) )
target_list target_list
in in
let ll = List.concat_map ~f:ff nl in let ll = List.concat_map ~f:ff nl in
@ -779,7 +780,7 @@ let filter_useless_spec_dollar_box (nodes: dotty_node list) (links: link list) =
let remove_node n ns = let remove_node n ns =
List.filter List.filter
~f:(fun n' -> ~f:(fun n' ->
match n' with Dotpointsto _ -> get_coordinate_id n' <> get_coordinate_id n | _ -> true) match n' with Dotpointsto _ -> get_coordinate_id n' <> get_coordinate_id n | _ -> true )
ns ns
in in
let rec boxes_pointed_by n lns = let rec boxes_pointed_by n lns =
@ -1065,7 +1066,7 @@ let pp_dotty_one_spec f pre posts =
for j = 1 to 4 do for j = 1 to 4 do
F.fprintf f " inv_%i%i%i%i -> state_pi_%i [style=invis]@\n" !spec_counter j j j F.fprintf f " inv_%i%i%i%i -> state_pi_%i [style=invis]@\n" !spec_counter j j j
!target_invisible_arrow_pre !target_invisible_arrow_pre
done) done )
posts ; posts ;
F.fprintf f "@\n } @\n" F.fprintf f "@\n } @\n"
@ -1082,7 +1083,7 @@ let pp_dotty_prop_list_in_path f plist prev_n curr_n =
List.iter List.iter
~f:(fun po -> ~f:(fun po ->
incr proposition_counter ; incr proposition_counter ;
pp_dotty f Generic_proposition po None) pp_dotty f Generic_proposition po None )
plist ; plist ;
if prev_n <> -1 then F.fprintf f "@\n state%iN ->state%iN@\n" prev_n curr_n ; if prev_n <> -1 then F.fprintf f "@\n state%iN ->state%iN@\n" prev_n curr_n ;
F.fprintf f "@\n } @\n" F.fprintf f "@\n } @\n"
@ -1164,7 +1165,7 @@ let pp_etlist byvals fmt etl =
let byval_mark = let byval_mark =
if is_ptr && List.mem byvals index ~equal:Int.equal then "(byval)" else "" if is_ptr && List.mem byvals index ~equal:Int.equal then "(byval)" else ""
in in
Format.fprintf fmt " %a:%a%s" Mangled.pp id (Typ.pp_full Pp.text) ty byval_mark) Format.fprintf fmt " %a:%a%s" Mangled.pp id (Typ.pp_full Pp.text) ty byval_mark )
etl etl
@ -1445,7 +1446,7 @@ let make_set_dangling_nodes allocated_nodes (sigma: Sil.hpred list) =
| VH_pointsto (_, e', _, _) | VH_lseg (_, e', _, _) | VH_dllseg (_, e', _, _, _, _) -> | VH_pointsto (_, e', _, _) | VH_lseg (_, e', _, _) | VH_dllseg (_, e', _, _, _, _) ->
Exp.equal e e' Exp.equal e e'
| _ -> | _ ->
false) false )
allocated_nodes allocated_nodes
in in
not allocated not allocated
@ -1712,7 +1713,7 @@ let print_specs_xml signature specs loc fmt =
:: List.map :: List.map
~f:(fun (po, _) -> ~f:(fun (po, _) ->
jj := !jj + 1 ; jj := !jj + 1 ;
prop_to_xml (add_stack_to_prop po) "postcondition" !jj) prop_to_xml (add_stack_to_prop po) "postcondition" !jj )
posts posts
in in
Io_infer.Xml.create_tree "specification" [("id", string_of_int n)] xml_spec Io_infer.Xml.create_tree "specification" [("id", string_of_int n)] xml_spec
@ -1722,7 +1723,7 @@ let print_specs_xml signature specs loc fmt =
List.map List.map
~f:(fun s -> ~f:(fun s ->
j := !j + 1 ; j := !j + 1 ;
do_one_spec (Specs.Jprop.to_prop s.Specs.pre) s.Specs.posts !j) do_one_spec (Specs.Jprop.to_prop s.Specs.pre) s.Specs.posts !j )
specs specs
in in
let xml_specifications = Io_infer.Xml.create_tree "specifications" [] list_of_specs_xml in let xml_specifications = Io_infer.Xml.create_tree "specifications" [] list_of_specs_xml in
@ -1733,4 +1734,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

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

@ -218,4 +218,3 @@ let iter_files f exe_env =
SourceFile.Set.add fname seen_files_acc ) SourceFile.Set.add fname seen_files_acc )
in in
ignore (Typ.Procname.Hash.fold do_file exe_env.proc_map SourceFile.Set.empty) ignore (Typ.Procname.Hash.fold do_file exe_env.proc_map SourceFile.Set.empty)

@ -38,7 +38,8 @@ let setup () =
if not if not
( Driver.(equal_mode driver_mode Analyze) ( Driver.(equal_mode driver_mode Analyze)
|| ||
Config.(buck || continue_capture || infer_is_clang || infer_is_javac || reactive_mode) ) Config.(buck || continue_capture || infer_is_clang || infer_is_javac || reactive_mode)
)
then ResultsDir.remove_results_dir () ; then ResultsDir.remove_results_dir () ;
ResultsDir.create_results_dir () ResultsDir.create_results_dir ()
| Explore -> | Explore ->

@ -41,7 +41,7 @@ let is_matching patterns source_file =
let path = SourceFile.to_rel_path source_file in let path = SourceFile.to_rel_path source_file in
List.exists List.exists
~f:(fun pattern -> ~f:(fun pattern ->
try Int.equal (Str.search_forward pattern path 0) 0 with Not_found -> false) try Int.equal (Str.search_forward pattern path 0) 0 with Not_found -> false )
patterns patterns
@ -83,7 +83,6 @@ module FileContainsStringMatcher = struct
source_map := SourceFile.Map.add source_file pattern_found !source_map ; source_map := SourceFile.Map.add source_file pattern_found !source_map ;
pattern_found pattern_found
with Sys_error _ -> false with Sys_error _ -> false
end end
type method_pattern = type method_pattern =
@ -106,7 +105,7 @@ module FileOrProcMatcher = struct
List.fold List.fold
~f:(fun map pattern -> ~f:(fun map pattern ->
let previous = try String.Map.find_exn map pattern.class_name with Not_found -> [] in let previous = try String.Map.find_exn map pattern.class_name with Not_found -> [] in
String.Map.add ~key:pattern.class_name ~data:(pattern :: previous) map) String.Map.set ~key:pattern.class_name ~data:(pattern :: previous) map )
~init:String.Map.empty m_patterns ~init:String.Map.empty m_patterns
in in
let do_java pname_java = let do_java pname_java =
@ -116,7 +115,7 @@ module FileOrProcMatcher = struct
let class_patterns = String.Map.find_exn pattern_map class_name in let class_patterns = String.Map.find_exn pattern_map class_name in
List.exists List.exists
~f:(fun p -> ~f:(fun p ->
match p.method_name with None -> true | Some m -> String.equal m method_name) match p.method_name with None -> true | Some m -> String.equal m method_name )
class_patterns class_patterns
with Not_found -> false with Not_found -> false
in in
@ -171,7 +170,6 @@ module FileOrProcMatcher = struct
Format.fprintf fmt "Source contains (%s) {@\n%a}@\n" Format.fprintf fmt "Source contains (%s) {@\n%a}@\n"
(Config.string_of_language language) (Config.string_of_language language)
pp_source_contains sc pp_source_contains sc
end end
(* of module FileOrProcMatcher *) (* of module FileOrProcMatcher *)
@ -186,7 +184,6 @@ module OverridesMatcher = struct
L.(die UserError) "Expecting method pattern" L.(die UserError) "Expecting method pattern"
in in
List.exists ~f:is_matching patterns List.exists ~f:is_matching patterns
end end
let patterns_of_json_with_key (json_key, json) = let patterns_of_json_with_key (json_key, json) =
@ -369,6 +366,5 @@ let test () =
let matching = matching_analyzers source_file in let matching = matching_analyzers source_file in
if matching <> [] then if matching <> [] then
let matching_s = String.concat ~sep:", " (List.map ~f:fst matching) in let matching_s = String.concat ~sep:", " (List.map ~f:fst matching) in
L.result "%s -> {%s}@." (SourceFile.to_rel_path source_file) matching_s) L.result "%s -> {%s}@." (SourceFile.to_rel_path source_file) matching_s )
(Sys.getcwd ()) (Sys.getcwd ())

@ -62,7 +62,6 @@ module NodeVisitSet = Caml.Set.Make (struct
| _ -> | _ ->
compare_number_of_visits x1 x2 compare_number_of_visits x1 x2
else compare_ids x1.node x2.node else compare_ids x1.node x2.node
end) end)
(** Table for the results of the join operation on nodes. *) (** Table for the results of the join operation on nodes. *)
@ -122,7 +121,6 @@ module Worklist = struct
with Not_found -> with Not_found ->
L.internal_error "@\n...Work list is empty! Impossible to remove edge...@\n" ; L.internal_error "@\n...Work list is empty! Impossible to remove edge...@\n" ;
assert false assert false
end end
(* =============== END of module Worklist =============== *) (* =============== END of module Worklist =============== *)
@ -325,8 +323,8 @@ let do_symexec_join proc_cfg tenv wl curr_node (edgeset_todo: Paths.PathSet.t) =
State.set_path path None ; State.set_path path None ;
propagate wl pname ~is_exception:false propagate wl pname ~is_exception:false
(Paths.PathSet.from_renamed_list [(prop, path)]) (Paths.PathSet.from_renamed_list [(prop, path)])
node) node )
new_dset') new_dset' )
succ_nodes succ_nodes
@ -575,7 +573,7 @@ let report_context_leaks pname sigma tenv =
Errdesc.explain_context_leak pname (Typ.mk (Tstruct name)) fld_name leak_path Errdesc.explain_context_leak pname (Typ.mk (Tstruct name)) fld_name leak_path
in in
let exn = Exceptions.Context_leak (err_desc, __POS__) in let exn = Exceptions.Context_leak (err_desc, __POS__) in
Reporting.log_error_deprecated pname exn) Reporting.log_error_deprecated pname exn )
context_exps context_exps
in in
(* get the set of pointed-to expressions of type T <: Context *) (* get the set of pointed-to expressions of type T <: Context *)
@ -588,7 +586,7 @@ let report_context_leaks pname sigma tenv =
&& not (AndroidFramework.is_application tenv name) -> && not (AndroidFramework.is_application tenv name) ->
(exp, name) :: exps (exp, name) :: exps
| _ -> | _ ->
exps) exps )
~init:[] sigma ~init:[] sigma
in in
List.iter List.iter
@ -596,7 +594,7 @@ let report_context_leaks pname sigma tenv =
| Sil.Hpointsto (Exp.Lvar pv, Sil.Estruct (static_flds, _), _) when Pvar.is_global pv -> | Sil.Hpointsto (Exp.Lvar pv, Sil.Estruct (static_flds, _), _) when Pvar.is_global pv ->
List.iter List.iter
~f:(fun (f_name, f_strexp) -> ~f:(fun (f_name, f_strexp) ->
check_reachable_context_from_fld (f_name, f_strexp) context_exps) check_reachable_context_from_fld (f_name, f_strexp) context_exps )
static_flds static_flds
| _ -> | _ ->
()) ())
@ -733,7 +731,7 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * Specs.Visitedset
(fun prop -> (fun prop ->
Attribute.remove_resource tenv Racquire (Rmemory Mobjc) Attribute.remove_resource tenv Racquire (Rmemory Mobjc)
(Attribute.remove_resource tenv Racquire (Rmemory Mmalloc) (Attribute.remove_resource tenv Racquire (Rmemory Mmalloc)
(Attribute.remove_resource tenv Racquire Rfile prop))) (Attribute.remove_resource tenv Racquire Rfile prop)) )
pathset pathset
else pathset else pathset
| _ -> | _ ->
@ -1135,7 +1133,7 @@ let update_specs tenv prev_summary phase (new_specs: Specs.NormSpec.t list)
(List.fold (List.fold
~f:(fun map spec -> ~f:(fun map spec ->
SpecMap.add spec.Specs.pre SpecMap.add spec.Specs.pre
(Paths.PathSet.from_renamed_list spec.Specs.posts, spec.Specs.visited) map) (Paths.PathSet.from_renamed_list spec.Specs.posts, spec.Specs.visited) map )
~init:SpecMap.empty old_specs) ~init:SpecMap.empty old_specs)
in in
let re_exe_filter old_spec = let re_exe_filter old_spec =
@ -1230,7 +1228,8 @@ let transition_footprint_re_exe tenv proc_name joined_pres =
let specs = let specs =
List.map List.map
~f:(fun jp -> ~f:(fun jp ->
Specs.spec_normalize tenv {Specs.pre= jp; posts= []; visited= Specs.Visitedset.empty}) Specs.spec_normalize tenv {Specs.pre= jp; posts= []; visited= Specs.Visitedset.empty}
)
joined_pres joined_pres
in in
let payload = {summary.Specs.payload with Specs.preposts= Some specs} in let payload = {summary.Specs.payload with Specs.preposts= Some specs} in

@ -936,4 +936,3 @@ let hpara_dll_create tenv corres sigma1 root1 blink1 flink1 =
; Sil.body_dll= body } ; Sil.body_dll= body }
in in
(hpara_dll, es_shared) (hpara_dll, es_shared)

@ -65,7 +65,7 @@ let rec slink ~stats ~skiplevels src dst =
Array.iter Array.iter
~f:(fun item -> ~f:(fun item ->
slink ~stats ~skiplevels:(skiplevels - 1) (Filename.concat src item) slink ~stats ~skiplevels:(skiplevels - 1) (Filename.concat src item)
(Filename.concat dst item)) (Filename.concat dst item) )
items ) items )
else if skiplevels > 0 then () else if skiplevels > 0 then ()
else create_link ~stats src dst else create_link ~stats src dst
@ -92,7 +92,7 @@ let should_link ~target ~target_results_dir ~stats infer_out_src infer_out_dst =
~f:(fun file -> ~f:(fun file ->
let file_path = Filename.concat captured_file file in let file_path = Filename.concat captured_file file in
Sys.file_exists file_path = `Yes Sys.file_exists file_path = `Yes
&& (not check_timestamp_of_symlinks || symlink_up_to_date file_path)) && (not check_timestamp_of_symlinks || symlink_up_to_date file_path) )
contents contents
else true else true
in in
@ -129,8 +129,8 @@ let process_merge_file deps_file =
match Str.split_delim (Str.regexp (Str.quote "\t")) line with match Str.split_delim (Str.regexp (Str.quote "\t")) line with
| target :: _ :: target_results_dir :: _ -> | target :: _ :: target_results_dir :: _ ->
let infer_out_src = let infer_out_src =
if Filename.is_relative target_results_dir then Filename.dirname (buck_out ()) if Filename.is_relative target_results_dir then
^/ target_results_dir Filename.dirname (buck_out ()) ^/ target_results_dir
else target_results_dir else target_results_dir
in in
let skiplevels = 2 in let skiplevels = 2 in
@ -156,4 +156,3 @@ let merge_captured_targets () =
MergeResults.merge_buck_flavors_results infer_deps_file ; MergeResults.merge_buck_flavors_results infer_deps_file ;
process_merge_file infer_deps_file ; process_merge_file infer_deps_file ;
L.progress "Merging captured Buck targets took %a@\n%!" Mtime.Span.pp (Mtime_clock.count time0) L.progress "Merging captured Buck targets took %a@\n%!" Mtime.Span.pp (Mtime_clock.count time0)

@ -211,4 +211,3 @@ let analyze_proc_name : Procdesc.t -> Typ.Procname.t -> Specs.summary option =
(** Find a proc desc for the procedure, perhaps loading it from disk. *) (** Find a proc desc for the procedure, perhaps loading it from disk. *)
let get_proc_desc callee_pname = let get_proc_desc callee_pname =
match !callbacks_ref with Some callbacks -> callbacks.get_proc_desc callee_pname | None -> None match !callbacks_ref with Some callbacks -> callbacks.get_proc_desc callee_pname | None -> None

@ -253,7 +253,6 @@ end = struct
let stats1 = compute_stats do_calls f path ; get_stats path in let stats1 = compute_stats do_calls f path ; get_stats path in
stats.max_length <- stats1.max_length ; stats.max_length <- stats1.max_length ;
stats.linear_num <- stats1.linear_num stats.linear_num <- stats1.linear_num
end end
(* End of module Invariant *) (* End of module Invariant *)
@ -376,7 +375,7 @@ end = struct
(fun node num -> (fun node num ->
if num > !max_rep_num then ( if num > !max_rep_num then (
max_rep_node := node ; max_rep_node := node ;
max_rep_num := num )) max_rep_num := num ) )
!map ; !map ;
(!max_rep_node, !max_rep_num) (!max_rep_node, !max_rep_num)
@ -480,7 +479,7 @@ end = struct
let definition_descr = let definition_descr =
Format.sprintf "Definition of %s" (Typ.Procname.to_simplified_string pname) Format.sprintf "Definition of %s" (Typ.Procname.to_simplified_string pname)
in in
trace := Errlog.make_trace_element (level + 1) loc definition_descr [] :: !trace) trace := Errlog.make_trace_element (level + 1) loc definition_descr [] :: !trace )
loc_opt loc_opt
| _, Some curr_node | _, Some curr_node
-> ( -> (
@ -548,7 +547,6 @@ end = struct
in in
let relevant lt = lt.Errlog.lt_node_tags <> [] in let relevant lt = lt.Errlog.lt_node_tags <> [] in
IList.remove_irrelevant_duplicates compare relevant (List.rev !trace) IList.remove_irrelevant_duplicates compare relevant (List.rev !trace)
end end
(* =============== END of the Path module ===============*) (* =============== END of the Path module ===============*)
@ -740,7 +738,6 @@ end = struct
(** It's the caller's resposibility to ensure that Prop.prop_rename_primed_footprint_vars was called on the list *) (** It's the caller's resposibility to ensure that Prop.prop_rename_primed_footprint_vars was called on the list *)
let from_renamed_list (pl: ('a Prop.t * Path.t) list) : t = let from_renamed_list (pl: ('a Prop.t * Path.t) list) : t =
List.fold ~f:(fun ps (p, pa) -> add_renamed_prop p pa ps) ~init:empty pl List.fold ~f:(fun ps (p, pa) -> add_renamed_prop p pa ps) ~init:empty pl
end end
(* =============== END of the PathSet module ===============*) (* =============== END of the PathSet module ===============*)

@ -108,7 +108,6 @@ module NullifyTransferFunctions = struct
"Should not add nullify instructions before running nullify analysis!" "Should not add nullify instructions before running nullify analysis!"
in in
if is_last_instr_in_node instr node then postprocess astate' node extras else astate' if is_last_instr_in_node instr node then postprocess astate' node extras else astate'
end end
module NullifyAnalysis = module NullifyAnalysis =
@ -162,13 +161,13 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
| Exp.Var id -> | Exp.Var id ->
(pvars_acc, id :: ids_acc) (pvars_acc, id :: ids_acc)
| _ -> | _ ->
(pvars_acc, ids_acc)) (pvars_acc, ids_acc) )
to_nullify ([], []) to_nullify ([], [])
in in
node_add_removetmps_instructions node ids_to_remove ; node_add_removetmps_instructions node ids_to_remove ;
node_add_nullify_instructions node pvars_to_nullify node_add_nullify_instructions node pvars_to_nullify
| None -> | None ->
()) () )
(ProcCfg.Exceptional.nodes nullify_proc_cfg) ; (ProcCfg.Exceptional.nodes nullify_proc_cfg) ;
(* nullify all address taken variables *) (* nullify all address taken variables *)
if not (AddressTaken.Domain.is_empty address_taken_vars) then if not (AddressTaken.Domain.is_empty address_taken_vars) then
@ -199,4 +198,3 @@ let do_abstraction pdesc =
let do_preanalysis pdesc tenv = let do_preanalysis pdesc tenv =
if not (Procdesc.did_preanalysis pdesc) then ( do_liveness pdesc tenv ; do_abstraction pdesc ) if not (Procdesc.did_preanalysis pdesc) then ( do_liveness pdesc tenv ; do_abstraction pdesc )

@ -151,7 +151,6 @@ end = struct
let fd = Hashtbl.find log_files (node_fname, source) in let fd = Hashtbl.find log_files (node_fname, source) in
Unix.close fd ; Unix.close fd ;
curr_html_formatter := F.std_formatter curr_html_formatter := F.std_formatter
end end
(* =============== END of module NodesHtml =============== *) (* =============== END of module NodesHtml =============== *)
@ -380,7 +379,7 @@ let write_proc_html pdesc =
~succs:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_succs n) :> int list) ~succs:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_succs n) :> int list)
~exn:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_exn n) :> int list) ~exn:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_exn n) :> int list)
~isvisited:(is_visited n) ~isproof:false fmt ~isvisited:(is_visited n) ~isproof:false fmt
(Procdesc.Node.get_id n :> int)) (Procdesc.Node.get_id n :> int) )
nodes ; nodes ;
match Specs.get_summary pname with match Specs.get_summary pname with
| None -> | None ->
@ -483,7 +482,7 @@ let write_html_file linereader filename procs =
~succs:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_succs n) :> int list) ~succs:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_succs n) :> int list)
~exn:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_exn n) :> int list) ~exn:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_exn n) :> int list)
~isvisited:(is_visited n) ~isproof fmt ~isvisited:(is_visited n) ~isproof fmt
(Procdesc.Node.get_id n :> int)) (Procdesc.Node.get_id n :> int) )
nodes_at_linenum ; nodes_at_linenum ;
List.iter List.iter
~f:(fun n -> ~f:(fun n ->
@ -502,7 +501,7 @@ let write_html_file linereader filename procs =
in in
Io_infer.Html.pp_proc_link [fname_encoding] proc_name fmt label Io_infer.Html.pp_proc_link [fname_encoding] proc_name fmt label
| _ -> | _ ->
()) () )
nodes_at_linenum ; nodes_at_linenum ;
List.iter List.iter
~f:(fun err_string -> F.fprintf fmt "%s" (create_err_message err_string)) ~f:(fun err_string -> F.fprintf fmt "%s" (create_err_message err_string))
@ -557,5 +556,5 @@ let write_all_html_files cluster =
in in
SourceFile.Set.iter SourceFile.Set.iter
(fun file -> write_html_file linereader file (Cfg.get_all_procs cfg)) (fun file -> write_html_file linereader file (Cfg.get_all_procs cfg))
source_files_in_cfg) source_files_in_cfg )
exe_env exe_env

@ -1318,8 +1318,7 @@ module Normalize = struct
in in
let handle_unary_negation (e1: Exp.t) (e2: Exp.t) = let handle_unary_negation (e1: Exp.t) (e2: Exp.t) =
match (e1, e2) with match (e1, e2) with
| UnOp (LNot, e1', _), Const Cint i | (UnOp (LNot, e1', _), Const Cint i | Const Cint i, UnOp (LNot, e1', _))
| Const Cint i, UnOp (LNot, e1', _)
when IntLit.iszero i -> when IntLit.iszero i ->
(e1', Exp.zero, true) (e1', Exp.zero, true)
| _ -> | _ ->
@ -1389,7 +1388,7 @@ module Normalize = struct
List.map List.map
~f:(fun (idx, cnt) -> ~f:(fun (idx, cnt) ->
let idx' = exp_normalize tenv sub idx in let idx' = exp_normalize tenv sub idx in
(idx', strexp_normalize tenv sub cnt)) (idx', strexp_normalize tenv sub cnt) )
idx_cnts idx_cnts
in in
let idx_cnts'' = List.sort ~cmp:[%compare : Exp.t * Sil.strexp] idx_cnts' in let idx_cnts'' = List.sort ~cmp:[%compare : Exp.t * Sil.strexp] idx_cnts' in
@ -1578,7 +1577,7 @@ module Normalize = struct
~f:(fun (n', e') -> Exp.equal e e' && IntLit.leq n n') ~f:(fun (n', e') -> Exp.equal e e' && IntLit.leq n n')
lt_list_tightened) lt_list_tightened)
| _ -> | _ ->
true) true )
nonineq_list nonineq_list
in in
(ineq_list', nonineq_list') (ineq_list', nonineq_list')
@ -1712,7 +1711,6 @@ module Normalize = struct
let nprop = List.fold ~f:(prop_atom_and tenv) ~init:p0 (get_pure_extended eprop) in let nprop = List.fold ~f:(prop_atom_and tenv) ~init:p0 (get_pure_extended eprop) in
unsafe_cast_to_normal unsafe_cast_to_normal
(footprint_normalize tenv (set nprop ~pi_fp:eprop.pi_fp ~sigma_fp:eprop.sigma_fp)) (footprint_normalize tenv (set nprop ~pi_fp:eprop.pi_fp ~sigma_fp:eprop.sigma_fp))
end end
(* End of module Normalize *) (* End of module Normalize *)
@ -1730,7 +1728,7 @@ let lexp_normalize_prop tenv p lexp =
let noffsets = let noffsets =
List.map List.map
~f:(fun (n: Sil.offset) -> ~f:(fun (n: Sil.offset) ->
match n with Off_fld _ -> n | Off_index e -> Sil.Off_index (exp_normalize_prop tenv p e)) match n with Off_fld _ -> n | Off_index e -> Sil.Off_index (exp_normalize_prop tenv p e) )
offsets offsets
in in
Sil.exp_add_offsets nroot noffsets Sil.exp_add_offsets nroot noffsets
@ -2668,7 +2666,6 @@ end = struct
let prop_chain_size p = let prop_chain_size p =
let fp_size = pi_size p.pi_fp + sigma_size p.sigma_fp in let fp_size = pi_size p.pi_fp + sigma_size p.sigma_fp in
pi_size p.pi + sigma_size p.sigma + fp_size pi_size p.pi + sigma_size p.sigma + fp_size
end end
(*** END of module Metrics ***) (*** END of module Metrics ***)
@ -2729,7 +2726,6 @@ module CategorizePreconditions = struct
OnlyAllocation OnlyAllocation
| _ :: _, [], [] -> | _ :: _, [], [] ->
DataConstraints DataConstraints
end end
(* Export for interface *) (* Export for interface *)

@ -90,7 +90,8 @@ let get_subl footprint_part g = if footprint_part then [] else Sil.sub_to_list g
let edge_from_source g n footprint_part is_hpred = let edge_from_source g n footprint_part is_hpred =
let edges = let edges =
if is_hpred then List.map ~f:(fun hpred -> Ehpred hpred) (get_sigma footprint_part g) if is_hpred then List.map ~f:(fun hpred -> Ehpred hpred) (get_sigma footprint_part g)
else List.map ~f:(fun a -> Eatom a) (get_pi footprint_part g) else
List.map ~f:(fun a -> Eatom a) (get_pi footprint_part g)
@ List.map ~f:(fun entry -> Esub_entry entry) (get_subl footprint_part g) @ List.map ~f:(fun entry -> Esub_entry entry) (get_subl footprint_part g)
in in
let starts_from hpred = let starts_from hpred =

@ -102,4 +102,3 @@ let pp pe prop f pset =
let d p ps = let d p ps =
let plist = to_proplist ps in let plist = to_proplist ps in
Propgraph.d_proplist p plist Propgraph.d_proplist p plist

@ -194,7 +194,6 @@ end = struct
let saturate constraints = let saturate constraints =
let constraints_cleaned = sort_then_remove_redundancy constraints in let constraints_cleaned = sort_then_remove_redundancy constraints in
saturate_ constraints_cleaned constraints_cleaned saturate_ constraints_cleaned constraints_cleaned
end end
(** Return true if the two types have sizes which can be compared *) (** Return true if the two types have sizes which can be compared *)
@ -460,7 +459,7 @@ end = struct
List.iter List.iter
~f:(fun (idx, se) -> ~f:(fun (idx, se) ->
add_lt_minus1_e idx ; add_lt_minus1_e idx ;
strexp_extract (se, elt_t)) strexp_extract (se, elt_t) )
isel isel
in in
let hpred_extract = function let hpred_extract = function
@ -604,7 +603,6 @@ end = struct
List.exists ~f:inconsistent_neq neqs || List.exists ~f:inconsistent_leq leqs List.exists ~f:inconsistent_neq neqs || List.exists ~f:inconsistent_leq leqs
|| List.exists ~f:inconsistent_lt lts || List.exists ~f:inconsistent_lt lts
(* (*
(** Pretty print inequalities and disequalities *) (** Pretty print inequalities and disequalities *)
let pp pe fmt { leqs = leqs; lts = lts; neqs = neqs } = let pp pe fmt { leqs = leqs; lts = lts; neqs = neqs } =
@ -871,7 +869,7 @@ let get_smt_key a p =
let fmt_tmp = F.formatter_of_out_channel outc_tmp in let fmt_tmp = F.formatter_of_out_channel outc_tmp in
let () = F.fprintf fmt_tmp "%a%a" (Sil.pp_atom Pp.text) a (Prop.pp_prop Pp.text) p in let () = F.fprintf fmt_tmp "%a%a" (Sil.pp_atom Pp.text) a (Prop.pp_prop Pp.text) p in
Out_channel.close outc_tmp ; Out_channel.close outc_tmp ;
Digest.to_hex (Digest.file tmp_filename) Caml.Digest.to_hex (Caml.Digest.file tmp_filename)
(** Check whether [prop |- a]. False means dont know. *) (** Check whether [prop |- a]. False means dont know. *)
@ -1323,7 +1321,6 @@ end = struct
d_inner () ; d_inner () ;
L.d_strln " returning FALSE" ; L.d_strln " returning FALSE" ;
L.d_ln () L.d_ln ()
end end
let d_impl (s1, s2) = ProverState.d_implication (`Exp s1, `Exp s2) let d_impl (s1, s2) = ProverState.d_implication (`Exp s1, `Exp s2)
@ -1939,7 +1936,6 @@ module Subtyping_check = struct
| _ -> | _ ->
(* don't know, consider both possibilities *) (* don't know, consider both possibilities *)
(Some texp1, Some texp1) (Some texp1, Some texp1)
end end
let cast_exception tenv texp1 texp2 e1 subs = let cast_exception tenv texp1 texp2 e1 subs =
@ -2774,7 +2770,6 @@ let find_minimum_pure_cover tenv cases =
let shrink cases = if List.length cases > 2 then shrink_ [] cases else cases in let shrink cases = if List.length cases > 2 then shrink_ [] cases else cases in
try Some (shrink (grow [] cases)) with NO_COVER -> None try Some (shrink (grow [] cases)) with NO_COVER -> None
(* (*
(** Check [prop |- e1<e2]. Result [false] means "don't know". *) (** Check [prop |- e1<e2]. Result [false] means "don't know". *)
let check_lt prop e1 e2 = let check_lt prop e1 e2 =

@ -367,7 +367,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
let isel_new = list_rev_and_concat isel_seen_rev ((i, se') :: isel_unseen) in let isel_new = list_rev_and_concat isel_seen_rev ((i, se') :: isel_unseen) in
let array_new = Sil.Earray (array_len, isel_new, inst_arr) in let array_new = Sil.Earray (array_len, isel_new, inst_arr) in
let typ_new = Typ.mk ~default:typ_array (Tarray (typ', typ_array_len, None)) in let typ_new = Typ.mk ~default:typ_array (Tarray (typ', typ_array_len, None)) in
(atoms_new, array_new, typ_new) :: acc') (atoms_new, array_new, typ_new) :: acc' )
~init:[] atoms_se_typ_list ~init:[] atoms_se_typ_list
in in
let acc_new = atoms_se_typ_list' :: acc in let acc_new = atoms_se_typ_list' :: acc in
@ -444,7 +444,7 @@ let strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se t
in in
List.map List.map
~f:(fun (atoms', se', typ') -> ~f:(fun (atoms', se', typ') ->
(laundry_atoms @ atoms', se', Exp.Sizeof {sizeof_data with typ= typ'})) (laundry_atoms @ atoms', se', Exp.Sizeof {sizeof_data with typ= typ'}) )
atoms_se_typ_list_filtered atoms_se_typ_list_filtered
@ -667,7 +667,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
let iter' = let iter' =
List.fold ~f:(Prop.prop_iter_add_atom !Config.footprint) ~init:iter atoms List.fold ~f:(Prop.prop_iter_add_atom !Config.footprint) ~init:iter atoms
in in
Prop.prop_iter_replace_footprint_sigma iter' fp_sigma) Prop.prop_iter_replace_footprint_sigma iter' fp_sigma )
iter_atoms_fp_sigma_list iter_atoms_fp_sigma_list
in in
let res_prop_list = List.map ~f:(Prop.prop_iter_to_prop tenv) res_iter_list in let res_prop_list = List.map ~f:(Prop.prop_iter_to_prop tenv) res_iter_list in
@ -888,7 +888,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
&& Pvar.is_this pvar -> && Pvar.is_this pvar ->
Some (rhs_exp, typ) Some (rhs_exp, typ)
| _ -> | _ ->
None) None )
sigma sigma
in in
(* warn if the access to [lexp] is not protected by the [guarded_by_fld_str] lock *) (* warn if the access to [lexp] is not protected by the [guarded_by_fld_str] lock *)
@ -964,7 +964,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
| Sil.Eexp (rhs_exp, _) -> | Sil.Eexp (rhs_exp, _) ->
Exp.equal exp rhs_exp && not (Typ.Fieldname.equal fld accessed_fld) Exp.equal exp rhs_exp && not (Typ.Fieldname.equal fld accessed_fld)
| _ -> | _ ->
false) false )
flds flds
| _ -> | _ ->
false) false)
@ -1775,4 +1775,3 @@ let rearrange ?(report_deref_errors= true) pdesc tenv lexp typ prop loc
raise (Exceptions.Symexec_memory_error __POS__) ) raise (Exceptions.Symexec_memory_error __POS__) )
| Some iter -> | Some iter ->
iter_rearrange pname tenv nlexp typ prop' iter inst iter_rearrange pname tenv nlexp typ prop' iter inst

@ -11,7 +11,7 @@ open! IStd
module L = Logging module L = Logging
type log_t = type log_t =
?loc:Location.t -> ?node_id:int * Digest.t -> ?session:int -> ?ltr:Errlog.loc_trace ?loc:Location.t -> ?node_id:int * Caml.Digest.t -> ?session:int -> ?ltr:Errlog.loc_trace
-> ?linters_def_file:string -> ?doc_url:string -> ?access:string -> exn -> unit -> ?linters_def_file:string -> ?doc_url:string -> ?access:string -> exn -> unit
type log_issue_from_errlog = Errlog.t -> log_t type log_issue_from_errlog = Errlog.t -> log_t
@ -24,7 +24,7 @@ let log_issue_from_errlog err_kind err_log ?loc ?node_id ?session ?ltr ?linters_
let node_id = let node_id =
match node_id with match node_id with
| None -> | None ->
(State.get_node_id_key () :> int * Digest.t) (State.get_node_id_key () :> int * Caml.Digest.t)
| Some node_id -> | Some node_id ->
node_id node_id
in in
@ -88,4 +88,3 @@ let log_warning_deprecated ?(store_summary= false) =
let log_info_deprecated ?(store_summary= false) = let log_info_deprecated ?(store_summary= false) =
log_issue_deprecated ~store_summary Exceptions.Kinfo log_issue_deprecated ~store_summary Exceptions.Kinfo

@ -12,7 +12,7 @@ open! IStd
(** Type of functions to report issues to the error_log in a spec. *) (** Type of functions to report issues to the error_log in a spec. *)
type log_t = type log_t =
?loc:Location.t -> ?node_id:int * Digest.t -> ?session:int -> ?ltr:Errlog.loc_trace ?loc:Location.t -> ?node_id:int * Caml.Digest.t -> ?session:int -> ?ltr:Errlog.loc_trace
-> ?linters_def_file:string -> ?doc_url:string -> ?access:string -> exn -> unit -> ?linters_def_file:string -> ?doc_url:string -> ?access:string -> exn -> unit
type log_issue_from_errlog = Errlog.t -> log_t type log_issue_from_errlog = Errlog.t -> log_t

@ -135,7 +135,6 @@ module Jprop = struct
| Joined (n, p, jp1, jp2) -> | Joined (n, p, jp1, jp2) ->
Joined (n, f p, map f jp1, map f jp2) Joined (n, f p, map f jp1, map f jp2)
(* (*
let rec jprop_sub sub = function let rec jprop_sub sub = function
| Prop (n, p) -> Prop (n, Prop.prop_sub sub p) | Prop (n, p) -> Prop (n, Prop.prop_sub sub p)
@ -232,7 +231,6 @@ end = struct
let erase_join_info_pre tenv spec = let erase_join_info_pre tenv spec =
let spec' = {spec with pre= Jprop.Prop (1, Jprop.to_prop spec.pre)} in let spec' = {spec with pre= Jprop.Prop (1, Jprop.to_prop spec.pre)} in
normalize tenv spec' normalize tenv spec'
end end
(** Convert spec into normal form w.r.t. variable renaming *) (** Convert spec into normal form w.r.t. variable renaming *)
@ -311,7 +309,6 @@ module CallStats = struct
in in
List.iter ~f:(fun (x, tr) -> f x tr) sorted_elems List.iter ~f:(fun (x, tr) -> f x tr) sorted_elems
(* (*
let pp fmt t = let pp fmt t =
let do_call (pname, loc) tr = let do_call (pname, loc) tr =
@ -443,13 +440,13 @@ let pp_specs pe fmt specs =
List.iter List.iter
~f:(fun spec -> ~f:(fun spec ->
incr cnt ; incr cnt ;
F.fprintf fmt "%a" (pp_spec pe (Some (!cnt, total))) spec) F.fprintf fmt "%a" (pp_spec pe (Some (!cnt, total))) spec )
specs specs
| HTML -> | HTML ->
List.iter List.iter
~f:(fun spec -> ~f:(fun spec ->
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
@ -464,7 +461,7 @@ let get_signature summary =
~f:(fun (p, typ) -> ~f:(fun (p, typ) ->
let pp f = F.fprintf f "%a %a" (Typ.pp_full Pp.text) typ Mangled.pp p in let pp f = F.fprintf f "%a %a" (Typ.pp_full Pp.text) typ Mangled.pp p in
let decl = F.asprintf "%t" pp in let decl = F.asprintf "%t" pp in
s := if String.equal !s "" then decl else !s ^ ", " ^ decl) s := if String.equal !s "" then decl else !s ^ ", " ^ decl )
(get_formals summary) ; (get_formals summary) ;
let pp f = let pp f =
F.fprintf f "%a %a" (Typ.pp_full Pp.text) (get_ret_type summary) Typ.Procname.pp F.fprintf f "%a %a" (Typ.pp_full Pp.text) (get_ret_type summary) Typ.Procname.pp
@ -579,8 +576,7 @@ let res_dir_specs_filename pname =
(** paths to the .specs file for the given procedure in the current spec libraries *) (** paths to the .specs file for the given procedure in the current spec libraries *)
let specs_library_filenames pname = let specs_library_filenames pname =
List.map List.map
~f:(fun specs_dir -> ~f:(fun specs_dir -> DB.filename_from_string (Filename.concat specs_dir (specs_filename pname)))
DB.filename_from_string (Filename.concat specs_dir (specs_filename pname)))
Config.specs_library Config.specs_library

@ -25,7 +25,7 @@ type failure_stats =
; (* number of node failures (i.e. at least one instruction failure) *) ; (* number of node failures (i.e. at least one instruction failure) *)
mutable node_ok: int mutable node_ok: int
; (* number of node successes (i.e. no instruction failures) *) ; (* number of node successes (i.e. no instruction failures) *)
mutable first_failure: (Location.t * (int * Digest.t) * int * Errlog.loc_trace * exn) option mutable first_failure: (Location.t * (int * Caml.Digest.t) * int * Errlog.loc_trace * exn) option
(* exception at the first failure *) } (* exception at the first failure *) }
module NodeHash = Procdesc.NodeHash module NodeHash = Procdesc.NodeHash
@ -310,7 +310,7 @@ let mark_instr_ok () =
let mark_instr_fail exn = let mark_instr_fail exn =
let loc = get_loc () in let loc = get_loc () in
let key = (get_node_id_key () :> int * Digest.t) in let key = (get_node_id_key () :> int * Caml.Digest.t) in
let session = get_session () in let session = get_session () in
let loc_trace = get_loc_trace () in let loc_trace = get_loc_trace () in
let fs = get_failure_stats (get_node ()) in let fs = get_failure_stats (get_node ()) in
@ -320,7 +320,7 @@ let mark_instr_fail exn =
type log_issue = type log_issue =
?store_summary:bool -> Typ.Procname.t -> ?loc:Location.t -> ?node_id:int * Digest.t ?store_summary:bool -> Typ.Procname.t -> ?loc:Location.t -> ?node_id:int * Caml.Digest.t
-> ?session:int -> ?ltr:Errlog.loc_trace -> ?linters_def_file:string -> ?doc_url:string -> ?session:int -> ?ltr:Errlog.loc_trace -> ?linters_def_file:string -> ?doc_url:string
-> ?access:string -> exn -> unit -> ?access:string -> exn -> unit

@ -42,7 +42,7 @@ val get_node : unit -> Procdesc.Node.t
val get_node_id : unit -> Procdesc.Node.id val get_node_id : unit -> Procdesc.Node.id
(** Get id of last node seen in symbolic execution *) (** Get id of last node seen in symbolic execution *)
val get_node_id_key : unit -> Procdesc.Node.id * Digest.t val get_node_id_key : unit -> Procdesc.Node.id * Caml.Digest.t
(** Get id and key of last node seen in symbolic execution *) (** Get id and key of last node seen in symbolic execution *)
val get_normalized_pre : val get_normalized_pre :
@ -80,7 +80,7 @@ val mk_find_duplicate_nodes : Procdesc.t -> Procdesc.Node.t -> Procdesc.NodeSet.
and normalized (w.r.t. renaming of let - bound ids) list of instructions. *) and normalized (w.r.t. renaming of let - bound ids) list of instructions. *)
type log_issue = type log_issue =
?store_summary:bool -> Typ.Procname.t -> ?loc:Location.t -> ?node_id:int * Digest.t ?store_summary:bool -> Typ.Procname.t -> ?loc:Location.t -> ?node_id:int * Caml.Digest.t
-> ?session:int -> ?ltr:Errlog.loc_trace -> ?linters_def_file:string -> ?doc_url:string -> ?session:int -> ?ltr:Errlog.loc_trace -> ?linters_def_file:string -> ?doc_url:string
-> ?access:string -> exn -> unit -> ?access:string -> exn -> unit

@ -53,7 +53,7 @@ let get_blocks_nullified node =
let null_blocks = let null_blocks =
List.concat_map List.concat_map
~f:(fun i -> ~f:(fun i ->
match i with Sil.Nullify (pvar, _) when Sil.is_block_pvar pvar -> [pvar] | _ -> []) match i with Sil.Nullify (pvar, _) when Sil.is_block_pvar pvar -> [pvar] | _ -> [] )
(ProcCfg.Exceptional.instrs node) (ProcCfg.Exceptional.instrs node)
in in
null_blocks null_blocks
@ -642,7 +642,7 @@ let resolve_java_pname tenv prop args pname_java call_flags : Typ.Procname.java
| Some class_name -> | Some class_name ->
Typ.Procname.split_classname (Typ.Name.name class_name) :: accu Typ.Procname.split_classname (Typ.Name.name class_name) :: accu
| None -> | None ->
name :: accu) name :: accu )
~init:[] args ~init:[] args
(Typ.Procname.java_get_parameters resolved_pname_java) (Typ.Procname.java_get_parameters resolved_pname_java)
|> List.rev |> List.rev
@ -700,8 +700,7 @@ let resolve_and_analyze tenv caller_pdesc prop args callee_proc_name call_flags
Some resolved_proc_desc Some resolved_proc_desc
| None -> | None ->
Option.map Option.map
~f:(fun callee_proc_desc -> ~f:(fun callee_proc_desc -> Cfg.specialize_types callee_proc_desc resolved_pname args)
Cfg.specialize_types callee_proc_desc resolved_pname args)
(Ondemand.get_proc_desc callee_proc_name) (Ondemand.get_proc_desc callee_proc_name)
in in
Option.bind resolved_proc_desc_option ~f:analyze Option.bind resolved_proc_desc_option ~f:analyze
@ -753,7 +752,7 @@ let receiver_self receiver prop =
Exp.equal e receiver && Pvar.is_seed pv Exp.equal e receiver && Pvar.is_seed pv
&& Mangled.equal (Pvar.get_name pv) (Mangled.from_string "self") && Mangled.equal (Pvar.get_name pv) (Mangled.from_string "self")
| _ -> | _ ->
false) false )
prop.Prop.sigma prop.Prop.sigma
@ -914,7 +913,7 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nonnull_annot typ cal
| Sil.Hpointsto (Exp.Lvar pv, _, exp) when Pvar.equal pv abduced_ret_pv -> | Sil.Hpointsto (Exp.Lvar pv, _, exp) when Pvar.equal pv abduced_ret_pv ->
Some exp Some exp
| _ -> | _ ->
None) None )
p.Prop.sigma_fp p.Prop.sigma_fp
in in
(* find an hpred [abduced] |-> A in [prop] and add [exp] = A to prop *) (* find an hpred [abduced] |-> A in [prop] and add [exp] = A to prop *)
@ -1432,7 +1431,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
| Sil.Hpointsto (Exp.Lvar pv, _, _) -> | Sil.Hpointsto (Exp.Lvar pv, _, _) ->
Pvar.equal pv abduced Pvar.equal pv abduced
| _ -> | _ ->
false) false )
p.Prop.sigma_fp p.Prop.sigma_fp
in in
(* prevent introducing multiple abduced retvals for a single call site in a loop *) (* prevent introducing multiple abduced retvals for a single call site in a loop *)
@ -1480,7 +1479,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
let new_hpred = Sil.Hpointsto (actual, rhs, texp) in let new_hpred = Sil.Hpointsto (actual, rhs, texp) in
Prop.normalize tenv (Prop.set p ~sigma:(new_hpred :: prop'.Prop.sigma)) Prop.normalize tenv (Prop.set p ~sigma:(new_hpred :: prop'.Prop.sigma))
| _ -> | _ ->
p) p )
~init:prop' prop'.Prop.sigma ~init:prop' prop'.Prop.sigma
in in
let non_const_actuals_by_ref = let non_const_actuals_by_ref =
@ -1549,7 +1548,7 @@ and unknown_or_scan_call ~is_scan ~reason ret_type_option ret_annots
| (Exp.Var _ as e), ({Typ.desc= Tptr _} as t) when should_abduce_param_value callee_pname -> | (Exp.Var _ as e), ({Typ.desc= Tptr _} as t) when should_abduce_param_value callee_pname ->
Some (e, t, i) Some (e, t, i)
| _ -> | _ ->
None) None )
args args
in in
let has_nonnull_annot = Annotations.ia_is_nonnull ret_annots in let has_nonnull_annot = Annotations.ia_is_nonnull ret_annots in
@ -1819,7 +1818,7 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t),
let res_list = let res_list =
Config.run_with_abs_val_equal_zero Config.run_with_abs_val_equal_zero
(* no exp abstraction during sym exe *) (* no exp abstraction during sym exe *)
(fun () -> sym_exec tenv (ProcCfg.Exceptional.proc_desc proc_cfg) instr prop' path) (fun () -> sym_exec tenv (ProcCfg.Exceptional.proc_desc proc_cfg) instr prop' path )
() ()
in in
let res_list_nojunk = let res_list_nojunk =

@ -353,7 +353,7 @@ let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre fo
let deref_err_list = let deref_err_list =
List.fold List.fold
~f:(fun deref_errs hpred -> ~f:(fun deref_errs hpred ->
match check_hpred hpred with Some reason -> reason :: deref_errs | None -> deref_errs) match check_hpred hpred with Some reason -> reason :: deref_errs | None -> deref_errs )
~init:[] spec_pre.Prop.sigma ~init:[] spec_pre.Prop.sigma
in in
match deref_err_list with match deref_err_list with
@ -789,13 +789,14 @@ let combine tenv ret_id (posts: ('a Prop.t * Paths.Path.t) list) actual_pre path
else else
List.map List.map
~f:(fun (p, path_post) -> ~f:(fun (p, path_post) ->
(p, Paths.Path.add_call (include_subtrace callee_pname) path_pre callee_pname path_post)) (p, Paths.Path.add_call (include_subtrace callee_pname) path_pre callee_pname path_post)
)
posts posts
in in
List.map List.map
~f:(fun (p, path) -> ~f:(fun (p, path) ->
post_process_post tenv caller_pname callee_pname loc actual_pre post_process_post tenv caller_pname callee_pname loc actual_pre
(Prop.prop_sub split.sub p, path)) (Prop.prop_sub split.sub p, path) )
posts' posts'
in in
L.d_increase_indent 1 ; L.d_increase_indent 1 ;
@ -1029,7 +1030,7 @@ let check_uninitialize_dangling_deref caller_pname tenv callee_pname actual_pre
| Some (Deref_undef_exp, desc) -> | Some (Deref_undef_exp, desc) ->
raise (Exceptions.Dangling_pointer_dereference (Some PredSymb.DAuninit, desc, __POS__)) raise (Exceptions.Dangling_pointer_dereference (Some PredSymb.DAuninit, desc, __POS__))
| _ -> | _ ->
()) () )
props props
@ -1366,4 +1367,3 @@ let exe_function_call callee_summary tenv ret_id_opt caller_pdesc callee_pname l
in in
let results = List.map ~f:exe_one_spec spec_list in let results = List.map ~f:exe_one_spec spec_list in
exe_call_postprocess tenv ret_id_opt trace_call callee_pname callee_attrs loc results exe_call_postprocess tenv ret_id_opt trace_call callee_pname callee_attrs loc results

@ -118,10 +118,9 @@ let exe_timeout f x =
~f:(fun () -> ~f:(fun () ->
suspend_existing_timeout_and_start_new_one () ; suspend_existing_timeout_and_start_new_one () ;
f x ; f x ;
None) None )
~finally:resume_previous_timeout ~finally:resume_previous_timeout
with SymOp.Analysis_failure_exe kind -> with SymOp.Analysis_failure_exe kind ->
L.progressbar_timeout_event kind ; L.progressbar_timeout_event kind ;
Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind ; Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind ;
Some kind Some kind

@ -283,4 +283,3 @@ let command_to_data =
let data_of_command command = let data_of_command command =
List.Assoc.find_exn ~equal:CLOpt.equal_command command_to_data command List.Assoc.find_exn ~equal:CLOpt.equal_command command_to_data command

@ -181,7 +181,7 @@ let xdesc {long; short; spec} =
(Arg.Bad (Arg.Bad
(F.sprintf "wrong argument '%s'; option '%s' expects one of: %s" arg (F.sprintf "wrong argument '%s'; option '%s' expects one of: %s" arg
(dashdash ~short long) (dashdash ~short long)
(String.concat ~sep:" | " symbols)))) (String.concat ~sep:" | " symbols))) )
| _ -> | _ ->
spec spec
in in
@ -218,7 +218,6 @@ module SectionMap = Caml.Map.Make (struct
-1 -1
else (* reverse order *) else (* reverse order *)
String.compare s2 s1 String.compare s2 s1
end) end)
let help_sections_desc_lists = let help_sections_desc_lists =
@ -384,8 +383,10 @@ let mk_set var value ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta=
let setter () = var := value in let setter () = var := value in
ignore ignore
(mk ~deprecated ~long ?short ~default:() ?parse_mode ?in_help ~meta doc (mk ~deprecated ~long ?short ~default:() ?parse_mode ?in_help ~meta doc
~default_to_string:(fun () -> "") ~decode_json:(string_json_decoder ~long) ~default_to_string:(fun () -> "")
~mk_setter:(fun _ _ -> setter ()) ~mk_spec:(fun _ -> Unit setter )) ~decode_json:(string_json_decoder ~long)
~mk_setter:(fun _ _ -> setter ())
~mk_spec:(fun _ -> Unit setter))
let mk_with_reset value ~reset_doc ?deprecated ~long ?parse_mode mk = let mk_with_reset value ~reset_doc ?deprecated ~long ?parse_mode mk =
@ -405,8 +406,9 @@ let mk_option ?(default= None) ?(default_to_string= fun _ -> "") ~f ?(mk_reset=
?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "string") doc = ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "string") doc =
let mk () = let mk () =
mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta doc ~default_to_string mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta doc ~default_to_string
~decode_json:(string_json_decoder ~long) ~mk_setter:(fun var str -> var := f str) ~mk_spec: ~decode_json:(string_json_decoder ~long)
(fun set -> String set ) ~mk_setter:(fun var str -> var := f str)
~mk_spec:(fun set -> String set)
in in
if mk_reset then if mk_reset then
let reset_doc = reset_doc_opt ~long in let reset_doc = reset_doc_opt ~long in
@ -423,7 +425,7 @@ let mk_bool ?(deprecated_no= []) ?(default= false) ?(f= fun b -> b) ?(deprecated
and noshort = and noshort =
Option.map Option.map
~f:(fun short -> ~f:(fun short ->
if Char.is_lowercase short then Char.uppercase short else Char.lowercase short) if Char.is_lowercase short then Char.uppercase short else Char.lowercase short )
short short
in in
let doc long short = let doc long short =
@ -444,7 +446,7 @@ let mk_bool ?(deprecated_no= []) ?(default= false) ?(f= fun b -> b) ?(deprecated
mk ~long ?short ~deprecated ~default ?parse_mode ?in_help ~meta doc ~default_to_string mk ~long ?short ~deprecated ~default ?parse_mode ?in_help ~meta doc ~default_to_string
~mk_setter:(fun var _ -> var := f true) ~mk_setter:(fun var _ -> var := f true)
~decode_json:(fun ~inferconfig_dir:_ json -> ~decode_json:(fun ~inferconfig_dir:_ json ->
[dashdash (if YBU.to_bool json then long else nolong)]) [dashdash (if YBU.to_bool json then long else nolong)] )
~mk_spec ~mk_spec
in in
ignore ignore
@ -452,7 +454,7 @@ let mk_bool ?(deprecated_no= []) ?(default= false) ?(f= fun b -> b) ?(deprecated
?in_help ~meta nodoc ~default_to_string ?in_help ~meta nodoc ~default_to_string
~mk_setter:(fun _ _ -> var := f false) ~mk_setter:(fun _ _ -> var := f false)
~decode_json:(fun ~inferconfig_dir:_ json -> ~decode_json:(fun ~inferconfig_dir:_ json ->
[dashdash (if YBU.to_bool json then nolong else long)]) [dashdash (if YBU.to_bool json then nolong else long)] )
~mk_spec) ; ~mk_spec) ;
var var
@ -470,8 +472,10 @@ let mk_bool_group ?(deprecated_no= []) ?(default= false) ?f:(f0 = Fn.id) ?(depre
let mk_int ~default ?(f= Fn.id) ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "int") let mk_int ~default ?(f= Fn.id) ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "int")
doc = doc =
mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta doc mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta doc
~default_to_string:string_of_int ~mk_setter:(fun var str -> var := f (int_of_string str)) ~default_to_string:string_of_int
~decode_json:(string_json_decoder ~long) ~mk_spec:(fun set -> String set ) ~mk_setter:(fun var str -> var := f (int_of_string str))
~decode_json:(string_json_decoder ~long)
~mk_spec:(fun set -> String set)
let mk_int_opt ?default ?f:(f0 = Fn.id) ?(deprecated= []) ~long ?short ?parse_mode ?in_help let mk_int_opt ?default ?f:(f0 = Fn.id) ?(deprecated= []) ~long ?short ?parse_mode ?in_help
@ -483,8 +487,10 @@ let mk_int_opt ?default ?f:(f0 = Fn.id) ?(deprecated= []) ~long ?short ?parse_mo
let mk_float ~default ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "float") doc = let mk_float ~default ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "float") doc =
mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta doc mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta doc
~default_to_string:string_of_float ~mk_setter:(fun var str -> var := float_of_string str) ~default_to_string:string_of_float
~decode_json:(string_json_decoder ~long) ~mk_spec:(fun set -> String set ) ~mk_setter:(fun var str -> var := float_of_string str)
~decode_json:(string_json_decoder ~long)
~mk_spec:(fun set -> String set)
let mk_float_opt ?default ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "float") doc = let mk_float_opt ?default ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "float") doc =
@ -496,8 +502,10 @@ let mk_float_opt ?default ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(
let mk_string ~default ?(f= fun s -> s) ?(deprecated= []) ~long ?short ?parse_mode ?in_help let mk_string ~default ?(f= fun s -> s) ?(deprecated= []) ~long ?short ?parse_mode ?in_help
?(meta= "string") doc = ?(meta= "string") doc =
mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta doc mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta doc
~default_to_string:(fun s -> s) ~mk_setter:(fun var str -> var := f str) ~default_to_string:(fun s -> s)
~decode_json:(string_json_decoder ~long) ~mk_spec:(fun set -> String set ) ~mk_setter:(fun var str -> var := f str)
~decode_json:(string_json_decoder ~long)
~mk_spec:(fun set -> String set)
let mk_string_opt ?default ?(f= fun s -> s) ?mk_reset ?(deprecated= []) ~long ?short ?parse_mode let mk_string_opt ?default ?(f= fun s -> s) ?mk_reset ?(deprecated= []) ~long ?short ?parse_mode
@ -512,9 +520,10 @@ let mk_string_list ?(default= []) ?(f= fun s -> s) ?(deprecated= []) ~long ?shor
?in_help ?(meta= "string") doc = ?in_help ?(meta= "string") doc =
let mk () = let mk () =
mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta:("+" ^ meta) doc mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta:("+" ^ meta) doc
~default_to_string:(String.concat ~sep:",") ~mk_setter:(fun var str -> var := f str :: !var) ~default_to_string:(String.concat ~sep:",")
~decode_json:(list_json_decoder (string_json_decoder ~long)) ~mk_spec:(fun set -> String set ~mk_setter:(fun var str -> var := f str :: !var)
) ~decode_json:(list_json_decoder (string_json_decoder ~long))
~mk_spec:(fun set -> String set)
in in
let reset_doc = reset_doc_list ~long in let reset_doc = reset_doc_list ~long in
mk_with_reset [] ~reset_doc ~long ?parse_mode mk mk_with_reset [] ~reset_doc ~long ?parse_mode mk
@ -539,7 +548,8 @@ let mk_path_helper ~setter ~default_to_string ~default ~deprecated ~long ~short
~default_to_string ~default_to_string
~mk_setter:(fun var str -> ~mk_setter:(fun var str ->
let abs_path = normalize_path_in_args_being_parsed ~is_anon_arg:false str in let abs_path = normalize_path_in_args_being_parsed ~is_anon_arg:false str in
setter var abs_path) ~mk_spec:(fun set -> String set ) setter var abs_path )
~mk_spec:(fun set -> String set)
let mk_path ~default ?(f= Fn.id) ?(deprecated= []) ~long ?short ?parse_mode ?in_help let mk_path ~default ?(f= Fn.id) ?(deprecated= []) ~long ?short ?parse_mode ?in_help
@ -589,8 +599,10 @@ let mk_symbol ~default ~symbols ~eq ?(f= Fn.id) ?(deprecated= []) ~long ?short ?
let to_string sym = List.Assoc.find_exn ~equal:eq sym_to_str sym in let to_string sym = List.Assoc.find_exn ~equal:eq sym_to_str sym in
let meta = Option.value meta ~default:(mk_symbols_meta symbols) in let meta = Option.value meta ~default:(mk_symbols_meta symbols) in
mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta doc mk ~deprecated ~long ?short ~default ?parse_mode ?in_help ~meta doc
~default_to_string:(fun s -> to_string s) ~mk_setter:(fun var str -> var := of_string str |> f) ~default_to_string:(fun s -> to_string s)
~decode_json:(string_json_decoder ~long) ~mk_spec:(fun set -> Symbol (strings, set) ) ~mk_setter:(fun var str -> var := of_string str |> f)
~decode_json:(string_json_decoder ~long)
~mk_spec:(fun set -> Symbol (strings, set))
let mk_symbol_opt ~symbols ?(f= Fn.id) ?(mk_reset= true) ?(deprecated= []) ~long ?short ?parse_mode let mk_symbol_opt ~symbols ?(f= Fn.id) ?(mk_reset= true) ?(deprecated= []) ~long ?short ?parse_mode
@ -600,8 +612,10 @@ let mk_symbol_opt ~symbols ?(f= Fn.id) ?(mk_reset= true) ?(deprecated= []) ~long
let meta = Option.value meta ~default:(mk_symbols_meta symbols) in let meta = Option.value meta ~default:(mk_symbols_meta symbols) in
let mk () = let mk () =
mk ~deprecated ~long ?short ~default:None ?parse_mode ?in_help ~meta doc mk ~deprecated ~long ?short ~default:None ?parse_mode ?in_help ~meta doc
~default_to_string:(fun _ -> "") ~mk_setter:(fun var str -> var := Some (f (of_string str))) ~default_to_string:(fun _ -> "")
~decode_json:(string_json_decoder ~long) ~mk_spec:(fun set -> Symbol (strings, set) ) ~mk_setter:(fun var str -> var := Some (f (of_string str)))
~decode_json:(string_json_decoder ~long)
~mk_spec:(fun set -> Symbol (strings, set))
in in
if mk_reset then if mk_reset then
let reset_doc = reset_doc_opt ~long in let reset_doc = reset_doc_opt ~long in
@ -619,8 +633,8 @@ let mk_symbol_seq ?(default= []) ~symbols ~eq ?(deprecated= []) ~long ?short ?pa
~default_to_string:(fun syms -> String.concat ~sep:" " (List.map ~f:to_string syms)) ~default_to_string:(fun syms -> String.concat ~sep:" " (List.map ~f:to_string syms))
~mk_setter:(fun var str_seq -> var := List.map ~f:of_string (String.split ~on:',' str_seq)) ~mk_setter:(fun var str_seq -> var := List.map ~f:of_string (String.split ~on:',' str_seq))
~decode_json:(fun ~inferconfig_dir:_ json -> ~decode_json:(fun ~inferconfig_dir:_ json ->
[dashdash long; String.concat ~sep:"," (YBU.convert_each YBU.to_string json)]) ~mk_spec: [dashdash long; String.concat ~sep:"," (YBU.convert_each YBU.to_string json)] )
(fun set -> String set ) ~mk_spec:(fun set -> String set)
let mk_set_from_json ~default ~default_to_string ~f ?(deprecated= []) ~long ?short ?parse_mode let mk_set_from_json ~default ~default_to_string ~f ?(deprecated= []) ~long ?short ?parse_mode
@ -628,7 +642,7 @@ let mk_set_from_json ~default ~default_to_string ~f ?(deprecated= []) ~long ?sho
mk ~deprecated ~long ?short ?parse_mode ?in_help ~meta doc ~default ~default_to_string mk ~deprecated ~long ?short ?parse_mode ?in_help ~meta doc ~default ~default_to_string
~mk_setter:(fun var json -> var := f (Yojson.Basic.from_string json)) ~mk_setter:(fun var json -> var := f (Yojson.Basic.from_string json))
~decode_json:(fun ~inferconfig_dir:_ json -> [dashdash long; Yojson.Basic.to_string json]) ~decode_json:(fun ~inferconfig_dir:_ json -> [dashdash long; Yojson.Basic.to_string json])
~mk_spec:(fun set -> String set ) ~mk_spec:(fun set -> String set)
let mk_json ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "json") doc = let mk_json ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "json") doc =
@ -636,7 +650,7 @@ let mk_json ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "json")
~default_to_string:Yojson.Basic.to_string ~default_to_string:Yojson.Basic.to_string
~mk_setter:(fun var json -> var := Yojson.Basic.from_string json) ~mk_setter:(fun var json -> var := Yojson.Basic.from_string json)
~decode_json:(fun ~inferconfig_dir:_ json -> [dashdash long; Yojson.Basic.to_string json]) ~decode_json:(fun ~inferconfig_dir:_ json -> [dashdash long; Yojson.Basic.to_string json])
~mk_spec:(fun set -> String set ) ~mk_spec:(fun set -> String set)
(** [mk_anon] always return the same ref. Anonymous arguments are only accepted if (** [mk_anon] always return the same ref. Anonymous arguments are only accepted if
@ -756,7 +770,7 @@ let mk_rest_actions ?(parse_mode= InferCommand) ?(in_help= []) doc ~usage decode
String String
(fun arg -> (fun arg ->
rest := List.rev (Array.to_list (Array.slice !args_to_parse (!arg_being_parsed + 1) 0)) ; rest := List.rev (Array.to_list (Array.slice !args_to_parse (!arg_being_parsed + 1) 0)) ;
select_parse_mode ~usage (decode_action arg) |> ignore) select_parse_mode ~usage (decode_action arg) |> ignore )
in in
add parse_mode in_help add parse_mode in_help
{long= "--"; short= ""; meta= ""; doc; spec; decode_json= (fun ~inferconfig_dir:_ _ -> [])} ; {long= "--"; short= ""; meta= ""; doc; spec; decode_json= (fun ~inferconfig_dir:_ _ -> [])} ;
@ -772,12 +786,14 @@ let mk_subcommand command ?on_unknown_arg:(on_unknown = `Reject) ~name ?deprecat
( match deprecated_long with ( match deprecated_long with
| Some long -> | Some long ->
ignore ignore
(mk ~long ~default:() ?parse_mode ?in_help ~meta:"" "" ~default_to_string:(fun () -> "") (mk ~long ~default:() ?parse_mode ?in_help ~meta:"" ""
~default_to_string:(fun () -> "")
~decode_json:(fun ~inferconfig_dir:_ _ -> ~decode_json:(fun ~inferconfig_dir:_ _ ->
raise (Arg.Bad ("Bad option in config file: " ^ long))) raise (Arg.Bad ("Bad option in config file: " ^ long)) )
~mk_setter:(fun _ _ -> ~mk_setter:(fun _ _ ->
warnf "WARNING: '%s' is deprecated. Please use '%s' instead.@\n" (dashdash long) name ; warnf "WARNING: '%s' is deprecated. Please use '%s' instead.@\n" (dashdash long) name ;
switch ()) ~mk_spec:(fun set -> Unit (fun () -> set "") )) switch () )
~mk_spec:(fun set -> Unit (fun () -> set "")))
| None -> | None ->
() ) ; () ) ;
subcommands := (command, (command_doc, name, in_help)) :: !subcommands ; subcommands := (command, (command_doc, name, in_help)) :: !subcommands ;
@ -856,7 +872,7 @@ let decode_inferconfig_to_argv path =
~f:(fun {long; short} -> ~f:(fun {long; short} ->
String.equal key long || String.equal key short String.equal key long || String.equal key short
(* for deprecated options *) (* for deprecated options *)
|| (* for deprecated options that start with "-" *) String.equal ("-" ^ key) short) || (* for deprecated options that start with "-" *) String.equal ("-" ^ key) short )
!desc_list !desc_list
in in
decode_json ~inferconfig_dir json_val @ result decode_json ~inferconfig_dir json_val @ result
@ -883,7 +899,7 @@ let encode_argv_to_env argv =
|| ||
(warnf "WARNING: Ignoring unsupported option containing '%c' character: %s@\n" env_var_sep (warnf "WARNING: Ignoring unsupported option containing '%c' character: %s@\n" env_var_sep
arg ; arg ;
false)) false) )
argv) argv)
@ -1008,8 +1024,8 @@ let wrap_line indent_string wrap_length line0 =
let add_word_to_paragraph (rev_lines, non_empty, line, line_length) word = let add_word_to_paragraph (rev_lines, non_empty, line, line_length) word =
let word_length = let word_length =
let len = String.length word in let len = String.length word in
if String.is_prefix ~prefix:"$(b," word || String.is_prefix ~prefix:"$(i," word then len - 4 if String.is_prefix ~prefix:"$(b," word || String.is_prefix ~prefix:"$(i," word then
(* length of formatting tag prefix *) len - 4 (* length of formatting tag prefix *)
- 1 (* APPROXIMATION: closing parenthesis that will come after the word, or maybe later *) - 1 (* APPROXIMATION: closing parenthesis that will come after the word, or maybe later *)
else len else len
in in
@ -1059,8 +1075,9 @@ let show_manual ?internal_section format default_doc command_opt =
(* base indentation of documentation strings *) (* base indentation of documentation strings *)
in in
`I (Format.asprintf "$(b,%s)%a%a" (dashdash long) pp_short short pp_meta meta, doc_first_line) `I (Format.asprintf "$(b,%s)%a%a" (dashdash long) pp_short short pp_meta meta, doc_first_line)
:: List.concat_map (List.concat_map ~f:(wrap_line indent_string width) doc_other_lines) ~f: :: List.concat_map
(fun s -> [`Noblank; `Pre s] ) (List.concat_map ~f:(wrap_line indent_string width) doc_other_lines)
~f:(fun s -> [`Noblank; `Pre s])
in in
let option_blocks = let option_blocks =
match command_doc.manual_options with match command_doc.manual_options with
@ -1085,7 +1102,7 @@ let show_manual ?internal_section format default_doc command_opt =
(fun section descs result -> (fun section descs result ->
`S section `S section
:: (if String.equal section Cmdliner.Manpage.s_options then blocks else []) :: (if String.equal section Cmdliner.Manpage.s_options then blocks else [])
@ List.concat_map ~f:block_of_desc (normalize_desc_list descs) @ result) @ List.concat_map ~f:block_of_desc (normalize_desc_list descs) @ result )
!sections hidden !sections hidden
| None -> | None ->
`S Cmdliner.Manpage.s_options :: blocks `S Cmdliner.Manpage.s_options :: blocks
@ -1098,4 +1115,3 @@ let show_manual ?internal_section format default_doc command_opt =
in in
Cmdliner.Manpage.print format Format.std_formatter (command_doc.title, blocks) ; Cmdliner.Manpage.print format Format.std_formatter (command_doc.title, blocks) ;
() ()

@ -667,7 +667,7 @@ and analyzer =
- $(b,compile): similar to specifying the $(b,compile) subcommand (DEPRECATED) - $(b,compile): similar to specifying the $(b,compile) subcommand (DEPRECATED)
- $(b,crashcontext): experimental (see $(b,--crashcontext))|} - $(b,crashcontext): experimental (see $(b,--crashcontext))|}
~f:(function ~f:(function
| CaptureOnly | CompileOnly as x -> | (CaptureOnly | CompileOnly) as x ->
let analyzer_str = let analyzer_str =
List.find_map_exn string_to_analyzer ~f:(fun (s, y) -> List.find_map_exn string_to_analyzer ~f:(fun (s, y) ->
if equal_analyzer x y then Some s else None ) if equal_analyzer x y then Some s else None )
@ -752,7 +752,7 @@ and ( annotation_reachability
~f:(fun b -> ~f:(fun b ->
disable_all_checkers () ; disable_all_checkers () ;
var := b ; var := b ;
b) b )
( if String.equal doc "" then "" ( if String.equal doc "" then ""
else Printf.sprintf "Enable $(b,--%s) and disable all other checkers" long ) else Printf.sprintf "Enable $(b,--%s) and disable all other checkers" long )
[] (* do all the work in ~f *) [] (* do all the work in ~f *)
@ -769,15 +769,14 @@ and ( annotation_reachability
( "Default checkers: " ( "Default checkers: "
^ ( List.rev_filter_map ^ ( List.rev_filter_map
~f:(fun (_, long, _, default) -> ~f:(fun (_, long, _, default) ->
if default then Some (Printf.sprintf "$(b,--%s)" long) else None) if default then Some (Printf.sprintf "$(b,--%s)" long) else None )
!all_checkers !all_checkers
|> String.concat ~sep:", " ) ) |> String.concat ~sep:", " ) )
~f:(fun b -> ~f:(fun b ->
List.iter List.iter
~f:(fun (var, _, _, default) -> ~f:(fun (var, _, _, default) -> var := if b then default || !var else not default && !var)
var := if b then default || !var else not default && !var)
!all_checkers ; !all_checkers ;
b) b )
[] (* do all the work in ~f *) [] (* do all the work in ~f *)
[] []
(* do all the work in ~f *) (* do all the work in ~f *)
@ -1058,7 +1057,7 @@ and ( bo_debug
"Debug mode (also sets $(b,--debug-level 2), $(b,--developer-mode), $(b,--no-filtering), $(b,--print-buckets), $(b,--print-types), $(b,--reports-include-ml-loc), $(b,--no-only-cheap-debug), $(b,--trace-error), $(b,--write-dotty), $(b,--write-html))" "Debug mode (also sets $(b,--debug-level 2), $(b,--developer-mode), $(b,--no-filtering), $(b,--print-buckets), $(b,--print-types), $(b,--reports-include-ml-loc), $(b,--no-only-cheap-debug), $(b,--trace-error), $(b,--write-dotty), $(b,--write-html))"
~f:(fun debug -> ~f:(fun debug ->
if debug then set_debug_level 2 else set_debug_level 0 ; if debug then set_debug_level 2 else set_debug_level 0 ;
debug) debug )
[ developer_mode [ developer_mode
; print_buckets ; print_buckets
; print_types ; print_types
@ -1104,7 +1103,7 @@ and ( bo_debug
"Debug mode for developing new linters. (Sets the analyzer to $(b,linters); also sets $(b,--debug), $(b,--debug-level-linters 2), $(b,--developer-mode), and unsets $(b,--allowed-failures) and $(b,--default-linters)." "Debug mode for developing new linters. (Sets the analyzer to $(b,linters); also sets $(b,--debug), $(b,--debug-level-linters 2), $(b,--developer-mode), and unsets $(b,--allowed-failures) and $(b,--default-linters)."
~f:(fun debug -> ~f:(fun debug ->
debug_level_linters := if debug then 2 else 0 ; debug_level_linters := if debug then 2 else 0 ;
debug) debug )
[debug; developer_mode] [default_linters; keep_going] [debug; developer_mode] [default_linters; keep_going]
in in
( bo_debug ( bo_debug
@ -1156,7 +1155,7 @@ and () =
CLOpt.mk_string_list ?deprecated ~long CLOpt.mk_string_list ?deprecated ~long
~f:(fun issue_id -> ~f:(fun issue_id ->
let issue = IssueType.from_string issue_id in let issue = IssueType.from_string issue_id in
IssueType.set_enabled issue b ; issue_id) IssueType.set_enabled issue b ; issue_id )
?default ~meta:"issue_type" ?default ~meta:"issue_type"
~in_help:CLOpt.([(Report, manual_generic)]) ~in_help:CLOpt.([(Report, manual_generic)])
doc doc
@ -1728,10 +1727,12 @@ and report_previous =
and rest = and rest =
CLOpt.mk_rest_actions ~in_help:CLOpt.([(Capture, manual_generic); (Run, manual_generic)]) CLOpt.mk_rest_actions
~in_help:CLOpt.([(Capture, manual_generic); (Run, manual_generic)])
"Stop argument processing, use remaining arguments as a build command" ~usage:exe_usage "Stop argument processing, use remaining arguments as a build command" ~usage:exe_usage
(fun build_exe -> (fun build_exe ->
match Filename.basename build_exe with "java" | "javac" -> CLOpt.Javac | _ -> CLOpt.NoParse ) match Filename.basename build_exe with "java" | "javac" -> CLOpt.Javac | _ -> CLOpt.NoParse
)
and results_dir = and results_dir =
@ -1834,7 +1835,7 @@ and specs_library =
~long:"specs-library-index" ~default:"" ~long:"specs-library-index" ~default:""
~f:(fun file -> ~f:(fun file ->
specs_library := read_specs_dir_list_file file @ !specs_library ; specs_library := read_specs_dir_list_file file @ !specs_library ;
"") "" )
~in_help:CLOpt.([(Analyze, manual_generic)]) ~in_help:CLOpt.([(Analyze, manual_generic)])
~meta:"file" "" ~meta:"file" ""
in in
@ -2013,7 +2014,7 @@ let javac_classes_out =
(* extend env var args to pass args to children that do not receive the rest args *) (* extend env var args to pass args to children that do not receive the rest args *)
CLOpt.extend_env_args ["--results-dir"; classes_out_infer] ; CLOpt.extend_env_args ["--results-dir"; classes_out_infer] ;
results_dir := classes_out_infer ) ; results_dir := classes_out_infer ) ;
classes_out) classes_out )
"" ""
@ -2025,7 +2026,7 @@ and _ =
let files = List.filter paths ~f:(fun path -> Sys.is_file path = `Yes) in let files = List.filter paths ~f:(fun path -> Sys.is_file path = `Yes) in
CLOpt.extend_env_args (List.concat_map files ~f:(fun file -> ["--specs-library"; file])) ; CLOpt.extend_env_args (List.concat_map files ~f:(fun file -> ["--specs-library"; file])) ;
specs_library := List.rev_append files !specs_library ) ; specs_library := List.rev_append files !specs_library ) ;
classpath) classpath )
"" ""
@ -2093,7 +2094,7 @@ let post_parsing_initialization command_opt =
match inferconfig_file with match inferconfig_file with
| Some inferconfig -> | Some inferconfig ->
Printf.sprintf "version %s/inferconfig %s" Version.commit Printf.sprintf "version %s/inferconfig %s" Version.commit
(Digest.to_hex (Digest.file inferconfig)) (Caml.Digest.to_hex (Caml.Digest.file inferconfig))
| None -> | None ->
Version.commit Version.commit
in in
@ -2786,7 +2787,7 @@ let set_reference_and_call_function reference value f x =
Utils.try_finally_swallow_timeout Utils.try_finally_swallow_timeout
~f:(fun () -> ~f:(fun () ->
reference := value ; reference := value ;
f x) f x )
~finally:restore ~finally:restore

@ -92,13 +92,13 @@ let find_source_dirs () =
List.iter List.iter
~f:(fun fname -> ~f:(fun fname ->
let path = Filename.concat dir fname in let path = Filename.concat dir fname in
if Filename.check_suffix path ".cg" then source_dirs := dir :: !source_dirs) if Filename.check_suffix path ".cg" then source_dirs := dir :: !source_dirs )
files files
in in
List.iter List.iter
~f:(fun fname -> ~f:(fun fname ->
let dir = Filename.concat Config.captured_dir fname in let dir = Filename.concat Config.captured_dir fname in
if Sys.is_directory dir = `Yes then add_cg_files_from_dir dir) if Sys.is_directory dir = `Yes then add_cg_files_from_dir dir )
files_in_results_dir ; files_in_results_dir ;
List.rev !source_dirs List.rev !source_dirs
@ -164,7 +164,7 @@ let update_file_with_lock dir fname update =
let buf = read_whole_file fd in let buf = read_whole_file fd in
reset_file fd ; reset_file fd ;
let str = update buf in let str = update buf in
let i = Unix.write fd ~buf:str ~pos:0 ~len:(String.length str) in let i = Unix.write fd ~buf:(Bytes.of_string str) ~pos:0 ~len:(String.length str) in
if Int.equal i (String.length str) then ( if Int.equal i (String.length str) then (
Unix.lockf fd ~mode:Unix.F_ULOCK ~len:0L ; Unix.lockf fd ~mode:Unix.F_ULOCK ~len:0L ;
Unix.close fd ) Unix.close fd )
@ -265,7 +265,6 @@ module Results_dir = struct
in in
let full_fname = Filename.concat (create dir_path) filename in let full_fname = Filename.concat (create dir_path) filename in
Unix.openfile full_fname ~mode:Unix.([O_WRONLY; O_CREAT; O_TRUNC]) ~perm:0o777 Unix.openfile full_fname ~mode:Unix.([O_WRONLY; O_CREAT; O_TRUNC]) ~perm:0o777
end end
let global_tenv_fname = let global_tenv_fname =
@ -304,7 +303,8 @@ let fold_paths_matching ~dir ~p ~init ~f =
Array.fold Array.fold
~f:(fun acc file -> ~f:(fun acc file ->
let path = dir ^/ file in let path = dir ^/ file in
if Sys.is_directory path = `Yes then paths acc path else if p path then f path acc else acc) if Sys.is_directory path = `Yes then paths acc path else if p path then f path acc else acc
)
~init:path_list (Sys.readdir dir) ~init:path_list (Sys.readdir dir)
in in
paths init dir paths init dir

@ -50,4 +50,3 @@ let exit_code_of_exception = function
exitcode exitcode
| _ -> | _ ->
(* exit code 2 is used by the OCaml runtime in cases of uncaught exceptions *) 2 (* exit code 2 is used by the OCaml runtime in cases of uncaught exceptions *) 2

@ -36,4 +36,3 @@ let register ~f desc =
Pervasives.at_exit f_no_exn ; Pervasives.at_exit f_no_exn ;
(* Register signal masking. *) (* Register signal masking. *)
Lazy.force activate_run_epilogues_on_signal Lazy.force activate_run_epilogues_on_signal

@ -70,7 +70,6 @@ end = struct
let new_id = generate () in let new_id = generate () in
Unix.putenv ~key:infer_run_identifier_env_var ~data:new_id ; Unix.putenv ~key:infer_run_identifier_env_var ~data:new_id ;
new_id new_id
end end
let get_log_identifier () = Random_id.get () let get_log_identifier () = Random_id.get ()

@ -37,7 +37,6 @@ end = struct
; wrap_bold= wrap_simple ; wrap_bold= wrap_simple
; pp_bold= pp_simple ; pp_bold= pp_simple
; bold_to_string= Fn.id } ; bold_to_string= Fn.id }
end end
module PhabricatorFormatter : sig module PhabricatorFormatter : sig
@ -72,7 +71,6 @@ end = struct
; wrap_bold ; wrap_bold
; pp_bold ; pp_bold
; bold_to_string } ; bold_to_string }
end end
let formatter = let formatter =

@ -78,4 +78,3 @@ let merge_buck_flavors_results infer_deps_file =
List.iter ~f:one_line lines List.iter ~f:one_line lines
| Error error -> | Error error ->
L.internal_error "Couldn't read deps file '%s': %s" infer_deps_file error L.internal_error "Couldn't read deps file '%s': %s" infer_deps_file error

@ -64,4 +64,3 @@ let resolve fname =
fname fname
| Some links -> | Some links ->
try DB.filename_from_string (String.Table.find_exn links base) with Not_found -> fname try DB.filename_from_string (String.Table.find_exn links base) with Not_found -> fname

@ -63,7 +63,8 @@ let text =
(** Default html print environment *) (** Default html print environment *)
let html color = let html color =
{ text with { text with
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
}
(** Extend the normal colormap for the given object with the given color *) (** Extend the normal colormap for the given object with the given color *)
@ -146,4 +147,3 @@ let pp_argfile fmt fname =
let cli_args fmt args = let cli_args fmt args =
F.fprintf fmt "'%a'@\n%a" (seq ~sep:"' '" string) args (seq ~sep:"\n" pp_argfile) F.fprintf fmt "'%a'@\n%a" (seq ~sep:"' '" string) args (seq ~sep:"\n" pp_argfile)
(List.filter_map ~f:(String.chop_prefix ~prefix:"@") args) (List.filter_map ~f:(String.chop_prefix ~prefix:"@") args)

@ -63,5 +63,4 @@ module MakePPMap (Ord : PrintableOrderedType) = struct
let pp ~pp_value fmt m = let pp ~pp_value fmt m =
let pp_item fmt (k, v) = F.fprintf fmt "%a -> %a" Ord.pp k pp_value v in let pp_item fmt (k, v) = F.fprintf fmt "%a -> %a" Ord.pp k pp_value v in
pp_collection ~pp_item fmt (bindings m) pp_collection ~pp_item fmt (bindings m)
end end

@ -17,7 +17,7 @@ let print_error_and_exit ?(exit_code= 1) fmt =
F.kfprintf F.kfprintf
(fun _ -> (fun _ ->
L.external_error "%s" (F.flush_str_formatter ()) ; L.external_error "%s" (F.flush_str_formatter ()) ;
L.exit exit_code) L.exit exit_code )
F.str_formatter fmt F.str_formatter fmt
@ -65,4 +65,3 @@ let pipeline ~producer_prog ~producer_args ~consumer_prog ~consumer_args =
let producer_status = Unix.waitpid producer_pid in let producer_status = Unix.waitpid producer_pid in
let consumer_status = Unix.waitpid consumer_pid in let consumer_status = Unix.waitpid consumer_pid in
(producer_status, consumer_status) (producer_status, consumer_status)

@ -45,4 +45,3 @@ let start_child ~f ~pool x =
| `In_the_parent _pid -> | `In_the_parent _pid ->
incr pool ; incr pool ;
if should_wait pool then wait pool if should_wait pool then wait pool

@ -34,7 +34,6 @@ module Key = struct
, 579094948 , 579094948
, 972393003 , 972393003
, 852343110 ) , 852343110 )
end end
(** version of the binary files, to be incremented for each change *) (** version of the binary files, to be incremented for each change *)
@ -95,8 +94,9 @@ let create_serializer (key: Key.t) : 'a serializer =
(* Retry to read for 1 second in case of end of file, *) (* Retry to read for 1 second in case of end of file, *)
(* which indicates that another process is writing the same file. *) (* which indicates that another process is writing the same file. *)
let one_second = Mtime.Span.of_uint64_ns (Int64.of_int 1_000_000_000) in let one_second = Mtime.Span.of_uint64_ns (Int64.of_int 1_000_000_000) in
SymOp.try_finally ~f:(fun () -> retry_exception ~timeout:one_second ~catch_exn ~f:read ()) SymOp.try_finally
~finally:(fun () -> In_channel.close inc ) ~f:(fun () -> retry_exception ~timeout:one_second ~catch_exn ~f:read ())
~finally:(fun () -> In_channel.close inc)
in in
let write_to_tmp_file fname data = let write_to_tmp_file fname data =
let fname_tmp = let fname_tmp =

@ -179,5 +179,4 @@ module SQLite = struct
RelativeProjectRoot rel_path RelativeProjectRoot rel_path
| Sqlite3.Data.BLOB b -> | Sqlite3.Data.BLOB b ->
Marshal.from_string b 0 Marshal.from_string b 0
end end

Some files were not shown because too many files have changed in this diff Show More

Loading…
Cancel
Save