How to deal MWP analysis over CFG ?
SSA Intermediate Representation is presented as a Control Flow Graph.
It means we have to "detect" loops and if-then-else structure by ourself. We're thinking there are 3 methods (@seiller, sorry but I still didn't get the 3rd one maybe you can edit this post for more precision ^^)
-
Tarjan path algo : when detecting a junction point (means the current program point has several predecessors) we can compute the common dominator program point of the predecessors and run a Tarjan algorithm to build all possible paths from that common dominator to the current program point. For each path correspond a matrix, we can then sum them.
-
LLVM pass implementation (kind of opposite of 1.) : when a program point is an
if-then-else
instruction, we use post-dominance tree to figure out where is the junction pointjp
of his successorss1, s2, …, sn
. We can recursively compute each sub-program matrices by starting with each successors as entry point andjp
as terminal program point. -
As I understood we could just figure out what does mean a junction point regarding to our MWP matrices (a sum of predecessors matrices seems not be sufficient for me but something else ?) and what does mean a branching point ?
For information, SSA function is a represented as below (from SSA.v) :
Inductive instruction: Type :=
| Inop: node -> instruction
(** No operation -- just branch to the successor. *)
| Iop: operation -> list reg -> reg -> node -> instruction
(** [Iop op args dst succ] performs the arithmetic operation [op]
over the values of registers [args], stores the result in [dst],
and branches to [succ]. *)
[...]
| Icond: condition -> list reg -> node -> node -> instruction
(** [Icond cond args ifso ifnot] evaluates the boolean condition
[cond] over the values of registers [args]. If the condition
is true, it transitions to [ifso]. If the condition is false,
it transitions to [ifnot]. *)
| Ijumptable: reg -> list node -> instruction
(** [Ijumptable arg tbl] transitions to the node that is the [n]-th
element of the list [tbl], where [n] is the signed integer
value of register [arg]. *)
| Ireturn: option reg -> instruction.
(** [Ireturn] terminates the execution of the current function
(it has no successor). It returns the value of the given
register, or [Vundef] if none is given. *)
Definition code: Type := PTree.t instruction. (* PTree.t is a map with keys in Z *)
Record function: Type := mkfunction {
fn_sig: signature;
fn_params: list reg;
fn_code: code;
fn_phicode: phicode;
fn_entrypoint: node;
[...]
}.