[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

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 ->
+          | Some {Models.exec} ->
-              model callee_pname ret node location mem
+              exec callee_pname ret node location mem
           | None ->
             match Summary.read_summary pdesc callee_pname with
             | Some summary ->

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 =
+  type check_fun =
-    match typ.desc with
+    Typ.Procname.t -> CFG.node -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t
-    | Tint _ | Tfloat _ ->
+    -> PO.ConditionSet.t
-        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 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,7 +42,27 @@ 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 =
+  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 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 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
@@ -60,13 +78,14 @@ module Make (CFG : ProcCfg.S) = struct
           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 model_realloc size_arg pname ret node location mem =
+  let realloc = malloc
-    model_malloc size_arg pname ret node location mem
 
-
+  let inferbo_min (e1, _) (e2, _) =
-  let model_min (e1, _) (e2, _) _pname ret _node _location mem =
+    let exec _pname ret _node _location mem =
       match ret with
       | Some (id, _) ->
           let i1 = Sem.eval e1 mem |> Dom.Val.get_itv in
@@ -75,14 +94,19 @@ module Make (CFG : ProcCfg.S) = struct
           mem |> Dom.Mem.add_stack (Loc.of_id id) v
       | _ ->
           mem
+    in
+    {exec; check= no_check}
 
 
-  let model_set_size (e1, _) (e2, _) _pname _ret _node _location mem =
+  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,15 +119,24 @@ 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 =
+  let bottom =
+    let exec _pname _ret _node _location _mem = Bottom in
+    {exec; check= no_check}
+
+
+  let infer_print (e, _) =
+    let exec _pname _ret _node location mem =
       L.(debug BufferOverrun Medium)
         "@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ;
       mem
+    in
+    {exec; check= no_check}
 
 
-  let model_infer_set_array_length array (length_exp, _) pname _ret node _location mem =
+  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
@@ -113,21 +146,23 @@ module Make (CFG : ProcCfg.S) = struct
           |> 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_min" <>$ capt_arg $+ capt_arg $!--> inferbo_min
-      ; -"__inferbo_set_size" <>$ capt_arg $+ capt_arg $!--> model_set_size
+      ; -"__inferbo_set_size" <>$ capt_arg $+ capt_arg $!--> inferbo_set_size
-      ; -"__exit" <>--> model_bottom
+      ; -"__exit" <>--> bottom
-      ; -"exit" <>--> model_bottom
+      ; -"exit" <>--> bottom
-      ; -"fgetc" <>--> model_by_value Dom.Val.Itv.m1_255
+      ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255
-      ; -"infer_print" <>$ capt_arg $!--> model_infer_print
+      ; -"infer_print" <>$ capt_arg $!--> infer_print
-      ; -"malloc" <>$ capt_arg $+...$--> model_malloc
+      ; -"malloc" <>$ capt_arg $+...$--> malloc
-      ; -"__new_array" <>$ capt_arg $+...$--> model_malloc
+      ; -"__new_array" <>$ capt_arg $+...$--> malloc
-      ; -"realloc" <>$ any_arg $+ capt_arg $+...$--> model_realloc
+      ; -"realloc" <>$ any_arg $+ capt_arg $+...$--> realloc
-      ; -"__set_array_length" <>$ capt_arg $+ capt_arg $!--> model_infer_set_array_length
+      ; -"__set_array_length" <>$ capt_arg $+ capt_arg $!--> set_array_length
-      ; -"strlen" <>--> model_by_value Dom.Val.Itv.nat ]
+      ; -"strlen" <>--> by_value Dom.Val.Itv.nat ]
 
 end

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