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

(** Common definition and proofs on Asmblock required by various modules *)

Require Import Coqlib.
Require Import Integers.
Require Import Memory.
Require Import Globalenvs.
Require Import Values.
Require Import Asmblock.
Require Import Axioms.

Definition bblock_simu (lk: aarch64_linker) (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
  forall rs m rs' m' t,
    exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk ge f bb' rs m t rs' m'.
    
Definition bblock_simu_aux (lk: aarch64_linker) (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
  forall rs m,
    bbstep lk ge f bb rs m <> Stuck ->
    bbstep lk ge f bb rs m = bbstep lk ge f bb' rs m.

Hint Extern 2 (_ <> _) => congruence: asmgen.

Lemma preg_of_data:
  forall r, data_preg (preg_of r) = true.
Proof.
  intros. destruct r; reflexivity.
Qed.

Lemma dreg_of_data:
  forall r, data_preg (dreg_of r) = true.
Proof.
  intros. destruct r; reflexivity.
Qed.
Hint Resolve preg_of_data dreg_of_data: asmgen.

Lemma data_diff:
  forall r r',
  data_preg r = true -> data_preg r' = false -> r <> r'.
Proof.
  congruence.
Qed.
Hint Resolve data_diff: asmgen.

Lemma preg_of_not_PC:
  forall r, preg_of r <> PC.
Proof.
  intros. apply data_diff; auto with asmgen.
Qed.

Lemma preg_of_not_SP:
  forall r, preg_of r <> SP.
Proof.
  intros. unfold preg_of; destruct r; simpl; try discriminate.
Qed.

Ltac desif :=
  repeat match goal with
  | [ |- context[ if ?f then _ else _ ] ] => destruct f
  end.
  
Ltac decomp :=
  repeat match goal with
  | [ |- context[ match (?rs ?r) with | _ => _ end ] ] => destruct (rs r)
  end.

Ltac Simplif :=
  ((desif)
  || (try unfold compare_long)
  || (try unfold compare_int)
  || (try unfold compare_float)
  || (try unfold compare_single)
  || decomp
  || (rewrite Pregmap.gss)
  || (rewrite Pregmap.gso by eauto with asmgen)
  ); auto with asmgen.

Ltac Simpl := repeat Simplif.

Section EPC.

Variable lk: aarch64_linker.

(* For Asmblockgenproof0 *)

Theorem exec_basic_instr_pc:
  forall ge b rs1 m1 rs2 m2,
  exec_basic lk ge b rs1 m1 = Next rs2 m2 ->
  rs2 PC = rs1 PC.
Proof.
  intros. destruct b; try destruct i; try destruct i; try destruct ld; try destruct ld;
  try destruct st; try destruct st; try destruct a.
  all: try (inv H; simpl in *; auto; Simpl).
  all: try (try unfold exec_load_rd_a in H1; try destruct (Mem.loadv _ _ _); inv H1; Simpl).
  all: try (try unfold exec_load_double in H0; destruct (Mem.loadv _ _ _); simpl in *;
            try destruct (Mem.loadv _ _ _); simpl in *; inv H0; Simpl).
  all: try (try unfold exec_store_rs_a in H0; try destruct (Mem.storev _ _ _); inv H0; auto; Simpl).
  all: try (try unfold exec_store_double in H1; destruct (Mem.storev _ _ _); simpl in *;
            try destruct (Mem.storev _ _ _); simpl in *; inv H1; auto; Simpl).
  - (* alloc *)
    destruct (Mem.alloc _ _ _); destruct (Mem.store _ _ _); inv H1; auto; Simpl.
  - (* free *)
    destruct (rs1 SP); try discriminate; destruct (Mem.free _ _ _ _); inv H1; Simpl.
Qed.

End EPC.