diff options
-rw-r--r-- | aarch64/Asmblockgenproof.v | 47 | ||||
-rw-r--r-- | aarch64/Asmgen.v | 17 | ||||
-rw-r--r-- | aarch64/Asmgenproof.v | 127 | ||||
-rwxr-xr-x | configure | 5 | ||||
-rw-r--r-- | kvx/lib/PseudoAsmblock.v | 7 | ||||
-rw-r--r-- | kvx/lib/PseudoAsmblockproof.v | 2 |
6 files changed, 198 insertions, 7 deletions
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index bcd4495f..0e90cbf5 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -1,3 +1,50 @@ +(** Correctness proof for aarch64/Asmblock generation: main proof. +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. + +Module MB := Machblock. +Module AB := Asmblock. + +Definition match_prog (p: MB.program) (tp: AB.program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transf_program p = OK tp -> match_prog p tp. +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 prog: Machblock.program. +Variable tprog: Asmblock.program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +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. + +Lemma transf_program_correct: + forward_simulation (PseudoAsmblock.semantics next prog) (AB.semantics tprog). +Admitted. + +End PRESERVATION. + + (* ORIGINAL aarch64/Asmgenproof file that needs to be adapted (* *********************************************************************) diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index f81f37d6..b0fec14b 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -16,11 +16,16 @@ Require Import Recdef Coqlib Zwf Zbits. Require Import Errors AST Integers Floats Op. -Require Import Locations Asmblock Asm. +Require Import Locations Compopts. +Require Import Mach Asm Asmblock Asmblockgen Machblockgen PseudoAsmblock PseudoAsmblockproof. + + +Local Open Scope error_monad_scope. (** * Translation from Asmblock to assembly language - Inspired from the KVX backend. *) + Inspired from the KVX backend (see kvx/Asm.v and kvx/Asmgen.v) *) +Module Asmblock_TRANSF. (* STUB *) Definition transf_function (f: Asmblock.function) : res Asm.function := @@ -31,3 +36,11 @@ Definition transf_fundef (f: Asmblock.fundef) : res Asm.fundef := Definition transf_program (p: Asmblock.program) : res Asm.program := transform_partial_program transf_fundef p. + +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'; + Asmblock_TRANSF.transf_program abp. diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index e69de29b..b9f931c0 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -0,0 +1,127 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Justus Fasse UGA, 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. *) +(* *) +(* *************************************************************) + +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. +Require Machblockgenproof Asmblockgenproof. +Require Import Asmgen. + + +Module Asmblock_PRESERVATION. + +Import Asmblock_TRANSF. + +Definition match_prog (p: Asmblock.program) (tp: Asm.program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + intros. eapply match_transform_partial_program; eauto. +Qed. + +Section PRESERVATION. + +Variable prog: Asmblock.program. +Variable tprog: Asm.program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma transf_program_correct: + forward_simulation (Asmblock.semantics prog) (Asm.semantics tprog). +Admitted. (* TODO *) + +End PRESERVATION. + +End Asmblock_PRESERVATION. + + +Local Open Scope linking_scope. + +Definition block_passes := + mkpass Machblockgenproof.match_prog + ::: mkpass PseudoAsmblockproof.match_prog + ::: mkpass Asmblockgenproof.match_prog + ::: mkpass Asmblock_PRESERVATION.match_prog + ::: pass_nil _. + +Definition match_prog := pass_match (compose_passes block_passes). + +Lemma transf_program_match: + forall p tp, Asmgen.transf_program p = OK tp -> match_prog p tp. +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. inversion H2. 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 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). + +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. + +Section PRESERVATION. + +Variable prog: Mach.program. +Variable tprog: Asm.program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +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. + 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. + + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto. + apply Asmblock_PRESERVATION.transf_program_correct. eauto. +Qed. + +End PRESERVATION. + +Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes). + +(*******************************************) +(* Stub actually needed by driver/Compiler *) + +Module Asmgenproof0. + +Definition return_address_offset := return_address_offset. + +End Asmgenproof0. + @@ -845,10 +845,9 @@ if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling cat >> Makefile.config <<EOF ARCHDIRS=$arch kvx/lib kvx/abstractbb kvx/abstractbb/Impure BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.v ForwardSimulationBlock.v\\ - AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\ + AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v\\ ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v\\ - Asmblock.v Asmblockgen.v\\ - Asmgenproof.v # TODO: CHANGE THIS + Asmblock.v Asmblockgen.v Asmblockgenproof.v # TODO: UPDATE THIS EOF fi diff --git a/kvx/lib/PseudoAsmblock.v b/kvx/lib/PseudoAsmblock.v index 336e315c..b33ea1bd 100644 --- a/kvx/lib/PseudoAsmblock.v +++ b/kvx/lib/PseudoAsmblock.v @@ -27,10 +27,16 @@ Module Pregmap := EMap(PregEq). Definition regset := Pregmap.t val. +Module AsmNotations. + (* Declare Scope asm. *) Notation "a # b" := (a b) (at level 1, only parsing) : asm. Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. +Open Scope asm. + +End AsmNotations. +Import AsmNotations. Definition to_Machrs (rs: regset): Mach.regset := fun (r:mreg) => rs r. @@ -44,7 +50,6 @@ Definition set_from_Machrs (mrs: Mach.regset) (rs: regset): regset := end. Local Open Scope option_monad_scope. -Local Open Scope asm. Record state: Type := State { _rs: regset; _m: mem }. Definition outcome := option state. diff --git a/kvx/lib/PseudoAsmblockproof.v b/kvx/lib/PseudoAsmblockproof.v index 3eb80ebb..67308278 100644 --- a/kvx/lib/PseudoAsmblockproof.v +++ b/kvx/lib/PseudoAsmblockproof.v @@ -52,6 +52,7 @@ End TRANSLATION. *) Require Import Linking. +Import PseudoAsmblock.AsmNotations. Section PRESERVATION. @@ -65,7 +66,6 @@ Proof. Qed. Local Open Scope Z_scope. -Local Open Scope asm. Local Open Scope option_monad_scope. Variable prog: program. |