From ae22df3c5ef0a60527ea85b83bb71e8c95a6ab9c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 11 May 2019 07:59:11 +0200
Subject: Pmsub compiled

---
 mppa_k1c/SelectOp.vp | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 6adcebe5..81e288cb 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -151,6 +151,10 @@ Nondetfunction sub (e1: expr) (e2: expr) :=
       addimm n1 (Eop Osub (t1:::t2:::Enil))
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
+  | t1, (Eop Omul (t2:::t3:::Enil)) =>
+      Eop Omsub (t1:::t2:::t3:::Enil)
+  | t1, (Eop (Omulimm n) (t2:::Enil)) =>
+      Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil)
   | _, _ => Eop Osub (e1:::e2:::Enil)
   end.
 
-- 
cgit 


From 2c428ad4e0177756db2f6dfe56831b5a44f6de5c Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 11 May 2019 15:20:02 +0200
Subject: add with shift, beginning

---
 mppa_k1c/SelectOp.vp | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 81e288cb..ae9d64b9 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -114,6 +114,12 @@ Nondetfunction addimm (n: int) (e: expr) :=
   | _ => Eop (Oaddimm n) (e ::: Enil)
   end.
 
+Definition add_shlimm n e1 e2 :=
+  match shift1_4_of_z (Int.unsigned n) with
+  | Some s14 => Eop (Oaddx s14) (e1:::e2:::Enil)
+  | None => Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil)
+  end.
+
 Nondetfunction add (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 => addimm n1 t2
@@ -135,7 +141,9 @@ Nondetfunction add (e1: expr) (e2: expr) :=
   | t1, (Eop (Omulimm n) (t2:::Enil)) =>
       Eop (Omaddimm n) (t1:::t2:::Enil)
   | (Eop (Omulimm n) (t2:::Enil)), t1 =>
-      Eop (Omaddimm n) (t1:::t2:::Enil)
+    Eop (Omaddimm n) (t1:::t2:::Enil)
+  | (Eop (Oshlimm n) (t1:::Enil)), t2 =>
+    add_shlimm n t1 t2
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 
-- 
cgit 


From a17d3c0419ef5531142c4826d962009c9ba81fbc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 11 May 2019 17:03:50 +0200
Subject: maddx ordre opposé
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mppa_k1c/SelectOp.vp | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index ae9d64b9..61365be2 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -144,6 +144,8 @@ Nondetfunction add (e1: expr) (e2: expr) :=
     Eop (Omaddimm n) (t1:::t2:::Enil)
   | (Eop (Oshlimm n) (t1:::Enil)), t2 =>
     add_shlimm n t1 t2
+  | t2, (Eop (Oshlimm n) (t1:::Enil)) =>
+    add_shlimm n t1 t2
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 
-- 
cgit 


From a095ac045485f5693d937864f7990ab5de427f1d Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 11 May 2019 17:46:45 +0200
Subject: more maddx

---
 mppa_k1c/SelectOp.vp | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 61365be2..9b4cfeb0 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -104,6 +104,12 @@ Definition addrstack (ofs: ptrofs) :=
 
 (** ** Integer addition and pointer addition *)
 
+Definition addimm_shlimm sh k2 e1 :=
+  match shift1_4_of_z (Int.unsigned sh) with
+  | Some s14 => Eop (Oaddximm s14 k2) (e1:::Enil)
+  | None => Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil)
+  end.
+
 Nondetfunction addimm (n: int) (e: expr) :=
   if Int.eq n Int.zero then e else
   match e with
@@ -111,6 +117,8 @@ Nondetfunction addimm (n: int) (e: expr) :=
   | Eop (Oaddrsymbol s m) Enil   => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil
   | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil
   | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
+  | Eop (Oshlimm sh) (t1:::Enil) =>
+    addimm_shlimm sh n t1
   | _ => Eop (Oaddimm n) (e ::: Enil)
   end.
 
-- 
cgit 


From 17a8d91a82f67d7f62f8cbad41ba76a4b0b82a30 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 11 May 2019 20:17:09 +0200
Subject: apply .xs onto addx4 etc

---
 mppa_k1c/SelectOp.vp | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 9b4cfeb0..3427dda3 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -611,13 +611,14 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
      else (Aglobal id ofs, Enil))
   | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil)
   | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
