A segmented memory model for symbolic execution
| Autor: | Cristian Cadar, Timotej Kapus |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Computer science
020207 software engineering 02 engineering and technology Parallel computing Data structure Symbolic execution Single segment Memory object 020204 information systems Pointer (computer programming) 0202 electrical engineering electronic engineering information engineering Memory segmentation Memory model Heap (data structure) |
| Zdroj: | ESEC/SIGSOFT FSE ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE ’19) |
| DOI: | 10.1145/3338906.3338936 |
| Popis: | 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 paper, we propose a technique that avoids this expensive forking by using a segmented memory model. In this model, memory is split into segments, so that each symbolic pointer refers to objects in a single segment. The size of the segments are bound by a threshold, in order to avoid expensive constraints. This results in a memory model where forking due to symbolic pointer dereferences is significantly reduced, often completely. We evaluate our segmented memory model on a mix of whole program benchmarks (such as m4 and make) and library benchmarks (such as SQLite), and observe significant decreases in execution time and memory usage. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|