Changeset 2837 for src/LIN


Ignore:
Timestamp:
Mar 9, 2013, 12:19:39 PM (7 years ago)
Author:
tranquil
Message:
  • filled in evaluation of LTL/LIN's extended instrucitons
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2830 r2837  
    3232
    3333(*CSC: XXXX, for external functions only*)
    34 axiom ltl_lin_fetch_external_args: external_function → state LTL_LIN_state → res (list val).
     34axiom ltl_lin_fetch_external_args: external_function → state LTL_LIN_state → ℕ → res (list val).
    3535axiom ltl_lin_set_result: list val → unit → state LTL_LIN_state → res (state LTL_LIN_state).
    3636
     
    4343[ PTR ⇒ return (st_no_pc … st)
    4444| ID ⇒ push_ra … st (pc … st)
    45 ].
     45].
     46
     47definition eval_LTL_LIN_ext_seq :
     48 ∀F.∀globals.∀ge : genv_gen F globals.ltl_lin_seq → ident → state LTL_LIN_state → res (state LTL_LIN_state) ≝
     49λF,globals,ge,s,curr_id,st.
     50match s with
     51[ SAVE_CARRY ⇒
     52  let regs ≝ hwreg_set_other … (carry … st) (regs … st) in
     53  return set_regs LTL_LIN_state regs st
     54| RESTORE_CARRY ⇒
     55  let carry ≝ other_bit (regs … st) in
     56  return set_carry LTL_LIN_state carry st
     57| LOW_ADDRESS r l ⇒  ! pc_lab ← get_pc_from_label … ge curr_id l;
     58                    let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
     59                    let regs ≝ hwreg_store r addrl (regs … st) in
     60                    return set_regs LTL_LIN_state regs st
     61| HIGH_ADDRESS r l ⇒ ! pc_lab ← get_pc_from_label … ge curr_id l;
     62                    let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
     63                    let regs ≝ hwreg_store r addrh (regs … st) in
     64                    return set_regs LTL_LIN_state regs st
     65].
    4666
    4767definition LTL_LIN_semantics ≝
     
    6686*)  (* save_frame         ≝ *) LTL_LIN_save_frame
    6787  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
    68   (* fetch_external_args≝ *) ?(*ltl_lin_fetch_external_args*)
     88  (* fetch_external_args≝ *) ltl_lin_fetch_external_args
    6989  (* set_result         ≝ *) ltl_lin_set_result
    7090  (* call_args_for_main ≝ *) 0
     
    7292  (* read_result        ≝ *) (λ_.λ_.λ_.
    7393  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
    74   (* eval_ext_seq       ≝ *) ?(*(λ_.λ_.λs.λ_.eval_ltl_lin_seq s)*)
    75 (*  (* eval_ext_tailcall  ≝ *) ?(*(λ_.λ_.λabs.match abs in void with [ ])*)
    76   (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    77 *)  (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st))
    78 (*  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)*).
    79 [ #x cases daemon
    80 | #globals #genv whd in ⊢ (% → ?); cases daemon ]
    81 qed.
     94  (* eval_ext_seq       ≝ *) (eval_LTL_LIN_ext_seq ?)
     95  (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st)).
Note: See TracChangeset for help on using the changeset viewer.