Static check for zero_alloc: ignore allocation that lead to exceptional return

[gretay-js]

A new version of #864 + #863 + #870.

Best reviewed commit by commit.

I can try to split them into separate PRs, but it is quite tricky to get the separate PRs to build and pass the tests on their own.

• The main change: abstract domain is a triple { nor; exn; div; } where each of the components represents different paths through the function: paths to normal return, paths to exception return, and diverging paths that never retrun, resp. Each component can have one of the following values: Bot for unreachable (empty set of paths), Safe for "guaranteed to not allocate on any of the relevant paths", and Top for arbitray allocation on the relevant paths.
  The "strict" check requires no allocation on any path. The "relaxed" check, which is the defaul, allows allocation on paths that lead to exceptional return from the function (i.e., exn can be Top in the summary of the function), but not on normal return or infinite loops. Allocatins on paths that end in a call to an external function that never returns, such as exit, are not ignored in "relaxed" mode (it was simpler to implement).

• Checkmach uses backend/dataflow.ml which is essentially a copy of the upstream backwards dataflow analysis. The div component is computed as a postprocessing step using another run of the same dataflow analysis, after the other components are computed. To make this postprocessing faster and simpler to implement, there is a small change to the interface of Dataflow to expose the mapping of labels to abstract value.

• Attrbutes are now named [@zero_alloc] and [@zero_alloc strict] with the corresponding [@zero_alloc assume] and [@zero_alloc strict assume]. The internal representation of these attributes has been reworked to make it easier to parse them and extend the static checker with other properties in the future. This involves changes throughout the compilation pipeline to propagate the new representation of these attributes all the way to the backend. Currently, this is in 3 separate separate commits. I can split this out as a separate PR, but it would mean fixing the existing checkmach.ml, which is substantially modified in the following steps.

• Better user-error messages: locations when check fails point to the attribute instead of the entire body of the function. Location.t is passed all the way to the backend.

• Refactor cmx format representation of the results of the static checker: move Checks module out of Cmx_format into a separate module. Decomple the representation of function summaries used in Compilenv from the "raw" version saved to cmx. Change the "raw" representation from maps to lists. Should it use arrays? It is now easy to change.

• Flambda2: results may be unsound in the presence of Delayed Try-with that cannot be represented as a Regular Try-with. I can make the analysis conservatively sound, but it causes the CI tests to fail, and there is no easy way to distinguish flambda2 in dune tests. Also I am not sure if the current optimizatons in flambda2 generate the cases. We need to fix backend/dataflow.ml to support them and maybe update backend/liveness.ml to use this dataflow as well. Separate PRs.

• There are several ways in which the current analysis can be optimized to use less memory and finish early when a function is established to be allocating. I am leaving them for later as it makes it harder to reason about soundness.

[xclerc]

I am not sure I understand the semantics of
the non-strict variant. My understanding is
that it would accept allocations on paths
leading to an exception, but the following is
being rejected:

exception E of string
let[@zero_alloc] fail () = raise (E "msg")

[gretay-js]

This example is accepted when we pass -g compiler flag. Without this flag, raise is treated as raise_notrace, which has a special case in the analysis. If we don't treat raise_notrace specially, we will end up accepting the following example:

exception Found

let[@zero_alloc strict] find a =
  let i = 0 in
  while true do
    if a.(i) then
      raise_notrace Found;
  done

let[@zero_alloc] foo n =
  let a = Array.make n true in
  find a

The dependency on a seemingly unrelated compiler flag is quite annoying for testing, but allocations depend on compiler configuration and optimization flags.

[xclerc]

Noted; here is another example I don't think I understand
(failing while I am expecting it to pass):

let[@inline never] forever () = while true do () done
let[@zero_alloc strict] f g x =
  try
    while true do
      forever ()
    done;
    x
  with _ ->
    g x;
    x

It works if never is changed to always. Isn't the div
component expected to provide support for such cases?

[xclerc]

I am not sure whether it is related to the previous
comment or is more linked to how callees and
callers work, but the following is accepted:

let[@zero_alloc] rec forever () = while true do () done
and[@zero_alloc] order () =
  forever ();
  alloc (2, 3)

while the following is rejected:

let[@zero_alloc] rec order () =
  forever ();
  alloc (2, 3)
and[@zero_alloc] forever () = while true do () done

[xclerc]

Back to #1157 (comment), it seems to fail if
raise ... is replaced with failwith "..."
even though stdlib is apparently built with
-g.

[lthls]

I can write the code for correctly handling delayed try-with in dataflow.ml if you want, it shouldn't take me too long.

