From 7dd2fce8926e3d9fa30ad2619dd38c5e2d535a5e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 27 Jan 2020 20:27:20 +0100 Subject: goes to the end but does not find available ops --- backend/CSE2.v | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) (limited to 'backend/CSE2.v') diff --git a/backend/CSE2.v b/backend/CSE2.v index 36558033..d5412d73 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -621,23 +621,16 @@ Definition forward_map (f : RTL.function) := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). -(* -Definition get_r (rel : RELATION.t) (x : reg) := - match move_cases (PTree.get x rel) with - | Move_case x' => x' - | Other_case _ => x - end. - -Definition get_rb (rb : RB.t) (x : reg) := +Definition forward_move_b (rb : RB.t) (x : reg) := match rb with | None => x - | Some rel => get_r rel x + | Some rel => forward_move rel x end. Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg := match fmap with | None => x - | Some inv => get_rb (PMap.get pc inv) x + | Some inv => forward_move_b (PMap.get pc inv) x end. Definition subst_args fmap pc := List.map (subst_arg fmap pc). @@ -648,8 +641,8 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) match instr with | Iop op args dst s => Iop op (subst_args fmap pc args) dst s - | Iload trap chunk addr args dst s => - Iload trap chunk addr (subst_args fmap pc args) dst s + | Iload chunk addr args dst s => + Iload chunk addr (subst_args fmap pc args) dst s | Istore chunk addr args src s => Istore chunk addr (subst_args fmap pc args) src s | Icall sig ros args dst s => @@ -678,4 +671,3 @@ Definition transf_fundef (fd: fundef) : fundef := Definition transf_program (p: program) : program := transform_program transf_fundef p. -*) \ No newline at end of file -- cgit