Improving Symbolic Flat Memory Models with Pointer Alias Analysis
Junior Submission
Symbolic execution is an effective technique for exploring paths in a program and reasoning about all possible values on those paths. However, the technique still struggles with code that uses complex heap data structures, in which a pointer is allowed to refer to more than one memory object. In such cases, symbolic execution typically forks execution into multiple states, one for each object to which the pointer could refer. In this work, we propose a technique that avoids this expensive forking scheme by using a flat memory scheme instead, i.e. essentially merging all memory objects into one. To make this approach feasible, we use alias analysis to split the flat memory into multiple memory pools, and also implement a hybrid approach in which the flat memory and forking schemes co-exist. We evaluate our technique on a mix of synthetic benchmarks (which manipulate standard data structures such as matrices and hash tables) and real programs (such as m4 and make), and observe significant gains in terms of performance and memory usage, respectively.
(TimotejKapus.pdf) | 998KiB |
Wed 18 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:24 | |||
14:00 25mDoctoral symposium paper | Optimization based on Facts and Fiction Doc Symposium Olivier Flückiger Northeastern University, USA File Attached | ||
14:25 16mDoctoral symposium paper | Two-phase Analysis for Precision and Scalability Doc Symposium Anastasios Antoniadis University of Athens, Greece File Attached | ||
14:41 16mDoctoral symposium paper | Transparent Static Analysis for the Detection of Security Vulnerabilities Doc Symposium Goran Piskachev Fraunhofer IEM File Attached | ||
14:57 16mDoctoral symposium paper | Improving Symbolic Flat Memory Models with Pointer Alias Analysis Doc Symposium Timotej Kapus Imperial College London File Attached | ||
15:13 16mDoctoral symposium paper | Auto-tuning Framework for Multi-core Interference Analysis Doc Symposium Dan Iorga Imperial College London, UK |