Towards a Verified Range Analysis for Java']JavaScript JITs

被引：8

作者：

Brown, Fraser

Renner, John ^{[1
]}

Notzli, Andres

Lerner, Sorin ^{[1
]}

Shacham, Hovav ^{[2
]}

Stefan, Deian ^{[1
]}

机构：

[1] Univ Calif San Diego, La Jolla, CA USA

[2] UT Austin, Austin, TX USA

来源：

PROCEEDINGS OF THE 41ST ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '20) | 2020年

关键词：

JIT verification; range analysis; !text type='Java']Java[!/text]Script;

D O I：

10.1145/3385412.3385968

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We present VeRA, a system for verifying the range analysis pass in browser just-in-time (JIT) compilers. Browser developers write range analysis routines in a subset of C++, and verification developers write infrastructure to verify custom analysis properties. Then, VeRA automatically verifies the range analysis routines, which browser developers can integrate directly into the JIT. We use VeRA to translate and verify Firefox range analysis routines, and it detects a new, confirmed bug that has existed in the browser for six years.

引用

页码：135 / 150

页数：16

共 50 条

[31] Java']JavaScript revisited
Udell, J
BYTE, 1997, 22 (05): : 99 - &
[32] Java']JavaScript ROOT
Bellenot, Bertrand
Linev, Sergey
21ST INTERNATIONAL CONFERENCE ON COMPUTING IN HIGH ENERGY AND NUCLEAR PHYSICS (CHEP2015), PARTS 1-9, 2015, 664
[33] Adventures in Java']JavaScript
Moncur, M
BYTE, 1996, 21 (12): : 20 - 20
[34] The ABCs of Java']JavaScript
Kelly, AG
INTERNATIONAL JOURNAL OF INFORMATION MANAGEMENT, 1998, 18 (02) : 162 - 162
[35] The Rise of Java']JavaScript
DiPierro, Massimo
COMPUTING IN SCIENCE & ENGINEERING, 2018, 20 (01) : 9 - 10
[36] Brewing Java']JavaScript
Hoque, R
INTERNET WORLD, 1997, 8 (02): : 104 - 106
[37] All about the with Statement in Java']JavaScript: Removing with Statements in Java']JavaScript Applications
Park, Changhee
Lee, Hongki
Ryu, Sukyoung
ACM SIGPLAN NOTICES, 2014, 49 (02) : 73 - 84
[38] A Survey of Dynamic Analysis and Test Generation for Java']JavaScript
Andreasen, Esben
Gong, Liang
Moller, Anders
Pradel, Michael
Selakovic, Marija
Sen, Koushik
Staicu, Cristian-Alexandru
ACM COMPUTING SURVEYS, 2017, 50 (05)
[39] AUGUR: Dynamic Taint Analysis for Asynchronous Java']JavaScript
Aldrich, Mark W.
Turcotte, Alexi
Blanco, Matthew
Tip, Frank
PROCEEDINGS OF THE 37TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, ASE 2022, 2022,
[40] Purity analysis for Java']JavaScript through abstract interpretation
Nicolay, Jens
Stievenart, Quentin
De Meuter, Wolfgang
De Roover, Coen
JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS, 2017, 29 (12)

← 1 2 3 4 5 →