Changeset 9 for C-semantics/Cexec.ma


Ignore:
Timestamp:
Jun 21, 2010, 4:22:09 PM (10 years ago)
Author:
campbell
Message:

Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Cexec.ma

    r5 r9  
    128128  ##| #b i t0; @ true; @; //
    129129  ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
    130   ##| #i s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
    131   ##| #t; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
     130  ##| #i s; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)
     131  ##| #t; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)
    132132  ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
    133133  ##]
     
    213213  ##| #b i t0; @ true; @; //
    214214  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
    215   ##| #i s; @ false; @; //; nwhd; nrewrite > (eq_true …); //;
    216   ##| #t; @ false; @; //; nwhd; nrewrite > (eq_true …); //;
     215  ##| #i s; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
     216  ##| #t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
    217217  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
    218218  ##]
     
    220220
    221221(* Prove a few minor results to make proof obligations easy. *)
     222
     223nlemma bind_assoc_r: ∀A,B,C,e,f,g.
     224  bind B C (bind A B e f) g = bind A C e (λx.bind B C (f x) g).
     225#A B C e f g; ncases e; nnormalize; //; nqed.
    222226
    223227nlemma bind_OK: ∀A,B,P,e,f.
     
    290294  match e' with
    291295  [ Econst_int i ⇒ Some ? (OK ? (Vint i))
     296  | Econst_float f ⇒ Some ? (OK ? (Vfloat f))
    292297  | Evar _ ⇒ Some ? (
     298      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
     299      opt_to_res ? (load_value_of_type ty m loc ofs))
     300  | Ederef _ ⇒ Some ? (
    293301      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
    294302      opt_to_res ? (load_value_of_type ty m loc ofs))
     
    296304      〈loc, ofs〉 ← exec_lvalue ge en m a;:
    297305      OK ? (Vptr loc ofs))
     306  | Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty'))))
    298307  | Eunop op a ⇒ Some ? (
    299308      v1 ← exec_expr ge en m a;:
    300309      opt_to_res ? (sem_unary_operation op v1 (typeof a)))
     310  | Ebinop op a1 a2 ⇒ Some ? (
     311      v1 ← exec_expr ge en m a1;:
     312      v2 ← exec_expr ge en m a2;:
     313      opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m))
    301314  | Econdition a1 a2 a3 ⇒ Some ? (
    302315      v ← exec_expr ge en m a1;:
     
    312325      l ← opt_to_res ? (get ? PTree ? id en);:
    313326      OK ? 〈l, zero〉)
     327  | Ederef a ⇒ Some ? (
     328      v ← exec_expr ge en m a;:
     329      match v with
     330      [ Vptr l ofs ⇒ OK ? 〈l,ofs〉
     331      | _ ⇒ Error ?
     332      ])
    314333  | _ ⇒ Some ? (Error ?)
    315334  ]
     
    319338##[ napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
    320339    napply opt_OK;  #v ev; /2/;
     340##| napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
     341    napply opt_OK;  #v ev; /2/;
    321342##| napply sig_bind2_OK; #loc ofs H;
    322343    nwhd; napply eval_Eaddrof; //;
     
    324345    napply opt_OK; #v ev;
    325346    napply (eval_Eunop … Hv1 ev);
     347##| napply sig_bind_OK; #v1 ev1 Hv1;
     348    napply sig_bind_OK; #v2 ev2 Hv2;
     349    napply opt_OK; #v ev;
     350    napply (eval_Ebinop … Hv1 Hv2 ev);
    326351##| napply sig_bind_OK; #vb evb Hvb;
    327352    napply sig_bind_OK; #b;
     
    330355    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    331356    ##]
    332 ##| napply opt_bind_OK; #l el; napply eval_Evar_local; //
     357##| napply opt_bind_OK; #l el; napply eval_Evar_local; //
     358##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
     359    napply eval_Ederef; //
     360
    333361##] nqed.
     362
     363(* TODO: Can we do this sensibly with a map combinator? *)
     364nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (Σvl:list val. eval_exprlist ge e m l vl) ≝
     365match l with
     366[ nil ⇒ Some ? (OK ? (nil val))
     367| cons e1 es ⇒ Some ? (
     368  v ← exec_expr ge e m e1;:
     369  vs ← exec_exprlist ge e m es;:
     370  OK ? (cons val v vs))
     371]. nwhd; //;
     372napply sig_bind_OK; #v ev Hv;
     373napply sig_bind_OK; #vs evs Hvs;
     374nnormalize; /2/;
     375nqed.
    334376
    335377(* Don't really want to use subset rather than sigma here, but can't be bothered
     
    377419]. nwhd; //; @; #H; ndestruct; nqed.
    378420
     421ninductive decide : Type ≝
     422| dy : decide | dn : decide.
     423
     424ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P.
     425#P d;ncases d;/2/; nqed.
     426
     427ncoercion decide_inject :
     428  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P ≝ dodecide
     429  on d:decide to ? + (¬?).
     430
     431alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
     432alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
     433ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
     434#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
     435ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
     436#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
     437ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
     438#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
     439
     440(* Not very happy about this. *)
     441nlet rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
     442match t1 with
     443[ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ]
     444| Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
     445| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
     446| Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
     447| Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒
     448    match type_eq_dec t t' with [ inl _ ⇒
     449      match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]
     450| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match typelist_eq_dec tl tl' with [ inl _ ⇒
     451    match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]
     452| Tstruct i fl ⇒
     453    match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
     454      match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
     455| Tunion i fl ⇒
     456    match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
     457      match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
     458| Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
     459]
     460and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
     461match tl1 with
     462[ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ]
     463| Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒
     464    match type_eq_dec t1 t2 with [ inl _ ⇒
     465      match typelist_eq_dec ts1 ts2 with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
     466]
     467and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
     468match fl1 with
     469[ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ]
     470| Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒
     471    match ident_eq i1 i2 with [ inl _ ⇒
     472      match type_eq_dec t1 t2 with [ inl _ ⇒
     473        match fieldlist_eq_dec fs1 fs2 with [ inl _ ⇒ dy | _ ⇒ dn ]
     474        | _ ⇒ dn ] | _ ⇒ dn ] ]
     475].
     476(* A poor man's clear, otherwise automation picks up recursive calls without
     477   checking that the argument is smaller. *)
     478ngeneralize in type_eq_dec;
     479ngeneralize in typelist_eq_dec;
     480ngeneralize in fieldlist_eq_dec; #avoid1 avoid2 avoid3 avoid4 avoid5 avoid6;
     481ndestruct; //; @; #H; ndestruct;
     482##[ nelim c8; /2/
     483##| nelim c6; /2/
     484##| nelim c4; /2/
     485##| nelim c4; /2/
     486##| nelim c8; /2/
     487##| nelim c6; /2/
     488##| nelim c8; /2/
     489##| nelim c6; /2/
     490##| nelim c8; /2/
     491##| nelim c6; /2/
     492##| nelim c8; /2/
     493##| nelim c6; /2/
     494##| nelim c4; /2/
     495##| nelim c8; /2/
     496##| nelim c6; /2/
     497##| nelim c12; /2/
     498##| nelim c10; /2/
     499##| nelim c8; /2/
     500##] nqed.
     501
     502ndefinition are_equal : ∀A:Type. (∀x,y:A.(x=y)+(x≠y)) → ∀x,y:A. res (x=y) ≝
     503λA,dec,x,y.
     504match dec … x y with
     505[ inl p ⇒ OK ? p
     506| inr _ ⇒ Error ?
     507].
     508
     509nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
     510match k with
     511[ Kstop ⇒ dy
     512| Kcall _ _ _ _ ⇒ dy
     513| _ ⇒ dn
     514]. nwhd; //; @; #H; nelim H; nqed.
     515
    379516nlet rec exec_step (ge:genv) (st:state) on st : res (Σr:trace × state. step ge st (\fst r) (\snd r)) ≝
    380517match st with
     
    386523    m' ← opt_to_res ? (store_value_of_type (typeof a1) m loc ofs v2);:
    387524    OK ? 〈E0, State f Sskip k e m'〉)
     525  | Scall lhs a al ⇒ Some ? (
     526    vf ← exec_expr ge e m a;:
     527    vargs ← exec_exprlist ge e m al;:
     528    fd ← opt_to_res ? (find_funct Genv ? ge vf);:
     529    p ← are_equal ? type_eq_dec (type_of_fundef fd) (typeof a);:
     530    k' ← match lhs with
     531         [ None ⇒ OK ? (Kcall (None ?) f e k)
     532         | Some lhs' ⇒
     533           locofs ← exec_lvalue ge e m lhs';:
     534           OK ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
     535         ];:
     536    OK ? 〈E0, Callstate fd vargs k' m〉)
     537  | Ssequence s1 s2 ⇒ Some ? (OK ? 〈E0, State f s1 (Kseq s2 k) e m〉)
     538  | Sskip ⇒
     539      match k with
     540      [ Kseq s k' ⇒ Some ? (OK ? 〈E0, State  f s k' e m〉)
     541      | Kstop ⇒
     542          match fn_return f with
     543          [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
     544          | _ ⇒ Some ? (Error ?)
     545          ]
     546      | Kcall _ _ _ _ ⇒
     547          match fn_return f with
     548          [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
     549          | _ ⇒ Some ? (Error ?)
     550          ]
     551      | _ ⇒ Some ? (Error ?) (* TODO more *)
     552      ]
    388553  | Sreturn a_opt ⇒
    389554    match a_opt with
     
    410575| _ ⇒ Some ? (Error ?)
    411576]. nwhd; //;
    412 ##[ napply sig_bind2_OK; #loc ofs Hlval;
     577##[ nrewrite > c7; napply step_skip_call; //; napply c8;
     578##| nrewrite > c11; napply step_skip_call; //; napply c12;
     579##| napply sig_bind2_OK; #loc ofs Hlval;
    413580    napply sig_bind_OK; #v2 ev2 Hv2;
    414581    napply opt_bind_OK; #m' em';
    415582    nwhd; napply (step_assign … Hlval Hv2 em');
     583##| napply sig_bind_OK; #vf evf Hvf;
     584    napply sig_bind_OK; #vargs evargs Hvargs;
     585    napply opt_bind_OK; #fd efd;
     586    napply bind_OK; #ety ety';
     587    ncases c6; nwhd;
     588    ##[ napply (step_call_none … Hvf Hvargs efd ety);
     589    ##| #lhs'; nrewrite > (bind_assoc_r …);
     590        napply sig_bind_OK; #locofs; ncases locofs; #loc ofs elocofs Hlocofs;
     591        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
     592    ##]
    416593##| napply step_return_0; napply c9;
    417594##| napply sig_bind_OK; #u eu Hnotvoid;
     
    436613nwhd; napply (initial_state_intro … eb ef);
    437614nqed.
     615
     616ndefinition is_final_state : ∀st:state. (∃r. final_state st r) + (¬∃r. final_state st r).
     617#st; nelim st;
     618##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
     619##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
     620##| #v k m; ncases k;
     621  ##[ ncases v;
     622    ##[ ##2: #i; @1; @ i; //;
     623    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
     624    ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
     625    ##| #b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
     626    ##]
     627  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
     628  ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
     629  ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
     630  ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
     631  ##]
     632##] nqed.
     633
     634nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
     635 res (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
     636match is_final_state s with
     637[ inl _ ⇒ Some ? (OK ? 〈E0, s〉)
     638| inr _ ⇒
     639  match n with
     640  [ O ⇒ Some ? (OK ? 〈E0, s〉)
     641  | S n' ⇒ Some ? (
     642      〈t,s'〉 ← exec_step ge s;:
     643      〈t',s''〉 ← exec_steps n' ge s';:
     644      OK ? 〈t ⧺ t',s''〉)
     645  ]
     646]. nwhd; /2/;
     647napply sig_bind2_OK; #t s' H1;
     648napply sig_bind2_OK; #t' s'' IH;
     649nwhd; napply (star_step … IH); //;
     650nqed.
Note: See TracChangeset for help on using the changeset viewer.