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

[inferbo] Lift the Init module up

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D13253573

fbshipit-source-id: f50500a05
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 4e166f3375
commit c3823671f5
1 changed files with 151 additions and 150 deletions
Show Stats Download Patch File Download Diff File

301
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -28,7 +28,156 @@ end)
type extras = {symbol_table: Itv.SymbolTable.t; integer_type_widths: Typ.IntegerWidths.t}
module TransferFunctions (CFG : ProcCfg.S) = struct
module CFG = ProcCfg.NormalOneInstrPerNode
module Init = struct
let declare_symbolic_val :
Typ.Procname.t
-> Itv.SymbolTable.t
-> Itv.SymbolPath.partial
-> Tenv.t
-> Typ.IntegerWidths.t
-> node_hash:int
-> Location.t
-> Loc.t
-> Typ.typ
-> new_sym_num:Counter.t
-> Dom.Mem.t
-> Dom.Mem.t =
fun pname symbol_table path tenv integer_type_widths ~node_hash location loc typ ~new_sym_num
mem ->
let max_depth = 2 in
let rec decl_sym_val pname path tenv location ~depth ~may_last_field loc typ mem =
if depth > max_depth then mem
else
let depth = depth + 1 in
match typ.Typ.desc with
| Typ.Tint ikind ->
let unsigned = Typ.ikind_is_unsigned ikind in
let v = Dom.Val.make_sym ~unsigned loc pname symbol_table path new_sym_num location in
mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
| Typ.Tfloat _ ->
let v = Dom.Val.make_sym loc pname symbol_table path new_sym_num location in
mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
| Typ.Tptr (typ, _) when Language.curr_language_is Java -> (
match typ with
| {desc= Typ.Tarray {elt}} ->
BoUtils.Exec.decl_sym_arr
~decl_sym_val:(decl_sym_val ~may_last_field:false)
Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc
elt ~new_sym_num mem
| _ ->
BoUtils.Exec.decl_sym_java_ptr
~decl_sym_val:(decl_sym_val ~may_last_field:false)
pname path tenv location ~depth loc typ mem )
| Typ.Tptr (typ, _) ->
BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field)
Symb.SymbolPath.Deref_CPointer pname symbol_table path tenv location ~depth loc typ
~new_sym_num mem
| Typ.Tarray {elt; length; stride} ->
let size =
match length with
| Some length when may_last_field && (IntLit.iszero length || IntLit.isone length) ->
None (* Will be made symbolic by [decl_sym_arr] *)
| _ ->
Option.map ~f:Itv.of_int_lit length
in
let offset = Itv.zero in
let stride = Option.map ~f:IntLit.to_int_exn stride in
BoUtils.Exec.decl_sym_arr
~decl_sym_val:(decl_sym_val ~may_last_field:false)
Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc elt
~offset ?size ?stride ~new_sym_num mem
| Typ.Tstruct typename -> (
match Models.TypName.dispatch tenv typename with
| Some {Models.declare_symbolic} ->
let model_env =
Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table
in
declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~depth
loc ~new_sym_num mem
| None ->
let decl_fld ~may_last_field mem (fn, typ, _) =
let loc_fld = Loc.append_field loc ~fn in
let path = Itv.SymbolPath.field path fn in
decl_sym_val pname path tenv location ~depth loc_fld typ ~may_last_field mem
in
let decl_flds str =
IList.fold_last ~f:(decl_fld ~may_last_field:false)
~f_last:(decl_fld ~may_last_field) ~init:mem str.Typ.Struct.fields
in
let opt_struct = Tenv.lookup tenv typename in
Option.value_map opt_struct ~default:mem ~f:decl_flds )
| _ ->
if Config.bo_debug >= 3 then
L.(debug BufferOverrun Verbose)
"/!\\ decl_fld of unhandled type: %a at %a@." (Typ.pp Pp.text) typ Location.pp
location ;
mem
in
decl_sym_val pname path tenv location ~depth:0 ~may_last_field:true loc typ mem
let declare_symbolic_parameters :
Typ.Procname.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> node_hash:int
-> Location.t
-> Itv.SymbolTable.t
-> (Pvar.t * Typ.t) list
-> Dom.Mem.t
-> Dom.Mem.t =
fun pname tenv integer_type_widths ~node_hash location symbol_table formals mem ->
let new_sym_num = Counter.make 0 in
let add_formal mem (pvar, typ) =
let loc = Loc.of_pvar pvar in
let path = Itv.SymbolPath.of_pvar pvar in
declare_symbolic_val pname symbol_table path tenv integer_type_widths ~node_hash location loc
typ ~new_sym_num mem
in
List.fold ~f:add_formal ~init:mem formals
let initial_state {ProcData.pdesc; tenv; extras= {symbol_table; integer_type_widths}} start_node
=
let node_hash = CFG.Node.hash start_node in
let location = CFG.Node.loc start_node in
let pname = Procdesc.get_proc_name pdesc in
let rec decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values
~dimension mem =
match typ.Typ.desc with
| Typ.Tarray {elt= typ; length; stride} ->
let stride = Option.map ~f:IntLit.to_int_exn stride in
BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length
?stride ~inst_num ~represents_multiple_values ~dimension mem
| Typ.Tstruct typname -> (
match Models.TypName.dispatch tenv typname with
| Some {Models.declare_local} ->
let model_env =
Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table
in
declare_local ~decl_local model_env loc ~inst_num ~represents_multiple_values
~dimension mem
| None ->
(mem, inst_num) )
| _ ->
(mem, inst_num)
in
let try_decl_local (mem, inst_num) {ProcAttributes.name; typ} =
let pvar = Pvar.mk name pname in
let loc = Loc.of_pvar pvar in
decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:false
~dimension:1 mem
in
let mem = Dom.Mem.init in
let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
let formals = Sem.get_formals pdesc in
declare_symbolic_parameters pname tenv integer_type_widths ~node_hash location symbol_table
formals mem
end
module TransferFunctions = struct
module CFG = CFG
module Domain = Dom.Mem
@ -249,8 +398,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pp_session_name node fmt = F.fprintf fmt "bufferoverrun %a" CFG.Node.pp_id (CFG.Node.id node)
end
module CFG = ProcCfg.NormalOneInstrPerNode
module Analyzer = AbstractInterpreter.MakeWTO (TransferFunctions (CFG))
module Analyzer = AbstractInterpreter.MakeWTO (TransferFunctions)
type invariant_map = Analyzer.invariant_map
@ -266,153 +414,6 @@ end)
let inv_map_cache = WeakInvMapHashTbl.create 100
module Init = struct
let declare_symbolic_val :
Typ.Procname.t
-> Itv.SymbolTable.t
-> Itv.SymbolPath.partial
-> Tenv.t
-> Typ.IntegerWidths.t
-> node_hash:int
-> Location.t
-> Loc.t
-> Typ.typ
-> new_sym_num:Counter.t
-> Dom.Mem.t
-> Dom.Mem.t =
fun pname symbol_table path tenv integer_type_widths ~node_hash location loc typ ~new_sym_num
mem ->
let max_depth = 2 in
let rec decl_sym_val pname path tenv location ~depth ~may_last_field loc typ mem =
if depth > max_depth then mem
else
let depth = depth + 1 in
match typ.Typ.desc with
| Typ.Tint ikind ->
let unsigned = Typ.ikind_is_unsigned ikind in
let v = Dom.Val.make_sym ~unsigned loc pname symbol_table path new_sym_num location in
mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
| Typ.Tfloat _ ->
let v = Dom.Val.make_sym loc pname symbol_table path new_sym_num location in
mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
| Typ.Tptr (typ, _) when Language.curr_language_is Java -> (
match typ with
| {desc= Typ.Tarray {elt}} ->
BoUtils.Exec.decl_sym_arr
~decl_sym_val:(decl_sym_val ~may_last_field:false)
Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc
elt ~new_sym_num mem
| _ ->
BoUtils.Exec.decl_sym_java_ptr
~decl_sym_val:(decl_sym_val ~may_last_field:false)
pname path tenv location ~depth loc typ mem )
| Typ.Tptr (typ, _) ->
BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field)
Symb.SymbolPath.Deref_CPointer pname symbol_table path tenv location ~depth loc typ
~new_sym_num mem
| Typ.Tarray {elt; length; stride} ->
let size =
match length with
| Some length when may_last_field && (IntLit.iszero length || IntLit.isone length) ->
None (* Will be made symbolic by [decl_sym_arr] *)
| _ ->
Option.map ~f:Itv.of_int_lit length
in
let offset = Itv.zero in
let stride = Option.map ~f:IntLit.to_int_exn stride in
BoUtils.Exec.decl_sym_arr
~decl_sym_val:(decl_sym_val ~may_last_field:false)
Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc elt
~offset ?size ?stride ~new_sym_num mem
| Typ.Tstruct typename -> (
match Models.TypName.dispatch tenv typename with
| Some {Models.declare_symbolic} ->
let model_env =
Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table
in
declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~depth
loc ~new_sym_num mem
| None ->
let decl_fld ~may_last_field mem (fn, typ, _) =
let loc_fld = Loc.append_field loc ~fn in
let path = Itv.SymbolPath.field path fn in
decl_sym_val pname path tenv location ~depth loc_fld typ ~may_last_field mem
in
let decl_flds str =
IList.fold_last ~f:(decl_fld ~may_last_field:false)
~f_last:(decl_fld ~may_last_field) ~init:mem str.Typ.Struct.fields
in
let opt_struct = Tenv.lookup tenv typename in
Option.value_map opt_struct ~default:mem ~f:decl_flds )
| _ ->
if Config.bo_debug >= 3 then
L.(debug BufferOverrun Verbose)
"/!\\ decl_fld of unhandled type: %a at %a@." (Typ.pp Pp.text) typ Location.pp
location ;
mem
in
decl_sym_val pname path tenv location ~depth:0 ~may_last_field:true loc typ mem
let declare_symbolic_parameters :
Typ.Procname.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> node_hash:int
-> Location.t
-> Itv.SymbolTable.t
-> (Pvar.t * Typ.t) list
-> Dom.Mem.t
-> Dom.Mem.t =
fun pname tenv integer_type_widths ~node_hash location symbol_table formals mem ->
let new_sym_num = Counter.make 0 in
let add_formal mem (pvar, typ) =
let loc = Loc.of_pvar pvar in
let path = Itv.SymbolPath.of_pvar pvar in
declare_symbolic_val pname symbol_table path tenv integer_type_widths ~node_hash location loc
typ ~new_sym_num mem
in
List.fold ~f:add_formal ~init:mem formals
let initial_state {ProcData.pdesc; tenv; extras= {symbol_table; integer_type_widths}} start_node
=
let node_hash = CFG.Node.hash start_node in
let location = CFG.Node.loc start_node in
let pname = Procdesc.get_proc_name pdesc in
let rec decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values
~dimension mem =
match typ.Typ.desc with
| Typ.Tarray {elt= typ; length; stride} ->
let stride = Option.map ~f:IntLit.to_int_exn stride in
BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length
?stride ~inst_num ~represents_multiple_values ~dimension mem
| Typ.Tstruct typname -> (
match Models.TypName.dispatch tenv typname with
| Some {Models.declare_local} ->
let model_env =
Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table
in
declare_local ~decl_local model_env loc ~inst_num ~represents_multiple_values
~dimension mem
| None ->
(mem, inst_num) )
| _ ->
(mem, inst_num)
in
let try_decl_local (mem, inst_num) {ProcAttributes.name; typ} =
let pvar = Pvar.mk name pname in
let loc = Loc.of_pvar pvar in
decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:false
~dimension:1 mem
in
let mem = Dom.Mem.init in
let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
let formals = Sem.get_formals pdesc in
declare_symbolic_parameters pname tenv integer_type_widths ~node_hash location symbol_table
formals mem
end
module Report = struct
module PO = BufferOverrunProofObligations

Write Preview
Loading…
Cancel
Save