[ocamlformat] upgrade to ocamlformat 0.7

Reviewed By: mbouaziz

Differential Revision: D9496601

fbshipit-source-id: 83c6fd241
master
Josh Berdine 6 years ago committed by Facebook Github Bot
parent 060924adff
commit 40ab73037e

@ -1,3 +1,3 @@
margin 100
sparse true
version 0.5
break-cases = nested
margin = 100
version = 0.7

@ -1 +1 @@
19b52cea4dd5ffff8094aaa671ae019a969863f8
b3ed72b3997cb7712e54f90d47128d6dd8e18f53

@ -638,7 +638,7 @@ endif
# This is a magical version number that doesn't reinstall the world when added on top of what we
# have in opam.lock. To upgrade this version number, manually try to install several utop versions
# until you find one that doesn't recompile the world. TODO(t20828442): get rid of magic
OPAM_DEV_DEPS = ocamlformat.$$(grep version .ocamlformat | cut -d ' ' -f 2) ocp-indent merlin utop.2.2.0 webbrowser
OPAM_DEV_DEPS = ocamlformat.$$(grep version .ocamlformat | cut -d ' ' -f 3) ocp-indent merlin utop.2.2.0 webbrowser
ifneq ($(EMACS),no)
OPAM_DEV_DEPS += tuareg

@ -75,8 +75,7 @@ let rec get_typ t tenv : Typ.t option =
match t with
| Base (_, typ) ->
Some typ
| FieldOffset (ae, fld)
-> (
| FieldOffset (ae, fld) -> (
let base_typ_opt = get_typ ae tenv in
match base_typ_opt with
| Some base_typ ->
@ -88,9 +87,9 @@ let rec get_typ t tenv : Typ.t option =
| AddressOf ae ->
let base_typ_opt = get_typ ae tenv in
Option.map base_typ_opt ~f:(fun base_typ -> Typ.mk (Tptr (base_typ, Pk_pointer)))
| Dereference ae ->
| Dereference ae -> (
let base_typ_opt = get_typ ae tenv in
match base_typ_opt with Some {Typ.desc= Tptr (typ, _)} -> Some typ | _ -> None
match base_typ_opt with Some {Typ.desc= Tptr (typ, _)} -> Some typ | _ -> None )
let rec pp fmt = function
@ -202,12 +201,10 @@ let of_exp ~include_array_indexes ~add_deref exp0 typ0 ~(f_resolve_id: Var.t ->
let of_lhs_exp ~include_array_indexes ~add_deref lhs_exp typ ~(f_resolve_id : Var.t -> t option) =
match lhs_exp with
| Exp.Lfield _ when not add_deref
-> (
| Exp.Lfield _ when not add_deref -> (
let res = of_exp ~include_array_indexes ~add_deref:true lhs_exp typ ~f_resolve_id in
match res with [lhs_ae] -> Some (AddressOf lhs_ae) | _ -> None )
| Exp.Lindex _ when not add_deref
-> (
| Exp.Lindex _ when not add_deref -> (
let res =
let typ' =
match typ.Typ.desc with
@ -220,6 +217,6 @@ let of_lhs_exp ~include_array_indexes ~add_deref lhs_exp typ ~(f_resolve_id: Var
of_exp ~include_array_indexes ~add_deref:true lhs_exp typ' ~f_resolve_id
in
match res with [lhs_ae] -> Some (AddressOf lhs_ae) | _ -> None )
| _ ->
| _ -> (
let res = of_exp ~include_array_indexes ~add_deref lhs_exp typ ~f_resolve_id in
match res with [lhs_ae] -> Some lhs_ae | _ -> None
match res with [lhs_ae] -> Some lhs_ae | _ -> None )

@ -39,8 +39,12 @@ val pp : Format.formatter -> t -> unit
val equal : t -> t -> bool
val of_lhs_exp :
include_array_indexes:bool -> add_deref:bool -> Exp.t -> Typ.t
-> f_resolve_id:(Var.t -> t option) -> t option
include_array_indexes:bool
-> add_deref:bool
-> Exp.t
-> Typ.t
-> f_resolve_id:(Var.t -> t option)
-> t option
(** convert [lhs_exp] to an access expression, resolving identifiers using [f_resolve_id] *)
val normalize : t -> t

@ -21,7 +21,7 @@ module Raw = struct
type access = ArrayAccess of Typ.t * t list | FieldAccess of Typ.Fieldname.t
and t = (base * access list) [@@deriving compare]
and t = base * access list [@@deriving compare]
let equal_access = [%compare.equal: access]
@ -96,12 +96,12 @@ module Raw = struct
(Some base_typ, None)
| [last_access] ->
(Some base_typ, Some last_access)
| curr_access :: rest ->
| curr_access :: rest -> (
match get_access_type tenv base_typ curr_access with
| Some access_typ ->
last_access_info_impl tenv access_typ rest
| None ->
(None, None)
(None, None) )
in
last_access_info_impl tenv base_typ accesses
@ -296,8 +296,7 @@ let inner_class_normalize p =
(base, accesses) ) )
(* this$n.f ... -> this.f . ... *)
(* happens in ctrs only *)
| Some ((Var.ProgramVar pvar, typ), all_accesses)
when is_synthetic_this pvar ->
| Some ((Var.ProgramVar pvar, typ), all_accesses) when is_synthetic_this pvar ->
let varname = Mangled.from_string "this" in
mk_pvar_as varname pvar
|> Option.map ~f:(fun new_pvar -> (base_of_pvar new_pvar typ, all_accesses))

@ -8,6 +8,7 @@
(** The Smallfoot Intermediate Language: Annotations *)
open! IStd
module F = Format
type parameters = string list [@@deriving compare]
@ -33,6 +34,7 @@ let pp fmt annotation =
module Item = struct
(* Don't use nonrec due to https://github.com/janestreet/ppx_compare/issues/2 *)
(* type nonrec t = list (t, bool) [@@deriving compare]; *)
(** Annotation for one item: a list of annotations with visibility. *)
type t_ = (t * bool) list [@@deriving compare]

@ -8,6 +8,7 @@
(** The Smallfoot Intermediate Language: Annotations *)
open! IStd
module F = Format
type parameters = string list

@ -20,7 +20,8 @@ let iter_over_sorted_procs cfg ~f =
Typ.Procname.compare (Procdesc.get_proc_name pdesc1) (Procdesc.get_proc_name pdesc2)
in
Typ.Procname.Hash.fold (fun _ pdesc acc -> pdesc :: acc) cfg []
|> List.sort ~compare:compare_proc_desc_by_proc_name |> List.iter ~f
|> List.sort ~compare:compare_proc_desc_by_proc_name
|> List.iter ~f
let get_all_proc_names cfg =
@ -44,7 +45,8 @@ let iter_all_nodes ~sorted cfg ~f =
if not sorted then Typ.Procname.Hash.iter do_proc_desc cfg
else
iter_over_sorted_procs cfg ~f:(fun pdesc ->
Procdesc.get_nodes pdesc |> List.sort ~compare:Procdesc.Node.compare
Procdesc.get_nodes pdesc
|> List.sort ~compare:Procdesc.Node.compare
|> List.iter ~f:(fun node -> f pdesc node) )
@ -58,7 +60,8 @@ end)
let load source =
ResultsDatabase.with_registered_statement load_statement ~f:(fun db load_stmt ->
SourceFile.SQLite.serialize source |> Sqlite3.bind load_stmt 1
SourceFile.SQLite.serialize source
|> Sqlite3.bind load_stmt 1
|> SqliteUtils.check_result_code db ~log:"load bind source file" ;
SqliteUtils.result_single_column_option ~finalize:false ~log:"Cfg.load" db load_stmt
|> Option.map ~f:SQLite.deserialize )
@ -98,7 +101,8 @@ let inline_synthetic_method ((ret_id, _) as ret) etl pdesc loc_call : Sil.instr
| Sil.Store (Exp.Lfield (_, fn, ft), bt, _, _), [(* setter for fields *) (e1, _); (e2, _)] ->
let instr' = Sil.Store (Exp.Lfield (e1, fn, ft), bt, e2, loc_call) in
found instr instr'
| Sil.Store (Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, _, _), [(e1, _)] when Pvar.is_global pvar ->
| Sil.Store (Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, _, _), [(e1, _)] when Pvar.is_global pvar
->
(* setter for static fields *)
let instr' = Sil.Store (Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, e1, loc_call) in
found instr instr'

@ -50,7 +50,7 @@ let rec pp fmt = function
match builtin_functions_to_string pn with
| Some str ->
F.pp_print_string fmt str
| None ->
| None -> (
let procname_str = Typ.Procname.to_simplified_string pn in
match pn with
| Typ.Procname.ObjC_Cpp {kind= ObjCInstanceMethod}
@ -61,7 +61,7 @@ let rec pp fmt = function
| None ->
F.pp_print_string fmt procname_str )
| _ ->
F.pp_print_string fmt procname_str )
F.pp_print_string fmt procname_str ) )
| Dconst c ->
(Const.pp Pp.text) fmt c
| Dderef de ->
@ -148,7 +148,8 @@ let pp_vpath pe fmt vpath =
let rec has_tmp_var = function
| Dpvar pvar | Dpvaraddr pvar ->
Pvar.is_frontend_tmp pvar
| Dderef dexp | Ddot (dexp, _) | Darrow (dexp, _) | Dunop (_, dexp) | Dsizeof (_, Some dexp, _) ->
| Dderef dexp | Ddot (dexp, _) | Darrow (dexp, _) | Dunop (_, dexp) | Dsizeof (_, Some dexp, _)
->
has_tmp_var dexp
| Darray (dexp1, dexp2) | Dbinop (_, dexp1, dexp2) ->
has_tmp_var dexp1 || has_tmp_var dexp2

@ -221,7 +221,7 @@ let log_issue procname ~clang_method_kind severity err_log ~loc ~node ~session ~
let severity = Option.value error.severity ~default:severity in
let hide_java_loc_zero =
(* hide java errors at location zero unless in -developer_mode *)
not Config.developer_mode && Language.curr_language_is Java && Int.equal loc.Location.line 0
(not Config.developer_mode) && Language.curr_language_is Java && Int.equal loc.Location.line 0
in
let hide_memory_error =
match Localise.error_desc_get_bucket error.description with
@ -261,7 +261,7 @@ let log_issue procname ~clang_method_kind severity err_log ~loc ~node ~session ~
; source_location= loc }
in
EventLogger.log issue ) ;
if should_report && not hide_java_loc_zero && not hide_memory_error then
if should_report && (not hide_java_loc_zero) && not hide_memory_error then
let added =
let node_id, node_key =
match node with

@ -95,6 +95,17 @@ val update : t -> t -> unit
(** Update an old error log with a new one *)
val log_issue :
Typ.Procname.t -> clang_method_kind:ClangMethodKind.t option -> Exceptions.severity -> t
-> loc:Location.t -> node:node -> session:int -> ltr:loc_trace -> linters_def_file:string option
-> doc_url:string option -> access:string option -> extras:Jsonbug_t.extra option -> exn -> unit
Typ.Procname.t
-> clang_method_kind:ClangMethodKind.t option
-> Exceptions.severity
-> t
-> loc:Location.t
-> node:node
-> session:int
-> ltr:loc_trace
-> linters_def_file:string option
-> doc_url:string option
-> access:string option
-> extras:Jsonbug_t.extra option
-> exn
-> unit

@ -152,8 +152,14 @@ val print_exception_html : string -> exn -> unit
(** print a description of the exception to the html output *)
val pp_err :
Location.t -> severity -> IssueType.t -> Localise.error_desc -> Logging.ocaml_pos option
-> Format.formatter -> unit -> unit
Location.t
-> severity
-> IssueType.t
-> Localise.error_desc
-> Logging.ocaml_pos option
-> Format.formatter
-> unit
-> unit
(** pretty print an error *)
type t =

@ -274,9 +274,8 @@ let rec gen_free_vars =
gen_free_vars e
| Closure {captured_vars} ->
ISequence.gen_sequence_list captured_vars ~f:(fun (e, _, _) -> gen_free_vars e)
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _)
| Lvar _
| Sizeof {dynamic_length= None} ->
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _) | Lvar _ | Sizeof {dynamic_length= None}
->
return ()
| BinOp (_, e1, e2) | Lindex (e1, e2) ->
gen_free_vars e1 >>= fun () -> gen_free_vars e2

@ -32,14 +32,14 @@ let mk_procedure_name_filter ~filter =
match filter with
| None ->
(None, None)
| Some filter_string ->
| Some filter_string -> (
match String.lsplit2 ~on:':' filter_string with
| Some (source_file_filter, proc_name_filter) ->
(Some (Str.regexp source_file_filter), Some (Str.regexp proc_name_filter))
| None ->
(* if only one filter is supplied assume it's for procedure names and the source files are
a wildcard *)
(None, Some (Str.regexp filter_string))
(None, Some (Str.regexp filter_string)) )
in
let source_file_filter =
filter_of_regexp_opt ~to_string:SourceFile.to_string source_file_regexp

@ -57,11 +57,9 @@ let rec get_typ tenv = function
| BinaryOperator ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) ->
Some (Typ.mk (Typ.Tint Typ.IBool))
| BinaryOperator (_, e1, e2) -> (
match
(* TODO: doing this properly will require taking account of language-specific coercion
semantics. Only return a type when the operands have the same type for now *)
(get_typ tenv e1, get_typ tenv e2)
with
match (get_typ tenv e1, get_typ tenv e2) with
| Some typ1, Some typ2 when Typ.equal typ1 typ2 ->
Some typ1
| _ ->
@ -168,7 +166,8 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ =
(Exp.Lfield
( Var (Ident.create_normal (Ident.string_to_name (Exp.to_string root_exp)) 0)
, fld
, root_exp_typ )) typ )
, root_exp_typ ))
typ )
| Lindex (Const (Cstr s), index_exp) ->
(* indexed string literal (e.g., "foo"[1]). represent this by introducing a dummy variable
for the string literal. if you actually need to see the value of the string literal in the
@ -186,15 +185,16 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ =
of_sil_
(Exp.Lindex
( Var (Ident.create_normal (Ident.string_to_name (Exp.to_string root_exp)) 0)
, index_exp )) typ )
| Lvar _ ->
, index_exp ))
typ )
| Lvar _ -> (
match
AccessExpression.of_lhs_exp ~include_array_indexes ~add_deref exp typ ~f_resolve_id
with
| Some access_expr ->
AccessExpression access_expr
| None ->
L.(die InternalError) "Couldn't convert var expression %a to access path" Exp.pp exp
L.(die InternalError) "Couldn't convert var expression %a to access path" Exp.pp exp )
in
of_sil_ exp typ

@ -28,8 +28,12 @@ val get_typ : Tenv.t -> t -> Typ.t option
(** Get the type of the expression. Warning: not fully implemented *)
val of_sil :
include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessExpression.t option) -> add_deref:bool
-> Exp.t -> Typ.t -> t
include_array_indexes:bool
-> f_resolve_id:(Var.t -> AccessExpression.t option)
-> add_deref:bool
-> Exp.t
-> Typ.t
-> t
(** Convert SIL expression to HIL expression *)
val get_access_exprs : t -> AccessExpression.t list

