diff options
Diffstat (limited to 'riscV/SelectOpproof.v')
| -rw-r--r-- | riscV/SelectOpproof.v | 122 |
1 files changed, 120 insertions, 2 deletions
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 1d13702a..ce80fc57 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -24,6 +24,7 @@ Require Import Cminor Op CminorSel. Require Import SelectOp. Require Import OpHelpers. Require Import OpHelpersproof. +Require Import Lia. Local Open Scope cminorsel_scope. @@ -875,6 +876,71 @@ Proof. red; intros. unfold floatofsingle. TrivialExists. Qed. +Lemma mod_small_negative: + forall a modulus, + modulus > 0 -> -modulus < a < 0 -> a mod modulus = a + modulus. +Proof. + intros. + replace (a mod modulus) with ((a + modulus) mod modulus). + apply Z.mod_small. + lia. + rewrite <- Zplus_mod_idemp_r. + rewrite Z.mod_same by lia. + rewrite Z.add_0_r. + reflexivity. +Qed. + +Remark normalize_low_long: forall + (PTR64 : Archi.ptr64 = true) v1, + Val.loword (Val.normalize (Val.longofint v1) Tlong) = Val.normalize v1 Tint. +Proof. + intros. + destruct v1; cbn; try rewrite PTR64; trivial. + f_equal. + unfold Int64.loword. + unfold Int.signed. + destruct zlt. + { rewrite Int64.int_unsigned_repr. + apply Int.repr_unsigned. + } + pose proof (Int.unsigned_range i). + rewrite Int64.unsigned_repr_eq. + replace ((Int.unsigned i - Int.modulus) mod Int64.modulus) + with (Int64.modulus + Int.unsigned i - Int.modulus). + { + rewrite <- (Int.repr_unsigned i) at 2. + apply Int.eqm_samerepr. + unfold Int.eqm, eqmod. + change Int.modulus with 4294967296 in *. + change Int64.modulus with 18446744073709551616 in *. + exists 4294967295. + lia. + } + { rewrite mod_small_negative. + lia. + constructor. + constructor. + change Int.modulus with 4294967296 in *. + change Int.half_modulus with 2147483648 in *. + change Int64.modulus with 18446744073709551616 in *. + lia. + lia. + } +Qed. + +Lemma same_expr_pure_correct: + forall le a1 a2 v1 v2 + (PURE : same_expr_pure a1 a2 = true) + (EVAL1 : eval_expr ge sp e m le a1 v1) + (EVAL2 : eval_expr ge sp e m le a2 v2), + v1 = v2. +Proof. + intros. + destruct a1; destruct a2; cbn in *; try discriminate. + inv EVAL1. inv EVAL2. + destruct (ident_eq i i0); congruence. +Qed. + Theorem eval_select: forall le ty cond al vl a1 v1 a2 v2 a b, select ty cond al a1 a2 = Some a -> @@ -886,7 +952,56 @@ Theorem eval_select: eval_expr ge sp e m le a v /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v. Proof. - unfold select; intros; discriminate. + unfold select; intros. + pose proof (same_expr_pure_correct le a1 a2 v1 v2) as PURE. + destruct (same_expr_pure a1 a2). + { rewrite <- PURE by auto. + inv H. + exists v1. split. assumption. + unfold Val.select. + destruct b; apply Val.lessdef_normalize. + } + clear PURE. + destruct Archi.ptr64 eqn:PTR64. + 2: discriminate. + destruct ty; cbn in *; try discriminate. + - (* Tint *) + inv H. TrivialExists. + + cbn. repeat econstructor; eassumption. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + rewrite H3. destruct b. + * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption. + * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption. + + - (* Tfloat *) + inv H. TrivialExists. + + cbn. repeat econstructor; eassumption. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + rewrite H3. destruct b. + * rewrite ExtValues.select01_long_true. + apply ExtValues.float_bits_normalize. + * rewrite ExtValues.select01_long_false. + apply ExtValues.float_bits_normalize. + + - (* Tlong *) + inv H. TrivialExists. + + cbn. repeat econstructor; eassumption. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + rewrite H3. destruct b. + * rewrite ExtValues.select01_long_true. reflexivity. + * rewrite ExtValues.select01_long_false. reflexivity. + + - (* Tsingle *) + inv H. TrivialExists. + + cbn. repeat econstructor; eassumption. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + rewrite H3. destruct b. + * rewrite ExtValues.select01_long_true. + rewrite normalize_low_long by assumption. + apply ExtValues.single_bits_normalize. + * rewrite ExtValues.select01_long_false. + rewrite normalize_low_long by assumption. + apply ExtValues.single_bits_normalize. Qed. Theorem eval_addressing: @@ -969,7 +1084,10 @@ Theorem eval_platform_builtin: platform_builtin_sem bf vl = Some v -> exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. Proof. - intros. discriminate. + destruct bf; intros until le; intro Heval. + all: try (inversion Heval; subst a; clear Heval; + exists v; split; trivial; + repeat (try econstructor; try eassumption)). Qed. End CMCONSTR. |