Commit 728888d8 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

Val_cmp* -> Val.mxcmp*

parent ac8b7ae0
......@@ -274,10 +274,14 @@ latexdoc:
@tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; }
@chmod a-w $*.v
# this trick aims to allow extraction to depend on the target processor
# (currently: export extra Coq-functions for OCaml code, depending on the target)
extraction/extraction.v: Makefile extraction/extraction.vexpand
cat extraction/extraction.vexpand > extraction/extraction.v
echo "$(EXTRA_EXTRACTION)" >> extraction/extraction.v
echo "." >> extraction/extraction.v
(echo "(* WARNING: this file is generated from extraction.vexpand *)"; \
echo "(* by the Makefile -- target \"extraction/extraction.v\" *)\n"; \
cat extraction/extraction.vexpand; \
echo "$(EXTRA_EXTRACTION)"; \
echo ".") > extraction/extraction.v
driver/Compiler.v: driver/Compiler.vexpand tools/compiler_expand
tools/compiler_expand driver/Compiler.vexpand $@
......
......@@ -416,60 +416,6 @@ Definition outcome := option state.
Definition Next rs m: outcome := Some (State rs m).
Definition Stuck: outcome := None.
(* a few lemma on comparisons of unsigned (e.g. pointers)
TODO: these lemma are a copy/paste of kvx/Asmvliw.v (sharing to improve!)
*)
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.
(** Testing a condition *)
Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
......@@ -540,8 +486,8 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
Definition eval_testzero (sz: isize) (v: val): option bool :=
match sz with
| W => Val_cmpu_bool Ceq v (Vint Int.zero)
| X => Val_cmplu_bool Ceq v (Vlong Int64.zero)
| W => Val.mxcmpu_bool Ceq v (Vint Int.zero)
| X => Val.mxcmplu_bool Ceq v (Vlong Int64.zero)
end.
(** Integer "bit is set?" test *)
......@@ -557,14 +503,14 @@ Definition eval_testbit (sz: isize) (v: val) (n: int): option bool :=
Definition compare_int (rs: regset) (v1 v2: val) :=
rs#CN <- (Val.negative (Val.sub v1 v2))
#CZ <- (Val_cmpu Ceq v1 v2)
#CC <- (Val_cmpu Cge v1 v2)
#CZ <- (Val.mxcmpu Ceq v1 v2)
#CC <- (Val.mxcmpu Cge v1 v2)
#CV <- (Val.sub_overflow v1 v2).
Definition compare_long (rs: regset) (v1 v2: val) :=
rs#CN <- (Val.negativel (Val.subl v1 v2))
#CZ <- (Val_cmplu Ceq v1 v2)
#CC <- (Val_cmplu Cge v1 v2)
#CZ <- (Val.mxcmplu Ceq v1 v2)
#CC <- (Val.mxcmplu Cge v1 v2)
#CV <- (Val.subl_overflow v1 v2).
(** Semantics of [fcmp] instructions:
......
......@@ -211,14 +211,14 @@ Coercion Control: control_op >-> op_wrap.
Definition v_compare_int (v1 v2: val) : CRflags :=
{| _CN := (Val.negative (Val.sub v1 v2));
_CZ := (Val_cmpu Ceq v1 v2);
_CC := (Val_cmpu Cge v1 v2);
_CZ := (Val.mxcmpu Ceq v1 v2);
_CC := (Val.mxcmpu Cge v1 v2);
_CV := (Val.sub_overflow v1 v2) |}.
Definition v_compare_long (v1 v2: val) : CRflags :=
{| _CN := (Val.negativel (Val.subl v1 v2));
_CZ := (Val_cmplu Ceq v1 v2);
_CC := (Val_cmplu Cge v1 v2);
_CZ := (Val.mxcmplu Ceq v1 v2);
_CC := (Val.mxcmplu Cge v1 v2);
_CV := (Val.subl_overflow v1 v2) |}.
Definition v_compare_float (v1 v2: val) : CRflags :=
......@@ -1842,8 +1842,8 @@ Proof.
destruct (PregEq.eq r PC);
[ rewrite e; destruct sz0; simpl; Simpl sr |
destruct sz0; simpl; replace_pc; rewrite Pregmap.gso; auto; repeat Simpl_rep sr; try rewrite H0;
try (destruct (Val_cmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
try (destruct (Val_cmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
try (destruct (Val.mxcmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
try (destruct (Val.mxcmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
try (destruct (Val.cmp_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
try (destruct (Val.cmpl_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
try (simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr);
......
......@@ -1245,7 +1245,7 @@ Definition transf_function (f: Machblock.function) : res Asmblock.function :=
else OK tf.
Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
transf_partial_fundef transf_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *)
transf_partial_fundef transf_function f.
Definition transf_program (p: Machblock.program) : res Asmblock.program :=
transform_partial_program transf_fundef p.
......
......@@ -37,7 +37,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.
......
......@@ -896,8 +896,8 @@ Ltac TranslOpBase :=
Lemma compare_int_spec: forall rs v1 v2,
let rs' := compare_int rs v1 v2 in
rs'#CN = (Val.negative (Val.sub v1 v2))
/\ rs'#CZ = (Val_cmpu Ceq v1 v2)
/\ rs'#CC = (Val_cmpu Cge v1 v2)
/\ rs'#CZ = (Val.mxcmpu Ceq v1 v2)
/\ rs'#CC = (Val.mxcmpu Cge v1 v2)
/\ rs'#CV = (Val.sub_overflow v1 v2).
Proof.
intros; unfold rs'; auto.
......@@ -912,7 +912,7 @@ Proof.
unfold eval_testcond; rewrite B, C, D, E.
destruct v1; try discriminate; destruct v2; try discriminate.
simpl in H; inv H.
unfold Val_cmpu; simpl. destruct c; simpl.
unfold Val.mxcmpu; simpl. destruct c; simpl.
- destruct (Int.eq i i0); auto.
- destruct (Int.eq i i0); auto.
- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto.
......@@ -924,7 +924,7 @@ Proof.
Qed.
Lemma eval_testcond_compare_uint: forall c v1 v2 b rs,
Val_cmpu_bool c v1 v2 = Some b ->
Val.mxcmpu_bool c v1 v2 = Some b ->
eval_testcond (cond_for_unsigned_cmp c) (compare_int rs v1 v2) = Some b.
Proof.
intros. generalize (compare_int_spec rs v1 v2).
......@@ -932,7 +932,7 @@ Proof.
unfold eval_testcond; rewrite B, C, D, E.
destruct v1; try discriminate; destruct v2; try discriminate.
simpl in H; inv H.
unfold Val_cmpu; simpl. destruct c; simpl.
unfold Val.mxcmpu; simpl. destruct c; simpl.
- destruct (Int.eq i i0); auto.
- destruct (Int.eq i i0); auto.
- destruct (Int.ltu i i0); auto.
......@@ -944,8 +944,8 @@ Qed.
Lemma compare_long_spec: forall rs v1 v2,
let rs' := compare_long rs v1 v2 in
rs'#CN = (Val.negativel (Val.subl v1 v2))
/\ rs'#CZ = (Val_cmplu Ceq v1 v2)
/\ rs'#CC = (Val_cmplu Cge v1 v2)
/\ rs'#CZ = (Val.mxcmplu Ceq v1 v2)
/\ rs'#CC = (Val.mxcmplu Cge v1 v2)
/\ rs'#CV = (Val.subl_overflow v1 v2).
Proof.
intros; unfold rs'; auto.
......@@ -977,7 +977,7 @@ Proof.
unfold eval_testcond; rewrite B, C, D, E.
destruct v1; try discriminate; destruct v2; try discriminate.
simpl in H; inv H.
unfold Val_cmplu; simpl. destruct c; simpl.
unfold Val.mxcmplu; simpl. destruct c; simpl.
- destruct (Int64.eq i i0); auto.
- destruct (Int64.eq i i0); auto.
- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto.
......@@ -989,12 +989,12 @@ Proof.
Qed.
Lemma eval_testcond_compare_ulong: forall c v1 v2 b rs,
Val_cmplu_bool c v1 v2 = Some b ->
Val.mxcmplu_bool c v1 v2 = Some b ->
eval_testcond (cond_for_unsigned_cmp c) (compare_long rs v1 v2) = Some b.
Proof.
intros. generalize (compare_long_spec rs v1 v2).
set (rs' := compare_long rs v1 v2). intros (B & C & D & E).
unfold eval_testcond; rewrite B, C, D, E; unfold Val_cmplu.
unfold eval_testcond; rewrite B, C, D, E; unfold Val.mxcmplu.
destruct v1; try discriminate; destruct v2; try discriminate; simpl in H.
- (* int-int *)
inv H. destruct c; simpl.
......@@ -1207,7 +1207,7 @@ Proof.
- (* Ccomplu *)
econstructor; split. apply exec_straight_one. simpl; eauto.
split; intros. apply eval_testcond_compare_ulong; auto.
erewrite Val_cmplu_bool_correct; eauto.
erewrite Val.mxcmplu_bool_correct; eauto.
destruct r; reflexivity || discriminate.
- (* Ccomplimm *)
destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
......@@ -1228,19 +1228,19 @@ Proof.
destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))].
+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto.
erewrite Val_cmplu_bool_correct; eauto.
erewrite Val.mxcmplu_bool_correct; eauto.
destruct r; reflexivity || discriminate.
+ econstructor; split.
apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto.
split; intros. apply eval_testcond_compare_ulong; auto.
erewrite Val_cmplu_bool_correct; eauto.
erewrite Val.mxcmplu_bool_correct; eauto.
destruct r; reflexivity || discriminate.
+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C).
econstructor; split.
eapply exec_straight_trans. eexact A. apply exec_straight_one.
simpl. rewrite B, C by eauto with asmgen. eauto.
split; intros. apply eval_testcond_compare_ulong; auto.
erewrite Val_cmplu_bool_correct; eauto.
erewrite Val.mxcmplu_bool_correct; eauto.
transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen.
- (* Ccomplshift *)
econstructor; split. apply exec_straight_one. simpl; eauto.
......@@ -1249,7 +1249,7 @@ Proof.
- (* Ccomplushift *)
econstructor; split. apply exec_straight_one. simpl; eauto.
split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto.
erewrite Val_cmplu_bool_correct; eauto.
erewrite Val.mxcmplu_bool_correct; eauto.
destruct r; reflexivity || discriminate.
- (* Cmasklzero *)
destruct (is_logical_imm64 n).
......@@ -1368,7 +1368,7 @@ Local Opaque transl_cond transl_cond_branch_default.
apply Int.same_if_eq in N0; subst n; ArgsInv.
+ (* Ccompuimm Cne 0 *)
econstructor; split. econstructor.
split; auto. simpl. apply Val_cmpu_bool_correct in EV.
split; auto. simpl. apply Val.mxcmpu_bool_correct in EV.
unfold incrPC. Simpl. rewrite EV. auto.
+ (* Ccompuimm Ceq 0 *)
monadInv TR. ArgsInv. simpl in *.
......@@ -1408,7 +1408,7 @@ Local Opaque transl_cond transl_cond_branch_default.
apply Int64.same_if_eq in N0; subst n; ArgsInv.
+ (* Ccompluimm Cne 0 *)
econstructor; split. econstructor.
split; auto. simpl. apply Val_cmplu_bool_correct in EV.
split; auto. simpl. apply Val.mxcmplu_bool_correct in EV.
unfold incrPC. Simpl. rewrite EV. auto.
+ (* Ccompluimm Ceq 0 *)
econstructor; split. econstructor.
......
This diff is collapsed.
......@@ -2613,6 +2613,55 @@ Qed.
End VAL_INJ_OPS.
(* Specializations of cmpu_bool, cmpu, cmplu_bool, and cmplu for maximal pointer validity *)
Definition mxcmpu_bool cmp v1 v2: option bool :=
cmpu_bool (fun _ _ => true) cmp v1 v2.
Lemma mxcmpu_bool_correct vptr (cmp: comparison) (v1 v2: val) b:
cmpu_bool vptr cmp v1 v2 = Some b
-> mxcmpu_bool cmp v1 v2 = Some b.
Proof.
intros; eapply cmpu_bool_lessdef; (econstructor 1 || eauto).
Qed.
Definition mxcmpu cmp v1 v2 := of_optbool (mxcmpu_bool cmp v1 v2).
Lemma mxcmpu_correct vptr (cmp: comparison) (v1 v2: val):
lessdef (cmpu vptr cmp v1 v2) (mxcmpu cmp v1 v2).
Proof.
unfold cmpu, mxcmpu.
remember (cmpu_bool _ cmp v1 v2) as ob.
destruct ob; simpl.
- erewrite mxcmpu_bool_correct; eauto.
econstructor.
- econstructor.
Qed.
Definition mxcmplu_bool (cmp: comparison) (v1 v2: val)
:= (cmplu_bool (fun _ _ => true) cmp v1 v2).
Lemma mxcmplu_bool_correct vptr (cmp: comparison) (v1 v2: val) b:
(cmplu_bool vptr cmp v1 v2) = Some b
-> (mxcmplu_bool cmp v1 v2) = Some b.
Proof.
intros; eapply cmplu_bool_lessdef; (econstructor 1 || eauto).
Qed.
Definition mxcmplu cmp v1 v2 := of_optbool (mxcmplu_bool cmp v1 v2).
Lemma mxcmplu_correct vptr (cmp: comparison) (v1 v2: val):
lessdef (maketotal (cmplu vptr cmp v1 v2))
(mxcmplu cmp v1 v2).
Proof.
unfold cmplu, mxcmplu.
remember (cmplu_bool _ cmp v1 v2) as ob.
destruct ob as [b|]; simpl.
- erewrite mxcmplu_bool_correct; eauto.
simpl. econstructor.
- econstructor.
Qed.
End Val.
Notation meminj := Val.meminj.
......
......@@ -1053,6 +1053,41 @@ Proof.
induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto.
Qed.
Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2).
Proof.
induction l1; cbn; auto with coqlib.
Qed.
Hint Resolve is_tail_app: coqlib.
Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3.
Proof.
induction l1; cbn; auto with coqlib.
intros l2 l3 H; inversion H; eauto with coqlib.
Qed.
Hint Resolve is_tail_app_inv: coqlib.
Lemma is_tail_app_right A (l2 l1: list A): is_tail l1 (l2++l1).
Proof.
intros; eauto with coqlib.
Qed.
Lemma is_tail_app_def A (l1 l2: list A):
is_tail l1 l2 -> exists l3, l2 = l3 ++ l1.
Proof.
induction 1 as [|x l1 l2]; simpl.
- exists nil; simpl; auto.
- destruct IHis_tail as (l3 & EQ); rewrite EQ.
exists (x::l3); simpl; auto.
Qed.
Lemma is_tail_bound A (l1 l2: list A):
is_tail l1 l2 -> (length l1 <= length l2)%nat.
Proof.
intros H; destruct (is_tail_app_def H) as (l3 & EQ).
subst; rewrite app_length.
omega.
Qed.
(** [list_forall2 P [x1 ... xN] [y1 ... yM]] holds iff [N = M] and
[P xi yi] holds for all [i]. *)
......
......@@ -94,3 +94,18 @@ Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_
Proof.
intros; rewrite list_length_z_nat, Nat2Z.id. auto.
Qed.
Lemma is_tail_list_nth_z A (l1 l2: list A):
is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0.
Proof.
induction 1; simpl.
- replace (list_length_z c - list_length_z c) with 0; omega || auto.
- assert (X: list_length_z (i :: c2) > list_length_z c1).
{ rewrite !list_length_z_nat, <- Nat2Z.inj_gt.
exploit is_tail_bound; simpl; eauto.
omega. }
destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega.
replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto.
rewrite list_length_z_cons.
omega.
Qed.
......@@ -190,7 +190,7 @@ Proof.
intros H H0 H1.
unfold find_label.
remember (is_label l _) as b.
cutrewrite (b = false); auto.
replace b with false; auto.
subst; unfold is_label.
destruct i; cbn in * |- *; try (destruct (in_dec l nil); intuition).
inversion H.
......@@ -286,7 +286,7 @@ Lemma find_label_preserved:
Mach.find_label l (Mach.fn_code f) = Some c ->
exists h, In l h /\ find_label l (fn_code (transf_function f)) = Some (concat h (trans_code c)).
Proof.
intros. cutrewrite ((fn_code (transf_function f)) = trans_code (Mach.fn_code f)); eauto.
intros. replace (fn_code (transf_function f)) with (trans_code (Mach.fn_code f)); eauto.
apply find_label_transcode_preserved; auto.
Qed.
......@@ -661,7 +661,7 @@ Proof.
inversion H1; subst; clear H1.
inversion_clear H0; cbn.
- (* function_internal*)
cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto.
replace (trans_code (Mach.fn_code f0)) with (fn_code (transf_function f0)); eauto.
eapply exec_function_internal; eauto.
rewrite <- parent_sp_preserved; eauto.
rewrite <- parent_ra_preserved; eauto.
......@@ -733,12 +733,12 @@ Proof.
intro H; destruct c as [|i' c]. { inversion H. }
remember (trans_inst i) as ti.
destruct ti as [lbl|bi|cfi].
- (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ).
- (*i=lbl *) replace (i ) with (Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ).
exists nil; cbn; eexists. eapply Tr_add_label; eauto.
- (*i=basic*)
destruct i'.
10: { exists (add_to_new_bblock (MB_basic bi)::nil). exists b.
cutrewrite ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_basic bi) :: (b::l)));eauto.
replace ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)) with ((add_to_new_bblock (MB_basic bi) :: (b::l)));eauto.
rewrite Heqti.
eapply Tr_end_block; eauto.
rewrite <-Heqti.
......@@ -748,7 +748,7 @@ Proof.
- (*i=cfi*)
destruct i; try(cbn in Heqti; congruence).
all: exists (add_to_new_bblock (MB_cfi cfi)::nil); exists b;
cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto;
replace ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)) with ((add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto;
rewrite Heqti;
eapply Tr_end_block; eauto;
rewrite <-Heqti;
......@@ -765,21 +765,6 @@ Proof.
eauto.
Qed.
(* FIXME: these two lemma should go into [Coqlib.v] *)
Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2).
Proof.
induction l1; cbn; auto with coqlib.
Qed.
Hint Resolve is_tail_app: coqlib.
Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3.
Proof.
induction l1; cbn; auto with coqlib.
intros l2 l3 H; inversion H; eauto with coqlib.
Qed.
Hint Resolve is_tail_app_inv: coqlib.
Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 ->
exists b, is_tail (b :: trans_code c) (trans_code c2).
Proof.
......
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