Changeset 3178 for src/Clight/Csyntax.ma


Ignore:
Timestamp:
Apr 25, 2013, 6:03:24 PM (6 years ago)
Author:
campbell
Message:

Some progress on Callstate steps in Clight to Cminor.
Note that some bogus alignment has been removed in Csyntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r2645 r3178  
    346346
    347347(* * Natural alignment of a type, in bytes. *)
    348 let rec alignof (t: type) : nat ≝ (*1*)
    349 (* these are old values for 32 bit machines *)
     348let rec alignof (t: type) : nat ≝ 1.
     349(* these are old values for 32 bit machines
    350350  match t with
    351351  [ Tvoid ⇒ 1
     
    363363  [ Fnil ⇒ 1
    364364  | Fcons id t f' ⇒ max (alignof t) (alignof_fields f')
    365   ].
     365  ].*)
    366366
    367367(*
     
    412412                        (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs f')
    413413  ].
    414 
     414(*
    415415lemma alignof_fields_pos:
    416416  ∀f. alignof_fields f > 0.
    417417@fieldlist_ind //;
    418418#i #t #fs' #IH @max_r @IH qed.
    419 
     419*)
    420420lemma alignof_pos:
    421421  ∀t. alignof t > 0.
    422 #t elim t; normalize; //;
     422#t elim t; normalize; //;(*
    423423[ 1,2: #z cases z; /2/;
    424424| 3,4: #i @alignof_fields_pos
    425 ] qed.
     425]*) qed.
    426426
    427427(* * Size of a type, in bytes. *)
     
    450450  | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld')
    451451  ].
    452 (* TODO: needs some Z_times results
     452
    453453lemma sizeof_pos:
    454454  ∀t. sizeof t > 0.
    455 #t0
    456 napply (type_ind2 (λt. sizeof t > 0)
    457                   (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0));
    458 [ 1,4,6,9: //;
    459 | #i cases i;#s //;
    460 | #f cases f;//
    461 | #t #n #H whd in ⊢ (?%?);
    462 Proof.
    463   intro t0.
    464   apply (type_ind2 (fun t => sizeof t > 0)
    465                    (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
    466   intros; simpl; auto; try omega.
    467   destruct i; omega.
    468   destruct f; omega.
    469   apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
    470   destruct H.
    471   generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)).
    472   generalize (Zmax1 1 (sizeof_struct f 0)). omega.
    473   generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)).
    474   generalize (Zmax1 1 (sizeof_union f)). omega.
    475   split. omega. auto.
    476   destruct H0. split; intros.
    477   generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
    478   apply H1.
    479   generalize (align_le pos (alignof t) (alignof_pos t)). omega.
    480 Qed.
    481 
     455#t elim t //
     456[ * //
     457| #t' * [ /2/ | #n #H change with (0 < ?) whd in ⊢ (??%); change with (0*0) in ⊢ (?%?); @lt_times // ]
     458| #i #fl whd in ⊢ (?%?); whd in match (alignof ?); <times_n_1
     459  >commutative_plus cases (sizeof_struct ??) [2:#x] whd in ⊢ (?(?%?)?);
     460  //
     461| #i #fl whd in ⊢ (?%?); whd in match (alignof ?); <times_n_1
     462  >commutative_plus cases (sizeof_union ?) [2:#x] whd in ⊢ (?(?%?)?);
     463  //
     464] qed.
     465
     466(*
    482467Lemma sizeof_struct_incr:
    483468  forall fld pos, pos <= sizeof_struct fld pos.
Note: See TracChangeset for help on using the changeset viewer.