Changeset 2288


Ignore:
Timestamp:
Aug 2, 2012, 5:04:36 PM (7 years ago)
Author:
campbell
Message:

Remove jumptables from RTLabs. :(

Location:
src/RTLabs
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostSpec.ma

    r2226 r2288  
    2222    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
    2323    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
    24 | St_jumptable _ ls ⇒ λH.
     24(*| St_jumptable _ ls ⇒ λH.
    2525    (* I did have a dependent version of All here, but it's a pain. *)
    26     All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
     26    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls*)
    2727| _ ⇒ λ_. True
    2828]. whd in H;
     
    5555*)
    5656| St_cond _ l1 l2 ⇒ [l1; l2]
    57 | St_jumptable _ ls ⇒ ls
     57(*| St_jumptable _ ls ⇒ ls*)
    5858| St_return ⇒ [ ]
    5959].
  • src/RTLabs/Traces.ma

    r2226 r2288  
    102102    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
    103103    [ St_cond _ _ _ ⇒ cl_jump
    104     | St_jumptable _ _ ⇒ cl_jump
     104(*    | St_jumptable _ _ ⇒ cl_jump*)
    105105    | _ ⇒ cl_other
    106106    ]
     
    666666  ∃f,fs,m. s = State f fs m ∧
    667667  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
    668   (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
     668  (∃r,l1,l2. stmt = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*).
    669669*
    670670[ #f #fs #m #E
     
    673673  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
    674674    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
    675     [ %1 %{A} %{B} %{C} @refl
    676     | %2 %{A} %{B} @refl
    677     ]
     675    (*[ %1*) %{A} %{B} %{C} @refl
     676(*    | %2 %{A} %{B} @refl
     677    ]*)
    678678  ]
    679679| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
     
    689689#ge #s #tr #s' #EV #H #CL
    690690cases (rtlabs_jump_inv s CL)
    691 #fr * #fs * #m * #Es *
    692 [ * #r * #l1 * #l2 #Estmt
     691#fr * #fs * #m * #Es(* *
     692[*) * #r * #l1 * #l2 #Estmt
    693693  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
    694694  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
     
    701701  whd in ⊢ (% → ?);
    702702  * #H1 #H2 [ @H1 | @H2 ]
    703 | * #r * #ls #Estmt
     703(*| * #r * #ls #Estmt
    704704  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
    705705  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
     
    719719    #H1 #H2 @H2
    720720  ]
    721 ] qed.
     721]*) qed.
    722722
    723723lemma rtlabs_call_inv : ∀s.
     
    13441344| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    13451345| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
    1346 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
     1346(*| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
    13471347  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ]
    13481348  whd in ⊢ (??%? → ?);
     
    13511351  [ #e #E normalize in E; destruct
    13521352  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
    1353   ]
     1353  ]*)
    13541354| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
    13551355] qed.
     
    14231423| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
    14241424| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
    1425 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
     1425(*| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
    14261426  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ]
    14271427  whd in ⊢ (??%? → ?);
     
    14301430  [ #e #E normalize in E; destruct
    14311431  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
    1432   ]
     1432  ]*)
    14331433| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
    14341434] qed.
  • src/RTLabs/semantics.ma

    r2176 r2288  
    144144      ! b ← eval_bool_of_val v;
    145145      return 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉
    146 
     146(*
    147147  | St_jumptable r ls ⇒ λH.
    148148      ! v ← reg_retrieve (locals f) r;
     
    155155      | _ ⇒ Error ? (msg BadJumpValue)
    156156      ]
    157 
     157*)
    158158  | St_return ⇒ λH.
    159159      ! v ← match f_result (func f) with
     
    204204]. try @(next_ok f) try @lookup_lookup_present try @H
    205205[ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ]
    206 | whd in H; @(All_nth … H ? E)
    207206| cases (f_entry fn) //
    208207] qed.
     
    287286*)
    288287  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
    289   | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: [ 1,3: #vl ] #E whd in E:(??%?); destruct ]
     288(*  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: [ 1,3: #vl ] #E whd in E:(??%?); destruct ]*)
    290289  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %4
    291290  ]
     
    335334  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
    336335  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct
    337   | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct ] | *: [1,3: #vl] #E whd in E:(??%?); destruct ]
     336(*  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct ] | *: [1,3: #vl] #E whd in E:(??%?); destruct ]*)
    338337  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct
    339338  ]
  • src/RTLabs/syntax.ma

    r2287 r2288  
    2424*)
    2525| St_cond : register → label → label → statement
    26 | St_jumptable : register → list label → statement
    2726| St_return : statement
    2827.
     
    5756*)
    5857| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
    59 | St_jumptable _ ls ⇒ All ? P ls
    6058| St_return ⇒ True
    6159].
Note: See TracChangeset for help on using the changeset viewer.