Changeset 485


Ignore:
Timestamp:
Feb 2, 2011, 12:41:05 PM (9 years ago)
Author:
campbell
Message:

Fix treatment of pointers in initialisation data, a little like later versions
of CompCert?. Remove obsolete Init_pointer.

Location:
Deliverables/D3.1/C-semantics
Files:
1 added
10 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D3.1/C-semantics/AST.ma

    r483 r485  
    147147  | Init_space: Z → init_data
    148148  | Init_null: region → init_data
    149   | Init_addrof: ident → int → init_data   (*r address of symbol + offset *)
    150   | Init_pointer: list init_data → init_data.
     149  | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
    151150
    152151(* * Whole programs consist of:

  • Deliverables/D3.1/C-semantics/Cexec.ma

    r484 r485  
    9898#A B C P P' e f; nelim e; //;
    9999#v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.
    100 
    101 ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
    102 nlemma opt_OK: ∀A,P,e.
    103   (∀v. e = Some ? v → P v) →
    104   match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
    105 #A P e; nelim e; /2/;
    106 nqed.
    107100
    108101nlemma opt_bind_OK: ∀A,B,P,e,f.
    … …  
    679672].
    680673
    681 nlet rec make_initial_state (p:clight_program) : res state ≝
    682   let ge ≝ globalenv Genv ?? p in
    683   let m0 ≝ init_mem Genv ?? p in
    684     do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    685     do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
    686     do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
    687     OK ? (Callstate f (nil ?) Kstop m0).
     674nlet rec make_initial_state (p:clight_program) : res (genv × state) ≝
     675  do ge ← globalenv Genv ?? p;
     676  do m0 ← init_mem Genv ?? p;
     677  do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
     678  do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
     679  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
     680  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
    688681
    689682ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r).
    … …  
    756749
    757750ndefinition exec_inf : clight_program → execution ≝
    758 λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,s〉).
     751λp.
     752  match make_initial_state p with
     753  [ OK gs ⇒ exec_inf_aux (\fst gs) (ret ? 〈E0,\snd gs〉)
     754  | _ ⇒ e_wrong
     755  ].
    759756
    760757nremark execution_cases: ∀e.

  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r484 r485  
    5757initial_state p s → initial_state p s' → s = s'.
    5858#p s s' H1 H2;
    59 ninversion H1; #b1 f1 e11 e12 e13;
    60 ninversion H2; #b2 f2 e21 e22 e23;
    61 nrewrite > e11 in e21;
    62 #e1; nrewrite > (?:b1 = b2) in e12;
    63 ##[ nrewrite > e22; #e2; nrewrite > (?:f2 = f1);
     59ninversion H1; #b1 f1 ge1 m1 e11 e12 e13 e14 e15;
     60ninversion H2; #b2 f2 ge2 m2 e21 e22 e23 e24 e25;
     61nrewrite > e11 in e21; #e1; nrewrite > (?:ge1 = ge2) in e13 e14;
     62##[ ##2: ndestruct (e1) skip (e11); napply refl; ##]
     63#e13 e14;
     64
     65nrewrite > e12 in e22; #e2; ndestruct (e2) skip (e12);
     66
     67nrewrite > e13 in e23; #e3; nrewrite > (?:b1 = b2) in e14;
     68##[ nrewrite > e24; #e4; nrewrite > (?:f2 = f1);
    6469  ##[ //;
    65   ##| ndestruct (e2) skip (e22 e23); //;
     70  ##| ndestruct (e4) skip (e24 e25); //;
    6671  ##]
    67 ##| ndestruct (e1) skip (e11); //
     72##| ndestruct (e3) skip (e13); //
    6873##] nqed.
    6974
    … …  
    7883
    7984ntheorem the_initial_state:
    80   ∀p,s. initial_state p s → yields ? (make_initial_state p) s.
     85  ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉.
    8186#p s; ncases p; #fns main globs H;
    8287ninversion H;
    83 #b f e1 e2 e3;
     88#b f ge m e1 e2 e3 e4 e5; @ge;
    8489nwhd in ⊢ (??%?);
    8590nrewrite > e1;
    8691nwhd in ⊢ (??%?);
    8792nrewrite > e2;
     93nwhd in ⊢ (??%?);
     94nrewrite > e3;
     95nwhd in ⊢ (??%?);
     96nrewrite > e4;
    8897nwhd; napply refl;
    8998nqed.

  • Deliverables/D3.1/C-semantics/CexecEquiv.ma

    r399 r485  
    948948  ¬ ∃r.final_state s r.
    949949#ge s H; ncases H;
    950 #b f E1 E2; @; *; #r H2;
     950#b f ge m E1 E2 E3 E4; @; *; #r H2;
    951951ninversion H2;
    952 #r' m E3 E4; ndestruct (E3);
     952#r' m' E5 E6; ndestruct (E5);
    953953nqed.
    954954
    … …  
    972972   ∃b.execution_matches_behavior e b ∧ exec_program p b.
    973973#classic constructive_indefinite_description p e;
    974 nwhd in ⊢ (?%? → ??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);
     974nwhd in ⊢ (?%? → ??(λ_.?(?%?)%));
    975975nlapply (make_initial_state_sound p);
    976976nlapply (the_initial_state p);
    977977ncases (make_initial_state p);
    978 ##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?(??%)? → ?);
     978##[ #gs; ncases gs; #ge s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?%? → ?);
     979    ncases INITIAL; #Ege INITIAL'';
    979980    nrewrite > (exec_inf_aux_unfold …);
    980981    nwhd in ⊢ (?%? → ?);
    981982    ncases (is_final_state s);
    982983    ##[ #F; napply False_ind;
    983         napply (absurd ?? (initial_state_not_final … INITIAL));
     984        napply (absurd ?? (initial_state_not_final … INITIAL''));
    984985        ncases F; #r F'; @r; napply F';
    985986    ##| #NOTFINAL; nwhd in ⊢ (?%? → ?); ncases e;
    … …  
    989990              (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
    990991        *; #b MATCHES; @b; @; //;
     992        #ge'; nrewrite > Ege; #Ege'; nrewrite > (?:ge' = ge); ##[ ##2: ndestruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ##]
    991993        ninversion MATCHES;
    992994        ##[ #s0 e1 tr1 r m TERM EXEC BEHAVES; nrewrite < EXEC in TERM;
    … …  
    995997            nrewrite > E1 in TERM; #TERM;
    996998            napply (program_terminates (mk_transrel … step) ?? ge s);
    997             ##[ ##2: napply INITIAL
     999            ##[ ##2: napply INITIAL''
    9981000            ##| ##3: napply (terminates_sound … TERM EXEC');
    9991001            ##| ##skip
    … …  
    10081010            #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS;
    10091011            ncases (several_steps … INITSTEPS EXEC'); #INITSTAR EXECDIV;
    1010             napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);
     1012            napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL'' INITSTAR);
    10111013            napply (silent_sound … DIVERGING EXECDIV);
    10121014        ##| #s0 e tr REACTS EXEC E2; nrewrite < EXEC in REACTS; #REACTS;
    … …  
    10171019            ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
    10181020            #E7; nrewrite < E7 in REACTING; #REACTING;
    1019             napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL);
     1021            napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL'');
    10201022            napply (reacts_sound … REACTING EXEC');
    10211023        ##| #e s1 s2 tr WRONG EXEC E2; nrewrite < EXEC in WRONG; #WRONG;
    … …  
    10241026            ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
    10251027            nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
    1026             ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
     1028            ncut (e0 = e''); ##[ ndestruct (E6) skip (INITIAL MATCHES EXEC0 EXEC'); // ##]
    10271029            #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG;
    10281030            nelim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR STOP FINAL;
    1029             napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);
     1031            napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP);
    10301032            #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
    10311033        ##| #E; ndestruct (E);
    … …  
    10351037    #NOINIT; #_; #EXEC;
    10361038    @ (Goes_wrong E0); @;
    1037     ##[ nwhd in EXEC:(?(??%)?);
    1038         nrewrite > (exec_inf_aux_unfold …) in EXEC; nwhd in ⊢ (?%? → ?);
    1039         ncases e;
     1039    ##[ nwhd in EXEC:(?%?);
     1040        ncases e in EXEC;
    10401041        ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
    10411042        ncases (se_inv … EXEC0);
    10421043        napply emb_initially_wrong;
    1043     ##| napply program_goes_initially_wrong;
    1044         #s; @; napply NOINIT;
    1045     ##]
    1046 ##] nqed.
    1047 
     1044    ##| #ge Ege;
     1045        napply program_goes_initially_wrong;
     1046        #s; @; #INIT; ncases (NOINIT s INIT); #ge' H; napply H;
     1047    ##]
     1048##] nqed.
     1049

  • Deliverables/D3.1/C-semantics/CexecSound.ma

    r484 r485  
    11include "Cexec.ma".
     2
     3include "Plogic/connectives.ma".
    24
    35nlemma exec_bool_of_val_sound: ∀v,ty,r.
    … …  
    455457nqed.
    456458
    457 nlemma make_initial_state_sound : ∀p. P_res ? (λs.initial_state p s) (make_initial_state p).
     459nlemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
    458460#p; ncases p; #fns main vars;
    459461nwhd in ⊢ (???%);
     462napply bind_OK; #ge Ege;
     463napply bind_OK; #m Em;
    460464napply opt_bind_OK; #x; ncases x; #sp b esb;
    461465napply opt_bind_OK; #u ecode;
    462466napply opt_bind_OK; #f ef;
    463467ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##]
    464 nwhd; napply (initial_state_intro … esb ef);
     468nwhd; @; //; napply (initial_state_intro … Ege Em esb ef);
    465469nqed.
    466470

  • Deliverables/D3.1/C-semantics/Csem.ma

    r484 r485  
    14761476
    14771477ninductive initial_state (p: clight_program): state -> Prop :=
    1478   | initial_state_intro: ∀b,f.
    1479       let ge := globalenv Genv ?? p in
    1480       let m0 := init_mem Genv ?? p in
    1481       find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉 ->
    1482       find_funct_ptr ?? ge b = Some ? f ->
     1478  | initial_state_intro: ∀b,f,ge,m0.
     1479      globalenv Genv ?? p = OK ? ge →
     1480      init_mem Genv ?? p = OK ? m0 →
     1481      find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉 →
     1482      find_funct_ptr ?? ge b = Some ? f →
    14831483      initial_state p (Callstate f (nil ?) Kstop m0).
    14841484
    … …  
    14951495
    14961496ndefinition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
    1497   program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh.
     1497  ∀ge. globalenv ??? p = OK ? ge →
     1498  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
    14981499(*
    14991500(** Big-step execution of a whole program.  *)

  • Deliverables/D3.1/C-semantics/Errors.ma

    r250 r485  
    1717include "Plogic/equality.ma".
    1818include "Plogic/connectives.ma".
     19include "datatypes/sums.ma".
    1920
    2021(* * Error reporting and the error monad. *)
    … …  
    192193  end.
    193194*)
     195
     196
     197ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
     198nlemma opt_OK: ∀A,P,e.
     199  (∀v. e = Some ? v → P v) →
     200  match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
     201#A P e; nelim e; /2/;
     202nqed.

  • Deliverables/D3.1/C-semantics/Globalenvs.ma

    r480 r485  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V: Type. program F V → genv_t F;
     54  globalenv: ∀F,V: Type. program F V → res (genv_t F);
    5555   (* * Return the global environment for the given program. *)
    5656
    57   init_mem: ∀F,V: Type. program F V → mem;
     57  init_mem: ∀F,V: Type. program F V → res mem;
    5858   (* * Return the initial memory state for the given program. *)
    5959
    … …  
    396396  foldr ?? (add_funct F) init fns.
    397397
     398(* init *)
     399
     400ndefinition store_init_data : ∀F.genv F → mem → region → block → Z → init_data → option mem ≝
     401λF,ge,m,r,b,p,id.
     402  match id with
     403  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
     404  | Init_int16 n ⇒ store Mint16unsigned m r b p (Vint n)
     405  | Init_int32 n ⇒ store Mint32 m r b p (Vint n)
     406  | Init_float32 n ⇒ store Mfloat32 m r b p (Vfloat n)
     407  | Init_float64 n ⇒ store Mfloat64 m r b p (Vfloat n)
     408  | Init_addrof r' symb ofs ⇒
     409      match (*find_symbol ge symb*) symbols ? ge symb with
     410      [ None ⇒ None ?
     411      | Some b' ⇒ store (Mpointer r') m r b p (Vptr r' (snd ?? b') ofs)
     412      ]
     413  | Init_space n ⇒ Some ? m
     414  | Init_null r' ⇒ store (Mpointer r') m r b p (Vnull r')
     415  ].
     416
     417ndefinition size_init_data : init_data → Z ≝
     418 λi_data.match i_data with
     419  [ Init_int8 _ ⇒ 1
     420  | Init_int16 _ ⇒ 2
     421  | Init_int32 _ ⇒ 4
     422  | Init_float32 _ ⇒ 4
     423  | Init_float64 _ ⇒ 8
     424  | Init_space n ⇒ Zmax n 0
     425  | Init_null r ⇒ size_pointer r
     426  | Init_addrof r _ _ ⇒ size_pointer r].
     427
     428nlet rec store_init_data_list (F:Type) (ge:genv F)
     429                              (m: mem) (r: region) (b: block) (p: Z) (idl: list init_data)
     430                              on idl : option mem ≝
     431  match idl with
     432  [ nil ⇒ Some ? m
     433  | cons id idl' ⇒
     434      match store_init_data F ge m r b p id with
     435      [ None ⇒ None ?
     436      | Some m' ⇒ store_init_data_list F ge m' r b (p + size_init_data id) idl'
     437      ]
     438  ].
     439
     440ndefinition size_init_data_list : list init_data → Z ≝
     441  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.
     442
     443(* Nonessential properties that may require arithmetic
     444nremark size_init_data_list_pos:
     445  ∀i_data. OZ ≤ size_init_data_list i_data.
     446#i_data;nelim i_data;//;
     447#a;#tl;ncut (OZ ≤ size_init_data a)
     448##[ncases a;nnormalize;//;
     449   #x;ncases x;nnormalize;//;
     450##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));
     451   ncut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
     452   ##[ncases (size_init_data a) in Hsize IH;
     453      ##[##1,2:/3/
     454      ##|nnormalize;#n;#Hfalse;nelim Hfalse]
     455   ##|#Hdisc;ncases Hdisc
     456      ##[#Heq;nrewrite > Heq;//;
     457      ##|#Heq;ncases Heq;#x;#Heq2;nrewrite > Heq2;
     458         (* TODO: arithmetics *) napply daemon]
     459   ##]
     460##]
     461nqed.
     462*)
     463
     464ndefinition alloc_init_data : mem → list init_data → region → mem × block ≝
     465  λm,i_data,bcl.
     466  〈mk_mem (update ? (nextblock m)
     467                 (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef) bcl)
     468                 (blocks m))
     469         (Zsucc (nextblock m))
     470         (succ_nextblock_pos m),
     471   (nextblock m)〉.
     472
     473(* init *)
     474
    398475ndefinition add_globals : ∀F,V:Type.
    399476       genv F × mem → list (ident × (list init_data) × region × V) →
    400        genv F × mem ≝
    401 λF,V,init,vars.
    402   foldr ??
    403     (λid_init: ident × (list init_data) × region × V. λg_st: genv F × mem.
     477       res (genv F × mem) ≝
     478λF,V,init_env,vars.
     479  foldl ??
     480    (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V.
    404481      match id_init with [ mk_pair id_init1 info ⇒
    405       match id_init1 with [ mk_pair id_init2 bsp ⇒
     482      match id_init1 with [ mk_pair id_init2 r ⇒
    406483      match id_init2 with [ mk_pair id init ⇒
    407       match g_st with [ mk_pair g st ⇒
    408         match alloc_init_data st init bsp with [ mk_pair st' b ⇒
    409           〈add_symbol ? id bsp b g, st'〉
    410         ] ] ] ] ])
    411     init vars.
    412 
    413 ndefinition globalenv_initmem : ∀F,V:Type. program F V → genv F × mem ≝
     484        do 〈g,st〉 ← g_st;
     485        match alloc_init_data st init r with [ mk_pair st' b ⇒
     486          let g' ≝ add_symbol ? id r b g in
     487          do st'' ← opt_to_res ? (store_init_data_list F g' st' r b OZ init);
     488            OK ? 〈g', st''〉
     489        ] ] ] ])
     490    (OK ? init_env) vars.
     491
     492ndefinition globalenv_initmem : ∀F,V:Type. program F V → res (genv F × mem) ≝
    414493λF,V,p.
    415494  add_globals F V
    416     〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
    417     (prog_vars ?? p).
    418 
    419 ndefinition globalenv_ : ∀F,V:Type. program F V → genv F ≝
     495   〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
     496   (prog_vars ?? p).
     497
     498ndefinition globalenv_ : ∀F,V:Type. program F V → res (genv F) ≝
    420499λF,V,p.
    421   \fst (globalenv_initmem F V p).
    422 ndefinition init_mem_ : ∀F,V:Type. program F V → mem ≝
     500  do 〈g,m〉 ← globalenv_initmem F V p;
     501    OK ? g.
     502ndefinition init_mem_ : ∀F,V:Type. program F V → res (mem) ≝
    423503λF,V,p.
    424   \snd (globalenv_initmem F V p).
     504  do 〈g,m〉 ← globalenv_initmem F V p;
     505    OK ? m.
     506
     507
     508
    425509
    426510ndefinition Genv : GENV ≝ mk_GENV
    … …  
    13041388End Genv.
    13051389*)
     1390

  • Deliverables/D3.1/C-semantics/Mem.ma

    r484 r485  
    719719  [ Vptr psp b ofs ⇒ store chunk m psp b (signed ofs) v
    720720  | _ ⇒ None ? ].
    721 
    722 
    723 (* Build a block filled with the given initialization data. *)
    724 ndefinition contents_init_data_step :
    725   Z → init_data → (Z → contentmap) → contentmap ≝
    726   λpos,data,reccall.
    727   match data with
    728   [ Init_int8 n ⇒
    729       setN 0 pos (Vint n) (reccall (pos + oneZ))
    730   | Init_int16 n ⇒
    731       setN 1 pos (Vint n) (reccall (pos + oneZ))
    732   | Init_int32 n ⇒
    733       setN 3 pos (Vint n) (reccall (pos + oneZ))
    734   | Init_float32 f ⇒
    735       setN 3 pos (Vfloat f) (reccall (pos + oneZ))
    736   | Init_float64 f ⇒
    737       setN 7 pos (Vfloat f) (reccall (pos + oneZ))
    738   | Init_space n ⇒ reccall (pos + Zmax n 0) (*??*)
    739   | Init_null r ⇒ setN (pred_size_pointer r) pos (Vnull r) (reccall (pos + oneZ))
    740   | Init_addrof s n ⇒
    741       (* Not handled properly yet *)
    742       reccall (pos + 4)
    743   | Init_pointer x ⇒
    744       (* Not handled properly yet *)
    745       reccall (pos + 4)].
    746 
    747 nlet rec contents_init_data (pos: Z) (i_data: list init_data) on i_data
    748   : contentmap ≝
    749   match i_data with
    750   [ nil ⇒ (λ_.Undef)
    751   | cons data i_data' ⇒
    752       contents_init_data_step pos data (λn.contents_init_data n i_data') ].
    753 
    754 ndefinition size_init_data : init_data → Z ≝
    755  λi_data.match i_data with
    756   [ Init_int8 _ ⇒ 1
    757   | Init_int16 _ ⇒ 2
    758   | Init_int32 _ ⇒ 4
    759   | Init_float32 _ ⇒ 4
    760   | Init_float64 _ ⇒ 8
    761   | Init_space n ⇒ Zmax n 0
    762   | Init_null r ⇒ size_pointer r
    763   | Init_addrof _ _ ⇒ 4
    764   | Init_pointer _ ⇒ Z_of_nat (*** can't use implicit coercion??? *)4].
    765 
    766 ndefinition size_init_data_list : list init_data → Z ≝
    767   λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.
    768 
    769 (* Nonessential properties that may require arithmetic
    770 nremark size_init_data_list_pos:
    771   ∀i_data. OZ ≤ size_init_data_list i_data.
    772 #i_data;nelim i_data;//;
    773 #a;#tl;ncut (OZ ≤ size_init_data a)
    774 ##[ncases a;nnormalize;//;
    775    #x;ncases x;nnormalize;//;
    776 ##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));
    777    ncut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
    778    ##[ncases (size_init_data a) in Hsize IH;
    779       ##[##1,2:/3/
    780       ##|nnormalize;#n;#Hfalse;nelim Hfalse]
    781    ##|#Hdisc;ncases Hdisc
    782       ##[#Heq;nrewrite > Heq;//;
    783       ##|#Heq;ncases Heq;#x;#Heq2;nrewrite > Heq2;
    784          (* TODO: arithmetics *) napply daemon]
    785    ##]
    786 ##]
    787 nqed.
    788 *)
    789 
    790 ndefinition block_init_data : list init_data → region → block_contents ≝
    791   λi_data,bcl.mk_block_contents
    792     OZ (size_init_data_list i_data) (contents_init_data OZ i_data) bcl.
    793 
    794 ndefinition alloc_init_data : mem → list init_data → region → mem × block ≝
    795   λm,i_data,bcl.
    796   〈mk_mem (update ? (nextblock m)
    797                  (block_init_data i_data bcl)
    798                  (blocks m))
    799          (Zsucc (nextblock m))
    800          (succ_nextblock_pos m),
    801    (nextblock m)〉.
    802 
    803 nremark block_init_data_empty:
    804   ∀bcl. block_init_data [ ] bcl = empty_block OZ OZ bcl.
    805 //;
    806 nqed.
    807721
    808722(* * Properties of the memory operations *)

  • Deliverables/D3.1/C-semantics/test/insertsort.c

    r479 r485  
    44};
    55
    6 /* Init_addrof not yet supported
    76__pdata struct list l6 = {69, 0};
    87__pdata struct list l5 = {36, &l6};
    … …  
    1211__pdata struct list l1 = {240, &l2};
    1312__pdata struct list l0 = {102, &l1};
    14 */
    15 __pdata struct list l6 = {69, 0};
    16 __pdata struct list l5 = {36, 0};
    17 __pdata struct list l4 = {136, 0};
    18 __pdata struct list l3 = {105, 0};
    19 __pdata struct list l2 = {234, 0};
    20 __pdata struct list l1 = {240, 0};
    21 __pdata struct list l0 = {102, 0};
    2213
    2314void insert(__pdata struct list *element, __pdata struct list **dest) {
    … …  
    4637  __pdata struct list *l = &l0;
    4738
    48   /* Init_addrof not yet supported */
    49   l0.next = &l1;
    50   l1.next = &l2;
    51   l2.next = &l3;
    52   l3.next = &l4;
    53   l4.next = &l5;
    54   l5.next = &l6;
    55 
    5639  sort(&l);
    5740  while (l) {
Note: See TracChangeset for help on using the changeset viewer.