-  | Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) =>
+  | Eop (Oaddxl sh) (e1:::e2:::Enil) =>
+    let zscale := ExtValues.z_of_shift1_4 sh in
+    let scale := Int.repr zscale in
     (if Compopts.optim_fxsaddr tt
-     then let zscale := Int.unsigned scale in
-          if Z.eq_dec zscale (zscale_of_chunk chunk)
-          then (Aindexed2XS zscale, e1:::e2:::Enil) 
-          else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil)
-     else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil))
+     then if Z.eq_dec zscale (zscale_of_chunk chunk)
+          then (Aindexed2XS zscale, e2:::e1:::Enil) 
+          else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil)
+     else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil))
   | Eop Oaddl (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) 
   | _ => (Aindexed Ptrofs.zero, e:::Enil)
   end.
-- 
cgit 


From 66ee59d3dc8a861b468cfaf0ff46fc71dfb8fec2 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 11 May 2019 21:54:18 +0200
Subject: option -faddx (off by default until questions cleared)

---
 mppa_k1c/SelectOp.vp | 29 +++++++++++++++++++++--------
 1 file changed, 21 insertions(+), 8 deletions(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 3427dda3..4d2a948d 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -105,10 +105,13 @@ Definition addrstack (ofs: ptrofs) :=
 (** ** Integer addition and pointer addition *)
 
 Definition addimm_shlimm sh k2 e1 :=
-  match shift1_4_of_z (Int.unsigned sh) with
-  | Some s14 => Eop (Oaddximm s14 k2) (e1:::Enil)
-  | None => Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil)
-  end.
+  if Compopts.optim_faddx tt
+  then
+    match shift1_4_of_z (Int.unsigned sh) with
+    | Some s14 => Eop (Oaddximm s14 k2) (e1:::Enil)
+    | None => Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil)
+    end
+  else Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil).
 
 Nondetfunction addimm (n: int) (e: expr) :=
   if Int.eq n Int.zero then e else
@@ -123,10 +126,13 @@ Nondetfunction addimm (n: int) (e: expr) :=
   end.
 
 Definition add_shlimm n e1 e2 :=
-  match shift1_4_of_z (Int.unsigned n) with
-  | Some s14 => Eop (Oaddx s14) (e1:::e2:::Enil)
-  | None => Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil)
-  end.
+  if Compopts.optim_faddx tt
+  then
+    match shift1_4_of_z (Int.unsigned n) with
+    | Some s14 => Eop (Oaddx s14) (e1:::e2:::Enil)
+    | None => Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil)
+    end
+  else Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil).
 
 Nondetfunction add (e1: expr) (e2: expr) :=
   match e1, e2 with
@@ -611,6 +617,13 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
      else (Aglobal id ofs, Enil))
   | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil)
   | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
+  | Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) =>
+    (if Compopts.optim_fxsaddr tt
+     then let zscale := Int.unsigned scale in
+          if Z.eq_dec zscale (zscale_of_chunk chunk)
+          then (Aindexed2XS zscale, e1:::e2:::Enil) 
+          else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil)
+     else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil))
   | Eop (Oaddxl sh) (e1:::e2:::Enil) =>
     let zscale := ExtValues.z_of_shift1_4 sh in
     let scale := Int.repr zscale in
-- 
cgit 


From 005093b87250b6b27b320eb789574da4bda616c0 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 11 May 2019 22:40:50 +0200
Subject: correct -faddx option and propagate addim over addxim

---
 mppa_k1c/SelectOp.vp | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 4d2a948d..7cf300f8 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -105,7 +105,7 @@ Definition addrstack (ofs: ptrofs) :=
 (** ** Integer addition and pointer addition *)
 
 Definition addimm_shlimm sh k2 e1 :=
-  if Compopts.optim_faddx tt
+  if Compopts.optim_addx tt
   then
     match shift1_4_of_z (Int.unsigned sh) with
     | Some s14 => Eop (Oaddximm s14 k2) (e1:::Enil)
@@ -120,13 +120,13 @@ Nondetfunction addimm (n: int) (e: expr) :=
   | Eop (Oaddrsymbol s m) Enil   => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil
   | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil
   | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
