diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-02 06:33:52 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-02 06:33:52 +0100 |
commit | 9baeff3f8d858ee5d848d941ab655b227cfb14fd (patch) | |
tree | ee301649c9072bd159393ed848079e5de7414c88 | |
parent | 159986a5a2e6c465e60922a9a3ad76d27c86f946 (diff) | |
parent | 59948b3348964f4b16f408ffe690f2c78ca80959 (diff) | |
download | compcert-kvx-9baeff3f8d858ee5d848d941ab655b227cfb14fd.tar.gz compcert-kvx-9baeff3f8d858ee5d848d941ab655b227cfb14fd.zip |
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
-rwxr-xr-x | configure | 1 | ||||
-rw-r--r-- | driver/Clflags.ml | 2 | ||||
-rw-r--r-- | mppa_k1c/Asm.v | 22 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 110 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 632 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 135 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 140 | ||||
-rw-r--r-- | mppa_k1c/PostpassScheduling.v | 1017 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 37 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 1344 | ||||
-rw-r--r-- | mppa_k1c/SelectLong.v | 17 | ||||
-rw-r--r-- | mppa_k1c/SelectLong.vp | 17 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 16 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 41 | ||||
-rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 8 | ||||
-rw-r--r-- | runtime/Makefile | 6 | ||||
-rw-r--r-- | test/mppa/instr/Makefile | 5 | ||||
-rw-r--r-- | test/mppa/instr/faddw.c | 4 | ||||
-rwxr-xr-x | test/mppa/instr/floatcmp.py | 93 | ||||
-rw-r--r-- | test/mppa/instr/fmulw.c | 4 | ||||
-rw-r--r-- | test/mppa/instr/fnegw.c | 2 | ||||
-rw-r--r-- | test/mppa/instr/framework.h | 4 | ||||
-rw-r--r-- | test/mppa/instr/fsbfw.c | 2 |
24 files changed, 2286 insertions, 1377 deletions
@@ -805,6 +805,7 @@ ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ + Asmblockdeps.v\\ AbstractBasicBlocksDef.v DepTreeTheory.v ImpDep.v Parallelizability.v\\ ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v EOF diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 99ee41e7..77fae8ee 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -15,7 +15,7 @@ let prepro_options = ref ([]: string list) let linker_options = ref ([]: string list) let assembler_options = ref ([]: string list) -let option_flongdouble = ref false +let option_flongdouble = ref (Configuration.arch = "mppa_k1c") let option_fstruct_passing = ref false let option_fbitfields = ref false let option_fvararg_calls = ref true diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 7c735bf1..31bc855d 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -103,11 +103,18 @@ Inductive instruction : Type := | Pfnegw (rd rs: ireg) (**r float negate word *)
| Pfnarrowdw (rd rs: ireg) (**r float narrow 64 -> 32 bits *)
| Pfwidenlwd (rd rs: ireg) (**r float widen 32 -> 64 bits *)
- | Pfloatwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer *)
+ | Pfloatwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (32 -> 32) *)
+ | Pfloatuwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (u32 -> 32) *)
| Pfloatudrnsz (rd rs: ireg) (**r Floating Point Conversion from unsigned integer (64 bits) *)
+ | Pfloatudrnsz_i32 (rd rs: ireg) (**r Floating Point Conversion from unsigned integer (32 bits) *)
| Pfloatdrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (64 bits) *)
+ | Pfloatdrnsz_i32 (rd rs: ireg) (**r Floating Point Conversion from integer (32 bits) *)
| Pfixedwrzz (rd rs: ireg) (**r Integer conversion from floating point *)
- | Pfixeddrzz (rd rs: ireg) (**r Integer conversion from floating point (64 bits) *)
+ | Pfixeduwrzz (rd rs: ireg) (**r Integer conversion from floating point (f32 -> 32 bits unsigned *)
+ | Pfixeddrzz (rd rs: ireg) (**r Integer conversion from floating point (i64 -> 64 bits) *)
+ | Pfixeddrzz_i32 (rd rs: ireg) (**r Integer conversion from floating point (i32 -> f64) *)
+ | Pfixedudrzz (rd rs: ireg) (**r unsigned Integer conversion from floating point (u64 -> 64 bits) *)
+ | Pfixedudrzz_i32 (rd rs: ireg) (**r unsigned Integer conversion from floating point (u32 -> 64 bits) *)
(** Arith RI32 *)
| Pmake (rd: ireg) (imm: int) (**r load immediate *)
@@ -124,6 +131,8 @@ Inductive instruction : Type := (** Arith RRR *)
| Pcompw (it: itest) (rd rs1 rs2: ireg) (**r comparison word *)
| Pcompl (it: itest) (rd rs1 rs2: ireg) (**r comparison long *)
+ | Pfcompw (ft: ftest) (rd rs1 rs2: ireg) (**r comparison float *)
+ | Pfcompl (ft: ftest) (rd rs1 rs2: ireg) (**r comparison float64 *)
| Paddw (rd rs1 rs2: ireg) (**r add word *)
| Psubw (rd rs1 rs2: ireg) (**r sub word *)
@@ -216,11 +225,18 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmblock.Pfnegw rd rs => Pfnegw rd rs
| PArithRR Asmblock.Pfnarrowdw rd rs => Pfnarrowdw rd rs
| PArithRR Asmblock.Pfwidenlwd rd rs => Pfwidenlwd rd rs
+ | PArithRR Asmblock.Pfloatuwrnsz rd rs => Pfloatuwrnsz rd rs
| PArithRR Asmblock.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs
| PArithRR Asmblock.Pfloatudrnsz rd rs => Pfloatudrnsz rd rs
| PArithRR Asmblock.Pfloatdrnsz rd rs => Pfloatdrnsz rd rs
+ | PArithRR Asmblock.Pfloatudrnsz_i32 rd rs => Pfloatudrnsz_i32 rd rs
+ | PArithRR Asmblock.Pfloatdrnsz_i32 rd rs => Pfloatdrnsz_i32 rd rs
| PArithRR Asmblock.Pfixedwrzz rd rs => Pfixedwrzz rd rs
+ | PArithRR Asmblock.Pfixeduwrzz rd rs => Pfixeduwrzz rd rs
| PArithRR Asmblock.Pfixeddrzz rd rs => Pfixeddrzz rd rs
+ | PArithRR Asmblock.Pfixedudrzz rd rs => Pfixedudrzz rd rs
+ | PArithRR Asmblock.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs
+ | PArithRR Asmblock.Pfixedudrzz_i32 rd rs => Pfixedudrzz_i32 rd rs
(* RI32 *)
| PArithRI32 Asmblock.Pmake rd imm => Pmake rd imm
@@ -237,6 +253,8 @@ Definition basic_to_instruction (b: basic) := (* RRR *)
| PArithRRR (Asmblock.Pcompw it) rd rs1 rs2 => Pcompw it rd rs1 rs2
| PArithRRR (Asmblock.Pcompl it) rd rs1 rs2 => Pcompl it rd rs1 rs2
+ | PArithRRR (Asmblock.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2
+ | PArithRRR (Asmblock.Pfcompl ft) rd rs1 rs2 => Pfcompl ft rd rs1 rs2
| PArithRRR Asmblock.Paddw rd rs1 rs2 => Paddw rd rs1 rs2
| PArithRRR Asmblock.Psubw rd rs1 rs2 => Psubw rd rs1 rs2
| PArithRRR Asmblock.Pmulw rd rs1 rs2 => Pmulw rd rs1 rs2
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index b9c50517..86c47613 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -126,6 +126,17 @@ Inductive itest: Type := | ITnone (**r Not Any Bits Set in Mask *) . +Inductive ftest: Type := + | FTone (**r Ordered and Not Equal *) + | FTueq (**r Unordered or Equal *) + | FToeq (**r Ordered and Equal *) + | FTune (**r Unordered or Not Equal *) + | FTolt (**r Ordered and Less Than *) + | FTuge (**r Unordered or Greater Than or Equal *) + | FToge (**r Ordered and Greater Than or Equal *) + | FTult (**r Unordered or Less Than *) + . + (** Offsets for load and store instructions. An offset is either an immediate integer or the low part of a symbol. *) @@ -287,11 +298,18 @@ Inductive arith_name_rr : Type := | Pfnegw (**r float negate word *) | Pfnarrowdw (**r float narrow 64 -> 32 bits *) | Pfwidenlwd (**r Floating Point widen from 32 bits to 64 bits *) - | Pfloatwrnsz (**r Floating Point Conversion from integer (int -> single) *) - | Pfloatudrnsz (**r Floating Point Conversion from unsigned integer (ulong -> float) *) + | Pfloatwrnsz (**r Floating Point conversion from integer (int -> SINGLE) *) + | Pfloatuwrnsz (**r Floating Point conversion from integer (unsigned int -> SINGLE) *) + | Pfloatudrnsz (**r Floating Point Conversion from integer (unsigned long -> float) *) + | Pfloatudrnsz_i32 (**r Floating Point Conversion from integer (unsigned int -> float) *) | Pfloatdrnsz (**r Floating Point Conversion from integer (long -> float) *) + | Pfloatdrnsz_i32 (**r Floating Point Conversion from integer (int -> float) *) | Pfixedwrzz (**r Integer conversion from floating point (single -> int) *) + | Pfixeduwrzz (**r Integer conversion from floating point (single -> unsigned int) *) | Pfixeddrzz (**r Integer conversion from floating point (float -> long) *) + | Pfixedudrzz (**r Integer conversion from floating point (float -> unsigned long) *) + | Pfixeddrzz_i32 (**r Integer conversion from floating point (float -> int) *) + | Pfixedudrzz_i32 (**r Integer conversion from floating point (float -> unsigned int) *) . Inductive arith_name_ri32 : Type := @@ -313,6 +331,8 @@ Inductive arith_name_rf64 : Type := Inductive arith_name_rrr : Type := | Pcompw (it: itest) (**r comparison word *) | Pcompl (it: itest) (**r comparison long *) + | Pfcompw (ft: ftest) (**r comparison float32 *) + | Pfcompl (ft: ftest) (**r comparison float64 *) | Paddw (**r add word *) | Psubw (**r sub word *) @@ -578,6 +598,36 @@ Proof. - destruct e; simpl; try omega. contradict H; simpl; auto. *)Qed. + +Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; simpl. assumption. +Defined. + +Lemma no_header_size: + forall bb, size (no_header bb) = size bb. +Proof. + intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity. +Qed. + +Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; simpl. assumption. +Defined. + +Lemma stick_header_size: + forall h bb, size (stick_header h bb) = size bb. +Proof. + intros. destruct bb. unfold stick_header. simpl. reflexivity. +Qed. + +Lemma stick_header_no_header: + forall bb, stick_header (header bb) (no_header bb) = bb. +Proof. + intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity. +Qed. + + Definition bblocks := list bblock. Fixpoint size_blocks (l: bblocks): Z := @@ -779,6 +829,31 @@ Definition itest_for_cmp (c: comparison) (s: signedness) := | Cgt, Unsigned => ITgtu end. +Inductive oporder_ftest := + | Normal (ft: ftest) + | Reversed (ft: ftest) +. + +Definition ftest_for_cmp (c: comparison) := + match c with + | Ceq => Normal FToeq + | Cne => Normal FTune + | Clt => Normal FTolt + | Cle => Reversed FToge + | Cgt => Reversed FTolt + | Cge => Normal FToge + end. + +Definition notftest_for_cmp (c: comparison) := + match c with + | Ceq => Normal FTune + | Cne => Normal FToeq + | Clt => Normal FTuge + | Cle => Reversed FTult + | Cgt => Reversed FTuge + | Cge => Normal FTult + end. + (* CoMPare Signed Words to Zero *) Definition btest_for_cmpswz (c: comparison) := match c with @@ -873,6 +948,28 @@ Definition compare_long (t: itest) (v1 v2: val) (m: mem): val := end . +Definition compare_single (t: ftest) (v1 v2: val): val := + match t with + | FTone | FTueq => Vundef (* unused *) + | FToeq => Val.cmpfs Ceq v1 v2 + | FTune => Val.cmpfs Cne v1 v2 + | FTolt => Val.cmpfs Clt v1 v2 + | FTuge => Val.notbool (Val.cmpfs Clt v1 v2) + | FToge => Val.cmpfs Cge v1 v2 + | FTult => Val.notbool (Val.cmpfs Cge v1 v2) + end. + +Definition compare_float (t: ftest) (v1 v2: val): val := + match t with + | FTone | FTueq => Vundef (* unused *) + | FToeq => Val.cmpf Ceq v1 v2 + | FTune => Val.cmpf Cne v1 v2 + | FTolt => Val.cmpf Clt v1 v2 + | FTuge => Val.notbool (Val.cmpf Clt v1 v2) + | FToge => Val.cmpf Cge v1 v2 + | FTult => Val.notbool (Val.cmpf Cge v1 v2) + end. + (** Execution of arith instructions TODO: subsplitting by instruction type ? Could be useful for expressing auxiliary lemma... @@ -906,10 +1003,17 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset | Pfnarrowdw => rs#d <- (Val.singleoffloat rs#s) | Pfwidenlwd => rs#d <- (Val.floatofsingle rs#s) | Pfloatwrnsz => rs#d <- (match Val.singleofint rs#s with Some f => f | _ => Vundef end) + | Pfloatuwrnsz => rs#d <- (match Val.singleofintu rs#s with Some f => f | _ => Vundef end) | Pfloatudrnsz => rs#d <- (match Val.floatoflongu rs#s with Some f => f | _ => Vundef end) + | Pfloatudrnsz_i32 => rs#d <- (match Val.floatofintu rs#s with Some f => f | _ => Vundef end) | Pfloatdrnsz => rs#d <- (match Val.floatoflong rs#s with Some f => f | _ => Vundef end) + | Pfloatdrnsz_i32 => rs#d <- (match Val.floatofint rs#s with Some f => f | _ => Vundef end) | Pfixedwrzz => rs#d <- (match Val.intofsingle rs#s with Some i => i | _ => Vundef end) + | Pfixeduwrzz => rs#d <- (match Val.intuofsingle rs#s with Some i => i | _ => Vundef end) | Pfixeddrzz => rs#d <- (match Val.longoffloat rs#s with Some i => i | _ => Vundef end) + | Pfixeddrzz_i32 => rs#d <- (match Val.intoffloat rs#s with Some i => i | _ => Vundef end) + | Pfixedudrzz => rs#d <- (match Val.longuoffloat rs#s with Some i => i | _ => Vundef end) + | Pfixedudrzz_i32 => rs#d <- (match Val.intuoffloat rs#s with Some i => i | _ => Vundef end) end | PArithRI32 n d i => @@ -936,6 +1040,8 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset match n with | Pcompw c => rs#d <- (compare_int c rs#s1 rs#s2 m) | Pcompl c => rs#d <- (compare_long c rs#s1 rs#s2 m) + | Pfcompw c => rs#d <- (compare_single c rs#s1 rs#s2) + | Pfcompl c => rs#d <- (compare_float c rs#s1 rs#s2) | Paddw => rs#d <- (Val.add rs#s1 rs#s2) | Psubw => rs#d <- (Val.sub rs#s1 rs#s2) | Pmulw => rs#d <- (Val.mul rs#s1 rs#s2) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 83064762..c2477e66 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -80,9 +80,11 @@ Inductive op_wrap := | Store (so: store_op) | Control (co: control_op) | Allocframe (sz: Z) (pos: ptrofs) + | Allocframe2 (sz: Z) (pos: ptrofs) | Freeframe (sz: Z) (pos: ptrofs) | Freeframe2 (sz: Z) (pos: ptrofs) | Constant (v: val) + | Fail . Coercion Arith: arith_op >-> op_wrap. @@ -115,10 +117,17 @@ Definition arith_eval (ao: arith_op) (l: list value) := | Pfnarrowdw => Some (Val (Val.singleoffloat v)) | Pfwidenlwd => Some (Val (Val.floatofsingle v)) | Pfloatwrnsz => Some (Val (match Val.singleofint v with Some f => f | _ => Vundef end)) + | Pfloatuwrnsz => Some (Val (match Val.singleofintu v with Some f => f | _ => Vundef end)) | Pfloatudrnsz => Some (Val (match Val.floatoflongu v with Some f => f | _ => Vundef end)) | Pfloatdrnsz => Some (Val (match Val.floatoflong v with Some f => f | _ => Vundef end)) + | Pfloatudrnsz_i32 => Some (Val (match Val.floatofintu v with Some f => f | _ => Vundef end)) + | Pfloatdrnsz_i32 => Some (Val (match Val.floatofint v with Some f => f | _ => Vundef end)) | Pfixedwrzz => Some (Val (match Val.intofsingle v with Some i => i | _ => Vundef end)) + | Pfixeduwrzz => Some (Val (match Val.intuofsingle v with Some i => i | _ => Vundef end)) | Pfixeddrzz => Some (Val (match Val.longoffloat v with Some i => i | _ => Vundef end)) + | Pfixedudrzz => Some (Val (match Val.longuoffloat v with Some i => i | _ => Vundef end)) + | Pfixeddrzz_i32 => Some (Val (match Val.intoffloat v with Some i => i | _ => Vundef end)) + | Pfixedudrzz_i32 => Some (Val (match Val.intuoffloat v with Some i => i | _ => Vundef end)) end | OArithRI32 n i, [] => @@ -150,6 +159,9 @@ Definition arith_eval (ao: arith_op) (l: list value) := | OArithRRR n, [Val v1; Val v2] => match n with + | Pfcompw c => Some (Val (compare_single c v1 v2)) + | Pfcompl c => Some (Val (compare_float c v1 v2)) + | Paddw => Some (Val (Val.add v1 v2)) | Psubw => Some (Val (Val.sub v1 v2)) | Pmulw => Some (Val (Val.mul v1 v2)) @@ -328,6 +340,13 @@ Definition op_eval (o: op) (l: list value) := | None => None | Some m => Some (Memstate m) end + | Allocframe2 sz pos, [Val spv; Memstate m] => + let (m1, stk) := Mem.alloc m 0 sz in + let sp := (Vptr stk Ptrofs.zero) in + match Mem.storev Mptr m1 (Val.offset_ptr sp pos) spv with + | None => None + | Some m => Some (Val sp) + end | Freeframe sz pos, [Val spv; Memstate m] => match Mem.loadv Mptr m (Val.offset_ptr spv pos) with | None => None @@ -355,6 +374,7 @@ Definition op_eval (o: op) (l: list value) := end end | Constant v, [] => Some (Val v) + | Fail, _ => None | _, _ => None end. @@ -443,6 +463,7 @@ Definition op_eq (o1 o2: op): ?? bool := | Freeframe sz1 pos1, Freeframe sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2) | Freeframe2 sz1 pos1, Freeframe2 sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2) | Constant c1, Constant c2 => phys_eq c1 c2 + | Fail, Fail => RET true | _, _ => RET false end. @@ -559,9 +580,21 @@ Definition trans_arith (ai: ar_instruction) : macro := | PArithRI64 n d i => [(#d, Op (Arith (OArithRI64 n i)) Enil)] | PArithRF32 n d i => [(#d, Op (Arith (OArithRF32 n i)) Enil)] | PArithRF64 n d i => [(#d, Op (Arith (OArithRF64 n i)) Enil)] - | PArithRRR n d s1 s2 => [(#d, Op (Arith (OArithRRR n)) (Name (#s1) @ Name (#s2) @ Enil))] - | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Enil))] - | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Enil))] + | PArithRRR n d s1 s2 => + match n with + | Pcompw _ | Pcompl _ => [(#d, Op (Arith (OArithRRR n)) (Name (#s1) @ Name (#s2) @ Name pmem @ Enil))] + | _ => [(#d, Op (Arith (OArithRRR n)) (Name (#s1) @ Name (#s2) @ Enil))] + end + | PArithRRI32 n d s i => + match n with + | Pcompiw _ => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Name pmem @ Enil))] + | _ => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Enil))] + end + | PArithRRI64 n d s i => + match n with + | Pcompil _ => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Name pmem @ Enil))] + | _ => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Enil))] + end end. @@ -570,13 +603,19 @@ Definition trans_basic (b: basic) : macro := | PArith ai => trans_arith ai | PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (Name (#a) @ Name pmem @ Enil))] | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (Name (#s) @ Name (#a) @ Name pmem @ Enil))] - | Pallocframe sz pos => [(pmem, Op (Allocframe sz pos) (Name (#SP) @ Name pmem @ Enil)); - (#FP, Name (#SP)); (#SP, Name (#RTMP)); (#RTMP, Op (Constant Vundef) Enil)] + | Pallocframe sz pos => [(#FP, Name (#SP)); (#SP, Op (Allocframe2 sz pos) (Name (#SP) @ Name pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil); + (pmem, Op (Allocframe sz pos) (Old (Name (#SP)) @ Name pmem @ Enil))] | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (Name (#SP) @ Name pmem @ Enil)); - (#SP, Op (Freeframe2 sz pos) (Name (#SP) @ Name pmem @ Enil)); + (#SP, Op (Freeframe2 sz pos) (Name (#SP) @ Old (Name pmem) @ Enil)); (#RTMP, Op (Constant Vundef) Enil)] - | Pget rd ra => [(#rd, Name (#ra))] - | Pset ra rd => [(#ra, Name (#rd))] + | Pget rd ra => match ra with + | RA => [(#rd, Name (#ra))] + | _ => [(#rd, Op Fail Enil)] + end + | Pset ra rd => match ra with + | RA => [(#ra, Name (#rd))] + | _ => [(#rd, Op Fail Enil)] + end | Pnop => [] end. @@ -591,6 +630,16 @@ Definition trans_pcincr (sz: Z) := [(#PC, Op (Control (OIncremPC sz)) (Name (#PC Definition trans_block (b: Asmblock.bblock) : L.bblock := trans_body (body b) ++ trans_pcincr (size b) ++ trans_exit (exit b). +Theorem trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb. +Proof. + intros. destruct bb as [hd bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity. +Qed. + +Theorem trans_block_header_inv: forall bb hd, trans_block (stick_header hd bb) = trans_block bb. +Proof. + intros. destruct bb as [hdr bdy ex COR]; unfold no_header; simpl. unfold trans_block. simpl. reflexivity. +Qed. + Definition state := L.mem. Definition exec := L.run. @@ -609,14 +658,53 @@ Definition trans_state (s: Asmblock.state) : state := | None => Val Vundef end. -Lemma pos_gpreg_not_3: forall g: gpreg, 3 <> # g. +Lemma pos_gpreg_not: forall g: gpreg, pmem <> (#g) /\ 2 <> (#g) /\ 3 <> (#g). +Proof. + intros. split; try split. all: destruct g; try discriminate. +Qed. + +Lemma not_3_plus_n: + forall n, 3 + n <> pmem /\ 3 + n <> (# RA) /\ 3 + n <> (# PC). Proof. - destruct g; try discriminate. + intros. split; try split. + all: destruct n; simpl; try (destruct n; discriminate); try discriminate. Qed. -Lemma pos_gpreg_not_2: forall g: gpreg, 2 <> # g. +Lemma not_eq_add: + forall k n n', n <> n' -> k + n <> k + n'. +Proof. +Admitted. (* FIXME - help Sylvain ? *) + +Lemma not_eq_ireg_to_pos: + forall n r r', r' <> r -> n + ireg_to_pos r <> n + ireg_to_pos r'. Proof. - destruct g; try discriminate. + intros. destruct r; destruct r'; try contradiction; apply not_eq_add; discriminate. (* FIXME - quite long to prove *) +Qed. + +Lemma not_eq_ireg_ppos: + forall r r', r <> r' -> (# r') <> (# r). +Proof. + intros. unfold ppos. destruct r. + - destruct r'; try discriminate. + + apply not_eq_ireg_to_pos; congruence. + + destruct g; discriminate. + + destruct g; discriminate. + - destruct r'; try discriminate; try contradiction. + destruct g; discriminate. + - destruct r'; try discriminate; try contradiction. + destruct g; discriminate. +Qed. + +Lemma not_eq_ireg_to_pos_ppos: + forall r r', r' <> r -> 3 + ireg_to_pos r <> # r'. +Proof. + intros. unfold ppos. apply not_eq_ireg_to_pos. assumption. +Qed. + +Lemma not_eq_IR: + forall r r', r <> r' -> IR r <> IR r'. +Proof. + intros. congruence. Qed. Ltac Simplif := @@ -625,7 +713,7 @@ Ltac Simplif := || (rewrite Pregmap.gss) || (rewrite nextblock_pc) || (rewrite Pregmap.gso by eauto with asmgen) - || (rewrite assign_diff by (try discriminate; try (apply pos_gpreg_not_3); try (apply pos_gpreg_not_2))) + || (rewrite assign_diff by (try discriminate; try (apply pos_gpreg_not); try (apply not_3_plus_n); try (apply not_eq_ireg_ppos; apply not_eq_IR; auto); try (apply not_eq_ireg_to_pos_ppos; auto))) || (rewrite assign_eq) ); auto with asmgen. @@ -641,16 +729,174 @@ Proof. destruct g; reflexivity. Qed. -Lemma exec_match_app: +Lemma exec_app_some: forall c c' s s' s'', exec Ge c s = Some s' -> exec Ge c' s' = Some s'' -> exec Ge (c ++ c') s = Some s''. Proof. -Admitted. + induction c. + - simpl. intros. congruence. + - intros. simpl in *. destruct (macro_run _ _ _ _); auto. eapply IHc; eauto. discriminate. +Qed. + +Lemma exec_app_none: + forall c c' s, + exec Ge c s = None -> + exec Ge (c ++ c') s = None. +Proof. + induction c. + - simpl. discriminate. + - intros. simpl. simpl in H. destruct (macro_run _ _ _ _); auto. +Qed. + +Lemma trans_arith_correct: + forall ge fn i rs m rs' s, + exec_arith_instr ge i rs m = rs' -> + match_states (State rs m) s -> + exists s', + macro_run (Genv ge fn) (trans_arith i) s s = Some s' + /\ match_states (State rs' m) s'. +Proof. + intros. unfold exec_arith_instr in H. destruct i. +(* Ploadsymbol *) + - destruct i. inv H. inv H0. + eexists; split; try split. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRR *) + - destruct i. + all: inv H; inv H0; + eexists; split; try split; + [ simpl; pose (H1 rs0); simpl in e; rewrite e; reflexivity | + Simpl | + intros rr; destruct rr; Simpl; + destruct (ireg_eq g rd); subst; Simpl ]. +(* PArithRI32 *) + - destruct i. inv H. inv H0. + eexists; split; try split. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRI64 *) + - destruct i. inv H. inv H0. + eexists; split; try split. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRF32 *) + - destruct i. inv H. inv H0. + eexists; split; try split. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRF64 *) + - destruct i. inv H. inv H0. + eexists; split; try split. + * Simpl. + * intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd); subst; Simpl. +(* PArithRRR *) + - destruct i. + all: inv H; inv H0; + eexists; split; try split; + [ simpl; pose (H1 rs1); simpl in e; rewrite e; pose (H1 rs2); simpl in e0; rewrite e0; try (rewrite H); reflexivity + | Simpl + | intros rr; destruct rr; Simpl; + destruct (ireg_eq g rd); subst; Simpl ]. +(* PArithRRI32 *) + - destruct i. + all: inv H; inv H0; + eexists; split; try split; + [ simpl; pose (H1 rs0); simpl in e; rewrite e; try (rewrite H); reflexivity + | Simpl + | intros rr; destruct rr; Simpl; + destruct (ireg_eq g rd); subst; Simpl ]. +(* PArithRRI64 *) + - destruct i. + all: inv H; inv H0; + eexists; split; try split; + [ simpl; pose (H1 rs0); simpl in e; rewrite e; try (rewrite H); reflexivity + | Simpl + | intros rr; destruct rr; Simpl; + destruct (ireg_eq g rd); subst; Simpl ]. +Qed. + +Lemma forward_simu_basic: + forall ge fn b rs m rs' m' s, + exec_basic_instr ge b rs m = Next rs' m' -> + match_states (State rs m) s -> + exists s', + macro_run (Genv ge fn) (trans_basic b) s s = Some s' + /\ match_states (State rs' m') s'. +Proof. + intros. destruct b. +(* Arith *) + - simpl in H. inv H. simpl macro_run. eapply trans_arith_correct; eauto. +(* Load *) + - simpl in H. destruct i; destruct i. + all: unfold exec_load in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; + destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0; + eexists; split; try split; + [ simpl; rewrite EVALOFF; rewrite H; pose (H1 ra); simpl in e; rewrite e; rewrite MEML; reflexivity| + Simpl| + intros rr; destruct rr; Simpl; + destruct (ireg_eq g rd); [ + subst; Simpl| + Simpl; rewrite assign_diff; pose (H1 g); simpl in e; try assumption; Simpl; unfold ppos; apply not_eq_ireg_to_pos; assumption]]. +(* Store *) + - simpl in H. destruct i; destruct i. + all: unfold exec_store in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; + destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0; + eexists; split; try split; + [ simpl; rewrite EVALOFF; rewrite H; pose (H1 ra); simpl in e; rewrite e; pose (H1 rs0); simpl in e0; rewrite e0; rewrite MEML; reflexivity + | Simpl + | intros rr; destruct rr; Simpl]. +(* Allocframe *) + - simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate. + inv H. inv H0. eexists. split; try split. + * simpl. Simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite MEMAL. rewrite MEMS. Simpl. + rewrite H. rewrite MEMAL. rewrite MEMS. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]]. + ** subst. Simpl. + ** subst. Simpl. + ** subst. Simpl. + ** Simpl. repeat (rewrite assign_diff). auto. + pose (not_eq_ireg_to_pos_ppos GPR14 g). simpl ireg_to_pos in n2. auto. + pose (not_eq_ireg_to_pos_ppos GPR12 g). simpl ireg_to_pos in n2. auto. + pose (not_eq_ireg_to_pos_ppos GPR32 g). simpl ireg_to_pos in n2. auto. +(* Freeframe *) + - simpl in H. destruct (Mem.loadv _ _ _) eqn:MLOAD; try discriminate. destruct (rs GPR12) eqn:SPeq; try discriminate. + destruct (Mem.free _ _ _ _) eqn:MFREE; try discriminate. inv H. inv H0. + eexists. split; try split. + * simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite SPeq. rewrite MLOAD. rewrite MFREE. + Simpl. rewrite e. rewrite SPeq. rewrite MLOAD. rewrite MFREE. reflexivity. + * Simpl. + * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]]. + ** subst. Simpl. + ** subst. Simpl. + ** subst. Simpl. + ** Simpl. repeat (rewrite assign_diff). auto. + unfold ppos. pose (not_3_plus_n (ireg_to_pos g)). destruct a as (A & _ & _). auto. + pose (not_eq_ireg_to_pos_ppos GPR12 g). simpl ireg_to_pos in n2. auto. + pose (not_eq_ireg_to_pos_ppos GPR32 g). simpl ireg_to_pos in n2. auto. +(* Pget *) + - simpl in H. destruct rs0 eqn:rs0eq; try discriminate. inv H. inv H0. + eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. + destruct (ireg_eq g rd). + * subst. Simpl. + * Simpl. +(* Pset *) + - simpl in H. destruct rd eqn:rdeq; try discriminate. inv H. inv H0. + eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. +(* Pnop *) + - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption. +Qed. Lemma forward_simu_body: - forall ge bdy rs m rs' m' fn s, + forall bdy ge rs m rs' m' fn s, Ge = Genv ge fn -> exec_body ge bdy rs m = Next rs' m' -> match_states (State rs m) s -> @@ -658,7 +904,15 @@ Lemma forward_simu_body: exec Ge (trans_body bdy) s = Some s' /\ match_states (State rs' m') s'. Proof. -Admitted. + induction bdy. + - intros. inv H1. simpl in *. inv H0. eexists. repeat (split; auto). + - intros until s. intros GE EXEB MS. simpl in EXEB. destruct (exec_basic_instr _ _ _ _) eqn:EBI; try discriminate. + exploit forward_simu_basic; eauto. intros (s' & MRUN & MS'). subst Ge. + eapply IHbdy in MS'; eauto. destruct MS' as (s'' & EXECB & MS'). + eexists. split. + * simpl. rewrite MRUN. eassumption. + * eassumption. +Qed. Lemma forward_simu_control: forall ge fn ex b rs m rs2 m2 s, @@ -753,22 +1007,328 @@ Proof. intros. unfold nextblock. destruct r; Simpl. Qed. -Theorem forward_simu:
- forall rs1 m1 rs2 m2 s1' b ge fn,
- Ge = Genv ge fn ->
- exec_bblock ge fn b rs1 m1 = Next rs2 m2 ->
- match_states (State rs1 m1) s1' ->
- exists s2',
- exec Ge (trans_block b) s1' = Some s2'
- /\ match_states (State rs2 m2) s2'.
-Proof.
- intros until fn. intros GENV EXECB MS. unfold exec_bblock in EXECB. destruct (exec_body _ _ _) eqn:EXEB; try discriminate.
- exploit forward_simu_body; eauto. intros (s' & EXETRANSB & MS').
- exploit forward_simu_control; eauto. intros (s'' & EXETRANSEX & MS'').
-
- eexists. split.
- unfold trans_block. eapply exec_match_app. eassumption. eassumption.
- eassumption.
-Qed.
-
-End SECT.
+Theorem forward_simu: + forall rs1 m1 rs2 m2 s1' b ge fn, + Ge = Genv ge fn -> + exec_bblock ge fn b rs1 m1 = Next rs2 m2 -> + match_states (State rs1 m1) s1' -> + exists s2', + exec Ge (trans_block b) s1' = Some s2' + /\ match_states (State rs2 m2) s2'. +Proof. + intros until fn. intros GENV EXECB MS. unfold exec_bblock in EXECB. destruct (exec_body _ _ _) eqn:EXEB; try discriminate. + exploit forward_simu_body; eauto. intros (s' & EXETRANSB & MS'). + exploit forward_simu_control; eauto. intros (s'' & EXETRANSEX & MS''). + + eexists. split. + unfold trans_block. eapply exec_app_some. eassumption. eassumption. + eassumption. +Qed. + +Lemma exec_bblock_stuck_nec: + forall ge fn b rs m, + exec_body ge (body b) rs m = Stuck + \/ (exists rs' m', exec_body ge (body b) rs m = Next rs' m' /\ exec_control ge fn (exit b) (nextblock b rs') m' = Stuck) + <-> exec_bblock ge fn b rs m = Stuck. +Proof. + intros. split. + + intros. destruct H. + - unfold exec_bblock. rewrite H. reflexivity. + - destruct H as (rs' & m' & EXEB & EXEC). unfold exec_bblock. rewrite EXEB. assumption. + + intros. unfold exec_bblock in H. destruct (exec_body _ _ _ _) eqn:EXEB. + - right. repeat eexists. assumption. + - left. reflexivity. +Qed. + +Lemma exec_basic_instr_next_exec: + forall ge fn i rs m rs' m' s tc, + Ge = Genv ge fn -> + exec_basic_instr ge i rs m = Next rs' m' -> + match_states (State rs m) s -> + exists s', + exec Ge (trans_basic i :: tc) s = exec Ge tc s' + /\ match_states (State rs' m') s'. +Proof. + intros. exploit forward_simu_basic; eauto. + intros (s' & MRUN & MS'). + simpl exec. exists s'. subst. rewrite MRUN. split; auto. +Qed. + +Lemma exec_body_next_exec: + forall c ge fn rs m rs' m' s tc, + Ge = Genv ge fn -> + exec_body ge c rs m = Next rs' m' -> + match_states (State rs m) s -> + exists s', + exec Ge (trans_body c ++ tc) s = exec Ge tc s' + /\ match_states (State rs' m') s'. +Proof. + induction c. + - intros. simpl in H0. inv H0. simpl. exists s. split; auto. + - intros. simpl in H0. destruct (exec_basic_instr _ _ _ _) eqn:EBI; try discriminate. + exploit exec_basic_instr_next_exec; eauto. intros (s' & EXEGEBASIC & MS'). + simpl trans_body. rewrite <- app_comm_cons. rewrite EXEGEBASIC. + eapply IHc; eauto. +Qed. + +Lemma exec_trans_pcincr_exec: + forall rs m s b, + match_states (State rs m) s -> + exists s', + exec Ge (trans_pcincr (size b) ++ trans_exit (exit b)) s = exec Ge (trans_exit (exit b)) s' + /\ match_states (State (nextblock b rs) m) s'. +Proof. + intros. inv H. eexists. split. simpl. + unfold control_eval. pose (H1 PC); simpl in e; rewrite e. destruct Ge. reflexivity. + simpl. split. + - Simpl. + - intros rr; destruct rr; Simpl. +Qed. + +Lemma exec_exit_none: + forall ge fn rs m s ex, + Ge = Genv ge fn -> + match_states (State rs m) s -> + exec Ge (trans_exit ex) s = None -> + exec_control ge fn ex rs m = Stuck. +Proof. + intros. inv H0. destruct ex as [ctl|]; try discriminate. + destruct ctl; destruct i; try reflexivity; try discriminate. +(* Pj_l *) + - simpl in *. pose (H3 PC); simpl in e; rewrite e in H1. clear e. + unfold goto_label_deps in H1. unfold goto_label. + destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. +(* Pcb *) + - simpl in *. destruct (cmp_for_btest bt). destruct i. + + pose (H3 PC); simpl in e; rewrite e in H1; clear e. + destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e. + unfold eval_branch_deps in H1; unfold eval_branch. + destruct (Val.cmp_bool _ _ _); auto. destruct b; try discriminate. + unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto. + destruct (rs PC); auto. discriminate. + + pose (H3 PC); simpl in e; rewrite e in H1; clear e. + destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e. + unfold eval_branch_deps in H1; unfold eval_branch. + destruct (Val.cmpl_bool _ _ _); auto. destruct b; try discriminate. + unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto. + destruct (rs PC); auto. discriminate. +(* Pcbu *) + - simpl in *. destruct (cmpu_for_btest bt). destruct i. + + pose (H3 PC); simpl in e; rewrite e in H1; clear e. + destruct o; auto. rewrite H2 in H1. + pose (H3 r); simpl in e; rewrite e in H1; clear e. + unfold eval_branch_deps in H1; unfold eval_branch. + destruct (Val.cmpu_bool _ _ _ _); auto. destruct b; try discriminate. + unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto. + destruct (rs PC); auto. discriminate. + + pose (H3 PC); simpl in e; rewrite e in H1; clear e. + destruct o; auto. rewrite H2 in H1. + pose (H3 r); simpl in e; rewrite e in H1; clear e. + unfold eval_branch_deps in H1; unfold eval_branch. + destruct (Val.cmplu_bool _ _ _); auto. destruct b; try discriminate. + unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto. + destruct (rs PC); auto. discriminate. +Qed. + +Theorem trans_block_reverse_stuck: + forall ge fn b rs m s, + Ge = Genv ge fn -> + exec Ge (trans_block b) s = None -> + match_states (State rs m) s -> + exec_bblock ge fn b rs m = Stuck. +Proof. + intros until s. intros Geq EXECBK MS. + apply exec_bblock_stuck_nec. + destruct (exec_body _ _ _ _) eqn:EXEB. + - right. repeat eexists. + exploit exec_body_next_exec; eauto. + intros (s' & EXECBK' & MS'). unfold trans_block in EXECBK. rewrite EXECBK' in EXECBK. clear EXECBK'. clear EXEB MS. + exploit exec_trans_pcincr_exec; eauto. intros (s'' & EXECINCR' & MS''). rewrite EXECINCR' in EXECBK. clear EXECINCR' MS'. + eapply exec_exit_none; eauto. + - left. reflexivity. +Qed. + +Lemma forward_simu_basic_instr_stuck: + forall i ge fn rs m s, + Ge = Genv ge fn -> + exec_basic_instr ge i rs m = Stuck -> + match_states (State rs m) s -> + exec Ge [trans_basic i] s = None. +Proof. + intros. inv H1. unfold exec_basic_instr in H0. destruct i; try discriminate. +(* PLoad *) + - destruct i; destruct i. + all: simpl; rewrite H2; pose (H3 ra); simpl in e; rewrite e; clear e; + unfold exec_load in H0; destruct (eval_offset _ _); auto; destruct (Mem.loadv _ _ _); auto; discriminate. +(* PStore *) + - destruct i; destruct i; + simpl; rewrite H2; pose (H3 ra); simpl in e; rewrite e; clear e; pose (H3 rs0); simpl in e; rewrite e; clear e; + unfold exec_store in H0; destruct (eval_offset _ _); auto; destruct (Mem.storev _ _ _); auto; discriminate. +(* Pallocframe *) + - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. destruct (Mem.alloc _ _ _). simpl in H0. + destruct (Mem.store _ _ _ _); try discriminate. reflexivity. +(* Pfreeframe *) + - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. + destruct (Mem.loadv _ _ _); auto. destruct (rs GPR12); auto. destruct (Mem.free _ _ _ _); auto. + discriminate. +(* Pget *) + - simpl. destruct rs0; subst; try discriminate. + all: simpl; auto. + - simpl. destruct rd; subst; try discriminate. + all: simpl; auto. +Qed. + +Lemma forward_simu_body_stuck: + forall bdy ge fn rs m s, + Ge = Genv ge fn -> + exec_body ge bdy rs m = Stuck -> + match_states (State rs m) s -> + exec Ge (trans_body bdy) s = None. +Proof. + induction bdy. + - simpl. discriminate. + - intros. simpl trans_body. simpl in H0. + destruct (exec_basic_instr _ _ _ _) eqn:EBI. + + exploit exec_basic_instr_next_exec; eauto. intros (s' & EXEGEB & MS'). rewrite EXEGEB. eapply IHbdy; eauto. + + cutrewrite (trans_basic a :: trans_body bdy = (trans_basic a :: nil) ++ trans_body bdy); try reflexivity. apply exec_app_none. + eapply forward_simu_basic_instr_stuck; eauto. +Qed. + + +Lemma forward_simu_exit_stuck: + forall ex ge fn rs m s, + Ge = Genv ge fn -> + exec_control ge fn ex rs m = Stuck -> + match_states (State rs m) s -> + exec Ge (trans_exit ex) s = None. +Proof. + intros. inv H1. destruct ex as [ctl|]; try discriminate. + destruct ctl; destruct i; try discriminate; try (simpl; reflexivity). +(* Pj_l *) + - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold goto_label in H0. + destruct (label_pos _ _ _); auto. clear e. destruct (rs PC); auto. discriminate. +(* Pcb *) + - simpl in *. destruct (cmp_for_btest bt). destruct i. + -- destruct o. + + unfold eval_branch in H0; unfold eval_branch_deps. + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmp_bool _ _ _); auto. + destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0. + destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. + + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. + -- destruct o. + + unfold eval_branch in H0; unfold eval_branch_deps. + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmpl_bool _ _ _); auto. + destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0. + destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. + + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. +(* Pcbu *) + - simpl in *. destruct (cmpu_for_btest bt). destruct i. + -- destruct o. + + rewrite H2. unfold eval_branch in H0; unfold eval_branch_deps. + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmpu_bool _ _ _); auto. + destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0. + destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. + + rewrite H2. pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. + -- destruct o. + + rewrite H2. unfold eval_branch in H0; unfold eval_branch_deps. + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmplu_bool _ _ _); auto. + destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0. + destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate. + + rewrite H2. pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity. +Qed. + + +Theorem forward_simu_stuck: + forall rs1 m1 s1' b ge fn, + Ge = Genv ge fn -> + exec_bblock ge fn b rs1 m1 = Stuck -> + match_states (State rs1 m1) s1' -> + exec Ge (trans_block b) s1' = None. +Proof. + intros until fn. intros GENV EXECB MS. apply exec_bblock_stuck_nec in EXECB. destruct EXECB. + - unfold trans_block. apply exec_app_none. eapply forward_simu_body_stuck; eauto. + - destruct H as (rs' & m' & EXEB & EXEC). unfold trans_block. exploit exec_body_next_exec; eauto. + intros (s' & EXEGEBODY & MS'). rewrite EXEGEBODY. exploit exec_trans_pcincr_exec; eauto. + intros (s'' & EXEGEPC & MS''). rewrite EXEGEPC. eapply forward_simu_exit_stuck; eauto. +Qed. + + +Lemma state_eq_decomp: + forall rs1 m1 rs2 m2, rs1 = rs2 -> m1 = m2 -> State rs1 m1 = State rs2 m2. +Proof. + intros. congruence. +Qed. + +Theorem state_equiv: + forall S1 S2 S', match_states S1 S' /\ match_states S2 S' -> S1 = S2. +Proof. + intros. inv H. unfold match_states in H0, H1. destruct S1 as (rs1 & m1). destruct S2 as (rs2 & m2). inv H0. inv H1. + apply state_eq_decomp. + - apply functional_extensionality. intros. assert (Val (rs1 x) = Val (rs2 x)) by congruence. congruence. + - congruence. +Qed. + + +Axiom bblock_equiv_reduce: + forall p1 p2 ge fn, + Ge = Genv ge fn -> + L.bblock_equiv Ge (trans_block p1) (trans_block p2) -> + Asmblockgenproof0.bblock_equiv ge fn p1 p2. (* FIXME *) + +Definition string_of_name (x: P.R.t): ?? pstring := RET (Str ("resname")). +(* match x with + | xH => RET (Str ("the_mem")) + | _ as x => + DO s <~ string_of_Z (Zpos (Pos.pred x)) ;; + RET ("R" +; s) + end. *) + +Definition string_of_op (op: P.op): ?? pstring := RET (Str ("OP")). +(* match op with + | P.Imm i => + DO s <~ string_of_Z i ;; + RET s + | P.ARITH ADD => RET (Str "ADD") + | P.ARITH SUB => RET (Str "SUB") + | P.ARITH MUL => RET (Str "MUL") + | P.LOAD => RET (Str "LOAD") + | P.STORE => RET (Str "STORE") + end. *) + +Definition bblock_eq_test (verb: bool) (p1 p2: Asmblock.bblock) : ?? bool := + if verb then + IDT.verb_bblock_eq_test string_of_name string_of_op Ge (trans_block p1) (trans_block p2) + else + IDT.bblock_eq_test Ge (trans_block p1) (trans_block p2). + +Local Hint Resolve IDT.bblock_eq_test_correct bblock_equiv_reduce IDT.verb_bblock_eq_test_correct: wlp. + +Theorem bblock_eq_test_correct verb p1 p2 : + forall ge fn, Ge = Genv ge fn -> + WHEN bblock_eq_test verb p1 p2 ~> b THEN b=true -> Asmblockgenproof0.bblock_equiv ge fn p1 p2. +Proof. + intros ge fn genv_eq. + wlp_simplify. +Admitted. (* FIXME - Ã voir avec Sylvain *) +Global Opaque bblock_eq_test. +Hint Resolve bblock_eq_test_correct: wlp. + +Inductive bblock_equiv' (bb bb': L.bblock) := + | bblock_equiv_intro': + (forall s, exec Ge bb s = exec Ge bb' s) -> + bblock_equiv' bb bb'. + +Lemma bblock_equiv'_refl: forall tbb, bblock_equiv' tbb tbb. +Proof. + repeat constructor. +Qed. + +Axiom bblock_equivb: L.bblock -> L.bblock -> bool. + +Axiom bblock_equiv'_eq: + forall b1 b2, + bblock_equivb b1 b2 = true <-> bblock_equiv' b1 b2. (* FIXME - Ã voir avec Sylvain *) + +End SECT. + +Extract Constant bblock_equivb => "PostpassSchedulingOracle.bblock_equivb'". diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 6503e5b3..edffd879 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -282,6 +282,30 @@ Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k: Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: bcode) := Pcompil (itest_for_cmp cmp Unsigned) rd r1 n ::i k. +Definition transl_cond_float32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompw ft rd r1 r2 ::i k + | Reversed ft => Pfcompw ft rd r2 r1 ::i k + end. + +Definition transl_cond_notfloat32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompw ft rd r1 r2 ::i k + | Reversed ft => Pfcompw ft rd r2 r1 ::i k + end. + +Definition transl_cond_float64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompl ft rd r1 r2 ::i k + | Reversed ft => Pfcompl ft rd r2 r1 ::i k + end. + +Definition transl_cond_notfloat64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompl ft rd r1 r2 ::i k + | Reversed ft => Pfcompl ft rd r2 r1 ::i k + end. + Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: bcode) := match cond, args with @@ -309,27 +333,19 @@ Definition transl_cond_op | Ccompluimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (transl_condimm_int64u c rd r1 n k) - | Ccompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Ccompf") - | Cnotcompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Cnotcompf") - | Ccompfs _, _ => Error(msg "Asmblockgen.transl_cond_op: Ccompfs") - | Cnotcompfs _, _ => Error(msg "Asmblockgen.transl_cond_op: Cnotcompfs") -(*| Ccompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c rd r1 r2 in - OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) - | Ccompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) -*)| _, _ => + | Ccompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_float32 c rd r1 r2 k) + | Cnotcompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_notfloat32 c rd r1 r2 k) + | Ccompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_float64 c rd r1 r2 k) + | Cnotcompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_cond_notfloat64 c rd r1 r2 k) + | _, _ => Error(msg "Asmblockgen.transl_cond_op") end. @@ -388,13 +404,7 @@ Definition transl_op OK (Pmulw rd rs1 rs2 ::i k) | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") -(*| Omulhs, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pmulhw rd rs1 rs2 :: k) - | Omulhu, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pmulhuw rd rs1 rs2 :: k) -*)| Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.") + | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.") (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pdivw rd rs1 rs2 :: k) *) | Odivu, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odivu: 32-bits division not supported yet. Please use 64-bits.") @@ -483,25 +493,7 @@ Definition transl_op | Odivlu, _ => Error (msg "Asmblockgen.transl_op: Odivlu") | Omodl, _ => Error (msg "Asmblockgen.transl_op: Omodl") | Omodlu, _ => Error (msg "Asmblockgen.transl_op: Omodlu") -(*| Omullhs, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pmulhl rd rs1 rs2 :: k) - | Omullhu, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pmulhul rd rs1 rs2 :: k) - | Odivl, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivl rd rs1 rs2 :: k) - | Odivlu, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivul rd rs1 rs2 :: k) - | Omodl, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Preml rd rs1 rs2 :: k) - | Omodlu, a1 :: a2 :: nil => - do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Premul rd rs1 rs2 :: k) -*)| Oandl, a1 :: a2 :: nil => + | Oandl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandl rd rs1 rs2 ::i k) | Oandlimm n, a1 :: nil => @@ -579,18 +571,39 @@ Definition transl_op | Osingleofint, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfloatwrnsz rd rs ::i k) + | Osingleofintu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfloatuwrnsz rd rs ::i k) | Ofloatoflong, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfloatdrnsz rd rs ::i k) | Ofloatoflongu, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfloatudrnsz rd rs ::i k) + | Ofloatofint, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfloatdrnsz_i32 rd rs ::i k) + | Ofloatofintu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfloatudrnsz_i32 rd rs ::i k) | Ointofsingle, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; OK (Pfixedwrzz rd rs ::i k) + | Ointuofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixeduwrzz rd rs ::i k) | Olongoffloat, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; OK (Pfixeddrzz rd rs ::i k) + | Ointoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixeddrzz_i32 rd rs ::i k) + | Ointuoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixedudrzz_i32 rd rs ::i k) + | Olonguoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfixedudrzz rd rs ::i k) | Ofloatofsingle, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; @@ -600,34 +613,16 @@ Definition transl_op OK (Pfnarrowdw rd rs ::i k) - | Oabsf , _ => Error (msg "Asmblockgen.transl_op: Oabsf") - | Oaddf , _ => Error (msg "Asmblockgen.transl_op: Oaddf") - | Osubf , _ => Error (msg "Asmblockgen.transl_op: Osubf") - | Omulf , _ => Error (msg "Asmblockgen.transl_op: Omulf") | Odivf , _ => Error (msg "Asmblockgen.transl_op: Odivf") - | Onegfs , _ => Error (msg "Asmblockgen.transl_op: Onegfs") - | Oabsfs , _ => Error (msg "Asmblockgen.transl_op: Oabsfs") - | Oaddfs , _ => Error (msg "Asmblockgen.transl_op: Oaddfs") - | Osubfs , _ => Error (msg "Asmblockgen.transl_op: Osubfs") - | Omulfs , _ => Error (msg "Asmblockgen.transl_op: Omulfs") - | Odivfs , _ => Error (msg "Asmblockgen.transl_op: Odivfs") - | Ofloatoflongu , _ => Error (msg "Asmblockgen.transl_op: Ofloatoflongu") - | Osingleoflong , _ => Error (msg "Asmblockgen.transl_op: Osingleoflong") - | Osingleoflongu , _ => Error (msg "Asmblockgen.transl_op: Osingleoflongu") - | Osingleoffloat , _ => Error (msg "Asmblockgen.transl_op: Osingleoffloat") - | Ofloatofsingle , _ => Error (msg "Asmblockgen.transl_op: Ofloatofsingle") - | Ointoffloat , _ => Error (msg "Asmblockgen.transl_op: Ointoffloat") - | Ointuoffloat , _ => Error (msg "Asmblockgen.transl_op: Ointuoffloat") - | Ofloatofint , _ => Error (msg "Asmblockgen.transl_op: Ofloatofint") - | Ofloatofintu , _ => Error (msg "Asmblockgen.transl_op: Ofloatofintu") - | Ointuofsingle , _ => Error (msg "Asmblockgen.transl_op: Ointuofsingle") - | Osingleofintu , _ => Error (msg "Asmblockgen.transl_op: Osingleofintu") - | Olonguoffloat , _ => Error (msg "Asmblockgen.transl_op: Olonguoffloat") - + (* We use the Splitlong instead for these four conversions *) + | Osingleoflong , _ => Error (msg "Asmblockgen.transl_op: Osingleoflong") + | Osingleoflongu , _ => Error (msg "Asmblockgen.transl_op: Osingleoflongu") | Olongofsingle , _ => Error (msg "Asmblockgen.transl_op: Olongofsingle") | Olonguofsingle , _ => Error (msg "Asmblockgen.transl_op: Olonguofsingle") + + | Ocmp cmp, _ => do rd <- ireg_of res; transl_cond_op cmp rd args k diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 9cba8402..1ac9a211 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -950,6 +950,10 @@ Proof. - simpl in TIB. monadInv TIB. unfold loadind in EQ. exploreInst; try discriminate.
- simpl in TIB. unfold transl_op in TIB. exploreInst; try discriminate.
unfold transl_cond_op in EQ0. exploreInst; try discriminate.
+ unfold transl_cond_float64. exploreInst; try discriminate.
+ unfold transl_cond_notfloat64. exploreInst; try discriminate.
+ unfold transl_cond_float32. exploreInst; try discriminate.
+ unfold transl_cond_notfloat32. exploreInst; try discriminate.
- simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate.
all: unfold transl_memory_access in EQ0; exploreInst; try discriminate.
- simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 175eca73..76404257 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -968,6 +968,138 @@ Proof. split; intros; Simpl. Qed. +Lemma swap_comparison_cmpfs: + forall v1 v2 cmp, + Val.lessdef (Val.cmpfs cmp v1 v2) (Val.cmpfs (swap_comparison cmp) v2 v1). +Proof. + intros. unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. + rewrite Float32.cmp_swap. auto. +Qed. + +Lemma transl_cond_float32_correct: + forall cmp rd r1 r2 k rs m, + exists rs', + exec_straight ge (basics_to_code (transl_cond_float32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.cmpfs cmp rs#r1 rs#r2) rs'#rd + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + intros. destruct cmp; simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpfs. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpfs. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +Qed. + +Lemma transl_cond_nofloat32_correct: + forall cmp rd r1 r2 k rs m, + exists rs', + exec_straight ge (basics_to_code (transl_cond_notfloat32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpfs_bool cmp (rs r1) (rs r2)))) rs'#rd + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + intros. destruct cmp; simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. + rewrite Float32.cmp_ne_eq. auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. + rewrite Float32.cmp_ne_eq. simpl. destruct (Float32.cmp Ceq f f0); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + destruct (Float32.cmp Clt f f0); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float32.cmp_swap. + destruct (Float32.cmp _ _ _); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float32.cmp_swap. + destruct (Float32.cmp _ _ _); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + destruct (Float32.cmp _ _ _); auto. +Qed. + +Lemma swap_comparison_cmpf: + forall v1 v2 cmp, + Val.lessdef (Val.cmpf cmp v1 v2) (Val.cmpf (swap_comparison cmp) v2 v1). +Proof. + intros. unfold Val.cmpf. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. + rewrite Float.cmp_swap. auto. +Qed. + +Lemma transl_cond_float64_correct: + forall cmp rd r1 r2 k rs m, + exists rs', + exec_straight ge (basics_to_code (transl_cond_float64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.cmpf cmp rs#r1 rs#r2) rs'#rd + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + intros. destruct cmp; simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpf. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpf. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +Qed. + +Lemma transl_cond_nofloat64_correct: + forall cmp rd r1 r2 k rs m, + exists rs', + exec_straight ge (basics_to_code (transl_cond_notfloat64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpf_bool cmp (rs r1) (rs r2)))) rs'#rd + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + intros. destruct cmp; simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. + rewrite Float.cmp_ne_eq. auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. + rewrite Float.cmp_ne_eq. simpl. destruct (Float.cmp Ceq f f0); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + destruct (Float.cmp Clt f f0); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float.cmp_swap. + destruct (Float.cmp _ _ _); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float.cmp_swap. + destruct (Float.cmp _ _ _); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + destruct (Float.cmp _ _ _); auto. +Qed. + Lemma transl_cond_op_correct: forall cond rd args k c rs m, transl_cond_op cond rd args k = OK c -> @@ -1003,6 +1135,14 @@ Proof. exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite MKTOT; eauto. ++ (* cmpfloat *) + exploit transl_cond_float64_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. ++ (* cmpnosingle *) + exploit transl_cond_nofloat64_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. ++ (* cmpsingle *) + exploit transl_cond_float32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. ++ (* cmpnosingle *) + exploit transl_cond_nofloat32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. Qed. (* diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 1b56d3ab..fa0ebfe6 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -12,6 +12,7 @@ Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. +Require Import Asmblockdeps Asmblockgenproof0. Local Open Scope error_monad_scope. @@ -21,555 +22,467 @@ Axiom schedule: bblock -> list bblock. Extract Constant schedule => "PostpassSchedulingOracle.schedule". -(** Specification of the "coming soon" Asmblockdeps.v *) -Inductive bblock_equiv (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
- | bblock_equiv_intro:
- (forall rs m,
- exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m) ->
- bblock_equiv ge f bb bb'.
-
-Axiom state': Type.
-Definition outcome' := option state'.
-
-Axiom bblock': Type.
-Extract Constant bblock' => "PostpassSchedulingOracle.bblock'". (* FIXME *)
-Axiom exec': genv -> function -> bblock' -> state' -> outcome'.
-Axiom match_states: state -> state' -> Prop.
-Axiom trans_block: bblock -> bblock'.
-Extract Constant trans_block => "PostpassSchedulingOracle.trans_block". (* FIXME *)
-Axiom trans_state: state -> state'.
-
-Axiom trans_state_match: forall S, match_states S (trans_state S).
-
-Inductive bblock_equiv' (ge: Genv.t fundef unit) (f: function) (bb bb': bblock') :=
- | bblock_equiv_intro':
- (forall s,
- exec' ge f bb s = exec' ge f bb' s) ->
- bblock_equiv' ge f bb bb'.
-
-Lemma bblock_equiv'_refl: forall ge fn tbb, bblock_equiv' ge fn tbb tbb.
-Proof.
- repeat constructor.
-Qed.
-
-
-
-Definition exec := exec_bblock.
-
-Axiom forward_simu:
- forall rs1 m1 rs2 m2 s1' b ge fn,
- exec ge fn b rs1 m1 = Next rs2 m2 ->
- match_states (State rs1 m1) s1' ->
- exists s2',
- exec' ge fn (trans_block b) s1' = Some s2'
- /\ match_states (State rs2 m2) s2'.
-
-Axiom forward_simu_stuck:
- forall rs1 m1 s1' b ge fn,
- exec ge fn b rs1 m1 = Stuck ->
- match_states (State rs1 m1) s1' ->
- exec' ge fn (trans_block b) s1' = None.
-
-Axiom trans_block_reverse_stuck:
- forall ge fn b rs m s',
- exec' ge fn (trans_block b) s' = None ->
- match_states (State rs m) s' ->
- exec ge fn b rs m = Stuck.
-
-Axiom state_equiv:
- forall S1 S2 S', match_states S1 S' /\ match_states S2 S' -> S1 = S2.
-
-
-(* TODO - replace it by the actual bblock_equivb' *)
-Axiom bblock_equivb': bblock' -> bblock' -> bool.
-Extract Constant bblock_equivb' => "PostpassSchedulingOracle.bblock_equivb'". (* FIXME *)
-
-Axiom bblock_equiv'_eq:
- forall ge fn b1 b2,
- bblock_equivb' b1 b2 = true <-> bblock_equiv' ge fn b1 b2.
-
-Lemma bblock_equivb'_refl: forall tbb, bblock_equivb' tbb tbb = true.
-Proof.
- intros. rewrite bblock_equiv'_eq. apply bblock_equiv'_refl.
- Unshelve. (* FIXME - problem of Genv and function *)
-Admitted.
-
-
-Lemma trans_equiv_stuck:
- forall b1 b2 ge fn rs m,
- bblock_equiv' ge fn (trans_block b1) (trans_block b2) ->
- (exec ge fn b1 rs m = Stuck <-> exec ge fn b2 rs m = Stuck).
-Proof.
- intros. inv H.
- pose (trans_state_match (State rs m)).
- split.
- - intros. eapply forward_simu_stuck in H; eauto. rewrite H0 in H. eapply trans_block_reverse_stuck; eassumption.
- - intros. eapply forward_simu_stuck in H; eauto. rewrite <- H0 in H. eapply trans_block_reverse_stuck; eassumption.
-Qed.
-
-
-
-Lemma bblock_equiv'_comm:
- forall ge fn b1 b2,
- bblock_equiv' ge fn b1 b2 <-> bblock_equiv' ge fn b2 b1.
-Proof.
- intros. repeat constructor. all: inv H; congruence.
-Qed.
-
-Theorem trans_exec:
- forall b1 b2 ge f, bblock_equiv' ge f (trans_block b1) (trans_block b2) -> bblock_equiv ge f b1 b2.
-Proof.
- repeat constructor. intros rs1 m1.
- destruct (exec_bblock _ _ b1 _ _) as [rs2 m2|] eqn:EXEB; destruct (exec_bblock _ _ b2 _ _) as [rs3 m3|] eqn:EXEB2; auto.
- - pose (trans_state_match (State rs1 m1)).
- exploit forward_simu.
- eapply EXEB.
- eapply m.
- intros (s2' & EXEB' & MS).
- exploit forward_simu.
- eapply EXEB2.
- eapply m.
- intros (s3' & EXEB'2 & MS2). inv H.
- rewrite H0 in EXEB'. rewrite EXEB'2 in EXEB'. inv EXEB'.
- exploit (state_equiv (State rs2 m2) (State rs3 m3) s2'). eauto.
- congruence.
- - rewrite trans_equiv_stuck in EXEB2. 2: eapply bblock_equiv'_comm; eauto. unfold exec in EXEB2. rewrite EXEB2 in EXEB. discriminate.
- - rewrite trans_equiv_stuck in EXEB; eauto. unfold exec in EXEB. rewrite EXEB in EXEB2. discriminate.
-Qed.
-
-
-
-(* Lemmas necessary for defining concat_all *)
-Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil.
-Proof.
- intros. destruct l; simpl.
- - contradiction.
- - discriminate.
-Qed.
-
-Lemma app_nonil2 {A: Type} : forall (l l': list A), l' <> nil -> l ++ l' <> nil.
-Proof.
- destruct l.
- - intros. simpl; auto.
- - intros. rewrite <- app_comm_cons. discriminate.
-Qed.
-
-
-
-Definition check_size bb :=
- if zlt Ptrofs.max_unsigned (size bb)
- then Error (msg "PostpassSchedulingproof.check_size")
- else OK tt.
-
-Program Definition concat2 (bb bb': bblock) : res bblock :=
- do ch <- check_size bb;
- do ch' <- check_size bb';
- match (exit bb) with
- | None =>
- match (header bb') with
- | nil =>
- match (exit bb') with
- | Some (PExpand (Pbuiltin _ _ _)) => Error (msg "PostpassSchedulingproof.concat2: builtin not alone")
- | _ => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |}
- end
- | _ => Error (msg "PostpassSchedulingproof.concat2")
- end
- | _ => Error (msg "PostpassSchedulingproof.concat2")
- end.
-Next Obligation.
- apply wf_bblock_refl. constructor.
- - destruct bb' as [hd' bdy' ex' WF']. destruct bb as [hd bdy ex WF]. simpl in *.
- apply wf_bblock_refl in WF'. apply wf_bblock_refl in WF.
- inversion_clear WF'. inversion_clear WF. clear H1 H3.
- inversion H2; inversion H0.
- + left. apply app_nonil. auto.
- + right. auto.
- + left. apply app_nonil2. auto.
- + right. auto.
- - unfold builtin_alone. intros. rewrite H0 in H.
- assert (Some (PExpand (Pbuiltin ef args res)) <> Some (PExpand (Pbuiltin ef args res))).
- apply (H ef args res). contradict H1. auto.
-Defined.
-
-Lemma concat2_zlt_size:
- forall a b bb,
- concat2 a b = OK bb ->
- size a <= Ptrofs.max_unsigned
- /\ size b <= Ptrofs.max_unsigned.
-Proof.
- intros. monadInv H.
- split.
- - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega.
- - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega.
-Qed.
-
-Lemma concat2_noexit:
- forall a b bb,
- concat2 a b = OK bb ->
- exit a = None.
-Proof.
- intros. destruct a as [hd bdy ex WF]; simpl in *.
- destruct ex as [e|]; simpl in *; auto.
- unfold concat2 in H. simpl in H. monadInv H.
-Qed.
-
-Lemma concat2_decomp:
- forall a b bb,
- concat2 a b = OK bb ->
- body bb = body a ++ body b
- /\ exit bb = exit b.
-Proof.
- intros. exploit concat2_noexit; eauto. intros.
- destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]; simpl in *.
- subst exa.
- unfold concat2 in H; simpl in H.
- destruct hdb.
- - destruct exb.
- + destruct c.
- * destruct i. monadInv H.
- * monadInv H. split; auto.
- + monadInv H. split; auto.
- - monadInv H.
-Qed.
-
-Lemma concat2_size:
- forall a b bb, concat2 a b = OK bb -> size bb = size a + size b.
-Proof.
- intros. unfold concat2 in H.
- destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *.
- destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2).
- - destruct c.
- + destruct i; try (monadInv EQ2).
- + monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity.
- - unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity.
-Qed.
-
-Lemma concat2_header:
- forall bb bb' tbb,
- concat2 bb bb' = OK tbb -> header bb = header tbb.
-Proof.
- intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *.
- unfold concat2 in H. simpl in H. monadInv H.
- destruct ex; try discriminate. destruct hd'; try discriminate. destruct ex'.
- - destruct c.
- + destruct i; discriminate.
- + congruence.
- - congruence.
-Qed.
-
-Lemma concat2_no_header_in_middle:
- forall bb bb' tbb,
- concat2 bb bb' = OK tbb ->
- header bb' = nil.
-Proof.
- intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *.
- unfold concat2 in H. simpl in H. monadInv H.
- destruct ex; try discriminate. destruct hd'; try discriminate. reflexivity.
-Qed.
-
-
-
-Fixpoint concat_all (lbb: list bblock) : res bblock :=
- match lbb with
- | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list")
- | bb::nil => OK bb
- | bb::lbb =>
- do bb' <- concat_all lbb;
- concat2 bb bb'
- end.
-
-Lemma concat_all_size :
- forall lbb a bb bb',
- concat_all (a :: lbb) = OK bb ->
- concat_all lbb = OK bb' ->
- size bb = size a + size bb'.
-Proof.
- intros. unfold concat_all in H. fold concat_all in H.
- destruct lbb; try discriminate.
- monadInv H. rewrite H0 in EQ. inv EQ.
- apply concat2_size. assumption.
-Qed.
-
-Lemma concat_all_header:
- forall lbb bb tbb,
- concat_all (bb::lbb) = OK tbb -> header bb = header tbb.
-Proof.
- destruct lbb.
- - intros. simpl in H. congruence.
- - intros. simpl in H. destruct lbb.
- + inv H. eapply concat2_header; eassumption.
- + monadInv H. eapply concat2_header; eassumption.
-Qed.
-
-Lemma concat_all_no_header_in_middle:
- forall lbb tbb,
- concat_all lbb = OK tbb ->
- Forall (fun b => header b = nil) (tail lbb).
-Proof.
- induction lbb; intros; try constructor.
- simpl. simpl in H. destruct lbb.
- - constructor.
- - monadInv H. simpl tl in IHlbb. constructor.
- + apply concat2_no_header_in_middle in EQ0. apply concat_all_header in EQ. congruence.
- + apply IHlbb in EQ. assumption.
-Qed.
-
-
-
-Definition verify_schedule (bb bb' : bblock) : res unit :=
- match (bblock_equivb' (trans_block bb) (trans_block bb')) with
- | true => OK tt
- | false => Error (msg "PostpassScheduling.verify_schedule")
- end.
-
-Lemma verify_schedule_refl:
- forall bb, verify_schedule bb bb = OK tt.
-Proof.
- intros. unfold verify_schedule. rewrite bblock_equivb'_refl. reflexivity.
-Qed.
-
-
-
-Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").
-
-Lemma verify_size_size:
- forall bb lbb, verify_size bb lbb = OK tt -> size bb = size_blocks lbb.
-Proof.
- intros. unfold verify_size in H. destruct (size bb =? size_blocks lbb) eqn:SIZE; try discriminate.
- apply Z.eqb_eq. assumption.
-Qed.
-
-
-
-Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}.
-Next Obligation.
- destruct bb; simpl. assumption.
-Defined.
-
-Lemma no_header_size:
- forall bb, size (no_header bb) = size bb.
-Proof.
- intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity.
-Qed.
-
-Axiom trans_block_noheader_inv: forall bb, trans_block (no_header bb) = trans_block bb.
-
-Lemma verify_schedule_no_header:
- forall bb bb',
- verify_schedule (no_header bb) bb' = verify_schedule bb bb'.
-Proof.
- intros. unfold verify_schedule. rewrite trans_block_noheader_inv. reflexivity.
-Qed.
-
-
-
-Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}.
-Next Obligation.
- destruct bb; simpl. assumption.
-Defined.
-
-Axiom trans_block_header_inv: forall bb hd, trans_block (stick_header hd bb) = trans_block bb.
-
-Lemma stick_header_size:
- forall h bb, size (stick_header h bb) = size bb.
-Proof.
- intros. destruct bb. unfold stick_header. simpl. reflexivity.
-Qed.
-
-Lemma stick_header_no_header:
- forall bb, stick_header (header bb) (no_header bb) = bb.
-Proof.
- intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity.
-Qed.
-
-Lemma stick_header_verify_schedule:
- forall hd bb' hbb' bb,
- stick_header hd bb' = hbb' ->
- verify_schedule bb bb' = verify_schedule bb hbb'.
-Proof.
- intros. unfold verify_schedule. rewrite <- H. rewrite trans_block_header_inv. reflexivity.
-Qed.
-
-Lemma check_size_stick_header:
- forall bb hd,
- check_size bb = check_size (stick_header hd bb).
-Proof.
- intros. unfold check_size. rewrite stick_header_size. reflexivity.
-Qed.
-
-Lemma stick_header_concat2:
- forall bb bb' hd tbb,
- concat2 bb bb' = OK tbb ->
- concat2 (stick_header hd bb) bb' = OK (stick_header hd tbb).
-Proof.
- intros. monadInv H. erewrite check_size_stick_header in EQ.
- unfold concat2. rewrite EQ. rewrite EQ1. simpl.
- destruct bb as [hdr bdy ex COR]; destruct bb' as [hdr' bdy' ex' COR']; simpl in *.
- destruct ex; try discriminate. destruct hdr'; try discriminate. destruct ex'.
- - destruct c.
- + destruct i. discriminate.
- + inv EQ2. unfold stick_header; simpl. reflexivity.
- - inv EQ2. unfold stick_header; simpl. reflexivity.
-Qed.
-
-Lemma stick_header_concat_all:
- forall bb c tbb hd,
- concat_all (bb :: c) = OK tbb ->
- concat_all (stick_header hd bb :: c) = OK (stick_header hd tbb).
-Proof.
- intros. simpl in *. destruct c; try congruence.
- monadInv H. rewrite EQ. simpl.
- apply stick_header_concat2. assumption.
-Qed.
-
-
-
-Definition stick_header_code (h : list label) (lbb : list bblock) :=
- match (head lbb) with
- | None => Error (msg "PostpassScheduling.stick_header: empty schedule")
- | Some fst => OK ((stick_header h fst) :: tail lbb)
- end.
-
-Lemma stick_header_code_no_header:
- forall bb c,
- stick_header_code (header bb) (no_header bb :: c) = OK (bb :: c).
-Proof.
- intros. unfold stick_header_code. simpl. rewrite stick_header_no_header. reflexivity.
-Qed.
-
-Lemma hd_tl_size:
- forall lbb bb, hd_error lbb = Some bb -> size_blocks lbb = size bb + size_blocks (tl lbb).
-Proof.
- destruct lbb.
- - intros. simpl in H. discriminate.
- - intros. simpl in H. inv H. simpl. reflexivity.
-Qed.
-
-Lemma stick_header_code_size:
- forall h lbb lbb', stick_header_code h lbb = OK lbb' -> size_blocks lbb = size_blocks lbb'.
-Proof.
- intros. unfold stick_header_code in H. destruct (hd_error lbb) eqn:HD; try discriminate.
- inv H. simpl. rewrite stick_header_size. erewrite hd_tl_size; eauto.
-Qed.
-
-Lemma stick_header_code_no_header_in_middle:
- forall c h lbb,
- stick_header_code h c = OK lbb ->
- Forall (fun b => header b = nil) (tl c) ->
- Forall (fun b => header b = nil) (tl lbb).
-Proof.
- destruct c; intros.
- - unfold stick_header_code in H. simpl in H. discriminate.
- - unfold stick_header_code in H. simpl in H. inv H. simpl in H0.
- simpl. assumption.
-Qed.
-
-Lemma stick_header_code_concat_all:
- forall hd lbb hlbb tbb,
- stick_header_code hd lbb = OK hlbb ->
- concat_all lbb = OK tbb ->
- exists htbb,
- concat_all hlbb = OK htbb
- /\ stick_header hd tbb = htbb.
-Proof.
- intros. exists (stick_header hd tbb). split; auto.
- destruct lbb.
- - unfold stick_header_code in H. simpl in H. discriminate.
- - unfold stick_header_code in H. simpl in H. inv H.
- apply stick_header_concat_all. assumption.
-Qed.
-
-
-
-Definition do_schedule (bb: bblock) : list bblock :=
- if (Z.eqb (size bb) 1) then bb::nil else schedule bb.
-
-Definition verified_schedule (bb : bblock) : res (list bblock) :=
- let bb' := no_header bb in
- let lbb := do_schedule bb' in
- do tbb <- concat_all lbb;
- do sizecheck <- verify_size bb lbb;
- do schedcheck <- verify_schedule bb' tbb;
- stick_header_code (header bb) lbb.
-
-Lemma verified_schedule_size:
- forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb.
-Proof.
- intros. monadInv H. erewrite <- stick_header_code_size; eauto.
- apply verify_size_size.
- destruct x0; try discriminate. assumption.
-Qed.
-
-Lemma verified_schedule_single_inst:
- forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil).
-Proof.
- intros. unfold verified_schedule.
- unfold do_schedule. rewrite no_header_size. rewrite H. simpl.
- unfold verify_size. simpl. rewrite no_header_size. rewrite Z.add_0_r. cutrewrite (size bb =? size bb = true). rewrite verify_schedule_refl. simpl.
- apply stick_header_code_no_header.
- rewrite H. reflexivity.
-Qed.
-
-Lemma verified_schedule_no_header_in_middle:
- forall lbb bb,
- verified_schedule bb = OK lbb ->
- Forall (fun b => header b = nil) (tail lbb).
-Proof.
- intros. monadInv H. eapply stick_header_code_no_header_in_middle; eauto.
- eapply concat_all_no_header_in_middle. eassumption.
-Qed.
-
-Lemma verified_schedule_header:
- forall bb tbb lbb,
- verified_schedule bb = OK (tbb :: lbb) ->
- header bb = header tbb
- /\ Forall (fun b => header b = nil) lbb.
-Proof.
- intros. split.
- - monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3.
- simpl. reflexivity.
- - apply verified_schedule_no_header_in_middle in H. assumption.
-Qed.
-
-Theorem verified_schedule_correct:
- forall ge f bb lbb,
- verified_schedule bb = OK lbb ->
- exists tbb,
- concat_all lbb = OK tbb
- /\ bblock_equiv ge f bb tbb.
-Proof.
- intros. monadInv H.
- exploit stick_header_code_concat_all; eauto.
- intros (tbb & CONC & STH).
- exists tbb. split; auto.
- rewrite verify_schedule_no_header in EQ0. erewrite stick_header_verify_schedule in EQ0; eauto.
- apply trans_exec. apply bblock_equiv'_eq. unfold verify_schedule in EQ0.
- destruct (bblock_equivb' _ _); auto; try discriminate.
-Qed.
-
-
-
-Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
- match lbb with
- | nil => OK nil
- | (cons bb lbb) =>
- do tlbb <- transf_blocks lbb;
- do tbb <- verified_schedule bb;
- OK (tbb ++ tlbb)
- end.
-
-Definition transl_function (f: function) : res function :=
- do lb <- transf_blocks (fn_blocks f);
- OK (mkfunction (fn_sig f) lb).
-
-Definition transf_function (f: function) : res 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: fundef) : res fundef :=
- transf_partial_fundef transf_function f.
-
-Definition transf_program (p: program) : res program :=
- transform_partial_program transf_fundef p.
\ No newline at end of file +Definition state' := L.mem. +Definition outcome' := option state'. + +Definition bblock' := L.bblock. + +Definition exec' := L.run. + +Definition exec := exec_bblock. + +Definition bblock_equivb' := bblock_equivb. + +Lemma bblock_equivb'_refl (ge: Genv.t fundef unit) (fn: function): forall tbb, bblock_equivb' tbb tbb = true. +Proof. + intros. rewrite bblock_equiv'_eq. apply bblock_equiv'_refl. + Unshelve. (* FIXME - problem of Genv and function *) + constructor; auto. +Qed. + +Lemma trans_equiv_stuck: + forall b1 b2 ge fn rs m, + bblock_equiv' (P.Genv ge fn) (trans_block b1) (trans_block b2) -> + (exec ge fn b1 rs m = Stuck <-> exec ge fn b2 rs m = Stuck). +Proof. + intros. inv H. + pose (trans_state_match (State rs m)). + split. + - intros. eapply forward_simu_stuck in H; eauto. rewrite H0 in H. eapply trans_block_reverse_stuck. + reflexivity. eassumption. eassumption. + - intros. eapply forward_simu_stuck in H; eauto. rewrite <- H0 in H. eapply trans_block_reverse_stuck. + reflexivity. eassumption. eassumption. +Qed. + + +Lemma bblock_equiv'_comm: + forall ge fn b1 b2, + bblock_equiv' (P.Genv ge fn) b1 b2 <-> bblock_equiv' (P.Genv ge fn) b2 b1. +Proof. + intros. repeat constructor. all: inv H; congruence. +Qed. + +Theorem trans_exec: + forall b1 b2 ge f, bblock_equiv' (P.Genv ge f) (trans_block b1) (trans_block b2) -> bblock_equiv ge f b1 b2. +Proof. + repeat constructor. intros rs1 m1. + destruct (exec_bblock _ _ b1 _ _) as [rs2 m2|] eqn:EXEB; destruct (exec_bblock _ _ b2 _ _) as [rs3 m3|] eqn:EXEB2; auto. + - pose (trans_state_match (State rs1 m1)). + exploit forward_simu. + reflexivity. + eapply EXEB. + eapply m. + intros (s2' & EXEB' & MS). + exploit forward_simu. + reflexivity. + eapply EXEB2. + eapply m. + intros (s3' & EXEB'2 & MS2). inv H. + rewrite H0 in EXEB'. rewrite EXEB'2 in EXEB'. inv EXEB'. + exploit (state_equiv (State rs2 m2) (State rs3 m3) s2'). eauto. + congruence. + - rewrite trans_equiv_stuck in EXEB2. 2: eapply bblock_equiv'_comm; eauto. unfold exec in EXEB2. rewrite EXEB2 in EXEB. discriminate. + - rewrite trans_equiv_stuck in EXEB; eauto. unfold exec in EXEB. rewrite EXEB in EXEB2. discriminate. +Qed. + + + +(* Lemmas necessary for defining concat_all *) +Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil. +Proof. + intros. destruct l; simpl. + - contradiction. + - discriminate. +Qed. + +Lemma app_nonil2 {A: Type} : forall (l l': list A), l' <> nil -> l ++ l' <> nil. +Proof. + destruct l. + - intros. simpl; auto. + - intros. rewrite <- app_comm_cons. discriminate. +Qed. + + + +Definition check_size bb := + if zlt Ptrofs.max_unsigned (size bb) + then Error (msg "PostpassSchedulingproof.check_size") + else OK tt. + +Program Definition concat2 (bb bb': bblock) : res bblock := + do ch <- check_size bb; + do ch' <- check_size bb'; + match (exit bb) with + | None => + match (header bb') with + | nil => + match (exit bb') with + | Some (PExpand (Pbuiltin _ _ _)) => Error (msg "PostpassSchedulingproof.concat2: builtin not alone") + | _ => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |} + end + | _ => Error (msg "PostpassSchedulingproof.concat2") + end + | _ => Error (msg "PostpassSchedulingproof.concat2") + end. +Next Obligation. + apply wf_bblock_refl. constructor. + - destruct bb' as [hd' bdy' ex' WF']. destruct bb as [hd bdy ex WF]. simpl in *. + apply wf_bblock_refl in WF'. apply wf_bblock_refl in WF. + inversion_clear WF'. inversion_clear WF. clear H1 H3. + inversion H2; inversion H0. + + left. apply app_nonil. auto. + + right. auto. + + left. apply app_nonil2. auto. + + right. auto. + - unfold builtin_alone. intros. rewrite H0 in H. + assert (Some (PExpand (Pbuiltin ef args res)) <> Some (PExpand (Pbuiltin ef args res))). + apply (H ef args res). contradict H1. auto. +Defined. + +Lemma concat2_zlt_size: + forall a b bb, + concat2 a b = OK bb -> + size a <= Ptrofs.max_unsigned + /\ size b <= Ptrofs.max_unsigned. +Proof. + intros. monadInv H. + split. + - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega. + - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega. +Qed. + +Lemma concat2_noexit: + forall a b bb, + concat2 a b = OK bb -> + exit a = None. +Proof. + intros. destruct a as [hd bdy ex WF]; simpl in *. + destruct ex as [e|]; simpl in *; auto. + unfold concat2 in H. simpl in H. monadInv H. +Qed. + +Lemma concat2_decomp: + forall a b bb, + concat2 a b = OK bb -> + body bb = body a ++ body b + /\ exit bb = exit b. +Proof. + intros. exploit concat2_noexit; eauto. intros. + destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]; simpl in *. + subst exa. + unfold concat2 in H; simpl in H. + destruct hdb. + - destruct exb. + + destruct c. + * destruct i. monadInv H. + * monadInv H. split; auto. + + monadInv H. split; auto. + - monadInv H. +Qed. + +Lemma concat2_size: + forall a b bb, concat2 a b = OK bb -> size bb = size a + size b. +Proof. + intros. unfold concat2 in H. + destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *. + destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2). + - destruct c. + + destruct i; try (monadInv EQ2). + + monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity. + - unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity. +Qed. + +Lemma concat2_header: + forall bb bb' tbb, + concat2 bb bb' = OK tbb -> header bb = header tbb. +Proof. + intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *. + unfold concat2 in H. simpl in H. monadInv H. + destruct ex; try discriminate. destruct hd'; try discriminate. destruct ex'. + - destruct c. + + destruct i; discriminate. + + congruence. + - congruence. +Qed. + +Lemma concat2_no_header_in_middle: + forall bb bb' tbb, + concat2 bb bb' = OK tbb -> + header bb' = nil. +Proof. + intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *. + unfold concat2 in H. simpl in H. monadInv H. + destruct ex; try discriminate. destruct hd'; try discriminate. reflexivity. +Qed. + + + +Fixpoint concat_all (lbb: list bblock) : res bblock := + match lbb with + | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list") + | bb::nil => OK bb + | bb::lbb => + do bb' <- concat_all lbb; + concat2 bb bb' + end. + +Lemma concat_all_size : + forall lbb a bb bb', + concat_all (a :: lbb) = OK bb -> + concat_all lbb = OK bb' -> + size bb = size a + size bb'. +Proof. + intros. unfold concat_all in H. fold concat_all in H. + destruct lbb; try discriminate. + monadInv H. rewrite H0 in EQ. inv EQ. + apply concat2_size. assumption. +Qed. + +Lemma concat_all_header: + forall lbb bb tbb, + concat_all (bb::lbb) = OK tbb -> header bb = header tbb. +Proof. + destruct lbb. + - intros. simpl in H. congruence. + - intros. simpl in H. destruct lbb. + + inv H. eapply concat2_header; eassumption. + + monadInv H. eapply concat2_header; eassumption. +Qed. + +Lemma concat_all_no_header_in_middle: + forall lbb tbb, + concat_all lbb = OK tbb -> + Forall (fun b => header b = nil) (tail lbb). +Proof. + induction lbb; intros; try constructor. + simpl. simpl in H. destruct lbb. + - constructor. + - monadInv H. simpl tl in IHlbb. constructor. + + apply concat2_no_header_in_middle in EQ0. apply concat_all_header in EQ. congruence. + + apply IHlbb in EQ. assumption. +Qed. + + + +Definition verify_schedule (bb bb' : bblock) : res unit := + match (bblock_equivb' (trans_block bb) (trans_block bb')) with + | true => OK tt + | false => Error (msg "PostpassScheduling.verify_schedule") + end. + +Lemma verify_schedule_refl (ge: Genv.t fundef unit) (fn: function): + forall bb, verify_schedule bb bb = OK tt. +Proof. + intros. unfold verify_schedule. rewrite bblock_equivb'_refl. reflexivity. all: auto. +Qed. + + + +Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size"). + +Lemma verify_size_size: + forall bb lbb, verify_size bb lbb = OK tt -> size bb = size_blocks lbb. +Proof. + intros. unfold verify_size in H. destruct (size bb =? size_blocks lbb) eqn:SIZE; try discriminate. + apply Z.eqb_eq. assumption. +Qed. + +Lemma verify_schedule_no_header: + forall bb bb', + verify_schedule (no_header bb) bb' = verify_schedule bb bb'. +Proof. + intros. unfold verify_schedule. rewrite trans_block_noheader_inv. reflexivity. +Qed. + + +Lemma stick_header_verify_schedule: + forall hd bb' hbb' bb, + stick_header hd bb' = hbb' -> + verify_schedule bb bb' = verify_schedule bb hbb'. +Proof. + intros. unfold verify_schedule. rewrite <- H. rewrite trans_block_header_inv. reflexivity. +Qed. + +Lemma check_size_stick_header: + forall bb hd, + check_size bb = check_size (stick_header hd bb). +Proof. + intros. unfold check_size. rewrite stick_header_size. reflexivity. +Qed. + +Lemma stick_header_concat2: + forall bb bb' hd tbb, + concat2 bb bb' = OK tbb -> + concat2 (stick_header hd bb) bb' = OK (stick_header hd tbb). +Proof. + intros. monadInv H. erewrite check_size_stick_header in EQ. + unfold concat2. rewrite EQ. rewrite EQ1. simpl. + destruct bb as [hdr bdy ex COR]; destruct bb' as [hdr' bdy' ex' COR']; simpl in *. + destruct ex; try discriminate. destruct hdr'; try discriminate. destruct ex'. + - destruct c. + + destruct i. discriminate. + + inv EQ2. unfold stick_header; simpl. reflexivity. + - inv EQ2. unfold stick_header; simpl. reflexivity. +Qed. + +Lemma stick_header_concat_all: + forall bb c tbb hd, + concat_all (bb :: c) = OK tbb -> + concat_all (stick_header hd bb :: c) = OK (stick_header hd tbb). +Proof. + intros. simpl in *. destruct c; try congruence. + monadInv H. rewrite EQ. simpl. + apply stick_header_concat2. assumption. +Qed. + + + +Definition stick_header_code (h : list label) (lbb : list bblock) := + match (head lbb) with + | None => Error (msg "PostpassScheduling.stick_header: empty schedule") + | Some fst => OK ((stick_header h fst) :: tail lbb) + end. + +Lemma stick_header_code_no_header: + forall bb c, + stick_header_code (header bb) (no_header bb :: c) = OK (bb :: c). +Proof. + intros. unfold stick_header_code. simpl. rewrite stick_header_no_header. reflexivity. +Qed. + +Lemma hd_tl_size: + forall lbb bb, hd_error lbb = Some bb -> size_blocks lbb = size bb + size_blocks (tl lbb). +Proof. + destruct lbb. + - intros. simpl in H. discriminate. + - intros. simpl in H. inv H. simpl. reflexivity. +Qed. + +Lemma stick_header_code_size: + forall h lbb lbb', stick_header_code h lbb = OK lbb' -> size_blocks lbb = size_blocks lbb'. +Proof. + intros. unfold stick_header_code in H. destruct (hd_error lbb) eqn:HD; try discriminate. + inv H. simpl. rewrite stick_header_size. erewrite hd_tl_size; eauto. +Qed. + +Lemma stick_header_code_no_header_in_middle: + forall c h lbb, + stick_header_code h c = OK lbb -> + Forall (fun b => header b = nil) (tl c) -> + Forall (fun b => header b = nil) (tl lbb). +Proof. + destruct c; intros. + - unfold stick_header_code in H. simpl in H. discriminate. + - unfold stick_header_code in H. simpl in H. inv H. simpl in H0. + simpl. assumption. +Qed. + +Lemma stick_header_code_concat_all: + forall hd lbb hlbb tbb, + stick_header_code hd lbb = OK hlbb -> + concat_all lbb = OK tbb -> + exists htbb, + concat_all hlbb = OK htbb + /\ stick_header hd tbb = htbb. +Proof. + intros. exists (stick_header hd tbb). split; auto. + destruct lbb. + - unfold stick_header_code in H. simpl in H. discriminate. + - unfold stick_header_code in H. simpl in H. inv H. + apply stick_header_concat_all. assumption. +Qed. + + + +Definition do_schedule (bb: bblock) : list bblock := + if (Z.eqb (size bb) 1) then bb::nil else schedule bb. + +Definition verified_schedule (bb : bblock) : res (list bblock) := + let bb' := no_header bb in + let lbb := do_schedule bb' in + do tbb <- concat_all lbb; + do sizecheck <- verify_size bb lbb; + do schedcheck <- verify_schedule bb' tbb; + stick_header_code (header bb) lbb. + +Lemma verified_schedule_size: + forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb. +Proof. + intros. monadInv H. erewrite <- stick_header_code_size; eauto. + apply verify_size_size. + destruct x0; try discriminate. assumption. +Qed. + +Lemma verified_schedule_single_inst (ge: Genv.t fundef unit) (fn: function): + forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil). +Proof. + intros. unfold verified_schedule. + unfold do_schedule. rewrite no_header_size. rewrite H. simpl. + unfold verify_size. simpl. rewrite no_header_size. rewrite Z.add_0_r. cutrewrite (size bb =? size bb = true). rewrite verify_schedule_refl. simpl. + apply stick_header_code_no_header. all: auto. + rewrite H. reflexivity. +Qed. + +Lemma verified_schedule_no_header_in_middle: + forall lbb bb, + verified_schedule bb = OK lbb -> + Forall (fun b => header b = nil) (tail lbb). +Proof. + intros. monadInv H. eapply stick_header_code_no_header_in_middle; eauto. + eapply concat_all_no_header_in_middle. eassumption. +Qed. + +Lemma verified_schedule_header: + forall bb tbb lbb, + verified_schedule bb = OK (tbb :: lbb) -> + header bb = header tbb + /\ Forall (fun b => header b = nil) lbb. +Proof. + intros. split. + - monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3. + simpl. reflexivity. + - apply verified_schedule_no_header_in_middle in H. assumption. +Qed. + +Theorem verified_schedule_correct: + forall ge f bb lbb, + verified_schedule bb = OK lbb -> + exists tbb, + concat_all lbb = OK tbb + /\ bblock_equiv ge f bb tbb. +Proof. + intros. monadInv H. + exploit stick_header_code_concat_all; eauto. + intros (tbb & CONC & STH). + exists tbb. split; auto. + rewrite verify_schedule_no_header in EQ0. erewrite stick_header_verify_schedule in EQ0; eauto. + apply trans_exec. apply bblock_equiv'_eq. unfold verify_schedule in EQ0. unfold bblock_equivb' in EQ0. + destruct (bblock_equivb _ _); auto; try discriminate. +Qed. + + + +Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) := + match lbb with + | nil => OK nil + | (cons bb lbb) => + do tlbb <- transf_blocks lbb; + do tbb <- verified_schedule bb; + OK (tbb ++ tlbb) + end. + +Definition transl_function (f: function) : res function := + do lb <- transf_blocks (fn_blocks f); + OK (mkfunction (fn_sig f) lb). + +Definition transf_function (f: function) : res 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: fundef) : res fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 54a27966..db50e3a5 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -40,14 +40,23 @@ let arith_rr_str = function | Pfnarrowdw -> "Pfnarrowdw" | Pfwidenlwd -> "Pfwidenlwd" | Pfloatwrnsz -> "Pfloatwrnsz" + | Pfloatuwrnsz -> "Pfloatuwrnsz" + | Pfloatudrnsz_i32 -> "Pfloatudrnsz_i32" | Pfloatudrnsz -> "Pfloatudrnsz" | Pfloatdrnsz -> "Pfloatdrnsz" + | Pfloatdrnsz_i32 -> "Pfloatdrnsz_i32" | Pfixedwrzz -> "Pfixedwrzz" + | Pfixeduwrzz -> "Pfixeduwrzz" | Pfixeddrzz -> "Pfixeddrzz" + | Pfixedudrzz -> "Pfixedudrzz" + | Pfixeddrzz_i32 -> "Pfixeddrzz_i32" + | Pfixedudrzz_i32 -> "Pfixedudrzz_i32" let arith_rrr_str = function | Pcompw it -> "Pcompw" | Pcompl it -> "Pcompl" + | Pfcompw ft -> "Pfcompw" + | Pfcompl ft -> "Pfcompl" | Paddw -> "Paddw" | Psubw -> "Psubw" | Pmulw -> "Pmulw" @@ -298,6 +307,10 @@ let alu_lite : int array = let resmap = fun r -> match r with | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 | _ -> 0 in Array.of_list (List.map resmap resource_names) +let alu_lite_x : int array = let resmap = fun r -> match r with + | "ISSUE" -> 2 | "TINY" -> 1 | "LITE" -> 1 | _ -> 0 + in Array.of_list (List.map resmap resource_names) + let alu_full : int array = let resmap = fun r -> match r with | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 | "ALU" -> 1 | _ -> 0 in Array.of_list (List.map resmap resource_names) @@ -365,7 +378,8 @@ type real_instruction = (* FPU *) | Fabsd | Fabsw | Fnegw | Fnegd | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw - | Fnarrowdw | Fwidenlwd | Floatwz | Floatdz | Floatudz | Fixedwz | Fixeddz + | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz + | Fcompw | Fcompd let ab_inst_to_real = function | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw @@ -374,6 +388,8 @@ let ab_inst_to_real = function | "Pandl" | "Pandil" -> Andd | "Pcompw" | "Pcompiw" -> Compw | "Pcompl" | "Pcompil" -> Compd + | "Pfcompw" -> Fcompw + | "Pfcompl" -> Fcompd | "Pmulw" -> Mulw | "Pmull" -> Muld | "Porw" | "Poriw" -> Orw @@ -395,10 +411,17 @@ let ab_inst_to_real = function | "Pfnarrowdw" -> Fnarrowdw | "Pfwidenlwd" -> Fwidenlwd | "Pfloatwrnsz" -> Floatwz + | "Pfloatuwrnsz" -> Floatuwz | "Pfloatdrnsz" -> Floatdz + | "Pfloatdrnsz_i32" -> Floatdz | "Pfloatudrnsz" -> Floatudz + | "Pfloatudrnsz_i32" -> Floatudz | "Pfixedwrzz" -> Fixedwz + | "Pfixeduwrzz" -> Fixeduwz | "Pfixeddrzz" -> Fixeddz + | "Pfixedudrzz" -> Fixedudz + | "Pfixeddrzz_i32" -> Fixeddz + | "Pfixedudrzz_i32" -> Fixedudz | "Plb" -> Lbs | "Plbu" -> Lbz @@ -456,6 +479,12 @@ let rec_to_usage r = | Compd -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y) + | Fcompw -> (match encoding with None -> alu_lite + | Some U6 | Some S10 | Some U27L5 -> alu_lite_x + | _ -> raise InvalidEncoding) + | Fcompd -> (match encoding with None -> alu_lite + | Some U6 | Some S10 | Some U27L5 -> alu_lite_x + | _ -> raise InvalidEncoding) | Make -> (match encoding with Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y @@ -469,7 +498,7 @@ let rec_to_usage r = | Nop -> alu_nop | Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding) | Sxwd | Zxwd -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding) - | Fixedwz | Floatwz | Fixeddz | Floatdz | Floatudz -> mau + | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> (match encoding with None | Some U6 | Some S10 -> lsu_data | Some U27L5 | Some U27L10 -> lsu_data_x @@ -488,9 +517,9 @@ let real_inst_to_latency = function | Nop -> 0 (* Only goes through ID *) | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make - | Sxwd | Zxwd + | Sxwd | Zxwd | Fcompw | Fcompd -> 1 - | Floatwz | Fixedwz | Floatdz | Floatudz | Fixeddz -> 4 + | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 | Mulw | Muld -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Sb | Sh | Sw | Sd diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2c3b8454..2ecb494d 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -10,675 +10,675 @@ (* *) (* *********************************************************************) -Require Import Coqlib Errors.
-Require Import Integers Floats AST Linking.
-Require Import Values Memory Events Globalenvs Smallstep.
-Require Import Op Locations Machblock Conventions Asmblock.
-Require Import Asmblockgenproof0.
-Require Import PostpassScheduling.
-Require Import Asmblockgenproof.
-Require Import Axioms.
-
-Local Open Scope error_monad_scope.
-
-Definition match_prog (p tp: Asmblock.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.
-
-Remark builtin_body_nil:
- forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
-Proof.
- intros. destruct bb as [hd bdy ex WF]. simpl in *.
- apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.
- eapply H1; eauto.
-Qed.
-
-Lemma verified_schedule_builtin_idem:
- forall bb ef args res lbb,
- exit bb = Some (PExpand (Pbuiltin ef args res)) ->
- verified_schedule bb = OK lbb ->
- lbb = bb :: nil.
-Proof.
- intros. exploit builtin_body_nil; eauto. intros.
- rewrite verified_schedule_single_inst in H0.
- - inv H0. auto.
- - unfold size. rewrite H. rewrite H1. simpl. auto.
-Qed.
-
-Lemma exec_body_app:
- forall l l' ge rs m rs'' m'',
- exec_body ge (l ++ l') rs m = Next rs'' m'' ->
- exists rs' m',
- exec_body ge l rs m = Next rs' m'
- /\ exec_body ge l' rs' m' = Next rs'' m''.
-Proof.
- induction l.
- - intros. simpl in H. repeat eexists. auto.
- - intros. rewrite <- app_comm_cons in H. simpl in H.
- destruct (exec_basic_instr ge a rs m) eqn:EXEBI.
- + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).
- repeat eexists. simpl. rewrite EXEBI. eauto. auto.
- + discriminate.
-Qed.
-
-Lemma exec_body_pc:
- forall l ge rs1 m1 rs2 m2,
- exec_body ge l rs1 m1 = Next rs2 m2 ->
- rs2 PC = rs1 PC.
-Proof.
- induction l.
- - intros. inv H. auto.
- - intros until m2. intro EXEB.
- inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.
- eapply IHl in H0. rewrite H0.
- erewrite exec_basic_instr_pc; eauto.
-Qed.
-
-Lemma next_eq {A: Type}:
- forall (rs rs':A) m m',
- rs = rs' -> m = m' -> Next rs m = Next rs' m'.
-Proof.
- intros. congruence.
-Qed.
-
-Lemma regset_double_set:
- forall r1 r2 (rs: regset) v1 v2,
- r1 <> r2 ->
- (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1).
-Proof.
- intros. apply functional_extensionality. intros r. destruct (preg_eq r r1).
- - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto.
- - destruct (preg_eq r r2).
- + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto.
- + repeat (rewrite Pregmap.gso; auto).
-Qed.
-
-Lemma regset_double_set_id:
- forall r (rs: regset) v1 v2,
- (rs # r <- v1 # r <- v2) = (rs # r <- v2).
-Proof.
- intros. apply functional_extensionality. intros. destruct (preg_eq r x).
- - subst r. repeat (rewrite Pregmap.gss; auto).
- - repeat (rewrite Pregmap.gso); auto.
-Qed.
-
-Lemma exec_load_pc_var:
- forall ge t rs m rd ra ofs rs' m' v,
- exec_load ge t rs m rd ra ofs = Next rs' m' ->
- exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
-Proof.
- intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
- destruct (Mem.loadv _ _ _).
- - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
- - discriminate.
-Qed.
-
-Lemma exec_store_pc_var:
- forall ge t rs m rd ra ofs rs' m' v,
- exec_store ge t rs m rd ra ofs = Next rs' m' ->
- exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
-Proof.
- intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
- destruct (Mem.storev _ _ _).
- - inv H. apply next_eq; auto.
- - discriminate.
-Qed.
-
-Lemma exec_basic_instr_pc_var:
- forall ge i rs m rs' m' v,
- exec_basic_instr ge i rs m = Next rs' m' ->
- exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.
-Proof.
- intros. unfold exec_basic_instr in *. destruct i.
- - unfold exec_arith_instr in *. destruct i; destruct i.
- all: try (exploreInst; inv H; apply next_eq; auto;
- apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
-
- (* Some cases treated seperately because exploreInst destructs too much *)
- all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
- - exploreInst; apply exec_load_pc_var; auto.
- - exploreInst; apply exec_store_pc_var; auto.
- - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).
- destruct (Mem.storev _ _ _ _); try discriminate.
- inv H. apply next_eq; auto. apply functional_extensionality. intros.
- rewrite (regset_double_set GPR32 PC); try discriminate.
- rewrite (regset_double_set GPR12 PC); try discriminate.
- rewrite (regset_double_set GPR14 PC); try discriminate. reflexivity.
- - repeat (rewrite Pregmap.gso; try discriminate).
- destruct (Mem.loadv _ _ _); try discriminate.
- destruct (rs GPR12); try discriminate.
- destruct (Mem.free _ _ _ _); try discriminate.
- inv H. apply next_eq; auto.
- rewrite (regset_double_set GPR32 PC).
- rewrite (regset_double_set GPR12 PC). reflexivity.
- all: discriminate.
- - destruct rs0; try discriminate. inv H. apply next_eq; auto.
- repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
- - destruct rd; try discriminate. inv H. apply next_eq; auto.
- repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
- - inv H. apply next_eq; auto.
-Qed.
-
-Lemma exec_body_pc_var:
- forall l ge rs m rs' m' v,
- exec_body ge l rs m = Next rs' m' ->
- exec_body ge l (rs # PC <- v) m = Next (rs' # PC <- v) m'.
-Proof.
- induction l.
- - intros. simpl. simpl in H. inv H. auto.
- - intros. simpl in *.
- destruct (exec_basic_instr ge a rs m) eqn:EXEBI; try discriminate.
- erewrite exec_basic_instr_pc_var; eauto.
-Qed.
-
-Lemma pc_set_add:
- forall rs v r x y,
- 0 <= x <= Ptrofs.max_unsigned ->
- 0 <= y <= Ptrofs.max_unsigned ->
- rs # r <- (Val.offset_ptr v (Ptrofs.repr (x + y))) = rs # r <- (Val.offset_ptr (rs # r <- (Val.offset_ptr v (Ptrofs.repr x)) r) (Ptrofs.repr y)).
-Proof.
- intros. apply functional_extensionality. intros r0. destruct (preg_eq r r0).
- - subst. repeat (rewrite Pregmap.gss); auto.
- destruct v; simpl; auto.
- rewrite Ptrofs.add_assoc.
- cutrewrite (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)); auto.
- unfold Ptrofs.add.
- cutrewrite (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)); auto.
- repeat (rewrite Ptrofs.unsigned_repr); auto.
- - repeat (rewrite Pregmap.gso; auto).
-Qed.
-
-Lemma concat2_straight:
- forall a b bb rs m rs'' m'' f ge,
- concat2 a b = OK bb ->
- exec_bblock ge f bb rs m = Next rs'' m'' ->
- exists rs' m',
- exec_bblock ge f a rs m = Next rs' m'
- /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
- /\ exec_bblock ge f b rs' m' = Next rs'' m''.
-Proof.
- intros until ge. intros CONC2 EXEB.
- exploit concat2_zlt_size; eauto. intros (LTA & LTB).
- exploit concat2_noexit; eauto. intros EXA.
- exploit concat2_decomp; eauto. intros. inv H.
- unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate.
- rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2).
- repeat eexists.
- unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.
- exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.
- unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto.
- rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
- assert (size bb = size a + size b).
- { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
- repeat (rewrite Nat2Z.inj_add). omega. }
- clear EXA H0 H1. rewrite H in EXEB.
- assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }
- rewrite H0. rewrite <- pc_set_add; auto.
- exploit AB.size_positive. instantiate (1 := a). intro. omega.
- exploit AB.size_positive. instantiate (1 := b). intro. omega.
-Qed.
-
-Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :
- forall a bb rs m lbb rs'' m'',
- lbb <> nil ->
- concat_all (a :: lbb) = OK bb ->
- exec_bblock ge f bb rs m = Next rs'' m'' ->
- exists bb' rs' m',
- concat_all lbb = OK bb'
- /\ exec_bblock ge f a rs m = Next rs' m'
- /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
- /\ exec_bblock ge f bb' rs' m' = Next rs'' m''.
-Proof.
- intros until m''. intros Hnonil CONC EXEB.
- simpl in CONC.
- destruct lbb as [|b lbb]; try contradiction. clear Hnonil.
- monadInv CONC. exploit concat2_straight; eauto. intros (rs' & m' & EXEB1 & PCeq & EXEB2).
- exists x. repeat econstructor. all: eauto.
-Qed.
-
-Lemma ptrofs_add_repr :
- forall a b,
- Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr a) (Ptrofs.repr b)) = Ptrofs.unsigned (Ptrofs.repr (a + b)).
-Proof.
- intros a b.
- rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq).
- rewrite <- Zplus_mod. auto.
-Qed.
-
-Section PRESERVATION.
-
-Variables prog tprog: program.
-Hypothesis TRANSL: match_prog prog tprog.
-Let ge := Genv.globalenv prog.
-Let tge := Genv.globalenv tprog.
-
-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.
-
-Lemma symbols_preserved:
- forall id,
- Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (Genv.find_symbol_match TRANSL).
-
-Lemma senv_preserved:
- Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSL).
-
-Lemma functions_translated:
- forall v f,
- Genv.find_funct ge v = Some f ->
- exists tf,
- Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial TRANSL).
-
-Lemma function_ptr_translated:
- forall v f,
- Genv.find_funct_ptr ge v = Some f ->
- exists tf,
- Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSL).
-
-Lemma functions_transl:
- forall fb f tf,
- Genv.find_funct_ptr ge fb = Some (Internal f) ->
- transf_function f = OK tf ->
- Genv.find_funct_ptr tge fb = Some (Internal tf).
-Proof.
- intros. exploit function_ptr_translated; eauto.
- intros (tf' & A & B). monadInv B. rewrite H0 in EQ. inv EQ. auto.
-Qed.
-
-Inductive match_states: state -> state -> Prop :=
- | match_states_intro:
- forall s1 s2, s1 = s2 -> match_states s1 s2.
-
-Lemma prog_main_preserved:
- prog_main tprog = prog_main prog.
-Proof (match_program_main TRANSL).
-
-Lemma prog_main_address_preserved:
- (Genv.symbol_address (Genv.globalenv prog) (prog_main prog) Ptrofs.zero) =
- (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero).
-Proof.
- unfold Genv.symbol_address. rewrite symbols_preserved.
- rewrite prog_main_preserved. auto.
-Qed.
-
-Lemma transf_initial_states:
- forall st1, initial_state prog st1 ->
- exists st2, initial_state tprog st2 /\ match_states st1 st2.
-Proof.
- intros. inv H.
- econstructor; split.
- - eapply initial_state_intro.
- eapply (Genv.init_mem_transf_partial TRANSL); eauto.
- - econstructor; eauto. subst ge0. subst rs0. rewrite prog_main_address_preserved. auto.
-Qed.
-
-Lemma transf_final_states:
- forall st1 st2 r,
- match_states st1 st2 -> final_state st1 r -> final_state st2 r.
-Proof.
- intros. inv H0. inv H. econstructor; eauto.
-Qed.
-
-Lemma tail_find_bblock:
- forall lbb pos bb,
- find_bblock pos lbb = Some bb ->
- exists c, code_tail pos lbb (bb::c).
-Proof.
- induction lbb.
- - intros. simpl in H. inv H.
- - intros. simpl in H.
- destruct (zlt pos 0); try (inv H; fail).
- destruct (zeq pos 0).
- + inv H. exists lbb. constructor; auto.
- + apply IHlbb in H. destruct H as (c & TAIL). exists c.
- cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto.
- omega.
-Qed.
-
-Lemma code_tail_head_app:
- forall l pos c1 c2,
- code_tail pos c1 c2 ->
- code_tail (pos + size_blocks l) (l++c1) c2.
-Proof.
- induction l.
- - intros. simpl. rewrite Z.add_0_r. auto.
- - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption.
-Qed.
-
-Lemma transf_blocks_verified:
- forall c tc pos bb c',
- transf_blocks c = OK tc ->
- code_tail pos c (bb::c') ->
- exists lbb,
- verified_schedule bb = OK lbb
- /\ exists tc', code_tail pos tc (lbb ++ tc').
-Proof.
- induction c; intros.
- - simpl in H. inv H. inv H0.
- - inv H0.
- + monadInv H. exists x0.
- split; simpl; auto. eexists; eauto. econstructor; eauto.
- + unfold transf_blocks in H. fold transf_blocks in H. monadInv H.
- exploit IHc; eauto.
- intros (lbb & TRANS & tc' & TAIL).
-(* monadInv TRANS. *)
- repeat eexists; eauto.
- erewrite verified_schedule_size; eauto.
- apply code_tail_head_app.
- eauto.
-Qed.
-
-Lemma transf_find_bblock:
- forall ofs f bb tf,
- find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->
- transf_function f = OK tf ->
- exists lbb,
- verified_schedule bb = OK lbb
- /\ exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c).
-Proof.
- intros.
- monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.
- monadInv EQ. apply tail_find_bblock in H. destruct H as (c & TAIL).
- eapply transf_blocks_verified; eauto.
-Qed.
-
-Lemma symbol_address_preserved:
- forall l ofs, Genv.symbol_address ge l ofs = Genv.symbol_address tge l ofs.
-Proof.
- intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity.
-Qed.
-
-Lemma head_tail {A: Type}:
- forall (l: list A) hd, hd::l = hd :: (tail (hd::l)).
-Proof.
- intros. simpl. auto.
-Qed.
-
-Lemma verified_schedule_not_empty:
- forall bb lbb,
- verified_schedule bb = OK lbb -> lbb <> nil.
-Proof.
- intros. apply verified_schedule_size in H.
- pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g.
- destruct lbb; simpl in *; discriminate.
-Qed.
-
-Lemma header_nil_label_pos_none:
- forall lbb l p,
- Forall (fun b => header b = nil) lbb -> label_pos l p lbb = None.
-Proof.
- induction lbb.
- - intros. simpl. auto.
- - intros. inv H. simpl. unfold is_label. rewrite H2. destruct (in_dec l nil). { inv i. }
- auto.
-Qed.
-
-Lemma verified_schedule_label:
- forall bb tbb lbb l,
- verified_schedule bb = OK (tbb :: lbb) ->
- is_label l bb = is_label l tbb
- /\ label_pos l 0 lbb = None.
-Proof.
- intros. exploit verified_schedule_header; eauto.
- intros (HdrEq & HdrNil).
- split.
- - unfold is_label. rewrite HdrEq. reflexivity.
- - apply header_nil_label_pos_none. assumption.
-Qed.
-
-Lemma label_pos_app_none:
- forall c c' l p p',
- label_pos l p c = None ->
- label_pos l (p' + size_blocks c) c' = label_pos l p' (c ++ c').
-Proof.
- induction c.
- - intros. simpl in *. rewrite Z.add_0_r. reflexivity.
- - intros. simpl in *. destruct (is_label _ _) eqn:ISLABEL.
- + discriminate.
- + eapply IHc in H. rewrite Z.add_assoc. eauto.
-Qed.
-
-Remark label_pos_pvar_none_add:
- forall tc l p p' k,
- label_pos l (p+k) tc = None -> label_pos l (p'+k) tc = None.
-Proof.
- induction tc.
- - intros. simpl. auto.
- - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
- + discriminate.
- + pose (IHtc l p p' (k + size a)). repeat (rewrite Z.add_assoc in e). auto.
-Qed.
-
-Lemma label_pos_pvar_none:
- forall tc l p p',
- label_pos l p tc = None -> label_pos l p' tc = None.
-Proof.
- intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
- eapply label_pos_pvar_none_add; eauto.
-Qed.
-
-Remark label_pos_pvar_some_add_add:
- forall tc l p p' k k',
- label_pos l (p+k') tc = Some (p+k) -> label_pos l (p'+k') tc = Some (p'+k).
-Proof.
- induction tc.
- - intros. simpl in H. discriminate.
- - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
- + inv H. assert (k = k') by omega. subst. reflexivity.
- + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
-Qed.
-
-Lemma label_pos_pvar_some_add:
- forall tc l p p' k,
- label_pos l p tc = Some (p+k) -> label_pos l p' tc = Some (p'+k).
-Proof.
- intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
- eapply label_pos_pvar_some_add_add; eauto.
-Qed.
-
-Remark label_pos_pvar_add:
- forall c tc l p p' k,
- label_pos l (p+k) c = label_pos l p tc ->
- label_pos l (p'+k) c = label_pos l p' tc.
-Proof.
- induction c.
- - intros. simpl in *.
- exploit label_pos_pvar_none; eauto.
- - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
- + exploit label_pos_pvar_some_add; eauto.
- + pose (IHc tc l p p' (k+size a)). repeat (rewrite Z.add_assoc in e). auto.
-Qed.
-
-Lemma label_pos_pvar:
- forall c tc l p p',
- label_pos l p c = label_pos l p tc ->
- label_pos l p' c = label_pos l p' tc.
-Proof.
- intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
- eapply label_pos_pvar_add; eauto.
-Qed.
-
-Lemma label_pos_head_app:
- forall c bb lbb l tc p,
- verified_schedule bb = OK lbb ->
- label_pos l p c = label_pos l p tc ->
- label_pos l p (bb :: c) = label_pos l p (lbb ++ tc).
-Proof.
- intros. simpl. destruct lbb as [|tbb lbb].
- - apply verified_schedule_not_empty in H. contradiction.
- - simpl. exploit verified_schedule_label; eauto. intros (ISLBL & LBLPOS).
- rewrite ISLBL.
- destruct (is_label l tbb) eqn:ISLBL'; simpl; auto.
- eapply label_pos_pvar in H0. erewrite H0.
- erewrite verified_schedule_size; eauto. simpl size_blocks. rewrite Z.add_assoc.
- erewrite label_pos_app_none; eauto.
-Qed.
-
-Lemma label_pos_preserved:
- forall c tc l,
- transf_blocks c = OK tc -> label_pos l 0 c = label_pos l 0 tc.
-Proof.
- induction c.
- - intros. simpl in *. inv H. reflexivity.
- - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ.
- eapply label_pos_head_app; eauto.
-Qed.
-
-Lemma label_pos_preserved_blocks:
- forall l f tf,
- transf_function f = OK tf ->
- label_pos l 0 (fn_blocks f) = label_pos l 0 (fn_blocks tf).
-Proof.
- intros. monadInv H. monadInv EQ.
- destruct (zlt Ptrofs.max_unsigned _); try discriminate.
- monadInv EQ0. simpl. eapply label_pos_preserved; eauto.
-Qed.
-
-Lemma transf_exec_control:
- forall f tf ex rs m,
- transf_function f = OK tf ->
- exec_control ge f ex rs m = exec_control tge tf ex rs m.
-Proof.
- intros. destruct ex; simpl; auto.
- assert (ge = Genv.globalenv prog). auto.
- assert (tge = Genv.globalenv tprog). auto.
- pose symbol_address_preserved.
- exploreInst; simpl; auto; try congruence.
- - unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
- - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
- - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
- - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
- - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-Qed.
-
-Lemma eval_offset_preserved:
- forall ofs, eval_offset ge ofs = eval_offset tge ofs.
-Proof.
- intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto.
-Qed.
-
-Lemma transf_exec_load:
- forall t rs m rd ra ofs, exec_load ge t rs m rd ra ofs = exec_load tge t rs m rd ra ofs.
-Proof.
- intros. unfold exec_load. rewrite eval_offset_preserved. reflexivity.
-Qed.
-
-Lemma transf_exec_store:
- forall t rs m rs0 ra ofs, exec_store ge t rs m rs0 ra ofs = exec_store tge t rs m rs0 ra ofs.
-Proof.
- intros. unfold exec_store. rewrite eval_offset_preserved. reflexivity.
-Qed.
-
-Lemma transf_exec_basic_instr:
- forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m.
-Proof.
- intros. pose symbol_address_preserved.
- unfold exec_basic_instr. exploreInst; simpl; auto; try congruence.
- 1: unfold exec_arith_instr; exploreInst; simpl; auto; try congruence.
- 1-10: apply transf_exec_load.
- all: apply transf_exec_store.
-Qed.
-
-Lemma transf_exec_body:
- forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m.
-Proof.
- induction bdy; intros.
- - simpl. reflexivity.
- - simpl. rewrite transf_exec_basic_instr.
- destruct (exec_basic_instr _ _ _); auto.
-Qed.
-
-Lemma transf_exec_bblock:
- forall f tf bb rs m,
- transf_function f = OK tf ->
- exec_bblock ge f bb rs m = exec_bblock tge tf bb rs m.
-Proof.
- intros. unfold exec_bblock. rewrite transf_exec_body. destruct (exec_body _ _ _ _); auto.
- eapply transf_exec_control; eauto.
-Qed.
-
-Lemma transf_step_simu:
- forall tf b lbb ofs c tbb rs m rs' m',
- Genv.find_funct_ptr tge b = Some (Internal tf) ->
- size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned ->
- rs PC = Vptr b ofs ->
- code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c) ->
- concat_all lbb = OK tbb ->
- exec_bblock tge tf tbb rs m = Next rs' m' ->
- plus step tge (State rs m) E0 (State rs' m').
-Proof.
- induction lbb.
- - intros until m'. simpl. intros. discriminate.
- - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB.
- destruct lbb.
- + simpl in *. clear IHlbb. inv CONC. eapply plus_one. econstructor; eauto. eapply find_bblock_tail; eauto.
- + exploit concat_all_exec_bblock; eauto; try discriminate.
- intros (tbb0 & rs0 & m0 & CONC0 & EXEB0 & PCeq' & EXEB1).
- eapply plus_left.
- econstructor.
- 3: eapply find_bblock_tail. rewrite <- app_comm_cons in TAIL. 3: eauto.
- all: eauto.
- eapply plus_star. eapply IHlbb; eauto. rewrite PCeq in PCeq'. simpl in PCeq'. all: eauto.
- eapply code_tail_next_int; eauto.
-Qed.
-
-Theorem transf_step_correct:
- forall s1 t s2, step ge s1 t s2 ->
- forall s1' (MS: match_states s1 s1'),
- (exists s2', plus step tge s1' t s2' /\ match_states s2 s2').
-Proof.
- induction 1; intros; inv MS.
- - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
- exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).
- exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ).
- assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned).
- eapply transf_function_no_overflow; eauto.
-
- erewrite transf_exec_bblock in H2; eauto.
- inv BBEQ. rewrite H3 in H2.
- exists (State rs' m'). split; try (constructor; auto).
- eapply transf_step_simu; eauto.
-
- - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
- exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).
- exploit verified_schedule_builtin_idem; eauto. intros. subst lbb.
-
- remember (State (nextblock _ _) _) as s'. exists s'.
- split; try constructor; auto.
- eapply plus_one. subst s'.
- eapply exec_step_builtin.
- 3: eapply find_bblock_tail. simpl in TAIL. 3: eauto.
- all: eauto.
- eapply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. eauto.
- eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-
- - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
- remember (State _ m') as s'. exists s'. split; try constructor; auto.
- subst s'. eapply plus_one. eapply exec_step_external; eauto.
- eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-Qed.
-
-Theorem transf_program_correct:
- forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog).
-Proof.
- eapply forward_simulation_plus.
- - apply senv_preserved.
- - apply transf_initial_states.
- - apply transf_final_states.
- - apply transf_step_correct.
-Qed.
-
-End PRESERVATION.
+Require Import Coqlib Errors. +Require Import Integers Floats AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Op Locations Machblock Conventions Asmblock. +Require Import Asmblockgenproof0. +Require Import PostpassScheduling. +Require Import Asmblockgenproof. +Require Import Axioms. + +Local Open Scope error_monad_scope. + +Definition match_prog (p tp: Asmblock.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. + +Remark builtin_body_nil: + forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil. +Proof. + intros. destruct bb as [hd bdy ex WF]. simpl in *. + apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1. + eapply H1; eauto. +Qed. + +Lemma verified_schedule_builtin_idem (ge: Genv.t fundef unit) (fn: function): + forall bb ef args res lbb, + exit bb = Some (PExpand (Pbuiltin ef args res)) -> + verified_schedule bb = OK lbb -> + lbb = bb :: nil. +Proof. + intros. exploit builtin_body_nil; eauto. intros. + rewrite verified_schedule_single_inst in H0; auto. + - inv H0. auto. + - unfold size. rewrite H. rewrite H1. simpl. auto. +Qed. + +Lemma exec_body_app: + forall l l' ge rs m rs'' m'', + exec_body ge (l ++ l') rs m = Next rs'' m'' -> + exists rs' m', + exec_body ge l rs m = Next rs' m' + /\ exec_body ge l' rs' m' = Next rs'' m''. +Proof. + induction l. + - intros. simpl in H. repeat eexists. auto. + - intros. rewrite <- app_comm_cons in H. simpl in H. + destruct (exec_basic_instr ge a rs m) eqn:EXEBI. + + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2). + repeat eexists. simpl. rewrite EXEBI. eauto. auto. + + discriminate. +Qed. + +Lemma exec_body_pc: + forall l ge rs1 m1 rs2 m2, + exec_body ge l rs1 m1 = Next rs2 m2 -> + rs2 PC = rs1 PC. +Proof. + induction l. + - intros. inv H. auto. + - intros until m2. intro EXEB. + inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate. + eapply IHl in H0. rewrite H0. + erewrite exec_basic_instr_pc; eauto. +Qed. + +Lemma next_eq {A: Type}: + forall (rs rs':A) m m', + rs = rs' -> m = m' -> Next rs m = Next rs' m'. +Proof. + intros. congruence. +Qed. + +Lemma regset_double_set: + forall r1 r2 (rs: regset) v1 v2, + r1 <> r2 -> + (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1). +Proof. + intros. apply functional_extensionality. intros r. destruct (preg_eq r r1). + - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto. + - destruct (preg_eq r r2). + + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto. + + repeat (rewrite Pregmap.gso; auto). +Qed. + +Lemma regset_double_set_id: + forall r (rs: regset) v1 v2, + (rs # r <- v1 # r <- v2) = (rs # r <- v2). +Proof. + intros. apply functional_extensionality. intros. destruct (preg_eq r x). + - subst r. repeat (rewrite Pregmap.gss; auto). + - repeat (rewrite Pregmap.gso); auto. +Qed. + +Lemma exec_load_pc_var: + forall ge t rs m rd ra ofs rs' m' v, + exec_load ge t rs m rd ra ofs = Next rs' m' -> + exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. + destruct (Mem.loadv _ _ _). + - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. + - discriminate. +Qed. + +Lemma exec_store_pc_var: + forall ge t rs m rd ra ofs rs' m' v, + exec_store ge t rs m rd ra ofs = Next rs' m' -> + exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. + destruct (Mem.storev _ _ _). + - inv H. apply next_eq; auto. + - discriminate. +Qed. + +Lemma exec_basic_instr_pc_var: + forall ge i rs m rs' m' v, + exec_basic_instr ge i rs m = Next rs' m' -> + exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'. +Proof. + intros. unfold exec_basic_instr in *. destruct i. + - unfold exec_arith_instr in *. destruct i; destruct i. + all: try (exploreInst; inv H; apply next_eq; auto; + apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). + + (* Some cases treated seperately because exploreInst destructs too much *) + all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). + - exploreInst; apply exec_load_pc_var; auto. + - exploreInst; apply exec_store_pc_var; auto. + - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate). + destruct (Mem.storev _ _ _ _); try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. + rewrite (regset_double_set GPR32 PC); try discriminate. + rewrite (regset_double_set GPR12 PC); try discriminate. + rewrite (regset_double_set GPR14 PC); try discriminate. reflexivity. + - repeat (rewrite Pregmap.gso; try discriminate). + destruct (Mem.loadv _ _ _); try discriminate. + destruct (rs GPR12); try discriminate. + destruct (Mem.free _ _ _ _); try discriminate. + inv H. apply next_eq; auto. + rewrite (regset_double_set GPR32 PC). + rewrite (regset_double_set GPR12 PC). reflexivity. + all: discriminate. + - destruct rs0; try discriminate. inv H. apply next_eq; auto. + repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate. + - destruct rd; try discriminate. inv H. apply next_eq; auto. + repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate. + - inv H. apply next_eq; auto. +Qed. + +Lemma exec_body_pc_var: + forall l ge rs m rs' m' v, + exec_body ge l rs m = Next rs' m' -> + exec_body ge l (rs # PC <- v) m = Next (rs' # PC <- v) m'. +Proof. + induction l. + - intros. simpl. simpl in H. inv H. auto. + - intros. simpl in *. + destruct (exec_basic_instr ge a rs m) eqn:EXEBI; try discriminate. + erewrite exec_basic_instr_pc_var; eauto. +Qed. + +Lemma pc_set_add: + forall rs v r x y, + 0 <= x <= Ptrofs.max_unsigned -> + 0 <= y <= Ptrofs.max_unsigned -> + rs # r <- (Val.offset_ptr v (Ptrofs.repr (x + y))) = rs # r <- (Val.offset_ptr (rs # r <- (Val.offset_ptr v (Ptrofs.repr x)) r) (Ptrofs.repr y)). +Proof. + intros. apply functional_extensionality. intros r0. destruct (preg_eq r r0). + - subst. repeat (rewrite Pregmap.gss); auto. + destruct v; simpl; auto. + rewrite Ptrofs.add_assoc. + cutrewrite (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)); auto. + unfold Ptrofs.add. + cutrewrite (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)); auto. + repeat (rewrite Ptrofs.unsigned_repr); auto. + - repeat (rewrite Pregmap.gso; auto). +Qed. + +Lemma concat2_straight: + forall a b bb rs m rs'' m'' f ge, + concat2 a b = OK bb -> + exec_bblock ge f bb rs m = Next rs'' m'' -> + exists rs' m', + exec_bblock ge f a rs m = Next rs' m' + /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a)) + /\ exec_bblock ge f b rs' m' = Next rs'' m''. +Proof. + intros until ge. intros CONC2 EXEB. + exploit concat2_zlt_size; eauto. intros (LTA & LTB). + exploit concat2_noexit; eauto. intros EXA. + exploit concat2_decomp; eauto. intros. inv H. + unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate. + rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2). + repeat eexists. + unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto. + exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto. + unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto. + rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id. + assert (size bb = size a + size b). + { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r. + repeat (rewrite Nat2Z.inj_add). omega. } + clear EXA H0 H1. rewrite H in EXEB. + assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. } + rewrite H0. rewrite <- pc_set_add; auto. + exploit AB.size_positive. instantiate (1 := a). intro. omega. + exploit AB.size_positive. instantiate (1 := b). intro. omega. +Qed. + +Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) : + forall a bb rs m lbb rs'' m'', + lbb <> nil -> + concat_all (a :: lbb) = OK bb -> + exec_bblock ge f bb rs m = Next rs'' m'' -> + exists bb' rs' m', + concat_all lbb = OK bb' + /\ exec_bblock ge f a rs m = Next rs' m' + /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a)) + /\ exec_bblock ge f bb' rs' m' = Next rs'' m''. +Proof. + intros until m''. intros Hnonil CONC EXEB. + simpl in CONC. + destruct lbb as [|b lbb]; try contradiction. clear Hnonil. + monadInv CONC. exploit concat2_straight; eauto. intros (rs' & m' & EXEB1 & PCeq & EXEB2). + exists x. repeat econstructor. all: eauto. +Qed. + +Lemma ptrofs_add_repr : + forall a b, + Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr a) (Ptrofs.repr b)) = Ptrofs.unsigned (Ptrofs.repr (a + b)). +Proof. + intros a b. + rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq). + rewrite <- Zplus_mod. auto. +Qed. + +Section PRESERVATION. + +Variables prog tprog: program. +Hypothesis TRANSL: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +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. + +Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. +Proof (Genv.find_symbol_match TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSL). + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_transf_partial TRANSL). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + exists tf, + Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial TRANSL). + +Lemma functions_transl: + forall fb f tf, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transf_function f = OK tf -> + Genv.find_funct_ptr tge fb = Some (Internal tf). +Proof. + intros. exploit function_ptr_translated; eauto. + intros (tf' & A & B). monadInv B. rewrite H0 in EQ. inv EQ. auto. +Qed. + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall s1 s2, s1 = s2 -> match_states s1 s2. + +Lemma prog_main_preserved: + prog_main tprog = prog_main prog. +Proof (match_program_main TRANSL). + +Lemma prog_main_address_preserved: + (Genv.symbol_address (Genv.globalenv prog) (prog_main prog) Ptrofs.zero) = + (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero). +Proof. + unfold Genv.symbol_address. rewrite symbols_preserved. + rewrite prog_main_preserved. auto. +Qed. + +Lemma transf_initial_states: + forall st1, initial_state prog st1 -> + exists st2, initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inv H. + econstructor; split. + - eapply initial_state_intro. + eapply (Genv.init_mem_transf_partial TRANSL); eauto. + - econstructor; eauto. subst ge0. subst rs0. rewrite prog_main_address_preserved. auto. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> final_state st1 r -> final_state st2 r. +Proof. + intros. inv H0. inv H. econstructor; eauto. +Qed. + +Lemma tail_find_bblock: + forall lbb pos bb, + find_bblock pos lbb = Some bb -> + exists c, code_tail pos lbb (bb::c). +Proof. + induction lbb. + - intros. simpl in H. inv H. + - intros. simpl in H. + destruct (zlt pos 0); try (inv H; fail). + destruct (zeq pos 0). + + inv H. exists lbb. constructor; auto. + + apply IHlbb in H. destruct H as (c & TAIL). exists c. + cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto. + omega. +Qed. + +Lemma code_tail_head_app: + forall l pos c1 c2, + code_tail pos c1 c2 -> + code_tail (pos + size_blocks l) (l++c1) c2. +Proof. + induction l. + - intros. simpl. rewrite Z.add_0_r. auto. + - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption. +Qed. + +Lemma transf_blocks_verified: + forall c tc pos bb c', + transf_blocks c = OK tc -> + code_tail pos c (bb::c') -> + exists lbb, + verified_schedule bb = OK lbb + /\ exists tc', code_tail pos tc (lbb ++ tc'). +Proof. + induction c; intros. + - simpl in H. inv H. inv H0. + - inv H0. + + monadInv H. exists x0. + split; simpl; auto. eexists; eauto. econstructor; eauto. + + unfold transf_blocks in H. fold transf_blocks in H. monadInv H. + exploit IHc; eauto. + intros (lbb & TRANS & tc' & TAIL). +(* monadInv TRANS. *) + repeat eexists; eauto. + erewrite verified_schedule_size; eauto. + apply code_tail_head_app. + eauto. +Qed. + +Lemma transf_find_bblock: + forall ofs f bb tf, + find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb -> + transf_function f = OK tf -> + exists lbb, + verified_schedule bb = OK lbb + /\ exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c). +Proof. + intros. + monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0. + monadInv EQ. apply tail_find_bblock in H. destruct H as (c & TAIL). + eapply transf_blocks_verified; eauto. +Qed. + +Lemma symbol_address_preserved: + forall l ofs, Genv.symbol_address ge l ofs = Genv.symbol_address tge l ofs. +Proof. + intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity. +Qed. + +Lemma head_tail {A: Type}: + forall (l: list A) hd, hd::l = hd :: (tail (hd::l)). +Proof. + intros. simpl. auto. +Qed. + +Lemma verified_schedule_not_empty: + forall bb lbb, + verified_schedule bb = OK lbb -> lbb <> nil. +Proof. + intros. apply verified_schedule_size in H. + pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g. + destruct lbb; simpl in *; discriminate. +Qed. + +Lemma header_nil_label_pos_none: + forall lbb l p, + Forall (fun b => header b = nil) lbb -> label_pos l p lbb = None. +Proof. + induction lbb. + - intros. simpl. auto. + - intros. inv H. simpl. unfold is_label. rewrite H2. destruct (in_dec l nil). { inv i. } + auto. +Qed. + +Lemma verified_schedule_label: + forall bb tbb lbb l, + verified_schedule bb = OK (tbb :: lbb) -> + is_label l bb = is_label l tbb + /\ label_pos l 0 lbb = None. +Proof. + intros. exploit verified_schedule_header; eauto. + intros (HdrEq & HdrNil). + split. + - unfold is_label. rewrite HdrEq. reflexivity. + - apply header_nil_label_pos_none. assumption. +Qed. + +Lemma label_pos_app_none: + forall c c' l p p', + label_pos l p c = None -> + label_pos l (p' + size_blocks c) c' = label_pos l p' (c ++ c'). +Proof. + induction c. + - intros. simpl in *. rewrite Z.add_0_r. reflexivity. + - intros. simpl in *. destruct (is_label _ _) eqn:ISLABEL. + + discriminate. + + eapply IHc in H. rewrite Z.add_assoc. eauto. +Qed. + +Remark label_pos_pvar_none_add: + forall tc l p p' k, + label_pos l (p+k) tc = None -> label_pos l (p'+k) tc = None. +Proof. + induction tc. + - intros. simpl. auto. + - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL. + + discriminate. + + pose (IHtc l p p' (k + size a)). repeat (rewrite Z.add_assoc in e). auto. +Qed. + +Lemma label_pos_pvar_none: + forall tc l p p', + label_pos l p tc = None -> label_pos l p' tc = None. +Proof. + intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1. + eapply label_pos_pvar_none_add; eauto. +Qed. + +Remark label_pos_pvar_some_add_add: + forall tc l p p' k k', + label_pos l (p+k') tc = Some (p+k) -> label_pos l (p'+k') tc = Some (p'+k). +Proof. + induction tc. + - intros. simpl in H. discriminate. + - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL. + + inv H. assert (k = k') by omega. subst. reflexivity. + + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto. +Qed. + +Lemma label_pos_pvar_some_add: + forall tc l p p' k, + label_pos l p tc = Some (p+k) -> label_pos l p' tc = Some (p'+k). +Proof. + intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1. + eapply label_pos_pvar_some_add_add; eauto. +Qed. + +Remark label_pos_pvar_add: + forall c tc l p p' k, + label_pos l (p+k) c = label_pos l p tc -> + label_pos l (p'+k) c = label_pos l p' tc. +Proof. + induction c. + - intros. simpl in *. + exploit label_pos_pvar_none; eauto. + - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL. + + exploit label_pos_pvar_some_add; eauto. + + pose (IHc tc l p p' (k+size a)). repeat (rewrite Z.add_assoc in e). auto. +Qed. + +Lemma label_pos_pvar: + forall c tc l p p', + label_pos l p c = label_pos l p tc -> + label_pos l p' c = label_pos l p' tc. +Proof. + intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1. + eapply label_pos_pvar_add; eauto. +Qed. + +Lemma label_pos_head_app: + forall c bb lbb l tc p, + verified_schedule bb = OK lbb -> + label_pos l p c = label_pos l p tc -> + label_pos l p (bb :: c) = label_pos l p (lbb ++ tc). +Proof. + intros. simpl. destruct lbb as [|tbb lbb]. + - apply verified_schedule_not_empty in H. contradiction. + - simpl. exploit verified_schedule_label; eauto. intros (ISLBL & LBLPOS). + rewrite ISLBL. + destruct (is_label l tbb) eqn:ISLBL'; simpl; auto. + eapply label_pos_pvar in H0. erewrite H0. + erewrite verified_schedule_size; eauto. simpl size_blocks. rewrite Z.add_assoc. + erewrite label_pos_app_none; eauto. +Qed. + +Lemma label_pos_preserved: + forall c tc l, + transf_blocks c = OK tc -> label_pos l 0 c = label_pos l 0 tc. +Proof. + induction c. + - intros. simpl in *. inv H. reflexivity. + - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ. + eapply label_pos_head_app; eauto. +Qed. + +Lemma label_pos_preserved_blocks: + forall l f tf, + transf_function f = OK tf -> + label_pos l 0 (fn_blocks f) = label_pos l 0 (fn_blocks tf). +Proof. + intros. monadInv H. monadInv EQ. + destruct (zlt Ptrofs.max_unsigned _); try discriminate. + monadInv EQ0. simpl. eapply label_pos_preserved; eauto. +Qed. + +Lemma transf_exec_control: + forall f tf ex rs m, + transf_function f = OK tf -> + exec_control ge f ex rs m = exec_control tge tf ex rs m. +Proof. + intros. destruct ex; simpl; auto. + assert (ge = Genv.globalenv prog). auto. + assert (tge = Genv.globalenv tprog). auto. + pose symbol_address_preserved. + exploreInst; simpl; auto; try congruence. + - unfold goto_label. erewrite label_pos_preserved_blocks; eauto. + - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. + - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. + - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. + - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto. +Qed. + +Lemma eval_offset_preserved: + forall ofs, eval_offset ge ofs = eval_offset tge ofs. +Proof. + intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto. +Qed. + +Lemma transf_exec_load: + forall t rs m rd ra ofs, exec_load ge t rs m rd ra ofs = exec_load tge t rs m rd ra ofs. +Proof. + intros. unfold exec_load. rewrite eval_offset_preserved. reflexivity. +Qed. + +Lemma transf_exec_store: + forall t rs m rs0 ra ofs, exec_store ge t rs m rs0 ra ofs = exec_store tge t rs m rs0 ra ofs. +Proof. + intros. unfold exec_store. rewrite eval_offset_preserved. reflexivity. +Qed. + +Lemma transf_exec_basic_instr: + forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m. +Proof. + intros. pose symbol_address_preserved. + unfold exec_basic_instr. exploreInst; simpl; auto; try congruence. + 1: unfold exec_arith_instr; exploreInst; simpl; auto; try congruence. + 1-10: apply transf_exec_load. + all: apply transf_exec_store. +Qed. + +Lemma transf_exec_body: + forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m. +Proof. + induction bdy; intros. + - simpl. reflexivity. + - simpl. rewrite transf_exec_basic_instr. + destruct (exec_basic_instr _ _ _); auto. +Qed. + +Lemma transf_exec_bblock: + forall f tf bb rs m, + transf_function f = OK tf -> + exec_bblock ge f bb rs m = exec_bblock tge tf bb rs m. +Proof. + intros. unfold exec_bblock. rewrite transf_exec_body. destruct (exec_body _ _ _ _); auto. + eapply transf_exec_control; eauto. +Qed. + +Lemma transf_step_simu: + forall tf b lbb ofs c tbb rs m rs' m', + Genv.find_funct_ptr tge b = Some (Internal tf) -> + size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned -> + rs PC = Vptr b ofs -> + code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (lbb ++ c) -> + concat_all lbb = OK tbb -> + exec_bblock tge tf tbb rs m = Next rs' m' -> + plus step tge (State rs m) E0 (State rs' m'). +Proof. + induction lbb. + - intros until m'. simpl. intros. discriminate. + - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB. + destruct lbb. + + simpl in *. clear IHlbb. inv CONC. eapply plus_one. econstructor; eauto. eapply find_bblock_tail; eauto. + + exploit concat_all_exec_bblock; eauto; try discriminate. + intros (tbb0 & rs0 & m0 & CONC0 & EXEB0 & PCeq' & EXEB1). + eapply plus_left. + econstructor. + 3: eapply find_bblock_tail. rewrite <- app_comm_cons in TAIL. 3: eauto. + all: eauto. + eapply plus_star. eapply IHlbb; eauto. rewrite PCeq in PCeq'. simpl in PCeq'. all: eauto. + eapply code_tail_next_int; eauto. +Qed. + +Theorem transf_step_correct: + forall s1 t s2, step ge s1 t s2 -> + forall s1' (MS: match_states s1 s1'), + (exists s2', plus step tge s1' t s2' /\ match_states s2 s2'). +Proof. + induction 1; intros; inv MS. + - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. + exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL). + exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). + assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + + erewrite transf_exec_bblock in H2; eauto. + inv BBEQ. rewrite H3 in H2. + exists (State rs' m'). split; try (constructor; auto). + eapply transf_step_simu; eauto. + + - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. + exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL). + exploit verified_schedule_builtin_idem; eauto. intros. subst lbb. + + remember (State (nextblock _ _) _) as s'. exists s'. + split; try constructor; auto. + eapply plus_one. subst s'. + eapply exec_step_builtin. + 3: eapply find_bblock_tail. simpl in TAIL. 3: eauto. + all: eauto. + eapply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. + remember (State _ m') as s'. exists s'. split; try constructor; auto. + subst s'. eapply plus_one. eapply exec_step_external; eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. +Qed. + +Theorem transf_program_correct: + forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog). +Proof. + eapply forward_simulation_plus. + - apply senv_preserved. + - apply transf_initial_states. + - apply transf_final_states. + - apply transf_step_correct. +Qed. + +End PRESERVATION. diff --git a/mppa_k1c/SelectLong.v b/mppa_k1c/SelectLong.v index f2aa6be2..ea42b9c3 100644 --- a/mppa_k1c/SelectLong.v +++ b/mppa_k1c/SelectLong.v @@ -755,20 +755,29 @@ Definition floatoflongu (e: expr) := if Archi.splitlong then SplitLong.floatoflongu e else Eop Ofloatoflongu (e:::Enil). -Definition longofsingle (e: expr) := +(* FIXME - normally we can have it natively, but in practice it requires proving that we can do Fwidenlwd + fixedd.rz.. To do later *) +Definition longofsingle (e: expr) := SplitLong.longofsingle e. +(* if Archi.splitlong then SplitLong.longofsingle e else Eop Olongofsingle (e:::Enil). +*) -Definition longuofsingle (e: expr) := +Definition longuofsingle (e: expr) := SplitLong.longuofsingle e. +(* if Archi.splitlong then SplitLong.longuofsingle e else Eop Olonguofsingle (e:::Enil). +*) -Definition singleoflong (e: expr) := +Definition singleoflong (e: expr) := SplitLong.singleoflong e. +(* if Archi.splitlong then SplitLong.singleoflong e else Eop Osingleoflong (e:::Enil). +*) -Definition singleoflongu (e: expr) := +Definition singleoflongu (e: expr) := SplitLong.singleoflongu e. +(* if Archi.splitlong then SplitLong.singleoflongu e else Eop Osingleoflongu (e:::Enil). +*) End SELECT. diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 26735c99..a3aefb15 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -341,20 +341,29 @@ Definition floatoflongu (e: expr) := if Archi.splitlong then SplitLong.floatoflongu e else Eop Ofloatoflongu (e:::Enil). -Definition longofsingle (e: expr) := +(* FIXME - normally we can have it natively, but in practice it requires proving that we can do Fwidenlwd + fixedd.rz.. To do later *) +Definition longofsingle (e: expr) := SplitLong.longofsingle e. +(* if Archi.splitlong then SplitLong.longofsingle e else Eop Olongofsingle (e:::Enil). +*) -Definition longuofsingle (e: expr) := +Definition longuofsingle (e: expr) := SplitLong.longuofsingle e. +(* if Archi.splitlong then SplitLong.longuofsingle e else Eop Olonguofsingle (e:::Enil). +*) -Definition singleoflong (e: expr) := +Definition singleoflong (e: expr) := SplitLong.singleoflong e. +(* if Archi.splitlong then SplitLong.singleoflong e else Eop Osingleoflong (e:::Enil). +*) -Definition singleoflongu (e: expr) := +Definition singleoflongu (e: expr) := SplitLong.singleoflongu e. +(* if Archi.splitlong then SplitLong.singleoflongu e else Eop Osingleoflongu (e:::Enil). +*) End SELECT. diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index d12fb9ae..44846a6f 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -582,30 +582,30 @@ Qed. Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle. Proof. - unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL. + unfold longofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *) eapply SplitLongproof.eval_longofsingle; eauto. - TrivialExists. +(* TrivialExists. *) Qed. Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle. Proof. - unfold longuofsingle; red; intros. destruct Archi.splitlong eqn:SL. + unfold longuofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *) eapply SplitLongproof.eval_longuofsingle; eauto. - TrivialExists. +(* TrivialExists. *) Qed. Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong. Proof. - unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL. + unfold singleoflong; red; intros. (* destruct Archi.splitlong eqn:SL. *) eapply SplitLongproof.eval_singleoflong; eauto. - TrivialExists. +(* TrivialExists. *) Qed. Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu. Proof. - unfold singleoflongu; red; intros. destruct Archi.splitlong eqn:SL. + unfold singleoflongu; red; intros. (* destruct Archi.splitlong eqn:SL. *) eapply SplitLongproof.eval_singleoflongu; eauto. - TrivialExists. +(* TrivialExists. *) Qed. End CMCONSTR. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index bbb608de..5d59e7d2 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -173,6 +173,18 @@ module Target (*: TARGET*) = | ITnone -> "none" let icond oc c = fprintf oc "%s" (icond_name c) + + let fcond_name = let open Asmblock in function + | FTone -> "one" + | FTueq -> "ueq" + | FToeq -> "oeq" + | FTune -> "une" + | FTolt -> "olt" + | FTuge -> "uge" + | FToge -> "oge" + | FTult -> "ult" + + let fcond oc c = fprintf oc "%s" (fcond_name c) let bcond_name = let open Asmblock in function | BTwnez -> "wnez" @@ -295,23 +307,29 @@ module Target (*: TARGET*) = | Pfabsw(rd, rs) -> fprintf oc " fabsw %a = %a\n" ireg rd ireg rs | Pfnegd(rd, rs) -> - fprintf oc " fnegd %a = %a\n" ireg rs ireg rd + fprintf oc " fnegd %a = %a\n" ireg rd ireg rs | Pfnegw(rd, rs) -> - fprintf oc " fnegw %a = %a\n" ireg rs ireg rd + fprintf oc " fnegw %a = %a\n" ireg rd ireg rs | Pfnarrowdw(rd, rs) -> - fprintf oc " fnarrowdw %a = %a\n" ireg rs ireg rd + fprintf oc " fnarrowdw %a = %a\n" ireg rd ireg rs | Pfwidenlwd(rd, rs) -> - fprintf oc " fwidenlwd %a = %a\n" ireg rs ireg rd + fprintf oc " fwidenlwd %a = %a\n" ireg rd ireg rs + | Pfloatuwrnsz(rd, rs) -> + fprintf oc " floatuw.rn.s %a = %a, 0\n" ireg rd ireg rs | Pfloatwrnsz(rd, rs) -> fprintf oc " floatw.rn.s %a = %a, 0\n" ireg rd ireg rs - | Pfloatudrnsz(rd, rs) -> + | Pfloatudrnsz(rd, rs) | Pfloatudrnsz_i32(rd, rs) -> fprintf oc " floatud.rn.s %a = %a, 0\n" ireg rd ireg rs - | Pfloatdrnsz(rd, rs) -> + | Pfloatdrnsz(rd, rs) | Pfloatdrnsz_i32(rd, rs) -> fprintf oc " floatd.rn.s %a = %a, 0\n" ireg rd ireg rs | Pfixedwrzz(rd, rs) -> fprintf oc " fixedw.rz %a = %a, 0\n" ireg rd ireg rs - | Pfixeddrzz(rd, rs) -> + | Pfixeduwrzz(rd, rs) -> + fprintf oc " fixeduw.rz %a = %a, 0\n" ireg rd ireg rs + | Pfixeddrzz(rd, rs) | Pfixeddrzz_i32(rd, rs) -> fprintf oc " fixedd.rz %a = %a, 0\n" ireg rd ireg rs + | Pfixedudrzz(rd, rs) | Pfixedudrzz_i32(rd, rs) -> + fprintf oc " fixedud.rz %a = %a, 0\n" ireg rd ireg rs (* Arith RI32 instructions *) | Pmake (rd, imm) -> @@ -339,6 +357,11 @@ module Target (*: TARGET*) = | Pcompl (it, rd, rs1, rs2) -> fprintf oc " compd.%a %a = %a, %a\n" icond it ireg rd ireg rs1 ireg rs2 + | Pfcompw (ft, rd, rs1, rs2) -> + fprintf oc " fcompw.%a %a = %a, %a\n" fcond ft ireg rd ireg rs1 ireg rs2 + | Pfcompl (ft, rd, rs1, rs2) -> + fprintf oc " fcompd.%a %a = %a, %a\n" fcond ft ireg rd ireg rs1 ireg rs2 + | Paddw (rd, rs1, rs2) -> fprintf oc " addw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Psubw (rd, rs1, rs2) -> @@ -382,9 +405,9 @@ module Target (*: TARGET*) = | Pfaddw (rd, rs1, rs2) -> fprintf oc " faddw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pfsbfd (rd, rs1, rs2) -> - fprintf oc " fsbfd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + fprintf oc " fsbfd %a = %a, %a\n" ireg rd ireg rs2 ireg rs1 | Pfsbfw (rd, rs1, rs2) -> - fprintf oc " fsbfw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + fprintf oc " fsbfw %a = %a, %a\n" ireg rd ireg rs2 ireg rs1 | Pfmuld (rd, rs1, rs2) -> fprintf oc " fmuld %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pfmulw (rd, rs1, rs2) -> diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 8c299f88..69234938 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -20,6 +20,12 @@ Module AB:=Asmblock. Hint Extern 2 (_ <> _) => congruence: asmgen. +Inductive bblock_equiv (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) := + | bblock_equiv_intro: + (forall rs m, + exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m) -> + bblock_equiv ge f bb bb'. + Lemma ireg_of_eq: forall r r', ireg_of r = OK r' -> preg_of r = IR r'. Proof. @@ -1096,4 +1102,4 @@ Proof. intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. Qed. -End MATCH_STACK.
\ No newline at end of file +End MATCH_STACK. diff --git a/runtime/Makefile b/runtime/Makefile index 66ec6fec..f58d4b6a 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -23,7 +23,9 @@ OBJS=i64_dtou.o i64_utod.o i64_utof.o vararg.o else ifeq ($(ARCH),powerpc64) OBJS=i64_dtou.o i64_stof.o i64_utod.o i64_utof.o vararg.o else ifeq ($(ARCH),mppa_k1c) -OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o vararg.o +OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o vararg.o\ + i64_dtos.o i64_dtou.o i64_utod.o i64_utof.o i64_stod.o i64_stof.o +# Missing: i64_utod.o i64_utof.o i64_stod.o i64_stof.o DOMAKE:=$(shell (cd mppa_k1c && make)) else OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \ @@ -66,7 +68,7 @@ $(LIB): $(OBJS) ../ccomp -O2 -S -o $*.s -I./c c/$*.c sed -i -e 's/i64_/__compcert_i64_/g' $*.s $(CASMRUNTIME) -o $*.o $*.s - @rm -f $*.s + @rm $*.s clean:: rm -f *.o $(LIB) *.tmp?.s diff --git a/test/mppa/instr/Makefile b/test/mppa/instr/Makefile index b4abb6a4..ea86114c 100644 --- a/test/mppa/instr/Makefile +++ b/test/mppa/instr/Makefile @@ -5,6 +5,7 @@ OPTIM ?= -O2 CFLAGS ?= $(OPTIM) SIMU ?= k1-mppa TIMEOUT ?= --signal=SIGTERM 120s +DIFF ?= python2.7 floatcmp.py -reltol .00001 DIR=./ SRCDIR=$(DIR) @@ -50,7 +51,7 @@ test: $(X86_GCC_OUT) $(GCC_OUT) @for test in $(TESTNAMES); do\ x86out=$(OUTDIR)/$$test.x86-gcc.out;\ gccout=$(OUTDIR)/$$test.gcc.out;\ - if diff -q $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ + if $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ >&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\ else\ printf "$(GREEN)GOOD: $$x86out and $$gccout concur$(NC)\n";\ @@ -63,7 +64,7 @@ check: $(GCC_OUT) $(CCOMP_OUT) @for test in $(TESTNAMES); do\ gccout=$(OUTDIR)/$$test.gcc.out;\ ccompout=$(OUTDIR)/$$test.ccomp.out;\ - if diff -q $$ccompout $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ + if $(DIFF) $$ccompout $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ >&2 printf "$(RED)ERROR: $$ccompout and $$gccout differ$(NC)\n";\ else\ printf "$(GREEN)GOOD: $$ccompout and $$gccout concur$(NC)\n";\ diff --git a/test/mppa/instr/faddw.c b/test/mppa/instr/faddw.c index a00e9afe..e0e635ae 100644 --- a/test/mppa/instr/faddw.c +++ b/test/mppa/instr/faddw.c @@ -1,5 +1,5 @@ #include "framework.h" -BEGIN_TEST(double) +BEGIN_TEST(float) c = ((float)a + (float)b); -END_TESTF64() +END_TESTF32() diff --git a/test/mppa/instr/floatcmp.py b/test/mppa/instr/floatcmp.py new file mode 100755 index 00000000..49f1bc13 --- /dev/null +++ b/test/mppa/instr/floatcmp.py @@ -0,0 +1,93 @@ +#!/usr/bin/python2.7 + +import argparse as ap +import sys + +parser = ap.ArgumentParser() +parser.add_argument("file1", help="First file to compare") +parser.add_argument("file2", help="Second file to compare") +parser.add_argument("-reltol", help="Relative error") +parser.add_argument("-abstol", help="Absolute error") +parser.add_argument("-s", help="Silent output", action="store_true") +args = parser.parse_args() + +reltol = float(args.reltol) if args.reltol else None +abstol = float(args.abstol) if args.abstol else None +silent = args.s + +if silent: + sys.stdout = open("/dev/null", "w") + +import re +from math import fabs + +def floatcmp(f1, f2): + if abstol: + if fabs(f1 - f2) > abstol: + return False + if reltol: + if f2 != 0. and fabs((f1 - f2) / f2) > reltol: + return False + return True + +class Parsed(list): + def __eq__(self, other): + if len(self) != len(other): + return False + comps = zip(self, other) + for comp in comps: + if all(isinstance(compElt, str) for compElt in comp): + if comp[0] != comp[1]: + return False + elif all (isinstance(compElt, float) for compElt in comp): + if not floatcmp(comp[0], comp[1]): + return False + else: + return False + return True + + def __ne__(self, other): + return not self.__eq__(other) + +parseLine = re.compile(r"\s*(\S+)") +def readline(line): + words = parseLine.findall(line) + parsed = Parsed([]) + for word in words: + try: + parse = float(word) + parsed.append(parse) + except ValueError: + parsed.append(word) + return parsed + +def readfile(filename): + L = [] + try: + with open(filename) as f: + for line in f: + L.append(readline(line)) + except IOError: + print "Unable to read {}".format(filename) + sys.exit(2) + return L + +L1 = readfile(args.file1) +L2 = readfile(args.file2) + +if len(L1) != len(L2): + print "The files have different amount of lines" + print "\t{}: {} lines".format(args.file1, len(L1)) + print "\t{}: {} lines".format(args.file2, len(L2)) + sys.exit(1) + +cmpL = zip(L1, L2) +for i, cmpElt in enumerate(cmpL): + if cmpElt[0] != cmpElt[1]: + print "The files differ at line {}".format(i) + print "\t{}: {}".format(args.file1, cmpElt[0]) + print "\t{}: {}".format(args.file2, cmpElt[1]) + sys.exit(1) + +print "Comparison succeeded" +sys.exit(0) diff --git a/test/mppa/instr/fmulw.c b/test/mppa/instr/fmulw.c index 030a6d9c..f85eba64 100644 --- a/test/mppa/instr/fmulw.c +++ b/test/mppa/instr/fmulw.c @@ -1,7 +1,7 @@ #include "framework.h" -BEGIN_TEST(double) +BEGIN_TEST(float) { c = ((float)a * (float)b); } -END_TESTF64() +END_TESTF32() diff --git a/test/mppa/instr/fnegw.c b/test/mppa/instr/fnegw.c index acbabf68..fbeaab8e 100644 --- a/test/mppa/instr/fnegw.c +++ b/test/mppa/instr/fnegw.c @@ -1,6 +1,6 @@ #include "framework.h" -BEGIN_TEST(double) +BEGIN_TEST(float) { c = (-(float)a); } diff --git a/test/mppa/instr/framework.h b/test/mppa/instr/framework.h index d4f36f6b..3bbfa271 100644 --- a/test/mppa/instr/framework.h +++ b/test/mppa/instr/framework.h @@ -46,7 +46,7 @@ /* END END_TEST32 */ #define END_TESTF32()\ - printf("%f\t%f\t%f\n", a, b, c);\ + printf("%e\t%e\t%e\n", a, b, c);\ S += c;\ }\ return 0;\ @@ -54,7 +54,7 @@ /* END END_TESTF32 */ #define END_TESTF64()\ - printf("%lf\t%lf\t%lf\n", a, b, c);\ + printf("%e\t%e\t%e\n", a, b, c);\ S += c;\ }\ return 0;\ diff --git a/test/mppa/instr/fsbfw.c b/test/mppa/instr/fsbfw.c index 835963d5..067c40b5 100644 --- a/test/mppa/instr/fsbfw.c +++ b/test/mppa/instr/fsbfw.c @@ -1,6 +1,6 @@ #include "framework.h" -BEGIN_TEST(double) +BEGIN_TEST(float) { c = ((float)a - (float)b); } |