Source file dataflow.ml

module IH = Inthash
module E = Errormsg

open Cil
open Pretty

(** A framework for data flow analysis for CIL code.  Before using
    this framework, you must initialize the Control-flow Graph for your
    program, e.g using {!Cfg.computeFileCFG} *)

type 't action =
    Default (** The default action *)
  | Done of 't (** Do not do the default action. Use this result *)
  | Post of ('t -> 't) (** The default action, followed by the given
                        * transformer *)

type 't stmtaction =
    SDefault   (** The default action *)
  | SDone      (** Do not visit this statement or its successors *)
  | SUse of 't (** Visit the instructions and successors of this statement
                  as usual, but use the specified state instead of the
                  one that was passed to doStmt *)

(* For if statements *)
type 't guardaction =
    GDefault      (** The default state *)
  | GUse of 't    (** Use this data for the branch *)
  | GUnreachable  (** The branch will never be taken. *)


(******************************************************************
 **********
 **********         FORWARDS
 **********
 ********************************************************************)

module type ForwardsTransfer = sig
  val name: string (** For debugging purposes, the name of the analysis *)

  val debug: bool ref (** Whether to turn on debugging *)

  type t  (** The type of the data we compute for each block start. May be
           * imperative.  *)

  val copy: t -> t
  (** Make a deep copy of the data *)


  val stmtStartData: t Inthash.t
  (** For each statement id, the data at the start. Not found in the hash
   * table means nothing is known about the state at this point. At the end
   * of the analysis this means that the block is not reachable. *)

  val pretty: unit -> t -> Pretty.doc
  (** Pretty-print the state *)

  val computeFirstPredecessor: Cil.stmt -> t -> t
  (** Give the first value for a predecessors, compute the value to be set
   * for the block *)

  val combinePredecessors: Cil.stmt -> old:t -> t -> t option
  (** Take some old data for the start of a statement, and some new data for
   * the same point. Return None if the combination is identical to the old
   * data. Otherwise, compute the combination, and return it. *)

  val doInstr: Cil.instr -> t -> t action
  (** The (forwards) transfer function for an instruction. The
   * {!Cil.currentLoc} is set before calling this. The default action is to
   * continue with the state unchanged. *)

  val doStmt: Cil.stmt -> t -> t stmtaction
  (** The (forwards) transfer function for a statement. The {!Cil.currentLoc}
   * is set before calling this. The default action is to do the instructions
   * in this statement, if applicable, and continue with the successors. *)

  val doGuard: Cil.exp -> t -> t guardaction
  (** Generate the successor to an If statement assuming the given expression
    * is nonzero.  Analyses that don't need guard information can return
    * GDefault; this is equivalent to returning GUse of the input.
    * A return value of GUnreachable indicates that this half of the branch
    * will not be taken and should not be explored.  This will be called
    * twice per If, once for "then" and once for "else".
    *)

  val filterStmt: Cil.stmt -> bool
  (** Whether to put this statement in the worklist. This is called when a
   * block would normally be put in the worklist. *)

end


