diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-06-17 16:52:09 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-06-17 16:52:09 +0200 |
commit | 9759e94256fd09f4995418b67b7aedbcf84b4b10 (patch) | |
tree | ec7c2a0a8564f49278005bc6c2a863e9f7ae0c4a | |
parent | 4413c27d6c6a3d69df34955d9d453c38b32174c7 (diff) | |
parent | 04b2489d7c2a9b0d203b3d431517367a07bd6b30 (diff) | |
download | compcert-kvx-9759e94256fd09f4995418b67b7aedbcf84b4b10.tar.gz compcert-kvx-9759e94256fd09f4995418b67b7aedbcf84b4b10.zip |
Merge remote-tracking branch 'origin/kvx-work' into kvx-sched-w-reg-press
-rw-r--r-- | .gitlab-ci.yml | 78 | ||||
-rwxr-xr-x | config_macos_x86_64.sh | 1 | ||||
-rwxr-xr-x | config_simple.sh | 2 | ||||
-rwxr-xr-x | filter_peeplog.fish | 39 | ||||
-rw-r--r-- | kvx/Asmvliw.v | 9 | ||||
-rw-r--r-- | lib/Integers.v | 3 | ||||
-rw-r--r-- | riscV/Asmgenproof1.v | 16 | ||||
-rw-r--r-- | runtime/Makefile | 2 | ||||
-rwxr-xr-x | test/gourdinl/compare_pp.sh | 16 | ||||
-rw-r--r-- | test/gourdinl/postpass_exp.c | 5 | ||||
-rw-r--r-- | test/monniaux/cycles.h | 2 | ||||
-rw-r--r-- | test/monniaux/division/harness.c | 82 | ||||
-rw-r--r-- | test/monniaux/division/my_udiv32.s | 36 | ||||
-rw-r--r-- | x86/TargetPrinter.ml | 14 |
14 files changed, 221 insertions, 84 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a7811ae3..b3bb418f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -14,7 +14,9 @@ check-admitted: rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 @@ -35,7 +37,9 @@ build_x86_64: rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 @@ -58,7 +62,9 @@ build_ia32: rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 @@ -76,14 +82,14 @@ build_aarch64: script: - ./config_aarch64.sh - make -j "$NJOBS" - - export LD_LIBRARY_PATH=/usr/aarch64-linux-gnu/lib - - sudo ln -s /usr/aarch64-linux-gnu/lib/ld-linux-aarch64.so.1 /lib - - make -C test CCOMPOPTS='-static' SIMU='qemu-aarch64' EXECUTE='qemu-aarch64' all test - - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='aarch64-linux-gnu-gcc' EXECUTE='qemu-aarch64' CCOMPOPTS='-static' TARGET_CFLAGS='-static' + - make -C test SIMU='qemu-aarch64 -L /usr/aarch64-linux-gnu' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu' all test + - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='aarch64-linux-gnu-gcc' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu' CCOMPOPTS='-static' TARGET_CFLAGS='-static' rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 @@ -101,14 +107,14 @@ build_arm: script: - ./config_arm.sh - make -j "$NJOBS" - - export LD_LIBRARY_PATH=/usr/arm-linux-gnueabi/lib - - sudo ln -s /usr/arm-linux-gnueabi/lib/ld-linux.so.3 /lib # FIXME: UGLY ! - - make -C test CCOMPOPTS=-static SIMU='qemu-arm' EXECUTE='qemu-arm' all test - - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabi-gcc' EXECUTE='qemu-arm' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32 + - make -C test SIMU='qemu-arm -L /usr/arm-linux-gnueabi' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabi' all test + - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabi-gcc' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabi' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32 rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 @@ -127,14 +133,14 @@ build_armhf: script: - ./config_armhf.sh - make -j "$NJOBS" - - export LD_LIBRARY_PATH=/usr/arm-linux-gnueabihf/lib - - sudo ln -s /usr/arm-linux-gnueabihf/lib/ld-linux-armhf.so.3 /lib # FIXME: UGLY ! - - make -C test CCOMPOPTS=-static SIMU='qemu-arm' EXECUTE='qemu-arm' all test - - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabihf-gcc' EXECUTE='qemu-arm' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32 + - make -C test SIMU='qemu-arm -L /usr/arm-linux-gnueabihf' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabihf' all test + - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabihf-gcc' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabihf' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32 rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 @@ -145,17 +151,25 @@ build_ppc: image: coqorg/coq:8.12.2-ocaml-4.11.1-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 qemu-user + - sudo apt-get -y install gcc-powerpc-linux-gnu wget ninja-build libglib2.0-dev libpixman-1-dev + - wget --no-verbose https://download.qemu.org/qemu-6.0.0.tar.xz + - tar xJf qemu-6.0.0.tar.xz + - (cd qemu-6.0.0 && ./configure --target-list=ppc-linux-user && make && sudo make install) - eval `opam config env` - opam update - opam install -y menhir script: - ./config_ppc.sh - make -j "$NJOBS" + - qemu-ppc --version + - make -C test SIMU='qemu-ppc -L /usr/powerpc-linux-gnu -cpu 7400' EXECUTE='qemu-ppc -L /usr/powerpc-linux-gnu -cpu 7400' all test + - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='powerpc-linux-gnu-gcc' EXECUTE='qemu-ppc -L /usr/powerpc-linux-gnu -cpu 7400' BITS=32 rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 @@ -173,10 +187,14 @@ build_ppc64: script: - ./config_ppc64.sh - make -j "$NJOBS" + #- make -C test SIMU='qemu-ppc64 -L /usr/powerpc64-linux-gnu -cpu 7400' EXECUTE='qemu-ppc64 -L /usr/powerpc64-linux-gnu -cpu 7400' all test + #- ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='powerpc64-linux-gnu-gcc' EXECUTE='qemu-ppc64 -L /usr/powerpc64-linux-gnu -cpu 7400' BITS=32 rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 @@ -194,14 +212,14 @@ build_rv64: script: - ./config_rv64.sh - make -j "$NJOBS" - - export LD_LIBRARY_PATH=/usr/riscv64-linux-gnu/lib - - sudo ln -s /usr/riscv64-linux-gnu/lib/ld-linux-riscv64-lp64d.so.1 /lib - - make -C test CCOMPOPTS=-static SIMU='qemu-riscv64' EXECUTE='qemu-riscv64' all test - - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='riscv64-linux-gnu-gcc' EXECUTE='qemu-riscv64' CCOMPOPTS='-static' TARGET_CFLAGS='-static' + - make -C test SIMU='qemu-riscv64 -L /usr/riscv64-linux-gnu' EXECUTE='qemu-riscv64 -L /usr/riscv64-linux-gnu' all test + - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='riscv64-linux-gnu-gcc' EXECUTE='qemu-riscv64 -L /usr/riscv64-linux-gnu' CCOMPOPTS='-static' TARGET_CFLAGS='-static' rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 @@ -222,7 +240,9 @@ build_rv32: rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 @@ -249,7 +269,9 @@ build_kvx: rules: - if: '$CI_COMMIT_BRANCH == "kvx-work"' when: always - - if: '$CI_COMMIT_BRANCH == "mppa-kvx"' + - 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 diff --git a/config_macos_x86_64.sh b/config_macos_x86_64.sh new file mode 100755 index 00000000..9d5b3f5e --- /dev/null +++ b/config_macos_x86_64.sh @@ -0,0 +1 @@ +exec ./config_simple.sh x86_64-macos "$@" diff --git a/config_simple.sh b/config_simple.sh index e2d3844c..52b7d1a6 100755 --- a/config_simple.sh +++ b/config_simple.sh @@ -2,7 +2,7 @@ arch=$1 shift version=`git rev-parse --short HEAD` branch=`git rev-parse --abbrev-ref HEAD` -date=`date -I` +date=`date +%Y-%m-%d` if test "x$CCOMP_INSTALL_PREFIX" = "x" ; then CCOMP_INSTALL_PREFIX=/opt/CompCert ; diff --git a/filter_peeplog.fish b/filter_peeplog.fish deleted file mode 100755 index 72a0eaf1..00000000 --- a/filter_peeplog.fish +++ /dev/null @@ -1,39 +0,0 @@ -echo "LDP_CONSEC_PEEP_IMM_INC_ldr32" (cat log | ack "LDP_CONSEC_PEEP_IMM_INC_ldr32" | wc -l) -echo "LDP_CONSEC_PEEP_IMM_INC_ldr64" (cat log | ack "LDP_CONSEC_PEEP_IMM_INC_ldr64" | wc -l) -echo "LDP_CONSEC_PEEP_IMM_DEC_ldr32" (cat log | ack "LDP_CONSEC_PEEP_IMM_DEC_ldr32" | wc -l) -echo "LDP_CONSEC_PEEP_IMM_DEC_ldr64" (cat log | ack "LDP_CONSEC_PEEP_IMM_DEC_ldr64" | wc -l) -echo "LDP_FORW_SPACED_PEEP_IMM_INC_ldr32" (cat log | ack "LDP_FORW_SPACED_PEEP_IMM_INC_ldr32" | wc -l) -echo "LDP_FORW_SPACED_PEEP_IMM_INC_ldr64" (cat log | ack "LDP_FORW_SPACED_PEEP_IMM_INC_ldr64" | wc -l) -echo "LDP_FORW_SPACED_PEEP_IMM_DEC_ldr32" (cat log | ack "LDP_FORW_SPACED_PEEP_IMM_DEC_ldr32" | wc -l) -echo "LDP_FORW_SPACED_PEEP_IMM_DEC_ldr64" (cat log | ack "LDP_FORW_SPACED_PEEP_IMM_DEC_ldr64" | wc -l) -echo "LDP_BACK_SPACED_PEEP_IMM_INC_ldr32" (cat log | ack "LDP_BACK_SPACED_PEEP_IMM_INC_ldr32" | wc -l) -echo "LDP_BACK_SPACED_PEEP_IMM_INC_ldr64" (cat log | ack "LDP_BACK_SPACED_PEEP_IMM_INC_ldr64" | wc -l) -echo "LDP_BACK_SPACED_PEEP_IMM_DEC_ldr32" (cat log | ack "LDP_BACK_SPACED_PEEP_IMM_DEC_ldr32" | wc -l) -echo "LDP_BACK_SPACED_PEEP_IMM_DEC_ldr64" (cat log | ack "LDP_BACK_SPACED_PEEP_IMM_DEC_ldr64" | wc -l) -echo "\n" -echo "LDP_CONSEC_PEEP_IMM_INC_ldr32f" (cat log | ack "LDP_CONSEC_PEEP_IMM_INC_ldr32f" | wc -l) -echo "LDP_CONSEC_PEEP_IMM_INC_ldr64f" (cat log | ack "LDP_CONSEC_PEEP_IMM_INC_ldr64f" | wc -l) -echo "LDP_CONSEC_PEEP_IMM_DEC_ldr32f" (cat log | ack "LDP_CONSEC_PEEP_IMM_DEC_ldr32f" | wc -l) -echo "LDP_CONSEC_PEEP_IMM_DEC_ldr64f" (cat log | ack "LDP_CONSEC_PEEP_IMM_DEC_ldr64f" | wc -l) -echo "LDP_FORW_SPACED_PEEP_IMM_INC_ldr32f" (cat log | ack "LDP_FORW_SPACED_PEEP_IMM_INC_ldr32f" | wc -l) -echo "LDP_FORW_SPACED_PEEP_IMM_INC_ldr64f" (cat log | ack "LDP_FORW_SPACED_PEEP_IMM_INC_ldr64f" | wc -l) -echo "LDP_FORW_SPACED_PEEP_IMM_DEC_ldr32f" (cat log | ack "LDP_FORW_SPACED_PEEP_IMM_DEC_ldr32f" | wc -l) -echo "LDP_FORW_SPACED_PEEP_IMM_DEC_ldr64f" (cat log | ack "LDP_FORW_SPACED_PEEP_IMM_DEC_ldr64f" | wc -l) -echo "LDP_BACK_SPACED_PEEP_IMM_INC_ldr32f" (cat log | ack "LDP_BACK_SPACED_PEEP_IMM_INC_ldr32f" | wc -l) -echo "LDP_BACK_SPACED_PEEP_IMM_INC_ldr64f" (cat log | ack "LDP_BACK_SPACED_PEEP_IMM_INC_ldr64f" | wc -l) -echo "LDP_BACK_SPACED_PEEP_IMM_DEC_ldr32f" (cat log | ack "LDP_BACK_SPACED_PEEP_IMM_DEC_ldr32f" | wc -l) -echo "LDP_BACK_SPACED_PEEP_IMM_DEC_ldr64f" (cat log | ack "LDP_BACK_SPACED_PEEP_IMM_DEC_ldr64f" | wc -l) -echo "\n" -echo "STP_CONSEC_PEEP_IMM_INC_str32" (cat log | ack "STP_CONSEC_PEEP_IMM_INC_str32" | wc -l) -echo "STP_CONSEC_PEEP_IMM_INC_str64" (cat log | ack "STP_CONSEC_PEEP_IMM_INC_str64" | wc -l) -echo "STP_FORW_SPACED_PEEP_IMM_INC_str32" (cat log | ack "STP_FORW_SPACED_PEEP_IMM_INC_str32" | wc -l) -echo "STP_FORW_SPACED_PEEP_IMM_INC_str64" (cat log | ack "STP_FORW_SPACED_PEEP_IMM_INC_str64" | wc -l) -echo "STP_BACK_SPACED_PEEP_IMM_INC_str32" (cat log | ack "STP_BACK_SPACED_PEEP_IMM_INC_str32" | wc -l) -echo "STP_BACK_SPACED_PEEP_IMM_INC_str64" (cat log | ack "STP_BACK_SPACED_PEEP_IMM_INC_str64" | wc -l) -echo "\n" -echo "STP_CONSEC_PEEP_IMM_INC_str32f" (cat log | ack "STP_CONSEC_PEEP_IMM_INC_str32f" | wc -l) -echo "STP_CONSEC_PEEP_IMM_INC_str64f" (cat log | ack "STP_CONSEC_PEEP_IMM_INC_str64f" | wc -l) -echo "STP_FORW_SPACED_PEEP_IMM_INC_str32f" (cat log | ack "STP_FORW_SPACED_PEEP_IMM_INC_str32f" | wc -l) -echo "STP_FORW_SPACED_PEEP_IMM_INC_str64f" (cat log | ack "STP_FORW_SPACED_PEEP_IMM_INC_str64f" | wc -l) -echo "STP_BACK_SPACED_PEEP_IMM_INC_str32f" (cat log | ack "STP_BACK_SPACED_PEEP_IMM_INC_str32f" | wc -l) -echo "STP_BACK_SPACED_PEEP_IMM_INC_str64f" (cat log | ack "STP_BACK_SPACED_PEEP_IMM_INC_str64f" | wc -l) diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v index aa2e0885..304e45a8 100644 --- a/kvx/Asmvliw.v +++ b/kvx/Asmvliw.v @@ -313,7 +313,12 @@ Inductive cf_instruction : Type := . (** *** Loads *) -Definition concrete_default_notrap_load_value (chunk : memory_chunk) := +Definition concrete_default_notrap_load_value (chunk : memory_chunk) := Vundef. + +(* What follows was the original spec, but is subtly incorrect. + Our definition of the assembly-level memory model is already an abstraction of the real world. + In particular, we consider that a load is incorrect when it points outside of CompCert's visible memory, whereas this memory could be correct at the assembly level. + This means that CompCert would believe an incorrect load would yield 0 whereas it would yield another value. match chunk with | Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned | Mint32 => Vint Int.zero @@ -321,7 +326,7 @@ Definition concrete_default_notrap_load_value (chunk : memory_chunk) := | Many32 | Many64 => Vundef | Mfloat32 => Vsingle Float32.zero | Mfloat64 => Vfloat Float.zero - end. + end. *) Inductive load_name : Type := | Plb (**r load byte *) diff --git a/lib/Integers.v b/lib/Integers.v index 3e103ab7..2addc78b 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -3747,8 +3747,7 @@ Proof. unfold lt. rewrite signed_zero. rewrite bits_zero. - destruct (zlt _ _); try lia. - reflexivity. + destruct (zlt _ _); try lia; reflexivity. } change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i + 63)). rewrite bits_zero. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 6abde89f..42ab8375 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -821,18 +821,18 @@ Proof. unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. unfold Int.lt. rewrite zlt_false. auto. change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed. - generalize (Int.signed_range i); omega. + generalize (Int.signed_range i); lia. * exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). exists rs1; split. eexact A1. split; auto. rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto. unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int.add_signed. symmetry; apply Int.signed_repr. assert (Int.signed n <> Int.max_signed). { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. + generalize (Int.signed_range n); lia. + apply DFL. + apply DFL. Qed. @@ -919,18 +919,18 @@ Proof. unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. unfold Int64.lt. rewrite zlt_false. auto. change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed. - generalize (Int64.signed_range i); omega. + generalize (Int64.signed_range i); lia. * exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). exists rs1; split. eexact A1. split; auto. rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto. unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. assert (Int64.signed n <> Int64.max_signed). { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. + generalize (Int64.signed_range n); lia. + apply DFL. + apply DFL. Qed. diff --git a/runtime/Makefile b/runtime/Makefile index 6f70fa87..ff51b7d7 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -1,5 +1,7 @@ include ../Makefile.config +.PRECIOUS: .s + CFLAGS=-O1 -Wall ifeq ($(ARCH),x86) diff --git a/test/gourdinl/compare_pp.sh b/test/gourdinl/compare_pp.sh new file mode 100755 index 00000000..09183cf9 --- /dev/null +++ b/test/gourdinl/compare_pp.sh @@ -0,0 +1,16 @@ +ffname=$(basename $1) +fname=${ffname%.*} +nopp=$fname.nopp.s +pp=$fname.pp.s + +../../ccomp -fno-coalesce-mem -fno-postpass -S $1 -o $nopp +../../ccomp -fno-coalesce-mem -fpostpass= list -S $1 -o $pp +sed -i '1,2d' $nopp +sed -i '1,2d' $pp +if cmp -s $nopp $pp; then + echo "same!" +else + echo "differents!" + diff -y $nopp $pp +fi + diff --git a/test/gourdinl/postpass_exp.c b/test/gourdinl/postpass_exp.c new file mode 100644 index 00000000..522ac2a6 --- /dev/null +++ b/test/gourdinl/postpass_exp.c @@ -0,0 +1,5 @@ +int main(int x, int y) { + int z = x << 32; + y = y - z; + return x + y; +} diff --git a/test/monniaux/cycles.h b/test/monniaux/cycles.h index f26060a7..2905938b 100644 --- a/test/monniaux/cycles.h +++ b/test/monniaux/cycles.h @@ -6,7 +6,7 @@ typedef uint64_t cycle_t; #define PRcycle PRId64 -#include <../../kvx-cos/include/hal/cos_registers.h> +#include "/opt/kalray/accesscore/kvx-cos/include/hal/cos_registers.h" static inline void cycle_count_config(void) { diff --git a/test/monniaux/division/harness.c b/test/monniaux/division/harness.c new file mode 100644 index 00000000..b6ce674d --- /dev/null +++ b/test/monniaux/division/harness.c @@ -0,0 +1,82 @@ +#include <stdint.h> +#include <inttypes.h> +#include <stdio.h> +#include <math.h> +#include <assert.h> +#include "../cycles.h" + +static uint32_t dm_random_uint32(void) { + static uint32_t current=UINT32_C(0xDEADBEEF); + current = ((uint64_t) current << 6) % UINT32_C(4294967291); + return current; +} + +static uint64_t dm_biased_random_uint32(void) { + uint32_t flags = dm_random_uint32(); + uint32_t r; + switch (flags & 15) { + case 0: + r = dm_random_uint32() & 0xFU; + break; + case 1: + r = dm_random_uint32() & 0xFFU; + break; + case 2: + r = dm_random_uint32() & 0xFFFU; + break; + case 3: + r = dm_random_uint32() & 0xFFFFU; + break; + case 4: + r = dm_random_uint32() & 0xFFFFFU; + break; + case 5: + r = dm_random_uint32() & 0xFFFFFFU; + break; + case 6: + r = dm_random_uint32() & 0xFFFFFFFU; + break; + case 7: + r = dm_random_uint32() & 0x3; + break; + default: + r = dm_random_uint32(); + } + return r; +} + +inline uint32_t native_udiv32(uint32_t x, uint32_t y) { + return x/y; +} +extern uint32_t my_udiv32(uint32_t x, uint32_t y); + +int main() { + cycle_t time_me=0, time_native=0; + cycle_count_config(); + + for(int i=0; i<1000; i++) { + uint32_t x = dm_biased_random_uint32(); + uint32_t y = dm_biased_random_uint32(); + if (y == 0) continue; + + cycle_t cycle_a, cycle_b, cycle_c; + + uint32_t q1, q2; + cycle_a = get_cycle(); + q1 = native_udiv32(x, y); + cycle_b = get_cycle(); + q2 = my_udiv32(x, y); + cycle_c = get_cycle(); + + if(q1 != q2) { + printf("ERREUR %u %u\n", q1, q2); + } + + time_native += cycle_b - cycle_a; + time_me += cycle_c - cycle_b; + } + + printf("%" PRcycle "\t%" PRcycle "\n", time_native, time_me); + + return 0; +} diff --git a/test/monniaux/division/my_udiv32.s b/test/monniaux/division/my_udiv32.s new file mode 100644 index 00000000..0f4fd127 --- /dev/null +++ b/test/monniaux/division/my_udiv32.s @@ -0,0 +1,36 @@ + .align 8 + .global my_udiv32 + .type my_udiv32, @function +my_udiv32: + zxwd $r1 = $r1 + make $r3 = 0x3ff0000000000000 # 1.0 + zxwd $r0 = $r0 + ;; + floatud.rn $r5 = $r1, 0 + ;; + floatuw.rn $r2 = $r1, 0 + ;; + finvw $r2 = $r2 + ;; + + fwidenlwd $r2 = $r2 + floatud.rn $r4 = $r0, 0 + ;; + ffmsd $r3 = $r2, $r5 + ;; + ffmad $r2 = $r2, $r3 + ;; + fmuld $r2 = $r2, $r4 + ;; + fixedud.rn $r2 = $r2, 0 + ;; + msbfw $r0 = $r2, $r1 + zxwd $r1 = $r2 + addw $r2 = $r2, -1 + ;; + cmoved.wltz $r0? $r1 = $r2 + ;; + copyd $r0 = $r1 + ret + ;; + .size my_udiv32, .-my_udiv32 diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 2000f96a..00e70f65 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -95,9 +95,6 @@ let z oc n = output_string oc (Z.to_string n) let data_pointer = if Archi.ptr64 then ".quad" else ".long" -(* The comment deliminiter *) -let comment = "#" - (* Base-2 log of a Caml integer *) let rec log2 n = assert (n > 0); @@ -106,6 +103,7 @@ let rec log2 n = (* System dependent printer functions *) module type SYSTEM = sig + val comment: string val raw_symbol: out_channel -> string -> unit val symbol: out_channel -> P.t -> unit val label: out_channel -> int -> unit @@ -124,6 +122,9 @@ module type SYSTEM = module ELF_System : SYSTEM = struct + (* The comment delimiter *) + let comment = "#" + let raw_symbol oc s = fprintf oc "%s" s @@ -219,6 +220,10 @@ module ELF_System : SYSTEM = module MacOS_System : SYSTEM = struct + (* The comment delimiter. + `##` instead of `#` to please the Clang assembler. *) + let comment = "##" + let raw_symbol oc s = fprintf oc "_%s" s @@ -280,6 +285,9 @@ module MacOS_System : SYSTEM = module Cygwin_System : SYSTEM = struct + (* The comment delimiter *) + let comment = "#" + let symbol_prefix = if Archi.ptr64 then "" else "_" |