Changeset 1371 for src/joint


Ignore:
Timestamp:
Oct 14, 2011, 1:42:42 PM (8 years ago)
Author:
sacerdot
Message:

save_frame changed to accept also the formal/actual argument pairs, required
in the RTL semantics. The function returns now a res, but this could be fixed
with a dependent type for function call to disallow calling a function with the
wrong arguments.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1359 r1371  
    5151 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    5252 ; pop_frame: list beval → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    53  ; save_frame: call_dest p → state (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams)
     53   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
     54     type of arguments. To be fixed using a dependent type *)
     55 ; save_frame: paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    5456 }.
    5557
     
    286288        ! st ← pair_reg_move … st dst_src ;
    287289          ret ? 〈E0, next … l st〉
    288       | CALL_ID id argsno dest ⇒
     290      | CALL_ID id args dest ⇒
    289291        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    290292        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     
    292294          [ Internal fn ⇒
    293295            ! st ← save_ra … st l;
    294               let st ≝ save_frame … dest st in
    295               let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    296 (*+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
    297 + ALLOCARE LO STACK FRAME*)
    298               let l' ≝ joint_if_entry … fn in
     296            ! st ← save_frame … (joint_if_params … fn) args dest st ;
     297            let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
     298            let l' ≝ joint_if_entry … fn in
    299299             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
    300300          | External fn ⇒
Note: See TracChangeset for help on using the changeset viewer.