Module Archi

Architecture-dependent parameters for ARM

From Coq Require Import ZArith List Extraction.
From Flocq Require Import Binary Bits.

Definition ptr64 := false.
Definition canary64 := false.

Parameter big_endian: bool.

Definition align_int64 := 8%Z.
Definition align_float64 := 8%Z.

Definition splitlong := true.

Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.

Proof.

unfold splitlong, ptr64; congruence.
Qed.

Parameter expanse_memcpy_fpu: bool.
Extract Constant expanse_memcpy_fpu => "false".

Definition default_nan_64 := (false, iter_nat 51 _ xO xH).
Definition default_nan_32 := (false, iter_nat 22 _ xO xH).

Choose the first signaling NaN, if any; otherwise choose the first NaN; otherwise use default.

Definition choose_nan (is_signaling: positive -> bool)
                      (default: bool * positive)
                      (l0: list (bool * positive)) : bool * positive :=
  let fix choose_snan (l1: list (bool * positive)) :=
    match l1 with
    | nil =>
        match l0 with nil => default | n :: _ => n end
    | ((s, p) as n) :: l1 =>
        if is_signaling p then n else choose_snan l1
    end
  in choose_snan l0.

Lemma choose_nan_idem: forall is_signaling default n,
  choose_nan is_signaling default (n :: n :: nil) =
  choose_nan is_signaling default (n :: nil).

Proof.

intros. destruct n as [s p]; unfold choose_nan; simpl.
destruct (is_signaling p); auto.
Qed.

Definition choose_nan_64 :=
  choose_nan (fun p => negb (Pos.testbit p 51)) default_nan_64.

Definition choose_nan_32 :=
  choose_nan (fun p => negb (Pos.testbit p 22)) default_nan_32.

Lemma choose_nan_64_idem: forall n,
  choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).

Proof.

intros; apply choose_nan_idem. Qed.

Lemma choose_nan_32_idem: forall n,
choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).

Proof.

intros; apply choose_nan_idem. Qed.

Definition fma_order {A: Type} (x y z: A) := (z, x, y).

Definition fma_invalid_mul_is_nan := true.

Definition float_of_single_preserves_sNaN := false.

Definition float_conversion_default_nan := false.

Global Opaque ptr64 big_endian splitlong
              default_nan_64 choose_nan_64
              default_nan_32 choose_nan_32
              fma_order fma_invalid_mul_is_nan
              float_of_single_preserves_sNaN
              float_conversion_default_nan.

Which ABI to use: either the standard ARM EABI with floats passed in integer registers, or the "hardfloat" variant of the EABI that uses FP registers instead.

Inductive abi_kind := Softfloat | Hardfloat.
Parameter abi: abi_kind.

Whether instructions added with Thumb2 are supported. True for ARMv6T2 and above.

Parameter thumb2_support: bool.

Whether the VFPv3 immediate float encodings (vmov.f64 / vmov.f32 with 8-bit immediate) are available. True for ARMv7 and above.

Parameter vfpv3: bool.

Whether the hardware supports unaligned 32-bit loads and stores. True for ARMv6 and later.

Definition has_unaligned_int32 (_ : unit) := true.

Definition has_notrap_loads := false.
Definition has_mulhu := true.
Definition has_mulhs := true.
Definition has_mullhu := true.
Definition has_mullhs := true.

Whether the hardware supports sdiv and udiv

Parameter hardware_idiv : unit -> bool.

Recognition of integer immediate arguments for arithmetic operations.

ARM: immediates are 8-bit quantities zero-extended and rotated right by 0, 2, 4, ... 30 bits. In other words, n is an immediate iff rotate-left(n, p) is between 0 and 255 for some p = 0, 2, 4, ..., 30.
Thumb: immediates are 8-bit quantities zero-extended and shifted left by 0, 1, ..., 31 bits. In other words, n is an immediate if all bits are 0 except a run of 8 adjacent bits. In addition, 00XY00XY and XY00XY00 and XYXYXYXY are immediates for a given XY 8-bit constant.