-  | Eop (Oshlimm sh) (t1:::Enil) =>
-    addimm_shlimm sh n t1
+  | Eop (Oaddximm sh m) (t ::: Enil) => Eop (Oaddximm sh (Int.add n m)) (t ::: Enil)
+  | Eop (Oshlimm sh) (t1:::Enil) => addimm_shlimm sh n t1
   | _ => Eop (Oaddimm n) (e ::: Enil)
   end.
 
 Definition add_shlimm n e1 e2 :=
-  if Compopts.optim_faddx tt
+  if Compopts.optim_addx tt
   then
     match shift1_4_of_z (Int.unsigned n) with
     | Some s14 => Eop (Oaddx s14) (e1:::e2:::Enil)
@@ -612,13 +612,13 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   match e with
   | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
   | Eop (Oaddrsymbol id ofs) Enil =>
-    (if (orb (Archi.pic_code tt) (negb (Compopts.optim_fglobaladdrtmp tt)))
+    (if (orb (Archi.pic_code tt) (negb (Compopts.optim_globaladdrtmp tt)))
      then (Aindexed Ptrofs.zero, e:::Enil)
      else (Aglobal id ofs, Enil))
   | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil)
   | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
   | Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) =>
-    (if Compopts.optim_fxsaddr tt
+    (if Compopts.optim_xsaddr tt
      then let zscale := Int.unsigned scale in
           if Z.eq_dec zscale (zscale_of_chunk chunk)
           then (Aindexed2XS zscale, e1:::e2:::Enil) 
@@ -627,7 +627,7 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | Eop (Oaddxl sh) (e1:::e2:::Enil) =>
     let zscale := ExtValues.z_of_shift1_4 sh in
     let scale := Int.repr zscale in
-    (if Compopts.optim_fxsaddr tt
+    (if Compopts.optim_xsaddr tt
      then if Z.eq_dec zscale (zscale_of_chunk chunk)
           then (Aindexed2XS zscale, e2:::e1:::Enil) 
           else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil)
-- 
cgit 


From 487fc42595bb43450f2b0b5a49b4edbc22892b9f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 3 Jun 2019 22:26:06 +0200
Subject: rm old select/selectl/selectf/selectfs

---
 mppa_k1c/SelectOp.vp | 47 ++---------------------------------------------
 1 file changed, 2 insertions(+), 45 deletions(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 23d234aa..219a462b 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -66,33 +66,8 @@ Section SELECT.
 Context {hf: helper_functions}.
 
 (** Ternary operator *)
-Definition select_base o0 o1 oselect :=
- Eop (Oselect (Ccomp0 Cne))
-              (o0:::o1:::oselect:::Enil).
-				      
-Definition select o0 o1 oselect :=
-  select_base o0 o1 oselect.
-				      
-Definition selectl_base o0 o1 oselect :=
- Eop (Oselectl (Ccomp0 Cne))
-              (o0:::o1:::oselect:::Enil).
-				      
-Definition selectl o0 o1 oselect :=
-  selectl_base o0 o1 oselect.
-				      
-Definition selectf_base o0 o1 oselect :=
- Eop (Oselectf (Ccomp0 Cne))
-              (o0:::o1:::oselect:::Enil).
-				      
-Definition selectf o0 o1 oselect :=
-  selectf_base o0 o1 oselect.
-				      
-Definition selectfs_base o0 o1 oselect :=
- Eop (Oselectfs (Ccomp0 Cne))
-              (o0:::o1:::oselect:::Enil).
-				      
-Definition selectfs o0 o1 oselect :=
-  selectfs_base o0 o1 oselect.
+Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr)  : option expr := None.
+
 				      
 (** ** Constants **)
 
@@ -349,24 +324,6 @@ Nondetfunction or (e1: expr) (e2: expr) :=
       else Eop Oor (e1:::e2:::Enil)
   | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) 
   | t1, (Eop Onot (t2:::Enil))  => Eop Oorn (t2:::t1:::Enil)
-  |  (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompimm Ceq zero0))
-        (y0:::Enil)):::Enil)):::v0:::Enil)),
-     (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompimm Cne zero1))
-        (y1:::Enil)):::Enil)):::v1:::Enil)) =>
-     if same_expr_pure y0 y1
-     && Int.eq zero0 Int.zero
-     && Int.eq zero1 Int.zero                 
-     then select_base v0 v1 y0
-     else Eop Oor (e1:::e2:::Enil)
-  |  (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Ceq zero0))
-        (y0:::Enil)):::Enil)):::v0:::Enil)),
-     (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Cne zero1))
-        (y1:::Enil)):::Enil)):::v1:::Enil)) =>
-     if same_expr_pure y0 y1
-     && Int.eq zero0 Int.zero
-     && Int.eq zero1 Int.zero                 
-     then select_base v0 v1 y0
-     else Eop Oor (e1:::e2:::Enil)
   | (Eop (Oandimm nmask) (prev:::Enil)),
     (Eop (Oandimm mask)
       ((Eop (Oshlimm start) (fld:::Enil)):::Enil)) =>
