From 82ecfc692b0f84b52162e5f0972fbcc6a9f7f51e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 29 Oct 2020 23:15:49 +0100 Subject: reinstated previous forward_move function --- backend/CSE3analysis.v | 31 ++++++++++++++++++++++++++++--- 1 file changed, 28 insertions(+), 3 deletions(-) (limited to 'backend/CSE3analysis.v') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 34df644e..dbf1afe2 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -236,7 +236,30 @@ Section OPERATIONS. | nil => before end. - Definition pick_source (l : list reg) := + Definition pick_source (l : list reg) := (* todo: take min? *) + match l with + | h::t => Some h + | nil => None + end. + + Definition forward_move1 (rel : RELATION.t) (x : reg) : reg := + match pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x))) with + | None => x + | Some eqno => + match eq_catalog ctx eqno with + | Some eq => + if is_smove (eq_op eq) && peq x (eq_lhs eq) + then + match eq_args eq with + | src::nil => src + | _ => x + end + else x + | _ => x + end + end. + + Definition pick_min_source (l : list reg) := match l with | h::t => Some (reg_min_rec t h) | nil => None @@ -259,11 +282,13 @@ Section OPERATIONS. end end. - Definition forward_move (rel : RELATION.t) (x : reg) : reg := - match pick_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with + Definition forward_move2 (rel : RELATION.t) (x : reg) : reg := + match pick_min_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with | None => x | Some src => src end. + + Definition forward_move := forward_move1. Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := List.map (forward_move rel). -- cgit