[inferbo] Use a dispatcher for models

Summary: : As we want to model many C++ methods, using a lot of matchers with `if / else if` will be tiring. This diff introduces a dispatcher which is a nicer way to write the same thing. No new model for now, just a refactoring. Ideally we'd need a parser generator for C++ names... Reviewed By: jvillard Differential Revision: D6209234 fbshipit-source-id: 49fae5e
7 years ago · eb33fb7a97
parent 8274453277
commit eb33fb7a97
3 changed files with 108 additions and 99 deletions
--- a/infer/src/IR/QualifiedCppName.ml
+++ b/infer/src/IR/QualifiedCppName.ml
@ -72,10 +72,8 @@ module Match = struct


  let qualifiers_list_matcher quals_list =
-    ( if List.is_empty quals_list then "a^"
-    else
-      (* regexp that does not match anything *)
-      List.map ~f:regexp_string_of_qualifiers quals_list |> String.concat ~sep:"\\|" )
+    ( if List.is_empty quals_list then "a^" (* regexp that does not match anything *)
+    else List.rev_map ~f:regexp_string_of_qualifiers quals_list |> String.concat ~sep:"\\|" )
    |> Str.regexp


@ -92,7 +90,7 @@ module Match = struct


  let of_fuzzy_qual_names fuzzy_qual_names =
-    List.map fuzzy_qual_names ~f:qualifiers_of_fuzzy_qual_name |> qualifiers_list_matcher
+    List.rev_map fuzzy_qual_names ~f:qualifiers_of_fuzzy_qual_name |> qualifiers_list_matcher


  let match_qualifiers matcher quals =
@ -102,3 +100,18 @@ module Match = struct
    Str.string_match matcher (to_separated_string ~sep:matching_separator normalized_qualifiers) 0

 end
+
+module Dispatch = struct
+  (* Simple implementation of a dispatcher, could be much more optimized *)
+
+  type 'a quals_dispatcher = (Match.quals_matcher * 'a) list
+
+  let of_fuzzy_qual_names fqnames_val_pairs =
+    List.map fqnames_val_pairs ~f:(fun (fqns, v) -> (Match.of_fuzzy_qual_names fqns, v))
+
+
+  let dispatch_qualifiers dispatcher quals =
+    List.find_map dispatcher ~f:(fun (matcher, v) ->
+        Option.some_if (Match.match_qualifiers matcher quals) v )
+
+end
--- a/infer/src/IR/QualifiedCppName.mli
+++ b/infer/src/IR/QualifiedCppName.mli
@ -85,3 +85,11 @@ module Match : sig

  val match_qualifiers : quals_matcher -> t -> bool
 end
+
+module Dispatch : sig
+  type 'a quals_dispatcher
+
+  val of_fuzzy_qual_names : (string list * 'a) list -> 'a quals_dispatcher
+
+  val dispatch_qualifiers : 'a quals_dispatcher -> t -> 'a option
+end
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@ -59,62 +59,56 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
        (Typ.mk (Typ.Tint Typ.IChar), Some 1, x)


-  let model_malloc
-      : Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node
-        -> Location.t -> Dom.Mem.astate -> Dom.Mem.astate =
-    fun pname ret params node location mem ->
-      match ret with
-      | Some (id, _) ->
-          let typ, stride, length0 = get_malloc_info (List.hd_exn params |> fst) in
-          let length = Sem.eval length0 mem (CFG.loc node) 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
+  type model_fun =
+    Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node -> Location.t
+    -> Dom.Mem.astate -> Dom.Mem.astate

+  let model_malloc pname ret params node location mem =
+    match ret with
+    | Some (id, _) ->
+        let typ, stride, length0 = get_malloc_info (List.hd_exn params |> fst) in
+        let length = Sem.eval length0 mem (CFG.loc node) 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 model_realloc
-      : Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node
-        -> Location.t -> Dom.Mem.astate -> Dom.Mem.astate =
-    fun pname ret params node location mem ->
-      model_malloc pname ret (List.tl_exn params) node location mem

+  let model_realloc pname ret params node location mem =
+    model_malloc pname ret (List.tl_exn params) node location mem

-  let model_min
-      : (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> Location.t -> Dom.Mem.astate
-        -> Dom.Mem.astate =
-    fun ret params location mem ->
-      match (ret, params) with
-      | Some (id, _), [(e1, _); (e2, _)] ->
-          let i1 = Sem.eval e1 mem location |> Dom.Val.get_itv in
-          let i2 = Sem.eval e2 mem location |> 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

+  let model_min _pname ret params _node location mem =
+    match (ret, params) with
+    | Some (id, _), [(e1, _); (e2, _)] ->
+        let i1 = Sem.eval e1 mem location |> Dom.Val.get_itv in
+        let i2 = Sem.eval e2 mem location |> 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

-  let model_set_size : (Exp.t * Typ.t) list -> Location.t -> Dom.Mem.astate -> Dom.Mem.astate =
-    fun params location mem ->
-      match params with
-      | [(e1, _); (e2, _)] ->
-          let locs = Sem.eval_locs e1 mem location |> Dom.Val.get_pow_loc in
-          let size = Sem.eval e2 mem location |> 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
-      | _ ->
-          mem
+
+  let model_set_size _pname _ret params _node location mem =
+    match params with
+    | [(e1, _); (e2, _)] ->
+        let locs = Sem.eval_locs e1 mem location |> Dom.Val.get_pow_loc in
+        let size = Sem.eval e2 mem location |> 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
+    | _ ->
+        mem


-  let model_by_value value ret mem =
+  let model_by_value value _pname ret _params _node _location mem =
    match ret with
    | Some (id, _) ->
        Dom.Mem.add_stack (Loc.of_id id) value mem
@ -124,22 +118,23 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
        mem


-  let model_infer_print : (Exp.t * Typ.t) list -> Dom.Mem.astate -> Location.t -> Dom.Mem.astate =
-    fun params mem loc ->
-      match params with
-      | (e, _) :: _ ->
-          L.(debug BufferOverrun Medium)
-            "@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp loc Dom.Val.pp
-            (Sem.eval e mem loc) ;
-          mem
-      | _ ->
-          mem
+  let model_bottom _pname _ret _params _node _location _mem = Bottom
+
+  let model_infer_print _pname _ret params _node location mem =
+    match params with
+    | (e, _) :: _ ->
+        L.(debug BufferOverrun Medium)
+          "@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp
+          (Sem.eval e mem location) ;
+        mem
+    | _ ->
+        mem


-  let model_infer_set_array_length pname node params mem loc =
+  let model_infer_set_array_length pname _ret params node location mem =
    match params with
    | [(Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)}); (length_exp, _)] ->