Regarding this PR, the problem is quite tricky and I think this PR comes short in a few places.
First, the handling of future functions is not perfect. The ideal solution would be a fixpoint computation, but that may end up too expensive. The current solution should be correct but could give false positives.
One example where it could matter:

exception E
let rec f x b =
  if b then (g x; raise E)
  else ()
and g y = ignore (y, y) (* Allocating *)

With a fixpoint computation, we should be able to infer that f only allocates on exceptional paths, but since we haven't seen g yet we can only record a dependency. When g gets treated later we find that it allocates, and propagate the property to its caller f, without the information that it's only on exceptional paths.

More problematic, the handling of exception paths looks weird. I think this is because the allocation check is naturally expressed as a forward dataflow analysis, but you're trying to use the backwards one. It should be possible to make it work anyway, but it doesn't look obvious when looking at your code that it is correct (the fine details around the handling of raise look like a red flag).
I would suggest to rewrite your analysis either without using Dataflow, or with a new Dataflow.Forward functor (I can write this one if you need it).

Divergence can be handled relatively easily in both forward and backward analyses. For the backwards one, I think it can be done by specifying a ?(diverging = D.bot) parameter to analyze and use that in get_lbl instead of D.bot for the Not_found case. In your case, since you want to handle diverging paths in the same way as normal paths, I think you could use Value.normal_return as the diverging value (and get rid of the div field of your record).

[xclerc]

The following is really a corner case, and quite
possibly not one we want to support:

exception E
type t = { x : int; mutable y : int }
let[@zero_alloc] f {x; y} () = Printf.eprintf "%d\n%!" (y); raise E

It fails because the zero_alloc annotation is
left on a function which end up simply calling
the helper, which is the one unconditionally
raising.

[xclerc]

(Actually, proper support for "forward" references
will quite probably be enough to support this case.)

[gretay-js]

(Actually, proper support for "forward" references will quite probably be enough to support this case.)

I don't think so, there is no call to the helper function. It's a bug - the annotation should not be on the helper function.
It feels similar to #1273 in the sense that the optimizer inlines/lifts some functions.

[xclerc]

Oh, indeed I misread the output of -dsel: there
is a reference to the helper function, but not a
call to it.

[xclerc]

(And to be clear, as far as I can see the annotation
stays on the original function, which happens to be
essentially a stub eventually.)

[gretay-js]

(And to be clear, as far as I can see the annotation stays on the original function, which happens to be essentially a stub eventually.)

Ah, yes, you are right about it! so, it's not a bug, good.

[lthls]

The following is really a corner case, and quite possibly not one we want to support:

exception E
type t = { x : int; mutable y : int }
let[@zero_alloc] f {x; y} () = Printf.eprintf "%d\n%!" (y); raise E

It fails because the zero_alloc annotation is left on a function which end up simply calling the helper, which is the one unconditionally raising.

I think this is one of those cases where mutable patterns cause functions to have different arities than expected. In this case, we end up with let[@zero_alloc] f {x; y} = (fun () -> Printf.eprintf "%d\n%!" (y); raise E), which is allocating as it returns a closure containing one of its arguments.
You can have a look at ocaml/RFCs#32, which describes a small change to the language that would solve this problem (or you could talk with @stedolan directly, he might like having another concrete example where his proposal would fix bugs).

[xclerc]

Two usability quibbles, for a follow-up PR:

• it would be nice to give to the user the
  location of a violation, rather than only
  the fail/pass status;
• possibly also keep the name of the
  function as it appears in the source for
  the error messages.

[gretay-js]

Two usability quibbles, for a follow-up PR:

@xclerc ah these are tricky, but I'll look into it.

it would be nice to give to the user the location of a violation, rather than only the fail/pass status;

it's not clear to me how to do it in a low-overhead way for the relaxed propery, because some of the encountered allocation sites would later be discarded. I think the best way to do it would be editor ui integrtion for inspecting the intermediate represetnation of this analysis alongside the source.

possibly also keep the name of the function as it appears in the source for the error messages.

looks like this information is no longer available at lambda, even when the function is not anonymous.

[xclerc]

I was thinking maybe the debuginfo,
when present, could be used but it
may not be reliable enough.

For the name, that would indeed
involve some bookkeeping, unless
we can leverage the scopes from
the debuginfo.

Anyway, what would go into a
follow-up PR.

[gretay-js]

@lthls do you have any other comments about this version? (A follow up PR will do the outer fixpoint on function summaries, lifted from Value.t to essentially Env.t->Value.t.)

[lthls]

I don't have anything new to add, for me this PR can go forward.