> Lastly there's a cost to maintaining a system that doesn’t appear to exist outside of Psalm.
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!
Funny that the author mentions TypeScript, then complains that maintaining a system like this that "doesn't exist elsewhere" would be hard. TypeScript, in fact, does an analysis almost exactly like what is described in the article. Possibly even more expansive, since it also allows for user-defined assertions and guards, in addition to simple syntactic narrowing.
You're correct that this generates a false-positive! This is a really interesting feature. Would love to see more static analysers/compilers implement this.
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!
> You might be aware already, but the examples aren't the same
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:
> 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
Author here: I'm not aware this analysis in typechecking systems outside of Typed Racket and Psalm – if you point me to them I'll happily update the article!
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.
I'm very sure that I'm not the first person to have stumbled across this idea, and I'm sure that lots of much smarter people have written at length about the theory, but I'm not aware of that theory having been applied to the analysis of interpreted languages, except with Typed Racket.
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.
I get your point, but I think you're being a bit harsh on OP. Yes the material is covered in the literature, but for people who aren't already familiar with it, it can take an enormous amount of time and effort to both find and understand the right papers (I know because I've been doing exactly that for the past few months for a language I'm designing).
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
I think it is a useful tool. I also think that getting meaningful results on a 6% performance hit is impressive. IMO, the blog post would be a great little piece with two or three sentences removed.
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...
I think this might fall over pretty quickly in the presence of first-class functions. In that case, you can’t determine the control graph statically. You’ll need Control-Flow Analysis for that.
Also, not surprised Racket already has occurrence typing. It’s got basically everything else.
19 comments
[ 2.7 ms ] story [ 52.8 ms ] threadThis 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:
https://psalm.dev/docs/annotating_code/adding_assertions/
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.