-        let length = Sem.eval length_exp mem loc |> Dom.Val.get_itv in
+        let length = Sem.eval length_exp mem location |> 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
@ -150,33 +145,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
        L.(die InternalError) "Unexpected number of arguments for __set_array_length()"


-  let handle_unknown_call
-      : Typ.Procname.t -> (Ident.t * Typ.t) option -> Typ.Procname.t -> (Exp.t * Typ.t) list
-        -> CFG.node -> Dom.Mem.astate -> Location.t -> Dom.Mem.astate =
-    fun pname ret callee_pname params node mem loc ->
-      match Typ.Procname.get_method callee_pname with
-      | "__inferbo_min" ->
-          model_min ret params loc mem
-      | "__inferbo_set_size" ->
-          model_set_size params loc mem
-      | "__exit" | "exit" ->
-          Bottom
-      | "fgetc" ->
-          model_by_value Dom.Val.Itv.m1_255 ret mem
-      | "infer_print" ->
-          model_infer_print params mem loc
-      | "malloc" | "__new_array" ->
-          model_malloc pname ret params node loc mem
-      | "realloc" ->
-          model_realloc pname ret params node loc mem
-      | "__set_array_length" ->
-          model_infer_set_array_length pname node params mem loc
-      | "strlen" ->
-          model_by_value Dom.Val.Itv.nat ret mem
-      | proc_name ->
-          L.(debug BufferOverrun Verbose)
-            "/!\\ Unknown call to %s at %a@\n" proc_name Location.pp loc ;
-          model_by_value Dom.Val.unknown ret mem |> Dom.Mem.add_heap Loc.unknown Dom.Val.unknown
+  let model_dispatcher : model_fun QualifiedCppName.Dispatch.quals_dispatcher =
+    QualifiedCppName.Dispatch.of_fuzzy_qual_names
+      [ (["__inferbo_min"], model_min)
+      ; (["__inferbo_set_size"], model_set_size)
+      ; (["__exit"; "exit"], model_bottom)
+      ; (["fgetc"], model_by_value Dom.Val.Itv.m1_255)
+      ; (["infer_print"], model_infer_print)
+      ; (["malloc"; "__new_array"], model_malloc)
+      ; (["realloc"], model_realloc)
+      ; (["__set_array_length"], model_infer_set_array_length)
+      ; (["strlen"], model_by_value Dom.Val.Itv.nat) ]


  let rec declare_array
@ -405,13 +384,22 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
            else mem
        | Prune (exp, loc, _, _) ->
            Sem.prune exp loc mem
-        | Call (ret, Const Cfun callee_pname, params, loc, _) -> (
-          match Summary.read_summary pdesc callee_pname with
-          | Some summary ->
-              let callee = extras callee_pname in
-              instantiate_mem tenv ret callee callee_pname params mem summary loc
-          | None ->
-              handle_unknown_call pname ret callee_pname params node mem loc )
+        | Call (ret, Const Cfun callee_pname, params, loc, _)
+          -> (
+            let quals = Typ.Procname.get_qualifiers callee_pname in
+            match QualifiedCppName.Dispatch.dispatch_qualifiers model_dispatcher quals with
+            | Some model ->
+                model callee_pname ret params node loc mem
+            | None ->
+              match Summary.read_summary pdesc callee_pname with
+              | Some summary ->
+                  let callee = extras callee_pname in
+                  instantiate_mem tenv ret callee callee_pname params mem summary loc
+              | None ->
+                  L.(debug BufferOverrun Verbose)
+                    "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp loc ;
+                  model_by_value Dom.Val.unknown callee_pname ret params node loc mem
+                  |> Dom.Mem.add_heap Loc.unknown Dom.Val.unknown )
        | Declare_locals (locals, location) ->
            (* array allocation in stack e.g., int arr[10] *)
            let try_decl_arr location (mem, inst_num) (pvar, typ) =