Changeset 2588 for src/Clight/Cexec.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/Cexec.ma

    r2560 r2588  
    1919    | _ ⇒ Error ? (msg TypeMismatch)
    2020    ]
    21 (*  | Vfloat f ⇒ match ty with
    22     [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero)
    23     | _ ⇒ Error ? (msg TypeMismatch)
    24     ]*)
    2521  | Vptr _ ⇒ match ty with
    2622    [ Tpointer _ ⇒ OK ? true
     
    3834  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
    3935  | #ptr #ty %{ true} % //
    40 (*  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //; *)
    4136  | * #sg %{ false} % //
    4237  | #t %{ false} % //;
    43 (*  | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;*)
    4438  ]
    4539qed.
     
    215209      do 〈v1,tr1〉 ← exec_expr ge en m a1;
    216210      do 〈v2,tr2〉 ← exec_expr ge en m a2;
    217       do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
     211      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m ty);
    218212      OK ? 〈v,tr1⧺tr2〉
    219213  | Econdition a1 a2 a3 ⇒
     
    228222      do 〈v1,tr1〉 ← exec_expr ge en m a1;
    229223      do b1 ← exec_bool_of_val v1 (typeof a1);
    230       match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
     224      match b1 return λ_.res (val×trace) with
     225      [ true ⇒
     226        match cast_bool_to_target ty (Some ? Vtrue) with
     227        [ None ⇒
     228          Error ? (msg BadlyTypedTerm)
     229        | Some vtr ⇒
     230          OK ? 〈vtr,tr1〉 ]
     231      | false ⇒
    231232        do 〈v2,tr2〉 ← exec_expr ge en m a2;
    232233        do b2 ← exec_bool_of_val v2 (typeof a2);
    233         OK ? 〈of_bool b2, tr1⧺tr2〉 ]
     234        match cast_bool_to_target ty (Some ? (of_bool b2)) with
     235        [ None ⇒
     236          Error ? (msg BadlyTypedTerm)
     237        | Some v2 ⇒
     238          OK ? 〈v2,tr1⧺tr2〉 ] ]
    234239  | Eandbool a1 a2 ⇒
    235240      do 〈v1,tr1〉 ← exec_expr ge en m a1;
    236241      do b1 ← exec_bool_of_val v1 (typeof a1);
    237       match b1 return λ_.res (val×trace) with [ true ⇒
     242      match b1 return λ_.res (val×trace) with
     243      [ true ⇒
    238244        do 〈v2,tr2〉 ← exec_expr ge en m a2;
    239245        do b2 ← exec_bool_of_val v2 (typeof a2);
    240         OK ? 〈of_bool b2, tr1⧺tr2〉
    241       | false ⇒ OK ? 〈Vfalse,tr1〉 ]
     246        match cast_bool_to_target ty (Some ? (of_bool b2)) with
     247        [ None ⇒
     248          Error ? (msg BadlyTypedTerm)
     249        | Some v2 ⇒
     250          OK ? 〈v2, tr1⧺tr2〉
     251        ]
     252      | false ⇒
     253        match cast_bool_to_target ty (Some ? Vfalse) with
     254        [ None ⇒
     255          Error ? (msg BadlyTypedTerm)
     256        | Some vfls ⇒
     257          OK ? 〈vfls,tr1〉 ]
     258      ]
    242259  | Ecast ty' a ⇒
    243260      do 〈v,tr〉 ← exec_expr ge en m a;
     
    267284          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
    268285          do delta ← field_offset i fList;
    269           OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I32 delta)〉,tr〉
     286          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I16 delta)〉,tr〉
    270287      | Tunion id fList ⇒
    271288          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
Note: See TracChangeset for help on using the changeset viewer.