From 4b119d6f9f0e846edccaf5c08788ca1615b22526 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 16 Aug 2009 15:35:09 +0000
Subject: Cil2Csyntax: added goto and labels; added assignment between structs
 Kildall: simplified the interface Constprop, CSE, Allocation, Linearize:
 updated for the new Kildall RTL, LTL: removed the well-formedness condition
 on the CFG,   it is no longer necessary with the new Kildall and it is
 problematic   for validated optimizations. Maps: more efficient
 implementation of PTree.fold.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/RTL.v | 35 +++++++++++++++++++----------------
 1 file changed, 19 insertions(+), 16 deletions(-)

(limited to 'backend/RTL.v')

diff --git a/backend/RTL.v b/backend/RTL.v
index 344d271..5de073e 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -87,9 +87,7 @@ Record function: Type := mkfunction {
   fn_params: list reg;
   fn_stacksize: Z;
   fn_code: code;
-  fn_entrypoint: node;
-  fn_nextpc: node;
-  fn_code_wf: forall (pc: node), Plt pc fn_nextpc \/ fn_code!pc = None
+  fn_entrypoint: node
 }.
 
 (** A function description comprises a control-flow graph (CFG) [fn_code]
@@ -332,6 +330,22 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop :=
 (** Computation of the possible successors of an instruction.
   This is used in particular for dataflow analyses. *)
 
+Definition successors_instr (i: instruction) : list node :=
+  match i with
+  | Inop s => s :: nil
+  | Iop op args res s => s :: nil
+  | Iload chunk addr args dst s => s :: nil
+  | Istore chunk addr args src s => s :: nil
+  | Icall sig ros args res s => s :: nil
+  | Itailcall sig ros args => nil
+  | Icond cond args ifso ifnot => ifso :: ifnot :: nil
+  | Ireturn optarg => nil
+  end.
+
+Definition successors (f: function) : PTree.t (list node) :=
+  PTree.map (fun pc i => successors_instr i) f.(fn_code).
+
+(*
 Definition successors (f: function) (pc: node) : list node :=
   match f.(fn_code)!pc with
   | None => nil
@@ -347,6 +361,7 @@ Definition successors (f: function) (pc: node) : list node :=
       | Ireturn optarg => nil
       end
   end.
+*)
 
 (** Transformation of a RTL function instruction by instruction.
   This applies a given transformation function to all instructions
@@ -356,24 +371,12 @@ Section TRANSF.
 
 Variable transf: node -> instruction -> instruction.
 
-Lemma transf_code_wf:
-  forall (c: code) (nextpc: node),
-  (forall (pc: node), Plt pc nextpc \/ c!pc = None) ->
-  (forall (pc: node), Plt pc nextpc \/ (PTree.map transf c)!pc = None).
-Proof.
-  intros. elim (H pc); intro.
-  left; assumption.
-  right. rewrite PTree.gmap. rewrite H0. reflexivity.
-Qed.
-
 Definition transf_function (f: function) : function :=
   mkfunction
     f.(fn_sig)
     f.(fn_params)
     f.(fn_stacksize)
     (PTree.map transf f.(fn_code))
-    f.(fn_entrypoint)
-    f.(fn_nextpc)
-    (transf_code_wf f.(fn_code) f.(fn_nextpc) f.(fn_code_wf)).
+    f.(fn_entrypoint).
 
 End TRANSF.
-- 
cgit v1.2.3