Changeset 702


Ignore:
Timestamp:
Mar 21, 2011, 6:27:22 PM (9 years ago)
Author:
campbell
Message:

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r700 r702  
    719719].
    720720
    721 definition clight_exec : clight_program → execstep ≝
    722 λp. mk_execstep … (initial_state p) is_final mem_of_state exec_step.
    723 
    724 definition exec_inf : ∀p:clight_program. execution (state (clight_exec p)) io_out io_in ≝
     721definition clight_exec : execstep ≝
     722  mk_execstep … is_final mem_of_state exec_step.
     723
     724definition exec_inf : ∀p:clight_program. execution state io_out io_in ≝
    725725λp.
    726726  match make_initial_state p with
    727   [ OK gs ⇒ exec_inf_aux (clight_exec p) (\fst gs) (ret ? 〈E0,\snd gs〉)
     727  [ OK gs ⇒ exec_inf_aux clight_exec (\fst gs) (ret ? 〈E0,\snd gs〉)
    728728  | _ ⇒ e_wrong ???
    729729  ].
  • src/Clight/CexecEquiv.ma

    r700 r702  
    4949] qed.
    5050
    51 lemma exec_e_step: ∀p,ge,x,tr,s,e.
    52   exec_inf_aux (clight_exec p) ge x = e_step ??? tr s e →
    53   exec_inf_aux (clight_exec p) ge (exec_step ge s) = e.
    54 #p #ge #x #tr #s #e
     51lemma is_final_elim: ∀s.∀P:option int → Type[0].
     52 (∀r. final_state s r → P (Some ? r)) →
     53 ((¬∃r.final_state s r) → P (None ?)) →
     54P (is_final clight_exec s).
     55#s #P #F #NF whd in ⊢ (?%) cases (is_final_state s)
     56[ * #r #FINAL @F @FINAL
     57| #NOTFINAL @NF @NOTFINAL
     58] qed.
     59
     60lemma exec_e_step: ∀ge,x,tr,s,e.
     61  exec_inf_aux clight_exec ge x = e_step ??? tr s e →
     62  exec_inf_aux clight_exec ge (exec_step ge s) = e.
     63#ge #x #tr #s #e
    5564>(exec_inf_aux_unfold …) cases x;
    5665[ #o #k #EXEC whd in EXEC:(??%?); destruct
    57 | #y cases y; #tr' #s' whd in ⊢ (??%? → ?); >(?:? (clight_exec p) s' = is_final s'); whd in match (? (clight_exec) s') in ⊢ %; whd in ⊢ (??%? → ?);
    58     cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
    59     @refl
     66| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
     67  @is_final_elim
     68  [ #r #FINAL | #FINAL ]
     69  (* Some trickery to prevent destruct normalizing clight_exec *)
     70  #EXEC whd in EXEC:(??%?); [ @False_ind destruct |
     71  cut (s = s') [ generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #E destruct @refl ]
     72  #Es <Es in EXEC #EXEC
     73  generalize in EXEC:(??(??????%)?) ⊢ (??%?)
     74  #e0 #E destruct @refl
     75  ]
    6076| #EXEC whd in EXEC:(??%?); destruct
    6177] qed.
    6278
    6379lemma exec_e_step_inv: ∀ge,x,tr,s,e.
    64   exec_inf_aux ge x = e_step tr s e →
     80  exec_inf_aux clight_exec ge x = e_step ??? tr s e →
    6581  x = Value ??? 〈tr,s〉.
    6682#ge #x #tr #s #e
     
    6884[ #o #k #EXEC whd in EXEC:(??%?); destruct
    6985| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
    70     cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
     86  @is_final_elim
     87  [ #r ] #FINAL #EXEC whd in EXEC:(??%?)
     88  (* Again, prevent destruct blowing up *)
     89  [ 2: generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #EXEC ]
     90  destruct;
    7191    @refl
    7292| #EXEC whd in EXEC:(??%?); destruct
     
    7494
    7595lemma exec_e_step_inv2: ∀ge,x,tr,s,e.
    76   exec_inf_aux ge x = e_step tr s e →
     96  exec_inf_aux clight_exec ge x = e_step ??? tr s e →
    7797  ¬∃r.final_state s r.
    7898#ge #x #tr #s #e
    7999>(exec_inf_aux_unfold …) cases x;
    80100[ #o #k #EXEC whd in EXEC:(??%?); destruct
    81 | #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
    82     cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
    83     @FINAL
     101| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
     102  @is_final_elim [ #r #F #EXEC whd in EXEC:(??%?); destruct
     103  | #F whd in ⊢ (??%? → ?) generalize in ⊢ (??(??????%)? → ?) #e0 #EXEC destruct  @F ]
    84104| #EXEC whd in EXEC:(??%?); destruct
    85105] qed.
    86106
    87107definition exec_from : genv → state → s_execution → Prop ≝
    88 λge,s,se. single_exec_of (exec_inf_aux ge (exec_step ge s)) se.
     108λge,s,se. single_exec_of (exec_inf_aux clight_exec ge (exec_step ge s)) se.
     109
     110lemma se_step_eq : ∀tr,s,e,tr',s',e'.
     111 se_step tr s e = se_step tr' s' e' →
     112 tr = tr' ∧ s = s' ∧ e = e'.
     113#tr #s #e #tr' #s' #e' #E
     114(* destruct  This takes a hideous amount of time, not sure why. *)
     115@(match E return λl.λ_. match l with [ se_step tr0 s0 e0 ⇒ tr = tr0 ∧ s = s0 ∧ e = e0 | _ ⇒ False ] with [ refl ⇒ ? ])
     116whd % try % @refl qed.
    89117
    90118lemma exec_from_step : ∀ge,s,tr,s',e.
     
    93121#ge #s0 #tr0 #s0' #e0 #H inversion H;
    94122[ #tr #r #m #E1 #E2 destruct
    95 | #tr #s #e #se #H1 #H2 #E destruct (E);
     123| #tr #s #e #se #H1 #H2 #E (*destruct (E);*)
     124  lapply (se_step_eq … E) * * #E1 #E2 #E3 >E1 >E2 >E3
    96125    >(exec_e_step_inv … H2)
    97126    <(exec_e_step … H2) in H1 #H1 % //
     
    100129] qed.
    101130
    102 lemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
     131axiom exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
    103132exec_from ge s (se_interact o k i (se_step tr s' e)) →
    104133step ge s tr s' ∧
    105134(*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e.
     135(*
    106136#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
    107137[ #tr #r #m #E1 #E2 destruct
    108138| #tr #s #e #se #H1 #H2 #E destruct (E)
    109139| #_ #E destruct
    110 | #o #k #i #se #H1 #H2 #E destruct (E);
     140| #o #k #i #se #H1 #H2 #E (*destruct (E);*)
    111141    lapply (exec_step_sound ge s0);
    112142    cases (exec_step ge s0) in H2 ⊢ %;
     
    130160        #E' whd in E':(??%?); destruct (E');
    131161    ]
    132 ] qed.
    133 
    134 lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
     162] qed.*)
     163
     164axiom exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
    135165exec_from ge s (se_interact o k i (se_stop tr r m)) →
    136166step ge s tr (Returnstate (Vint r) Kstop m).
     167(*
    137168#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
    138169[ #tr #r #m #E1 #E2 destruct
     
    169200   | #E whd in E:(??%?); destruct (E)
    170201   ]
    171 ] qed.
     202] qed.*)
    172203
    173204(* NB: the E0 in the execs are irrelevant. *)
     
    251282] qed.
    252283
    253 lemma final_step: ∀ge,tr,r,m,s.
     284axiom final_step: ∀ge,tr,r,m,s.
    254285  exec_from ge s (se_stop tr r m) →
    255286  step ge s tr (Returnstate (Vint r) Kstop m).
     287  (*
    256288#ge #tr #r #m #s #EXEC
    257289whd in EXEC;
     
    272304| #EXEC' #E destruct
    273305| #o #k #i #e #H #EXEC #E destruct
    274 ] qed.
     306] qed.*)
    275307
    276308
    277309lemma e_stop_inv: ∀ge,x,tr,r,m.
    278   exec_inf_aux ge x = e_stop tr r m →
     310  exec_inf_aux clight_exec ge x = e_stop ??? tr r m →
    279311  x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
    280312#ge #x #tr #r #m
    281313>(exec_inf_aux_unfold …) cases x;
    282314[ #o #k #EXEC whd in EXEC:(??%?); destruct;
    283 | #z cases z; #tr' #s' whd in ⊢ (??%? → ?); cases (is_final_state s');
    284   [ #F cases F; #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
     315| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim
     316  [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
    285317      destruct (EXEC); @refl
    286318  | #F #EXEC whd in EXEC:(??%?); destruct (EXEC);
     
    347379    cases (exec_step ge s);
    348380  [ #o #k #EXEC whd in EXEC:(??%?); destruct
    349   | #x cases x; #tr #s' whd in ⊢ (??%? → ?); cases (is_final_state s');
    350       #F #EXEC whd in EXEC:(??%?); destruct
     381  | #x cases x; #tr #s' whd in ⊢ (??%? → ?) @is_final_elim
     382      [ #r ] #F #EXEC whd in EXEC:(??%?); destruct
    351383  | //
    352384  ]
     
    363395    cases (exec_step ge s);
    364396    [ #o #k #EXEC whd in EXEC:(??%?); destruct
    365     | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?); cases (is_final_state s1);
    366         #F #E whd in E:(??%?); destruct; @F
     397    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim
     398        [ #r ] #F #E whd in E:(??%?); [ destruct | generalize in E:(??(??????%)?) ⊢ ? #e0 #E destruct; @F ]
    367399    | #E whd in E:(??%?); destruct
    368400    ]
  • src/RTLabs/RTLabs-sem.ma

    r693 r702  
    55include "RTLabs/RTLabs-syntax.ma".
    66
    7 include "Values.ma".
    8 include "Errors.ma".
    9 include "Events.ma".
    10 include "Globalenvs.ma".
    11 include "IOMonad.ma".
    12 include "SmallstepExec.ma".
     7include "common/Values.ma".
     8include "common/Errors.ma".
     9include "common/Events.ma".
     10include "common/Globalenvs.ma".
     11include "common/IOMonad.ma".
     12include "common/SmallstepExec.ma".
    1313
    1414definition genv ≝ (genv_t Genv) (fundef internal_function).
     
    287287].
    288288
    289 definition RTLabs_exec : RTLabs_program → execstep ≝
    290 λp. mk_execstep … ? is_final mem_of_state eval_statement.
     289definition RTLabs_exec : execstep ≝
     290  mk_execstep … ? is_final mem_of_state eval_statement.
     291
     292definition make_initial_state : RTLabs_program → res (genv × state) ≝
     293λp.
     294  do ge ← globalenv Genv ?? p;
     295  do m ← init_mem Genv ?? p;
     296  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
     297  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
     298  OK ? 〈ge,Callstate f (nil ?) (dp ??? [[ ]]) (nil ?) m〉.
     299
     300definition exec_inf : ∀p:RTLabs_program. execution state io_out io_in ≝
     301λp.
     302  match make_initial_state p with
     303  [ OK gs ⇒ exec_inf_aux RTLabs_exec (\fst gs) (ret ? 〈E0,\snd gs〉)
     304  | _ ⇒ e_wrong ???
     305  ].
  • src/RTLabs/RTLabs-syntax.ma

    r639 r702  
    22include "basics/logic.ma".
    33
    4 include "AST.ma".
    5 include "CostLabel.ma".
    6 include "FrontEndOps.ma".
    7 include "Registers.ma".
     4include "Clight/AST.ma".
     5include "Clight/CostLabel.ma".
     6include "common/FrontEndOps.ma".
     7include "common/Registers.ma".
    88
    9 include "cerco/Vector.ma".
    10 include "Graphs.ma".
     9include "ASM/Vector.ma".
     10include "common/Graphs.ma".
    1111
    1212(* XXX: ASTish stuff *)
  • src/common/FrontEndOps.ma

    r695 r702  
    1818(* *********************************************************************)
    1919
    20 include "Values.ma".
     20include "common/Values.ma".
    2121
    2222inductive constant : Type[0] ≝
  • src/common/Graphs.ma

    r695 r702  
    22include "basics/logic.ma".
    33
    4 include "binary/positive.ma".
    5 include "Maps.ma".
     4include "utilities/binary/positive.ma".
     5include "common/Maps.ma".
    66
    77definition label : Type[0] ≝ Pos.
  • src/common/Registers.ma

    r695 r702  
    33
    44include "basics/types.ma".
    5 include "binary/positive.ma".
     5include "utilities/binary/positive.ma".
    66
    7 include "Maps.ma".
     7include "common/Maps.ma".
    88
    99definition register ≝ Pos.
  • src/common/SmallstepExec.ma

    r700 r702  
    1111; output : Type[0]
    1212; input : output → Type[0]
    13 ; initial : state → Prop
    1413; is_final : state → option int
    1514; mem_of_state : state → mem
     
    7271*)
    7372
     73record execstep' : Type[1] ≝
     74{ es0 :> execstep
     75; initial : state es0 → Prop
     76}.
    7477
    7578
    7679alias symbol "and" (instance 2) = "logical and".
    7780record related_semantics : Type[1] ≝
    78 { sem1 : execstep
    79 ; sem2 : execstep
     81{ sem1 : execstep'
     82; sem2 : execstep'
    8083; ge1 : genv sem1
    8184; ge2 : genv sem2
Note: See TracChangeset for help on using the changeset viewer.