From bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 11 Jan 2009 11:57:02 +0000 Subject: - Added alignment constraints to memory loads and stores. - In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'cfrontend/Cminorgen.v') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 755aa28..cc5e5ab 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -287,8 +287,13 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := (** Layout of the Cminor stack data block and construction of the compilation environment. Csharpminor local variables that are arrays or whose address is taken are allocated a slot in the Cminor - stack data. While this is not important for correctness, sufficient - padding is inserted to ensure adequate alignment of addresses. *) + stack data. Sufficient padding is inserted to ensure adequate alignment + of addresses. *) + +Definition array_alignment (sz: Z) : Z := + if zlt sz 2 then 1 + else if zlt sz 4 then 2 + else if zlt sz 8 then 4 else 8. Definition assign_variable (atk: Identset.t) @@ -297,7 +302,7 @@ Definition assign_variable let (cenv, stacksize) := cenv_stacksize in match id_lv with | (id, Varray sz) => - let ofs := align stacksize 8 in + let ofs := align stacksize (array_alignment sz) in (PMap.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz) | (id, Vscalar chunk) => if Identset.mem id atk then -- cgit v1.2.3