From b4fd9f9612629c04ddbe492425c679a50bbf3365 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Mar 2019 15:48:16 +0100 Subject: remove dep of exec_arith_instr on memory. TODO: - prove admitted lemma in Asmblockdeps. - remove axioms in Asmblock if possible. --- mppa_k1c/Asmblock.v | 64 +++++++++++++++++++++++++++++++------------- mppa_k1c/Asmblockdeps.v | 25 ++++++----------- mppa_k1c/Asmblockgenproof1.v | 54 ++++++++++++++++--------------------- 3 files changed, 77 insertions(+), 66 deletions(-) diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 3305bf95..0d6c2e79 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -902,20 +902,29 @@ Definition cmpu_for_btest (bt: btest) := | _ => (None, Int) end. -(* FIXME: move these axioms and definitions in a separate file (e.g. PatchMemoryModel). *) -Axiom Val_cmpu_bool: comparison -> val -> val -> option bool. +(* FIXME: put this stuff related to the memory model in a distinct module *) +(* FIXME: currently, only deal with the special case with Archi.ptr64 = true *) +Definition Val_cmpu_bool c v1 v2: option bool := + match v1, v2 with + | Vint n1, Vint n2 => Some (Int.cmpu c n1 n2) + | _, _ => None + end. -Axiom Val_cmpu_bool_correct: forall (m:mem) (cmp: comparison) (v1 v2: val) b, +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. + unfold Val.cmpu_bool, Val_cmpu_bool. + destruct v1, v2; try congruence; vm_compute; try congruence. +Qed. Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2). -Lemma Val_cmpu_correct: forall (m:mem) (cmp: comparison) (v1 v2: val), +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. - intros; unfold Val.cmpu, Val_cmpu. + 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. @@ -923,6 +932,27 @@ Proof. - econstructor. Qed. +Axiom Val_cmplu_bool: forall (cmp: comparison) (v1 v2: val), option bool. + +Axiom Val_cmplu_bool_correct: forall (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. + +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): val := match t with @@ -944,7 +974,7 @@ Definition compare_int (t: itest) (v1 v2: val): val := | 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 @@ -952,12 +982,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 @@ -995,14 +1025,12 @@ 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 exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset := +Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := match ai with | PArithR n d => match n with @@ -1060,7 +1088,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset | PArithRRR n d s1 s2 => match n with | Pcompw c => rs#d <- (compare_int c rs#s1 rs#s2) - | Pcompl c => rs#d <- (compare_long c rs#s1 rs#s2 m) + | Pcompl c => rs#d <- (compare_long c rs#s1 rs#s2) | 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) @@ -1108,7 +1136,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset | PArithRRI64 n d s i => match n with - | Pcompil c => rs#d <- (compare_long c rs#s (Vlong i) m) + | Pcompil c => rs#d <- (compare_long c rs#s (Vlong i)) | 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)) @@ -1156,7 +1184,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 fa21d3b1..fc012557 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -154,7 +154,7 @@ Definition arith_eval (ao: arith_op) (l: list value) := | OArithRRR n, [Val v1; Val v2; Memstate m] => match n with | Pcompw c => Some (Val (compare_int c v1 v2)) - | Pcompl c => Some (Val (compare_long c v1 v2 m)) + | Pcompl c => Some (Val (compare_long c v1 v2)) | _ => None end @@ -193,14 +193,9 @@ Definition arith_eval (ao: arith_op) (l: list value) := | _ => None end - | OArithRRI32 n i, [Val v; Memstate m] => - match n with - | Pcompiw c => Some (Val (compare_int c v (Vint i))) - | _ => None - end - | OArithRRI32 n i, [Val v] => match n with + | Pcompiw c => Some (Val (compare_int c v (Vint i))) | Paddiw => Some (Val (Val.add v (Vint i))) | Pandiw => Some (Val (Val.and v (Vint i))) | Poriw => Some (Val (Val.or v (Vint i))) @@ -211,22 +206,15 @@ Definition arith_eval (ao: arith_op) (l: list value) := | 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 + | Pcompil c => Some (Val (compare_long c v (Vlong i))) | 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 | _, _ => None @@ -796,7 +784,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' @@ -851,9 +839,11 @@ Proof. destruct (ireg_eq g rd); subst; Simpl ]. (* PArithRRI32 *) - destruct i. +Admitted. +(* FIXME: A FINIR all: 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 ]. @@ -866,6 +856,7 @@ Proof. | 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, diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index e6e5d11e..d9ce95ab 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -374,7 +374,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)) . @@ -390,7 +390,7 @@ Proof. 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. + 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. @@ -413,16 +413,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. @@ -433,7 +433,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)) . @@ -443,16 +443,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. @@ -608,7 +607,7 @@ Proof. destruct cmp; discriminate. Qed. -Local Hint Resolve Val_cmpu_bool_correct. +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, @@ -701,7 +700,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. @@ -862,12 +861,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]. @@ -903,7 +902,7 @@ Proof. split; intros; Simpl. Qed. -Local Hint Resolve Val_cmpu_correct. +Local Hint Resolve Val_cmpu_correct Val_cmplu_correct. Lemma transl_condimm_int32u_correct: forall cmp rd r1 n k rs m, @@ -959,19 +958,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: @@ -1000,7 +990,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. @@ -1133,6 +1124,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). -- cgit