Commit 10da6dfa authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

update kvx

parent 728888d8
......@@ -398,8 +398,8 @@ Definition control_eval (o: control_op) (l: list value) :=
end
| Ocbu bt l, [Val v; Val vpc] =>
match cmpu_for_btest bt with
| (Some c, Int) => eval_branch_deps fn l vpc (Val_cmpu_bool c v (Vint (Int.repr 0)))
| (Some c, Long) => eval_branch_deps fn l vpc (Val_cmplu_bool c v (Vlong (Int64.repr 0)))
| (Some c, Int) => eval_branch_deps fn l vpc (Val.mxcmpu_bool c v (Vint (Int.repr 0)))
| (Some c, Long) => eval_branch_deps fn l vpc (Val.mxcmplu_bool c v (Vlong (Int64.repr 0)))
| (None, _) => None
end
| Odiv, [Val v1; Val v2] =>
......@@ -1232,12 +1232,12 @@ Proof.
(* Pcbu *)
+ rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto.
unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i.
++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b.
++ destruct (Val.mxcmpu_bool _ _ _); simpl; auto. destruct b.
+++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl.
intros rr; destruct rr; Simpl.
+++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl.
++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b.
++ destruct (Val.mxcmplu_bool _ _ _); simpl; auto. destruct b.
+++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl.
intros rr; destruct rr; Simpl.
......
......@@ -36,7 +36,6 @@ Require Import Asmblock.
Require Import Asmblockgen.
Require Import Conventions1.
Require Import Axioms.
Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *)
Require Import Asmblockprops.
Module MB:=Machblock.
......
......@@ -256,7 +256,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 cmp rs#r1 rs#r2 = Some b ->
/\ (Val.mxcmpu_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))
.
......@@ -272,8 +272,8 @@ 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 cmp rs#r1 rs#r2) as cmpubool.
destruct cmp; simpl; unfold Val_cmpu;
remember (Val.mxcmpu_bool cmp rs#r1 rs#r2) as cmpubool.
destruct cmp; simpl; unfold Val.mxcmpu;
rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto;
destruct b0; simpl; auto.
}
......@@ -285,7 +285,7 @@ Lemma transl_compui_correct:
exists rs',
exec_straight ge (transl_compi cmp Unsigned r1 n 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 cmp rs#r1 (Vint n) = Some b ->
/\ (Val.mxcmpu_bool cmp rs#r1 (Vint n) = 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))
.
......@@ -301,8 +301,8 @@ Proof.
assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 (Vint n))).
{ rewrite Heqrs'. auto. }
rewrite H0. rewrite <- H.
remember (Val_cmpu_bool cmp rs#r1 (Vint n)) as cmpubool.
destruct cmp; simpl; unfold Val_cmpu;
remember (Val.mxcmpu_bool cmp rs#r1 (Vint n)) as cmpubool.
destruct cmp; simpl; unfold Val.mxcmpu;
rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto;
destruct b0; simpl; auto.
}
......@@ -656,7 +656,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 cmp rs#r1 rs#r2 = Some b ->
/\ ( Val.mxcmplu_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))
.
......@@ -672,9 +672,9 @@ Proof.
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 cmp rs#r1 rs#r2) as cmpbool.
remember (Val.mxcmplu_bool cmp rs#r1 rs#r2) as cmpbool.
destruct cmp; simpl;
unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
unfold compare_long, Val.mxcmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
destruct b0; simpl; auto.
}
rewrite H0. simpl; auto.
......@@ -685,7 +685,7 @@ Lemma transl_compilu_correct:
exists rs',
exec_straight ge (transl_compil cmp Unsigned r1 n 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 cmp rs#r1 (Vlong n) = Some b ->
/\ ( Val.mxcmplu_bool cmp rs#r1 (Vlong n) = 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))
.
......@@ -701,9 +701,9 @@ Proof.
assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 (Vlong n))).
{ rewrite Heqrs'. auto. }
rewrite H0. rewrite <- H.
remember (Val_cmplu_bool cmp rs#r1 (Vlong n)) as cmpbool.
remember (Val.mxcmplu_bool cmp rs#r1 (Vlong n)) as cmpbool.
destruct cmp; simpl;
unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
unfold compare_long, Val.mxcmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
destruct b0; simpl; auto.
}
rewrite H0. simpl; auto.
......@@ -715,7 +715,7 @@ Lemma transl_opt_compuimm_correct:
exists rs', exists insn,
exec_straight_opt (transl_opt_compuimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m
/\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
/\ ( Val_cmpu_bool cmp rs#r1 (Vint n) = Some b ->
/\ ( Val.mxcmpu_bool cmp rs#r1 (Vint n) = Some b ->
exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b))
.
Proof.
......@@ -791,7 +791,7 @@ Lemma transl_opt_compluimm_correct:
exists rs', exists insn,
exec_straight_opt (transl_opt_compluimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m
/\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
/\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = Some b ->
/\ ( Val.mxcmplu_bool cmp rs#r1 (Vlong n) = Some b ->
exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b))
.
Proof.
......@@ -859,7 +859,7 @@ Proof.
destruct cmp; discriminate.
Qed.
Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct: core.
Local Hint Resolve Val.mxcmpu_bool_correct Val.mxcmplu_bool_correct: core.
Lemma transl_cbranch_correct_1:
forall cond args lbl k c m ms b sp rs m' tbb,
......@@ -988,7 +988,7 @@ Proof.
split.
* constructor. eexact A'.
* split; auto.
{ apply C'; auto. eapply Val_cmplu_bool_correct; eauto. }
{ apply C'; auto. eapply Val.mxcmplu_bool_correct; eauto. }
(* Ccompf *)
- exploit (transl_compf_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
......@@ -1078,7 +1078,7 @@ 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 cmp rs#r1 rs#r2
/\ rs'#rd = Val.mxcmpu cmp rs#r1 rs#r2
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
intros. destruct cmp; simpl.
......@@ -1122,7 +1122,7 @@ 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_cmplu cmp rs#r1 rs#r2
/\ rs'#rd = Val.mxcmplu cmp rs#r1 rs#r2
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
intros. destruct cmp; simpl.
......@@ -1163,7 +1163,7 @@ Proof.
split; intros; Simpl.
Qed.
Local Hint Resolve Val_cmpu_correct Val_cmplu_correct: core.
Local Hint Resolve Val.mxcmpu_correct Val.mxcmplu_correct: core.
Lemma transl_condimm_int32u_correct:
forall cmp rd r1 n k rs m,
......@@ -1279,12 +1279,12 @@ Proof.
- 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.
replace (Cge) with (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.
replace (Clt) with (swap_comparison Cgt); auto. rewrite Float32.cmp_swap.
destruct (Float32.cmp _ _ _); auto.
- econstructor; split. apply exec_straight_one; [simpl; eauto].
split; intros; Simpl.
......@@ -1345,12 +1345,12 @@ Proof.
- 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.
replace (Cge) with (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.
replace (Clt) with (swap_comparison Cgt); auto. rewrite Float.cmp_swap.
destruct (Float.cmp _ _ _); auto.
- econstructor; split. apply exec_straight_one; [simpl; eauto].
split; intros; Simpl.
......@@ -1374,7 +1374,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; eapply Val_cmpu_correct.
exists rs'; repeat split; eauto. rewrite B; eapply Val.mxcmpu_correct.
+ (* cmpimm *)
apply transl_condimm_int32s_correct; eauto with asmgen.
+ (* cmpuimm *)
......@@ -1385,7 +1385,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.
eapply Val.mxcmplu_correct.
+ (* cmplimm *)
exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl.
intros (rs' & A & B & C).
......
......@@ -853,58 +853,6 @@ Definition cmpu_for_btest (bt: btest) :=
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; cbn.
- 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|]; cbn.
- erewrite Val_cmplu_bool_correct; eauto.
cbn. econstructor.
- econstructor.
Qed.
(** **** Comparing integers *)
Definition compare_int (t: itest) (v1 v2: val): val :=
match t with
......@@ -914,12 +862,12 @@ Definition compare_int (t: itest) (v1 v2: val): val :=
| ITge => Val.cmp Cge v1 v2
| ITle => Val.cmp Cle v1 v2
| ITgt => Val.cmp 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
| ITneu => Val.mxcmpu Cne v1 v2
| ITequ => Val.mxcmpu Ceq v1 v2
| ITltu => Val.mxcmpu Clt v1 v2
| ITgeu => Val.mxcmpu Cge v1 v2
| ITleu => Val.mxcmpu Cle v1 v2
| ITgtu => Val.mxcmpu Cgt v1 v2
end.
Definition compare_long (t: itest) (v1 v2: val): val :=
......@@ -930,12 +878,12 @@ Definition compare_long (t: itest) (v1 v2: val): val :=
| ITge => Val.cmpl Cge v1 v2
| ITle => Val.cmpl Cle v1 v2
| ITgt => Val.cmpl 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)
| ITneu => Some (Val.mxcmplu Cne v1 v2)
| ITequ => Some (Val.mxcmplu Ceq v1 v2)
| ITltu => Some (Val.mxcmplu Clt v1 v2)
| ITgeu => Some (Val.mxcmplu Cge v1 v2)
| ITleu => Some (Val.mxcmplu Cle v1 v2)
| ITgtu => Some (Val.mxcmplu Cgt v1 v2)
end in
match res with
| Some v => v
......@@ -1147,13 +1095,13 @@ Definition cmove bt v1 v2 v3 :=
Definition cmoveu bt v1 v2 v3 :=
match cmpu_for_btest bt with
| (Some c, Int) =>
match Val_cmpu_bool c v2 (Vint Int.zero) with
match Val.mxcmpu_bool c v2 (Vint Int.zero) with
| None => Vundef
| Some true => v3
| Some false => v1
end
| (Some c, Long) =>
match Val_cmplu_bool c v2 (Vlong Int64.zero) with
match Val.mxcmplu_bool c v2 (Vlong Int64.zero) with
| None => Vundef
| Some true => v3
| Some false => v1
......@@ -1529,8 +1477,8 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset)
end
| Pcbu bt r l =>
match cmpu_for_btest bt with
| (Some c, Int) => par_eval_branch f l rsr rsw mw (Val_cmpu_bool c rsr#r (Vint (Int.repr 0)))
| (Some c, Long) => par_eval_branch f l rsr rsw mw (Val_cmplu_bool c rsr#r (Vlong (Int64.repr 0)))
| (Some c, Int) => par_eval_branch f l rsr rsw mw (Val.mxcmpu_bool c rsr#r (Vint (Int.repr 0)))
| (Some c, Long) => par_eval_branch f l rsr rsw mw (Val.mxcmplu_bool c rsr#r (Vlong (Int64.repr 0)))
| (None, _) => Stuck
end
(**r Pseudo-instructions *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment