From 2dcd93204cd14c50446c5730b2b71464993c8293 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 27 Mar 2016 15:11:40 -0700 Subject: [PATCH] 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 | 63 ++++++++++++++++++++++ infer/src/backend/builtin.mli | 41 ++++++++++++++ infer/src/backend/inferanalyze.ml | 2 +- infer/src/backend/inferconfig.ml | 2 +- infer/src/backend/symExec.ml | 65 +---------------------- infer/src/backend/symExec.mli | 6 --- infer/src/checkers/dataflow.ml | 2 +- infer/src/checkers/performanceCritical.ml | 4 +- infer/src/clang/cTrans.ml | 4 +- infer/src/eradicate/typeCheck.ml | 4 +- infer/src/java/jTrans.ml | 2 +- 11 files changed, 116 insertions(+), 79 deletions(-) create mode 100644 infer/src/backend/builtin.ml create mode 100644 infer/src/backend/builtin.mli diff --git a/infer/src/backend/builtin.ml b/infer/src/backend/builtin.ml new file mode 100644 index 000000000..c233e9ea2 --- /dev/null +++ b/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 diff --git a/infer/src/backend/builtin.mli b/infer/src/backend/builtin.mli new file mode 100644 index 000000000..95b0deab6 --- /dev/null +++ b/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 *) diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index 6399ae0bb..a6bc11a8b 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/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" ; diff --git a/infer/src/backend/inferconfig.ml b/infer/src/backend/inferconfig.ml index e107e18fb..658c4e9ad 100644 --- a/infer/src/backend/inferconfig.ml +++ b/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 diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index ad48bf3aa..131cff262 100644 --- a/infer/src/backend/symExec.ml +++ b/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; diff --git a/infer/src/backend/symExec.mli b/infer/src/backend/symExec.mli index af3da4493..f2476f4ce 100644 --- a/infer/src/backend/symExec.mli +++ b/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 diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index 9db6c7610..5d267be89 100644 --- a/infer/src/checkers/dataflow.ml +++ b/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 diff --git a/infer/src/checkers/performanceCritical.ml b/infer/src/checkers/performanceCritical.ml index c844fb296..7526cf47b 100644 --- a/infer/src/checkers/performanceCritical.ml +++ b/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 diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 63a1bb52e..09ee10465 100644 --- a/infer/src/clang/cTrans.ml +++ b/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 diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index c9eaa6b8f..9fa660c73 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/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, diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 1342a3915..6028bbf82 100644 --- a/infer/src/java/jTrans.ml +++ b/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 =