3 ms·

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

by muglug 6y ago

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 6y ago
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 6y ago
  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 6y ago
    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 6y ago
      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 https://psalm.dev/r/7098c7bb59. Might try to implement a cut-down version of their method.

by muglug 6y ago

UncleMeat 6y ago

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 6y ago
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 6y ago
  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 6y ago
    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 https://psalm.dev/r/7098c7bb59. Might try to implement a cut-down version of their method.