diff --git a/src/plugins/instantiate/Instantiate.mli b/src/plugins/instantiate/Instantiate.mli index 061723344f1df682af0b1900e95324f0cc451b5e..d47de410b8fddfe50846106aa801e72f649dd4a8 100644 --- a/src/plugins/instantiate/Instantiate.mli +++ b/src/plugins/instantiate/Instantiate.mli @@ -41,19 +41,20 @@ module Instantiator_builder: sig (** Name of the implemented instantiator function *) val function_name: string - (** [well_typed_call ret args] must return true if and only if the + (** [well_typed_call ret fct args] must return true if and only if the corresponding call is well typed in the sens that the generator can produce a function override for the corresponding return value and parameters, according to their types and/or values. *) - val well_typed_call: lval option -> exp list -> bool + val well_typed_call: lval option -> varinfo -> exp list -> bool - (** [key_from_call ret args] must return an identifier for the corresponding - call. [key_from_call ret1 args1] and [key_from_call ret2 args2] must equal - if and only if the same override function can be used for both call. Any - call for which [well_typed_call] returns true must be able to give a key. + (** [key_from_call ret fct args] must return an identifier for the + corresponding call. [key_from_call ret1 fct1 args1] and + [key_from_call ret2 fct2 args2] must equal if and only if the same + override function can be used for both call. Any call for which + [well_typed_call] returns true must be able to give a key. *) - val key_from_call: lval option -> exp list -> override_key + val key_from_call: lval option -> varinfo -> exp list -> override_key (** [retype_args key args] must returns a new argument list compatible with the function identified by [override_key]. [args] is the list of arguments diff --git a/src/plugins/instantiate/instantiator_builder.ml b/src/plugins/instantiate/instantiator_builder.ml index 6b98b3ad9d26c521d5cbb90be41c7c45bed3383f..74242ed7bb5f1a50f2fbde264954abda3404141e 100644 --- a/src/plugins/instantiate/instantiator_builder.ml +++ b/src/plugins/instantiate/instantiator_builder.ml @@ -28,8 +28,8 @@ module type Generator_sig = sig type override_key = Hashtbl.key val function_name: string - val well_typed_call: lval option -> exp list -> bool - val key_from_call: lval option -> exp list -> override_key + val well_typed_call: lval option -> varinfo -> exp list -> bool + val key_from_call: lval option -> varinfo -> exp list -> override_key val retype_args: override_key -> exp list -> exp list val args_for_original: override_key -> exp list -> exp list val generate_prototype: override_key -> (string * typ) @@ -41,8 +41,8 @@ module type Instantiator = sig type override_key val function_name: string - val well_typed_call: lval option -> exp list -> bool - val key_from_call: lval option -> exp list -> override_key + val well_typed_call: lval option -> varinfo -> exp list -> bool + val key_from_call: lval option -> varinfo -> exp list -> override_key val retype_args: override_key -> exp list -> exp list val get_override: override_key -> fundec val get_kfs: unit -> kernel_function list diff --git a/src/plugins/instantiate/instantiator_builder.mli b/src/plugins/instantiate/instantiator_builder.mli index 87c268d2d49824682e3f4e2d0ddfa18cd7d081ba..b0eb2f79fcf975b1957079beed9ac29d32c14e6d 100644 --- a/src/plugins/instantiate/instantiator_builder.mli +++ b/src/plugins/instantiate/instantiator_builder.mli @@ -40,19 +40,20 @@ module type Generator_sig = sig (** Name of the implemented function *) val function_name: string - (** [well_typed_call ret args] must return true if and only if the + (** [well_typed_call ret fct args] must return true if and only if the corresponding call is well typed in the sens that the generator can produce a function override for the corresponding return value and parameters, according to their types and/or values. *) - val well_typed_call: lval option -> exp list -> bool + val well_typed_call: lval option -> varinfo -> exp list -> bool - (** [key_from_call ret args] must return an identifier for the corresponding - call. [key_from_call ret1 args1] and [key_from_call ret2 args2] must equal - if and only if the same override function can be used for both call. Any - call for which [well_typed_call] returns true must be able to give a key. + (** [key_from_call ret fct args] must return an identifier for the + corresponding call. [key_from_call ret1 fct1 args1] and + [key_from_call ret2 fct2 args2] must equal if and only if the same + override function can be used for both call. Any call for which + [well_typed_call] returns true must be able to give a key. *) - val key_from_call: lval option -> exp list -> override_key + val key_from_call: lval option -> varinfo -> exp list -> override_key (** [retype_args key args] must returns a new argument list compatible with the function identified by [override_key]. [args] is the list of arguments @@ -105,9 +106,9 @@ module type Instantiator = sig (** Same as [Generator_sig.override_key] *) val function_name: string (** Same as [Generator_sig.override_key] *) - val well_typed_call: lval option -> exp list -> bool + val well_typed_call: lval option -> varinfo -> exp list -> bool (** Same as [Generator_sig.override_key] *) - val key_from_call: lval option -> exp list -> override_key + val key_from_call: lval option -> varinfo -> exp list -> override_key (** Same as [Generator_sig.override_key] *) val retype_args: override_key -> exp list -> exp list diff --git a/src/plugins/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml index 1e064706c5b6eb1a4230eb414f71e60a1fc9689e..89af52fd24d8e1b71b7bc6468b506bdb65bf8c68 100644 --- a/src/plugins/instantiate/stdlib/calloc.ml +++ b/src/plugins/instantiate/stdlib/calloc.ml @@ -131,21 +131,21 @@ let generate_prototype alloc_type = ] in name, (TFun((ptr_of alloc_type), Some params, false, [])) -let well_typed_call ret args = +let well_typed_call ret fct args = match ret, args with - | Some ret, [ _ ; _ ] -> + | Some ret, [ _ ; _ ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> let t = Cil.typeOfLval ret in Cil.isPointerType t && not (Cil.isVoidPtrType t) && Cil.isCompleteType (Cil.typeOf_pointed t) | _ -> false -let key_from_call ret _ = +let key_from_call ret fct _ = match ret with - | Some ret -> + | Some ret when Cil.hasAttribute "fc_stdlib" fct.vattr -> let ret_t = Cil.unrollTypeDeep (Cil.typeOfLval ret) in let ret_t = Cil.type_remove_qualifier_attributes_deep ret_t in Cil.typeOf_pointed ret_t - | None -> unexpected "trying to generate a key on an ill-typed call" + | _ -> unexpected "trying to generate a key on an ill-typed call" let retype_args _typ args = args let args_for_original _typ args = args diff --git a/src/plugins/instantiate/stdlib/free.ml b/src/plugins/instantiate/stdlib/free.ml index 7ef4c509bb20f13e505b79ab71a2feabc99d5436..ec63f84f4aa307d5cec0d97d4ba8f6c5b8f25d0b 100644 --- a/src/plugins/instantiate/stdlib/free.ml +++ b/src/plugins/instantiate/stdlib/free.ml @@ -83,16 +83,16 @@ let generate_prototype alloc_t = ] in name, (TFun(Cil.voidType, Some params, false, [])) -let well_typed_call _ret args = +let well_typed_call _ret fct args = match args with - | [ ptr ] -> + | [ ptr ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> let t = Cil.typeOf (Cil.stripCasts ptr) in Cil.isPointerType t && not (Cil.isVoidPtrType t) | _ -> false -let key_from_call _ret args = +let key_from_call _ret fct args = match args with - | [ ptr ] -> + | [ ptr ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> let ptr = Cil.stripCasts ptr in let ptr_t = Cil.unrollTypeDeep (Cil.typeOf ptr) in let ptr_t = Cil.type_remove_qualifier_attributes_deep ptr_t in diff --git a/src/plugins/instantiate/stdlib/malloc.ml b/src/plugins/instantiate/stdlib/malloc.ml index 16521b530aebe5561a445c1e30216d24b338feef..fbf3374bcdd266c04f82936c4a422e903f64b196 100644 --- a/src/plugins/instantiate/stdlib/malloc.ml +++ b/src/plugins/instantiate/stdlib/malloc.ml @@ -70,21 +70,21 @@ let generate_prototype alloc_t = ] in name, (TFun((ptr_of alloc_t), Some params, false, [])) -let well_typed_call ret args = +let well_typed_call ret fct args = match ret, args with - | Some ret, [ _ ] -> + | Some ret, [ _ ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> let t = Cil.typeOfLval ret in Cil.isPointerType t && not (Cil.isVoidPtrType t) && Cil.isCompleteType (Cil.typeOf_pointed t) | _ -> false -let key_from_call ret _ = +let key_from_call ret fct _ = match ret with - | Some ret -> + | Some ret when Cil.hasAttribute "fc_stdlib" fct.vattr -> let ret_t = Cil.unrollTypeDeep (Cil.typeOfLval ret) in let ret_t = Cil.type_remove_qualifier_attributes_deep ret_t in Cil.typeOf_pointed ret_t - | None -> unexpected "trying to generate a key on an ill-typed call" + | _ -> unexpected "trying to generate a key on an ill-typed call" let retype_args _typ args = args let args_for_original _typ args = args diff --git a/src/plugins/instantiate/string/mem_utils.ml b/src/plugins/instantiate/string/mem_utils.ml index 9d88bb79b94c2361688d64793874fc85360ca382..02ccd376309958c77e2e5701327a2567db8d2bbe 100644 --- a/src/plugins/instantiate/string/mem_utils.ml +++ b/src/plugins/instantiate/string/mem_utils.ml @@ -128,9 +128,10 @@ struct let name = F.name ^ "_" ^ (string_of_typ t) in name, ftype - let well_typed_call lval args = + let well_typed_call lval fct args = let _, ps = F.prototype () in if List.length args <> List.length ps then false + else if not (Cil.hasAttribute "fc_stdlib" fct.vattr) then false else let extract e = function | _, (CPtr | Ptr), _ -> exp_type_of_pointed e @@ -157,10 +158,12 @@ struct in List.map2 retype args ps - let key_from_call _ret args = + let key_from_call _ret fct args = let _, ps = F.prototype () in match ps, args with - | (_, (Ptr|CPtr), _)::ps, fst::args when List.(length ps = length args) -> + | (_, (Ptr|CPtr), _) :: ps, fst :: args + when List.(length ps = length args) + && Cil.hasAttribute "fc_stdlib" fct.vattr -> begin match exp_type_of_pointed fst with | Value_of t -> t | _ -> diff --git a/src/plugins/instantiate/string/mem_utils.mli b/src/plugins/instantiate/string/mem_utils.mli index d4b205be01ee5ee4ca8cd05ec4b0630cd4e76202..fca57bd58d0ed47e5acccb5cb39bbe5fd55a12c8 100644 --- a/src/plugins/instantiate/string/mem_utils.mli +++ b/src/plugins/instantiate/string/mem_utils.mli @@ -44,9 +44,9 @@ end module Make (F: Function) : sig val generate_function_type : typ -> typ val generate_prototype : typ -> string * typ - val well_typed_call : lval option -> exp list -> bool - val retype_args : 'a -> exp list -> exp list - val key_from_call : 'a -> exp list -> typ + val well_typed_call : lval option -> varinfo -> exp list -> bool + val retype_args : typ -> exp list -> exp list + val key_from_call : lval option -> varinfo -> exp list -> typ end (** location -> key -> s1 -> s2 -> len -> spec_result *) diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml index b62c37aa2caf64cadded791992bd87d7c44eb2cc..21e44be2106cd71a710f2a9992cab90110011752 100644 --- a/src/plugins/instantiate/string/memset.ml +++ b/src/plugins/instantiate/string/memset.ml @@ -195,8 +195,8 @@ let rec contains_union_type t = contains_union_type t | _ -> false -let well_typed_call _ret = function - | [ ptr ; value ; _ ] -> +let well_typed_call _ret fct = function + | [ ptr ; value ; _ ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> begin match Mem_utils.exp_type_of_pointed ptr, memset_value value with | (No_pointed | Of_null _) , _ -> false | Value_of t , _ when any_char_composed_type t -> true @@ -208,8 +208,8 @@ let well_typed_call _ret = function end | _ -> false -let key_from_call _ret = function - | [ ptr ; value ; _ ] -> +let key_from_call _ret fct = function + | [ ptr ; value ; _ ] when Cil.hasAttribute "fc_stdlib" fct.vattr -> begin match Mem_utils.exp_type_of_pointed ptr, memset_value value with | Value_of t, _ when any_char_composed_type t -> t, None | Value_of t, value when not (contains_union_type t) -> t, value diff --git a/src/plugins/instantiate/tests/api/external_instantiator_registration.ml b/src/plugins/instantiate/tests/api/external_instantiator_registration.ml index b800bd1efbdd4bd92fe985fab4771f1f001c95cd..aa3c9b5c6a425206aeae937f7d69d88e2f9db39c 100644 --- a/src/plugins/instantiate/tests/api/external_instantiator_registration.ml +++ b/src/plugins/instantiate/tests/api/external_instantiator_registration.ml @@ -1,12 +1,12 @@ let function_name = "mine" -let well_typed_call _ = function +let well_typed_call _ _ = function | [ e ] -> let t = Cil.typeOf(Cil.stripCasts e) in not (Cil.isVoidPtrType t) && Cil.isPointerType t | _ -> false -let key_from_call _ = function +let key_from_call _ _ = function | [ e ] -> let t = Cil.typeOf(Cil.stripCasts e) in Cil.typeOf_pointed t diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml index c1f0f29d170495ca9c3421cf725d8c3d5c7a8d37..4970a5913e2b477160548a6b11b34155ad5124d2 100644 --- a/src/plugins/instantiate/transform.ml +++ b/src/plugins/instantiate/transform.ml @@ -90,8 +90,8 @@ class transformer = object(self) method private replace_call (lval, fct, args) = try let module I = (val (self#find_enabled_instantiator fct): Instantiator) in - if I.well_typed_call lval args then - let key = I.key_from_call lval args in + if I.well_typed_call lval fct args then + let key = I.key_from_call lval fct args in let fundec = I.get_override key in let new_args = I.retype_args key args in Queue.add fundec used_instantiator_last_kf ;