[HN Gopher] Avoiding type inference false-positives with flow-se...
___________________________________________________________________
Avoiding type inference false-positives with flow-sensitive
conditional analysis
Author : muglug
Score : 32 points
Date : 2021-03-15 23:32 UTC (23 hours ago)
(HTM) web link (psalm.dev)
(TXT) w3m dump (psalm.dev)
| savant_penguin wrote:
| Is there a reason not to disallow type inferences altogether?
| ashton314 wrote:
| 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.
| UncleMeat wrote:
| > 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!
| mshockwave wrote:
| second this, I believe there are tons of similar research of
| similar techniques
| peterkelly wrote:
| 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
| UncleMeat wrote:
| 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.
| muglug wrote:
| I'm always happy to receive knowledge!
|
| 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...
| wwwigham wrote:
| 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.
| muglug wrote:
| TypeScript doesn't perform this conditional analysis:
|
| 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/
| spoiler wrote:
| 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!
| muglug wrote:
| > 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:
|
| https://www.typescriptlang.org/play?#code/GYVwdgxgLglg9mA
| BMO...
|
| > 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
| muglug wrote:
| 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.
| UncleMeat wrote:
| I don't really know how to answer this.
|
| 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.
| muglug wrote:
| 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.
| UncleMeat wrote:
| A few examples of many.
|
| 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.
| muglug wrote:
| Thanks, that's a great collection.
|
| 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.
| ordu wrote:
| Doesn't Rust do the same, when I write `let a = match ... ;` and
| then rustc complains that return types of branches do not match?
| [deleted]
| ncmncm wrote:
| Psalm appears to be a static analyzer tool for PHP code.
___________________________________________________________________
(page generated 2021-03-16 23:03 UTC)