Commit ffc27e40 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Removing the PseudoAsm IR

parent 9d5f379c
......@@ -420,6 +420,22 @@ Fixpoint size_blocks (l: bblocks): Z :=
end
.
Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0.
Proof.
intros. destruct z; auto.
- contradict H. cbn. apply gt_irrefl.
- apply Zgt_pos_0.
- contradict H. cbn. apply gt_irrefl.
Qed.
Lemma size_positive (b:bblock): size b > 0.
Proof.
unfold size. destruct b as [hd bdy ex cor]. cbn.
destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega);
unfold non_empty_bblockb in cor; simpl in cor.
inversion cor.
Qed.
Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.
......
......@@ -160,6 +160,7 @@ Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity).
(* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *)
(** Alignment check for symbols *)
Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity).
Notation "a @@ b" := (app a b) (at level 49, right associativity).
(* The pop_bc and push_bc functions are used to adapt the output of some definitions
in bblocks format and avoid some redefinitions. *)
......@@ -1194,10 +1195,10 @@ Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instructio
*)
(* XXX: the simulation proof may be complex with this pattern. We may fix this later *)
Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control) (k:bblocks): bblocks :=
Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks :=
match non_empty_bblockb bdy ex with
| true => {| header := ll; body:= bdy; exit := ex |}::k
| false => k
| true => {| header := ll; body:= bdy; exit := ex |} :: nil
| false => {| header := ll; body:= Pnop::nil; exit := None |} :: nil
end.
Obligation 1.
rewrite <- Heq_anonymous. constructor.
......@@ -1225,32 +1226,50 @@ Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) :
| None => OK (nil, None)
end.
Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) (k:bblocks): res (list bblock) :=
Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
let stub := false in
do (bdy, ex) <- transl_exit f fb.(Machblock.exit);
do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy;
OK (cons_bblocks fb.(Machblock.header) bdy' ex k)
OK (cons_bblocks fb.(Machblock.header) bdy' ex)
.
Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks :=
Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) :=
match lmb with
| nil => OK nil
| mb :: lmb =>
do lb <- transl_block f mb (if Machblock.header mb then ep else false);
do lb' <- transl_blocks f lmb false;
OK (lb @@ lb')
end
.
(* match lmb with
| nil => OK nil
| mb :: lmb =>
do lb <- transl_blocks f lmb false;
transl_block f mb (if Machblock.header mb then ep else false) lb
end.
end. *)
(* OK (make_epilogue f ((Pret X0)::c nil))*)
(* Currently, we assume to be after the PseudoAsmblockproof.transf_program pass... *)
Program Definition make_prologue (f: Machblock.function) (k:bblocks) :=
Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
push_bc (storeptr_bc RA XSP f.(fn_retaddr_ofs) (pop_bc k)) k.
{| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::bi
storeptr_bc RA XSP f.(fn_retaddr_ofs) nil;
exit := None |} :: k.
(* Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
push_bc (storeptr_bc RA XSP f.(fn_retaddr_ofs) (pop_bc k)) k. *)
Definition transl_function (f: Machblock.function) : res Asmblock.function :=
do lb <- transl_blocks f f.(Machblock.fn_code) true;
OK (mkfunction f.(Machblock.fn_sig)
(make_prologue f lb)).
Definition transf_function (f: Machblock.function) : res Asmblock.function :=
do tf <- transl_function f;
if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
then Error (msg "code size exceeded")
else OK tf.
Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
transf_partial_fundef transl_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *)
......
......@@ -5,8 +5,8 @@ CURRENTLY A STUB !
Require Import Coqlib Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock IterList.
Require Import PseudoAsmblockproof Asmblockgen.
Require Import Op Locations Machblock Conventions Asmblock IterList.
Require Import Asmblockgen Asmblockgenproof0.
Module MB := Machblock.
Module AB := Asmblock.
......@@ -20,13 +20,8 @@ Proof.
intros. eapply match_transform_partial_program; eauto.
Qed.
Parameter next: MB.function -> Z -> Z.
Section PRESERVATION.
Lemma next_progress: forall (f:MB.function) (pos:Z), (pos < (next f pos))%Z.
Admitted.
Variable lk: aarch64_linker.
Variable prog: Machblock.program.
Variable tprog: Asmblock.program.
......@@ -38,15 +33,39 @@ Let tge := Genv.globalenv tprog.
Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs.
Lemma functions_bound_max_pos: forall fb f,
(*Lemma functions_bound_max_pos: forall fb f,
Genv.find_funct_ptr ge fb = Some (Internal f) ->
(max_pos next f) <= Ptrofs.max_unsigned.
Admitted.
Admitted.*)
Lemma transf_function_no_overflow:
forall f tf,
transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
Proof.
intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
omega.
Qed.
(** Existence of return addresses *)
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. eapply Asmblockgenproof0.return_address_exists; eauto.
- intros. monadInv H0.
destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. monadInv EQ. simpl.
exists x; exists true; split; auto.
repeat constructor.
- exact transf_function_no_overflow.
Qed.
Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop :=
Asmblockgenproof0.return_address_offset.
Lemma transf_program_correct:
forward_simulation (PseudoAsmblock.semantics next prog) (AB.semantics lk tprog).
forward_simulation (MB.semantics return_address_offset prog) (AB.semantics lk tprog).
Admitted.
End PRESERVATION.
......
(* *************************************************************)
(* *)
(* 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.
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.
\ No newline at end of file
......@@ -18,7 +18,7 @@
Require Import Recdef Coqlib Zwf Zbits.
Require Import Errors AST Integers Floats Op.
Require Import Locations Compopts.
Require Import Mach Asm Asmblock Asmblockgen Machblockgen PseudoAsmblock PseudoAsmblockproof PostpassScheduling.
Require Import Mach Asm Asmblock Asmblockgen Machblockgen PostpassScheduling.
Local Open Scope error_monad_scope.
......@@ -450,7 +450,6 @@ End Asmblock_TRANSF.
Definition transf_program (p: Mach.program) : res Asm.program :=
let mbp := Machblockgen.transf_program p in
do mbp' <- PseudoAsmblockproof.transf_program mbp;
do abp <- Asmblockgen.transf_program mbp';
do abp <- Asmblockgen.transf_program mbp;
do abp' <- (time "PostpassScheduling total oracle+verification" PostpassScheduling.transf_program) abp;
Asmblock_TRANSF.transf_program abp'.
......@@ -18,7 +18,7 @@
Require Import Coqlib Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Machblock Conventions PseudoAsmblock PseudoAsmblockproof Asm Asmblock.
Require Import Op Locations Machblock Conventions Asm Asmblock.
Require Machblockgenproof Asmblockgenproof PostpassSchedulingproof.
Require Import Asmgen.
Require Import Axioms.
......@@ -2281,7 +2281,6 @@ Local Open Scope linking_scope.
Definition block_passes :=
mkpass Machblockgenproof.match_prog
::: mkpass PseudoAsmblockproof.match_prog
::: mkpass Asmblockgenproof.match_prog
::: mkpass PostpassSchedulingproof.match_prog
::: mkpass Asmblock_PRESERVATION.match_prog
......@@ -2295,27 +2294,27 @@ Proof.
intros p tp H.
unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
inversion_clear H. apply bind_inversion in H1. destruct H1.
inversion_clear H. apply bind_inversion in H2. destruct H2. inversion_clear H.
inversion_clear H.
unfold Compopts.time in *. remember (Machblockgen.transf_program p) as mbp.
unfold match_prog; simpl.
exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
exists x; split. apply PseudoAsmblockproof.transf_program_match; auto.
exists x0; split. apply Asmblockgenproof.transf_program_match; auto.
exists x1; split. apply PostpassSchedulingproof.transf_program_match; auto.
exists x; split. apply Asmblockgenproof.transf_program_match; auto.
exists x0; split. apply PostpassSchedulingproof.transf_program_match; auto.
exists tp; split. apply Asmblock_PRESERVATION.transf_program_match; auto. auto.
Qed.
(** Return Address Offset *)
Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop :=
Machblockgenproof.Mach_return_address_offset (PseudoAsmblockproof.rao Asmblockgenproof.next).
Machblockgenproof.Mach_return_address_offset (Asmblockgenproof.return_address_offset).
Lemma return_address_exists:
forall f sg ros c, is_tail (Mach.Mcall sg ros :: c) f.(Mach.fn_code) ->
exists ra, return_address_offset f c ra.
Proof.
intros; eapply Machblockgenproof.Mach_return_address_exists; eauto.
Admitted.
intros; unfold return_address_offset; eapply Machblockgenproof.Mach_return_address_exists; eauto.
intros; eapply Asmblockgenproof.return_address_exists; eauto.
Qed.
Section PRESERVATION.
......@@ -2329,28 +2328,19 @@ Theorem transf_program_correct:
forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
Proof.
unfold match_prog in TRANSF. simpl in TRANSF.
inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H. inv H4. inv H.
inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H.
eapply compose_forward_simulations.
{ exploit Machblockgenproof.transf_program_correct; eauto. }
eapply compose_forward_simulations.
+ apply PseudoAsmblockproof.transf_program_correct; eauto.
- intros; apply Asmblockgenproof.next_progress.
- intros. eapply Asmblockgenproof.functions_bound_max_pos; eauto.
{ intros.
unfold Genv.symbol_address.
erewrite <- PostpassSchedulingproof.symbols_preserved; eauto.
erewrite Asmblock_PRESERVATION.symbol_high_low; eauto.
reflexivity.
}
+ eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
+ apply Asmblockgenproof.transf_program_correct; eauto.
{ intros.
unfold Genv.symbol_address.
erewrite <- PostpassSchedulingproof.symbols_preserved; eauto.
erewrite Asmblock_PRESERVATION.symbol_high_low; eauto.
reflexivity.
}
eapply compose_forward_simulations.
+ eapply compose_forward_simulations.
- apply PostpassSchedulingproof.transf_program_correct; eauto.
- apply Asmblock_PRESERVATION.transf_program_correct; eauto.
Qed.
......
......@@ -843,8 +843,8 @@ fi
if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling
cat >> Makefile.config <<EOF
ARCHDIRS=$arch
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.v\\
Asmblock.v Asmblockgen.v Asmblockgenproof.v Asm.v Asmblockprops.v\\
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v \\
Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof.v Asm.v Asmblockprops.v\\
ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
Asmblockdeps.v\\
AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment