From 9cf4ca7760982b40e5721b2d6510eae0ced248a8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 10 Mar 2020 09:11:12 +0100 Subject: forward_move_l --- backend/CSE3analysis.v | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'backend/CSE3analysis.v') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index bbe76f75..c88f06fa 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -128,14 +128,18 @@ Definition get_moves (eqs : PTree.t equation) : Record eq_context := mkeqcontext { eq_catalog : node -> option equation; - eq_kills : reg -> PSet.t; + eq_kill_reg : reg -> PSet.t; + eq_kill_mem : PSet.t; eq_moves : reg -> PSet.t }. Section OPERATIONS. Context {ctx : eq_context}. Definition kill_reg (r : reg) (rel : RELATION.t) : RELATION.t := - PSet.subtract rel (eq_kills ctx r). + PSet.subtract rel (eq_kill_reg ctx r). + + Definition kill_mem (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_mem ctx). Definition pick_source (l : list reg) := (* todo: take min? *) match l with @@ -159,7 +163,9 @@ Section OPERATIONS. | _ => x end end. - + + Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := + List.map (forward_move rel). End OPERATIONS. Definition totoro := RELATION.lub. -- cgit