diff options
| -rw-r--r-- | mppa_k1c/Asmblock.v | 308 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 181 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 72 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 2 |
4 files changed, 246 insertions, 317 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 86c47613..f2ad60e6 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -902,8 +902,60 @@ Definition cmpu_for_btest (bt: btest) := | _ => (None, Int) end. + +(* a few lemma on comparisons of unsigned (e.g. pointers) *) + +Definition Val_cmpu_bool cmp v1 v2: option bool := + Val.cmpu_bool (fun _ _ => true) cmp v1 v2. + +Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: + (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b + -> (Val_cmpu_bool cmp v1 v2) = Some b. +Proof. + intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto). +Qed. + +Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2). + +Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val): + Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2) + (Val_cmpu cmp v1 v2). +Proof. + unfold Val.cmpu, Val_cmpu. + remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. + destruct ob; simpl. + - erewrite Val_cmpu_bool_correct; eauto. + econstructor. + - econstructor. +Qed. + +Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val) + := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2). + +Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: + (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b + -> (Val_cmplu_bool cmp v1 v2) = Some b. +Proof. + intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto). +Qed. + +Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2). + +Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val): + Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2)) + (Val_cmplu cmp v1 v2). +Proof. + unfold Val.cmplu, Val_cmplu. + remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. + destruct ob as [b|]; simpl. + - erewrite Val_cmplu_bool_correct; eauto. + simpl. econstructor. + - econstructor. +Qed. + + (** Comparing integers *) -Definition compare_int (t: itest) (v1 v2: val) (m: mem): val := +Definition compare_int (t: itest) (v1 v2: val): val := match t with | ITne => Val.cmp Cne v1 v2 | ITeq => Val.cmp Ceq v1 v2 @@ -911,19 +963,19 @@ Definition compare_int (t: itest) (v1 v2: val) (m: mem): val := | ITge => Val.cmp Cge v1 v2 | ITle => Val.cmp Cle v1 v2 | ITgt => Val.cmp Cgt v1 v2 - | ITneu => Val.cmpu (Mem.valid_pointer m) Cne v1 v2 - | ITequ => Val.cmpu (Mem.valid_pointer m) Ceq v1 v2 - | ITltu => Val.cmpu (Mem.valid_pointer m) Clt v1 v2 - | ITgeu => Val.cmpu (Mem.valid_pointer m) Cge v1 v2 - | ITleu => Val.cmpu (Mem.valid_pointer m) Cle v1 v2 - | ITgtu => Val.cmpu (Mem.valid_pointer m) Cgt v1 v2 + | ITneu => Val_cmpu Cne v1 v2 + | ITequ => Val_cmpu Ceq v1 v2 + | ITltu => Val_cmpu Clt v1 v2 + | ITgeu => Val_cmpu Cge v1 v2 + | ITleu => Val_cmpu Cle v1 v2 + | ITgtu => Val_cmpu Cgt v1 v2 | ITall | ITnall | ITany | ITnone => Vundef end. -Definition compare_long (t: itest) (v1 v2: val) (m: mem): val := +Definition compare_long (t: itest) (v1 v2: val): val := let res := match t with | ITne => Val.cmpl Cne v1 v2 | ITeq => Val.cmpl Ceq v1 v2 @@ -931,12 +983,12 @@ Definition compare_long (t: itest) (v1 v2: val) (m: mem): val := | ITge => Val.cmpl Cge v1 v2 | ITle => Val.cmpl Cle v1 v2 | ITgt => Val.cmpl Cgt v1 v2 - | ITneu => Val.cmplu (Mem.valid_pointer m) Cne v1 v2 - | ITequ => Val.cmplu (Mem.valid_pointer m) Ceq v1 v2 - | ITltu => Val.cmplu (Mem.valid_pointer m) Clt v1 v2 - | ITgeu => Val.cmplu (Mem.valid_pointer m) Cge v1 v2 - | ITleu => Val.cmplu (Mem.valid_pointer m) Cle v1 v2 - | ITgtu => Val.cmplu (Mem.valid_pointer m) Cgt v1 v2 + | ITneu => Some (Val_cmplu Cne v1 v2) + | ITequ => Some (Val_cmplu Ceq v1 v2) + | ITltu => Some (Val_cmplu Clt v1 v2) + | ITgeu => Some (Val_cmplu Cge v1 v2) + | ITleu => Some (Val_cmplu Cle v1 v2) + | ITgtu => Some (Val_cmplu Cgt v1 v2) | ITall | ITnall | ITany @@ -974,125 +1026,139 @@ Definition compare_float (t: ftest) (v1 v2: val): val := TODO: subsplitting by instruction type ? Could be useful for expressing auxiliary lemma... -FIXME: replace parameter "m" by a function corresponding to the resul of "(Mem.valid_pointer m)" - *) Variable ge: genv. +Definition arith_eval_r n := + match n with + | Ploadsymbol s ofs => Genv.symbol_address ge s ofs + end +. -Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset := - match ai with - | PArithR n d => - match n with - | Ploadsymbol s ofs => rs#d <- (Genv.symbol_address ge s ofs) - end +Definition arith_eval_rr n v := + match n with + | Pmv => v + | Pnegw => Val.neg v + | Pnegl => Val.negl v + | Pcvtl2w => Val.loword v + | Psxwd => Val.longofint v + | Pzxwd => Val.longofintu v + | Pfnegd => Val.negf v + | Pfnegw => Val.negfs v + | Pfabsd => Val.absf v + | Pfabsw => Val.absfs v + | Pfnarrowdw => Val.singleoffloat v + | Pfwidenlwd => Val.floatofsingle v + | Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end + | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end + | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end + | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end + | Pfloatudrnsz_i32 => match Val.floatofintu v with Some f => f | _ => Vundef end + | Pfloatdrnsz_i32 => match Val.floatofint v with Some f => f | _ => Vundef end + | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end + | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end + | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end + | Pfixedudrzz => match Val.longuoffloat v with Some i => i | _ => Vundef end + | Pfixeddrzz_i32 => match Val.intoffloat v with Some i => i | _ => Vundef end + | Pfixedudrzz_i32 => match Val.intuoffloat v with Some i => i | _ => Vundef end + end. - | PArithRR n d s => - match n with - | Pmv => rs#d <- (rs#s) - | Pnegw => rs#d <- (Val.neg rs#s) - | Pnegl => rs#d <- (Val.negl rs#s) - | Pcvtl2w => rs#d <- (Val.loword rs#s) - | Psxwd => rs#d <- (Val.longofint rs#s) - | Pzxwd => rs#d <- (Val.longofintu rs#s) - | Pfnegd => rs#d <- (Val.negf rs#s) - | Pfnegw => rs#d <- (Val.negfs rs#s) - | Pfabsd => rs#d <- (Val.absf rs#s) - | Pfabsw => rs#d <- (Val.absfs rs#s) - | 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 +Definition arith_eval_ri32 n i := + match n with + | Pmake => Vint i + end. - | PArithRI32 n d i => - match n with - | Pmake => rs#d <- (Vint i) - end +Definition arith_eval_ri64 n i := + match n with + | Pmakel => Vlong i + end. - | PArithRI64 n d i => - match n with - | Pmakel => rs#d <- (Vlong i) - end +Definition arith_eval_rf32 n i := + match n with + | Pmakefs => Vsingle i + end. - | PArithRF32 n d i => - match n with - | Pmakefs => rs#d <- (Vsingle i) - end +Definition arith_eval_rf64 n i := + match n with + | Pmakef => Vfloat i + end. - | PArithRF64 n d i => - match n with - | Pmakef => rs#d <- (Vfloat i) - end +Definition arith_eval_rrr n v1 v2 := + match n with + | Pcompw c => compare_int c v1 v2 + | Pcompl c => compare_long c v1 v2 + | Pfcompw c => compare_single c v1 v2 + | Pfcompl c => compare_float c v1 v2 + + | Paddw => Val.add v1 v2 + | Psubw => Val.sub v1 v2 + | Pmulw => Val.mul v1 v2 + | Pandw => Val.and v1 v2 + | Porw => Val.or v1 v2 + | Pxorw => Val.xor v1 v2 + | Psrlw => Val.shru v1 v2 + | Psraw => Val.shr v1 v2 + | Psllw => Val.shl v1 v2 + + | Paddl => Val.addl v1 v2 + | Psubl => Val.subl v1 v2 + | Pandl => Val.andl v1 v2 + | Porl => Val.orl v1 v2 + | Pxorl => Val.xorl v1 v2 + | Pmull => Val.mull v1 v2 + | Pslll => Val.shll v1 v2 + | Psrll => Val.shrlu v1 v2 + | Psral => Val.shrl v1 v2 + + | Pfaddd => Val.addf v1 v2 + | Pfaddw => Val.addfs v1 v2 + | Pfsbfd => Val.subf v1 v2 + | Pfsbfw => Val.subfs v1 v2 + | Pfmuld => Val.mulf v1 v2 + | Pfmulw => Val.mulfs v1 v2 + end. - | PArithRRR n d s1 s2 => - 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) - | Pandw => rs#d <- (Val.and rs#s1 rs#s2) - | Porw => rs#d <- (Val.or rs#s1 rs#s2) - | Pxorw => rs#d <- (Val.xor rs#s1 rs#s2) - | Psrlw => rs#d <- (Val.shru rs#s1 rs#s2) - | Psraw => rs#d <- (Val.shr rs#s1 rs#s2) - | Psllw => rs#d <- (Val.shl rs#s1 rs#s2) - - | Paddl => rs#d <- (Val.addl rs#s1 rs#s2) - | Psubl => rs#d <- (Val.subl rs#s1 rs#s2) - | Pandl => rs#d <- (Val.andl rs#s1 rs#s2) - | Porl => rs#d <- (Val.orl rs#s1 rs#s2) - | Pxorl => rs#d <- (Val.xorl rs#s1 rs#s2) - | Pmull => rs#d <- (Val.mull rs#s1 rs#s2) - | Pslll => rs#d <- (Val.shll rs#s1 rs#s2) - | Psrll => rs#d <- (Val.shrlu rs#s1 rs#s2) - | Psral => rs#d <- (Val.shrl rs#s1 rs#s2) - - | Pfaddd => rs#d <- (Val.addf rs#s1 rs#s2) - | Pfaddw => rs#d <- (Val.addfs rs#s1 rs#s2) - | Pfsbfd => rs#d <- (Val.subf rs#s1 rs#s2) - | Pfsbfw => rs#d <- (Val.subfs rs#s1 rs#s2) - | Pfmuld => rs#d <- (Val.mulf rs#s1 rs#s2) - | Pfmulw => rs#d <- (Val.mulfs rs#s1 rs#s2) - end +Definition arith_eval_rri32 n v i := + match n with + | Pcompiw c => compare_int c v (Vint i) + | Paddiw => Val.add v (Vint i) + | Pandiw => Val.and v (Vint i) + | Poriw => Val.or v (Vint i) + | Pxoriw => Val.xor v (Vint i) + | Psraiw => Val.shr v (Vint i) + | Psrliw => Val.shru v (Vint i) + | Pslliw => Val.shl v (Vint i) + | Psllil => Val.shll v (Vint i) + | Psrlil => Val.shrlu v (Vint i) + | Psrail => Val.shrl v (Vint i) + end. - | PArithRRI32 n d s i => - match n with - | Pcompiw c => rs#d <- (compare_int c rs#s (Vint i) m) - | Paddiw => rs#d <- (Val.add rs#s (Vint i)) - | Pandiw => rs#d <- (Val.and rs#s (Vint i)) - | Poriw => rs#d <- (Val.or rs#s (Vint i)) - | Pxoriw => rs#d <- (Val.xor rs#s (Vint i)) - | Psraiw => rs#d <- (Val.shr rs#s (Vint i)) - | Psrliw => rs#d <- (Val.shru rs#s (Vint i)) - | Pslliw => rs#d <- (Val.shl rs#s (Vint i)) - | Psllil => rs#d <- (Val.shll rs#s (Vint i)) - | Psrlil => rs#d <- (Val.shrlu rs#s (Vint i)) - | Psrail => rs#d <- (Val.shrl rs#s (Vint i)) - end +Definition arith_eval_rri64 n v i := + match n with + | Pcompil c => compare_long c v (Vlong i) + | Paddil => Val.addl v (Vlong i) + | Pandil => Val.andl v (Vlong i) + | Poril => Val.orl v (Vlong i) + | Pxoril => Val.xorl v (Vlong i) + end. - | PArithRRI64 n d s i => - match n with - | Pcompil c => rs#d <- (compare_long c rs#s (Vlong i) m) - | Paddil => rs#d <- (Val.addl rs#s (Vlong i)) - | Pandil => rs#d <- (Val.andl rs#s (Vlong i)) - | Poril => rs#d <- (Val.orl rs#s (Vlong i)) - | Pxoril => rs#d <- (Val.xorl rs#s (Vlong i)) - end +Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := + match ai with + | PArithR n d => rs#d <- (arith_eval_r n) + + | PArithRR n d s => rs#d <- (arith_eval_rr n rs#s) + + | PArithRI32 n d i => rs#d <- (arith_eval_ri32 n i) + | PArithRI64 n d i => rs#d <- (arith_eval_ri64 n i) + | PArithRF32 n d i => rs#d <- (arith_eval_rf32 n i) + | PArithRF64 n d i => rs#d <- (arith_eval_rf64 n i) + + | PArithRRR n d s1 s2 => rs#d <- (arith_eval_rrr n rs#s1 rs#s2) + + | PArithRRI32 n d s i => rs#d <- (arith_eval_rri32 n rs#s i) + + | PArithRRI64 n d s i => rs#d <- (arith_eval_rri64 n rs#s i) end. (** * load/store *) @@ -1135,7 +1201,7 @@ Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem) Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset := match bi with - | PArith ai => Next (exec_arith_instr ai rs m) m + | PArith ai => Next (exec_arith_instr ai rs) m | PLoadRRO n d a ofs => match n with diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 8e176f2d..b7e7b87c 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -98,136 +98,19 @@ Definition op := op_wrap. Definition arith_eval (ao: arith_op) (l: list value) := let (ge, fn) := Ge in match ao, l with - | OArithR n, [] => - match n with - | Ploadsymbol s ofs => Some (Val (Genv.symbol_address ge s ofs)) - end - - | OArithRR n, [Val v] => - match n with - | Pmv => Some (Val v) - | Pnegw => Some (Val (Val.neg v)) - | Pnegl => Some (Val (Val.negl v)) - | Pcvtl2w => Some (Val (Val.loword v)) - | Psxwd => Some (Val (Val.longofint v)) - | Pzxwd => Some (Val (Val.longofintu v)) - | Pfnegd => Some (Val (Val.negf v)) - | Pfnegw => Some (Val (Val.negfs v)) - | Pfabsd => Some (Val (Val.absf v)) - | Pfabsw => Some (Val (Val.absfs v)) - | 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, [] => - match n with - | Pmake => Some (Val (Vint i)) - end - - | OArithRI64 n i, [] => - match n with - | Pmakel => Some (Val (Vlong i)) - end + | OArithR n, [] => Some (Val (arith_eval_r ge n)) - | OArithRF32 n i, [] => - match n with - | Pmakefs => Some (Val (Vsingle i)) - end + | OArithRR n, [Val v] => Some (Val (arith_eval_rr n v)) - | OArithRF64 n i, [] => - match n with - | Pmakef => Some (Val (Vfloat i)) - end + | OArithRI32 n i, [] => Some (Val (arith_eval_ri32 n i)) + | OArithRI64 n i, [] => Some (Val (arith_eval_ri64 n i)) + | OArithRF32 n i, [] => Some (Val (arith_eval_rf32 n i)) + | OArithRF64 n i, [] => Some (Val (arith_eval_rf64 n i)) - | OArithRRR n, [Val v1; Val v2; Memstate m] => - match n with - | Pcompw c => Some (Val (compare_int c v1 v2 m)) - | Pcompl c => Some (Val (compare_long c v1 v2 m)) - | _ => None - end + | OArithRRR n, [Val v1; Val v2] => Some (Val (arith_eval_rrr n v1 v2)) - | 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)) - | Pandw => Some (Val (Val.and v1 v2)) - | Porw => Some (Val (Val.or v1 v2)) - | Pxorw => Some (Val (Val.xor v1 v2)) - | Psrlw => Some (Val (Val.shru v1 v2)) - | Psraw => Some (Val (Val.shr v1 v2)) - | Psllw => Some (Val (Val.shl v1 v2)) - - | Paddl => Some (Val (Val.addl v1 v2)) - | Psubl => Some (Val (Val.subl v1 v2)) - | Pandl => Some (Val (Val.andl v1 v2)) - | Porl => Some (Val (Val.orl v1 v2)) - | Pxorl => Some (Val (Val.xorl v1 v2)) - | Pmull => Some (Val (Val.mull v1 v2)) - | Pslll => Some (Val (Val.shll v1 v2)) - | Psrll => Some (Val (Val.shrlu v1 v2)) - | Psral => Some (Val (Val.shrl v1 v2)) - - | Pfaddd => Some (Val (Val.addf v1 v2)) - | Pfaddw => Some (Val (Val.addfs v1 v2)) - | Pfsbfd => Some (Val (Val.subf v1 v2)) - | Pfsbfw => Some (Val (Val.subfs v1 v2)) - | Pfmuld => Some (Val (Val.mulf v1 v2)) - | Pfmulw => Some (Val (Val.mulfs v1 v2)) - - | _ => None - end - - | OArithRRI32 n i, [Val v; Memstate m] => - match n with - | Pcompiw c => Some (Val (compare_int c v (Vint i) m)) - | _ => None - end - - | OArithRRI32 n i, [Val v] => - match n with - | Paddiw => Some (Val (Val.add v (Vint i))) - | Pandiw => Some (Val (Val.and v (Vint i))) - | Poriw => Some (Val (Val.or v (Vint i))) - | Pxoriw => Some (Val (Val.xor v (Vint i))) - | Psraiw => Some (Val (Val.shr v (Vint i))) - | Psrliw => Some (Val (Val.shru v (Vint i))) - | Pslliw => Some (Val (Val.shl v (Vint i))) - | Psllil => Some (Val (Val.shll v (Vint i))) - | Psrlil => Some (Val (Val.shrlu v (Vint i))) - | Psrail => Some (Val (Val.shrl v (Vint i))) - | _ => None - end - - | OArithRRI64 n i, [Val v; Memstate m] => - match n with - | Pcompil c => Some (Val (compare_long c v (Vlong i) m)) - | _ => None - end - - | OArithRRI64 n i, [Val v] => - match n with - | Paddil => Some (Val (Val.addl v (Vlong i))) - | Pandil => Some (Val (Val.andl v (Vlong i))) - | Poril => Some (Val (Val.orl v (Vlong i))) - | Pxoril => Some (Val (Val.xorl v (Vlong i))) - | _ => None - end + | OArithRRI32 n i, [Val v] => Some (Val (arith_eval_rri32 n v i)) + | OArithRRI64 n i, [Val v] => Some (Val (arith_eval_rri64 n v i)) | _, _ => None end. @@ -621,21 +504,9 @@ 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 => - 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 + | 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))] end. @@ -800,7 +671,7 @@ Qed. Lemma trans_arith_correct: forall ge fn i rs m rs' s, - exec_arith_instr ge i rs m = rs' -> + exec_arith_instr ge i rs = rs' -> match_states (State rs m) s -> exists s', macro_run (Genv ge fn) (trans_arith i) s s = Some s' @@ -808,62 +679,56 @@ Lemma trans_arith_correct: Proof. intros. unfold exec_arith_instr in H. destruct i. (* Ploadsymbol *) - - destruct i. inv H. inv H0. - eexists; split; try split. + - 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; + - 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. + - 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. + - 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. + - 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. + - 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; + - 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; + - inv H; inv H0; eexists; split; try split; - [ simpl; pose (H1 rs0); simpl in e; rewrite e; try (rewrite H); reflexivity + [ simpl; pose (H1 rs0); simpl in e; rewrite e; try (rewrite H); auto | Simpl | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. -(* PArithRRI64 *) - - destruct i. - all: inv H; inv H0; + - inv H; inv H0; eexists; split; try split; [ simpl; pose (H1 rs0); simpl in e; rewrite e; try (rewrite H); reflexivity | Simpl diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 060f1a85..1a55f58e 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -353,10 +353,10 @@ Proof. - split. + intros; Simpl. + intros. - remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)) as rs'. + remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Signed) rs # r1 rs # r2)) as rs'. simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b). { - assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)). + assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Signed) rs # r1 rs # r2)). { rewrite Heqrs'. auto. } rewrite H0. rewrite <- H. remember (Val.cmp_bool cmp rs#r1 rs#r2) as cmpbool. @@ -372,7 +372,7 @@ Lemma transl_compu_correct: exists rs', exec_straight ge (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ ( Val.cmpu_bool (Mem.valid_pointer m) cmp rs#r1 rs#r2 = Some b -> + /\ (Val_cmpu_bool cmp rs#r1 rs#r2 = Some b -> exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . @@ -382,14 +382,15 @@ Proof. - split. + intros; Simpl. + intros. - remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)) as rs'. + remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)) as rs'. simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b). { - assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)). + assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)). { rewrite Heqrs'. auto. } rewrite H0. rewrite <- H. - remember (Val.cmpu_bool (Mem.valid_pointer m) cmp rs#r1 rs#r2) as cmpubool. - destruct cmp; simpl; unfold Val.cmpu; rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto; + remember (Val_cmpu_bool cmp rs#r1 rs#r2) as cmpubool. + destruct cmp; simpl; unfold Val_cmpu; + rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto; destruct b0; simpl; auto. } rewrite H0. simpl; auto. @@ -410,16 +411,16 @@ Proof. - split. + intros; Simpl. + intros. - remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)) as rs'. + remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2)) as rs'. simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b). { - assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)). + assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2)). { rewrite Heqrs'. auto. } rewrite H0. rewrite <- H. remember (Val.cmpl_bool cmp rs#r1 rs#r2) as cmpbool. destruct cmp; simpl; - unfold compare_long; - unfold Val.cmpl; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + unfold compare_long, Val.cmpl; + rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto. } rewrite H0. simpl; auto. @@ -712,7 +713,7 @@ Lemma transl_complu_correct: exists rs', exec_straight ge (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ ( Val.cmplu_bool (Mem.valid_pointer m) cmp rs#r1 rs#r2 = Some b -> + /\ ( Val_cmplu_bool cmp rs#r1 rs#r2 = Some b -> exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . @@ -722,16 +723,15 @@ Proof. - split. + intros; Simpl. + intros. - remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)) as rs'. + remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)) as rs'. simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b). { - assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2 m)). + assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)). { rewrite Heqrs'. auto. } rewrite H0. rewrite <- H. - remember (Val.cmplu_bool (Mem.valid_pointer m) cmp rs#r1 rs#r2) as cmpbool. + remember (Val_cmplu_bool cmp rs#r1 rs#r2) as cmpbool. destruct cmp; simpl; - unfold compare_long; - unfold Val.cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto. } rewrite H0. simpl; auto. @@ -887,6 +887,8 @@ Proof. destruct cmp; discriminate. Qed. +Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct. + Lemma transl_cbranch_correct_1: forall cond args lbl k c m ms b sp rs m' tbb, transl_cbranch cond args lbl k = OK c -> @@ -915,7 +917,7 @@ Proof. exists rs', (Pcb BTwnez RTMP lbl). split. + constructor. eexact A. - + split; auto. apply C; auto. + + split; auto. apply C; eauto. (* Ccompimm *) - remember (Int.eq n Int.zero) as eqz. destruct eqz. @@ -978,7 +980,7 @@ Proof. exists rs', (Pcb BTwnez RTMP lbl). split. + constructor. eexact A. - + split; auto. apply C; auto. + + split; auto. apply C; eauto. (* Ccomplimm *) - remember (Int64.eq n Int64.zero) as eqz. destruct eqz. @@ -1118,11 +1120,12 @@ Proof. split; intros; Simpl. Qed. + Lemma transl_cond_int32u_correct: forall cmp rd r1 r2 k rs m, exists rs', exec_straight ge (basics_to_code (transl_cond_int32u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m - /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs#r1 rs#r2 + /\ rs'#rd = Val_cmpu cmp rs#r1 rs#r2 /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. @@ -1166,12 +1169,12 @@ Lemma transl_cond_int64u_correct: forall cmp rd r1 r2 k rs m, exists rs', exec_straight ge (basics_to_code (transl_cond_int64u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m - /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 rs#r2) + /\ rs'#rd = Val_cmplu cmp rs#r1 rs#r2 /\ 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. + split; intros; Simpl. - econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. - econstructor; split. apply exec_straight_one; [simpl; eauto]. @@ -1207,6 +1210,8 @@ Proof. split; intros; Simpl. Qed. +Local Hint Resolve Val_cmpu_correct Val_cmplu_correct. + Lemma transl_condimm_int32u_correct: forall cmp rd r1 n k rs m, r1 <> RTMP -> @@ -1261,19 +1266,10 @@ Lemma transl_condimm_int64u_correct: /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> 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. -- econstructor; split. apply exec_straight_one; [simpl; eauto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto]. - split; intros; Simpl. + intros. destruct cmp; simpl; + (econstructor; split; + [ apply exec_straight_one; [simpl; eauto] | + split; intros; Simpl; unfold compare_long; eauto]). Qed. Lemma swap_comparison_cmpfs: @@ -1302,7 +1298,8 @@ Proof. 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]. +- econstructor; split. apply exec_straight_one; [simpl; + eauto]. split; intros; Simpl. Qed. @@ -1424,7 +1421,7 @@ Proof. exploit transl_cond_int32s_correct; eauto. simpl. intros (rs' & A & B & C). exists rs'; eauto. + (* cmpu *) exploit transl_cond_int32u_correct; eauto. simpl. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite B; auto. + exists rs'; repeat split; eauto. rewrite B; eapply Val_cmpu_correct. + (* cmpimm *) apply transl_condimm_int32s_correct; eauto with asmgen. + (* cmpuimm *) @@ -1435,6 +1432,7 @@ Proof. + (* cmplu *) exploit transl_cond_int64u_correct; eauto. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto. + eapply Val_cmplu_correct. + (* cmplimm *) exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. intros (rs' & A & B & C). diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index f969e5b4..8ad30e81 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -575,7 +575,7 @@ Lemma transf_exec_basic_instr: 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: unfold exec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. 1-10: apply transf_exec_load. all: apply transf_exec_store. Qed. |