Support for 64-bit architectures: x86 in 64-bit mode

This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model.

To activate x86-64 bit support, configure with "x86_64-linux".

Main steps:
- Enrich Op.v and Asm.v with 64-bit operations
- SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers
- Conventions1: support x86-64 ABI in addition to the 32-bit ABI.
- Add support for the new 64-bit operations everywhere.
- runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode

To do:
- More optimizations are possible on 64-bit integer arithmetic operations.
- Could add new chunks to load, say, an unsigned byte into a 64-bit long
  (currently we load as a 32-bit int then zero-extend).
- Implements the wrong ABI for struct passing.

1 files changed, 365 insertions, 0 deletions

diff --git a/ia32/SelectLong.vp b/ia32/SelectLong.vp
new file mode 100644
index 00000000..c28777e8
--- /dev/null
+++ b/ia32/SelectLong.vp
@@ -0,0 +1,365 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*                 Xavier Leroy, INRIA Paris                           *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Instruction selection for 64-bit integer operations *)
+
+Require Import Coqlib.
+Require Import Compopts.
+Require Import AST Integers Floats.
+Require Import Op CminorSel.
+Require Import SelectOp SplitLong.
+
+Local Open Scope cminorsel_scope.
+Local Open Scope string_scope.
+
+Section SELECT.
+
+Context {hf: helper_functions}.
+
+Definition longconst (n: int64) : expr :=
+  if Archi.splitlong then SplitLong.longconst n else Eop (Olongconst n) Enil.
+
+Definition is_longconst (e: expr) :=
+  match e with
+  | Eop (Olongconst n) Enil => Some n
+  | _ => None
+  end.
+
+Definition intoflong (e: expr) :=
+  if Archi.splitlong then SplitLong.intoflong e else
+  match is_longconst e with
+  | Some n => Eop (Ointconst (Int.repr (Int64.unsigned n))) Enil
+  | None =>  Eop Olowlong (e ::: Enil)
+  end.
+
+Definition longofint (e: expr) :=
+  if Archi.splitlong then SplitLong.longofint e else
+  match is_intconst e with
+  | Some n => longconst (Int64.repr (Int.signed n))
+  | None =>  Eop Ocast32signed (e ::: Enil)
+  end.
+
+Definition longofintu (e: expr) :=
+  if Archi.splitlong then SplitLong.longofintu e else
+  match is_intconst e with
+  | Some n => longconst (Int64.repr (Int.unsigned n))
+  | None =>  Eop Ocast32unsigned (e ::: Enil)
+  end.
+
+Nondetfunction notl (e: expr) :=
+  if Archi.splitlong then SplitLong.notl e else
+  match e with
+  | Eop (Olongconst n) Enil => longconst (Int64.not n)
+  | Eop Onotl (t1:::Enil) => t1
+  | _ => Eop Onotl (e:::Enil)
+  end.
+
+Nondetfunction andlimm (n1: int64) (e2: expr) := 
+  if Int64.eq n1 Int64.zero then longconst Int64.zero else
+  if Int64.eq n1 Int64.mone then e2 else
+  match e2 with
+  | Eop (Olongconst n2) Enil =>
+      longconst (Int64.and n1 n2)
+  | Eop (Oandlimm n2) (t2:::Enil) =>
+      Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil)
+  | _ =>
+      Eop (Oandlimm n1) (e2:::Enil)
+  end.
+
+Nondetfunction andl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.andl e1 e2 else
+  match e1, e2 with
+  | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2
+  | t1, Eop (Olongconst n2) Enil => andlimm n2 t1
+  | _, _ => Eop Oandl (e1:::e2:::Enil)
+  end.
+
+Nondetfunction orlimm (n1: int64) (e2: expr) :=
+  if Int64.eq n1 Int64.zero then e2 else
+  if Int64.eq n1 Int64.mone then longconst Int64.mone else
+  match e2 with
+  | Eop (Olongconst n2) Enil => longconst (Int64.or n1 n2)
+  | Eop (Oorlimm n2) (t2:::Enil) => Eop (Oorlimm (Int64.or n1 n2)) (t2:::Enil)
+  | _ => Eop (Oorlimm n1) (e2:::Enil)
+  end.
+
+Nondetfunction orl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.orl e1 e2 else
+  match e1, e2 with
+  | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2
+  | t1, Eop (Olongconst n2) Enil => orlimm n2 t1
+  | Eop (Oshllimm n1) (t1:::Enil), Eop (Oshrluimm n2) (t2:::Enil) =>
+      if Int.eq (Int.add n1 n2) Int64.iwordsize' && same_expr_pure t1 t2
+      then Eop (Ororlimm n2) (t1:::Enil)
+      else Eop Oorl (e1:::e2:::Enil)
+  | Eop (Oshrluimm n2) (t2:::Enil), Eop (Oshllimm n1) (t1:::Enil) =>
+      if Int.eq (Int.add n1 n2) Int64.iwordsize' && same_expr_pure t1 t2
+      then Eop (Ororimm n2) (t1:::Enil)
+      else Eop Oorl (e1:::e2:::Enil)
+  | _, _ =>
+      Eop Oorl (e1:::e2:::Enil)
+  end.
+
+Nondetfunction xorlimm (n1: int64) (e2: expr) :=
+  if Int64.eq n1 Int64.zero then e2 else
+  if Int64.eq n1 Int64.mone then notl e2 else
+  match e2 with
+  | Eop (Olongconst n2) Enil => longconst (Int64.xor n1 n2)
+  | Eop (Oxorlimm n2) (t2:::Enil) => Eop (Oxorlimm (Int64.xor n1 n2)) (t2:::Enil)
+  | Eop Onotl (t2:::Enil) => Eop (Oxorlimm (Int64.not n1)) (t2:::Enil)
+  | _ => Eop (Oxorlimm n1) (e2:::Enil)
+  end.
+
+Nondetfunction xorl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.xorl e1 e2 else
+  match e1, e2 with
+  | Eop (Olongconst n1) Enil, t2 => xorlimm n1 t2
+  | t1, Eop (Olongconst n2) Enil => xorlimm n2 t1
+  | _, _ => Eop Oxorl (e1:::e2:::Enil)
+  end.
+
+Nondetfunction shllimm (e1: expr) (n: int) :=
+  if Archi.splitlong then SplitLong.shllimm e1 n else
+  if Int.eq n Int.zero then e1 else
+  if negb (Int.ltu n Int64.iwordsize') then
+    Eop Oshll (e1:::Eop (Ointconst n) Enil:::Enil)
+  else
+    match e1 with
+    | Eop (Olongconst n1) Enil =>
+        Eop (Olongconst(Int64.shl' n1 n)) Enil
+    | Eop (Oshllimm n1) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int64.iwordsize'
+        then Eop (Oshllimm (Int.add n n1)) (t1:::Enil)
+        else Eop (Oshllimm n) (e1:::Enil)
+    | Eop (Oleal (Aindexed n1)) (t1:::Enil) =>
+        if shift_is_scale n
+        then Eop (Oleal (Ascaled (Int64.unsigned (Int64.shl' Int64.one n))
+                                 (Int64.unsigned (Int64.shl' (Int64.repr n1) n)))) (t1:::Enil)
+        else Eop (Oshllimm n) (e1:::Enil)
+    | _ =>
+        if shift_is_scale n
+        then Eop (Oleal (Ascaled (Int64.unsigned (Int64.shl' Int64.one n)) 0)) (e1:::Enil)
+        else Eop (Oshllimm n) (e1:::Enil)
+    end.
+
+Nondetfunction shrluimm (e1: expr) (n: int) :=
+  if Archi.splitlong then SplitLong.shrluimm e1 n else
+  if Int.eq n Int.zero then e1 else
+  if negb (Int.ltu n Int64.iwordsize') then
+    Eop Oshrlu (e1:::Eop (Ointconst n) Enil:::Enil)
+  else
+    match e1 with
+    | Eop (Olongconst n1) Enil =>
+        Eop (Olongconst(Int64.shru' n1 n)) Enil
+    | Eop (Oshrluimm n1) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int64.iwordsize'
+        then Eop (Oshrluimm (Int.add n n1)) (t1:::Enil)
+        else Eop (Oshrluimm n) (e1:::Enil)
+    | _ =>
+        Eop (Oshrluimm n) (e1:::Enil)
+    end.
+
+Nondetfunction shrlimm (e1: expr) (n: int) :=
+  if Archi.splitlong then SplitLong.shrlimm e1 n else
+  if Int.eq n Int.zero then e1 else
+  if negb (Int.ltu n Int64.iwordsize') then
+    Eop Oshrl (e1:::Eop (Ointconst n) Enil:::Enil)
+  else
+  match e1 with
+  | Eop (Olongconst n1) Enil =>
+      Eop (Olongconst(Int64.shr' n1 n)) Enil
+  | Eop (Oshrlimm n1) (t1:::Enil) =>
+      if Int.ltu (Int.add n n1) Int64.iwordsize'
+      then Eop (Oshrlimm (Int.add n n1)) (t1:::Enil)
+      else Eop (Oshrlimm n) (e1:::Enil)
+  | _ =>
+      Eop (Oshrlimm n) (e1:::Enil)
+  end.
+
+Definition shll (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.shll e1 e2 else
+  match is_intconst e2 with
+  | Some n2 => shllimm e1 n2
+  | None => Eop Oshll (e1:::e2:::Enil)
+  end.
+
+Definition shrl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.shrl e1 e2 else
+  match is_intconst e2 with
+  | Some n2 => shrlimm e1 n2
+  | None => Eop Oshrl (e1:::e2:::Enil)
+  end.
+
+Definition shrlu (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.shrlu e1 e2 else
+  match is_intconst e2 with
+  | Some n2 => shrluimm e1 n2
+  | _ => Eop Oshrlu (e1:::e2:::Enil)
+  end.
+
+Nondetfunction addlimm (n: int64) (e: expr) :=
+  if Int64.eq n Int64.zero then e else
+  match e with
+  | Eop (Olongconst m) Enil => longconst (Int64.add n m)
+  | Eop (Oleal addr) args   => Eop (Oleal (offset_addressing_total addr (Int64.signed n))) args
+  | _                       => Eop (Oleal (Aindexed (Int64.signed n))) (e ::: Enil)
+  end.
+
+Nondetfunction addl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.addl e1 e2 else
+  match e1, e2 with
+  | Eop (Olongconst n1) Enil, t2 => addlimm n1 t2
+  | t1, Eop (Olongconst n2) Enil => addlimm n2 t1
+  | Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) =>
+      Eop (Oleal (Aindexed2 (n1 + n2))) (t1:::t2:::Enil)
+  | Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Ascaled sc n2)) (t2:::Enil) =>
+      Eop (Oleal (Aindexed2scaled sc (n1 + n2))) (t1:::t2:::Enil)
+  | Eop (Oleal (Ascaled sc n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) =>
+      Eop (Oleal (Aindexed2scaled sc (n1 + n2))) (t2:::t1:::Enil)
+  | Eop (Oleal (Ascaled sc n)) (t1:::Enil), t2 =>
+      Eop (Oleal (Aindexed2scaled sc n)) (t2:::t1:::Enil)
+  | t1, Eop (Oleal (Ascaled sc n)) (t2:::Enil) =>
+      Eop (Oleal (Aindexed2scaled sc n)) (t1:::t2:::Enil)
+  | Eop (Oleal (Aindexed n)) (t1:::Enil), t2 =>
+      Eop (Oleal (Aindexed2 n)) (t1:::t2:::Enil)
+  | t1, Eop (Oleal (Aindexed n)) (t2:::Enil) =>
+      Eop (Oleal (Aindexed2 n)) (t1:::t2:::Enil)
+  | _, _ =>
+      Eop (Oleal (Aindexed2 0)) (e1:::e2:::Enil)
+  end.
+
+Definition negl (e: expr) :=
+  if Archi.splitlong then SplitLong.negl e else
+  match is_longconst e with
+  | Some n => longconst (Int64.neg n)
+  | None =>  Eop Onegl (e ::: Enil)
+  end.
+
+Nondetfunction subl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.subl e1 e2 else
+  match e1, e2 with
+  | t1, Eop (Olongconst n2) Enil => addlimm (Int64.neg n2) t1
+  | Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) =>
+      addlimm (Int64.repr (n1 - n2)) (Eop Osubl (t1:::t2:::Enil))
+  | Eop (Oleal (Aindexed n1)) (t1:::Enil), t2 =>
+      addlimm (Int64.repr n1) (Eop Osubl (t1:::t2:::Enil))
+  | t1, Eop (Oleal (Aindexed n2)) (t2:::Enil) =>
+      addlimm (Int64.repr (- n2)) (Eop Osubl (t1:::t2:::Enil))
+  | _, _ =>
+      Eop Osubl (e1:::e2:::Enil)
+  end.
+
+Definition mullimm_base (n1: int64) (e2: expr) :=
+  match Int64.one_bits n1 with
+  | i :: nil =>
+      shllimm e2 (Int.repr (Int64.unsigned i))
+  | i :: j :: nil =>
+      Elet e2 (addl (shllimm (Eletvar 0) (Int.repr (Int64.unsigned i)))
+                    (shllimm (Eletvar 0) (Int.repr (Int64.unsigned j))))
+  | _ =>
+      Eop (Omullimm n1) (e2:::Enil)
+  end.
+
+Nondetfunction mullimm (n1: int64) (e2: expr) :=
+  if Int64.eq n1 Int64.zero then longconst Int64.zero
+  else if Int64.eq n1 Int64.one then e2
+  else match e2 with
+  | Eop (Olongconst n2) Enil => longconst (Int64.mul n1 n2)
+  | Eop (Oleal (Aindexed n2)) (t2:::Enil) => addlimm (Int64.mul n1 (Int64.repr n2)) (mullimm_base n1 t2)
+  | _ => mullimm_base n1 e2
+  end.
+
+Nondetfunction mull (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.mull e1 e2 else
+  match e1, e2 with
+  | Eop (Olongconst n1) Enil, t2 => mullimm n1 t2
+  | t1, Eop (Olongconst n2) Enil => mullimm n2 t1
+  | _, _ => Eop Omull (e1:::e2:::Enil)
+  end.
+
+Definition divl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.divl e1 e2 else
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 => longconst (Int64.divs n1 n2)
+  | _, _ => Eop Odivl (e1:::e2:::Enil)
+  end.
+
+Definition modl (e1: expr) (e2: expr) :=
+  if Archi.splitlong then SplitLong.modl e1 e2 else
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 => longconst (Int64.mods n1 n2)
+  | _, _ => Eop Omodl (e1:::e2:::Enil)
+  end.
+
+Definition divlu (e1 e2: expr) :=
+  if Archi.splitlong then SplitLong.divlu e1 e2 else
+  let default := Eop Odivlu (e1:::e2:::Enil) in
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 => longconst (Int64.divu n1 n2)
+  | _, Some n2 =>
+      match Int64.is_power2 n2 with
+      | Some l => shrluimm e1 (Int.repr (Int64.unsigned l))
+      | None   => default
+      end
+  | _, _ => default
+  end.
+
+Definition modlu (e1 e2: expr) :=
+  if Archi.splitlong then SplitLong.modlu e1 e2 else
+  let default := Eop Omodlu (e1:::e2:::Enil) in
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 => longconst (Int64.modu n1 n2)
+  | _, Some n2 =>
+      match Int64.is_power2 n2 with
+      | Some l => andl e1 (longconst (Int64.sub n2 Int64.one))
+      | None   => default
+      end
+  | _, _ => default
+  end.
+
+Definition cmplu (c: comparison) (e1 e2: expr) :=
+  if Archi.splitlong then SplitLong.cmplu c e1 e2 else
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 =>
+      Eop (Ointconst (if Int64.cmpu c n1 n2 then Int.one else Int.zero)) Enil
+  | Some n1, None => Eop (Ocmp (Ccompluimm (swap_comparison c) n1)) (e2:::Enil)
+  | None, Some n2 => Eop (Ocmp (Ccompluimm c n2)) (e1:::Enil)
+  | None, None => Eop (Ocmp (Ccomplu c)) (e1:::e2:::Enil)
+  end.
+
+Definition cmpl (c: comparison) (e1 e2: expr) :=
+  if Archi.splitlong then SplitLong.cmpl c e1 e2 else
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 =>
+      Eop (Ointconst (if Int64.cmp c n1 n2 then Int.one else Int.zero)) Enil
+  | Some n1, None => Eop (Ocmp (Ccomplimm (swap_comparison c) n1)) (e2:::Enil)
+  | None, Some n2 => Eop (Ocmp (Ccomplimm c n2)) (e1:::Enil)
+  | None, None => Eop (Ocmp (Ccompl c)) (e1:::e2:::Enil)
+  end.
+
+Definition longoffloat (e: expr) :=
+  if Archi.splitlong then SplitLong.longoffloat e else 
+  Eop Olongoffloat (e:::Enil).
+
+Definition floatoflong (e: expr) := 
+  if Archi.splitlong then SplitLong.floatoflong e else 
+  Eop Ofloatoflong (e:::Enil).
+
+Definition longofsingle (e: expr) := 
+  if Archi.splitlong then SplitLong.longofsingle e else 
+  Eop Olongofsingle (e:::Enil).
+
+Definition singleoflong (e: expr) := 
+  if Archi.splitlong then SplitLong.singleoflong e else 
+  Eop Osingleoflong (e:::Enil).
+
+End SELECT.