Join points at return?

[lambdageek]

Consider

void foo () {
  f1 ();
  if (cond) {
    f2 ();
    return;
  }
  f3 ();
}

I haven't looked too closely, but does CallTree represent the join point between the return after f2 and the fallthrough after f3()? Does it need to? (the usual representation for functions is a graph - not tree - of single-entry-single-exit basic blocks)

[evincarofautumn]

It doesn’t currently, and it doesn’t need to, but that would be a good enhancement.

Basically, we don’t have a lot of code using functions that affect permissions around control flow, and where we do, Ward already complains about it and it’s easy to refactor. Stuff like:

void foo ()
{
  lock ();
  if (bar ()) {
    unlock ();
    return 0;
  }
  baz ();
  unlock ();
  return 1;
}

[lambdageek]

hmm. i'm not entirely convinced we'll always have conflicts if we just treat return as a fallthru. or perhaps we will but they might be difficult to understand. but it does look like the right thing would happen for things like lock/unlock, so i'm content to revisit this in the future.

[evincarofautumn]

An easy hack would be to convert the graph to a tree by duplicating segments, maybe with sharing so there’s no actual copying:

if (a ()) goto skip;
b ();
skip: c ();

(a → { b, c }, b → c) ⇒ (a & (c₁ | b & c₂))

  a          a
 / \        / \
b   |  =>  b   |
 \ /       |   |
  c        c   c

But of course this doesn’t work with back-edges.

[evincarofautumn]

It occurs to me that we could also decompose call trees into one “function” for each basic block. So the example you gave could be:

foo = foo1
foo1 = f1 & (foo2 | foo3)
foo2 = f2 & foo4
foo3 = f3 & foo4
foo4 = 0

(Then during inference, some basic optimisations like TCO would show up: when we’re inferring a node in tail position, we wouldn’t need to add another stack frame.)

[lambdageek]

Yea I think I basically agree with this. One property that we should have is that we enjoy an abstraction property: it should be sound to abstract out any CallTree into a separate toplevel function and have an inference result that is no less precise than before. (I think in general abstraction may lose precision - not sure if that can happen in ward).

I'm not sure what you mean about TCO or stack frames