Merge branch 'feature/blanchard/specialize-string-functions' into 'master'

Specialize string functions on usage

See merge request frama-c/frama-c!2381

headers/header_spec.txt

@@ -930,6 +930,34 @@ src/plugins/occurrence/options.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/occurrence/register.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/occurrence/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/occurrence/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/basic_blocks.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/basic_blocks.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/Builtin.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/builtin_builder.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/builtin_builder.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/configure.ac: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/Makefile.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/basic_alloc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/basic_alloc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/calloc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/calloc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/free.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/free.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/malloc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/stdlib/malloc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/string/memcmp.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/string/memcmp.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/string/memcpy.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/string/memcpy.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/string/memmove.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/string/memmove.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/string/memset.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/string/memset.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/options.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/options.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/transform.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/transform.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/pdg/Pdg.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/pdg/annot.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/pdg/annot.mli: CEA_LGPL_OR_PROPRIETARY

src/plugins/builtin/.gitignore

+/configure
+/Makefile
+/tests/ptests_config
+/tests/*/result

src/plugins/builtin/Builtin.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2019                                               *)
+(*    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
+
+module Builtin_builder: sig
+  (** Builds a [Builtin] module (used by [Transform]) from a [Generator_sig] *)
+
+  (** Signature for a new builtin generator.
+
+      In order to support a new function, this module must be implemented and
+      registered to the [Transform] module.
+  *)
+  module type Generator_sig = sig
+    (** [Hashtbl] module used by the [Make_builtin] module to generate the
+        function cache. The [key] ([override_key]) must identify a function
+        override.
+    *)
+    module Hashtbl: Datatype.Hashtbl
+    type override_key = Hashtbl.key
+
+    (** Name of the implemented builtin function *)
+    val function_name: string
+
+    (** [well_typed_call ret args] must return true if and only if the
+        corresponding call is well typed in the sens that the generator can
+        produce a function override for the corresponding return value and
+        parameters, according to their types and/or values.
+    *)
+    val well_typed_call: lval option -> exp list -> bool
+
+    (** [key_from_call ret args] must return an identifier for the corresponding
+        call. [key_from_call ret1 args1] and [key_from_call ret2 args2] must equal
+        if and only if the same override function can be used for both call. Any
+        call for which [well_typed_call] returns true must be able to give a key.
+    *)
+    val key_from_call: lval option -> exp list -> override_key
+
+    (** [retype_args key args] must returns a new argument list compatible with
+        the function identified by [override_key]. [args] is the list of arguments
+        that were given to the call for with [Transform] is currently replacing.
+        Most of the time, it will consists in removing/changing some casts. But
+        note that arguments can be removed (for example if the override is built
+        because some constant have specialized).
+    *)
+    val retype_args: override_key -> exp list -> exp list
+
+    (** [args_for_original key args] must transform the list of parameters of the
+        override function such that the new list can be given to the original
+        function. For example, if for a call:
+        [foo(x, 0, z)]
+        The [Builtin] module generates an override:
+        [void foo_spec(int p1, int p3);]
+        The received list of expression is [ p1 ; p3 ] and thus the returned list
+        should be [ p1 ; 0 ; p3 ] (so that the replaced call [foo_spec(x, z)] has
+        the same behavior).
+        Note that there is no need to introduce casts to the original type, it is
+        introduced by [Make_builtin].
+    *)
+    val args_for_original: override_key -> exp list -> exp list
+
+    (** [generate_prototype key] must generate the name and the type corresponding
+        to [key].
+    *)
+    val generate_prototype: override_key -> (string * typ)
+
+    (** [generate_spec key fundec loc] must generate the specification of the
+        [fundec] generated from [key]. The location is the one generated by the
+        [Transform] visitor. Note that it must return a [funspec] but should
+        {b not} register it in [Annotations] tables.
+    *)
+    val generate_spec: override_key -> fundec -> location -> funspec
+  end
+end
+
+module Transform: sig
+  (** Registers a new [Builtin] to the visitor from the [Generator_sig] module
+      of this builtin. Each new builtin function generator should call this
+      globally.
+  *)
+  val register: (module Builtin_builder.Generator_sig) -> unit
+end

src/plugins/builtin/Makefile.in

+##########################################################################
+#                                                                        #
+#  This file is part of Frama-C.                                         #
+#                                                                        #
+#  Copyright (C) 2007-2019                                               #
+#    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).            #
+#                                                                        #
+##########################################################################
+
+# Do not use ?= to initialize both below variables
+# (fixed efficiency issue, see GNU Make manual, Section 8.11)
+ifndef FRAMAC_SHARE
+FRAMAC_SHARE  :=$(shell frama-c-config -print-share-path)
+endif
+ifndef FRAMAC_LIBDIR
+FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
+endif
+
+SRC_STRING:= \
+	memcmp \
+	memcpy \
+	memmove \
+	memset
+SRC_STRING:=$(addprefix string/, $(SRC_STRING))
+
+SRC_STDLIB:= \
+	basic_alloc \
+	calloc \
+	free \
+	malloc
+SRC_STDLIB:=$(addprefix stdlib/, $(SRC_STDLIB))
+
+###################
+# Plug-in Setting #
+###################
+
+PLUGIN_DIR ?= .
+PLUGIN_ENABLE := @ENABLE_BUILTIN@
+PLUGIN_NAME := Builtin
+PLUGIN_EXTRA_DIRS:=\
+	string\
+	stdlib
+PLUGIN_CMI :=
+PLUGIN_CMO := \
+	basic_blocks options builtin_builder transform register \
+	$(SRC_STRING) \
+	$(SRC_STDLIB)
+
+PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE)
+PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
+#PLUGIN_NO_DEFAULT_TEST := no
+PLUGIN_TESTS_DIRS := string stdlib options api
+
+################
+# Generic part #
+################
+
+include $(FRAMAC_SHARE)/Makefile.dynamic
+
+#####################################
+# Regenerating the Makefile on need #
+#####################################
+
+ifeq ("$(FRAMAC_INTERNAL)","yes")
+CONFIG_STATUS_DIR=$(FRAMAC_SRC)
+else
+CONFIG_STATUS_DIR=.
+endif
+
+$(Builtin_DIR)/Makefile: $(Builtin_DIR)/Makefile.in \
+				$(CONFIG_STATUS_DIR)/config.status
+	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/builtin/README.md

+# Builtin plugin
+
+## Description
+
+The builtin plugin is meant to build function specialization to C functions in
+a project when the original specification (or prototype of the function) cannot
+be efficiently used by some plugins.
+
+For example, the specification of a function like `memcpy` cannot be efficiently
+used by a plugin like `WP` because it involves `void*` pointers and requires to
+deduce that bytes equality implies (typed) data equality. While for example it
+is easy to produce a typed specification for a type `int`:
+
+```c
+/*@ requires valid_dest: \valid(dest + (0 .. len-1));
+    requires valid_read_src: \valid_read(src + (0 .. len-1));
+    requires separation: \separated(dest + (0 .. len-1), src + (0 .. len-1));
+    ensures copied: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(dest + j0) ≡ *(src + j0);
+    ensures result: \result ≡ dest;
+    assigns *(dest + (0 .. len - 1)), \result;
+    assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
+    assigns \result \from dest;
+ */
+int *memcpy_int(int *dest, int const *src, size_t len);
+```
+
+That can be easily used by WP.
+
+The role of the Builtin plugin is to find each call for which a builtin
+generator is available and if the call is well-typed according to the generator
+(for example for `memcpy` if `dest` and `src` are both pointers to integers), to
+replace this call with a call to an automatically generated specialization
+corresponding to the call.
+
+## Options
+
+- `-builtin` activate builtin replacement
+- `-builtin-fct=f,...` only replace calls in specified functions (default to all)
+- `-builtin-(no-)<function_name>` activate or deactivate a particular builtin
+  function, defaults to true.
+
+## Available builtin functions
+
+### `string.h`
+
+```c
+int memcmp(void const* s1, void const* s2, size_t len);
+```
+
+The parameters `s1` and `s2` must have the same types, except that qualifiers
+and typedefs are ignored. The type of `s1` or `s2` cannot be `void*`.
+
+```c
+void* memcpy(void * dest, void const* src, size_t len);
+```
+
+The parameters `dest` and `src` must have the same types, except that qualifiers
+and typedefs are ignored. The type of `dest` or `src` cannot be `void*`.
+
+```c
+void* memmove(void * dest, void const* src, size_t len);
+```
+
+The parameters `dest` and `src` must have the same types, except that qualifiers
+and typedefs are ignored. The type of `dest` or `src` cannot be `void*`.
+
+```c
+void* memset(void * ptr, int value, size_t len);
+```
+
+If `ptr` is of `char*` type (include signed and unsigned variants), `value` must
+be a `char`.
+
+If `ptr` is of any other pointer type (except `void*`), `value` must be a
+constant that statically evaluates to `0x00` or `0xFF`.
+
+### `stdlib.h`
+
+```c
+void* calloc(size_t num, size_t size);
+
+{
+  type* res = calloc(...) ;
+}
+```
+
+`calloc` is typed according to the variable that receives its result. It must be
+a pointer type different from `void*`. If the pointed type has a flexible array
+member, `num` is assumed to evaluate to `1` (a precondition is created for this).
+
+```c
+void free(void* ptr);
+```
+
+The type of `ptr` must be different from `void*`.
+
+
+```c
+void* malloc(size_t num, size_t size);
+
+{
+  type* res = calloc(...) ;
+}
+```
+
+`malloc` is typed according to the variable that receives its result. It must be
+a pointer type different from `void*`.
+
+## Adding a new builtin
+
+To add a new builtin, one has to register a new module implementing the
+`Builtin_builder.Generator_sig` module type to the `Transform` module. The
+lasts steps of the code should look like:
+
+```ocaml
+let () = Transform.register (module struct
+    module Hashtbl = ...
+    type override_key = ...
+
+    let function_name = "my_builtin_function"
+    let well_typed_call = ...
+    let key_from_call = ...
+    let retype_args = ...
+    let generate_prototype = ...
+    let generate_spec = ...
+    let args_for_original = ...
+  end)
+```
+
+The role and types of each function is documented in `Builtin_builder.mli`.
\ No newline at end of file

src/plugins/builtin/basic_blocks.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2019                                               *)
+(*    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
+open Cil_types
+open Cil_const
+open Logic_const
+
+let ptr_of t = TPtr(t, [])
+let const_of t = Cil.typeAddAttributes [Attr("const", [])] t
+
+let size_t () =
+  Globals.Types.find_type Logic_typing.Typedef "size_t"
+
+let prepare_definition name fun_type =
+  let vi = Cil.makeGlobalVar ~referenced:true name fun_type in
+  vi.vdefined <- true ;
+  let fd = Cil.emptyFunctionFromVI vi in
+  Cil.setFormalsDecl vi fun_type ;
+  fd.sformals <- Cil.getFormalsDecl vi ;
+  fd
+
+let call_function lval vi args =
+  let loc  = Cil_datatype.Location.unknown in
+  let _, typs, _, _ = Cil.splitFunctionTypeVI vi in
+  let typs = Cil.argsToList typs in
+  let gen_arg exp (_, typ, _) =
+    if Cil_datatype.Typ.equal vi.vtype typ then exp
+    else Cil.mkCast exp typ
+  in
+  let args = List.map2 gen_arg args typs in
+  Call(lval, (Cil.evar vi), args, loc)
+
+let rec string_of_typ_aux = function
+  | TVoid(_) -> "void"
+  | TInt(IBool, _) -> "bool"
+  | TInt(IChar, _) -> "char"
+  | TInt(ISChar, _) -> "schar"
+  | TInt(IUChar, _) -> "uchar"
+  | TInt(IInt, _) -> "int"
+  | TInt(IUInt, _) -> "uint"
+  | TInt(IShort, _) -> "short"
+  | TInt(IUShort, _) -> "ushort"
+  | TInt(ILong, _) -> "long"
+  | TInt(IULong, _) -> "ulong"
+  | TInt(ILongLong, _) -> "llong"
+  | TInt(IULongLong, _) -> "ullong"
+  | TFloat(FFloat, _) -> "float"
+  | TFloat(FDouble, _) -> "double"
+  | TFloat(FLongDouble, _) -> "ldouble"
+  | TPtr(t, _) -> "ptr_" ^ string_of_typ t
+  | TEnum (ei, _) -> "e_" ^ ei.ename
+  | TComp (ci, _, _) when ci.cstruct -> "st_" ^ ci.cname
+  | TComp (ci, _, _) -> "un_" ^ ci.cname
+  | TArray (t, Some e, _, _) ->
+    "arr" ^ (string_of_exp e) ^ "_" ^ string_of_typ t
+  | _ -> assert false
+and string_of_typ t = string_of_typ_aux (Cil.unrollType t)
+and string_of_exp e = Format.asprintf "%a" Cil_printer.pp_exp e
+
+let size_var ?(name_ext="") t value = {
+  l_var_info = make_logic_var_local ("__fc_" ^ name_ext ^ "len") t;
+  l_type = Some t;
+  l_tparams = [];
+  l_labels = [];
+  l_profile = [];
+  l_body = LBterm value;
+}
+
+(** Features related to terms *)
+
+let cvar_to_tvar vi = tvar (cvar_to_lvar vi)
+
+let tminus ?loc t1 t2 =
+  let minus, typ = match t1.term_type, t2.term_type with
+    | Ctype(t1), Ctype(t2) when Cil.isPointerType t1 && Cil.isPointerType t2 ->
+      MinusPP, Linteger
+    | Ctype(t), _ when Cil.isPointerType t ->
+      MinusPI, Ctype(t)
+    | t, _ ->
+      MinusA, t
+  in
+  term ?loc (TBinOp(minus, t1, t2)) typ
+
+let tplus ?loc t1 t2 =
+  let plus = match t1.term_type with
+    | Ctype(t) when Cil.isPointerType t -> PlusPI
+    | _ -> PlusA
+  in
+  term ?loc (TBinOp(plus, t1, t2)) t1.term_type
+
+let tdivide ?loc t1 t2 =
+  term ?loc (TBinOp(Div, t1, t2)) t1.term_type
+
+let ttype_of_pointed = function
+  | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> Ctype t
+  | _ -> assert false
+
+let tbuffer_range ?loc ptr len =
+  let last = tminus ?loc len (tinteger ?loc 1) in
+  let range = trange ?loc (Some (tinteger ?loc 0), Some last) in
+  tplus ?loc ptr range
+
+let rec tunref_range ?loc ptr len =
+  let typ = ttype_of_pointed ptr.term_type in
+  let range = tbuffer_range ?loc ptr len in
+  let tlval = (TMem range), TNoOffset in
+  let tlval, typ = tunref_range_unfold ?loc tlval typ in
+  term (TLval tlval) typ
+and tunref_range_unfold ?loc lval typ =
+  match typ with
+  | Ctype(TArray(typ, Some e, _, _)) ->
+    let len = Logic_utils.expr_to_term ~cast:false e in
+    let last = tminus ?loc len (tinteger ?loc 1) in
+    let range = trange ?loc (Some (tinteger ?loc 0), Some last) in
+    let lval = addTermOffsetLval (TIndex(range, TNoOffset)) lval in
+    tunref_range_unfold lval (Ctype typ)
+  | _ -> lval, typ
+
+let taccess ?loc ptr offset =
+  let get_lval = function
+    | TLval(lval) -> lval
+    | _ -> assert false
+  in
+  match ptr.term_type with
+  | Ctype(TPtr(_)) ->
+    let address = tplus ?loc ptr offset in
+    let lval = TLval(TMem(address), TNoOffset) in
+    term ?loc lval (ttype_of_pointed ptr.term_type)
+  | Ctype(TArray(_)) ->
+    let lval = get_lval ptr.term_node in
+    let lval = addTermOffsetLval (TIndex(offset, TNoOffset)) lval in
+    term ?loc (TLval lval) (ttype_of_pointed ptr.term_type)
+  | _ -> assert false
+
+let sizeofpointed = function
+  | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> Cil.bytesSizeOf t
+  | _ -> assert false
+
+let sizeof = function
+  | Ctype t -> Cil.bytesSizeOf t
+  | _ -> assert false
+
+let unroll_logic_type = function
+  | Ctype t -> Ctype (Cil.unrollType t)
+  | t -> t
+
+let tunref_range_bytes_len ?loc ptr bytes_len =
+  let sizeof = sizeofpointed ptr.term_type in
+  if sizeof = 1 then
+    tunref_range ?loc ptr bytes_len
+  else
+    let sizeof = tinteger ?loc sizeof in
+    let len = tdivide ?loc bytes_len sizeof in
+    tunref_range ?loc ptr len
+
+
+(** Features related to predicates *)
+
+let plet_len_div_size ?loc ?name_ext t bytes_len pred =
+  let sizeof = sizeofpointed t in
+  if sizeof = 1 then
+    pred bytes_len
+  else
+    let len = tdivide ?loc bytes_len (tinteger ?loc sizeof) in
+    let len_var = size_var ?name_ext Linteger len in
+    plet ?loc len_var (pred (tvar len_var.l_var_info))
+
+let pgeneric_valid_buffer ?loc validity lbl ptr len =
+  let buffer = tbuffer_range ?loc ptr len in
+  validity ?loc (lbl, buffer)
+
+let pgeneric_valid_len_bytes ?loc validity lbl ptr bytes_len =
+  plet_len_div_size ?loc ptr.term_type bytes_len
+    (pgeneric_valid_buffer ?loc validity lbl ptr)
+
+let pvalid_len_bytes ?loc = pgeneric_valid_len_bytes ?loc pvalid
+let pvalid_read_len_bytes ?loc = pgeneric_valid_len_bytes ?loc pvalid_read
+
+let pcorrect_len_bytes ?loc t bytes_len =
+  let sizeof = tinteger ?loc (sizeofpointed t) in
+  let modulo = term ?loc (TBinOp(Mod, bytes_len, sizeof)) Linteger in
+  prel ?loc (Req, modulo, tinteger ?loc 0)
+
+let pbounds_incl_excl ?loc low value up =
+  let geq_0 = prel ?loc (Rle, low, value) in
+  let lt_len = prel ?loc (Rlt, value, up) in
+  pand ?loc (geq_0, lt_len)
+
+let rec punfold_all_elems_eq ?loc t1 t2 len =
+  assert(Cil_datatype.Logic_type.equal t1.term_type t2.term_type) ;
+  pall_elems_eq ?loc 0 t1 t2 len
+and pall_elems_eq ?loc depth t1 t2 len =
+  let ind = make_logic_var_quant ("j" ^ (string_of_int depth)) Linteger in
+  let tind = tvar ind in
+  let bounds = pbounds_incl_excl ?loc (tinteger 0) tind len in
+  let t1_acc = taccess ?loc t1 tind in
+  let t2_acc = taccess ?loc t2 tind in
+  let eq = peq_unfold ?loc (depth+1) t1_acc t2_acc in
+  pforall ?loc ([ind], (pimplies ?loc (bounds, eq)))
+and peq_unfold ?loc depth t1 t2 =
+  match unroll_logic_type t1.term_type with
+  | Ctype(TArray(_, Some len, _, _)) ->
+    let len = Logic_utils.expr_to_term ~cast:false len in
+    pall_elems_eq ?loc depth t1 t2 len
+  | _ -> prel ?loc (Req, t1, t2)
+
+let rec punfold_all_elems_pred ?loc t1 len pred =
+  pall_elems_pred ?loc 0 t1 len pred
+and pall_elems_pred ?loc depth t1 len pred =
+  let ind = make_logic_var_quant ("j" ^ (string_of_int depth)) Linteger in
+  let tind = tvar ind in
+  let bounds = pbounds_incl_excl ?loc (tinteger 0) tind len in
+  let t1_acc = taccess ?loc t1 tind in
+  let eq = punfold_pred ?loc depth t1_acc pred in
+  pforall ?loc ([ind], (pimplies ?loc (bounds, eq)))
+and punfold_pred ?loc ?(dyn_len = None) depth t1 pred =
+  match unroll_logic_type t1.term_type with
+  | Ctype(TArray(_, opt_len, _, _)) ->
+    let len = match opt_len, dyn_len with
+      | Some len, None -> Logic_utils.expr_to_term ~cast:false len
+      | _   , Some len -> len
+      | None, None -> assert false
+    in
+    pall_elems_pred ?loc (depth+1) t1 len pred
+  | Ctype(TComp(ci, _, _)) ->
+    pall_fields_pred ?loc depth t1 ci pred
+  | _ -> pred ?loc t1
+and pall_fields_pred ?loc ?(flex_mem_len=None) depth t1 ci pred =