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

[ocamlformat] Set break-sequences = true

Browse Source 
Summary: Add `break-sequences = true` to .ocamlformat and reformat.

Reviewed By: jvillard

Differential Revision: D21583901

fbshipit-source-id: eb4ec836c
master
Josh Berdine 5 years ago committed by Facebook GitHub Bot
parent 65f369cf35
commit 61566caddf
93 changed files with 827 additions and 292 deletions
Show Stats Download Patch File Download Diff File

1
infer/src/.ocamlformat
Unescape View File

@ -1,5 +1,6 @@
profile = ocamlformat profile = ocamlformat
break-before-in = fit-or-vertical break-before-in = fit-or-vertical
break-sequences = true
let-binding-spacing = sparse let-binding-spacing = sparse
margin = 100 margin = 100
parse-docstrings = true parse-docstrings = true

8
infer/src/IR/AccessPath.ml
Unescape View File

@ -29,13 +29,17 @@ module Raw = struct
if Config.debug_level_analysis >= 3 then F.fprintf fmt ":%a" (Typ.pp Pp.text) typ if Config.debug_level_analysis >= 3 then F.fprintf fmt ":%a" (Typ.pp Pp.text) typ
let pp_base fmt (pvar, typ) = Var.pp fmt pvar ; may_pp_typ fmt typ let pp_base fmt (pvar, typ) =
Var.pp fmt pvar ;
may_pp_typ fmt typ
let rec pp_access fmt = function let rec pp_access fmt = function
| FieldAccess field_name -> | FieldAccess field_name ->
F.pp_print_string fmt (Fieldname.get_field_name field_name) F.pp_print_string fmt (Fieldname.get_field_name field_name)
| ArrayAccess (typ, []) -> | ArrayAccess (typ, []) ->
F.pp_print_string fmt "[_]" ; may_pp_typ fmt typ F.pp_print_string fmt "[_]" ;
may_pp_typ fmt typ
| ArrayAccess (typ, index_aps) -> | ArrayAccess (typ, index_aps) ->
F.fprintf fmt "[%a]" (PrettyPrintable.pp_collection ~pp_item:pp) index_aps ; F.fprintf fmt "[%a]" (PrettyPrintable.pp_collection ~pp_item:pp) index_aps ;
may_pp_typ fmt typ may_pp_typ fmt typ

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

@ -11,7 +11,8 @@ let scan_models () =
let rec next_entry index dir = let rec next_entry index dir =
match Unix.readdir_opt dir with match Unix.readdir_opt dir with
| None -> | None ->
Unix.closedir dir ; index Unix.closedir dir ;
index
| Some entry -> ( | Some entry -> (
match String.chop_suffix entry ~suffix:Config.specs_files_suffix with match String.chop_suffix entry ~suffix:Config.specs_files_suffix with
| Some file_proc_name -> | Some file_proc_name ->

6
infer/src/IR/BuiltinDecl.ml
Unescape View File

@ -15,7 +15,8 @@ let register pname = builtin_decls := Procname.Set.add pname !builtin_decls
let create_procname name = let create_procname name =
let pname = Procname.from_string_c_fun name in let pname = Procname.from_string_c_fun name in
register pname ; pname register pname ;
pname
let create_objc_class_method class_name method_name parameters = let create_objc_class_method class_name method_name parameters =
@ -25,7 +26,8 @@ let create_objc_class_method class_name method_name parameters =
Procname.ObjC_Cpp Procname.ObjC_Cpp
(Procname.ObjC_Cpp.make tname method_name method_kind Typ.NoTemplate parameters) (Procname.ObjC_Cpp.make tname method_name method_kind Typ.NoTemplate parameters)
in in
register pname ; pname register pname ;
pname
let is_declared pname = Procname.Set.mem pname !builtin_decls let is_declared pname = Procname.Set.mem pname !builtin_decls

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

@ -27,7 +27,8 @@ let iter_over_sorted_procs cfg ~f =
let get_all_defined_proc_names cfg = let get_all_defined_proc_names cfg =
let procs = ref [] in let procs = ref [] in
let f pname pdesc = if Procdesc.is_defined pdesc then procs := pname :: !procs in let f pname pdesc = if Procdesc.is_defined pdesc then procs := pname :: !procs in
Procname.Hash.iter f cfg ; !procs Procname.Hash.iter f cfg ;
!procs
(** Create a new procdesc *) (** Create a new procdesc *)

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

@ -276,6 +276,7 @@ let log_issue severity err_log ~loc ~node ~session ~ltr ~linters_def_file ~doc_u
| Exceptions.Info | Exceptions.Advice | Exceptions.Like -> | Exceptions.Info | Exceptions.Advice | Exceptions.Like ->
L.d_info L.d_info
in in
d warn_str ; L.d_ln () ) d warn_str ;
L.d_ln () )
in in
if should_print_now then print_now () if should_print_now then print_now ()

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

@ -147,7 +147,8 @@ let pp_array_offset_opt pp_offset fmt = function
let rec pp_access_expr fmt = function let rec pp_access_expr fmt = function
| Base (pvar, typ) -> | Base (pvar, typ) ->
Var.pp fmt pvar ; may_pp_typ fmt typ Var.pp fmt pvar ;
may_pp_typ fmt typ
| FieldOffset (Dereference ae, fld) -> | FieldOffset (Dereference ae, fld) ->
F.fprintf fmt "%a->%a" pp_access_expr ae Fieldname.pp fld F.fprintf fmt "%a->%a" pp_access_expr ae Fieldname.pp fld
| FieldOffset (ae, fld) -> | FieldOffset (ae, fld) ->

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

@ -140,7 +140,9 @@ module NameGenerator = struct
let stamp = NameHash.find !name_map name in let stamp = NameHash.find !name_map name in
NameHash.replace !name_map name (stamp + 1) ; NameHash.replace !name_map name (stamp + 1) ;
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 in
{kind; name; stamp} {kind; name; stamp}
@ -261,4 +263,5 @@ let counts_of_sequence seq =
let h = Hash.create (Sequence.length seq) in let h = Hash.create (Sequence.length seq) in
let get id = Option.value (Hash.find_opt h id) ~default:0 in let get id = Option.value (Hash.find_opt h id) ~default:0 in
let bump id = Hash.replace h id (1 + get id) in let bump id = Hash.replace h id (1 + get id) in
Sequence.iter ~f:bump seq ; get Sequence.iter ~f:bump seq ;
get

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

@ -56,7 +56,8 @@ h1 { font-size:14pt }
<body> <body>
|} |}
in in
F.pp_print_string fmt s ; (fd, fmt) F.pp_print_string fmt s ;
(fd, fmt)
(** Get the full html filename from a path *) (** Get the full html filename from a path *)

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

@ -55,7 +55,8 @@ let load entry =
(fun _ issues1 issues2 -> (fun _ issues1 issues2 ->
match (issues1, issues2) with match (issues1, issues2) with
| Some issues1, Some issues2 -> | Some issues1, Some issues2 ->
Errlog.update issues1 issues2 ; Some issues1 Errlog.update issues1 issues2 ;
Some issues1
| Some issues1, None -> | Some issues1, None ->
Some issues1 Some issues1
| None, Some issues2 -> | None, Some issues2 ->

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

@ -656,7 +656,8 @@ let desc_unary_minus_applied_to_unsigned_expression expr_str_opt typ_str loc =
let expression = let expression =
match expr_str_opt with match expr_str_opt with
| Some s -> | Some s ->
Tags.update tags Tags.value s ; "expression " ^ s Tags.update tags Tags.value s ;
"expression " ^ s
| None -> | None ->
"an expression" "an expression"
in in

6
infer/src/IR/Tenv.ml
Unescape View File

@ -113,7 +113,8 @@ let merge_per_file ~src ~dst =
| Global, Global -> | Global, Global ->
Global Global
| FileLocal src_tenv, FileLocal dst_tenv -> | FileLocal src_tenv, FileLocal dst_tenv ->
merge ~src:src_tenv ~dst:dst_tenv ; FileLocal dst_tenv merge ~src:src_tenv ~dst:dst_tenv ;
FileLocal dst_tenv
| Global, FileLocal _ | FileLocal _, Global -> | Global, FileLocal _ | FileLocal _, Global ->
L.die InternalError "Cannot merge Global tenv with FileLocal tenv" L.die InternalError "Cannot merge Global tenv with FileLocal tenv"
@ -154,7 +155,8 @@ let store_debug_file tenv tenv_filename =
let debug_filename = DB.filename_to_string (DB.filename_add_suffix tenv_filename ".debug") in let debug_filename = DB.filename_to_string (DB.filename_add_suffix tenv_filename ".debug") in
let out_channel = Out_channel.create debug_filename in let out_channel = Out_channel.create debug_filename in
let fmt = Format.formatter_of_out_channel out_channel in let fmt = Format.formatter_of_out_channel out_channel in
pp fmt tenv ; Out_channel.close out_channel pp fmt tenv ;
Out_channel.close out_channel
let store_debug_file_for_source source_file tenv = let store_debug_file_for_source source_file tenv =

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

@ -258,7 +258,8 @@ let patterns_of_json_with_key (json_key, json) =
| Ok pattern -> | Ok pattern ->
pattern :: accu pattern :: accu
| Error msg -> | Error msg ->
warn_user msg ; accu ) warn_user msg ;
accu )
| `List l -> | `List l ->
List.fold ~f:translate ~init:accu l List.fold ~f:translate ~init:accu l
| json -> | json ->

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

@ -212,7 +212,12 @@ end = struct
actuals actuals
in in
let guard_action ~f ~error = let guard_action ~f ~error =
match actuals with [guard] -> f guard | _ -> log_parse_error error ; NoEffect match actuals with
| [guard] ->
f guard
| _ ->
log_parse_error error ;
NoEffect
in in
let fst_arg = match actuals with x :: _ -> [x] | _ -> [] in let fst_arg = match actuals with x :: _ -> [x] | _ -> [] in
if is_std_lock pname then Lock actuals if is_std_lock pname then Lock actuals

3
infer/src/absint/DataFlow.ml
Unescape View File

@ -138,7 +138,8 @@ module MakeDF (St : DFStateType) : DF with type state = St.t = struct
let init_set = S.singleton start_node in let init_set = S.singleton start_node in
let init_statemap = let init_statemap =
let m = H.create 1 in let m = H.create 1 in
H.replace m start_node state ; m H.replace m start_node state ;
m
in in
{ worklist= init_set { worklist= init_set
; pre_states= init_statemap ; pre_states= init_statemap

10
infer/src/absint/PatternMatch.ml
Unescape View File

@ -318,7 +318,8 @@ let proc_calls resolve_attributes pdesc filter : (Procname.t * ProcAttributes.t)
Instrs.iter ~f:(do_instruction node) instrs Instrs.iter ~f:(do_instruction node) instrs
in in
let nodes = Procdesc.get_nodes pdesc 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 has_same_signature proc_name = let has_same_signature proc_name =
@ -370,7 +371,12 @@ let override_exists ?(check_current_type = true) f tenv proc_name =
(* Only java supported at the moment *) (* Only java supported at the moment *)
let override_iter f tenv proc_name = let override_iter f tenv proc_name =
ignore (override_exists (fun pname -> f pname ; false) tenv proc_name) ignore
(override_exists
(fun pname ->
f pname ;
false )
tenv proc_name)
let lookup_attributes tenv proc_name = let lookup_attributes tenv proc_name =

9
infer/src/al/ALDebugger.ml
Unescape View File

@ -194,7 +194,8 @@ module EvaluationTracker = struct
stop_and_explain_step () ; stop_and_explain_step () ;
{t with debugger_active= true} {t with debugger_active= true}
| true, _, _ -> | true, _, _ ->
stop_and_explain_step () ; t stop_and_explain_step () ;
t
| _ -> | _ ->
t t
@ -244,7 +245,8 @@ module EvaluationTracker = struct
| Tree (node, children), ntd -> | Tree (node, children), ntd ->
(Tree (node, evaluated_tree :: children), ntd) (Tree (node, evaluated_tree :: children), ntd)
in in
Stack.push t'.eval_stack parent ; t'.forest Stack.push t'.eval_stack parent ;
t'.forest
in in
{t' with forest= forest'} {t' with forest= forest'}
@ -257,7 +259,8 @@ module EvaluationTracker = struct
let open Ctl_parser_types in let open Ctl_parser_types in
let buffer_content buf = let buffer_content buf =
let result = Buffer.contents buf in let result = Buffer.contents buf in
Buffer.reset buf ; result Buffer.reset buf ;
result
in in
let dotty_of_tree cluster_id tree = let dotty_of_tree cluster_id tree =
let get_root tree = match tree with Tree (root, _) -> root in let get_root tree = match tree with Tree (root, _) -> root in

3
infer/src/al/CTL.ml
Unescape View File

@ -999,4 +999,5 @@ and eval_formula ?keep_witness f an lcxt : Ctl_parser_types.ast_node option =
| InObjCClass (f1, f2) -> | InObjCClass (f1, f2) ->
eval_InObjCClass an lcxt f1 f2 eval_InObjCClass an lcxt f1 f2
in in
debug_eval_end res ; res debug_eval_end res ;
res

9
infer/src/al/ctl_parser_types.ml
Unescape View File

@ -423,7 +423,8 @@ let builtin_equal (bi : Clang_ast_t.builtin_type_kind) (abi : builtin_kind) =
| Some assoc_abi when equal_builtin_kind assoc_abi abi -> | Some assoc_abi when equal_builtin_kind assoc_abi abi ->
true true
| _ -> | _ ->
display_equality_warning () ; false display_equality_warning () ;
false
let typename_to_string pointer = let typename_to_string pointer =
@ -446,7 +447,8 @@ let rec pointer_type_equal p ap =
| PointerType (_, qt), BuiltIn _ -> | PointerType (_, qt), BuiltIn _ ->
check_type_ptr qt.qt_type_ptr ap check_type_ptr qt.qt_type_ptr ap
| _, _ -> | _, _ ->
display_equality_warning () ; false display_equality_warning () ;
false
and objc_object_type_equal c_type abs_ctype = and objc_object_type_equal c_type abs_ctype =
@ -562,7 +564,8 @@ and c_type_equal c_type abs_ctype =
| AttributedType (ti, _), TypeName _ -> ( | AttributedType (ti, _), TypeName _ -> (
match ti.ti_desugared_type with Some dt -> check_type_ptr dt abs_ctype | None -> false ) match ti.ti_desugared_type with Some dt -> check_type_ptr dt abs_ctype | None -> false )
| _, _ -> | _, _ ->
display_equality_warning () ; false display_equality_warning () ;
false
(* to be extended with more types *) (* to be extended with more types *)

14
infer/src/backend/CallGraph.ml
Unescape View File

@ -52,7 +52,10 @@ module NodeMap = Caml.Hashtbl.Make (Int)
[trim_id_map] makes the image equal to the domain of [node_map]. *) [trim_id_map] makes the image equal to the domain of [node_map]. *)
type t = {id_map: int IdMap.t; node_map: Node.t NodeMap.t} type t = {id_map: int IdMap.t; node_map: Node.t NodeMap.t}
let reset {id_map; node_map} = IdMap.reset id_map ; NodeMap.reset node_map let reset {id_map; node_map} =
IdMap.reset id_map ;
NodeMap.reset node_map
let create initial_capacity = let create initial_capacity =
{id_map= IdMap.create initial_capacity; node_map= NodeMap.create initial_capacity} {id_map= IdMap.create initial_capacity; node_map= NodeMap.create initial_capacity}
@ -80,7 +83,8 @@ let get_or_set_id ({id_map} as graph) procname =
match id_of_procname graph procname with match id_of_procname graph procname with
| None -> | None ->
let id = IdMap.length id_map in let id = IdMap.length id_map in
IdMap.replace id_map procname id ; id IdMap.replace id_map procname id ;
id
| Some id -> | Some id ->
id id
@ -98,7 +102,8 @@ let get_or_init_node node_map id pname =
node node
| None -> | None ->
let new_node = Node.make id pname [] in let new_node = Node.make id pname [] in
NodeMap.add node_map id new_node ; new_node NodeMap.add node_map id new_node ;
new_node
let add_edge ({node_map} as graph) ~pname ~successor_pname = let add_edge ({node_map} as graph) ~pname ~successor_pname =
@ -135,7 +140,8 @@ let pp_dot fmt {node_map} =
let to_dotty g filename = let to_dotty g filename =
let outc = Filename.concat Config.results_dir filename |> Out_channel.create in let outc = Filename.concat Config.results_dir filename |> Out_channel.create in
let fmt = F.formatter_of_out_channel outc in let fmt = F.formatter_of_out_channel outc in
pp_dot fmt g ; Out_channel.close outc pp_dot fmt g ;
Out_channel.close outc
let iter_unflagged_leaves ~f g = let iter_unflagged_leaves ~f g =

13
infer/src/backend/InferAnalyze.ml
Unescape View File

@ -14,10 +14,15 @@ module L = Logging
module CLOpt = CommandLineOption module CLOpt = CommandLineOption
let clear_caches_except_lrus () = let clear_caches_except_lrus () =
Summary.OnDisk.clear_cache () ; Procname.SQLite.clear_cache () ; BufferOverrunUtils.clear_cache () Summary.OnDisk.clear_cache () ;
Procname.SQLite.clear_cache () ;
BufferOverrunUtils.clear_cache ()
let clear_caches () = Ondemand.LocalCache.clear () ; clear_caches_except_lrus () let clear_caches () =
Ondemand.LocalCache.clear () ;
clear_caches_except_lrus ()
let analyze_target : (TaskSchedulerTypes.target, Procname.t) Tasks.doer = let analyze_target : (TaskSchedulerTypes.target, Procname.t) Tasks.doer =
let analyze_source_file exe_env source_file = let analyze_source_file exe_env source_file =
@ -173,7 +178,9 @@ let invalidate_changed_procedures changed_files =
CallGraph.to_dotty reverse_callgraph "reverse_analysis_callgraph.dot" ; CallGraph.to_dotty reverse_callgraph "reverse_analysis_callgraph.dot" ;
let invalidated_nodes = let invalidated_nodes =
CallGraph.fold_flagged reverse_callgraph CallGraph.fold_flagged reverse_callgraph
~f:(fun node acc -> SpecsFiles.delete node.pname ; acc + 1) ~f:(fun node acc ->
SpecsFiles.delete node.pname ;
acc + 1 )
0 0
in in
L.progress L.progress

9
infer/src/backend/ProcLocker.ml
Unescape View File

@ -15,7 +15,8 @@ let log_unlock_time = BackendStats.add_to_proc_locker_unlock_time
let record_time_of ~f ~log_f = let record_time_of ~f ~log_f =
let ExecutionDuration.{result; execution_duration} = ExecutionDuration.timed_evaluate ~f in let ExecutionDuration.{result; execution_duration} = ExecutionDuration.timed_evaluate ~f in
log_f execution_duration ; result log_f execution_duration ;
result
let locks_dir = ResultsDir.get_path ProcnamesLocks let locks_dir = ResultsDir.get_path ProcnamesLocks
@ -24,7 +25,11 @@ let locks_target = locks_dir ^/ "locks_target"
let create_file filename = Unix.openfile ~mode:[O_CREAT; O_RDONLY] filename |> Unix.close let create_file filename = Unix.openfile ~mode:[O_CREAT; O_RDONLY] filename |> Unix.close
let setup () = Utils.rmtree locks_dir ; Utils.create_dir locks_dir ; create_file locks_target let setup () =
Utils.rmtree locks_dir ;
Utils.create_dir locks_dir ;
create_file locks_target
let clean () = () let clean () = ()

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

@ -45,7 +45,8 @@ let select_proc_names_interactive ~filter =
| Some n when 0 <= n && n < Array.length proc_names_array -> | Some n when 0 <= n && n < Array.length proc_names_array ->
Some [proc_names_array.(n)] Some [proc_names_array.(n)]
| _ -> | _ ->
print_endline "Invalid input" ; ask_user_input () print_endline "Invalid input" ;
ask_user_input ()
in in
ask_user_input () ask_user_input ()

6
infer/src/backend/RestartScheduler.ml
Unescape View File

@ -24,7 +24,8 @@ let of_list (lst : work_with_dependency list) : ('a, Procname.t) ProcessPool.Tas
let work_if_dependency_allows w = let work_if_dependency_allows w =
match w.need_to_finish with match w.need_to_finish with
| Some pname when ProcLocker.is_locked pname -> | Some pname when ProcLocker.is_locked pname ->
Queue.enqueue content w ; None Queue.enqueue content w ;
None
| None | Some _ -> | None | Some _ ->
Some w.work Some w.work
in in
@ -107,7 +108,8 @@ let unlock pname =
caller.callees_useful <- caller.callees_useful <-
ExecutionDuration.add_duration_since caller.callees_useful start ExecutionDuration.add_duration_since caller.callees_useful start
| None -> | None ->
add_to_useful_time start ; add_to_total_time start ) ; add_to_useful_time start ;
add_to_total_time start ) ;
ProcLocker.unlock pname ) ProcLocker.unlock pname )

