Changeset 1451


Ignore:
Timestamp:
Oct 22, 2011, 4:18:11 AM (8 years ago)
Author:
sacerdot
Message:
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
Location:
src
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1415 r1451  
    2323  (list (register_env beval)) [] ((register_env beval) × hw_register_env)
    2424   (λsp.〈empty_map …,init_hw_register_env sp〉) 0 it
    25    graph_succ_p
    2625   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    2726    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
     
    3332       match \fst dest_src with
    3433       [ pseudo reg ⇒ ps_reg_store reg v locals
    35        | hardware reg ⇒ hw_reg_store reg v locals])
    36      pointer_of_label.
     34       | hardware reg ⇒ hw_reg_store reg v locals]).
    3735definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
    3836
     
    9189  set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st.
    9290
     91definition ertl_more_sem_params1: ∀globals. more_sem_params1 … (ertl_params globals) ≝
     92 λglobals.
     93  mk_more_sem_params1 … ertl_more_sem_params graph_succ_p (graph_pointer_of_label …)
     94    (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
     95    ertl_init_locals ertl_save_frame (ertl_pop_frame …)
     96    ertl_fetch_external_args ertl_set_result.
     97definition ertl_sem_params1: ∀globals. sem_params1 globals ≝
     98 λglobals. mk_sem_params1 … (ertl_more_sem_params1 globals).
     99
    93100definition ertl_exec_extended:
    94101 ∀globals. genv globals (ertl_params globals) →
     
    102109      ! newsp ← addr_sub sp v;
    103110      let st ≝ set_hwsp newsp st in
    104         ret ? 〈E0,goto … l st〉
     111      ! st ← next … (ertl_sem_params1 globals) l st ;
     112        ret ? 〈E0,st〉
    105113   | ertl_st_ext_del_frame ⇒
    106114      ! v ← framesize … ge st;
     
    108116      ! newsp ← addr_add sp v;
    109117      let st ≝ set_hwsp newsp st in
    110         ret ? 〈E0,goto … l st〉
     118      ! st ← next … (ertl_sem_params1 …) l st ;
     119        ret ? 〈E0,st〉
    111120   | ertl_st_ext_frame_size dst ⇒
    112121      ! v ← framesize … ge st;
    113122      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
    114         ret ? 〈E0, goto … l st〉
     123      ! st ← next … (ertl_sem_params1 …) l st ;
     124        ret ? 〈E0, st〉
    115125   ].
    116126
    117127definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
    118  λglobals.
    119   mk_more_sem_params2 …
    120    (mk_more_sem_params1 … ertl_more_sem_params
    121     (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
    122     ertl_init_locals ertl_save_frame (ertl_pop_frame …)
    123     ertl_fetch_external_args ertl_set_result)
    124    (ertl_exec_extended …).
     128 λglobals. mk_more_sem_params2 … (ertl_more_sem_params1 …) (ertl_exec_extended …).
    125129
    126 definition ertl_fullexec
     130definition ertl_fullexec: fullexec io_out io_in
    127131 joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1415 r1451  
    55definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
    66
    7 (*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
    8 definition ltl_lin_more_sem_params: ∀succT,succ,pointer_of_label. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
    9  λsuccT,succ,pointer_of_label.
     7definition ltl_lin_more_sem_params: ∀succT. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
     8 λsuccT.
    109 mk_more_sem_params ?
    11   unit it hw_register_env init_hw_register_env 0 it succ
     10  unit it hw_register_env init_hw_register_env 0 it
    1211   hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA)
    1312    (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB)
     
    2120       | to_acc reg ⇒
    2221          do v ← hw_reg_retrieve locals reg ;
    23           hw_reg_store RegisterA v locals ])
    24      pointer_of_label.
     22          hw_reg_store RegisterA v locals ]).
    2523
    26 definition ltl_lin_sem_params:
    27  ∀succT,succ,pointer_of_label. sem_params ≝
    28  λsuccT,succ,pointer_of_label.mk_sem_params … (ltl_lin_more_sem_params succT succ pointer_of_label).
     24definition ltl_lin_sem_params: ∀succT. sem_params ≝
     25 λsuccT.mk_sem_params … (ltl_lin_more_sem_params succT).
    2926
    3027
    3128definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    3229definition ltl_lin_pop_frame:
    33  ∀succT,succ,pointer_of_label,codeT,lookup.
     30 ∀succT,codeT,lookup.
    3431 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    35  state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
    36  λ_.λ_.λ_.λ_.λ_.λ_.λ_.λt.OK … t.
     32 state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
     33 λ_.λ_.λ_.λ_.λ_.λt.OK … t.
    3734definition ltl_lin_save_frame:
    38  ∀succT,succ,pointer_of_label. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
    39  λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
     35 ∀succT. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
     36 λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    4037
    4138(* The following implementation only works for functions that return 32 bits *)
    4239definition ltl_lin_result_regs:
    43  ∀succT,succ,pointer_of_label,codeT,lookup.
     40 ∀succT,codeT,lookup.
    4441 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    45  state (ltl_lin_sem_params succT succ pointer_of_label) → res (list Register) ≝
    46  λ_.λ_.λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
     42 state (ltl_lin_sem_params succT) → res (list Register) ≝
     43 λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
    4744
    4845(*CSC: XXXX, for external functions only*)
    49 axiom ltl_lin_fetch_external_args: ∀succT,succ,pointer_of_label.external_function → state (ltl_lin_sem_params succT succ pointer_of_label) → res (list val).
    50 axiom ltl_lin_set_result: ∀succT,succ,pointer_of_label.list val → state (ltl_lin_sem_params succT succ pointer_of_label) → res (state (ltl_lin_sem_params … succ pointer_of_label)).
     46axiom ltl_lin_fetch_external_args: ∀succT.external_function → state (ltl_lin_sem_params succT) → res (list val).
     47axiom ltl_lin_set_result: ∀succT.list val → state (ltl_lin_sem_params succT) → res (state (ltl_lin_sem_params succT)).
    5148
    52 definition ltl_lin_exec_extended: ∀succT,succ,pointer_of_label.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT succ pointer_of_label) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ pointer_of_label)))
    53  ≝ λsuccT,succ,pointer_of_label,p,globals,ge,abs. ⊥.
     49definition ltl_lin_exec_extended: ∀succT.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT) → IO io_out io_in (trace × (state (ltl_lin_sem_params succT)))
     50 ≝ λsuccT,p,globals,ge,abs. ⊥.
    5451@abs qed.
    5552
    5653definition ltl_lin_more_sem_params2:
    57  ∀succT,succ,pointer_of_label,codeT,lookup,fetch.
     54 ∀succT,codeT,lookup.∀succ: succT → address → res address.∀fetch.
     55 ∀pointer_of_label: ∀globals. genv globals
     56  (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals))
     57  →pointer→label→res (Σp0:pointer.ptype p0=Code).
    5858 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
    59  λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
     59 λsuccT,codeT,lookup,succ,fetch,pointer_of_label,globals.
    6060  mk_more_sem_params2 …
    61    (mk_more_sem_params1 … (ltl_lin_more_sem_params … succ pointer_of_label)
    62     (fetch globals) (load_ra …) (ltl_lin_result_regs …)
     61   (mk_more_sem_params1 … (ltl_lin_more_sem_params …)
     62    succ (pointer_of_label …) (fetch globals) (load_ra …) (ltl_lin_result_regs …)
    6363    ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    6464    (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …).
    6565
    6666definition ltl_lin_fullexec ≝
    67  λsuccT,succ,pointer_of_label,codeT,lookup,fetch.
    68   joint_fullexec … (λp. ltl_lin_more_sem_params2 succT succ pointer_of_label codeT lookup fetch (prog_var_names … p)).
     67 λsuccT,codeT,lookup,succ,fetch,pointer_of_label.
     68  joint_fullexec … (λp. ltl_lin_more_sem_params2 succT codeT lookup succ fetch pointer_of_label (prog_var_names … p)).
  • src/LIN/semantics.ma

    r1408 r1451  
    55 λ_.λaddr. addr_add addr 1.
    66
    7 (*CSC: XXXX here re-use the code for the lookup argument of LIN params__ *)
    8 axiom lin_pointer_of_label: label → Σp:pointer. ptype p = Code.
     7axiom BadOldPointer: String.
     8(*CSC: XXX factorize the code with graph_fetch_function!!! *)
     9definition lin_fetch_function:
     10 ∀globals. genv … (lin_params globals) → pointer → res (joint_internal_function globals (lin_params globals)) ≝
     11 λglobals,ge,old.
     12  let b ≝ pblock old in
     13  do def ← opt_to_res ? [MSG BadOldPointer] (find_funct_ptr … ge b);
     14  match def with
     15  [ Internal fn ⇒ OK … fn
     16  | External _ ⇒ Error … [MSG BadOldPointer]].
    917
    10 (*CSC: XXX factorize code with graph_fetch_statement!!!!!*)
     18axiom BadLabel: String.
     19definition lin_pointer_of_label:
     20 ∀globals. genv … (lin_params globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
     21 λglobals,ge,old,l.
     22  do fn ← lin_fetch_function … ge old ;
     23  do pos ←
     24   opt_to_res ? [MSG BadLabel]
     25    (position_of ?
     26      (λs. let 〈l',x〉 ≝ s in
     27        match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
     28     (joint_if_code … (lin_params …) fn)) ;
     29  OK … (inject … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
     30// qed.
     31
     32(*CSC: XXX factorize code with graph_fetch_statement?*)
    1133axiom BadProgramCounter: String.
    12 axiom lin_fetch_statement:
    13  ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).
    14 (* λglobals,ge,st.
    15   do p ← pointer_of_address (pc … st) ;
    16   let b ≝ pblock p in
    17   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    18   [ Internal def' ⇒
    19      let off ≝ poff p in
    20      opt_to_res ? [MSG BadProgramCounter] (\snd (nth ?? (joint_if_code … def') off))
    21   | External _ ⇒ Error … [MSG BadProgramCounter]].*)
     34definition lin_fetch_statement:
     35 ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params unit) → res (pre_lin_statement globals) ≝
     36 λglobals,ge,st.
     37  do ppc ← pointer_of_address (pc … st) ;
     38  do fn ← lin_fetch_function … ge ppc ;
     39  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
     40  do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
     41  OK … (\snd found).
    2242
    23 definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc lin_pointer_of_label … lin_fetch_statement.
     43definition lin_fullexec: fullexec io_out io_in ≝
     44 ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement lin_pointer_of_label.
  • src/LTL/semantics.ma

    r1383 r1451  
    22include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 definition ltl_fullexec
    5  ltl_lin_fullexec … (graph_succ_p …) pointer_of_label …
    6   (graph_fetch_statement … (ltl_lin_sem_params …)).
     4definition ltl_fullexec : fullexec io_out io_in
     5 ltl_lin_fullexec … graph_succ_p (graph_fetch_statement … (ltl_lin_sem_params …))
     6  (graph_pointer_of_label …).
  • src/RTL/semantics.ma

    r1415 r1451  
    1414definition rtl_more_sem_params: more_sem_params rtl_params_ :=
    1515 mk_more_sem_params rtl_params_
    16   (list frame) [] (register_env beval) (λ_.empty_map …) [] [](*dummy*) graph_succ_p
     16  (list frame) [] (register_env beval) (λ_.empty_map …) [] [](*dummy*)
    1717   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
    1818    reg_store reg_retrieve reg_store reg_retrieve
    1919     (λlocals,dest_src.
    2020       do v ← reg_retrieve locals (\snd dest_src) ;
    21        reg_store (\fst dest_src) v locals)
    22      pointer_of_label.
     21       reg_store (\fst dest_src) v locals).
    2322definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
    2423
     
    9998definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
    10099 λglobals.
    101   mk_more_sem_params1 … rtl_more_sem_params
     100  mk_more_sem_params1 … rtl_more_sem_params graph_succ_p (graph_pointer_of_label …)
    102101   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
    103102   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
    104103   rtl_fetch_external_args rtl_set_result.
     104definition rtl_sem_params1: ∀globals. sem_params1 … globals ≝
     105 λglobals. mk_sem_params1 … (rtl_more_sem_params1 globals).
    105106
    106107definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
     
    123124      let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in
    124125      let l' ≝ joint_if_entry … fn in
    125        ret ? 〈 E0, goto … l' (set_regs rtl_sem_params regs st)〉
     126      ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ;
     127       ret ? 〈 E0, st〉
    126128    | External fn ⇒ ?(*
    127129      ! params ← fetch_external_args … fn st;
     
    151153      ! st ← greg_store rtl_sem_params dreg1 dpl st ;
    152154      ! st ← greg_store rtl_sem_params dreg2 dph st ;
    153        ret ? 〈E0, goto … l st〉
     155      ! st ← next … (rtl_sem_params1 globals) l st ;
     156       ret ? 〈E0, st〉
    154157   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
    155158      ! b ← block_of_register_pair r1 r2 st ;
  • src/TODO

    r1431 r1451  
    33VOLKER SORGE
    44
    5 1) implementare LIN/semantics.ma
     50) factorize lin_fetch_function and graph_fetch_function
     6    and maybe also lin_fetch_statement and graph_fetch_statement
     71) bug rappresentazione dei pointer come address
    682) traduzione LINToASM ed etichetti uniche
    793) funzioni esterne
     
    10124) codice ERTLToLTL da abbellire
    1113
    12 1) bug rappresentazione dei pointer come address
    13142) spurious PUSH/POP in the syntax,
    14153) spurious entry/exit label in the syntax
  • src/joint/SemanticUtils.ma

    r1416 r1451  
    3434  pointer arithmetics on Code pointers.
    3535*)
    36 definition pointer_of_label: label → Σp:pointer. ptype p = Code ≝
    37  λl.
     36definition graph_pointer_of_label0:
     37 pointer → label → Σp:pointer. ptype p = Code ≝
     38 λoldpc,l.
    3839  mk_pointer Code
    3940   (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l))))
     
    4142// qed.
    4243
     44definition graph_pointer_of_label:
     45 ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
     46 λ_.λ_.λ_.λoldpc,l.
     47  OK ? (graph_pointer_of_label0 oldpc l).
     48
    4349(*CSC: XXXX; inverse of the previous function, but it does not check that
    4450  the offset is zero and thus it never fails. *)
    45 definition label_of_pointer: pointer → res label ≝
     51definition graph_label_of_pointer: pointer → res label ≝
    4652 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))).
    4753
     
    5258 to organize the code? *)
    5359definition graph_succ_p: label → address → res address ≝
    54  λl.λ_.address_of_pointer (pointer_of_label l).
     60 λl,old.
     61  do ptr ← pointer_of_address old ;
     62  let newptr ≝ graph_pointer_of_label0 ptr l in
     63  address_of_pointer newptr.
    5564
    5665axiom BadProgramCounter: String.
     
    7584  do p ← code_pointer_of_address (pc … st) ;
    7685  do f ← graph_fetch_function … ge st ;
    77   do l ← label_of_pointer p;
     86  do l ← graph_label_of_pointer p;
    7887  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
  • src/joint/semantics.ma

    r1430 r1451  
    1919 ; call_dest_for_main: call_dest p
    2020
    21  (*CSC: XXXX succ_pc and pointer_of_label deal with fetching; same for
    22    fetch_statement below.
    23    should we take 'em out in a different record to simplify the code? *)
    24  ; succ_pc: succ p → address → res address
    2521 ; greg_store_: generic_reg p → beval → regsT → res regsT
    2622 ; greg_retrieve_: regsT → generic_reg p → res beval
     
    3430 ; dph_retrieve_: regsT → dph_reg p → res beval
    3531 ; pair_reg_move_: regsT → pair_reg p → res regsT
    36  
    37  ; pointer_of_label: label → Σp:pointer. ptype p = Code
    3832 }.
    3933
     
    6357 { more_sparams :> more_sem_params p
    6458
     59 (*CSC: XXXX succ_pc, pointer_of_label and fetch_statement all deal with fetching
     60   should we take 'em out in a different record to simplify the code? *)
     61 ; succ_pc: succ p → address → res address
     62 ; pointer_of_label: genv … p → pointer → label → res (Σp:pointer. ptype p = Code)
    6563 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
    6664
     
    10199 ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1 ?.
    102100
    103 definition address_of_label: sem_params → label → address ≝
    104  λp,l.address_of_code_pointer (pointer_of_label … p l).
    105 
    106101definition set_m: ∀p. bemem → state p → state p ≝
    107102 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
     
    125120 λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    126121
    127 definition goto: ∀p:sem_params. label → state p → state p ≝
    128  λp,l,st. set_pc … (address_of_label p l) st.
    129 
    130 definition next: ∀p:sem_params. succ … p → state p → res (state p) ≝
    131  λp,l,st.
    132   do l' ← succ_pc … (more_sem_pars p) l (pc … st) ;
     122
     123definition address_of_label: ∀globals. ∀p:sem_params1 globals. genv globals p → pointer → label → res address ≝
     124 λglobals,p,ge,ptr,l.
     125  do newptr ← pointer_of_label … p ge … ptr l ;
     126  OK … (address_of_code_pointer newptr).
     127
     128definition goto: ∀globals. ∀p:sem_params1 globals. genv globals p → label → state p → res (state p) ≝
     129 λglobals,p,ge,l,st.
     130  do oldpc ← pointer_of_address (pc … st) ;
     131  do newpc ← address_of_label … ge oldpc l ;
     132  OK … (set_pc … newpc st).
     133
     134definition next: ∀globals. ∀p:sem_params1 globals. succ … p → state p → res (state p) ≝
     135 λglobals,p,l,st.
     136  do l' ← succ_pc … p l (pc … st) ;
    133137  OK … (set_pc … l' st).
    134138
     
    222226      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    223227      let l' ≝ joint_if_entry … fn in
    224        ret ? 〈 E0, goto … l' (set_regs p regs st)〉
     228      ! st ← goto … ge l' (set_regs p regs st) ;
     229       ret ? 〈 E0, st〉
    225230    | External fn ⇒
    226231      ! params ← fetch_external_args … fn st;
     
    247252  ! s ← fetch_statement … ge st;
    248253  match s with
    249     [ GOTO l ⇒ ret ? 〈E0, goto … l st〉
     254    [ GOTO l ⇒
     255       ! st ← goto … p ge l st ;
     256       ret ? 〈E0, st〉
    250257    | sequential seq l ⇒
    251258      match seq with
    252259      [ extension c ⇒ exec_extended … p ge c l st
    253260      | COST_LABEL cl ⇒
    254          ! st ← next … l st ;
     261         ! st ← next … p l st ;
    255262         ret ? 〈Echarge cl, st〉
    256263      | COMMENT c ⇒
    257          ! st ← next … l st ;
     264         ! st ← next … p l st ;
    258265         ret ? 〈E0, st〉
    259266      | INT dest v ⇒
    260267         ! st ← greg_store p dest (BVByte v) st;
    261          ! st ← next … l st ;
     268         ! st ← next … p l st ;
    262269          ret ? 〈E0, st〉
    263270      | LOAD dst addrl addrh ⇒
     
    267274        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    268275        ! st ← acca_store p … dst v st;
    269         ! st ← next … l st ;
     276        ! st ← next … p l st ;
    270277          ret ? 〈E0, st〉
    271278      | STORE addrl addrh src ⇒
     
    276283        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    277284        let st ≝ set_m … m' st in
    278         ! st ← next … l st ;
     285        ! st ← next … p l st ;
    279286          ret ? 〈E0, st〉
    280287      | COND src ltrue ⇒
     
    282289        ! b ← bool_of_beval v;
    283290        if b then
    284          ret ? 〈E0, goto … ltrue st〉
     291         ! st ← goto … p ge ltrue st ;
     292         ret ? 〈E0, st〉
    285293        else
    286          ! st ← next … l st ;
     294         ! st ← next … p l st ;
    287295         ret ? 〈E0, st〉
    288296      | ADDRESS ident prf ldest hdest ⇒
     
    291299        ! st ← dpl_store p ldest laddr st;
    292300        ! st ← dph_store p hdest haddr st;
    293         ! st ← next … l st ;
     301        ! st ← next … p l st ;
    294302          ret ? 〈E0, st〉
    295303      | OP1 op dacc_a sacc_a ⇒
     
    298306          let v' ≝ BVByte (op1 eval op v) in
    299307        ! st ← acca_store p dacc_a v' st;
    300         ! st ← next … l st ;
     308        ! st ← next … p l st ;
    301309          ret ? 〈E0, st〉
    302310      | OP2 op dacc_a sacc_a src ⇒
     
    311319        ! st ← acca_store p dacc_a v' st;
    312320          let st ≝ set_carry … carry st in
    313         ! st ← next … l st ;
     321        ! st ← next … p l st ;
    314322          ret ? 〈E0, st〉
    315323      | CLEAR_CARRY ⇒
    316         ! st ← next … l (set_carry … BVfalse st) ;
     324        ! st ← next … p l (set_carry … BVfalse st) ;
    317325         ret ? 〈E0, st〉
    318326      | SET_CARRY ⇒
    319         ! st ← next … l (set_carry … BVtrue st) ;
     327        ! st ← next … p l (set_carry … BVtrue st) ;
    320328         ret ? 〈E0, st〉
    321329      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     
    329337        ! st ← acca_store p dacc_a_reg v1' st;
    330338        ! st ← accb_store p dacc_b_reg v2' st;
    331         ! st ← next … l st ;
     339        ! st ← next … p l st ;
    332340          ret ? 〈E0, st〉
    333341      | POP dst ⇒
    334342        ! 〈st,v〉 ← pop … st;
    335343        ! st ← acca_store p dst v st;
    336         ! st ← next … l st ;
     344        ! st ← next … p l st ;
    337345          ret ? 〈E0, st〉
    338346      | PUSH src ⇒
    339347        ! v ← acca_retrieve … st src;
    340348        ! st ← push … st v;
    341         ! st ← next … l st ;
     349        ! st ← next … p l st ;
    342350          ret ? 〈E0, st〉
    343351      | MOVE dst_src ⇒
    344352        ! st ← pair_reg_move … st dst_src ;
    345         ! st ← next … l st ;
     353        ! st ← next … p l st ;
    346354          ret ? 〈E0, st〉
    347355      | CALL_ID id args dest ⇒
    348         ! ra ← succ_pc … (more_sem_pars p) l (pc … st) ;         
     356        ! ra ← succ_pc … p l (pc … st) ;         
    349357          eval_call_id … p ge st id args dest ra ]
    350358    | RETURN ⇒
     
    419427[3: % | cases ispb | cases spb] *; #r #off #E >E %
    420428qed.
    421 (*
    422 RTL:
    423  init_prog == init_mem
    424  init_sp: inizializzare lo stack pointer
    425  init_isp: inizializzare l'altro stack pointer
    426  init_renv: inizializzare i registri fisici
    427  init_main_call: chiamata di funzione
    428    --- init_fun_call: cambia fra ERTL e LTL
    429  change_carry: a 0
    430 *)
    431429
    432430definition joint_fullexec :
  • src/utilities/lists.ma

    r1351 r1451  
    120120    ]
    121121].
     122
     123let rec position_of_aux (A:Type[0]) (found: A → bool) (l:list A) (acc:nat) on l : option nat ≝
     124match l with
     125[ nil ⇒ None ?
     126| cons h t ⇒
     127   match found h with [true ⇒ Some … acc | false ⇒ position_of_aux … found t (S acc)]].
     128
     129definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝
     130 λA,found,l. position_of_aux A found l 0.
Note: See TracChangeset for help on using the changeset viewer.