Library FminortoCminor_proof2

Specification of the GC behavior on the memory model of Cminor

Author : Zaynah Dargaye

Created: 29th April 2009





Require Import List.

Require Import Coqlib.

Require Import Coqlib2.

Require Import AST.

Require Import Globalenvs.

Require Import Maps.

Require Import Mml.

Require Import Mml_pre.

Require Import FSets.

Require Import FSetAVL.

Require Import Ordered.

Require Import Compare_dec.

Require Import EqNat.

Require Import Fminor.

Require Import Cminor.

Require Import Op.

Require Import Integers.

Require Import Cmconstr.

Require Import Values.

Require Import Cmconstrproof.

Require Import Mem.

Require Import FminortoCminor.

Require Import Switch.

Require Import FminortoCminor_proof1.

Require Import Fminor_well.




Definition lim_stack (q:nat):= 

 8+Z_of_nat q*4+4 < Int.max_signed.




Lemma load_valid: 

 forall chunk m b ofs v, load chunk m b ofs = Some v -> 

 valid_block m b.




Inductive same_bound:mem->mem->block->Prop:= 

| sbound_intro: forall m1 m2 b, 

      (high_bound m1 b) = (high_bound m2 b) -> 

      (low_bound m1 b) = (low_bound m2 b) ->

      same_bound m1 m2 b.

Preservation of a stack block between 2 different memory configurations


Inductive same_block:mem->mem->block->Prop:= 

|sheap_intro: forall m1 m2 b   , 

     same_bound m1 m2 b ->

     (forall delta , load Mint32 m1 b delta = 

                              load Mint32 m2 b delta)->

    same_block m1 m2  b .




Lemma same_bound_sym: 

 forall m m1 b, same_bound m m1 b -> 

   same_bound m1 m b.




Lemma same_bound_refl: 

 forall m r, same_bound m m r.




Lemma same_bound_trans : 

 forall m1 m2 m3 r, same_bound m1 m2 r -> 

 same_bound m2 m3 r -> 

 same_bound m1 m3 r.




Lemma same_block_refl: 

 forall m r , same_block m m r.




Lemma same_block_sym: 

 forall m1 m2 r, 

   same_block m1 m2 r -> 

   same_block m2 m1 r.




Lemma same_block_trans: 

 forall r m1 m2 m3,  

   same_block m1 m2 r -> 

   same_block m2 m3 r ->

   same_block m1 m3 r.

Preservation of a heap block into 2 different memory configurations


Inductive same_block_heap:mem->mem->block->Prop:=

| sb_info: forall m1 m2 b, 

        (valid_block m1 b ->valid_block m2 b) ->

        same_block m1 m2 b ->

        same_block_heap m1 m2 b.




Lemma same_block_heap_refl: 

 forall m r , same_block_heap m m r.




Lemma same_block_heap_trans: 

 forall r m1 m2 m3,  

   same_block_heap m1 m2 r -> 

   same_block_heap m2 m3 r ->

   same_block_heap m1 m3 r.

Block kinds and mapping


Inductive Bkind:Set:= 

 |RB : Bkind |HB: Bkind| GB:Bkind.




Definition block_kind :Set:= block -> option Bkind.




Section ACC.




Variable bkind:block_kind.

Reachability between stack blocks


Inductive acc_root:mem->block ->block->Prop:= 

| acc_simpl : forall m r, 

     bkind r = Some RB -> acc_root m r r 

| acc_ctrans: forall m  r v v' ,

     load Mint32 m r 0 = Some (Vptr v Int.zero)->

     Zlt v r -> Zle v' v -> 

     bkind r = Some RB -> bkind v = Some RB -> 

      bkind v' = Some RB -> 

     acc_root m v v' ->  

     acc_root m r v'.




Lemma acc_root_lt: 

 forall m r r', acc_root m r r' -> r >= r'.




Lemma not_acc_root_new: 

 forall m r r' , r < r' -> ~acc_root m r r'.




Lemma acc_root_trans: 

 forall m r r1, acc_root m r r1 -> 

   forall r2, acc_root m r1 r2 -> 

       acc_root m r r2.




Lemma acc_root_valid: 

 forall m r r', acc_root m r r' -> 

  valid_block m r ->valid_block m r'.




Lemma acc_root_tail : 

 forall  m spn sp2, acc_root m spn sp2 -> 

    forall sp 

       (AR: acc_root m spn sp)  

       (Neq: spn <> sp2)

       (L:load Mint32 m spn 0 = Some (Vptr sp Int.zero)) 

       (C: sp < spn), 

       acc_root  m sp sp2.




