Problem
This means the following free-related bugs are not detected:
- use after free
- double free
- ABA problem
Solution
To come to a solution, there are two kinds of solutions:
- Keep the memory slab currently employed by LLMC
- Implement a more sophisticated graph memory mechanism in order to detect heap-isomorphism
Memory slab
Within a memory slab, it is possible to implement a free list to keep track of free regions. This is a commonly used technique, even in real-world operating systems. Performance-wise, this might not be the ideal choice, as determining if a random memory address is allocated or not might involve traversing the list. To this end, a shadow memory could be added, with a bit (or more if the need arises) per 32-bit section to indicate if the section is allocated or not. There is no need to worry about the memory foot-print, since we use dtree for compression anyway.
Graph memory
Heap isomorphism detection is a great way or achieving partial order reduction [1]. When two traces in the state space are equivalent, except for the way the memory is laid out, it may be desirable to reduce them.
How exactly we can leverage dtree for graph memory remains to be researched.
[1] DiVM: Model Checking with LLVM and Graph Memory, https://arxiv.org/abs/1703.05341
Problem
This means the following free-related bugs are not detected:
Solution
To come to a solution, there are two kinds of solutions:
Memory slab
Within a memory slab, it is possible to implement a free list to keep track of free regions. This is a commonly used technique, even in real-world operating systems. Performance-wise, this might not be the ideal choice, as determining if a random memory address is allocated or not might involve traversing the list. To this end, a shadow memory could be added, with a bit (or more if the need arises) per 32-bit section to indicate if the section is allocated or not. There is no need to worry about the memory foot-print, since we use dtree for compression anyway.
Graph memory
Heap isomorphism detection is a great way or achieving partial order reduction [1]. When two traces in the state space are equivalent, except for the way the memory is laid out, it may be desirable to reduce them.
How exactly we can leverage dtree for graph memory remains to be researched.
[1] DiVM: Model Checking with LLVM and Graph Memory, https://arxiv.org/abs/1703.05341