aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2019-03-07 09:59:25 +0100
committerSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2019-03-07 09:59:25 +0100
commit7ef1d2eafecfd428e25e3cbf37300ebf73a57c02 (patch)
tree0ec2ca7f5a13c01ba5efa5eae3c1b8083cacb066
parent60d41ee18346ff6725ae62a7fa054708805ac9c4 (diff)
downloadcompcert-kvx-7ef1d2eafecfd428e25e3cbf37300ebf73a57c02.tar.gz
compcert-kvx-7ef1d2eafecfd428e25e3cbf37300ebf73a57c02.zip
Experiment Patch of Memory Model
-rw-r--r--mppa_k1c/Asmblock.v39
-rw-r--r--mppa_k1c/Asmblockdeps.v4
-rw-r--r--mppa_k1c/Asmblockgenproof1.v26
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 *)