Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (7 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1451 r2286  
    44definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
    55definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
     6definition hw_arg_retrieve ≝
     7  λl,a.match a with
     8  [ Reg r ⇒ hw_reg_retrieve l r
     9  | Imm b ⇒ OK … b
     10  ].
    611
    7 definition ltl_lin_more_sem_params: ∀succT. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
    8  λsuccT.
    9  mk_more_sem_params ?
    10   unit it hw_register_env init_hw_register_env 0 it
    11    hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA)
    12     (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB)
    13     (λ_.hw_reg_store RegisterDPL) (λe.λ_.hw_reg_retrieve e RegisterDPL)
    14     (λ_.hw_reg_store RegisterDPH) (λe.λ_.hw_reg_retrieve e RegisterDPH)
    15      (λlocals,dest_src.
    16        match dest_src with
    17        [ from_acc reg ⇒
    18           do v ← hw_reg_retrieve locals RegisterA ;
    19           hw_reg_store reg v locals
    20        | to_acc reg ⇒
    21           do v ← hw_reg_retrieve locals reg ;
    22           hw_reg_store RegisterA v locals ]).
     12definition eval_registers_move ≝ λe,m.
     13match m with
     14[ from_acc r _ ⇒
     15  hw_reg_store r (hwreg_retrieve e RegisterA) e
     16| to_acc _ r ⇒
     17  hw_reg_store RegisterA (hwreg_retrieve e r) e
     18| int_to_reg r v ⇒
     19  hw_reg_store r v e
     20| int_to_acc _ v ⇒
     21  hw_reg_store RegisterA v e
     22].
    2323
    24 definition ltl_lin_sem_params: ∀succT. sem_params ≝
    25  λsuccT.mk_sem_params … (ltl_lin_more_sem_params succT).
    26 
    27 
    28 definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    29 definition ltl_lin_pop_frame:
    30  ∀succT,codeT,lookup.
    31  ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    32  state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
    33  λ_.λ_.λ_.λ_.λ_.λt.OK … t.
    34 definition ltl_lin_save_frame:
    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.
    37 
    38 (* The following implementation only works for functions that return 32 bits *)
    39 definition ltl_lin_result_regs:
    40  ∀succT,codeT,lookup.
    41  ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    42  state (ltl_lin_sem_params succT) → res (list Register) ≝
    43  λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
     24definition LTL_LIN_state : sem_state_params ≝
     25  mk_sem_state_params
     26 (* framesT ≝ *) unit
     27 (* empty_framesT ≝ *) it
     28 (* regsT ≝ *) hw_register_env
     29 (* empty_regsT ≝ *) init_hw_register_env.
    4430
    4531(*CSC: XXXX, for external functions only*)
    46 axiom ltl_lin_fetch_external_args: ∀succT.external_function → state (ltl_lin_sem_params succT) → res (list val).
    47 axiom ltl_lin_set_result: ∀succT.list val → state (ltl_lin_sem_params succT) → res (state (ltl_lin_sem_params succT)).
     32axiom ltl_lin_fetch_external_args: external_function → state LTL_LIN_state → res (list val).
     33axiom ltl_lin_set_result: list val → unit → state LTL_LIN_state → res (state LTL_LIN_state).
    4834
    49 definition 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. ⊥.
    51 @abs qed.
     35(* TODO (needs another bit to be added to hdw) *)
     36axiom eval_ltl_lin_seq : ltl_lin_seq → state LTL_LIN_state → IO io_out io_in (state LTL_LIN_state).
    5237
    53 definition ltl_lin_more_sem_params2:
    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).
    58  ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
    59  λsuccT,codeT,lookup,succ,fetch,pointer_of_label,globals.
    60   mk_more_sem_params2 …
    61    (mk_more_sem_params1 … (ltl_lin_more_sem_params …)
    62     succ (pointer_of_label …) (fetch globals) (load_ra …) (ltl_lin_result_regs …)
    63     ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    64     (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …).
    65 
    66 definition ltl_lin_fullexec ≝
    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)).
     38definition LTL_LIN_semantics ≝
     39  λF.mk_more_sem_unserialized_params LTL_LIN F
     40  (* st_pars            ≝ *) LTL_LIN_state
     41  (* acca_store_        ≝ *) (λ_.hw_reg_store RegisterA)
     42  (* acca_retrieve_     ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA)
     43  (* acca_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterA)
     44  (* accb_store_        ≝ *) (λ_.hw_reg_store RegisterB)
     45  (* accb_retrieve_     ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB)
     46  (* accb_arg_retrieve_ ≝ *) (λe.λ_.hw_reg_retrieve e RegisterB)
     47  (* dpl_store_         ≝ *) (λ_.hw_reg_store RegisterDPL)
     48  (* dpl_retrieve_      ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL)
     49  (* dpl_arg_retrieve_  ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPL)
     50  (* dph_store_         ≝ *) (λ_.hw_reg_store RegisterDPH)
     51  (* dph_retrieve_      ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH)
     52  (* dph_arg_retrieve_  ≝ *) (λe.λ_.hw_reg_retrieve e RegisterDPH)
     53  (* snd_arg_retrieve_  ≝ *) hw_arg_retrieve
     54  (* pair_reg_move_     ≝ *) eval_registers_move
     55  (* fetch_ra           ≝ *) (load_ra …)
     56  (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
     57  (* save_frame         ≝ *) (λp.λ_.λst.save_ra … st p)
     58  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
     59  (* fetch_external_args≝ *) ltl_lin_fetch_external_args
     60  (* set_result         ≝ *) ltl_lin_set_result
     61  (* call_args_for_main ≝ *) 0
     62  (* call_dest_for_main ≝ *) it
     63  (* read_result        ≝ *) (λ_.λ_.λ_.
     64  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
     65  (* eval_ext_seq       ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s)
     66  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     67  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     68  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
     69  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st).
Note: See TracChangeset for help on using the changeset viewer.