Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 9a0bf569 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

fix riscv merge?

parent f2e69135
......@@ -256,17 +256,10 @@ Inductive instruction : Type :=
(* floating point register move *)
| Pfmv (rd: freg) (rs: freg) (**r move *)
<<<<<<< HEAD
| Pfmvxs (rd: ireg) (rs: freg) (**r bitwise move FP single to integer register *)
| Pfmvxd (rd: ireg) (rs: freg) (**r bitwise move FP double to integer register *)
| Pfmvsx (rd: freg) (rs: ireg) (**r bitwise move integer register to FP single *)
| Pfmvdx (rd: freg) (rs: ireg) (**r bitwise move integer register to FP double*)
=======
| Pfmvxs (rd: ireg) (rs: freg) (**r move FP single to integer register *)
| Pfmvsx (rd: freg) (rs: ireg) (**r move integer register to FP single *)
| Pfmvxd (rd: ireg) (rs: freg) (**r move FP double to integer register *)
| Pfmvdx (rd: freg) (rs: ireg) (**r move integer register to FP double *)
>>>>>>> master
(* 32-bit (single-precision) floating point *)
| Pfls (rd: freg) (ra: ireg) (ofs: offset) (**r load float *)
......@@ -994,14 +987,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
so we do not model them. *)
| Pfence
<<<<<<< HEAD
=======
| Pfmvxs _ _
| Pfmvsx _ _
| Pfmvxd _ _
| Pfmvdx _ _
>>>>>>> master
| Pfmins _ _ _
| Pfmaxs _ _ _
| Pfsqrts _ _
......
......@@ -432,408 +432,6 @@ Proof.
intros; Simpl.
Qed.
<<<<<<< HEAD
=======
(** Translation of condition operators *)
Lemma transl_cond_int32s_correct:
forall cmp rd r1 r2 k rs m,
exists rs',
exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m
/\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
intros. destruct cmp; simpl.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl.
- econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool.
simpl. rewrite (Val.negate_cmp_bool Clt).
destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto.
- econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt).
destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto.
Qed.
Lemma transl_cond_int32u_correct:
forall cmp rd r1 r2 k rs m,
exists rs',
exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m
/\ rs'#rd = Val.cmpu (Mem.valid_pointer m) 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|auto].
split; intros; Simpl.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl.
- econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool.
simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle).
destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto.
- econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt).
destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto.
Qed.
Lemma transl_cond_int64s_correct:
forall cmp rd r1 r2 k rs m,
exists rs',
exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m
/\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd
/\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.
Proof.
intros. destruct cmp; simpl.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl.
- econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool.
simpl. rewrite (Val.negate_cmpl_bool Clt).
destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto.
- econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt).
destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto.
Qed.
Lemma transl_cond_int64u_correct:
forall cmp rd r1 r2 k rs m,
exists rs',
exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m
/\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) 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|auto].
split; intros; Simpl.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl.
- econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool.
simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle).
destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto.
- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto.
- econstructor; split.
eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto.
split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt).
destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto.
Qed.
Lemma transl_condimm_int32s_correct:
forall cmp rd r1 n k rs m,
r1 <> X31 ->
exists rs',
exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m
/\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
intros. unfold transl_condimm_int32s.
predSpec Int.eq Int.eq_spec n Int.zero.
- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C).
exists rs'; eauto.
- assert (DFL:
exists rs',
exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m
/\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
{ exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
exists rs2; split.
eapply exec_straight_trans. eexact A1. eexact A2.
split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
intros; transitivity (rs1 r); auto. }
destruct cmp.
+ unfold xorimm32.
exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
exists rs2; split.
eapply exec_straight_trans. eexact A1. eexact A2.
split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
intros; transitivity (rs1 r); auto.
+ unfold xorimm32.
exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
exists rs2; split.
eapply exec_straight_trans. eexact A1. eexact A2.
split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
intros; transitivity (rs1 r); auto.
+ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
+ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed).
* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
exists rs1; split. eexact A1. split; auto.
unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1.
unfold Int.lt. rewrite zlt_false. auto.
change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed.
generalize (Int.signed_range i); lia.
* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
exists rs1; split. eexact A1. split; auto.
rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto.
unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
destruct (zlt (Int.signed n) (Int.signed i)).
rewrite zlt_false by lia. auto.
rewrite zlt_true by lia. auto.
rewrite Int.add_signed. symmetry; apply Int.signed_repr.
assert (Int.signed n <> Int.max_signed).
{ red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. }
generalize (Int.signed_range n); lia.
+ apply DFL.
+ apply DFL.
Qed.
Lemma transl_condimm_int32u_correct:
forall cmp rd r1 n k rs m,
r1 <> X31 ->
exists rs',
exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m
/\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
intros. unfold transl_condimm_int32u.
predSpec Int.eq Int.eq_spec n Int.zero.
- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C).
exists rs'; split. eexact A. split; auto. rewrite B; auto.
- assert (DFL:
exists rs',
exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m
/\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
{ exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2).
exists rs2; split.
eapply exec_straight_trans. eexact A1. eexact A2.
split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
intros; transitivity (rs1 r); auto. }
destruct cmp.
+ apply DFL.
+ apply DFL.
+ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto.
intros (rs1 & A1 & B1 & C1).
exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
+ apply DFL.
+ apply DFL.
+ apply DFL.
Qed.
Lemma transl_condimm_int64s_correct:
forall cmp rd r1 n k rs m,
r1 <> X31 ->
exists rs',
exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m
/\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
intros. unfold transl_condimm_int64s.
predSpec Int64.eq Int64.eq_spec n Int64.zero.
- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C).
exists rs'; eauto.
- assert (DFL:
exists rs',
exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m
/\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
{ exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
exists rs2; split.
eapply exec_straight_trans. eexact A1. eexact A2.
split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
intros; transitivity (rs1 r); auto. }
destruct cmp.
+ unfold xorimm64.
exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
exists rs2; split.
eapply exec_straight_trans. eexact A1. eexact A2.
split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
intros; transitivity (rs1 r); auto.
+ unfold xorimm64.
exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
exists rs2; split.
eapply exec_straight_trans. eexact A1. eexact A2.
split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
intros; transitivity (rs1 r); auto.
+ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
+ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed).
* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
exists rs1; split. eexact A1. split; auto.
unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1.
unfold Int64.lt. rewrite zlt_false. auto.
change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed.
generalize (Int64.signed_range i); lia.
* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
exists rs1; split. eexact A1. split; auto.
rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto.
unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
destruct (zlt (Int64.signed n) (Int64.signed i)).
rewrite zlt_false by lia. auto.
rewrite zlt_true by lia. auto.
rewrite Int64.add_signed. symmetry; apply Int64.signed_repr.
assert (Int64.signed n <> Int64.max_signed).
{ red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
generalize (Int64.signed_range n); lia.
+ apply DFL.
+ apply DFL.
Qed.
Lemma transl_condimm_int64u_correct:
forall cmp rd r1 n k rs m,
r1 <> X31 ->
exists rs',
exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m
/\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
intros. unfold transl_condimm_int64u.
predSpec Int64.eq Int64.eq_spec n Int64.zero.
- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C).
exists rs'; split. eexact A. split; auto. rewrite B; auto.
- assert (DFL:
exists rs',
exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m
/\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
{ exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2).
exists rs2; split.
eapply exec_straight_trans. eexact A1. eexact A2.
split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
intros; transitivity (rs1 r); auto. }
destruct cmp.
+ apply DFL.
+ apply DFL.
+ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto.
intros (rs1 & A1 & B1 & C1).
exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
+ apply DFL.
+ apply DFL.
+ apply DFL.
Qed.
Lemma transl_cond_op_correct:
forall cond rd args k c rs m,
transl_cond_op cond rd args k = OK c ->
exists rs',
exec_straight ge fn c rs m k rs' m
/\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd
/\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
Proof.
assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)).
{ destruct ob as [[]|]; reflexivity. }
intros until m; intros TR.
destruct cond; simpl in TR; ArgsInv.
+ (* cmp *)
exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
+ (* cmpu *)
exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C).
exists rs'; repeat split; eauto. rewrite B; auto.
+ (* cmpimm *)
apply transl_condimm_int32s_correct; eauto with asmgen.
+ (* cmpuimm *)
apply transl_condimm_int32u_correct; eauto with asmgen.
+ (* cmpl *)
exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C).
exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
+ (* cmplu *)
exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C).
exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
+ (* cmplimm *)
exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen.
intros (rs' & A & B & C).
exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
+ (* cmpluimm *)
exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen.
intros (rs' & A & B & C).
exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
+ (* cmpf *)
destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
fold (Val.cmpf c0 (rs x) (rs x0)).
set (v := Val.cmpf c0 (rs x) (rs x0)).
destruct normal; inv EQ2.
* econstructor; split.
apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
split; intros; Simpl.
* econstructor; split.
eapply exec_straight_two.
eapply transl_cond_float_correct with (v := Val.notbool v); eauto.
simpl; reflexivity.
auto. auto.
split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
+ (* notcmpf *)
destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)).
set (v := Val.cmpf c0 (rs x) (rs x0)).
destruct normal; inv EQ2.
* econstructor; split.
eapply exec_straight_two.
eapply transl_cond_float_correct with (v := v); eauto.
simpl; reflexivity.
auto. auto.
split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
* econstructor; split.
apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto.
split; intros; Simpl.
+ (* cmpfs *)
destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
fold (Val.cmpfs c0 (rs x) (rs x0)).
set (v := Val.cmpfs c0 (rs x) (rs x0)).
destruct normal; inv EQ2.
* econstructor; split.
apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
split; intros; Simpl.
* econstructor; split.
eapply exec_straight_two.
eapply transl_cond_single_correct with (v := Val.notbool v); eauto.
simpl; reflexivity.
auto. auto.
split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
+ (* notcmpfs *)
destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)).
set (v := Val.cmpfs c0 (rs x) (rs x0)).
destruct normal; inv EQ2.
* econstructor; split.
eapply exec_straight_two.
eapply transl_cond_single_correct with (v := v); eauto.
simpl; reflexivity.
auto. auto.
split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
* econstructor; split.
apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
split; intros; Simpl.
Qed.
>>>>>>> master
(** Some arithmetic properties. *)
Remark cast32unsigned_from_cast32signed:
......
......@@ -506,39 +506,9 @@ Proof.
- subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto.
change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto.
- TrivialExists.
<<<<<<< HEAD
cbn.
rewrite H0.
reflexivity.
=======
(*
intros. unfold shrxlimm. destruct Archi.splitlong eqn:SL.
+ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32.
+ destruct x; simpl in H0; try discriminate.
destruct (Int.ltu n (Int.repr 63)) eqn:LTU; inv H0.
predSpec Int.eq Int.eq_spec n Int.zero.
- subst n. exists (Vlong i); split; auto. rewrite Int64.shrx'_zero. auto.
- assert (NZ: Int.unsigned n <> 0).
{ intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
assert (LT: 0 <= Int.unsigned n < 63) by (apply Int.ltu_inv in LTU; assumption).
assert (LTU2: Int.ltu (Int.sub Int64.iwordsize' n) Int64.iwordsize' = true).
{ unfold Int.ltu; apply zlt_true.
unfold Int.sub. change (Int.unsigned Int64.iwordsize') with 64.
rewrite Int.unsigned_repr. lia.
assert (64 < Int.max_unsigned) by reflexivity. lia. }
assert (X: eval_expr ge sp e m le
(Eop (Oshrlimm (Int.repr (Int64.zwordsize - 1))) (a ::: Enil))
(Vlong (Int64.shr' i (Int.repr (Int64.zwordsize - 1))))).
{ EvalOp. }
assert (Y: eval_expr ge sp e m le (shrxlimm_inner a n)
(Vlong (Int64.shru' (Int64.shr' i (Int.repr (Int64.zwordsize - 1))) (Int.sub Int64.iwordsize' n)))).
{ EvalOp. simpl. rewrite LTU2. auto. }
TrivialExists.
constructor. EvalOp. simpl; eauto. constructor.
simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int64.shrx'_shr_2 by auto. reflexivity.
change (Int.unsigned Int64.iwordsize') with 64; lia.
*)
>>>>>>> master
Qed.
Theorem eval_cmplu:
......
......@@ -574,43 +574,12 @@ Proof.
replace (Int.shrx i Int.zero) with i. auto.
unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
<<<<<<< HEAD
econstructor; split. EvalOp.
cbn.
rewrite H0.
cbn.
reflexivity.
apply Val.lessdef_refl.
=======
econstructor; split. EvalOp. auto.
(*
intros. destruct x; simpl in H0; try discriminate.
destruct (Int.ltu n (Int.repr 31)) eqn:LTU; inv H0.
unfold shrximm.
predSpec Int.eq Int.eq_spec n Int.zero.
- subst n. exists (Vint i); split; auto.
unfold Int.shrx, Int.divs. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto.
- assert (NZ: Int.unsigned n <> 0).
{ intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
assert (LT: 0 <= Int.unsigned n < 31) by (apply Int.ltu_inv in LTU; assumption).
assert (LTU2: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true).
{ unfold Int.ltu; apply zlt_true.
unfold Int.sub. change (Int.unsigned Int.iwordsize) with 32.
rewrite Int.unsigned_repr. lia.
assert (32 < Int.max_unsigned) by reflexivity. lia. }
assert (X: eval_expr ge sp e m le
(Eop (Oshrimm (Int.repr (Int.zwordsize - 1))) (a ::: Enil))
(Vint (Int.shr i (Int.repr (Int.zwordsize - 1))))).
{ EvalOp. }
assert (Y: eval_expr ge sp e m le (shrximm_inner a n)
(Vint (Int.shru (Int.shr i (Int.repr (Int.zwordsize - 1))) (Int.sub Int.iwordsize n)))).
{ EvalOp. simpl. rewrite LTU2. auto. }
TrivialExists.
constructor. EvalOp. simpl; eauto. constructor.
simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int.shrx_shr_2 by auto. reflexivity.
change (Int.unsigned Int.iwordsize) with 32; lia.
*)
>>>>>>> master
Qed.
Theorem eval_shl: binary_constructor_sound shl Val.shl.
......
......@@ -107,15 +107,10 @@ module Target : TARGET =
let name_of_section = function
| Section_text -> ".text"
<<<<<<< HEAD
| Section_data(i, true) ->
failwith "_Thread_local unsupported on this platform"
| Section_data(i, false) | Section_small_data i ->
if i then ".data" else common_section ()
=======
| Section_data i | Section_small_data i ->
variable_section ~sec:".data" ~bss:".bss" i
>>>>>>> master
| Section_const i | Section_small_const i ->
variable_section ~sec:".section .rodata" i
| Section_string -> ".section .rodata"
......@@ -403,11 +398,6 @@ module Target : TARGET =
fprintf oc " fmv.s.x %a, %a\n" freg fd ireg rs
| Pfmvxd (rd,fs) ->
fprintf oc " fmv.x.d %a, %a\n" ireg rd freg fs
<<<<<<< HEAD
| Pfmvsx (fd,rs) ->
fprintf oc " fmv.s.x %a, %a\n" freg fd ireg rs