Ignore:
Timestamp:
Dec 5, 2012, 6:57:16 PM (8 years ago)
Author:
tranquil
Message:

added FCOND in LIN, and rewritten linearise so that it never adds a GOTO after a COND (writes in FCOND instead)
LIN to ASM is broken atm

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2529 r2532  
    55include "joint/Joint.ma".
    66include "ASM/I8051bis.ma".
    7 include "common/extraGlobalenvs.ma".
     7(* include "common/extraGlobalenvs.ma". *)
    88
    99(* CSC: external functions never fail (??) and always return something of the
     
    162162  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
    163163  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    164 
     164 
    165165  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    166166  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
     
    177177
    178178  (* from now on, parameters that use the type of functions *)
    179   ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval)
     179  ; block_of_call : ∀globals.genv_t (fundef (F globals)) → call_spec uns_pars →
     180      state st_pars →  res (Σbl.block_region bl = Code)
     181  ; read_result: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars →
     182      state st_pars → res (list beval)
    180183  ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars →
    181184    ident → F globals (* current *) → state st_pars → res (state st_pars)
     
    374377  ] (refl …).
    375378
    376 definition block_of_call ≝ λp:sem_params.λglobals.
    377   λge: genv_t (joint_function p globals).λst : state p.λf.
    378   ! bl ← match f with
    379     [ inl id ⇒ opt_to_res … [MSG BadFunction; CTX … id] (find_symbol … ge id)
    380     | inr addr ⇒
    381       ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
    382       ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
    383       ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
    384       if eq_bv … (bv_zero …) (offv (poff ptr)) then
    385         return (pblock … ptr)
    386       else
    387         Error … [MSG BadFunction; MSG BadPointer]
    388     ] ;
    389   opt_to_res … [MSG BadFunction; MSG BadPointer] (code_block_of_block bl).
     379(* to be used in implementations *)
     380definition block_of_call_id ≝  λF.λsp:sem_state_params.
     381  λge: genv_t F.λid.λst:state sp.
     382  opt_to_res … [MSG BadFunction; CTX … id] (
     383    ! bl ← find_symbol … ge id;
     384    code_block_of_block bl).
     385 
     386definition block_of_call_id_ptr ≝ λp,F.λsp : sem_unserialized_params p F.
     387  λglobals.λge: genv_t (F globals).λf.λst : state sp.
     388  match f with
     389  [ inl id ⇒ block_of_call_id … ge id st
     390  | inr addr ⇒
     391    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
     392    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
     393    ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ;
     394    if eq_bv … (bv_zero …) (offv (poff ptr)) then
     395      opt_to_res … [MSG BadFunction; MSG BadPointer]
     396        (code_block_of_block (pblock … ptr))
     397    else
     398      Error … [MSG BadFunction; MSG BadPointer]
     399  ].
    390400
    391401(* Paolo: why external calls do not need args?? *)
     
    488498λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
    489499λst : state_pc p.
    490 ! bl ← block_of_call … ge st f : IO ???;
     500! bl ← block_of_call … ge f st : IO ???;
    491501! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
    492502match fd with
     
    523533    | COND a l ⇒ return st
    524534    ]
    525   | final s ⇒ return st
     535  | _ ⇒ return st
    526536  ].
    527537
     
    538548λcurr_fn : joint_closed_internal_function ??.
    539549λst : state_pc p.
    540 ! bl ← block_of_call … ge st f : IO ???;
     550! bl ← block_of_call … ge f st : IO ???;
    541551! 〈i, fd〉 ← fetch_function … ge bl : IO ???;
    542552match fd with
     
    557567  IO io_out io_in (state_pc p) ≝
    558568  λp,g,ge,curr_id,curr_fn,s,st.
    559   match s with
     569  match s return λ_.IO ??? with
    560570  [ sequential s nxt ⇒
    561571    match s return λ_.IO ??? with
     
    577587      eval_tailcall … ge f args curr_id curr_fn st
    578588    ]
     589  | FCOND _ a lbltrue lblfalse ⇒
     590    ! v ← acca_retrieve … st a ;
     591    ! b ← bool_of_beval … v ;
     592    if b then
     593      goto … ge lbltrue st
     594    else
     595      goto … ge lblfalse st
    579596  ].
    580597
Note: See TracChangeset for help on using the changeset viewer.