4
infer/src/backend/SpecsFiles.ml
Unescape View File

@ -43,7 +43,9 @@ let spec_files_from_cmdline () =
if (not (Filename.check_suffix arg Config.specs_files_suffix)) && not (String.equal arg ".") if (not (Filename.check_suffix arg Config.specs_files_suffix)) && not (String.equal arg ".")
then print_usage_exit ("file " ^ arg ^ ": arguments must be .specs files") ) then print_usage_exit ("file " ^ arg ^ ": arguments must be .specs files") )
Config.anon_args ; Config.anon_args ;
if Config.test_filtering then (Inferconfig.test () ; L.exit 0) ; if Config.test_filtering then (
Inferconfig.test () ;
L.exit 0 ) ;
if List.is_empty Config.anon_args then load_specfiles () else List.rev Config.anon_args ) if List.is_empty Config.anon_args then load_specfiles () else List.rev Config.anon_args )
else load_specfiles () else load_specfiles ()

8
infer/src/backend/Tasks.ml
Unescape View File

@ -9,7 +9,10 @@ open! IStd
type ('a, 'b) doer = 'a -> 'b option type ('a, 'b) doer = 'a -> 'b option
let fork_protect ~f x = BackendStats.reset () ; ForkUtils.protect ~f x let fork_protect ~f x =
BackendStats.reset () ;
ForkUtils.protect ~f x
let with_new_db_connection ~f () = let with_new_db_connection ~f () =
ResultsDatabase.new_database_connection () ; ResultsDatabase.new_database_connection () ;
@ -59,4 +62,5 @@ let run_sequentially ~(f : ('a, 'b) doer) (tasks : 'a list) : unit =
TaskBar.refresh task_bar ; TaskBar.refresh task_bar ;
run_tasks () ) run_tasks () )
in in
run_tasks () ; TaskBar.finish task_bar run_tasks () ;
TaskBar.finish task_bar

7
infer/src/backend/ondemand.ml
Unescape View File

@ -179,7 +179,8 @@ let run_proc_analysis ~caller_pdesc callee_pdesc =
if Config.debug_mode then if Config.debug_mode then
DotCfg.emit_proc_desc (Procdesc.get_attributes callee_pdesc).translation_unit callee_pdesc ; DotCfg.emit_proc_desc (Procdesc.get_attributes callee_pdesc).translation_unit callee_pdesc ;
let initial_callee_summary = Summary.OnDisk.reset callee_pdesc in let initial_callee_summary = Summary.OnDisk.reset callee_pdesc in
add_active callee_pname ; initial_callee_summary add_active callee_pname ;
initial_callee_summary
in in
let postprocess summary = let postprocess summary =
decr nesting ; decr nesting ;
@ -223,7 +224,9 @@ let run_proc_analysis ~caller_pdesc callee_pdesc =
IExn.reraise_if exn ~f:(fun () -> IExn.reraise_if exn ~f:(fun () ->
match exn with match exn with
| TaskSchedulerTypes.ProcnameAlreadyLocked _ -> | TaskSchedulerTypes.ProcnameAlreadyLocked _ ->
clear_actives () ; restore_global_state old_state ; true clear_actives () ;
restore_global_state old_state ;
true
| _ -> | _ ->
if not !logged_error then ( if not !logged_error then (
let source_file = attributes.ProcAttributes.translation_unit in let source_file = attributes.ProcAttributes.translation_unit in

6
infer/src/backend/printer.ml
Unescape View File

@ -162,7 +162,8 @@ end = struct
with Caml.Not_found -> with Caml.Not_found ->
Hashtbl.add err_per_line err_data.loc.Location.line (String.Set.singleton err_str) Hashtbl.add err_per_line err_data.loc.Location.line (String.Set.singleton err_str)
in in
Errlog.iter add_err err_log ; err_per_line Errlog.iter add_err err_log ;
err_per_line
(** Create error message for html file *) (** Create error message for html file *)
@ -287,7 +288,8 @@ end = struct
fun node -> fun node ->
let file = (Procdesc.Node.get_loc node).Location.file in let file = (Procdesc.Node.get_loc node).Location.file in
if not (Hashtbl.mem written_files file) then ( if not (Hashtbl.mem written_files file) then (
write_all_html_files file ; Hashtbl.add written_files file () ) write_all_html_files file ;
Hashtbl.add written_files file () )
end end
(* =============== Printing functions =============== *) (* =============== Printing functions =============== *)

3
infer/src/base/CommandLineOption.ml
Unescape View File

@ -1001,7 +1001,8 @@ let parse_args ~usage initial_action ?initial_command args =
anymore *) anymore *)
assert false assert false
in in
parse_loop () ; curr_usage parse_loop () ;
curr_usage
let keep_args_file = ref false let keep_args_file = ref false

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

@ -399,7 +399,8 @@ let implicit_sdk_root =
| None -> | None ->
let maybe_root = locate_sdk_root () in let maybe_root = locate_sdk_root () in
let putenv x = Unix.putenv ~key:infer_sdkroot_env_var ~data:x in let putenv x = Unix.putenv ~key:infer_sdkroot_env_var ~data:x in
Option.iter ~f:putenv maybe_root ; maybe_root ) Option.iter ~f:putenv maybe_root ;
maybe_root )
let startup_action = let startup_action =
@ -1067,7 +1068,9 @@ and ( biabduction_models_mode
[only_cheap_debug] [only_cheap_debug]
and (_ : int option ref) = and (_ : int option ref) =
CLOpt.mk_int_opt ~long:"debug-level" ~in_help:all_generic_manuals ~meta:"level" CLOpt.mk_int_opt ~long:"debug-level" ~in_help:all_generic_manuals ~meta:"level"
~f:(fun level -> set_debug_level level ; level) ~f:(fun level ->
set_debug_level level ;
level )
{|Debug level (sets $(b,--bo-debug) $(i,level), $(b,--debug-level-analysis) $(i,level), $(b,--debug-level-capture) $(i,level), $(b,--debug-level-linters) $(i,level)): {|Debug level (sets $(b,--bo-debug) $(i,level), $(b,--debug-level-analysis) $(i,level), $(b,--debug-level-capture) $(i,level), $(b,--debug-level-linters) $(i,level)):
- 0: only basic debugging enabled - 0: only basic debugging enabled
- 1: verbose debugging enabled - 1: verbose debugging enabled
@ -1167,7 +1170,8 @@ and () =
CLOpt.mk_string_list ?deprecated ~long CLOpt.mk_string_list ?deprecated ~long
~f:(fun issue_id -> ~f:(fun issue_id ->
let issue = IssueType.register_from_string issue_id in let issue = IssueType.register_from_string issue_id in
IssueType.set_enabled issue b ; issue_id ) IssueType.set_enabled issue b ;
issue_id )
?default ~meta:"issue_type" ?default ~meta:"issue_type"
~default_to_string:(fun _ -> "") ~default_to_string:(fun _ -> "")
~in_help:InferCommand.[(Report, manual_generic)] ~in_help:InferCommand.[(Report, manual_generic)]
@ -2370,7 +2374,8 @@ let post_parsing_initialization command_opt =
( match !version with ( match !version with
| `Full when !buck -> | `Full when !buck ->
(* Buck reads stderr in some versions, stdout in others *) (* Buck reads stderr in some versions, stdout in others *)
print_endline version_string ; prerr_endline version_string print_endline version_string ;
prerr_endline version_string
| `Javac when !buck -> | `Javac when !buck ->
(* print buck key *) (* print buck key *)
let infer_version = let infer_version =
@ -3131,7 +3136,10 @@ let is_in_custom_symbols list_name symbol =
false false
let execution_id = Random.self_init () ; Random.int64 Int64.max_value let execution_id =
Random.self_init () ;
Random.int64 Int64.max_value
let toplevel_results_dir = let toplevel_results_dir =
if CLOpt.is_originator then ( if CLOpt.is_originator then (

6
infer/src/base/DB.ml
Unescape View File

@ -148,10 +148,12 @@ module Results_dir = struct
let rec create = function let rec create = function
| [] -> | [] ->
let fname = path_to_filename pk [] in let fname = path_to_filename pk [] in
Utils.create_dir fname ; fname Utils.create_dir fname ;
fname
| name :: names -> | name :: names ->
let new_path = Filename.concat (create names) name in let new_path = Filename.concat (create names) name in
Utils.create_dir new_path ; new_path Utils.create_dir new_path ;
new_path
in in
let filename, dir_path = let filename, dir_path =
match List.rev path with match List.rev path with

9
infer/src/base/DBWriter.ml
Unescape View File

@ -288,7 +288,11 @@ module Server = struct
the number of workers, though even that is a guess. *) the number of workers, though even that is a guess. *)
Unix.listen socket ~backlog:Config.jobs ; Unix.listen socket ~backlog:Config.jobs ;
L.debug Analysis Quiet "Sqlite write daemon: set up complete, waiting for connections@." ; L.debug Analysis Quiet "Sqlite write daemon: set up complete, waiting for connections@." ;
let shutdown () = in_results_dir ~f:(fun () -> Unix.close socket ; Unix.remove socket_name) in let shutdown () =
in_results_dir ~f:(fun () ->
Unix.close socket ;
Unix.remove socket_name )
in
Utils.try_finally_swallow_timeout ~f:(fun () -> server_loop socket) ~finally:shutdown Utils.try_finally_swallow_timeout ~f:(fun () -> server_loop socket) ~finally:shutdown
@ -311,7 +315,8 @@ module Server = struct
let start () = let start () =
match Unix.fork () with match Unix.fork () with
| `In_the_child -> | `In_the_child ->
ForkUtils.protect ~f:server () ; L.exit 0 ForkUtils.protect ~f:server () ;
L.exit 0
| `In_the_parent _child_pid -> | `In_the_parent _child_pid ->
(* wait for socket to appear, try 5 times, with a 0.1 sec timeout each time ; (* wait for socket to appear, try 5 times, with a 0.1 sec timeout each time ;
choice of numbers is completely arbitrary *) choice of numbers is completely arbitrary *)

10
infer/src/base/Epilogues.ml
Unescape View File

@ -19,7 +19,10 @@ let register callback_ref ~f ~description =
(Unix.getpid ()) description Exn.pp exn (Unix.getpid ()) description Exn.pp exn
in in
let g = !callback_ref in let g = !callback_ref in
callback_ref := fun () -> f_no_exn () ; g () callback_ref :=
fun () ->
f_no_exn () ;
g ()
let register_early ~f ~description = register early_callback ~f ~description let register_early ~f ~description = register early_callback ~f ~description
@ -30,7 +33,10 @@ let early () = !early_callback ()
let late () = !late_callback () let late () = !late_callback ()
let run () = early () ; late () let run () =
early () ;
late ()
(* Run the epilogues when we get SIGINT (Control-C). *) (* Run the epilogues when we get SIGINT (Control-C). *)
let () = let () =

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

@ -29,7 +29,9 @@ let read_file fname =
lines := line :: !lines lines := line :: !lines
done ; done ;
assert false (* execution never reaches here *) assert false (* execution never reaches here *)
with End_of_file -> In_channel.close cin ; Array.of_list_rev !lines with End_of_file ->
In_channel.close cin ;
Array.of_list_rev !lines
let file_data (hash : t) fname = let file_data (hash : t) fname =
@ -37,7 +39,8 @@ let file_data (hash : t) fname =
with Caml.Not_found -> ( with Caml.Not_found -> (
try try
let lines_arr = read_file (SourceFile.to_abs_path fname) in let lines_arr = read_file (SourceFile.to_abs_path fname) in
Hashtbl.add hash fname lines_arr ; Some lines_arr 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 )

50
infer/src/base/Logging.ml
Unescape View File

@ -30,11 +30,26 @@ let dup_formatter fmt1 fmt2 =
let out_funs2 = F.pp_get_formatter_out_functions fmt2 () in let out_funs2 = F.pp_get_formatter_out_functions fmt2 () in
let f = copy_formatter fmt1 in let f = copy_formatter fmt1 in
F.pp_set_formatter_out_functions f F.pp_set_formatter_out_functions f
{ F.out_string= (fun s p n -> out_funs1.out_string s p n ; out_funs2.out_string s p n) { F.out_string=
; out_indent= (fun n -> out_funs1.out_indent n ; out_funs2.out_indent n) (fun s p n ->
; out_flush= (fun () -> out_funs1.out_flush () ; out_funs2.out_flush ()) out_funs1.out_string s p n ;
; out_newline= (fun () -> out_funs1.out_newline () ; out_funs2.out_newline ()) out_funs2.out_string s p n )
; out_spaces= (fun n -> out_funs1.out_spaces n ; out_funs2.out_spaces n) } ; ; out_indent=
(fun n ->
out_funs1.out_indent n ;
out_funs2.out_indent n )
; out_flush=
(fun () ->
out_funs1.out_flush () ;
out_funs2.out_flush () )
; out_newline=
(fun () ->
out_funs1.out_newline () ;
out_funs2.out_newline () )
; out_spaces=
(fun n ->
out_funs1.out_spaces n ;
out_funs2.out_spaces n ) } ;
f f
@ -73,13 +88,19 @@ let mk_file_formatter file_fmt category0 =
print_prefix_if_newline () ; print_prefix_if_newline () ;
out_functions_orig.out_string s p n out_functions_orig.out_string s p n
in in
let out_indent n = print_prefix_if_newline () ; out_functions_orig.out_indent n in let out_indent n =
print_prefix_if_newline () ;
out_functions_orig.out_indent n
in
let out_newline () = let out_newline () =
print_prefix_if_newline () ; print_prefix_if_newline () ;
out_functions_orig.out_newline () ; out_functions_orig.out_newline () ;
is_newline := true is_newline := true
in in
let out_spaces n = print_prefix_if_newline () ; out_functions_orig.out_spaces n in let out_spaces n =
print_prefix_if_newline () ;
out_functions_orig.out_spaces n
in
F.pp_set_formatter_out_functions f F.pp_set_formatter_out_functions f
{F.out_string; out_flush= out_functions_orig.out_flush; out_indent; out_newline; out_spaces} ; {F.out_string; out_flush= out_functions_orig.out_flush; out_indent; out_newline; out_spaces} ;
f f
@ -163,7 +184,8 @@ let close_logs () =
let close_fmt (_, formatters) = flush_formatters formatters in let close_fmt (_, formatters) = flush_formatters formatters in
List.iter ~f:close_fmt !logging_formatters ; List.iter ~f:close_fmt !logging_formatters ;
Option.iter !log_file ~f:(function file_fmt, chan -> Option.iter !log_file ~f:(function file_fmt, chan ->
F.pp_print_flush file_fmt () ; Out_channel.close chan ) F.pp_print_flush file_fmt () ;
Out_channel.close chan )
let () = Epilogues.register ~f:close_logs ~description:"flushing logs and closing log file" let () = Epilogues.register ~f:close_logs ~description:"flushing logs and closing log file"
@ -216,7 +238,8 @@ let log_task fmt =
let task_progress ~f pp x = let task_progress ~f pp x =
log_task "%a starting@." pp x ; log_task "%a starting@." pp x ;
let result = f () in let result = f () in
log_task "%a DONE@." pp x ; result log_task "%a DONE@." pp x ;
result
let user_warning fmt = log ~to_console:(not Config.quiet) user_warning_file_fmts fmt let user_warning fmt = log ~to_console:(not Config.quiet) user_warning_file_fmts fmt
@ -372,7 +395,8 @@ let reset_delayed_prints () = delayed_prints := new_delayed_prints ()
(** return the delayed prints *) (** return the delayed prints *)
let get_and_reset_delayed_prints () = let get_and_reset_delayed_prints () =
let res = !delayed_prints in let res = !delayed_prints in
reset_delayed_prints () ; res reset_delayed_prints () ;
res
let force_and_reset_delayed_prints f = let force_and_reset_delayed_prints f =
@ -394,7 +418,11 @@ let d_kfprintf ?color k f fmt =
match color with match color with
| Some color when Config.write_html -> | Some color when Config.write_html ->
F.fprintf f "<span class='%s'>" (Pp.color_string color) ; F.fprintf f "<span class='%s'>" (Pp.color_string color) ;
F.kfprintf (fun f -> F.pp_print_string f "</span>" ; k f) f fmt F.kfprintf
(fun f ->
F.pp_print_string f "</span>" ;
k f )
f fmt
| _ -> | _ ->
F.kfprintf k f fmt F.kfprintf k f fmt

9
infer/src/base/ProcessPool.ml
Unescape View File

@ -308,7 +308,8 @@ let collect_results (pool : (_, 'final, _) t) =
let wait_all pool = let wait_all pool =
(* tell each alive worker to go home *) (* tell each alive worker to go home *)
Array.iter pool.slots ~f:(fun {down_pipe} -> Array.iter pool.slots ~f:(fun {down_pipe} ->
marshal_to_pipe down_pipe GoHome ; Out_channel.close down_pipe ) ; marshal_to_pipe down_pipe GoHome ;
Out_channel.close down_pipe ) ;
let results = collect_results pool in let results = collect_results pool in
(* wait(2) workers one by one; the order doesn't matter since we want to wait for all of them (* wait(2) workers one by one; the order doesn't matter since we want to wait for all of them
eventually anyway. *) eventually anyway. *)
@ -458,10 +459,12 @@ let run pool =
let buffer = Bytes.create buffer_size in let buffer = Bytes.create buffer_size in
(* wait for all children to run out of tasks *) (* wait for all children to run out of tasks *)
while not (pool.tasks.is_empty () && all_children_idle pool) do while not (pool.tasks.is_empty () && all_children_idle pool) do
process_updates pool buffer ; TaskBar.refresh pool.task_bar process_updates pool buffer ;
TaskBar.refresh pool.task_bar
done ; done ;
let results = wait_all pool in let results = wait_all pool in
TaskBar.finish pool.task_bar ; results ) TaskBar.finish pool.task_bar ;
results )
let run pool = let run pool =

3
infer/src/base/ScubaLogging.ml
Unescape View File

@ -75,7 +75,8 @@ let log_message ~label ~message = log_one (LogEntry.mk_string ~label ~message)
let execute_with_time_logging label f = let execute_with_time_logging label f =
let ret_val, duration_ms = Utils.timeit ~f in let ret_val, duration_ms = Utils.timeit ~f in
let entry = LogEntry.mk_time ~label ~duration_ms in let entry = LogEntry.mk_time ~label ~duration_ms in
log_one entry ; ret_val log_one entry ;
ret_val
let flush_log_events () = let flush_log_events () =

6
infer/src/base/SymOp.ml
Unescape View File

@ -25,7 +25,8 @@ let exn_not_failure = function Analysis_failure_exe _ -> false | _ -> true
let try_finally ~f ~finally = let try_finally ~f ~finally =
match f () with match f () with
| r -> | r ->
finally () ; r finally () ;
r
| exception (Analysis_failure_exe _ as f_exn) -> | exception (Analysis_failure_exe _ as f_exn) ->
IExn.reraise_after f_exn ~f:(fun () -> IExn.reraise_after f_exn ~f:(fun () ->
try finally () with _ -> (* swallow in favor of the original exception *) () ) try finally () with _ -> (* swallow in favor of the original exception *) () )
@ -112,7 +113,8 @@ let unset_wallclock_alarm () = !gs.last_wallclock <- None
let check_wallclock_alarm () = let check_wallclock_alarm () =
match (!gs.last_wallclock, !wallclock_timeout_handler) with match (!gs.last_wallclock, !wallclock_timeout_handler) with
| Some alarm_time, Some handler when Float.(Unix.gettimeofday () >= alarm_time) -> | Some alarm_time, Some handler when Float.(Unix.gettimeofday () >= alarm_time) ->
unset_wallclock_alarm () ; handler () unset_wallclock_alarm () ;
handler ()
| _ -> | _ ->
() ()

3
infer/src/base/TaskBar.ml
Unescape View File

@ -144,7 +144,8 @@ let create ~jobs =
; tasks_done= 0 ; tasks_done= 0
; tasks_total= 0 } ; tasks_total= 0 }
in in
ANSITerminal.erase Below ; MultiLine task_bar ANSITerminal.erase Below ;
MultiLine task_bar
let update_status_multiline task_bar ~slot:job t0 status = let update_status_multiline task_bar ~slot:job t0 status =

25
infer/src/base/Utils.ml
Unescape View File

@ -66,7 +66,8 @@ let read_file fname =
cleanup () ; cleanup () ;
Ok (List.rev !res) Ok (List.rev !res)
| Sys_error error -> | Sys_error error ->
cleanup () ; Error error cleanup () ;
Error error
(** type for files used for printing *) (** type for files used for printing *)
@ -223,7 +224,11 @@ let create_file_lock () =
let with_file_lock ~file_lock:{file; oc; fd} ~f = let with_file_lock ~file_lock:{file; oc; fd} ~f =
let finally () = Core.Unix.close fd ; Out_channel.close oc ; Core.Unix.remove file in let finally () =
Core.Unix.close fd ;
Out_channel.close oc ;
Core.Unix.remove file
in
try_finally_swallow_timeout ~f ~finally try_finally_swallow_timeout ~f ~finally
@ -256,7 +261,10 @@ let echo_in chan_in = with_channel_in ~f:print_endline chan_in
let with_process_in command read = let with_process_in command read =
let chan = Unix.open_process_in command in let chan = Unix.open_process_in command in
let f () = read chan in let f () = read chan in
let finally () = consume_in chan ; Unix.close_process_in chan in let finally () =
consume_in chan ;
Unix.close_process_in chan
in
do_finally_swallow_timeout ~f ~finally do_finally_swallow_timeout ~f ~finally
@ -310,7 +318,10 @@ let realpath ?(warn_on_error = true) path =
let devnull = lazy (Unix.openfile "/dev/null" ~mode:[Unix.O_WRONLY]) let devnull = lazy (Unix.openfile "/dev/null" ~mode:[Unix.O_WRONLY])
let suppress_stderr2 f2 x1 x2 = let suppress_stderr2 f2 x1 x2 =
let restore_stderr src = Unix.dup2 ~src ~dst:Unix.stderr ; Unix.close src in let restore_stderr src =
Unix.dup2 ~src ~dst:Unix.stderr ;
Unix.close src
in
let orig_stderr = Unix.dup Unix.stderr in let orig_stderr = Unix.dup Unix.stderr in
Unix.dup2 ~src:(Lazy.force devnull) ~dst:Unix.stderr ; Unix.dup2 ~src:(Lazy.force devnull) ~dst:Unix.stderr ;
let f () = f2 x1 x2 in let f () = f2 x1 x2 in
@ -343,7 +354,8 @@ let rec rmtree name =
then rmtree (name ^/ entry) ; then rmtree (name ^/ entry) ;
rmdir dir rmdir dir
| None -> | None ->
Unix.closedir dir ; Unix.rmdir name Unix.closedir dir ;
Unix.rmdir name
in in
rmdir dir rmdir dir
| _ -> | _ ->
@ -505,4 +517,5 @@ let zip_fold_filenames ~init ~f ~zip_filename =
let file_in = Zip.open_in zip_filename in let file_in = Zip.open_in zip_filename in
let collect acc (entry : Zip.entry) = f acc entry.filename in let collect acc (entry : Zip.entry) = f acc entry.filename in
let result = List.fold ~f:collect ~init (Zip.entries file_in) in let result = List.fold ~f:collect ~init (Zip.entries file_in) in
Zip.close_in file_in ; result Zip.close_in file_in ;
result

12
infer/src/biabduction/Abs.ml
Unescape View File

@ -560,7 +560,8 @@ let discover_para_candidates tenv p =
get_edges_sigma sigma_rest get_edges_sigma sigma_rest
| Predicates.Hpointsto (root, se, te) :: sigma_rest -> | Predicates.Hpointsto (root, se, te) :: sigma_rest ->
let rec_flds = typ_get_recursive_flds tenv te in let rec_flds = typ_get_recursive_flds tenv te in
get_edges_strexp rec_flds root se ; get_edges_sigma sigma_rest get_edges_strexp rec_flds root se ;
get_edges_sigma sigma_rest
in in
let rec find_all_consecutive_edges found edges_seen = function let rec find_all_consecutive_edges found edges_seen = function
| [] -> | [] ->
@ -610,7 +611,8 @@ let discover_para_dll_candidates tenv p =
get_edges_sigma sigma_rest get_edges_sigma sigma_rest
| Predicates.Hpointsto (root, se, te) :: sigma_rest -> | Predicates.Hpointsto (root, se, te) :: sigma_rest ->
let rec_flds = typ_get_recursive_flds tenv te in let rec_flds = typ_get_recursive_flds tenv te in
get_edges_strexp rec_flds root se ; get_edges_sigma sigma_rest get_edges_strexp rec_flds root se ;
get_edges_sigma sigma_rest
in in
let rec find_all_consecutive_edges found edges_seen = function let rec find_all_consecutive_edges found edges_seen = function
| [] -> | [] ->
@ -859,7 +861,8 @@ let abs_rules_apply_lists tenv (p_in : Prop.normal Prop.t) : Prop.normal Prop.t
let p1 = abs_rules_apply_rsets tenv old_rsets p_in in let p1 = abs_rules_apply_rsets tenv old_rsets p_in in
let p2 = discover_then_abstract p1 in let p2 = discover_then_abstract p1 in
let new_rules = old_rsets @ !new_rsets in let new_rules = old_rsets @ !new_rsets in
set_current_rules new_rules ; p2 set_current_rules new_rules ;
p2
let abs_rules_apply tenv (p_in : Prop.normal Prop.t) : Prop.normal Prop.t = let abs_rules_apply tenv (p_in : Prop.normal Prop.t) : Prop.normal Prop.t =
@ -1065,7 +1068,8 @@ let check_junk {InterproceduralAnalysis.proc_desc; err_log; tenv} prop =
| _ -> | _ ->
() ) ) () ) )
in in
List.iter ~f:do_entry entries ; !res List.iter ~f:do_entry entries ;
!res
in in
L.d_decrease_indent () ; L.d_decrease_indent () ;
let is_undefined = let is_undefined =

