Merge branch 'kvx-sched-w-reg-press' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press

16 files changed, 225 insertions, 86 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/aarch64/Machregsaux.mli b/aarch64/Machregsaux.mli
index 8487a557..23ac1c9a 100644
--- a/aarch64/Machregsaux.mli
+++ b/aarch64/Machregsaux.mli
@@ -16,4 +16,5 @@ val is_scratch_register: string -> bool
 
 val class_of_type: AST.typ -> int
 
+(* Number of registers in each class *)
 val nr_regs : int array
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/riscV/Machregsaux.mli b/riscV/Machregsaux.mli
index cf6d7b71..bb3777bf 100644
--- a/riscV/Machregsaux.mli
+++ b/riscV/Machregsaux.mli
@@ -15,5 +15,6 @@
 val is_scratch_register: string -> bool
 
 val class_of_type: AST.typ -> int
-
-val nr_regs: int array
+  
+(* Number of registers in each class *)
+val nr_regs : int array
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 "_"