Changeset 17 for C-semantics


Ignore:
Timestamp:
Jul 26, 2010, 7:04:30 PM (10 years ago)
Author:
campbell
Message:

Remainder of the statements for the executable semantics (except for
"external" function calls, which can do I/O).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Cexec.ma

    r16 r17  
    600600]. nwhd; //; @; #H; nelim H; nqed.
    601601
     602nlet rec is_Sskip (s:statement) : (s = Sskip) + (s ≠ Sskip) ≝
     603match s with
     604[ Sskip ⇒ dy
     605| _ ⇒ dn
     606].
     607##[ //;
     608##| ##*: @; #H; ndestruct;
     609##] nqed.
     610
    602611nlet rec exec_step (ge:genv) (st:state) on st : res (Σr:trace × state. step ge st (\fst r) (\snd r)) ≝
    603612match st with
     
    635644          | _ ⇒ Some ? (Error ?)
    636645          ]
    637       | _ ⇒ Some ? (Error ?) (* TODO more *)
     646      | Kwhile a s' k' ⇒ Some ? (OK ? 〈E0, State f (Swhile a s') k' e m〉)
     647      | Kdowhile a s' k' ⇒ Some ? (
     648          v ← exec_expr ge e m a;:
     649          b ← bool_of_val_3 v (typeof a);:
     650          match b with
     651          [ true ⇒ OK ? 〈E0, State f (Sdowhile a s') k' e m〉
     652          | false ⇒ OK ? 〈E0, State f Sskip k' e m〉
     653          ])
     654      | Kfor2 a2 a3 s' k' ⇒ Some ? (OK ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
     655      | Kfor3 a2 a3 s' k' ⇒ Some ? (OK ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉)
     656      | Kswitch k' ⇒ Some ? (OK ? 〈E0, State f Sskip k' e m〉)
     657      | _ ⇒ Some ? (Error ?)
     658      ]
     659  | Scontinue ⇒
     660      match k with
     661      [ Kseq s' k' ⇒ Some ? (OK ? 〈E0, State f Scontinue k' e m〉)
     662      | Kwhile a s' k' ⇒ Some ? (OK ? 〈E0, State f (Swhile a s') k' e m〉)
     663      | Kdowhile a s' k' ⇒ Some ? (
     664          v ← exec_expr ge e m a;:
     665          b ← bool_of_val_3 v (typeof a);:
     666          match b with
     667          [ true ⇒ OK ? 〈E0, State f (Sdowhile a s') k' e m〉
     668          | false ⇒ OK ? 〈E0, State f Sskip k' e m〉
     669          ])
     670      | Kfor2 a2 a3 s' k' ⇒ Some ? (OK ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
     671      | Kswitch k' ⇒ Some ? (OK ? 〈E0, State f Scontinue k' e m〉)
     672      | _ ⇒ Some ? (Error ?)
     673      ]
     674  | Sbreak ⇒
     675      match k with
     676      [ Kseq s' k' ⇒ Some ? (OK ? 〈E0, State f Sbreak k' e m〉)
     677      | Kwhile a s' k' ⇒ Some ? (OK ? 〈E0, State f Sskip k' e m〉)
     678      | Kdowhile a s' k' ⇒ Some ? (OK ? 〈E0, State f Sskip k' e m〉)
     679      | Kfor2 a2 a3 s' k' ⇒ Some ? (OK ? 〈E0, State f Sskip k' e m〉)
     680      | Kswitch k' ⇒ Some ? (OK ? 〈E0, State f Sskip k' e m〉)
     681      | _ ⇒ Some ? (Error ?)
     682      ]
     683  | Sifthenelse a s1 s2 ⇒ Some ? (
     684      v ← exec_expr ge e m a;:
     685      b ← bool_of_val_3 v (typeof a);:
     686      OK ? 〈E0, State f (if b then s1 else s2) k e m〉)
     687  | Swhile a s' ⇒ Some ? (
     688      v ← exec_expr ge e m a;:
     689      b ← bool_of_val_3 v (typeof a);:
     690      OK ? 〈E0, if b then State f s' (Kwhile a s' k) e m
     691                     else State f Sskip k e m〉)
     692  | Sdowhile a s' ⇒ Some ? (OK ? 〈E0, State f s' (Kdowhile a s' k) e m〉)
     693  | Sfor a1 a2 a3 s' ⇒
     694      match is_Sskip a1 with
     695      [ inl _ ⇒ Some ? (
     696          v ← exec_expr ge e m a2;:
     697          b ← bool_of_val_3 v (typeof a2);:
     698          OK ? 〈E0, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
     699      | inr _ ⇒ Some ? (OK ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉)
    638700      ]
    639701  | Sreturn a_opt ⇒
     
    648710        OK ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
    649711    ]
    650   | _ ⇒ Some ? (Error ?)
     712  | Sswitch a sl ⇒ Some ? (
     713      v ← exec_expr ge e m a;:
     714      match v with [ Vint n ⇒ OK ? 〈E0, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
     715                   | _ ⇒ Error ? ])
     716  | Slabel lbl s' ⇒ Some ? (OK ? 〈E0, State f s' k e m〉)
     717  | Sgoto lbl ⇒
     718      match find_label lbl (fn_body f) (call_cont k) with
     719      [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (OK ? 〈E0, State f s' k' e m〉) ]
     720      | None ⇒ Some ? (Error ?)
     721      ]
    651722  ]
    652723| Callstate f0 vargs k m ⇒
     
    680751]. nwhd; //;
    681752##[ nrewrite > c7; napply step_skip_call; //; napply c8;
     753##| napply step_skip_or_continue_while; @; //;
     754##| napply sig_bind_OK; #v ev Hv;
     755    napply sig_bind_OK; #b; ncases b; #eb Hb;
     756    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
     757      ##[ @; // ##| napply (bool_of … Hb); ##]
     758    ##| napply (step_skip_or_continue_dowhile_false … Hv);
     759      ##[ @; // ##| napply (bool_of … Hb); ##]
     760    ##]
     761##| napply step_skip_or_continue_for2; @; //;
     762##| napply step_skip_break_switch; @; //;
    682763##| nrewrite > c11; napply step_skip_call; //; napply c12;
    683764##| napply sig_bind2_OK; #loc ofs Hlval;
     
    695776        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
    696777    ##]
     778##| napply sig_bind_OK; #v ev Hv;
     779    napply sig_bind_OK; #b; ncases b; #eb Hb;
     780    ##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb);
     781    ##| napply (step_ifthenelse_false … Hv); napply (bool_of … Hb)
     782    ##]
     783##| napply sig_bind_OK; #v ev Hv;
     784    napply sig_bind_OK; #b; ncases b; #eb Hb;
     785    ##[ napply (step_while_true … Hv); napply (bool_of … Hb);
     786    ##| napply (step_while_false … Hv); napply (bool_of … Hb);
     787    ##]
     788##| nrewrite > c11;
     789    napply sig_bind_OK; #v ev Hv;
     790    napply sig_bind_OK; #b; ncases b; #eb Hb;
     791    ##[ napply (step_for_true … Hv); napply (bool_of … Hb);
     792    ##| napply (step_for_false … Hv); napply (bool_of … Hb);
     793    ##]
     794##| napply step_for_start; //;
     795##| napply step_skip_break_switch; @2; //;
     796##| napply step_skip_or_continue_while; @2; //;
     797##| napply sig_bind_OK; #v ev Hv;
     798    napply sig_bind_OK; #b; ncases b; #eb Hb;
     799    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
     800      ##[ @2; // ##| napply (bool_of … Hb); ##]
     801    ##| napply (step_skip_or_continue_dowhile_false … Hv);
     802      ##[ @2; // ##| napply (bool_of … Hb); ##]
     803    ##]
     804##| napply step_skip_or_continue_for2; @2; //
    697805##| napply step_return_0; napply c9;
    698806##| napply sig_bind_OK; #u eu Hnotvoid;
    699807    napply sig_bind_OK; #v ev Hv;
    700808    nwhd; napply (step_return_1 … Hnotvoid Hv);
     809##| napply sig_bind_OK; #v; ncases v; //; #n ev Hv;
     810    napply step_switch; //;
     811##| napply step_goto; nrewrite < c12; napply c9;
    701812##| napply extract_subset_pair; #e m1 ealloc Halloc;
    702813    napply sig_bind_OK; #m2 em1 Hbind;
Note: See TracChangeset for help on using the changeset viewer.