27
infer/src/biabduction/Absarray.ml
Unescape View File

@ -222,7 +222,8 @@ end = struct
() ) ; () ) ;
iterate (hpred :: sigma_seen) sigma_rest iterate (hpred :: sigma_seen) sigma_rest
in in
iterate [] sigma ; !found iterate [] sigma ;
!found
(** Get the matched strexp *) (** Get the matched strexp *)
@ -508,16 +509,26 @@ let strexp_do_abstract tenv footprint_part p ((path, se_in, _) : StrexpMatch.str
if Config.trace_absarray && not footprint_part then L.d_strln "strexp_do_abstract (nonfootprint)" ; if Config.trace_absarray && not footprint_part then L.d_strln "strexp_do_abstract (nonfootprint)" ;
let prune_and_blur d_keys keep blur path keep_keys blur_keys = let prune_and_blur d_keys keep blur path keep_keys blur_keys =
let p2, changed2 = let p2, changed2 =
if Config.trace_absarray then (L.d_str "keep " ; d_keys keep_keys ; L.d_ln ()) ; if Config.trace_absarray then (
L.d_str "keep " ;
d_keys keep_keys ;
L.d_ln () ) ;
keep p path keep_keys keep p path keep_keys
in in
let p3, changed3 = let p3, changed3 =
if List.is_empty blur_keys then (p2, false) if List.is_empty blur_keys then (p2, false)
else ( else (
if Config.trace_absarray then (L.d_str "blur " ; d_keys blur_keys ; L.d_ln ()) ; if Config.trace_absarray then (
L.d_str "blur " ;
d_keys blur_keys ;
L.d_ln () ) ;
blur p2 path blur_keys ) blur p2 path blur_keys )
in in
if Config.trace_absarray then (L.d_strln "Returns" ; Prop.d_prop p3 ; L.d_ln () ; L.d_ln ()) ; if Config.trace_absarray then (
L.d_strln "Returns" ;
Prop.d_prop p3 ;
L.d_ln () ;
L.d_ln () ) ;
(p3, changed2 || changed3) (p3, changed2 || changed3)
in in
let prune_and_blur_indices = let prune_and_blur_indices =
@ -548,7 +559,10 @@ let strexp_do_abstract tenv footprint_part p ((path, se_in, _) : StrexpMatch.str
let keep_ksel = List.filter ~f:should_keep ksel in let keep_ksel = List.filter ~f:should_keep ksel in
let keep_keys = List.map ~f:fst keep_ksel in let keep_keys = List.map ~f:fst keep_ksel in
let keep_keys' = if List.is_empty keep_keys then default_keys else keep_keys in let keep_keys' = if List.is_empty keep_keys then default_keys else keep_keys in
if Config.trace_absarray then (L.d_str "keep " ; d_keys keep_keys' ; L.d_ln ()) ; if Config.trace_absarray then (
L.d_str "keep " ;
d_keys keep_keys' ;
L.d_ln () ) ;
abstract keep_keys' [] abstract keep_keys' []
in in
let do_array_reexecution esel = let do_array_reexecution esel =
@ -625,7 +639,8 @@ let check_after_array_abstraction tenv prop =
in in
let check_sigma sigma = List.iter ~f:check_hpred sigma in let check_sigma sigma = List.iter ~f:check_hpred sigma in
(* check_footprint_pure prop; *) (* check_footprint_pure prop; *)
check_sigma prop.Prop.sigma ; check_sigma prop.Prop.sigma_fp check_sigma prop.Prop.sigma ;
check_sigma prop.Prop.sigma_fp
(** Apply array abstraction and check the result *) (** Apply array abstraction and check the result *)

9
infer/src/biabduction/Attribute.ml
Unescape View File

@ -35,7 +35,8 @@ let add_or_replace_check_changed tenv check_attribute_change prop atom =
let atom_map = function let atom_map = function
| (Predicates.Apred (att, exp :: _) | Anpred (att, exp :: _)) | (Predicates.Apred (att, exp :: _) | Anpred (att, exp :: _))
when Exp.equal nexp exp && attributes_in_same_category att att0 -> when Exp.equal nexp exp && attributes_in_same_category att att0 ->
check_attribute_change att att0 ; atom check_attribute_change att att0 ;
atom
| atom' -> | atom' ->
atom' atom'
in in
@ -57,7 +58,8 @@ let add_or_replace tenv prop atom =
let get_all (prop : 'a Prop.t) = let get_all (prop : 'a Prop.t) =
let res = ref [] in let res = ref [] in
let do_atom a = if is_pred a then res := a :: !res 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 *) (** Get the attribute associated to the expression, if any *)
@ -258,7 +260,8 @@ let find_arithmetic_problem tenv proc_node_session prop exp =
| Exp.Lfield (e, _, _) -> | Exp.Lfield (e, _, _) ->
walk e walk e
| Exp.Lindex (e1, e2) -> | Exp.Lindex (e1, e2) ->
walk e1 ; walk e2 walk e1 ;
walk e2
| Exp.Sizeof {dynamic_length= None} -> | Exp.Sizeof {dynamic_length= None} ->
() ()
| Exp.Sizeof {dynamic_length= Some len} -> | Exp.Sizeof {dynamic_length= Some len} ->

4
infer/src/biabduction/Builtin.ml
Unescape View File

@ -38,7 +38,9 @@ let check_register_populated () =
(** get the symbolic execution handler associated to the builtin function name *) (** get the symbolic execution handler associated to the builtin function name *)
let get name : t option = let get name : t option =
try Some (Procname.Hash.find builtin_functions name) try Some (Procname.Hash.find builtin_functions name)
with Caml.Not_found -> check_register_populated () ; None with Caml.Not_found ->
check_register_populated () ;
None
(** register a builtin [Procname.t] and symbolic execution handler *) (** register a builtin [Procname.t] and symbolic execution handler *)

273
infer/src/biabduction/Dom.ml
Unescape View File

@ -29,10 +29,13 @@ let equal_sigma sigma1 sigma2 =
| [], [] -> | [], [] ->
() ()
| [], _ :: _ | _ :: _, [] -> | [], _ :: _ | _ :: _, [] ->
L.d_strln "failure reason 1" ; raise Predicates.JoinFail L.d_strln "failure reason 1" ;
raise Predicates.JoinFail
| hpred1 :: sigma1_rest', hpred2 :: sigma2_rest' -> | hpred1 :: sigma1_rest', hpred2 :: sigma2_rest' ->
if Predicates.equal_hpred hpred1 hpred2 then f sigma1_rest' sigma2_rest' if Predicates.equal_hpred hpred1 hpred2 then f sigma1_rest' sigma2_rest'
else (L.d_strln "failure reason 2" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 2" ;
raise Predicates.JoinFail )
in in
let sigma1_sorted = List.sort ~compare:Predicates.compare_hpred sigma1 in let sigma1_sorted = List.sort ~compare:Predicates.compare_hpred sigma1 in
let sigma2_sorted = List.sort ~compare:Predicates.compare_hpred sigma2 in let sigma2_sorted = List.sort ~compare:Predicates.compare_hpred sigma2 in
@ -91,7 +94,10 @@ end = struct
let lookup' tbl e default = let lookup' tbl e default =
match e with match e with
| Exp.Var _ -> ( | Exp.Var _ -> (
try Hashtbl.find tbl e with Caml.Not_found -> Hashtbl.replace tbl e default ; default ) try Hashtbl.find tbl e
with Caml.Not_found ->
Hashtbl.replace tbl e default ;
default )
| _ -> | _ ->
assert false assert false
@ -107,7 +113,8 @@ end = struct
if Exp.equal e e' then e if Exp.equal e e' then e
else else
let root = find' tbl e' in let root = find' tbl e' in
Hashtbl.replace tbl e root ; root Hashtbl.replace tbl e root ;
root
| _ -> | _ ->
assert false assert false
@ -119,7 +126,9 @@ end = struct
let new_c = lookup_const' const_tbl new_r in let new_c = lookup_const' const_tbl new_r in
let old_c = lookup_const' const_tbl old_r in let old_c = lookup_const' const_tbl old_r in
let res_c = Exp.Set.union new_c old_c in let res_c = Exp.Set.union new_c old_c in
if Exp.Set.cardinal res_c > 1 then (L.d_strln "failure reason 3" ; raise Predicates.JoinFail) ; if Exp.Set.cardinal res_c > 1 then (
L.d_strln "failure reason 3" ;
raise Predicates.JoinFail ) ;
Hashtbl.replace tbl old_r new_r ; Hashtbl.replace tbl old_r new_r ;
Hashtbl.replace const_tbl new_r res_c Hashtbl.replace const_tbl new_r res_c
@ -127,7 +136,9 @@ end = struct
let replace_const' tbl const_tbl e c = let replace_const' tbl const_tbl e c =
let r = find' tbl e in let r = find' tbl e in
let set = Exp.Set.add c (lookup_const' const_tbl r) in let set = Exp.Set.add c (lookup_const' const_tbl r) in
if Exp.Set.cardinal set > 1 then (L.d_strln "failure reason 4" ; raise Predicates.JoinFail) ; if Exp.Set.cardinal set > 1 then (
L.d_strln "failure reason 4" ;
raise Predicates.JoinFail ) ;
Hashtbl.replace const_tbl r set Hashtbl.replace const_tbl r set
@ -145,15 +156,22 @@ end = struct
| false, true -> | false, true ->
replace_const' tbl const_tbl e' e replace_const' tbl const_tbl e' e
| _ -> | _ ->
L.d_strln "failure reason 5" ; raise Predicates.JoinFail ) L.d_strln "failure reason 5" ;
raise Predicates.JoinFail )
| Exp.Var id, Exp.Const _ | Exp.Var id, Exp.Lvar _ -> | Exp.Var id, Exp.Const _ | Exp.Var id, Exp.Lvar _ ->
if can_rename id then replace_const' tbl const_tbl e e' if can_rename id then replace_const' tbl const_tbl e e'
else (L.d_strln "failure reason 6" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 6" ;
raise Predicates.JoinFail )
| Exp.Const _, Exp.Var id' | Exp.Lvar _, Exp.Var id' -> | Exp.Const _, Exp.Var id' | Exp.Lvar _, Exp.Var id' ->
if can_rename id' then replace_const' tbl const_tbl e' e if can_rename id' then replace_const' tbl const_tbl e' e
else (L.d_strln "failure reason 7" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 7" ;
raise Predicates.JoinFail )
| _ -> | _ ->
if not (Exp.equal e e') then (L.d_strln "failure reason 8" ; raise Predicates.JoinFail) if not (Exp.equal e e') then (
L.d_strln "failure reason 8" ;
raise Predicates.JoinFail )
else () else ()
@ -228,9 +246,15 @@ end = struct
end end
module CheckJoinPre : InfoLossCheckerSig = struct module CheckJoinPre : InfoLossCheckerSig = struct
let init sigma1 sigma2 = NonInj.init () ; Dangling.init sigma1 sigma2 let init sigma1 sigma2 =
NonInj.init () ;
Dangling.init sigma1 sigma2
let final () =
NonInj.final () ;
Dangling.final ()
let final () = NonInj.final () ; Dangling.final ()
let fail_case side e es = let fail_case side e es =
let side_op = opposite side in let side_op = opposite side in
@ -607,7 +631,8 @@ end = struct
| _ -> | _ ->
() ()
in in
List.iter ~f !tbl ; List.rev !res List.iter ~f !tbl ;
List.rev !res
(* Return the triple whose side is [e], if it exists unique *) (* Return the triple whose side is [e], if it exists unique *)
@ -620,12 +645,14 @@ end = struct
if todo then Todo.push t ; if todo then Todo.push t ;
id id
| _ -> | _ ->
L.d_strln "failure reason 9" ; raise Predicates.JoinFail ) L.d_strln "failure reason 9" ;
raise Predicates.JoinFail )
| Exp.Var _ | Exp.Const _ | Exp.Lvar _ -> | Exp.Var _ | Exp.Const _ | Exp.Lvar _ ->
if todo then Todo.push (e, e, e) ; if todo then Todo.push (e, e, e) ;
e e
| _ -> | _ ->
L.d_strln "failure reason 10" ; raise Predicates.JoinFail L.d_strln "failure reason 10" ;
raise Predicates.JoinFail
let lookup side e = lookup' false side e let lookup side e = lookup' false side e
@ -657,7 +684,8 @@ end = struct
false false
in in
if find_duplicates sub_list_side_sorted then ( if find_duplicates sub_list_side_sorted then (
L.d_strln "failure reason 11" ; raise Predicates.JoinFail ) L.d_strln "failure reason 11" ;
raise Predicates.JoinFail )
else Predicates.subst_of_list sub_list_side else Predicates.subst_of_list sub_list_side
@ -752,7 +780,10 @@ end = struct
let get_other_atoms tenv side atom_in = let get_other_atoms tenv side atom_in =
let build_other_atoms construct side e = let build_other_atoms construct side e =
if Config.trace_join then (L.d_str "build_other_atoms: " ; Exp.d_exp e ; L.d_ln ()) ; if Config.trace_join then (
L.d_str "build_other_atoms: " ;
Exp.d_exp e ;
L.d_ln () ) ;
let others1 = get_others_direct_or_induced side e in let others1 = get_others_direct_or_induced side e in
let others2 = match others1 with None -> get_others_deep side e | Some _ -> others1 in let others2 = match others1 with None -> get_others_deep side e | Some _ -> others1 in
match others2 with match others2 with
@ -829,7 +860,9 @@ end = struct
&& not (Exp.free_vars e2 |> Sequence.exists ~f:can_rename) && not (Exp.free_vars e2 |> Sequence.exists ~f:can_rename)
then then
if Exp.equal e1 e2 then e1 if Exp.equal e1 e2 then e1
else (L.d_strln "failure reason 13" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 13" ;
raise Predicates.JoinFail )
else else
match default_op with match default_op with
| ExtDefault e -> | ExtDefault e ->
@ -842,7 +875,9 @@ end = struct
Exp.Var (Ident.create_fresh kind) Exp.Var (Ident.create_fresh kind)
in in
let entry = (e1, e2, e) in let entry = (e1, e2, e) in
push entry ; Todo.push entry ; e push entry ;
Todo.push entry ;
e
end end
(** {2 Functions for constructing fresh sil data types} *) (** {2 Functions for constructing fresh sil data types} *)
@ -917,12 +952,15 @@ let ident_partial_join (id1 : Ident.t) (id2 : Ident.t) =
match (Ident.is_normal id1, Ident.is_normal id2) with match (Ident.is_normal id1, Ident.is_normal id2) with
| true, true -> | true, true ->
if Ident.equal id1 id2 then Exp.Var id1 if Ident.equal id1 id2 then Exp.Var id1
else (L.d_strln "failure reason 14" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 14" ;
raise Predicates.JoinFail )
| true, _ | _, true -> | true, _ | _, true ->
Rename.extend (Exp.Var id1) (Exp.Var id2) Rename.ExtFresh Rename.extend (Exp.Var id1) (Exp.Var id2) Rename.ExtFresh
| _ -> | _ ->
if not (ident_same_kind_primed_footprint id1 id2) then ( if not (ident_same_kind_primed_footprint id1 id2) then (
L.d_strln "failure reason 15" ; raise Predicates.JoinFail ) L.d_strln "failure reason 15" ;
raise Predicates.JoinFail )
else else
let e1 = Exp.Var id1 in let e1 = Exp.Var id1 in
let e2 = Exp.Var id2 in let e2 = Exp.Var id2 in
@ -933,7 +971,9 @@ let ident_partial_meet (id1 : Ident.t) (id2 : Ident.t) =
match (Ident.is_normal id1, Ident.is_normal id2) with match (Ident.is_normal id1, Ident.is_normal id2) with
| true, true -> | true, true ->
if Ident.equal id1 id2 then Exp.Var id1 if Ident.equal id1 id2 then Exp.Var id1
else (L.d_strln "failure reason 16" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 16" ;
raise Predicates.JoinFail )
| true, _ -> | true, _ ->
let e1, e2 = (Exp.Var id1, Exp.Var id2) in let e1, e2 = (Exp.Var id1, Exp.Var id2) in
Rename.extend e1 e2 (Rename.ExtDefault e1) Rename.extend e1 e2 (Rename.ExtDefault e1)
@ -946,7 +986,9 @@ let ident_partial_meet (id1 : Ident.t) (id2 : Ident.t) =
else if Ident.is_footprint id1 && Ident.equal id1 id2 then else if Ident.is_footprint id1 && Ident.equal id1 id2 then
let e = Exp.Var id1 in let e = Exp.Var id1 in
Rename.extend e e (Rename.ExtDefault e) Rename.extend e e (Rename.ExtDefault e)
else (L.d_strln "failure reason 17" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 17" ;
raise Predicates.JoinFail )
(** {2 Join and Meet for Exps} *) (** {2 Join and Meet for Exps} *)
@ -959,10 +1001,13 @@ let const_partial_join c1 c2 =
let is_int = function Const.Cint _ -> true | _ -> false in let is_int = function Const.Cint _ -> true | _ -> false in
if Const.equal c1 c2 then Exp.Const c1 if Const.equal c1 c2 then Exp.Const c1
else if Const.kind_equal c1 c2 && not (is_int c1) then ( else if Const.kind_equal c1 c2 && not (is_int c1) then (
L.d_strln "failure reason 18" ; raise Predicates.JoinFail ) L.d_strln "failure reason 18" ;
raise Predicates.JoinFail )
else if !BiabductionConfig.abs_val >= 2 then else if !BiabductionConfig.abs_val >= 2 then
FreshVarExp.get_fresh_exp (Exp.Const c1) (Exp.Const c2) FreshVarExp.get_fresh_exp (Exp.Const c1) (Exp.Const c2)
else (L.d_strln "failure reason 19" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 19" ;
raise Predicates.JoinFail )
let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t = let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
@ -971,12 +1016,16 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
| Exp.Var id1, Exp.Var id2 -> | Exp.Var id1, Exp.Var id2 ->
ident_partial_join id1 id2 ident_partial_join id1 id2
| Exp.Var id, Exp.Const _ | Exp.Const _, Exp.Var id -> | Exp.Var id, Exp.Const _ | Exp.Const _, Exp.Var id ->
if Ident.is_normal id then (L.d_strln "failure reason 20" ; raise Predicates.JoinFail) if Ident.is_normal id then (
L.d_strln "failure reason 20" ;
raise Predicates.JoinFail )
else Rename.extend e1 e2 Rename.ExtFresh else Rename.extend e1 e2 Rename.ExtFresh
| Exp.Const c1, Exp.Const c2 -> | Exp.Const c1, Exp.Const c2 ->
const_partial_join c1 c2 const_partial_join c1 c2
| Exp.Var id, Exp.Lvar _ | Exp.Lvar _, Exp.Var id -> | Exp.Var id, Exp.Lvar _ | Exp.Lvar _, Exp.Var id ->
if Ident.is_normal id then (L.d_strln "failure reason 21" ; raise Predicates.JoinFail) if Ident.is_normal id then (
L.d_strln "failure reason 21" ;
raise Predicates.JoinFail )
else Rename.extend e1 e2 Rename.ExtFresh else Rename.extend e1 e2 Rename.ExtFresh
| Exp.BinOp (Binop.PlusA _, Exp.Var id1, Exp.Const _), Exp.Var id2 | Exp.BinOp (Binop.PlusA _, Exp.Var id1, Exp.Const _), Exp.Var id2
| Exp.Var id1, Exp.BinOp (Binop.PlusA _, Exp.Var id2, Exp.Const _) | Exp.Var id1, Exp.BinOp (Binop.PlusA _, Exp.Var id2, Exp.Const _)
@ -993,13 +1042,16 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
let e_res = Rename.extend (Exp.int c1') (Exp.Var id2) Rename.ExtFresh in let e_res = Rename.extend (Exp.int c1') (Exp.Var id2) Rename.ExtFresh in
Exp.BinOp (Binop.PlusA None, e_res, Exp.int c2) Exp.BinOp (Binop.PlusA None, e_res, Exp.int c2)
| Exp.Cast (t1, e1), Exp.Cast (t2, e2) -> | Exp.Cast (t1, e1), Exp.Cast (t2, e2) ->
if not (Typ.equal t1 t2) then (L.d_strln "failure reason 22" ; raise Predicates.JoinFail) if not (Typ.equal t1 t2) then (
L.d_strln "failure reason 22" ;
raise Predicates.JoinFail )
else else
let e1'' = exp_partial_join e1 e2 in let e1'' = exp_partial_join e1 e2 in
Exp.Cast (t1, e1'') Exp.Cast (t1, e1'')
| Exp.UnOp (unop1, e1, topt1), Exp.UnOp (unop2, e2, _) -> | Exp.UnOp (unop1, e1, topt1), Exp.UnOp (unop2, e2, _) ->
if not (Unop.equal unop1 unop2) then ( if not (Unop.equal unop1 unop2) then (
L.d_strln "failure reason 23" ; raise Predicates.JoinFail ) L.d_strln "failure reason 23" ;
raise Predicates.JoinFail )
else Exp.UnOp (unop1, exp_partial_join e1 e2, topt1) (* should be topt1 = topt2 *) else Exp.UnOp (unop1, exp_partial_join e1 e2, topt1) (* should be topt1 = topt2 *)
| Exp.BinOp (Binop.PlusPI, e1, e1'), Exp.BinOp (Binop.PlusPI, e2, e2') -> | Exp.BinOp (Binop.PlusPI, e1, e1'), Exp.BinOp (Binop.PlusPI, e2, e2') ->
let e1'' = exp_partial_join e1 e2 in let e1'' = exp_partial_join e1 e2 in
@ -1013,18 +1065,21 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
Exp.BinOp (Binop.PlusPI, e1'', e2'') Exp.BinOp (Binop.PlusPI, e1'', e2'')
| Exp.BinOp (binop1, e1, e1'), Exp.BinOp (binop2, e2, e2') -> | Exp.BinOp (binop1, e1, e1'), Exp.BinOp (binop2, e2, e2') ->
if not (Binop.equal binop1 binop2) then ( if not (Binop.equal binop1 binop2) then (
L.d_strln "failure reason 24" ; raise Predicates.JoinFail ) L.d_strln "failure reason 24" ;
raise Predicates.JoinFail )
else else
let e1'' = exp_partial_join e1 e2 in let e1'' = exp_partial_join e1 e2 in
let e2'' = exp_partial_join e1' e2' in let e2'' = exp_partial_join e1' e2' in
Exp.BinOp (binop1, e1'', e2'') Exp.BinOp (binop1, e1'', e2'')
| Exp.Lvar pvar1, Exp.Lvar pvar2 -> | Exp.Lvar pvar1, Exp.Lvar pvar2 ->
if not (Pvar.equal pvar1 pvar2) then ( if not (Pvar.equal pvar1 pvar2) then (
L.d_strln "failure reason 25" ; raise Predicates.JoinFail ) L.d_strln "failure reason 25" ;
raise Predicates.JoinFail )
else e1 else e1
| Exp.Lfield (e1, f1, t1), Exp.Lfield (e2, f2, _) -> | Exp.Lfield (e1, f1, t1), Exp.Lfield (e2, f2, _) ->
if not (Fieldname.equal f1 f2) then ( if not (Fieldname.equal f1 f2) then (
L.d_strln "failure reason 26" ; raise Predicates.JoinFail ) L.d_strln "failure reason 26" ;
raise Predicates.JoinFail )
else Exp.Lfield (exp_partial_join e1 e2, f1, t1) (* should be t1 = t2 *) else Exp.Lfield (exp_partial_join e1 e2, f1, t1) (* should be t1 = t2 *)
| Exp.Lindex (e1, e1'), Exp.Lindex (e2, e2') -> | Exp.Lindex (e1, e1'), Exp.Lindex (e2, e2') ->
let e1'' = exp_partial_join e1 e2 in let e1'' = exp_partial_join e1 e2 in
@ -1100,48 +1155,66 @@ let rec exp_partial_meet (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
ident_partial_meet id1 id2 ident_partial_meet id1 id2
| Exp.Var id, Exp.Const _ -> | Exp.Var id, Exp.Const _ ->
if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e2) if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e2)
else (L.d_strln "failure reason 27" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 27" ;
raise Predicates.JoinFail )
| Exp.Const _, Exp.Var id -> | Exp.Const _, Exp.Var id ->
if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e1) if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e1)
else (L.d_strln "failure reason 28" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 28" ;
raise Predicates.JoinFail )
| Exp.Const c1, Exp.Const c2 -> | Exp.Const c1, Exp.Const c2 ->
if Const.equal c1 c2 then e1 else (L.d_strln "failure reason 29" ; raise Predicates.JoinFail) if Const.equal c1 c2 then e1
else (
L.d_strln "failure reason 29" ;
raise Predicates.JoinFail )
| Exp.Cast (t1, e1), Exp.Cast (t2, e2) -> | Exp.Cast (t1, e1), Exp.Cast (t2, e2) ->
if not (Typ.equal t1 t2) then (L.d_strln "failure reason 30" ; raise Predicates.JoinFail) if not (Typ.equal t1 t2) then (
L.d_strln "failure reason 30" ;
raise Predicates.JoinFail )
else else
let e1'' = exp_partial_meet e1 e2 in let e1'' = exp_partial_meet e1 e2 in
Exp.Cast (t1, e1'') Exp.Cast (t1, e1'')
| Exp.UnOp (unop1, e1, topt1), Exp.UnOp (unop2, e2, _) -> | Exp.UnOp (unop1, e1, topt1), Exp.UnOp (unop2, e2, _) ->
if not (Unop.equal unop1 unop2) then ( if not (Unop.equal unop1 unop2) then (
L.d_strln "failure reason 31" ; raise Predicates.JoinFail ) L.d_strln "failure reason 31" ;
raise Predicates.JoinFail )
else Exp.UnOp (unop1, exp_partial_meet e1 e2, topt1) (* should be topt1 = topt2 *) else Exp.UnOp (unop1, exp_partial_meet e1 e2, topt1) (* should be topt1 = topt2 *)
| Exp.BinOp (binop1, e1, e1'), Exp.BinOp (binop2, e2, e2') -> | Exp.BinOp (binop1, e1, e1'), Exp.BinOp (binop2, e2, e2') ->
if not (Binop.equal binop1 binop2) then ( if not (Binop.equal binop1 binop2) then (
L.d_strln "failure reason 32" ; raise Predicates.JoinFail ) L.d_strln "failure reason 32" ;
raise Predicates.JoinFail )
else else
let e1'' = exp_partial_meet e1 e2 in let e1'' = exp_partial_meet e1 e2 in
let e2'' = exp_partial_meet e1' e2' in let e2'' = exp_partial_meet e1' e2' in
Exp.BinOp (binop1, e1'', e2'') Exp.BinOp (binop1, e1'', e2'')
| Exp.Var id, Exp.Lvar _ -> | Exp.Var id, Exp.Lvar _ ->
if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e2) if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e2)
else (L.d_strln "failure reason 33" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 33" ;
raise Predicates.JoinFail )
| Exp.Lvar _, Exp.Var id -> | Exp.Lvar _, Exp.Var id ->
if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e1) if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e1)
else (L.d_strln "failure reason 34" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 34" ;
raise Predicates.JoinFail )
| Exp.Lvar pvar1, Exp.Lvar pvar2 -> | Exp.Lvar pvar1, Exp.Lvar pvar2 ->
if not (Pvar.equal pvar1 pvar2) then ( if not (Pvar.equal pvar1 pvar2) then (
L.d_strln "failure reason 35" ; raise Predicates.JoinFail ) L.d_strln "failure reason 35" ;
raise Predicates.JoinFail )
else e1 else e1
| Exp.Lfield (e1, f1, t1), Exp.Lfield (e2, f2, _) -> | Exp.Lfield (e1, f1, t1), Exp.Lfield (e2, f2, _) ->
if not (Fieldname.equal f1 f2) then ( if not (Fieldname.equal f1 f2) then (
L.d_strln "failure reason 36" ; raise Predicates.JoinFail ) L.d_strln "failure reason 36" ;
raise Predicates.JoinFail )
else Exp.Lfield (exp_partial_meet e1 e2, f1, t1) (* should be t1 = t2 *) else Exp.Lfield (exp_partial_meet e1 e2, f1, t1) (* should be t1 = t2 *)
| Exp.Lindex (e1, e1'), Exp.Lindex (e2, e2') -> | Exp.Lindex (e1, e1'), Exp.Lindex (e2, e2') ->
let e1'' = exp_partial_meet e1 e2 in let e1'' = exp_partial_meet e1 e2 in
let e2'' = exp_partial_meet e1' e2' in let e2'' = exp_partial_meet e1' e2' in
Exp.Lindex (e1'', e2'') Exp.Lindex (e1'', e2'')
| _ -> | _ ->
L.d_strln "failure reason 37" ; raise Predicates.JoinFail L.d_strln "failure reason 37" ;
raise Predicates.JoinFail
let exp_list_partial_join = List.map2_exn ~f:exp_partial_join let exp_list_partial_join = List.map2_exn ~f:exp_partial_join
@ -1159,7 +1232,8 @@ let rec strexp_partial_join mode (strexp1 : Predicates.strexp) (strexp2 : Predic
| [], _ | _, [] -> ( | [], _ | _, [] -> (
match mode with match mode with
| JoinState.Pre -> | JoinState.Pre ->
L.d_strln "failure reason 42" ; raise Predicates.JoinFail L.d_strln "failure reason 42" ;
raise Predicates.JoinFail
| JoinState.Post -> | JoinState.Post ->
Predicates.Estruct (List.rev acc, inst) ) Predicates.Estruct (List.rev acc, inst) )
| (fld1, se1) :: fld_se_list1', (fld2, se2) :: fld_se_list2' -> ( | (fld1, se1) :: fld_se_list1', (fld2, se2) :: fld_se_list2' -> (
@ -1171,7 +1245,8 @@ let rec strexp_partial_join mode (strexp1 : Predicates.strexp) (strexp2 : Predic
else else
match mode with match mode with
| JoinState.Pre -> | JoinState.Pre ->
L.d_strln "failure reason 43" ; raise Predicates.JoinFail L.d_strln "failure reason 43" ;
raise Predicates.JoinFail
| JoinState.Post -> | JoinState.Post ->
if comparison < 0 then f_fld_se_list inst mode acc fld_se_list1' fld_se_list2 if comparison < 0 then f_fld_se_list inst mode acc fld_se_list1' fld_se_list2
else if comparison > 0 then f_fld_se_list inst mode acc fld_se_list1 fld_se_list2' else if comparison > 0 then f_fld_se_list inst mode acc fld_se_list1 fld_se_list2'
@ -1185,7 +1260,8 @@ let rec strexp_partial_join mode (strexp1 : Predicates.strexp) (strexp2 : Predic
| [], _ | _, [] -> ( | [], _ | _, [] -> (
match mode with match mode with
| JoinState.Pre -> | JoinState.Pre ->
L.d_strln "failure reason 44" ; raise Predicates.JoinFail L.d_strln "failure reason 44" ;
raise Predicates.JoinFail
| JoinState.Post -> | JoinState.Post ->
Predicates.Earray (len, List.rev idx_se_list_acc, inst) ) Predicates.Earray (len, List.rev idx_se_list_acc, inst) )
| (idx1, se1) :: idx_se_list1', (idx2, se2) :: idx_se_list2' -> | (idx1, se1) :: idx_se_list1', (idx2, se2) :: idx_se_list2' ->
@ -1264,7 +1340,8 @@ let rec strexp_partial_meet (strexp1 : Predicates.strexp) (strexp2 : Predicates.
let inst = Predicates.inst_partial_meet inst1 inst2 in let inst = Predicates.inst_partial_meet inst1 inst2 in
f_idx_se_list inst len1 [] idx_se_list1 idx_se_list2 f_idx_se_list inst len1 [] idx_se_list1 idx_se_list2
| _ -> | _ ->
L.d_strln "failure reason 52" ; raise Predicates.JoinFail L.d_strln "failure reason 52" ;
raise Predicates.JoinFail
(** {2 Join and Meet for kind, hpara, hpara_dll} *) (** {2 Join and Meet for kind, hpara, hpara_dll} *)
@ -1281,28 +1358,36 @@ let hpara_partial_join tenv (hpara1 : Predicates.hpara) (hpara2 : Predicates.hpa
Predicates.hpara = Predicates.hpara =
if Match.hpara_match_with_impl tenv true hpara2 hpara1 then hpara1 if Match.hpara_match_with_impl tenv true hpara2 hpara1 then hpara1
else if Match.hpara_match_with_impl tenv true hpara1 hpara2 then hpara2 else if Match.hpara_match_with_impl tenv true hpara1 hpara2 then hpara2
else (L.d_strln "failure reason 53" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 53" ;
raise Predicates.JoinFail )
let hpara_partial_meet tenv (hpara1 : Predicates.hpara) (hpara2 : Predicates.hpara) : let hpara_partial_meet tenv (hpara1 : Predicates.hpara) (hpara2 : Predicates.hpara) :
Predicates.hpara = Predicates.hpara =
if Match.hpara_match_with_impl tenv true hpara2 hpara1 then hpara2 if Match.hpara_match_with_impl tenv true hpara2 hpara1 then hpara2
else if Match.hpara_match_with_impl tenv true hpara1 hpara2 then hpara1 else if Match.hpara_match_with_impl tenv true hpara1 hpara2 then hpara1
else (L.d_strln "failure reason 54" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 54" ;
raise Predicates.JoinFail )
let hpara_dll_partial_join tenv (hpara1 : Predicates.hpara_dll) (hpara2 : Predicates.hpara_dll) : let hpara_dll_partial_join tenv (hpara1 : Predicates.hpara_dll) (hpara2 : Predicates.hpara_dll) :
Predicates.hpara_dll = Predicates.hpara_dll =
if Match.hpara_dll_match_with_impl tenv true hpara2 hpara1 then hpara1 if Match.hpara_dll_match_with_impl tenv true hpara2 hpara1 then hpara1
else if Match.hpara_dll_match_with_impl tenv true hpara1 hpara2 then hpara2 else if Match.hpara_dll_match_with_impl tenv true hpara1 hpara2 then hpara2
else (L.d_strln "failure reason 55" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 55" ;
raise Predicates.JoinFail )
let hpara_dll_partial_meet tenv (hpara1 : Predicates.hpara_dll) (hpara2 : Predicates.hpara_dll) : let hpara_dll_partial_meet tenv (hpara1 : Predicates.hpara_dll) (hpara2 : Predicates.hpara_dll) :
Predicates.hpara_dll = Predicates.hpara_dll =
if Match.hpara_dll_match_with_impl tenv true hpara2 hpara1 then hpara2 if Match.hpara_dll_match_with_impl tenv true hpara2 hpara1 then hpara2
else if Match.hpara_dll_match_with_impl tenv true hpara1 hpara2 then hpara1 else if Match.hpara_dll_match_with_impl tenv true hpara1 hpara2 then hpara1
else (L.d_strln "failure reason 56" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 56" ;
raise Predicates.JoinFail )
(** {2 Join and Meet for hpred} *) (** {2 Join and Meet for hpred} *)
@ -1327,7 +1412,9 @@ let hpred_partial_join tenv mode (todo : Exp.t * Exp.t * Exp.t) (hpred1 : Predic
let iF', iB' = let iF', iB' =
if fwd1 && fwd2 then (e, exp_partial_join iB1 iB2) if fwd1 && fwd2 then (e, exp_partial_join iB1 iB2)
else if (not fwd1) && not fwd2 then (exp_partial_join iF1 iF2, e) else if (not fwd1) && not fwd2 then (exp_partial_join iF1 iF2, e)
else (L.d_strln "failure reason 57" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 57" ;
raise Predicates.JoinFail )
in in
let oF' = exp_partial_join oF1 oF2 in let oF' = exp_partial_join oF1 oF2 in
let oB' = exp_partial_join oB1 oB2 in let oB' = exp_partial_join oB1 oB2 in
@ -1344,7 +1431,8 @@ let hpred_partial_meet tenv (todo : Exp.t * Exp.t * Exp.t) (hpred1 : Predicates.
| Hpointsto (_, se1, te1), Hpointsto (_, se2, te2) when Exp.equal te1 te2 -> | Hpointsto (_, se1, te1), Hpointsto (_, se2, te2) when Exp.equal te1 te2 ->
Prop.mk_ptsto tenv e (strexp_partial_meet se1 se2) te1 Prop.mk_ptsto tenv e (strexp_partial_meet se1 se2) te1
| Hpointsto _, _ | _, Hpointsto _ -> | Hpointsto _, _ | _, Hpointsto _ ->
L.d_strln "failure reason 58" ; raise Predicates.JoinFail L.d_strln "failure reason 58" ;
raise Predicates.JoinFail
| Hlseg (k1, hpara1, _, next1, shared1), Hlseg (k2, hpara2, _, next2, shared2) -> | Hlseg (k1, hpara1, _, next1, shared1), Hlseg (k2, hpara2, _, next2, shared2) ->
let hpara' = hpara_partial_meet tenv hpara1 hpara2 in let hpara' = hpara_partial_meet tenv hpara1 hpara2 in
let next' = exp_partial_meet next1 next2 in let next' = exp_partial_meet next1 next2 in
@ -1358,7 +1446,9 @@ let hpred_partial_meet tenv (todo : Exp.t * Exp.t * Exp.t) (hpred1 : Predicates.
let iF', iB' = let iF', iB' =
if fwd1 && fwd2 then (e, exp_partial_meet iB1 iB2) if fwd1 && fwd2 then (e, exp_partial_meet iB1 iB2)
else if (not fwd1) && not fwd2 then (exp_partial_meet iF1 iF2, e) else if (not fwd1) && not fwd2 then (exp_partial_meet iF1 iF2, e)
else (L.d_strln "failure reason 59" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 59" ;
raise Predicates.JoinFail )
in in
let oF' = exp_partial_meet oF1 oF2 in let oF' = exp_partial_meet oF1 oF2 in
let oB' = exp_partial_meet oB1 oB2 in let oB' = exp_partial_meet oB1 oB2 in
@ -1426,7 +1516,8 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop
let lookup_and_expand side e e' = let lookup_and_expand side e e' =
match (Rename.get_others side e, side) with match (Rename.get_others side e, side) with
| None, _ -> | None, _ ->
L.d_strln "failure reason 60" ; raise Predicates.JoinFail L.d_strln "failure reason 60" ;
raise Predicates.JoinFail
| Some (e_res, e_op), Lhs -> | Some (e_res, e_op), Lhs ->
(e_res, exp_partial_join e' e_op) (e_res, exp_partial_join e' e_op)
| Some (e_res, e_op), Rhs -> | Some (e_res, e_op), Rhs ->
@ -1487,7 +1578,9 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop
'todo' describes the start point. *) 'todo' describes the start point. *)
let cut_sigma side todo (target : Prop.sigma) (other : Prop.sigma) = let cut_sigma side todo (target : Prop.sigma) (other : Prop.sigma) =
let list_is_empty l = let list_is_empty l =
if not (List.is_empty l) then (L.d_strln "failure reason 61" ; raise Predicates.JoinFail) if not (List.is_empty l) then (
L.d_strln "failure reason 61" ;
raise Predicates.JoinFail )
in in
let x = Todo.take () in let x = Todo.take () in
Todo.push todo ; Todo.push todo ;
@ -1504,7 +1597,8 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop
sigma_renaming_check_rhs target res ; sigma_renaming_check_rhs target res ;
other' other'
in in
Todo.set x ; res Todo.set x ;
res
in in
let cut_lseg side todo lseg sigma = let cut_lseg side todo lseg sigma =
match (lseg : Predicates.hpred) with match (lseg : Predicates.hpred) with
@ -1551,15 +1645,20 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop
if (not Config.nelseg) || Predicates.equal_lseg_kind k Lseg_PE then if (not Config.nelseg) || Predicates.equal_lseg_kind k Lseg_PE then
let sigma_acc' = join_list_and_non Lhs e lseg e1 e2 :: sigma_acc in let sigma_acc' = join_list_and_non Lhs e lseg e1 e2 :: sigma_acc in
sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2 sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2
else (L.d_strln "failure reason 62" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 62" ;
raise Predicates.JoinFail )
| None, Some (Predicates.Hlseg (k, _, _, _, _) as lseg) | None, Some (Predicates.Hlseg (k, _, _, _, _) as lseg)
| None, Some (Predicates.Hdllseg (k, _, _, _, _, _, _) as lseg) -> | None, Some (Predicates.Hdllseg (k, _, _, _, _, _, _) as lseg) ->
if (not Config.nelseg) || Predicates.equal_lseg_kind k Lseg_PE then if (not Config.nelseg) || Predicates.equal_lseg_kind k Lseg_PE then
let sigma_acc' = join_list_and_non Rhs e lseg e2 e1 :: sigma_acc in let sigma_acc' = join_list_and_non Rhs e lseg e2 e1 :: sigma_acc in
sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2 sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2
else (L.d_strln "failure reason 63" ; raise Predicates.JoinFail) else (
L.d_strln "failure reason 63" ;
raise Predicates.JoinFail )
| None, _ | _, None -> | None, _ | _, None ->
L.d_strln "failure reason 64" ; raise Predicates.JoinFail L.d_strln "failure reason 64" ;
raise Predicates.JoinFail
| Some hpred1, Some hpred2 when same_pred hpred1 hpred2 -> | Some hpred1, Some hpred2 when same_pred hpred1 hpred2 ->
let hpred_res1 = hpred_partial_join tenv mode todo_curr hpred1 hpred2 in let hpred_res1 = hpred_partial_join tenv mode todo_curr hpred1 hpred2 in
sigma_partial_join' tenv mode (hpred_res1 :: sigma_acc) sigma1 sigma2 sigma_partial_join' tenv mode (hpred_res1 :: sigma_acc) sigma1 sigma2
@ -1622,7 +1721,9 @@ let sigma_partial_join tenv mode (sigma1 : Prop.sigma) (sigma2 : Prop.sigma) :
SymOp.try_finally SymOp.try_finally
~f:(fun () -> ~f:(fun () ->
if Rename.check lost_little then (s1, s2, s3) if Rename.check lost_little then (s1, s2, s3)
else (L.d_strln "failed Rename.check" ; raise Predicates.JoinFail) ) else (
L.d_strln "failed Rename.check" ;
raise Predicates.JoinFail ) )
~finally:CheckJoin.final ~finally:CheckJoin.final
@ -1663,7 +1764,8 @@ let rec sigma_partial_meet' tenv (sigma_acc : Prop.sigma) (sigma1_in : Prop.sigm
let hpred' = hpred_partial_meet tenv todo_curr hpred1 hpred2 in let hpred' = hpred_partial_meet tenv todo_curr hpred1 hpred2 in
sigma_partial_meet' tenv (hpred' :: sigma_acc) sigma1 sigma2 sigma_partial_meet' tenv (hpred' :: sigma_acc) sigma1 sigma2
| Some _, Some _ -> | Some _, Some _ ->
L.d_strln "failure reason 65" ; raise Predicates.JoinFail L.d_strln "failure reason 65" ;
raise Predicates.JoinFail
with Todo.Empty -> ( with Todo.Empty -> (
match (sigma1_in, sigma2_in) with match (sigma1_in, sigma2_in) with
| [], [] -> | [], [] ->
@ -1799,20 +1901,33 @@ let pi_partial_join tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.exposed Pr
a' :: atom_list a' :: atom_list
in in
if Config.trace_join then ( if Config.trace_join then (
L.d_str "pi1: " ; Prop.d_pi pi1 ; L.d_ln () ; L.d_str "pi2: " ; Prop.d_pi pi2 ; L.d_ln () ) ; L.d_str "pi1: " ;
Prop.d_pi pi1 ;
L.d_ln () ;
L.d_str "pi2: " ;
Prop.d_pi pi2 ;
L.d_ln () ) ;
let atom_list1 = let atom_list1 =
let p2 = Prop.normalize tenv ep2 in let p2 = Prop.normalize tenv ep2 in
List.fold ~f:(handle_atom_with_widening Lhs p2 pi2) ~init:[] pi1 List.fold ~f:(handle_atom_with_widening Lhs p2 pi2) ~init:[] pi1
in in
if Config.trace_join then (L.d_str "atom_list1: " ; Prop.d_pi atom_list1 ; L.d_ln ()) ; if Config.trace_join then (
L.d_str "atom_list1: " ;
Prop.d_pi atom_list1 ;
L.d_ln () ) ;
let atom_list2 = let atom_list2 =
let p1 = Prop.normalize tenv ep1 in let p1 = Prop.normalize tenv ep1 in
List.fold ~f:(handle_atom_with_widening Rhs p1 pi1) ~init:[] pi2 List.fold ~f:(handle_atom_with_widening Rhs p1 pi1) ~init:[] pi2
in in
if Config.trace_join then (L.d_str "atom_list2: " ; Prop.d_pi atom_list2 ; L.d_ln ()) ; if Config.trace_join then (
L.d_str "atom_list2: " ;
Prop.d_pi atom_list2 ;
L.d_ln () ) ;
let atom_list_combined = IList.inter ~cmp:Predicates.compare_atom atom_list1 atom_list2 in let atom_list_combined = IList.inter ~cmp:Predicates.compare_atom atom_list1 atom_list2 in
if Config.trace_join then ( if Config.trace_join then (
L.d_str "atom_list_combined: " ; Prop.d_pi atom_list_combined ; L.d_ln () ) ; L.d_str "atom_list_combined: " ;
Prop.d_pi atom_list_combined ;
L.d_ln () ) ;
atom_list_combined atom_list_combined
@ -1862,7 +1977,9 @@ let eprop_partial_meet tenv (ep1 : 'a Prop.t) (ep2 : 'b Prop.t) : 'c Prop.t =
let f e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in let f e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in
Predicates.equal_subst sub1 sub2 && List.for_all ~f range1 Predicates.equal_subst sub1 sub2 && List.for_all ~f range1
in in
if not (sub_check ()) then (L.d_strln "sub_check() failed" ; raise Predicates.JoinFail) if not (sub_check ()) then (
L.d_strln "sub_check() failed" ;
raise Predicates.JoinFail )
else else
let todos = List.map ~f:(fun x -> (x, x, x)) es in let todos = List.map ~f:(fun x -> (x, x, x)) es in
List.iter ~f:Todo.push todos ; List.iter ~f:Todo.push todos ;
@ -1882,7 +1999,10 @@ let prop_partial_meet tenv p1 p2 =
try try
SymOp.try_finally SymOp.try_finally
~f:(fun () -> Some (eprop_partial_meet tenv p1 p2)) ~f:(fun () -> Some (eprop_partial_meet tenv p1 p2))
~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ()) ~finally:(fun () ->
Rename.final () ;
FreshVarExp.final () ;
Todo.final () )
with Predicates.JoinFail -> None with Predicates.JoinFail -> None
@ -1946,7 +2066,8 @@ let eprop_partial_join' tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.expose
in in
p_sub_sigma_pi p_sub_sigma_pi
| _ -> | _ ->
L.d_strln "leftovers not empty" ; raise Predicates.JoinFail L.d_strln "leftovers not empty" ;
raise Predicates.JoinFail
let footprint_partial_join' tenv (p1 : Prop.normal Prop.t) (p2 : Prop.normal Prop.t) : let footprint_partial_join' tenv (p1 : Prop.normal Prop.t) (p2 : Prop.normal Prop.t) :
@ -1966,7 +2087,9 @@ let footprint_partial_join' tenv (p1 : Prop.normal Prop.t) (p2 : Prop.normal Pro
let f a = let f a =
Predicates.hpred_free_vars a |> Sequence.exists ~f:(fun a -> not (Ident.is_footprint a)) Predicates.hpred_free_vars a |> Sequence.exists ~f:(fun a -> not (Ident.is_footprint a))
in in
if List.exists ~f sigma_fp0 then (L.d_strln "failure reason 66" ; raise Predicates.JoinFail) ; if List.exists ~f sigma_fp0 then (
L.d_strln "failure reason 66" ;
raise Predicates.JoinFail ) ;
sigma_fp0 sigma_fp0
in in
let ep1' = Prop.set p1 ~pi_fp ~sigma_fp in let ep1' = Prop.set p1 ~pi_fp ~sigma_fp in
@ -1996,7 +2119,10 @@ let prop_partial_join ({InterproceduralAnalysis.tenv; _} as analysis_data) mode
let res = eprop_partial_join' tenv mode (Prop.expose p1') (Prop.expose p2') in let res = eprop_partial_join' tenv mode (Prop.expose p1') (Prop.expose p2') in
if !BiabductionConfig.footprint then JoinState.set_footprint false ; if !BiabductionConfig.footprint then JoinState.set_footprint false ;
Some res ) Some res )
~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ()) ~finally:(fun () ->
Rename.final () ;
FreshVarExp.final () ;
Todo.final () )
with Predicates.JoinFail -> None ) with Predicates.JoinFail -> None )
| Some _ -> | Some _ ->
res_by_implication_only res_by_implication_only
@ -2009,7 +2135,10 @@ let eprop_partial_join tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.exposed
Todo.init () ; Todo.init () ;
SymOp.try_finally SymOp.try_finally
~f:(fun () -> eprop_partial_join' tenv mode ep1 ep2) ~f:(fun () -> eprop_partial_join' tenv mode ep1 ep2)
~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ()) ~finally:(fun () ->
Rename.final () ;
FreshVarExp.final () ;
Todo.final () )
(** {2 Join and Meet for Propset} *) (** {2 Join and Meet for Propset} *)

7
infer/src/biabduction/DotBiabduction.ml
Unescape View File

@ -115,7 +115,9 @@ let strip_special_chars b =
let replace st c c' = let replace st c c' =
if Bytes.contains st c then ( if Bytes.contains st c then (
let idx = String.index_exn (Bytes.to_string st) c in let idx = String.index_exn (Bytes.to_string st) c in
try Bytes.set st idx c' ; st try
Bytes.set st idx c' ;
st
with Invalid_argument _ -> with Invalid_argument _ ->
L.internal_error "@\n@\nstrip_special_chars: Invalid argument!@\n@." ; L.internal_error "@\n@\nstrip_special_chars: Invalid argument!@\n@." ;
assert false ) assert false )
@ -423,7 +425,8 @@ let compute_fields_struct sigma =
| [] -> | [] ->
() ()
| Predicates.Hpointsto (_, se, _) :: s' -> | Predicates.Hpointsto (_, se, _) :: s' ->
do_strexp se false ; fs s' do_strexp se false ;
fs s'
| _ :: s' -> | _ :: s' ->
fs s' fs s'
in in

47
infer/src/biabduction/Paths.ml
Unescape View File

@ -172,13 +172,19 @@ end = struct
| Pstart (_, stats) -> | Pstart (_, stats) ->
if not (stats_is_dummy stats) then set_dummy_stats stats if not (stats_is_dummy stats) then set_dummy_stats stats
| Pnode (_, _, _, path, stats, _) | Pcall (path, _, ExecSkipped _, stats) -> | Pnode (_, _, _, path, stats, _) | Pcall (path, _, ExecSkipped _, stats) ->
if not (stats_is_dummy stats) then (reset_stats path ; set_dummy_stats stats) if not (stats_is_dummy stats) then (
reset_stats path ;
set_dummy_stats stats )
| Pjoin (path1, path2, stats) -> | Pjoin (path1, path2, stats) ->
if not (stats_is_dummy stats) then ( if not (stats_is_dummy stats) then (
reset_stats path1 ; reset_stats path2 ; set_dummy_stats stats ) reset_stats path1 ;
reset_stats path2 ;
set_dummy_stats stats )
| Pcall (path1, _, ExecCompleted path2, stats) -> | Pcall (path1, _, ExecCompleted path2, stats) ->
if not (stats_is_dummy stats) then ( if not (stats_is_dummy stats) then (
reset_stats path1 ; reset_stats path2 ; set_dummy_stats stats ) reset_stats path1 ;
reset_stats path2 ;
set_dummy_stats stats )
(** Iterate [f] over the path and compute the stats, assuming the invariant: all the stats are (** Iterate [f] over the path and compute the stats, assuming the invariant: all the stats are
@ -218,7 +224,8 @@ end = struct
let stats2 = let stats2 =
match do_calls with match do_calls with
| true -> | true ->
compute_stats do_calls f path2 ; get_stats path2 compute_stats do_calls f path2 ;
get_stats path2
| false -> | false ->
{max_length= 0; linear_num= 0.0} {max_length= 0; linear_num= 0.0}
in in
@ -228,13 +235,17 @@ end = struct
(* already found in call, no need to search before the call *) (* already found in call, no need to search before the call *)
else f else f
in in
compute_stats do_calls f' path1 ; get_stats path1 compute_stats do_calls f' path1 ;
get_stats path1
in in
stats.max_length <- stats1.max_length + stats2.max_length ; stats.max_length <- stats1.max_length + stats2.max_length ;
stats.linear_num <- stats1.linear_num ) stats.linear_num <- stats1.linear_num )
| Pcall (path, _, ExecSkipped _, stats) -> | Pcall (path, _, ExecSkipped _, stats) ->
if stats_is_dummy stats then ( if stats_is_dummy stats then (
let stats1 = compute_stats do_calls f path ; get_stats path in let stats1 =
compute_stats do_calls f path ;
get_stats path
in
stats.max_length <- stats1.max_length ; stats.max_length <- stats1.max_length ;
stats.linear_num <- stats1.linear_num ) stats.linear_num <- stats1.linear_num )
end end
@ -295,7 +306,8 @@ end = struct
doit (level + 1) session p2 next_exn_opt doit (level + 1) session p2 next_exn_opt
| Pcall (p, _, ExecSkipped _, _) -> | Pcall (p, _, ExecSkipped _, _) ->
let next_exn_opt = None in let next_exn_opt = None in
doit level session p next_exn_opt ; f level path session prev_exn_opt doit level session p next_exn_opt ;
f level path session prev_exn_opt
in in
Invariant.compute_stats true filter path ; Invariant.compute_stats true filter path ;
doit 0 0 path None ; doit 0 0 path None ;
@ -407,7 +419,10 @@ end = struct
add_delayed p add_delayed p
| Pjoin (p1, p2, _) | Pcall (p1, _, ExecCompleted p2, _) -> | Pjoin (p1, p2, _) | Pcall (p1, _, ExecCompleted p2, _) ->
(* delay paths occurring in a join *) (* delay paths occurring in a join *)
add_delayed p1 ; add_delayed p2 ; add_path p1 ; add_path p2 add_delayed p1 ;
add_delayed p2 ;
add_path p1 ;
add_path p2
in in
let rec doit n fmt path = let rec doit n fmt path =
try try
@ -430,9 +445,12 @@ end = struct
let print_delayed () = let print_delayed () =
if not (PathMap.is_empty !delayed) then ( if not (PathMap.is_empty !delayed) then (
let f path num = F.fprintf fmt "P%d = %a@\n" num (doit 1) path in let f path num = F.fprintf fmt "P%d = %a@\n" num (doit 1) path in
F.fprintf fmt "where@\n" ; PathMap.iter f !delayed ) F.fprintf fmt "where@\n" ;
PathMap.iter f !delayed )
in in
add_delayed path ; doit 0 fmt path ; print_delayed () add_delayed path ;
doit 0 fmt path ;
print_delayed ()
let create_loc_trace path pos_opt : Errlog.loc_trace = let create_loc_trace path pos_opt : Errlog.loc_trace =
@ -606,7 +624,8 @@ end = struct
let elements ps = let elements ps =
let plist = ref [] in let plist = ref [] in
let f prop path = plist := (prop, path) :: !plist in let f prop path = plist := (prop, path) :: !plist in
PropMap.iter f ps ; !plist PropMap.iter f ps ;
!plist
let to_proplist ps = List.map ~f:fst (elements ps) let to_proplist ps = List.map ~f:fst (elements ps)
@ -656,7 +675,8 @@ end = struct
then res := PropMap.remove p !res then res := PropMap.remove p !res
with Caml.Not_found -> res := PropMap.remove p !res with Caml.Not_found -> res := PropMap.remove p !res
in in
PropMap.iter rem ps2 ; !res PropMap.iter rem ps2 ;
!res
let is_empty = PropMap.is_empty let is_empty = PropMap.is_empty
@ -670,7 +690,8 @@ end = struct
let do_elem prop path = let do_elem prop path =
match f prop with None -> () | Some prop' -> res := add_renamed_prop prop' path !res match f prop with None -> () | Some prop' -> res := add_renamed_prop prop' path !res
in in
iter do_elem ps ; !res iter do_elem ps ;
!res
let map f ps = map_option (fun p -> Some (f p)) ps let map f ps = map_option (fun p -> Some (f p)) ps

5
infer/src/biabduction/Predicates.ml
Unescape View File

@ -1115,7 +1115,10 @@ let create_sharing_env () = {exph= Exp.Hash.create 3; hpredh= HpredInstHash.crea
(** Return a canonical representation of the exp *) (** Return a canonical representation of the exp *)
let exp_compact sh e = let exp_compact sh e =
try Exp.Hash.find sh.exph e with Caml.Not_found -> Exp.Hash.add sh.exph e e ; e try Exp.Hash.find sh.exph e
with Caml.Not_found ->
Exp.Hash.add sh.exph e e ;
e
let rec sexp_compact sh se = let rec sexp_compact sh se =

10
infer/src/biabduction/Prop.ml
Unescape View File

@ -206,7 +206,9 @@ let d_pi_sigma pi sigma =
let d_separator () = let d_separator () =
if (not (List.is_empty pi)) && not (List.is_empty sigma) then L.d_strln " *" if (not (List.is_empty pi)) && not (List.is_empty sigma) then L.d_strln " *"
in in
d_pi pi ; d_separator () ; d_sigma sigma d_pi pi ;
d_separator () ;
d_sigma sigma
let pi_of_subst sub = let pi_of_subst sub =
@ -539,7 +541,8 @@ let sigma_get_unsigned_exps sigma =
| _ -> | _ ->
() ()
in in
List.iter ~f:do_hpred sigma ; !uexps List.iter ~f:do_hpred sigma ;
!uexps
(** Collapse consecutive indices that should be added. For instance, this function reduces (** Collapse consecutive indices that should be added. For instance, this function reduces
@ -1952,7 +1955,8 @@ let sigma_dfs_sort tenv sigma =
in in
init () ; init () ;
let sigma' = handle_sigma [] sigma in let sigma' = handle_sigma [] sigma in
final () ; sigma' final () ;
sigma'
let dfs_sort tenv p : sorted t = let dfs_sort tenv p : sorted t =

73
infer/src/biabduction/Prover.ml
Unescape View File

@ -1044,7 +1044,12 @@ exception MISSING_EXC of string
type check = Bounds_check | Class_cast_check of Exp.t * Exp.t * Exp.t type check = Bounds_check | Class_cast_check of Exp.t * Exp.t * Exp.t
let d_typings typings = let d_typings typings =
let d_elem (exp, texp) = Exp.d_exp exp ; L.d_str ": " ; Exp.d_texp_full texp ; L.d_str " " in let d_elem (exp, texp) =
Exp.d_exp exp ;
L.d_str ": " ;
Exp.d_texp_full texp ;
L.d_str " "
in
List.iter ~f:d_elem typings List.iter ~f:d_elem typings
@ -1187,9 +1192,16 @@ end = struct
Prop.d_sub sub ; Prop.d_sub sub ;
L.d_decrease_indent () ; L.d_decrease_indent () ;
if (not (List.is_empty !missing_pi)) && not (List.is_empty !missing_sigma) then ( if (not (List.is_empty !missing_pi)) && not (List.is_empty !missing_sigma) then (
L.d_ln () ; Prop.d_pi !missing_pi ; L.d_strln "*" ; Prop.d_sigma !missing_sigma ) L.d_ln () ;
else if not (List.is_empty !missing_pi) then (L.d_ln () ; Prop.d_pi !missing_pi) Prop.d_pi !missing_pi ;
else if not (List.is_empty !missing_sigma) then (L.d_ln () ; Prop.d_sigma !missing_sigma) ; L.d_strln "*" ;
Prop.d_sigma !missing_sigma )
else if not (List.is_empty !missing_pi) then (
L.d_ln () ;
Prop.d_pi !missing_pi )
else if not (List.is_empty !missing_sigma) then (
L.d_ln () ;
Prop.d_sigma !missing_sigma ) ;
if not (List.is_empty !missing_fld) then ( if not (List.is_empty !missing_fld) then (
L.d_ln () ; L.d_ln () ;
L.d_strln "MISSING FLD:" ; L.d_strln "MISSING FLD:" ;
@ -1212,7 +1224,11 @@ end = struct
|| (not (List.is_empty !missing_fld)) || (not (List.is_empty !missing_fld))
|| (not (List.is_empty !missing_typ)) || (not (List.is_empty !missing_typ))
|| not (Predicates.is_sub_empty sub) || not (Predicates.is_sub_empty sub)
then ( L.d_ln () ; L.d_str "[" ; d_missing_ sub ; L.d_str "]" ) then (
L.d_ln () ;
L.d_str "[" ;
d_missing_ sub ;
L.d_str "]" )
let d_frame_fld () = let d_frame_fld () =
@ -1261,15 +1277,24 @@ end = struct
| EXC_FALSE -> | EXC_FALSE ->
() ()
| EXC_FALSE_HPRED hpred -> | EXC_FALSE_HPRED hpred ->
L.d_str " on " ; Predicates.d_hpred hpred L.d_str " on " ;
Predicates.d_hpred hpred
| EXC_FALSE_EXPS (e1, e2) -> | EXC_FALSE_EXPS (e1, e2) ->
L.d_str " on " ; Exp.d_exp e1 ; L.d_str "," ; Exp.d_exp e2 L.d_str " on " ;
Exp.d_exp e1 ;
L.d_str "," ;
Exp.d_exp e2
| EXC_FALSE_SEXPS (se1, se2) -> | EXC_FALSE_SEXPS (se1, se2) ->
L.d_str " on " ; Predicates.d_sexp se1 ; L.d_str "," ; Predicates.d_sexp se2 L.d_str " on " ;
Predicates.d_sexp se1 ;
L.d_str "," ;
Predicates.d_sexp se2
| EXC_FALSE_ATOM a -> | EXC_FALSE_ATOM a ->
L.d_str " on " ; Predicates.d_atom a L.d_str " on " ;
Predicates.d_atom a
| EXC_FALSE_SIGMA sigma -> | EXC_FALSE_SIGMA sigma ->
L.d_str " on " ; Prop.d_sigma sigma L.d_str " on " ;
Prop.d_sigma sigma
in in
L.d_ln () ; L.d_ln () ;
L.d_strln "$$$$$$$ Implication" ; L.d_strln "$$$$$$$ Implication" ;
@ -1995,7 +2020,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
(Prop.prop_iter_to_prop tenv iter1'') (Prop.prop_iter_to_prop tenv iter1'')
sigma2 hpred2 ) sigma2 hpred2 )
in in
L.d_decrease_indent () ; res L.d_decrease_indent () ;
res
| Predicates.Hdllseg (Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _ | Predicates.Hdllseg (Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
when Exp.equal (Predicates.exp_sub (fst subs) iF1) e2 -> when Exp.equal (Predicates.exp_sub (fst subs) iF1) e2 ->
(* Unroll dllseg forward *) (* Unroll dllseg forward *)
@ -2012,7 +2038,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
(Prop.prop_iter_to_prop tenv iter1'') (Prop.prop_iter_to_prop tenv iter1'')
sigma2 hpred2 ) sigma2 hpred2 )
in in
L.d_decrease_indent () ; res L.d_decrease_indent () ;
res
| Predicates.Hdllseg (Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _ | Predicates.Hdllseg (Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
when Exp.equal (Predicates.exp_sub (fst subs) iB1) e2 -> when Exp.equal (Predicates.exp_sub (fst subs) iB1) e2 ->
(* Unroll dllseg backward *) (* Unroll dllseg backward *)
@ -2029,7 +2056,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
(Prop.prop_iter_to_prop tenv iter1'') (Prop.prop_iter_to_prop tenv iter1'')
sigma2 hpred2 ) sigma2 hpred2 )
in in
L.d_decrease_indent () ; res L.d_decrease_indent () ;
res
| _ -> | _ ->
assert false ) ) ) assert false ) ) )
| Predicates.Hlseg (k, para2, e2_, f2_, elist2_) -> ( | Predicates.Hlseg (k, para2, e2_, f2_, elist2_) -> (
@ -2063,7 +2091,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
sigma_imply tenv calc_index_frame false subs prop1 para_inst2 ) sigma_imply tenv calc_index_frame false subs prop1 para_inst2 )
in in
(* calc_missing is false as we're checking an instantiation of the original list *) (* calc_missing is false as we're checking an instantiation of the original list *)
L.d_decrease_indent () ; res L.d_decrease_indent () ;
res
| Some iter1' -> ( | Some iter1' -> (
let elist2 = List.map ~f:(fun e -> Predicates.exp_sub (snd subs) e) elist2_ in let elist2 = List.map ~f:(fun e -> Predicates.exp_sub (snd subs) e) elist2_ in
(* force instantiation of existentials *) (* force instantiation of existentials *)
@ -2093,7 +2122,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
let _, para_inst3 = Predicates.hpara_instantiate para2 e2_ f2_ elist2 in let _, para_inst3 = Predicates.hpara_instantiate para2 e2_ f2_ elist2 in
sigma_imply tenv calc_index_frame calc_missing subs prop1 para_inst3 ) sigma_imply tenv calc_index_frame calc_missing subs prop1 para_inst3 )
in in
L.d_decrease_indent () ; res L.d_decrease_indent () ;
res
| Predicates.Hdllseg _ -> | Predicates.Hdllseg _ ->
assert false ) ) ) assert false ) ) )
| Predicates.Hdllseg (Lseg_PE, _, _, _, _, _, _) -> | Predicates.Hdllseg (Lseg_PE, _, _, _, _, _, _) ->
@ -2142,7 +2172,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
sigma_imply tenv calc_index_frame false subs prop1 para_inst2 ) sigma_imply tenv calc_index_frame false subs prop1 para_inst2 )
in in
(* calc_missing is false as we're checking an instantiation of the original list *) (* calc_missing is false as we're checking an instantiation of the original list *)
L.d_decrease_indent () ; res L.d_decrease_indent () ;
res
| Some iter1' -> | Some iter1' ->
(* Only consider implications between identical listsegs for now *) (* Only consider implications between identical listsegs for now *)
let elist2 = List.map ~f:(fun e -> Predicates.exp_sub (snd subs) e) elist2 in let elist2 = List.map ~f:(fun e -> Predicates.exp_sub (snd subs) e) elist2 in
@ -2254,7 +2285,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
decrease_indent_when_exception (fun () -> decrease_indent_when_exception (fun () ->
hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2' ) hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2' )
in in
L.d_decrease_indent () ; res L.d_decrease_indent () ;
res
with IMPL_EXC _ when calc_missing -> ( with IMPL_EXC _ when calc_missing -> (
match is_constant_string_class subs hpred2' with match is_constant_string_class subs hpred2' with
| Some (s, is_string) -> | Some (s, is_string) ->
@ -2287,7 +2319,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
decrease_indent_when_exception (fun () -> decrease_indent_when_exception (fun () ->
sigma_imply tenv calc_index_frame calc_missing subs' prop1' sigma2' ) sigma_imply tenv calc_index_frame calc_missing subs' prop1' sigma2' )
in in
L.d_decrease_indent () ; res L.d_decrease_indent () ;
res
in in
match hpred2 with match hpred2 with
| Predicates.Hpointsto (e2_, se2, t) -> | Predicates.Hpointsto (e2_, se2, t) ->
@ -2433,7 +2466,9 @@ let check_implication_base {InterproceduralAnalysis.proc_desc; err_log; tenv} ch
L.d_decrease_indent () ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
if not (List.is_empty pi2_bcheck) then ( if not (List.is_empty pi2_bcheck) then (
L.d_str "pi2 bounds checks: " ; Prop.d_pi pi2_bcheck ; L.d_ln () ) ; L.d_str "pi2 bounds checks: " ;
Prop.d_pi pi2_bcheck ;
L.d_ln () ) ;
L.d_strln "returns" ; L.d_strln "returns" ;
L.d_strln "sub1:" ; L.d_strln "sub1:" ;
L.d_increase_indent () ; L.d_increase_indent () ;

20
infer/src/biabduction/Rearrange.ml
Unescape View File

@ -69,7 +69,11 @@ let check_bad_index {InterproceduralAnalysis.proc_desc; err_log; tenv} pname p l
(** Perform bounds checking *) (** Perform bounds checking *)
let bounds_check analysis_data pname prop len e = let bounds_check analysis_data pname prop len e =
if Config.trace_rearrange then ( if Config.trace_rearrange then (
L.d_str "Bounds check index:" ; Exp.d_exp e ; L.d_str " len: " ; Exp.d_exp len ; L.d_ln () ) ; L.d_str "Bounds check index:" ;
Exp.d_exp e ;
L.d_str " len: " ;
Exp.d_exp len ;
L.d_ln () ) ;
check_bad_index analysis_data pname prop len e check_bad_index analysis_data pname prop len e
@ -86,7 +90,10 @@ let rec create_struct_values analysis_data pname tenv orig_prop footprint_part k
Predicates.d_offset_list off ; Predicates.d_offset_list off ;
L.d_ln () ; L.d_ln () ;
L.d_ln () ) ; L.d_ln () ) ;
let new_id () = incr max_stamp ; Ident.create kind !max_stamp in let new_id () =
incr max_stamp ;
Ident.create kind !max_stamp
in
let res = let res =
let fail t off pos = let fail t off pos =
L.d_str "create_struct_values type:" ; L.d_str "create_struct_values type:" ;
@ -190,7 +197,10 @@ let rec create_struct_values analysis_data pname tenv orig_prop footprint_part k
function. *) function. *)
let rec strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp se let rec strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp se
(typ : Typ.t) (off : Predicates.offset list) inst = (typ : Typ.t) (off : Predicates.offset list) inst =
let new_id () = incr max_stamp ; Ident.create kind !max_stamp in let new_id () =
incr max_stamp ;
Ident.create kind !max_stamp
in
match (off, se, typ.desc) with match (off, se, typ.desc) with
| [], Predicates.Eexp _, _ | [], Predicates.Estruct _, _ -> | [], Predicates.Eexp _, _ | [], Predicates.Estruct _, _ ->
[([], se, typ)] [([], se, typ)]
@ -1007,7 +1017,9 @@ let check_type_size {InterproceduralAnalysis.proc_desc; err_log; tenv} pname pro
BiabductionReporting.log_issue_deprecated_using_state proc_desc err_log Exceptions.Warning BiabductionReporting.log_issue_deprecated_using_state proc_desc err_log Exceptions.Warning
exn exn
| None -> | None ->
L.d_str "texp: " ; Exp.d_texp_full texp ; L.d_ln () L.d_str "texp: " ;
Exp.d_texp_full texp ;
L.d_ln ()
(** Exposes lexp |->- from iter. In case that it is not possible to * expose lexp |->-, this (** Exposes lexp |->- from iter. In case that it is not possible to * expose lexp |->-, this

3
infer/src/biabduction/RetainCyclesType.ml
Unescape View File

@ -210,4 +210,5 @@ let pp_dotty fmt cycle =
let write_dotty_to_file fname cycle = let write_dotty_to_file fname cycle =
let chan = Out_channel.create fname in let chan = Out_channel.create fname in
let fmt = Format.formatter_of_out_channel chan in let fmt = Format.formatter_of_out_channel chan in
pp_dotty fmt cycle ; Out_channel.close chan pp_dotty fmt cycle ;
Out_channel.close chan

5
infer/src/biabduction/State.ml
Unescape View File

@ -85,7 +85,10 @@ let instrs_normalize instrs =
in in
let subst = let subst =
let count = ref Int.min_value in let count = ref Int.min_value in
let gensym id = incr count ; Ident.set_stamp id !count in let gensym id =
incr count ;
Ident.set_stamp id !count
in
Predicates.subst_of_list (List.rev_map ~f:(fun id -> (id, Exp.Var (gensym id))) bound_ids) Predicates.subst_of_list (List.rev_map ~f:(fun id -> (id, Exp.Var (gensym id))) bound_ids)
in in
let subst_and_add acc instr = Predicates.instr_sub subst instr :: acc in let subst_and_add acc instr = Predicates.instr_sub subst instr :: acc in

3
infer/src/biabduction/SymExec.ml
Unescape View File

@ -324,7 +324,8 @@ and prune_inter tenv ~positive condition1 condition2 prop =
let res = ref Propset.empty in let res = ref Propset.empty in
let pset1 = prune tenv ~positive condition1 prop in let pset1 = prune tenv ~positive condition1 prop in
let do_p p = res := Propset.union (prune tenv ~positive condition2 p) !res in let do_p p = res := Propset.union (prune tenv ~positive condition2 p) !res in
Propset.iter do_p pset1 ; !res Propset.iter do_p pset1 ;
!res
and prune_union tenv ~positive condition1 condition2 prop = and prune_union tenv ~positive condition1 condition2 prop =

16
infer/src/biabduction/Tabulation.ml
Unescape View File

@ -806,7 +806,9 @@ let combine ({InterproceduralAnalysis.proc_desc= caller_pdesc; tenv; _} as analy
Prop.d_sigma split.frame_fld ; Prop.d_sigma split.frame_fld ;
L.d_ln () ; L.d_ln () ;
if not (List.is_empty split.frame_typ) then ( if not (List.is_empty split.frame_typ) then (
L.d_strln "Frame typ:" ; Prover.d_typings split.frame_typ ; L.d_ln () ) ; L.d_strln "Frame typ:" ;
Prover.d_typings split.frame_typ ;
L.d_ln () ) ;
L.d_strln "Missing fld:" ; L.d_strln "Missing fld:" ;
Prop.d_sigma split.missing_fld ; Prop.d_sigma split.missing_fld ;
L.d_ln () ; L.d_ln () ;
@ -926,7 +928,8 @@ let mk_actual_precondition tenv prop actual_params formal_params =
^ string_of_int (List.length formal_params) ^ string_of_int (List.length formal_params)
^ ")" ^ ")"
in in
L.d_warning str ; L.d_ln () ) ; L.d_warning str ;
L.d_ln () ) ;
[] []
| _ :: _, [] -> | _ :: _, [] ->
raise (Exceptions.Wrong_argument_number __POS__) raise (Exceptions.Wrong_argument_number __POS__)
@ -1249,7 +1252,11 @@ let exe_call_postprocess tenv ret_id callee_pname callee_attrs loc results =
let deref_errors = let deref_errors =
List.filter ~f:(function Dereference_error _ -> true | _ -> false) invalid_res List.filter ~f:(function Dereference_error _ -> true | _ -> false) invalid_res
in in
let print_pi pi = L.d_str "pi: " ; Prop.d_pi pi ; L.d_ln () in let print_pi pi =
L.d_str "pi: " ;
Prop.d_pi pi ;
L.d_ln ()
in
let call_desc kind_opt = Localise.desc_precondition_not_met kind_opt callee_pname loc in let call_desc kind_opt = Localise.desc_precondition_not_met kind_opt callee_pname loc in
let res_with_path_idents = let res_with_path_idents =
if !BiabductionConfig.footprint then if !BiabductionConfig.footprint then
@ -1325,7 +1332,8 @@ let exe_call_postprocess tenv ret_id callee_pname callee_attrs loc results =
in in
State.add_diverging_states (Paths.PathSet.from_renamed_list incons_res) State.add_diverging_states (Paths.PathSet.from_renamed_list incons_res)
in in
save_diverging_states () ; vr.vr_cons_res save_diverging_states () ;
vr.vr_cons_res
in in
List.map List.map
~f:(fun (p, path) -> (prop_pure_to_footprint tenv p, path)) ~f:(fun (p, path) -> (prop_pure_to_footprint tenv p, path))

9
infer/src/biabduction/Timeout.ml
Unescape View File

@ -91,11 +91,16 @@ let () =
ignore (Gc.create_alarm SymOp.check_wallclock_alarm) ignore (Gc.create_alarm SymOp.check_wallclock_alarm)
let unwind () = unset_alarm () ; SymOp.unset_alarm () ; GlobalState.pop () let unwind () =
unset_alarm () ;
SymOp.unset_alarm () ;
GlobalState.pop ()
let suspend_existing_timeout ~keep_symop_total = let suspend_existing_timeout ~keep_symop_total =
let current_status = get_current_status ~keep_symop_total in let current_status = get_current_status ~keep_symop_total in
unset_alarm () ; GlobalState.push current_status unset_alarm () ;
GlobalState.push current_status
let resume_previous_timeout () = let resume_previous_timeout () =

65
infer/src/biabduction/errdesc.ml
Unescape View File

@ -165,7 +165,10 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
let seen = Exp.Set.add e seen_ in let seen = Exp.Set.add e seen_ in
match Prop.exp_normalize_noabs tenv Predicates.sub_empty e with match Prop.exp_normalize_noabs tenv Predicates.sub_empty e with
| Exp.Const c -> | Exp.Const c ->
if verbose then (L.d_str "exp_lv_dexp: constant " ; Exp.d_exp e ; L.d_ln ()) ; if verbose then (
L.d_str "exp_lv_dexp: constant " ;
Exp.d_exp e ;
L.d_ln () ) ;
Some (DExp.Dderef (DExp.Dconst c)) Some (DExp.Dderef (DExp.Dconst c))
| Exp.BinOp (Binop.PlusPI, e1, e2) -> ( | Exp.BinOp (Binop.PlusPI, e1, e2) -> (
if verbose then ( if verbose then (
@ -225,7 +228,9 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
Some (DExp.Darrow (de, f)) ) Some (DExp.Darrow (de, f)) )
| Exp.Lfield (e1, f, _) -> ( | Exp.Lfield (e1, f, _) -> (
if verbose then ( if verbose then (
L.d_str "exp_lv_dexp: Lfield " ; Exp.d_exp e1 ; L.d_printfln " %a" Fieldname.pp f ) ; L.d_str "exp_lv_dexp: Lfield " ;
Exp.d_exp e1 ;
L.d_printfln " %a" Fieldname.pp f ) ;
match exp_lv_dexp_ tenv seen node e1 with match exp_lv_dexp_ tenv seen node e1 with
| None -> | None ->
None None
@ -233,7 +238,11 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
Some (DExp.Ddot (de, f)) ) Some (DExp.Ddot (de, f)) )
| Exp.Lindex (e1, e2) -> ( | Exp.Lindex (e1, e2) -> (
if verbose then ( if verbose then (
L.d_str "exp_lv_dexp: Lindex " ; Exp.d_exp e1 ; L.d_str " " ; Exp.d_exp e2 ; L.d_ln () ) ; L.d_str "exp_lv_dexp: Lindex " ;
Exp.d_exp e1 ;
L.d_str " " ;
Exp.d_exp e2 ;
L.d_ln () ) ;
match (exp_lv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with match (exp_lv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with
| None, _ -> | None, _ ->
None None
@ -261,7 +270,10 @@ and exp_rv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
let seen = Exp.Set.add e seen_ in let seen = Exp.Set.add e seen_ in
match e with match e with
| Exp.Const c -> | Exp.Const c ->
if verbose then (L.d_str "exp_rv_dexp: constant " ; Exp.d_exp e ; L.d_ln ()) ; if verbose then (
L.d_str "exp_rv_dexp: constant " ;
Exp.d_exp e ;
L.d_ln () ) ;
Some (DExp.Dconst c) Some (DExp.Dconst c)
| Exp.Lvar pv -> | Exp.Lvar pv ->
if verbose then ( if verbose then (
@ -279,7 +291,9 @@ and exp_rv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
find_normal_variable_load_ tenv seen node id find_normal_variable_load_ tenv seen node id
| Exp.Lfield (e1, f, _) -> ( | Exp.Lfield (e1, f, _) -> (
if verbose then ( if verbose then (
L.d_str "exp_rv_dexp: Lfield " ; Exp.d_exp e1 ; L.d_printfln " %a" Fieldname.pp f ) ; L.d_str "exp_rv_dexp: Lfield " ;
Exp.d_exp e1 ;
L.d_printfln " %a" Fieldname.pp f ) ;
match exp_rv_dexp_ tenv seen node e1 with match exp_rv_dexp_ tenv seen node e1 with
| None -> | None ->
None None
@ -287,31 +301,47 @@ and exp_rv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
Some (DExp.Ddot (de, f)) ) Some (DExp.Ddot (de, f)) )
| Exp.Lindex (e1, e2) -> ( | Exp.Lindex (e1, e2) -> (
if verbose then ( if verbose then (
L.d_str "exp_rv_dexp: Lindex " ; Exp.d_exp e1 ; L.d_str " " ; Exp.d_exp e2 ; L.d_ln () ) ; L.d_str "exp_rv_dexp: Lindex " ;
Exp.d_exp e1 ;
L.d_str " " ;
Exp.d_exp e2 ;
L.d_ln () ) ;
match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with
| None, _ | _, None -> | None, _ | _, None ->
None None
| Some de1, Some de2 -> | Some de1, Some de2 ->
Some (DExp.Darray (de1, 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 " ; Exp.d_exp e ; L.d_ln ()) ; if verbose then (
L.d_str "exp_rv_dexp: BinOp " ;
Exp.d_exp e ;
L.d_ln () ) ;
match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with
| None, _ | _, None -> | None, _ | _, None ->
None None
| Some de1, Some de2 -> | Some de1, Some de2 ->
Some (DExp.Dbinop (op, de1, 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 " ; Exp.d_exp e ; L.d_ln ()) ; if verbose then (
L.d_str "exp_rv_dexp: UnOp " ;
Exp.d_exp e ;
L.d_ln () ) ;
match exp_rv_dexp_ tenv seen node e1 with match exp_rv_dexp_ tenv seen node e1 with
| None -> | None ->
None None
| Some de1 -> | Some de1 ->
Some (DExp.Dunop (op, de1)) ) Some (DExp.Dunop (op, de1)) )
| Exp.Cast (_, e1) -> | Exp.Cast (_, e1) ->
if verbose then (L.d_str "exp_rv_dexp: Cast " ; Exp.d_exp e ; L.d_ln ()) ; if verbose then (
L.d_str "exp_rv_dexp: Cast " ;
Exp.d_exp e ;
L.d_ln () ) ;
exp_rv_dexp_ tenv seen node e1 exp_rv_dexp_ tenv seen node e1
| Exp.Sizeof {typ; dynamic_length; subtype} -> | Exp.Sizeof {typ; dynamic_length; subtype} ->
if verbose then (L.d_str "exp_rv_dexp: type " ; Exp.d_exp e ; L.d_ln ()) ; if verbose then (
L.d_str "exp_rv_dexp: type " ;
Exp.d_exp e ;
L.d_ln () ) ;
Some Some
(DExp.Dsizeof (typ, Option.bind dynamic_length ~f:(exp_rv_dexp_ tenv seen node), subtype)) (DExp.Dsizeof (typ, Option.bind dynamic_length ~f:(exp_rv_dexp_ tenv seen node), subtype))
| _ -> | _ ->
@ -513,7 +543,10 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
(** find the dexp, if any, where the given value is stored also return the type of the value if (** find the dexp, if any, where the given value is stored also return the type of the value if
found *) found *)
let vpath_find tenv prop exp_ : DExp.t option * Typ.t option = let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
if verbose then (L.d_str "in vpath_find exp:" ; Exp.d_exp exp_ ; L.d_ln ()) ; if verbose then (
L.d_str "in vpath_find exp:" ;
Exp.d_exp exp_ ;
L.d_ln () ) ;
let rec find sigma_acc sigma_todo exp = let rec find sigma_acc sigma_todo exp =
let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) =
match se with match se with
@ -614,7 +647,12 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
L.d_ln () L.d_ln ()
| Some de, typo -> ( | Some de, typo -> (
L.d_printf "vpath_find: found %a :" DExp.pp de ; L.d_printf "vpath_find: found %a :" DExp.pp de ;
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 res
@ -657,7 +695,8 @@ let explain_dexp_access prop dexp is_nullable =
| _ -> | _ ->
() ()
in in
List.iter ~f:do_hpred sigma ; !res List.iter ~f:do_hpred sigma ;
!res
in in
let rec lookup_fld fsel f = let rec lookup_fld fsel f =
match fsel with match fsel with

16
infer/src/biabduction/interproc.ml
Unescape View File

@ -396,7 +396,9 @@ let forward_tabulate ({InterproceduralAnalysis.proc_desc; err_log; tenv; _} as a
in in
( match pre_opt with ( match pre_opt with
| Some pre -> | Some pre ->
L.d_strln "Precondition:" ; Prop.d_prop pre ; L.d_ln () L.d_strln "Precondition:" ;
Prop.d_prop pre ;
L.d_ln ()
| None -> | None ->
() ) ; () ) ;
L.d_strln "SIL INSTR:" ; L.d_strln "SIL INSTR:" ;
@ -408,7 +410,11 @@ let forward_tabulate ({InterproceduralAnalysis.proc_desc; err_log; tenv; _} as a
let exe_iter f pathset = let exe_iter f pathset =
let ps_size = Paths.PathSet.size pathset in let ps_size = Paths.PathSet.size pathset in
let cnt = ref 0 in let cnt = ref 0 in
let exe prop path = State.set_path path None ; incr cnt ; f prop path !cnt ps_size in let exe prop path =
State.set_path path None ;
incr cnt ;
f prop path !cnt ps_size
in
Paths.PathSet.iter exe pathset Paths.PathSet.iter exe pathset
in in
let print_node_preamble curr_node pathset_todo = let print_node_preamble curr_node pathset_todo =
@ -489,7 +495,8 @@ let remove_locals_formals_and_check {InterproceduralAnalysis.proc_desc; err_log;
let exn = Exceptions.Stack_variable_address_escape (desc, __POS__) in let exn = Exceptions.Stack_variable_address_escape (desc, __POS__) in
BiabductionReporting.log_issue_deprecated_using_state proc_desc err_log Exceptions.Warning exn BiabductionReporting.log_issue_deprecated_using_state proc_desc err_log Exceptions.Warning exn
in in
List.iter ~f:check_pvar pvars ; p' List.iter ~f:check_pvar pvars ;
p'
(** Collect the analysis results for the exit node. *) (** Collect the analysis results for the exit node. *)
@ -739,7 +746,8 @@ let execute_filter_prop ({InterproceduralAnalysis.tenv; _} as analysis_data) pro
precondition precondition
in in
let spec = BiabductionSummary.{pre; posts; visited} in let spec = BiabductionSummary.{pre; posts; visited} in
L.d_decrease_indent () ; Some spec ) L.d_decrease_indent () ;
Some spec )
with RE_EXE_ERROR -> with RE_EXE_ERROR ->
AnalysisCallbacks.html_debug_new_node_session ~pp_name init_node ~f:(fun () -> AnalysisCallbacks.html_debug_new_node_session ~pp_name init_node ~f:(fun () ->
L.d_printfln ~color:Red "#### [FUNCTION %a] ...ERROR" Procname.pp pname ; L.d_printfln ~color:Red "#### [FUNCTION %a] ...ERROR" Procname.pp pname ;

5
infer/src/bufferoverrun/absLoc.ml
Unescape View File

@ -242,7 +242,10 @@ module Loc = struct
BufferOverrunField.pp ~pp_lhs:(pp_star ~paren:true) ~sep:"." fmt prefix last_field BufferOverrunField.pp ~pp_lhs:(pp_star ~paren:true) ~sep:"." fmt prefix last_field
and pp_star ~paren fmt l = pp_paren ~paren fmt l ; F.pp_print_string fmt ".*" and pp_star ~paren fmt l =
pp_paren ~paren fmt l ;
F.pp_print_string fmt ".*"
let pp = pp_paren ~paren:false let pp = pp_paren ~paren:false

14
infer/src/bufferoverrun/bounds.ml
Unescape View File

@ -74,8 +74,12 @@ module SymLinear = struct
let c = (c :> Z.t) in let c = (c :> Z.t) in
let c = let c =
if is_beginning then c if is_beginning then c
else if Z.gt c Z.zero then (F.pp_print_string f " + " ; c) else if Z.gt c Z.zero then (
else (F.pp_print_string f " - " ; Z.neg c) F.pp_print_string f " + " ;
c )
else (
F.pp_print_string f " - " ;
Z.neg c )
in in
if Z.(equal c one) then (Symb.Symbol.pp_mark ~markup) f s if Z.(equal c one) then (Symb.Symbol.pp_mark ~markup) f s
else if Z.(equal c minus_one) then F.fprintf f "-%a" (Symb.Symbol.pp_mark ~markup) s else if Z.(equal c minus_one) then F.fprintf f "-%a" (Symb.Symbol.pp_mark ~markup) s
@ -86,7 +90,11 @@ module SymLinear = struct
fun ~markup ~is_beginning f x -> fun ~markup ~is_beginning f x ->
if M.is_empty x then if is_beginning then F.pp_print_string f "0" else () if M.is_empty x then if is_beginning then F.pp_print_string f "0" else ()
else else
( M.fold (fun s c is_beginning -> pp1 ~markup ~is_beginning f s c ; false) x is_beginning ( M.fold
(fun s c is_beginning ->
pp1 ~markup ~is_beginning f s c ;
false )
x is_beginning
: bool ) : bool )
|> ignore |> ignore

3
infer/src/bufferoverrun/bufferOverrunAnalysis.ml
Unescape View File

@ -463,7 +463,8 @@ let cached_compute_invariant_map =
inv_map inv_map
| None -> | None ->
let inv_map = compute_invariant_map analysis_data in let inv_map = compute_invariant_map analysis_data in
cache_set pname inv_map ; inv_map cache_set pname inv_map ;
inv_map
let compute_summary : (Pvar.t * Typ.t) list -> CFG.t -> invariant_map -> memory_summary = let compute_summary : (Pvar.t * Typ.t) list -> CFG.t -> invariant_map -> memory_summary =

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

@ -1431,7 +1431,10 @@ end
module AliasRet = struct module AliasRet = struct
include AliasTargets include AliasTargets
let pp : F.formatter -> t -> unit = fun fmt x -> F.pp_print_string fmt "ret=" ; pp fmt x let pp : F.formatter -> t -> unit =
fun fmt x ->
F.pp_print_string fmt "ret=" ;
pp fmt x
end end
module Alias = struct module Alias = struct

5
infer/src/bufferoverrun/symb.ml
Unescape View File

@ -169,7 +169,10 @@ module SymbolPath = struct
if paren then F.fprintf fmt ")" if paren then F.fprintf fmt ")"
and pp_star ~paren fmt p = pp_partial_paren ~paren fmt p ; F.pp_print_string fmt ".*" and pp_star ~paren fmt p =
pp_partial_paren ~paren fmt p ;
F.pp_print_string fmt ".*"
let pp_partial = pp_partial_paren ~paren:false let pp_partial = pp_partial_paren ~paren:false

3
infer/src/checkers/NullabilityPreanalysis.ml
Unescape View File

@ -41,7 +41,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let exec_instr astate id_table _ instr = let exec_instr astate id_table _ instr =
match instr with match instr with
| Sil.Load {id; e= exp} -> | Sil.Load {id; e= exp} ->
Ident.Hash.add id_table id exp ; astate Ident.Hash.add id_table id exp ;
astate
| Sil.Store {e1= Exp.Lfield (Exp.Var lhs_id, name, typ); typ= exp_typ; e2= rhs} -> ( | Sil.Store {e1= Exp.Lfield (Exp.Var lhs_id, name, typ); typ= exp_typ; e2= rhs} -> (
match exp_typ.Typ.desc with match exp_typ.Typ.desc with
(* block field of a ObjC class *) (* block field of a ObjC class *)

3
infer/src/checkers/annotationReachability.ml
Unescape View File

@ -242,7 +242,8 @@ module CxxAnnotationSpecs = struct
let debug_pred ~spec_name ~desc pred pname = let debug_pred ~spec_name ~desc pred pname =
L.d_printf "%s: Checking if `%a` is a %s... " spec_name Procname.pp pname desc ; L.d_printf "%s: Checking if `%a` is a %s... " spec_name Procname.pp pname desc ;
let r = pred pname in let r = pred pname in
L.d_printf "%b %s.@." r desc ; r L.d_printf "%b %s.@." r desc ;
r
let at_least_one_nonempty ~src symbols symbol_regexps paths = let at_least_one_nonempty ~src symbols symbol_regexps paths =

3
infer/src/checkers/dominators.ml
Unescape View File

@ -27,7 +27,8 @@ let print_dominators cfg idom =
[idom n] returns the immediate dominator of [n]. *) [idom n] returns the immediate dominator of [n]. *)
let get_idoms pdesc = let get_idoms pdesc =
let idom = GDoms.compute_idom pdesc (ProcCfg.Normal.start_node pdesc) in let idom = GDoms.compute_idom pdesc (ProcCfg.Normal.start_node pdesc) in
print_dominators pdesc idom ; idom print_dominators pdesc idom ;
idom
(* make each node to be dominated by itself, i.e reflexive, unlike ocamlgraph *) (* make each node to be dominated by itself, i.e reflexive, unlike ocamlgraph *)

3
infer/src/checkers/uninit.ml
Unescape View File

@ -328,7 +328,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
() ) ; () ) ;
{astate with maybe_uninit_vars} {astate with maybe_uninit_vars}
| Assume (expr, _, _, loc) -> | Assume (expr, _, _, loc) ->
check_hil_expr expr ~loc ; astate check_hil_expr expr ~loc ;
astate
| Metadata _ -> | Metadata _ ->
astate astate

3
infer/src/clang/cAst_utils.ml
Unescape View File

@ -336,7 +336,8 @@ let generate_key_stmt stmt =
let _, stmts = Clang_ast_proj.get_stmt_tuple stmt in let _, stmts = Clang_ast_proj.get_stmt_tuple stmt in
List.iter ~f:add_stmt stmts List.iter ~f:add_stmt stmts
in in
add_stmt stmt ; Buffer.contents buffer add_stmt stmt ;
Buffer.contents buffer
(* Generates a key for a declaration based on its name and the declaration tag. *) (* Generates a key for a declaration based on its name and the declaration tag. *)

6
infer/src/clang/cMethod_trans.ml
Unescape View File

@ -126,7 +126,8 @@ let should_create_procdesc cfg procname ~defined ~set_objc_accessor_attr =
| previous_procdesc -> | previous_procdesc ->
let is_defined_previous = Procdesc.is_defined previous_procdesc in let is_defined_previous = Procdesc.is_defined previous_procdesc in
if (defined || set_objc_accessor_attr) && not is_defined_previous then ( if (defined || set_objc_accessor_attr) && not is_defined_previous then (
Procname.Hash.remove cfg procname ; true ) Procname.Hash.remove cfg procname ;
true )
else false else false
| exception Caml.Not_found -> | exception Caml.Not_found ->
true true
@ -264,7 +265,8 @@ let create_local_procdesc ?(set_objc_accessor_attr = false) trans_unit_ctx cfg t
Procdesc.set_exit_node procdesc exit_node ) Procdesc.set_exit_node procdesc exit_node )
in in
if should_create_procdesc cfg proc_name ~defined ~set_objc_accessor_attr then ( if should_create_procdesc cfg proc_name ~defined ~set_objc_accessor_attr then (
create_new_procdesc () ; true ) create_new_procdesc () ;
true )
else false else false

3
infer/src/clang/cScope.ml
Unescape View File

@ -203,7 +203,8 @@ module Variables = struct
and visit_stmt_list stmt_list scope_map = and visit_stmt_list stmt_list scope_map =
List.fold stmt_list ~init:scope_map ~f:(fun scope_map stmt -> List.fold stmt_list ~init:scope_map ~f:(fun scope_map stmt ->
L.debug Capture Verbose "@;" ; visit_stmt stmt scope_map ) L.debug Capture Verbose "@;" ;
visit_stmt stmt scope_map )
let empty_scope = {current= []; current_kind= InitialScope; outers= []} let empty_scope = {current= []; current_kind= InitialScope; outers= []}

3
infer/src/cost/boundMap.ml
Unescape View File

@ -83,7 +83,8 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map
Node.IdMap.add node_id BasicCost.zero bound_map ) Node.IdMap.add node_id BasicCost.zero bound_map )
in in
let bound_map = NodeCFG.fold_nodes node_cfg ~f:compute_node_upper_bound ~init:Node.IdMap.empty in let bound_map = NodeCFG.fold_nodes node_cfg ~f:compute_node_upper_bound ~init:Node.IdMap.empty in
print_upper_bound_map bound_map ; bound_map print_upper_bound_map bound_map ;
bound_map
let lookup_upperbound bound_map nid = let lookup_upperbound bound_map nid =

11
infer/src/infer.ml
Unescape View File

@ -56,7 +56,9 @@ let setup () =
if if
CLOpt.is_originator && (not Config.continue_capture) CLOpt.is_originator && (not Config.continue_capture)
&& not (Driver.is_analyze_mode driver_mode) && not (Driver.is_analyze_mode driver_mode)
then ( db_start () ; SourceFiles.mark_all_stale () ) then (
db_start () ;
SourceFiles.mark_all_stale () )
| Explore -> | Explore ->
ResultsDir.assert_results_dir "please run an infer analysis first" ) ; ResultsDir.assert_results_dir "please run an infer analysis first" ) ;
db_start () ; db_start () ;
@ -109,7 +111,9 @@ let log_environment_info () =
| Some available_memory -> | Some available_memory ->
L.environment_info "Available memory at startup: %d MB@\n" available_memory ; L.environment_info "Available memory at startup: %d MB@\n" available_memory ;
ScubaLogging.log_count ~label:"startup_mem_avail_MB" ~value:available_memory ) ; ScubaLogging.log_count ~label:"startup_mem_avail_MB" ~value:available_memory ) ;
print_active_checkers () ; print_scheduler () ; print_cores_used () print_active_checkers () ;
print_scheduler () ;
print_cores_used ()
let () = let () =
@ -121,7 +125,8 @@ let () =
| Ok () -> | Ok () ->
L.exit 0 L.exit 0
| Error e -> | Error e ->
print_endline e ; L.exit 3 ) ; print_endline e ;
L.exit 3 ) ;
( match Config.check_version with ( match Config.check_version with
| Some check_version -> | Some check_version ->
if not (String.equal check_version Version.versionString) then if not (String.equal check_version Version.versionString) then

3
infer/src/integration/IssuesTest.ml
Unescape View File

@ -80,7 +80,8 @@ let pp_custom_of_report fmt report fields =
Option.iter nullsafe_extra ~f:(fun nullsafe_extra -> Option.iter nullsafe_extra ~f:(fun nullsafe_extra ->
F.fprintf fmt "%s%a" (comma_separator index) pp_nullsafe_extra nullsafe_extra ) F.fprintf fmt "%s%a" (comma_separator index) pp_nullsafe_extra nullsafe_extra )
in in
List.iteri ~f:pp_field fields ; F.fprintf fmt "@." List.iteri ~f:pp_field fields ;
F.fprintf fmt "@."
in in
List.iter ~f:(pp_custom_of_issue fmt) report List.iter ~f:(pp_custom_of_issue fmt) report

3
infer/src/integration/JsonReports.ml
Unescape View File

@ -303,7 +303,8 @@ let write_lint_issues filters (issues_outf : Utils.outfile) linereader procname
(** Process a summary *) (** Process a summary *)
let process_summary ~costs_outf summary issues_acc = let process_summary ~costs_outf summary issues_acc =
write_costs summary costs_outf ; collect_issues summary issues_acc write_costs summary costs_outf ;
collect_issues summary issues_acc
let process_all_summaries_and_issues ~issues_outf ~costs_outf = let process_all_summaries_and_issues ~issues_outf ~costs_outf =

3
infer/src/integration/TraceBugs.ml
Unescape View File

@ -19,7 +19,8 @@ let has_trace {Jsonbug_t.bug_trace; _} = not (List.is_empty bug_trace)
let with_file_fmt file ~f = let with_file_fmt file ~f =
Utils.with_file_out file ~f:(fun outc -> Utils.with_file_out file ~f:(fun outc ->
let fmt = F.formatter_of_out_channel outc in let fmt = F.formatter_of_out_channel outc in
f fmt ; F.pp_print_flush fmt () ) f fmt ;
F.pp_print_flush fmt () )
let pp_trace_item ~show_source_context fmt let pp_trace_item ~show_source_context fmt

3
infer/src/integration/XcodeBuild.ml
Unescape View File

@ -44,7 +44,8 @@ let capture ~prog ~args =
Utils.with_channel_in stderr_chan ~f:(L.progress "XCODEBUILD: %s@.") ; Utils.with_channel_in stderr_chan ~f:(L.progress "XCODEBUILD: %s@.") ;
match Unix.waitpid pid with match Unix.waitpid pid with
| Ok () -> | Ok () ->
In_channel.close stdout_chan ; In_channel.close stderr_chan In_channel.close stdout_chan ;
In_channel.close stderr_chan
| Error _ as err -> | Error _ as err ->
L.die ExternalError "*** capture failed to execute: %s" L.die ExternalError "*** capture failed to execute: %s"
(Unix.Exit_or_signal.to_string_hum err) (Unix.Exit_or_signal.to_string_hum err)

9
infer/src/istd/IList.ml
Unescape View File

@ -195,7 +195,14 @@ let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf =
pp_v ppf v ; pp_v ppf v ;
aux (n + 1) rest ) aux (n + 1) rest )
in in
function [] -> () | [v] -> pp_v ppf v | v :: rest -> pp_v ppf v ; aux 1 rest function
| [] ->
()
| [v] ->
pp_v ppf v
| v :: rest ->
pp_v ppf v ;
aux 1 rest
let fold2_result ~init ~f l1 l2 = let fold2_result ~init ~f l1 l2 =

6
infer/src/istd/ImperativeUnionFind.ml
Unescape View File

@ -83,7 +83,8 @@ module Make (Set : Set) = struct
set set
| None -> | None ->
let set = Set.create (r :> Set.elt) in let set = Set.create (r :> Set.elt) in
H.replace t r set ; set H.replace t r set ;
set
let fold = H.fold let fold = H.fold
@ -146,7 +147,8 @@ module Make (Set : Set) = struct
t.nb_iterators <- t.nb_iterators + 1 ; t.nb_iterators <- t.nb_iterators + 1 ;
match IContainer.filter ~fold:Sets.fold ~filter:(is_still_a_repr t) t.sets ~init ~f with match IContainer.filter ~fold:Sets.fold ~filter:(is_still_a_repr t) t.sets ~init ~f with
| result -> | result ->
after_fold t ; result after_fold t ;
result
| exception e -> | exception e ->
(* Ensures [nb_iterators] is correct *) (* Ensures [nb_iterators] is correct *)
IExn.reraise_after ~f:(fun () -> after_fold t) e IExn.reraise_after ~f:(fun () -> after_fold t) e

22
infer/src/istd/LRUHashtbl.ml
Unescape View File

@ -67,7 +67,12 @@ module Make (Key : Hashtbl.HashedType) = struct
let create ~initial_size ~max_size = {map= Hash.create initial_size; lru= LRU.create max_size} let create ~initial_size ~max_size = {map= Hash.create initial_size; lru= LRU.create max_size}
let find_opt {map; lru} k = let find_opt {map; lru} k =
match Hash.find_opt map k with None -> None | Some (v, e) -> LRU.use lru e ; Some v match Hash.find_opt map k with
| None ->
None
| Some (v, e) ->
LRU.use lru e ;
Some v
let replace {map; lru} k v = let replace {map; lru} k v =
@ -78,7 +83,8 @@ module Make (Key : Hashtbl.HashedType) = struct
Option.iter removed_key ~f:(Hash.remove map) ; Option.iter removed_key ~f:(Hash.remove map) ;
n n
| Some (_, n) -> | Some (_, n) ->
LRU.use lru n ; n LRU.use lru n ;
n
in in
Hash.replace map k (v, n) Hash.replace map k (v, n)
@ -88,10 +94,14 @@ module Make (Key : Hashtbl.HashedType) = struct
| None -> | None ->
() ()
| Some (_, n) -> | Some (_, n) ->
LRU.remove lru n ; Hash.remove map k LRU.remove lru n ;
Hash.remove map k
let clear {map; lru} =
Hash.clear map ;
LRU.clear lru
let clear {map; lru} = Hash.clear map ; LRU.clear lru
let pp ~pp_key ~pp_v f {map} = let pp ~pp_key ~pp_v f {map} =
let is_first = ref true in let is_first = ref true in
@ -99,7 +109,9 @@ module Make (Key : Hashtbl.HashedType) = struct
if !is_first then is_first := false else F.pp_print_string f ", " ; if !is_first then is_first := false else F.pp_print_string f ", " ;
F.fprintf f "%a->%a" pp_key key pp_v v F.fprintf f "%a->%a" pp_key key pp_v v
in in
F.pp_print_string f "{" ; Hash.iter pp_key_v map ; F.pp_print_string f "}" F.pp_print_string f "{" ;
Hash.iter pp_key_v map ;
F.pp_print_string f "}"
let bindings {map} = Seq.fold_left (fun acc (k, (v, _node)) -> (k, v) :: acc) [] (Hash.to_seq map) let bindings {map} = Seq.fold_left (fun acc (k, (v, _node)) -> (k, v) :: acc) [] (Hash.to_seq map)

3
infer/src/istd/RecencyMap.ml
Unescape View File

@ -183,7 +183,8 @@ module Make
| None -> | None ->
None None
| Some _ as value_opt -> | Some _ as value_opt ->
incr count_old ; value_opt ) incr count_old ;
value_opt )
map1.old map2.old map1.old map2.old
in in
{count_new= !count_new; old; new_} {count_new= !count_new; old; new_}

3
infer/src/java/jFrontend.ml
Unescape View File

@ -67,7 +67,8 @@ let add_edges (context : JContext.t) start_node exn_node exit_nodes method_body_
| JTrans.Instr node -> | JTrans.Instr node ->
connect node pc connect node pc
| JTrans.Prune (node_true, node_false) -> | JTrans.Prune (node_true, node_false) ->
connect node_true pc ; connect node_false pc connect node_true pc ;
connect node_false pc
| JTrans.Loop (join_node, node_true, node_false) -> | JTrans.Loop (join_node, node_true, node_false) ->
Procdesc.node_set_succs context.procdesc join_node ~normal:[node_true; node_false] ~exn:[] ; Procdesc.node_set_succs context.procdesc join_node ~normal:[node_true; node_false] ~exn:[] ;
connect node_true pc ; connect node_true pc ;

3
infer/src/java/jMain.ml
Unescape View File

@ -44,7 +44,8 @@ let capture_libs program tenv =
let fake_source_file = SourceFile.from_abs_path (JFrontend.path_of_cached_classname cn) in let fake_source_file = SourceFile.from_abs_path (JFrontend.path_of_cached_classname cn) in
init_global_state fake_source_file ; init_global_state fake_source_file ;
let cfg = JFrontend.compute_class_icfg fake_source_file program tenv node in let cfg = JFrontend.compute_class_icfg fake_source_file program tenv node in
store_icfg fake_source_file cfg ; JFrontend.cache_classname cn store_icfg fake_source_file cfg ;
JFrontend.cache_classname cn
in in
JBasics.ClassMap.iter (capture_class tenv) (JClasspath.get_classmap program) JBasics.ClassMap.iter (capture_class tenv) (JClasspath.get_classmap program)

3
infer/src/java/jTrans.ml
Unescape View File

@ -102,7 +102,8 @@ let formals_from_signature program tenv cn ms kind =
let method_name = JBasics.ms_name ms in let method_name = JBasics.ms_name ms in
let get_arg_name () = let get_arg_name () =
let arg = method_name ^ "_arg_" ^ string_of_int !counter in let arg = method_name ^ "_arg_" ^ string_of_int !counter in
incr counter ; Mangled.from_string arg incr counter ;
Mangled.from_string arg
in in
let collect l vt = let collect l vt =
let arg_name = get_arg_name () in let arg_name = get_arg_name () in

7
infer/src/nullsafe/Initializers.ml
Unescape View File

@ -44,7 +44,8 @@ let final_typestates initializers_current_class tenv typecheck_proc =
in in
List.iter ~f:do_called private_called List.iter ~f:do_called private_called
in in
List.iter ~f:do_proc initializers ; !res List.iter ~f:do_proc initializers ;
!res
in in
(* Get the initializers recursively called by computing a fixpoint. (* Get the initializers recursively called by computing a fixpoint.
Start from the initializers of the current class and the current procedure. *) Start from the initializers of the current class and the current procedure. *)
@ -64,7 +65,9 @@ let final_typestates initializers_current_class tenv typecheck_proc =
mark_seen initializers_new' ; mark_seen initializers_new' ;
if not (List.is_empty initializers_new') then fixpoint initializers_new' if not (List.is_empty initializers_new') then fixpoint initializers_new'
in in
mark_seen initializers_base_case ; fixpoint initializers_base_case ; !res mark_seen initializers_base_case ;
fixpoint initializers_base_case ;
!res
in in
(* Get the final typestates of all the initializers. *) (* Get the final typestates of all the initializers. *)
let final_typestates = ref [] in let final_typestates = ref [] in

3
infer/src/nullsafe/eradicateChecks.ml
Unescape View File

@ -75,7 +75,8 @@ let check_condition_for_redundancy
if Location.equal loc (Procdesc.Node.get_loc n) then if Location.equal loc (Procdesc.Node.get_loc n) then
Instrs.iter ~f:do_instr (Procdesc.Node.get_instrs n) Instrs.iter ~f:do_instr (Procdesc.Node.get_instrs n)
in in
Procdesc.iter_nodes do_node pdesc ; !throwable_found Procdesc.iter_nodes do_node pdesc ;
!throwable_found
in in
let from_try_with_resources () : bool = let from_try_with_resources () : bool =
(* heuristic to check if the condition is the translation of try-with-resources *) (* heuristic to check if the condition is the translation of try-with-resources *)

3
infer/src/nullsafe/typeCheck.ml
Unescape View File

@ -1213,7 +1213,8 @@ let typecheck_instr ({IntraproceduralAnalysis.proc_desc= curr_pdesc; tenv; _} as
| _ -> | _ ->
typestate typestate
in in
check_field_assign () ; typestate2 check_field_assign () ;
typestate2
(* Java `new` operators *) (* Java `new` operators *)
| Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(_, typ)], _, _) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(_, typ)], _, _)
when Procname.equal pn BuiltinDecl.__new || Procname.equal pn BuiltinDecl.__new_array -> when Procname.equal pn BuiltinDecl.__new || Procname.equal pn BuiltinDecl.__new_array ->