-- 
cgit 


From 5feecb99712de3604f284e5934aed73f2b606659 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 4 Jun 2019 11:47:14 +0200
Subject: start to have whole path if-conversion?

---
 mppa_k1c/SelectOp.vp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 219a462b..ee614253 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -66,7 +66,10 @@ Section SELECT.
 Context {hf: helper_functions}.
 
 (** Ternary operator *)
-Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr)  : option expr := None.
+(** TODO *)
+Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr)  : option expr :=
+  Some (Eop (Osel (Ccomp0 Cne) ty) (e1 ::: e2 :::
+       (Eop (Ocmp cond) args) ::: Enil)).
 
 				      
 (** ** Constants **)
-- 
cgit 


From 7c054b47cad2f75efa661b298484dfbfdd976701 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 4 Jun 2019 13:03:38 +0200
Subject: little restructuring

---
 mppa_k1c/SelectOp.vp | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index ee614253..8101a9b0 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -66,10 +66,11 @@ Section SELECT.
 Context {hf: helper_functions}.
 
 (** Ternary operator *)
-(** TODO *)
+Definition select0 (ty : typ) (cond0 : condition0) (e1 e2 eC: expr) :=
+  (Eop (Osel cond0 ty) (e1 ::: e2 ::: eC ::: Enil)).
+
 Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr)  : option expr :=
-  Some (Eop (Osel (Ccomp0 Cne) ty) (e1 ::: e2 :::
-       (Eop (Ocmp cond) args) ::: Enil)).
+  Some (select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args)).
 
 				      
 (** ** Constants **)
-- 
cgit 


From 2facdc1ec4a51c0eeb31baa299677915e6155ed5 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 4 Jun 2019 18:04:47 +0200
Subject: why doesn't it work?

---
 mppa_k1c/SelectOp.vp | 44 +++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 43 insertions(+), 1 deletion(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 8101a9b0..f997d3d7 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -65,12 +65,54 @@ Section SELECT.
 
 Context {hf: helper_functions}.
 
+Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) :=
+  match cond, args with
+  | (Ccomp c), (e1 ::: (Eop (Ointconst x) Enil) ::: Enil) =>
+    if Int.eq_dec x Int.zero
+    then Some ((Ccomp0 c), e1)
+    else None
+  | (Ccomp c), ((Eop (Ointconst x) Enil) ::: e2 ::: Enil) =>
+    if Int.eq_dec x Int.zero
+    then Some ((Ccomp0 (swap_comparison c)), e2)
+    else None
+  | (Ccompu c), (e1 ::: (Eop (Ointconst x) Enil) ::: Enil) =>
+    if Int.eq_dec x Int.zero
+    then Some ((Ccompu0 c), e1)
+    else None
+  | (Ccompu c), ((Eop (Ointconst x) Enil) ::: e2 ::: Enil) =>
+    if Int.eq_dec x Int.zero
+    then Some ((Ccompu0 (swap_comparison c)), e2)
+    else None
+
+  | (Ccompl c), (e1 ::: (Eop (Olongconst x) Enil) ::: Enil) =>
+    if Int64.eq_dec x Int64.zero
+    then Some ((Ccompl0 c), e1)
+    else None
+  | (Ccompl c), ((Eop (Olongconst x) Enil) ::: e2 ::: Enil) =>
+    if Int64.eq_dec x Int64.zero
+    then Some ((Ccompl0 (swap_comparison c)), e2)
+    else None
+  | (Ccomplu c), (e1 ::: (Eop (Olongconst x) Enil) ::: Enil) =>
+    if Int64.eq_dec x Int64.zero
+    then Some ((Ccomplu0 c), e1)
+    else None
+  | (Ccomplu c), ((Eop (Olongconst x) Enil) ::: e2 ::: Enil) =>
+    if Int64.eq_dec x Int64.zero
+    then Some ((Ccomplu0 (swap_comparison c)), e2)
+    else None
+  | _, _ => None
+  end.
+  
 (** Ternary operator *)
 Definition select0 (ty : typ) (cond0 : condition0) (e1 e2 eC: expr) :=
   (Eop (Osel cond0 ty) (e1 ::: e2 ::: eC ::: Enil)).
 
 Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr)  : option expr :=
