Changeset 16


Ignore:
Timestamp:
Jul 26, 2010, 5:19:31 PM (10 years ago)
Author:
campbell
Message:

Add rest of the expressions to executable Clight semantics.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Cexec.ma

    r13 r16  
    285285##] nqed.
    286286
     287nlet rec is_neutral_cast (ty:type) : res (Σu:unit.neutral_for_cast ty) ≝
     288match ty with
     289[ Tint sz _ ⇒ match sz with [ I32 ⇒ Some ? (OK ? something) | _ ⇒ Some ? (Error ?) ]
     290| Tpointer _ ⇒ Some ? (OK ? something)
     291| Tarray _ _ ⇒ Some ? (OK ? something)
     292| Tfunction _ _ ⇒ Some ? (OK ? something)
     293| _ ⇒ Some ? (Error ?)
     294]. nwhd; //; nqed.
     295(*
     296nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B.
     297#A B e; ncases e; //; nqed.
     298*)
     299
     300nlet rec exec_cast (v:val) (ty:type) (ty':type) : res (Σv':val. cast v ty ty' v') ≝
     301match v with
     302[ Vint i ⇒
     303  match ty with
     304  [ Tint sz1 si1 ⇒
     305    match ty' with
     306    [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i)))
     307    | Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))))
     308    (* no change in data repr *)
     309    | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
     310    ]
     311  | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
     312  ]
     313| Vfloat f ⇒
     314  match ty with
     315  [ Tfloat sz ⇒
     316    match ty' with
     317    [ Tint sz' si' ⇒ Some ? (OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f))))
     318    | Tfloat sz' ⇒ Some ? (OK ? (Vfloat (cast_float_float sz' f)))
     319    | _ ⇒ Some ? (Error ?)
     320    ]
     321  | _ ⇒ Some ? (Error ?)
     322  ]
     323| Vptr b ofs ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vptr b ofs))
     324| _ ⇒ Some ? (Error ?)
     325]. ndestruct; /2/;
     326##[ ##1,2,3: ncases c2; //; napply cast_nn_i; //
     327##| ##4,5,6: napply sig_bind_OK; #u;#_;#H; napply cast_nn_i; //;
     328##| napply sig_bind_OK; #u;#_;#H; napply sig_bind_OK; #u';#_;#H';
     329    napply cast_nn_p; //
     330##] nqed.
     331
    287332(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
    288333   a structurally smaller value, we break out the surrounding Expr constructor
     
    299344      opt_to_res ? (load_value_of_type ty m loc ofs))
    300345  | Ederef _ ⇒ Some ? (
     346      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
     347      opt_to_res ? (load_value_of_type ty m loc ofs))
     348  | Efield _ _ ⇒ Some ? (
    301349      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
    302350      opt_to_res ? (load_value_of_type ty m loc ofs))
     
    317365      match b return λ_.res val with [ true ⇒ (exec_expr ge en m a2) | false ⇒ (exec_expr ge en m a3) ])
    318366(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
    319   | _ ⇒ Some ? (Error ?)
     367  | Eorbool a1 a2 ⇒ Some ? (
     368      v1 ← exec_expr ge en m a1;:
     369      b1 ← bool_of_val_3 v1 (typeof a1);:
     370      match b1 return λ_.res val with [ true ⇒ OK ? Vtrue | false ⇒
     371        v2 ← exec_expr ge en m a2;:
     372        b2 ← bool_of_val_3 v2 (typeof a2);:
     373        OK ? (of_bool b2) ])
     374  | Eandbool a1 a2 ⇒ Some ? (
     375      v1 ← exec_expr ge en m a1;:
     376      b1 ← bool_of_val_3 v1 (typeof a1);:
     377      match b1 return λ_.res val with [ true ⇒
     378        v2 ← exec_expr ge en m a2;:
     379        b2 ← bool_of_val_3 v2 (typeof a2);:
     380        OK ? (of_bool b2)
     381      | false ⇒ OK ? Vfalse ])
     382  | Ecast ty' a ⇒ Some ? (
     383      v ← exec_expr ge en m a;:
     384      exec_cast v (typeof a) ty')
    320385  ]
    321386]
     
    333398      | _ ⇒ Error ?
    334399      ])
     400  | Efield a i ⇒
     401      match (typeof a) with
     402      [ Tstruct id fList ⇒ Some ? (
     403          〈l,ofs〉 ← exec_lvalue ge en m a;:
     404          delta ← field_offset i fList;:
     405          OK ? 〈l,add ofs (repr delta)〉)
     406      | Tunion id fList ⇒ Some ? (
     407          〈l,ofs〉 ← exec_lvalue ge en m a;:
     408          OK ? 〈l,ofs〉)
     409      | _ ⇒ Some ? (Error ?)
     410      ]
    335411  | _ ⇒ Some ? (Error ?)
    336412  ]
     
    351427    napply opt_OK; #v ev;
    352428    napply (eval_Ebinop … Hv1 Hv2 ev);
     429##| napply sig_bind_OK; #v ev Hv;
     430    napply sig_bind_OK; #v' ev' Hv';
     431    napply (eval_Ecast … Hv Hv');
    353432##| napply sig_bind_OK; #vb evb Hvb;
    354433    napply sig_bind_OK; #b;
     
    357436    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    358437    ##]
     438##| napply sig_bind_OK; #v1 ev1 Hv1;
     439    napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
     440    ##[ napply sig_bind_OK; #v2 ev2 Hv2;
     441        napply sig_bind_OK; #b2 eb2 Hb2;
     442        napply (eval_Eandbool_2 … Hv1 … Hv2);
     443        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
     444    ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
     445    ##]
     446##| napply sig_bind_OK; #v1 ev1 Hv1;
     447    napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
     448    ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
     449    ##| napply sig_bind_OK; #v2 ev2 Hv2;
     450        napply sig_bind_OK; #b2 eb2 Hb2;
     451        napply (eval_Eorbool_2 … Hv1 … Hv2);
     452        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
     453    ##]
     454##| napply sig_bind2_OK; nrewrite > c5; #l ofs H;
     455    napply opt_OK; #v ev; /2/;
    359456##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/;
    360457##| napply eval_Evar_local; /2/
    361458##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
    362459    napply eval_Ederef; //
    363 
     460##| napply sig_bind2_OK; #l ofs H;
     461    napply bind_OK; #delta Hdelta;
     462    napply (eval_Efield_struct … H c5 Hdelta);
     463##| napply sig_bind2_OK; #l ofs H;
     464    napply (eval_Efield_union … H c5);
    364465##] nqed.
    365466
  • C-semantics/extralib.ma

    r15 r16  
    3131nlemma eq_rect_Type2_r:
    3232 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
     33 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
     34nqed.
     35
     36nlemma eq_rect_CProp0_r:
     37 ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
    3338 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
    3439nqed.
Note: See TracChangeset for help on using the changeset viewer.