path: root/aarch64/Asmblockgenproof0.v

(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Cyril Six          Kalray                         *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

(** * "block" version of Asmgenproof0

    This module is largely adapted from Asmgenproof0.v of the other backends
    It needs to stand apart because of the block structure, and the distinction control/basic that there isn't in the other backends
    It has similar definitions than Asmgenproof0, but adapted to this new structure *)

Require Import Coqlib.
Require Intv.
Require Import AST.
Require Import Errors.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Locations.
Require Import Machblock.
Require Import Asmblock.
Require Import Asmblockgen.
Require Import Conventions1.
Require Import Axioms.
Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *)
Require Import Asmblockprops.

Module MB:=Machblock.
Module AB:=Asmblock.

(** * Agreement between Mach registers and processor registers *)

Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree {
  agree_sp: rs#SP = sp;
  agree_sp_def: sp <> Vundef;
  agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r))
}.

Lemma agree_exten:
  forall ms sp rs rs',
  agree ms sp rs ->
  (forall r, data_preg r = true -> rs'#r = rs#r) ->
  agree ms sp rs'.
Proof.
  intros. destruct H. split; auto.
  rewrite H0; auto. auto.
  intros. rewrite H0; auto. apply preg_of_data.
Qed.

Lemma preg_val:
  forall ms sp rs r, agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r).
Proof.
  intros. destruct H. auto.
Qed.

Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
  | code_tail_0: forall c,
      code_tail 0 c c
  | code_tail_S: forall pos bi c1 c2,
      code_tail pos c1 c2 ->
      code_tail (pos + (size bi)) (bi :: c1) c2.
      
Lemma code_tail_pos:
  forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
Proof.
  induction 1. omega. generalize (size_positive bi); intros; omega.
Qed.

Lemma find_bblock_tail:
  forall c1 bi c2 pos,
  code_tail pos c1 (bi :: c2) ->
  find_bblock pos c1 = Some bi.
Proof.
  induction c1; simpl; intros.
  inversion H.  
  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
  destruct (zeq pos 0). subst pos.
  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
  inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
  eauto.
Qed.

Local Hint Resolve code_tail_0 code_tail_S: core.

Lemma code_tail_next:
  forall fn ofs c0,
  code_tail ofs fn c0 ->
  forall bi c1, c0 = bi :: c1 -> code_tail (ofs + (size bi)) fn c1.
Proof.
  induction 1; intros.
  - subst; eauto.
  - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
    omega.
Qed.

Lemma size_blocks_pos c: 0 <= size_blocks c.
Proof.
  induction c as [| a l ]; simpl; try omega.
  generalize (size_positive a); omega.
Qed.

Remark code_tail_positive:
  forall fn ofs c,
  code_tail ofs fn c -> 0 <= ofs.
Proof.
  induction 1; intros; simpl.
  - omega.
  - generalize (size_positive bi). omega.
Qed.

Remark code_tail_size:
  forall fn ofs c,
  code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c.
Proof.
  induction 1; intros; simpl; try omega.
Qed.

Remark code_tail_bounds fn ofs c:
  code_tail ofs fn c -> 0 <= ofs <= size_blocks fn.
Proof.
  intro H; 
  exploit code_tail_size; eauto.
  generalize (code_tail_positive _ _ _ H), (size_blocks_pos c).
  omega.
Qed.

Local Hint Resolve code_tail_next: core.

Lemma code_tail_next_int:
  forall fn ofs bi c,
  size_blocks fn <= Ptrofs.max_unsigned ->
  code_tail (Ptrofs.unsigned ofs) fn (bi :: c) ->
  code_tail (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bi)))) fn c.
Proof.
  intros. 
  exploit code_tail_size; eauto.
  simpl; generalize (code_tail_positive _ _ _ H0), (size_positive bi), (size_blocks_pos c).
  intros.
  rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr.
  - rewrite Ptrofs.unsigned_repr; eauto.
    omega.
  - rewrite Ptrofs.unsigned_repr; omega.
Qed.

(** Predictor for return addresses in generated Asm code.

  The [return_address_offset] predicate defined here is used in the
  semantics for Mach to determine the return addresses that are
  stored in activation records. *)

(** 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 Asm code obtained by translating the
  code of [f]. Graphically:
<<
     Mach function f    |--------- Mcall ---------|
         Mach code c    |                |--------|
                        |                 \        \
                        |                  \        \
                        |                   \        \
     Asm code           |                    |--------|
     Asm function       |------------- Pcall ---------|

                        <-------- ofs ------->
>>
*)

Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : Prop :=
  forall tf  tc,
  transf_function f = OK tf ->
  transl_blocks f c false = OK tc ->
  code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc.

