diff options
| -rw-r--r-- | aarch64/Asmgen.v | 22 | ||||
| -rw-r--r-- | aarch64/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | aarch64/Asmgenproof1.v | 52 | ||||
| -rw-r--r-- | arm/Asmgen.v | 3 | ||||
| -rw-r--r-- | arm/Asmgenproof1.v | 24 | ||||
| -rw-r--r-- | common/Values.v | 106 | ||||
| -rw-r--r-- | cparser/Elab.ml | 7 | ||||
| -rw-r--r-- | lib/Integers.v | 179 | ||||
| -rw-r--r-- | riscV/Asmgen.v | 30 | ||||
| -rw-r--r-- | riscV/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | riscV/Asmgenproof1.v | 45 | ||||
| -rw-r--r-- | x86/CBuiltins.ml | 3 |
12 files changed, 419 insertions, 60 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 0c72c7cc..46dd875d 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -268,18 +268,24 @@ Definition arith_extended Definition shrx32 (rd r1: ireg) (n: int) (k: code) : code := if Int.eq n Int.zero then Pmov rd r1 :: k - else - Porr W X16 XZR r1 (SOasr (Int.repr 31)) :: - Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) :: - Porr W rd XZR X16 (SOasr n) :: k. + else if Int.eq n Int.one then + Padd W X16 r1 r1 (SOlsr (Int.repr 31)) :: + Porr W rd XZR X16 (SOasr n) :: k + else + Porr W X16 XZR r1 (SOasr (Int.repr 31)) :: + Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) :: + Porr W rd XZR X16 (SOasr n) :: k. Definition shrx64 (rd r1: ireg) (n: int) (k: code) : code := if Int.eq n Int.zero then Pmov rd r1 :: k - else - Porr X X16 XZR r1 (SOasr (Int.repr 63)) :: - Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) :: - Porr X rd XZR X16 (SOasr n) :: k. + else if Int.eq n Int.one then + Padd X X16 r1 r1 (SOlsr (Int.repr 63)) :: + Porr X rd XZR X16 (SOasr n) :: k + else + Porr X X16 XZR r1 (SOasr (Int.repr 63)) :: + Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) :: + Porr X rd XZR X16 (SOasr n) :: k. (** Load the address [id + ofs] in [rd] *) diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index c860b961..88258cd6 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -259,13 +259,13 @@ Proof. - apply logicalimm32_label; unfold nolabel; auto. - apply logicalimm32_label; unfold nolabel; auto. - apply logicalimm32_label; unfold nolabel; auto. -- unfold shrx32. destruct Int.eq; TailNoLabel. +- unfold shrx32. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel. - apply arith_extended_label; unfold nolabel; auto. - apply arith_extended_label; unfold nolabel; auto. - apply logicalimm64_label; unfold nolabel; auto. - apply logicalimm64_label; unfold nolabel; auto. - apply logicalimm64_label; unfold nolabel; auto. -- unfold shrx64. destruct Int.eq; TailNoLabel. +- unfold shrx64. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel. - eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. - destruct (preg_of r); try discriminate; TailNoLabel; (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto | TailNoLabel]). diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v index b622a0bb..6f296f56 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmgenproof1.v @@ -754,16 +754,28 @@ Lemma exec_shrx32: forall (rd r1: ireg) (n: int) k v (rs: regset) m, /\ rs'#rd = v /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. - unfold shrx32; intros. apply Val.shrx_shr_2 in H. + unfold shrx32; intros. apply Val.shrx_shr_3 in H. destruct (Int.eq n Int.zero) eqn:E. - econstructor; split. apply exec_straight_one; [simpl;eauto|auto]. split. Simpl. subst v; auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto. - simpl; eauto. - unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto. - auto. auto. auto. - split. subst v; Simpl. intros; Simpl. +- generalize (Int.eq_spec n Int.one). + destruct (Int.eq n Int.one); intro ONE. + * subst n. + econstructor; split. eapply exec_straight_two. + all: simpl; auto. + split. + ** subst v; Simpl. + destruct (Val.add _ _); simpl; trivial. + change (Int.ltu Int.one Int.iwordsize) with true; simpl. + rewrite Int.or_zero_l. + reflexivity. + ** intros; Simpl. + * econstructor; split. eapply exec_straight_three. + unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto. + simpl; eauto. + unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto. + auto. auto. auto. + split. subst v; Simpl. intros; Simpl. Qed. Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m, @@ -774,16 +786,28 @@ Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m, /\ rs'#rd = v /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. - unfold shrx64; intros. apply Val.shrxl_shrl_2 in H. + unfold shrx64; intros. apply Val.shrxl_shrl_3 in H. destruct (Int.eq n Int.zero) eqn:E. - econstructor; split. apply exec_straight_one; [simpl;eauto|auto]. split. Simpl. subst v; auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto. - simpl; eauto. - unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto. - auto. auto. auto. - split. subst v; Simpl. intros; Simpl. +- generalize (Int.eq_spec n Int.one). + destruct (Int.eq n Int.one); intro ONE. + * subst n. + econstructor; split. eapply exec_straight_two. + all: simpl; auto. + split. + ** subst v; Simpl. + destruct (Val.addl _ _); simpl; trivial. + change (Int.ltu Int.one Int64.iwordsize') with true; simpl. + rewrite Int64.or_zero_l. + reflexivity. + ** intros; Simpl. + * econstructor; split. eapply exec_straight_three. + unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto. + simpl; eauto. + unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto. + auto. auto. auto. + split. subst v; Simpl. intros; Simpl. Qed. (** Condition bits *) diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 016a1c5a..f428feea 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -481,6 +481,9 @@ Definition transl_op do r <- ireg_of res; do r1 <- ireg_of a1; if Int.eq n Int.zero then OK (Pmov r (SOreg r1) :: k) + else if Int.eq n Int.one then + OK (Padd IR14 r1 (SOlsr r1 (Int.repr 31)) :: + Pmov r (SOasr IR14 n) :: k) else OK (Pmov IR14 (SOasr r1 (Int.repr 31)) :: Padd IR14 r1 (SOlsr IR14 (Int.sub Int.iwordsize n)) :: diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 7ef7b776..cdac697e 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -1264,15 +1264,32 @@ Local Transparent destroyed_by_op. destruct (rs x0) eqn: X0; simpl in H0; try discriminate. destruct (Int.ltu i (Int.repr 31)) eqn: LTU; inv H0. revert EQ2. predSpec Int.eq Int.eq_spec i Int.zero; intros EQ2. + { (* i = 0 *) inv EQ2. econstructor. split. apply exec_straight_one. simpl. reflexivity. auto. split. Simpl. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto. intros. Simpl. - (* i <> 0 *) - inv EQ2. - assert (LTU': Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize = true). + } + { (* i <> 0 *) + revert EQ2. predSpec Int.eq Int.eq_spec i Int.one; intros EQ2. + { + inv EQ2. + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. + { rewrite X0. + rewrite Int.shrx1_shr by reflexivity. + Simpl. + } + { intros. + Simpl. + } + } + clear H0. + inv EQ2. + assert (LTU': Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize = true). { generalize (Int.ltu_inv _ _ LTU). intros. unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. @@ -1306,6 +1323,7 @@ Local Transparent destroyed_by_op. rewrite LTU'; simpl. rewrite LTU''; simpl. f_equal. symmetry. apply Int.shrx_shr_2. assumption. intros. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. + } (* intoffloat *) econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. Transparent destroyed_by_op. diff --git a/common/Values.v b/common/Values.v index de317734..84030123 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1439,6 +1439,60 @@ Proof. assert (32 < Int.max_unsigned) by reflexivity. omega. Qed. +Theorem shrx1_shr: + forall x z, + shrx x (Vint (Int.repr 1)) = Some z -> + z = shr (add x (shru x (Vint (Int.repr 31)))) (Vint (Int.repr 1)). +Proof. + intros. destruct x; simpl in H; try discriminate. + change (Int.ltu (Int.repr 1) (Int.repr 31)) with true in H; simpl in H. + inversion_clear H. + simpl. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true; simpl. + change (Int.ltu (Int.repr 1) Int.iwordsize) with true; simpl. + f_equal. + rewrite Int.shrx1_shr by reflexivity. + reflexivity. +Qed. + +Theorem shrx_shr_3: + forall n x z, + shrx x (Vint n) = Some z -> + z = (if Int.eq n Int.zero then x else + if Int.eq n Int.one + then shr (add x (shru x (Vint (Int.repr 31)))) (Vint Int.one) + else shr (add x (shru (shr x (Vint (Int.repr 31))) + (Vint (Int.sub (Int.repr 32) n)))) + (Vint n)). +Proof. + intros. destruct x; simpl in H; try discriminate. + destruct (Int.ltu n (Int.repr 31)) eqn:LT; inv H. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31; intros LT'. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. change (Int.signed Int.one) with 1. + rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. +- predSpec Int.eq Int.eq_spec n Int.one. + * subst n. simpl. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + change (Int.ltu Int.one Int.iwordsize) with true. simpl. + f_equal. + apply Int.shrx1_shr. + reflexivity. + * clear H0. + simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl. + replace (Int.ltu n Int.iwordsize) with true. + f_equal; apply Int.shrx_shr_2; assumption. + symmetry; apply zlt_true. change (Int.unsigned n < 32); omega. + symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32. + assert (Int.unsigned n <> 0). + { red; intros; elim H. + rewrite <- (Int.repr_unsigned n), H0. auto. } + rewrite Int.unsigned_repr. + change (Int.unsigned Int.iwordsize) with 32; omega. + assert (32 < Int.max_unsigned) by reflexivity. omega. +Qed. + Theorem or_rolm: forall x n m1 m2, or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2). @@ -1698,6 +1752,58 @@ Proof. assert (64 < Int.max_unsigned) by reflexivity. omega. Qed. +Theorem shrxl1_shrl: + forall x z, + shrxl x (Vint (Int.repr 1)) = Some z -> + z = shrl (addl x (shrlu x (Vint (Int.repr 63)))) (Vint (Int.repr 1)). +Proof. + intros. destruct x; simpl in H; try discriminate. + change (Int.ltu (Int.repr 1) (Int.repr 63)) with true in H; simpl in H. + inversion_clear H. + simpl. + change (Int.ltu (Int.repr 63) Int64.iwordsize') with true; simpl. + change (Int.ltu (Int.repr 1) Int64.iwordsize') with true; simpl. + f_equal. + rewrite Int64.shrx'1_shr' by reflexivity. + reflexivity. +Qed. + +Theorem shrxl_shrl_3: + forall n x z, + shrxl x (Vint n) = Some z -> + z = (if Int.eq n Int.zero then x else + if Int.eq n Int.one + then shrl (addl x (shrlu x (Vint (Int.repr 63)))) (Vint Int.one) + else shrl (addl x (shrlu (shrl x (Vint (Int.repr 63))) + (Vint (Int.sub (Int.repr 64) n)))) + (Vint n)). +Proof. + intros. destruct x; simpl in H; try discriminate. + destruct (Int.ltu n (Int.repr 63)) eqn:LT; inv H. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63; intros LT'. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. unfold Int64.shrx'. rewrite Int64.shl'_zero. unfold Int64.divs. change (Int64.signed Int64.one) with 1. + rewrite Z.quot_1_r. rewrite Int64.repr_signed; auto. +- predSpec Int.eq Int.eq_spec n Int.one. + * subst n. simpl. + change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. + change (Int.ltu Int.one Int64.iwordsize') with true. simpl. + f_equal. + apply Int64.shrx'1_shr'. + reflexivity. + * clear H0. +simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. + replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl. + replace (Int.ltu n Int64.iwordsize') with true. + f_equal; apply Int64.shrx'_shr_2; assumption. + symmetry; apply zlt_true. change (Int.unsigned n < 64); omega. + symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64. + assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } + rewrite Int.unsigned_repr. + change (Int.unsigned Int64.iwordsize') with 64; omega. + assert (64 < Int.max_unsigned) by reflexivity. omega. +Qed. + Theorem negate_cmp_bool: forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y). Proof. diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 2b04340e..3dbb9d45 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1853,7 +1853,12 @@ let elab_expr ctx loc env a = having declared it *) match a1 with | VARIABLE n when not (Env.ident_is_bound env n) -> - warning Implicit_function_declaration "implicit declaration of function '%s' is invalid in C99" n; + let is_builtin = String.length n > 10 + && String.sub n 0 10 = "__builtin_" in + if is_builtin then + error "use of unknown builtin '%s'" n + else + warning Implicit_function_declaration "implicit declaration of function '%s' is invalid in C99" n; let ty = TFun(TInt(IInt, []), None, false, []) in (* Check against other definitions and enter in env *) let (id, sto, env, ty, linkage) = diff --git a/lib/Integers.v b/lib/Integers.v index bc05a4da..246c708c 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -4,7 +4,7 @@ (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) (* *) -(* Copyright Institut National de Recherche en Informatique et en *) +(* Copyright Institut National de Recherstestche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) (* under the terms of the GNU General Public License as published by *) (* the Free Software Foundation, either version 2 of the License, or *) @@ -1194,6 +1194,34 @@ Proof. rewrite <- half_modulus_modulus. apply unsigned_range. Qed. +Local Transparent repr. +Lemma sign_bit_of_signed: forall x, + (testbit x (zwordsize - 1)) = lt x zero. +Proof. + intro. + rewrite sign_bit_of_unsigned. + unfold lt. + unfold signed, unsigned. + simpl. + pose proof half_modulus_pos as HMOD. + destruct (zlt 0 half_modulus) as [HMOD' | HMOD']. + 2: omega. + clear HMOD'. + destruct (zlt (intval x) half_modulus) as [ LOW | HIGH]. + { + destruct x as [ix RANGE]. + simpl in *. + destruct (zlt ix 0). omega. + reflexivity. + } + destruct (zlt _ _) as [LOW' | HIGH']; trivial. + destruct x as [ix RANGE]. + simpl in *. + rewrite half_modulus_modulus in *. + omega. +Qed. +Local Opaque repr. + Lemma bits_signed: forall x i, 0 <= i -> Z.testbit (signed x) i = testbit x (if zlt i zwordsize then i else zwordsize - 1). @@ -2427,6 +2455,57 @@ Proof. bit_solve. destruct (zlt (i + unsigned (sub iwordsize y)) zwordsize); auto. Qed. +Theorem shrx1_shr: + forall x, + ltu one (repr (zwordsize - 1)) = true -> + shrx x (repr 1) = shr (add x (shru x (repr (zwordsize - 1)))) (repr 1). +Proof. + intros. + rewrite shrx_shr by assumption. + rewrite shl_mul_two_p. + rewrite mul_commut. rewrite mul_one. + change (repr 1) with one. + rewrite unsigned_one. + change (two_p 1) with 2. + unfold sub. + rewrite unsigned_one. + assert (0 <= 2 <= max_unsigned). + { + unfold max_unsigned, modulus. + unfold zwordsize in *. + unfold ltu in *. + rewrite unsigned_one in H. + rewrite unsigned_repr in H. + { + destruct (zlt 1 (Z.of_nat wordsize - 1)) as [ LT | NONE]. + 2: discriminate. + clear H. + rewrite two_power_nat_two_p. + split. + omega. + set (w := (Z.of_nat wordsize)) in *. + assert ((two_p 2) <= (two_p w)) as MONO. + { + apply two_p_monotone. + omega. + } + change (two_p 2) with 4 in MONO. + omega. + } + generalize wordsize_max_unsigned. + fold zwordsize. + generalize wordsize_pos. + omega. + } + rewrite unsigned_repr by assumption. + simpl. + rewrite shru_lt_zero. + destruct (lt x zero). + reflexivity. + rewrite add_zero. + reflexivity. +Qed. + Theorem shrx_carry: forall x y, ltu y (repr (zwordsize - 1)) = true -> @@ -3593,6 +3672,104 @@ Proof. unfold ltu. apply zlt_true. change (unsigned z < 63). rewrite A; omega. Qed. +Lemma shr'63: + forall x, (shr' x (Int.repr 63)) = if lt x zero then mone else zero. +Proof. + intro. + unfold shr', mone, zero. + rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; omega). + apply same_bits_eq. + intros i BIT. + rewrite testbit_repr by assumption. + rewrite Z.shiftr_spec by omega. + rewrite bits_signed by omega. + simpl. + change zwordsize with 64 in *. + destruct (zlt _ _) as [LT | GE]. + { + replace i with 0 in * by omega. + change (0 + 63) with (zwordsize - 1). + rewrite sign_bit_of_signed. + destruct (lt x _). + all: rewrite testbit_repr by (change zwordsize with 64 in *; omega). + all: simpl; reflexivity. + } + change (64 - 1) with (zwordsize - 1). + rewrite sign_bit_of_signed. + destruct (lt x _). + all: rewrite testbit_repr by (change zwordsize with 64 in *; omega). + { symmetry. + apply Ztestbit_m1. + tauto. + } + symmetry. + apply Ztestbit_0. +Qed. + +Lemma shru'63: + forall x, (shru' x (Int.repr 63)) = if lt x zero then one else zero. +Proof. + intro. + unfold shru'. + rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; omega). + apply same_bits_eq. + intros i BIT. + rewrite testbit_repr by assumption. + rewrite Z.shiftr_spec by omega. + unfold lt. + rewrite signed_zero. + unfold one, zero. + destruct (zlt _ 0) as [LT | GE]. + { + rewrite testbit_repr by assumption. + destruct (zeq i 0) as [IZERO | INONZERO]. + { subst i. + change (Z.testbit (unsigned x) (0 + 63)) with (testbit x (zwordsize - 1)). + rewrite sign_bit_of_signed. + unfold lt. + rewrite signed_zero. + destruct (zlt _ _); try omega. + reflexivity. + } + change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i+63)). + rewrite bits_above by (change zwordsize with 64; omega). + rewrite Ztestbit_1. + destruct (zeq i 0); trivial. + subst i. + omega. + } + destruct (zeq i 0) as [IZERO | INONZERO]. + { subst i. + change (Z.testbit (unsigned x) (0 + 63)) with (testbit x (zwordsize - 1)). + rewrite sign_bit_of_signed. + unfold lt. + rewrite signed_zero. + rewrite bits_zero. + destruct (zlt _ _); try omega. + reflexivity. + } + change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i + 63)). + rewrite bits_zero. + apply bits_above. + change zwordsize with 64. + omega. +Qed. + +Theorem shrx'1_shr': + forall x, + Int.ltu Int.one (Int.repr (zwordsize - 1)) = true -> + shrx' x (Int.repr 1) = shr' (add x (shru' x (Int.repr (Int64.zwordsize - 1)))) (Int.repr 1). +Proof. + intros. + rewrite shrx'_shr_2 by reflexivity. + change (Int.sub (Int.repr 64) (Int.repr 1)) with (Int.repr 63). + f_equal. f_equal. + rewrite shr'63. + rewrite shru'63. + rewrite shru'63. + destruct (lt x zero); reflexivity. +Qed. + Remark int_ltu_2_inv: forall y z, Int.ltu y iwordsize' = true -> diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 0fa47fca..b431d63d 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -505,11 +505,16 @@ Definition transl_op OK (Psrliw rd rs n :: k) | Oshrximm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psraiw X31 rs (Int.repr 31) :: - Psrliw X31 X31 (Int.sub Int.iwordsize n) :: - Paddw X31 rs X31 :: - Psraiw rd X31 n :: k) + OK (if Int.eq n Int.zero + then Pmv rd rs :: k + else if Int.eq n Int.one + then Psrliw X31 rs (Int.repr 31) :: + Paddw X31 rs X31 :: + Psraiw rd X31 Int.one :: k + else Psraiw X31 rs (Int.repr 31) :: + Psrliw X31 X31 (Int.sub Int.iwordsize n) :: + Paddw X31 rs X31 :: + Psraiw rd X31 n :: k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => @@ -594,11 +599,16 @@ Definition transl_op OK (Psrlil rd rs n :: k) | Oshrxlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psrail X31 rs (Int.repr 63) :: - Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: - Paddl X31 rs X31 :: - Psrail rd X31 n :: k) + OK (if Int.eq n Int.zero + then Pmv rd rs :: k + else if Int.eq n Int.one + then Psrlil X31 rs (Int.repr 63) :: + Paddl X31 rs X31 :: + Psrail rd X31 Int.one :: k + else Psrail X31 rs (Int.repr 63) :: + Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: + Paddl X31 rs X31 :: + Psrail rd X31 n :: k) | Onegf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index e2fafb16..8e9f022c 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -285,12 +285,12 @@ Opaque Int.eq. - apply opimm32_label; intros; exact I. - apply opimm32_label; intros; exact I. - apply opimm32_label; intros; exact I. -- destruct (Int.eq n Int.zero); TailNoLabel. +- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. -- destruct (Int.eq n Int.zero); TailNoLabel. +- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. - eapply transl_cond_op_label; eauto. Qed. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 54a86ae7..8678a5dc 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1035,17 +1035,23 @@ Opaque Int.eq. intros (rs' & A & B & C). exists rs'; split; eauto. rewrite B; auto with asmgen. - (* shrximm *) - clear H. exploit Val.shrx_shr_2; eauto. intros E; subst v; clear EV. + clear H. exploit Val.shrx_shr_3; eauto. intros E; subst v; clear EV. destruct (Int.eq n Int.zero). + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. -+ change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. ++ destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. - (* longofintu *) econstructor; split. eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto. @@ -1070,17 +1076,24 @@ Opaque Int.eq. intros (rs' & A & B & C). exists rs'; split; eauto. rewrite B; auto with asmgen. - (* shrxlimm *) - clear H. exploit Val.shrxl_shrl_2; eauto. intros E; subst v; clear EV. + clear H. exploit Val.shrxl_shrl_3; eauto. intros E; subst v; clear EV. destruct (Int.eq n Int.zero). + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. -+ change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. ++ destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + + * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. - (* cond *) exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml index f4f40a31..e7f714c7 100644 --- a/x86/CBuiltins.ml +++ b/x86/CBuiltins.ml @@ -73,9 +73,6 @@ let builtins = { (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false); "__builtin_write32_reversed", (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false); - (* no operation *) - "__builtin_nop", - (TVoid [], [], false); ] } |