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 Jul Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 14:25 Doctoral symposium paper | Optimization based on Facts and Fiction Doc Symposium Olivier FlückigerNortheastern University, USA File Attached | ||
14:25 - 14:41 Doctoral symposium paper | Two-phase Analysis for Precision and Scalability Doc Symposium Anastasios AntoniadisUniversity of Athens, Greece File Attached | ||
14:41 - 14:57 Doctoral symposium paper | Transparent Static Analysis for the Detection of Security Vulnerabilities Doc Symposium Goran PiskachevFraunhofer IEM File Attached | ||
14:57 - 15:13 Doctoral symposium paper | Improving Symbolic Flat Memory Models with Pointer Alias Analysis Doc Symposium Timotej KapusImperial College London File Attached | ||
15:13 - 15:29 Doctoral symposium paper | Auto-tuning Framework for Multi-core Interference Analysis Doc Symposium Dan IorgaImperial College London, UK |