From 1cd64f429262ac333021571ef60bea1e1d7fe57a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sun, 6 Jun 2021 15:50:24 +0200
Subject: omega -> lia

---
 scheduling/RTLpath.v              | 43 ++++++++++++++++++++-------------------
 scheduling/RTLpathSE_simu_specs.v | 11 +++++-----
 2 files changed, 28 insertions(+), 26 deletions(-)

diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v
index 2f73f1fa..a4fce97e 100644
--- a/scheduling/RTLpath.v
+++ b/scheduling/RTLpath.v
@@ -26,6 +26,7 @@ Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import Op Registers.
 Require Import RTL Linking.
+Require Import Lia.
 
 Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
          (at level 200, X ident, A at level 100, B at level 200)
@@ -582,8 +583,8 @@ Lemma wellformed_suffix_path c pm path path':
    exists pc', nth_default_succ c (path-path') pc = Some pc' /\ wellformed_path c pm path' pc'.
 Proof.
   induction 1 as [|m].
-  + intros. enough (path'-path'=0)%nat as ->; [simpl;eauto|omega].
-  + intros pc WF; enough (S m-path'=S (m-path'))%nat as ->; [simpl;eauto|omega].
+  + intros. enough (path'-path'=0)%nat as ->; [simpl;eauto|lia].
+  + intros pc WF; enough (S m-path'=S (m-path'))%nat as ->; [simpl;eauto|lia].
     inversion WF; subst; clear WF; intros; simplify_someHyps.
     intros; simplify_someHyps; eauto.
 Qed.
@@ -600,9 +601,9 @@ Proof.
   intros; exploit fn_path_wf; eauto.
   intro WF.
   set (ps:=path.(psize)).
-  exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps O); omega || eauto.
+  exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps O); lia || eauto.
   destruct 1 as (pc' & NTH_SUCC & WF'); auto.
-  assert (ps - 0 = ps)%nat as HH by omega. rewrite HH in NTH_SUCC. clear HH.
+  assert (ps - 0 = ps)%nat as HH by lia. rewrite HH in NTH_SUCC. clear HH.
   unfold nth_default_succ_inst.
   inversion WF'; clear WF'; subst. simplify_someHyps; eauto.
 Qed.
@@ -617,11 +618,11 @@ Lemma internal_node_path path f path0 pc:
 Proof.
   intros; exploit fn_path_wf; eauto.
   set (ps:=path0.(psize)).
-  intro WF; exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps (ps-path)); eauto. { omega. }
+  intro WF; exploit (wellformed_suffix_path (fn_code f) (fn_path f) ps (ps-path)); eauto. { lia. }
   destruct 1 as (pc' & NTH_SUCC & WF').
-  assert (ps - (ps - path) = path)%nat as HH by omega. rewrite HH in NTH_SUCC. clear HH.
+  assert (ps - (ps - path) = path)%nat as HH by lia. rewrite HH in NTH_SUCC. clear HH.
   unfold nth_default_succ_inst. 
-  inversion WF'; clear WF'; subst. { omega. }
+  inversion WF'; clear WF'; subst. { lia. }
   simplify_someHyps; eauto.
 Qed.
 
@@ -706,7 +707,7 @@ Proof.
       rewrite CONT. auto.
     + intros; try_simplify_someHyps; try congruence.
       eexists. exists i. exists O; simpl. intuition eauto.
-      omega.
+      lia.
 Qed.
 
 Lemma isteps_resize ge path0 path1 f sp rs m pc st: 
@@ -837,15 +838,15 @@ Lemma stuttering path idx stack f sp rs m pc st t s1':
    RTL.step ge (State stack f sp st.(ipc) st.(irs) st.(imem)) t s1' ->
    t = E0 /\ match_inst_states idx s1' (State stack f sp pc rs m).
 Proof.
