Changeset 3037 for src/joint/Joint.ma


Ignore:
Timestamp:
Mar 29, 2013, 5:19:53 PM (7 years ago)
Author:
tranquil
Message:
  • ADDRESS joint instruction now has also an offset
  • corrected call to pointer (needed to clear the accumulator)
  • now we make sure globals contain also function names

LINToASM will be fixed in an upcoming commit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2946 r3037  
    119119  | POP: acc_a_reg p → joint_seq p globals
    120120  | PUSH: acc_a_arg p → joint_seq p globals
    121   | ADDRESS: ∀i: ident. i ∈ globals → dpl_reg p → dph_reg p → joint_seq p globals
     121  | ADDRESS: ∀i: ident. i ∈ globals → Word → dpl_reg p → dph_reg p → joint_seq p globals
    122122  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
    123123  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
     
    139139| POP r ⇒ acc_a_regs … functs r
    140140| PUSH r ⇒ acc_a_args … functs r
    141 | ADDRESS i prf r1 r2 ⇒ (dpl_regs … functs r1) @ (dph_regs … functs r2)
     141| ADDRESS _ _ _ r1 r2 ⇒ (dpl_regs … functs r1) @ (dph_regs … functs r2)
    142142| OPACCS o r1 r2 r3 r4 ⇒ (acc_a_regs … functs r1) @ (acc_b_regs … functs r2)
    143143       @ (acc_a_args … functs r3) @ (acc_b_args … functs r4)
     
    592592     (*(pi1 … (joint_if_exit … p))*).
    593593
    594 definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
     594definition joint_function ≝ λp,functions,globals.
     595  fundef (joint_closed_internal_function p (globals @ functions)).
    595596
    596597record joint_program (p : params) : Type[0] ≝
    597 { joint_prog :> program (joint_function p) (list init_data)
     598{ jp_functions : list ident
     599; joint_prog :> program (joint_function p jp_functions) (list init_data)
    598600; init_cost_label : costlabel
    599601(* here we can have global invariants (like injectivity of cost labels) *)
     602; functions_ok : (prog_funct_names … joint_prog) = jp_functions
    600603}.
     604
     605definition prog_names ≝ λpars.λp : joint_program pars.
     606  prog_var_names … p @ jp_functions … p.
     607
     608lemma transform_prog_funct_names : ∀A,B,V.∀p : program A V.
     609∀trans: ∀vars.A vars → B vars.
     610prog_funct_names … (transform_program A B V p trans) =
     611prog_funct_names … p.
     612#A #B #V * #vars #functs #main #trans elim functs //
     613* #id #f #tl #IH whd in ⊢ (??%%); @eq_f @IH qed.
     614
     615definition transform_joint_program :
     616 ∀src,dst : params.
     617 (∀globals.joint_closed_internal_function src globals →
     618  joint_closed_internal_function dst globals) →
     619 joint_program src → joint_program dst ≝
     620 λsrc,dst,trans,prog_in.
     621 mk_joint_program dst
     622  (jp_functions … prog_in)
     623  (transform_program … prog_in (λvars.transf_fundef … (trans ?)))
     624  (init_cost_label … prog_in)
     625  ?.
     626@hide_prf
     627>transform_prog_funct_names @functions_ok qed.
    601628
    602629(* The cost model for stack consumption *)
Note: See TracChangeset for help on using the changeset viewer.