Lemma transl_blocks_tail:
  forall f c1 c2, is_tail c1 c2 ->
  forall tc2 ep2, transl_blocks f c2 ep2 = OK tc2 ->
  exists tc1, exists ep1, transl_blocks f c1 ep1 = OK tc1 /\ is_tail tc1 tc2.
Proof.
  induction 1; simpl; intros.
  exists tc2; exists ep2; split; auto with coqlib.
  monadInv H0. exploit IHis_tail; eauto. intros (tc1 & ep1 & A & B).
  exists tc1; exists ep1; split. auto.
  eapply is_tail_trans with x0; eauto with coqlib.
Qed.

Lemma is_tail_code_tail:
  forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1.
Proof.
  induction 1; eauto.
  destruct IHis_tail; eauto. 
Qed.

Section RETADDR_EXISTS.

Hypothesis transf_function_inv:
  forall f tf, transf_function f = OK tf ->
  exists tc ep, transl_blocks f (Machblock.fn_code f) ep = OK tc /\ is_tail tc (fn_blocks tf).

Hypothesis transf_function_len:
  forall f tf, transf_function f = OK tf -> size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned.


Lemma return_address_exists:
  forall b f c, is_tail (b :: c) f.(MB.fn_code) ->
  exists ra, return_address_offset f c ra.
Proof.
  intros. destruct (transf_function f) as [tf|] eqn:TF.
  + exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1).
    exploit transl_blocks_tail; eauto. intros (tc2 & ep2 & TR2 & TL2).
    monadInv TR2.
    assert (TL3: is_tail x0 (fn_blocks tf)).
    { apply is_tail_trans with tc1; auto. 
      apply is_tail_trans with (x++x0); auto. eapply is_tail_app.
    }
    exploit is_tail_code_tail. eexact TL3. intros [ofs CT].
    exists (Ptrofs.repr ofs). red; intros.
    rewrite Ptrofs.unsigned_repr. congruence.
    exploit code_tail_bounds; eauto.
    intros; apply transf_function_len in TF. omega.
  + exists Ptrofs.zero; red; intros. congruence.
Qed.

End RETADDR_EXISTS.

(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points
  within the Asmblock code generated by translating Machblock function [f],
  and [tc] is the tail of the generated code at the position corresponding
  to the code pointer [pc]. *)

Inductive transl_code_at_pc (ge: MB.genv):
    val -> block -> MB.function -> MB.code -> bool -> AB.function -> AB.bblocks -> Prop :=
  transl_code_at_pc_intro:
    forall b ofs f c ep tf tc,
    Genv.find_funct_ptr ge b = Some(Internal f) ->
    transf_function f = Errors.OK tf ->
    transl_blocks f c ep = OK tc ->
    code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc ->
    transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc.

Remark code_tail_no_bigger:
  forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
Proof.
  induction 1; simpl; omega.
Qed.

Remark code_tail_unique:
  forall fn c pos pos',
  code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
Proof.
  induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
  f_equal. eauto.
Qed.

Lemma return_address_offset_correct:
  forall ge b ofs fb f c tf tc ofs',
  transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc ->
  return_address_offset f c ofs' ->
  ofs' = ofs.
Proof.
  intros. inv H. red in H0.
  exploit code_tail_unique. eexact H12. eapply H0; eauto. intro.
  rewrite <- (Ptrofs.repr_unsigned ofs).
  rewrite <- (Ptrofs.repr_unsigned ofs').
  congruence.
Qed.

(** * Properties of the Machblock call stack *)

Section MATCH_STACK.

Variable ge: MB.genv.

Inductive match_stack: list MB.stackframe -> Prop :=
  | match_stack_nil:
      match_stack nil
  | match_stack_cons: forall fb sp ra c s f tf tc,
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      transl_code_at_pc ge ra fb f c false tf tc ->
      sp <> Vundef ->
      match_stack s ->
      match_stack (Stackframe fb sp ra c :: s).

Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
Proof.
  induction 1; simpl.
  unfold Vnullptr; destruct Archi.ptr64; congruence.
  auto.
Qed.

Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef.
Proof.
  induction 1; simpl.
  unfold Vnullptr; destruct Archi.ptr64; congruence.
  inv H0. congruence.
Qed.

Lemma lessdef_parent_sp:
  forall s v,
  match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
Proof.
  intros. inv H0. auto. exploit parent_sp_def; eauto. tauto.
Qed.

Lemma lessdef_parent_ra:
  forall s v,
  match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s.
Proof.
  intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
Qed.

End MATCH_STACK.