diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 2005a848b..dc26cd0ad 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -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