Changeset 1643


Ignore:
Timestamp:
Jan 13, 2012, 12:23:30 PM (8 years ago)
Author:
tranquil
Message:
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r1641 r1643  
    1919  are not sequential. Thus there is a dummy label at the moment in the code.
    2020  To be fixed once we understand exactly what to do with tail calls. *)
    21 inductive rtl_statement_extension: Type[0] ≝
    22   | rtl_st_ext_stack_address: register → register → rtl_statement_extension
    23   | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_statement_extension
     21inductive rtl_instruction_extension: Type[0] ≝
     22  | rtl_st_ext_stack_address: register → register → rtl_instruction_extension
     23  | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_instruction_extension.
     24
     25inductive rtl_statement_extension : Type[0] ≝
    2426  | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
    2527  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
     
    3941    (* call_args ≝ *) (list rtl_argument)
    4042    (* call_dest ≝ *) (list register)
    41     (* extend_statements ≝ *) rtl_statement_extension
    42     (* ext_forall_labels ≝ *) (λP.λes.True))
     43    (* ext_instruction ≝ *) rtl_instruction_extension
     44    (* ext_forall_labels ≝ *) (λP.λes.True)
     45    (* ext_fin_instruction ≝ *) rtl_statement_extension
     46    (* ext_fin_forall_labels ≝ *) (λP.λes.True))
    4347  (mk_local_params
    4448    (mk_funct_params
     
    122126    (* call_dest ≝ *) (list register)
    123127    (* extend_statements ≝ *) rtlntc_statement_extension
    124     (* ext_forall_labels ≝ *) (λP.λes.True))
     128    (* ext_forall_labels ≝ *) (λP.λes.True)
     129    void (λP,es.True))
    125130  (mk_local_params
    126131    (mk_funct_params
  • src/RTL/semantics_paolo.ma

    r1641 r1643  
    4242
    4343
    44 definition rtl_call_function:
     44definition rtl_setup_call:
    4545 nat → list register → list rtl_argument → state rtl_sem_state_params → res (state rtl_sem_state_params) ≝
    4646  λstacksize,formal_arg_regs,actual_arg_regs,st.
     
    5959qed.
    6060
    61 definition rtl_save_frame:
    62  address → nat → list register → list rtl_argument → list register →
    63   state rtl_sem_state_params → res (state rtl_sem_state_params) ≝
    64  λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
    65   let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st) in
    66   let st ≝ set_frms rtl_sem_state_params frame st in
    67   rtl_call_function stacksize formal_arg_regs actual_arg_regs st.
     61definition rtl_save_frame ≝ λl.λretregs.λst : state rtl_sem_state_params.
     62  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
     63  set_frms rtl_sem_state_params frame st. 
    6864
    6965(*CSC: XXXX, for external functions only*)
     
    7167axiom rtl_set_result: list val → state rtl_sem_state_params → res (state rtl_sem_state_params).
    7268
    73 definition rtl_more_sem_unserialized_params :
     69definition rtl_msu_params :
    7470  more_sem_unserialized_params rtl_uns_params ≝
    7571 mk_more_sem_unserialized_params rtl_uns_params rtl_sem_state_params
     
    8581    rtl_init_locals
    8682    rtl_save_frame
     83    rtl_setup_call
    8784    rtl_fetch_external_args
    8885    rtl_set_result
    8986    [ ] [ ] (*dummy*).
    9087
    91 (* Paolo: got until here *)
     88(* alias *)
     89definition rtl_reg_store : register→beval→state rtl_sem_state_params→
     90    res (state rtl_sem_state_params) ≝ acca_store ? rtl_msu_params.
     91definition rtl_reg_retrieve : state rtl_sem_state_params→register→res beval ≝
     92    acca_retrieve ? rtl_msu_params.
    9293
    93 definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
    94 
    95 definition rtl_result_regs:
    96  ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list register) ≝
     94definition rtl_read_result :
     95 ∀globals. genv globals rtl_params → state rtl_sem_state_params → res (list beval) ≝
    9796 λglobals,ge,st.
    98   do fn ← graph_fetch_function … globals ge st ;
    99   OK … (joint_if_result … fn).
     97  ! p ← code_pointer_of_address (pc … st) ;
     98  ! fn ← fetch_function … ge p ;
     99  m_mmap … (rtl_reg_retrieve st) (joint_if_result … fn).
    100100
    101101(*CSC: we could use a dependent type here: the list of return values should have
     
    103103  saves the OutOfBounds exception *)
    104104definition rtl_pop_frame:
    105  ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     105 ∀globals. genv globals rtl_params → state rtl_sem_state_params →
     106  res (state rtl_sem_state_params) ≝
    106107 λglobals,ge,st.
    107   do ret_regs ← rtl_result_regs … ge st ;
    108   do ret_vals ← mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_regs ;
     108  do ret_vals ← rtl_read_result … ge st ;
    109109  match st_frms ? st with
    110110  [ nil ⇒ Error ? [MSG EmptyStack]
    111111  | cons hd tl ⇒
    112112     do st ←
    113       mfold_left_i ??
     113      mfold_left_i
    114114       (λi.λst.λreg.
    115115         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
    116          greg_store rtl_sem_params reg v st)
     116         rtl_reg_store reg v st)
    117117       (OK … st) (fr_ret_regs hd) ;
    118118     OK …
    119       (set_frms rtl_sem_params tl
    120         (set_regs rtl_sem_params (fr_regs hd)
     119      (set_frms rtl_sem_state_params tl
     120        (set_regs rtl_sem_state_params (fr_regs hd)
    121121         (set_sp … (fr_sp hd)
    122122          (set_carry … (fr_carry hd)
    123123           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    124124
    125 definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
    126  λglobals.
    127   mk_more_sem_params1 … rtl_more_sem_params graph_succ_p (graph_pointer_of_label …)
    128    (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
    129    rtl_init_locals rtl_save_frame (rtl_pop_frame …)
    130    rtl_fetch_external_args rtl_set_result.
    131 definition rtl_sem_params1: ∀globals. sem_params1 … globals ≝
    132  λglobals. mk_sem_params1 … (rtl_more_sem_params1 globals).
    133125
    134 definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
     126(* This code is quite similar to eval_call_block: can we factorize it out? *)
     127definition eval_tail_call_block:
     128 ∀globals.genv globals rtl_params → state rtl_sem_state_params →
     129  block → call_args rtl_uns_params → IO io_out io_in (trace×(state rtl_sem_state_params)) ≝
     130 λglobals,ge,st,b,args.
     131  ! 〈next, tr, st〉 ← eval_call_block_preamble ? rtl_params rtl_msu_params ge st b args (None ?) ;
     132  match next with
     133  [ None ⇒ (* Paolo: external tailcall, copied from evaluation of return, is it right? *)
     134    ! 〈st,ra〉 ← fetch_ra … st ;
     135    ! st ← rtl_pop_frame … ge st;
     136    return 〈tr,st〉
     137  | Some lbl ⇒
     138    return 〈tr,st〉
     139  ].
     140
     141definition block_of_register_pair: register → register → state rtl_sem_state_params → res block ≝
    135142 λr1,r2,st.
    136  do v1 ← greg_retrieve rtl_sem_params st r1 ;
    137  do v2 ← greg_retrieve rtl_sem_params st r2 ;
     143 do v1 ← rtl_reg_retrieve st r1 ;
     144 do v2 ← rtl_reg_retrieve st r2 ;
    138145 do ptr ← pointer_of_address 〈v1,v2〉 ;
    139146 OK … (pblock ptr). 
    140147
    141 (* This code is quite similar to eval_call_block: can we factorize it out? *)
    142 definition eval_tail_call_block:
    143  ∀globals.genv … (rtl_params globals) → state rtl_sem_params →
    144   block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝
    145  λglobals,ge,st,b,args.
    146   ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b);
    147     match fd with
    148     [ Internal fn ⇒
    149       let st ≝ set_m … (free … (m … st) (pblock (sp … st))) st in
    150       ! st ← rtl_call_function (joint_if_stacksize … fn) (joint_if_params … fn) args st ;
    151       let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in
    152       let l' ≝ joint_if_entry … fn in
    153       ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ;
    154        ret ? 〈 E0, st〉
    155     | External fn ⇒ ?(*
    156       ! params ← fetch_external_args … fn st;
    157       ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    158       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    159       (* CSC: XXX bug here; I think I should split it into Byte-long
    160          components; instead I am making a singleton out of it. To be
    161          fixed once we fully implement external functions. *)
    162         let vs ≝ [mk_val ? evres] in
    163       ! st ← set_result … vs st;
    164       let st ≝ set_pc … ra st in
    165         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 *)
    166      ].
    167 cases daemon (*CSC: XXX tailcall to external function not implemented yet;
    168                     it needs alls other functions on external calls *)
    169 qed.
    170 
    171148definition rtl_exec_extended:
    172  ∀globals. genv globals (rtl_params globals)
    173   rtl_statement_extension → label → state rtl_sem_params →
    174    IO io_out io_in (trace × (state rtl_sem_params)) ≝
    175  λglobals,ge,stm,l,st.
     149 ∀globals. genv globals rtl_params
     150  rtl_instruction_extension → state rtl_sem_state_params → address →
     151   IO io_out io_in ((option (label)) × trace × (state rtl_sem_state_params)) ≝
     152 λglobals,ge,stm,st,next_addr.
    176153  match stm with
    177154   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
    178155      let sp ≝ sp ? st in
    179156      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
    180       ! st ← greg_store rtl_sem_params dreg1 dpl st ;
    181       ! st ← greg_store rtl_sem_params dreg2 dph st ;
    182       ! st ← next … (rtl_sem_params1 globals) l st ;
    183        ret ? 〈E0, st〉
     157      ! st ← rtl_reg_store dreg1 dpl st ;
     158      ! st ← rtl_reg_store dreg2 dph st ;
     159      return 〈None label,E0, st〉
    184160   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
    185       ! b ← block_of_register_pair r1 r2 st ;
    186       ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) ;
    187       eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
    188        ge st b args dest ra
    189    | rtl_st_ext_tailcall_id id args ⇒
    190       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     161     ! b ← block_of_register_pair r1 r2 st : IO ???;
     162     eval_call_block_preamble ? rtl_params rtl_msu_params
     163                              ge st b args (Some ? 〈dest,next_addr〉) ].
     164
     165definition rtl_exec_fin_extended:
     166 ∀globals. genv globals rtl_params →
     167  rtl_statement_extension → state rtl_sem_state_params →
     168   IO io_out io_in (trace × (state rtl_sem_state_params)) ≝
     169   λglobals,ge,stm,st.
     170   match stm with
     171   [ rtl_st_ext_tailcall_id id args ⇒
     172      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
    191173      eval_tail_call_block … ge st b args
    192    | rtl_st_ext_tailcall_ptr r1 r2 args ⇒ 
    193       ! b ← block_of_register_pair r1 r2 st ;
     174   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
     175      ! b ← block_of_register_pair r1 r2 st : IO ???;
    194176      eval_tail_call_block … ge st b args
    195177   ].
    196178
    197 definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
    198  λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …).
     179definition rtl_msg_params : more_sem_genv_params rtl_params ≝
     180  mk_more_sem_genv_params rtl_params rtl_msu_params
     181    rtl_read_result
     182    rtl_exec_extended
     183    rtl_exec_fin_extended
     184    rtl_pop_frame.
    199185
    200 definition rtl_fullexec ≝
    201  joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
     186
     187
     188definition rtl_sem_params : sem_params ≝ make_sem_graph_params … rtl_msg_params.
     189
     190definition rtl_fullexec ≝ joint_fullexec … rtl_sem_params.
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1640 r1643  
    816816axiom fake_label: label.
    817817
    818 definition stmt_not_return ≝ λstmt.match stmt with
     818definition stmt_not_final ≝ λstmt.match stmt with
    819819  [ St_return ⇒ False
     820  | St_tailcall_id _ _ ⇒ False
     821  | St_tailcall_ptr _ _ ⇒ False
    820822  | _ ⇒ True ].
    821823
     
    824826        tailcall_* instructions. *)
    825827definition translate_inst : ∀globals.?→?→?→
    826   Prod (bind_list register unit (rtl_instruction globals)) label ≝
     828  (bind_list register unit (rtl_instruction globals)) × label ≝
    827829  λglobals: list ident.
    828830  λlenv: local_env.
    829831  λstmt.
    830   λstmt_prf : stmt_not_return stmt.
     832  λstmt_prf : stmt_not_final stmt.
    831833  match stmt return λx.stmt = x →
    832834    (bind_list register unit (rtl_instruction globals)) × label with
     
    873875        extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])
    874876      ]) [ ], lbl'〉
    875   | St_tailcall_id f args ⇒ λ_.
    876     〈[extension rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))], fake_label〉
    877   | St_tailcall_ptr f args ⇒ λ_.
    878     let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    879     〈bcons … (extension rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) [ ], fake_label〉
    880877  | St_cond r lbl_true lbl_false ⇒ λ_.
    881878    〈translate_cond globals (find_local_env r lenv) lbl_true, lbl_false〉
    882879  | St_jumptable r l ⇒  λ_.? (* assert false: not implemented yet *)
    883   | St_return ⇒ λeq_stmt.⊥
     880  | _ ⇒ λeq_stmt.⊥
    884881  ] (refl …).
    885   [11: cases not_implemented (* jtable case *)
    886   |12: >eq_stmt in stmt_prf; normalize //
     882  [12: cases not_implemented (* jtable case *)
     883  |10,11,13: >eq_stmt in stmt_prf; normalize //
    887884  |*: cases daemon
    888885  (* TODO: proofs regarding lengths of lists, examine! *)
     
    895892  match stmt return λx.stmt = x → rtl_internal_function globals with
    896893  [ St_return ⇒ λ_.add_graph rtl_params globals lbl (RETURN …) def
     894  | St_tailcall_id f args ⇒ λ_.
     895    add_graph rtl_params globals lbl
     896      (extension_fin rtl_params globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) def
     897  | St_tailcall_ptr f args ⇒ λ_.
     898    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
     899    add_graph rtl_params globals lbl
     900      (extension_fin rtl_params globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) def
    897901  | _ ⇒ λstmt_eq.
    898902    let 〈translation, lbl'〉 ≝ translate_inst globals lenv stmt ? in
    899903    rtl_adds_graph globals translation lbl lbl' def
    900904  ] (refl …).
    901 >stmt_eq normalize % qed.
     905[10: cases daemon (* length of address lookup *)
     906|*: >stmt_eq normalize %] qed.
    902907 
    903908 
  • src/joint/Joint_paolo.ma

    r1640 r1643  
    4646 ; call_args: Type[0] (* arguments of function calls *)
    4747 ; call_dest: Type[0] (* possible destination of function computation *)
    48  ; extend_statements: Type[0] (* other statements not fitting in the general framework *)
    49  ; ext_forall_labels : (label → Prop) → extend_statements → Prop
     48 ; ext_instruction: Type[0] (* other instructions not fitting in the general framework *)
     49 ; ext_forall_labels : (label → Prop) → ext_instruction → Prop
     50 ; ext_fin_instruction: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
     51 ; ext_fin_forall_labels : (label → Prop) → ext_fin_instruction → Prop
    5052 }.
    5153 
     
    6870  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
    6971  | COND: acc_a_reg p → label → joint_instruction p globals
    70   | extension: extend_statements p → joint_instruction p globals.
     72  | extension: ext_instruction p → joint_instruction p globals.
    7173
    7274(* Paolo: to be moved elsewhere *)
     
    8688
    8789
    88 
    8990definition inst_forall_labels : ∀p : inst_params.∀globals.
    9091    (label → Prop) → joint_instruction p globals → Prop ≝
     
    119120  | sequential: joint_instruction p globals → succ p → joint_statement p globals
    120121  | GOTO: label → joint_statement p globals
    121   | RETURN: joint_statement p globals.
     122  | RETURN: joint_statement p globals
     123  | extension_fin : ext_fin_instruction p → joint_statement p globals.
    122124
    123125record params : Type[1] ≝
    124126 { stmt_pars :> stmt_params
    125127 ; codeT: list ident → Type[0]
    126  ; lookup: ∀globals.codeT globals → label → option (joint_statement stmt_pars globals)
    127  }.
    128 
    129 
    130 (* for all labels in statement. Uses succ_choice to consider the successor of
    131    a statement when such successors are labels *)
     128 ; code_has_label: ∀globals.codeT globals → label → Prop
     129 ; forall_statements : ∀globals.(joint_statement stmt_pars globals → Prop) →
     130    codeT globals → Prop
     131 }.
     132
     133
    132134definition stmt_forall_labels : ∀p : stmt_params.∀globals.
    133135    (label → Prop) → joint_statement p globals → Prop ≝
     
    136138  | GOTO l ⇒ P l
    137139  | RETURN ⇒ True
     140  | extension_fin c ⇒ ext_fin_forall_labels … P c
    138141  ].
    139142
     
    144147
    145148definition lin_params_to_params ≝
    146   λlp : lin_params. mk_params
    147     (mk_stmt_params lp unit (λ_.λ_.True))
    148     (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    149     (* lookup ≝ *)(λglobals,code,lbl.find ??
    150         (λl_stmt. let 〈lbl_opt, stmt〉 ≝ l_stmt in
    151           ! lbl' ← lbl_opt ;
    152           if eq_identifier … lbl lbl' then return stmt else None ?) code).
     149  λlp : lin_params.let stmt_pars ≝ (mk_stmt_params lp unit (λ_.λ_.True)) in
     150     mk_params
     151      stmt_pars
     152    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement stmt_pars globals)))
     153    (* code_has_label ≝ *)(λglobals,code,lbl.Exists ?
     154        (λl_stmt. \fst l_stmt = Some ? lbl) code)
     155    (* forall_statements ≝ *)(λglobals,P,code.All ?
     156        (λl_stmt. P (\snd l_stmt)) code).
    153157
    154158coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
     
    157161record graph_params : Type[1] ≝
    158162  { g_u_pars :> unserialized_params }.
    159 
    160 include alias "common/Graphs.ma". (* To pick the right lookup *)
    161163
    162164(* One common instantiation of params via Graphs of joint_statements
    163165   (all languages but LIN) *)
    164166definition graph_params_to_params ≝
    165   λgp : graph_params. mk_params
    166     (mk_stmt_params gp label (λP.P))
    167     (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    168     (* lookup ≝ *)(λglobals.lookup …).
     167  λgp : graph_params.let stmt_pars ≝ mk_stmt_params gp label (λP.P) in
     168     mk_params
     169      stmt_pars
     170    (* codeT ≝ *)(λglobals.graph (joint_statement stmt_pars globals))
     171    (* code_has_label ≝ *)(λglobals,code,lbl.lookup … code lbl ≠ None ?)
     172    (* forall_statements ≝ *)(λglobals,P,code.
     173      ∀l,s.lookup … code l = Some ? s → P s).
    169174   
    170 coercion gp_to_p : ∀gp:graph_params.params ≝ λgp.graph_params_to_params gp
     175coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
    171176on _gp : graph_params to params.
    172177   
    173178
    174 definition labels_present : ∀p : params.∀globals.
     179definition labels_present : ∀globals.∀p : params.
    175180  codeT p globals → (joint_statement p globals) → Prop ≝
    176 λglobals,p,code,s. stmt_forall_labels globals p
    177   (λl.lookup … code l ≠ None ?) s.
    178 
    179 definition forall_stmts : ∀p : params.∀globals.
    180   ∀P: joint_statement p globals → Prop. codeT p globals → Prop ≝
    181 λglobals,p,P,code. ∀l,s. lookup … code l = Some ? s → P s.
     181λglobals,p,code,s. stmt_forall_labels p globals
     182  (λl.code_has_label ?? code l) s.
    182183
    183184definition code_closed : ∀p : params.∀globals.
    184185  codeT p globals → Prop ≝ λp,globals,code.
    185     forall_stmts … (labels_present … code) code.
     186    forall_statements … (labels_present … code) code.
    186187
    187188(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
     
    202203  joint_if_code     : codeT p globals ;
    203204(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    204   joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
     205  joint_if_entry    : Σl: label. code_has_label … joint_if_code l;
    205206(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    206   joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
     207  joint_if_exit     : Σl: label. code_has_label …  … joint_if_code l
    207208}.
    208209
     
    216217  λexit: label.
    217218  λp:joint_internal_function globals pars.
    218   λprf: lookup … (joint_if_code … p) exit ≠ None ?.
     219  λprf: code_has_label … (joint_if_code … p) exit.
    219220   mk_joint_internal_function globals pars
    220221    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     
    238239  λgraph.
    239240  λp:joint_internal_function globals pars.
    240   λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
    241   λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
     241  λentry_prf: code_has_label … graph (joint_if_entry … p).
     242  λexit_prf: code_has_label … graph (joint_if_exit … p).
    242243    set_joint_code globals pars p
    243244      graph
  • src/joint/TranslateUtils_paolo.ma

    r1640 r1643  
    9797    bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
    9898    (* this can be added to allow redirections: × label *)) →
     99  (label → ext_fin_instruction src_g_pars →
     100    (bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals))
     101    ×
     102    (joint_statement dst_g_pars globals)) →
    99103  (* initialized function definition with empty graph *)
    100104  joint_internal_function globals dst_g_pars →
     
    103107  (* destination function *)
    104108  joint_internal_function globals dst_g_pars ≝
    105   λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,empty,def.
     109  λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,trans',empty,def.
    106110  let f : label → joint_statement (src_g_pars : params) globals →
    107111    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     
    111115    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    112116    | RETURN ⇒ add_graph … lbl (RETURN …) def
     117    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
     118      let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     119      b_adds_graph … fresh_reg l lbl tmp_lbl (add_graph … tmp_lbl fin def)
    113120    ] in
    114121  foldi … f (joint_if_code … def) empty.
     122
     123definition b_graph_translate_no_fin :
     124  ∀src_g_pars : graph_params.
     125  ext_fin_instruction src_g_pars = void →
     126  ∀dst_g_pars : graph_params.
     127  ∀globals: list ident.
     128  (* type of allocatable registers (unit if not in RTLabs) *)
     129  ∀T : Type[0].
     130  (* fresh register creation *)
     131  freshT globals dst_g_pars (localsT dst_g_pars) T →
     132  (* function dictating the translation *)
     133  (label → joint_instruction src_g_pars globals →
     134    bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
     135    (* this can be added to allow redirections: × label *)) →
     136  (* initialized function definition with empty graph *)
     137  joint_internal_function globals dst_g_pars →
     138  (* source function *)
     139  joint_internal_function globals src_g_pars →
     140  (* destination function *)
     141  joint_internal_function globals dst_g_pars ≝
     142  λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,registerT,fresh_reg,trans.
     143    b_graph_translate src_g_pars dst_g_pars globals registerT fresh_reg
     144      trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
    115145 
    116146(* translation without register allocation *)
     
    121151  (label → joint_instruction src_g_pars globals →
    122152    list (joint_instruction dst_g_pars globals)) →
     153  (label → ext_fin_instruction src_g_pars →
     154    (list (joint_instruction dst_g_pars globals))
     155    ×
     156    (joint_statement dst_g_pars globals)) →
    123157  (* initialized function definition with empty graph *)
    124158  joint_internal_function … dst_g_pars →
     
    127161  (* destination function *)
    128162  joint_internal_function … dst_g_pars ≝
    129   λsrc_g_pars,dst_g_pars,globals,trans,empty,def.
     163  λsrc_g_pars,dst_g_pars,globals,trans,trans',empty,def.
    130164  let f : label → joint_statement (src_g_pars : params) globals →
    131165    joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝
     
    136170    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    137171    | RETURN ⇒ add_graph … lbl (RETURN …) def
     172    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
     173      let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     174      adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def)
    138175    ] in
    139176  foldi ??? f (joint_if_code ?? def) empty.
     177 
     178definition graph_translate_no_fin :
     179  ∀src_g_pars : graph_params.
     180  ext_fin_instruction src_g_pars = void →
     181  ∀dst_g_pars : graph_params.
     182  ∀globals: list ident.
     183  (* type of allocatable registers (unit if not in RTLabs) *)
     184  (* function dictating the translation *)
     185  (label → joint_instruction src_g_pars globals →
     186    list (joint_instruction dst_g_pars globals)
     187    (* this can be added to allow redirections: × label *)) →
     188  (* initialized function definition with empty graph *)
     189  joint_internal_function globals dst_g_pars →
     190  (* source function *)
     191  joint_internal_function globals src_g_pars →
     192  (* destination function *)
     193  joint_internal_function globals dst_g_pars ≝
     194  λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,trans.
     195    graph_translate src_g_pars dst_g_pars globals
     196      trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
     197 
     198
    140199     
    141200(*
  • src/joint/semantics_paolo.ma

    r1641 r1643  
    8686
    8787  ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars
    88    (*CSC: save_frame returns a res only because we can call a function with the wrong number and
     88  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
     89  ; save_frame: address → call_dest uns_pars → state st_pars → state st_pars
     90   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    8991     type of arguments. To be fixed using a dependent type *)
    90   ; save_frame: address → nat → paramsT … uns_pars → call_args uns_pars → call_dest uns_pars →
     92  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
    9193      state st_pars → res (state st_pars)
    9294  ; fetch_external_args: external_function → state st_pars →
     
    129131    return (set_regs ? r st).
    130132
     133axiom BadPointer : String.
     134
     135(* this is preamble to all calls (including tail ones). The optional argument in
     136   input tells the function whether it has to save the frame for internal
     137   calls.
     138   the first element of the triple is the label at the start of the function
     139   in case of an internal call, or None in case of an external one.
     140   The actual update of the pc is left to later, as it depends on
     141   serialization and on whether the call is a tail one. *)
     142definition eval_call_block_preamble:
     143 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
     144  genv globals p → state p' → block → call_args p → option ((call_dest p) × address) →
     145    IO io_out io_in ((option label)×trace×(state p')) ≝
     146 λglobals,p,p',ge,st,b,args,dest_ra.
     147  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
     148    match fd with
     149    [ Internal fn ⇒
     150      let st ≝ match dest_ra with
     151        [ Some p ⇒ let 〈dest, ra〉 ≝ p in save_frame … ra dest st
     152        | None ⇒ st
     153        ] in
     154      ! st ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
     155              args st ;
     156      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
     157      let l' ≝ joint_if_entry … fn in
     158      let st ≝ set_regs p' regs st in
     159      return 〈Some label l', E0, st〉
     160    | External fn ⇒
     161      ! params ← fetch_external_args … p' fn st : IO ???;
     162      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     163      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     164      (* CSC: XXX bug here; I think I should split it into Byte-long
     165         components; instead I am making a singleton out of it. To be
     166         fixed once we fully implement external functions. *)
     167      let vs ≝ [mk_val ? evres] in
     168      ! st ← set_result … p' vs st : IO ???;
     169      return 〈None ?, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     170      ].
     171
     172axiom FailedStore: String.
     173
     174definition push: ∀p. state p → beval → res (state p) ≝
     175 λp,st,v.
     176  let isp ≝ isp … st in
     177  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
     178  let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
     179  OK … (set_m … m (set_sp … isp st)).
     180
     181definition pop: ∀p. state p → res (state p × beval) ≝
     182 λp,st.
     183  let isp ≝ isp ? st in
     184  let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
     185  let ist ≝ set_sp … isp st in
     186  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
     187  OK ? 〈st,v〉.
     188
     189definition save_ra : ∀p. state p → address → res (state p) ≝
     190 λp,st,l.
     191  let 〈addrl,addrh〉 ≝ l in
     192  do st ← push … st addrl;
     193  push … st addrh.
     194
     195definition load_ra : ∀p.state p → res (state p × address) ≝
     196 λp,st.
     197  do 〈st,addrh〉 ← pop … st;
     198  do 〈st,addrl〉 ← pop … st;
     199  OK ? 〈st, 〈addrl,addrh〉〉.
     200
     201
    131202(* parameters that need full params to have type of functions,
    132    but are still independent of serialization *)
     203   but are still independent of serialization
     204   Paolo: the first element returned by exec extended is None if flow is
     205   left to regular sequential one, otherwise a label.
     206   The address input is the address of the next statement, to be provided to
     207   accomodate extensions that make calls. *)
    133208record more_sem_genv_params (pp : params) : Type[1] ≝
    134209  { msu_pars :> more_sem_unserialized_params pp
    135210  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    136   ; exec_extended: ∀globals.genv globals pp → extend_statements pp →
    137       state msu_pars → IO io_out io_in ((option label) × trace × (state msu_pars))
     211  ; exec_extended: ∀globals.genv globals pp → ext_instruction pp →
     212      state msu_pars → address → IO io_out io_in ((option label)× trace × (state msu_pars))
     213  ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_instruction pp →
     214      state msu_pars → IO io_out io_in (trace × (state msu_pars))
    138215  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    139216  }.
     217 
    140218
    141219(* parameters that are defined by serialization *)
     
    165243  OK (state p) (set_pc … newpc st).
    166244
    167 axiom FailedStore: String.
    168 
    169 definition push: ∀p. state p → beval → res (state p) ≝
    170  λp,st,v.
    171   let isp ≝ isp … st in
    172   do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
    173   let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
    174   OK … (set_m … m (set_sp … isp st)).
    175 
    176 definition pop: ∀p. state p → res (state p × beval) ≝
    177  λp,st.
    178   let isp ≝ isp ? st in
    179   let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
    180   let ist ≝ set_sp … isp st in
    181   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    182   OK ? 〈st,v〉.
    183 
    184 definition save_ra : ∀p. state p → address → res (state p) ≝
    185  λp,st,l.
    186   let 〈addrl,addrh〉 ≝ l in
    187   do st ← push … st addrl;
    188   push … st addrh.
    189 
    190 definition load_ra : ∀p.state p → res (state p × address) ≝
    191  λp,st.
    192   do 〈st,addrh〉 ← pop … st;
    193   do 〈st,addrl〉 ← pop … st;
    194   OK ? 〈st, 〈addrl,addrh〉〉.
    195 
    196 
    197245(*
    198246definition empty_state: ∀p. more_sem_params p → state p ≝
     
    208256axiom FailedLoad : String.
    209257axiom BadFunction : String.
    210 axiom BadPointer : String.
    211258
    212259definition eval_call_block:
     
    214261  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    215262 λglobals,p,ge,st,b,args,dest,ra.
    216   ! fd ← (opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
    217     match fd with
    218     [ Internal fn ⇒
    219       ! st ← save_frame … ra (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
    220       let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    221       let l' ≝ joint_if_entry … fn in
    222       let st ≝ set_regs p regs st in
    223       let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
    224       ! newpc ← address_of_label … ge pointer_in_fn l' ;
    225       let st ≝ set_pc … newpc st in
    226       return 〈 E0, st〉
    227     | External fn ⇒
    228       ! params ← fetch_external_args … p fn st : IO ???;
    229       ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    230       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    231       (* CSC: XXX bug here; I think I should split it into Byte-long
    232          components; instead I am making a singleton out of it. To be
    233          fixed once we fully implement external functions. *)
    234       let vs ≝ [mk_val ? evres] in
    235       ! st ← set_result … p vs st : IO ???;
    236       let st ≝ set_pc … ra st in
    237       return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    238       ].
     263 ! 〈next, tr, st〉 ← eval_call_block_preamble … ge st b args (Some ? 〈dest,ra〉) ;
     264 ! new_pc ← match next with
     265  [ Some lbl ⇒
     266    let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
     267    address_of_label globals p ge pointer_in_fn lbl
     268  | None ⇒ return ra
     269  ] ;
     270 let st ≝ set_pc … new_pc st in
     271 return 〈tr, st〉.
    239272% qed.
    240273
     
    273306
    274307(* defining because otherwise typechecker stalls *)
    275 definition eval_call_id_succ:
     308definition eval_sequential :
    276309 ∀globals.∀p:sem_params. genv globals p → state p →
    277   ident → call_args p → call_dest p → succ p → IO io_out io_in (trace×(state p)) ≝
    278  λglobals,p,ge,st,id,args,dest,l.
    279    ! ra ← succ_pc … p l (pc … st) : IO ??? ;
    280    eval_call_id … ge st id args dest ra.
     310  joint_instruction p globals → succ p → IO io_out io_in (trace×(state p)) ≝
     311 λglobals,p,ge,st,seq,l.
     312  match seq with
     313  [ extension c ⇒
     314    ! next_addr ← succ_pc … p l (pc … st) : IO ? ? ? ;
     315    ! 〈next_pc, tr, st〉 ← exec_extended … ge c st next_addr;
     316    ! st ← match next_pc with
     317      [ None ⇒ next … p l st
     318      | Some lbl ⇒ goto … ge lbl st
     319      ] ;
     320    return 〈tr, st〉
     321  | COST_LABEL cl ⇒
     322    ! st ← next … p l st ;
     323    return 〈Echarge cl, st〉
     324  | COMMENT c ⇒
     325    ! st ← next … p l st ;
     326    return 〈E0, st〉
     327  | LOAD dst addrl addrh ⇒
     328    ! vaddrh ← dph_arg_retrieve … st addrh ;
     329    ! vaddrl ← dpl_arg_retrieve … st addrl;
     330    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     331    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
     332    ! st ← acca_store p … dst v st ;
     333    ! st ← next … p l st ;
     334    return 〈E0, st〉
     335  | STORE addrl addrh src ⇒
     336    ! vaddrh ← dph_arg_retrieve … st addrh;
     337    ! vaddrl ← dpl_arg_retrieve … st addrl;
     338    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     339    ! v ← acca_arg_retrieve … st src;
     340    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
     341    let st ≝ set_m … m' st in
     342    ! st ← next … p l st ;
     343    return 〈E0, st〉
     344  | COND src ltrue ⇒
     345    ! v ← acca_retrieve … st src;
     346    ! b ← bool_of_beval v;
     347    if b then
     348     ! st ← goto … p ge ltrue st ;
     349     return 〈E0, st〉
     350    else
     351     ! st ← next … p l st ;
     352     return 〈E0, st〉
     353  | ADDRESS ident prf ldest hdest ⇒
     354    eval_address … ge st ident prf ldest hdest l
     355  | OP1 op dacc_a sacc_a ⇒
     356    ! v ← acca_retrieve … st sacc_a;
     357    ! v ← Byte_of_val v;
     358    let v' ≝ BVByte (op1 eval op v) in
     359    ! st ← acca_store … dacc_a v' st;
     360    ! st ← next … l st ;
     361    return 〈E0, st〉
     362  | OP2 op dacc_a sacc_a src ⇒
     363    ! v1 ← acca_arg_retrieve … st sacc_a;
     364    ! v1 ← Byte_of_val v1;
     365    ! v2 ← snd_arg_retrieve … st src;
     366    ! v2 ← Byte_of_val v2;
     367    ! carry ← bool_of_beval (carry … st);
     368      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
     369      let v' ≝ BVByte v' in
     370      let carry ≝ beval_of_bool carry in
     371    ! st ← acca_store … dacc_a v' st;
     372      let st ≝ set_carry … carry st in
     373    ! st ← next … l st ;
     374    return 〈E0, st〉
     375  | CLEAR_CARRY ⇒
     376    ! st ← next … l (set_carry … BVfalse st) ;
     377    return 〈E0, st〉
     378  | SET_CARRY ⇒
     379    ! st ← next … l (set_carry … BVtrue st) ;
     380    return 〈E0, st〉
     381  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     382    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
     383    ! v1 ← Byte_of_val v1;
     384    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
     385    ! v2 ← Byte_of_val v2;
     386    let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
     387    let v1' ≝ BVByte v1' in
     388    let v2' ≝ BVByte v2' in
     389    ! st ← acca_store … dacc_a_reg v1' st;
     390    ! st ← accb_store … dacc_b_reg v2' st;
     391    ! st ← next … l st ;
     392    return 〈E0, st〉
     393  | POP dst ⇒
     394    eval_pop … ge st dst l
     395  | PUSH src ⇒
     396    ! v ← acca_arg_retrieve … st src;
     397    ! st ← push … st v;
     398    ! st ← next … l st ;
     399    return 〈E0, st〉
     400  | MOVE dst_src ⇒
     401    ! st ← pair_reg_move … st dst_src ;
     402    ! st ← next … l st ;
     403    return 〈E0, st〉
     404  | CALL_ID id args dest ⇒
     405    ! ra ← succ_pc … p l (pc … st) : IO ??? ;
     406    eval_call_id … ge st id args dest ra
     407  ].
    281408
    282409definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
     
    289416       return 〈E0, st〉
    290417    | RETURN ⇒
    291       ! p ← fetch_ra … st ;
    292       let 〈st,ra〉 ≝ p in
     418      ! 〈st,ra〉 ← fetch_ra … st ;
    293419      ! st ← pop_frame … ge st;
    294420      return 〈E0,set_pc … ra st〉
    295    | sequential seq l ⇒
    296       match seq with
    297       [ extension c ⇒
    298         ! 〈lbl_opt, tr, st〉 ← exec_extended … ge c st ;
    299         match lbl_opt with
    300         [ Some lbl ⇒
    301           ! st ← goto … ge lbl st ;
    302           return 〈tr, st〉
    303         | None ⇒
    304           ! st ← next … l st ;
    305           return 〈tr, st〉
    306         ]       
    307        | COST_LABEL cl ⇒
    308          ! st ← next … p l st ;
    309          return 〈Echarge cl, st〉
    310       | COMMENT c ⇒
    311          ! st ← next … p l st ;
    312          return 〈E0, st〉
    313       | LOAD dst addrl addrh ⇒
    314         ! vaddrh ← dph_arg_retrieve … st addrh ;
    315         ! vaddrl ← dpl_arg_retrieve … st addrl;
    316         ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    317         ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    318         ! st ← acca_store p … dst v st ;
    319         ! st ← next … p l st ;
    320         return 〈E0, st〉
    321       | STORE addrl addrh src ⇒
    322         ! vaddrh ← dph_arg_retrieve … st addrh;
    323         ! vaddrl ← dpl_arg_retrieve … st addrl;
    324         ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
    325         ! v ← acca_arg_retrieve … st src;
    326         ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    327         let st ≝ set_m … m' st in
    328         ! st ← next … p l st ;
    329         return 〈E0, st〉
    330       | COND src ltrue ⇒
    331         ! v ← acca_retrieve … st src;
    332         ! b ← bool_of_beval v;
    333         if b then
    334          ! st ← goto … p ge ltrue st ;
    335          return 〈E0, st〉
    336         else
    337          ! st ← next … p l st ;
    338          return 〈E0, st〉
    339       | ADDRESS ident prf ldest hdest ⇒
    340         eval_address … ge st ident prf ldest hdest l
    341       | OP1 op dacc_a sacc_a ⇒
    342         ! v ← acca_retrieve … st sacc_a;
    343         ! v ← Byte_of_val v;
    344         let v' ≝ BVByte (op1 eval op v) in
    345         ! st ← acca_store … dacc_a v' st;
    346         ! st ← next … l st ;
    347         return 〈E0, st〉
    348       | OP2 op dacc_a sacc_a src ⇒
    349         ! v1 ← acca_arg_retrieve … st sacc_a;
    350         ! v1 ← Byte_of_val v1;
    351         ! v2 ← snd_arg_retrieve … st src;
    352         ! v2 ← Byte_of_val v2;
    353         ! carry ← bool_of_beval (carry … st);
    354           let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    355           let v' ≝ BVByte v' in
    356           let carry ≝ beval_of_bool carry in
    357         ! st ← acca_store … dacc_a v' st;
    358           let st ≝ set_carry … carry st in
    359         ! st ← next … l st ;
    360         return 〈E0, st〉
    361       | CLEAR_CARRY ⇒
    362         ! st ← next … l (set_carry … BVfalse st) ;
    363         return 〈E0, st〉
    364       | SET_CARRY ⇒
    365         ! st ← next … l (set_carry … BVtrue st) ;
    366         return 〈E0, st〉
    367       | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    368         ! v1 ← acca_arg_retrieve … st sacc_a_reg;
    369         ! v1 ← Byte_of_val v1;
    370         ! v2 ← accb_arg_retrieve … st sacc_b_reg;
    371         ! v2 ← Byte_of_val v2;
    372         let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    373         let v1' ≝ BVByte v1' in
    374         let v2' ≝ BVByte v2' in
    375         ! st ← acca_store … dacc_a_reg v1' st;
    376         ! st ← accb_store … dacc_b_reg v2' st;
    377         ! st ← next … l st ;
    378         return 〈E0, st〉
    379       | POP dst ⇒
    380         eval_pop … ge st dst l
    381       | PUSH src ⇒
    382         ! v ← acca_arg_retrieve … st src;
    383         ! st ← push … st v;
    384         ! st ← next … l st ;
    385         return 〈E0, st〉
    386       | MOVE dst_src ⇒
    387         ! st ← pair_reg_move … st dst_src ;
    388         ! st ← next … l st ;
    389         return 〈E0, st〉
    390       | CALL_ID id args dest ⇒
    391         eval_call_id_succ … ge st id args dest l
    392      ]
     421   | sequential seq l ⇒ eval_sequential … ge st seq l
     422   | extension_fin c ⇒ exec_fin_extended … ge c st
    393423   ].
    394424
Note: See TracChangeset for help on using the changeset viewer.