From b4a08d0815342b6238d307864f0823d0f07bb691 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 26 May 2020 22:04:20 +0200
Subject: k1c -> kvx changes

---
 kvx/CombineOp.v | 141 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 141 insertions(+)
 create mode 100644 kvx/CombineOp.v

(limited to 'kvx/CombineOp.v')

diff --git a/kvx/CombineOp.v b/kvx/CombineOp.v
new file mode 100644
index 00000000..ff1db3cd
--- /dev/null
+++ b/kvx/CombineOp.v
@@ -0,0 +1,141 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** Recognition of combined operations, addressing modes and conditions
+  during the [CSE] phase. *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Op.
+Require Import CSEdomain.
+
+Section COMBINE.
+
+Variable get: valnum -> option rhs.
+
+Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (c, ys)
+  | _ => None
+  end.
+
+Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
+  | _ => None
+  end.
+
+Function combine_compimm_eq_1 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (c, ys)
+  | _ => None
+  end.
+
+Function combine_compimm_ne_1 (x: valnum) : option(condition * list valnum) :=
+  match get x with
+  | Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
+  | _ => None
+  end.
+
+Function combine_cond (cond: condition) (args: list valnum) : option(condition * list valnum) :=
+  match cond, args with
+  | Ccompimm Cne n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x
+      else if Int.eq_dec n Int.one then combine_compimm_ne_1 x
+      else None
+  | Ccompimm Ceq n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x
+      else if Int.eq_dec n Int.one then combine_compimm_eq_1 x
+      else None
+  | Ccompuimm Cne n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_ne_0 x
+      else if Int.eq_dec n Int.one then combine_compimm_ne_1 x
+      else None
+  | Ccompuimm Ceq n, x::nil =>
+      if Int.eq_dec n Int.zero then combine_compimm_eq_0 x
+      else if Int.eq_dec n Int.one then combine_compimm_eq_1 x
+      else None
+  | _, _ => None
+  end.
+
+Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
+  match addr, args with
+  | Aindexed n, x::nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) =>
+          if Archi.ptr64 then None else Some(Aindexed (Ptrofs.add (Ptrofs.of_int m) n), ys)
+      | Some(Op (Oaddlimm m) ys) =>
+          if Archi.ptr64 then Some(Aindexed (Ptrofs.add (Ptrofs.of_int64 m) n), ys) else None
+      | _ => None
+      end
+  | _, _ => None
+  end.
+
+Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) :=
+  match op, args with
+  | Oaddimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oaddimm m) ys) => Some(Oaddimm (Int.add m n), ys)
+      | _ => None
+      end
+  | Oandimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oandimm m) ys) =>
+          Some(let p := Int.and m n in
+               if Int.eq p m then (Omove, x :: nil) else (Oandimm p, ys))
+      | _ => None
+      end
+  | Oorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys)
+      | _ => None
+      end
+  | Oxorimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys)
+      | _ => None
+      end
+  | Oaddlimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oaddlimm m) ys) => Some(Oaddlimm (Int64.add m n), ys)
+      | _ => None
+      end
+  | Oandlimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oandlimm m) ys) =>
+          Some(let p := Int64.and m n in
+               if Int64.eq p m then (Omove, x :: nil) else (Oandlimm p, ys))
+      | _ => None
+      end
+  | Oorlimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oorlimm m) ys) => Some(Oorlimm (Int64.or m n), ys)
+      | _ => None
+      end
+  | Oxorlimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oxorlimm m) ys) => Some(Oxorlimm (Int64.xor m n), ys)
+      | _ => None
+      end
+  | Ocmp cond, _ =>
+      match combine_cond cond args with
+      | Some(cond', args') => Some(Ocmp cond', args')
+      | None => None
+      end
+  | _, _ => None
+  end.
+
+End COMBINE.
-- 
cgit