Changeset 2588 for src/Clight/label.ma


Ignore:
Timestamp:
Jan 23, 2013, 2:38:06 PM (7 years ago)
Author:
garnier
Message:

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2505 r2588  
    7979  〈Expr (Ecost l e) (typeof e), gen〉.
    8080
    81 definition const_int : nat → expr ≝
    82 λn. Expr (Econst_int ? (repr I32 n)) (Tint I32 Signed).
     81definition const_int : intsize → nat → expr ≝
     82λsz,n. Expr (Econst_int ? (repr sz n)) (Tint sz Signed).
    8383
    8484let rec label_expr (e:expr) (costgen:universe CostTag)
     
    119119| Eandbool e1 e2 ⇒
    120120    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
     121    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
     122    match ty with
     123    [ Tint sz sg ⇒
     124      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
     125      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
     126      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
     127      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
     128      〈Econdition e1 e2 ef, costgen〉
     129    | _ ⇒ (* default on 32 bit consts if inconsistent type. *)
     130      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
     131      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
     132      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
     133      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
     134      〈Econdition e1 e2 ef, costgen〉       
     135    ]
     136| Eorbool e1 e2 ⇒
     137    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
    121138    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    122     let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    123     let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
    124     let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
    125     let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
    126     〈Econdition e1 e2 ef, costgen〉
    127 | Eorbool e1 e2 ⇒
    128     let 〈e1,costgen〉 ≝ label_expr e1 costgen in
    129     let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    130     let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    131     let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
    132     let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
    133     let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    134     〈Econdition e1 et e2, costgen〉
    135 
     139    match ty with
     140    [ Tint sz sg ⇒   
     141      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
     142      let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in
     143      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
     144      let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in
     145      〈Econdition e1 et e2, costgen〉
     146    | _ ⇒
     147      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
     148      let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in
     149      let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
     150      let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in
     151      〈Econdition e1 et e2, costgen〉
     152    ]
    136153| Efield e' id ⇒
    137154    let 〈e',costgen〉 ≝ label_expr e' costgen in
Note: See TracChangeset for help on using the changeset viewer.