From 4f03d04f2058f9ce95bc7d2a1f6798fe8cfb0da4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 15 Sep 2021 11:55:56 +0200 Subject: bump OCaml version in CI --- .gitlab-ci.yml | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6da3a91d..28311ddc 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -3,7 +3,7 @@ stages: check-admitted: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - eval `opam config env` - opam update @@ -24,7 +24,7 @@ check-admitted: build_x86_64: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - eval `opam config env` - opam update @@ -47,7 +47,7 @@ build_x86_64: build_ia32: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-multilib @@ -72,7 +72,7 @@ build_ia32: build_aarch64: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-aarch64-linux-gnu qemu-user @@ -97,7 +97,7 @@ build_aarch64: build_arm: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-arm-linux-gnueabi libc6-dev-armel-cross qemu-user @@ -123,7 +123,7 @@ build_arm: build_armhf: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-arm-linux-gnueabihf libc6-dev-armhf-cross qemu-user @@ -148,7 +148,7 @@ build_armhf: build_ppc: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-powerpc-linux-gnu wget ninja-build libglib2.0-dev libpixman-1-dev @@ -177,7 +177,7 @@ build_ppc: build_ppc64: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-powerpc64-linux-gnu @@ -202,7 +202,7 @@ build_ppc64: build_rv64: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user @@ -227,7 +227,7 @@ build_rv64: build_rv32: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user @@ -250,7 +250,7 @@ build_rv32: build_kvx: stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace @@ -279,7 +279,7 @@ build_kvx: pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "build_kvx" above ?) stage: build - image: coqorg/coq:8.12.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace @@ -309,7 +309,7 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil build_aarch64_coq13: stage: build - image: coqorg/coq:8.13.2-ocaml-4.11.1-flambda + image: coqorg/coq:8.13.2-ocaml-4.11.2-flambda before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-aarch64-linux-gnu qemu-user -- cgit From b892d177945e9a5188cebe58f277a9d62dc6675e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Sep 2021 13:48:43 +0200 Subject: reachable --- kvx/Asmblockgen.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kvx/Asmblockgen.v b/kvx/Asmblockgen.v index e218f4ef..ab827b1c 100644 --- a/kvx/Asmblockgen.v +++ b/kvx/Asmblockgen.v @@ -299,7 +299,7 @@ Definition btest_for_cmpuwz (c: comparison) := match c with | Cne => OK BTwnez | Ceq => OK BTweqz - | Clt => Error (msg "btest_for_compuwz: Clt") + | Clt => Error (msg "btest_for_compuwz: Clt") (* TODO reachable *) | Cge => Error (msg "btest_for_compuwz: Cge") | Cle => OK BTweqz | Cgt => OK BTwnez -- cgit From b09852e25159fd5c2634d3cf87fe6c9e120a1941 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 17 Sep 2021 09:33:59 +0200 Subject: many parameters --- test/monniaux/params/call_many.c | 313 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 313 insertions(+) create mode 100644 test/monniaux/params/call_many.c diff --git a/test/monniaux/params/call_many.c b/test/monniaux/params/call_many.c new file mode 100644 index 00000000..4d2529c0 --- /dev/null +++ b/test/monniaux/params/call_many.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 fccfa9b6ac74953af188a2538eb9cd7258544c1a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 17 Sep 2021 10:12:12 +0200 Subject: FIX CODEGEN BUG Pallocframe --- kvx/Asmexpand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kvx/Asmexpand.ml b/kvx/Asmexpand.ml index 35c980bb..f84cf22d 100644 --- a/kvx/Asmexpand.ml +++ b/kvx/Asmexpand.ml @@ -517,8 +517,8 @@ let expand_instruction instr = end else begin let below = Integers.Ptrofs.repr (Z.neg sz) in expand_addptrofs stack_pointer stack_pointer below; - emit Psemi; (* Psemi required to fit in resource constraints *) expand_storeind_ptr stack_pointer stack_pointer (Integers.Ptrofs.add ofs below); + emit Psemi; (* Psemi required to fit in resource constraints *) vararg_start_ofs := None end | Pfreeframe (sz, ofs) -> -- cgit