Avoiding type inference false-positives with flow-sensitive conditional analysis
psalm.dev
psalm.dev
This seems like an odd claim to make (OP also repeats it elsewhere in the text and seems to be aware of a single exception). The analysis described in the blog post is not novel or unique. It is useful but I don't really know what to make of this claim. Abstract interpretation, symbolic execution, and even typechecking systems have all used this kind of approach for many decades. There are hundreds of papers and tools using this approach.
Usually, you'd call this "path sensitive analysis".
I love seeing static analysis show up outside of academic papers, but there is a wealth of material for people to immerse themselves in if they want to learn!
This is a false-positive:
https://www.typescriptlang.org/play?#code/GYVwdgxgLglg9mABMO...
> since it also allows for user-defined assertions and guards
Psalm allows user-defined type guards:
You might be aware already, but the examples aren't the same (I know it illustrated the same idea tho) as on the Psalm post. It might make sense to align them with the PHP example so people don't get tripped up on that (esp if they're not too familiar with TS and PHP quirks)! Additionally `!a` and `a !== null` (or `!=`) aren't the same in JS/TS, so maybe change those in your example too, just to get your point across better.
BTW, Psalm seems really cool! I've not used PHP in a long time, but I always felt it lacks tooling, so it's great to see people are making progress in that area. Keep up the good work!
Yeah, because both TS and PHP have the same treatment of `!expr` I use the two interchangeably when demonstrating functionality, but the exactly comparable example is here:
https://www.typescriptlang.org/play?#code/GYVwdgxgLglg9mABMO...
> BTW, Psalm seems really cool! I've not used PHP in a long time, but I always felt it lacks tooling, so it's great to see people are making progress in that area.
Yeah, it's not the only open-source static analysis tool for PHP – there's also https://phpstan.org, which is even more popular
I've also discussed the article with the authors of the linked paper, who didn't suggest anything else in the way of prior art.
The technique is broader than type inference / type checking. Like, if you just type "symbolic execution" into google scholar you'll find piles of systems that do this sort of collection of branch predicates and narrowing. Notably, you seem to be doing this on values in addition to types (since you care about which value a string matches), which makes this more closely related to something like symbolic execution than classic type inference.
If you want something in the typing space, there are oodles of tools that use the theory of dependent types to achieve things like this.
If you want something in the abstract interpretation space, numerical analysis does this sort of path-sensitive narrowing for bounds all the time. A scholar search for "abstract interpretation numerical domain" will turn up mountains of papers.
Specifically I don't know of another widely-used static analysis tool for Python, Ruby, PHP, Perl, JS or TypeScript that performs this analysis.
I also haven't come across a paper that describes the application of this technique to those languages, which is why I wrote this post – I want others to see its use, and adopt it too.
Prototyping Symbolic Execution Engines for Interpreted Languages. Bucer, Kinder, Candea - symexec of python
ExpoSE: practical symbolic execution of standalone JavaScript. Loring, Mitchell, Kinder - symexec of javascript
Path Sensitive Static Analysis of Web Applications for Remote Code Execution Vulnerability Detection, Zheng, Zhang - path sensitive analysis for strings, doing the same sort of value narrowing based on branches for JS.
JSAI: A Static Analysis Platform for JavaScript, Kashyap et al. - static analysis of JS support path sensitive analysis.
AppReduce, by Google, does condition-based type narrowing for nullability inference on davik bytecode (an untyped interpreted language).
I also believe that WALA (which supports JS) supports path-based narrowing.
Other than the AppReduce case, these aren't literally the same thing (type narrowing for inferring types in an untyped interpreted language) but they all play in this same space of "collect path conditions to some instruction, convert them into predicates, run some solving on those predicates, and draw a conclusion about the semantics of the program along that path" that you are playing in.
The Zheng & Zhang paper is particularly interesting, given it tackles taint analysis and succeeds where Psalm (which also has a taint analysis mode) fails: https://psalm.dev/r/7098c7bb59. Might try to implement a cut-down version of their method.
This blog post gives a nice and easily-understood explanation of the concept, which is more than can be said for the way that much of the literature on type theory and static analysis is written. HN isn't an academic journal or PhD defense; ideas described don't have to be new to be useful.
And making ideas more widely known is valuable; even the just-released Java 16 missed out on this exact feature in its "pattern matching" (really type narrowing) support, requiring the programmer to declare an additional variable rather than using information just established about an existing one: https://openjdk.java.net/jeps/394
My hope is that OP finds kinship in the community, not to discourage them.
That last sentence was meant as an exhortation to authors of similar static analysis tools: "Please implement this so I don't feel it’s a spurious addition". Many of those authors are like me – engineers who lack a post-grad education in program analysis, but are still interested in the subject. I hope some of them did read it, and can bring the same analysis to their own tools.
I was also really happy when I discovered Typed Racket had implemented it, mostly because it meant that the idea wasn't flawed for some theoretical reason I’m too ill-educated to understand...
Also, not surprised Racket already has occurrence typing. It’s got basically everything else.