Module SelectLong

Instruction selection for 64-bit integer operations

Require Import Coqlib.
Require Import Compopts.
Require Import AST Integers Floats.
Require Import Op CminorSel.
Require Import OpHelpers SelectOp SplitLong.

Local Open Scope cminorsel_scope.

Section SELECT.

Context {hf: helper_functions}.

Detect the SplitLong.longofint shape: Elet a (Eop Omakelong (Eop (Oshift (Sasr 31)) (Eletvar 0 ::: Enil) ::: Eletvar 0 ::: Enil)). If matched, return the underlying 32-bit expression so that signed widening multiplication can be lowered to a single Psmull.

Definition is_longofint_signed (e: expr) : option expr :=
  match e with
  | Elet a (Eop Omakelong
              (Eop (Oshift (Sasr c)) (Eletvar O ::: Enil)
               ::: Eletvar O ::: Enil)) =>
      if Int.eq (s_amount c) (Int.repr 31) then Some a else None
  | _ => None
  end.

Override mull to detect signed widening multiplication (int64)a * (int64)b and emit a single __builtin_smull (lowered to Psmull).

Definition mull (e1 e2: expr) : expr :=
  match is_longofint_signed e1, is_longofint_signed e2 with
  | Some a, Some b =>
      Ebuiltin (EF_builtin "__builtin_smull" sig_ii_l) (a ::: b ::: Enil)
  | _, _ => SplitLong.mull e1 e2
  end.

Override cmplu/cmpl for the four ordered comparisons so that they emit Eop (Ocmp (Ccompcarryu/Ccompcarry c)) over the four split halves. Wrapping the comparison in Ocmp of a condition lets Selection.condition_of_expr strip Ocmp when the result feeds an if/Sifthenelse, giving a direct cmp+sbcs+b<cc> branch (3 instructions). When used as a value, the existing Ocmp-of-condition path lowers to cmp+sbcs+movite (4 instructions), versus SplitLong's Econdition-tree (~11 instructions). Ceq/Cne go on the existing SplitLong path: they have a tight xor; xor; or lowering already.

Definition cmplu_via_carry (c: comparison) (e1 e2: expr) : expr :=
  Eop (Ocmp (Ccompcarryu c))
      (highlong e1 ::: lowlong e1 ::: highlong e2 ::: lowlong e2 ::: Enil).

Definition cmpl_via_carry (c: comparison) (e1 e2: expr) : expr :=
  Eop (Ocmp (Ccompcarry c))
      (highlong e1 ::: lowlong e1 ::: highlong e2 ::: lowlong e2 ::: Enil).

Definition cmplu (c: comparison) (e1 e2: expr) : expr :=
  match c with
  | Ceq | Cne => SplitLong.cmplu c e1 e2
  | _ => cmplu_via_carry c e1 e2
  end.

Definition cmpl (c: comparison) (e1 e2: expr) : expr :=
  match c with
  | Ceq | Cne => SplitLong.cmpl c e1 e2
  | _ => cmpl_via_carry c e1 e2
  end.

End SELECT.