From 49cd989a1c992317c000a608d462cf0b2ec3ff7f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 26 Mar 2020 18:16:35 +0100
Subject: [PATCH] [Instantiate] Takes care of constants in Memset
---
src/plugins/instantiate/basic_blocks.ml | 3 +-
src/plugins/instantiate/string/memset.ml | 42 +++++++++++-------------
2 files changed, 22 insertions(+), 23 deletions(-)
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index 830911e482e..0fcd642c58f 100644
--- a/src/plugins/instantiate/basic_blocks.ml
+++ b/src/plugins/instantiate/basic_blocks.ml
@@ -54,7 +54,8 @@ let exp_type_of_pointed x =
let no_cast = Cil.stripCasts x in
if not (Cil.isPointerType (Cil.typeOf no_cast)) then
match Cil.constFoldToInt x with
- | Some t when Integer.(equal t (of_int 0)) -> Some (Cil.typeOf x)
+ | Some t when Integer.(equal t (of_int 0)) ->
+ Some (Cil.typeOf_pointed (Cil.typeOf x))
| _ -> None
else
let xt = Cil.unrollTypeDeep (Cil.typeOf no_cast) in
diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index 393f6ae626b..3eef4cdd5b9 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -175,12 +175,6 @@ let generate_spec (_t, e) { svar = vi } loc =
let ensures = generate_ensures e loc t ptr value len in
make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
-let type_from_arg x =
- let x = Cil.stripCasts x in
- let xt = Cil.unrollTypeDeep (Cil.typeOf x) in
- let xt = Cil.type_remove_qualifier_attributes_deep xt in
- Cil.typeOf_pointed xt
-
let memset_value e =
let ff = Integer.of_int 255 in
match (Cil.constFold false e).enode with
@@ -199,22 +193,25 @@ let rec contains_union_type t =
| _ -> false
let well_typed_call _ret = function
- | [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) -> true
- | [ ptr ; _ ; _ ] when contains_union_type (type_from_arg ptr) -> false
- | [ ptr ; _ ; _ ] when Cil.isVoidType (type_from_arg ptr) -> false
- | [ ptr ; _ ; _ ] when not (Cil.isCompleteType (type_from_arg ptr)) -> false
- | [ _ ; value ; _ ] ->
- begin match memset_value value with
- | None -> false
- | Some _ -> true
+ | [ ptr ; value ; _ ] ->
+ begin match exp_type_of_pointed ptr, memset_value value with
+ | None , _ -> false
+ | Some t, _ when any_char_composed_type t -> true
+ | Some t, _ when contains_union_type t -> false
+ | Some t, _ when Cil.isVoidType t -> false
+ | Some t, _ when not (Cil.isCompleteType t) -> false
+ | _, None -> false
+ | _, Some _ -> true
end
| _ -> false
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 (contains_union_type (type_from_arg ptr)) ->
- (type_from_arg ptr), (memset_value value)
+ | [ ptr ; value ; _ ] ->
+ begin match exp_type_of_pointed ptr, memset_value value with
+ | Some t, _ when any_char_composed_type t -> t, None
+ | Some t, value when not (contains_union_type t) -> t, value
+ | _ , _ -> unexpected "trying to generate a key on an ill-typed call"
+ end
| _ -> unexpected "trying to generate a key on an ill-typed call"
let char_prototype t =
@@ -246,17 +243,18 @@ let generate_prototype = function
| _, _ ->
unexpected "trying to generate a prototype on an ill-typed call"
-let retype_args (t, e) args =
+let retype_args (_t, e) args =
match e, args with
| None, [ ptr ; v ; n ] ->
let ptr = Cil.stripCasts ptr in
- assert (any_char_composed_type (type_from_arg ptr)) ;
- let base_type = base_char_type (type_from_arg ptr) in
+ let base_type = match exp_type_of_pointed ptr with
+ | Some t -> base_char_type t
+ | None -> unexpected "trying to retype arguments on an ill-typed call"
+ in
let v = Cil.mkCast (Cil.stripCasts v) base_type in
[ ptr ; v ; n ]
| Some fv, [ ptr ; v ; n ] ->
let ptr = Cil.stripCasts ptr in
- assert (Cil_datatype.Typ.equal (type_from_arg ptr) t) ;
assert (match memset_value v with Some x when x = fv -> true | _ -> false) ;
[ ptr ; n ]
| _ ->
--
GitLab