diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-03-23 19:12:19 +0100 |
commit | dcb523736e82d72b03fa8d055bf74472dba7345c (patch) | |
tree | 71e797c92d45dca509527043d233c51b2ed8fc86 /kvx | |
parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
parent | 6bf310dd678285dc193798e89fc2c441d8430892 (diff) | |
download | compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.tar.gz compcert-kvx-dcb523736e82d72b03fa8d055bf74472dba7345c.zip |
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
Diffstat (limited to 'kvx')
-rw-r--r-- | kvx/Asmexpand.ml | 6 | ||||
-rw-r--r-- | kvx/Conventions1.v | 45 | ||||
-rw-r--r-- | kvx/TargetPrinter.ml | 10 |
3 files changed, 38 insertions, 23 deletions
diff --git a/kvx/Asmexpand.ml b/kvx/Asmexpand.ml index 1e76a355..35c980bb 100644 --- a/kvx/Asmexpand.ml +++ b/kvx/Asmexpand.ml @@ -103,7 +103,7 @@ let fixup_variadic_call pos tyl = assert false *) let fixup_call sg = - if sg.sig_cc.cc_vararg then fixup_variadic_call 0 sg.sig_args + if sg.sig_cc.cc_vararg <> None then fixup_variadic_call 0 sg.sig_args (* Handling of annotations *) @@ -501,7 +501,7 @@ let expand_instruction instr = | Pallocframe (sz, ofs) -> let sg = get_current_function_sig() in emit (Pmv (Asmvliw.GPR17, stack_pointer)); - if sg.sig_cc.cc_vararg then begin + if sg.sig_cc.cc_vararg <> None then begin let n = arguments_size sg in let extra_sz = if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize) in let full_sz = Z.add sz (Z.of_uint extra_sz) in @@ -524,7 +524,7 @@ let expand_instruction instr = | Pfreeframe (sz, ofs) -> let sg = get_current_function_sig() in let extra_sz = - if sg.sig_cc.cc_vararg then begin + if sg.sig_cc.cc_vararg <> None then begin let n = arguments_size sg in if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize) end else 0 in diff --git a/kvx/Conventions1.v b/kvx/Conventions1.v index 0b2cf406..d8eff34e 100644 --- a/kvx/Conventions1.v +++ b/kvx/Conventions1.v @@ -240,11 +240,18 @@ Fixpoint loc_arguments_rec (va: bool) *) end. +(* FIX Sylvain: not sure to understand what I have done... *) +Definition has_va (s: signature) : bool := + match s.(sig_cc).(cc_vararg) with + | Some n => true + | None => false + 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_cc).(cc_vararg) s.(sig_args) 0 0. + loc_arguments_rec (has_va s) s.(sig_args) 0 0. (** [size_arguments s] returns the number of [Outgoing] slots used to call a function with signature [s]. *) @@ -287,11 +294,11 @@ Proof. assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typealign ty) >= 0). { intros. assert (ofs <= align ofs (typealign ty)) by (apply align_le; apply typealign_pos). - omega. } + lia. } assert (SK: (if Archi.ptr64 then 2 else 1) > 0). - { destruct Archi.ptr64; omega. } + { destruct Archi.ptr64; lia. } assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0). - { intros. destruct Archi.ptr64. omega. apply typesize_pos. } + { intros. destruct Archi.ptr64. lia. apply typesize_pos. } assert (A: forall regs rn ofs ty f, OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)). { intros until f; intros OR OF OO; red; unfold one_arg; intros. @@ -300,7 +307,7 @@ Proof. - eapply OF; eauto. - subst p; cbn. auto using align_divides, typealign_pos. - eapply OF; [idtac|eauto]. - generalize (AL ofs ty OO) (SKK ty); omega. + generalize (AL ofs ty OO) (SKK ty); lia. } assert (B: forall regs rn ofs f, OKREGS regs -> OKF f -> ofs >= 0 -> OK (two_args regs rn ofs f)). @@ -312,8 +319,8 @@ Proof. :: f rn' (ofs' + 2))). { red; cbn; intros. destruct H. - subst p; cbn. - repeat split; auto using Z.divide_1_l. omega. - - eapply OF; [idtac|eauto]. omega. + repeat split; auto using Z.divide_1_l. lia. + - eapply OF; [idtac|eauto]. lia. } destruct (list_nth_z regs rn') as [r1|] eqn:NTH1; destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2; @@ -330,7 +337,7 @@ Proof. - subst p; cbn. apply OR. eapply list_nth_z_in; eauto. - eapply OF; eauto. - subst p; cbn. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. - - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); cbn; omega. + - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); cbn; lia. } assert (D: OKREGS param_regs). { red. decide_goal. } @@ -359,7 +366,7 @@ Lemma loc_arguments_acceptable: forall (s: signature) (p: rpair loc), In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p. Proof. - unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. omega. + unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. lia. Qed. (** The offsets of [Outgoing] arguments are below [size_arguments s]. *) @@ -368,9 +375,9 @@ Remark fold_max_outgoing_above: forall l n, fold_left max_outgoing_2 l n >= n. Proof. assert (A: forall n l, max_outgoing_1 n l >= n). - { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } + { intros; unfold max_outgoing_1. destruct l as [_ | []]; lia. } induction l; cbn; intros. - - omega. + - lia. - eapply Zge_trans. eauto. destruct a; cbn. apply A. eapply Zge_trans; eauto. Qed. @@ -388,14 +395,14 @@ Lemma loc_arguments_bounded: Proof. intros until ty. assert (A: forall n l, n <= max_outgoing_1 n l). - { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } + { intros; unfold max_outgoing_1. destruct l as [_ | []]; lia. } assert (B: forall p n, In (S Outgoing ofs ty) (regs_of_rpair p) -> ofs + typesize ty <= max_outgoing_2 n p). { intros. destruct p; cbn in H; intuition; subst; cbn. - - xomega. - - eapply Z.le_trans. 2: apply A. xomega. - - xomega. } + - lia. + - eapply Z.le_trans. 2: apply A. lia. + - lia. } assert (C: forall l n, In (S Outgoing ofs ty) (regs_of_rpairs l) -> ofs + typesize ty <= fold_left max_outgoing_2 l n). @@ -415,4 +422,10 @@ Proof. Qed. -Definition return_value_needs_normalization (t: rettype) : bool := false. +(** ** Normalization of function results and parameters *) + +(** No normalization needed. *) + +Definition return_value_needs_normalization (t: rettype): bool := false. +Definition parameter_needs_normalization (t: rettype): bool := false. + diff --git a/kvx/TargetPrinter.ml b/kvx/TargetPrinter.ml index 5b6230ca..9e2e3776 100644 --- a/kvx/TargetPrinter.ml +++ b/kvx/TargetPrinter.ml @@ -201,14 +201,16 @@ module Target (*: TARGET*) = let name_of_section = function | Section_text -> ".text" - | Section_data(true, true) -> + | Section_data(Init, true) -> ".section .tdata,\"awT\",@progbits" - | Section_data(false, true) -> + | Section_data(Uninit, true) -> ".section .tbss,\"awT\",@nobits" + | Section_data(Init_reloc, true) -> + failwith "Sylvain does not how to fix this" | Section_data(i, false) | Section_small_data(i) -> - (if i then ".data" else "COMM") + variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - if i then ".section .rodata" else "COMM" + variable_section ~sec:".section .rodata" i | Section_string -> ".section .rodata" | Section_literal -> ".section .rodata" | Section_jumptable -> ".section .rodata" |