Lemma acc_root_incr: 

 forall m v v', acc_root m v v' -> 

 forall chunk m' sp ofs x 

      (ST:store chunk m' sp ofs x = Some m)

      (CMP: ofs>= 4) , 

      acc_root m' v v'.







Lemma acc_root_store: 

 forall m r r', acc_root m r r' -> 

  forall  b ofs w m1

       (NEQ1: b >r)   

      (ST: store Mint32 m b ofs w = Some m1),

      acc_root m1 r r'.




Lemma acc_root_store_heap: 

  forall m r r', acc_root m r r' -> 

  forall  b ofs w m1 

       (NEQ1: bkind b = Some HB)   

      (ST: store Mint32 m b ofs w = Some m1),

      acc_root m1 r r'.






Inductive acc_heap:mem->block->block ->Prop:= 

|acc_h1: forall m b ,  

   bkind b = Some HB-> 

   valid_block m b-> acc_heap m b b  

|acc_h2: forall m b n v v' ,

        (low_bound m b) = 0 -> 

        0<= n*4 <  (high_bound m b) ->

        (high_bound m b) < Int.max_signed -> 

        load Mint32 m b (n*4) = Some (Vptr v Int.zero)->

        bkind b= Some HB -> bkind v= Some HB-> 

        bkind v' = Some HB->

        Zlt v b -> Zle v' v ->

        acc_heap m v v' ->

        acc_heap m b v'.




Lemma acc_heap_lt: 

 forall m v v', acc_heap m v v' -> v'<=v.




Lemma acc_heap_kind: 

 forall m v v' , acc_heap m v v' -> 

 bkind v = Some HB /\ bkind v' = Some HB.




Lemma acc_heap_trans: 

 forall   m v v',   acc_heap m v v'-> 

     forall v'' (A2: acc_heap m v' v''),    

     acc_heap m v v''.




Lemma acc_heap_valid: 

 forall m b b', acc_heap m b b' -> 

     valid_block m b /\ valid_block m b'.




Lemma loadlist_acc_heap: 

 forall  vpl  b m  k

   (COND3: low_bound m b = 0) 

   (COND2: (high_bound m b) < Int.max_signed)

   (COND:(high_bound m b)= (Z_of_nat (plus k (length vpl))*4)+4  )

   (LDL: loadlist m b (Z_of_nat k*4)  (length vpl) = 

         Some (map (fun x=>Vptr x Int.zero) vpl))

   (KD: bkind b = Some HB )

   (VDL : forall i, In i vpl -> 

         valid_block m i/\ 

        bkind i=Some HB /\ i < b),

   (forall vi , In vi vpl -> acc_heap m b vi).

Reachability from the current stack block


Inductive acc:mem->block->block->Prop:= 

| acc_intro: forall m r r'  k v v', 

   acc_root m r r' ->

   load Mint32 m r' (8+k*4) = Some (Vptr v Int.zero) ->

   (8+k*4) < (high_bound m r')-> 

   (high_bound m r') < Int.max_signed ->  

    acc_heap m v v' ->

   acc m r v'.




Lemma acc_kind: 

 forall m r b, acc m r b -> 

  bkind r = Some RB /\ bkind b = Some HB.




Lemma acc_valid: 

 forall m r v, acc m r v -> valid_block m v.







Lemma acc_acc_root_trans: 

 forall m r v, acc_root m r v -> 

  forall v0 (AC:acc m v v0) , 

     acc m r v0.




Lemma acc_acc_heap_acc: 

 forall m sp b l k q

     (LDSz: load Mint32 m sp 4 = Some  (Vint (Int.repr (Z_of_nat q))))

     (COND:  0<=k <  Z_of_nat q) 

     (CONDz : 8+Z_of_nat q*4+4 = high_bound m sp)

     (COND2: lim_stack q)

      (ID: bkind sp = Some RB)

     (ACC: load Mint32 m sp (8+ k*4) = Some (Vptr b Int.zero)) 

     (ACH: forall i, In i l -> acc_heap m b i) , 

    (forall ni i, nth_error l ni = Some i  -> acc m sp i).







Lemma acc_same_blocks:

forall cvl sp m1 ma 

   (K: forall v : block, acc m1 sp v -> 

           same_block m1 ma v)

  (K2:forall (ni : nat) (i : block),

     nth_error cvl ni = Some i -> acc m1 sp i),

  (forall i , In i cvl ->    same_block m1 ma i) .




Lemma heap_acc_same_heap: 

forall m1 sp b ma

  (ACC: acc m1 sp b )

 (SHB: forall v : block, acc m1 sp v -> 

      same_block_heap m1 ma v )

 (SHA: same_block_heap m1 ma b), 

 (forall k, acc_heap m1 b k -> 

               same_block_heap m1 ma k).




Lemma acc_trans: 

  forall m sp b v ofs 

   (ACC : acc m sp b) 

   (C1: low_bound m b = 0) 

   (C2: high_bound m b < Int.max_signed)

   (C3: valid_block m v) 

   (ID1:bkind b = Some HB)

   (ID2:bkind v = Some HB)

   (NEQ: v<b)  

   (LD: load Mint32 m b (ofs*4) = Some (Vptr v Int.zero) ), 

    acc m sp v.




Lemma acc_loadlist:

forall cvl m sp b  j  

 (ACC:acc m sp b)

   (KD: bkind b = Some HB)

  (C1: low_bound m b = 0) 

  (C2: high_bound m b < Int.max_signed) 

  (C3: forall i, In i cvl -> valid_block m i) 

  (NEQ: forall i, In i cvl ->  

     bkind i = Some HB /\ i<b)

 (LDL:  loadlist m b (j*4) (length cvl) =

      Some (map (fun x : block => Vptr x Int.zero) cvl)) , 

 forall c : block, In c cvl -> acc m sp c .







Inductive fresh_block :block->Prop:= 

 | fresh_intro: forall b, 

      bkind b = Some HB -> 

     (forall b', bkind b' = Some HB -> b' < b) ->

     fresh_block b.




Lemma acc_heap_store:

 forall m v v',   acc_heap m v v'->

    forall chunk  b ofs m1 w 

      (NEQ1: fresh_block b)       

      (ST: store chunk m b ofs w = Some m1),

       acc_heap m1 v v'.




Lemma acc_store_heap: 

 forall m r v, acc m r v -> 

     forall b ofs w m1 

      (ID: bkind b = Some HB) 

      (NEQ1: fresh_block b) 

      (ST: store Mint32 m b ofs w = Some m1),

      acc m1 r v.







Lemma acc_store_root: 

 forall m r v, acc m r v -> 

     forall  ofs w m1 b

      (NEQ1: fresh_block b) 

      (ST: store Mint32 m b ofs w = Some m1),

      acc m1 r v.










End ACC.

Mapping of block in a memory configuration to block-kind


Inductive mem_block_kind:mem->block_kind->Prop:= 

 | mb_intro: forall m f, 

      (forall b, ~valid_block m b<-> f b = None) -> 

      (forall b info, f b = Some info -> valid_block m b) ->

      (forall b, valid_block m b -> exists info, f b = Some info)->

      mem_block_kind m f.




Inductive block_kind_incr:block_kind-> block_kind->Prop:=

| bki: forall f1 f2 , 

   (forall b info, f1 b = Some info -> f2 b  = Some info) -> 

   (forall b, f2 b = Some GB -> f1 b = Some GB) -> 

   block_kind_incr f1 f2.




Lemma block_kind_incr_refl: 

 forall f, block_kind_incr f f.




Definition block_kind_incr_trans: 

 forall f1 f2 f3 

    (A:block_kind_incr f1 f2) (B:block_kind_incr f2 f3),

    block_kind_incr f1 f3.




Lemma acc_root_same_block: 

 forall f1 m r r1, acc_root f1 m r r1 -> 

     forall m2 f2

     (BI:block_kind_incr f1 f2)

     (M1: mem_block_kind m f1) 

     (M2: mem_block_kind m2 f2)  

     (LD:forall r2, acc_root f1 m r r2 -> same_block m m2 r2), 

    acc_root f2 m2 r r1.

Preservation of roots and reachables datas





Inductive gc_mem:mem->block_kind->

                              block->mem->block_kind->Prop:= 

|gcm_intro: forall r m1 f1 m2 f2, 

      mem_block_kind m1 f1 -> 

      mem_block_kind m2 f2 -> 

      block_kind_incr f1 f2->

      f1 r = Some RB -> 

      (forall r',  acc_root f1 m1 r r' -> same_block  m1 m2 r')->

     (forall v, acc f1 m1 r v ->same_block_heap m1 m2 v)-> 

     gc_mem m1 f1 r m2 f2.




Lemma gc_mem_refl: 

 forall sp ma fa, fa sp = Some RB-> 

 mem_block_kind ma fa-> 

 gc_mem ma fa sp ma fa.




Lemma gc_mem_trans: 

 forall f1 m1 sp r, acc_root f1 m1 sp r -> 

    forall f2 m2 (GC: gc_mem m1 f1 sp m2 f2 ) , 

    gc_mem m1 f1 r m2 f2.







Lemma acc_heap_smbh:

forall f1 m v v', acc_heap f1 m v v' -> 

 forall f2 m2 b

 (FI: block_kind_incr f1 f2)

 (K : forall k : block, acc_heap f1 m b k -> 

        same_block_heap m m2 k) 

 (AH: acc_heap f1 m b v), 

 acc_heap f2 m2 v v'.










Lemma acc_heap_same_block: 

 forall f1 m v r1, acc_heap f1 m v r1-> 

 forall r r' k m2 f2

   (AR:acc_root f1 m r r') 

   (LD:load Mint32 m r' (8 + k * 4) = Some (Vptr v Int.zero))

   (C1:8 + k * 4 < high_bound m r')

   (C2:high_bound m r' < Int.max_signed) 

   (GC:gc_mem m f1 r m2 f2), 

 acc_heap f2 m2 v r1.













Lemma acc_same_block: 

 forall f1 m r r1, acc f1 m r r1 -> 

     forall f2 m2, gc_mem m f1 r m2 f2 -> 

    acc f2 m2 r r1.




Lemma gc_trans: 

   forall m1 f1 m2 f2 m3 f3 sp

    (A: gc_mem m1 f1 sp m2 f2) 

    (B:gc_mem m2 f2 sp m3 f3), 

    gc_mem m1 f1 sp m3 f3.




Lemma mem_block_kind_store:

 forall fa ma   z0 ofs v m1  

 (MBK:mem_block_kind ma fa)

 (ST: store Mint32 ma z0 ofs v = Some m1) ,  

 mem_block_kind m1 fa.




Lemma gc_mem_sp_new:

 forall fa ma  sp z0 ofs v m1  

 (VB: valid_block ma sp)

 (NEQ:z0>sp) (ID1:fa z0 = Some RB) 

 (ID2:fa sp = Some RB)

 (MBK:mem_block_kind ma fa)

 (ST: store Mint32 ma z0 ofs v = Some m1) ,  

 gc_mem ma fa sp m1 fa.













Lemma gc_mem_store:

 forall v fa ma  sp z0 ofs m1 

 (ID: fa z0 = Some HB)

 (FRE: fresh_block fa z0) (NEQ:fa sp= Some RB)

 (ST: store Mint32 ma z0 ofs v = Some m1) 

  (MBK:mem_block_kind ma fa) ,  

 gc_mem ma fa sp m1 fa.







Lemma gc_mem_storelist:

 forall v fa ma  sp z0 ofs m1 

 (ID: fa z0 = Some HB)

 (FRE: fresh_block fa z0) (NEQ:fa sp= Some RB)

 (ST: storelist ma z0 ofs v = Some m1) 

  (MBK:mem_block_kind ma fa) ,  

 gc_mem ma fa sp m1 fa.

Allocated a new stack block consequencies


Definition add_root (f: block_kind) (b: block):= 

 fun b' => if (zeq b b') then (Some RB) else f b'.




Lemma block_kind_incr_alloc: 

 forall f spa, 

  f spa= None -> block_kind_incr f (add_root f spa).




Lemma mem_block_kind_alloc: 

 forall f ms ma spa q 

 (ALL: alloc ms 0 q = (ma,spa ))

 (MBK: mem_block_kind ms f) , 

 mem_block_kind ma (add_root f spa).













Lemma gc_mem_alloc: 

 forall f ms sp  ma spa q 

 (VB: valid_block ms sp)

 (ID: f sp = Some RB)

 (ALL: alloc ms 0 q = (ma,spa ))

 (MBK: mem_block_kind ms f) , 

  gc_mem ms f sp  ma (add_root f spa).







Lemma mem_block_kind_free: 

 forall ms f b (MBK:mem_block_kind ms f), 

  mem_block_kind (free ms b) f.




Lemma gc_free: 

 forall f ms sp spnew (NEQ: sp<spnew)

 (ID1: f sp = Some RB) 

 (ID2: f spnew = Some RB)

 (MBK:mem_block_kind ms f), 

 gc_mem ms f sp (free ms spnew) f .

Ancestor roots preservation between two memory configurations





Inductive roots_trans:

 mem->block_kind->block->mem->block_kind->Prop:= 

 |rt_intro: 

   forall m1 f1 sp m2 f2,

       mem_block_kind m1 f1 -> 

       mem_block_kind m2 f2 -> 

       block_kind_incr f1 f2->      

       f1 sp = Some RB ->  

       (forall R, R < sp -> f1 R = Some RB -> 

       load Mint32 m1 sp 0 = Some (Vptr R Int.zero) ->

       gc_mem m1 f1 R m2 f2)  ->

       load Mint32 m1 sp 0 = load Mint32 m2 sp 0 -> 

       roots_trans m1 f1 sp m2 f2.




Lemma rt_refl: 

 forall f1 m1 sp  (ID: f1 sp = Some RB)

   (MBK:mem_block_kind m1 f1), 

   roots_trans m1 f1 sp m1 f1.




Lemma rt_store_sp: 

 forall f1 m1 sp ofs v m2 

    (ID: f1 sp = Some RB)

    (ST: store Mint32 m1 sp ofs v =Some m2) 

    (COND: ofs >=4)

    (MBK:mem_block_kind m1 f1), 

    roots_trans m1 f1 sp m2 f1.
















Lemma gc_mem_roots_trans: 

 forall m1 f1 sp m2 f2

    (GC: gc_mem m1 f1 sp m2 f2) ,  

    roots_trans m1 f1 sp m2 f2.




Lemma rt_trans: 

 forall m1 f1 m2 f2 m3 f3 sp 

          (A: roots_trans m1 f1 sp m2 f2) 

          (B: roots_trans m2 f2 sp m3 f3), 

          roots_trans m1 f1 sp m3 f3.




Lemma rt_root_trans: 

 forall f1 m1 sp r, acc_root f1 m1 sp r -> 

    forall f2 m2 (GC: roots_trans m1 f1 sp m2 f2 ) , 

    roots_trans m1 f1 r m2 f2.










Lemma gc_roots_trans:

 forall f1 m1 sp sp2, acc_root f1 m1 sp sp2 -> 

  forall ml fl  (C1: sp2 < sp) 

            (RT:roots_trans m1 f1 sp ml fl ),  

            gc_mem m1 f1 sp2 ml fl.




Lemma gc_mem_acc_root_inv: 

 forall fl ml sp sp2, acc_root fl ml sp sp2 -> 

  forall m1 f1  (C1: sp2 < sp) 

            (RT:roots_trans m1 f1 sp ml fl ),  

            acc_root f1 m1 sp sp2.




Lemma gc_tail: 

 forall   fl ml sp sp2, acc_root fl ml sp sp2 -> 

  forall m1 f1  (C1: sp2 < sp) 

            (RT:roots_trans m1 f1 sp ml fl ),  

   acc_root f1 m1 sp sp2/\gc_mem m1 f1 sp2 ml fl.

Properties of the stack block bound





Definition sp_block (sp:block) (m:mem) (q:nat):= 

 (high_bound m sp ) = 8 + Z_of_nat q * 4 + 4 /\

 (low_bound m sp) = 0%Z /\ 

 valid_block m sp .




Lemma valid_store_stack_access: 

 forall sp m q n , 

 lim_stack q ->sp_block sp m q -> bound_test n q -> 

 valid_access m Mint32 sp (8+Z_of_nat n*4).




Lemma valid_store_size_access: 

 forall sp m q , 

 lim_stack q ->sp_block sp m q ->  

 valid_access m Mint32 sp 4.




Lemma slotaddr_correct: 

forall n q, 

    lim_stack q-> bound_test n q-> 

    (Int.signed (slotaddr n)) = (8 + Z_of_nat n * 4).




Lemma sp_block_store: 

 forall sp m q chunk  b ofs v m2 

     (SB:sp_block sp m q) 

     (ST: store chunk m b ofs v = Some m2) , 

     sp_block sp m2 q.




Lemma sp_block_storelist: 

 forall sp m q b ofs v m2 

     (SB:sp_block sp m q) 

     (ST: storelist m b ofs v = Some m2) , 

     sp_block sp m2 q.




Lemma vt_prop: 

 forall id, var_test id = true -> var_test_prop id.




Lemma ceval_length: 

 forall  e s1 al vl, 

ceval_atlist  e s1 al vl -> length vl = length al.







Lemma store1_eval: 

forall t v g sp e ma z0 mf k id 

 (GET: e!id = Some (Vptr z0 Int.zero))

 (E:Eval_expr  g sp e ma t  v) 

 (ST:store Mint32 ma z0 k  (Vptr v Int.zero) = Some mf) 

 (COND: 0 <= k < Int.max_signed),

 exec_stmt g sp e ma (Sstore Mint32 (addimm (Evar id) k) t)

 Eve e mf Out_normal.







Lemma store_2_eval: 

forall ma z0 k v mf 

 (ST:store Mint32 ma z0 k  v = Some mf),  

 (forall c, c<>z0 ->same_block ma mf c).




Definition mem_incr (m1 m2: mem)(x:block):Prop:= 

 forall chunk b v ofs, b<>x ->load chunk m1 b ofs=Some v -> 

              load chunk m2 b ofs= Some v.




Lemma store_incr: 

 forall ma z0 k v mf 

 (ST:store Mint32 ma z0 k  v = Some mf) , 

 mem_incr ma mf z0.




Lemma mem_incr_trans : 

 forall z0 ma mb mc, mem_incr ma mb z0 -> 

          mem_incr mb mc z0 -> 

          mem_incr ma mc z0.

Evaluation of some specific smart constructors





Lemma storelist_eval: 

forall tl pvl g sp e ma fa z0 mf k id

 (ID0: fa z0 = Some HB)

 (FRESH: fresh_block fa z0)

 (MBK:mem_block_kind ma fa) 

 (GET: e!id = Some (Vptr z0 Int.zero))

 (E:Eval_exprlist g sp e ma tl  pvl)

 (Vb: forall mi, mem_incr ma mi z0-> 

        Eval_exprlist g sp e mi tl  pvl)

 (ST:storelist ma z0 k  (map (fun x=> Vptr x Int.zero) pvl) = Some mf) 

 (COND: 0 <= k+ (Z_of_nat (length pvl) *4) < Int.max_signed)

 (COND2: 0<=k),

 exec_stmt g sp e ma (gen_fill_block id k tl) 

 Eve e mf Out_normal.




Lemma map_nth_error: 

 forall A B l n (v:A) (f:A->B) , nth_error l n = Some v -> 

                       nth_error (map f l) n = Some (f v).




Lemma in_map_vptr: 

 forall l a, In a (map (fun x => Vptr x Int.zero) l) -> 

   (exists i, a= Vint i) \/ (exists b, exists o,a=Vptr b o)  .




Lemma mkconstr_eval: 

forall g sp ce1 m1 z ms id z0 ma  mf tl cv v t fa

 (A: exec_stmt g (Vptr sp Int.zero) ce1 m1 (Store_stsize (Z_of_nat z)) Eve

        ce1 ms Out_normal) 

 (B: exec_stmt g (Vptr sp Int.zero) ce1 ms (alloc_call id (S (length cv)))

       Eve (PTree.set id (Vptr z0 Int.zero) (PTree.empty val)) ma Out_normal)

 (V: forall mi, mem_incr ma mi z0-> 

        Eval_exprlist g (Vptr sp Int.zero)

      (PTree.set id (Vptr z0 Int.zero) (PTree.empty val)) mi tl  cv)

 (D:Eval_exprlist g (Vptr sp Int.zero)

      (PTree.set id (Vptr z0 Int.zero) (PTree.empty val)) ma tl cv)

 (E : storelist ma z0 (Z_of_nat 0 * 4) 

         (v:: (map (fun x=>Vptr x Int.zero) cv))

        = Some mf)

 (F: Z_of_nat (S (length cv)) * 4 + 4 < Int.max_signed)

 (ID0: fa z0 = Some HB)

 (X: mem_block_kind ma fa)

 (G: fresh_block fa z0)

 (I: eval_expr g (Vptr sp Int.zero) nil

      (PTree.set id (Vptr z0 Int.zero)

       (PTree.empty val)) ma t Eve ma v),

 exec_stmt g (Vptr sp Int.zero) ce1 m1

  (Sseq (Store_stsize (Z_of_nat z))

     (Sseq (alloc_call id (S (length cv)))

        (Sseq (Sstore Mint32 (Evar id) t)

           (gen_fill_block id 4 tl)))) Eve

  (PTree.set id (Vptr z0 Int.zero) (PTree.empty val)) mf Out_normal.