From 613848182d167782fa5ee383b0e73b87e5ef1351 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 17 Sep 2021 14:54:49 +0200 Subject: Select condition x < 0 with x unsigned leads to false Squashed commit of the following: commit 808e72db2022d05a4e34818b33cc9af17aaa4df0 Author: David Monniaux Date: Fri Sep 17 14:53:39 2021 +0200 selectOp for comp0 commit f38e1f15359cceb3c0764635336125a1ceae78ff Author: David Monniaux Date: Fri Sep 17 14:49:45 2021 +0200 SelectOp for ccomp0 ok commit ca969280380a593aef590a1fe2ec6f0fc112c2f5 Author: David Monniaux Date: Fri Sep 17 14:46:01 2021 +0200 progress commit e60a970f541ae6be30ec51cf95d60eb672ade829 Author: David Monniaux Date: Fri Sep 17 14:40:49 2021 +0200 progres sur ltu etc. commit 6f7d51e59a61d43fca06b1b4bad6dedada6e031e Author: David Monniaux Date: Fri Sep 17 14:13:07 2021 +0200 change selection commit c2af349c6dd3e09fec25f3a96e1272377b6450ef Author: David Monniaux Date: Fri Sep 17 14:03:31 2021 +0200 begin rewrite selector --- kvx/SelectOpproof.v | 108 ++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 105 insertions(+), 3 deletions(-) (limited to 'kvx/SelectOpproof.v') diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index a7169881..45aa3343 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1533,6 +1533,70 @@ Proof. apply Val.swap_cmplu_bool. Qed. +Lemma int_ltu_zero : forall i, Int.ltu i Int.zero = false. +Proof. + intro. + unfold Int.ltu. + apply zlt_false. + rewrite Int.unsigned_zero. + pose proof (Int.unsigned_range i). + lia. +Qed. + +Lemma cmpu_bool_Clt : forall pred v0 b, + Val.cmpu_bool pred Clt v0 (Vint Int.zero) = Some b -> b = false. +Proof. + intros until b. intro CMP. + destruct v0; cbn in CMP; try discriminate. + inv CMP. + apply int_ltu_zero. +Qed. + +Lemma cmpu_bool_Cge : forall pred v0 b, + Val.cmpu_bool pred Cge v0 (Vint Int.zero) = Some b -> b = true. +Proof. + intros until b. intro CMP. + destruct v0; cbn in CMP; try discriminate. + inv CMP. + rewrite int_ltu_zero. + reflexivity. +Qed. + +Lemma int64_ltu_zero : forall i, Int64.ltu i Int64.zero = false. +Proof. + intro. + unfold Int64.ltu. + apply zlt_false. + rewrite Int64.unsigned_zero. + pose proof (Int64.unsigned_range i). + lia. +Qed. + +Lemma cmplu_bool_Clt : forall pred v0 b, + Val.cmplu_bool pred Clt v0 (Vlong Int64.zero) = Some b -> b = false. +Proof. + intros until b. intro CMP. + destruct v0; cbn in CMP; try discriminate. + { inv CMP. + apply int64_ltu_zero. + } + repeat rewrite if_same in CMP. + discriminate. +Qed. + +Lemma cmplu_bool_Cge : forall pred v0 b, + Val.cmplu_bool pred Cge v0 (Vlong Int64.zero) = Some b -> b = true. +Proof. + intros until b. intro CMP. + destruct v0; cbn in CMP; try discriminate. + { inv CMP. + rewrite int64_ltu_zero. + reflexivity. + } + repeat rewrite if_same in CMP. + discriminate. +Qed. + Theorem eval_select: forall le ty cond al vl a1 v1 a2 v2 a b, select ty cond al a1 a2 = Some a -> @@ -1581,8 +1645,27 @@ Proof. simpl. change (Val.cmpu_bool (Mem.valid_pointer m) c v0 (Vint Int.zero)) with (eval_condition0 (Ccompu0 c) v0 m). - eapply eval_select0; eassumption. - } + destruct c. + all: try (eapply eval_select0; eassumption). + all: cbn. + all: cbn in HeC. + { + destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt v0 (Vint Int.zero)) eqn:CMP; try discriminate. + inv HeC. + rewrite (cmpu_bool_Clt (Mem.valid_pointer m) v0 b CMP). + cbn. + exists v2. + split; auto using Val.lessdef_normalize. + } + { + destruct (Val.cmpu_bool (Mem.valid_pointer m) Cge v0 (Vint Int.zero)) eqn:CMP; try discriminate. + inv HeC. + rewrite (cmpu_bool_Cge (Mem.valid_pointer m) v0 b CMP). + cbn. + exists v1. + split; auto using Val.lessdef_normalize. + } + } simpl. erewrite <- (bool_cond0_ne (Val.cmpu_bool (Mem.valid_pointer m) c v0 (Vint x))). eapply eval_select0; repeat (try econstructor; try eassumption). @@ -1609,7 +1692,26 @@ Proof. simpl. change (Val.cmplu_bool (Mem.valid_pointer m) c v0 (Vlong Int64.zero)) with (eval_condition0 (Ccomplu0 c) v0 m). - eapply eval_select0; eassumption. + destruct c. + all: try (eapply eval_select0; eassumption). + all: cbn. + all: cbn in HeC. + { + destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt v0 (Vlong Int64.zero)) eqn:CMP; try discriminate. + inv HeC. + rewrite (cmplu_bool_Clt (Mem.valid_pointer m) v0 b CMP). + cbn. + exists v2. + split; auto using Val.lessdef_normalize. + } + { + destruct (Val.cmplu_bool (Mem.valid_pointer m) Cge v0 (Vlong Int64.zero)) eqn:CMP; try discriminate. + inv HeC. + rewrite (cmplu_bool_Cge (Mem.valid_pointer m) v0 b CMP). + cbn. + exists v1. + split; auto using Val.lessdef_normalize. + } } simpl. erewrite <- (bool_cond0_ne (Val.cmplu_bool (Mem.valid_pointer m) c v0 (Vlong x))). -- cgit