Refactor SymExec.Builtin into toplevel module

Summary:public
This will allow SymExec to depend on Inferconfig with introducing
circular dependencies, as Inferconfig calls Builtin.is_registered.

Reviewed By: jeremydubreil

Differential Revision: D3100614

fb-gh-sync-id: 786cf62
fbshipit-source-id: 786cf62

infer/src/backend/builtin.ml

@@ -0,0 +1,63 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+(** Module for builtin functions with their symbolic execution handler *)
+
+type args = {
+  pdesc : Cfg.Procdesc.t;
+  instr : Sil.instr;
+  tenv : Sil.tenv;
+  prop_ : Prop.normal Prop.t;
+  path : Paths.Path.t;
+  ret_ids : Ident.t list;
+  args : (Sil.exp * Sil.typ) list;
+  proc_name : Procname.t;
+  loc : Location.t;
+}
+
+type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list
+
+type t = args -> ret_typ
+
+(* builtin function names for which we do symbolic execution *)
+let builtin_functions = Procname.Hash.create 4
+
+(* Check if the function is a builtin *)
+let is_registered name =
+  Procname.Hash.mem builtin_functions name
+
+(* get the symbolic execution handler associated to the builtin function name *)
+let get name : t =
+  try Procname.Hash.find builtin_functions name
+  with Not_found -> assert false
+
+(* register a builtin function name and symbolic execution handler *)
+let register proc_name_str (sym_exe_fun: t) =
+  let proc_name = Procname.from_string_c_fun proc_name_str in
+  Procname.Hash.replace builtin_functions proc_name sym_exe_fun;
+  proc_name
+
+(* register a builtin [Procname.t] and symbolic execution handler *)
+let register_procname proc_name (sym_exe_fun: t) =
+  Procname.Hash.replace builtin_functions proc_name sym_exe_fun
+
+(** print the functions registered *)
+let pp_registered fmt () =
+  let builtin_names = ref [] in
+  Procname.Hash.iter (fun name _ -> builtin_names := name :: !builtin_names) builtin_functions;
+  builtin_names := IList.sort Procname.compare !builtin_names;
+  let pp pname = Format.fprintf fmt "%a@\n" Procname.pp pname in
+  Format.fprintf fmt "Registered builtins:@\n  @[";
+  IList.iter pp !builtin_names;
+  Format.fprintf fmt "@]@."
+
+(** print the builtin functions and exit *)
+let print_and_exit () =
+  pp_registered Format.std_formatter ();
+  exit 0

infer/src/backend/builtin.mli

@@ -0,0 +1,41 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+(** Module for builtin functions with their symbolic execution handler *)
+
+type args = {
+  pdesc : Cfg.Procdesc.t;
+  instr : Sil.instr;
+  tenv : Sil.tenv;
+  prop_ : Prop.normal Prop.t;
+  path : Paths.Path.t;
+  ret_ids : Ident.t list;
+  args : (Sil.exp * Sil.typ) list;
+  proc_name : Procname.t;
+  loc : Location.t;
+}
+
+type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list
+
+type t = args -> ret_typ
+
+val register : string -> t -> Procname.t
+(** Register a builtin function name and symbolic execution handler *)
+
+val register_procname : Procname.t -> t -> unit
+(** Register a builtin [Procname.t] and symbolic execution handler *)
+
+val is_registered : Procname.t -> bool
+(** Check if the function is a builtin *)
+
+val get : Procname.t -> t
+(** Get the symbolic execution handler associated to the builtin function name *)
+
+val print_and_exit : unit -> 'a
+(** Print the builtin functions and exit *)

infer/src/backend/inferanalyze.ml

@@ -73,7 +73,7 @@ let arg_desc =
         "use file for the out channel"
         ;
         "-print_builtins",
-        Arg.Unit SymExec.print_builtins,
+        Arg.Unit Builtin.print_and_exit,
         None,
         "print the builtin functions and exit"
         ;

infer/src/backend/inferconfig.ml

