Changeset 1324


Ignore:
Timestamp:
Oct 7, 2011, 3:32:07 PM (8 years ago)
Author:
sacerdot
Message:

The semantics of extended statements must also consider the label since
the program counter is not automatically incremented
(because of cond instructions :-(

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1318 r1324  
    6565axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
    6666
    67 axiom ertl_exec_extended: ∀globals. genv globals (ertl_params globals) → ertl_statement_extension → state ertl_sem_params → IO io_out io_in (trace × (state ertl_sem_params)).
     67axiom ertl_exec_extended: ∀globals. genv globals (ertl_params globals) → ertl_statement_extension → label → state ertl_sem_params → IO io_out io_in (trace × (state ertl_sem_params)).
    6868
    6969definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
  • src/LIN/semantics.ma

    r1312 r1324  
    4343axiom lin_set_result: list val → state lin_sem_params → res (state lin_sem_params).
    4444
    45 definition lin_exec_extended: ∀globals. genv globals (lin_params globals) → False → state lin_sem_params → IO io_out io_in (trace × (state lin_sem_params))
     45definition lin_exec_extended: ∀globals. genv globals (lin_params globals) → False → unit → state lin_sem_params → IO io_out io_in (trace × (state lin_sem_params))
    4646 ≝ λglobals,ge,abs. ⊥.
    4747@abs qed.
  • src/LTL/semantics.ma

    r1312 r1324  
    3535axiom ltl_set_result: list val → state ltl_sem_params → res (state ltl_sem_params).
    3636
    37 definition ltl_exec_extended: ∀globals. genv globals (ltl_params globals) → False → state ltl_sem_params → IO io_out io_in (trace × (state ltl_sem_params))
     37definition ltl_exec_extended: ∀globals. genv globals (ltl_params globals) → False → label → state ltl_sem_params → IO io_out io_in (trace × (state ltl_sem_params))
    3838 ≝ λglobals,ge,abs. ⊥.
    3939@abs qed.
  • src/RTL/semantics.ma

    r1322 r1324  
    6767definition rtl_exec_extended:
    6868 ∀globals. genv globals (rtl_params globals) →
    69   rtl_statement_extension → state rtl_sem_params →
     69  rtl_statement_extension → label → state rtl_sem_params →
    7070   IO io_out io_in (trace × (state rtl_sem_params)) ≝
    71  λglobals,ge,stm,st.
     71 λglobals,ge,stm,l,st.
    7272  match stm with
    73    [ rtl_st_ext_address dreg sreg ⇒
    74      
     73   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
     74      let sp ≝ sp ? st in
     75      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
     76      ! regs ← reg_store dreg1 dpl (regs ? st) ;
     77      ! regs ← reg_store dreg2 dph regs ;
     78       ret ? 〈E0, goto … l (set_regs rtl_sem_params regs st)〉
    7579   | rtl_st_ext_call_ptr _ _ _ _ ⇒ ?
    7680   | rtl_st_ext_tailcall_id id regs ⇒ ?
    7781   | rtl_st_ext_tailcall_ptr _ _ _ ⇒ ?
    7882   ].
     83[1,2,3: cases not_implemented ] (*CSC: tailcalls and pointer calls not implemented ATM *)
     84qed.
    7985
    8086definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
  • src/joint/semantics.ma

    r1312 r1324  
    8181 ; set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1))
    8282
    83  ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
     83 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → succ p → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
    8484 }.
    8585
     
    220220    | sequential seq l ⇒
    221221      match seq with
    222       [ extension c ⇒ exec_extended … p ge c st
     222      [ extension c ⇒ exec_extended … p ge c l st
    223223      | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉
    224224      | COMMENT c ⇒ ret ? 〈E0, next … l st〉
Note: See TracChangeset for help on using the changeset viewer.