From 46592ffdd928af0946dfff6a75e6bfaf56600611 Mon Sep 17 00:00:00 2001 From: Andrzej Kotulski Date: Fri, 28 Oct 2016 17:12:34 -0700 Subject: [PATCH] [backend] Split construction of builtin pnames and builtin registration Summary: this makes frontends no longer depend on SymExec.ml. `ModelBuiltins` was split into two modules: - `BuiltinDecl` with procnames for builtins (used to determine whether some function is a builtin) - `BuiltinDefn` with implementations used by `SymExec` - they both have similar type defined in `BUILTINS.S` which makes sure that new builtin gets added into both modules. During the refactor I ran some scripts: `BuiltinDecl.ml`: let X = create_procname "X" cat BuiltinDecl.ml | grep "create_procname" | tail -70 | awk ' { print $1,$2,$3,$4,"\42"$2"\42"} ' then manually confirm string match. Exceptions: "__exit" -> "_exit" "objc_cpp_throw" -> "__infer_objc_cpp_throw" __objc_dictionary_literal nsArray_arrayWithObjects nsArray_arrayWithObjectsCount `BuiltinDefn.ml`: let X = Builtin.register BuiltinDecl.X execute_X cat BuiltinDecl.ml | grep "create_procname" | tail -70 | awk ' { print $1,$2,$3,"Builtin.register BuiltinDecl."$2,"execute_"$2} ' then, fix all compilation problems Reviewed By: jberdine Differential Revision: D3951035 fbshipit-source-id: f059602 --- infer/src/IR/BUILTINS.mli | 85 ++++ infer/src/IR/BuiltinDecl.ml | 100 +++++ infer/src/IR/BuiltinDecl.mli | 15 + .../{modelBuiltins.ml => BuiltinDefn.ml} | 405 ++++++++---------- infer/src/backend/BuiltinDefn.mli | 18 + infer/src/backend/InferAnalyze.re | 1 + infer/src/backend/builtin.ml | 27 +- infer/src/backend/builtin.mli | 7 +- infer/src/backend/inferconfig.ml | 2 +- infer/src/backend/modelBuiltins.mli | 49 --- infer/src/backend/symExec.ml | 2 +- infer/src/checkers/ThreadSafety.ml | 4 +- infer/src/checkers/annotationReachability.ml | 4 +- infer/src/checkers/dataflow.ml | 4 +- infer/src/checkers/repeatedCallsChecker.ml | 4 +- infer/src/clang/ast_expressions.ml | 2 +- infer/src/clang/cArithmetic_trans.ml | 6 +- infer/src/clang/cTrans.ml | 22 +- infer/src/clang/cTrans_models.ml | 14 +- infer/src/clang/cTrans_utils.ml | 14 +- infer/src/eradicate/eradicateChecks.ml | 2 +- infer/src/eradicate/typeCheck.ml | 14 +- infer/src/harness/inhabit.ml | 4 +- infer/src/java/jTrans.ml | 26 +- infer/src/java/jTransExn.ml | 4 +- infer/src/quandary/CppTrace.ml | 4 +- infer/src/quandary/JavaTaintAnalysis.ml | 2 +- infer/src/quandary/JavaTrace.ml | 4 +- infer/src/quandary/TaintAnalysis.ml | 4 +- infer/src/unit/analyzerTester.ml | 2 +- 30 files changed, 492 insertions(+), 359 deletions(-) create mode 100644 infer/src/IR/BUILTINS.mli create mode 100644 infer/src/IR/BuiltinDecl.ml create mode 100644 infer/src/IR/BuiltinDecl.mli rename infer/src/backend/{modelBuiltins.ml => BuiltinDefn.ml} (82%) create mode 100644 infer/src/backend/BuiltinDefn.mli delete mode 100644 infer/src/backend/modelBuiltins.mli diff --git a/infer/src/IR/BUILTINS.mli b/infer/src/IR/BUILTINS.mli new file mode 100644 index 000000000..3a56fcc22 --- /dev/null +++ b/infer/src/IR/BUILTINS.mli @@ -0,0 +1,85 @@ +(* + * 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. + *) + +(** List of all builtins that are interpreted specially by the backend *) +module type S = sig + type t + val __assert_fail : t + val __builtin_va_arg : t + val __builtin_va_copy : t + val __builtin_va_end : t + val __builtin_va_start : t + val __cast : t (** [__cast(val,typ)] implements java's [typ(val)] *) + + val __check_untainted : t + val __cxx_typeid : t + val __delete : t + val __delete_array : t + val __delete_locked_attribute : t + val __exit : t + val __get_array_length : t + val __get_hidden_field : t + val __get_type_of : t + val __infer_assume : t + val __infer_fail : t + val __instanceof : t (** [__instanceof(val,typ)] implements java's [val instanceof typ] *) + + val __method_set_ignore_attribute : t + val __new : t + val __new_array : t + val __objc_alloc : t + val __objc_alloc_no_fail : t + val __objc_cast : t + val __objc_dictionary_literal : t + val __objc_release : t + val __objc_release_autorelease_pool : t + val __objc_release_cf : t + val __objc_retain : t + val __objc_retain_cf : t + val __placement_delete : t + val __placement_new : t + val __print_value : t + val __require_allocated_array : t + val __set_array_length : t + val __set_autorelease_attribute : t + val __set_file_attribute : t + val __set_hidden_field : t + val __set_lock_attribute : t + val __set_locked_attribute : t + val __set_mem_attribute : t + val __set_observer_attribute : t + val __set_taint_attribute : t + val __set_unlocked_attribute : t + val __set_unsubscribed_observer_attribute : t + val __set_untaint_attribute : t + val __split_get_nth : t + val __throw : t + val __unwrap_exception : t + val abort : t + val exit : t + val free : t + val fscanf : t + val fwscanf : t + val malloc : t + val malloc_no_fail : t + val nsArray_arrayWithObjects : t + val nsArray_arrayWithObjectsCount : t + val objc_cpp_throw : t + val pthread_create : t + val scanf : t + val sscanf : t + val swscanf : t + val vfscanf : t + val vfwscanf : t + val vscanf : t + val vsscanf : t + val vswscanf : t + val vwscanf : t + val wscanf : t +end diff --git a/infer/src/IR/BuiltinDecl.ml b/infer/src/IR/BuiltinDecl.ml new file mode 100644 index 000000000..0eb458d04 --- /dev/null +++ b/infer/src/IR/BuiltinDecl.ml @@ -0,0 +1,100 @@ +(* + * 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. + *) + +type t = Procname.t + +let builtin_decls = ref Procname.Set.empty + +let register pname = + builtin_decls := Procname.Set.add pname !builtin_decls + +let create_procname name = + let pname = Procname.from_string_c_fun name in + register pname; + pname + +let create_objc_class_method class_name method_name = + let method_kind = Procname.ObjCClassMethod in + let pname = (Procname.ObjC_Cpp (Procname.objc_cpp class_name method_name method_kind)) in + register pname; + pname + +let is_declared pname = Procname.Set.mem pname !builtin_decls + +let __assert_fail = create_procname "__assert_fail" +let __builtin_va_arg = create_procname "__builtin_va_arg" +let __builtin_va_copy = create_procname "__builtin_va_copy" +let __builtin_va_end = create_procname "__builtin_va_end" +let __builtin_va_start = create_procname "__builtin_va_start" +let __cast = create_procname "__cast" +let __check_untainted = create_procname "__check_untainted" +let __cxx_typeid = create_procname "__cxx_typeid" +let __delete = create_procname "__delete" +let __delete_array = create_procname "__delete_array" +let __delete_locked_attribute = create_procname "__delete_locked_attribute" +let __exit = create_procname "_exit" +let __get_array_length = create_procname "__get_array_length" +let __get_hidden_field = create_procname "__get_hidden_field" +let __get_type_of = create_procname "__get_type_of" +let __infer_assume = create_procname "__infer_assume" +let __infer_fail = create_procname "__infer_fail" +let __instanceof = create_procname "__instanceof" +let __method_set_ignore_attribute = create_procname "__method_set_ignore_attribute" +let __new = create_procname "__new" +let __new_array = create_procname "__new_array" +let __objc_alloc = create_procname "__objc_alloc" +let __objc_alloc_no_fail = create_procname "__objc_alloc_no_fail" +let __objc_cast = create_procname "__objc_cast" +let __objc_dictionary_literal = + create_objc_class_method "NSDictionary" "dictionaryWithObjects:forKeys:count:" +let __objc_release = create_procname "__objc_release" +let __objc_release_autorelease_pool = create_procname "__objc_release_autorelease_pool" +let __objc_release_cf = create_procname "__objc_release_cf" +let __objc_retain = create_procname "__objc_retain" +let __objc_retain_cf = create_procname "__objc_retain_cf" +let __placement_delete = create_procname "__placement_delete" +let __placement_new = create_procname "__placement_new" +let __print_value = create_procname "__print_value" +let __require_allocated_array = create_procname "__require_allocated_array" +let __set_array_length = create_procname "__set_array_length" +let __set_autorelease_attribute = create_procname "__set_autorelease_attribute" +let __set_file_attribute = create_procname "__set_file_attribute" +let __set_hidden_field = create_procname "__set_hidden_field" +let __set_lock_attribute = create_procname "__set_lock_attribute" +let __set_locked_attribute = create_procname "__set_locked_attribute" +let __set_mem_attribute = create_procname "__set_mem_attribute" +let __set_observer_attribute = create_procname "__set_observer_attribute" +let __set_taint_attribute = create_procname "__set_taint_attribute" +let __set_unlocked_attribute = create_procname "__set_unlocked_attribute" +let __set_unsubscribed_observer_attribute = create_procname "__set_unsubscribed_observer_attribute" +let __set_untaint_attribute = create_procname "__set_untaint_attribute" +let __split_get_nth = create_procname "__split_get_nth" +let __throw = create_procname "__throw" +let __unwrap_exception = create_procname "__unwrap_exception" +let abort = create_procname "abort" +let exit = create_procname "exit" +let free = create_procname "free" +let fscanf = create_procname "fscanf" +let fwscanf = create_procname "fwscanf" +let malloc = create_procname "malloc" +let malloc_no_fail = create_procname "malloc_no_fail" +let nsArray_arrayWithObjects = create_objc_class_method "NSArray" "arrayWithObjects:" +let nsArray_arrayWithObjectsCount = create_objc_class_method "NSArray" "arrayWithObjects:count:" +let objc_cpp_throw = create_procname "__infer_objc_cpp_throw" +let pthread_create = create_procname "pthread_create" +let scanf = create_procname "scanf" +let sscanf = create_procname "sscanf" +let swscanf = create_procname "swscanf" +let vfscanf = create_procname "vfscanf" +let vfwscanf = create_procname "vfwscanf" +let vscanf = create_procname "vscanf" +let vsscanf = create_procname "vsscanf" +let vswscanf = create_procname "vswscanf" +let vwscanf = create_procname "vwscanf" +let wscanf = create_procname "wscanf" diff --git a/infer/src/IR/BuiltinDecl.mli b/infer/src/IR/BuiltinDecl.mli new file mode 100644 index 000000000..a2adf83ff --- /dev/null +++ b/infer/src/IR/BuiltinDecl.mli @@ -0,0 +1,15 @@ +(* + * 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. + *) + +open! Utils + +(** Procnames for the builtin functions supported *) +include BUILTINS.S with type t = Procname.t + +val is_declared : Procname.t -> bool diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/BuiltinDefn.ml similarity index 82% rename from infer/src/backend/modelBuiltins.ml rename to infer/src/backend/BuiltinDefn.ml index b16a296b1..7c888cf70 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/BuiltinDefn.ml @@ -16,6 +16,8 @@ open SymExec module L = Logging module F = Format +type t = Builtin.registered + let execute___no_op prop path: Builtin.ret_typ = [(prop, path)] @@ -941,207 +943,10 @@ let execute___assert_fail { Builtin.pdesc; tenv; prop_; path; args; loc; } Sil.Store (Exp.Lvar Sil.custom_error, Typ.Tvoid, Exp.Const (Const.Cstr error_str), loc) in SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)] -let __assert_fail = Builtin.register - "__assert_fail" execute___assert_fail -let _ = Builtin.register - (* model for va_arg *) - "__builtin_va_arg" execute___builtin_va_arg -let _ = Builtin.register - "__builtin_va_copy" execute_skip -let _ = Builtin.register - (* model va_end as skip *) - "__builtin_va_end" execute_skip -let _ = Builtin.register - "__builtin_va_start" execute_skip -let __cast = Builtin.register - (* [__cast(val,typ)] implements java's [typ(val)] *) - "__cast" execute___cast -let _ = Builtin.register - (* report a taint error if the parameter is tainted, and assume it is untainted afterward *) - "__check_untainted" execute___check_untainted -let __delete = Builtin.register - (* like free *) - "__delete" (execute_free PredSymb.Mnew) -let __delete_array = Builtin.register - (* like free *) - "__delete_array" (execute_free PredSymb.Mnew_array) -let __exit = Builtin.register - (* _exit from C library *) - "_exit" execute_exit -let __get_array_length = Builtin.register - (* return the length of the array passed as a parameter *) - "__get_array_length" execute___get_array_length -let __require_allocated_array = Builtin.register - (* require the parameter to point to an allocated array *) - "__require_allocated_array" execute___require_allocated_array -let _ = Builtin.register - (* return the value of a hidden field in the struct *) - "__get_hidden_field" execute___get_hidden_field -let __get_type_of = Builtin.register - (* return the get the type of the allocated object passed as a parameter *) - "__get_type_of" execute___get_type_of -let __infer_assume = Builtin.register - (* infer assume, diverging on inconsistencies *) - "__infer_assume" execute___infer_assume -let __infer_fail = Builtin.register - (* externally create new errors *) - "__infer_fail" execute___infer_fail -let __instanceof = Builtin.register - (* [__instanceof(val,typ)] implements java's [val instanceof typ] *) - "__instanceof" execute___instanceof -let _ = Builtin.register - "__method_set_ignore_attribute" execute___method_set_ignore_attribute -let __new = Builtin.register - (* like malloc, but always succeeds *) - "__new" (execute_alloc PredSymb.Mnew false) -let __new_array = Builtin.register - (* like malloc, but always succeeds *) - "__new_array" (execute_alloc PredSymb.Mnew_array false) -let __objc_alloc = Builtin.register - (* Objective C alloc *) - "__objc_alloc" (execute_alloc PredSymb.Mobjc true) -let __objc_alloc_no_fail = Builtin.register - (* like __objc_alloc, but does not return nil *) - "__objc_alloc_no_fail" (execute_alloc PredSymb.Mobjc false) -let __objc_cast = Builtin.register - (* objective-c "cast" *) - "__objc_cast" execute___objc_cast -let __objc_release = Builtin.register - (* objective-c "release" *) - "__objc_release" execute___objc_release -let __objc_release_autorelease_pool = Builtin.register - (* set the attribute of the parameter as autorelease *) - "__objc_release_autorelease_pool" execute___release_autorelease_pool -let __objc_release_cf = Builtin.register - (* objective-c "release" *) - "__objc_release_cf" execute___objc_release_cf -let __objc_retain = Builtin.register - (* objective-c "retain" *) - "__objc_retain" execute___objc_retain -let __objc_retain_cf = Builtin.register - "__objc_retain_cf" execute___objc_retain_cf -let __cxx_typeid = Builtin.register - (* C++ "typeid" *) - "__cxx_typeid" execute___cxx_typeid -let __placement_delete = Builtin.register - (* placement delete is skip *) - "__placement_delete" execute_skip -let __placement_new = Builtin.register - (* placement new returns the first argument *) - "__placement_new" execute_return_first_argument -let _ = Builtin.register - (* print a value as seen by the engine *) - "__print_value" execute___print_value -let __set_array_length = Builtin.register - (* set the length of the array passed as a parameter *) - "__set_array_length" execute___set_array_length -let __set_autorelease_attribute = Builtin.register - (* set the attribute of the parameter as autorelease *) - "__set_autorelease_attribute" execute___set_autorelease_attribute -let __set_file_attribute = Builtin.register - (* set the attribute of the parameter as file *) - "__set_file_attribute" execute___set_file_attribute -let __set_lock_attribute = Builtin.register - (* set the attribute of the parameter as file *) - "__set_lock_attribute" execute___set_lock_attribute -let __set_mem_attribute = Builtin.register - (* set the attribute of the parameter as memory *) - "__set_mem_attribute" execute___set_mem_attribute -let __set_observer_attribute = Builtin.register - (* set the observer attribute of the parameter *) - "__set_observer_attribute" (execute___set_attr PredSymb.Aobserver) -let __set_unsubscribed_observer_attribute = Builtin.register - (* set the unregistered observer attribute of the parameter *) - "__set_unsubscribed_observer_attribute" - (execute___set_attr PredSymb.Aunsubscribed_observer) -let __split_get_nth = Builtin.register - (* splits a string given a separator and returns the nth string *) - "__split_get_nth" execute___split_get_nth -let _ = Builtin.register - (* set a hidden field in the struct to the given value *) - "__set_hidden_field" execute___set_hidden_field -let _ = Builtin.register - (* set the attribute of the parameter as tainted *) - "__set_taint_attribute" execute___set_taint_attribute -let _ = Builtin.register - (* set the attribute of the parameter as untainted *) - "__set_untaint_attribute" execute___set_untaint_attribute -let __set_locked_attribute = Builtin.register - (* set the attribute of the parameter as locked *) - "__set_locked_attribute" execute___set_locked_attribute -let __set_unlocked_attribute = Builtin.register - (* set the attribute of the parameter as unlocked *) - "__set_unlocked_attribute" execute___set_unlocked_attribute -let __delete_locked_attribute = Builtin.register - (* delete the locked attribute, when it exists *) - "__delete_locked_attribute" execute___delete_locked_attribute -let objc_cpp_throw = Builtin.register - (* model throwing exception in objc/c++ as divergence *) - "__infer_objc_cpp_throw" execute_exit -let _ = Builtin.register - "__throw" execute_skip -let __unwrap_exception = Builtin.register - (* unwrap an exception *) - "__unwrap_exception" execute__unwrap_exception -let _ = Builtin.register - (* abort from C library *) - "abort" execute_abort -let _ = Builtin.register - (* exit from C library *) - "exit" execute_exit -let _ = Builtin.register - (* free from C library, requires allocated memory *) - "free" (execute_free PredSymb.Mmalloc) -let _ = Builtin.register - (* fscanf from C library *) - "fscanf" (execute_scan_function 2) -let _ = Builtin.register - (* vsscanf from C library *) - "fwscanf" (execute_scan_function 2) -let _ = Builtin.register - (* malloc from C library *) - "malloc" (execute_alloc PredSymb.Mmalloc (not Config.unsafe_malloc)) -let malloc_no_fail = Builtin.register - (* malloc from ObjC library *) - "malloc_no_fail" (execute_alloc PredSymb.Mmalloc false) -let _ = Builtin.register - (* register execution handler for pthread_create *) - "pthread_create" execute_pthread_create -let _ = Builtin.register - (* scanf from C library *) - "scanf" (execute_scan_function 1) -let _ = Builtin.register - (* sscanf from C library *) - "sscanf" (execute_scan_function 2) -let _ = Builtin.register - (* vsscanf from C library *) - "swscanf" (execute_scan_function 2) -let _ = Builtin.register - (* vfwscanf from C library *) - "vfscanf" (execute_scan_function 2) -let _ = Builtin.register - (* vsscanf from C library *) - "vfwscanf" (execute_scan_function 2) -let _ = Builtin.register - (* vscanf from C library *) - "vscanf" (execute_scan_function 1) -let _ = Builtin.register - (* vsscanf from C library *) - "vsscanf" (execute_scan_function 2) -let _ = Builtin.register - (* vsscanf from C library *) - "vswscanf" (execute_scan_function 2) -let _ = Builtin.register - (* vsscanf from C library *) - "vwscanf" (execute_scan_function 1) -let _ = Builtin.register - (* vsscanf from C library *) - "wscanf" (execute_scan_function 1) - let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt { Builtin.pdesc; tenv; ret_id; loc; } = - let alloc_fun = Exp.Const (Const.Cfun __objc_alloc_no_fail) in + let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.__objc_alloc_no_fail) in let ptr_typ = Typ.Tptr (typ, Typ.Pk_pointer) in let sizeof_typ = Exp.Sizeof (typ, None, Subtype.exact) in let alloc_fun_exp = @@ -1153,17 +958,7 @@ let execute_objc_alloc_no_fail (ret_id, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) in SymExec.instrs tenv pdesc [alloc_instr] symb_state -let mk_objc_class_method class_name method_name = - let method_kind = Procname.ObjCClassMethod in - (Procname.ObjC_Cpp - (Procname.objc_cpp class_name method_name method_kind)) - (* NSArray models *) - -let arrayWithObjects_pname = mk_objc_class_method "NSArray" "arrayWithObjects:" - -let arrayWithObjectsCount_pname = mk_objc_class_method "NSArray" "arrayWithObjects:count:" - let execute_objc_NSArray_alloc_no_fail builtin_args symb_state pname = let ret_typ = match builtin_args.Builtin.ret_id with @@ -1174,19 +969,15 @@ let execute_objc_NSArray_alloc_no_fail builtin_args symb_state pname = let execute_NSArray_arrayWithObjects_count builtin_args = let n_formals = 1 in let res = SymExec.check_variadic_sentinel ~fails_on_nil: true n_formals (0,1) builtin_args in - execute_objc_NSArray_alloc_no_fail builtin_args res arrayWithObjectsCount_pname + execute_objc_NSArray_alloc_no_fail builtin_args res BuiltinDecl.nsArray_arrayWithObjectsCount let execute_NSArray_arrayWithObjects builtin_args = let n_formals = 1 in let res = SymExec.check_variadic_sentinel n_formals (0,1) builtin_args in - execute_objc_NSArray_alloc_no_fail builtin_args res arrayWithObjects_pname + execute_objc_NSArray_alloc_no_fail builtin_args res BuiltinDecl.nsArray_arrayWithObjects -let _ = - Builtin.register_procname arrayWithObjectsCount_pname execute_NSArray_arrayWithObjects_count; - Builtin.register_procname arrayWithObjects_pname execute_NSArray_arrayWithObjects (* NSDictionary models *) - let execute_objc_NSDictionary_alloc_no_fail symb_state pname builtin_args = let ret_typ = match builtin_args.Builtin.ret_id with @@ -1194,16 +985,186 @@ let execute_objc_NSDictionary_alloc_no_fail symb_state pname builtin_args = | None -> Typ.Tptr (Tvoid, Pk_pointer) in execute_objc_alloc_no_fail symb_state ret_typ (Some pname) builtin_args -let __objc_dictionary_literal_pname = - mk_objc_class_method "NSDictionary" "dictionaryWithObjects:forKeys:count:" - let execute___objc_dictionary_literal builtin_args = let n_formals = 1 in let res' = SymExec.check_variadic_sentinel ~fails_on_nil: true n_formals (0,1) builtin_args in - let pname = __objc_dictionary_literal_pname in + let pname = BuiltinDecl.__objc_dictionary_literal in execute_objc_NSDictionary_alloc_no_fail res' pname builtin_args -let __objc_dictionary_literal = - let pname = __objc_dictionary_literal_pname in - Builtin.register_procname pname execute___objc_dictionary_literal; - pname +let __assert_fail = Builtin.register BuiltinDecl.__assert_fail execute___assert_fail + +let __builtin_va_arg = Builtin.register BuiltinDecl.__builtin_va_arg execute___builtin_va_arg + +let __builtin_va_copy = Builtin.register BuiltinDecl.__builtin_va_copy execute_skip + +let __builtin_va_end = Builtin.register BuiltinDecl.__builtin_va_end execute_skip + +let __builtin_va_start = Builtin.register BuiltinDecl.__builtin_va_start execute_skip + +(* [__cast(val,typ)] implements java's [typ(val)] *) +let __cast = Builtin.register BuiltinDecl.__cast execute___cast + +(* report a taint error if the parameter is tainted, and assume it is untainted afterward *) +let __check_untainted = Builtin.register BuiltinDecl.__check_untainted execute___check_untainted + +let __cxx_typeid = Builtin.register BuiltinDecl.__cxx_typeid execute___cxx_typeid + +let __delete = Builtin.register BuiltinDecl.__delete (execute_free PredSymb.Mnew) + +let __delete_array = Builtin.register BuiltinDecl.__delete_array + (execute_free PredSymb.Mnew_array) + +let __delete_locked_attribute = Builtin.register BuiltinDecl.__delete_locked_attribute + execute___delete_locked_attribute + +let __exit = Builtin.register BuiltinDecl.__exit execute_exit + +(* return the length of the array passed as a parameter *) +let __get_array_length = Builtin.register BuiltinDecl.__get_array_length execute___get_array_length + +let __get_hidden_field = Builtin.register BuiltinDecl.__get_hidden_field execute___get_hidden_field + +let __get_type_of = Builtin.register BuiltinDecl.__get_type_of execute___get_type_of + +(* infer assume, diverging on inconsistencies *) +let __infer_assume = Builtin.register BuiltinDecl.__infer_assume execute___infer_assume + +(* externally create new errors *) +let __infer_fail = Builtin.register BuiltinDecl.__infer_fail execute___infer_fail + +(* [__instanceof(val,typ)] implements java's [val instanceof typ] *) +let __instanceof = Builtin.register BuiltinDecl.__instanceof execute___instanceof + +let __method_set_ignore_attribute = Builtin.register BuiltinDecl.__method_set_ignore_attribute + execute___method_set_ignore_attribute + +let __new = Builtin.register BuiltinDecl.__new (execute_alloc PredSymb.Mnew false) + +let __new_array = Builtin.register BuiltinDecl.__new_array (execute_alloc PredSymb.Mnew_array false) + +let __objc_alloc = Builtin.register BuiltinDecl.__objc_alloc (execute_alloc PredSymb.Mobjc true) + +(* like __objc_alloc, but does not return nil *) +let __objc_alloc_no_fail = Builtin.register BuiltinDecl.__objc_alloc_no_fail + (execute_alloc PredSymb.Mobjc false) + +let __objc_cast = Builtin.register BuiltinDecl.__objc_cast execute___objc_cast + +let __objc_dictionary_literal = Builtin.register BuiltinDecl.__objc_dictionary_literal + execute___objc_dictionary_literal + +let __objc_release = Builtin.register BuiltinDecl.__objc_release execute___objc_release + +let __objc_release_autorelease_pool = Builtin.register BuiltinDecl.__objc_release_autorelease_pool + execute___release_autorelease_pool + +let __objc_release_cf = Builtin.register BuiltinDecl.__objc_release_cf execute___objc_release_cf + +let __objc_retain = Builtin.register BuiltinDecl.__objc_retain execute___objc_retain + +let __objc_retain_cf = Builtin.register BuiltinDecl.__objc_retain_cf execute___objc_retain_cf + +let __placement_delete = Builtin.register BuiltinDecl.__placement_delete execute_skip + +let __placement_new = Builtin.register BuiltinDecl.__placement_new execute_return_first_argument + +(* print a value as seen by the engine *) +let __print_value = Builtin.register BuiltinDecl.__print_value execute___print_value + +(* require the parameter to point to an allocated array *) +let __require_allocated_array = Builtin.register BuiltinDecl.__require_allocated_array + execute___require_allocated_array + +let __set_array_length = Builtin.register BuiltinDecl.__set_array_length execute___set_array_length + +let __set_autorelease_attribute = Builtin.register BuiltinDecl.__set_autorelease_attribute + execute___set_autorelease_attribute + +let __set_file_attribute = Builtin.register BuiltinDecl.__set_file_attribute + execute___set_file_attribute + +(* set a hidden field in the struct to the given value *) +let __set_hidden_field = Builtin.register BuiltinDecl.__set_hidden_field execute___set_hidden_field + +let __set_lock_attribute = Builtin.register BuiltinDecl.__set_lock_attribute + execute___set_lock_attribute + +let __set_locked_attribute = Builtin.register BuiltinDecl.__set_locked_attribute + execute___set_locked_attribute + +let __set_mem_attribute = Builtin.register BuiltinDecl.__set_mem_attribute + execute___set_mem_attribute + +let __set_observer_attribute = Builtin.register BuiltinDecl.__set_observer_attribute + (execute___set_attr PredSymb.Aobserver) + +let __set_taint_attribute = Builtin.register BuiltinDecl.__set_taint_attribute + execute___set_taint_attribute + +let __set_unlocked_attribute = Builtin.register BuiltinDecl.__set_unlocked_attribute + execute___set_unlocked_attribute + +let __set_unsubscribed_observer_attribute = Builtin.register + BuiltinDecl.__set_unsubscribed_observer_attribute + (execute___set_attr PredSymb.Aunsubscribed_observer) + +let __set_untaint_attribute = Builtin.register + BuiltinDecl.__set_untaint_attribute execute___set_untaint_attribute + +(* splits a string given a separator and returns the nth string *) +let __split_get_nth = Builtin.register BuiltinDecl.__split_get_nth execute___split_get_nth + +let __throw = Builtin.register BuiltinDecl.__throw execute_skip + +let __unwrap_exception = Builtin.register BuiltinDecl.__unwrap_exception execute__unwrap_exception + +let abort = Builtin.register BuiltinDecl.abort execute_abort + +let exit = Builtin.register BuiltinDecl.exit execute_exit + +let free = Builtin.register BuiltinDecl.free (execute_free PredSymb.Mmalloc) + +let fscanf = Builtin.register BuiltinDecl.fscanf (execute_scan_function 2) + +let fwscanf = Builtin.register BuiltinDecl.fwscanf (execute_scan_function 2) + +let malloc = Builtin.register BuiltinDecl.malloc (execute_alloc PredSymb.Mmalloc + (not Config.unsafe_malloc)) + +let malloc_no_fail = Builtin.register BuiltinDecl.malloc_no_fail + (execute_alloc PredSymb.Mmalloc false) + +let nsArray_arrayWithObjects = Builtin.register BuiltinDecl.nsArray_arrayWithObjects + execute_NSArray_arrayWithObjects + +let nsArray_arrayWithObjectsCount = Builtin.register BuiltinDecl.nsArray_arrayWithObjectsCount + execute_NSArray_arrayWithObjects_count + +(* model throwing exception in objc/c++ as divergence *) +let objc_cpp_throw = Builtin.register BuiltinDecl.objc_cpp_throw execute_exit + +let pthread_create = Builtin.register BuiltinDecl.pthread_create execute_pthread_create + +let scanf = Builtin.register BuiltinDecl.scanf (execute_scan_function 1) + +let sscanf = Builtin.register BuiltinDecl.sscanf (execute_scan_function 2) + +let swscanf = Builtin.register BuiltinDecl.swscanf (execute_scan_function 2) + +let vfscanf = Builtin.register BuiltinDecl.vfscanf (execute_scan_function 2) + +let vfwscanf = Builtin.register BuiltinDecl.vfwscanf (execute_scan_function 2) + +let vscanf = Builtin.register BuiltinDecl.vscanf (execute_scan_function 1) + +let vsscanf = Builtin.register BuiltinDecl.vsscanf (execute_scan_function 2) + +let vswscanf = Builtin.register BuiltinDecl.vswscanf (execute_scan_function 2) + +let vwscanf = Builtin.register BuiltinDecl.vwscanf (execute_scan_function 1) + +let wscanf = Builtin.register BuiltinDecl.wscanf (execute_scan_function 1) + +(* Function exists to load module and guarantee that the side-effects of Builtin.register + calls have been done. *) +let init () = () diff --git a/infer/src/backend/BuiltinDefn.mli b/infer/src/backend/BuiltinDefn.mli new file mode 100644 index 000000000..43583c1b9 --- /dev/null +++ b/infer/src/backend/BuiltinDefn.mli @@ -0,0 +1,18 @@ +(* + * 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. + *) + +open! Utils + +(** Models for the builtin functions supported *) +include BUILTINS.S with type t = Builtin.registered + +(** Clients of Builtin module should call this before Builtin module is used. + WARNING: builtins are not guaranteed to be registered with the Builtin module + until after init has been called. *) +val init : unit -> unit diff --git a/infer/src/backend/InferAnalyze.re b/infer/src/backend/InferAnalyze.re index 8714cd08c..242b33215 100644 --- a/infer/src/backend/InferAnalyze.re +++ b/infer/src/backend/InferAnalyze.re @@ -127,6 +127,7 @@ let register_perf_stats_report () => { let () = { register_perf_stats_report (); + BuiltinDefn.init (); if Config.developer_mode { Printexc.record_backtrace true }; diff --git a/infer/src/backend/builtin.ml b/infer/src/backend/builtin.ml index 67b57af69..34eef23ae 100644 --- a/infer/src/backend/builtin.ml +++ b/infer/src/backend/builtin.ml @@ -27,27 +27,30 @@ type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list type t = args -> ret_typ +type registered = t + (** builtin function names for which we do symbolic execution *) let builtin_functions = Procname.Hash.create 4 +let check_register_populated () = + (* check if BuiltinDefn were loaded before accessing register *) + if Procname.Hash.length builtin_functions = 0 then + failwith "Builtins were not initialized" + else () + (** check if the function is a builtin *) let is_registered name = - Procname.Hash.mem builtin_functions name + Procname.Hash.mem builtin_functions name || (check_register_populated (); false) (** 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 +let get name : t option = + try Some (Procname.Hash.find builtin_functions name) + with Not_found -> (check_register_populated (); None) (** 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 +let register proc_name sym_exe_fun : registered = + Procname.Hash.replace builtin_functions proc_name sym_exe_fun; + sym_exe_fun (** print the functions registered *) let pp_registered fmt () = diff --git a/infer/src/backend/builtin.mli b/infer/src/backend/builtin.mli index 1118754cc..3efbe035f 100644 --- a/infer/src/backend/builtin.mli +++ b/infer/src/backend/builtin.mli @@ -27,16 +27,15 @@ 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 *) +type registered -val register_procname : Procname.t -> t -> unit +val register : Procname.t -> t -> registered (** 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 +val get : Procname.t -> t option (** Get the symbolic execution handler associated to the builtin function name *) val print_and_exit : unit -> 'a diff --git a/infer/src/backend/inferconfig.ml b/infer/src/backend/inferconfig.ml index 822642b59..9ffe8407d 100644 --- a/infer/src/backend/inferconfig.ml +++ b/infer/src/backend/inferconfig.ml @@ -54,7 +54,7 @@ let is_matching patterns = (** Check if a proc name is matching the name given as string. *) let match_method language proc_name method_name = - not (Builtin.is_registered proc_name) && + not (BuiltinDecl.is_declared proc_name) && Procname.get_language proc_name = language && Procname.get_method proc_name = method_name diff --git a/infer/src/backend/modelBuiltins.mli b/infer/src/backend/modelBuiltins.mli deleted file mode 100644 index cbb36ea05..000000000 --- a/infer/src/backend/modelBuiltins.mli +++ /dev/null @@ -1,49 +0,0 @@ -(* - * 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. - *) - -open! Utils - -(** Models for the builtin functions supported *) - -val __assert_fail : Procname.t -val __delete : Procname.t -val __delete_array : Procname.t -val __exit : Procname.t -val __get_array_length : Procname.t -val __get_type_of : Procname.t -val __infer_fail : Procname.t -val __instanceof : Procname.t (** [__instanceof(val,typ)] implements java's [val instanceof typ] *) - -val __cast : Procname.t (** [__cast(val,typ)] implements java's [typ(val)] *) - -val __placement_delete : Procname.t -val __placement_new : Procname.t -val __new : Procname.t -val __new_array : Procname.t -val __objc_alloc : Procname.t -val __objc_alloc_no_fail : Procname.t -val __set_array_length : Procname.t -val __unwrap_exception : Procname.t -val __set_file_attribute : Procname.t -val __set_mem_attribute : Procname.t -val __set_locked_attribute : Procname.t -val __set_unlocked_attribute : Procname.t -val __delete_locked_attribute : Procname.t -val __infer_assume : Procname.t -val __objc_retain : Procname.t -val __objc_release : Procname.t -val __objc_retain_cf : Procname.t -val __objc_release_cf : Procname.t -val __set_autorelease_attribute : Procname.t -val __objc_release_autorelease_pool : Procname.t -val __objc_cast : Procname.t -val __objc_dictionary_literal : Procname.t -val __cxx_typeid : Procname.t -val malloc_no_fail : Procname.t -val objc_cpp_throw : Procname.t diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 52b2f8427..4f5e9d0cf 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1054,7 +1054,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path ret_old_path (Propset.to_proplist (prune tenv ~positive:true n_cond prop)) | Sil.Call (ret_id, Exp.Const (Const.Cfun callee_pname), args, loc, _) when Builtin.is_registered callee_pname -> - let sym_exe_builtin = Builtin.get callee_pname in + let sym_exe_builtin = Option.get (Builtin.get callee_pname) in sym_exe_builtin (call_args prop_ callee_pname args ret_id loc) | Sil.Call (ret_id, Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)), diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index b700ec4b6..e4ad8fa2e 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -33,9 +33,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module Domain = CombinedDomain type extras = ProcData.no_extras - let is_lock_procedure pn = Procname.equal pn ModelBuiltins.__set_locked_attribute + let is_lock_procedure pn = Procname.equal pn BuiltinDecl.__set_locked_attribute - let is_unlock_procedure pn = Procname.equal pn ModelBuiltins.__delete_locked_attribute + let is_unlock_procedure pn = Procname.equal pn BuiltinDecl.__delete_locked_attribute let add_path_to_state exp typ pathdomainstate = IList.fold_left diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index b721f68e1..709835b8d 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -112,7 +112,7 @@ let annotation_reachability_error = "CHECKERS_ANNOTATION_REACHABILITY_ERROR" let is_modeled_expensive tenv = function | Procname.Java proc_name_java as proc_name -> - not (Builtin.is_registered proc_name) && + not (BuiltinDecl.is_declared proc_name) && let is_subclass = let classname = Typename.Java.from_string (Procname.java_get_class_name proc_name_java) in PatternMatch.is_subtype_of_str tenv classname in @@ -128,7 +128,7 @@ let is_allocator tenv pname = Typename.Java.from_string (Procname.java_get_class_name pname_java) in PatternMatch.is_throwable tenv class_name in Procname.is_constructor pname - && not (Builtin.is_registered pname) + && not (BuiltinDecl.is_declared pname) && not (is_throwable ()) | _ -> false diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index 7fe7f893a..8fc0e6b0b 100644 --- a/infer/src/checkers/dataflow.ml +++ b/infer/src/checkers/dataflow.ml @@ -58,8 +58,8 @@ let node_throws node (proc_throws : Procname.t -> throws) : throws = (* assignment to return variable is an artifact of a throw instruction *) Throws | Sil.Call (_, Exp.Const (Const.Cfun callee_pn), _, _, _) - when Builtin.is_registered callee_pn -> - if Procname.equal callee_pn ModelBuiltins.__cast + when BuiltinDecl.is_declared callee_pn -> + if Procname.equal callee_pn BuiltinDecl.__cast then DontKnow else DoesNotThrow | Sil.Call (_, Exp.Const (Const.Cfun callee_pn), _, _, _) -> diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml index eb041c91e..e7a8b38f7 100644 --- a/infer/src/checkers/repeatedCallsChecker.ml +++ b/infer/src/checkers/repeatedCallsChecker.ml @@ -66,8 +66,8 @@ struct let node_allocates node : Location.t option = let found = ref None in let proc_is_new pn = - Procname.equal pn ModelBuiltins.__new || - Procname.equal pn ModelBuiltins.__new_array in + Procname.equal pn BuiltinDecl.__new || + Procname.equal pn BuiltinDecl.__new_array in let do_instr instr = match instr with | Sil.Call (_, Exp.Const (Const.Cfun pn), _, loc, _) when proc_is_new pn -> diff --git a/infer/src/clang/ast_expressions.ml b/infer/src/clang/ast_expressions.ml index 45c3f88a5..43d8e34d3 100644 --- a/infer/src/clang/ast_expressions.ml +++ b/infer/src/clang/ast_expressions.ml @@ -627,6 +627,6 @@ let create_assume_not_null_call decl_info var_name var_type = let bin_op_expr_info = make_general_expr_info create_BOOL_type `RValue `Ordinary in let bin_op = make_binary_stmt decl_ref_exp_cast null_expr stmt_info bin_op_expr_info boi in let parameters = [bin_op] in - let procname = Procname.to_string ModelBuiltins.__infer_assume in + let procname = Procname.to_string BuiltinDecl.__infer_assume in let qual_procname = Ast_utils.make_name_decl procname in create_call stmt_info var_decl_ptr qual_procname create_void_star_type parameters diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index f272e4cc2..6f56b30f1 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/infer/src/clang/cArithmetic_trans.ml @@ -22,9 +22,9 @@ open CFrontend_utils (* See document: "Objective-C Automatic Reference Counting" describing the semantics *) let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl = let assign = Sil.Store (e1, typ, e2, loc) in - let retain_pname = ModelBuiltins.__objc_retain in - let release_pname = ModelBuiltins.__objc_release in - let autorelease_pname = ModelBuiltins.__set_autorelease_attribute in + let retain_pname = BuiltinDecl.__objc_retain in + let release_pname = BuiltinDecl.__objc_release in + let autorelease_pname = BuiltinDecl.__set_autorelease_attribute in let mk_call procname e t = let bi_retain = Exp.Const (Const.Cfun procname) in Sil.Call (None, bi_retain, [(e, t)], loc, CallFlags.default) in diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 7b50c019f..4ac0b7390 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -73,7 +73,7 @@ struct if !Config.arc_mode && not (CTrans_utils.is_owning_name method_name) && ObjcInterface_decl.is_pointer_to_objc_class typ then - let fname = ModelBuiltins.__set_autorelease_attribute in + let fname = BuiltinDecl.__set_autorelease_attribute in let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.Tvoid) in (* TODO(jjb): change ret_id to None? *) let stmt_call = @@ -445,12 +445,12 @@ struct | _ when CTrans_models.is_modeled_builtin name -> Some (Procname.from_string_c_fun (CFrontend_config.infer ^ name)) | _ when CTrans_models.is_release_builtin name type_ptr -> - Some ModelBuiltins.__objc_release_cf + Some BuiltinDecl.__objc_release_cf | _ when CTrans_models.is_retain_builtin name type_ptr -> - Some ModelBuiltins.__objc_retain_cf + Some BuiltinDecl.__objc_retain_cf | _ when name = CFrontend_config.malloc && General_utils.is_objc_extension trans_unit_ctx -> - Some ModelBuiltins.malloc_no_fail + Some BuiltinDecl.malloc_no_fail | _ -> None @@ -1961,7 +1961,7 @@ struct let typ = CTypes_decl.class_from_pointer_type trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in - let dictionary_literal_pname = ModelBuiltins.__objc_dictionary_literal in + let dictionary_literal_pname = BuiltinDecl.__objc_dictionary_literal in let dictionary_literal_s = Procname.get_method dictionary_literal_pname in let obj_c_message_expr_info = Ast_expressions.make_obj_c_message_expr_info_class dictionary_literal_s typ None in @@ -1989,7 +1989,7 @@ struct and objcAutoreleasePool_trans trans_state stmt_info stmts = let context = trans_state.context in let sil_loc = CLocation.get_sil_location stmt_info context in - let fname = ModelBuiltins.__objc_release_autorelease_pool in + let fname = BuiltinDecl.__objc_release_autorelease_pool in let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.Tvoid) in (* TODO(jjb): change ret_id to None? *) let autorelease_pool_vars = CVar_decl.compute_autorelease_pool_vars context stmts in @@ -2148,8 +2148,8 @@ struct let sil_loc = CLocation.get_sil_location stmt_info context in let is_array = delete_expr_info.Clang_ast_t.xdei_is_array in let fname = - if is_array then ModelBuiltins.__delete_array - else ModelBuiltins.__delete in + if is_array then BuiltinDecl.__delete_array + else BuiltinDecl.__delete in let param = match stmt_list with [p] -> p | _ -> assert false in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in let trans_state_param = { trans_state_pri with succ_nodes = [] } in @@ -2211,7 +2211,7 @@ struct let sizeof_expr = match cast_type with | Typ.Tptr (typ, _) -> Exp.Sizeof (typ, None, subtypes) | _ -> assert false in - let builtin = Exp.Const (Const.Cfun ModelBuiltins.__cast) in + let builtin = Exp.Const (Const.Cfun BuiltinDecl.__cast) in let stmt = match stmts with [stmt] -> stmt | _ -> assert false in let res_trans_stmt = exec_with_glvalue_as_reference instruction trans_state' stmt in let exp = match res_trans_stmt.exps with | [e] -> e | _ -> assert false in @@ -2252,7 +2252,7 @@ struct let pname = Procname.from_string_c_fun CFrontend_config.infer_skip_gcc_asm_stmt in call_function_with_args "GCCAsmStmt" pname trans_state and objc_cxx_throw_trans trans_state = - call_function_with_args "ObjCCPPThrow" ModelBuiltins.objc_cpp_throw trans_state + call_function_with_args "ObjCCPPThrow" BuiltinDecl.objc_cpp_throw trans_state and cxxPseudoDestructorExpr_trans () = let fun_name = Procname.from_string_c_fun CFrontend_config.infer_skip_fun in @@ -2269,7 +2269,7 @@ struct let trans_state_param = { trans_state_pri with succ_nodes = [] } in instruction trans_state_param stmt | _ -> empty_res_trans in - let fun_name = ModelBuiltins.__cxx_typeid in + let fun_name = BuiltinDecl.__cxx_typeid in let sil_fun = Exp.Const (Const.Cfun fun_name) in let ret_id = Ident.create_fresh Ident.knormal in let type_info_objc = (Exp.Sizeof (typ, None, Subtype.exact), Typ.Tvoid) in diff --git a/infer/src/clang/cTrans_models.ml b/infer/src/clang/cTrans_models.ml index 6bd01ee4f..73171e40e 100644 --- a/infer/src/clang/cTrans_models.ml +++ b/infer/src/clang/cTrans_models.ml @@ -56,11 +56,11 @@ let is_autorelease_method funct = let get_builtinname method_name = if is_retain_method method_name then - Some ModelBuiltins.__objc_retain + Some BuiltinDecl.__objc_retain else if is_autorelease_method method_name then - Some ModelBuiltins.__set_autorelease_attribute + Some BuiltinDecl.__set_autorelease_attribute else if is_release_method method_name then - Some ModelBuiltins.__objc_release + Some BuiltinDecl.__objc_release else None let is_modeled_builtin funct = @@ -115,8 +115,8 @@ let is_toll_free_bridging pn = funct = CFrontend_config.ns_make_collectable let is_cf_retain_release pn = - Procname.equal pn ModelBuiltins.__objc_retain_cf - || Procname.equal pn ModelBuiltins.__objc_release_cf + Procname.equal pn BuiltinDecl.__objc_retain_cf + || Procname.equal pn BuiltinDecl.__objc_release_cf (** If the function is a builtin model, return the model, otherwise return the function *) let is_assert_log pname = @@ -180,7 +180,7 @@ let get_predefined_ms_nsautoreleasepool_release class_name method_name mk_procna let args = [(Mangled.from_string CFrontend_config.self, class_type)] in get_predefined_ms_method condition class_name method_name Procname.ObjCInstanceMethod mk_procname lang args Ast_expressions.create_void_type - [] (Some ModelBuiltins.__objc_release_autorelease_pool) + [] (Some BuiltinDecl.__objc_release_autorelease_pool) let get_predefined_ms_is_kind_of_class class_name method_name mk_procname lang = let condition = method_name = CFrontend_config.is_kind_of_class in @@ -188,7 +188,7 @@ let get_predefined_ms_is_kind_of_class class_name method_name mk_procname lang = let args = [(Mangled.from_string CFrontend_config.self, class_type)] in get_predefined_ms_method condition class_name method_name Procname.ObjCInstanceMethod mk_procname lang args Ast_expressions.create_BOOL_type - [] (Some ModelBuiltins.__instanceof) + [] (Some BuiltinDecl.__instanceof) let get_predefined_model_method_signature class_name method_name mk_procname lang = let next_predefined f = function diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index e446b7b68..3af8ef6d2 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -313,9 +313,9 @@ let create_alloc_instrs sil_loc function_type fname size_exp_opt procname_opt = let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc procname_opt = let fname = if is_cf_non_null_alloc then - ModelBuiltins.__objc_alloc_no_fail + BuiltinDecl.__objc_alloc_no_fail else - ModelBuiltins.__objc_alloc in + BuiltinDecl.__objc_alloc in let (function_type, stmt_call, exp) = create_alloc_instrs loc function_type fname None procname_opt in let res_trans_tmp = { empty_res_trans with instrs =[stmt_call]} in @@ -325,7 +325,7 @@ let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc pro { res_trans with exps =[(exp, function_type)]} let objc_new_trans trans_state loc stmt_info cls_name function_type = - let fname = ModelBuiltins.__objc_alloc_no_fail in + let fname = BuiltinDecl.__objc_alloc_no_fail in let (alloc_ret_type, alloc_stmt_call, alloc_ret_exp) = create_alloc_instrs loc function_type fname None None in let init_ret_id = Ident.create_fresh Ident.knormal in @@ -362,8 +362,8 @@ let new_or_alloc_trans trans_state loc stmt_info type_ptr class_name_opt selecto let cpp_new_trans sil_loc function_type size_exp_opt = let fname = match size_exp_opt with - | Some _ -> ModelBuiltins.__new_array - | None -> ModelBuiltins.__new in + | Some _ -> BuiltinDecl.__new_array + | None -> BuiltinDecl.__new in let (function_type, stmt_call, exp) = create_alloc_instrs sil_loc function_type fname size_exp_opt None in { empty_res_trans with instrs = [stmt_call]; exps = [(exp, function_type)] } @@ -373,7 +373,7 @@ let create_cast_instrs exp cast_from_typ cast_to_typ sil_loc = let ret_id_typ = Some (ret_id, cast_to_typ) in let typ = CTypes.remove_pointer_to_typ cast_to_typ in let sizeof_exp = Exp.Sizeof (typ, None, Subtype.exact) in - let pname = ModelBuiltins.__objc_cast in + let pname = BuiltinDecl.__objc_cast in let args = [(exp, cast_from_typ); (sizeof_exp, Typ.Tint Typ.IULong)] in let stmt_call = Sil.Call (ret_id_typ, Exp.Const (Const.Cfun pname), args, sil_loc, CallFlags.default) in @@ -439,7 +439,7 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged = ([], (exp, cast_typ)) let trans_assertion_failure sil_loc context = - let assert_fail_builtin = Exp.Const (Const.Cfun ModelBuiltins.__infer_fail) in + let assert_fail_builtin = Exp.Const (Const.Cfun BuiltinDecl.__infer_fail) in let args = [Exp.Const (Const.Cstr Config.default_failure_name), Typ.Tvoid] in let call_instr = Sil.Call (None, assert_fail_builtin, args, sil_loc, CallFlags.default) in let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context) diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml index f31740585..6835c0bed 100644 --- a/infer/src/eradicate/eradicateChecks.ml +++ b/infer/src/eradicate/eradicateChecks.ml @@ -122,7 +122,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname | _ -> false in let do_instr = function | Sil.Call (_, Exp.Const (Const.Cfun pn), [_; (Exp.Sizeof(t, _, _), _)], _, _) when - Procname.equal pn ModelBuiltins.__instanceof && typ_is_throwable t -> + Procname.equal pn BuiltinDecl.__instanceof && typ_is_throwable t -> throwable_found := true | _ -> () in let do_node n = diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index a74f21341..e2c45d78d 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -41,7 +41,7 @@ module ComplexExpressions = struct let procname_optional_isPresent = Models.is_optional_isPresent - let procname_instanceof = Procname.equal ModelBuiltins.__instanceof + let procname_instanceof = Procname.equal BuiltinDecl.__instanceof let procname_is_false_on_null pn = match Specs.proc_resolve_attributes pn with @@ -73,7 +73,7 @@ module ComplexExpressions = struct procname_optional_isPresent pn || procname_instanceof pn || procname_containsKey pn || - Builtin.is_registered pn + BuiltinDecl.is_declared pn exception Not_handled @@ -508,14 +508,14 @@ let typecheck_instr check_field_assign (); typestate2 | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), [(_, typ)], loc, _) - when Procname.equal pn ModelBuiltins.__new || - Procname.equal pn ModelBuiltins.__new_array -> + when Procname.equal pn BuiltinDecl.__new || + Procname.equal pn BuiltinDecl.__new_array -> TypeState.add_id id (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.New, [loc]) typestate (* new never returns null *) | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), (e, typ):: _, loc, _) - when Procname.equal pn ModelBuiltins.__cast -> + when Procname.equal pn BuiltinDecl.__cast -> typecheck_expr_for_errors typestate e loc; let e', typestate' = convert_complex_exp_to_pvar node false e typestate loc in @@ -524,7 +524,7 @@ let typecheck_instr (typecheck_expr_simple typestate' e' typ TypeOrigin.ONone loc) typestate' | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), [(array_exp, t)], loc, _) - when Procname.equal pn ModelBuiltins.__get_array_length -> + when Procname.equal pn BuiltinDecl.__get_array_length -> let (_, ta, _) = typecheck_expr find_canonical_duplicate calls_this @@ -555,7 +555,7 @@ let typecheck_instr [loc] ) typestate - | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when Builtin.is_registered pn -> + | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when BuiltinDecl.is_declared pn -> typestate (* skip othe builtins *) | Sil.Call (ret_id, diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index f72fa5f9c..11d33b024 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -87,11 +87,11 @@ let rec inhabit_typ tenv typ cfg env = | Typ.Tptr (Typ.Tarray (inner_typ, Some _), Typ.Pk_pointer) -> let len = Exp.Const (Const.Cint (IntLit.one)) in let arr_typ = Typ.Tarray (inner_typ, Some IntLit.one) in - inhabit_alloc arr_typ (Some len) typ ModelBuiltins.__new_array env + inhabit_alloc arr_typ (Some len) typ BuiltinDecl.__new_array env | Typ.Tptr (typ, Typ.Pk_pointer) as ptr_to_typ -> (* TODO (t4575417): this case does not work correctly for enums, but they are currently * broken in Infer anyway (see t4592290) *) - let (allocated_obj_exp, env) = inhabit_alloc typ None typ ModelBuiltins.__new env in + let (allocated_obj_exp, env) = inhabit_alloc typ None typ BuiltinDecl.__new env in (* select methods that are constructors and won't force us into infinite recursion because * we are already inhabiting one of their argument types *) let get_all_suitable_constructors (typ: Typ.t) = diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 18206d61f..78cf3a79b 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -339,10 +339,10 @@ let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t optio None let builtin_new = - Exp.Const (Const.Cfun ModelBuiltins.__new) + Exp.Const (Const.Cfun BuiltinDecl.__new) let builtin_get_array_length = - Exp.Const (Const.Cfun ModelBuiltins.__get_array_length) + Exp.Const (Const.Cfun BuiltinDecl.__get_array_length) let create_sil_deref exp typ loc = let no_id = Ident.create_none () in @@ -405,8 +405,8 @@ let rec expression (context : JContext.t) pc expr = JTransType.sizeof_of_object_type program tenv ot subtypes in let builtin = (match unop with - | JBir.InstanceOf _ -> Exp.Const (Const.Cfun ModelBuiltins.__instanceof) - | JBir.Cast _ -> Exp.Const (Const.Cfun ModelBuiltins.__cast) + | JBir.InstanceOf _ -> Exp.Const (Const.Cfun BuiltinDecl.__instanceof) + | JBir.Cast _ -> Exp.Const (Const.Cfun BuiltinDecl.__cast) | _ -> assert false) in let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.Tvoid)] in let ret_id = Ident.create_fresh Ident.knormal in @@ -519,7 +519,7 @@ let method_invocation let callee_procname = let proc = Procname.from_string_c_fun (JBasics.ms_name ms) in if JBasics.cn_equal cn' (JBasics.make_cn JConfig.infer_builtins_cl) && - Builtin.is_registered proc + BuiltinDecl.is_declared proc then proc else Procname.Java (JTransType.get_method_procname cn' ms method_kind) in let call_instrs = @@ -550,7 +550,7 @@ let method_invocation | (_, typ) as exp :: _ when Procname.is_constructor callee_procname && JTransType.is_closeable program tenv typ -> let set_file_attr = - let set_builtin = Exp.Const (Const.Cfun ModelBuiltins.__set_file_attribute) in + let set_builtin = Exp.Const (Const.Cfun BuiltinDecl.__set_file_attribute) in Sil.Call (None, set_builtin, [exp], loc, CallFlags.default) in (* Exceptions thrown in the constructor should prevent adding the resource attribute *) call_instrs @ [set_file_attr] @@ -559,7 +559,7 @@ let method_invocation | (_, typ) as exp :: [] when Procname.java_is_close callee_procname && JTransType.is_closeable program tenv typ -> let set_mem_attr = - let set_builtin = Exp.Const (Const.Cfun ModelBuiltins.__set_mem_attribute) in + let set_builtin = Exp.Const (Const.Cfun BuiltinDecl.__set_mem_attribute) in Sil.Call (None, set_builtin, [exp], loc, CallFlags.default) in (* Exceptions thrown in the close method should not prevent the resource from being *) (* considered as closed *) @@ -690,7 +690,7 @@ let is_this expr = let assume_not_null loc sil_expr = - let builtin_infer_assume = Exp.Const (Const.Cfun ModelBuiltins.__infer_assume) in + let builtin_infer_assume = Exp.Const (Const.Cfun BuiltinDecl.__infer_assume) in let not_null_expr = Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in let assume_call_flag = { CallFlags.default with CallFlags.cf_noreturn = true; } in @@ -818,7 +818,7 @@ let rec instruction (context : JContext.t) pc instr : translation = JContext.add_goto_jump context pc JContext.Exit; Instr node | JBir.New (var, cn, constr_type_list, constr_arg_list) -> - let builtin_new = Exp.Const (Const.Cfun ModelBuiltins.__new) in + let builtin_new = Exp.Const (Const.Cfun BuiltinDecl.__new) in let class_type = JTransType.get_class_type program tenv cn in let class_type_np = JTransType.get_class_type_no_pointer program tenv cn in let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in @@ -840,7 +840,7 @@ let rec instruction (context : JContext.t) pc instr : translation = Cg.add_edge cg caller_procname constr_procname; Instr node | JBir.NewArray (var, vt, expr_list) -> - let builtin_new_array = Exp.Const (Const.Cfun ModelBuiltins.__new_array) in + let builtin_new_array = Exp.Const (Const.Cfun BuiltinDecl.__new_array) in let content_type = JTransType.value_type program tenv vt in let array_type = JTransType.create_array_type content_type (IList.length expr_list) in let array_name = JContext.set_pvar context var array_type in @@ -1016,7 +1016,7 @@ let rec instruction (context : JContext.t) pc instr : translation = and ret_id = Ident.create_fresh Ident.knormal and sizeof_expr = JTransType.sizeof_of_object_type program tenv object_type Subtype.subtypes_instof in - let check_cast = Exp.Const (Const.Cfun ModelBuiltins.__instanceof) in + let check_cast = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in let args = [(sil_expr, sil_type); (sizeof_expr, Typ.Tvoid)] in let call = Sil.Call (Some (ret_id, ret_type), check_cast, args, loc, CallFlags.default) in let res_ex = Exp.Var ret_id in @@ -1050,11 +1050,11 @@ let rec instruction (context : JContext.t) pc instr : translation = Prune (is_instance_node, throw_cast_exception_node) | JBir.MonitorEnter expr -> trans_monitor_enter_exit - context expr pc loc ModelBuiltins.__set_locked_attribute "MonitorEnter" + context expr pc loc BuiltinDecl.__set_locked_attribute "MonitorEnter" | JBir.MonitorExit expr -> trans_monitor_enter_exit - context expr pc loc ModelBuiltins.__delete_locked_attribute "MonitorExit" + context expr pc loc BuiltinDecl.__delete_locked_attribute "MonitorExit" | _ -> Skip with Frontend_error s -> diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index 95db3ca11..fecf5d859 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -40,7 +40,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle let instr_get_ret_val = Sil.Load (id_ret_val, Exp.Lvar ret_var, ret_type, loc) in let instr_deactivate_exn = Sil.Store (Exp.Lvar ret_var, ret_type, Exp.null, loc) in let instr_unwrap_ret_val = - let unwrap_builtin = Exp.Const (Const.Cfun ModelBuiltins.__unwrap_exception) in + let unwrap_builtin = Exp.Const (Const.Cfun BuiltinDecl.__unwrap_exception) in Sil.Call (Some (id_exn_val, ret_type), unwrap_builtin, [(Exp.Var id_ret_val, ret_type)], loc, CallFlags.default) in @@ -68,7 +68,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle | _ -> assert false in let id_instanceof = Ident.create_fresh Ident.knormal in let instr_call_instanceof = - let instanceof_builtin = Exp.Const (Const.Cfun ModelBuiltins.__instanceof) in + let instanceof_builtin = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in let args = [ (Exp.Var id_exn_val, Typ.Tptr(exn_type, Typ.Pk_pointer)); (Exp.Sizeof (exn_type, None, Subtype.exact), Typ.Tvoid)] in diff --git a/infer/src/quandary/CppTrace.ml b/infer/src/quandary/CppTrace.ml index 544030ecf..8ca66fe99 100644 --- a/infer/src/quandary/CppTrace.ml +++ b/infer/src/quandary/CppTrace.ml @@ -68,7 +68,7 @@ module CppSource = struct | "__infer_taint_source" -> Some (make Other site) | _ -> None end - | pname when Builtin.is_registered pname -> + | pname when BuiltinDecl.is_declared pname -> None | pname -> failwithf "Non-C++ procname %a in C++ analysis@." Procname.pp pname @@ -145,7 +145,7 @@ module CppSink = struct | _ -> [] end - | pname when Builtin.is_registered pname -> + | pname when BuiltinDecl.is_declared pname -> [] | pname -> failwithf "Non-C++ procname %a in C++ analysis@." Procname.pp pname diff --git a/infer/src/quandary/JavaTaintAnalysis.ml b/infer/src/quandary/JavaTaintAnalysis.ml index c08845dd9..856035793 100644 --- a/infer/src/quandary/JavaTaintAnalysis.ml +++ b/infer/src/quandary/JavaTaintAnalysis.ml @@ -89,7 +89,7 @@ include | _ -> [] end - | pname when Builtin.is_registered pname -> + | pname when BuiltinDecl.is_declared pname -> [] | pname -> failwithf "Non-Java procname %a in Java analysis@." Procname.pp pname diff --git a/infer/src/quandary/JavaTrace.ml b/infer/src/quandary/JavaTrace.ml index 3f0f8970d..da127e2cb 100644 --- a/infer/src/quandary/JavaTrace.ml +++ b/infer/src/quandary/JavaTrace.ml @@ -78,7 +78,7 @@ module JavaSource = struct | _ -> None end - | pname when Builtin.is_registered pname -> None + | pname when BuiltinDecl.is_declared pname -> None | pname -> failwithf "Non-Java procname %a in Java analysis@." Procname.pp pname let compare src1 src2 = @@ -177,7 +177,7 @@ module JavaSink = struct | _ -> [] end - | pname when Builtin.is_registered pname -> [] + | pname when BuiltinDecl.is_declared pname -> [] | pname -> failwithf "Non-Java procname %a in Java analysis@." Procname.pp pname let to_callee t callee_site = diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index fe3e020f9..4c2662d4a 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -297,8 +297,8 @@ module Make (TaintSpec : TaintSpec.S) = struct astate' end | Sil.Call (Some (ret_id, _), Const (Cfun callee_pname), args, loc, _) - when Builtin.is_registered callee_pname -> - if Procname.equal callee_pname ModelBuiltins.__cast + when BuiltinDecl.is_declared callee_pname -> + if Procname.equal callee_pname BuiltinDecl.__cast then match args with | (cast_target, cast_typ) :: _ -> diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 96fbcc01a..b9a565395 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -124,7 +124,7 @@ module StructuredSil = struct let cast_id_to_id lhs cast_typ rhs = let lhs_id = ident_of_str lhs in let rhs_id = Exp.Var (ident_of_str rhs) in - make_call ~procname:ModelBuiltins.__cast (Some (lhs_id, cast_typ)) [rhs_id, cast_typ] + make_call ~procname:BuiltinDecl.__cast (Some (lhs_id, cast_typ)) [rhs_id, cast_typ] let var_assign_exp ~rhs_typ lhs rhs_exp = let lhs_exp = var_of_str lhs in