From c45fc2431ea70e0cb5a80e65d0ac99f91e94693e Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 8 May 2011 07:07:25 +0000
Subject: Added pass CleanupLabels to remove unreferenced labels in a proved
 way. ia32/PrintAsm.ml: simplified accordingly; other PrintAsm.ml to be fixed.
 ia32/Asm.v: Pmov_ri can undef flags (if translated to xor) cparser/Ceval.ml:
 treat ~ in constant exprs

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/CleanupLabels.v | 75 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)
 create mode 100644 backend/CleanupLabels.v

(limited to 'backend/CleanupLabels.v')

diff --git a/backend/CleanupLabels.v b/backend/CleanupLabels.v
new file mode 100644
index 00000000..7401abc6
--- /dev/null
+++ b/backend/CleanupLabels.v
@@ -0,0 +1,75 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Removal of useless labels introduced by the linearization pass.
+  
+  The linearization pass introduces one label for each node of the 
+  control-flow graph.  Many of these labels are never branched to,
+  which can complicate further optimizations over linearized code.
+  (There are no such optimizations yet.)  In preparation for these
+  further optimizations, and to make the generated LTLin code 
+  better-looking, the present pass removes labels that cannot be
+  branched to. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import Ordered.
+Require Import FSets.
+Require FSetAVL.
+Require Import LTLin.
+
+Module Labelset := FSetAVL.Make(OrderedPositive).
+
+(** Compute the set of labels that are mentioned in branch instructions. *)
+
+Definition add_label_branched_to (ls: Labelset.t) (i: instruction) :=
+  match i with
+  | Lgoto lbl => Labelset.add lbl ls
+  | Lcond cond args lbl => Labelset.add lbl ls
+  | Ljumptable arg tbl => List.fold_right Labelset.add ls tbl
+  | _ => ls
+  end.
+
+Definition labels_branched_to (c: code) : Labelset.t :=
+  List.fold_left add_label_branched_to c Labelset.empty.
+
+(** Remove label declarations for labels that are not in
+    the [bto] (branched-to) set. *)
+
+Fixpoint remove_unused_labels (bto: Labelset.t) (c: code) : code :=
+  match c with
+  | nil => nil
+  | Llabel lbl :: c' =>
+      if Labelset.mem lbl bto
+      then Llabel lbl :: remove_unused_labels bto c'
+      else remove_unused_labels bto c'
+  | i :: c' =>
+      i :: remove_unused_labels bto c'
+  end.
+
+Definition cleanup_labels (c: code) :=
+  remove_unused_labels (labels_branched_to c) c.
+
+(** Entry points *)
+
+Definition transf_function (f: function) : function :=
+  mkfunction
+     (fn_sig f)
+     (fn_params f)
+     (fn_stacksize f)
+     (cleanup_labels (fn_code f)).
+
+Definition transf_fundef (f: fundef) : fundef :=
+  AST.transf_fundef transf_function f.
+
+Definition transf_program (p: program) : program :=
+  AST.transform_program transf_fundef p.
-- 
cgit