@@ -153,7 +153,7 @@ let load_patterns json_key inferconfig =
 
 (** Check if a proc name is matching the name given as string. *)
 let match_method language proc_name method_name =
-  not (SymExec.function_is_builtin proc_name) &&
+  not (Builtin.is_registered proc_name) &&
   Procname.get_language proc_name = language &&
   Procname.get_method proc_name = method_name
 

infer/src/backend/symExec.ml

@@ -248,67 +248,6 @@ let update_iter iter pi sigma =
   let iter' = Prop.prop_iter_update_current_by_list iter sigma in
   IList.fold_left (Prop.prop_iter_add_atom false) iter' pi
 
-(** Module for builtin functions with their symbolic execution handler *)
-module Builtin = struct
-  type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list
-
-  type builtin_args =
-    {
-      pdesc : Cfg.Procdesc.t;
-      instr : Sil.instr;
-      tenv : Sil.tenv;
-      prop_ : Prop.normal Prop.t;
-      path : Paths.Path.t;
-      ret_ids : Ident.t list;
-      args : (Sil.exp * Sil.typ) list;
-      proc_name : Procname.t;
-      loc : Location.t;
-    }
-
-  type sym_exe_builtin = builtin_args -> ret_typ
-
-  (* builtin function names for which we do symbolic execution *)
-  let builtin_functions = Procname.Hash.create 4
-
-  (* Check if the function is a builtin *)
-  let is_registered name =
-    Procname.Hash.mem builtin_functions name
-
-  (* get the symbolic execution handler associated to the builtin function name *)
-  let get_sym_exe_builtin name : sym_exe_builtin =
-    try Procname.Hash.find builtin_functions name
-    with Not_found -> assert false
-
-  (* register a builtin function name and symbolic execution handler *)
-  let register proc_name_str (sym_exe_fun: sym_exe_builtin) =
-    let proc_name = Procname.from_string_c_fun proc_name_str in
-    Procname.Hash.replace builtin_functions proc_name sym_exe_fun;
-    proc_name
-
-  (* register a builtin [Procname.t] and symbolic execution handler *)
-  let register_procname proc_name (sym_exe_fun: sym_exe_builtin) =
-    Procname.Hash.replace builtin_functions proc_name sym_exe_fun
-
-  (** print the functions registered *)
-  let pp_registered fmt () =
-    let builtin_names = ref [] in
-    Procname.Hash.iter (fun name _ -> builtin_names := name :: !builtin_names) builtin_functions;
-    builtin_names := IList.sort Procname.compare !builtin_names;
-    let pp pname = Format.fprintf fmt "%a@\n" Procname.pp pname in
-    Format.fprintf fmt "Registered builtins:@\n  @[";
-    IList.iter pp !builtin_names;
-    Format.fprintf fmt "@]@."
-
-end
-
-(** print the builtin functions and exit *)
-let print_builtins () =
-  Builtin.pp_registered Format.std_formatter ();
-  exit 0
-
-(** Check if the function is a builtin *)
-let function_is_builtin = Builtin.is_registered
-
 (** Precondition: se should not include hpara_psto
     that could mean nonempty heaps. *)
 let rec execute_nullify_se = function
@@ -1084,8 +1023,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       let n_cond, prop = exp_norm_check_arith current_pname prop__ cond in
       ret_old_path (Propset.to_proplist (prune_prop n_cond prop))
   | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), args, loc, _)
-    when function_is_builtin callee_pname ->
-      let sym_exe_builtin = Builtin.get_sym_exe_builtin callee_pname in
+    when Builtin.is_registered callee_pname ->
+      let sym_exe_builtin = Builtin.get callee_pname in
       sym_exe_builtin
         {
           pdesc = current_pdesc;

infer/src/backend/symExec.mli

@@ -13,12 +13,6 @@
 (** Lookup Java types by name. *)
 val lookup_java_typ_from_string :  Sil.tenv -> string -> Sil.typ
 
-(** print the builtin functions and exit *)
-val print_builtins : unit -> unit
-
-(** Check if the function is a builtin *)
-val function_is_builtin : Procname.t -> bool
-
 (** symbolic execution on the level of sets of propositions *)
 val lifted_sym_exec : (exn -> unit) -> Sil.tenv -> Cfg.Procdesc.t ->
   Paths.PathSet.t -> Cfg.Node.t -> Sil.instr list -> Paths.PathSet.t

infer/src/checkers/dataflow.ml

@@ -50,7 +50,7 @@ let node_throws node (proc_throws : Procname.t -> throws) : throws =
         (* assignment to return variable is an artifact of a throw instruction *)
         Throws
     | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, _, _)
