From 0ed1a51944c56c4b7701b1bdfcf0dfe892d43da3 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 4 Dec 2017 03:39:34 -0800 Subject: [PATCH] [inferbo] Prepare for type models Reviewed By: skcho Differential Revision: D6408369 fbshipit-source-id: 43be92a --- .../src/bufferoverrun/bufferOverrunChecker.ml | 31 ++++++++---- .../src/bufferoverrun/bufferOverrunModels.ml | 49 +++++++++++++------ 2 files changed, 55 insertions(+), 25 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 638b958a5..d997b271f 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -70,14 +70,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let offset = Itv.zero in BoUtils.Exec.decl_sym_arr ~decl_sym_val pname tenv node location ~depth loc typ ~offset ?size ~inst_num ~new_sym_num ~new_alloc_num mem - | Typ.Tstruct typename -> - let decl_fld mem (fn, typ, _) = - let loc_fld = Loc.append_field loc fn in - decl_sym_val pname tenv node location ~depth loc_fld typ mem - in - let decl_flds str = List.fold ~f:decl_fld ~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 + | Typ.Tstruct typename -> ( + match Models.TypName.dispatch typename with + | Some {Models.declare_symbolic} -> + declare_symbolic ~decl_sym_val pname tenv node location ~depth loc ~inst_num + ~new_sym_num ~new_alloc_num mem + | None -> + let decl_fld mem (fn, typ, _) = + let loc_fld = Loc.append_field loc fn in + decl_sym_val pname tenv node location ~depth loc_fld typ mem + in + let decl_flds str = List.fold ~f:decl_fld ~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) @@ -215,7 +220,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Prune (exp, _, _, _) -> Sem.prune exp mem | Call (ret, Const Cfun callee_pname, params, location, _) -> ( - match Models.dispatcher callee_pname params with + match Models.Procname.dispatch callee_pname params with | Some {Models.exec} -> exec callee_pname ret node location mem | None -> @@ -237,6 +242,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let stride = Option.map ~f:IntLit.to_int stride0 in BoUtils.Exec.decl_local_array ~decl_local pname node location loc typ ~length ?stride ~inst_num ~dimension mem + | Typ.Tstruct typname -> ( + match Models.TypName.dispatch typname with + | Some {Models.declare_local} -> + declare_local ~decl_local pname node location loc ~inst_num ~dimension mem + | None -> + (mem, inst_num) ) | _ -> (mem, inst_num) in @@ -385,7 +396,7 @@ module Report = struct | Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) -> add_condition pname exp location mem cond_set | Sil.Call (_, Const Cfun callee_pname, params, location, _) -> ( - match Models.dispatcher callee_pname params with + match Models.Procname.dispatch callee_pname params with | Some {Models.check} -> check pname node location mem cond_set | None -> diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 4511cf7b4..3f614fa5c 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -30,6 +30,17 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct type model = {exec: exec_fun; check: check_fun} + type declare_local_fun = + decl_local:BoUtils.Exec.decl_local -> Typ.Procname.t -> CFG.node -> Location.t -> Loc.t + -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int + + type declare_symbolic_fun = + decl_sym_val:BoUtils.Exec.decl_sym_val -> Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t + -> depth:int -> Loc.t -> inst_num:int -> new_sym_num:BoUtils.counter + -> new_alloc_num:BoUtils.counter -> Dom.Mem.astate -> Dom.Mem.astate + + type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun} + let no_check _pname _node _location _mem cond_set = cond_set (* NOTE: heuristic *) @@ -154,19 +165,27 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct {exec; check} - let dispatcher : model ProcnameDispatcher.dispatcher = - let open ProcnameDispatcher.Procname in - make_dispatcher - [ -"__inferbo_min" <>$ capt_arg $+ capt_arg $!--> inferbo_min - ; -"__inferbo_set_size" <>$ capt_arg $+ capt_arg $!--> inferbo_set_size - ; -"__exit" <>--> bottom - ; -"exit" <>--> bottom - ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255 - ; -"infer_print" <>$ capt_arg $!--> infer_print - ; -"malloc" <>$ capt_arg $+...$--> malloc - ; -"__new_array" <>$ capt_arg $+...$--> malloc - ; -"realloc" <>$ any_arg $+ capt_arg $+...$--> realloc - ; -"__set_array_length" <>$ capt_arg $+ capt_arg $!--> set_array_length - ; -"strlen" <>--> by_value Dom.Val.Itv.nat ] - + module Procname = struct + let dispatch : model ProcnameDispatcher.dispatcher = + let open ProcnameDispatcher.Procname in + make_dispatcher + [ -"__inferbo_min" <>$ capt_arg $+ capt_arg $!--> inferbo_min + ; -"__inferbo_set_size" <>$ capt_arg $+ capt_arg $!--> inferbo_set_size + ; -"__exit" <>--> bottom + ; -"exit" <>--> bottom + ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255 + ; -"infer_print" <>$ capt_arg $!--> infer_print + ; -"malloc" <>$ capt_arg $+...$--> malloc + ; -"__new_array" <>$ capt_arg $+...$--> malloc + ; -"realloc" <>$ any_arg $+ capt_arg $+...$--> realloc + ; -"__set_array_length" <>$ capt_arg $+ capt_arg $!--> set_array_length + ; -"strlen" <>--> by_value Dom.Val.Itv.nat ] + + end + + module TypName = struct + let dispatch : typ_model ProcnameDispatcher.typ_dispatcher = + ProcnameDispatcher.TypName.make_dispatcher [] + + end end