[inferbo] Prepare for type models

Reviewed By: skcho

Differential Revision: D6408369

fbshipit-source-id: 43be92a

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 ->

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