From f642817f0dc761e51c3bd362f75b0068a8d4b0c8 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 28 Apr 2017 15:56:59 +0200 Subject: RISC-V port and assorted changes This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress. --- riscV/Stacklayout.v | 147 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 riscV/Stacklayout.v (limited to 'riscV/Stacklayout.v') diff --git a/riscV/Stacklayout.v b/riscV/Stacklayout.v new file mode 100644 index 00000000..ba116380 --- /dev/null +++ b/riscV/Stacklayout.v @@ -0,0 +1,147 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Machine- and ABI-dependent layout information for activation records. *) + +Require Import Coqlib. +Require Import AST Memory Separation. +Require Import Bounds. + +Local Open Scope sep_scope. + +(** The general shape of activation records is as follows, + from bottom (lowest offsets) to top: +- Space for outgoing arguments to function calls. +- Back link to parent frame +- Return address +- Saved values of callee-save registers used by the function. +- Local stack slots. +- Space for the stack-allocated data declared in Cminor. + +The stack pointer is kept 16-aligned. +*) + +Definition fe_ofs_arg := 0. + +Definition make_env (b: bounds) : frame_env := + let w := if Archi.ptr64 then 8 else 4 in + let olink := align (4 * b.(bound_outgoing)) w in (* back link *) + let oretaddr := olink + w in (* return address *) + let ocs := oretaddr + w in (* callee-saves *) + let ol := align (size_callee_save_area b ocs) 8 in (* locals *) + let ostkdata := align (ol + 4 * b.(bound_local)) 8 in (* stack data *) + let sz := align (ostkdata + b.(bound_stack_data)) 16 in + {| fe_size := sz; + fe_ofs_link := olink; + fe_ofs_retaddr := oretaddr; + fe_ofs_local := ol; + fe_ofs_callee_save := ocs; + fe_stack_data := ostkdata; + fe_used_callee_save := b.(used_callee_save) |}. + +Lemma frame_env_separated: + forall b sp m P, + let fe := make_env b in + m |= range sp 0 (fe_stack_data fe) ** range sp (fe_stack_data fe + bound_stack_data b) (fe_size fe) ** P -> + m |= range sp (fe_ofs_local fe) (fe_ofs_local fe + 4 * bound_local b) + ** range sp fe_ofs_arg (fe_ofs_arg + 4 * bound_outgoing b) + ** range sp (fe_ofs_link fe) (fe_ofs_link fe + size_chunk Mptr) + ** range sp (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + size_chunk Mptr) + ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) + ** P. +Proof. +Local Opaque Z.add Z.mul sepconj range. + intros; simpl. + set (w := if Archi.ptr64 then 8 else 4). + set (olink := align (4 * b.(bound_outgoing)) w). + set (oretaddr := olink + w). + set (ocs := oretaddr + w). + set (ol := align (size_callee_save_area b ocs) 8). + set (ostkdata := align (ol + 4 * b.(bound_local)) 8). + replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto). + assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. + assert (0 <= 4 * b.(bound_outgoing)) by omega. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). + assert (olink + w <= oretaddr) by (unfold oretaddr; omega). + assert (oretaddr + w <= ocs) by (unfold ocs; omega). + assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). + assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). +(* Reorder as: + outgoing + back link + retaddr + callee-save + local *) + rewrite sep_swap12. + rewrite sep_swap23. + rewrite sep_swap34. + rewrite sep_swap45. +(* Apply range_split and range_split2 repeatedly *) + unfold fe_ofs_arg. + apply range_split_2. fold olink; omega. omega. + apply range_split. omega. + apply range_split. omega. + apply range_split_2. fold ol. omega. omega. + apply range_drop_right with ostkdata. omega. + eapply sep_drop2. eexact H. +Qed. + +Lemma frame_env_range: + forall b, + let fe := make_env b in + 0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size fe. +Proof. + intros; simpl. + set (w := if Archi.ptr64 then 8 else 4). + set (olink := align (4 * b.(bound_outgoing)) w). + set (oretaddr := olink + w). + set (ocs := oretaddr + w). + set (ol := align (size_callee_save_area b ocs) 8). + set (ostkdata := align (ol + 4 * b.(bound_local)) 8). + assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. + assert (0 <= 4 * b.(bound_outgoing)) by omega. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). + assert (olink + w <= oretaddr) by (unfold oretaddr; omega). + assert (oretaddr + w <= ocs) by (unfold ocs; omega). + assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). + assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). + split. omega. apply align_le. omega. +Qed. + +Lemma frame_env_aligned: + forall b, + let fe := make_env b in + (8 | fe_ofs_arg) + /\ (8 | fe_ofs_local fe) + /\ (8 | fe_stack_data fe) + /\ (align_chunk Mptr | fe_ofs_link fe) + /\ (align_chunk Mptr | fe_ofs_retaddr fe). +Proof. + intros; simpl. + set (w := if Archi.ptr64 then 8 else 4). + set (olink := align (4 * b.(bound_outgoing)) w). + set (oretaddr := olink + w). + set (ocs := oretaddr + w). + set (ol := align (size_callee_save_area b ocs) 8). + set (ostkdata := align (ol + 4 * b.(bound_local)) 8). + assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). + split. apply Zdivide_0. + split. apply align_divides; omega. + split. apply align_divides; omega. + split. apply align_divides; omega. + apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl. +Qed. -- cgit