diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-07 09:59:25 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-07 09:59:25 +0100 |
commit | 7ef1d2eafecfd428e25e3cbf37300ebf73a57c02 (patch) | |
tree | 0ec2ca7f5a13c01ba5efa5eae3c1b8083cacb066 | |
parent | 60d41ee18346ff6725ae62a7fa054708805ac9c4 (diff) | |
download | compcert-kvx-7ef1d2eafecfd428e25e3cbf37300ebf73a57c02.tar.gz compcert-kvx-7ef1d2eafecfd428e25e3cbf37300ebf73a57c02.zip |
Experiment Patch of Memory Model
-rw-r--r-- | mppa_k1c/Asmblock.v | 39 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 26 |
3 files changed, 48 insertions, 21 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 86c47613..3305bf95 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -902,8 +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. + +Axiom Val_cmpu_bool_correct: forall (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. + +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), + Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2) + (Val_cmpu cmp v1 v2). +Proof. + intros; 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. + (** 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,12 +932,12 @@ 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 @@ -1038,7 +1059,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 m) + | Pcompw c => rs#d <- (compare_int c rs#s1 rs#s2) | 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) @@ -1072,7 +1093,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset | PArithRRI32 n d s i => match n with - | Pcompiw c => rs#d <- (compare_int c rs#s (Vint i) m) + | Pcompiw c => rs#d <- (compare_int c rs#s (Vint i)) | 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)) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index aa1e7824..fa21d3b1 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -153,7 +153,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 m)) + | Pcompw c => Some (Val (compare_int c v1 v2)) | Pcompl c => Some (Val (compare_long c v1 v2 m)) | _ => None end @@ -195,7 +195,7 @@ Definition arith_eval (ao: arith_op) (l: list value) := | OArithRRI32 n i, [Val v; Memstate m] => match n with - | Pcompiw c => Some (Val (compare_int c v (Vint i) m)) + | Pcompiw c => Some (Val (compare_int c v (Vint i))) | _ => None end diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 76404257..e6e5d11e 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -355,10 +355,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. @@ -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 (*Mem.valid_pointer m*) 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)) . @@ -384,14 +384,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 (*Mem.valid_pointer m*) 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. @@ -607,6 +608,8 @@ Proof. destruct cmp; discriminate. Qed. +Local Hint Resolve Val_cmpu_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 -> @@ -635,7 +638,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. @@ -810,11 +813,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. @@ -899,6 +903,8 @@ Proof. split; intros; Simpl. Qed. +Local Hint Resolve Val_cmpu_correct. + Lemma transl_condimm_int32u_correct: forall cmp rd r1 n k rs m, r1 <> RTMP -> @@ -1116,7 +1122,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 *) |