-  Some (select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args)).
+  Some(
+  match cond_to_condition0 cond args with
+  | None => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args)
+  | Some(cond0, ec) => select0 ty cond0 e1 e2 ec
+  end).
 
 				      
 (** ** Constants **)
-- 
cgit 


From 74d93ac506f605a1c27179cb7acca2d033aca94b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 4 Jun 2019 18:16:30 +0200
Subject: shortcut cmove works

---
 mppa_k1c/SelectOp.vp | 27 +++++++--------------------
 1 file changed, 7 insertions(+), 20 deletions(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index f997d3d7..01985060 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -67,39 +67,26 @@ Context {hf: helper_functions}.
 
 Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) :=
   match cond, args with
-  | (Ccomp c), (e1 ::: (Eop (Ointconst x) Enil) ::: Enil) =>
+  | (Ccompimm c x), (e1 ::: Enil) =>
     if Int.eq_dec x Int.zero
     then Some ((Ccomp0 c), e1)
     else None
-  | (Ccomp c), ((Eop (Ointconst x) Enil) ::: e2 ::: Enil) =>
-    if Int.eq_dec x Int.zero
-    then Some ((Ccomp0 (swap_comparison c)), e2)
-    else None
-  | (Ccompu c), (e1 ::: (Eop (Ointconst x) Enil) ::: Enil) =>
+           
+  | (Ccompuimm c x), (e1 ::: Enil) =>
     if Int.eq_dec x Int.zero
     then Some ((Ccompu0 c), e1)
     else None
-  | (Ccompu c), ((Eop (Ointconst x) Enil) ::: e2 ::: Enil) =>
-    if Int.eq_dec x Int.zero
-    then Some ((Ccompu0 (swap_comparison c)), e2)
-    else None
 
-  | (Ccompl c), (e1 ::: (Eop (Olongconst x) Enil) ::: Enil) =>
+  | (Ccomplimm c x), (e1 ::: Enil) =>
     if Int64.eq_dec x Int64.zero
     then Some ((Ccompl0 c), e1)
     else None
-  | (Ccompl c), ((Eop (Olongconst x) Enil) ::: e2 ::: Enil) =>
-    if Int64.eq_dec x Int64.zero
-    then Some ((Ccompl0 (swap_comparison c)), e2)
-    else None
-  | (Ccomplu c), (e1 ::: (Eop (Olongconst x) Enil) ::: Enil) =>
+           
+  | (Ccompluimm c x), (e1 ::: Enil) =>
     if Int64.eq_dec x Int64.zero
     then Some ((Ccomplu0 c), e1)
     else None
-  | (Ccomplu c), ((Eop (Olongconst x) Enil) ::: e2 ::: Enil) =>
-    if Int64.eq_dec x Int64.zero
-    then Some ((Ccomplu0 (swap_comparison c)), e2)
-    else None
+           
   | _, _ => None
   end.
   
-- 
cgit 


From 68a6d0dd0ea5774529d823fb9a9ca981c1ecebb0 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 4 Jun 2019 22:58:34 +0200
Subject: osel imm

---
 mppa_k1c/SelectOp.vp | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 01985060..2618983b 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -91,8 +91,14 @@ Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) :=
   end.
   
 (** Ternary operator *)
