arXiv 1708.080212017-08-30cs.PL

Fast and Precise Type Checking for JavaScript

Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, Gabriel Levi

英文摘要：

In this paper we present the design and implementation of Flow, a fast and precise type checker for JavaScript that is used by thousands of developers on millions of lines of code at Facebook every day. Flow uses sophisticated type inference to understand common JavaScript idioms precisely. This helps it find non-trivial bugs in code and provide code intelligence to editors without requiring significant rewriting or annotations from the developer. We formalize an important fragment of Flow's analysis and prove its soundness. Furthermore, Flow uses aggressive parallelization and incrementalization to deliver near-instantaneous response times. This helps it avoid introducing any latency in the usual edit-refresh cycle of rapid JavaScript development. We describe the algorithms and systems infrastructure that we built to scale Flow's analysis.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Interprocedural Type Specialization of JavaScript Programs Without Type Analysis

Dynamically typed programming languages such as Python and JavaScript defer type checking to run time. VM implementations can improve performance by eliminating redundant dynamic type checks. However, type inference analyses are often costly and involve tradeoffs between compilation time and resulting precision. This has lead to the creation of increasingly complex multi-tiered VM architectures. Lazy basic block versioning is a simple JIT compilation technique which effectively removes redundant type checks from critical code paths. This novel approach lazily generates type-specialized version…

2015-11-10cs.PL

Dependent Types for JavaScript

We present Dependent JavaScript (DJS), a statically-typed dialect of the imperative, object-oriented, dynamic language. DJS supports the particularly challenging features such as run-time type-tests, higher-order functions, extensible objects, prototype inheritance, and arrays through a combination of nested refinement types, strong updates to the heap, and heap unrolling to precisely track prototype hierarchies. With our implementation of DJS, we demonstrate that the type system is expressive enough to reason about a variety of tricky idioms found in small examples drawn from several sources,…

2012-08-01cs.PL

SafeRESTScript: Statically Checking REST API Consumers

Consumption of REST services has become a popular means of invoking code provided by third parties, particularly in web applications. Nowadays programmers of web applications can choose TypeScript over JavaScript to benefit from static type checking that enables validating calls to local functions or to those provided by libraries. Errors in calls to REST services, however, can only be found at run-time. In this paper, we present SafeRESTScript (SRS, for short) a language that extends the support of static analysis to calls to REST services, with the ability to statically find common errors su…

2020-07-16cs.PLcs.SE

Simple and Effective Type Check Removal through Lazy Basic Block Versioning

Dynamically typed programming languages such as JavaScript and Python defer type checking to run time. In order to maximize performance, dynamic language VM implementations must attempt to eliminate redundant dynamic type checks. However, type inference analyses are often costly and involve tradeoffs between compilation time and resulting precision. This has lead to the creation of increasingly complex multi-tiered VM architectures. This paper introduces lazy basic block versioning, a simple JIT compilation technique which effectively removes redundant type checks from critical code paths. Thi…

2015-05-29cs.PL

Just-in-Time Static Type Checking for Dynamic Languages

Dynamic languages such as Ruby, Python, and JavaScript have many compelling benefits, but the lack of static types means subtle errors can remain latent in code for a long time. While many researchers have developed various systems to bring some of the benefits of static types to dynamic languages, prior approaches have trouble dealing with metaprogramming, which generates code as the program executes. In this paper, we propose Hummingbird, a new system that uses a novel technique, just-in-time static type checking, to type check Ruby code even in the presence of metaprogramming. In Hummingbir…

2016-04-13cs.PL

Petrification：面向具有动态线程管理程序的软件模型检测（扩展版）

Petrification: Software Model Checking for Programs with Dynamic Thread Management (Extended Version)

本文针对动态 fork/join 线程的并发程序验证，提出 petrification 转换，将其归约为基于 Petri 网的固定线程数形式化体系，并在支持 pthreads 的 C 程序模型检测工具中实现。

2023-11-02cs.PL

更多相关论文收起更多论文

Bidirectional Type Checking for Relational Properties

Relational type systems have been designed for several applications including information flow, differential privacy, and cost analysis. In order to achieve the best results, these systems often use relational refinements and relational effects to maximally exploit the similarity in the structure of the two programs being compared. Relational type systems are appealing for relational properties because they deliver simpler and more precise verification than what could be derived from typing the two programs separately. However, relational type systems do not yet achieve the practical appeal of…

2018-12-12cs.PL

AgenticTyper: 使用代理AI自动类型化遗留软件项目

AgenticTyper: Automated Typing of Legacy Software Projects Using Agentic AI

Darmstadt University of Applied Sciences（达姆斯塔德应用技术大学）；MaibornWolff GmbH（马本沃尔夫公司）

AgenticTyper利用代理AI自动类型化遗留软件项目，通过迭代错误纠正和行为保留技术，高效解决类型错误问题。

