ifds2.mlog

module type IFDS_PROGRAM = sig
  type procedure

  type point

  (* intra-procedural edges *)
  edge : point * point

  (* edge from a procedure call to first node in procedure *)
  start_edge : procedure * point

  (* call edge from one procedure to another *)
  call : point * procedure

  (* return (callsite, exitnode, returnnode) *)
  return : point * point * point

  (* set of procedures that are called initially *)
  initial : procedure
end

module type IFDS_PROGRAM_EXT = sig
  type procedure
  type point
  type entry_fact
  type fact

  edge : point * fact * point * fact

  start_edge : procedure * entry_fact * point * fact

  call : point * fact * procedure * entry_fact

  return : point * fact * point * fact * point * fact

  initial : procedure * entry_fact
end

module IFDS_of_Extended (P : IFDS_PROGRAM_EXT) = struct
  type procedure = P.procedure * P.entry_fact
  type point = P.point * P.fact

  define
    edge : point * point
    edge ((?n,?s), (?n',?s')) :- P.edge (?n, ?s, ?n', ?s')

  define
    start_edge : procedure * point
    start_edge ((?p, ?ef), (?n, ?s)) :- P.start_edge (?p, ?ef, ?n, ?s)

  define
    call : point * procedure
    call ((?n, ?s), (?p, ?ef)) :- P.call (?n, ?s, ?p, ?ef)

  define
    return : point * point * point
    return ((?nc,?sc), (?ne, ?se), (?nr, ?sr)) :-
      P.return (?nc, ?sc, ?ne, ?se, ?nr, ?sr)

  define
    initial : procedure
    initial ((?p, ?ef)) :- P.initial (?p, ?ef)
end

module IFDS (P : IFDS_PROGRAM) = struct

  define
    intra : P.procedure * P.point
    intra (?Proc, ?Node) :- invoked (?Proc), P.start_edge (?Proc, ?Node)
    intra (?Proc, ?Node) :- intra (?Proc, ?Node'), P.edge (?Node', ?Node)
    intra (?Proc, ?Node) :- intra (?Proc, ?Node'), callreturn (?Node', ?Node)

  and
    invoked : P.procedure
    invoked (?Proc) :- P.initial (?Proc)
    invoked (?Proc) :- callsite (?Node, ?Proc)

  and
    callsite : P.point * P.procedure
    callsite (?Node, ?CalledProc) :-
       intra (?Proc, ?Node), P.call (?Node, ?CalledProc)

  and
    callreturn : P.point * P.point
    callreturn (?CallNode, ?ReturnNode) :-
       callsite (?CallNode, ?CalledProc),
       intra (?CalledProc, ?ExitNode),
       P.return (?CallNode, ?ExitNode, ?ReturnNode)

end

module Test (P : IFDS_PROGRAM_EXT) = struct
  module P' = IFDS_of_Extended (P)
  module A  = IFDS (P')
end

(* A nonsense example program *)
module P = struct

  type procedure = int

  type point = int * int

  define
      edge : point * point
      edge ((1,4),(2,5))
      edge ((1,2),(4,3))

  define
      start_edge : procedure * point
      start_edge (2,(1,4))

  define
      call : point * procedure
      call ((2,5),2)

  define
      return : point * point * point

  define
      initial : procedure
      initial (1)
end

module A = IFDS (P)