From 213bf38509f4f92545d4c5749c25a55b9a9dda36 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 3 Aug 2009 15:32:27 +0000 Subject: Transition semantics for Clight and Csharpminor git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 115 +++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 96 insertions(+), 19 deletions(-) (limited to 'cfrontend/Cminorgen.v') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 1045d1a0..5977dedd 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -38,11 +38,15 @@ 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. - The other task performed during the translation to Cminor is the + Another 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 Clight and Csharpminor. + + Finally, the Clight-like [switch] construct of Csharpminor + is transformed into the simpler, lower-level [switch] construct + of Cminor. *) (** Translation of constants. *) @@ -190,9 +194,50 @@ Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr) OK (te1 :: te2) end. -(** Translation of statements. Entirely straightforward. *) +(** To translate [switch] statements, we wrap the statements associated with + the various cases in a cascade of nested Cminor blocks. + The multi-way branch is performed by a Cminor [switch] + statement that exits to the appropriate case. For instance: +<< +switch (e) { ---> block { block { block { + case N1: s1; switch (e) { N1: exit 0; N2: exit 1; default: exit 2; } + case N2: s2; } ; s1 // with exits shifted by 2 + default: s; } ; s2 // with exits shifted by 1 +} } ; s // with exits unchanged +>> + To shift [exit] statements appropriately, we use a second + compile-time environment, of type [exit_env], which + records the blocks inserted during the translation. + A [true] element means the block was present in the original code; + a [false] element, that it was inserted during translation. +*) + +Definition exit_env := list bool. + +Fixpoint shift_exit (e: exit_env) (n: nat) {struct e} : nat := + match e, n with + | nil, _ => n + | false :: e', _ => S (shift_exit e' n) + | true :: e', O => O + | true :: e', S m => S (shift_exit e' m) + end. + +Fixpoint switch_table (ls: lbl_stmt) (k: nat) {struct ls} : list (int * nat) := + match ls with + | LSdefault _ => nil + | LScase ni _ rem => (ni, k) :: switch_table rem (S k) + end. + +Fixpoint switch_env (ls: lbl_stmt) (e: exit_env) {struct ls}: exit_env := + match ls with + | LSdefault _ => e + | LScase _ _ ls' => false :: switch_env ls' e + end. + +(** Translation of statements. The only nonobvious part is + the translation of [switch] statements, outlined above. *) -Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) +Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) {struct s}: res stmt := match s with | Csharpminor.Sskip => @@ -213,28 +258,47 @@ Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) do s <- var_set cenv id (Evar id); OK (Sseq (Scall (Some id) sig te tel) s) | Csharpminor.Sseq s1 s2 => - do ts1 <- transl_stmt cenv s1; - do ts2 <- transl_stmt cenv s2; + do ts1 <- transl_stmt cenv xenv s1; + do ts2 <- transl_stmt cenv xenv s2; OK (Sseq ts1 ts2) | Csharpminor.Sifthenelse e s1 s2 => do te <- transl_expr cenv e; - do ts1 <- transl_stmt cenv s1; - do ts2 <- transl_stmt cenv s2; + do ts1 <- transl_stmt cenv xenv s1; + do ts2 <- transl_stmt cenv xenv s2; OK (Sifthenelse te ts1 ts2) | Csharpminor.Sloop s => - do ts <- transl_stmt cenv s; + do ts <- transl_stmt cenv xenv s; OK (Sloop ts) | Csharpminor.Sblock s => - do ts <- transl_stmt cenv s; + do ts <- transl_stmt cenv (true :: xenv) s; OK (Sblock ts) | Csharpminor.Sexit n => - OK (Sexit n) - | Csharpminor.Sswitch e cases default => - do te <- transl_expr cenv e; OK(Sswitch te cases default) + OK (Sexit (shift_exit xenv n)) + | Csharpminor.Sswitch e ls => + let cases := switch_table ls O in + let default := length cases in + do te <- transl_expr cenv e; + transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch te cases default) | Csharpminor.Sreturn None => OK (Sreturn None) | Csharpminor.Sreturn (Some e) => do te <- transl_expr cenv e; OK (Sreturn (Some te)) + | Csharpminor.Slabel lbl s => + do ts <- transl_stmt cenv xenv s; OK (Slabel lbl ts) + | Csharpminor.Sgoto lbl => + OK (Sgoto lbl) + end + +with transl_lblstmt (cenv: compilenv) (xenv: exit_env) + (ls: Csharpminor.lbl_stmt) (body: stmt) + {struct ls}: res stmt := + match ls with + | Csharpminor.LSdefault s => + do ts <- transl_stmt cenv xenv s; + OK (Sseq (Sblock body) ts) + | Csharpminor.LScase _ s ls' => + do ts <- transl_stmt cenv xenv s; + transl_lblstmt cenv (List.tail xenv) ls' (Sseq (Sblock body) ts) end. (** Computation of the set of variables whose address is taken in @@ -279,9 +343,18 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := | Csharpminor.Sloop s => addr_taken_stmt s | Csharpminor.Sblock s => addr_taken_stmt s | Csharpminor.Sexit n => Identset.empty - | Csharpminor.Sswitch e cases default => addr_taken_expr e + | Csharpminor.Sswitch e ls => + Identset.union (addr_taken_expr e) (addr_taken_lblstmt ls) | Csharpminor.Sreturn None => Identset.empty | Csharpminor.Sreturn (Some e) => addr_taken_expr e + | Csharpminor.Slabel lbl s => addr_taken_stmt s + | Csharpminor.Sgoto lbl => Identset.empty + end + +with addr_taken_lblstmt (ls: Csharpminor.lbl_stmt): Identset.t := + match ls with + | Csharpminor.LSdefault s => addr_taken_stmt s + | Csharpminor.LScase _ s ls' => Identset.union (addr_taken_stmt s) (addr_taken_lblstmt ls') end. (** Layout of the Cminor stack data block and construction of the @@ -362,18 +435,22 @@ Fixpoint store_parameters otherwise address computations within the stack block could overflow machine arithmetic and lead to incorrect code. *) -Definition transl_function - (gce: compilenv) (f: Csharpminor.function): res function := - let (cenv, stacksize) := build_compilenv gce f in - if zle stacksize Int.max_signed then - do tbody <- transl_stmt cenv f.(Csharpminor.fn_body); +Definition transl_funbody + (cenv: compilenv) (stacksize: Z) (f: Csharpminor.function): res function := + do tbody <- transl_stmt cenv nil f.(Csharpminor.fn_body); do sparams <- store_parameters cenv f.(Csharpminor.fn_params); OK (mkfunction (Csharpminor.fn_sig f) (Csharpminor.fn_params_names f) (Csharpminor.fn_vars_names f) stacksize - (Sseq sparams tbody)) + (Sseq sparams tbody)). + +Definition transl_function + (gce: compilenv) (f: Csharpminor.function): res function := + let (cenv, stacksize) := build_compilenv gce f in + if zle stacksize Int.max_signed + then transl_funbody cenv stacksize f else Error(msg "Cminorgen: too many local variables, stack size exceeded"). Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): res fundef := -- cgit