From c0bc146622528e3d52534909f5ae5cd2e375da8f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 5 Aug 2007 13:41:45 +0000 Subject: Documentation git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'cfrontend/Cminorgen.v') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 23faf785..d021a63c 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -26,16 +26,11 @@ Open Local Scope error_monad_scope. taken in the Csharpminor code can be mapped to Cminor local variable, since the latter do not reside in memory. - Other tasks performed during the translation to Cminor: -- Transformation of Csharpminor's standard set of operators and - trivial addressing modes to Cminor's processor-dependent operators - and addressing modes. This is done using the optimizing Cminor - constructor functions provided in file [Cmconstr], therefore performing - instruction selection on the fly. -- Insertion of truncation, zero- and sign-extension operations when + The other task performed during the translation to Cminor is the + insertion of truncation, zero- and sign-extension operations when assigning to a Csharpminor local variable of ``small'' type (e.g. [Mfloat32] or [Mint8signed]). This is necessary to preserve - the ``normalize at assignment-time'' semantics of Csharpminor. + the ``normalize at assignment-time'' semantics of Clight and Csharpminor. *) (** Translation of constants. *) @@ -62,6 +57,12 @@ Definition make_cast (chunk: memory_chunk) (e: expr): expr := | Mfloat64 => e end. +(** When the translation of an expression is stored in memory, + the normalization performed by [make_cast] can be redundant + with that implicitly performed by the memory store. + [store_arg] detects this case and strips away the redundant + normalization. *) + Definition store_arg (chunk: memory_chunk) (e: expr) : expr := match e with | Eunop Ocast8signed e1 => -- cgit