[Instantiate] Refacto in string modules

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 \

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"

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
 

src/plugins/instantiate/string/mem_utils.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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

src/plugins/instantiate/string/mem_utils.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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

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)

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)

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)

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;

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;

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;