From a5be6f574c3b001254c9b370762045f1675702c1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Jan 2020 11:16:50 +0100 Subject: transfer function --- backend/ForwardMoves.v | 45 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 44 insertions(+), 1 deletion(-) (limited to 'backend/ForwardMoves.v') diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v index 317ffd8c..ae836c1a 100644 --- a/backend/ForwardMoves.v +++ b/backend/ForwardMoves.v @@ -8,6 +8,8 @@ Definition t := (PTree.t reg). Definition eq (r1 r2 : t) := forall x, (PTree.get x r1) = (PTree.get x r2). +Definition top : t := PTree.empty reg. + Lemma eq_refl: forall x, eq x x. Proof. unfold eq. @@ -127,7 +129,7 @@ Module Type SEMILATTICE_WITHOUT_BOTTOM. End SEMILATTICE_WITHOUT_BOTTOM. -Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM) : SEMILATTICE. +Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM). Definition t := option L.t. Definition eq (a b : t) := match a, b with @@ -223,3 +225,44 @@ Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM) : SEMILATTICE. Qed. End ADD_BOTTOM. +Module RB := ADD_BOTTOM(RELATION). +Module DS := Dataflow_Solver(RB)(NodeSetForward). + +Definition kill (dst : reg) (rel : RELATION.t) := + PTree.remove dst rel. + +Definition move (src dst : reg) (rel : RELATION.t) := + PTree.set dst src rel. + +Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) := + match res with + | BR z => kill z rel + | BR_none => rel + | BR_splitlong hi lo => kill_builtin_res hi (kill_builtin_res lo rel) + end. + +Definition apply_instr instr x := + match instr with + | Inop _ + | Istore _ _ _ _ _ => Some x + | Iop Omove (src :: nil) dst _ => Some (move src dst x) + | Iop _ _ dst _ + | Iload _ _ _ _ dst _ + | Icall _ _ _ dst _ => Some (kill dst x) + | Ibuiltin _ _ res _ => Some (kill_builtin_res res x) + | Icond _ _ _ _ | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot + end. + +Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t := + match ro with + | None => None + | Some x => + match code ! pc with + | None => RB.bot + | Some instr => apply_instr instr x + end + end. + +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). \ No newline at end of file -- cgit