From c67732283d828aa9f5ea795f14749210d2761bbd Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Mar 2020 09:01:43 +0100
Subject: [PATCH] [Instantiate] Moves a not generic function from basic_blocks
to mem_utils
---
src/plugins/instantiate/basic_blocks.ml | 12 -----
src/plugins/instantiate/basic_blocks.mli | 5 --
src/plugins/instantiate/string/mem_utils.ml | 49 ++++++++++++++------
src/plugins/instantiate/string/mem_utils.mli | 19 +++++++-
src/plugins/instantiate/string/memcmp.ml | 8 +++-
src/plugins/instantiate/string/memcpy.ml | 8 +++-
src/plugins/instantiate/string/memmove.ml | 8 +++-
src/plugins/instantiate/string/memset.ml | 24 +++++-----
8 files changed, 85 insertions(+), 48 deletions(-)
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index 0fcd642c58f..660db8c83c0 100644
--- a/src/plugins/instantiate/basic_blocks.ml
+++ b/src/plugins/instantiate/basic_blocks.ml
@@ -50,18 +50,6 @@ let call_function lval vi args =
let args = List.map2 gen_arg args typs in
Call(lval, (Cil.evar vi), args, loc)
-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_pointed (Cil.typeOf x))
- | _ -> None
- else
- let xt = Cil.unrollTypeDeep (Cil.typeOf no_cast) in
- let xt = Cil.type_remove_qualifier_attributes_deep xt in
- Some (Cil.typeOf_pointed xt)
-
let rec string_of_typ_aux = function
| TVoid(_) -> "void"
| TInt(IBool, _) -> "bool"
diff --git a/src/plugins/instantiate/basic_blocks.mli b/src/plugins/instantiate/basic_blocks.mli
index d8723d96765..8b22347ecc1 100644
--- a/src/plugins/instantiate/basic_blocks.mli
+++ b/src/plugins/instantiate/basic_blocks.mli
@@ -42,11 +42,6 @@ val ttype_of_pointed: logic_type -> logic_type
(** {2 C} *)
-(** For an expression, return the type of the pointed data.
- If the expression is not a pointer, returns None.
-*)
-val exp_type_of_pointed: exp -> typ option
-
(** For a type [T], returns [T*] *)
val ptr_of: typ -> typ
diff --git a/src/plugins/instantiate/string/mem_utils.ml b/src/plugins/instantiate/string/mem_utils.ml
index 71247c78162..9d88bb79b94 100644
--- a/src/plugins/instantiate/string/mem_utils.ml
+++ b/src/plugins/instantiate/string/mem_utils.ml
@@ -24,12 +24,30 @@ open Basic_blocks
open Cil_types
open Logic_const
-type kind = CPtr | Ptr | Len | Int
+type kind = CPtr | Ptr | Data of typ
type action = Strip | Id
type param = string * kind * action
type proto = kind * param list
type 'a spec_gen = location -> typ -> term -> term -> term -> 'a
+type pointed_expr_type =
+ | Of_null of typ
+ | Value_of of typ
+ | No_pointed
+
+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)) ->
+ Of_null (Cil.typeOf_pointed (Cil.typeOf x))
+ | _ ->
+ No_pointed
+ else
+ let xt = Cil.unrollTypeDeep (Cil.typeOf no_cast) in
+ let xt = Cil.type_remove_qualifier_attributes_deep xt in
+ Value_of (Cil.typeOf_pointed xt)
+
let unexpected = Options.fatal "Mem_utils: %s"
let mem2s_typing _ = function
@@ -88,7 +106,7 @@ let memcpy_memmove_common_ensures name loc t dest src len =
module type Function = sig
val name: string
- val prototype: proto
+ val prototype: unit -> proto
val well_typed: typ option -> typ list -> bool
end
@@ -98,10 +116,9 @@ struct
let to_type = function
| CPtr -> ptr_of (const_of t)
| Ptr -> ptr_of t
- | Len -> size_t()
- | Int -> Cil.intType
+ | Data t -> t
in
- let ret, ps = F.prototype in
+ let ret, ps = F.prototype () in
let ret = to_type ret in
let ps = List.map (fun (name, kind, _) -> name, (to_type kind), []) ps in
TFun(ret, Some ps, false, [])
@@ -112,21 +129,25 @@ struct
name, ftype
let well_typed_call lval args =
- let _, ps = F.prototype in
+ let _, ps = F.prototype () in
if List.length args <> List.length ps then false
else
let extract e = function
| _, (CPtr | Ptr), _ -> exp_type_of_pointed e
- | _, (Len | Int), _ -> Some (Cil.typeOf e)
+ | _, Data _ , _ -> Value_of (Cil.typeOf e)
in
let lvt = Extlib.opt_map Cil.typeOfLval lval in
let pts = List.map2 extract args ps in
- let is_none = function None -> true | _ -> false in
- if List.exists is_none pts then false
- else F.well_typed lvt (List.map (fun x -> Extlib.the x) pts)
+ let is_no_pointed = function No_pointed -> true | _ -> false in
+ let the_typ = function
+ | No_pointed -> assert false
+ | Value_of t | Of_null t -> t
+ in
+ if List.exists is_no_pointed pts then false
+ else F.well_typed lvt (List.map the_typ pts)
let retype_args _ args =
- let _, ps = F.prototype in
+ let _, ps = F.prototype () in
if List.length args <> List.length ps then
unexpected "trying to retype arguments on an ill-typed call"
else
@@ -137,12 +158,12 @@ struct
List.map2 retype args ps
let key_from_call _ret args =
- let _, ps = F.prototype in
+ let _, ps = F.prototype () in
match ps, args with
| (_, (Ptr|CPtr), _)::ps, fst::args when List.(length ps = length args) ->
begin match exp_type_of_pointed fst with
- | Some t -> t
- | None ->
+ | Value_of t -> t
+ | _ ->
unexpected "Mem_utils: trying to get key on an ill-typed call"
end
| _ ->
diff --git a/src/plugins/instantiate/string/mem_utils.mli b/src/plugins/instantiate/string/mem_utils.mli
index 543e5b06bc1..d4b205be01e 100644
--- a/src/plugins/instantiate/string/mem_utils.mli
+++ b/src/plugins/instantiate/string/mem_utils.mli
@@ -22,14 +22,22 @@
open Cil_types
-type kind = CPtr | Ptr | Len | Int
+type kind = CPtr | Ptr | Data of typ
type action = Strip | Id
type param = string * kind * action
type proto = kind * param list
module type Function = sig
val name: string
- val prototype: proto
+
+ val prototype: unit -> proto
+
+ (** receives the type of the lvalue and the types of the arguments recieved
+ for a call to the function and returns [true] iff they are correct.
+ The received types depend on the [prototype] of the module.
+ - if the kind is [Data t] -> it is the exact type of the expr/lvalue
+ - it the kind is [(C)Ptr] -> it is the pointed type of the expr/lvalue
+ *)
val well_typed: typ option -> typ list -> bool
end
@@ -58,3 +66,10 @@ val memcpy_memmove_common_assigns: assigns spec_gen
val memcpy_memmove_common_ensures:
string -> (termination_kind * identified_predicate) list spec_gen
+
+type pointed_expr_type =
+ | Of_null of typ
+ | Value_of of typ
+ | No_pointed
+
+val exp_type_of_pointed: exp -> pointed_expr_type
\ No newline at end of file
diff --git a/src/plugins/instantiate/string/memcmp.ml b/src/plugins/instantiate/string/memcmp.ml
index c8518480ed8..59969c7ddee 100644
--- a/src/plugins/instantiate/string/memcmp.ml
+++ b/src/plugins/instantiate/string/memcmp.ml
@@ -66,7 +66,13 @@ module Function =
struct
open Mem_utils
let name = function_name
- let prototype = Int, [ ("s1",CPtr,Strip);("s2",CPtr,Strip);("len",Len,Id)]
+ let prototype () =
+ Data Cil.intType,
+ [
+ ("s1" , CPtr,Strip) ;
+ ("s2" , CPtr,Strip) ;
+ ("len", Data (size_t ()) ,Id)
+ ]
let well_typed = Mem_utils.mem2s_typing
end
module Memcmp_base = Mem_utils.Make(Function)
diff --git a/src/plugins/instantiate/string/memcpy.ml b/src/plugins/instantiate/string/memcpy.ml
index b13a13067cb..e56778e6a57 100644
--- a/src/plugins/instantiate/string/memcpy.ml
+++ b/src/plugins/instantiate/string/memcpy.ml
@@ -45,7 +45,13 @@ let generate_spec = mem2s_spec ~requires ~assigns ~ensures
module Function =
struct
let name = function_name
- let prototype = Ptr, [("dest",Ptr,Strip);("src",CPtr,Strip);("len",Len,Id)]
+ let prototype () =
+ Ptr,
+ [
+ ("dest", Ptr, Strip) ;
+ ("src", CPtr, Strip) ;
+ ("len", Data (size_t()), Id)
+ ]
let well_typed = Mem_utils.mem2s_typing
end
module Memcpy_base = Mem_utils.Make(Function)
diff --git a/src/plugins/instantiate/string/memmove.ml b/src/plugins/instantiate/string/memmove.ml
index 0295236f2cd..9ce6d75b6bd 100644
--- a/src/plugins/instantiate/string/memmove.ml
+++ b/src/plugins/instantiate/string/memmove.ml
@@ -33,7 +33,13 @@ let generate_spec = mem2s_spec ~requires ~assigns ~ensures
module Function =
struct
let name = function_name
- let prototype = Ptr, [("dest",Ptr,Strip);("src",CPtr,Strip);("len",Len,Id)]
+ let prototype () =
+ Ptr,
+ [
+ ("dest", Ptr, Strip);
+ ("src" , CPtr, Strip);
+ ("len", Data (Basic_blocks.size_t()), Id)
+ ]
let well_typed = Mem_utils.mem2s_typing
end
module Memmove_base = Mem_utils.Make(Function)
diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index a8fc72f07a5..f681aa0ef13 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -194,12 +194,12 @@ let rec contains_union_type t =
let well_typed_call _ret = function
| [ 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
+ 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
+ | Value_of t , _ when contains_union_type t -> false
+ | Value_of t , _ when Cil.isVoidType t -> false
+ | Value_of t , _ when not (Cil.isCompleteType t) -> false
| _, None -> false
| _, Some _ -> true
end
@@ -207,9 +207,9 @@ let well_typed_call _ret = function
let key_from_call _ret = function
| [ 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
+ 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
| _ , _ -> unexpected "trying to generate a key on an ill-typed call"
end
| _ -> unexpected "trying to generate a key on an ill-typed call"
@@ -247,9 +247,9 @@ let retype_args (_t, e) args =
match e, args with
| None, [ ptr ; v ; n ] ->
let ptr = Cil.stripCasts 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"
+ let base_type = match Mem_utils.exp_type_of_pointed ptr with
+ | Value_of t -> base_char_type t
+ | _ -> unexpected "trying to retype arguments on an ill-typed call"
in
let v = Cil.mkCast (Cil.stripCasts v) base_type in
[ ptr ; v ; n ]
--
GitLab