From 3de92484dff135aaf6a221e9c541703dff390f4e Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Fri, 17 Jan 2020 04:00:20 -0800
Subject: [PATCH] [inferbo] Refactoring: move get_formals type definition
Summary:
This diffs does: (1) move `get_formals` to `BufferOverrunUtils` (2) use separate `get_formals` in
`BufferOverrunChecker`, in order to simplify the following diff.
Reviewed By: jvillard
Differential Revision: D19432280
fbshipit-source-id: bfb4df118
---
.../bufferoverrun/bufferOverrunAnalysis.ml | 6 +--
.../src/bufferoverrun/bufferOverrunChecker.ml | 37 +++++++++++--------
infer/src/bufferoverrun/bufferOverrunUtils.ml | 2 +
.../src/bufferoverrun/bufferOverrunUtils.mli | 2 +
4 files changed, 27 insertions(+), 20 deletions(-)
diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
index 47436c8bd..efcc1b215 100644
--- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
+++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
@@ -25,11 +25,9 @@ module Payload = SummaryPayload.Make (struct
let field = Payloads.Fields.buffer_overrun_analysis
end)
-type get_formals = Procname.t -> (Pvar.t * Typ.t) list option
-
type extras =
{ get_summary: BufferOverrunAnalysisSummary.get_summary
- ; get_formals: get_formals
+ ; get_formals: BoUtils.get_formals
; oenv: OndemandEnv.t }
module CFG = ProcCfg.NormalOneInstrPerNode
@@ -449,7 +447,7 @@ let compute_invariant_map :
-> Tenv.t
-> Typ.IntegerWidths.t
-> BufferOverrunAnalysisSummary.get_summary
- -> get_formals
+ -> BoUtils.get_formals
-> invariant_map =
fun summary tenv integer_type_widths get_summary get_formals ->
let pdesc = Summary.get_proc_desc summary in
diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index 02e2f64df..8917de708 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -250,10 +250,11 @@ let instantiate_cond :
type checks_summary = BufferOverrunCheckerSummary.t
-type get_checks_summary = Procname.t -> ((Pvar.t * Typ.t) list * checks_summary) option
+type get_checks_summary = Procname.t -> checks_summary option
let check_instr :
get_checks_summary
+ -> BoUtils.get_formals
-> Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
@@ -262,7 +263,7 @@ let check_instr :
-> Dom.Mem.t
-> PO.ConditionSet.checked_t
-> PO.ConditionSet.checked_t =
- fun get_checks_summary pdesc tenv integer_type_widths node instr mem cond_set ->
+ fun get_checks_summary get_formals pdesc tenv integer_type_widths node instr mem cond_set ->
match instr with
| Sil.Load {e= exp; loc= location} ->
cond_set
@@ -291,12 +292,12 @@ let check_instr :
in
check model_env mem cond_set
| None -> (
- match get_checks_summary callee_pname with
- | Some (callee_formals, callee_condset) ->
+ match (get_checks_summary callee_pname, get_formals callee_pname) with
+ | Some callee_condset, Some callee_formals ->
instantiate_cond integer_type_widths callee_pname callee_formals params mem
callee_condset location
|> PO.ConditionSet.join cond_set
- | None ->
+ | _, _ ->
(* unknown call / no inferbo payload *) cond_set ) )
| Sil.Prune (exp, location, _, _) ->
check_expr_for_integer_overflow integer_type_widths exp location mem cond_set
@@ -316,6 +317,7 @@ let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> un
let check_instrs :
get_checks_summary
+ -> BoUtils.get_formals
-> Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
@@ -325,7 +327,7 @@ let check_instrs :
-> Dom.Mem.t AbstractInterpreter.State.t
-> Checks.t
-> Checks.t =
- fun get_checks_summary pdesc tenv integer_type_widths cfg node instrs state checks ->
+ fun get_checks_summary get_formals pdesc tenv integer_type_widths cfg node instrs state checks ->
match state with
| _ when Instrs.is_empty instrs ->
checks
@@ -342,7 +344,8 @@ let check_instrs :
checks
in
let cond_set =
- check_instr get_checks_summary pdesc tenv integer_type_widths node instr pre checks.cond_set
+ check_instr get_checks_summary get_formals pdesc tenv integer_type_widths node instr pre
+ checks.cond_set
in
print_debug_info instr pre cond_set ;
{checks with cond_set}
@@ -350,6 +353,7 @@ let check_instrs :
let check_node :
get_checks_summary
+ -> BoUtils.get_formals
-> Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
@@ -358,11 +362,12 @@ let check_node :
-> Checks.t
-> CFG.Node.t
-> Checks.t =
- fun get_checks_summary pdesc tenv integer_type_widths cfg inv_map checks node ->
+ fun get_checks_summary get_formals pdesc tenv integer_type_widths cfg inv_map checks node ->
match BufferOverrunAnalysis.extract_state (CFG.Node.id node) inv_map with
| Some state ->
let instrs = CFG.instrs node in
- check_instrs get_checks_summary pdesc tenv integer_type_widths cfg node instrs state checks
+ check_instrs get_checks_summary get_formals pdesc tenv integer_type_widths cfg node instrs
+ state checks
| _ ->
checks
@@ -371,15 +376,16 @@ type checks = Checks.t
let compute_checks :
get_checks_summary
+ -> BoUtils.get_formals
-> Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> CFG.t
-> BufferOverrunAnalysis.invariant_map
-> checks =
- fun get_checks_summary pdesc tenv integer_type_widths cfg inv_map ->
+ fun get_checks_summary get_formals pdesc tenv integer_type_widths cfg inv_map ->
CFG.fold_nodes cfg
- ~f:(check_node get_checks_summary pdesc tenv integer_type_widths cfg inv_map)
+ ~f:(check_node get_checks_summary get_formals pdesc tenv integer_type_widths cfg inv_map)
~init:Checks.empty
@@ -422,12 +428,11 @@ let checker : Callbacks.proc_callback_args -> Summary.t =
NodePrinter.with_session ~pp_name underlying_exit_node ~f:(fun () ->
let cfg = CFG.from_pdesc proc_desc in
let checks =
- let get_checks_summary callee_pname =
- Payload.read_full ~caller_summary:summary ~callee_pname
- |> Option.map ~f:(fun (callee_pdesc, callee_summary) ->
- (Procdesc.get_pvar_formals callee_pdesc, callee_summary) )
+ let get_checks_summary callee_pname = Payload.read ~caller_summary:summary ~callee_pname in
+ let get_formals callee_pname =
+ Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals
in
- compute_checks get_checks_summary proc_desc tenv integer_type_widths cfg inv_map
+ compute_checks get_checks_summary get_formals proc_desc tenv integer_type_widths cfg inv_map
in
report_errors tenv checks summary ;
let cond_set = get_checks_summary checks in
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml
index c2b093af5..3afda4bac 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.ml
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml
@@ -328,3 +328,5 @@ module Check = struct
| _, _ ->
cond_set
end
+
+type get_formals = Procname.t -> (Pvar.t * Typ.t) list option
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli
index 1eb2a4404..18737a9a2 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.mli
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli
@@ -92,3 +92,5 @@ module Check : sig
-> PO.ConditionSet.checked_t
-> PO.ConditionSet.checked_t
end
+
+type get_formals = Procname.t -> (Pvar.t * Typ.t) list option