From c673b6a5f66c931819fbcee8b7abcc974b0418f8 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 18 Sep 2018 18:26:18 +0200 Subject: premier jet Asmblockgenproof.return_address_offset --- Makefile | 2 +- mppa_k1c/Asmblockgenproof.v | 4 +- mppa_k1c/Asmblockgenproof0.v | 95 ++++++++++++++++++++++++++++++++++++++++++++ mppa_k1c/Asmgenproof.v | 7 ---- 4 files changed, 98 insertions(+), 10 deletions(-) create mode 100644 mppa_k1c/Asmblockgenproof0.v diff --git a/Makefile b/Makefile index 02cb3cc3..255c43db 100644 --- a/Makefile +++ b/Makefile @@ -96,7 +96,7 @@ BACKEND=\ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ Machblock.v Machblockgen.v Machblockgenproof.v \ - Asmblock.v Asmblockgen.v Asmblockgenproof.v \ + Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof.v \ Asm.v Asmgen.v Asmgenproof.v # C front-end modules (in cfrontend/) diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index de00218e..0476e76a 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -17,7 +17,7 @@ Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions Asmblock. (* Require Import Asmgen Asmgenproof0 Asmgenproof1. *) -Require Import Asmblockgen. +Require Import Asmblockgen Asmblockgenproof0. Definition match_prog (p: Machblock.program) (tp: Asmblock.program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. @@ -1104,7 +1104,7 @@ Qed. *) Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop := - (fun a b c => False). + Asmblockgenproof0.return_address_offset. Axiom transf_program_correct: forward_simulation (Machblock.semantics return_address_offset prog) (Asmblock.semantics tprog). diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v new file mode 100644 index 00000000..374ae0d1 --- /dev/null +++ b/mppa_k1c/Asmblockgenproof0.v @@ -0,0 +1,95 @@ +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. + +Module MB:=Machblock. +Module AB:=Asmblock. + +(* inspired from Mach *) + +Lemma find_label_tail: + forall lbl c c', MB.find_label lbl c = Some c' -> is_tail c' c. +Proof. + induction c; simpl; intros. discriminate. + destruct (MB.is_label lbl a). inv H. auto with coqlib. eauto with coqlib. +Qed. + +(* inspired from Asmgenproof0 *) + +(* ... skip ... *) + +(** The ``code tail'' of an instruction list [c] is the list of instructions + starting at PC [pos]. *) + +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. + +(* ... skip ... *) + + +(** 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 = OK tc -> + code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc. diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 32e8e8a8..f85445f2 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -42,13 +42,6 @@ Qed. (** Return Address Offset *) -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. - Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop := Asmblockgenproof.return_address_offset (Machblockgen.transf_function f) (Machblockgen.trans_code c) ofs. -- cgit