Hook for MPPA_K1c (generates Risc-V code for now)

configure

@@ -49,6 +49,7 @@ Supported targets:
   x86_64-macosx        (x86 64 bits, MacOS X)
   rv32-linux           (RISC-V 32 bits, Linux)
   rv64-linux           (RISC-V 64 bits, Linux)
+  k1c-linux            (Kalray K1c, Linux)
   manual               (edit configuration file by hand)
 
 For x86 targets, the "x86_32-" prefix can also be written "ia32-" or "i386-".
@@ -152,6 +153,8 @@ case "$target" in
       arch="riscV"; model="32"; endianness="little"; bitsize=32;;
   rv64-*)
       arch="riscV"; model="64"; endianness="little"; bitsize=64;;
+  k1c-*)
+      arch="mppa_k1c"; model="64"; endianness="little"; bitsize=64;;
   manual)
       ;;
   "")
@@ -405,6 +408,25 @@ if test "$arch" = "riscV"; then
   system="linux"
 fi
 
+#
+# K1c Target Configuration
+#
+if test "$arch" = "mppa_k1c"; then
+  #model_options="-march=rv64imafd -mabi=lp64d"
+  # FIXME - maybe later add it for NodeOS & cie
+  model_options=
+  abi="standard"
+  casm="${toolprefix}gcc"
+  casm_options="$model_options -c"
+  cc="${toolprefix}gcc $model_options"
+  clinker="${toolprefix}gcc"
+  clinker_options="$model_options"
+  cprepro="${toolprefix}gcc"
+  cprepro_options="$model_options -std=c99 -U__GNUC__ -E"
+  libmath="-lm"
+  system="linux"
+fi
+
 
 #
 # Finalize Target Configuration

cparser/Machine.ml

@@ -224,6 +224,11 @@ let rv64 =
                    struct_passing_style = SP_ref_callee; (* Wrong *)
                    struct_return_style = SR_ref } (* to check *)
 
+let mppa_k1c =
+  { ilp32ll64 with name = "k1c";
+                   char_signed = true;
+                   supports_unaligned_accesses = true }
+
 (* Add GCC extensions re: sizeof and alignof *)
 
 let gcc_extensions c =

cparser/Machine.mli

@@ -82,6 +82,7 @@ val arm_littleendian : t
 val arm_bigendian : t
 val rv32 : t
 val rv64 : t
+val mppa_k1c : t
 
 val gcc_extensions : t -> t
 val compcert_interpreter : t -> t

driver/Configuration.ml

@@ -123,7 +123,7 @@ let get_bool_config key =
 
 let arch =
   match get_config_string "arch" with
-  | "powerpc"|"arm"|"x86"|"riscV" as a -> a
+  | "powerpc"|"arm"|"x86"|"riscV"|"mppa_k1c" as a -> a
   | v -> bad_config "arch" [v]
 let model = get_config_string "model"
 let abi = get_config_string "abi"

driver/Frontend.ml

@@ -83,6 +83,7 @@ let init () =
     | "riscV"   -> if Configuration.model = "64"
                    then Machine.rv64
                    else Machine.rv32
+    | "mppa_k1c" -> Machine.mppa_k1c
     | _         -> assert false
   end;
   Builtins.set C2C.builtins;

mppa_k1c/Archi.v

+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*                Xavier Leroy, INRIA Paris                            *)
+(*                Jacques-Henri Jourdan, INRIA Paris                   *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Architecture-dependent parameters for RISC-V *)
+
+Require Import ZArith.
+Require Import Fappli_IEEE.
+Require Import Fappli_IEEE_bits.
+
+Parameter ptr64 : bool.
+
+Definition big_endian := false.
+
+Definition align_int64 := 8%Z.
+Definition align_float64 := 8%Z.
+
+Definition splitlong := negb ptr64.
+
+Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
+Proof.
+  unfold splitlong. destruct ptr64; simpl; congruence. 
+Qed.
+
+(** Section 7.3: "Except when otherwise stated, if the result of a
+   floating-point operation is NaN, it is the canonical NaN. The
+   canonical NaN has a positive sign and all significand bits clear
+   except the MSB, a.k.a. the quiet bit."
+   We need to extend the [choose_binop_pl] functions to account for
+   this case. *)
+
+Program Definition default_pl_64 : bool * nan_pl 53 :=
+  (false, iter_nat 51 _ xO xH).
+
+Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
+  false.                        (**r always choose first NaN *)
+
+Program Definition default_pl_32 : bool * nan_pl 24 :=
+  (false, iter_nat 22 _ xO xH).
+
+Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) :=
+  false.                        (**r always choose first NaN *)
+
+Definition float_of_single_preserves_sNaN := false.
+
+Global Opaque ptr64 big_endian splitlong
+              default_pl_64 choose_binop_pl_64
+              default_pl_32 choose_binop_pl_32
+              float_of_single_preserves_sNaN.
+
+(** Whether to generate position-independent code or not *)
+
+Parameter pic_code: unit -> bool.

