Changeset 1713


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
Files:
8 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]
  • src/Cminor/semantics.ma

    r1680 r1713  
    7878    ∀    m: mem.
    7979    ∀   st: stack.
    80             state.
    81 
    82 definition mem_of_state : state → mem ≝
    83 λst. match st with
    84 [ State _ _ _ _ _ m _ _ _ _ ⇒ m
    85 | Callstate _ _ m _ ⇒ m
    86 | Returnstate _ m _ ⇒ m
    87 ].
     80            state
     81| Finalstate:
     82    ∀    r: int.
     83            state
     84.
    8885
    8986axiom UnknownLocal : String.
     
    387384                   ] dstP
    388385        ]
    389     | _ ⇒ Error ? (msg BadState)
     386    | SStop ⇒
     387        match result with
     388        [ None ⇒ Error ? (msg ReturnMismatch)
     389        | Some v ⇒ match v with
     390                   [ Vint sz r ⇒ match sz return λsz. bvint sz → res ? with
     391                                 [ I32 ⇒ λr. return 〈E0, Finalstate r〉
     392                                 | _ ⇒ λ_. Error ? (msg ReturnMismatch) ] r
     393                   | _ ⇒ Error ? (msg ReturnMismatch) ]
     394        ]
    390395    ])
     396| Finalstate r ⇒ Error ? (msg BadState)
    391397].
    392398try @(π1 kInv)
     
    431437definition is_final : state → option int ≝
    432438λs. match s with
    433 [ Returnstate res m st ⇒
    434     match st with
    435     [ SStop ⇒
    436         match res with
    437         [ None ⇒ None ?
    438         | Some v ⇒
    439             match v with
    440             [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
    441             | _ ⇒ None ?
    442             ]
    443         ]
    444     | _ ⇒ None ?
    445     ]
     439[ Finalstate r ⇒ Some ? r
    446440| _ ⇒ None ?
    447441].
  • src/RTLabs/Traces.ma

    r1712 r1713  
    1818| Callstate _ _ _ _ _ ⇒ cl_call
    1919| Returnstate _ _ _ _ ⇒ cl_return
     20| Finalstate _ ⇒ cl_other
    2021].
    2122
     
    4344          λ_. match s' with
    4445          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
     46          | Finalstate r ⇒ True
    4547          | _ ⇒ False
    4648          ]
     
    5052      ]).
    5153[ normalize in H; destruct
     54| normalize in H; destruct
    5255| whd in H:(??%?);
    5356  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
     
    369372                          All ? (λf. well_cost_labelled_fn (func f)) fs
    370373| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
     374| Finalstate _ ⇒ True
    371375].
    372376
     
    385389| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
    386390| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
     391| //
    387392] qed.
    388393
     
    404409| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
    405410| normalize #H8 #H9 #H10 #H11 #H12 destruct
     411| #r #E normalize in E; destruct
    406412] qed.
    407413
     
    453459  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
    454460  | normalize #H411 #H412 #H413 #H414 #H415 destruct
     461  | normalize #H1 #H2 destruct
    455462  ] qed.
    456463
     
    497504    next f = next f' →
    498505    stack_of_state (f::fs) s1 →
    499     stack_preserved ends_with_ret s1 (State f' fs m).
     506    stack_preserved ends_with_ret s1 (State f' fs m)
     507| sp_stop : ∀e,s1,r.
     508    stack_preserved e s1 (Finalstate r)
     509.
    500510
    501511discriminator list.
     
    507517#fs0 #fs0' #s0 *
    508518[ #f #fs #m #H inversion H
    509   #a #b #c #d #e #g try #h try #i try #j destruct @refl
     519  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
    510520| #fd #args #dst #f #fs #m #H inversion H
    511   #a #b #c #d #e #g try #h try #i try #j destruct @refl
     521  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
    512522| #rtv #dst #fs #m #H inversion H
    513   #a #b #c #d #e #g try #h try #i try #j destruct @refl
     523  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
     524] qed.
     525
     526lemma stack_preserved_final : ∀e,r,s.
     527  stack_preserved e (Finalstate r) s → ∃r'. s = Finalstate r'.
     528#e #r #s #H inversion H
     529[ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
     530  inversion SOS #a #b #c #d #e #f try #g try #h destruct
     531| #H194 #H195 #H196 #H197 #H198 #H199 #SOS #H201 #H202 #H203 #H204 destruct
     532  inversion SOS #a #b #c #d #e #f try #g try #h destruct
     533| #e' #s' #r' #E1 #E2 #E3 #E4 destruct %{r'} @refl
    514534] qed.
    515535
     
    525545  | #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct
    526546    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
     547  | #s1'' #r #E1 #E2 #E3 #E4 destruct //
    527548  ]
    528549| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
     550| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
     551  cases (stack_preserved_final … H) #r #E destruct //
    529552] qed.
    530553
     
    539562| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
    540563| #res #dst *
    541   [ #m #s2 #tr #_ #EV whd in EV:(??%?); destruct
     564  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct // | *: normalize #a try #b destruct ] ]
    542565  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
    543566    whd in EV:(??%?); destruct @(sp_finished ? f) //
    544567  ]
     568| #r #s2 #tr #E normalize in E; destruct
    545569] qed.
    546570
     
    557581| #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
    558582  #E normalize in E; destruct
     583| #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct
    559584] qed.
    560585
     
    581606  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
    582607  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
    583   ]
     608  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
     609  ]
     610| #e #s1 #r #E1 #E2 #E3 #_ destruct //
    584611] qed.
    585612 
     
    605632  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
    606633  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
    607   ]
     634  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
     635  ]
     636| #e #s1 #r #E1 #E2 #E3 #E4 destruct //
    608637] qed.
    609638
     
    751780  match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth s trace (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
    752781  [ ft_stop st FINAL ⇒
    753       λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ?
     782      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
    754783
    755784  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
     
    836865| @le_S_S_to_le @TERMINATES_IN_TIME
    837866| @(wrl_nonzero … TERMINATES_IN_TIME)
    838 | (* Bad - we've reached the end of the trace; need to fix semantics so that
    839      this can't happen *)
     867| (* We can't reach the final state because the function terminates with a
     868     return *)
     869  inversion TERMINATES
     870  [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct
     871  | #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct
     872  | #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct
     873  | #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct
     874  ]
    840875| @(will_return_return … CL TERMINATES)
    841876| /2 by stack_preserved_return/
     
    902937  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
    903938  ]
    904 ] cases daemon qed.
     939] qed.
    905940
    906941(* We can initialise TIME with a suitably large value based on the length of the
     
    918953qed.
    919954 
    920 (* FIXME: there's trouble at the end of the program because we can't make a step
    921    away from the final return.
    922    
    923    We need to show that the "next pc" is preserved through a function call.
    924    
    925    Tail-calls are not handled properly (which means that if we try to show the
     955(* Tail-calls would not be handled properly (which means that if we try to show the
    926956   full version with non-termination we'll fail because calls and returns aren't
    927957   balanced.
     
    9901020| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
    9911021| Returnstate _ _ _ _ ⇒ None ?
     1022| Finalstate _ ⇒ None ?
    9921023].
    9931024
     
    10981129  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
    10991130  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
    1100   match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 ].
     1131  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
    11011132#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
    11021133whd in ⊢ (??%? → ?);
     
    11571188      normalize in S1; destruct
    11581189    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
     1190    | #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct
    11591191    ]
    11601192  ]
     
    11691201  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
    11701202    %1 whd in FS ⊢ %;
    1171     inversion (stack_preserved_return … EVAL) [ @refl | #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct ]
     1203    inversion (stack_preserved_return … EVAL) [ @refl | #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct | 4: #H276 #H277 #H278 #H279 #H280 #H281 #H282 destruct ]
    11721204    #s1 #f1 #f2 #fs #m #FE #SS1 #_ #E1 #E2 #_ destruct <FE
    11731205    inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ]
     
    11791211    | #lx #nx #H #E1x #E2x #_ destruct @H
    11801212    ]
     1213  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
    11811214  ]
    11821215] qed.
  • src/RTLabs/semantics.ma

    r1681 r1713  
    4444   ∀ stk : list frame.
    4545   ∀   m : mem.
    46    state.
    47 
    48 definition mem_of_state : state → mem ≝
    49 λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
     46   state
     47| Finalstate :
     48   ∀   r : int.
     49   state
     50.
    5051
    5152definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
     
    183184| Returnstate v dst fs m ⇒
    184185    match fs with
    185     [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
     186    [ nil ⇒
     187        match v with
     188        [ Some v' ⇒
     189          match v' with
     190          [ Vint sz r ⇒ match sz return λsz. bvint sz → monad Res ? with
     191                        [ I32 ⇒ λr. return 〈E0, Finalstate r〉
     192                        | _ ⇒ λ_. Error ? (msg ReturnMismatch)
     193                        ] r
     194          | _ ⇒ Error ? (msg ReturnMismatch)
     195          ]
     196        | _ ⇒ Error ? (msg ReturnMismatch)
     197        ]
    186198    | cons f fs' ⇒
    187199        ! locals ← match dst with
     
    192204        return 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉
    193205    ]
     206| Finalstate r ⇒ Error ? (msg FinalState) (* Already in final state *)
    194207]. try @(next_ok f) try @lookup_lookup_present try @H
    195208[ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ]
     
    200213definition RTLabs_is_final : state → option int ≝
    201214λs. match s with
    202 [ State _ _ _ ⇒ None ?
    203 | Callstate _ _ _ _ _ ⇒ None ?
    204 | Returnstate v _ fs _ ⇒
    205     match fs with [ nil ⇒
    206       match v with [ Some v' ⇒
    207         match v' with
    208         [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
    209         | _ ⇒ None ? ]
    210       | None ⇒ None ? ]
    211     | cons _ _ ⇒ None ? ]
     215[ Finalstate r ⇒ Some ? r
     216| _ ⇒ None ?
    212217].
    213218
     
    251256| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
    252257| from_ret : ∀ge,f,fs,rtv,dst,f',m. frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m)
     258| finish : ∀ge,r,dst,m. state_rel ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) (Finalstate r)
    253259.
    254260
     
    315321  [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct
    316322    %5 cases f #func #locals #next #next_ok #sp #retdst %
    317   | #E destruct
     323  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct // | *: normalize #a try #b destruct ] ]
    318324  ]
    319 ] qed.
    320 
     325| #r #tr #s' normalize #E destruct
     326] qed.
     327
Note: See TracChangeset for help on using the changeset viewer.