It just adds the ability to query Funcs for their definition location. Adding it to error messages or profiling results is more annoying, because you need to account for environments where it will just be an empty string because I never figured out how to parse the debug metadata (Windows, Google)
It may be that llvm has better support for parsing DWARF and PDB that it did when I wrote the dwarf parser
I’ve narrowed it down to a case where the only difference in assembly output between good and bad appears to be the choice of xmm registers selected by LLVM in one section… literally identical instruction selection though. Which seems to be ~impossible to be the culprit, so I think I’ve gone astray in my debugging. Will let you know. (If I can narrow it down to a publicly-shareable chunk of code, will put it out there for inspection.)
C-like language that uses bounds proving to guarantee no out of bounds buffer accesses
Nigel Tao is the main person behind it.
Halide's bounds support has been mentioned in the context of this.
(Given the language is intended for secure file format support, I'm a bit disappointed that it doesn't have more domain specificity. The thinking on that appears to be that the bugs in file formats are always in the things that are weirdly irregular and pretty much require arbitrary code and can't be expressed with a more conventional grammar. I'm not sure I agree, but I haven't spent a lot of time on this.)