From 4b119d6f9f0e846edccaf5c08788ca1615b22526 Mon Sep 17 00:00:00 2001 From: xleroy 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/LTL.v | 31 ++++++++++++++----------------- 1 file changed, 14 insertions(+), 17 deletions(-) (limited to 'backend/LTL.v') diff --git a/backend/LTL.v b/backend/LTL.v index 3a61e6d0..2505566f 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -51,9 +51,7 @@ Record function: Type := mkfunction { fn_params: list loc; 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 }. Definition fundef := AST.fundef function. @@ -256,18 +254,17 @@ 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 (f: function) (pc: node) : list node := - match f.(fn_code)!pc with - | None => nil - | Some i => - match i with - | Lnop s => s :: nil - | Lop op args res s => s :: nil - | Lload chunk addr args dst s => s :: nil - | Lstore chunk addr args src s => s :: nil - | Lcall sig ros args res s => s :: nil - | Ltailcall sig ros args => nil - | Lcond cond args ifso ifnot => ifso :: ifnot :: nil - | Lreturn optarg => nil - end +Definition successors_instr (i: instruction) : list node := + match i with + | Lnop s => s :: nil + | Lop op args res s => s :: nil + | Lload chunk addr args dst s => s :: nil + | Lstore chunk addr args src s => s :: nil + | Lcall sig ros args res s => s :: nil + | Ltailcall sig ros args => nil + | Lcond cond args ifso ifnot => ifso :: ifnot :: nil + | Lreturn optarg => nil end. + +Definition successors (f: function): PTree.t (list node) := + PTree.map (fun pc i => successors_instr i) f.(fn_code). -- cgit