-      when SymExec.function_is_builtin callee_pn ->
+      when Builtin.is_registered callee_pn ->
         if Procname.equal callee_pn SymExec.ModelBuiltins.__cast
         then DontKnow
         else DoesNotThrow

infer/src/checkers/performanceCritical.ml

@@ -31,7 +31,7 @@ let is_modeled_expensive =
           Inferconfig.ModeledExpensiveMatcher.load_matcher config_file) in
   fun tenv proc_name -> match proc_name with
     | Procname.Java proc_name_java ->
-        not (SymExec.function_is_builtin proc_name) &&
+        not (Builtin.is_registered proc_name) &&
         let classname =
           Typename.Java.from_string (Procname.java_get_class_name proc_name_java) in
         (Lazy.force matcher) (AndroidFramework.is_subclass tenv classname) proc_name
@@ -123,7 +123,7 @@ let is_allocator tenv pname = match pname with
           Typename.Java.from_string (Procname.java_get_class_name pname_java) in
         AndroidFramework.is_throwable tenv class_name in
       Procname.is_constructor pname
-      && not (SymExec.function_is_builtin pname)
+      && not (Builtin.is_registered pname)
       && not (is_throwable ())
   | _ ->
       false

infer/src/clang/cTrans.ml

@@ -442,7 +442,7 @@ struct
           !CFrontend_config.language = CFrontend_config.OBJCPP) then
         SymExec.ModelBuiltins.malloc_no_fail
       else Procname.from_string_c_fun name in
-    let is_builtin = SymExec.function_is_builtin non_mangled_func_name in
+    let is_builtin = Builtin.is_registered non_mangled_func_name in
     if is_builtin then (* malloc, free, exit, scanf, ... *)
       { empty_res_trans with exps = [(Sil.Const (Sil.Cfun non_mangled_func_name), typ)] }
     else
@@ -849,7 +849,7 @@ struct
           (match callee_pname_opt with
            | Some callee_pname ->
                let open CContext in
-               if not (SymExec.function_is_builtin callee_pname) then
+               if not (Builtin.is_registered callee_pname) then
                  begin
                    Cg.add_edge context.cg procname callee_pname;
                  end

infer/src/eradicate/typeCheck.ml

@@ -73,7 +73,7 @@ module ComplexExpressions = struct
     procname_optional_isPresent pn ||
     procname_instanceof pn ||
     procname_containsKey pn ||
-    SymExec.function_is_builtin pn
+    Builtin.is_registered pn
 
 
   exception Not_handled
@@ -557,7 +557,7 @@ let typecheck_instr
           [loc]
         )
         typestate
-  | Sil.Call (_, Sil.Const (Sil.Cfun pn), _, _, _) when SymExec.function_is_builtin pn ->
+  | Sil.Call (_, Sil.Const (Sil.Cfun pn), _, _, _) when Builtin.is_registered pn ->
       typestate (* skip othe builtins *)
   | Sil.Call
       (ret_ids,

infer/src/java/jTrans.ml

@@ -589,7 +589,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
   let callee_procname =
     let proc = Procname.from_string_c_fun (JBasics.ms_name ms) in
     if JBasics.cn_equal cn' JConfig.infer_builtins_cl &&
-       SymExec.function_is_builtin proc
+       Builtin.is_registered proc
     then proc
     else Procname.Java (JTransType.get_method_procname cn' ms method_kind) in
   let call_idl, call_instrs =