-  intros PSTEP PATH BOUND CONT RSTEP; exploit (internal_node_path (path.(psize)-(S idx))); omega || eauto.
+  intros PSTEP PATH BOUND CONT RSTEP; exploit (internal_node_path (path.(psize)-(S idx))); lia || eauto.
   intros (i & pc' & Hi & Hpc & DUM).
   unfold nth_default_succ_inst in Hi.
   erewrite isteps_normal_exit in Hi; eauto.
   exploit istep_complete; congruence || eauto.
   intros (SILENT & st0 & STEP0 & EQ).
   intuition; subst; unfold match_inst_states; simpl.
-  intros; refine (State_match _ _ path stack f sp pc rs m _ PATH _ _ _); simpl; omega || eauto.
-  set (ps:=path.(psize)). enough (ps - idx = S (ps - (S idx)))%nat as ->; try omega.
+  intros; refine (State_match _ _ path stack f sp pc rs m _ PATH _ _ _); simpl; lia || eauto.
+  set (ps:=path.(psize)). enough (ps - idx = S (ps - (S idx)))%nat as ->; try lia.
   erewrite <- isteps_step_right; eauto.
 Qed.
 
@@ -874,7 +875,7 @@ Proof.
     destruct (initialize_path (*fn_code f*) (fn_path f) (ipc st0)) as (path0 & Hpath0); eauto.
     exists (path0.(psize)); intuition eauto.
     econstructor; eauto.
-    * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
+    * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
     * simpl; eauto.
   + generalize Hi; inversion RSTEP; clear RSTEP; subst; (repeat (simplify_someHyp; simpl in * |- * )); try congruence; eauto.
     - (* Icall *)
@@ -897,7 +898,7 @@ Proof.
       destruct (initialize_path (*fn_code f*) (fn_path f) pc') as (path0 & Hpath0); eauto.
       exists path0.(psize); intuition eauto.
       econstructor; eauto.
-      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
+      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
       * simpl; eauto.
    - (* Ijumptable *)
       intros; exploit exec_Ijumptable; eauto.
@@ -906,7 +907,7 @@ Proof.
       destruct (initialize_path (*fn_code f*) (fn_path f) pc') as (path0 & Hpath0); eauto.
       exists path0.(psize); intuition eauto.
       econstructor; eauto.
-      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || omega.
+      * enough (path0.(psize)-path0.(psize)=0)%nat as ->; simpl; eauto || lia.
       * simpl; eauto.
   - (* Ireturn *)
       intros; exploit exec_Ireturn; eauto.
@@ -933,7 +934,7 @@ Proof.
   intros PSTEP PATH BOUND RSTEP WF; destruct (st.(icontinue)) eqn: CONT.
   destruct idx as [ | idx].
   + (* path_step on normal_exit *)
-     assert (path.(psize)-0=path.(psize))%nat as HH by omega. rewrite HH in PSTEP. clear HH.
+     assert (path.(psize)-0=path.(psize))%nat as HH by lia. rewrite HH in PSTEP. clear HH.
      exploit normal_exit; eauto.
      intros (s2' & LSTEP & (idx' & MATCH)).
      exists idx'; exists s2'; intuition eauto.
@@ -942,7 +943,7 @@ Proof.
     unfold match_states; exists idx; exists (State stack f sp pc rs m); 
     intuition.
   + (* one or two path_step on early_exit *)
-    exploit (isteps_resize ge (path.(psize) - idx)%nat path.(psize)); eauto; try omega.
+    exploit (isteps_resize ge (path.(psize) - idx)%nat path.(psize)); eauto; try lia.
     clear PSTEP; intros PSTEP.
     (* TODO for clarification: move the assert below into a separate lemma *)
     assert (HPATH0: exists path0, (fn_path f)!(ipc st) = Some path0).
@@ -952,7 +953,7 @@ Proof.
       exploit istep_early_exit; eauto.
       intros (X1 & X2 & EARLY_EXIT).
       destruct st as [cont pc0 rs0 m0]; simpl in * |- *; intuition subst.
-      exploit (internal_node_path path0); omega || eauto.
+      exploit (internal_node_path path0); lia || eauto.
       intros (i' & pc' & Hi' & Hpc' & ENTRY).
       unfold nth_default_succ_inst in Hi'.
       erewrite isteps_normal_exit in Hi'; eauto.
@@ -974,8 +975,8 @@ Proof.
       - simpl; eauto.
     * (* single step case *)
       exploit (stuttering path1 ps stack f sp (irs st) (imem st) (ipc st)); simpl; auto.
-      - { rewrite Hpath1size; enough (S ps-S ps=0)%nat as ->; try omega.  simpl; eauto. }
-      - omega.
+      - { rewrite Hpath1size; enough (S ps-S ps=0)%nat as ->; try lia.  simpl; eauto. }
+      - lia.
       - simpl; eauto.
       - simpl; eauto.
       - intuition subst.
@@ -1000,7 +1001,7 @@ Proof.
       exists path.(psize). constructor; auto.
       econstructor; eauto.
       - set (ps:=path.(psize)). enough (ps-ps=O)%nat as ->; simpl; eauto.
-        omega.
+        lia.
       - simpl; auto.
   + (* exec_function_external *)
     destruct f; simpl in H3 |-; inversion H3; subst; clear H3.
@@ -1019,7 +1020,7 @@ Proof.
       exists path.(psize). constructor; auto.
       econstructor; eauto.
       - set (ps:=path.(psize)). enough (ps-ps=O)%nat as ->; simpl; eauto.
-        omega.
+        lia.
       - simpl; auto.
 Qed.
 
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v
index 4bb3e18e..5051d805 100644
--- a/scheduling/RTLpathSE_simu_specs.v
+++ b/scheduling/RTLpathSE_simu_specs.v
@@ -7,6 +7,7 @@ Require Import RTL RTLpath.
 Require Import Errors.
 Require Import RTLpathSE_theory RTLpathLivegenproof.
 Require Import Axioms.
+Require Import Lia.
 
 Local Open Scope error_monad_scope.
 Local Open Scope option_monad_scope.
@@ -666,7 +667,7 @@ Proof.
   induction l2.
   - intro. destruct l1; auto. apply is_tail_false in H. contradiction.
   - intros ITAIL. inv ITAIL; auto.
-    apply IHl2 in H1. clear IHl2. simpl. omega.
+    apply IHl2 in H1. clear IHl2. simpl. lia.
 Qed.
 
 Lemma is_tail_nth_error {A} (l1 l2: list A) x:
@@ -676,14 +677,14 @@ Proof.
   induction l2.
   - intro ITAIL. apply is_tail_false in ITAIL. contradiction.
   - intros ITAIL. assert (length (a::l2) = S (length l2)) by auto. rewrite H. clear H.
-    assert (forall n n', ((S n) - n' - 1)%nat = (n - n')%nat) by (intros; omega). rewrite H. clear H.
+    assert (forall n n', ((S n) - n' - 1)%nat = (n - n')%nat) by (intros; lia). rewrite H. clear H.
     inv ITAIL.
-    + assert (forall n, (n - n)%nat = 0%nat) by (intro; omega). rewrite H.
+    + assert (forall n, (n - n)%nat = 0%nat) by (intro; lia). rewrite H.
       simpl. reflexivity.
     + exploit IHl2; eauto. intros. clear IHl2.
-      assert (forall n n', (n > n')%nat -> (n - n')%nat = S (n - n' - 1)%nat) by (intros; omega).
+      assert (forall n n', (n > n')%nat -> (n - n')%nat = S (n - n' - 1)%nat) by (intros; lia).
       exploit (is_tail_length (x::l1)); eauto. intro. simpl in H2.
-      assert ((length l2 > length l1)%nat) by omega. clear H2.
+      assert ((length l2 > length l1)%nat) by lia. clear H2.
       rewrite H0; auto.
 Qed.
 
-- 
cgit 


From c21c794ec0abb307ff4d0948e2a504da936ea602 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 7 Jun 2021 14:42:48 +0200
Subject: timing

---
 test/monniaux/division/harness.c   | 81 ++++++++++++++++++++++++++++++++++++++
 test/monniaux/division/my_udiv32.s | 36 +++++++++++++++++
 2 files changed, 117 insertions(+)
 create mode 100644 test/monniaux/division/harness.c
 create mode 100644 test/monniaux/division/my_udiv32.s

diff --git a/test/monniaux/division/harness.c b/test/monniaux/division/harness.c
new file mode 100644
index 00000000..8d7e7d13
--- /dev/null
+++ b/test/monniaux/division/harness.c
@@ -0,0 +1,81 @@
+#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();
+
+    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("%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
-- 
cgit 


From f0124301f874520bfdf76f16e016ffb2e1a8ca37 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 7 Jun 2021 14:47:57 +0200
Subject: division

---
 test/monniaux/cycles.h           | 2 +-
 test/monniaux/division/harness.c | 5 +++--
 2 files changed, 4 insertions(+), 3 deletions(-)

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
index 8d7e7d13..b6ce674d 100644
--- a/test/monniaux/division/harness.c
+++ b/test/monniaux/division/harness.c
@@ -57,7 +57,8 @@ int main() {
   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;
@@ -68,7 +69,7 @@ int main() {
     cycle_c = get_cycle();
 
     if(q1 != q2) {
-      printf("%u %u\n", q1, q2);
+      printf("ERREUR %u %u\n", q1, q2);
     }
     
     time_native += cycle_b - cycle_a;
-- 
cgit 


From a14865049571f157896107ebf0b2f908b1b95cbc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 7 Jun 2021 22:45:39 +0200
Subject: coq 8.13.2

---
 lib/Integers.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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.
-- 
cgit 


From dbff5b8a016fe9f6667ea007be3de764a50b620a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 8 Jun 2021 00:30:31 +0200
Subject: omega -> lia

---
 riscV/Asmgenproof1.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

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.
-- 
cgit 


From 2bf707f9fe5259f869999347a46ec52ab096e030 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 8 Jun 2021 01:06:09 +0200
Subject: run CI on kvx-work-ssa kvx-work-velus

---
 .gitlab-ci.yml | 106 +++++++++++++++++++++++++++++++--------------------------
 1 file changed, 57 insertions(+), 49 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index a7811ae3..9f407912 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -14,7 +14,7 @@ check-admitted:
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
       when: always
-    - if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
+    - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
       when: always
     - if: '$CI_COMMIT_BRANCH == "master"'
       when: always
@@ -35,7 +35,7 @@ build_x86_64:
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
       when: always
-    - if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
+    - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
       when: always
     - if: '$CI_COMMIT_BRANCH == "master"'
       when: always
@@ -58,7 +58,7 @@ build_ia32:
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
       when: always
-    - if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
+    - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
       when: always
     - if: '$CI_COMMIT_BRANCH == "master"'
       when: always
@@ -83,7 +83,7 @@ build_aarch64:
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
       when: always
-    - if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
+    - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
       when: always
     - if: '$CI_COMMIT_BRANCH == "master"'
       when: always
@@ -108,7 +108,9 @@ build_arm:
   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
@@ -134,53 +136,55 @@ build_armhf:
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
       when: always
-    - if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
-      when: always
-    - if: '$CI_COMMIT_BRANCH == "master"'
-      when: always
-    - when: manual
-
-build_ppc:
-  stage: build
-  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
-    - eval `opam config env`
-    - opam update
-    - opam install -y menhir
-  script:
-    - ./config_ppc.sh
-    - make -j "$NJOBS"
-  rules:
-    - if: '$CI_COMMIT_BRANCH == "kvx-work"'
+    - if: '$CI_COMMIT_BRANCH == "kvx-work-ssa"'
       when: always
-    - if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
+    - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
       when: always
     - if: '$CI_COMMIT_BRANCH == "master"'
       when: always
     - when: manual
 
-build_ppc64:
-  stage: build
-  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-powerpc64-linux-gnu
-    - eval `opam config env`
-    - opam update
-    - opam install -y menhir
-  script:
-    - ./config_ppc64.sh
-    - make -j "$NJOBS"
-  rules:
-    - if: '$CI_COMMIT_BRANCH == "kvx-work"'
-      when: always
-    - if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
-      when: always
-    - if: '$CI_COMMIT_BRANCH == "master"'
-      when: always
-    - when: manual
+# build_ppc:
+#   stage: build
+#   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
+#     - eval `opam config env`
+#     - opam update
+#     - opam install -y menhir
+#   script:
+#     - ./config_ppc.sh
+#     - make -j "$NJOBS"
+#   rules:
+#     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
+#       when: always
+#     - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
+#       when: always
+#     - if: '$CI_COMMIT_BRANCH == "master"'
+#       when: always
+#     - when: manual
+
+# build_ppc64:
+#   stage: build
+#   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-powerpc64-linux-gnu
+#     - eval `opam config env`
+#     - opam update
+#     - opam install -y menhir
+#   script:
+#     - ./config_ppc64.sh
+#     - make -j "$NJOBS"
+#   rules:
+#     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
+#       when: always
+#     - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
+#       when: always
+#     - if: '$CI_COMMIT_BRANCH == "master"'
+#       when: always
+#     - when: manual
 
 build_rv64:
   stage: build
@@ -201,7 +205,7 @@ build_rv64:
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
       when: always
-    - if: '$CI_COMMIT_BRANCH == "mppa-kvx"'
+    - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
       when: always
     - if: '$CI_COMMIT_BRANCH == "master"'
       when: always
@@ -222,7 +226,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 +255,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
-- 
cgit 


From 9fdd2f1d82387950bd72f865920f189d756109d9 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 9 Jun 2021 10:24:47 +0200
Subject: MacOS compatibility

---
 config_simple.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 ;
-- 
cgit 


From cfd5e458e8fb8a92db60e90b40c9889e370f116b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 9 Jun 2021 13:24:24 +0200
Subject: comment is now ## due to some weird MacOS bug

---
 x86/TargetPrinter.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 2000f96a..50c871e4 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -96,7 +96,7 @@ 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 = "#"
+let comment = "##"
 
 (* Base-2 log of a Caml integer *)
 let rec log2 n =
-- 
cgit 


From 2a650bdab340d7a31cdc224f7e7ad1673b248af1 Mon Sep 17 00:00:00 2001
From: Olivier Lebeltel <olivier.lebeltel@univ-grenoble-alpes.fr>
Date: Wed, 9 Jun 2021 13:58:13 +0200
Subject: added config_macos_x86_64.sh

---
 config_macos_x86_64.sh | 1 +
 1 file changed, 1 insertion(+)
 create mode 100755 config_macos_x86_64.sh

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 "$@"
-- 
cgit 


From d703ae1ad5e1fcdc63e07b2a50a3e8576a11e61e Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 9 Jun 2021 23:54:07 +0200
Subject: push afadl test example

---
 test/gourdinl/compare_pp.sh  | 16 ++++++++++++++++
 test/gourdinl/postpass_exp.c |  5 +++++
 2 files changed, 21 insertions(+)
 create mode 100755 test/gourdinl/compare_pp.sh
 create mode 100644 test/gourdinl/postpass_exp.c

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;
+}
-- 
cgit 


From a0ad5ff6f9c7603610a7448935b36c9ed22c6435 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 10 Jun 2021 18:33:58 +0200
Subject: x86 assembly: fix the comment delimiter for macos and make it per-OS

As reported in #399, it seems better to use `##` instead of `#` as
comment delimiter under macOS.

For the time being we keep using `#` for Linux and Cygwin.

Closes: #399
---
 x86/TargetPrinter.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 1b27ee73..5bc2be1c 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
 
@@ -180,6 +181,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
 
@@ -239,6 +244,9 @@ module MacOS_System : SYSTEM =
 module Cygwin_System : SYSTEM =
   struct
 
+    (* The comment delimiter *)
+    let comment = "#"
+
     let symbol_prefix =
       if Archi.ptr64 then "" else "_"
 
-- 
cgit 


From 146320253dffbcb348a1651cf73eea9ff96355ae Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Thu, 10 Jun 2021 18:36:57 +0200
Subject: remove filter file

---
 filter_peeplog.fish | 39 ---------------------------------------
 1 file changed, 39 deletions(-)
 delete mode 100755 filter_peeplog.fish

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)
-- 
cgit 


From 2c56ce62c6bfd59aabccbb0df47b8247375556b4 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Jun 2021 13:28:12 +0200
Subject: add PPC to CI and remove ugly hack for qemu linker paths

---
 .gitlab-ci.yml | 118 ++++++++++++++++++++++++++++++---------------------------
 1 file changed, 62 insertions(+), 56 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 9f407912..9eac61a0 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -14,6 +14,8 @@ check-admitted:
   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"'
@@ -35,6 +37,8 @@ build_x86_64:
   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"'
@@ -58,6 +62,8 @@ build_ia32:
   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"'
@@ -76,13 +82,13 @@ 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 CCOMPOPTS='-static' SIMU='qemu-aarch64' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu/lib' all test
+    - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='aarch64-linux-gnu-gcc' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu/lib' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
   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"'
@@ -101,10 +107,8 @@ 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 CCOMPOPTS=-static SIMU='qemu-arm' 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
@@ -129,10 +133,8 @@ 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 CCOMPOPTS=-static SIMU='qemu-arm' 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
@@ -144,47 +146,51 @@ build_armhf:
       when: always
     - when: manual
 
-# build_ppc:
-#   stage: build
-#   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
-#     - eval `opam config env`
-#     - opam update
-#     - opam install -y menhir
-#   script:
-#     - ./config_ppc.sh
-#     - make -j "$NJOBS"
-#   rules:
-#     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
-#       when: always
-#     - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
-#       when: always
-#     - if: '$CI_COMMIT_BRANCH == "master"'
-#       when: always
-#     - when: manual
+build_ppc:
+  stage: build
+  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
+    - eval `opam config env`
+    - opam update
+    - opam install -y menhir
+  script:
+    - ./config_ppc.sh
+    - make -j "$NJOBS"
+    - make -C test CCOMPOPTS=-static SIMU='qemu-ppc' 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' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32
+  rules:
+    - if: '$CI_COMMIT_BRANCH == "kvx-work"'
+      when: always
+    - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
+      when: always
+    - if: '$CI_COMMIT_BRANCH == "master"'
+      when: always
+    - when: manual
 
-# build_ppc64:
-#   stage: build
-#   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-powerpc64-linux-gnu
-#     - eval `opam config env`
-#     - opam update
-#     - opam install -y menhir
-#   script:
-#     - ./config_ppc64.sh
-#     - make -j "$NJOBS"
-#   rules:
-#     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
-#       when: always
-#     - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
-#       when: always
-#     - if: '$CI_COMMIT_BRANCH == "master"'
-#       when: always
-#     - when: manual
+build_ppc64:
+  stage: build
+  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-powerpc64-linux-gnu
+    - eval `opam config env`
+    - opam update
+    - opam install -y menhir
+  script:
+    - ./config_ppc64.sh
+    - make -j "$NJOBS"
+    - make -C test CCOMPOPTS=-static SIMU='qemu-ppc64' 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-ppc -L /usr/powerpc64-linux-gnu -cpu 7400' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32
+  rules:
+    - if: '$CI_COMMIT_BRANCH == "kvx-work"'
+      when: always
+    - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
+      when: always
+    - if: '$CI_COMMIT_BRANCH == "master"'
+      when: always
+    - when: manual
 
 build_rv64:
   stage: build
@@ -198,13 +204,13 @@ 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 CCOMPOPTS=-static SIMU='qemu-riscv64' 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 == "kvx-work-ssa"'
+      when: always
     - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
       when: always
     - if: '$CI_COMMIT_BRANCH == "master"'
-- 
cgit 


From 9c91b4daf1632dfe295748fc19ebedf0b93985b7 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Jun 2021 13:47:25 +0200
Subject: path issues

---
 .gitlab-ci.yml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 9eac61a0..b3558971 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -82,7 +82,7 @@ build_aarch64:
   script:
     - ./config_aarch64.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS='-static' SIMU='qemu-aarch64' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu/lib' all test
+    - make -C test CCOMPOPTS='-static' SIMU='qemu-aarch64 -L /usr/aarch64-linux-gnu/lib' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu/lib' all test
     - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='aarch64-linux-gnu-gcc' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu/lib' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
@@ -107,7 +107,7 @@ build_arm:
   script:
     - ./config_arm.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS=-static SIMU='qemu-arm' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabi' all test
+    - make -C test CCOMPOPTS=-static 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"'
@@ -133,7 +133,7 @@ build_armhf:
   script:
     - ./config_armhf.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS=-static SIMU='qemu-arm' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabihf' all test
+    - make -C test CCOMPOPTS=-static 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"'
@@ -158,7 +158,7 @@ build_ppc:
   script:
     - ./config_ppc.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS=-static SIMU='qemu-ppc' EXECUTE='qemu-ppc -L /usr/powerpc-linux-gnu -cpu 7400' all test
+    - make -C test CCOMPOPTS=-static 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' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
@@ -181,7 +181,7 @@ build_ppc64:
   script:
     - ./config_ppc64.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS=-static SIMU='qemu-ppc64' EXECUTE='qemu-ppc64 -L /usr/powerpc64-linux-gnu -cpu 7400' all test
+    - make -C test CCOMPOPTS=-static 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-ppc -L /usr/powerpc64-linux-gnu -cpu 7400' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
@@ -204,7 +204,7 @@ build_rv64:
   script:
     - ./config_rv64.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS=-static SIMU='qemu-riscv64' EXECUTE='qemu-riscv64 -L /usr/riscv64-linux-gnu' all test
+    - make -C test CCOMPOPTS=-static 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"'
-- 
cgit 


From 2affa0523a16284316d88b6d2c32638b0a8dea88 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Jun 2021 13:50:32 +0200
Subject: don't use -static on ppc

---
 .gitlab-ci.yml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b3558971..cd864546 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -158,8 +158,8 @@ build_ppc:
   script:
     - ./config_ppc.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS=-static 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' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32
+    - 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
@@ -181,8 +181,8 @@ build_ppc64:
   script:
     - ./config_ppc64.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS=-static 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-ppc -L /usr/powerpc64-linux-gnu -cpu 7400' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32
+    - 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-ppc -L /usr/powerpc64-linux-gnu -cpu 7400' BITS=32
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
       when: always
-- 
cgit 


From efe8ddef663f0eb511ae4303afb7f799f31c3a68 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Jun 2021 14:17:16 +0200
Subject: fix  bad paths

---
 .gitlab-ci.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index cd864546..969ef169 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -82,8 +82,8 @@ build_aarch64:
   script:
     - ./config_aarch64.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS='-static' SIMU='qemu-aarch64 -L /usr/aarch64-linux-gnu/lib' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu/lib' all test
-    - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='aarch64-linux-gnu-gcc' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu/lib' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
+    - make -C test CCOMPOPTS='-static' 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
-- 
cgit 


From f502e3bc8a400b32c19b67052d0b6c96df1d88e4 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Jun 2021 14:37:16 +0200
Subject: disable PPC64; can't link and don't know why

---
 .gitlab-ci.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 969ef169..c9d53c66 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -181,8 +181,8 @@ 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-ppc -L /usr/powerpc64-linux-gnu -cpu 7400' BITS=32
+      #- 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-ppc -L /usr/powerpc64-linux-gnu -cpu 7400' BITS=32
   rules:
     - if: '$CI_COMMIT_BRANCH == "kvx-work"'
       when: always
-- 
cgit 


From d44976886e34a38b2ae36fd5b0dd86ff466ffaff Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Jun 2021 15:18:19 +0200
Subject: compile non yarpgen tests without -static; this should work

---
 .gitlab-ci.yml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index c9d53c66..a52ad5fb 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -82,7 +82,7 @@ build_aarch64:
   script:
     - ./config_aarch64.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS='-static' SIMU='qemu-aarch64 -L /usr/aarch64-linux-gnu' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu' all test
+    - 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"'
@@ -107,7 +107,7 @@ build_arm:
   script:
     - ./config_arm.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS=-static SIMU='qemu-arm -L /usr/arm-linux-gnueabi' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabi' all test
+    - 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"'
@@ -133,7 +133,7 @@ build_armhf:
   script:
     - ./config_armhf.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS=-static SIMU='qemu-arm -L /usr/arm-linux-gnueabihf' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabihf' all test
+    - 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"'
@@ -204,7 +204,7 @@ build_rv64:
   script:
     - ./config_rv64.sh
     - make -j "$NJOBS"
-    - make -C test CCOMPOPTS=-static SIMU='qemu-riscv64 -L /usr/riscv64-linux-gnu' EXECUTE='qemu-riscv64 -L /usr/riscv64-linux-gnu' all test
+    - 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"'
-- 
cgit 


From 293455988549527895a5a79a5d862cb54b217d53 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Jun 2021 15:51:34 +0200
Subject: disable ppc partially

---
 .gitlab-ci.yml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index a52ad5fb..11d7ab58 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -158,11 +158,13 @@ build_ppc:
   script:
     - ./config_ppc.sh
     - make -j "$NJOBS"
-    - 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
+    # problems with float on qemu on CI - 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 == "kvx-work-ssa"'
+      when: always
     - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
       when: always
     - if: '$CI_COMMIT_BRANCH == "master"'
@@ -182,10 +184,12 @@ build_ppc64:
     - ./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-ppc -L /usr/powerpc64-linux-gnu -cpu 7400' BITS=32
+      #- 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 == "kvx-work-ssa"'
+      when: always
     - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
       when: always
     - if: '$CI_COMMIT_BRANCH == "master"'
-- 
cgit 


From f5e95c5647e2c5d3012c613de1c072ca2cbead8d Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Jun 2021 23:49:56 +0200
Subject: show qemu version

---
 .gitlab-ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 11d7ab58..8ebca587 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -158,6 +158,7 @@ build_ppc:
   script:
     - ./config_ppc.sh
     - make -j "$NJOBS"
+    - qemu-ppc --version
     # problems with float on qemu on CI - 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:
-- 
cgit 


From 8c7a5100478611c8278ccef5e06951c831d07ad8 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 12 Jun 2021 01:06:34 +0200
Subject: Use qemu-6.0.0 for PPC as the 3.1.0 version shipping with the Debian
 in the docker has buggy float

Squashed commit of the following:

commit 54d1983cd8d8551c28109a506a752a971897f4ed
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date:   Sat Jun 12 00:48:02 2021 +0200

    sudo make install

commit 49af5c63eff29a49f3cb466a6b6af44570d85352
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date:   Sat Jun 12 00:43:17 2021 +0200

    pixman

commit d78ab98e5751dd3ae0299a3e8c271472ebd8bb63
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date:   Sat Jun 12 00:36:30 2021 +0200

    libglib

commit 0808bf51be42b04c2db4ccc914633407c1309585
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date:   Sat Jun 12 00:31:46 2021 +0200

    don't show verbose untar

commit 972c244c72d9a30fee41dc7cbcc3698a49b6cde6
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date:   Sat Jun 12 00:30:32 2021 +0200

    ninja-build

commit a1c261d01abc1c62ea94d56cfc9cce90887db680
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date:   Sat Jun 12 00:28:14 2021 +0200

    install ninja

commit 92990598283f624d598853851c3edb2650f45b4b
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date:   Sat Jun 12 00:25:17 2021 +0200

    untar

commit a225a0dcea26dd8888be535aa1aec4a58007679d
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date:   Sat Jun 12 00:20:32 2021 +0200

    install wget first

commit 3b2c30ab6a953bde9d09034d38c5919a9425163d
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date:   Sat Jun 12 00:17:09 2021 +0200

    install recent qemu
---
 .gitlab-ci.yml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8ebca587..b3bb418f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -151,7 +151,10 @@ 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
@@ -159,7 +162,7 @@ build_ppc:
     - ./config_ppc.sh
     - make -j "$NJOBS"
     - qemu-ppc --version
-    # problems with float on qemu on CI - 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
+    - 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"'
-- 
cgit 


From 04b2489d7c2a9b0d203b3d431517367a07bd6b30 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 16 Jun 2021 11:39:25 +0200
Subject: fix modeling issue (Vundef for load outside of bounds)

---
 kvx/Asmvliw.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

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 *)
-- 
cgit 


From 8f399dfa9d794f2f728f523ff1aa7788cc3599b2 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 17 Jun 2021 17:04:52 +0200
Subject: fix for Risc-V

---
 aarch64/Machregsaux.mli | 1 +
 riscV/Machregsaux.mli   | 3 +++
 2 files changed, 4 insertions(+)

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/riscV/Machregsaux.mli b/riscV/Machregsaux.mli
index 01b0f9fd..bb3777bf 100644
--- a/riscV/Machregsaux.mli
+++ b/riscV/Machregsaux.mli
@@ -15,3 +15,6 @@
 val is_scratch_register: string -> bool
 
 val class_of_type: AST.typ -> int
+  
+(* Number of registers in each class *)
+val nr_regs : int array
-- 
cgit