-Definition select0 (ty : typ) (cond0 : condition0) (e1 e2 eC: expr) :=
-  (Eop (Osel cond0 ty) (e1 ::: e2 ::: eC ::: Enil)).
+Nondetfunction select0 (ty : typ) (cond0 : condition0) (e1 e2 e3: expr) :=
+  match ty, cond0, e1, e2, e3 with
+  | Tint, cond0, e1, (Eop (Ointconst imm) Enil), e3 =>
+    (Eop (Oselimm cond0 imm) (e1 ::: e3 ::: Enil))
+  | Tlong, cond0, e1, (Eop (Olongconst imm) Enil), e3 =>
+    (Eop (Osellimm cond0 imm) (e1 ::: e3 ::: Enil))
+  | _, _, _ => (Eop (Osel cond0 ty) (e1 ::: e2 ::: e3 ::: Enil))
+  end.
 
 Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr)  : option expr :=
   Some(
-- 
cgit 


From b5352b040da8c38b371316d67c2180dbab758295 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 4 Jun 2019 23:16:35 +0200
Subject: move with immediates

---
 mppa_k1c/SelectOp.vp | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 2618983b..3df0c682 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -95,8 +95,12 @@ Nondetfunction select0 (ty : typ) (cond0 : condition0) (e1 e2 e3: expr) :=
   match ty, cond0, e1, e2, e3 with
   | Tint, cond0, e1, (Eop (Ointconst imm) Enil), e3 =>
     (Eop (Oselimm cond0 imm) (e1 ::: e3 ::: Enil))
+  | Tint, cond0, (Eop (Ointconst imm) Enil), e2, e3 =>
+    (Eop (Oselimm (negate_condition0 cond0) imm) (e2 ::: e3 ::: Enil))
   | Tlong, cond0, e1, (Eop (Olongconst imm) Enil), e3 =>
     (Eop (Osellimm cond0 imm) (e1 ::: e3 ::: Enil))
+  | Tlong, cond0, (Eop (Olongconst imm) Enil), e2, e3 =>
+    (Eop (Osellimm (negate_condition0 cond0) imm) (e2 ::: e3 ::: Enil))
   | _, _, _ => (Eop (Osel cond0 ty) (e1 ::: e2 ::: e3 ::: Enil))
   end.
 
-- 
cgit 


From 4c379d48b35e7c8156f3953fede31d5e47faf8ca Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 19 Jul 2019 18:59:44 +0200
Subject: helpers broke compilation

---
 mppa_k1c/SelectOp.vp | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 3df0c682..688820b3 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -54,6 +54,7 @@ Require Import OpHelpers.
 Require Import ExtValues.
 Require Import DecBoolOps.
 Require Import Chunks.
+Require Import Builtins.
 Require Compopts.
 
 Local Open Scope cminorsel_scope.
@@ -673,6 +674,8 @@ Definition divfs_base (e1: expr) (e2: expr) :=
   Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil).
 End SELECT.
 
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+  None.
 (* Local Variables: *)
 (* mode: coq *)
 (* End: *)
\ No newline at end of file
-- 
cgit 


From 51094cecd5d24023e3de2487e66765f8c54b5fcc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 29 Aug 2019 19:33:33 +0200
Subject: fmin/fmax/fminf/fmaxf non bien testés
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mppa_k1c/SelectOp.vp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 688820b3..72597a2b 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -675,7 +675,13 @@ Definition divfs_base (e1: expr) (e2: expr) :=
 End SELECT.
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
-  None.
+  match b with
+  | BI_fmin => Some (Eop Ominf args)
+  | BI_fmax => Some (Eop Omaxf args)
+  | BI_fminf => Some (Eop Ominfs args)
+  | BI_fmaxf => Some (Eop Omaxfs args)
+  end.
+
 (* Local Variables: *)
 (* mode: coq *)
 (* End: *)
\ No newline at end of file
-- 
cgit 


From c0984982ea5b8481bfc75c0ea4254eb5db07d875 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 29 Aug 2019 21:46:52 +0200
Subject: fabsf

---
 mppa_k1c/SelectOp.vp | 1 +
 1 file changed, 1 insertion(+)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 72597a2b..c8139ecb 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -680,6 +680,7 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
   | BI_fmax => Some (Eop Omaxf args)
   | BI_fminf => Some (Eop Ominfs args)
   | BI_fmaxf => Some (Eop Omaxfs args)
