Changeset 1713 for src/Clight


Ignore:
Timestamp:
Feb 21, 2012, 11:58:12 AM (8 years ago)
Author:
campbell
Message:

Add a distinguished final state to the front-end languages to match up
with the structured traces.

Location:
src/Clight
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1647 r1713  
    490490          ret ? 〈E0, (State f Sskip k' e m')〉
    491491    ]
     492  | Kstop ⇒
     493    match res with
     494    [ Vint sz r ⇒ match sz return λsz.bvint sz → ? with [ I32 ⇒ λr. ret ? 〈E0, Finalstate r〉 | _ ⇒ λ_. Wrong ??? (msg ReturnMismatch) ] r
     495    | _ ⇒ Wrong ??? (msg ReturnMismatch)
     496    ]
    492497  | _ ⇒ Wrong ??? (msg NonsenseState)
    493498  ]
     499| Finalstate r ⇒
     500    Wrong ??? (msg NonsenseState)
    494501].
    495502
     
    508515let rec is_final (s:state) : option int ≝
    509516match s with
    510 [ Returnstate res k m ⇒
    511   match k with
    512   [ Kstop ⇒
    513     match res with
    514     [ Vint sz r ⇒ intsize_eq_elim ? sz I32 ? r (λr. Some ? r) (None ?)
    515     | _ ⇒ None ?
    516     ]
    517   | _ ⇒ None ?
    518   ]
     517[ Finalstate r ⇒ Some ? r
    519518| _ ⇒ None ?
    520519].
     
    524523[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
    525524| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
    526 | #v #k #m cases k;
    527   [ cases v;
    528     [ 2: * #i [ 1,2: %2 % * #r #H inversion H #i' #m #e destruct
    529               | %1 ; %{ i} //;
    530               ]
    531     | 1: %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    532     | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    533     | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    534     | #ptr %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    535     ]
    536   | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
    537   | 3,4: #a #b #c %2 ; % *; #r #H inversion H; #i #m #e destruct;
    538   | 5,6,8: #a #b #c #d %2 ; % *; #r #H inversion H; #i #m #e destruct;
    539   | #a %2 ; % *; #r #H inversion H; #i #m #e destruct;
    540   ]
     525| #v #k #m %2 % * #r #H inversion H #H1 #H2 #H3 #H4 destruct
     526| #r %1 %{r} %
    541527] qed.
    542528
     
    554540  ]
    555541].
    556 
     542(*
    557543definition mem_of_state : state → mem ≝
    558544λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
    559 
     545*)
    560546definition clight_exec : trans_system io_out io_in ≝
    561547  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
  • src/Clight/CexecComplete.ma

    r1672 r1713  
    456456    #H whd in ⊢ (??%?); >H @refl
    457457| #f #l #s #k #env #m @refl
     458| #r #m //
    458459] qed.
    459460
    460461lemma is_final_complete : ∀s,r. final_state s r → is_final s = Some ? r.
    461 #s0 #r0 * #r #m @refl qed.
     462#s0 #r0 * #r @refl qed.
    462463 
  • src/Clight/CexecEquiv.ma

    r1605 r1713  
    88(* A "single execution" - where all of the input values are made explicit. *)
    99coinductive s_execution : Type[0] ≝
    10 | se_stop : trace → int → mem → s_execution
     10| se_stop : trace → int → s_execution
    1111| se_step : trace → state → s_execution → s_execution
    1212| se_wrong : errmsg → s_execution
     
    1414
    1515coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝
    16 | seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r (mem_of_state s))
     16| seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r)
    1717| seo_step : ∀tr,s,e,se.
    1818    single_exec_of e se →
     
    157157] qed.
    158158
    159 lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
    160 exec_from ge s (se_interact o k i (se_stop tr r m)) →
    161 step ge s tr (Returnstate (Vint I32 r) Kstop m).
    162 #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
     159lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r.
     160exec_from ge s (se_interact o k i (se_stop tr r)) →
     161step ge s tr (Finalstate r).
     162#ge #s0 #o0 #k0 #i0 #tr0 #r0 #H inversion H
    163163[ #tr #r #m #E1 #E2 destruct
    164164| #tr #s #e #se #H1 #H2 #E destruct (E)
    165165| #msg #_ #E destruct
    166 | #o #k #i #se #H1 #H2 #E #_ destruct (E);
    167     lapply (exec_step_sound ge s0);
     166| #o #k #i #se #H1 #H2 #E #_ destruct (E)
     167    lapply (exec_step_sound ge s0)
    168168    >(exec_inf_aux_unfold …) in H2;
    169     cases (exec_step ge s0);
     169    cases (exec_step ge s0)
    170170    [ #o' #k'
    171171        #E' whd in E':(??%??); destruct (E');
     
    226226] qed.
    227227
    228 inductive execution_terminates : trace → state → s_execution → int → mem → Prop ≝
    229 | terminates : ∀s,s',tr,tr',r,e,m.
    230     execution_isteps tr s e s' (se_stop tr' r m) →
    231     execution_terminates (tr⧺tr') s (se_step E0 s e) r m
     228inductive execution_terminates : trace → state → s_execution → int → Prop ≝
     229| terminates : ∀s,s',tr,tr',r,e.
     230    execution_isteps tr s e s' (se_stop tr' r) →
     231    execution_terminates (tr⧺tr') s (se_step E0 s e) r
    232232(* We should only be able to get to here if main is an external function, which is silly. *)
    233 | annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i.
    234     execution_isteps tr s e s' (se_interact o k i (se_stop tr' r m)) →
    235     execution_terminates (tr⧺tr') s (se_step E0 s e) r m.
     233| annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,o,k,i.
     234    execution_isteps tr s e s' (se_interact o k i (se_stop tr' r)) →
     235    execution_terminates (tr⧺tr') s (se_step E0 s e) r.
    236236
    237237coinductive execution_diverging : s_execution → Prop ≝
     
    278278] qed.
    279279
    280 lemma final_step: ∀ge,tr,r,m,s.
    281   exec_from ge s (se_stop tr r m) →
    282   step ge s tr (Returnstate (Vint I32 r) Kstop m).
    283 #ge #tr #r #m #s #EXEC
     280lemma final_step: ∀ge,tr,r,s.
     281  exec_from ge s (se_stop tr r) →
     282  step ge s tr (Finalstate r).
     283#ge #tr #r #s #EXEC
    284284whd in EXEC;
    285285inversion EXEC;
    286 [ #tr' #r' #m' #EXEC' #E #_ destruct (E);
    287     lapply (exec_step_sound ge s);
     286[ #tr' #r' #s' #EXEC' #E #_ destruct (E)
     287    lapply (exec_step_sound ge s)
    288288    >(exec_inf_aux_unfold …) in EXEC';
    289     cases (exec_step ge s);
     289    cases (exec_step ge s)
    290290    [ #o #k #EXEC' whd in EXEC':(??%??); destruct (EXEC');
    291291    | #x cases x; #tr'' #s' whd in ⊢ (??%?? → ?);
     
    294294    | #msg #EXEC' whd in EXEC':(??%??); destruct (EXEC');
    295295    ]
    296     inversion FINAL; #r''' #m'' #E1 #E2 #_ #H destruct (E1 E2);
     296    inversion FINAL #r''' #E1 #E2 #_ #H destruct (E1 E2);
    297297    @H
    298298| #tr' #s' #e' #se' #H #EXEC' #E destruct
     
    304304lemma e_stop_inv: ∀ge,x,tr,r,s.
    305305  exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r s →
    306   x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop (mem_of_state s)〉.
     306  x = Value ??? 〈tr,Finalstate r〉.
    307307#ge #x #tr #r #s
    308308>(exec_inf_aux_unfold …) cases x;
    309309[ #o #k #EXEC whd in EXEC:(??%?); destruct;
    310310| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim'
    311   [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
     311  [ #r' #FINAL cases FINAL; #r'' #EXEC whd in EXEC:(??%?);
    312312      destruct (EXEC); @refl
    313313  | #F #EXEC whd in EXEC:(??%?); destruct (EXEC);
     
    316316] qed.
    317317
    318 lemma terminates_sound: ∀ge,tr,s,r,m,e.
    319   execution_terminates tr s (se_step E0 s e) r m
     318lemma terminates_sound: ∀ge,tr,s,r,e.
     319  execution_terminates tr s (se_step E0 s e) r
    320320  exec_from ge s e →
    321   star (mk_transrel … step) ge s tr (Returnstate (Vint I32 r) Kstop m).
    322 #ge #tr0 #s0 #r #m #e0 #H inversion H;
    323 [ #s #s' #tr #tr' #r' #e #m' #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
     321  star (mk_transrel … step) ge s tr (Finalstate r).
     322#ge #tr0 #s0 #r #e0 #H inversion H;
     323[ #s #s' #tr #tr' #r' #e #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC
    324324    destruct (E1 E2 E3 E4 E5);
    325325    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
    326326    @(star_right … STARs')
    327     [ 2: @(final_step ge tr' r' m' s' … EXECs')
     327    [ 2: @(final_step ge tr' r' s' … EXECs')
    328328    | skip
    329329    | @refl
    330330    ]
    331 | #s #s' #tr #tr' #r' #e #m' #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
    332     destruct;
    333     cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
     331| #s #s' #tr #tr' #r' #e #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC
     332    destruct
     333    cases (several_steps … ESTEPS EXEC) #STARs' #EXECs'
    334334    @(star_right … STARs')
    335335    [ @tr'
     
    403403  ¬(∃r. final_state s' r).
    404404#ge #s #o #k #i #tr #s' #e #H
    405 % *; #r #F cases F in H; #r' #m #H
     405% *; #r #F cases F in H; #r' #H
    406406inversion H;
    407407[ #tr' #r #m #EXEC #E destruct
     
    469469
    470470inductive execution_characterisation : state → s_execution → Prop ≝
    471 | ec_terminates: ∀s,r,m,e,tr.
    472     execution_terminates tr s e r m
     471| ec_terminates: ∀s,r,e,tr.
     472    execution_terminates tr s e r
    473473    execution_characterisation s e
    474474| ec_diverges: ∀s,e,tr.
     
    543543  ]
    544544| #v #kk #m whd in ⊢ (???%); cases kk;
    545     [ 8: #x1 #x2 #x3 #x4 cases x1;
     545    [ cases v // * //
     546    | 8: #x1 #x2 #x3 #x4 cases x1;
    546547      [ whd in ⊢ (???%); cases v; // | #x5 whd in ⊢ (???%); cases x5;
    547548          #x6 #x7 @opt_does_not_interact // ]
    548549    | *: // ]
     550| #r //
    549551] qed.
    550552
     
    615617| eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)).
    616618
    617 lemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False.
    618 #tr0 #r0 #m0 #H inversion H;
     619lemma eno_stop: ∀tr,r. execution_not_over (se_stop tr r) → False.
     620#tr0 #r0 #H inversion H;
    619621[ #tr #s #e #E destruct
    620622| #o #k #tr #s #e #i #E destruct
     
    635637lapply (NONTERMINATING E0 s e ?); //;
    636638cases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
    637 [ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO);
     639[ #tr #i #_ #_ #_ #ENO elim (eno_stop … ENO);
    638640| #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?);
    639641  [ <(E0_right tr) in ⊢ (?%????);
     
    667669  single_exec_of e1 e2 →
    668670  match e1 with
    669   [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ mem_of_state s = m' | _ ⇒ False ]
     671  [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' ⇒ tr = tr' ∧ r = r' | _ ⇒ False ]
    670672  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
    671673  | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ]
     
    859861    *; #e #NNT4 elim (imply_to_and classic … NNT4);
    860862    cases e;
    861     [ #tr' #r #m #STEPS #NOSTEP
    862         @(ec_terminates s r m ? (Eapp tr tr')) %
     863    [ #tr' #r #STEPS #NOSTEP
     864        @(ec_terminates s r ? (Eapp tr tr')) %
    863865        [ @s'
    864866        | @STEPS
     
    872874    | #o #k #i #e' #STEPS #NOSTEP
    873875        cases e' in STEPS NOSTEP;
    874         [ #tr' #r #m #STEPS #NOSTEP
     876        [ #tr' #r #STEPS #NOSTEP
    875877            @(ec_terminates s ???)
    876            [ 4: @(annoying_corner_case_terminates … STEPS) ]
     878           [ 3: @(annoying_corner_case_terminates … STEPS) ]
    877879        | #tr1 #s1 #e1 #STEPS *; #NOSTEP
    878880            @False_ind @NOSTEP //
     
    917919
    918920inductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
    919 | emb_terminates: ∀s,e,tr,r,m.
    920     execution_terminates tr s e r m
     921| emb_terminates: ∀s,e,tr,r.
     922    execution_terminates tr s e r
    921923    execution_matches_behavior e (Terminates tr r)
    922924| emb_diverges: ∀s,e,tr.
     
    932934    execution_matches_behavior (se_wrong msg) (Goes_wrong E0).
    933935
    934 lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
    935   execution_terminates tr s (se_step tr' s' e) r m → s = s'.
    936 #tr #tr' #s #s' #e #r #m #H inversion H;
    937 [ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl
    938 | #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl
     936lemma exec_state_terminates: ∀tr,tr',s,s',e,r.
     937  execution_terminates tr s (se_step tr' s' e) r → s = s'.
     938#tr #tr' #s #s' #e #r #H inversion H;
     939[ #s1 #s2 #tr1 #tr2 #r' #e' #H' #E1 #E2 #E3 #E4 #_ destruct; @refl
     940| #s1 #s2 #tr1 #tr2 #r' #e' #o #k #i #H' #E1 #E2 #E3 #E4 #_ destruct; @refl
    939941] qed.
    940942
     
    959961#s0 #e0 #exec
    960962cases exec;
    961 [ #s #r #m #e #tr #TERM
     963[ #s #r #e #tr #TERM
    962964    %{ (Terminates tr r)}
    963965    @(emb_terminates … TERM)
     
    979981#b #f #ge #m #E1 #E2 #E3 #E4 % *; #r #H2
    980982inversion H2;
    981 #r' #m' #E5 #E6 destruct (E5);
     983#r' #E5 #E6 destruct (E5);
    982984qed.
    983985
     
    10131015        %{r} @F
    10141016    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
    1015         [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
     1017        [ #tr #r #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
    10161018        cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC'
    10171019    lapply (behavior_of_execution ??
     
    10201022        #ge #Ege
    10211023        inversion MATCHES;
    1022         [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM;
     1024        [ #s0 #e1 #tr1 #r #TERM #EXEC #BEHAVES <EXEC in TERM;
    10231025            #TERM
    10241026            lapply (exec_state_terminates … TERM); #E1
     
    10701072    [ whd in EXEC:(?%?);
    10711073        cases e in EXEC;
    1072         [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
     1074        [ #tr #r #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
    10731075        cases (se_inv … EXEC0);
    10741076        @emb_initially_wrong
  • src/Clight/CexecSound.ma

    r1672 r1713  
    511511  ] 
    512512| #v #k' #m' whd in ⊢ (?????%); cases k'; //;
    513     #r #f #e #k whd in ⊢ (?????%); cases r;
    514   [ whd; @step_returnstate_0
    515   | #x cases x; #y cases y; #z cases z; #pcl #b #ofs #ty
    516     @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); //;
    517   ]
     513  [ whd in ⊢ (?????%); cases v // * //
     514  | #r #f #e #k whd in ⊢ (?????%); cases r //
     515    * * #b #ofs #ty
     516    @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); //
     517    ]
     518| //
    518519]
    519520qed.
     
    536537  [ whd; %
    537538  | @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s';
    538       [ #f #s #k #e #m | #fd #args #k #m | #r #k #m ] normalize
    539 (*      whd in ⊢ (? → ?????(??????%?)); *)
    540       cases m; #mc #mn #mp #Hstep normalize
    541 (*      whd in ⊢ (?????(??????%?));*)
     539      [ #f #s #k #e #m | #fd #args #k #m | #r #k #m | #r ] normalize
     540      [ 1,2,3: cases m; #mc #mn #mp ] #Hstep normalize
    542541      @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps
    543       whd; @(star_step ????????? Hsteps) [ 2,5,8: @Hstep | 3,6,9: // ]
     542      whd; @(star_step ????????? Hsteps) [ 2,5,8,11: @Hstep | 3,6,9,12: // ]
    544543  ]
    545544qed.
    546545
    547546lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r.
    548 * [ 3: #v * [ #m #r cases v [ 2: * #r' #E normalize in E; destruct %
    549                             | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 destruct
    550                             ]
    551             | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 try #x6 try #x7 destruct
    552             ]
    553   | *: normalize #x1 #x2 #x3 #x4 #x5 #x6 try #x7 destruct
     547* [ 4: #r #r' normalize #E destruct %
     548  | *: normalize #x1 #x2 #x3 #x4 #x5 try #x6 try #x7 destruct
    554549  ] qed.
  • src/Clight/Csem.ma

    r1672 r1713  
    956956      ∀res: val.
    957957      ∀k: cont.
    958       ∀m: mem. state.
     958      ∀m: mem. state
     959  | Finalstate:
     960      ∀r: int.
     961      state.
    959962                 
    960963(* * Find the statement and manufacture the continuation
     
    11961199  | step_cost: ∀f,lbl,s,k,e,m.
    11971200      step ge (State f (Scost lbl s) k e m)
    1198            (Echarge lbl) (State f s k e m).
     1201           (Echarge lbl) (State f s k e m)
     1202 
     1203  | step_final: ∀r,m.
     1204      step ge (Returnstate (Vint I32 r) Kstop m)
     1205           E0 (Finalstate r).
    11991206
    12001207(*
     
    12201227
    12211228inductive final_state: state -> int -> Prop :=
    1222   | final_state_intro: ∀r,m.
    1223       final_state (Returnstate (Vint I32 r) Kstop m) r.
     1229  | final_state_intro: ∀r.
     1230      final_state (Finalstate r) r.
    12241231
    12251232(* * Execution of a whole program: [exec_program p beh]
Note: See TracChangeset for help on using the changeset viewer.