From ac00a6ecddf22bac391ac28f87d309c7d9cdfbad Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 26 Mar 2020 15:30:46 +0100
Subject: [PATCH] [Instantiate] Refacto in string modules
---
src/plugins/instantiate/Makefile.in | 1 +
src/plugins/instantiate/basic_blocks.ml | 11 ++
src/plugins/instantiate/basic_blocks.mli | 5 +
src/plugins/instantiate/string/mem_utils.ml | 150 ++++++++++++++++++
src/plugins/instantiate/string/mem_utils.mli | 60 +++++++
src/plugins/instantiate/string/memcmp.ml | 83 ++--------
src/plugins/instantiate/string/memcpy.ml | 118 +++-----------
src/plugins/instantiate/string/memmove.ml | 116 ++------------
.../oracle/ignore-functions.res.oracle | 10 +-
.../options/oracle/only-functions.res.oracle | 10 +-
.../tests/string/oracle/memcpy.res.oracle | 80 +++++-----
11 files changed, 332 insertions(+), 312 deletions(-)
create mode 100644 src/plugins/instantiate/string/mem_utils.ml
create mode 100644 src/plugins/instantiate/string/mem_utils.mli
diff --git a/src/plugins/instantiate/Makefile.in b/src/plugins/instantiate/Makefile.in
index 144f5c7128e..a8fc2764589 100644
--- a/src/plugins/instantiate/Makefile.in
+++ b/src/plugins/instantiate/Makefile.in
@@ -30,6 +30,7 @@ FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
endif
SRC_STRING:= \
+ mem_utils \
memcmp \
memcpy \
memmove \
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index 660db8c83c0..830911e482e 100644
--- a/src/plugins/instantiate/basic_blocks.ml
+++ b/src/plugins/instantiate/basic_blocks.ml
@@ -50,6 +50,17 @@ 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 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 8b22347ecc1..d8723d96765 100644
--- a/src/plugins/instantiate/basic_blocks.mli
+++ b/src/plugins/instantiate/basic_blocks.mli
@@ -42,6 +42,11 @@ 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
new file mode 100644
index 00000000000..71247c78162
--- /dev/null
+++ b/src/plugins/instantiate/string/mem_utils.ml
@@ -0,0 +1,150 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Basic_blocks
+open Cil_types
+open Logic_const
+
+type kind = CPtr | Ptr | Len | Int
+type action = Strip | Id
+type param = string * kind * action
+type proto = kind * param list
+type 'a spec_gen = location -> typ -> term -> term -> term -> 'a
+
+let unexpected = Options.fatal "Mem_utils: %s"
+
+let mem2s_typing _ = function
+ | [ dest ; src ; len ] ->
+ (Cil.isIntegralType len) &&
+ (Cil_datatype.Typ.equal dest src) &&
+ (not (Cil.isVoidType dest)) &&
+ (Cil.isCompleteType dest)
+ | _ -> false
+
+let mem2s_spec ~requires ~assigns ~ensures _t { svar = vi } loc =
+ let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
+ | [ dest ; src ; len ] -> dest, src, len
+ | _ -> unexpected "ill-formed fundec in specification generation"
+ in
+ let t = cdest.vtype in
+ let dest = cvar_to_tvar cdest in
+ let src = cvar_to_tvar csrc in
+ let len = cvar_to_tvar clen in
+ let requires = requires loc t dest src len in
+ let assigns = assigns loc t dest src len in
+ let ensures = ensures loc t dest src len in
+ make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
+
+let pcopied_len_bytes ?loc p1 p2 bytes_len =
+ plet_len_div_size ?loc p1.term_type bytes_len
+ (punfold_all_elems_eq ?loc p1 p2)
+
+let memcpy_memmove_common_requires loc _ dest src len =
+ List.map new_predicate [
+ { (pcorrect_len_bytes ~loc dest.term_type len)
+ with pred_name = ["aligned_end"] } ;
+ { (pvalid_len_bytes ~loc here_label dest len)
+ with pred_name = ["valid_dest"] } ;
+ { (pvalid_read_len_bytes ~loc here_label src len)
+ with pred_name = ["valid_read_src"] } ;
+ ]
+
+let memcpy_memmove_common_assigns loc t dest src len =
+ let dest_range = new_identified_term (tunref_range_bytes_len ~loc dest len) in
+ let src_range = new_identified_term(tunref_range_bytes_len ~loc src len) in
+ let copy = dest_range, From [src_range] in
+ let result = new_identified_term (tresult t) in
+ let dest = new_identified_term dest in
+ let res = result, From [dest] in
+ Writes [ copy ; res ]
+
+let presult_dest ?loc t dest =
+ prel ?loc (Req, (tresult ?loc t), dest)
+
+let memcpy_memmove_common_ensures name loc t dest src len =
+ List.map (fun p -> Normal, new_predicate p) [
+ { (pcopied_len_bytes ~loc dest src len) with pred_name = [name] } ;
+ { (presult_dest ~loc t dest) with pred_name = ["result"] }
+ ]
+
+module type Function = sig
+ val name: string
+ val prototype: proto
+ val well_typed: typ option -> typ list -> bool
+end
+
+module Make (F: Function) =
+struct
+ let generate_function_type t =
+ let to_type = function
+ | CPtr -> ptr_of (const_of t)
+ | Ptr -> ptr_of t
+ | Len -> size_t()
+ | Int -> Cil.intType
+ 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, [])
+
+ let generate_prototype t =
+ let ftype = generate_function_type t in
+ let name = F.name ^ "_" ^ (string_of_typ t) in
+ name, ftype
+
+ let well_typed_call lval args =
+ 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)
+ 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 retype_args _ args =
+ let _, ps = F.prototype in
+ if List.length args <> List.length ps then
+ unexpected "trying to retype arguments on an ill-typed call"
+ else
+ let retype x = function
+ | _, _, Strip -> Cil.stripCasts x
+ | _, _, Id -> x
+ in
+ List.map2 retype args ps
+
+ let key_from_call _ret args =
+ 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 ->
+ unexpected "Mem_utils: trying to get key on an ill-typed call"
+ end
+ | _ ->
+ 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
new file mode 100644
index 00000000000..543e5b06bc1
--- /dev/null
+++ b/src/plugins/instantiate/string/mem_utils.mli
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+type kind = CPtr | Ptr | Len | Int
+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 well_typed: typ option -> typ list -> bool
+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
+end
+
+(** location -> key -> s1 -> s2 -> len -> spec_result *)
+type 'a spec_gen = location -> typ -> term -> term -> term -> 'a
+
+val mem2s_spec:
+ requires: (identified_predicate list) spec_gen ->
+ assigns: assigns spec_gen ->
+ ensures: (termination_kind * identified_predicate) list spec_gen ->
+ typ -> fundec -> location -> funspec
+
+val mem2s_typing: typ option -> typ list -> bool
+
+val memcpy_memmove_common_requires: (identified_predicate list) spec_gen
+
+val memcpy_memmove_common_assigns: assigns spec_gen
+
+val memcpy_memmove_common_ensures:
+ string -> (termination_kind * identified_predicate) list spec_gen
diff --git a/src/plugins/instantiate/string/memcmp.ml b/src/plugins/instantiate/string/memcmp.ml
index 633294db95b..c8518480ed8 100644
--- a/src/plugins/instantiate/string/memcmp.ml
+++ b/src/plugins/instantiate/string/memcmp.ml
@@ -26,9 +26,7 @@ open Basic_blocks
let function_name = "memcmp"
-let unexpected = Options.fatal "String.Memcmp: unexpected: %s"
-
-let generate_requires loc s1 s2 len =
+let requires loc _ s1 s2 len =
List.map new_predicate [
{ (pcorrect_len_bytes ~loc s1.term_type len)
with pred_name = ["aligned_end"] } ;
@@ -43,7 +41,7 @@ let presult_memcmp ?loc p1 p2 len =
let res = prel ?loc (Req, (tresult ?loc Cil.intType), (tinteger ?loc 0)) in
piff ?loc (res, eq)
-let generate_assigns loc s1 s2 len =
+let assigns loc _ s1 s2 len =
let indirect_range loc s len =
new_identified_term
{ (tunref_range_bytes_len ~loc s len) with term_name = ["indirect"] }
@@ -57,78 +55,31 @@ let generate_assigns loc s1 s2 len =
let presult_memcmp_len_bytes ?loc p1 p2 bytes_len =
plet_len_div_size ?loc p1.term_type bytes_len (presult_memcmp ?loc p1 p2)
-let generate_ensures loc s1 s2 len =
+let ensures loc _ s1 s2 len =
List.map (fun p -> Normal, new_predicate p) [
{ (presult_memcmp_len_bytes ~loc s1 s2 len) with pred_name = [ "equals" ] }
]
-let generate_spec _t { svar = vi } loc =
- let (c_s1, c_s2, clen) = match Cil.getFormalsDecl vi with
- | [ s1 ; s2 ; len ] -> s1, s2, len
- | _ -> unexpected "ill-formed fundec in specification generation"
- in
- let s1 = cvar_to_tvar c_s1 in
- let s2 = cvar_to_tvar c_s2 in
- let len = cvar_to_tvar clen in
- let requires = generate_requires loc s1 s2 len in
- let assigns = generate_assigns loc s1 s2 len in
- let ensures = generate_ensures loc s1 s2 len in
- make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
-
-let generate_function_type t =
- let t = ptr_of (const_of t) in
- let params = [
- ("s1", t, []) ;
- ("s2", t, []) ;
- ("len", size_t (), [])
- ] in
- TFun(Cil.intType, Some params, false, [])
-
-let generate_prototype t =
- let fun_type = generate_function_type t in
- let name = function_name ^ "_" ^ (string_of_typ t) in
- name, fun_type
-
-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 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)) &&
- (not (Cil.isVoidType (type_from_arg s1))) &&
- (Cil.isCompleteType (type_from_arg s1))
- | _ -> false
-
-let key_from_call _ret = function
- | [ s1 ; _ ; _ ] -> type_from_arg s1
- | _ -> unexpected "trying to generate a key on an ill-typed call"
-
-let retype_args override_key = function
- | [ s1 ; s2 ; len ] ->
- let s1 = Cil.stripCasts s1 in
- let s2 = Cil.stripCasts s2 in
- assert (
- Cil_datatype.Typ.equal (type_from_arg s1) override_key &&
- Cil_datatype.Typ.equal (type_from_arg s2) override_key
- ) ;
- [ s1 ; s2 ; len ]
- | _ -> unexpected "trying to retype arguments on an ill-typed call"
+let generate_spec = Mem_utils.mem2s_spec ~requires ~assigns ~ensures
-let args_for_original _t args = args
+module Function =
+struct
+ open Mem_utils
+ let name = function_name
+ let prototype = Int, [ ("s1",CPtr,Strip);("s2",CPtr,Strip);("len",Len,Id)]
+ let well_typed = Mem_utils.mem2s_typing
+end
+module Memcmp_base = Mem_utils.Make(Function)
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = typ
let function_name = function_name
- let well_typed_call = well_typed_call
- let key_from_call = key_from_call
- let retype_args = retype_args
- let generate_prototype = generate_prototype
+ let well_typed_call = Memcmp_base.well_typed_call
+ let key_from_call = Memcmp_base.key_from_call
+ let retype_args = Memcmp_base.retype_args
+ let generate_prototype = Memcmp_base.generate_prototype
let generate_spec = generate_spec
- let args_for_original = args_for_original
+ let args_for_original _ = Extlib.id
end)
diff --git a/src/plugins/instantiate/string/memcpy.ml b/src/plugins/instantiate/string/memcpy.ml
index d0db608eef1..b13a13067cb 100644
--- a/src/plugins/instantiate/string/memcpy.ml
+++ b/src/plugins/instantiate/string/memcpy.ml
@@ -23,118 +23,42 @@
open Cil_types
open Logic_const
open Basic_blocks
+open Mem_utils
let function_name = "memcpy"
-let unexpected = Options.fatal "String.Memcpy: unexpected: %s"
-
let pseparated_memcpy_len_bytes ?loc p1 p2 bytes_len =
let generate len = pseparated_memories ?loc p1 len p2 len in
plet_len_div_size ?loc p1.term_type bytes_len generate
-let pcopied_len_bytes ?loc p1 p2 bytes_len =
- plet_len_div_size ?loc p1.term_type bytes_len
- (punfold_all_elems_eq ?loc p1 p2)
-
-let presult_dest ?loc t dest =
- prel ?loc (Req, (tresult ?loc t), dest)
-
-let generate_requires loc dest src len =
- List.map new_predicate [
- { (pcorrect_len_bytes ~loc dest.term_type len)
- with pred_name = ["aligned_end"] } ;
- { (pvalid_len_bytes ~loc here_label dest len)
- with pred_name = ["valid_dest"] } ;
- { (pvalid_read_len_bytes ~loc here_label src len)
- with pred_name = ["valid_read_src"] } ;
- { (pseparated_memcpy_len_bytes ~loc dest src len)
- with pred_name = ["separation"] }
- ]
-
-let generate_assigns loc t dest src len =
- let dest_range = new_identified_term (tunref_range_bytes_len ~loc dest len) in
- let src_range = new_identified_term(tunref_range_bytes_len ~loc src len) in
- let copy = dest_range, From [src_range] in
- let result = new_identified_term (tresult t) in
- let dest = new_identified_term dest in
- let res = result, From [dest] in
- Writes [ copy ; res ]
-
-let generate_ensures loc t dest src len =
- List.map (fun p -> Normal, new_predicate p) [
- { (pcopied_len_bytes ~loc dest src len) with pred_name = [ "copied"] } ;
- { (presult_dest ~loc t dest) with pred_name = [ "result"] }
- ]
-
-let generate_spec _t { svar = vi } loc =
- let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
- | [ dest ; src ; len ] -> dest, src, len
- | _ -> unexpected "ill-formed fundec in specification generation"
+let requires loc t dest src len =
+ let separated = new_predicate
+ { (pseparated_memcpy_len_bytes ~loc dest src len)
+ with pred_name = ["separation"] }
in
- let t = cdest.vtype in
- let dest = cvar_to_tvar cdest in
- let src = cvar_to_tvar csrc in
- let len = cvar_to_tvar clen in
- let requires = generate_requires loc dest src len in
- let assigns = generate_assigns loc t dest src len in
- let ensures = generate_ensures loc t dest src len in
- make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
-
-let generate_function_type t =
- let dt = ptr_of t in
- let st = ptr_of (const_of t) in
- let params = [
- ("dest", dt, []) ;
- ("src", st, []) ;
- ("len", size_t (), [])
- ] in
- TFun(dt, Some params, false, [])
-
-let generate_prototype t =
- let fun_type = generate_function_type t in
- let name = function_name ^ "_" ^ (string_of_typ t) in
- name, fun_type
-
-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 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)) &&
- (not (Cil.isVoidType (type_from_arg dest))) &&
- (Cil.isCompleteType (type_from_arg dest))
- | _ -> false
-
-let key_from_call _ret = function
- | [ dest ; _ ; _ ] -> type_from_arg dest
- | _ -> unexpected "trying to generate a key on an ill-typed call"
+ separated :: (memcpy_memmove_common_requires loc t dest src len)
-let retype_args override_key = function
- | [ dest ; src ; len ] ->
- let dest = Cil.stripCasts dest in
- let src = Cil.stripCasts src in
- assert (
- Cil_datatype.Typ.equal (type_from_arg dest) override_key &&
- Cil_datatype.Typ.equal (type_from_arg src) override_key
- ) ;
- [ dest ; src ; len ]
- | _ -> unexpected "trying to retype arguments on an ill-typed call"
+let assigns = memcpy_memmove_common_assigns
+let ensures = memcpy_memmove_common_ensures "copied"
+let generate_spec = mem2s_spec ~requires ~assigns ~ensures
-let args_for_original _t args = args
+module Function =
+struct
+ let name = function_name
+ let prototype = Ptr, [("dest",Ptr,Strip);("src",CPtr,Strip);("len",Len,Id)]
+ let well_typed = Mem_utils.mem2s_typing
+end
+module Memcpy_base = Mem_utils.Make(Function)
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = typ
let function_name = function_name
- let well_typed_call = well_typed_call
- let key_from_call = key_from_call
- let retype_args = retype_args
- let generate_prototype = generate_prototype
+ let well_typed_call = Memcpy_base.well_typed_call
+ let key_from_call = Memcpy_base.key_from_call
+ let retype_args = Memcpy_base.retype_args
+ let generate_prototype = Memcpy_base.generate_prototype
let generate_spec = generate_spec
- let args_for_original = args_for_original
+ let args_for_original _ = Extlib.id
end)
diff --git a/src/plugins/instantiate/string/memmove.ml b/src/plugins/instantiate/string/memmove.ml
index 6481c423a1f..0295236f2cd 100644
--- a/src/plugins/instantiate/string/memmove.ml
+++ b/src/plugins/instantiate/string/memmove.ml
@@ -21,114 +21,32 @@
(**************************************************************************)
open Cil_types
-open Logic_const
-open Basic_blocks
+open Mem_utils
let function_name = "memmove"
-let unexpected = Options.fatal "String.Memmove: unexpected: %s"
+let requires = memcpy_memmove_common_requires
+let assigns = memcpy_memmove_common_assigns
+let ensures = memcpy_memmove_common_ensures "moved"
+let generate_spec = mem2s_spec ~requires ~assigns ~ensures
-let pmoved_len_bytes ?loc dest src bytes_len =
- plet_len_div_size ?loc dest.term_type bytes_len
- (punfold_all_elems_eq ?loc dest src)
-
-let presult_dest ?loc t dest =
- prel ?loc (Req, (tresult ?loc t), dest)
-
-let generate_requires loc dest src len =
- List.map new_predicate [
- { (pcorrect_len_bytes ~loc dest.term_type len)
- with pred_name = ["aligned_end"] } ;
- { (pvalid_len_bytes ~loc here_label dest len)
- with pred_name = ["valid_dest"] } ;
- { (pvalid_read_len_bytes ~loc here_label src len)
- with pred_name = ["valid_read_src"] } ;
- ]
-
-let generate_assigns loc t dest src len =
- let dest_range = new_identified_term (tunref_range_bytes_len ~loc dest len) in
- let src_range = new_identified_term(tunref_range_bytes_len ~loc src len) in
- let copy = dest_range, From [src_range] in
- let result = new_identified_term (tresult t) in
- let dest = new_identified_term dest in
- let res = result, From [dest] in
- Writes [ copy ; res ]
-
-let generate_ensures loc t dest src len =
- List.map (fun p -> Normal, new_predicate p) [
- { (pmoved_len_bytes ~loc dest src len) with pred_name = [ "moved"] } ;
- { (presult_dest ~loc t dest) with pred_name = [ "result"] }
- ]
-
-let generate_spec _t { svar = vi } loc =
- let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
- | [ dest ; src ; len ] -> dest, src, len
- | _ -> unexpected "ill-formed fundec in specification generation"
- in
- let t = cdest.vtype in
- let dest = cvar_to_tvar cdest in
- let src = cvar_to_tvar csrc in
- let len = cvar_to_tvar clen in
- let requires = generate_requires loc dest src len in
- let assigns = generate_assigns loc t dest src len in
- let ensures = generate_ensures loc t dest src len in
- make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
-
-let generate_function_type t =
- let dt = ptr_of t in
- let st = ptr_of (const_of t) in
- let params = [
- ("dest", dt, []) ;
- ("src", st, []) ;
- ("len", size_t (), [])
- ] in
- TFun(dt, Some params, false, [])
-
-let generate_prototype t =
- let fun_type = generate_function_type t in
- let name = function_name ^ "_" ^ (string_of_typ t) in
- name, fun_type
-
-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 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)) &&
- (not (Cil.isVoidType (type_from_arg dest))) &&
- (Cil.isCompleteType (type_from_arg dest))
- | _ -> false
-
-let key_from_call _ret = function
- | [ dest ; _ ; _ ] -> type_from_arg dest
- | _ -> unexpected "trying to generate a key on an ill-typed call"
-
-let retype_args override_key = function
- | [ dest ; src ; len ] ->
- let dest = Cil.stripCasts dest in
- let src = Cil.stripCasts src in
- assert (
- Cil_datatype.Typ.equal (type_from_arg dest) override_key &&
- Cil_datatype.Typ.equal (type_from_arg src) override_key
- ) ;
- [ dest ; src ; len ]
- | _ -> unexpected "trying to retype arguments on an ill-typed call"
-
-let args_for_original _t args = args
+module Function =
+struct
+ let name = function_name
+ let prototype = Ptr, [("dest",Ptr,Strip);("src",CPtr,Strip);("len",Len,Id)]
+ let well_typed = Mem_utils.mem2s_typing
+end
+module Memmove_base = Mem_utils.Make(Function)
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = typ
let function_name = function_name
- let well_typed_call = well_typed_call
- let key_from_call = key_from_call
- let retype_args = retype_args
- let generate_prototype = generate_prototype
+ let well_typed_call = Memmove_base.well_typed_call
+ let key_from_call = Memmove_base.key_from_call
+ let retype_args = Memmove_base.retype_args
+ let generate_prototype = Memmove_base.generate_prototype
let generate_spec = generate_spec
- let args_for_original = args_for_original
+ let args_for_original _ = Extlib.id
end)
diff --git a/src/plugins/instantiate/tests/options/oracle/ignore-functions.res.oracle b/src/plugins/instantiate/tests/options/oracle/ignore-functions.res.oracle
index 8aacf1fa757..b260fc61afd 100644
--- a/src/plugins/instantiate/tests/options/oracle/ignore-functions.res.oracle
+++ b/src/plugins/instantiate/tests/options/oracle/ignore-functions.res.oracle
@@ -11,16 +11,16 @@ void foo(void)
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 4;
diff --git a/src/plugins/instantiate/tests/options/oracle/only-functions.res.oracle b/src/plugins/instantiate/tests/options/oracle/only-functions.res.oracle
index cc08c601aac..d84cec92ebc 100644
--- a/src/plugins/instantiate/tests/options/oracle/only-functions.res.oracle
+++ b/src/plugins/instantiate/tests/options/oracle/only-functions.res.oracle
@@ -3,16 +3,16 @@
#include "stddef.h"
#include "string.h"
#include "strings.h"
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 4;
diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
index 05681aeb44e..78076d88eb1 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
@@ -13,16 +13,16 @@ struct X {
};
typedef int named;
struct incomplete;
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 4;
@@ -53,16 +53,16 @@ void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: len % 8 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 8;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 8 ≡ 0;
requires
valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 8;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 8;
@@ -86,16 +86,16 @@ void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 4;
@@ -119,17 +119,17 @@ void pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
return;
}
-/*@ requires aligned_end: len % 40 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 40;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
\let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 40;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = len / 40;
@@ -185,16 +185,16 @@ struct X {
};
typedef int named;
struct incomplete;
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 4;
@@ -228,16 +228,16 @@ void with_named(named *src, named *dest)
return;
}
-/*@ requires aligned_end: len % 8 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 8;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 8 ≡ 0;
requires
valid_dest: \let __fc_len = len / 8; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 8; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 8;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 8;
@@ -264,16 +264,16 @@ void structure(struct X *src, struct X *dest)
return;
}
-/*@ requires aligned_end: len % 4 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 4;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 4; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 4;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 4;
@@ -299,17 +299,17 @@ void pointers(int **src, int **dest)
return;
}
-/*@ requires aligned_end: len % 40 ≡ 0;
+/*@ requires
+ separation:
+ \let __fc_len = len / 40;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
\let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
requires
valid_read_src:
\let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 40;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
\let __fc_len = \old(len) / 40;
--
GitLab