From d94a33f4b0a592ce22f6cf67970f541358d4f6e4 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 22 Oct 2019 15:40:17 +0200
Subject: [PATCH] [Builtin] Adds return value to builtin selection
---
src/plugins/builtin/builtin_builder.ml | 8 ++++----
src/plugins/builtin/builtin_builder.mli | 8 ++++----
src/plugins/builtin/memcmp.ml | 4 ++--
src/plugins/builtin/memcpy.ml | 4 ++--
src/plugins/builtin/memmove.ml | 4 ++--
src/plugins/builtin/memset.ml | 4 ++--
src/plugins/builtin/transform.ml | 10 +++++-----
7 files changed, 21 insertions(+), 21 deletions(-)
diff --git a/src/plugins/builtin/builtin_builder.ml b/src/plugins/builtin/builtin_builder.ml
index 12299a7886d..c3c201351ed 100644
--- a/src/plugins/builtin/builtin_builder.ml
+++ b/src/plugins/builtin/builtin_builder.ml
@@ -28,8 +28,8 @@ module type Generator_sig = sig
type override_key = Hashtbl.key
val function_name: string
- val well_typed_call: exp list -> bool
- val key_from_call: exp list -> override_key
+ val well_typed_call: lval option -> exp list -> bool
+ val key_from_call: lval option -> exp list -> override_key
val retype_args: override_key -> exp list -> exp list
val generate_prototype: override_key -> (string * typ)
val generate_spec: override_key -> fundec -> location -> funspec
@@ -41,8 +41,8 @@ module type Builtin = sig
type override_key
val function_name: string
- val well_typed_call: exp list -> bool
- val key_from_call: exp list -> override_key
+ val well_typed_call: lval option -> exp list -> bool
+ val key_from_call: lval option -> 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/builtin/builtin_builder.mli b/src/plugins/builtin/builtin_builder.mli
index f45a623f370..7e16ff3d2f6 100644
--- a/src/plugins/builtin/builtin_builder.mli
+++ b/src/plugins/builtin/builtin_builder.mli
@@ -27,8 +27,8 @@ module type Generator_sig = sig
type override_key = Hashtbl.key
val function_name: string
- val well_typed_call: exp list -> bool
- val key_from_call: exp list -> override_key
+ val well_typed_call: lval option -> exp list -> bool
+ val key_from_call: lval option -> exp list -> override_key
val retype_args: override_key -> exp list -> exp list
val generate_prototype: override_key -> (string * typ)
val generate_spec: override_key -> fundec -> location -> funspec
@@ -40,8 +40,8 @@ module type Builtin = sig
type override_key
val function_name: string
- val well_typed_call: exp list -> bool
- val key_from_call: exp list -> override_key
+ val well_typed_call: lval option -> exp list -> bool
+ val key_from_call: lval option -> 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/builtin/memcmp.ml b/src/plugins/builtin/memcmp.ml
index 96dcef8d6ae..b6052d003d2 100644
--- a/src/plugins/builtin/memcmp.ml
+++ b/src/plugins/builtin/memcmp.ml
@@ -96,13 +96,13 @@ let type_from_arg x =
let xt = Cil.type_remove_qualifier_attributes_deep xt in
Cil.typeOf_pointed xt
-let well_typed_call = function
+let well_typed_call _ret = function
| [ s1 ; s2 ; len ] ->
(Cil.isIntegralType (Cil.typeOf len)) &&
(Cil_datatype.Typ.equal (type_from_arg s1) (type_from_arg s2))
| _ -> false
-let key_from_call = function
+let key_from_call _ret = function
| [ s1 ; _ ; _ ] -> type_from_arg s1
| _ -> failwith "Call to Memmove.key_from_call on an ill-typed builtin call"
diff --git a/src/plugins/builtin/memcpy.ml b/src/plugins/builtin/memcpy.ml
index 84cbca6cd61..c69f8761334 100644
--- a/src/plugins/builtin/memcpy.ml
+++ b/src/plugins/builtin/memcpy.ml
@@ -102,13 +102,13 @@ let type_from_arg x =
let xt = Cil.type_remove_qualifier_attributes_deep xt in
Cil.typeOf_pointed xt
-let well_typed_call = function
+let well_typed_call _ret = function
| [ dest ; src ; len ] ->
(Cil.isIntegralType (Cil.typeOf len)) &&
(Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src))
| _ -> false
-let key_from_call = function
+let key_from_call _ret = function
| [ dest ; _ ; _ ] -> type_from_arg dest
| _ -> failwith "Call to Memcpy.key_from_call on an ill-typed builtin call"
diff --git a/src/plugins/builtin/memmove.ml b/src/plugins/builtin/memmove.ml
index 67e7ec47962..e0445c020be 100644
--- a/src/plugins/builtin/memmove.ml
+++ b/src/plugins/builtin/memmove.ml
@@ -96,13 +96,13 @@ let type_from_arg x =
let xt = Cil.type_remove_qualifier_attributes_deep xt in
Cil.typeOf_pointed xt
-let well_typed_call = function
+let well_typed_call _ret = function
| [ dest ; src ; len ] ->
(Cil.isIntegralType (Cil.typeOf len)) &&
(Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src))
| _ -> false
-let key_from_call = function
+let key_from_call _ret = function
| [ dest ; _ ; _ ] -> type_from_arg dest
| _ -> failwith "Call to Memmove.key_from_call on an ill-typed builtin call"
diff --git a/src/plugins/builtin/memset.ml b/src/plugins/builtin/memset.ml
index ef758fbcf6e..9be7f29ca81 100644
--- a/src/plugins/builtin/memset.ml
+++ b/src/plugins/builtin/memset.ml
@@ -187,7 +187,7 @@ let is_union_type = function
| TComp({ cstruct = false }, _, _) -> true
| _ -> false
-let well_typed_call = function
+let well_typed_call _ret = function
| [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) -> true
| [ ptr ; _ ; _ ] when is_union_type (type_from_arg ptr) -> false
| [ _ ; value ; _ ] ->
@@ -197,7 +197,7 @@ let well_typed_call = function
end
| _ -> false
-let key_from_call = function
+let key_from_call _ret = function
| [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) ->
(type_from_arg ptr), None
| [ ptr ; value ; _ ] when not (is_union_type (type_from_arg ptr)) ->
diff --git a/src/plugins/builtin/transform.ml b/src/plugins/builtin/transform.ml
index a8265b21159..c501c73ee29 100644
--- a/src/plugins/builtin/transform.ml
+++ b/src/plugins/builtin/transform.ml
@@ -91,11 +91,11 @@ class transformer = object(self)
if not (B.Enabled.get ()) then raise Not_found ;
builtin
- method private replace_call (fct, args) =
+ method private replace_call (lval, fct, args) =
try
let module B = (val (self#find_enabled_builtin fct): Builtin) in
- if B.well_typed_call args then
- let key = B.key_from_call args in
+ if B.well_typed_call lval args then
+ let key = B.key_from_call lval args in
let fundec = B.get_override key in
let new_args = B.retype_args key args in
Queue.add fundec used_builtin_last_kf ;
@@ -111,10 +111,10 @@ class transformer = object(self)
| Call(_) | Local_init(_, ConsInit(_, _, Plain_func), _) ->
let change = function
| [ Call(r, ({ enode = Lval((Var f), NoOffset) } as e), args, loc) ] ->
- let f, args = self#replace_call (f, args) in
+ let f, args = self#replace_call (r, f, args) in
[ Call(r, { e with enode = Lval((Var f), NoOffset) }, args, loc) ]
| [ Local_init(r, ConsInit(f, args, Plain_func), loc) ] ->
- let f, args = self#replace_call (f, args) in
+ let f, args = self#replace_call (Some (Cil.var r), f, args) in
[ Local_init(r, ConsInit(f, args, Plain_func), loc) ]
| _ -> assert false
in
--
GitLab