+  | BI_fabsf => Some (Eop Oabsfs args)
   end.
 
 (* Local Variables: *)
-- 
cgit 


From 344fd96e0690ff4809623198baeee823132f7219 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 30 Aug 2019 12:30:16 +0200
Subject: use finvw

---
 mppa_k1c/SelectOp.vp | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index c8139ecb..6539184c 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -51,7 +51,7 @@ Require Import Floats.
 Require Import Op.
 Require Import CminorSel.
 Require Import OpHelpers.
-Require Import ExtValues.
+Require Import ExtValues ExtFloats.
 Require Import DecBoolOps.
 Require Import Chunks.
 Require Import Builtins.
@@ -669,9 +669,20 @@ Definition divf_base (e1: expr) (e2: expr) :=
   (* Eop Odivf (e1 ::: e2 ::: Enil). *)
   Eexternal f64_div sig_ff_f (e1 ::: e2 ::: Enil).
 
-Definition divfs_base (e1: expr) (e2: expr) :=
+Definition divfs_base1 (e2 : expr) :=
+  Eop Oinvfs (e2 ::: Enil).
+Definition divfs_baseX (e1 : expr) (e2 : expr) :=
   (* Eop Odivf (e1 ::: e2 ::: Enil). *)
   Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil).
+
+Nondetfunction divfs_base (e1: expr) :=
+  match e1 with
+  | Eop (Osingleconst f) Enil =>
+    (if Float32.eq_dec f ExtFloat32.one
+     then divfs_base1
+     else divfs_baseX e1)
+  | _ => divfs_baseX e1
+  end.
 End SELECT.
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
-- 
cgit 


From caac487ae23a9785602cf235f5b4a2b6749f2c18 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 30 Aug 2019 19:10:42 +0200
Subject: fma

---
 mppa_k1c/SelectOp.vp | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 6539184c..71078046 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -683,7 +683,18 @@ Nondetfunction divfs_base (e1: expr) :=
      else divfs_baseX e1)
   | _ => divfs_baseX e1
   end.
-End SELECT.
+
+Nondetfunction gen_fma args :=
+  match args with
+  | e1:::e2:::e3:::Enil => Some (Eop Ofmaddf (e3:::e1:::e2:::Enil))
+  | _ => None
+  end.
+
+Nondetfunction gen_fmaf args :=
+  match args with
+  | e1:::e2:::e3:::Enil => Some (Eop Ofmaddfs (e3:::e1:::e2:::Enil))
+  | _ => None
+  end.
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
   match b with
@@ -692,7 +703,10 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
   | BI_fminf => Some (Eop Ominfs args)
   | BI_fmaxf => Some (Eop Omaxfs args)
   | BI_fabsf => Some (Eop Oabsfs args)
+  | BI_fma => gen_fma args
+  | BI_fmaf => gen_fmaf args
   end.
+End SELECT.
 
 (* Local Variables: *)
 (* mode: coq *)
-- 
cgit 


From 9a19f2fdf735785947cc469d2ceef83cbe4f1679 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 30 Aug 2019 19:23:24 +0200
Subject: fma with first negated operand

---
 mppa_k1c/SelectOp.vp | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 71078046..ec3985c5 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -686,12 +686,14 @@ Nondetfunction divfs_base (e1: expr) :=
 
 Nondetfunction gen_fma args :=
   match args with
+  | (Eop Onegf (e1:::Enil)):::e2:::e3:::Enil => Some (Eop Ofmsubf (e3:::e1:::e2:::Enil))
   | e1:::e2:::e3:::Enil => Some (Eop Ofmaddf (e3:::e1:::e2:::Enil))
   | _ => None
   end.
 
 Nondetfunction gen_fmaf args :=
   match args with
+  | (Eop Onegfs (e1:::Enil)):::e2:::e3:::Enil => Some (Eop Ofmsubfs (e3:::e1:::e2:::Enil))
   | e1:::e2:::e3:::Enil => Some (Eop Ofmaddfs (e3:::e1:::e2:::Enil))
   | _ => None
   end.
-- 
cgit