add "skip global checks" attribute for AOs

[bakkot]

which disables analyses which require knowing every callsite - currently just the "every callsite invokes with !" check, but we'd also use this for a future "every callsite passes this optional argument" check and similar.

[michaelficarra]

This looks okay, though I would've phrased it as something like "public interface". We don't always know who calls it or how many call sites there are, but we do know that we want it to be part of the document's integration surface. That's the thing we're trying to communicate.

[bakkot]

I kind of wanted to go the other way, and make it a very technical "exempt from whole-program analysis", because that's what it's actually going to get used for - we're not going to go annotate all the things which are actually the de-facto public interface in the near future.

[michaelficarra]

we're not going to go annotate all the things which are actually the de-facto public interface in the near future

I want to do exactly that.

[bakkot]

Fair enough.

The other factor is, I'd like to extend this so that we can have a useful "this AO is never called, you should remove it" check, which I started doing here. But it turns out there's a bunch of stuff which is called but not in a way we can determine, like ToInt16, whose sole call site is this table. So I want to exempt ToInt16 from whole-program analysis. But that doesn't mean it needs to be part of the public interface.

Maybe I'll change this to "exempt from whole program analysis" for now, and we can add a "public interface" one later which implies it.

[michaelficarra]

@bakkot Instead of exempting the AO, we should probably just find a way to annotate the dynamic call site with the AOs that could be reached.

[bakkot]

Well, some of the checks I'd like to do are along the lines of "does every use assert !", and there's no easy way to do that sort of analysis for the dynamic callsites. That sounds like a whole bunch more work which I don't want to do.

There's not enough dynamic callsites that it makes sense to put in a bunch of work just for those cases, rather than simply skipping analysis for them.

[bakkot]

Renamed to "skip global checks"; gonna land as-is. We can add the "public interface" one separately and have it imply this.