From 81a2cfe0971ca2456ff04c1e661b9a56279728ac Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 17 Sep 2021 11:15:32 +0200 Subject: test for many parameters --- test/monniaux/params/call_many.c | 313 -------------------------------- test/regression/Makefile | 2 +- test/regression/Results/many_parameters | 1 + test/regression/many_parameters.c | 313 ++++++++++++++++++++++++++++++++ 4 files changed, 315 insertions(+), 314 deletions(-) delete mode 100644 test/monniaux/params/call_many.c create mode 100644 test/regression/Results/many_parameters create mode 100644 test/regression/many_parameters.c diff --git a/test/monniaux/params/call_many.c b/test/monniaux/params/call_many.c deleted file mode 100644 index 4d2529c0..00000000 --- a/test/monniaux/params/call_many.c +++ /dev/null @@ -1,313 +0,0 @@ -#include - -int call1( - int call00, - int call01, - int call02, - int call03, - int call04, - int call05, - int call06, - int call07, - int call08, - int call09, - int call10, - int call11, - int call12, - int call13, - int call14, - int call15, - int call16, - int call17, - int call18, - int call19, - int call20, - int call21, - int call22, - int call23, - int call24, - int call25, - int call26, - int call27, - int call28, - int call29, - int call30, - int call31, - int call32, - int call33, - int call34, - int call35, - int call36, - int call37, - int call38, - int call39, - int call40, - int call41, - int call42, - int call43, - int call44, - int call45, - int call46, - int call47, - int call48, - int call49, - int call50, - int call51, - int call52, - int call53, - int call54, - int call55, - int call56, - int call57, - int call58, - int call59) { - return ( call00 - + call01 - + call02 - + call03 - + call04 - + call05 - + call06 - + call07 - + call08 - + call09 - + call10 - + call11 - + call12 - + call13 - + call14 - + call15 - + call16 - + call17 - + call18 - + call19 - + call20 - + call21 - + call22 - + call23 - + call24 - + call25 - + call26 - + call27 - + call28 - + call29 - + call30 - + call31 - + call32 - + call33 - + call34 - + call35 - + call36 - + call37 - + call38 - + call39 - + call40 - + call41 - + call42 - + call43 - + call44 - + call45 - + call46 - + call47 - + call48 - + call49 - + call50 - + call51 - + call52 - + call53 - + call54 - + call55 - + call56 - + call57 - + call58 - + call59); -} - -int call2( - int call00, - int call01, - int call02, - int call03, - int call04, - int call05, - int call06, - int call07, - int call08, - int call09, - int call10, - int call11, - int call12, - int call13, - int call14, - int call15, - int call16, - int call17, - int call18, - int call19, - int call20, - int call21, - int call22, - int call23, - int call24, - int call25, - int call26, - int call27, - int call28, - int call29, - int call30, - int call31, - int call32, - int call33, - int call34, - int call35, - int call36, - int call37, - int call38, - int call39, - int call40, - int call41, - int call42, - int call43, - int call44, - int call45, - int call46, - int call47, - int call48, - int call49, - int call50, - int call51, - int call52, - int call53, - int call54, - int call55, - int call56, - int call57, - int call58, - int call59) { - return 10 + call1( - call00, - call01, - call02, - call03, - call04, - call05, - call06, - call07, - call08, - call09, - call10, - call11, - call12, - call13, - call14, - call15, - call16, - call17, - call18, - call19, - call20, - call21, - call22, - call23, - call24, - call25, - call26, - call27, - call28, - call29, - call30, - call31, - call32, - call33, - call34, - call35, - call36, - call37, - call38, - call39, - call40, - call41, - call42, - call43, - call44, - call45, - call46, - call47, - call48, - call49, - call50, - call51, - call52, - call53, - call54, - call55, - call56, - call57, - call58, - call59); -} - -int main() { - int x = - call2( 0, - 1, - 2, - 3, - 4, - 5, - 6, - 7, - 8, - 9, - 10, - 11, - 12, - 13, - 14, - 15, - 16, - 17, - 18, - 19, - 20, - 21, - 22, - 23, - 24, - 25, - 26, - 27, - 28, - 29, - 30, - 31, - 32, - 33, - 34, - 35, - 36, - 37, - 38, - 39, - 40, - 41, - 42, - 43, - 44, - 45, - 46, - 47, - 48, - 49, - 50, - 51, - 52, - 53, - 54, - 55, - 56, - 57, - 58, - 59); - printf("%d\n", x); -} diff --git a/test/regression/Makefile b/test/regression/Makefile index 9661a99e..0f9e368f 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -18,7 +18,7 @@ TESTS?=int32 int64 floats floats-basics floats-lit \ funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \ sizeof1 sizeof2 binops bool for1 for2 switch switch2 compound \ decl1 bitfields9 ptrs3 \ - parsing krfun ifconv + parsing krfun ifconv many_parameters # Can run, but only in compiled mode, and have reference output in Results diff --git a/test/regression/Results/many_parameters b/test/regression/Results/many_parameters new file mode 100644 index 00000000..838cfd7e --- /dev/null +++ b/test/regression/Results/many_parameters @@ -0,0 +1 @@ +1780 diff --git a/test/regression/many_parameters.c b/test/regression/many_parameters.c new file mode 100644 index 00000000..4d2529c0 --- /dev/null +++ b/test/regression/many_parameters.c @@ -0,0 +1,313 @@ +#include + +int call1( + int call00, + int call01, + int call02, + int call03, + int call04, + int call05, + int call06, + int call07, + int call08, + int call09, + int call10, + int call11, + int call12, + int call13, + int call14, + int call15, + int call16, + int call17, + int call18, + int call19, + int call20, + int call21, + int call22, + int call23, + int call24, + int call25, + int call26, + int call27, + int call28, + int call29, + int call30, + int call31, + int call32, + int call33, + int call34, + int call35, + int call36, + int call37, + int call38, + int call39, + int call40, + int call41, + int call42, + int call43, + int call44, + int call45, + int call46, + int call47, + int call48, + int call49, + int call50, + int call51, + int call52, + int call53, + int call54, + int call55, + int call56, + int call57, + int call58, + int call59) { + return ( call00 + + call01 + + call02 + + call03 + + call04 + + call05 + + call06 + + call07 + + call08 + + call09 + + call10 + + call11 + + call12 + + call13 + + call14 + + call15 + + call16 + + call17 + + call18 + + call19 + + call20 + + call21 + + call22 + + call23 + + call24 + + call25 + + call26 + + call27 + + call28 + + call29 + + call30 + + call31 + + call32 + + call33 + + call34 + + call35 + + call36 + + call37 + + call38 + + call39 + + call40 + + call41 + + call42 + + call43 + + call44 + + call45 + + call46 + + call47 + + call48 + + call49 + + call50 + + call51 + + call52 + + call53 + + call54 + + call55 + + call56 + + call57 + + call58 + + call59); +} + +int call2( + int call00, + int call01, + int call02, + int call03, + int call04, + int call05, + int call06, + int call07, + int call08, + int call09, + int call10, + int call11, + int call12, + int call13, + int call14, + int call15, + int call16, + int call17, + int call18, + int call19, + int call20, + int call21, + int call22, + int call23, + int call24, + int call25, + int call26, + int call27, + int call28, + int call29, + int call30, + int call31, + int call32, + int call33, + int call34, + int call35, + int call36, + int call37, + int call38, + int call39, + int call40, + int call41, + int call42, + int call43, + int call44, + int call45, + int call46, + int call47, + int call48, + int call49, + int call50, + int call51, + int call52, + int call53, + int call54, + int call55, + int call56, + int call57, + int call58, + int call59) { + return 10 + call1( + call00, + call01, + call02, + call03, + call04, + call05, + call06, + call07, + call08, + call09, + call10, + call11, + call12, + call13, + call14, + call15, + call16, + call17, + call18, + call19, + call20, + call21, + call22, + call23, + call24, + call25, + call26, + call27, + call28, + call29, + call30, + call31, + call32, + call33, + call34, + call35, + call36, + call37, + call38, + call39, + call40, + call41, + call42, + call43, + call44, + call45, + call46, + call47, + call48, + call49, + call50, + call51, + call52, + call53, + call54, + call55, + call56, + call57, + call58, + call59); +} + +int main() { + int x = + call2( 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59); + printf("%d\n", x); +} -- cgit 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/SelectOp.vp | 44 ++++++++++++----- kvx/SelectOpproof.v | 108 ++++++++++++++++++++++++++++++++++++++++-- test/monniaux/codegen/comp0.c | 3 ++ 3 files changed, 141 insertions(+), 14 deletions(-) create mode 100644 test/monniaux/codegen/comp0.c 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; +} -- cgit