forked from ocaml/ocaml
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add a generic backward dataflow analyzer and use it for liveness anal…
…ysis (ocaml#10404) The analyzer is parameterized by an abstract domain and a transfer function. For recursive handlers, it remembers the latest inferred abstract state and uses it to start the next fixpoint iteration. This avoids behaviors exponential in the nesting of recursive handlers, like we would have if we started every iteration with bottom. This exponential behavior was present in the old implementation of liveness analysis. It is gone in the new implementation that just calls into the generic analyzer.
- Loading branch information
1 parent
9915ccb
commit 1dc931e
Showing
7 changed files
with
222 additions
and
103 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,86 @@ | ||
| (**************************************************************************) | ||
| (* *) | ||
| (* OCaml *) | ||
| (* *) | ||
| (* Xavier Leroy, projet Cambium, INRIA Paris *) | ||
| (* *) | ||
| (* Copyright 2021 Institut National de Recherche en Informatique et *) | ||
| (* en Automatique. *) | ||
| (* *) | ||
| (* All rights reserved. This file is distributed under the terms of *) | ||
| (* the GNU Lesser General Public License version 2.1, with the *) | ||
| (* special exception on linking described in the file LICENSE. *) | ||
| (* *) | ||
| (**************************************************************************) | ||
|
|
||
| open Mach | ||
|
|
||
| module type DOMAIN = sig | ||
| type t | ||
| val bot: t | ||
| val join: t -> t -> t | ||
| val lessequal: t -> t -> bool | ||
| end | ||
|
|
||
| module Backward(D: DOMAIN) = struct | ||
|
|
||
| let analyze ?(exnhandler = fun x -> x) ~transfer instr = | ||
| let lbls = | ||
| (Hashtbl.create 20 : (int, D.t) Hashtbl.t) in | ||
| let get_lbl n = | ||
| match Hashtbl.find_opt lbls n with None -> D.bot | Some b -> b | ||
| and set_lbl n x = | ||
| Hashtbl.replace lbls n x in | ||
|
|
||
| let rec before end_ exn i = | ||
| match i.desc with | ||
| | Iend -> | ||
| transfer i ~next:end_ ~exn | ||
| | Ireturn | Iop (Itailcall_ind | Itailcall_imm _) -> | ||
| transfer i ~next:D.bot ~exn:D.bot | ||
| | Iop _ -> | ||
| let bx = before end_ exn i.next in | ||
| transfer i ~next:bx ~exn | ||
| | Iifthenelse(_, ifso, ifnot) -> | ||
| let bx = before end_ exn i.next in | ||
| let b1 = before bx exn ifso | ||
| and b0 = before bx exn ifnot in | ||
| transfer i ~next:(D.join b1 b0) ~exn | ||
| | Iswitch(_, cases) -> | ||
| let bx = before end_ exn i.next in | ||
| let b1 = | ||
| Array.fold_left | ||
| (fun accu case -> D.join accu (before bx exn case)) | ||
| D.bot cases in | ||
| transfer i ~next:b1 ~exn | ||
| | Icatch(rc, handlers, body) -> | ||
| let bx = before end_ exn i.next in | ||
| begin match rc with | ||
| | Cmm.Nonrecursive -> | ||
| List.iter | ||
| (fun (n, h) -> set_lbl n (before bx exn h)) | ||
| handlers | ||
| | Cmm.Recursive -> | ||
| let update changed (n, h) = | ||
| let b0 = get_lbl n in | ||
| let b1 = before bx exn h in | ||
| if D.lessequal b1 b0 then changed else (set_lbl n b1; true) in | ||
| while List.fold_left update false handlers do () done | ||
| end; | ||
| let b = before bx exn body in | ||
| transfer i ~next:b ~exn | ||
| | Iexit n -> | ||
| transfer i ~next:(get_lbl n) ~exn | ||
| | Itrywith(body, handler) -> | ||
| let bx = before end_ exn i.next in | ||
| let bh = exnhandler (before bx exn handler) in | ||
| let bb = before bx bh body in | ||
| transfer i ~next:bb ~exn | ||
| | Iraise _ -> | ||
| transfer i ~next:D.bot ~exn | ||
| in | ||
| let b = before D.bot D.bot instr in | ||
| (b, get_lbl) | ||
|
|
||
| end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,85 @@ | ||
| (**************************************************************************) | ||
| (* *) | ||
| (* OCaml *) | ||
| (* *) | ||
| (* Xavier Leroy, projet Cambium, INRIA Paris *) | ||
| (* *) | ||
| (* Copyright 2021 Institut National de Recherche en Informatique et *) | ||
| (* en Automatique. *) | ||
| (* *) | ||
| (* All rights reserved. This file is distributed under the terms of *) | ||
| (* the GNU Lesser General Public License version 2.1, with the *) | ||
| (* special exception on linking described in the file LICENSE. *) | ||
| (* *) | ||
| (**************************************************************************) | ||
|
|
||
| (* An abstract domain for dataflow analysis. Defines a type [t] | ||
| of abstractions, with lattice operations. *) | ||
|
|
||
| module type DOMAIN = sig | ||
| type t | ||
| val bot: t | ||
| val join: t -> t -> t | ||
| val lessequal: t -> t -> bool | ||
| end | ||
|
|
||
| (* Build a backward dataflow analysis engine for the given domain. *) | ||
|
|
||
| module Backward(D: DOMAIN) : sig | ||
|
|
||
| val analyze: ?exnhandler: (D.t -> D.t) -> | ||
| transfer: (Mach.instruction -> next: D.t -> exn: D.t -> D.t) -> | ||
| Mach.instruction -> | ||
| D.t * (int -> D.t) | ||
|
|
||
| (* [analyze ~exnhandler ~transfer instr] performs a backward dataflow | ||
| analysis on the Mach instruction [instr], typically a function body. | ||
| It returns a pair of | ||
| - the abstract state at the function entry point; | ||
| - a mapping from catch handler label to the abstract state at the | ||
| beginning of the handler with this label. | ||
| The [transfer] function is called as [transfer i ~next ~exn]. | ||
| - [i] is a sub-instruction of [instr]. | ||
| - [next] is the abstract state "after" the instruction for | ||
| normal control flow, falling through the successor(s) of [i]. | ||
| - [exn] is the abstract state "after" the instruction for | ||
| exceptional control flow, branching to the nearest exception handler | ||
| or exiting the function with an unhandled exception. | ||
| The [transfer] function, then, returns the abstract state "before" | ||
| the instruction. The dataflow analysis will, then, propagate this | ||
| state "before" as the state "after" the predecessor instructions. | ||
| For compound instructions like [Iifthenelse], the [next] abstract | ||
| value that is passed to [transfer] is not the abstract state at | ||
| the end of the compound instruction (e.g. after the "then" and "else" | ||
| branches have joined), but the join of the abstract states at | ||
| the beginning of the sub-instructions. More precisely: | ||
| - for [Iifthenelse(tst, ifso, ifnot)], it's the join of the | ||
| abstract states at the beginning of the [ifso] and [ifnot] | ||
| branches; | ||
| - for [Iswitch(tbl, cases)], it's the join of the abstract states | ||
| at the beginning of the [cases] branches; | ||
| - for [Icatch(recflag, body, handlers)] and [Itrywith(body, handler)], | ||
| it's the abstract state at the beginning of [body]. | ||
| The [transfer] function is called for every sub-instruction of [instr], | ||
| as many times as needed to reach a fixpoint. Hence, it can record | ||
| the results of the analysis at each sub-instruction in a mutable | ||
| data structure. For instance, the transfer function for liveness | ||
| analysis updates the [live] fields of instructions as a side | ||
| effect. | ||
| The optional [exnhandler] argument deals with exception handlers. | ||
| This is a function that transforms the abstract state at the | ||
| beginning of an exception handler into the exceptional abstract | ||
| state for the instructions within the body of the handler. | ||
| Typically, for liveness analysis, it takes the registers live at | ||
| the beginning of the handler and removes the register | ||
| [Proc.loc_exn_bucket] that carries the exception value. If not | ||
| specified, [exnhandler] defaults to the identity function. | ||
| *) | ||
|
|
||
| end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.