Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit dcb52373 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

Merge branch 'master' into merge_master_8.13.1

PARTIAL MERGE (PARTLY BROKEN).

See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE

WARNING:
 interface of va_args and assembly sections have changed
parents 3e953ef4 6bf310dd
......@@ -49,7 +49,23 @@ RECDIRS += MenhirLib
COQINCLUDES += -R MenhirLib MenhirLib
endif
COQCOPTS ?= -w -undeclared-scope -w -omega-is-deprecated
# Notes on silenced Coq warnings:
#
# undeclared-scope:
# warning introduced in 8.12
# suggested change (use `Declare Scope`) supported since 8.12
# unused-pattern-matching-variable:
# warning introduced in 8.13
# the code rewrite that avoids the warning is not desirable
# deprecated-ident-entry:
# warning introduced in 8.13
# suggested change (use `name` instead of `ident`) supported since 8.13
COQCOPTS ?= \
-w -undeclared-scope \
-w -unused-pattern-matching-variable \
-w -deprecated-ident-entry
COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
COQDOC="$(COQBIN)coqdoc"
......@@ -65,6 +81,7 @@ GPATH=$(DIRS)
ifeq ($(LIBRARY_FLOCQ),local)
FLOCQ=\
SpecFloatCompat.v \
Raux.v Zaux.v Defs.v Digits.v Float_prop.v FIX.v FLT.v FLX.v FTZ.v \
Generic_fmt.v Round_pred.v Round_NE.v Ulp.v Core.v \
Bracket.v Div.v Operations.v Round.v Sqrt.v \
......
......@@ -17,7 +17,7 @@ Require Import Alphabet.
Class IsValidator (P : Prop) (b : bool) :=
is_validator : b = true -> P.
Hint Mode IsValidator + - : typeclass_instances.
Global Hint Mode IsValidator + - : typeclass_instances.
Instance is_validator_true : IsValidator True true.
Proof. done. Qed.
......@@ -55,12 +55,12 @@ Qed.
(* We do not use an instance directly here, because we need somehow to
force Coq to instantiate b with a lambda. *)
Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
Global Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
eapply (is_validator_forall_finite _ _ (fun (x:A) => _))
: typeclass_instances.
(* Hint for synthetizing pattern-matching. *)
Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
Global Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
let b := fresh "b" in
unshelve notypeclasses refine (let b : bool := _ in _);
[destruct u; intros; shelve|]; (* Synthetize `match .. with` in the validator. *)
......@@ -71,5 +71,5 @@ Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
(* Hint for unfolding definitions. This is necessary because many
hints for IsValidator use [Hint Extern], which do not automatically
unfold identifiers. *)
Hint Extern 100 (IsValidator ?X _) => unfold X
Global Hint Extern 100 (IsValidator ?X _) => unfold X
: typeclass_instances.
......@@ -140,7 +140,7 @@ Qed.
(* We do not declare this lemma as an instance, and use [Hint Extern]
instead, because the typeclass mechanism has trouble instantiating
some evars if we do not explicitely call [eassumption]. *)
Hint Extern 2 (IsValidator (state_has_future _ _ _ _) _) =>
Global Hint Extern 2 (IsValidator (state_has_future _ _ _ _) _) =>
eapply is_validator_state_has_future_subset; [eassumption|eassumption || reflexivity|]
: typeclass_instances.
......@@ -171,7 +171,7 @@ Proof.
- destruct (b lookahead). by destruct b'. exfalso. by induction l; destruct b'.
- eauto.
Qed.
Hint Extern 100 (IsValidator _ _) =>
Global Hint Extern 100 (IsValidator _ _) =>
match goal with
| H : TerminalSet.In ?lookahead ?lset |- _ =>
eapply (is_validator_iterate_lset _ (fun lookahead => _) _ _ H); clear H
......@@ -238,7 +238,7 @@ Proof.
revert EQ. unfold future_of_prod=>-> //.
Qed.
(* We need a hint for expplicitely instantiating b1 and b2 with lambdas. *)
Hint Extern 0 (IsValidator
Global Hint Extern 0 (IsValidator
(forall st prod fut lookahead,
state_has_future st prod fut lookahead -> _)
_) =>
......
......@@ -1398,7 +1398,7 @@ Ltac Equalities :=
split. auto. intros. destruct B; auto. subst. auto.
- (* trace length *)
red; intros. inv H; simpl.
omega.
lia.
eapply external_call_trace_length; eauto.
eapply external_call_trace_length; eauto.
- (* initial states *)
......
......@@ -47,17 +47,28 @@ let expand_storeptr (src: ireg) (base: iregsp) ofs =
(* Determine the number of int registers, FP registers, and stack locations
used to pass the fixed parameters. *)
let align n a = (n + a - 1) land (-a)
let typesize = function
| Tint | Tany32 | Tsingle -> 4
| Tlong | Tany64 | Tfloat -> 8
let reserve_stack stk ty =
match Archi.abi with
| Archi.AAPCS64 -> stk + 8
| Archi.Apple -> align stk (typesize ty) + typesize ty
let rec next_arg_locations ir fr stk = function
| [] ->
(ir, fr, stk)
| (Tint | Tlong | Tany32 | Tany64) :: l ->
| (Tint | Tlong | Tany32 | Tany64 as ty) :: l ->
if ir < 8
then next_arg_locations (ir + 1) fr stk l
else next_arg_locations ir fr (stk + 8) l
| (Tfloat | Tsingle) :: l ->
else next_arg_locations ir fr (reserve_stack stk ty) l
| (Tfloat | Tsingle as ty) :: l ->
if fr < 8
then next_arg_locations ir (fr + 1) stk l
else next_arg_locations ir fr (stk + 8) l
else next_arg_locations ir fr (reserve_stack stk ty) l
(* Allocate memory on the stack and use it to save the registers
used for parameter passing. As an optimization, do not save
......@@ -86,6 +97,8 @@ let save_parameter_registers ir fr =
emit (Pstrd(float_param_regs.(i), ADimm(XSP, Z.of_uint pos)))
done
let current_function_stacksize = ref 0L
(* Initialize a va_list as per va_start.
Register r points to the following struct:
......@@ -98,11 +111,7 @@ let save_parameter_registers ir fr =
}
*)
let current_function_stacksize = ref 0L
let expand_builtin_va_start r =
if not (is_current_function_variadic ()) then
invalid_arg "Fatal error: va_start used in non-vararg function";
let expand_builtin_va_start_aapcs64 r =
let (ir, fr, stk) =
next_arg_locations 0 0 0 (get_current_function_args ()) in
let stack_ofs = Int64.(add !current_function_stacksize (of_int stk))
......@@ -127,6 +136,25 @@ let expand_builtin_va_start r =
expand_loadimm32 X16 (coqint_of_camlint (Int32.of_int vr_offs));
emit (Pstrw(X16, ADimm(RR1 r, coqint_of_camlint64 28L)))
(* In macOS, va_list is just a pointer (char * ) and all variadic arguments
are passed on the stack. *)
let expand_builtin_va_start_apple r =
let (ir, fr, stk) =
next_arg_locations 0 0 0 (get_current_function_args ()) in
let stk = align stk 8 in
let stack_ofs = Int64.(add !current_function_stacksize (of_int stk)) in
(* *va = sp + stack_ofs *)
expand_addimm64 (RR1 X16) XSP (coqint_of_camlint64 stack_ofs);
emit (Pstrx(X16, ADimm(RR1 r, coqint_of_camlint64 0L)))
let expand_builtin_va_start r =
if not (is_current_function_variadic ()) then
invalid_arg "Fatal error: va_start used in non-vararg function";
match Archi.abi with
| Archi.AAPCS64 -> expand_builtin_va_start_aapcs64 r
| Archi.Apple -> expand_builtin_va_start_apple r
(* Handling of annotations *)
let expand_annot_val kind txt targ args res =
......@@ -382,7 +410,7 @@ let expand_instruction instr =
match instr with
| Pallocframe (sz, ofs) ->
emit (Pmov (RR1 X29, XSP));
if is_current_function_variadic() then begin
if is_current_function_variadic() && Archi.abi = Archi.AAPCS64 then begin
let (ir, fr, _) =
next_arg_locations 0 0 0 (get_current_function_args ()) in
save_parameter_registers ir fr;
......
......@@ -17,16 +17,28 @@
open C
(* va_list is a struct of size 32 and alignment 8, passed by reference *)
(* AAPCS64:
va_list is a struct of size 32 and alignment 8, passed by reference
Apple:
va_list is a pointer (size 8, alignment 8), passed by reference *)
let va_list_type = TArray(TInt(IULong, []), Some 4L, [])
let size_va_list = 32
let va_list_scalar = false
let (va_list_type, size_va_list, va_list_scalar) =
match Archi.abi with
| Archi.AAPCS64 -> (TArray(TInt(IULong, []), Some 4L, []), 32, false)
| Archi.Apple -> (TPtr(TVoid [], []), 8, true)
(* Some macOS headers use the GCC built-in types "__int128_t" and
"__uint128_t" unconditionally. Provide a dummy definition. *)
let int128_type = TArray(TInt(IULong, []), Some 2L, [])
let builtins = {
builtin_typedefs = [
"__builtin_va_list", va_list_type
];
builtin_typedefs =
[ "__builtin_va_list", va_list_type ] @
(if Configuration.system = "macos" then
[ "__int128_t", int128_type;
"__uint128_t", int128_type ]
else []);
builtin_functions = [
(* Synchronization *)
"__builtin_fence",
......
......@@ -13,11 +13,11 @@
(** Strength reduction for operators and conditions.
This is the machine-dependent part of [Constprop]. *)
Require Archi.
Require Import Coqlib Compopts.
Require Import AST Integers Floats.
Require Import Op Registers.
Require Import ValueDomain ValueAOp.
Require SelectOp.
(** * Converting known values to constants *)
......@@ -375,7 +375,7 @@ Nondetfunction op_strength_reduction
Nondetfunction addr_strength_reduction
(addr: addressing) (args: list reg) (vl: list aval) :=
match addr, args, vl with
| Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil =>
| Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil ?? negb (SelectOp.symbol_is_relocatable symb) =>
(Aglobal symb (Ptrofs.add n1 (Ptrofs.of_int64 n)), nil)
| Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil =>
(Ainstack (Ptrofs.add n1 (Ptrofs.of_int64 n)), nil)
......
......@@ -414,7 +414,7 @@ Proof.
Int.bit_solve. destruct (zlt i0 n0).
replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)).
rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto.
rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto.
rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto.
rewrite Int.bits_not by auto. apply negb_involutive.
rewrite H6 by auto. auto.
econstructor; split; eauto. auto.
......
......@@ -24,7 +24,12 @@ Require Archi.
- Caller-save registers that can be modified during a function call.
We follow the Procedure Call Standard for the ARM 64-bit Architecture
(AArch64) document: R19-R28 and F8-F15 are callee-save. *)
(AArch64) document: R19-R28 and F8-F15 are callee-save.
X16 is reserved as a temporary for asm generation.
X18 is reserved as the platform register.
X29 is reserved as the frame pointer register.
X30 is reserved as the return address register. *)
Definition is_callee_save (r: mreg): bool :=
match r with
......@@ -154,9 +159,23 @@ Qed.
(**
- The first 8 integer arguments are passed in registers [R0...R7].
- The first 8 FP arguments are passed in registers [F0...F7].
- Extra arguments are passed on the stack, in [Outgoing] slots of size
64 bits (2 words), consecutively assigned, starting at word offset 0.
**)
- Extra arguments are passed on the stack, in [Outgoing] slots,
consecutively assigned, starting at word offset 0.
In the standard AAPCS64, all stack slots are 8-byte wide (2 words).
In the Apple variant, a stack slot has the size of the type of the
corresponding argument, and is aligned accordingly. We use 8-byte
slots (2 words) for C types [long] and [double], and 4-byte slots
(1 word) for C types [int] and [float]. For full conformance, we should
use 1-byte slots for [char] types and 2-byte slots for [short] types,
but this cannot be expressed in CompCert's type algebra, so we
incorrectly use 4-byte slots.
Concerning variable arguments to vararg functions:
- In the AAPCS64 standard, they are passed like regular, fixed arguments.
- In the Apple variant, they are always passed on stack, in 8-byte slots.
*)
Definition int_param_regs :=
R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: nil.
......@@ -164,31 +183,70 @@ Definition int_param_regs :=
Definition float_param_regs :=
F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil.
Definition stack_arg (ty: typ) (ir fr ofs: Z)
(rec: Z -> Z -> Z -> list (rpair loc)) :=
match Archi.abi with
| Archi.AAPCS64 =>
let ofs := align ofs 2 in
One (S Outgoing ofs ty) :: rec ir fr (ofs + 2)
| Archi.Apple =>
let ofs := align ofs (typesize ty) in
One (S Outgoing ofs ty) :: rec ir fr (ofs + typesize ty)
end.
Definition int_arg (ty: typ) (ir fr ofs: Z)
(rec: Z -> Z -> Z -> list (rpair loc)) :=
match list_nth_z int_param_regs ir with
| None =>
stack_arg ty ir fr ofs rec
| Some ireg =>
One (R ireg) :: rec (ir + 1) fr ofs
end.
Definition float_arg (ty: typ) (ir fr ofs: Z)
(rec: Z -> Z -> Z -> list (rpair loc)) :=
match list_nth_z float_param_regs fr with
| None =>
stack_arg ty ir fr ofs rec
| Some freg =>
One (R freg) :: rec ir (fr + 1) ofs
end.
Fixpoint loc_arguments_stack (tyl: list typ) (ofs: Z) {struct tyl} : list (rpair loc) :=
match tyl with
| nil => nil
| ty :: tys => One (S Outgoing ofs Tany64) :: loc_arguments_stack tys (ofs + 2)
end.
Fixpoint loc_arguments_rec
(tyl: list typ) (ir fr ofs: Z) {struct tyl} : list (rpair loc) :=
(tyl: list typ) (fixed ir fr ofs: Z) {struct tyl} : list (rpair loc) :=
match tyl with
| nil => nil
| (Tint | Tlong | Tany32 | Tany64) as ty :: tys =>
match list_nth_z int_param_regs ir with
| None =>
One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + 2)
| Some ireg =>
One (R ireg) :: loc_arguments_rec tys (ir + 1) fr ofs
end
| (Tfloat | Tsingle) as ty :: tys =>
match list_nth_z float_param_regs fr with
| None =>
One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + 2)
| Some freg =>
One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs
| ty :: tys =>
if zle fixed 0 then loc_arguments_stack tyl (align ofs 2) else
match ty with
| Tint | Tlong | Tany32 | Tany64 =>
int_arg ty ir fr ofs (loc_arguments_rec tys (fixed - 1))
| Tfloat | Tsingle =>
float_arg ty ir fr ofs (loc_arguments_rec tys (fixed - 1))
end
end.
(** Number of fixed arguments for a function with signature [s].
For AAPCS64, all arguments are treated as fixed, even for a vararg
function. *)
Definition fixed_arguments (s: signature) : Z :=
match Archi.abi, s.(sig_cc).(cc_vararg) with
| Archi.Apple, Some n => n
| _, _ => list_length_z s.(sig_args)
end.
(** [loc_arguments s] returns the list of locations where to store arguments
when calling a function with signature [s]. *)
Definition loc_arguments (s: signature) : list (rpair loc) :=
loc_arguments_rec s.(sig_args) 0 0 0.
loc_arguments_rec s.(sig_args) (fixed_arguments s) 0 0 0.
(** Argument locations are either caller-save registers or [Outgoing]
stack slots at nonnegative offsets. *)
......@@ -200,49 +258,73 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
| _ => False
end.
Definition loc_argument_charact (ofs: Z) (l: loc) : Prop :=
match l with
| R r => In r int_param_regs \/ In r float_param_regs
| S Outgoing ofs' ty => ofs' >= ofs /\ (2 | ofs')
| _ => False
end.
Remark loc_arguments_rec_charact:
forall tyl ir fr ofs p,
In p (loc_arguments_rec tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_charact ofs) p.
Lemma loc_arguments_rec_charact:
forall tyl fixed ri rf ofs p,
ofs >= 0 ->
In p (loc_arguments_rec tyl fixed ri rf ofs) -> forall_rpair loc_argument_acceptable p.
Proof.
assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l).
{ destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact ofs1) p).
{ destruct p; simpl; intuition eauto. }
assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)).
{ intros. apply Z.divide_add_r; auto. apply Z.divide_refl. }
Opaque list_nth_z.
induction tyl; simpl loc_arguments_rec; intros.
- contradiction.
- assert (A: forall ty, In p
match list_nth_z int_param_regs ir with
| Some ireg => One (R ireg) :: loc_arguments_rec tyl (ir + 1) fr ofs
| None => One (S Outgoing ofs ty) :: loc_arguments_rec tyl ir fr (ofs + 2)
end ->
forall_rpair (loc_argument_charact ofs) p).
{ intros. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H1.
subst. left. eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
subst. split. omega. assumption.
eapply Y; eauto. omega. }
assert (B: forall ty, In p
match list_nth_z float_param_regs fr with
| Some ireg => One (R ireg) :: loc_arguments_rec tyl ir (fr + 1) ofs
| None => One (S Outgoing ofs ty) :: loc_arguments_rec tyl ir fr (ofs + 2)
end ->
forall_rpair (loc_argument_charact ofs) p).
{ intros. destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H1.
subst. right. eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
subst. split. omega. assumption.
eapply Y; eauto. omega. }
destruct a; eauto.
set (OK := fun (l: list (rpair loc)) =>
forall p, In p l -> forall_rpair loc_argument_acceptable p).
set (OKF := fun (f: Z -> Z -> Z -> list (rpair loc)) =>
forall ri rf ofs, ofs >= 0 -> OK (f ri rf ofs)).
assert (CSI: forall r, In r int_param_regs -> is_callee_save r = false).
{ decide_goal. }
assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false).
{ decide_goal. }
assert (ALP: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0).
{ intros.
assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos).
lia. }
assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))).
{ intros. apply Z.divide_trans with (typesize ty). apply typealign_typesize. apply align_divides. apply typesize_pos. }
assert (ALP2: forall ofs, ofs >= 0 -> align ofs 2 >= 0).
{ intros.
assert (ofs <= align ofs 2) by (apply align_le; lia).
lia. }
assert (ALD2: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs 2)).
{ intros. eapply Z.divide_trans with 2.
exists (2 / typealign ty). destruct ty; reflexivity.
apply align_divides. lia. }
assert (STK: forall tyl ofs,
ofs >= 0 -> OK (loc_arguments_stack tyl ofs)).
{ induction tyl as [ | ty tyl]; intros ofs OO; red; simpl; intros.
- contradiction.
- destruct H.
+ subst p. split. auto. simpl. apply Z.divide_1_l.
+ apply IHtyl with (ofs := ofs + 2). lia. auto.
}
assert (A: forall ty ri rf ofs f,
OKF f -> ofs >= 0 -> OK (stack_arg ty ri rf ofs f)).
{ intros until f; intros OF OO; red; unfold stack_arg; intros.
destruct Archi.abi; destruct H.
- subst p; simpl; auto.
- eapply OF; [|eauto]. apply ALP2 in OO. lia.
- subst p; simpl; auto.
- eapply OF; [|eauto]. apply (ALP ofs ty) in OO. generalize (typesize_pos ty). lia.
}
assert (B: forall ty ri rf ofs f,
OKF f -> ofs >= 0 -> OK (int_arg ty ri rf ofs f)).
{ intros until f; intros OF OO; red; unfold int_arg; intros.
destruct (list_nth_z int_param_regs ri) as [r|] eqn:NTH; [destruct H|].
- subst p; simpl. apply CSI. eapply list_nth_z_in; eauto.
- eapply OF; eauto.
- eapply A; eauto.
}
assert (C: forall ty ri rf ofs f,
OKF f -> ofs >= 0 -> OK (float_arg ty ri rf ofs f)).
{ intros until f; intros OF OO; red; unfold float_arg; intros.
destruct (list_nth_z float_param_regs rf) as [r|] eqn:NTH; [destruct H|].
- subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
- eapply OF; eauto.
- eapply A; eauto.
}
cut (forall tyl fixed ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec tyl fixed ri rf ofs)).
unfold OK. eauto.
induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl.
- red; simpl; tauto.
- destruct (zle fixed 0).
+ apply (STK (ty1 :: tyl)); auto.
+ unfold OKF in *; destruct ty1; eauto.
Qed.
Lemma loc_arguments_acceptable:
......@@ -250,19 +332,10 @@ Lemma loc_arguments_acceptable:
In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
Proof.
unfold loc_arguments; intros.
assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal.
assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal.
assert (X: forall l, loc_argument_charact 0 l -> loc_argument_acceptable l).
{ unfold loc_argument_charact, loc_argument_acceptable.
destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto.
intros [C D]. split; auto. apply Z.divide_trans with 2; auto.
exists (2 / typealign ty); destruct ty; reflexivity.
}
exploit loc_arguments_rec_charact; eauto using Z.divide_0_r.
unfold forall_rpair; destruct p; intuition auto.
eapply loc_arguments_rec_charact; eauto. lia.
Qed.
Hint Resolve loc_arguments_acceptable: locs.
Global Hint Resolve loc_arguments_acceptable: locs.
Lemma loc_arguments_main:
loc_arguments signature_main = nil.
......@@ -270,16 +343,29 @@ Proof.
unfold loc_arguments; reflexivity.
Qed.
(** ** Normalization of function results *)
(** ** Normalization of function results and parameters *)
(** According to the AAPCS64 ABI specification, "padding bits" in the return
value of a function have unpredictable values and must be ignored.
Consequently, we force normalization of return values of small integer
types (8- and 16-bit integers), so that the top bits (the "padding bits")
are proper sign- or zero-extensions of the small integer value. *)
value of a function or in a function parameter have unpredictable
values and must be ignored. Consequently, we force normalization
of return values and of function parameters when they have small
integer types (8- and 16-bit integers), so that the top bits (the
"padding bits") are proper sign- or zero-extensions of the small
integer value.
The Apple variant of the AAPCS64 requires the callee to return a normalized
value, and the caller to pass normalized parameters, hence no
normalization is needed.
*)
Definition return_value_needs_normalization (t: rettype) : bool :=
match t with
| Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true
| _ => false
match Archi.abi with
| Archi.Apple => false
| Archi.AAPCS64 =>
match t with
| Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true
| _ => false
end
end.
Definition parameter_needs_normalization := return_value_needs_normalization.
......@@ -985,25 +985,25 @@ End SHIFT_AMOUNT.
Program Definition mk_amount32 (n: int): amount32 :=
{| a32_amount := Int.zero_ext 5 n |}.
Next Obligation.
apply mk_amount_range. omega. reflexivity.
apply mk_amount_range. lia. reflexivity.
Qed.
Lemma mk_amount32_eq: forall n,
Int.ltu n Int.iwordsize = true -> a32_amount (mk_amount32 n) = n.
Proof.
intros. eapply mk_amount_eq; eauto. omega. reflexivity.
intros. eapply mk_amount_eq; eauto. lia. reflexivity.
Qed.
Program Definition mk_amount64 (n: int): amount64 :=
{| a64_amount := Int.zero_ext 6 n |}.
Next Obligation.
apply mk_amount_range. omega. reflexivity.
apply mk_amount_range. lia. reflexivity.
Qed.
Lemma mk_amount64_eq: forall n,
Int.ltu n Int64.iwordsize' = true -> a64_amount (mk_amount64 n) = n.
Proof.