Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 PLDI
Thu 24 Jun 2021 09:25 - 09:30 at PLDI-B - Talks 3B: Architectures and Systems
Thu 24 Jun 2021 21:25 - 21:30 at PLDI-B - Talks 3B: Architectures and Systems

Satisfiability Modulo Theories (SMT) solvers have been widely applied in automated software analysis to reason about the queries that encode the essence of program semantics, relieving the heavy burden of manual analysis. Many SMT solving techniques rely on solving Boolean satisfiability problem (SAT), which is an NP-complete problem, so they use heuristic search strategies to seek possible solutions, especially when no known theorem can efficiently reduce the problem. An emerging challenge, named Mixed-Bitwise-Arithmetic (MBA) obfuscation, impedes SMT solving by constructing identity equations with both bitwise operations (and, or, negate) and arithmetic computation (add, minus, multiply). Common math theorems for bitwise or arithmetic computation are inapplicable to simplifying MBA equations, leading to performance bottlenecks in SMT solving.

In this paper, we first scrutinize solvers' performance on solving different categories of MBA expressions: linear, polynomial, and non-polynomial. We observe that solvers can handle simple linear MBA expressions, but facing a severe performance slowdown when solving complex linear and non-linear MBA expressions. The root cause is that complex MBA expressions break the reduction laws for pure arithmetic or bitwise computation. To boost solvers' performance, we propose a semantic-preserving transformation to reduce the mixing degree of bitwise and arithmetic operations. We first calculate a signature vector based on the truth table extracted from an MBA expression, which captures the complete MBA semantics. Next, we generate a simpler MBA expression from the signature vector. Our large-scale evaluation on 3000 complex MBA equations shows that our technique significantly boost modern SMT solvers' performance on solving MBA formulas.

Thu 24 Jun

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 09:40
Talks 3B: Architectures and SystemsPLDI at PLDI-B +12h
09:00
5m
Talk
Reticle: A Virtual Machine for Programming Modern FPGAs
PLDI
Luis Vega University of Washington, Joseph McMahan University of Washington, Adrian Sampson Cornell University, Dan Grossman University of Washington, Luis Ceze University of Washington
DOI
09:05
5m
Talk
Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8
PLDI
Kyeongmin Cho KAIST, Sung-Hwan Lee Seoul National University, Azalea Raad Imperial College London, Jeehoon Kang KAIST
DOI
09:10
5m
Talk
Developer and User-Transparent Compiler Optimization for Interactive Applications
PLDI
Paschalis Mpeis University of Edinburgh, Pavlos Petoumenos University of Manchester, Kim Hazelwood Facebook AI Research, Hugh Leather Facebook
Link to publication DOI Media Attached
09:15
5m
Talk
Perceus: Garbage Free Reference Counting with Reuse
PLDI
Alex Reinking Microsoft Research, Ningning Xie University of Toronto, Leonardo de Moura Microsoft Research, Daan Leijen Microsoft Research
DOI
09:20
5m
Talk
Filling Typed Holes with Live GUIs
PLDI
Cyrus Omar University of Michigan, David Moon University of Michigan, Andrew Blinn University of Michigan, Ian Voysey Carnegie Mellon University, Nick Collins University of Chicago, Ravi Chugh University of Chicago
DOI Pre-print
09:25
5m
Talk
Boosting SMT Solver Performance on Mixed-Bitwise-Arithmetic Expressions
PLDI
Dongpeng Xu University of New Hampshire, Binbin Liu University of New Hampshire; University of Science and Technology of China, Weijie Feng University of Science and Technology of China, Jiang Ming University of Texas at Arlington, Qilong Zheng University of Science and Technology of China, Jing Li University of Science and Technology of China, Qiaoyan Yu University of New Hampshire
DOI
09:30
5m
Talk
Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems
PLDI
Milijana Surbatovich Carnegie Mellon University, Limin Jia Carnegie Mellon University, Brandon Lucia Carnegie Mellon University
DOI
09:35
5m
Talk
Bliss: Auto-tuning Complex Applications using a Pool of Diverse Lightweight Learning Models
PLDI
Rohan Basu Roy Northeastern University, Tirthak Patel Northeastern University, Vijay Gadepally MIT Lincoln Laboratory, Devesh Tiwari Northeastern University
DOI
21:00 - 21:40
Talks 3B: Architectures and SystemsPLDI at PLDI-B
21:00
5m
Talk
Reticle: A Virtual Machine for Programming Modern FPGAs
PLDI
Luis Vega University of Washington, Joseph McMahan University of Washington, Adrian Sampson Cornell University, Dan Grossman University of Washington, Luis Ceze University of Washington
DOI
21:05
5m
Talk
Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8
PLDI
Kyeongmin Cho KAIST, Sung-Hwan Lee Seoul National University, Azalea Raad Imperial College London, Jeehoon Kang KAIST
DOI
21:10
5m
Talk
Developer and User-Transparent Compiler Optimization for Interactive Applications
PLDI
Paschalis Mpeis University of Edinburgh, Pavlos Petoumenos University of Manchester, Kim Hazelwood Facebook AI Research, Hugh Leather Facebook
Link to publication DOI Media Attached
21:15
5m
Talk
Perceus: Garbage Free Reference Counting with Reuse
PLDI
Alex Reinking Microsoft Research, Ningning Xie University of Toronto, Leonardo de Moura Microsoft Research, Daan Leijen Microsoft Research
DOI
21:20
5m
Talk
Filling Typed Holes with Live GUIs
PLDI
Cyrus Omar University of Michigan, David Moon University of Michigan, Andrew Blinn University of Michigan, Ian Voysey Carnegie Mellon University, Nick Collins University of Chicago, Ravi Chugh University of Chicago
DOI Pre-print
21:25
5m
Talk
Boosting SMT Solver Performance on Mixed-Bitwise-Arithmetic Expressions
PLDI
Dongpeng Xu University of New Hampshire, Binbin Liu University of New Hampshire; University of Science and Technology of China, Weijie Feng University of Science and Technology of China, Jiang Ming University of Texas at Arlington, Qilong Zheng University of Science and Technology of China, Jing Li University of Science and Technology of China, Qiaoyan Yu University of New Hampshire
DOI
21:30
5m
Talk
Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems
PLDI
Milijana Surbatovich Carnegie Mellon University, Limin Jia Carnegie Mellon University, Brandon Lucia Carnegie Mellon University
DOI
21:35
5m
Talk
Bliss: Auto-tuning Complex Applications using a Pool of Diverse Lightweight Learning Models
PLDI
Rohan Basu Roy Northeastern University, Tirthak Patel Northeastern University, Vijay Gadepally MIT Lincoln Laboratory, Devesh Tiwari Northeastern University
DOI