Changeset 1680 for src/RTLabs


Ignore:
Timestamp:
Feb 9, 2012, 1:22:28 PM (9 years ago)
Author:
campbell
Message:

Comment out unused tailcalls in Cminor and RTLabs.
(They would be a little tricky to deal with in RTLabs/Traces.ma, and we
don't currently generate them.)

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1655 r1680  
    130130      ! vs ← m_mmap … (reg_retrieve (locals f)) args;
    131131      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     132(*
    132133  | St_tailcall_id id args ⇒ λH.
    133134      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     
    140141      ! vs ← m_mmap … (reg_retrieve (locals f)) args;
    141142      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    142 
     143*)
    143144  | St_cond src ltrue lfalse ⇒ λH.
    144145      ! v ← reg_retrieve (locals f) src;
     
    294295  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
    295296  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     297(*
    296298  | #id #rs #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    297299  | #r #rs #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     300*)
    298301  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
    299302  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_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 % % ] | *: #vl #E whd in E:(??%?); destruct ]
  • src/RTLabs/syntax.ma

    r1675 r1680  
    1919| St_call_id : ident → list register → option register → label → statement
    2020| St_call_ptr : register → list register → option register → label → statement
     21(* We're not using these just now, and they'd make the Traces.ma proofs more difficult.
    2122| St_tailcall_id : ident → list register → statement
    2223| St_tailcall_ptr : register → list register → statement
     24*)
    2325| St_cond : register → label → label → statement
    2426| St_jumptable : register → list label → statement
     
    4648| St_call_id _ _ _ l ⇒ P l
    4749| St_call_ptr _ _ _ l ⇒ P l
     50(*
    4851| St_tailcall_id _ _ ⇒ True
    4952| St_tailcall_ptr _ _ ⇒ True
     53*)
    5054| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
    5155| St_jumptable _ ls ⇒ All ? P ls
     
    105109| St_call_id _ _ _ l ⇒ [l]
    106110| St_call_ptr _ _ _ l ⇒ [l]
     111(*
    107112| St_tailcall_id _ _ ⇒ [ ]
    108113| St_tailcall_ptr _ _ ⇒ [ ]
     114*)
    109115| St_cond _ l1 l2 ⇒ [l1; l2]
    110116| St_jumptable _ ls ⇒ ls
Note: See TracChangeset for help on using the changeset viewer.