diff options
author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-17 14:54:49 +0200 |
---|---|---|
committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-17 14:54:49 +0200 |
commit | 613848182d167782fa5ee383b0e73b87e5ef1351 (patch) | |
tree | 4745d5acd821e604d82510ebbc097863a271a10f | |
parent | 81a2cfe0971ca2456ff04c1e661b9a56279728ac (diff) | |
download | compcert-kvx-613848182d167782fa5ee383b0e73b87e5ef1351.tar.gz compcert-kvx-613848182d167782fa5ee383b0e73b87e5ef1351.zip |
Select condition x < 0 with x unsigned leads to falsev3.9_kvx_fix1
Squashed commit of the following:
commit 808e72db2022d05a4e34818b33cc9af17aaa4df0
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:53:39 2021 +0200
selectOp for comp0
commit f38e1f15359cceb3c0764635336125a1ceae78ff
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:49:45 2021 +0200
SelectOp for ccomp0 ok
commit ca969280380a593aef590a1fe2ec6f0fc112c2f5
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:46:01 2021 +0200
progress
commit e60a970f541ae6be30ec51cf95d60eb672ade829
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:40:49 2021 +0200
progres sur ltu etc.
commit 6f7d51e59a61d43fca06b1b4bad6dedada6e031e
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:13:07 2021 +0200
change selection
commit c2af349c6dd3e09fec25f3a96e1272377b6450ef
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:03:31 2021 +0200
begin rewrite selector
-rw-r--r-- | kvx/SelectOp.vp | 44 | ||||
-rw-r--r-- | kvx/SelectOpproof.v | 108 | ||||
-rw-r--r-- | test/monniaux/codegen/comp0.c | 3 |
3 files changed, 141 insertions, 14 deletions
diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp index aa241c1e..16607cf5 100644 --- a/kvx/SelectOp.vp +++ b/kvx/SelectOp.vp @@ -64,29 +64,49 @@ Section SELECT. Context {hf: helper_functions}. +Inductive to_cond0 := +| Cond0_some : condition0 -> expr -> to_cond0 +| Cond0_none : to_cond0 +| Cond0_true : to_cond0 +| Cond0_false : to_cond0. + +Definition compu0 c e1 := + match c with + | Clt => Cond0_false + | Cge => Cond0_true + | _ => Cond0_some (Ccompu0 c) e1 + end. + +Definition complu0 c e1 := + match c with + | Clt => Cond0_false + | Cge => Cond0_true + | _ => Cond0_some (Ccomplu0 c) e1 + end. + Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) := match cond, args with | (Ccompimm c x), (e1 ::: Enil) => if Int.eq_dec x Int.zero - then Some ((Ccomp0 c), e1) - else None + then Cond0_some (Ccomp0 c) e1 + else Cond0_none | (Ccompuimm c x), (e1 ::: Enil) => if Int.eq_dec x Int.zero - then Some ((Ccompu0 c), e1) - else None + then compu0 c e1 + else Cond0_none | (Ccomplimm c x), (e1 ::: Enil) => if Int64.eq_dec x Int64.zero - then Some ((Ccompl0 c), e1) - else None + then Cond0_some (Ccompl0 c) e1 + else Cond0_none | (Ccompluimm c x), (e1 ::: Enil) => if Int64.eq_dec x Int64.zero - then Some ((Ccomplu0 c), e1) - else None + then complu0 c e1 + else Cond0_none - | _, _ => None + | _, _ => Cond0_none end. (** Ternary operator *) @@ -112,8 +132,10 @@ Definition same_expr_pure (e1 e2: expr) := Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr) : option expr := Some (if same_expr_pure e1 e2 then e1 else match cond_to_condition0 cond args with - | None => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args) - | Some(cond0, ec) => select0 ty cond0 e1 e2 ec + | Cond0_none => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args) + | Cond0_some cond0 ec => select0 ty cond0 e1 e2 ec + | Cond0_true => e1 + | Cond0_false => e2 end). 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))). diff --git a/test/monniaux/codegen/comp0.c b/test/monniaux/codegen/comp0.c new file mode 100644 index 00000000..60f8ba77 --- /dev/null +++ b/test/monniaux/codegen/comp0.c @@ -0,0 +1,3 @@ +int toto(unsigned x) { + return (x < 0) ? 1 : 2; +} |