6
infer/src/nullsafe/typeErr.ml
Unescape View File

@ -52,7 +52,8 @@ module InstrRef : InstrRefT = struct
let gen instr_ref_gen = let gen instr_ref_gen =
let node, ir = instr_ref_gen in let node, ir = instr_ref_gen in
incr ir ; (node, !ir) incr ir ;
(node, !ir)
end end
(* InstrRef *) (* InstrRef *)
@ -357,7 +358,8 @@ let report_forall_issues_and_reset analysis_data ~nullsafe_mode =
| None, _ -> | None, _ ->
() ()
in in
H.iter iter err_tbl ; reset () H.iter iter err_tbl ;
reset ()
let get_errors () = let get_errors () =

3
infer/src/pulse/PulseAbstractValue.ml
Unescape View File

@ -17,7 +17,8 @@ let next_fresh = ref initial_next_fresh
let mk_fresh () = let mk_fresh () =
let l = !next_fresh in let l = !next_fresh in
incr next_fresh ; l incr next_fresh ;
l
let pp f l = F.fprintf f "v%d" l let pp f l = F.fprintf f "v%d" l

28
infer/src/topl/Topl.ml
Unescape View File

@ -52,9 +52,11 @@ let evaluate_static_guard label_o (e_fun, arg_ts) =
let name = Procname.hashable_name n in let name = Procname.hashable_name n in
let re = Str.regexp label.ToplAst.procedure_name in let re = Str.regexp label.ToplAst.procedure_name in
let result = Str.string_match re name 0 in let result = Str.string_match re name 0 in
tt " check name='%s'@\n" name ; result tt " check name='%s'@\n" name ;
result
| _ -> | _ ->
tt " check name-unknown@\n" ; false tt " check name-unknown@\n" ;
false
in in
let pattern_len = Option.map ~f:List.length label.ToplAst.arguments in let pattern_len = Option.map ~f:List.length label.ToplAst.arguments in
let match_args () = let match_args () =
@ -65,8 +67,16 @@ let evaluate_static_guard label_o (e_fun, arg_ts) =
in in
tt "match name-pattern='%s' arg-len-pattern=%a@\n" label.ToplAst.procedure_name tt "match name-pattern='%s' arg-len-pattern=%a@\n" label.ToplAst.procedure_name
(Pp.option Int.pp) pattern_len ; (Pp.option Int.pp) pattern_len ;
let log f = f () || (tt " match result FALSE@\n" ; false) in let log f =
log match_args && log match_name && (tt " match result TRUE@\n" ; true) f ()
||
( tt " match result FALSE@\n" ;
false )
in
log match_args && log match_name
&&
( tt " match result TRUE@\n" ;
true )
in in
Option.value_map ~default:true ~f:evaluate_nonany label_o Option.value_map ~default:true ~f:evaluate_nonany label_o
@ -130,7 +140,11 @@ let add_types tenv =
let record_predicate = let record_predicate =
ToplAst.( ToplAst.(
function function
| Binop (_, v1, v2) -> record_value v1 ; record_value v2 | Value v -> record_value v) | Binop (_, v1, v2) ->
record_value v1 ;
record_value v2
| Value v ->
record_value v)
in in
let record_assignment (reg, _) = record reg in let record_assignment (reg, _) = record reg in
let record_label label = let record_label label =
@ -163,7 +177,9 @@ let instrument tenv procdesc =
let f _node = instrument_instruction in let f _node = instrument_instruction in
tt "instrument@\n" ; tt "instrument@\n" ;
let _updated = Procdesc.replace_instrs_by procdesc ~f in let _updated = Procdesc.replace_instrs_by procdesc ~f in
tt "add types@\n" ; add_types tenv ; tt "done@\n" ) tt "add types@\n" ;
add_types tenv ;
tt "done@\n" )
(** [lookup_static_var var prop] expects [var] to have the form [Exp.Lfield (obj, fieldname)], and (** [lookup_static_var var prop] expects [var] to have the form [Exp.Lfield (obj, fieldname)], and

6
infer/src/topl/ToplAutomaton.ml
Unescape View File

@ -101,7 +101,8 @@ let make properties =
let vcount = Array.length states in let vcount = Array.length states in
let a = Array.create ~len:vcount [] in let a = Array.create ~len:vcount [] in
let f i t = a.(t.source) <- i :: a.(t.source) in let f i t = a.(t.source) <- i :: a.(t.source) in
Array.iteri ~f transitions ; a Array.iteri ~f transitions ;
a
in in
let max_args = let max_args =
let llen l = Option.value_map ~default:0 ~f:List.length l.ToplAst.arguments in let llen l = Option.value_map ~default:0 ~f:List.length l.ToplAst.arguments in
@ -125,7 +126,8 @@ let make properties =
in in
List.iter ~f:set_nondet nondet List.iter ~f:set_nondet nondet
in in
List.iter ~f properties ; a List.iter ~f properties ;
a
in in
let skips : bool array = let skips : bool array =
(* TODO(rgrigore): Rename "anys"? *) (* TODO(rgrigore): Rename "anys"? *)

4
infer/src/topl/ToplMonitor.ml
Unescape View File

@ -32,7 +32,9 @@ let formals_of_procname proc_name =
let params = Procname.get_parameters proc_name in let params = Procname.get_parameters proc_name in
let new_arg_name = let new_arg_name =
let n = ref (-1) in let n = ref (-1) in
fun () -> incr n ; ToplName.arg !n fun () ->
incr n ;
ToplName.arg !n
in in
let f t = let f t =
let name = Mangled.from_string (new_arg_name ()) in let name = Mangled.from_string (new_arg_name ()) in

7
infer/src/unit/LRUHashtblTests.ml
Unescape View File

@ -14,7 +14,8 @@ let inputs =
; ( "singleton" ; ( "singleton"
, (fun () -> , (fun () ->
let map = LRUHash.create ~initial_size:5 ~max_size:3 in let map = LRUHash.create ~initial_size:5 ~max_size:3 in
LRUHash.replace map 0 10 ; map ) LRUHash.replace map 0 10 ;
map )
, [(0, 10)] ) , [(0, 10)] )
; ( "LRU1" ; ( "LRU1"
, (fun () -> , (fun () ->
@ -23,7 +24,9 @@ let inputs =
LRUHash.replace map 1 10 ; LRUHash.replace map 1 10 ;
LRUHash.replace map 2 10 ; LRUHash.replace map 2 10 ;
let (_ : int option) = LRUHash.find_opt map 1 in let (_ : int option) = LRUHash.find_opt map 1 in
LRUHash.replace map 3 10 ; LRUHash.replace map 4 10 ; map ) LRUHash.replace map 3 10 ;
LRUHash.replace map 4 10 ;
map )
, [(1, 10); (3, 10); (4, 10)] ) , [(1, 10); (3, 10); (4, 10)] )
; ( "LRU2" ; ( "LRU2"
, (fun () -> , (fun () ->

5
infer/src/unit/analyzerTester.ml
Unescape View File

@ -57,7 +57,10 @@ module StructuredSil = struct
let label_counter = ref 0 let label_counter = ref 0
let fresh_label () = incr label_counter ; !label_counter let fresh_label () =
incr label_counter ;
!label_counter
let invariant inv_str = Invariant (inv_str, fresh_label ()) let invariant inv_str = Invariant (inv_str, fresh_label ())

Write Preview
Loading…
Cancel
Save