2026-02-21cs.AIcs.MAcs.PL

用于快速准确边界检查的增强弱距离

Augmented Weak Distance for Fast and Accurate Bounds Checking

本研究提出增强弱距离（AWD）框架，通过单调收敛条件和逐路径分析解决原有WD框架的优化病态问题，在SV-COMP 2024边界检查基准上准确率达100%且速度较CBMC快170倍，为浮点程序验证提供高效精确的新方案。

2025-05-20cs.PL

扩展摘要：面向语法与类型指导的 NbE 的性能比较

Extended Abstract: Towards a Performance Comparison of Syntax and Type-Directed NbE

本文旨在开发一个平台，直接比较依赖类型检查器中语法指导与类型指导的相等性检查方法，量化后者的性能开销并分析改进途径。

2025-09-16cs.PL

Precise Null Pointer Analysis Through Global Value Numbering

Precise analysis of pointer information plays an important role in many static analysis techniques and tools today. The precision, however, must be balanced against the scalability of the analysis. This paper focusses on improving the precision of standard context and flow insensitive alias analysis algorithms at a low scalability cost. In particular, we present a semantics-preserving program transformation that drastically improves the precision of existing analyses when deciding if a pointer can alias NULL. Our program transformation is based on Global Value Numbering, a scheme inspired from…

2017-02-19cs.PL

使用上下文无关语言有序二叉决策图对RISC-V机器码进行有界模型检测

Bounded Model Checking of RISC-V Machine Code with Context-Free-Language Ordered Binary Decision Diagrams

本文将推理下沉至RISC-V机器码层面，开发了rotor和bitme工具，利用BDDs、ADDs和CFLOBDDs进行域传播以减少状态爆炸，显著加速SMT求解并提升位精确软件分析的可扩展性。

2025-07-13cs.PL

Local Refinement Typing

We introduce the Fusion algorithm for local refinement type inference, yielding a new SMT-based method for verifying programs with polymorphic data types and higher-order functions. Fusion is concise as the programmer need only write signatures for (externally exported) top-level functions and places with cyclic (recursive) dependencies, after which Fusion can predictably synthesize the most precise refinement types for all intermediate terms (expressible in the decidable refinement logic), thereby checking the program without false alarms. We have implemented Fusion and evaluated it on the be…

2017-06-24cs.PL

Structural Resolution for Abstract Compilation of Object-Oriented Languages

We propose abstract compilation for precise static type analysis of object-oriented languages based on coinductive logic programming. Source code is translated to a logic program, then type-checking and inference problems amount to queries to be solved with respect to the resulting logic program. We exploit a coinductive semantics to deal with infinite terms and proofs produced by recursive types and methods. Thanks to the recent notion of structural resolution for coinductive logic programming, we are able to infer very precise type information, including a class of irrational recursive types…

2017-09-14cs.PL

地方能力图：Rust所有权和借贷保证的通用模型

Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees

University of British Columbia（不列颠哥伦比亚大学）；ETH Zurich（苏黎世联邦理工学院）；New York University（纽约大学）

本文提出了一种名为地方能力图的模型，用于Rust所有权和借贷保证的验证和程序分析工具，支持超过97%的Rust函数。

2025-08-25cs.PL

Session Types Go Dynamic or How to Verify Your Python Conversations

This paper presents the first implementation of session types in a dynamically-typed language - Python. Communication safety of the whole system is guaranteed at runtime by monitors that check the execution traces comply with an associated protocol. Protocols are written in Scribble, a choreography description language based on multiparty session types, with addition of logic formulas for more precise behaviour properties. The presented framework overcomes the limitations of previous works on the session types where all endpoints should be statically typed so that they do not permit interopera…

2013-12-10cs.PL

VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts

We present VeriSmart, a highly precise verifier for ensuring arithmetic safety of Ethereum smart contracts. Writing safe smart contracts without unintended behavior is critically important because smart contracts are immutable and even a single flaw can cause huge financial damage. In particular, ensuring that arithmetic operations are safe is one of the most important and common security concerns of Ethereum smart contracts nowadays. In response, several safety analyzers have been proposed over the past few years, but state-of-the-art is still unsatisfactory; no existing tools achieve high pr…

2019-08-30cs.CRcs.PL

On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code

In recent projects on operating-system verification, C and C++ data types are often formalized using a semantics that does not fully specify the precise byte encoding of objects. It is well-known that such an underspecified data-type semantics can be used to detect certain kinds of type errors. In general, however, underspecified data-type semantics are unsound: they assign well-defined meaning to programs that have undefined behavior according to the C and C++ language standards. A precise characterization of the type-correctness properties that can be enforced with underspecified data-type s…

2012-11-27cs.LOcs.OScs.PL