aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml26
-rw-r--r--kvx/Asmblockgen.v2
-rw-r--r--kvx/Asmexpand.ml2
-rw-r--r--test/monniaux/params/call_many.c313
4 files changed, 339 insertions, 4 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7519377a..1ecdafdf 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -287,7 +287,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
@@ -314,4 +314,26 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil
rules:
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
- \ No newline at end of file
+
+build_aarch64_coq13:
+ stage: build
+ 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
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_aarch64.sh
+ - make -j "$NJOBS"
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "kvx-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "kvx-work-ssa"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual
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
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) ->
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 <stdio.h>
+
+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);
+}
generated by cgit (git 2.34.1) at 2024-05-19 23:55:03 +0000