Changeset 3255 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
May 8, 2013, 4:53:31 PM (7 years ago)
Author:
tranquil
Message:
  • dropped newframe and delframe (to be integrated in calls and returns

in the semantics), as they were too wild for the proof of ERTL to LTL

  • ERTL now has a policy on what hardware registers can be written or

read

  • Rearranged special hardware registers: dropped STS, ST2 and ST3, and

moved DPL and DPH out of RegistersRets?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r3145 r3255  
    304304definition translate_step:
    305305  ∀globals,fn.nat → ∀after : valuation register_lattice.
    306   coloured_graph (livebefore globals fn after) →
     306  coloured_graph (interferes globals fn after) →
    307307  ℕ → label → joint_step ERTL globals → bind_step_block LTL globals ≝
    308308  λglobals,fn,localss,after,grph,stack_sz,lbl,s.
     
    313313    | Imm b ⇒ arg_decision_imm b
    314314    ] in
    315   let carry_lives_after ≝ hlives RegisterCarry (after lbl) in
     315  let carry_lives_after ≝ h_in_lattice RegisterCarry (after lbl) in
    316316  let move ≝ move globals localss carry_lives_after in
    317317  if eliminable_step … (after lbl) s then ([ ] : step_block LTL globals) else
     
    368368    | extension_seq ext ⇒
    369369      match ext with
    370       [ ertl_new_frame ⇒ newframe ? stack_sz
    371       | ertl_del_frame ⇒ delframe ? stack_sz
    372       | ertl_frame_size r ⇒
     370      [ ertl_frame_size r ⇒
    373371        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    374372      ]
     
    395393
    396394definition translate_fin_step:
    397   ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
    398   λglobals,lbl,s.
    399   bret … (〈[ ],
    400   match s with
    401   [ RETURN ⇒ RETURN ?
    402   | GOTO l ⇒ GOTO ? l
     395  ∀globals.ℕ → label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
     396  λglobals,stack_sz,lbl,s.
     397  bret … (match s with
     398  [ RETURN ⇒ 〈delframe ? stack_sz, RETURN ?〉
     399  | GOTO l ⇒ 〈[ ], GOTO ? l〉
    403400  | TAILCALL abs _ _ ⇒ Ⓧabs
    404   ]).
     401  ]).
    405402
    406403definition translate_data :
     
    420417    (* init_params ≝ *) it
    421418    (* init_stack_size ≝ *) stack_sz
    422     (* added_prologue ≝ *) [ ]
     419    (* added_prologue ≝ *) (newframe ? stack_sz)
    423420    (* new_regs ≝ *) [ ]
    424421    (* f_step ≝ *) (translate_step ? int_fun (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz)
    425     (* f_fin ≝ *) (translate_fin_step globals)
     422    (* f_fin ≝ *) (translate_fin_step globals stack_sz)
    426423    ????).
    427424@hide_prf
Note: See TracChangeset for help on using the changeset viewer.