Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (9 years ago)
Author:
campbell
Message:

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r732 r797  
    99| se_stop : trace → int → mem → s_execution
    1010| se_step : trace → state → s_execution → s_execution
    11 | se_wrong : s_execution
     11| se_wrong : errmsg → s_execution
    1212| se_interact : ∀o:io_out. (io_in o → execution state io_out io_in) → io_in o → s_execution → s_execution.
    1313
     
    1717    single_exec_of e se →
    1818    single_exec_of (e_step ??? tr s e) (se_step tr s se)
    19 | seo_wrong : single_exec_of (e_wrong ???) se_wrong
     19| seo_wrong : ∀msg:errmsg. single_exec_of (e_wrong ??? msg) (se_wrong msg)
    2020| seo_interact : ∀o,k,i,se.
    2121    single_exec_of (k i) se →
     
    6969  [ #r #FINAL | #FINAL ]
    7070  #EXEC whd in EXEC:(??%?); destruct @refl
    71 | #EXEC whd in EXEC:(??%?); destruct
     71| #msg #EXEC whd in EXEC:(??%?); destruct
    7272] qed.
    7373
     
    8282  [ #r ] #FINAL #EXEC whd in EXEC:(??%?);
    8383  destruct @refl
    84 | #EXEC whd in EXEC:(??%?); destruct
     84| #msg #EXEC whd in EXEC:(??%?); destruct
    8585] qed.
    8686
     
    9393| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
    9494  @is_final_elim [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
    95 | #EXEC whd in EXEC:(??%?); destruct
     95| #msg #EXEC whd in EXEC:(??%?); destruct
    9696] qed.
    9797
     
    114114    >(exec_e_step_inv … H2)
    115115    <(exec_e_step … H2) in H1 #H1 % //
    116 | #_ #E destruct
     116| #msg #_ #E destruct
    117117| #o #k #i #se #H1 #H2 #E destruct
    118118] qed.
     
    125125[ #tr #r #m #E1 #E2 destruct
    126126| #tr #s #e #se #H1 #H2 #E destruct (E)
    127 | #_ #E destruct
     127| #msg #_ #E destruct
    128128| #o #k #i #se #H1 #H2 #E destruct (E);
    129129    lapply (exec_step_sound ge s0);
     
    139139            >(exec_e_step_inv … H3)
    140140            #S @S
    141         | #_ #E destruct
     141        | #msg #_ #E destruct
    142142        | #o #k #i #se #H1 #H2 #E destruct
    143143        ]
     
    145145        whd in ⊢ (??%? → ?); @is_final_elim
    146146        [ #r ] #F #E whd in E:(??%?); destruct
    147     | >(exec_inf_aux_unfold …)
     147    | #msg >(exec_inf_aux_unfold …)
    148148        #E' whd in E':(??%?); destruct (E');
    149149    ]
     
    156156[ #tr #r #m #E1 #E2 destruct
    157157| #tr #s #e #se #H1 #H2 #E destruct (E)
    158 | #_ #E destruct
     158| #msg #_ #E destruct
    159159| #o #k #i #se #H1 #H2 #E destruct (E);
    160160    lapply (exec_step_sound ge s0);
     
    177177                | #NF #E whd in E:(??%?); destruct (E)
    178178                ]
    179             | #E whd in E:(??%?); destruct (E)
     179            | #msg #E whd in E:(??%?); destruct (E)
    180180            ]
    181181       | #tr #s #e #e' #H #EXEC #E destruct (E)
    182        | #EXEC #E destruct (E)
     182       | #msg #EXEC #E destruct (E)
    183183       | #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E)
    184184       ]
    185185   | #x cases x; #tr #s whd in ⊢ (??%? → ?);
    186186       @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct (E)
    187    | #E whd in E:(??%?); destruct (E)
     187   | #msg #E whd in E:(??%?); destruct (E)
    188188   ]
    189189] qed.
     
    250250
    251251inductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝
    252 | go_wrong: ∀tr,s,s',e.
    253     execution_isteps tr s e s' se_wrong
     252| go_wrong: ∀tr,s,s',e,msg.
     253    execution_isteps tr s e s' (se_wrong msg)
    254254    execution_goes_wrong tr s (se_step E0 s e) s'.
    255255
     
    283283        @is_final_elim [ #r'' #FINAL | #F ]
    284284        #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    285     | #EXEC' whd in EXEC':(??%?); destruct (EXEC');
     285    | #msg #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    286286    ]
    287287    inversion FINAL; #r''' #m' #E1 #E2 #H destruct (E1 E2);
    288288    @H
    289289| #tr' #s' #e' #se' #H #EXEC' #E destruct
    290 | #EXEC' #E destruct
     290| #msg #EXEC' #E destruct
    291291| #o #k #i #e #H #EXEC #E destruct
    292292] qed.
     
    304304  | #F #EXEC whd in EXEC:(??%?); destruct (EXEC);
    305305  ]
    306 | #EXEC whd in EXEC:(??%?); destruct (EXEC);
     306| #msg #EXEC whd in EXEC:(??%?); destruct (EXEC);
    307307] qed.
    308308
     
    355355qed.
    356356
    357 lemma exec_from_wrong: ∀ge,s.
    358   exec_from ge s se_wrong
    359   exec_step ge s = Wrong ???.
    360 #ge #s #H whd in H;
     357lemma exec_from_wrong: ∀ge,s,msg.
     358  exec_from ge s (se_wrong msg)
     359  exec_step ge s = Wrong ??? msg.
     360#ge #s #msg #H whd in H;
    361361inversion H;
    362362[ #tr #r #m #EXEC #E destruct (E)
     
    364364| >(exec_inf_aux_unfold …)
    365365    cases (exec_step ge s);
    366   [ #o #k #EXEC whd in EXEC:(??%?); destruct
    367   | #x cases x; #tr #s' whd in ⊢ (??%? → ?) @is_final_elim
     366  [ #o #k #msg' #EXEC whd in EXEC:(??%?); destruct
     367  | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim
    368368      [ #r ] #F #EXEC whd in EXEC:(??%?); destruct
    369   | //
     369  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%?) destruct @refl
    370370  ]
    371371| #o #k #i #e #H #EXEC #E destruct
     
    383383    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim
    384384        [ #r ] #F #E whd in E:(??%?); destruct @F
    385     | #E whd in E:(??%?); destruct
    386     ]
    387 | #EXEC #E destruct
     385    | #msg #E whd in E:(??%?); destruct
     386    ]
     387| #msg #EXEC #E destruct
    388388| #o #k #i #e' #H #EXEC #E destruct
    389389] qed.
     
    397397[ #tr' #r #m #EXEC #E destruct
    398398| #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);
    399 | #EXEC #E destruct
     399| #msg #EXEC #E destruct
    400400| #o' #k' #i' #e' #H #EXEC #E destruct;
    401401    >(exec_inf_aux_unfold …) in EXEC;
     
    413413                @(absurd ?? F)
    414414                %{ r'} //;
    415             | #E whd in E:(??%?); destruct
     415            | #msg #E whd in E:(??%?); destruct
    416416            ]
    417         | #EXECK #E  whd in E:(??%?); destruct
     417        | #msg #EXECK #E  whd in E:(??%?); destruct
    418418        | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct
    419419        ]
    420420    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?);
    421421        @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct;
    422     | #E whd in E:(??%?); destruct
     422    | #msg #E whd in E:(??%?); destruct
    423423    ]
    424424] qed.
     
    432432  (¬∃r. final_state s' r).
    433433#ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG;
    434 #tr #s #s' #e #ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4);
     434#tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4);
    435435cases (several_steps … ESTEPS EXEC);
    436436#STAR #EXEC' %
     
    492492cases e1; //; qed.
    493493
    494 lemma opt_does_not_interact: ∀A,B,P,e1,e2.
     494lemma opt_does_not_interact: ∀A,B,P,e1,e2,msg.
    495495  (∀x:B.interact_prop A P (e2 x)) →
    496   interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).
    497 #A #B #P #e1 #e2 #H
     496  interact_prop A P (bindIO ?? B A (opt_to_io ??? msg e1) e2).
     497#A #B #P #e1 #e2 #msg #H
    498498cases e1; //; qed.
    499499
     
    609609] qed.
    610610
    611 lemma eno_wrong: execution_not_over se_wrong → False.
    612 #H inversion H;
     611lemma eno_wrong: ∀msg. execution_not_over (se_wrong msg) → False.
     612#msg #H inversion H;
    613613[ #tr #s #e #E destruct
    614614| #o #k #tr #s #e #i #E destruct
     
    641641      ]
    642642  ]
    643 | #_ #_ #_ #ENO elim (eno_wrong … ENO);
     643| #msg #_ #_ #_ #ENO elim (eno_wrong … ENO);
    644644| #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_
    645645    lapply (CONTINUES E0 s o k i e' (isteps_none …));
     
    678678  [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ]
    679679  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
    680   | e_wrong ⇒ match e2 with [ se_wrong ⇒ True | _ ⇒ False ]
     680  | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ]
    681681  | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ]
    682682  ].
     
    685685[ #tr #r #m whd; % [ % ] //
    686686| #tr #s #e1' #e2' #H' whd; % [ % ] //
    687 | whd; //
     687| #msg whd; //
    688688| #o #k #i #e #H' whd; % [ % ] //
    689689] qed.
     
    711711    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
    712712    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
    713     | 3,7: #E destruct
     713    | 3,7: #msg #E destruct
    714714    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
    715715    ]
    716 | #_ #E whd in E:(?%?);
     716| #msg #_ #E whd in E:(?%?);
    717717    inversion E;
    718718    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
    719719    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
    720     | 3,7: #E1 #E2 destruct
     720    | 3,7: #msg #E1 #E2 destruct
    721721    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
    722722    ]
     
    874874    | #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0
    875875        @NOSTEP //
    876     | #STEPS #NOSTEP
     876    | #msg #STEPS #NOSTEP
    877877        @(ec_wrong ? s s' tr) % //;
    878878    (* The following is stupidly complicated when most of the cases are impossible.
     
    885885        | #tr1 #s1 #e1 #STEPS *; #NOSTEP
    886886            @False_ind @NOSTEP //
    887         | #STEPS #NOSTEP
     887        | #msg #STEPS #NOSTEP
    888888            lapply (exec_step_interaction ge s');
    889889            cases (several_steps … STEPS EXEC); #_
     
    900900                @is_final_elim [ #r ] #F #S whd in S:(?%?);
    901901                cases (se_inv … S);
    902             | #S cases (se_inv … S);
     902            | #msg #S cases (se_inv … S);
    903903            ]
    904904        | #o1 #k1 #i1 #e1 #STEPS #NOSTEP
     
    917917                @is_final_elim [ #r ] #F #S whd in S:(?%?);
    918918                cases (se_inv … S);
    919             | #S cases (se_inv … S);
     919            | #msg #S cases (se_inv … S);
    920920            ]
    921921        ]
     
    937937    execution_goes_wrong tr s e s' →
    938938    execution_matches_behavior e (Goes_wrong tr)
    939 | emb_initially_wrong:
    940     execution_matches_behavior se_wrong (Goes_wrong E0).
     939| emb_initially_wrong: ∀msg.
     940    execution_matches_behavior (se_wrong msg) (Goes_wrong E0).
    941941
    942942lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
     
    960960  execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'.
    961961#tr #tr' #s #s' #s'' #e #H inversion H;
    962 #tr1 #s1 #s2 #e1 #H' #E1 #E2 #E3 #E4 destruct; @refl qed.
     962#tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 destruct; @refl qed.
    963963
    964964lemma behavior_of_execution: ∀s,e.
     
    10211021        %{r} @F
    10221022    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
    1023         [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ]
     1023        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
    10241024        cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC'
    10251025    lapply (behavior_of_execution ??
     
    10601060            lapply (exec_state_wrong … WRONG);
    10611061            #E1 >E1 in WRONG #WRONG
    1062             inversion WRONG; #tr' #s1' #s2' #e'' #GOESWRONG #E4 #E5 #E6 #E7
     1062            inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7
    10631063            <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG
    10641064            cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ]
     
    10671067            @(program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP)
    10681068            #r % #F @(absurd ?? FINAL) %{r} @F
    1069         | #E destruct (E);
     1069        | #msg #E destruct (E);
    10701070        ]
    10711071   ]
    1072 | whd in ⊢ ((∀_.? → %) → ?);
     1072| #msg whd in ⊢ ((∀_.? → %) → ?);
    10731073    #NOINIT #_ #EXEC
    10741074    %{ (Goes_wrong E0)} %
    10751075    [ whd in EXEC:(?%?);
    10761076        cases e in EXEC;
    1077         [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ]
     1077        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
    10781078        cases (se_inv … EXEC0);
    10791079        @emb_initially_wrong
Note: See TracChangeset for help on using the changeset viewer.