module ForwardsDataFlow =
  functor (T : ForwardsTransfer) ->
  struct

    (** Keep a worklist of statements to process. It is best to keep a queue,
     * because this way it is more likely that we are going to process all
     * predecessors of a statement before the statement itself. *)
    let worklist: Cil.stmt Queue.t = Queue.create ()

    (** We call this function when we have encountered a statement, with some
     * state. *)
    let reachedStatement (s: stmt) (d: T.t) : unit =
      let loc = get_stmtLoc s.skind in
      if loc != locUnknown then
        currentLoc := get_stmtLoc s.skind;
      (* see if we know about it already *)
      E.pushContext (fun _ -> dprintf "Reached statement %d with %a"
          s.sid T.pretty d);
      let newdata: T.t option =
        try
          let old = IH.find T.stmtStartData s.sid in
          match T.combinePredecessors s ~old:old d with
            None -> (* We are done here *)
              if !T.debug then
                ignore (E.log "FF(%s): reached stmt %d with %a\n  implies the old state %a\n"
                          T.name s.sid T.pretty d T.pretty old);
              None
          | Some d' -> begin
              (* We have changed the data *)
              if !T.debug then
                ignore (E.log "FF(%s): weaken data for block %d: %a\n"
                          T.name s.sid T.pretty d');
              Some d'
          end
        with Not_found -> (* was bottom before *)
          let d' = T.computeFirstPredecessor s d in
          if !T.debug then
            ignore (E.log "FF(%s): set data for block %d: %a\n"
                      T.name s.sid T.pretty d');
          Some d'
      in
      E.popContext ();
      match newdata with
        None -> ()
      | Some d' ->
          IH.replace T.stmtStartData s.sid d';
          if T.filterStmt s &&
            not (Queue.fold (fun exists s' -> exists || s'.sid = s.sid)
                            false
                            worklist) then
            Queue.add s worklist


    (** Get the two successors of an If statement *)
    let ifSuccs (s:stmt) : stmt * stmt =
      let fstStmt blk = match blk.bstmts with
          [] -> Cil.dummyStmt
        | fst::_ -> fst
      in
      match s.skind with
        If(e, b1, b2, _) ->
          let thenSucc = fstStmt b1 in
          let elseSucc = fstStmt b2 in
          let oneFallthrough () =
            let fallthrough =
              List.filter
                (fun s' -> thenSucc != s' && elseSucc != s')
                s.succs
            in
            match fallthrough with
              [] -> E.s (bug "Bad CFG: missing fallthrough for If.")
            | [s'] -> s'
            | _ ->  E.s (bug "Bad CFG: multiple fallthrough for If.")
          in
          (* If thenSucc or elseSucc is Cil.dummyStmt, it's an empty block.
             So the successor is the statement after the if *)
          let stmtOrFallthrough s' =
            if s' == Cil.dummyStmt then
              oneFallthrough ()
            else
              s'
          in
          (stmtOrFallthrough thenSucc,
           stmtOrFallthrough elseSucc)

      | _-> E.s (bug "ifSuccs on a non-If Statement.")

    (** Process a statement *)
    let processStmt (s: stmt) : unit =
      currentLoc := get_stmtLoc s.skind;
      if !T.debug then
        ignore (E.log "FF(%s).stmt %d at %t\n" T.name s.sid d_thisloc);

      (* It must be the case that the block has some data *)
      let init: T.t =
         try T.copy (IH.find T.stmtStartData s.sid)
         with Not_found ->
            E.s (E.bug "FF(%s): processing block without data" T.name)
      in

      (* See what the custom says *)
      match T.doStmt s init with
        SDone  -> ()
      | (SDefault | SUse _) as act -> begin
          let curr = match act with
              SDefault -> init
            | SUse d -> d
            | SDone -> E.s (bug "SDone")
          in
          (* Do the instructions in order *)
          let handleInstruction (s: T.t) (i: instr) : T.t =
            currentLoc := get_instrLoc i;

            (* Now handle the instruction itself *)
            let s' =
              let action = T.doInstr i s in
              match action with
               | Done s' -> s'
               | Default -> s (* do nothing *)
               | Post f -> f s
            in
            s'
          in

          let after: T.t =
            match s.skind with
              Instr il ->
                (* Handle instructions starting with the first one *)
                List.fold_left handleInstruction curr il

            | Goto _ | ComputedGoto _ | Break _ | Continue _ | If _
            | TryExcept _ | TryFinally _
            | Switch _ | Loop _ | Return _ | Block _ -> curr
          in
          currentLoc := get_stmtLoc s.skind;

          (* Handle If guards *)
          let succsToReach = match s.skind with
              If (e, _, _, _) -> begin
                let not_e = UnOp(LNot, e, intType) in
                let thenGuard = T.doGuard e after in
                let elseGuard = T.doGuard not_e after in
                if thenGuard = GDefault && elseGuard = GDefault then
                  (* this is the common case *)
                  s.succs
                else begin
                  let doBranch succ guard =
                    match guard with
                      GDefault -> reachedStatement succ after
                    | GUse d ->  reachedStatement succ d
                    | GUnreachable ->
                        if !T.debug then
                          ignore (E.log "FF(%s): Not exploring branch to %d\n"
                                    T.name succ.sid);

                        ()
                  in
                  let thenSucc, elseSucc = ifSuccs s  in
                  doBranch thenSucc thenGuard;
                  doBranch elseSucc elseGuard;
                  []
                end
              end
            | _ -> s.succs
          in
          (* Reach the successors *)
          List.iter (fun s' -> reachedStatement s' after) succsToReach;

      end




          (** Compute the data flow. Must have the CFG initialized *)
    let compute (sources: stmt list) =
      Queue.clear worklist;
      List.iter (fun s -> Queue.add s worklist) sources;

      (* All initial stmts must have non-bottom data *)
      List.iter (fun s ->
         if not (IH.mem T.stmtStartData s.sid) then
           E.s (E.error "FF(%s): initial stmt %d does not have data"
                  T.name s.sid))
         sources;
      if !T.debug then
        ignore (E.log "\nFF(%s): processing\n"
                  T.name);
      let rec fixedpoint () =
        if !T.debug && not (Queue.is_empty worklist) then
          ignore (E.log "FF(%s): worklist= %a\n"
                    T.name
                    (docList (fun s -> num s.sid))
                    (List.rev
                       (Queue.fold (fun acc s -> s :: acc) [] worklist)));
        let keepgoing =
          try
            let s = Queue.take worklist in
            processStmt s;
            true
          with Queue.Empty ->
            if !T.debug then
              ignore (E.log "FF(%s): done\n\n" T.name);
            false
        in
        if keepgoing then
          fixedpoint ()
      in
      fixedpoint ()

  end



(******************************************************************
 **********
 **********         BACKWARDS
 **********
 ********************************************************************)
module type BackwardsTransfer = sig
  val name: string (* For debugging purposes, the name of the analysis *)

  val debug: bool ref (** Whether to turn on debugging *)

  type t  (** The type of the data we compute for each block start. In many
           * presentations of backwards data flow analysis we maintain the
           * data at the block end. This is not easy to do with JVML because
           * a block has many exceptional ends. So we maintain the data for
           * the statement start. *)

  val pretty: unit -> t -> Pretty.doc (** Pretty-print the state *)

  val stmtStartData: t Inthash.t
  (** For each block id, the data at the start. This data structure must be
   * initialized with the initial data for each block *)

  val funcExitData: t
  (** The data at function exit.  Used for statements with no successors.
      This is usually bottom, since we'll also use doStmt on Return
      statements. *)

  val combineStmtStartData: Cil.stmt -> old:t -> t -> t option
  (** When the analysis reaches the start of a block, combine the old data
   * with the one we have just computed. Return None if the combination is
   * the same as the old data, otherwise return the combination. In the
   * latter case, the predecessors of the statement are put on the working
   * list. *)


  val combineSuccessors: t -> t -> t
  (** Take the data from two successors and combine it *)


  val doStmt: Cil.stmt -> t action
  (** The (backwards) transfer function for a branch. The {!Cil.currentLoc} is
   * set before calling this. If it returns None, then we have some default
   * handling. Otherwise, the returned data is the data before the branch
   * (not considering the exception handlers) *)

  val doInstr: Cil.instr -> t -> t action
  (** The (backwards) transfer function for an instruction. The
   * {!Cil.currentLoc} is set before calling this. If it returns None, then we
   * have some default handling. Otherwise, the returned data is the data
   * before the branch (not considering the exception handlers) *)

  val filterStmt: Cil.stmt -> Cil.stmt -> bool
  (** Whether to put this predecessor block in the worklist. We give the
   * predecessor and the block whose predecessor we are (and whose data has
   * changed)  *)

end

module BackwardsDataFlow =
  functor (T : BackwardsTransfer) ->
  struct

    let getStmtStartData (s: stmt) : T.t =
      try IH.find T.stmtStartData s.sid
      with Not_found ->
        E.s (E.bug "BF(%s): stmtStartData is not initialized for %d: %a"
               T.name s.sid d_stmt s)

    (** Process a statement and return true if the set of live return
     * addresses on its entry has changed. *)
    let processStmt (s: stmt) : bool =
      if !T.debug then
        ignore (E.log "FF(%s).stmt %d\n" T.name s.sid);


      (* Find the state before the branch *)
      currentLoc := get_stmtLoc s.skind;
      let d: T.t =
        match T.doStmt s with
           Done d -> d
         | (Default | Post _) as action -> begin
             (* Do the default one. Combine the successors *)
             let res =
               match s.succs with
                 [] -> T.funcExitData
               | fst :: rest ->
                   List.fold_left (fun acc succ ->
                     T.combineSuccessors acc (getStmtStartData succ))
                     (getStmtStartData fst)
                     rest
             in
             (* Now do the instructions *)
             let res' =
               match s.skind with
                 Instr il ->
                   (* Now scan the instructions in reverse order. This may
                    * Stack_overflow on very long blocks ! *)
                   let handleInstruction (i: instr) (s: T.t) : T.t =
                     currentLoc := get_instrLoc i;
                     (* First handle the instruction itself *)
                     let action = T.doInstr i s in
                     match action with
                     | Done s' -> s'
                     | Default -> s (* do nothing *)
                     | Post f -> f s
                   in
                   (* Handle instructions starting with the last one *)
                   List.fold_right handleInstruction il res

               | _ -> res
             in
             match action with
               Post f -> f res'
             | _ -> res'
         end
      in

      (* See if the state has changed. The only changes are that it may grow.*)
      let s0 = getStmtStartData s in

      match T.combineStmtStartData s ~old:s0 d with
        None -> (* The old data is good enough *)
          false

      | Some d' ->
          (* We have changed the data *)
          if !T.debug then
            ignore (E.log "BF(%s): set data for block %d: %a\n"
                      T.name s.sid T.pretty d');
          IH.replace T.stmtStartData s.sid d';
          true


          (** Compute the data flow. Must have the CFG initialized *)
    let compute (sinks: stmt list) =
      let worklist: Cil.stmt Queue.t = Queue.create () in
      List.iter (fun s -> Queue.add s worklist) sinks;
      if !T.debug && not (Queue.is_empty worklist) then
        ignore (E.log "\nBF(%s): processing\n"
                  T.name);
      let rec fixedpoint () =
        if !T.debug &&  not (Queue.is_empty worklist) then
          ignore (E.log "BF(%s): worklist= %a\n"
                    T.name
                    (docList (fun s -> num s.sid))
                    (List.rev
                       (Queue.fold (fun acc s -> s :: acc) [] worklist)));
        let keepgoing =
          try
            let s = Queue.take worklist in
            let changes = processStmt s in
            if changes then begin
              (* We must add all predecessors of block b, only if not already
               * in and if the filter accepts them. *)
              List.iter
                (fun p ->
                   if not (Queue.fold (fun exists s' -> exists || p.sid = s'.sid)
                             false worklist) &&
                     T.filterStmt p s then
                       Queue.add p worklist)
                s.preds;
            end;
            true

          with Queue.Empty ->
            if !T.debug then
              ignore (E.log "BF(%s): done\n\n" T.name);
            false
        in
        if keepgoing then
          fixedpoint ();
      in
      fixedpoint ();

  end


(** Helper utility that finds all of the statements of a function.
  It also lists the return statments (including statements that
  fall through the end of a void function).  Useful when you need an
  initial set of statements for BackwardsDataFlow.compute. *)
let sink_stmts = ref []
let all_stmts = ref []
let sinkFinder = object(self)
  inherit nopCilVisitor

  method! vstmt s =
    all_stmts := s ::(!all_stmts);
    match s.succs with
      [] -> (sink_stmts := s :: (!sink_stmts);
	     DoChildren)
    | _ -> DoChildren

end

(* returns (all_stmts, return_stmts).   *)
let find_stmts (fdec:fundec) : (stmt list * stmt list) =
  ignore(visitCilFunction (sinkFinder) fdec);
  let all = !all_stmts in
  let ret = !sink_stmts in
  all_stmts := [];
  sink_stmts := [];
  all, ret