From cb363d8dcb7d1aa2eae027e06ab6cba7e8fb50d6 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 22 Nov 2017 05:57:31 -0800 Subject: [PATCH] [inferbo] Modeled functions may also generate proof obligations Summary: A modeled function is not only an evaluator but also a checker, at least in Inferbo where both things happen in two passes. This diff just prepares for it without generating new alarms. Reviewed By: jvillard Differential Revision: D6373051 fbshipit-source-id: 264696f --- .../src/bufferoverrun/bufferOverrunChecker.ml | 4 +- .../src/bufferoverrun/bufferOverrunModels.ml | 175 +++++++++++------- .../bufferOverrunProofObligations.ml | 4 + 3 files changed, 111 insertions(+), 72 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 78c29abe7..f3eb0c453 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -265,8 +265,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Sem.prune exp mem | Call (ret, Const Cfun callee_pname, params, location, _) -> ( match Models.dispatcher callee_pname params with - | Some model -> - model callee_pname ret node location mem + | Some {Models.exec} -> + exec callee_pname ret node location mem | None -> match Summary.read_summary pdesc callee_pname with | Some summary -> diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index c03cf23d2..8c14ce69e 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -12,26 +12,24 @@ open AbsLoc open! AbstractDomain.Types module L = Logging module Dom = BufferOverrunDomain +module PO = BufferOverrunProofObligations module Trace = BufferOverrunTrace module TraceSet = Trace.Set module Make (CFG : ProcCfg.S) = struct module Sem = BufferOverrunSemantics.Make (CFG) - type model_fun = + type exec_fun = Typ.Procname.t -> (Ident.t * Typ.t) option -> CFG.node -> Location.t -> Dom.Mem.astate -> Dom.Mem.astate - let set_uninitialized node (typ: Typ.t) ploc mem = - match typ.desc with - | Tint _ | Tfloat _ -> - Dom.Mem.weak_update_heap ploc Dom.Val.Itv.top mem - | _ -> - L.(debug BufferOverrun Verbose) - "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp - (CFG.loc node) ; - mem + type check_fun = + Typ.Procname.t -> CFG.node -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t + -> PO.ConditionSet.t + + type model = {exec: exec_fun; check: check_fun} + let no_check _pname _node _location _mem cond_set = cond_set (* NOTE: heuristic *) let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t = function @@ -44,45 +42,71 @@ module Make (CFG : ProcCfg.S) = struct (Typ.mk (Typ.Tint Typ.IChar), Some 1, x) - let model_malloc (size_exp, _) pname ret node location mem = - match ret with - | Some (id, _) -> - let typ, stride, length0 = get_malloc_info size_exp in - let length = Sem.eval length0 mem in - let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in - let v = - Sem.eval_array_alloc pname node typ ?stride Itv.zero (Dom.Val.get_itv length) 0 1 - |> Dom.Val.set_traces traces - in - mem |> Dom.Mem.add_stack (Loc.of_id id) v - |> set_uninitialized node typ (Dom.Val.get_array_locs v) - | _ -> - L.(debug BufferOverrun Verbose) - "/!\\ Do not know where to model malloc at %a@\n" Location.pp (CFG.loc node) ; - mem + let check_alloc_size size_exp pname _node location mem cond_set = + let _, _, length0 = get_malloc_info size_exp in + let v_length = Sem.eval length0 mem in + let traces = Dom.Val.get_traces v_length in + let length = Dom.Val.get_itv v_length in + PO.ConditionSet.add_alloc_size pname location length traces cond_set - let model_realloc size_arg pname ret node location mem = - model_malloc size_arg pname ret node location mem - - - let model_min (e1, _) (e2, _) _pname ret _node _location mem = - match ret with - | Some (id, _) -> - let i1 = Sem.eval e1 mem |> Dom.Val.get_itv in - let i2 = Sem.eval e2 mem |> Dom.Val.get_itv in - let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in - mem |> Dom.Mem.add_stack (Loc.of_id id) v + let set_uninitialized node (typ: Typ.t) ploc mem = + match typ.desc with + | Tint _ | Tfloat _ -> + Dom.Mem.weak_update_heap ploc Dom.Val.Itv.top mem | _ -> + L.(debug BufferOverrun Verbose) + "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp + (CFG.loc node) ; mem - let model_set_size (e1, _) (e2, _) _pname _ret _node _location mem = - let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in - let size = Sem.eval e2 mem |> Dom.Val.get_itv in - let arr = Dom.Mem.find_heap_set locs mem in - let arr = Dom.Val.set_array_size size arr in - Dom.Mem.strong_update_heap locs arr mem + let malloc (size_exp, _) = + let exec pname ret node location mem = + match ret with + | Some (id, _) -> + let typ, stride, length0 = get_malloc_info size_exp in + let length = Sem.eval length0 mem in + let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in + let v = + Sem.eval_array_alloc pname node typ ?stride Itv.zero (Dom.Val.get_itv length) 0 1 + |> Dom.Val.set_traces traces + in + mem |> Dom.Mem.add_stack (Loc.of_id id) v + |> set_uninitialized node typ (Dom.Val.get_array_locs v) + | _ -> + L.(debug BufferOverrun Verbose) + "/!\\ Do not know where to model malloc at %a@\n" Location.pp (CFG.loc node) ; + mem + and check = check_alloc_size size_exp in + {exec; check} + + + let realloc = malloc + + let inferbo_min (e1, _) (e2, _) = + let exec _pname ret _node _location mem = + match ret with + | Some (id, _) -> + let i1 = Sem.eval e1 mem |> Dom.Val.get_itv in + let i2 = Sem.eval e2 mem |> Dom.Val.get_itv in + let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in + mem |> Dom.Mem.add_stack (Loc.of_id id) v + | _ -> + mem + in + {exec; check= no_check} + + + let inferbo_set_size (e1, _) (e2, _) = + let exec _pname _ret _node _location mem = + let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in + let size = Sem.eval e2 mem |> Dom.Val.get_itv in + let arr = Dom.Mem.find_heap_set locs mem in + let arr = Dom.Val.set_array_size size arr in + Dom.Mem.strong_update_heap locs arr mem + and check = check_alloc_size e2 in + {exec; check} let model_by_value value _pname ret _node _location mem = @@ -95,39 +119,50 @@ module Make (CFG : ProcCfg.S) = struct mem - let model_bottom _pname _ret _node _location _mem = Bottom + let by_value value = {exec= model_by_value value; check= no_check} - let model_infer_print (e, _) _pname _ret _node location mem = - L.(debug BufferOverrun Medium) - "@[=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ; - mem + let bottom = + let exec _pname _ret _node _location _mem = Bottom in + {exec; check= no_check} - let model_infer_set_array_length array (length_exp, _) pname _ret node _location mem = - match array with - | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)} -> - let length = Sem.eval length_exp mem |> Dom.Val.get_itv in - let stride = Option.map ~f:IntLit.to_int stride0 in - let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in - mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v - |> set_uninitialized node typ (Dom.Val.get_array_locs v) - | _ -> - L.(die InternalError) "Unexpected type of first argument for __set_array_length()" + let infer_print (e, _) = + let exec _pname _ret _node location mem = + L.(debug BufferOverrun Medium) + "@[=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ; + mem + in + {exec; check= no_check} + + + let set_array_length array (length_exp, _) = + let exec pname _ret node _location mem = + match array with + | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)} -> + let length = Sem.eval length_exp mem |> Dom.Val.get_itv in + let stride = Option.map ~f:IntLit.to_int stride0 in + let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in + mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v + |> set_uninitialized node typ (Dom.Val.get_array_locs v) + | _ -> + L.(die InternalError) "Unexpected type of first argument for __set_array_length()" + and check = check_alloc_size length_exp in + {exec; check} - let dispatcher : model_fun ProcnameDispatcher.dispatcher = + let dispatcher : model ProcnameDispatcher.dispatcher = let open ProcnameDispatcher in make_dispatcher - [ -"__inferbo_min" <>$ capt_arg $+ capt_arg $!--> model_min - ; -"__inferbo_set_size" <>$ capt_arg $+ capt_arg $!--> model_set_size - ; -"__exit" <>--> model_bottom - ; -"exit" <>--> model_bottom - ; -"fgetc" <>--> model_by_value Dom.Val.Itv.m1_255 - ; -"infer_print" <>$ capt_arg $!--> model_infer_print - ; -"malloc" <>$ capt_arg $+...$--> model_malloc - ; -"__new_array" <>$ capt_arg $+...$--> model_malloc - ; -"realloc" <>$ any_arg $+ capt_arg $+...$--> model_realloc - ; -"__set_array_length" <>$ capt_arg $+ capt_arg $!--> model_infer_set_array_length - ; -"strlen" <>--> model_by_value Dom.Val.Itv.nat ] + [ -"__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 diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 5c8d3b146..8ef16be24 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -283,6 +283,10 @@ module ConditionSet = struct join [cwt] condset + let add_alloc_size _pname _location _size _val_traces _condset = + L.(die InternalError) "Not implemented add_alloc_size" + + let subst condset (bound_map, trace_map) caller_pname callee_pname location = let subst_add_cwt condset cwt = match Condition.get_symbols cwt.cond with