Changeset 5


Ignore:
Timestamp:
Jun 8, 2010, 3:25:47 PM (7 years ago)
Author:
campbell
Message:

Add a few execution steps and calculation of the initial state to the
"executable" C semantics.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Cexec.ma

    r4 r5  
    273273#A B P e f; nelim e; nnormalize; /2/; nqed.
    274274
     275nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop.
     276  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) →
     277  match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ].
     278#A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
     279##[ #H; napply (False_ind … H);
     280##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
     281##] nqed.
     282
    275283(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
    276284   a structurally smaller value, we break out the surrounding Expr constructor
     
    324332##| napply opt_bind_OK; #l el; napply eval_Evar_local; //
    325333##] nqed.
     334
     335(* Don't really want to use subset rather than sigma here, but can't be bothered
     336   with *another* set of coercions. XXX: why do I have to get the recursive
     337   call's property manually? *)
     338
     339nlet rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : { r:env × mem | alloc_variables en m l (\fst r) (\snd r) } ≝
     340match l with
     341[ nil ⇒ Some ? 〈en, m〉
     342| cons h vars ⇒
     343  match h with [ mk_pair id ty ⇒
     344    match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒
     345      match exec_alloc_variables (set ? PTree ? id b1 en) m1 vars with
     346      [ sig_intro r p ⇒ r ]
     347]]]. nwhd; //;
     348nelim (exec_alloc_variables (set ident PTree block c3 c7 en) c6 c1);
     349#H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
     350napply (alloc_variables_cons … IH); /2/;
     351nqed.
     352
     353(* TODO: can we establish that length params = length vs in advance? *)
     354nlet rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res (Σm2:mem. bind_parameters e m params vs m2) ≝
     355  match params with
     356  [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ]
     357  | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒
     358      match vs with
     359      [ nil ⇒ Some ? (Error ?)
     360      | cons v1 vl ⇒ Some ? (
     361          b ← opt_to_res ? (get ? PTree ? id e);:
     362          m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:
     363          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
     364      ]
     365  ] ].
     366nwhd; //;
     367napply opt_bind_OK; #b eb;
     368napply opt_bind_OK; #m1 em1;
     369napply reinject; #m2 em2 Hm2;
     370napply (bind_parameters_cons … eb em1 Hm2);
     371nqed.
     372
     373ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝
     374λt. match t with
     375[ Tvoid ⇒ Some ? (Error ?)
     376| _ ⇒ Some ? (OK ??)
     377]. nwhd; //; @; #H; ndestruct; nqed.
     378
     379nlet rec exec_step (ge:genv) (st:state) on st : res (Σr:trace × state. step ge st (\fst r) (\snd r)) ≝
     380match st with
     381[ State f s k e m ⇒
     382  match s with
     383  [ Sassign a1 a2 ⇒ Some ? (
     384    〈loc, ofs〉 ← exec_lvalue ge e m a1;:
     385    v2 ← exec_expr ge e m a2;:
     386    m' ← opt_to_res ? (store_value_of_type (typeof a1) m loc ofs v2);:
     387    OK ? 〈E0, State f Sskip k e m'〉)
     388  | Sreturn a_opt ⇒
     389    match a_opt with
     390    [ None ⇒ match fn_return f with
     391      [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
     392      | _ ⇒ Some ? (Error ?)
     393      ]
     394    | Some a ⇒ Some ? (
     395        u ← is_not_void (fn_return f);:
     396        v ← exec_expr ge e m a;:
     397        OK ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
     398    ]
     399  | _ ⇒ Some ? (Error ?)
     400  ]
     401| Callstate f0 vargs k m ⇒
     402  match f0 with
     403  [ Internal f ⇒ Some ? (
     404    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
     405      m2 ← exec_bind_parameters e m1 (fn_params f) vargs;:
     406      OK ? 〈E0, State f (fn_body f) k e m2〉
     407    ])
     408  | _ ⇒ Some ? (Error ?)
     409  ]
     410| _ ⇒ Some ? (Error ?)
     411]. nwhd; //;
     412##[ napply sig_bind2_OK; #loc ofs Hlval;
     413    napply sig_bind_OK; #v2 ev2 Hv2;
     414    napply opt_bind_OK; #m' em';
     415    nwhd; napply (step_assign … Hlval Hv2 em');
     416##| napply step_return_0; napply c9;
     417##| napply sig_bind_OK; #u eu Hnotvoid;
     418    napply sig_bind_OK; #v ev Hv;
     419    nwhd; napply (step_return_1 … Hnotvoid Hv);
     420##| napply extract_subset_pair; #e m1 ealloc Halloc;
     421    napply sig_bind_OK; #m2 em1 Hbind;
     422    nwhd; napply (step_internal_function … Halloc Hbind);
     423##]
     424nqed.
     425
     426nlet rec make_initial_state (p:program) : res (Σs:state. initial_state p s) ≝
     427  let ge ≝ globalenv Genv ?? p in
     428  let m0 ≝ init_mem Genv ?? p in
     429  Some ? (
     430    b ← opt_to_res ? (find_symbol Genv ? ge (prog_main ?? p));:
     431    f ← opt_to_res ? (find_funct_ptr Genv ? ge b);:
     432    OK ? (Callstate f (nil ?) Kstop m0)).
     433nwhd;
     434napply opt_bind_OK; #b eb;
     435napply opt_bind_OK; #f ef;
     436nwhd; napply (initial_state_intro … eb ef);
     437nqed.
  • C-semantics/README

    r3 r5  
    3030  difficult if we keep using a unary representation of integers as
    3131  formalisation involves constants like 2^32.
     32
     33* Some experimental work on an executable semantics has been started in
     34  Cexec.ma.  At present only a small subset of expressions and statements
     35  are handled.
    3236
    3337matita issues and workarounds
Note: See TracChangeset for help on using the changeset viewer.