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 From 32c90e36e4018a5a49a0a45e2e98a9c94c0d185d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 17 Sep 2021 15:08:22 +0200 Subject: some csmith tests --- test/monniaux/csmith/Makefile | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/test/monniaux/csmith/Makefile b/test/monniaux/csmith/Makefile index aa4eccab..e6475fa2 100644 --- a/test/monniaux/csmith/Makefile +++ b/test/monniaux/csmith/Makefile @@ -1,9 +1,13 @@ +all: + +.SECONDARY: + INCLUDES=-I csmith/include/csmith-2.3.0/ TARGET_CCOMP=../../../ccomp -TARGET_CC=gcc +TARGET_CC=kvx-cos-gcc ifndef EXECUTE -EXECUTE=timeout 2s +EXECUTE=timeout 10s kvx-cluster -- endif CFLAGS += -Wno-incompatible-pointer-types @@ -11,8 +15,9 @@ CFLAGS += -Wno-incompatible-pointer-types ifndef CSMITH CSMITH=csmith/bin/csmith endif +CSMITHOPT=--max-funcs 10 -MAX=300 +MAX=10000 PREFIX=ran%06.f CCOMPOTS=-static @@ -69,7 +74,7 @@ ran%/example.gcc.host: ran%/source.gcc.host.o ran%/source.c: mkdir -p ran$* - $(CSMITH) --seed $* --output ran$*/source.c + $(CSMITH) $(CSMITHOPT) --seed $* --output ran$*/source.c ran%/example.target.cmp : ran%/example.gcc.target.out ran%/example.ccomp.target.out cmp $+ > $@ -- cgit From 124cd837a591df308221f236810c7f66847b1abe Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 17 Sep 2021 19:18:05 +0200 Subject: target cc --- test/monniaux/csmith/Makefile | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/test/monniaux/csmith/Makefile b/test/monniaux/csmith/Makefile index e6475fa2..f4b0d68a 100644 --- a/test/monniaux/csmith/Makefile +++ b/test/monniaux/csmith/Makefile @@ -4,7 +4,10 @@ all: INCLUDES=-I csmith/include/csmith-2.3.0/ TARGET_CCOMP=../../../ccomp + +ifndef TARGET_CC TARGET_CC=kvx-cos-gcc +endif ifndef EXECUTE EXECUTE=timeout 10s kvx-cluster -- @@ -21,7 +24,7 @@ MAX=10000 PREFIX=ran%06.f CCOMPOTS=-static -CCOMPFLAGS+= -fstruct-passing -fbitfields -fno-cse2 -stdlib ../../../runtime +CCOMPFLAGS+= -fstruct-passing -fbitfields -fno-cse2 -fno-cse -fno-cse3 -stdlib ../../../runtime TESTS_C=$(shell seq --format $(PREFIX)/source.c 1 $(MAX)) -- cgit From fd6f8114d91f1649e467571b39adcb0b8fa2f92e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 18 Sep 2021 10:18:34 +0200 Subject: reduce number of csmith tests --- test/monniaux/csmith/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/monniaux/csmith/Makefile b/test/monniaux/csmith/Makefile index f4b0d68a..30107695 100644 --- a/test/monniaux/csmith/Makefile +++ b/test/monniaux/csmith/Makefile @@ -20,7 +20,7 @@ CSMITH=csmith/bin/csmith endif CSMITHOPT=--max-funcs 10 -MAX=10000 +MAX=5000 PREFIX=ran%06.f CCOMPOTS=-static -- cgit From 68995e0afca237658728b2c82fff04133a5aae72 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 18 Sep 2021 12:47:14 +0200 Subject: fix for x86-64 --- test/monniaux/csmith/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/monniaux/csmith/Makefile b/test/monniaux/csmith/Makefile index 30107695..ab7931f1 100644 --- a/test/monniaux/csmith/Makefile +++ b/test/monniaux/csmith/Makefile @@ -6,7 +6,7 @@ INCLUDES=-I csmith/include/csmith-2.3.0/ TARGET_CCOMP=../../../ccomp ifndef TARGET_CC -TARGET_CC=kvx-cos-gcc +TARGET_CC=gcc endif ifndef EXECUTE -- cgit From a4c242f24d02bc69853b21071bc34beff8f31d3b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Sep 2021 09:59:03 +0200 Subject: creduce scripts --- test/monniaux/csmith/reduce/reduce.sh | 15 +++++++++++++++ test/monniaux/csmith/reduce/reduce_wrt_host.sh | 25 +++++++++++++++++++++++++ 2 files changed, 40 insertions(+) create mode 100755 test/monniaux/csmith/reduce/reduce.sh create mode 100755 test/monniaux/csmith/reduce/reduce_wrt_host.sh diff --git a/test/monniaux/csmith/reduce/reduce.sh b/test/monniaux/csmith/reduce/reduce.sh new file mode 100755 index 00000000..d8df11a5 --- /dev/null +++ b/test/monniaux/csmith/reduce/reduce.sh @@ -0,0 +1,15 @@ +#!/bin/bash +INCLUDE=-I$COMPCERT/test/monniaux/csmith/csmith/include/csmith-2.3.0 +if kvx-cos-gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -o source.gcc.target && kvx-cluster -- source.gcc.target >& source.gcc.log +then + if $COMPCERT/ccomp $INCLUDE -fall -fno-cse -fno-cse2 -fno-cse3 source.c -o source.ccomp.target + then + kvx-cluster -- source.ccomp.target >& source.ccomp.log + grep OPCODE source.ccomp.log + else + exit 2 + fi +else + exit 1 +fi + diff --git a/test/monniaux/csmith/reduce/reduce_wrt_host.sh b/test/monniaux/csmith/reduce/reduce_wrt_host.sh new file mode 100755 index 00000000..6e01f3a0 --- /dev/null +++ b/test/monniaux/csmith/reduce/reduce_wrt_host.sh @@ -0,0 +1,25 @@ +#!/bin/bash +INCLUDE=-I$COMPCERT/test/monniaux/csmith/csmith/include/csmith-2.3.0 +if gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -o source.gcc.host && valgrind --exit-on-first-error=yes --error-exitcode=120 --log-file=valgrind.out ./source.gcc.host > source.gcc.host.out ; +then + if gcc $INCLUDE -Werror=uninitialized -Werror=implicit -fsanitize=undefined -fsanitize=address source.c -o source.gcc+san.host && ./source.gcc+san.host > source.gcc+san.host.out ; + then + if kvx-cos-gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -o source.gcc.target && kvx-cluster -- source.gcc.target >& source.gcc.target.out && cmp source.gcc.host.out source.gcc.target.out + then + if $COMPCERT/ccomp $INCLUDE -fall -fno-cse -fno-cse2 -fno-cse3 source.c -o source.ccomp.target + then + kvx-cluster -- source.ccomp.target >& source.ccomp.target.out + cmp source.ccomp.target.out source.gcc.target.out + else + exit 2 + fi + else + exit 1 + fi + else + exit 4 + fi +else + exit 5 +fi + -- cgit From b2072e4497dbb109d391e89e20c89b87450cf728 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Sep 2021 10:00:49 +0200 Subject: fix script to answer 0 if differences --- test/monniaux/csmith/reduce/reduce_wrt_host.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/test/monniaux/csmith/reduce/reduce_wrt_host.sh b/test/monniaux/csmith/reduce/reduce_wrt_host.sh index 6e01f3a0..23e4208e 100755 --- a/test/monniaux/csmith/reduce/reduce_wrt_host.sh +++ b/test/monniaux/csmith/reduce/reduce_wrt_host.sh @@ -9,7 +9,10 @@ then if $COMPCERT/ccomp $INCLUDE -fall -fno-cse -fno-cse2 -fno-cse3 source.c -o source.ccomp.target then kvx-cluster -- source.ccomp.target >& source.ccomp.target.out - cmp source.ccomp.target.out source.gcc.target.out + if cmp source.ccomp.target.out source.gcc.target.out + then exit 40 + else exit 0 + fi else exit 2 fi -- cgit From 4a17125ee3f6766710e6e6e47d551cf0cf29cb47 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 19 Sep 2021 11:41:43 +0200 Subject: fix issue 244 --- aarch64/Asmexpand.ml | 1 + test/gourdinl/builtin_memcpy.c | 9 +++++++++ 2 files changed, 10 insertions(+) create mode 100644 test/gourdinl/builtin_memcpy.c diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index 828c96d6..68884550 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -185,6 +185,7 @@ let memcpy_small_arg sz arg tmp = | BA_addrstack ofs -> if offset_in_range ofs && offset_in_range (Ptrofs.add ofs (Ptrofs.repr (Z.of_uint sz))) + && (Z.to_int ofs) mod 8 = 0 then (XSP, ofs) else begin expand_addimm64 (RR1 tmp) XSP ofs; (RR1 tmp, _0) end | _ -> diff --git a/test/gourdinl/builtin_memcpy.c b/test/gourdinl/builtin_memcpy.c new file mode 100644 index 00000000..421f543c --- /dev/null +++ b/test/gourdinl/builtin_memcpy.c @@ -0,0 +1,9 @@ +struct a b; +struct a { + short; + int; + short; +} c() { + struct a d[2][16]; + b = d[1][7]; +} -- cgit From 012e76c21d78212f5456611ebb319d39846186c1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Sep 2021 15:11:24 +0200 Subject: RiscV --- test/monniaux/csmith/reduce/reduce_wrt_host.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/monniaux/csmith/reduce/reduce_wrt_host.sh b/test/monniaux/csmith/reduce/reduce_wrt_host.sh index 23e4208e..a37eb51b 100755 --- a/test/monniaux/csmith/reduce/reduce_wrt_host.sh +++ b/test/monniaux/csmith/reduce/reduce_wrt_host.sh @@ -4,12 +4,12 @@ if gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -o source.gcc.ho then if gcc $INCLUDE -Werror=uninitialized -Werror=implicit -fsanitize=undefined -fsanitize=address source.c -o source.gcc+san.host && ./source.gcc+san.host > source.gcc+san.host.out ; then - if kvx-cos-gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -o source.gcc.target && kvx-cluster -- source.gcc.target >& source.gcc.target.out && cmp source.gcc.host.out source.gcc.target.out + if riscv64-linux-gnu-gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -o source.gcc.target && qemu-riscv64 -L /usr/riscv64-linux-gnu source.gcc.target >& source.gcc.target.out && diff source.gcc.host.out source.gcc.target.out then if $COMPCERT/ccomp $INCLUDE -fall -fno-cse -fno-cse2 -fno-cse3 source.c -o source.ccomp.target then - kvx-cluster -- source.ccomp.target >& source.ccomp.target.out - if cmp source.ccomp.target.out source.gcc.target.out + qemu-riscv64 -L /usr/riscv64-linux-gnu source.ccomp.target >& source.ccomp.target.out + if diff source.ccomp.target.out source.gcc.target.out then exit 40 else exit 0 fi -- cgit From 9861bfb0838fb9fed84a32de67a4c983692b4dcf Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Sep 2021 07:36:09 +0200 Subject: use clang, better error reporting --- test/monniaux/csmith/reduce/reduce_wrt_host.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/monniaux/csmith/reduce/reduce_wrt_host.sh b/test/monniaux/csmith/reduce/reduce_wrt_host.sh index a37eb51b..698d078d 100755 --- a/test/monniaux/csmith/reduce/reduce_wrt_host.sh +++ b/test/monniaux/csmith/reduce/reduce_wrt_host.sh @@ -1,10 +1,10 @@ #!/bin/bash INCLUDE=-I$COMPCERT/test/monniaux/csmith/csmith/include/csmith-2.3.0 -if gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -o source.gcc.host && valgrind --exit-on-first-error=yes --error-exitcode=120 --log-file=valgrind.out ./source.gcc.host > source.gcc.host.out ; +if /usr/bin/clang $INCLUDE -O -Werror=uninitialized -Werror=implicit -Werror=return-type source.c -o source.clang.host && valgrind --exit-on-first-error=yes --error-exitcode=120 --log-file=valgrind.out ./source.clang.host > source.clang.host.out ; then - if gcc $INCLUDE -Werror=uninitialized -Werror=implicit -fsanitize=undefined -fsanitize=address source.c -o source.gcc+san.host && ./source.gcc+san.host > source.gcc+san.host.out ; + if gcc $INCLUDE -Werror=uninitialized -Werror=implicit -Werror=return-type -fsanitize=undefined -fsanitize=address source.c -o source.gcc+san.host && ./source.gcc+san.host > source.gcc+san.host.out ; then - if riscv64-linux-gnu-gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -o source.gcc.target && qemu-riscv64 -L /usr/riscv64-linux-gnu source.gcc.target >& source.gcc.target.out && diff source.gcc.host.out source.gcc.target.out + if cmp source.clang.host.out source.gcc+san.host.out && riscv64-linux-gnu-gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -Werror=return-type -o source.gcc.target && qemu-riscv64 -L /usr/riscv64-linux-gnu source.gcc.target >& source.gcc.target.out && diff source.clang.host.out source.gcc.target.out then if $COMPCERT/ccomp $INCLUDE -fall -fno-cse -fno-cse2 -fno-cse3 source.c -o source.ccomp.target then -- cgit From bc424c983d58b7da5a39e735cb76db1b89821c46 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Sep 2021 10:11:22 +0200 Subject: use large stacksize on KVX --- .gitlab-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1ecdafdf..6604997c 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -273,7 +273,7 @@ build_kvx: - source /opt/kalray/accesscore/kalray.sh && make -j "$NJOBS" - source /opt/kalray/accesscore/kalray.sh && make -C test CCOMPOPTS=-static SIMU='kvx-cluster -- ' EXECUTE='kvx-cluster -- ' all test - source /opt/kalray/accesscore/kalray.sh && ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='kvx-cos-gcc' EXECUTE='kvx-cluster -- ' CCOMPOPTS='-static' TARGET_CFLAGS='-static' - - source /opt/kalray/accesscore/kalray.sh && ulimit -s65536 && make -C test/monniaux/csmith TARGET_CC='kvx-cos-gcc' EXECUTE='timeout 10s kvx-cluster -- ' CCOMPOPTS='-static' TARGET_CFLAGS='-static' + - source /opt/kalray/accesscore/kalray.sh && ulimit -s65536 && make -C test/monniaux/csmith TARGET_CC='kvx-cos-gcc' CCOMPOPTS="-Wl,--defsym=USER_STACK_SIZE=0x20000" EXECUTE="timeout 10s kvx-cluster -- " rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always -- cgit From 81eadac7dfaa7fb05f11d45042b74e95e1a14a09 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Sep 2021 13:29:24 +0200 Subject: do 500 of them --- test/monniaux/csmith/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/monniaux/csmith/Makefile b/test/monniaux/csmith/Makefile index ab7931f1..78664c4b 100644 --- a/test/monniaux/csmith/Makefile +++ b/test/monniaux/csmith/Makefile @@ -20,7 +20,7 @@ CSMITH=csmith/bin/csmith endif CSMITHOPT=--max-funcs 10 -MAX=5000 +MAX=500 PREFIX=ran%06.f CCOMPOTS=-static -- cgit From ea881bf4002c6a2ee5cafff393ee0c8939d50835 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Sep 2021 14:45:49 +0200 Subject: separate wget/curl --- test/monniaux/csmith/Makefile | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/test/monniaux/csmith/Makefile b/test/monniaux/csmith/Makefile index ab7931f1..274b3b84 100644 --- a/test/monniaux/csmith/Makefile +++ b/test/monniaux/csmith/Makefile @@ -90,7 +90,9 @@ ran%/example.host_target.cmp : ran%/example.gcc.host.out ran%/example.ccomp.targ clean: -rm -rf ran* -csmith/bin/csmith: - curl -L -o csmith-2.3.0.tar.gz https://embed.cs.utah.edu/csmith/csmith-2.3.0.tar.gz +csmith-2.3.0.tar.gz: + curl -L -O $@ https://embed.cs.utah.edu/csmith/csmith-2.3.0.tar.gz + +csmith/bin/csmith: csmith-2.3.0.tar.gz tar xfz csmith-2.3.0.tar.gz WD=`pwd` && cd csmith-2.3.0 && ./configure --prefix=$$WD/csmith && make install -- cgit From 3a6a2f239aa00fc568d7206909e1ffd9eef1f31c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Sep 2021 17:09:23 +0200 Subject: better predicate --- test/monniaux/csmith/reduce/reduce_wrt_host.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/test/monniaux/csmith/reduce/reduce_wrt_host.sh b/test/monniaux/csmith/reduce/reduce_wrt_host.sh index 698d078d..5e86213e 100755 --- a/test/monniaux/csmith/reduce/reduce_wrt_host.sh +++ b/test/monniaux/csmith/reduce/reduce_wrt_host.sh @@ -1,15 +1,15 @@ #!/bin/bash INCLUDE=-I$COMPCERT/test/monniaux/csmith/csmith/include/csmith-2.3.0 -if /usr/bin/clang $INCLUDE -O -Werror=uninitialized -Werror=implicit -Werror=return-type source.c -o source.clang.host && valgrind --exit-on-first-error=yes --error-exitcode=120 --log-file=valgrind.out ./source.clang.host > source.clang.host.out ; +if /usr/bin/clang $INCLUDE -O -Werror=strict-prototypes -Werror=uninitialized -Werror=implicit -Werror=return-type source.c -o source.clang.host && valgrind --exit-on-first-error=yes --error-exitcode=120 --log-file=valgrind.out ./source.clang.host > source.clang.host.out ; then - if gcc $INCLUDE -Werror=uninitialized -Werror=implicit -Werror=return-type -fsanitize=undefined -fsanitize=address source.c -o source.gcc+san.host && ./source.gcc+san.host > source.gcc+san.host.out ; + if gcc $INCLUDE -Werror=strict-prototypes -Werror=uninitialized -Werror=implicit -Werror=return-type -fsanitize=undefined -fsanitize=address source.c -o source.gcc+san.host && ./source.gcc+san.host > source.gcc+san.host.out ; then - if cmp source.clang.host.out source.gcc+san.host.out && riscv64-linux-gnu-gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -Werror=return-type -o source.gcc.target && qemu-riscv64 -L /usr/riscv64-linux-gnu source.gcc.target >& source.gcc.target.out && diff source.clang.host.out source.gcc.target.out + if cmp source.clang.host.out source.gcc+san.host.out && riscv64-linux-gnu-gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -Werror=return-type -o source.gcc.target && qemu-riscv64 -L /usr/riscv64-linux-gnu source.gcc.target >& source.gcc.target.out && grep checksum source.gcc.target.out && diff source.clang.host.out source.gcc.target.out then if $COMPCERT/ccomp $INCLUDE -fall -fno-cse -fno-cse2 -fno-cse3 source.c -o source.ccomp.target then qemu-riscv64 -L /usr/riscv64-linux-gnu source.ccomp.target >& source.ccomp.target.out - if diff source.ccomp.target.out source.gcc.target.out + if grep checksum source.ccomp.target.out && diff source.ccomp.target.out source.gcc.target.out then exit 40 else exit 0 fi -- cgit From bc0900442d879635ca57bb613fe7644133a63d75 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Sep 2021 18:56:15 +0200 Subject: keep only checksum --- test/monniaux/csmith/reduce/reduce_wrt_host.sh | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/test/monniaux/csmith/reduce/reduce_wrt_host.sh b/test/monniaux/csmith/reduce/reduce_wrt_host.sh index 5e86213e..7666c31b 100755 --- a/test/monniaux/csmith/reduce/reduce_wrt_host.sh +++ b/test/monniaux/csmith/reduce/reduce_wrt_host.sh @@ -1,15 +1,15 @@ #!/bin/bash INCLUDE=-I$COMPCERT/test/monniaux/csmith/csmith/include/csmith-2.3.0 -if /usr/bin/clang $INCLUDE -O -Werror=strict-prototypes -Werror=uninitialized -Werror=implicit -Werror=return-type source.c -o source.clang.host && valgrind --exit-on-first-error=yes --error-exitcode=120 --log-file=valgrind.out ./source.clang.host > source.clang.host.out ; +if /usr/bin/clang $INCLUDE -O -Werror=format -Werror=strict-prototypes -Werror=uninitialized -Werror=implicit -Werror=return-type source.c -o source.clang.host && valgrind --exit-on-first-error=yes --error-exitcode=120 --log-file=valgrind.out ./source.clang.host > source.clang.host.out ; then - if gcc $INCLUDE -Werror=strict-prototypes -Werror=uninitialized -Werror=implicit -Werror=return-type -fsanitize=undefined -fsanitize=address source.c -o source.gcc+san.host && ./source.gcc+san.host > source.gcc+san.host.out ; + if gcc $INCLUDE -Werror=format -Werror=strict-prototypes -Werror=uninitialized -Werror=implicit -Werror=return-type -fsanitize=undefined -fsanitize=address source.c -o source.gcc+san.host && ./source.gcc+san.host > source.gcc+san.host.out ; then - if cmp source.clang.host.out source.gcc+san.host.out && riscv64-linux-gnu-gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -Werror=return-type -o source.gcc.target && qemu-riscv64 -L /usr/riscv64-linux-gnu source.gcc.target >& source.gcc.target.out && grep checksum source.gcc.target.out && diff source.clang.host.out source.gcc.target.out + if cmp source.clang.host.out source.gcc+san.host.out && aarch64-linux-gnu-gcc $INCLUDE -Werror=format -Werror=uninitialized -Werror=implicit source.c -Werror=return-type -o source.gcc.target && qemu-aarch64 -L /usr/aarch64-linux-gnu source.gcc.target >& source.gcc.target.out && grep checksum source.gcc.target.out > source.gcc.target.check && diff source.clang.host.out source.gcc.target.out then if $COMPCERT/ccomp $INCLUDE -fall -fno-cse -fno-cse2 -fno-cse3 source.c -o source.ccomp.target then - qemu-riscv64 -L /usr/riscv64-linux-gnu source.ccomp.target >& source.ccomp.target.out - if grep checksum source.ccomp.target.out && diff source.ccomp.target.out source.gcc.target.out + qemu-aarch64 -L /usr/aarch64-linux-gnu source.ccomp.target >& source.ccomp.target.out + if grep checksum source.ccomp.target.out > source.ccomp.target.check && diff source.ccomp.target.check source.gcc.target.check then exit 40 else exit 0 fi -- cgit From 2fd4ccbcda1494d3af6cbc1a9978ddeb76a8e014 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Sep 2021 20:38:43 +0200 Subject: don't use unions --- test/monniaux/csmith/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/monniaux/csmith/Makefile b/test/monniaux/csmith/Makefile index 1f32dccb..2e9d9d24 100644 --- a/test/monniaux/csmith/Makefile +++ b/test/monniaux/csmith/Makefile @@ -18,7 +18,7 @@ CFLAGS += -Wno-incompatible-pointer-types ifndef CSMITH CSMITH=csmith/bin/csmith endif -CSMITHOPT=--max-funcs 10 +CSMITHOPT=--max-funcs 10 --no-unions MAX=500 PREFIX=ran%06.f -- cgit From bb85a1c6fee93987bb5cb0948a0d0faa013999fe Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Sep 2021 21:17:52 +0200 Subject: wrong curl command --- test/monniaux/csmith/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/monniaux/csmith/Makefile b/test/monniaux/csmith/Makefile index 2e9d9d24..5a1d3843 100644 --- a/test/monniaux/csmith/Makefile +++ b/test/monniaux/csmith/Makefile @@ -91,7 +91,7 @@ clean: -rm -rf ran* csmith-2.3.0.tar.gz: - curl -L -O $@ https://embed.cs.utah.edu/csmith/csmith-2.3.0.tar.gz + curl -L -o $@ https://embed.cs.utah.edu/csmith/csmith-2.3.0.tar.gz csmith/bin/csmith: csmith-2.3.0.tar.gz tar xfz csmith-2.3.0.tar.gz -- cgit