Library Asmgenretaddr

Predictor for return addresses in generated PPC code.

The return_address_offset predicate defined here is used in the concrete semantics for Mach (module Machconcr) to determine the return addresses that are stored in activation records.





Require Import Coqlib.

Require Import Maps.

Require Import AST.

Require Import Integers.

Require Import Floats.

Require Import Values.

Require Import Mem.

Require Import Globalenvs.

Require Import Op.

Require Import Locations.

Require Import Mach.

Require Import Asm.

Require Import Asmgen.

The ``code tail'' of an instruction list c is the list of instructions starting at PC pos.





Inductive code_tail: Z -> code -> code -> Prop :=

  | code_tail_0: forall c,

      code_tail 0 c c

  | code_tail_S: forall pos i c1 c2,

      code_tail pos c1 c2 ->

      code_tail (pos + 1) (i :: c1) c2.




Lemma code_tail_pos:

  forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.

Consider a Mach function f and a sequence c of Mach instructions representing the Mach code that remains to be executed after a function call returns. The predicate return_address_offset f c ofs holds if ofs is the integer offset of the PPC instruction following the call in the PPC code obtained by translating the code of f. Graphically:

     Mach function f    |--------- Mcall ---------|
         Mach code c    |                |--------|
                        |                 \        \
                        |                  \        \
                        |                   \        \
     PPC code           |                    |--------|
     PPC function       |--------------- Pbl ---------|

                        <-------- ofs ------->





Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop :=

  | return_address_offset_intro:

      forall c f ofs,

      code_tail ofs (transl_function f) (transl_code f c) ->

      return_address_offset f c (Int.repr ofs).

We now show that such an offset always exists if the Mach code c is a suffix of f.(fn_code). This holds because the translation from Mach to PPC is compositional: each Mach instruction becomes zero, one or several PPC instructions, but the order of instructions is preserved.





Lemma is_tail_code_tail:

  forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1.






Hint Resolve is_tail_refl: ppcretaddr.




Ltac IsTail :=

  auto with ppcretaddr;

  match goal with

  | [ |- is_tail _ (_ :: _) ] => constructor; IsTail

  | [ |- is_tail _ (match ?x with true => _ | false => _ end) ] => destruct x; IsTail

  | [ |- is_tail _ (match ?x with left _ => _ | right _ => _ end) ] => destruct x; IsTail

  | [ |- is_tail _ (match ?x with nil => _ | _ :: _ => _ end) ] => destruct x; IsTail

  | [ |- is_tail _ (match ?x with Tint => _ | Tfloat => _ end) ] => destruct x; IsTail

  | [ |- is_tail _ (?f _ _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail

  | [ |- is_tail _ (?f _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail

  | [ |- is_tail _ (?f _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail

  | [ |- is_tail _ (?f _ _ _ ?k) ] => apply is_tail_trans with k; IsTail

  | [ |- is_tail _ (?f _ _ ?k) ] => apply is_tail_trans with k; IsTail

  | _ => idtac

  end.




Lemma loadimm_tail:

  forall r n k, is_tail k (loadimm r n k).



Hint Resolve loadimm_tail: ppcretaddr.




Lemma addimm_tail:

  forall r1 r2 n k, is_tail k (addimm r1 r2 n k).



Hint Resolve addimm_tail: ppcretaddr.




Lemma andimm_tail:

  forall r1 r2 n k, is_tail k (andimm r1 r2 n k).



Hint Resolve andimm_tail: ppcretaddr.




Lemma orimm_tail:

  forall r1 r2 n k, is_tail k (orimm r1 r2 n k).



Hint Resolve orimm_tail: ppcretaddr.




Lemma xorimm_tail:

  forall r1 r2 n k, is_tail k (xorimm r1 r2 n k).



Hint Resolve xorimm_tail: ppcretaddr.




Lemma loadind_tail:

  forall base ofs ty dst k, is_tail k (loadind base ofs ty dst k).



Hint Resolve loadind_tail: ppcretaddr.




Lemma storeind_tail:

  forall src base ofs ty k, is_tail k (storeind src base ofs ty k).



Hint Resolve storeind_tail: ppcretaddr.




Lemma floatcomp_tail:

  forall cmp r1 r2 k, is_tail k (floatcomp cmp r1 r2 k).



Hint Resolve floatcomp_tail: ppcretaddr.




Lemma transl_cond_tail:

  forall cond args k, is_tail k (transl_cond cond args k).



Hint Resolve transl_cond_tail: ppcretaddr.




Lemma transl_op_tail:

  forall op args r k, is_tail k (transl_op op args r k).



Hint Resolve transl_op_tail: ppcretaddr.




Lemma transl_load_store_tail:

  forall mk1 mk2 addr args k,

  is_tail k (transl_load_store mk1 mk2 addr args k).



Hint Resolve transl_load_store_tail: ppcretaddr.




Lemma transl_instr_tail:

  forall f i k, is_tail k (transl_instr f i k).



Hint Resolve transl_instr_tail: ppcretaddr.




Lemma transl_code_tail: 

  forall f c1 c2, is_tail c1 c2 -> is_tail (transl_code f c1) (transl_code f c2).






Lemma return_address_exists:

  forall f c, is_tail c f.(fn_code) ->

  exists ra, return_address_offset f c ra.