@ -77,23 +77,21 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =
| AccessExpression access_expr ->
access_expr
| BinaryOperator (_, exp0, exp1) -> (
match
(* pointer arithmetic. somewhere in one of the expressions, there should be at least
one pointer type represented as an access path. just use that access path and forget
about the arithmetic. if you need to model this more precisely, you should be using
SIL instead *)
HilExp.get_access_exprs exp0
with
match HilExp.get_access_exprs exp0 with
| ap :: _ ->
ap
| [] ->
| [] -> (
match HilExp.get_access_exprs exp1 with
| ap :: _ ->
ap
| [] ->
L.(die InternalError)
"Invalid pointer arithmetic expression %a used as LHS at %a" Exp.pp lhs_exp
Location.pp_file_pos loc )
Location.pp_file_pos loc ) )
| Constant (Const.Cint i) ->
(* this can happen in intentionally crashing code like *0xdeadbeef = 0 used for
debugging. doesn't really matter what we do here, so just create a dummy var *)

@ -30,7 +30,9 @@ type translation =
| Ignore (** no-op *)
val of_sil :
include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessExpression.t option) -> Sil.instr
include_array_indexes:bool
-> f_resolve_id:(Var.t -> AccessExpression.t option)
-> Sil.instr
-> translation
(** convert an SIL instruction into an HIL instruction. The [f_resolve_id] function should map an
SSA temporary variable to the access path it represents. Evaluating the HIL instruction should

@ -139,9 +139,7 @@ module NameGenerator = struct
let stamp = NameHash.find !name_map name in
NameHash.replace !name_map name (stamp + 1) ;
stamp + 1
with Caml.Not_found ->
NameHash.add !name_map name 0 ;
0
with Caml.Not_found -> NameHash.add !name_map name 0 ; 0
in
{kind; name; stamp}

@ -70,7 +70,9 @@ let filter_map (NotReversed instrs) ~f = NotReversed (Array.filter_map instrs ~f
let map_changed =
let aux_changed arr ~f i =
for i = i to Array.length arr - 1 do Array.unsafe_get arr i |> f |> Array.unsafe_set arr i done ;
for i = i to Array.length arr - 1 do
Array.unsafe_get arr i |> f |> Array.unsafe_set arr i
done ;
arr
in
let rec aux_unchanged ~equal arr ~f i =

@ -28,7 +28,9 @@ val of_rev_list : Sil.instr list -> not_reversed_t
val filter_map : not_reversed_t -> f:(Sil.instr -> Sil.instr option) -> not_reversed_t
val map_changed :
equal:(Sil.instr -> Sil.instr -> bool) -> not_reversed_t -> f:(Sil.instr -> Sil.instr)
equal:(Sil.instr -> Sil.instr -> bool)
-> not_reversed_t
-> f:(Sil.instr -> Sil.instr)
-> not_reversed_t
val reverse_order : not_reversed_t -> reversed t

@ -81,9 +81,9 @@ let iszero (_, i, _) = Int64.equal i 0L
let isnull (_, i, ptr) = Int64.equal i 0L && ptr
let isminusone (unsigned, i, _) = not unsigned && Int64.equal i (-1L)
let isminusone (unsigned, i, _) = (not unsigned) && Int64.equal i (-1L)
let isnegative (unsigned, i, _) = not unsigned && i < 0L
let isnegative (unsigned, i, _) = (not unsigned) && i < 0L
let neg (unsigned, i, ptr) = (unsigned, Int64.neg i, ptr)

@ -28,8 +28,13 @@ module Html : sig
(** Open an Html file to append data *)
val pp_line_link :
?with_name:bool -> ?text:string option -> SourceFile.t -> DB.Results_dir.path
-> Format.formatter -> int -> unit
?with_name:bool
-> ?text:string option
-> SourceFile.t
-> DB.Results_dir.path
-> Format.formatter
-> int
-> unit
(** Print an html link to the given line number of the current source file *)
val pp_hline : Format.formatter -> unit -> unit
@ -39,8 +44,17 @@ module Html : sig
(** Print end color *)
val pp_node_link :
DB.Results_dir.path -> Typ.Procname.t -> description:string -> preds:int list -> succs:int list
-> exn:int list -> isvisited:bool -> isproof:bool -> Format.formatter -> int -> unit
DB.Results_dir.path
-> Typ.Procname.t
-> description:string
-> preds:int list
-> succs:int list
-> exn:int list
-> isvisited:bool
-> isproof:bool
-> Format.formatter
-> int
-> unit
(** Print an html link to the given node.
Usage: [pp_node_link path_to_root ... fmt id].
[path_to_root] is the path to the dir for the procedure in the spec db.
@ -50,8 +64,13 @@ module Html : sig
(** Print an html link to the given proc *)
val pp_session_link :
?with_name:bool -> ?proc_name:Typ.Procname.t -> SourceFile.t -> string list -> Format.formatter
-> int * int * int -> unit
?with_name:bool
-> ?proc_name:Typ.Procname.t
-> SourceFile.t
-> string list
-> Format.formatter
-> int * int * int
-> unit
(** Print an html link given node id and session *)
val pp_start_color : Format.formatter -> Pp.color -> unit

@ -260,7 +260,8 @@ let deref_str_undef (proc_name, loc) =
; value_post= None
; problem_str=
"could be assigned by a call to skip function " ^ proc_name_str
^ at_line_tag tags Tags.call_line loc ^ " and is dereferenced or freed" }
^ at_line_tag tags Tags.call_line loc
^ " and is dereferenced or freed" }
(** dereference strings for a freed pointer dereference *)
@ -447,12 +448,14 @@ let dereference_string proc_name deref_str value_str access_opt loc =
"is annotated with " ^ annotation_name ^ " and is dereferenced without a null check"
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 ->
if String.equal weak_var_str value_str then
"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
"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"
| None, None ->
deref_str.problem_str
@ -460,7 +463,7 @@ let dereference_string proc_name deref_str value_str access_opt loc =
[problem_str ^ " " ^ at_line tags loc]
in
let access_desc = access_desc access_opt in
{no_desc with descriptions= value_desc :: access_desc @ problem_desc; tags= !tags}
{no_desc with descriptions= (value_desc :: access_desc) @ problem_desc; tags= !tags}
let parameter_field_not_null_checked_desc (desc : error_desc) exp =
@ -518,8 +521,10 @@ let desc_allocation_mismatch alloc dealloc =
else
" by call to " ^ MF.monospaced_to_string (Typ.Procname.to_simplified_string called_pname)
in
"using " ^ MF.monospaced_to_string (Typ.Procname.to_simplified_string primitive_pname)
^ by_call ^ " " ^ at_line (Tags.create ()) (* ignore the tag *) loc
"using "
^ MF.monospaced_to_string (Typ.Procname.to_simplified_string primitive_pname)
^ by_call ^ " "
^ at_line (Tags.create ()) (* ignore the tag *) loc
in
let description =
Format.sprintf "%s %s is deallocated %s" mem_dyn_allocated (using alloc) (using dealloc)
@ -631,7 +636,8 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
| None ->
("", "", "")
| Some s ->
Tags.update tags Tags.value s ; (MF.monospaced_to_string s, " to ", " on ")
Tags.update tags Tags.value s ;
(MF.monospaced_to_string s, " to ", " on ")
in
let typ_str =
match hpred_type_opt with
@ -672,7 +678,7 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
match bucket_opt with Some bucket when Config.show_buckets -> bucket | _ -> ""
in
{ no_desc with
descriptions= bucket_str :: xxx_allocated_to @ by_call_to @ is_not_rxxx_after; tags= !tags }
descriptions= (bucket_str :: xxx_allocated_to) @ by_call_to @ is_not_rxxx_after; tags= !tags }
let desc_buffer_overrun desc = verbatim_desc desc
@ -724,8 +730,8 @@ let desc_registered_observer_being_deallocated pvar loc =
let obj_str = MF.monospaced_to_string (Pvar.to_string pvar) in
{ no_desc with
descriptions=
[ registered_observer_being_deallocated_str obj_str ^ at_line tags loc
^ ". Being still registered as observer of the notification "
[ registered_observer_being_deallocated_str obj_str
^ at_line tags loc ^ ". Being still registered as observer of the notification "
^ "center, the deallocated object " ^ obj_str ^ " may be notified in the future." ]
; tags= !tags }

@ -113,7 +113,8 @@ val is_parameter_not_null_checked_desc : error_desc -> bool
val is_field_not_null_checked_desc : error_desc -> bool
val desc_allocation_mismatch :
Typ.Procname.t * Typ.Procname.t * Location.t -> Typ.Procname.t * Typ.Procname.t * Location.t
Typ.Procname.t * Typ.Procname.t * Location.t
-> Typ.Procname.t * Typ.Procname.t * Location.t
-> error_desc
val desc_class_cast_exception :
@ -136,8 +137,13 @@ val is_empty_vector_access_desc : error_desc -> bool
val desc_frontend_warning : string -> string option -> Location.t -> error_desc
val desc_leak :
Exp.t option -> string option -> PredSymb.resource option -> PredSymb.res_action option
-> Location.t -> string option -> error_desc
Exp.t option
-> string option
-> PredSymb.resource option
-> PredSymb.res_action option
-> Location.t
-> string option
-> error_desc
val desc_buffer_overrun : string -> error_desc

@ -19,7 +19,9 @@ let equal = [%compare.equal : t]
let from_string (s : string) = {plain= s; mangled= None}
(** Create a mangled name from a plain and mangled string *)
let mangled (plain: string) (mangled: string) = {plain; mangled= Some (plain ^ "{" ^ mangled ^ "}")}
let mangled (plain : string) (mangled : string) =
{plain; mangled= Some (plain ^ "{" ^ mangled ^ "}")}
(** Convert a mangled name to a string *)
let to_string (pn : t) = pn.plain

@ -221,8 +221,11 @@ let to_string pe = function
let str_vpath =
if Config.trace_error then F.asprintf "%a" (DecompiledExp.pp_vpath pe) ra.ra_vpath else ""
in
name ^ Binop.str pe Lt ^ Typ.Procname.to_string ra.ra_pname ^ ":"
^ string_of_int ra.ra_loc.Location.line ^ Binop.str pe Gt ^ str_vpath
name ^ Binop.str pe Lt
^ Typ.Procname.to_string ra.ra_pname
^ ":"
^ string_of_int ra.ra_loc.Location.line
^ Binop.str pe Gt ^ str_vpath
| Aautorelease ->
"AUTORELEASE"
| Adangling dk ->

@ -160,7 +160,8 @@ module Node = struct
let get_siblings node =
get_preds node
|> ISequence.gen_sequence_list ~f:(fun parent ->
get_succs parent |> Sequence.of_list |> Sequence.filter ~f:(fun n -> not (equal node n))
get_succs parent |> Sequence.of_list
|> Sequence.filter ~f:(fun n -> not (equal node n))
|> Sequence.Generator.of_sequence )
|> Sequence.Generator.run
@ -182,8 +183,7 @@ module Node = struct
let find_in_node_or_preds =
let rec find ~f visited nodes =
match nodes with
| node :: nodes when not (NodeSet.mem node visited)
-> (
| node :: nodes when not (NodeSet.mem node visited) -> (
let instrs = get_instrs node in
match Instrs.find_map ~f:(f node) instrs with
| Some res ->
@ -374,7 +374,8 @@ module Node = struct
in
Some instr_key
in
get_instrs node |> IContainer.rev_filter_map_to_list ~fold:Instrs.fold ~f:add_instr
get_instrs node
|> IContainer.rev_filter_map_to_list ~fold:Instrs.fold ~f:add_instr
|> Utils.better_hash
@ -769,7 +770,8 @@ let specialize_types_proc callee_pdesc resolved_pdesc substitutions =
in
subst_map := Ident.Map.add id specialized_typname !subst_map ;
Some (Sil.Load (id, convert_exp origin_exp, mk_ptr_typ specialized_typname, loc))
| Sil.Load (id, (Exp.Var origin_id as origin_exp), ({Typ.desc= Tstruct _} as origin_typ), loc) ->
| Sil.Load (id, (Exp.Var origin_id as origin_exp), ({Typ.desc= Tstruct _} as origin_typ), loc)
->
let updated_typ : Typ.t =
try Typ.mk ~default:origin_typ (Tstruct (Ident.Map.find origin_id !subst_map))
with Caml.Not_found -> origin_typ
@ -918,7 +920,7 @@ let specialize_with_block_args_instrs resolved_pdesc substitutions =
in
let closure = Exp.Closure {name= block_name; captured_vars= id_exp_typs} in
let instr = Sil.Store (assignee_exp, origin_typ, closure, loc) in
(remove_temps_instr :: instr :: load_instrs @ instrs, id_map)
((remove_temps_instr :: instr :: load_instrs) @ instrs, id_map)
| Sil.Store (assignee_exp, origin_typ, origin_exp, loc) ->
let set_instr =
Sil.Store (convert_exp assignee_exp, origin_typ, convert_exp origin_exp, loc)
@ -942,7 +944,7 @@ let specialize_with_block_args_instrs resolved_pdesc substitutions =
, loc
, call_flags )
in
let instrs = remove_temps_instr :: call_instr :: load_instrs @ instrs in
let instrs = (remove_temps_instr :: call_instr :: load_instrs) @ instrs in
(instrs, id_map)
with Caml.Not_found ->
convert_generic_call return_ids (Exp.Var id) origin_args loc call_flags )
@ -972,8 +974,8 @@ let specialize_with_block_args callee_pdesc pname_with_block_args block_args =
(* Substitution from a block parameter to the block name and the new formals
that correspond to the captured variables *)
let substitutions : (Typ.Procname.t * (Mangled.t * Typ.t) list) Mangled.Map.t =
List.fold2_exn callee_attributes.formals block_args ~init:Mangled.Map.empty ~f:
(fun subts (param_name, _) block_arg_opt ->
List.fold2_exn callee_attributes.formals block_args ~init:Mangled.Map.empty
~f:(fun subts (param_name, _) block_arg_opt ->
match block_arg_opt with
| Some (cl : Exp.closure) ->
let formals_from_captured =
@ -1044,8 +1046,7 @@ let is_connected proc_desc =
in
let rec is_consecutive_join_nodes n visited =
match Node.get_kind n with
| Node.Join_node
-> (
| Node.Join_node -> (
if NodeSet.mem n visited then false
else
let succs = Node.get_succs n in
@ -1064,7 +1065,7 @@ let is_connected proc_desc =
| Node.Start_node _ ->
if List.is_empty succs || not (List.is_empty preds) then Error `Other else Ok ()
| Node.Exit_node _ ->
if not (List.is_empty succs) || List.is_empty preds then Error `Other else Ok ()
if (not (List.is_empty succs)) || List.is_empty preds then Error `Other else Ok ()
| Node.Stmt_node _ | Node.Prune_node _ | Node.Skip_node _ ->
if List.is_empty succs || List.is_empty preds then Error `Other else Ok ()
| Node.Join_node ->
@ -1075,7 +1076,7 @@ let is_connected proc_desc =
introduce a sequence of join nodes *)
if
(List.is_empty preds && not (is_consecutive_join_nodes n NodeSet.empty))
|| (not (List.is_empty preds) && List.is_empty succs)
|| ((not (List.is_empty preds)) && List.is_empty succs)
then Error `Join
else Ok ()
in

@ -85,10 +85,14 @@ type ( 'f_in
type ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, 'list_constraint) templ_matcher
=
{ on_objc_cpp:
'context -> 'f_in -> objc_cpp
'context
-> 'f_in
-> objc_cpp
-> ('f_out * 'captured_types capt * Typ.template_arg list) option
; on_templated_name:
'context -> 'f_in -> templated_name
'context
-> 'f_in
-> templated_name
-> ('f_out * 'captured_types capt * Typ.template_arg list) option
; get_markers: 'markers_in -> 'markers_out }
@ -120,8 +124,8 @@ let empty : ('context, 'f, 'f, unit, 'markers, 'markers, empty) path_matcher =
{on_templated_name; path_extra= PathEmpty; get_markers}
let name_cons
: ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, _) path_matcher
let name_cons :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, _) path_matcher
-> string
-> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher =
fun m name ->
@ -144,8 +148,8 @@ let name_cons
{on_objc_cpp; on_qual_name; get_markers}
let name_cons_f
: ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, _) path_matcher
let name_cons_f :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, _) path_matcher
-> ('context -> string -> bool)
-> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher =
fun m f_name ->
@ -165,29 +169,23 @@ let name_cons_f
{on_objc_cpp; on_qual_name; get_markers}
let all_names_cons
: ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, non_empty) path_matcher
-> ( 'context
, 'f_in
, 'f_out
, 'captured_tpes
, 'markers_in
, 'markers_out
, non_empty )
path_matcher =
let all_names_cons :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, non_empty) path_matcher
-> ('context, 'f_in, 'f_out, 'captured_tpes, 'markers_in, 'markers_out, non_empty) path_matcher
=
fun m ->
let {on_templated_name; get_markers; path_extra= PathNonEmpty {on_objc_cpp}} = m in
let rec on_templated_name_rec context f templated_name =
match on_templated_name context f templated_name with
| Some _ as some ->
some
| None ->
| None -> (
let qual_name, _template_args = templated_name in
match QualifiedCppName.extract_last qual_name with
| None ->
None
| Some (_last, rest) ->
on_templated_name_rec context f (rest, [])
on_templated_name_rec context f (rest, []) )
in
let on_templated_name = on_templated_name_rec in
let on_objc_cpp context f (objc_cpp : Typ.Procname.ObjC_Cpp.t) =
@ -200,8 +198,8 @@ let all_names_cons
{on_templated_name; get_markers; path_extra= PathNonEmpty {on_objc_cpp}}
let templ_begin
: ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
let templ_begin :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
-> ( 'context
, 'f_in
, 'f_out
@ -230,8 +228,8 @@ let templ_begin
{on_objc_cpp; on_templated_name; get_markers}
let templ_cons
: ( 'context
let templ_cons :
( 'context
, 'f_in
, 'f_interm
, 'captured_types_in
@ -247,14 +245,8 @@ let templ_cons
, 'markers_interm
, 'lc )
template_arg
-> ( 'context
, 'f_in
, 'f_out
, 'captured_types_out
, 'markers_in
, 'markers_out
, 'lc )
templ_matcher =
-> ('context, 'f_in, 'f_out, 'captured_types_out, 'markers_in, 'markers_out, 'lc) templ_matcher
=
fun m template_arg ->
let {on_objc_cpp; on_templated_name; get_markers} = m in
let {eat_template_arg; add_marker} = template_arg in
@ -268,8 +260,8 @@ let templ_cons
{on_objc_cpp; on_templated_name; get_markers}
let templ_end
: ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, _) templ_matcher
let templ_end :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, _) templ_matcher
-> ( 'context
, 'f_in
, 'f_out
@ -381,7 +373,8 @@ module type Common = sig
val ( >:: ) :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, _) templ_matcher
-> string -> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
-> string
-> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
(** Ends template arguments and starts a name *)
val ( &+...>:: ) :
@ -392,17 +385,20 @@ module type Common = sig
, 'markers_in
, 'markers_out
, accept_more )
templ_matcher -> string
templ_matcher
-> string
-> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
(** Ends template arguments with eats-ALL and starts a name *)
val ( &:: ) :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher -> string
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
-> string
-> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
(** Separates names (accepts ALL template arguments on the left one) *)
val ( <>:: ) :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher -> string
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
-> string
-> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
(** Separates names (accepts NO template arguments on the left one) *)
end
@ -413,15 +409,15 @@ module Common = struct
let add_no_marker capture_markers = capture_markers
(** Eats all template args *)
let any_template_args
: ('f, 'f, 'captured_types, 'captured_types, 'markers, 'markers, end_of_list) template_arg =
let any_template_args :
('f, 'f, 'captured_types, 'captured_types, 'markers, 'markers, end_of_list) template_arg =
let eat_template_arg (f, captured_types, _) = Some (f, captured_types, []) in
{eat_template_arg; add_marker= add_no_marker}
(** Eats a type *)
let any_typ
: ('f, 'f, 'captured_types, 'captured_types, 'markers, 'markers, accept_more) template_arg =
let any_typ :
('f, 'f, 'captured_types, 'captured_types, 'markers, 'markers, accept_more) template_arg =
let eat_template_arg (f, captured_types, template_args) =
match template_args with Typ.TType _ :: rest -> Some (f, captured_types, rest) | _ -> None
in
@ -429,8 +425,8 @@ module Common = struct
(** Captures a type than can be back-referenced *)
let capt_typ
: 'marker
let capt_typ :
'marker
-> ( 'marker mtyp -> 'f
, 'f
, 'captured_types
@ -453,8 +449,8 @@ module Common = struct
(** Captures an int *)
let capt_int
: ( Int64.t -> 'f
let capt_int :
( Int64.t -> 'f
, 'f
, 'captured_types
, 'captured_types
@ -469,8 +465,8 @@ module Common = struct
(** Captures all template args *)
let capt_all
: ( Typ.template_arg list -> 'f
let capt_all :
( Typ.template_arg list -> 'f
, 'f
, 'captured_types
, 'captured_types
@ -580,8 +576,11 @@ module Call = struct
let pre_map_opt opt ~f = match opt with None -> DoesNotMatch | Some x -> Matches (f x)
type ('context, 'f_in, 'f_out, 'captured_types) func_args_end =
on_args:('context, 'f_in, 'f_out, 'captured_types) on_args -> 'context -> FuncArg.t list
-> 'f_in * 'captured_types -> ('context, 'f_out) pre_result
on_args:('context, 'f_in, 'f_out, 'captured_types) on_args
-> 'context
-> FuncArg.t list
-> 'f_in * 'captured_types
-> ('context, 'f_out) pre_result
type ('context, 'f_in, 'f_out) all_args_matcher =
{ on_objc_cpp: 'context -> 'f_in -> objc_cpp -> FuncArg.t list -> ('context, 'f_out) pre_result
@ -590,8 +589,8 @@ module Call = struct
type ('context, 'f) dispatcher = 'context -> Typ.Procname.t -> FuncArg.t list -> 'f option
let args_begin
: ('context, 'f_in, 'f_out, 'captured_types, unit, 'markers, non_empty) path_matcher
let args_begin :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers, non_empty) path_matcher
-> ('context, 'f_in, 'f_out, 'f_out, 'captured_types, 'markers) args_matcher =
let on_args _context _capt f_args = Some f_args in
fun m ->
@ -612,8 +611,8 @@ module Call = struct
{on_proc; on_args; markers}
let args_cons
: ('context, 'f_in, 'f_proc_out, 'f_interm, 'captured_types, 'markers) args_matcher
let args_cons :
('context, 'f_in, 'f_proc_out, 'f_interm, 'captured_types, 'markers) args_matcher
-> ('context, 'f_interm, 'f_out, 'captured_types, 'markers) func_arg
-> ('context, 'f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher =
fun m func_arg ->
@ -626,8 +625,8 @@ module Call = struct
{on_proc; on_args; markers}
let args_end
: ('context, 'f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher
let args_end :
('context, 'f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher
-> ('context, 'f_proc_out, 'f_out, 'captured_types) func_args_end
-> ('context, 'f_in, 'f_out) all_args_matcher =
fun m func_args_end ->
@ -644,10 +643,10 @@ module Call = struct
{on_c; on_java; on_objc_cpp}
let make_matcher
: ('context, 'f_in, 'f_out) all_args_matcher -> 'f_in -> ('context, 'f_out) matcher =
let make_matcher :
('context, 'f_in, 'f_out) all_args_matcher -> 'f_in -> ('context, 'f_out) matcher =
fun m f ->
let {on_c; on_java; on_objc_cpp} : (_, _, _) all_args_matcher = m in
let ({on_c; on_java; on_objc_cpp} : (_, _, _) all_args_matcher) = m in
let on_objc_cpp context objc_cpp args =
match on_objc_cpp context f objc_cpp args with
| DoesNotMatch ->
@ -713,8 +712,10 @@ module Call = struct
{match_arg; marker_static_checker= no_marker_checker}
let mk_match_typ_nth
: ('markers -> 'marker) -> ('captured_types -> 'marker mtyp) -> 'marker
let mk_match_typ_nth :
('markers -> 'marker)
-> ('captured_types -> 'marker mtyp)
-> 'marker
-> ('context, 'captured_types, 'markers) one_arg_matcher =
fun get_m get_c marker ->
let marker_static_checker markers = Polymorphic_compare.( = ) marker (get_m markers) in
@ -729,25 +730,26 @@ module Call = struct
(** Matches second captured type *)
let match_typ2 : 'marker -> ('context, _ * ('marker mtyp * _), _ * ('marker * _)) one_arg_matcher =
let match_typ2 : 'marker -> ('context, _ * ('marker mtyp * _), _ * ('marker * _)) one_arg_matcher
=
let pos2 (_, (x, _)) = x in
fun marker -> mk_match_typ_nth pos2 pos2 marker
(** Matches third captured type *)
let match_typ3
: 'marker
-> ('context, _ * (_ * ('marker mtyp * _)), _ * (_ * ('marker * _))) one_arg_matcher =
let match_typ3 :
'marker -> ('context, _ * (_ * ('marker mtyp * _)), _ * (_ * ('marker * _))) one_arg_matcher
=
let pos3 (_, (_, (x, _))) = x in
fun marker -> mk_match_typ_nth pos3 pos3 marker
(** Matches the type matched by the given path_matcher *)
let match_typ
: ('context, _, _, unit, unit, unit, non_empty) path_matcher
let match_typ :
('context, _, _, unit, unit, unit, non_empty) path_matcher
-> ('context, _, _) one_arg_matcher =
fun m ->
let {on_templated_name} : (_, _, _, unit, unit, unit, non_empty) path_matcher = m in
let ({on_templated_name} : (_, _, _, unit, unit, unit, non_empty) path_matcher) = m in
let rec match_typ context typ =
match typ with
| {Typ.desc= Tstruct name} ->
@ -762,6 +764,7 @@ module Call = struct
(* Function argument capture *)
(** Do not capture this argument *)
let no_capture : (_, _, 'f, 'f) arg_capture =
let get_captured_value _arg = () in
@ -802,8 +805,8 @@ module Call = struct
{on_empty; wrapper}
let make_arg
: ('arg_in, 'arg_out, 'f_in, 'f_out) arg_preparer
let make_arg :
('arg_in, 'arg_out, 'f_in, 'f_out) arg_preparer
-> ('context, 'arg_in, 'arg_out, 'f_in, 'f_out, _, _) one_arg
-> ('context, 'f_in, 'f_out, _, _) func_arg =
fun arg_preparer one_arg ->
@ -856,6 +859,7 @@ module Call = struct
(* Function args end *)
(** Matches if there is no function arguments left *)
let no_args_left : ('context, _, _, _) func_args_end =
let match_empty_args = function Some (f, []) -> Matches f | _ -> DoesNotMatch in
@ -868,8 +872,8 @@ module Call = struct
(** If [func_args_end1] does not match, use [func_args_end2] *)
let alternative_args_end
: ('context, 'f_in, 'f_out, 'captured_types) func_args_end
let alternative_args_end :
('context, 'f_in, 'f_out, 'captured_types) func_args_end
-> ('context, 'f_in, 'f_out, 'captured_types) func_args_end
-> ('context, 'f_in, 'f_out, 'captured_types) func_args_end =
fun func_args_end1 func_args_end2 ~on_args context args f_capt ->
@ -952,19 +956,23 @@ module type NameCommon = sig
include Common
val ( >--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers, _) templ_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers, _) templ_matcher
-> 'f_in
-> ('context, 'f_out) matcher
val ( <>--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
val ( &--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
val ( &::.*--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates),
accepts ALL function arguments, binds the function *)
@ -977,12 +985,13 @@ module NameCommon = struct
{ on_templated_name: 'context -> templated_name -> 'f option
; on_objc_cpp: 'context -> objc_cpp -> 'f option }
let make_matcher
: ('context, 'f_in, 'f_out, _, _, _, non_empty) path_matcher -> 'f_in
let make_matcher :
('context, 'f_in, 'f_out, _, _, _, non_empty) path_matcher
-> 'f_in
-> ('context, 'f_out) matcher =
fun m f ->
let {on_templated_name; path_extra= PathNonEmpty {on_objc_cpp}}
: ('context, 'f_in, 'f_out, _, _, _, non_empty) path_matcher =
let ({on_templated_name; path_extra= PathNonEmpty {on_objc_cpp}}
: ('context, 'f_in, 'f_out, _, _, _, non_empty) path_matcher) =
m
in
let on_templated_name context templated_name =

@ -142,7 +142,8 @@ module type Common = sig
val ( >:: ) :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, _) templ_matcher
-> string -> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
-> string
-> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
(** Ends template arguments and starts a name *)
val ( &+...>:: ) :
@ -153,17 +154,20 @@ module type Common = sig
, 'markers_in
, 'markers_out
, accept_more )
templ_matcher -> string
templ_matcher
-> string
-> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
(** Ends template arguments with eats-ALL and starts a name *)
val ( &:: ) :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher -> string
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
-> string
-> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
(** Separates names (accepts ALL template arguments on the left one) *)
val ( <>:: ) :
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher -> string
('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
-> string
-> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher
(** Separates names (accepts NO template arguments on the left one) *)
end
@ -172,19 +176,23 @@ module type NameCommon = sig
include Common
val ( >--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers, _) templ_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers, _) templ_matcher
-> 'f_in
-> ('context, 'f_out) matcher
val ( <>--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
val ( &--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
val ( &::.*--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates),
accepts ALL function arguments, binds the function *)
@ -192,7 +200,8 @@ end
(* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
include sig
include
sig
[@@@warning "-60"]
module ProcName :
@ -207,9 +216,9 @@ module Call : sig
type t = Exp.t * Typ.t
end
include Common
with type ('context, 'f) dispatcher =
'context -> Typ.Procname.t -> FuncArg.t list -> 'f option
include
Common
with type ('context, 'f) dispatcher = 'context -> Typ.Procname.t -> FuncArg.t list -> 'f option
type ('context, 'f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher
@ -270,7 +279,8 @@ module Call : sig
(** Ends template arguments and starts function arguments *)
val ( $--> ) :
('context, 'f_in, _, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in
('context, 'f_in, _, 'f_out, 'captured_types, 'markers) args_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** Ends function arguments, binds the function *)
@ -287,48 +297,57 @@ module Call : sig
(** Ends a name with accept-NO template arguments and starts function arguments *)
val ( >--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers, _) templ_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers, _) templ_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** Ends template arguments, accepts ALL function arguments, binds the function *)
val ( $+...$--> ) :
('context, 'f_in, _, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in
('context, 'f_in, _, 'f_out, 'captured_types, 'markers) args_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** Ends function arguments with eats-ALL and binds the function *)
val ( >$$--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers, _) templ_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers, _) templ_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** Ends template arguments, accepts NO function arguments, binds the function *)
val ( $$--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** After a name, accepts ALL template arguments, accepts NO function arguments, binds the function *)
val ( <>$$--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** After a name, accepts NO template arguments, accepts NO function arguments, binds the function *)
val ( &--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** After a name, accepts ALL template arguments, accepts ALL function arguments, binds the function *)
val ( <>--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** After a name, accepts NO template arguments, accepts ALL function arguments, binds the function *)
val ( &::.*--> ) :
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in
('context, 'f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** After a name, accepts ALL template arguments, accepts ALL path tails (names, templates),
accepts ALL function arguments, binds the function *)
val ( $!--> ) :
('context, 'f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in
('context, 'f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher
-> 'f_in
-> ('context, 'f_out) matcher
(** Ends function arguments, accepts NO more function arguments.
If the args do not match, raise an internal error.

@ -93,8 +93,13 @@ val mk_callee : Mangled.t -> Typ.Procname.t -> t
for a callee function with the given function name *)
val mk_global :
?is_constexpr:bool -> ?is_pod:bool -> ?is_static_local:bool -> ?is_static_global:bool
-> ?translation_unit:SourceFile.t -> Mangled.t -> t
?is_constexpr:bool
-> ?is_pod:bool
-> ?is_static_local:bool
-> ?is_static_global:bool
-> ?translation_unit:SourceFile.t
-> Mangled.t
-> t
(** create a global variable with the given name *)
val mk_tmp : string -> Typ.Procname.t -> t

@ -94,7 +94,7 @@ module Match = struct
let colon_splits = String.split qual_name ~on:':' in
List.iter colon_splits ~f:(fun s ->
(* Filter out the '<' in operator< and operator<= *)
if not (String.is_prefix s ~prefix:"operator<") && String.contains s '<' then
if (not (String.is_prefix s ~prefix:"operator<")) && String.contains s '<' then
raise (ParseError ("Unexpected template in fuzzy qualified name %s." ^ qual_name)) ) ;
of_qual_string qual_name

@ -573,14 +573,14 @@ end = struct
env.todo <- todo' ;
let n, emitted = HparaHash.find env.hash hpara in
if not emitted then f n hpara
| [] ->
| [] -> (
match env.todo_dll with
| hpara_dll :: todo_dll' ->
env.todo_dll <- todo_dll' ;
let n, emitted = HparaDllHash.find env.hash_dll hpara_dll in
if not emitted then f_dll n hpara_dll
| [] ->
()
() )
done
end
@ -1180,7 +1180,9 @@ let sub_filter_pair = List.filter
(** [sub_range_partition filter sub] partitions [sub] according to
whether range expressions satisfy [filter]. *)
let sub_range_partition filter (sub: exp_subst) = List.partition_tf ~f:(fun (_, e) -> filter e) sub
let sub_range_partition filter (sub : exp_subst) =
List.partition_tf ~f:(fun (_, e) -> filter e) sub
(** [sub_domain_partition filter sub] partitions [sub] according to
whether domain identifiers satisfy [filter]. *)
@ -1238,8 +1240,7 @@ let rec exp_sub_ids (f: subst_fun) exp =
if phys_equal e' e then exp else Exp.Exn e'
| Closure c ->
let captured_vars =
IList.map_changed
~equal:[%compare.equal : Exp.t * Pvar.t * Typ.t]
IList.map_changed ~equal:[%compare.equal: Exp.t * Pvar.t * Typ.t]
~f:(fun ((e, pvar, typ) as captured) ->
let e' = exp_sub_ids f e in
let typ' = f_typ typ in
@ -1333,8 +1334,7 @@ let instr_sub_ids ~sub_id_binders f instr =
in
let fun_exp' = exp_sub_ids f fun_exp in
let actuals' =
IList.map_changed
~equal:[%compare.equal : Exp.t * Typ.t]
IList.map_changed ~equal:[%compare.equal: Exp.t * Typ.t]
~f:(fun ((actual, typ) as actual_pair) ->
let actual' = exp_sub_ids f actual in
let typ' = sub_typ typ in
@ -1375,7 +1375,7 @@ let rec exp_replace_exp epairs e =
match List.find ~f:(fun (e1, _) -> Exp.equal e e1) epairs with
| Some (_, e2) ->
e2
| None ->
| None -> (
(* If e is a compound expression, we need to check for its subexpressions as well *)
match e with
| Exp.UnOp (op, e0, ty) ->
@ -1396,7 +1396,7 @@ let rec exp_replace_exp epairs e =
let index' = exp_replace_exp epairs index in
if phys_equal base base' && phys_equal index index' then e else Exp.Lindex (base', index')
| _ ->
e
e )
let atom_replace_exp epairs atom = atom_expmap (fun e -> exp_replace_exp epairs e) atom
@ -1568,7 +1568,7 @@ let hpara_instantiate para e1 e2 elist =
in
let subst =
`Exp
(exp_subst_of_list ((para.root, e1) :: (para.next, e2) :: subst_for_svars @ subst_for_evars))
(exp_subst_of_list (((para.root, e1) :: (para.next, e2) :: subst_for_svars) @ subst_for_evars))
in
(ids_evars, List.map ~f:(hpred_sub subst) para.body)
@ -1594,7 +1594,7 @@ let hpara_dll_instantiate (para: hpara_dll) cell blink flink elist =
let subst =
`Exp
(exp_subst_of_list
( (para.cell, cell) :: (para.blink, blink) :: (para.flink, flink) :: subst_for_svars
( ((para.cell, cell) :: (para.blink, blink) :: (para.flink, flink) :: subst_for_svars)
@ subst_for_evars ))
in
(ids_evars, List.map ~f:(hpred_sub subst) para.body_dll)

@ -8,6 +8,7 @@
(** The Smallfoot Intermediate Language *)
open! IStd
module F = Format
(** {2 Programs and Types} *)

@ -23,7 +23,8 @@ let select_existing_statement =
let get_existing_data source_file =
ResultsDatabase.with_registered_statement select_existing_statement ~f:(fun db stmt ->
SourceFile.SQLite.serialize source_file |> Sqlite3.bind stmt 1
SourceFile.SQLite.serialize source_file
|> Sqlite3.bind stmt 1
(* :source *)
|> SqliteUtils.check_result_code db ~log:"get_existing_data bind source file" ;
SqliteUtils.result_option ~finalize:false db ~log:"looking for pre-existing cfgs" stmt
@ -53,7 +54,8 @@ let add source_file cfg tenv =
sure that all attributes were written to disk (but not necessarily flushed) *)
Cfg.save_attributes source_file cfg ;
ResultsDatabase.with_registered_statement store_statement ~f:(fun db store_stmt ->
SourceFile.SQLite.serialize source_file |> Sqlite3.bind store_stmt 1
SourceFile.SQLite.serialize source_file
|> Sqlite3.bind store_stmt 1
(* :source *)
|> SqliteUtils.check_result_code db ~log:"store bind source file" ;
Cfg.SQLite.serialize cfg |> Sqlite3.bind store_stmt 2
@ -77,8 +79,8 @@ let get_all ~filter () =
it inside the function *)
Sqlite3.prepare db "SELECT source_file FROM source_files"
|> IContainer.rev_filter_map_to_list
~fold:(SqliteUtils.result_fold_single_column_rows db ~log:"getting all source files") ~f:
(fun column ->
~fold:(SqliteUtils.result_fold_single_column_rows db ~log:"getting all source files")
~f:(fun column ->
let source_file = SourceFile.SQLite.deserialize column in
Option.some_if (filter source_file) source_file )
@ -90,7 +92,8 @@ let load_proc_names_statement =
let proc_names_of_source source =
ResultsDatabase.with_registered_statement load_proc_names_statement ~f:(fun db load_stmt ->
SourceFile.SQLite.serialize source |> Sqlite3.bind load_stmt 1
SourceFile.SQLite.serialize source
|> Sqlite3.bind load_stmt 1
|> SqliteUtils.check_result_code db ~log:"load bind source file" ;
SqliteUtils.result_single_column_option ~finalize:false db
~log:"SourceFiles.proc_names_of_source" load_stmt
@ -103,7 +106,8 @@ let exists_source_statement =
let is_captured source =
ResultsDatabase.with_registered_statement exists_source_statement ~f:(fun db exists_stmt ->
SourceFile.SQLite.serialize source |> Sqlite3.bind exists_stmt 1
SourceFile.SQLite.serialize source
|> Sqlite3.bind exists_stmt 1
(* :k *)
|> SqliteUtils.check_result_code db ~log:"load captured source file" ;
SqliteUtils.result_single_column_option ~finalize:false ~log:"SourceFiles.is_captured" db
@ -133,7 +137,8 @@ let deserialize_freshly_captured = function[@warning "-8"]
let is_freshly_captured source =
ResultsDatabase.with_registered_statement is_freshly_captured_statement ~f:(fun db load_stmt ->
SourceFile.SQLite.serialize source |> Sqlite3.bind load_stmt 1
SourceFile.SQLite.serialize source
|> Sqlite3.bind load_stmt 1
|> SqliteUtils.check_result_code db ~log:"load bind source file" ;
SqliteUtils.result_single_column_option ~finalize:false
~log:"SourceFiles.is_freshly_captured" db load_stmt

@ -29,5 +29,11 @@ val mark_all_stale : unit -> unit
(** mark all source files as stale; do be called at the start of a new capture phase *)
val pp_all :
filter:Filtering.source_files_filter -> cfgs:bool -> type_environment:bool
-> procedure_names:bool -> freshly_captured:bool -> Format.formatter -> unit -> unit
filter:Filtering.source_files_filter
-> cfgs:bool
-> type_environment:bool
-> procedure_names:bool
-> freshly_captured:bool
-> Format.formatter
-> unit
-> unit

@ -44,7 +44,7 @@ let mk_struct tenv ?default ?fields ?statics ?methods ?supers ?annots name =
(** Look up a name in the global type environment. *)
let lookup tenv name : Typ.Struct.t option =
try Some (TypenameHash.find tenv name) with Caml.Not_found ->
try Some (TypenameHash.find tenv name) with Caml.Not_found -> (
(* ToDo: remove the following additional lookups once C/C++ interop is resolved *)
match (name : Typ.Name.t) with
| CStruct m -> (
@ -52,7 +52,7 @@ let lookup tenv name : Typ.Struct.t option =
| CppClass (m, NoTemplate) -> (
try Some (TypenameHash.find tenv (CStruct m)) with Caml.Not_found -> None )
| _ ->
None
None )
let compare_fields (name1, _, _) (name2, _, _) = Typ.Fieldname.compare name1 name2
@ -131,7 +131,8 @@ let load_global () : t option =
let load source =
ResultsDatabase.with_registered_statement load_statement ~f:(fun db load_stmt ->
SourceFile.SQLite.serialize source |> Sqlite3.bind load_stmt 1
SourceFile.SQLite.serialize source
|> Sqlite3.bind load_stmt 1
|> SqliteUtils.check_result_code db ~log:"load bind source file" ;
SqliteUtils.result_single_column_option ~finalize:false ~log:"Tenv.load" db load_stmt
|> Option.bind ~f:(fun x ->

@ -30,8 +30,14 @@ val lookup : t -> Typ.Name.t -> Typ.Struct.t option
(** Look up a name in the global type environment. *)
val mk_struct :
t -> ?default:Typ.Struct.t -> ?fields:Typ.Struct.fields -> ?statics:Typ.Struct.fields
-> ?methods:Typ.Procname.t list -> ?supers:Typ.Name.t list -> ?annots:Annot.Item.t -> Typ.Name.t
t
-> ?default:Typ.Struct.t
-> ?fields:Typ.Struct.fields
-> ?statics:Typ.Struct.fields
-> ?methods:Typ.Procname.t list
-> ?supers:Typ.Name.t list
-> ?annots:Annot.Item.t
-> Typ.Name.t
-> Typ.Struct.t
(** Construct a struct_typ, normalizing field types *)

@ -159,8 +159,8 @@ include T
let mk_type_quals ?default ?is_const ?is_restrict ?is_volatile () =
let default_ = {is_const= false; is_restrict= false; is_volatile= false} in
let mk_aux ?(default= default_) ?(is_const= default.is_const) ?(is_restrict= default.is_restrict)
?(is_volatile= default.is_volatile) () =
let mk_aux ?(default = default_) ?(is_const = default.is_const)
?(is_restrict = default.is_restrict) ?(is_volatile = default.is_volatile) () =
{is_const; is_restrict; is_volatile}
in
mk_aux ?default ?is_const ?is_restrict ?is_volatile ()
@ -830,7 +830,8 @@ module Procname = struct
| CPPMethod {mangled} | CPPDestructor {mangled} ->
"(" ^ Option.value ~default:"" mangled ^ ")"
| CPPConstructor {mangled; is_constexpr} ->
"{" ^ Option.value ~default:"" mangled ^ (if is_constexpr then "|constexpr" else "")
"{" ^ Option.value ~default:"" mangled
^ (if is_constexpr then "|constexpr" else "")
^ "}"
| ObjCClassMethod ->
"class"
@ -849,7 +850,8 @@ module Procname = struct
| Verbose ->
let m_str = kind_to_verbose_string osig.kind in
Name.name osig.class_name ^ "_" ^ osig.method_name
^ Parameter.parameters_to_string osig.parameters ^ m_str
^ Parameter.parameters_to_string osig.parameters
^ m_str
let get_parameters osig = osig.parameters
@ -885,12 +887,12 @@ module Procname = struct
plain ^ "()"
| Non_verbose ->
plain
| Verbose ->
| Verbose -> (
match mangled with
| None ->
plain ^ Parameter.parameters_to_string parameters
| Some s ->
plain ^ Parameter.parameters_to_string parameters ^ "{" ^ s ^ "}"
plain ^ Parameter.parameters_to_string parameters ^ "{" ^ s ^ "}" )
let get_parameters c = c.parameters
@ -1258,7 +1260,9 @@ module Procname = struct
:: Option.to_list mangled
|> String.concat ~sep:"#"
| ObjC_Cpp objc_cpp ->
get_qual_name_str pname ^ Parameter.parameters_to_string objc_cpp.parameters ^ "#"
get_qual_name_str pname
^ Parameter.parameters_to_string objc_cpp.parameters
^ "#"
^ ObjC_Cpp.kind_to_verbose_string objc_cpp.kind
| _ ->
to_unique_id pname

@ -56,7 +56,11 @@ val equal_ptr_kind : ptr_kind -> ptr_kind -> bool
type type_quals [@@deriving compare]
val mk_type_quals :
?default:type_quals -> ?is_const:bool -> ?is_restrict:bool -> ?is_volatile:bool -> unit
?default:type_quals
-> ?is_const:bool
-> ?is_restrict:bool
-> ?is_volatile:bool
-> unit
-> type_quals
val is_const : type_quals -> bool
@ -643,8 +647,14 @@ module Struct : sig
(** Pretty print a struct type. *)
val internal_mk_struct :
?default:t -> ?fields:fields -> ?statics:fields -> ?methods:Procname.t list
-> ?supers:Name.t list -> ?annots:Annot.Item.t -> unit -> t
?default:t
-> ?fields:fields
-> ?statics:fields
-> ?methods:Procname.t list
-> ?supers:Name.t list
-> ?annots:Annot.Item.t
-> unit
-> t
(** Construct a struct_typ, normalizing field types *)
val get_extensible_array_element_typ : lookup:lookup -> typ -> typ option

@ -1,6 +1,8 @@
(* -*- tuareg -*- *)
(* NOTE: prepend dune.common to this file! *)
;; Format.sprintf
;;
Format.sprintf
{|
(library
(name InferIR)

@ -297,7 +297,7 @@ module BooleanOr = struct
let is_empty astate = not astate
let ( <= ) ~lhs ~rhs = not lhs || rhs
let ( <= ) ~lhs ~rhs = (not lhs) || rhs
let join = ( || )

@ -59,7 +59,8 @@ module BottomLifted (Domain : S) : sig
end
(** Create a domain with Top element from a pre-domain *)
include sig
include
sig
(* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
[@@@warning "-60"]
@ -124,7 +125,8 @@ end
(** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's
true in both conditional branches. *)
include sig
include
sig
(* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
[@@@warning "-60"]

@ -19,12 +19,17 @@ module type S = sig
type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
val compute_post :
?debug:bool -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate
?debug:bool
-> TransferFunctions.extras ProcData.t
-> initial:TransferFunctions.Domain.astate
-> TransferFunctions.Domain.astate option
val exec_cfg :
TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t
-> initial:TransferFunctions.Domain.astate -> debug:bool -> invariant_map
TransferFunctions.CFG.t
-> TransferFunctions.extras ProcData.t
-> initial:TransferFunctions.Domain.astate
-> debug:bool
-> invariant_map
val exec_pdesc :
TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map
@ -139,14 +144,14 @@ struct
match extract_post_ pred with
| None ->
joined_post_opt
| Some post as some_post ->
| Some post as some_post -> (
match joined_post_opt with
| None ->
some_post
| Some joined_post ->
let res = Domain.join joined_post post in
if debug then debug_absint_operation (`Join (joined_post, post, res)) node ;
Some res )
Some res ) )
in
match Scheduler.pop work_queue with
| Some (_, [], work_queue') ->

@ -19,14 +19,19 @@ module type S = sig
type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
val compute_post :
?debug:bool -> TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate
?debug:bool
-> TransferFunctions.extras ProcData.t
-> initial:TransferFunctions.Domain.astate
-> TransferFunctions.Domain.astate option
(** compute and return the postcondition for the given procedure starting from [initial]. If
[debug] is true, print html debugging output. *)
val exec_cfg :
TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t
-> initial:TransferFunctions.Domain.astate -> debug:bool -> invariant_map
TransferFunctions.CFG.t
-> TransferFunctions.extras ProcData.t
-> initial:TransferFunctions.Domain.astate
-> debug:bool
-> invariant_map
(** compute and return invariant map for the given CFG/procedure starting from [initial]. if
[debug] is true, print html debugging output. *)

@ -42,7 +42,7 @@ struct
let is_java_unlock pname actuals =
(* would check is_java, but we want to include builtins too *)
not (Typ.Procname.is_c_method pname)
(not (Typ.Procname.is_c_method pname))
&& match RacerDConfig.Models.get_lock pname actuals with Unlock -> true | _ -> false

@ -289,8 +289,7 @@ let proc_calls resolve_attributes pdesc filter : (Typ.Procname.t * ProcAttribute
Instrs.iter ~f:(do_instruction node) instrs
in
let nodes = Procdesc.get_nodes pdesc in
List.iter ~f:do_node nodes ;
List.rev !res
List.iter ~f:do_node nodes ; List.rev !res
let override_find ?(check_current_type = true) f tenv proc_name =

@ -50,12 +50,17 @@ val java_get_vararg_values : Procdesc.Node.t -> Pvar.t -> Idenv.t -> Exp.t list
(** Get the values of a vararg parameter given the pvar used to assign the elements. *)
val proc_calls :
(Typ.Procname.t -> ProcAttributes.t option) -> Procdesc.t
-> (Typ.Procname.t -> ProcAttributes.t -> bool) -> (Typ.Procname.t * ProcAttributes.t) list
(Typ.Procname.t -> ProcAttributes.t option)
-> Procdesc.t
-> (Typ.Procname.t -> ProcAttributes.t -> bool)
-> (Typ.Procname.t * ProcAttributes.t) list
(** Return the callees that satisfy [filter]. *)
val override_find :
?check_current_type:bool -> (Typ.Procname.t -> bool) -> Tenv.t -> Typ.Procname.t
?check_current_type:bool
-> (Typ.Procname.t -> bool)
-> Tenv.t
-> Typ.Procname.t
-> Typ.Procname.t option
(** Return a method which overrides [procname] and satisfies [f] (including [procname] itself when [check_current_type] is true, which it is by default). *)

@ -74,9 +74,8 @@ end
module InstrNode : sig
type instr_index = int
include Node
with type t = Procdesc.Node.t * instr_index
and type id = Procdesc.Node.id * instr_index
include
Node with type t = Procdesc.Node.t * instr_index and type id = Procdesc.Node.id * instr_index
end = struct
type instr_index = int [@@deriving compare]
@ -297,10 +296,8 @@ module Backward (Base : S with type instrs_dir = Instrs.not_reversed) = struct
end
module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig
include S
with type t = Base.t
and module Node = InstrNode
and type instrs_dir = Instrs.not_reversed
include
S with type t = Base.t and module Node = InstrNode and type instrs_dir = Instrs.not_reversed
val last_of_underlying_node : Procdesc.Node.t -> Node.t
end = struct

@ -83,9 +83,8 @@ module DefaultNode : Node with type t = Procdesc.Node.t and type id = Procdesc.N
module InstrNode : sig
type instr_index
include Node
with type t = Procdesc.Node.t * instr_index
and type id = Procdesc.Node.id * instr_index
include
Node with type t = Procdesc.Node.t * instr_index and type id = Procdesc.Node.id * instr_index
end
(** Forward CFG with no exceptional control-flow *)
@ -107,10 +106,8 @@ module Backward (Base : S with type instrs_dir = Instrs.not_reversed) :
S with type t = Base.t and module Node = Base.Node and type instrs_dir = Instrs.reversed
module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig
include S
with type t = Base.t
and module Node = InstrNode
and type instrs_dir = Instrs.not_reversed
include
S with type t = Base.t and module Node = InstrNode and type instrs_dir = Instrs.not_reversed
val last_of_underlying_node : Procdesc.Node.t -> Node.t
end

@ -85,6 +85,7 @@ module ReversePostorder (CFG : ProcCfg.S) = struct
(* TODO: could do this slightly more efficiently by keeping a list of priority zero nodes for
quick popping, and do a linear search only when this list is empty *)
(** remove and return the node with the highest priority (note that smaller integers have higher
priority), the ids of its visited predecessors, and new schedule *)
let pop t =

@ -3,7 +3,8 @@
let cflags = common_cflags @ ["-w"; "-27-32-34-35-39"]
;; Format.sprintf
;;
Format.sprintf
{|
(library
(name InferGenerated)

@ -13,7 +13,7 @@ module LocListSet = struct
type t = Location.t list [@@deriving compare]
end)
let mem s xs = not (List.is_empty xs) && mem (List.sort ~compare:Location.compare xs) s
let mem s xs = (not (List.is_empty xs)) && mem (List.sort ~compare:Location.compare xs) s
let add s xs = if List.is_empty xs then s else add (List.sort ~compare:Location.compare xs) s
end
@ -41,8 +41,8 @@ let sort_by_location issues =
let dedup (issues : Jsonbug_t.jsonbug list) =
List.fold (sort_by_decreasing_preference_to_report issues) ~init:(LocListSet.empty, []) ~f:
(fun (reported_ends, nondup_issues) (issue: Jsonbug_t.jsonbug) ->
List.fold (sort_by_decreasing_preference_to_report issues) ~init:(LocListSet.empty, [])
~f:(fun (reported_ends, nondup_issues) (issue : Jsonbug_t.jsonbug) ->
match issue.access with
| Some encoded ->
let _, _, end_locs = IssueAuxData.decode encoded in

@ -26,8 +26,7 @@ module FileRenamings = struct
let renaming_of_assoc assoc : renaming =
try
match assoc with
| `Assoc l
-> (
| `Assoc l -> (
let current_opt = List.Assoc.find ~equal:String.equal l "current" in
let previous_opt = List.Assoc.find ~equal:String.equal l "previous" in
match (current_opt, previous_opt) with
@ -123,7 +122,8 @@ let skip_duplicated_types_on_filenames renamings (diff: Differential.t) : Differ
in
String.compare f1 f2
in
let compare ((issue1, _) as issue_with_previous_file1) ((issue2, _) as issue_with_previous_file2) =
let compare ((issue1, _) as issue_with_previous_file1) ((issue2, _) as issue_with_previous_file2)
=
[%compare: Caml.Digest.t * string * issue_file_with_renaming]
(issue1.Jsonbug_t.node_key, issue1.Jsonbug_t.bug_type, issue_with_previous_file1)
(issue2.Jsonbug_t.node_key, issue2.Jsonbug_t.bug_type, issue_with_previous_file2)
@ -159,7 +159,7 @@ let interesting_paths_filter (interesting_paths: SourceFile.t list option) =
let interesting_paths_set =
paths
|> List.filter_map ~f:(fun p ->
if not (SourceFile.is_invalid p) && SourceFile.is_under_project_root p then
if (not (SourceFile.is_invalid p)) && SourceFile.is_under_project_root p then
Some (SourceFile.to_string p)
else None )
|> String.Set.of_list

@ -30,12 +30,18 @@ module FileRenamings : sig
end
val do_filter :
Differential.t -> FileRenamings.t -> skip_duplicated_types:bool
-> interesting_paths:SourceFile.t list option -> Differential.t
Differential.t
-> FileRenamings.t
-> skip_duplicated_types:bool
-> interesting_paths:SourceFile.t list option
-> Differential.t
module VISIBLE_FOR_TESTING_DO_NOT_USE_DIRECTLY : sig
val relative_complements :
compare:('a -> 'a -> int) -> ?pred:('a -> bool) -> 'a list -> 'a list
compare:('a -> 'a -> int)
-> ?pred:('a -> bool)
-> 'a list
-> 'a list
-> 'a list * 'a list * 'a list
val skip_duplicated_types_on_filenames : FileRenamings.t -> Differential.t -> Differential.t

@ -8,6 +8,7 @@
(** Main module for the analysis after the capture phase *)
open! IStd
module L = Logging
let clear_caches () =

@ -162,7 +162,7 @@ module ProcsCsv = struct
end
let should_report (issue_kind : Exceptions.severity) issue_type error_desc eclass =
if not Config.filtering || Exceptions.equal_err_class eclass Exceptions.Linters then true
if (not Config.filtering) || Exceptions.equal_err_class eclass Exceptions.Linters then true
else
let issue_kind_is_blacklisted =
match issue_kind with Info -> true | Advice | Error | Like | Warning -> false
@ -189,10 +189,11 @@ let should_report (issue_kind: Exceptions.severity) issue_type error_desc eclass
string (that is "no reason") means that the issue should be reported. *)
let censored_reason (issue_type : IssueType.t) source_file =
let filename = SourceFile.to_rel_path source_file in
let rejected_by ((issue_type_polarity, issue_type_re), (filename_polarity, filename_re), reason) =
let rejected_by ((issue_type_polarity, issue_type_re), (filename_polarity, filename_re), reason)
=
let accepted =
(* matches issue_type_re implies matches filename_re *)
not (Bool.equal issue_type_polarity (Str.string_match issue_type_re issue_type.unique_id 0))
(not (Bool.equal issue_type_polarity (Str.string_match issue_type_re issue_type.unique_id 0)))
|| Bool.equal filename_polarity (Str.string_match filename_re filename 0)
in
Option.some_if (not accepted) reason
@ -216,9 +217,7 @@ module MakeJsonListPrinter (P : sig
type elt
val to_string : elt -> string option
end) :
Printer with type elt = P.elt =
struct
end) : Printer with type elt = P.elt = struct
include P
let is_first_item = ref true
@ -262,10 +261,11 @@ module JsonIssuePrinter = MakeJsonListPrinter (struct
"Invalid source file for %a %a@.Trace: %a@." IssueType.pp err_key.err_name
Localise.pp_error_desc err_key.err_desc Errlog.pp_loc_trace err_data.loc_trace ;
let should_report_source_file =
not (SourceFile.is_infer_model source_file) || Config.debug_mode || Config.debug_exceptions
(not (SourceFile.is_infer_model source_file)) || Config.debug_mode || Config.debug_exceptions
in
if
err_key.in_footprint && error_filter source_file err_key.err_name
err_key.in_footprint
&& error_filter source_file err_key.err_name
&& should_report_source_file
&& should_report err_key.severity err_key.err_name err_key.err_desc err_data.err_class
then
@ -383,7 +383,8 @@ let pp_custom_of_report fmt report fields =
| `Issue_field_bucket ->
let bucket =
match
String.lsplit2 issue.qualifier ~on:']' |> Option.map ~f:fst
String.lsplit2 issue.qualifier ~on:']'
|> Option.map ~f:fst
|> Option.bind ~f:(String.chop_prefix ~prefix:"[")
with
| Some bucket ->
@ -443,8 +444,9 @@ module IssuesTxt = struct
err_data.loc.Location.file
in
if
key.in_footprint && error_filter source_file key.err_name
&& (not Config.filtering || String.is_empty (censored_reason key.err_name source_file))
key.in_footprint
&& error_filter source_file key.err_name
&& ((not Config.filtering) || String.is_empty (censored_reason key.err_name source_file))
then Exceptions.pp_err err_data.loc key.severity key.err_name key.err_desc None fmt ()
@ -503,7 +505,9 @@ module Stats = struct
let res = ref [] in
let indent_string n =
let s = ref "" in
for _ = 1 to n do s := " " ^ !s done ;
for _ = 1 to n do
s := " " ^ !s
done ;
!s
in
let num = ref 0 in
@ -525,8 +529,7 @@ module Stats = struct
in
res := line :: "" :: !res
in
List.iter ~f:loc_to_string ltr ;
List.rev !res
List.iter ~f:loc_to_string ltr ; List.rev !res
let process_err_log error_filter linereader err_log stats =
@ -709,7 +712,8 @@ end
let error_filter filters proc_name file error_name =
(Config.write_html || not (IssueType.(equal skip_function) error_name))
&& filters.Inferconfig.path_filter file && filters.Inferconfig.error_filter error_name
&& filters.Inferconfig.path_filter file
&& filters.Inferconfig.error_filter error_name
&& filters.Inferconfig.proc_filter proc_name
@ -916,7 +920,8 @@ let pp_json_report_by_report_kind formats_by_report_kind fname =
L.(die UserError) "Error reading '%s': %s" fname error
let pp_lint_issues_by_report_kind formats_by_report_kind error_filter linereader procname error_log =
let pp_lint_issues_by_report_kind formats_by_report_kind error_filter linereader procname error_log
=
let pp_summary_by_report_kind (report_kind, format_list) =
match (report_kind, format_list) with
| Issues, _ :: _ ->
@ -955,7 +960,7 @@ let spec_files_from_cmdline () =
files may be generated between init and report time. *)
List.iter
~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") )
Config.anon_args ;
if Config.test_filtering then ( Inferconfig.test () ; L.exit 0 ) ;

@ -13,7 +13,7 @@ let compilation_db = lazy (CompilationDatabase.from_json_files !Config.clang_com
It may trigger capture of extra files to do so and when it does, it waits for
frontend to finish before returning *)
let try_capture (attributes : ProcAttributes.t) : ProcAttributes.t option =
let lazy cdb = compilation_db in
let (lazy cdb) = compilation_db in
( if Option.is_none (Attributes.load_defined attributes.proc_name) then
let decl_file = attributes.loc.file in
let definition_file_opt = SourceFile.of_header decl_file in
@ -28,8 +28,7 @@ let try_capture (attributes: ProcAttributes.t) : ProcAttributes.t option =
protect
~f:(fun () -> CaptureCompilationDatabase.capture_file_in_database cdb definition_file)
~finally:Timeout.resume_previous_timeout ;
if Config.debug_mode && Option.is_none (Attributes.load_defined attributes.proc_name)
then
if Config.debug_mode && Option.is_none (Attributes.load_defined attributes.proc_name) then
(* peek at the results to know if capture succeeded, but only in debug mode *)
L.(debug Capture Verbose)
"Captured file %a to get procedure %a but it wasn't found there@\n" SourceFile.pp

@ -10,8 +10,8 @@ module F = Format
let get_all ~filter () =
let db = ResultsDatabase.get_database () in
let stmt = Sqlite3.prepare db "SELECT source_file, proc_name FROM procedures" in
SqliteUtils.result_fold_rows db ~log:"reading all procedure names" stmt ~init:[] ~f:
(fun rev_results stmt ->
SqliteUtils.result_fold_rows db ~log:"reading all procedure names" stmt ~init:[]
~f:(fun rev_results stmt ->
let source_file = Sqlite3.column stmt 0 |> SourceFile.SQLite.deserialize in
let proc_name = Sqlite3.column stmt 1 |> Typ.Procname.SQLite.deserialize in
if filter source_file proc_name then proc_name :: rev_results else rev_results )
@ -31,7 +31,7 @@ let pp_all ~filter ~proc_name:proc_name_cond ~attr_kind ~source_file:source_file
pp_if ?new_line condition title pp fmt (Sqlite3.column stmt column |> deserialize)
in
let pp_row stmt fmt source_file proc_name =
let[@warning "-8"] Sqlite3.Data.TEXT proc_name_hum = Sqlite3.column stmt 1 in
let[@warning "-8"] (Sqlite3.Data.TEXT proc_name_hum) = Sqlite3.column stmt 1 in
Format.fprintf fmt "@[<v2>%s@,%a%a%a%a@]@\n" proc_name_hum
(pp_if source_file_cond "source_file" SourceFile.pp)
source_file
@ -47,8 +47,8 @@ let pp_all ~filter ~proc_name:proc_name_cond ~attr_kind ~source_file:source_file
(* we could also register this statement but it's typically used only once per run so just prepare
it inside the function *)
Sqlite3.prepare db "SELECT * FROM procedures"
|> Container.iter ~fold:(SqliteUtils.result_fold_rows db ~log:"print all procedures") ~f:
(fun stmt ->
|> Container.iter ~fold:(SqliteUtils.result_fold_rows db ~log:"print all procedures")
~f:(fun stmt ->
let proc_name = Sqlite3.column stmt 0 |> Typ.Procname.SQLite.deserialize in
let source_file = Sqlite3.column stmt 3 |> SourceFile.SQLite.deserialize in
if filter source_file proc_name then pp_row stmt fmt source_file proc_name )

@ -10,5 +10,11 @@ open! IStd
val get_all : filter:Filtering.procedures_filter -> unit -> Typ.Procname.t list
val pp_all :
filter:Filtering.procedures_filter -> proc_name:bool -> attr_kind:bool -> source_file:bool
-> proc_attributes:bool -> Format.formatter -> unit -> unit
filter:Filtering.procedures_filter
-> proc_name:bool
-> attr_kind:bool
-> source_file:bool
-> proc_attributes:bool
-> Format.formatter
-> unit
-> unit

@ -14,8 +14,11 @@ let aggregated_stats_by_target_filename = "aggregated_stats_by_target.json"
let json_files_to_ignore_regex =
Str.regexp
( ".*\\(" ^ Str.quote aggregated_stats_filename ^ "\\|"
^ Str.quote aggregated_stats_by_target_filename ^ "\\)$" )
( ".*\\("
^ Str.quote aggregated_stats_filename
^ "\\|"
^ Str.quote aggregated_stats_by_target_filename
^ "\\)$" )
let dir_exists dir = Sys.is_directory dir = `Yes
@ -24,7 +27,8 @@ let find_json_files_in_dir dir =
let is_valid_json_file path =
let s = Unix.lstat path in
let json_regex = Str.regexp_case_fold ".*\\.json$" in
not (Str.string_match json_files_to_ignore_regex path 0) && Str.string_match json_regex path 0
(not (Str.string_match json_files_to_ignore_regex path 0))
&& Str.string_match json_regex path 0
&& Polymorphic_compare.( = ) s.st_kind Unix.S_REG
in
match dir_exists dir with
@ -63,7 +67,8 @@ let load_data_from_infer_deps file =
Error (error "malformed input")
in
let parse_lines lines = List.map lines ~f:extract_target_and_path |> Result.all in
Utils.read_file file |> Result.map_error ~f:(fun msg -> error "%s" msg)
Utils.read_file file
|> Result.map_error ~f:(fun msg -> error "%s" msg)
|> Result.bind ~f:parse_lines

@ -96,7 +96,7 @@ let dump_duplicate_procs (exe_env: Exe_env.t) source_file procs =
match Attributes.load pname with
| Some {translation_unit; loc}
when (* defined in another file *)
not (SourceFile.equal source_file translation_unit)
(not (SourceFile.equal source_file translation_unit))
&& (* really defined in the current file and not in an include *)
SourceFile.equal source_file loc.file ->
Some (pname, translation_unit)

@ -24,9 +24,7 @@ type proc_callback_args =
type proc_callback_t = proc_callback_args -> Summary.t
type cluster_callback_args =
{ procedures: (Tenv.t * Procdesc.t) list
; source_file: SourceFile.t
; exe_env: Exe_env.t }
{procedures: (Tenv.t * Procdesc.t) list; source_file: SourceFile.t; exe_env: Exe_env.t}
type cluster_callback_t = cluster_callback_args -> unit

@ -74,7 +74,8 @@ let collect_all_summaries root_summaries_dir stacktrace_file stacktraces_dir =
(fun summaries path ->
(* check if the file is a JSON file under the crashcontext dir *)
if
Sys.is_directory path <> `Yes && Filename.check_suffix path "json"
Sys.is_directory path <> `Yes
&& Filename.check_suffix path "json"
&& String.is_suffix ~suffix:"crashcontext" (Filename.dirname path)
then path :: summaries
else summaries )
@ -86,14 +87,15 @@ let collect_all_summaries root_summaries_dir stacktrace_file stacktraces_dir =
None
| Some file ->
let crashcontext_dir = Config.results_dir ^/ "crashcontext" in
Utils.create_dir crashcontext_dir ; Some (file, crashcontext_dir ^/ "crashcontext.json")
Utils.create_dir crashcontext_dir ;
Some (file, crashcontext_dir ^/ "crashcontext.json")
in
let trace_file_regexp = Str.regexp "\\(.*\\)\\.json" in
let pairs_for_stactrace_dir =
match stacktraces_dir with
| None ->
[]
| Some s ->
| Some s -> (
let dir = DB.filename_from_string s in
let trace_file_matcher path =
let path_str = DB.filename_to_string path in
@ -110,7 +112,7 @@ let collect_all_summaries root_summaries_dir stacktrace_file stacktraces_dir =
DB.fold_paths_matching statement below, so we don't need to
call Str.string_match again. *)
| Caml.Not_found
-> assert false
-> assert false )
in
let input_output_file_pairs =
match pair_for_stacktrace_file with

@ -271,7 +271,8 @@ let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list
incr dotty_state_count ;
let coo = mk_coordinate n lambda in
match hpred with
| Sil.Hpointsto (_, Sil.Eexp (e, _), _) when not (Exp.equal e Exp.zero) && !print_full_prop ->
| Sil.Hpointsto (_, Sil.Eexp (e, _), _) when (not (Exp.equal e Exp.zero)) && !print_full_prop
->
let e_color_str = color_to_str (exp_color hpred e) in
[Dotdangling (coo, e, e_color_str)]
| Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Exp.zero) ->
@ -474,8 +475,7 @@ let node_in_cycle cycle node =
let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle =
let find_target_one_fld (fn, se) =
match se with
| Sil.Eexp (e, _)
-> (
| Sil.Eexp (e, _) -> (
if is_nil e p then
let n' = make_nil_node lambda in
if !print_full_prop then [(LinkStructToExp, Typ.Fieldname.to_string fn, n', "")] else []
@ -520,8 +520,7 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle =
let rec compute_target_array_elements dotnodes list_elements p f lambda =
let find_target_one_element (idx, se) =
match se with
| Sil.Eexp (e, _)
-> (
| Sil.Eexp (e, _) -> (
if is_nil e p then
let n' = make_nil_node lambda in
[(LinkArrayToExp, Exp.to_string idx, n', "")]
@ -598,15 +597,14 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
let lnk =
mk_link LinkToArray (mk_coordinate n lambda) "" (mk_coordinate (n + 1) lambda) trg_label
in
lnk :: links_from_elements @ dotty_mk_set_links dotnodes sigma' p f cycle
(lnk :: links_from_elements) @ dotty_mk_set_links dotnodes sigma' p f cycle
in
match sigma with
| [] ->
[]
| (Sil.Hpointsto (e, Sil.Earray (_, lie, _), _), lambda) :: sigma' ->
make_links_for_arrays e lie lambda sigma'
| (Sil.Hpointsto (e, Sil.Estruct (lfld, _), _), lambda) :: sigma'
-> (
| (Sil.Hpointsto (e, Sil.Estruct (lfld, _), _), lambda) :: sigma' -> (
let src = look_up dotnodes e lambda in
match src with
| [] ->
@ -639,8 +637,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
in
lnk_from_address_struct @ links_from_fields
@ dotty_mk_set_links dotnodes sigma' p f cycle )
| (Sil.Hpointsto (e, Sil.Eexp (e', _), _), lambda) :: sigma'
-> (
| (Sil.Hpointsto (e, Sil.Eexp (e', _), _), lambda) :: sigma' -> (
let src = look_up dotnodes e lambda in
match src with
| [] ->
@ -658,8 +655,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
let ll = List.concat_map ~f:ff nl in
ll @ dotty_mk_set_links dotnodes sigma' p f cycle
else dotty_mk_set_links dotnodes sigma' p f cycle )
| (Sil.Hlseg (_, _, e1, e2, _), lambda) :: sigma'
-> (
| (Sil.Hlseg (_, _, e1, e2, _), lambda) :: sigma' -> (
let src = look_up dotnodes e1 lambda in
match src with
| [] ->
@ -670,7 +666,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
mk_link LinkToSSL (mk_coordinate (n + 1) lambda) "" (mk_coordinate m lambda) lab
in
lnk :: dotty_mk_set_links dotnodes sigma' p f cycle )
| (Sil.Hdllseg (_, _, e1, e2, e3, _, _), lambda) :: sigma' ->
| (Sil.Hdllseg (_, _, e1, e2, e3, _, _), lambda) :: sigma' -> (
let src = look_up dotnodes e1 lambda in
match src with
| [] ->
@ -693,7 +689,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
| m :: _ ->
[mk_link LinkToDLL (mk_coordinate n lambda) "" (mk_coordinate m lambda) ""]
in
target_Blink @ target_Flink @ dotty_mk_set_links dotnodes sigma' p f cycle
target_Blink @ target_Flink @ dotty_mk_set_links dotnodes sigma' p f cycle )
let print_kind f kind =
@ -709,7 +705,7 @@ let print_kind f kind =
F.fprintf f "@\n POST%iL0 [label=\"POST %i \", style=filled, color= yellow]@\n"
!dotty_state_count !post_counter ;
print_stack_info := true
| Lambda_pred (no, lev, array) ->
| Lambda_pred (no, lev, array) -> (
match array with
| false ->
F.fprintf f "%s @\n state%iL%i [label=\"INTERNAL STRUCTURE %i \", %s]@\n"
@ -723,7 +719,7 @@ let print_kind f kind =
"style=filled, color= lightblue" ;
(* F.fprintf f "state%iL%i -> struct%iL%i:%s [color=\"lightblue \" arrowhead=none] @\n"
!dotty_state_count !lambda_counter no lev lab;*)
incr dotty_state_count
incr dotty_state_count )
(* print a link between two nodes in the graph *)
@ -825,8 +821,7 @@ let filter_useless_spec_dollar_box (nodes: dotty_node list) (links: link list) =
let rec print_struct f pe e te l coo c =
let print_type =
match te with
| Exp.Sizeof {typ}
-> (
| Exp.Sizeof {typ} -> (
let str_t = Typ.to_string typ in
match Str.split_delim (Str.regexp_string Config.anonymous_block_prefix) str_t with
| [_; _] ->
@ -887,7 +882,8 @@ and print_sll f pe nesting k e1 coo =
F.fprintf f "state%iL%i [label=\" \"] @\n" (n + 1) lambda ;
F.fprintf f "state%iL%i -> state%iL%i [label=\" \"] }" n' lambda (n + 1) lambda ;
incr lambda_counter ;
pp_dotty f (Lambda_pred (n + 1, lambda, false))
pp_dotty f
(Lambda_pred (n + 1, lambda, false))
(Prop.normalize (Tenv.create ()) (Prop.from_sigma nesting))
None
@ -914,7 +910,8 @@ and print_dll f pe nesting k e1 e4 coo =
F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]@\n" (n + 1) lambda n' lambda ;
F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]}@\n" n' lambda (n + 1) lambda ;
incr lambda_counter ;
pp_dotty f (Lambda_pred (n', lambda, false))
pp_dotty f
(Lambda_pred (n', lambda, false))
(Prop.normalize (Tenv.create ()) (Prop.from_sigma nesting))
None

@ -73,8 +73,8 @@ let verbose = Config.trace_error
(** Find the function call instruction used to initialize normal variable [id],
and return the function name and arguments *)
let find_normal_variable_funcall (node: Procdesc.Node.t) (id: Ident.t)
: (Exp.t * Exp.t list * Location.t * CallFlags.t) option =
let find_normal_variable_funcall (node : Procdesc.Node.t) (id : Ident.t) :
(Exp.t * Exp.t list * Location.t * CallFlags.t) option =
let find_declaration _ = function
| Sil.Call ((id0, _), fun_exp, args, loc, call_flags) when Ident.equal id id0 ->
Some (fun_exp, List.map ~f:fst args, loc, call_flags)
@ -93,7 +93,8 @@ let find_normal_variable_funcall (node: Procdesc.Node.t) (id: Ident.t)
(** Find a program variable assignment in the current node or predecessors. *)
let find_program_variable_assignment node pvar : (Procdesc.Node.t * Ident.t) option =
let find_instr node = function
| Sil.Store (Exp.Lvar pvar_, _, Exp.Var id, _) when Pvar.equal pvar pvar_ && Ident.is_normal id ->
| Sil.Store (Exp.Lvar pvar_, _, Exp.Var id, _) when Pvar.equal pvar pvar_ && Ident.is_normal id
->
Some (node, id)
| _ ->
None
@ -218,8 +219,7 @@ and exp_lv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option =
| Exp.Const c ->
if verbose then ( L.d_str "exp_lv_dexp: constant " ; Sil.d_exp e ; L.d_ln () ) ;
Some (DExp.Dderef (DExp.Dconst c))
| Exp.BinOp (Binop.PlusPI, e1, e2)
-> (
| Exp.BinOp (Binop.PlusPI, e1, e2) -> (
if verbose then (
L.d_str "exp_lv_dexp: (e1 +PI e2) " ;
Sil.d_exp e ;
@ -229,8 +229,7 @@ and exp_lv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option =
Some (DExp.Dbinop (Binop.PlusPI, de1, de2))
| _ ->
None )
| Exp.Var id when Ident.is_normal id
-> (
| Exp.Var id when Ident.is_normal id -> (
if verbose then (
L.d_str "exp_lv_dexp: normal var " ;
Sil.d_exp e ;
@ -253,7 +252,7 @@ and exp_lv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option =
Some (DExp.Dfcall (DExp.Dconst (Cfun pname), [], loc, call_flags))
| None ->
None )
| Some (node', id) ->
| Some (node', id) -> (
match find_normal_variable_funcall node' id with
| Some (fun_exp, eargs, loc, call_flags) ->
let fun_dexpo = exp_rv_dexp_ tenv seen node' fun_exp in
@ -264,10 +263,9 @@ and exp_lv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option =
let args = List.map ~f:unNone blame_args in
Some (DExp.Dfcall (unNone fun_dexpo, args, loc, call_flags))
| None ->
exp_rv_dexp_ tenv seen node' (Exp.Var id)
exp_rv_dexp_ tenv seen node' (Exp.Var id) )
else Some (DExp.Dpvar pvar)
| Exp.Lfield (Exp.Var id, f, _) when Ident.is_normal id
-> (
| Exp.Lfield (Exp.Var id, f, _) when Ident.is_normal id -> (
if verbose then (
L.d_str "exp_lv_dexp: Lfield with var " ;
Sil.d_exp (Exp.Var id) ;
@ -278,8 +276,7 @@ and exp_lv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option =
None
| Some de ->
Some (DExp.Darrow (de, f)) )
| Exp.Lfield (e1, f, _)
-> (
| Exp.Lfield (e1, f, _) -> (
if verbose then (
L.d_str "exp_lv_dexp: Lfield " ;
Sil.d_exp e1 ;
@ -290,8 +287,7 @@ and exp_lv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option =
None
| Some de ->
Some (DExp.Ddot (de, f)) )
| Exp.Lindex (e1, e2)
-> (
| Exp.Lindex (e1, e2) -> (
if verbose then (
L.d_str "exp_lv_dexp: Lindex " ; Sil.d_exp e1 ; L.d_str " " ; Sil.d_exp e2 ; L.d_ln () ) ;
match (exp_lv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with
@ -337,8 +333,7 @@ and exp_rv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option =
Sil.d_exp e ;
L.d_ln () ) ;
find_normal_variable_load_ tenv seen node id
| Exp.Lfield (e1, f, _)
-> (
| Exp.Lfield (e1, f, _) -> (
if verbose then (
L.d_str "exp_rv_dexp: Lfield " ;
Sil.d_exp e1 ;
@ -349,8 +344,7 @@ and exp_rv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option =
None
| Some de ->
Some (DExp.Ddot (de, f)) )
| Exp.Lindex (e1, e2)
-> (
| Exp.Lindex (e1, e2) -> (
if verbose then (
L.d_str "exp_rv_dexp: Lindex " ; Sil.d_exp e1 ; L.d_str " " ; Sil.d_exp e2 ; L.d_ln () ) ;
match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with
@ -358,16 +352,14 @@ and exp_rv_dexp_ tenv (seen_: Exp.Set.t) node e : DExp.t option =
None
| Some de1, Some de2 ->
Some (DExp.Darray (de1, de2)) )
| Exp.BinOp (op, e1, e2)
-> (
| Exp.BinOp (op, e1, e2) -> (
if verbose then ( L.d_str "exp_rv_dexp: BinOp " ; Sil.d_exp e ; L.d_ln () ) ;
match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with
| None, _ | _, None ->
None
| Some de1, Some de2 ->
Some (DExp.Dbinop (op, de1, de2)) )
| Exp.UnOp (op, e1, _)
-> (
| Exp.UnOp (op, e1, _) -> (
if verbose then ( L.d_str "exp_rv_dexp: UnOp " ; Sil.d_exp e ; L.d_ln () ) ;
match exp_rv_dexp_ tenv seen node e1 with
| None ->
@ -496,7 +488,8 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
let is_file = match resource_opt with Some PredSymb.Rfile -> true | _ -> false in
let check_pvar pvar =
(* check that pvar is local or global and has the same type as the leaked hpred *)
(Pvar.is_local pvar || Pvar.is_global pvar) && not (Pvar.is_frontend_tmp pvar)
(Pvar.is_local pvar || Pvar.is_global pvar)
&& (not (Pvar.is_frontend_tmp pvar))
&&
match (hpred_typ_opt, find_typ_without_ptr prop pvar) with
| Some (Exp.Sizeof {typ= t1}), Some (Exp.Sizeof {typ= {Typ.desc= Tptr (t2, _)}}) ->
@ -515,8 +508,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
L.d_str "explain_leak: no current instruction" ;
L.d_ln () ) ;
value_str_from_pvars_vpath [] vpath
| Some (Sil.Nullify (pvar, _)) when check_pvar pvar
-> (
| Some (Sil.Nullify (pvar, _)) when check_pvar pvar -> (
if verbose then (
L.d_str "explain_leak: current instruction is Nullify for pvar " ;
Pvar.d pvar ;
@ -547,8 +539,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
List.rev_filter ~f:(fun pvar -> not (Pvar.is_frontend_tmp pvar)) rev_nullify_pvars
in
value_str_from_pvars_vpath nullify_pvars_notmp vpath
| Some (Sil.Store (lexp, _, _, _)) when is_none vpath
-> (
| Some (Sil.Store (lexp, _, _, _)) when is_none vpath -> (
if verbose then (
L.d_str "explain_leak: current instruction Set for " ;
Sil.d_exp lexp ;
@ -588,8 +579,7 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
let rec find sigma_acc sigma_todo exp =
let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) =
match se with
| Sil.Eexp (e, _) when Exp.equal exp e
-> (
| Sil.Eexp (e, _) when Exp.equal exp e -> (
let sigma' = List.rev_append sigma_acc' sigma_todo' in
match lexp with
| Exp.Lvar pv ->
@ -622,8 +612,7 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
in
let do_sexp sigma_acc' sigma_todo' lexp sexp texp =
match sexp with
| Sil.Eexp (e, _) when Exp.equal exp e
-> (
| Sil.Eexp (e, _) when Exp.equal exp e -> (
let sigma' = List.rev_append sigma_acc' sigma_todo' in
match lexp with
| Exp.Lvar pv when not (Pvar.is_frontend_tmp pv) ->
@ -671,12 +660,12 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
match sigma_todo with
| [] ->
(None, None)
| hpred :: sigma_todo' ->
| hpred :: sigma_todo' -> (
match do_hpred sigma_acc sigma_todo' hpred with
| Some de, typo ->
(Some de, typo)
| None, _ ->
find (hpred :: sigma_acc) sigma_todo' exp
find (hpred :: sigma_acc) sigma_todo' exp )
in
let res = find [] prop.Prop.sigma exp_ in
( if verbose then
@ -685,11 +674,11 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
L.d_str "vpath_find: cannot find " ;
Sil.d_exp exp_ ;
L.d_ln ()
| Some de, typo ->
| Some de, typo -> (
L.d_str "vpath_find: found " ;
L.d_str (DExp.to_string de) ;
L.d_str " : " ;
match typo with None -> L.d_str " No type" | Some typ -> Typ.d_full typ ; L.d_ln () ) ;
match typo with None -> L.d_str " No type" | Some typ -> Typ.d_full typ ; L.d_ln () ) ) ;
res
@ -813,8 +802,7 @@ let explain_dexp_access prop dexp is_nullable =
| DExp.Dbinop (Binop.PlusPI, DExp.Dpvar _, DExp.Dconst _) as de ->
if verbose then L.d_strln ("lookup: case )pvar + constant) " ^ DExp.to_string de) ;
None
| DExp.Dfcall (DExp.Dconst c, _, loc, _)
-> (
| DExp.Dfcall (DExp.Dconst c, _, loc, _) -> (
if verbose then L.d_strln "lookup: found Dfcall " ;
match c with
| Const.Cfun _ ->
@ -968,8 +956,8 @@ let rec find_outermost_dereference tenv node e =
if outermost_dereference is true, stop at the outermost dereference
(skipping e.g. outermost field access) *)
let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = false)
?(outermost_dereference= false) ?(is_nullable= false) ?(is_premature_nil= false) deref_str prop
loc =
?(outermost_dereference = false) ?(is_nullable = false) ?(is_premature_nil = false) deref_str
prop loc =
let find_exp_dereferenced () =
match State.get_instr () with
| Some (Sil.Store (e, _, _, _)) ->
@ -1073,7 +1061,7 @@ let explain_nth_function_parameter proc_name tenv use_buckets deref_str prop n p
let find_with_exp prop exp =
let res = ref None in
let found_in_pvar pv =
if not (Pvar.is_abduced pv) && not (Pvar.is_this pv) then res := Some (pv, Fpvar)
if (not (Pvar.is_abduced pv)) && not (Pvar.is_this pv) then res := Some (pv, Fpvar)
in
let found_in_struct pv fld_lst =
(* found_in_pvar has priority *)

@ -44,7 +44,13 @@ val explain_array_access :
(** Produce a description of the array access performed in the current instruction, if any. *)
val explain_class_cast_exception :
Tenv.t -> Typ.Procname.t option -> Exp.t -> Exp.t -> Exp.t -> Procdesc.Node.t -> Location.t
Tenv.t
-> Typ.Procname.t option
-> Exp.t
-> Exp.t
-> Exp.t
-> Procdesc.Node.t
-> Location.t
-> Localise.error_desc
(** explain a class cast exception *)
@ -55,13 +61,29 @@ val explain_deallocate_constant_string : string -> PredSymb.res_action -> Locali
(** Explain a deallocate constant string error *)
val explain_dereference :
Typ.Procname.t -> Tenv.t -> ?use_buckets:bool -> ?is_nullable:bool -> ?is_premature_nil:bool
-> Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc
Typ.Procname.t
-> Tenv.t
-> ?use_buckets:bool
-> ?is_nullable:bool
-> ?is_premature_nil:bool
-> Localise.deref_str
-> 'a Prop.t
-> Location.t
-> Localise.error_desc
(** Produce a description of which expression is dereferenced in the current instruction, if any. *)
val explain_dereference_as_caller_expression :
Typ.Procname.t -> Tenv.t -> ?use_buckets:bool -> Localise.deref_str -> 'a Prop.t -> 'b Prop.t
-> Exp.t -> Procdesc.Node.t -> Location.t -> Pvar.t list -> Localise.error_desc
Typ.Procname.t
-> Tenv.t
-> ?use_buckets:bool
-> Localise.deref_str
-> 'a Prop.t
-> 'b Prop.t
-> Exp.t
-> Procdesc.Node.t
-> Location.t
-> Pvar.t list
-> Localise.error_desc
(** return a description explaining value [exp] in [prop] in terms of a source expression
using the formal parameters of the call *)
@ -87,7 +109,11 @@ val explain_unary_minus_applied_to_unsigned_expression :
(** explain unary minus applied to unsigned expression *)
val explain_leak :
Tenv.t -> Sil.hpred -> 'a Prop.t -> PredSymb.t option -> string option
Tenv.t
-> Sil.hpred
-> 'a Prop.t
-> PredSymb.t option
-> string option
-> Exceptions.visibility * Localise.error_desc
(** Produce a description of a leak by looking at the current state.
If the current instruction is a variable nullify, blame the variable.

@ -84,7 +84,7 @@ let get_tenv exe_env proc_name =
match proc_name with
| Typ.Procname.Java _ ->
Lazy.force java_global_tenv
| _ ->
| _ -> (
match get_file_data exe_env proc_name with
| Some file_data -> (
match file_data_to_tenv file_data with
@ -99,7 +99,7 @@ let get_tenv exe_env proc_name =
let loc = State.get_loc () in
L.(die InternalError)
"get_tenv: file_data not found for %a in file '%a' at %a" Typ.Procname.pp proc_name
SourceFile.pp loc.Location.file Location.pp loc
SourceFile.pp loc.Location.file Location.pp loc )
(** return the cfg associated to the procedure *)

@ -45,7 +45,7 @@ let is_matching patterns source_file =
(** Check if a proc name is matching the name given as string. *)
let match_method language proc_name method_name =
not (BuiltinDecl.is_declared proc_name)
(not (BuiltinDecl.is_declared proc_name))
&& Language.equal (Typ.Procname.get_language proc_name) language
&& String.equal (Typ.Procname.get_method proc_name) method_name
@ -73,14 +73,14 @@ module FileContainsStringMatcher = struct
let source_map = ref SourceFile.Map.empty in
let regexp = Str.regexp (String.concat ~sep:"\\|" s_patterns) in
fun source_file ->
try SourceFile.Map.find source_file !source_map with Caml.Not_found ->
try SourceFile.Map.find source_file !source_map with Caml.Not_found -> (
try
let file_in = In_channel.create (SourceFile.to_abs_path source_file) in
let pattern_found = file_contains regexp file_in in
In_channel.close file_in ;
source_map := SourceFile.Map.add source_file pattern_found !source_map ;
pattern_found
with Sys_error _ -> false
with Sys_error _ -> false )
end
type method_pattern = {class_name: string; method_name: string option}
@ -309,7 +309,8 @@ let filters_from_inferconfig inferconfig : filters =
in
function
| source_file ->
whitelist_filter source_file && not (blacklist_filter source_file)
whitelist_filter source_file
&& (not (blacklist_filter source_file))
&& not (blacklist_files_containing_filter source_file)
in
let error_filter = function

@ -89,7 +89,7 @@ let should_link ~target ~target_results_dir ~stats infer_out_src infer_out_dst =
~f:(fun file ->
let file_path = Filename.concat captured_file file in
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
else true
in

@ -60,7 +60,8 @@ let should_be_analyzed proc_name proc_attributes =
| None ->
false
in
should_create_summary proc_name proc_attributes && not (is_active proc_name)
should_create_summary proc_name proc_attributes
&& (not (is_active proc_name))
&& (* avoid infinite loops *)
not (already_analyzed proc_name)
@ -172,7 +173,7 @@ let run_proc_analysis analyze_proc ~caller_pdesc callee_pdesc =
in
let final_summary = postprocess summary in
restore_global_state old_state ; final_summary
with exn ->
with exn -> (
IExn.reraise_if exn ~f:(fun () -> restore_global_state old_state ; not Config.keep_going) ;
L.internal_error "@\nERROR RUNNING BACKEND: %a %s@\n@\nBACK TRACE@\n%s@?" Typ.Procname.pp
callee_pname (Exn.to_string exn) (Printexc.get_backtrace ()) ;
@ -183,7 +184,7 @@ let run_proc_analysis analyze_proc ~caller_pdesc callee_pdesc =
log_error_and_continue exn initial_summary kind
| _ ->
(* this happens with assert false or some other unrecognized exception *)
log_error_and_continue exn initial_summary (FKcrash (Exn.to_string exn))
log_error_and_continue exn initial_summary (FKcrash (Exn.to_string exn)) )
let analyze_proc ?caller_pdesc callee_pdesc =

@ -144,8 +144,7 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
(fun var (pvars_acc, ids_acc) ->
match Var.to_exp var with
(* we nullify all address taken variables at the end of the procedure *)
| Exp.Lvar pvar
when not (AddressTaken.Domain.mem pvar address_taken_vars) ->
| Exp.Lvar pvar when not (AddressTaken.Domain.mem pvar address_taken_vars) ->
(pvar :: pvars_acc, ids_acc)
| Exp.Var id ->
(pvars_acc, id :: ids_acc)

@ -36,19 +36,18 @@ module LineReader = struct
in
lines := line :: !lines
done ;
assert false
(* execution never reaches here *)
assert false (* execution never reaches here *)
with End_of_file ->
In_channel.close cin ;
Array.of_list (List.rev !lines)
let file_data (hash : t) fname =
try Some (Hashtbl.find hash fname) with Caml.Not_found ->
try Some (Hashtbl.find hash fname) with Caml.Not_found -> (
try
let lines_arr = read_file (SourceFile.to_abs_path fname) in
Hashtbl.add hash fname lines_arr ; Some lines_arr
with exn when SymOp.exn_not_failure exn -> None
with exn when SymOp.exn_not_failure exn -> None )
let from_file_linenum_original hash fname linenum =
@ -114,8 +113,14 @@ let pp_node_link path_to_root ?proof_cover ~description fmt node =
when starting and finishing the processing of a node *)
module NodesHtml : sig
val start_node :
int -> Location.t -> Typ.Procname.t -> Procdesc.Node.t list -> Procdesc.Node.t list
-> Procdesc.Node.t list -> SourceFile.t -> bool
int
-> Location.t
-> Typ.Procname.t
-> Procdesc.Node.t list
-> Procdesc.Node.t list
-> Procdesc.Node.t list
-> SourceFile.t
-> bool
val finish_node : Typ.Procname.t -> int -> SourceFile.t -> unit
end = struct
@ -189,7 +194,8 @@ let start_session ~pp_name node (loc: Location.t) proc_name session source =
node Io_infer.Html.pp_end_color () ;
F.fprintf !curr_html_formatter "%a%a %t" Io_infer.Html.pp_hline ()
(Io_infer.Html.pp_session_link source ~with_name:true [".."] ~proc_name)
((node_id :> int), session, loc.Location.line) pp_name ;
((node_id :> int), session, loc.Location.line)
pp_name ;
F.fprintf !curr_html_formatter "<LISTING>%a" Io_infer.Html.pp_start_color Pp.Black
@ -268,7 +274,8 @@ let write_html_proc source proof_cover table_nodes_at_linenum global_err_log pro
in
let proc_loc = Procdesc.get_loc proc_desc in
let process_proc =
Procdesc.is_defined proc_desc && SourceFile.equal proc_loc.Location.file source
Procdesc.is_defined proc_desc
&& SourceFile.equal proc_loc.Location.file source
&&
match Attributes.find_file_capturing_procedure proc_name with
| None ->

@ -9,19 +9,25 @@ open! IStd
module L = Logging
type log_t =
?ltr:Errlog.loc_trace -> ?linters_def_file:string -> ?doc_url:string -> ?access:string
-> ?extras:Jsonbug_t.extra -> exn -> unit
?ltr:Errlog.loc_trace
-> ?linters_def_file:string
-> ?doc_url:string
-> ?access:string
-> ?extras:Jsonbug_t.extra
-> exn
-> unit
let log_issue_from_errlog procname ~clang_method_kind severity err_log ~loc ~node ~ltr
~linters_def_file ~doc_url ~access ~extras exn =
let issue_type = (Exceptions.recognize_exception exn).name in
if not Config.filtering (* no-filtering takes priority *) || issue_type.IssueType.enabled then
if (not Config.filtering) (* no-filtering takes priority *) || issue_type.IssueType.enabled then
let session = (State.get_session () :> int) in
Errlog.log_issue procname ~clang_method_kind severity err_log ~loc ~node ~session ~ltr
~linters_def_file ~doc_url ~access ~extras exn
let log_frontend_issue procname severity errlog ~loc ~node_key ~ltr ~linters_def_file ~doc_url exn =
let log_frontend_issue procname severity errlog ~loc ~node_key ~ltr ~linters_def_file ~doc_url exn
=
let node = Errlog.FrontendNode {node_key} in
log_issue_from_errlog procname ~clang_method_kind:None severity errlog ~loc ~node ~ltr
~linters_def_file ~doc_url ~access:None ~extras:None exn

@ -10,8 +10,13 @@ open! IStd
(** Type of functions to report issues to the error_log in a spec. *)
type log_t =
?ltr:Errlog.loc_trace -> ?linters_def_file:string -> ?doc_url:string -> ?access:string
-> ?extras:Jsonbug_t.extra -> exn -> unit
?ltr:Errlog.loc_trace
-> ?linters_def_file:string
-> ?doc_url:string
-> ?access:string
-> ?extras:Jsonbug_t.extra
-> exn
-> unit
val log_issue_deprecated :
Exceptions.severity -> Typ.Procname.t -> ?node:Procdesc.Node.t -> ?loc:Location.t -> log_t
@ -20,9 +25,16 @@ val log_issue_deprecated :
Use log_error/warning instead *)
val log_frontend_issue :
Typ.Procname.t -> Exceptions.severity -> Errlog.t -> loc:Location.t
-> node_key:Procdesc.NodeKey.t -> ltr:Errlog.loc_trace -> linters_def_file:string option
-> doc_url:string option -> exn -> unit
Typ.Procname.t
-> Exceptions.severity
-> Errlog.t
-> loc:Location.t
-> node_key:Procdesc.NodeKey.t
-> ltr:Errlog.loc_trace
-> linters_def_file:string option
-> doc_url:string option
-> exn
-> unit
(** Report a frontend issue of a given kind in the given error log. *)
val log_error : Summary.t -> loc:Location.t -> log_t
@ -32,8 +44,14 @@ val log_warning : Summary.t -> loc:Location.t -> log_t
(** Add an warning to the given summary. *)
val log_issue_external :
Typ.Procname.t -> Exceptions.severity -> loc:Location.t -> ltr:Errlog.loc_trace -> ?access:string
-> IssueType.t -> string -> unit
Typ.Procname.t
-> Exceptions.severity
-> loc:Location.t
-> ltr:Errlog.loc_trace
-> ?access:string
-> IssueType.t
-> string
-> unit
(** Log an issue to the error log in [IssueLog] associated with the given procname. *)
val is_suppressed :

@ -238,7 +238,8 @@ $(b,infer) $(i,[options])|}
"cxx": false,
"infer-blacklist-files-containing": ["@generated","@Generated"]
}|}
] ~see_also:InferCommand.all_commands "infer"
]
~see_also:InferCommand.all_commands "infer"
let report =

@ -218,7 +218,8 @@ let add parse_mode sections desc =
in
(* in the help of `infer` itself, show in which specific commands the option is used *)
let commands =
List.map ~f:fst sections |> List.sort ~compare:InferCommand.compare
List.map ~f:fst sections
|> List.sort ~compare:InferCommand.compare
|> List.remove_consecutive_duplicates ~equal:InferCommand.equal
|> List.map ~f:(fun cmd ->
let exe = InferCommand.to_exe_name cmd in
@ -316,8 +317,14 @@ let curr_command = ref None
(* end parsing state *)
type 'a t =
?deprecated:string list -> long:Arg.key -> ?short:char -> ?parse_mode:parse_mode
-> ?in_help:(InferCommand.t * string) list -> ?meta:string -> Arg.doc -> 'a
?deprecated:string list
-> long:Arg.key
-> ?short:char
-> ?parse_mode:parse_mode
-> ?in_help:(InferCommand.t * string) list
-> ?meta:string
-> Arg.doc
-> 'a
let string_json_decoder ~long ~inferconfig_dir:_ json = [dashdash long; YBU.to_string json]
@ -370,8 +377,8 @@ let mk_option ?(default= None) ?(default_to_string= fun _ -> "") ~f ?(mk_reset=
else mk ()
let mk_bool ?(deprecated_no= []) ?(default= false) ?(f= fun b -> b) ?(deprecated= []) ~long ?short
?parse_mode ?in_help ?(meta= "") doc0 =
let mk_bool ?(deprecated_no = []) ?(default = false) ?(f = fun b -> b) ?(deprecated = []) ~long
?short ?parse_mode ?in_help ?(meta = "") doc0 =
let nolong =
let len = String.length long in
if len > 3 && String.sub long ~pos:0 ~len:3 = "no-" then String.sub long ~pos:3 ~len:(len - 3)
@ -423,8 +430,8 @@ let mk_bool_group ?(deprecated_no= []) ?(default= false) ?f:(f0 = Fn.id) ?(depre
mk_bool ~deprecated ~deprecated_no ~default ~long ?short ~f ?parse_mode ?in_help ?meta doc
let mk_int ~default ?(f= Fn.id) ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "int")
doc =
let mk_int ~default ?(f = Fn.id) ?(deprecated = []) ~long ?short ?parse_mode ?in_help
?(meta = "int") 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))
@ -439,7 +446,8 @@ let mk_int_opt ?default ?f:(f0 = Fn.id) ?(deprecated= []) ~long ?short ?parse_mo
mk_option ~deprecated ~long ?short ~default ~default_to_string ~f ?parse_mode ?in_help ~meta doc
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 =
let default_to_string = function Some f -> string_of_float f | None -> "" in
let f s = Some (float_of_string s) in
mk_option ~deprecated ~long ?short ~default ~default_to_string ~f ?parse_mode ?in_help ~meta doc
@ -507,7 +515,8 @@ let mk_path ~default ?(f= Fn.id) ?(deprecated= []) ~long ?short ?parse_mode ?in_
~default ~deprecated ~long ~short ~parse_mode ~in_help ~meta
let mk_path_opt ?default ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "path") doc =
let mk_path_opt ?default ?(deprecated = []) ~long ?short ?parse_mode ?in_help ?(meta = "path") doc
=
let mk () =
mk_path_helper
~setter:(fun var x -> var := Some x)
@ -519,8 +528,8 @@ let mk_path_opt ?default ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(m
mk_with_reset None ~reset_doc ~long ?parse_mode mk
let mk_path_list ?(default= []) ?(deprecated= []) ~long ?short ?parse_mode ?in_help ?(meta= "path")
doc =
let mk_path_list ?(default = []) ?(deprecated = []) ~long ?short ?parse_mode ?in_help
?(meta = "path") doc =
let mk () =
mk_path_helper
~setter:(fun var x -> var := x :: !var)
@ -537,8 +546,8 @@ let mk_symbols_meta symbols =
Printf.sprintf "{ %s }" (String.concat ~sep:" | " strings)
let mk_symbol ~default ~symbols ~eq ?(f= Fn.id) ?(deprecated= []) ~long ?short ?parse_mode ?in_help
?meta doc =
let mk_symbol ~default ~symbols ~eq ?(f = Fn.id) ?(deprecated = []) ~long ?short ?parse_mode
?in_help ?meta doc =
let strings = List.map ~f:fst symbols in
let sym_to_str = List.map ~f:(fun (x, y) -> (y, x)) symbols in
let of_string str = List.Assoc.find_exn ~equal:String.equal symbols str in
@ -551,8 +560,8 @@ let mk_symbol ~default ~symbols ~eq ?(f= Fn.id) ?(deprecated= []) ~long ?short ?
~mk_spec:(fun set -> Symbol (strings, set))
let mk_symbol_opt ~symbols ?(f= Fn.id) ?(mk_reset= true) ?(deprecated= []) ~long ?short ?parse_mode
?in_help ?meta doc =
let mk_symbol_opt ~symbols ?(f = Fn.id) ?(mk_reset = true) ?(deprecated = []) ~long ?short
?parse_mode ?in_help ?meta doc =
let strings = List.map ~f:fst symbols in
let of_string str = List.Assoc.find_exn ~equal:String.equal symbols str in
let meta = Option.value meta ~default:(mk_symbols_meta symbols) in
@ -677,8 +686,8 @@ let set_curr_speclist_for_parse_mode ~usage parse_mode =
List.Assoc.find_exn ~equal:equal_parse_mode parse_mode_desc_lists parse_mode
in
curr_speclist :=
normalize_desc_list !full_desc_list |> List.map ~f:xdesc |> add_or_suppress_help
|> to_arg_speclist ;
normalize_desc_list !full_desc_list
|> List.map ~f:xdesc |> add_or_suppress_help |> to_arg_speclist ;
assert (check_no_duplicates !curr_speclist) ;
curr_usage
@ -814,7 +823,7 @@ let encode_argv_to_env argv =
String.concat ~sep:(String.make 1 env_var_sep)
(List.filter
~f:(fun arg ->
not (String.contains arg env_var_sep)
(not (String.contains arg env_var_sep))
||
( warnf "WARNING: Ignoring unsupported option containing '%c' character: %s@\n"
env_var_sep arg ;
@ -973,12 +982,12 @@ let show_manual ?internal_section format default_doc command_opt =
match command_opt with
| None ->
default_doc
| Some command ->
| Some command -> (
match List.Assoc.find_exn ~equal:InferCommand.equal !subcommands command with
| Some command_doc, _, _ ->
command_doc
| None, _, _ ->
L.(die InternalError) "No manual for internal command %s" (string_of_command command)
L.(die InternalError) "No manual for internal command %s" (string_of_command command) )
in
let pp_meta f meta =
match meta with "" -> () | meta -> F.fprintf f " $(i,%s)" (Cmdliner.Manpage.escape meta)
@ -1007,12 +1016,11 @@ let show_manual ?internal_section format default_doc command_opt =
match command_doc.manual_options with
| `Replace blocks ->
`S Cmdliner.Manpage.s_options :: blocks
| `Prepend blocks ->
| `Prepend blocks -> (
let hidden =
match internal_section with
| Some section ->
`S section
:: `P "Use at your own risk."
`S section :: `P "Use at your own risk."
:: List.concat_map ~f:block_of_desc (normalize_desc_list !hidden_descs_list)
| None ->
[]
@ -1026,11 +1034,13 @@ let show_manual ?internal_section format default_doc command_opt =
(fun section descs result ->
`S section
:: (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
| None ->
`S Cmdliner.Manpage.s_options :: blocks
@ List.concat_map ~f:block_of_desc (normalize_desc_list !visible_descs_list) @ hidden
(`S Cmdliner.Manpage.s_options :: blocks)
@ List.concat_map ~f:block_of_desc (normalize_desc_list !visible_descs_list)
@ hidden )
in
let blocks =
[ `Blocks command_doc.manual_before_options

@ -41,8 +41,14 @@ val init_work_dir : string
- a documentation string
*)
type 'a t =
?deprecated:string list -> long:string -> ?short:char -> ?parse_mode:parse_mode
-> ?in_help:(InferCommand.t * string) list -> ?meta:string -> string -> 'a
?deprecated:string list
-> long:string
-> ?short:char
-> ?parse_mode:parse_mode
-> ?in_help:(InferCommand.t * string) list
-> ?meta:string
-> string
-> 'a
val mk_set : 'a ref -> 'a -> unit t
(** [mk_set variable value] defines a command line option which sets [variable] to [value]. *)
@ -55,7 +61,9 @@ val mk_bool : ?deprecated_no:string list -> ?default:bool -> ?f:(bool -> bool) -
either "Activates:" or "Deactivates:", so should be phrased accordingly. *)
val mk_bool_group :
?deprecated_no:string list -> ?default:bool -> ?f:(bool -> bool)
?deprecated_no:string list
-> ?default:bool
-> ?f:(bool -> bool)
-> (bool ref list -> bool ref list -> bool ref) t
(** [mk_bool_group children not_children] behaves as [mk_bool] with the addition that all the
[children] are also set and the [no_children] are unset. A child can be unset by including
@ -114,8 +122,12 @@ val mk_anon : unit -> string list ref
order they appeared on the command line. *)
val mk_rest_actions :
?parse_mode:parse_mode -> ?in_help:(InferCommand.t * string) list -> string -> usage:string
-> (string -> parse_mode) -> string list ref
?parse_mode:parse_mode
-> ?in_help:(InferCommand.t * string) list
-> string
-> usage:string
-> (string -> parse_mode)
-> string list ref
(** [mk_rest_actions doc ~usage command_to_parse_mode] defines a [string list ref] of the command
line arguments following ["--"], in the reverse order they appeared on the command line. [usage]
is the usage message in case of parse errors or if --help is passed. For example, calling
@ -127,13 +139,23 @@ val mk_rest_actions :
type command_doc
val mk_command_doc :
title:string -> section:int -> version:string -> date:string -> short_description:string
-> synopsis:Cmdliner.Manpage.block list -> description:Cmdliner.Manpage.block list
title:string
-> section:int
-> version:string
-> date:string
-> short_description:string
-> synopsis:Cmdliner.Manpage.block list
-> description:Cmdliner.Manpage.block list
-> ?options:[`Prepend of Cmdliner.Manpage.block list | `Replace of Cmdliner.Manpage.block list]
-> ?exit_status:Cmdliner.Manpage.block list -> ?environment:Cmdliner.Manpage.block list
-> ?files:Cmdliner.Manpage.block list -> ?notes:Cmdliner.Manpage.block list
-> ?bugs:Cmdliner.Manpage.block list -> ?examples:Cmdliner.Manpage.block list
-> see_also:Cmdliner.Manpage.block list -> string -> command_doc
-> ?exit_status:Cmdliner.Manpage.block list
-> ?environment:Cmdliner.Manpage.block list
-> ?files:Cmdliner.Manpage.block list
-> ?notes:Cmdliner.Manpage.block list
-> ?bugs:Cmdliner.Manpage.block list
-> ?examples:Cmdliner.Manpage.block list
-> see_also:Cmdliner.Manpage.block list
-> string
-> command_doc
(** [mk_command_doc ~title ~section ~version ~short_description ~synopsis ~description ~see_also
command_exe] records information about a command that is used to create its man page. A lot of
the concepts are taken from man-pages(7).
@ -152,9 +174,14 @@ val mk_command_doc :
*)
val mk_subcommand :
InferCommand.t -> ?on_unknown_arg:[`Add | `Skip | `Reject] -> name:string
-> ?deprecated_long:string -> ?parse_mode:parse_mode -> ?in_help:(InferCommand.t * string) list
-> command_doc option -> unit
InferCommand.t
-> ?on_unknown_arg:[`Add | `Skip | `Reject]
-> name:string
-> ?deprecated_long:string
-> ?parse_mode:parse_mode
-> ?in_help:(InferCommand.t * string) list
-> command_doc option
-> unit
(** [mk_subcommand command ~long command_doc] defines the subcommand [command]. A subcommand is
activated by passing [name], and by passing [--deprecated_long] if specified. A man page is
automatically generated for [command] based on the information in [command_doc], if available
@ -174,7 +201,10 @@ val extend_env_args : string list -> unit
(** [extend_env_args args] appends [args] to those passed via [args_env_var] *)
val parse :
?config_file:string -> usage:Arg.usage_msg -> parse_mode -> InferCommand.t option
?config_file:string
-> usage:Arg.usage_msg
-> parse_mode
-> InferCommand.t option
-> InferCommand.t option * (int -> 'a)
(** [parse ~usage parse_mode command] parses command line arguments as specified by preceding calls
to the [mk_*] functions, and returns:
@ -198,7 +228,10 @@ val is_env_var_set : string -> bool
(** [is_env_var_set var] is true if $[var]=1 *)
val show_manual :
?internal_section:string -> Cmdliner.Manpage.format -> command_doc -> InferCommand.t option
?internal_section:string
-> Cmdliner.Manpage.format
-> command_doc
-> InferCommand.t option
-> unit
(** Display the manual of [command] to the user, or [command_doc] if [command] is None. [format] is
used as for [Cmdliner.Manpage.print]. If [internal_section] is specified, add a section titled

@ -134,7 +134,8 @@ let build_system_of_exe_name name =
@[<v2> %a@]"
name
(Pp.seq ~print_env:Pp.text_break ~sep:"" F.pp_print_string)
( List.map ~f:fst build_system_exe_assoc |> List.map ~f:string_of_build_system
( List.map ~f:fst build_system_exe_assoc
|> List.map ~f:string_of_build_system
|> List.dedup_and_sort ~compare:String.compare )
@ -619,11 +620,7 @@ and analyzer =
match Checkers with
(* NOTE: if compilation fails here, it means you have added a new analyzer without updating the
documentation of this option *)
| CaptureOnly
| CompileOnly
| Checkers
| Crashcontext
| Linters ->
| CaptureOnly | CompileOnly | Checkers | Crashcontext | Linters ->
()
in
CLOpt.mk_symbol_opt ~deprecated:["analyzer"] ~long:"analyzer" ~short:'a'
@ -762,7 +759,8 @@ and ( annotation_reachability
|> String.concat ~sep:", " ) )
~f:(fun b ->
List.iter
~f:(fun (var, _, _, default) -> var := if b then default || !var else not default && !var)
~f:(fun (var, _, _, default) ->
var := if b then default || !var else (not default) && !var )
!all_checkers ;
b )
[] (* do all the work in ~f *)
@ -818,7 +816,9 @@ and array_level =
and blacklist =
CLOpt.mk_string_opt ~deprecated:["-blacklist-regex"; "-blacklist"] ~long:"buck-blacklist"
CLOpt.mk_string_opt
~deprecated:["-blacklist-regex"; "-blacklist"]
~long:"buck-blacklist"
~in_help:InferCommand.[(Run, manual_buck_flavors); (Capture, manual_buck_flavors)]
~meta:"regex" "Skip analysis of files matched by the specified regular expression"
@ -1105,7 +1105,8 @@ and ( bo_debug
; reports_include_ml_loc
; trace_error
; write_html
; write_dotty ] [filtering; only_cheap_debug]
; write_dotty ]
[filtering; only_cheap_debug]
and _ : int option ref =
CLOpt.mk_int_opt ~long:"debug-level" ~in_help:all_generic_manuals ~meta:"level"
~f:(fun level -> set_debug_level level ; level)
@ -1118,7 +1119,8 @@ and ( bo_debug
"Generate lightweight debugging information: just print the internal exceptions during \
analysis (also sets $(b,--developer-mode), $(b,--no-filtering), $(b,--print-buckets), \
$(b,--reports-include-ml-loc))"
[developer_mode; print_buckets; reports_include_ml_loc] [filtering; keep_going]
[developer_mode; print_buckets; reports_include_ml_loc]
[filtering; keep_going]
and default_linters =
CLOpt.mk_bool ~long:"default-linters"
~in_help:InferCommand.[(Capture, manual_clang_linters)]
@ -1228,7 +1230,8 @@ and () =
By default, the following issue types are disabled: %s.\n\n \
See also $(b,--report-issue-type).\n"
(String.concat ~sep:", " disabled_issues_ids)) ;
mk true ~long:"enable-issue-type" ~deprecated:["enable_checks"; "-enable-checks"]
mk true ~long:"enable-issue-type"
~deprecated:["enable_checks"; "-enable-checks"]
"Show reports coming from this type of issue. By default, all issue types are enabled except \
the ones listed in $(b,--disable-issue-type). Note that enabling issue types does not make \
the corresponding checker run; see individual checker options to turn them on or off."
@ -1446,7 +1449,8 @@ and issues_fields =
; `Issue_field_bug_type
; `Issue_field_bucket
; `Issue_field_kind
; `Issue_field_bug_trace ] ~symbols:issues_fields_symbols ~eq:PolyVariantEqual.( = )
; `Issue_field_bug_trace ]
~symbols:issues_fields_symbols ~eq:PolyVariantEqual.( = )
"Fields to emit with $(b,--issues-tests)"
@ -1765,15 +1769,17 @@ and progress_bar =
and progress_bar_style =
CLOpt.mk_symbol ~long:"progress-bar-style"
~symbols:[("auto", `Auto); ("plain", `Plain); ("multiline", `MultiLine)] ~eq:Pervasives.( = )
~default:`Auto ~in_help:[(Analyze, manual_generic); (Capture, manual_generic)]
~symbols:[("auto", `Auto); ("plain", `Plain); ("multiline", `MultiLine)]
~eq:Pervasives.( = ) ~default:`Auto
~in_help:[(Analyze, manual_generic); (Capture, manual_generic)]
"Style of the progress bar. $(b,auto) selects $(b,multiline) if connected to a tty, otherwise \
$(b,plain)."
and project_root =
CLOpt.mk_path ~deprecated:["project_root"; "-project_root"; "pr"] ~long:"project-root" ~short:'C'
~default:CLOpt.init_work_dir
CLOpt.mk_path
~deprecated:["project_root"; "-project_root"; "pr"]
~long:"project-root" ~short:'C' ~default:CLOpt.init_work_dir
~in_help:
InferCommand.
[ (Analyze, manual_generic)
@ -2016,7 +2022,8 @@ and specs_library =
in
(* Add the newline-separated directories listed in <file> to the list of directories to be
searched for .spec files *)
CLOpt.mk_path ~deprecated:["specs-dir-list-file"; "-specs-dir-list-file"]
CLOpt.mk_path
~deprecated:["specs-dir-list-file"; "-specs-dir-list-file"]
~long:"specs-library-index" ~default:""
~f:(fun file ->
specs_library := read_specs_dir_list_file file @ !specs_library ;
@ -2091,8 +2098,9 @@ and profiler_samples =
and testing_mode =
CLOpt.mk_bool ~deprecated:["testing_mode"; "-testing_mode"; "tm"] ~deprecated_no:["ntm"]
~long:"testing-mode"
CLOpt.mk_bool
~deprecated:["testing_mode"; "-testing_mode"; "tm"]
~deprecated_no:["ntm"] ~long:"testing-mode"
"Mode for testing, where no headers are translated, and dot files are created (clang only)"
@ -2326,7 +2334,7 @@ let post_parsing_initialization command_opt =
error "Uncaught Internal Error: " (Exn.to_string exn)
in
print_exception () ;
if not is_infer_exit_zero && (should_print_backtrace_default || !developer_mode) then (
if (not is_infer_exit_zero) && (should_print_backtrace_default || !developer_mode) then (
ANSITerminal.prerr_string L.(term_styles_of_style Error) "Error backtrace:\n" ;
ANSITerminal.prerr_string L.(term_styles_of_style Error) backtrace ) ;
if not is_infer_exit_zero then Out_channel.newline stderr ;

@ -80,7 +80,8 @@ type analysis_issue =
let create_analysis_issue_row base record =
let open JsonBuilder in
base |> add_string ~key:"bug_kind" ~data:record.bug_kind
base
|> add_string ~key:"bug_kind" ~data:record.bug_kind
|> add_string ~key:"bug_type" ~data:record.bug_type
|> add_string_opt ~key:"clang_method_kind" ~data:record.clang_method_kind
|> add_string_opt ~key:"exception_triggered_location"
@ -109,7 +110,8 @@ type analysis_stats =
let create_analysis_stats_row base record =
let open JsonBuilder in
base |> add_int ~key:"analysis_nodes_visited" ~data:record.analysis_nodes_visited
base
|> add_int ~key:"analysis_nodes_visited" ~data:record.analysis_nodes_visited
|> add_string ~key:"analysis_status"
~data:
(Option.value_map record.analysis_status ~default:"OK" ~f:(fun stats_failure ->
@ -171,7 +173,8 @@ let create_call_trace_row base record =
~data:(Option.map ~f:SourceFile.to_rel_path record.callee_source_file)
|> add_string ~key:"callee_name" ~data:record.callee_name
|> add_string ~key:"caller_name" ~data:record.caller_name
|> add_string ~key:"lang" ~data:record.lang |> add_string_opt ~key:"reason" ~data:record.reason
|> add_string ~key:"lang" ~data:record.lang
|> add_string_opt ~key:"reason" ~data:record.reason
|> add_string ~key:"dynamic_dispatch"
~data:(string_of_dynamic_dispatch_opt record.dynamic_dispatch)
@ -186,7 +189,8 @@ type frontend_exception =
let create_frontend_exception_row base record =
let open JsonBuilder in
base |> add_string_opt ~key:"ast_node" ~data:record.ast_node
base
|> add_string_opt ~key:"ast_node" ~data:record.ast_node
|> add_string ~key:"exception_triggered_location"
~data:(Logging.ocaml_pos_to_string record.exception_triggered_location)
|> add_string ~key:"exception_type" ~data:record.exception_type
@ -239,7 +243,8 @@ let create_performance_stats_row base record =
let open JsonBuilder in
let add_mem_perf t =
Option.value_map ~default:t record.mem_perf ~f:(fun mem_perf ->
t |> add_float ~key:"minor_heap_mem" ~data:mem_perf.minor_heap_mem
t
|> add_float ~key:"minor_heap_mem" ~data:mem_perf.minor_heap_mem
|> add_float ~key:"promoted_minor_heap_mem" ~data:mem_perf.promoted_minor_heap_mem
|> add_float ~key:"major_heap_mem" ~data:mem_perf.major_heap_mem
|> add_float ~key:"total_allocated_mem" ~data:mem_perf.total_allocated_mem
@ -252,16 +257,19 @@ let create_performance_stats_row base record =
in
let add_time_perf t =
Option.value_map ~default:t record.time_perf ~f:(fun time_perf ->
t |> add_float ~key:"real_time" ~data:time_perf.real_time
t
|> add_float ~key:"real_time" ~data:time_perf.real_time
|> add_float ~key:"user_time" ~data:time_perf.user_time
|> add_float ~key:"sys_time" ~data:time_perf.sys_time
|> add_float ~key:"children_user_time" ~data:time_perf.children_user_time
|> add_float ~key:"children_sys_time" ~data:time_perf.children_sys_time )
in
base |> add_string ~key:"lang" ~data:record.lang
base
|> add_string ~key:"lang" ~data:record.lang
|> add_string_opt ~key:"source_file"
~data:(Option.map ~f:SourceFile.to_rel_path record.source_file)
|> add_string ~key:"stats_type" ~data:record.stats_type |> add_mem_perf |> add_time_perf
|> add_string ~key:"stats_type" ~data:record.stats_type
|> add_mem_perf |> add_time_perf
type procedures_translated =
@ -272,7 +280,8 @@ type procedures_translated =
let create_procedures_translated_row base record =
let open JsonBuilder in
base |> add_string ~key:"lang" ~data:record.lang
base
|> add_string ~key:"lang" ~data:record.lang
|> add_int ~key:"procedures_translated_failed" ~data:record.procedures_translated_failed
|> add_int ~key:"procedures_translated_total" ~data:record.procedures_translated_total
|> add_string ~key:"source_file" ~data:(SourceFile.to_rel_path record.source_file)
@ -334,12 +343,14 @@ module LoggerImpl : S = struct
incr sequence_ctr ;
let open JsonBuilder in
let base =
empty |> add_string ~key:"command" ~data:(InferCommand.to_string Config.command)
empty
|> add_string ~key:"command" ~data:(InferCommand.to_string Config.command)
|> add_string ~key:"event_tag" ~data:(string_of_event event)
|> add_string ~key:"hostname" ~data:(Unix.gethostname ())
|> add_string ~key:"infer_commit" ~data:Version.commit
|> add_int ~key:"is_originator" ~data:(if CLOpt.is_originator then 1 else 0)
|> add_string_opt ~key:"job_id" ~data:Config.job_id |> add_int ~key:"pid" ~data:(pid ())
|> add_string_opt ~key:"job_id" ~data:Config.job_id
|> add_int ~key:"pid" ~data:(pid ())
|> add_string ~key:"run_identifier" ~data:(get_log_identifier ())
|> add_int ~key:"sequence" ~data:(!sequence_ctr - 1)
|> add_string ~key:"sysname" ~data:sysname
@ -359,7 +370,8 @@ module LoggerImpl : S = struct
| ProceduresTranslatedSummary record ->
create_procedures_translated_row base record
| UncaughtException (exn, exitcode) ->
base |> add_string ~key:"exception" ~data:(Caml.Printexc.exn_slot_name exn)
base
|> add_string ~key:"exception" ~data:(Caml.Printexc.exn_slot_name exn)
|> add_string ~key:"exception_info" ~data:(Exn.to_string exn)
|> add_int ~key:"exitcode" ~data:exitcode )
|> JsonBuilder.to_json

@ -62,7 +62,7 @@ let mk_file_formatter file_fmt category0 =
not (phys_equal !prev_category prefix)
in
if !is_newline || category_has_changed then (
if not !is_newline && category_has_changed then
if (not !is_newline) && category_has_changed then
(* category change but previous line has not ended: print newline *)
out_functions_orig.out_newline () ;
is_newline := false ;
@ -372,7 +372,9 @@ let pp_maybe_with_color color pp fmt x =
(** Execute the delayed print actions *)
let force_delayed_print fmt = function
| PTdecrease_indent n ->
for _ = 1 to n do F.fprintf fmt "@]" done
for _ = 1 to n do
F.fprintf fmt "@]"
done
| PTincrease_indent n ->
F.fprintf fmt "%s@[" (String.make (2 * n) ' ')
| PTstr s ->

@ -62,7 +62,7 @@ let resolve fname =
match lookup ~dir with
| None ->
fname
| Some links ->
| Some links -> (
try DB.filename_from_string (String.Table.find_exn links base) with
| Not_found_s _ | Caml.Not_found ->
fname
fname )

@ -23,7 +23,8 @@ let print_error_and_exit ?(exit_code= 1) fmt =
terminate. The standard out and error are not redirected. If the command fails to execute,
print an error message and exit. *)
let create_process_and_wait ~prog ~args =
Unix.fork_exec ~prog ~argv:(prog :: args) () |> Unix.waitpid
Unix.fork_exec ~prog ~argv:(prog :: args) ()
|> Unix.waitpid
|> function
| Ok () ->
()
@ -45,7 +46,7 @@ let pipeline ~producer_prog ~producer_args ~consumer_prog ~consumer_args =
Unix.close pipe_in ;
(* exec producer *)
never_returns (Unix.exec ~prog:producer_prog ~argv:producer_args ())
| `In_the_parent producer_pid ->
| `In_the_parent producer_pid -> (
match Unix.fork () with
| `In_the_child ->
(* redirect consumer's stdin to pipe_in *)
@ -62,4 +63,4 @@ let pipeline ~producer_prog ~producer_args ~consumer_prog ~consumer_args =
(* wait for children *)
let producer_status = Unix.waitpid producer_pid in
let consumer_status = Unix.waitpid consumer_pid in
(producer_status, consumer_status)
(producer_status, consumer_status) )

@ -17,6 +17,9 @@ val print_error_and_exit : ?exit_code:int -> ('a, Format.formatter, unit, 'b) fo
found in that file, and exist, with default code 1 or a given code. *)
val pipeline :
producer_prog:string -> producer_args:string list -> consumer_prog:string
-> consumer_args:string list -> Unix.Exit_or_signal.t * Unix.Exit_or_signal.t
producer_prog:string
-> producer_args:string list
-> consumer_prog:string
-> consumer_args:string list
-> Unix.Exit_or_signal.t * Unix.Exit_or_signal.t
(** Pipeline producer program into consumer program *)

@ -129,11 +129,11 @@ let process_updates pool buffer =
| UpdateStatus (slot, t, status) ->
TaskBar.update_status pool.task_bar ~slot t status
| Crash slot ->
let {pid} = (pool.slots).(slot) in
let {pid} = pool.slots.(slot) in
(* clean crash, give the child process a chance to cleanup *)
Unix.wait (`Pid pid) |> ignore ;
killall pool ~slot "see backtrace above"
| Ready slot ->
| Ready slot -> (
TaskBar.tasks_done_add pool.task_bar 1 ;
match pool.tasks with
| [] ->
@ -141,8 +141,8 @@ let process_updates pool buffer =
pool.idle_children <- pool.idle_children + 1
| x :: tasks ->
pool.tasks <- tasks ;
let {down_pipe} = (pool.slots).(slot) in
marshal_to_pipe down_pipe (Do x) )
let {down_pipe} = pool.slots.(slot) in
marshal_to_pipe down_pipe (Do x) ) )
(** terminate all worker processes *)
@ -235,7 +235,7 @@ let create : jobs:int -> child_prelude:(unit -> unit) -> f:('a -> unit) -> 'a t
(* Pipe to communicate from children to parent. Only one pipe is needed: the messages sent by
children include the identifier of the child sending the message (its [slot]). This way there
is only one pipe to wait on for updates. *)
let (pipe_child_r, pipe_child_w) as status_pipe = Unix.pipe () in
let ((pipe_child_r, pipe_child_w) as status_pipe) = Unix.pipe () in
let slots = Array.init jobs ~f:(fun slot -> fork_child ~child_prelude ~slot status_pipe ~f) in
(* we have forked the child processes and are now in the parent *)
let[@warning "-26"] pipe_child_w = Unix.close pipe_child_w in

@ -18,7 +18,8 @@ let is_results_dir ~check_correct_version () =
||
( not_found := d ^ "/" ;
false ) )
&& ( not check_correct_version || Sys.is_file ResultsDatabase.database_fullpath = `Yes
&& ( (not check_correct_version)
|| Sys.is_file ResultsDatabase.database_fullpath = `Yes
||
( not_found := ResultsDatabase.database_fullpath ;
false ) )

@ -58,13 +58,13 @@ let from_abs_path ?(warn_on_error= true) fname =
RelativeProjectRoot path
| None when Config.buck_cache_mode && Filename.check_suffix fname_real "java" ->
L.(die InternalError) "%s is not relative to %s" fname_real project_root_real
| None ->
| None -> (
match Utils.filename_to_relative ~root:models_dir_real fname_real with
| Some path ->
RelativeInferModel path
| None ->
(* fname_real is absolute already *)
Absolute fname_real
Absolute fname_real )
let to_string fname =

@ -22,17 +22,31 @@ val finalize : Sqlite3.db -> log:string -> Sqlite3.stmt -> unit
(** Finalize the given [stmt]. Raises {!Error} on failure. *)
val result_fold_rows :
?finalize:bool -> Sqlite3.db -> log:string -> Sqlite3.stmt -> init:'a
-> f:('a -> Sqlite3.stmt -> 'a) -> 'a
?finalize:bool
-> Sqlite3.db
-> log:string
-> Sqlite3.stmt
-> init:'a
-> f:('a -> Sqlite3.stmt -> 'a)
-> 'a
(** Fold [f] over each row of the result. [f] must not access the database. *)
val result_fold_single_column_rows :
?finalize:bool -> Sqlite3.db -> log:string -> Sqlite3.stmt -> init:'b
-> f:('b -> Sqlite3.Data.t -> 'b) -> 'b
?finalize:bool
-> Sqlite3.db
-> log:string
-> Sqlite3.stmt
-> init:'b
-> f:('b -> Sqlite3.Data.t -> 'b)
-> 'b
(** Like {!result_fold_rows} but pass column 0 of each row in the results to [f]. *)
val result_option :
?finalize:bool -> Sqlite3.db -> log:string -> read_row:(Sqlite3.stmt -> 'a) -> Sqlite3.stmt
?finalize:bool
-> Sqlite3.db
-> log:string
-> read_row:(Sqlite3.stmt -> 'a)
-> Sqlite3.stmt
-> 'a option
(** Same as {!result_fold_rows} but asserts that at most one row is returned. *)
@ -58,5 +72,4 @@ end
(** A default implementation of the Data API that encodes every objects as marshalled blobs *)
module MarshalledData (D : sig
type t
end) :
Data with type t = D.t
end) : Data with type t = D.t

@ -59,9 +59,12 @@ let draw_top_bar fmt ~term_width ~total ~finished ~elapsed =
(* add pairs of a partial format string and its expected size *)
let ( ++ ) (f1, l1) (f2, l2) = (f1 ^^ f2, l1 + l2) in
let ( +++ ) (f1, l1) f2 = (f1 ^^ f2, l1 + (string_of_format f2 |> String.length)) in
("%*d", bar_tasks_num_size (* finished *)) +++ "/" ++ ("%s", bar_tasks_num_size (* total *))
("%*d", bar_tasks_num_size (* finished *))
+++ "/"
++ ("%s", bar_tasks_num_size (* total *))
+++ " [" ++ ("%a%a", 0 (* progress bar *)) +++ "] "
++ ("%d%%", 3 (* "xxx%", even though sometimes it's just "x%" *)) +++ " "
++ ("%d%%", 3 (* "xxx%", even though sometimes it's just "x%" *))
+++ " "
++ ( "%s"
, max (String.length elapsed_string) 9
(* leave some room for elapsed_string to avoid flicker. 9 characters is "XXhXXmXXs" so it
@ -144,8 +147,8 @@ let create ~jobs =
let update_status_multiline task_bar ~slot:job t0 status =
(task_bar.jobs_statuses).(job) <- status ;
(task_bar.jobs_start_times).(job) <- t0 ;
task_bar.jobs_statuses.(job) <- status ;
task_bar.jobs_start_times.(job) <- t0 ;
()

@ -206,7 +206,11 @@ let write_json_to_file destfile json =
let with_channel_in ~f chan_in =
try while true do f @@ In_channel.input_line_exn chan_in done with End_of_file -> ()
try
while true do
f @@ In_channel.input_line_exn chan_in
done
with End_of_file -> ()
let consume_in chan_in = with_channel_in ~f:ignore chan_in
@ -246,14 +250,14 @@ let create_dir dir =
try
if (Unix.stat dir).Unix.st_kind <> Unix.S_DIR then
L.(die ExternalError) "file '%s' already exists and is not a directory" dir
with Unix.Unix_error _ ->
with Unix.Unix_error _ -> (
try Unix.mkdir dir ~perm:0o700 with Unix.Unix_error _ ->
let created_concurrently =
(* check if another process created it meanwhile *)
try Polymorphic_compare.( = ) (Unix.stat dir).Unix.st_kind Unix.S_DIR
with Unix.Unix_error _ -> false
in
if not created_concurrently then L.(die ExternalError) "cannot create directory '%s'" dir
if not created_concurrently then L.(die ExternalError) "cannot create directory '%s'" dir )
let realpath_cache = Hashtbl.create 1023

@ -69,8 +69,11 @@ val echo_in : In_channel.t -> unit
val with_process_in : string -> (In_channel.t -> 'a) -> 'a * Unix.Exit_or_signal.t
val with_process_lines :
debug:((string -> unit, Format.formatter, unit) format -> string -> unit) -> cmd:string list
-> tmp_prefix:string -> f:(string list -> 'res) -> 'res
debug:((string -> unit, Format.formatter, unit) format -> string -> unit)
-> cmd:string list
-> tmp_prefix:string
-> f:(string list -> 'res)
-> 'res
(** Runs the command [cmd] and calls [f] on the output lines. Uses [debug] to print debug
information, and [tmp_prefix] as a prefix for temporary files. *)

@ -11,7 +11,7 @@ open PolyVariantEqual
type zip_library = {zip_filename: string; zip_channel: Zip.in_file Lazy.t}
let load_from_zip serializer zip_path zip_library =
let lazy zip_channel = zip_library.zip_channel in
let (lazy zip_channel) = zip_library.zip_channel in
let deserialize = Serialization.read_from_string serializer in
match deserialize (Zip.read_entry zip_channel (Zip.find_entry zip_channel zip_path)) with
| Some data ->
@ -45,7 +45,7 @@ let zip_libraries =
line. *)
List.rev_filter_map Config.specs_library ~f:load_zip
in
if Config.biabduction && not Config.models_mode && Sys.file_exists Config.models_jar = `Yes
if Config.biabduction && (not Config.models_mode) && Sys.file_exists Config.models_jar = `Yes
then mk_zip_lib Config.models_jar :: zip_libs
else zip_libs)

@ -1,6 +1,8 @@
(* -*- tuareg -*- *)
(* NOTE: prepend dune.common to this file! *)
;; Format.sprintf
;;
Format.sprintf
{|
(library
(name InferBase)

@ -77,10 +77,11 @@ let create_condition_ls ids_private id_base p_leftover (inst: Sil.exp_subst) =
&& List.for_all ~f:(fun e -> Exp.program_vars e |> Sequence.is_empty) insts_of_private_ids
&&
let fav_insts_of_private_ids =
Sequence.of_list insts_of_private_ids |> Sequence.concat_map ~f:Exp.free_vars
Sequence.of_list insts_of_private_ids
|> Sequence.concat_map ~f:Exp.free_vars
|> Sequence.memoize
in
not (Sequence.exists fav_insts_of_private_ids ~f:Ident.is_normal)
(not (Sequence.exists fav_insts_of_private_ids ~f:Ident.is_normal))
&&
let fav_insts_of_private_ids = Ident.set_of_sequence fav_insts_of_private_ids in
let intersects_fav_insts_of_private_ids s =
@ -121,7 +122,7 @@ let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para: Sil.hpara) =
let ids_private = id_next :: (ids_exist_fst @ ids_exist_snd) in
create_condition_ls ids_private id_base
in
{ r_vars= id_base :: id_next :: id_end :: ids_shared @ ids_exist_fst @ ids_exist_snd
{ r_vars= (id_base :: id_next :: id_end :: ids_shared) @ ids_exist_fst @ ids_exist_snd
; r_root= para_fst_start
; r_sigma= para_fst_rest @ para_snd
; r_new_sigma= [lseg_res]
@ -152,7 +153,7 @@ let mk_rule_ptsls_ls tenv k2 impl_ok1 impl_ok2 para =
let ids_private = id_next :: ids_exist in
create_condition_ls ids_private id_base
in
{ r_vars= id_base :: id_next :: id_end :: ids_shared @ ids_exist
{ r_vars= (id_base :: id_next :: id_end :: ids_shared) @ ids_exist
; r_root= para_inst_start
; r_sigma= para_inst_rest @ [lseg_pat]
; r_new_pi= gen_pi_res
@ -179,7 +180,7 @@ let mk_rule_lspts_ls tenv k1 impl_ok1 impl_ok2 para =
let ids_private = id_next :: ids_exist in
create_condition_ls ids_private id_base
in
{ r_vars= id_base :: id_next :: id_end :: ids_shared @ ids_exist
{ r_vars= (id_base :: id_next :: id_end :: ids_shared) @ ids_exist
; r_root= lseg_pat
; r_sigma= para_inst_pat
; r_new_sigma= [lseg_res]
@ -306,7 +307,7 @@ let mk_rule_ptspts_dll tenv impl_ok1 impl_ok2 para =
L.out "para_snd=%a @.@." pp_hpat_list para_snd;
L.out "dllseg_res=%a @.@." pp_hpred dllseg_res;
*)
{ r_vars= id_iF :: id_oB :: id_iF' :: id_oF :: ids_shared @ ids_exist_fst @ ids_exist_snd
{ r_vars= (id_iF :: id_oB :: id_iF' :: id_oF :: ids_shared) @ ids_exist_fst @ ids_exist_snd
; r_root= para_fst_start
; r_sigma= para_fst_rest @ para_snd
; r_new_sigma= [dllseg_res]
@ -350,7 +351,7 @@ let mk_rule_ptsdll_dll tenv k2 impl_ok1 impl_ok2 para =
let ids_private = id_iF' :: ids_exist in
create_condition_dll ids_private id_iF
in
{ r_vars= id_iF :: id_oB :: id_iF' :: id_oF :: id_iB :: ids_shared @ ids_exist
{ r_vars= (id_iF :: id_oB :: id_iF' :: id_oF :: id_iB :: ids_shared) @ ids_exist
; r_root= para_inst_start
; r_sigma= para_inst_rest @ [dllseg_pat]
; r_new_pi= gen_pi_res
@ -390,7 +391,7 @@ let mk_rule_dllpts_dll tenv k1 impl_ok1 impl_ok2 para =
let ids_private = id_oB' :: ids_exist in
create_condition_dll ids_private id_iF
in
{ r_vars= id_iF :: id_oB :: id_iF' :: id_oB' :: id_oF :: ids_shared @ ids_exist
{ r_vars= (id_iF :: id_oB :: id_iF' :: id_oB' :: id_oF :: ids_shared) @ ids_exist
; r_root= dllseg_pat
; r_sigma= para_inst_pat
; r_new_pi= gen_pi_res
@ -480,8 +481,7 @@ let typ_get_recursive_flds tenv typ_exp =
L.(debug Analysis Quiet)
"@\ntyp_get_recursive_flds: unexpected %a unknown struct type: %a@." Exp.pp typ_exp
Typ.Name.pp name ;
[]
(* ToDo: assert false *) )
[] (* ToDo: assert false *) )
| Tint _ | Tvoid | Tfun _ | Tptr _ | Tfloat _ | Tarray _ | TVar _ ->
[] )
| Exp.Var _ ->
@ -496,7 +496,7 @@ let typ_get_recursive_flds tenv typ_exp =
let discover_para_roots tenv p root1 next1 root2 next2 : Sil.hpara option =
let eq_arg1 = Exp.equal root1 next1 in
let eq_arg2 = Exp.equal root2 next2 in
let precondition_check = not eq_arg1 && not eq_arg2 in
let precondition_check = (not eq_arg1) && not eq_arg2 in
if not precondition_check then None
else
let corres = [(next1, next2)] in
@ -776,8 +776,8 @@ let hpara_special_cases_dll hpara : Sil.hpara_dll list =
List.map ~f:update_para special_cases
let abs_rules_apply_rsets tenv (rsets: rule_set list) (p_in: Prop.normal Prop.t)
: Prop.normal Prop.t =
let abs_rules_apply_rsets tenv (rsets : rule_set list) (p_in : Prop.normal Prop.t) :
Prop.normal Prop.t =
let apply_rule (changed, p) r =
match sigma_rewrite tenv p r with
| None ->
@ -816,11 +816,11 @@ let abs_rules_apply_lists tenv (p_in: Prop.normal Prop.t) : Prop.normal Prop.t =
match rset with DLL para', _ -> Match.hpara_dll_iso tenv para para' | _ -> false
in
let filter_sll para =
not (List.exists ~f:(eq_sll para) old_rsets)
(not (List.exists ~f:(eq_sll para) old_rsets))
&& not (List.exists ~f:(eq_sll para) !new_rsets)
in
let filter_dll para =
not (List.exists ~f:(eq_dll para) old_rsets)
(not (List.exists ~f:(eq_dll para) old_rsets))
&& not (List.exists ~f:(eq_dll para) !new_rsets)
in
let todo_paras_sll = List.filter ~f:filter_sll closed_paras_sll in
@ -1002,7 +1002,8 @@ let check_junk pname tenv prop =
let should_remove_hpred entries =
let predicate = function
| Exp.Var id ->
(Ident.is_primed id || Ident.is_footprint id) && not (Ident.Set.mem id fav_root)
(Ident.is_primed id || Ident.is_footprint id)
&& (not (Ident.Set.mem id fav_root))
&& not (id_considered_reachable id)
| _ ->
false
@ -1034,20 +1035,20 @@ let check_junk pname tenv prop =
| Some (Apred ((Awont_leak as a), _)) ->
L.d_strln "WONT_LEAK" ;
res := Some a
| _ ->
| _ -> (
match Attribute.get_resource tenv prop e with
| Some (Apred ((Aresource {ra_kind= Racquire} as a), _)) ->
L.d_str "ATTRIBUTE: " ;
PredSymb.d_attribute a ;
L.d_ln () ;
res := Some a
| _ ->
| _ -> (
match Attribute.get_undef tenv prop e with
| Some (Apred ((Aundef _ as a), _)) ->
L.d_strln "UNDEF" ;
res := Some a
| _ ->
()
() ) )
in
List.iter ~f:do_entry entries ; !res
in
@ -1232,8 +1233,8 @@ let remove_local_stack sigma pvars =
(** [prop_set_fooprint p p_foot] removes a local stack from [p_foot],
and sets proposition [p_foot] as footprint of [p]. *)
let set_footprint_for_abs (p: 'a Prop.t) (p_foot: 'a Prop.t) local_stack_pvars
: Prop.exposed Prop.t =
let set_footprint_for_abs (p : 'a Prop.t) (p_foot : 'a Prop.t) local_stack_pvars :
Prop.exposed Prop.t =
let p_foot_pure = Prop.get_pure p_foot in
let p_sigma_fp = p_foot.Prop.sigma in
let pi = p_foot_pure in

@ -335,8 +335,8 @@ let array_abstraction_performed = ref false
let generic_strexp_abstract tenv (abstraction_name : string) (p_in : Prop.normal Prop.t)
(can_abstract_ : StrexpMatch.strexp_data -> bool)
(do_abstract :
bool -> Prop.normal Prop.t -> StrexpMatch.strexp_data -> Prop.normal Prop.t * bool)
: Prop.normal Prop.t =
bool -> Prop.normal Prop.t -> StrexpMatch.strexp_data -> Prop.normal Prop.t * bool) :
Prop.normal Prop.t =
let can_abstract data =
let r = can_abstract_ data in
if r then array_abstraction_performed := true ;
@ -385,7 +385,8 @@ let generic_strexp_abstract tenv (abstraction_name: string) (p_in: Prop.normal P
(** Return [true] if there's a pointer to the index *)
let index_is_pointed_to tenv (p: Prop.normal Prop.t) (path: StrexpMatch.path) (index: Exp.t) : bool =
let index_is_pointed_to tenv (p : Prop.normal Prop.t) (path : StrexpMatch.path) (index : Exp.t) :
bool =
let indices =
let index_plus_one = Exp.BinOp (Binop.PlusA, index, Exp.one) in
[index; index_plus_one]
@ -406,8 +407,8 @@ let index_is_pointed_to tenv (p: Prop.normal Prop.t) (path: StrexpMatch.path) (i
(** Given [p] containing an array at [path], blur [index] in it *)
let blur_array_index tenv (p: Prop.normal Prop.t) (path: StrexpMatch.path) (index: Exp.t)
: Prop.normal Prop.t =
let blur_array_index tenv (p : Prop.normal Prop.t) (path : StrexpMatch.path) (index : Exp.t) :
Prop.normal Prop.t =
try
let fresh_index =
Exp.Var (Ident.create_fresh (if !Config.footprint then Ident.kfootprint else Ident.kprimed))
@ -438,15 +439,15 @@ let blur_array_index tenv (p: Prop.normal Prop.t) (path: StrexpMatch.path) (inde
(** Given [p] containing an array at [root], blur [indices] in it *)
let blur_array_indices tenv (p: Prop.normal Prop.t) (root: StrexpMatch.path) (indices: Exp.t list)
: Prop.normal Prop.t * bool =
let blur_array_indices tenv (p : Prop.normal Prop.t) (root : StrexpMatch.path)
(indices : Exp.t list) : Prop.normal Prop.t * bool =
let f prop index = blur_array_index tenv prop root index in
(List.fold ~f ~init:p indices, List.length indices > 0)
(** Given [p] containing an array at [root], only keep [indices] in it *)
let keep_only_indices tenv (p: Prop.normal Prop.t) (path: StrexpMatch.path) (indices: Exp.t list)
: Prop.normal Prop.t * bool =
let keep_only_indices tenv (p : Prop.normal Prop.t) (path : StrexpMatch.path)
(indices : Exp.t list) : Prop.normal Prop.t * bool =
let prune_sigma footprint_part sigma =
try
let matched = StrexpMatch.find_path sigma path in
@ -491,8 +492,8 @@ let strexp_can_abstract ((_, se, typ): StrexpMatch.strexp_data) : bool =
(** This function abstracts a strexp *)
let strexp_do_abstract tenv footprint_part p ((path, se_in, _): StrexpMatch.strexp_data)
: Prop.normal Prop.t * bool =
let strexp_do_abstract tenv footprint_part p ((path, se_in, _) : StrexpMatch.strexp_data) :
Prop.normal Prop.t * bool =
if Config.trace_absarray && footprint_part then (
L.d_str "strexp_do_abstract (footprint)" ;
L.d_ln () ) ;
@ -630,7 +631,8 @@ let remove_redundant_elements tenv prop =
let occurs_at_most_once : Ident.t -> bool =
let fav_curr =
let ( @@@ ) = Sequence.append in
Sil.exp_subst_free_vars prop.Prop.sub @@@ Prop.pi_free_vars prop.Prop.pi
Sil.exp_subst_free_vars prop.Prop.sub
@@@ Prop.pi_free_vars prop.Prop.pi
@@@ Prop.sigma_free_vars prop.Prop.sigma
in
let fav_foot =
@ -656,9 +658,11 @@ let remove_redundant_elements tenv prop =
in
match (e, se) with
| Exp.Const (Const.Cint i), Sil.Eexp (Exp.Var id, _)
when (not fp_part || IntLit.iszero i) && not (Ident.is_normal id) && occurs_at_most_once id ->
when ((not fp_part) || IntLit.iszero i)
&& (not (Ident.is_normal id))
&& occurs_at_most_once id ->
remove () (* unknown value can be removed in re-execution mode or if the index is zero *)
| Exp.Var id, Sil.Eexp _ when not (Ident.is_normal id) && occurs_at_most_once id ->
| Exp.Var id, Sil.Eexp _ when (not (Ident.is_normal id)) && occurs_at_most_once id ->
remove () (* index unknown can be removed *)
| _ ->
true

@ -57,8 +57,7 @@ let add_or_replace tenv prop atom =
let get_all (prop : 'a Prop.t) =
let res = ref [] in
let do_atom a = if is_pred a then res := a :: !res in
List.iter ~f:do_atom prop.pi ;
List.rev !res
List.iter ~f:do_atom prop.pi ; List.rev !res
(** Get the attribute associated to the expression, if any *)
@ -349,7 +348,7 @@ let find_equal_formal_path tenv e prop =
match res with
| Some _ ->
res
| None ->
| None -> (
match hpred with
| Sil.Hpointsto (Exp.Lvar pvar1, Sil.Eexp (exp2, Sil.Iformal (_, _)), _)
when Exp.equal exp2 e && (Pvar.is_local pvar1 || Pvar.is_seed pvar1) ->
@ -360,7 +359,7 @@ let find_equal_formal_path tenv e prop =
match res with
| Some _ ->
res
| None ->
| None -> (
match strexp with
| Sil.Eexp (exp2, _) when Exp.equal exp2 e -> (
match find_in_sigma exp1 seen_hpreds with
@ -369,18 +368,18 @@ let find_equal_formal_path tenv e prop =
| None ->
None )
| _ ->
None )
None ) )
fields ~init:None
| _ ->
None )
None ) )
prop.Prop.sigma ~init:None
in
match find_in_sigma e [] with
| Some vfs ->
Some vfs
| None ->
| None -> (
match get_objc_null tenv prop e with
| Some (Apred (Aobjc_null, [_; vfs])) ->
Some vfs
| _ ->
None
None )

@ -14,7 +14,12 @@ val is_pred : Sil.atom -> bool
(** Check whether an atom is used to mark an attribute *)
val add :
Tenv.t -> ?footprint:bool -> ?polarity:bool -> Prop.normal Prop.t -> PredSymb.t -> Exp.t list
Tenv.t
-> ?footprint:bool
-> ?polarity:bool
-> Prop.normal Prop.t
-> PredSymb.t
-> Exp.t list
-> Prop.normal Prop.t
(** Add an attribute associated to the argument expressions *)
@ -22,7 +27,10 @@ val add_or_replace : Tenv.t -> Prop.normal Prop.t -> Sil.atom -> Prop.normal Pro
(** Replace an attribute associated to the expression *)
val add_or_replace_check_changed :
Tenv.t -> (PredSymb.t -> PredSymb.t -> unit) -> Prop.normal Prop.t -> Sil.atom
Tenv.t
-> (PredSymb.t -> PredSymb.t -> unit)
-> Prop.normal Prop.t
-> Sil.atom
-> Prop.normal Prop.t
(** Replace an attribute associated to the expression, and call the given function with new and
old attributes if they changed. *)
@ -62,7 +70,9 @@ val remove_resource :
(** Remove all attributes for the given resource and kind *)
val map_resource :
Tenv.t -> Prop.normal Prop.t -> (Exp.t -> PredSymb.res_action -> PredSymb.res_action)
Tenv.t
-> Prop.normal Prop.t
-> (Exp.t -> PredSymb.res_action -> PredSymb.res_action)
-> Prop.normal Prop.t
(** Apply f to every resource attribute in the prop *)
@ -75,8 +85,15 @@ val nullify_exp_with_objc_null : Tenv.t -> Prop.normal Prop.t -> Exp.t -> Prop.n
remove the attribute and conjoin an equality to zero. *)
val mark_vars_as_undefined :
Tenv.t -> Prop.normal Prop.t -> ret_exp:Exp.t -> undefined_actuals_by_ref:Exp.t list
-> Typ.Procname.t -> Annot.Item.t -> Location.t -> PredSymb.path_pos -> Prop.normal Prop.t
Tenv.t
-> Prop.normal Prop.t
-> ret_exp:Exp.t
-> undefined_actuals_by_ref:Exp.t list
-> Typ.Procname.t
-> Annot.Item.t
-> Location.t
-> PredSymb.path_pos
-> Prop.normal Prop.t
(** mark Exp.Var's or Exp.Lvar's as undefined *)
(** type for arithmetic problems *)
@ -87,7 +104,10 @@ type arith_problem =
| UminusUnsigned of Exp.t * Typ.t
val find_arithmetic_problem :
Tenv.t -> PredSymb.path_pos -> Prop.normal Prop.t -> Exp.t
Tenv.t
-> PredSymb.path_pos
-> Prop.normal Prop.t
-> Exp.t
-> arith_problem option * Prop.normal Prop.t
(** Look for an arithmetic problem in [exp] *)

@ -115,12 +115,12 @@ module Jprop = struct
acc
| (Prop _ as jp) :: jpl -> (
match f jp with Some x -> do_filter (x :: acc) jpl | None -> do_filter acc jpl )
| (Joined (_, _, jp1, jp2) as jp) :: jpl ->
| (Joined (_, _, jp1, jp2) as jp) :: jpl -> (
match f jp with
| Some x ->
do_filter (x :: acc) jpl
| None ->
do_filter acc (jpl @ [jp1; jp2])
do_filter acc (jpl @ [jp1; jp2]) )
in
do_filter [] jpl
@ -202,7 +202,9 @@ end = struct
let sub =
Sil.subst_of_list
(List.map
~f:(fun id -> incr count ; (id, Exp.Var (Ident.create_normal Ident.name_spec !count)))
~f:(fun id ->
incr count ;
(id, Exp.Var (Ident.create_normal Ident.name_spec !count)) )
idlist)
in
spec_sub tenv sub spec

@ -23,8 +23,7 @@ let check_nested_loop path pos_opt =
match !loop_visits_log with
| true :: true :: _ ->
if verbose then L.d_strln "in nested loop" ;
true
(* last two loop visits were entering loops *)
true (* last two loop visits were entering loops *)
| _ ->
false
in
@ -77,7 +76,7 @@ let check_access access_opt de_opt =
let process_formal_letref = function
| Sil.Load (id, Exp.Lvar pvar, _, _) ->
let is_java_this = Language.curr_language_is Java && Pvar.is_this pvar in
if not is_java_this && is_formal pvar then Some id else None
if (not is_java_this) && is_formal pvar then Some id else None
| _ ->
None
in
@ -147,8 +146,8 @@ let check_access access_opt de_opt =
find_bucket n false
| Some (Localise.Last_accessed (_, is_nullable)) when is_nullable ->
Some Localise.BucketLevel.b1
| _ ->
match de_opt with Some (DecompiledExp.Dconst _) -> Some Localise.BucketLevel.b1 | _ -> None
| _ -> (
match de_opt with Some (DecompiledExp.Dconst _) -> Some Localise.BucketLevel.b1 | _ -> None )
let classify_access desc access_opt de_opt is_nullable =

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

Loading…
Cancel
Save