mppa_k1c/AsmToJSON.ml

+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Simple functions to serialize RISC-V Asm to JSON *)
+
+(* Dummy function *)
+let destination: string option ref = ref None
+
+let sdump_folder = ref ""
+
+let print_if prog sourcename =
+  ()
+
+let pp_mnemonics pp = ()

mppa_k1c/CBuiltins.ml

+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Processor-dependent builtin C functions *)
+
+open C
+
+let builtins = {
+  Builtins.typedefs = [
+    "__builtin_va_list", TPtr(TVoid [], [])
+  ];
+  Builtins.functions = [
+    (* Synchronization *)
+    "__builtin_fence",
+      (TVoid [], [], false);
+    (* Integer arithmetic *)
+    "__builtin_bswap64",
+      (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
+    (* Float arithmetic *)
+    "__builtin_fmadd",
+      (TFloat(FDouble, []),
+       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
+       false);
+    "__builtin_fmsub",
+      (TFloat(FDouble, []),
+       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
+       false);
+    "__builtin_fnmadd",
+      (TFloat(FDouble, []),
+       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
+       false);
+    "__builtin_fnmsub",
+      (TFloat(FDouble, []),
+       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
+       false);
+    "__builtin_fmax",
+      (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
+    "__builtin_fmin",
+      (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
+  ]
+}
+
+let va_list_type = TPtr(TVoid [], [])  (* to check! *)
+let size_va_list = if Archi.ptr64 then 8 else 4
+let va_list_scalar = true
+
+(* Expand memory references inside extended asm statements.  Used in C2C. *)
+
+let asm_mem_argument arg = Printf.sprintf "0(%s)" arg

mppa_k1c/CombineOp.v

+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  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.

mppa_k1c/CombineOpproof.v

+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  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 FunInd.
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Memory.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import CSEdomain.
+Require Import CombineOp.
+
+Section COMBINE.
+
+Variable ge: genv.
+Variable sp: val.
+Variable m: mem.
+Variable get: valnum -> option rhs.
+Variable valu: valnum -> val.
+Hypothesis get_sound: forall v rhs, get v = Some rhs -> rhs_eval_to valu ge sp m rhs (valu v).
+
+Lemma get_op_sound:
+  forall v op vl, get v = Some (Op op vl) -> eval_operation ge sp op (map valu vl) m = Some (valu v).
+Proof.
+  intros. exploit get_sound; eauto. intros REV; inv REV; auto.
+Qed.
+
+Ltac UseGetSound :=
+  match goal with
+  | [ H: get _ = Some _ |- _ ] =>
+      let x := fresh "EQ" in (generalize (get_op_sound _ _ _ H); intros x; simpl in x; FuncInv)
+  end.
+
+Lemma combine_compimm_ne_0_sound:
+  forall x cond args,
+  combine_compimm_ne_0 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.zero) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.zero).
+Proof.
+  intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ.
+  (* of cmp *)
+  UseGetSound. rewrite <- H.
+  destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
+Qed.
+
+Lemma combine_compimm_eq_0_sound:
+  forall x cond args,
+  combine_compimm_eq_0 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.zero) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.zero).
+Proof.
+  intros until args. functional induction (combine_compimm_eq_0 get x); intros EQ; inv EQ.
+  (* of cmp *)
+  UseGetSound. rewrite <- H.
+  rewrite eval_negate_condition.
+  destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
+Qed.
+
+Lemma combine_compimm_eq_1_sound:
+  forall x cond args,
+  combine_compimm_eq_1 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.one) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.one).
+Proof.
+  intros until args. functional induction (combine_compimm_eq_1 get x); intros EQ; inv EQ.
+  (* of cmp *)
+  UseGetSound. rewrite <- H.
+  destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
+Qed.
+
+Lemma combine_compimm_ne_1_sound:
+  forall x cond args,
+  combine_compimm_ne_1 get x = Some(cond, args) ->
+  eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.one) /\
+  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.one).
+Proof.
+  intros until args. functional induction (combine_compimm_ne_1 get x); intros EQ; inv EQ.
+  (* of cmp *)
+  UseGetSound. rewrite <- H.
+  rewrite eval_negate_condition.
+  destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
+Qed.
+
+Theorem combine_cond_sound:
+  forall cond args cond' args',
+  combine_cond get cond args = Some(cond', args') ->
+  eval_condition cond' (map valu args') m = eval_condition cond (map valu args) m.
+Proof.
+  intros. functional inversion H; subst.
+  (* compimm ne zero *)
+  - simpl; eapply combine_compimm_ne_0_sound; eauto.
+  (* compimm ne one *)
+  - simpl; eapply combine_compimm_ne_1_sound; eauto.
+  (* compimm eq zero *)
+  - simpl; eapply combine_compimm_eq_0_sound; eauto.
+  (* compimm eq one *)
+  - simpl; eapply combine_compimm_eq_1_sound; eauto.
+  (* compuimm ne zero *)
+  - simpl; eapply combine_compimm_ne_0_sound; eauto.
+  (* compuimm ne one *)
+  - simpl; eapply combine_compimm_ne_1_sound; eauto.
+  (* compuimm eq zero *)
+  - simpl; eapply combine_compimm_eq_0_sound; eauto.
+  (* compuimm eq one *)
+  - simpl; eapply combine_compimm_eq_1_sound; eauto.
+Qed.
+
+Theorem combine_addr_sound:
+  forall addr args addr' args',
+  combine_addr get addr args = Some(addr', args') ->
+  eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args).
+Proof.
+  intros. functional inversion H; subst.
+- (* indexed - addimm *)
+  UseGetSound. simpl. rewrite <- H0. destruct v; auto. simpl; rewrite H7; simpl.
+  rewrite Ptrofs.add_assoc. auto.
+- (* indexed - addimml *)
+  UseGetSound. simpl. rewrite <- H0. destruct v; auto. simpl; rewrite H7; simpl.
+  rewrite Ptrofs.add_assoc. auto.
+Qed.
+
+Theorem combine_op_sound:
+  forall op args op' args',
+  combine_op get op args = Some(op', args') ->
+  eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m.
+Proof.
+  intros. functional inversion H; subst.
+  (* addimm - addimm *)
+  - UseGetSound. FuncInv. simpl.
+    rewrite <- H0. rewrite Val.add_assoc. auto.
+  (* andimm - andimm *)
+  - UseGetSound; simpl.
+    generalize (Int.eq_spec p m0); rewrite H7; intros.
+    rewrite <- H0. rewrite Val.and_assoc. simpl. fold p. rewrite H1. auto.
+  - UseGetSound; simpl.
+    rewrite <- H0. rewrite Val.and_assoc. auto.
+  (* orimm - orimm *)
+  - UseGetSound. simpl. rewrite <- H0. rewrite Val.or_assoc. auto.
+  (* xorimm - xorimm *)
+  - UseGetSound. simpl. rewrite <- H0. rewrite Val.xor_assoc. auto.
+  (* addlimm - addlimm *)
+  - UseGetSound. FuncInv. simpl.
+    rewrite <- H0. rewrite Val.addl_assoc. auto.
+  (* andlimm - andlimm *)
+  - UseGetSound; simpl.
+    generalize (Int64.eq_spec p m0); rewrite H7; intros.
+    rewrite <- H0. rewrite Val.andl_assoc. simpl. fold p. rewrite H1. auto.
+  - UseGetSound; simpl.
+    rewrite <- H0. rewrite Val.andl_assoc. auto.
+  (* orlimm - orlimm *)
+  - UseGetSound. simpl. rewrite <- H0. rewrite Val.orl_assoc. auto.
+  (* xorlimm - xorlimm *)
+  - UseGetSound. simpl. rewrite <- H0. rewrite Val.xorl_assoc. auto.
+  (* cmp *)
+  - simpl. decEq; decEq. eapply combine_cond_sound; eauto.
+Qed.
+
+End COMBINE.