pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Cleanup code for registering builtins.

Browse Source 
Reviewed By: jvillard

Differential Revision: D2959998

fb-gh-sync-id: b7e7083
shipit-source-id: b7e7083
master
Cristiano Calcagno 9 years ago committed by facebook-github-bot-5
parent bf2909dd34
commit c570d97ad8
1 changed files with 192 additions and 81 deletions
Show Stats Download Patch File Download Diff File

273
infer/src/backend/symExec.ml
Unescape View File

@ -2417,13 +2417,14 @@ module ModelBuiltins = struct
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
(* forces the expression passed as parameter to be assumed true at the point where this (* forces the expression passed as parameter to be assumed true at the point where this
builtin is called, blocks if this causes an inconsistency *) builtin is called, diverges if this causes an inconsistency *)
let execute___infer_assume _ _ _ _ prop path _ args _ _ let execute___infer_assume _ _ _ _ prop path _ args _ _
: Builtin.ret_typ = : Builtin.ret_typ =
match args with match args with
| [(lexp, _)] -> | [(lexp, _)] ->
let prop_assume = Prop.conjoin_eq lexp (Sil.exp_bool true) prop in let prop_assume = Prop.conjoin_eq lexp (Sil.exp_bool true) prop in
if Prover.check_inconsistency prop_assume then execute_diverge prop_assume path if Prover.check_inconsistency prop_assume
then execute_diverge prop_assume path
else [(prop_assume, path)] else [(prop_assume, path)]
| _ -> raise (Exceptions.Wrong_argument_number __POS__) | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -2457,86 +2458,196 @@ module ModelBuiltins = struct
Sil.Set (Sil.Lvar Sil.custom_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in Sil.Set (Sil.Lvar Sil.custom_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in
sym_exec_generated true cfg tenv pdesc [set_instr] [(prop, path)] sym_exec_generated true cfg tenv pdesc [set_instr] [(prop, path)]
let _ = Builtin.register "__method_set_ignore_attribute" execute___method_set_ignore_attribute let __assert_fail = Builtin.register
let _ = Builtin.register "__builtin_va_arg" execute___builtin_va_arg (* model va_arg *) "__assert_fail" execute___assert_fail
let _ = Builtin.register "__builtin_va_copy" execute_skip (** NOTE: __builtin_va_copy should have been handled in the translation already (see frontend.ml) *) let _ = Builtin.register
let _ = Builtin.register "__builtin_va_end" execute_skip (* model va_end as skip *) (* model for va_arg *)
let _ = Builtin.register "__builtin_va_start" execute_skip (** NOTE: __builtin_va_start should have been handled in the translation already (see frontend.ml) *) "__builtin_va_arg" execute___builtin_va_arg
let __create_tuple = Builtin.register "__create_tuple" execute___create_tuple (* create a tuple value from the arguments *) let _ = Builtin.register
let __delete = Builtin.register "__delete" (execute_free Sil.Mnew) (* like free *) "__builtin_va_copy" execute_skip
let __delete_array = Builtin.register "__delete_array" (execute_free Sil.Mnew_array) (* like free *) let _ = Builtin.register
let __exit = Builtin.register "_exit" execute_exit (* _exit from C library *) (* model va_end as skip *)
let __get_array_size = Builtin.register "__get_array_size" execute___get_array_size (* return the size of the array passed as a parameter *) "__builtin_va_end" execute_skip
let _ = Builtin.register "__get_hidden_field" execute___get_hidden_field (* return the value of a hidden field in the struct *) let _ = Builtin.register
let __get_type_of = Builtin.register "__get_type_of" execute___get_type_of (* return the get the type of the allocated object passed as a parameter *) "__builtin_va_start" execute_skip
let __instanceof = Builtin.register "__instanceof" execute___instanceof (** [__instanceof(val,typ)] implements java's [val instanceof typ] *) let __cast = Builtin.register
let __cast = Builtin.register "__cast" execute___cast (** [__cast(val,typ)] implements java's [typ(val)] *) (* [__cast(val,typ)] implements java's [typ(val)] *)
let __new = Builtin.register "__new" (execute_alloc Sil.Mnew false) (* like malloc, but always succeeds *) "__cast" execute___cast
let __new_array = Builtin.register "__new_array" (execute_alloc Sil.Mnew_array false) (* like malloc, but always succeeds *) let _ = Builtin.register
let __objc_alloc = Builtin.register "__objc_alloc" (execute_alloc Sil.Mobjc true) (* Objective C alloc *) (* report a taint error if the parameter is tainted, and assume it is untainted afterward *)
let __objc_alloc_no_fail = Builtin.register "__objc_alloc_no_fail" (execute_alloc Sil.Mobjc false) (* like __objc_alloc, but does not return nil *) "__check_untainted" execute___check_untainted
let __placement_delete = Builtin.register "__placement_delete" execute_skip (* placement delete is skip *) let __create_tuple = Builtin.register
let __placement_new = Builtin.register "__placement_new" execute_return_first_argument (* placement new returns the first argument *) (* create a tuple value from the arguments *)
let _ = Builtin.register "__print_value" execute___print_value (* print a value as seen by the engine *) "__create_tuple" execute___create_tuple
let __set_array_size = Builtin.register "__set_array_size" execute___set_array_size (* set the size of the array passed as a parameter *) let __delete = Builtin.register
let __set_file_attribute = Builtin.register "__set_file_attribute" execute___set_file_attribute (* set the attribute of the parameter as file *) (* like free *)
let __set_lock_attribute = Builtin.register "__set_lock_attribute" execute___set_lock_attribute (* set the attribute of the parameter as file *) "__delete" (execute_free Sil.Mnew)
let __set_mem_attribute = Builtin.register "__set_mem_attribute" execute___set_mem_attribute (* set the attribute of the parameter as memory *) let __delete_array = Builtin.register
let __set_autorelease_attribute = Builtin.register "__set_autorelease_attribute" execute___set_autorelease_attribute (* set the attribute of the parameter as autorelease *) (* like free *)
(* set the observer attribute of the parameter *) "__delete_array" (execute_free Sil.Mnew_array)
let __set_observer_attribute = let __exit = Builtin.register
Builtin.register "__set_observer_attribute" (execute___set_attr Sil.Aobserver) (* _exit from C library *)
(* set the unregistered observer attribute of the parameter *) "_exit" execute_exit
let __set_unsubscribed_observer_attribute = let __get_array_size = Builtin.register
Builtin.register "__set_unsubscribed_observer_attribute" (* return the size of the array passed as a parameter *)
"__get_array_size" execute___get_array_size
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 Sil.Mnew false)
let __new_array = Builtin.register
(* like malloc, but always succeeds *)
"__new_array" (execute_alloc Sil.Mnew_array false)
let __objc_alloc = Builtin.register
(* Objective C alloc *)
"__objc_alloc" (execute_alloc Sil.Mobjc true)
let __objc_alloc_no_fail = Builtin.register
(* like __objc_alloc, but does not return nil *)
"__objc_alloc_no_fail" (execute_alloc Sil.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 __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_size = Builtin.register
(* set the size of the array passed as a parameter *)
"__set_array_size" execute___set_array_size
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 Sil.Aobserver)
let __set_unsubscribed_observer_attribute = Builtin.register
(* set the unregistered observer attribute of the parameter *)
"__set_unsubscribed_observer_attribute"
(execute___set_attr Sil.Aunsubscribed_observer) (execute___set_attr Sil.Aunsubscribed_observer)
let __objc_release_autorelease_pool = Builtin.register "__objc_release_autorelease_pool" execute___release_autorelease_pool (* set the attribute of the parameter as autorelease *) let __split_get_nth = Builtin.register
let __split_get_nth = Builtin.register "__split_get_nth" execute___split_get_nth (* splits a string given a separator and returns the nth string *) (* splits a string given a separator and returns the nth string *)
"__split_get_nth" execute___split_get_nth
(* builtin function to externally create new errors *) let _ = Builtin.register
let __infer_fail = Builtin.register "__infer_fail" execute___infer_fail (* set a hidden field in the struct to the given value *)
let __assert_fail = Builtin.register "__assert_fail" execute___assert_fail "__set_hidden_field" execute___set_hidden_field
let _ = Builtin.register
(* set a hidden field in the struct to the given value *) (* set the attribute of the parameter as tainted *)
let _ = Builtin.register "__set_hidden_field" execute___set_hidden_field "__set_taint_attribute" execute___set_taint_attribute
(* set the attribute of the parameter as tainted *) let _ = Builtin.register
let _ = Builtin.register "__set_taint_attribute" execute___set_taint_attribute (* set the attribute of the parameter as untainted *)
(* set the attribute of the parameter as untainted *) "__set_untaint_attribute" (execute___set_attr Sil.Auntaint)
let _ = Builtin.register "__set_untaint_attribute" (execute___set_attr Sil.Auntaint) let __set_locked_attribute = Builtin.register
(* set the attribute of the parameter as locked *) (* set the attribute of the parameter as locked *)
let __set_locked_attribute = "__set_locked_attribute" (execute___set_attr Sil.Alocked)
Builtin.register "__set_locked_attribute" (execute___set_attr Sil.Alocked) let __set_unlocked_attribute = Builtin.register
(* set the attribute of the parameter as unlocked *) (* set the attribute of the parameter as unlocked *)
let __set_unlocked_attribute = "__set_unlocked_attribute" (execute___set_attr Sil.Aunlocked)
Builtin.register "__set_unlocked_attribute" (execute___set_attr Sil.Aunlocked) let _ = Builtin.register
let _ = Builtin.register "__check_untainted" execute___check_untainted (* report a taint error if the parameter is tainted, and assume it is untainted afterward *) "__throw" execute_skip
let __objc_retain = Builtin.register "__objc_retain" execute___objc_retain (* objective-c "retain" *) let __tuple_get_nth = Builtin.register
let __objc_release = Builtin.register "__objc_release" execute___objc_release (* objective-c "release" *) (* return the nth element of a tuple *)
let __objc_retain_cf = Builtin.register "__objc_retain_cf" execute___objc_retain_cf (* objective-c "retain" *) "__tuple_get_nth" execute___tuple_get_nth
let __objc_release_cf = Builtin.register "__objc_release_cf" execute___objc_release_cf (* objective-c "release" *) let __unwrap_exception = Builtin.register
let __objc_cast = Builtin.register "__objc_cast" execute___objc_cast (* objective-c "cast" *) (* unwrap an exception *)
let _ = Builtin.register "__throw" execute_skip (** NOTE: __throw should have been handled in the translation already (see frontend.ml) *) "__unwrap_exception" execute__unwrap_exception
let __tuple_get_nth = Builtin.register "__tuple_get_nth" execute___tuple_get_nth (* return the nth element of a tuple *) let _ = Builtin.register
let __unwrap_exception = Builtin.register "__unwrap_exception" execute__unwrap_exception (* the correct function to unwrapp execption remains to be written *) (* abort from C library *)
let __infer_assume = Builtin.register "__infer_assume" execute___infer_assume "abort" execute_abort
let _ = Builtin.register "abort" execute_abort (* abort from C library *) let _ = Builtin.register
let _ = Builtin.register "exit" execute_exit (* exit from C library *) (* exit from C library *)
let _ = Builtin.register "free" (execute_free Sil.Mmalloc) (* free from C library, requires allocated memory *) "exit" execute_exit
let _ = Builtin.register "fscanf" (execute_scan_function 2) (* fscanf from C library *) let _ = Builtin.register
let _ = Builtin.register "fwscanf" (execute_scan_function 2) (* vsscanf from C library *) (* free from C library, requires allocated memory *)
let _ = Builtin.register "malloc" (execute_alloc Sil.Mmalloc true) (* malloc from C library *) "free" (execute_free Sil.Mmalloc)
let malloc_no_fail = Builtin.register "malloc_no_fail" (execute_alloc Sil.Mmalloc false) (* malloc from ObjC library *) let _ = Builtin.register
let _ = Builtin.register "pthread_create" execute_pthread_create (* register execution handler for pthread_create *) (* fscanf from C library *)
let _ = Builtin.register "scanf" (execute_scan_function 1) (* scanf from C library *) "fscanf" (execute_scan_function 2)
let _ = Builtin.register "sscanf" (execute_scan_function 2) (* sscanf from C library *) let _ = Builtin.register
let _ = Builtin.register "swscanf" (execute_scan_function 2) (* vsscanf from C library *) (* vsscanf from C library *)
let _ = Builtin.register "vfscanf" (execute_scan_function 2) (* vfwscanf from C library *) "fwscanf" (execute_scan_function 2)
let _ = Builtin.register "vfwscanf" (execute_scan_function 2) (* vsscanf from C library *) let _ = Builtin.register
let _ = Builtin.register "vscanf" (execute_scan_function 1) (* vscanf from C library *) (* malloc from C library *)
let _ = Builtin.register "vsscanf" (execute_scan_function 2) (* vsscanf from C library *) "malloc" (execute_alloc Sil.Mmalloc true)
let _ = Builtin.register "vswscanf" (execute_scan_function 2) (* vsscanf from C library *) let malloc_no_fail = Builtin.register
let _ = Builtin.register "vwscanf" (execute_scan_function 1) (* vsscanf from C library *) (* malloc from ObjC library *)
let _ = Builtin.register "wscanf" (execute_scan_function 1) (* vsscanf from C library *) "malloc_no_fail" (execute_alloc Sil.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 cfg pdesc tenv symb_state ret_ids typ loc = let execute_objc_alloc_no_fail cfg pdesc tenv symb_state ret_ids typ loc =
let alloc_fun = Sil.Const (Sil.Cfun __objc_alloc_no_fail) in let alloc_fun = Sil.Const (Sil.Cfun __objc_alloc_no_fail) in

Write Preview
Loading…
Cancel
Save