1 Commits

Author	SHA1	Message	Date
Tristan Ravitch	80125921a9	This commit re-implements the memory model used by macaw symbolic ... There are two major changes: - The interface to memory models in Data.Macaw.Symbolic has changed - The suggested implementation in Data.Macaw.Symbolic.Memory has changed The change improves performance and fixes a soundness bug. * `macawExtensions` (Data.Macaw.Symbolic) takes a new argument: a `MkGlobalPointerValidityPred`. Use `mkGlobalPointerValidityPred` to provide one. * `mapRegionPointers` no longer takes a default pointer argument (delete it at call sites) * `GlobalMap` returns an `LLVMPtr sym w` instead of a `Maybe (LLVMPtr sym w)` Users of the suggested memory model do not need to worry about the last change, as it has been migrated. If you provided your own address mapping function, it must now be total. This is annoying, but the old API was unsound because macaw-symbolic did not have enough information to correctly handle the `Nothing` case. The idea of the change is that the mapping function should translate any concrete pointers as appropriate, while symbolic pointers should generate a mux over all possible allocations. Unfortunately, macaw-symbolic does not have enough information to generate the mux itself, as there may be allocations created externally. This interface and implementation is concerned with handling pointers to static memory in a binary. These are distinguished from pointers to dynamically-allocated or stack memory because many machine code instructions compute bitvectors and treat them as pointers. In the LLVM memory model used by macaw-symbolic, each memory allocation has a block identifier (a natural number). The stack and each heap allocation get unique block identifiers. However, pointers to static memory have no block identifier and must be mapped to a block in order to fit into the LLVM memory model. The previous implementation assigned each mapped memory segment in a binary to its own LLVM memory allocation. This had the nice property of implicitly proving that no memory access was touching unmapped memory. Unfortunately, it was especially inefficient in the presence of symbolic reads and writes, as it generated mux trees over all possible allocations and significantly slowed symbolic execution. The new memory model implementation (in Data.Macaw.Symbolic.Memory) instead uses a single allocation for all static allocations. This pushes more of the logic for resolving reads and writes into the SMT solver and the theory of arrays. In cases where sufficient constraints exist in path conditions, this means that we can support symbolic reads and writes. Additionally, since we have only a single SMT array backing all allocations, mapping bitvectors to LLVM pointers in the memory model is trivial: we just change their block identifier from zero (denoting a bitvector) to the block identifier of the unique allocation backing static data. This change has to do some extra work to ensure safety (especially that unmapped memory is never written to or read from). This is handled with the MkGlobalPointerValidityPred interface in Data.Macaw.Symbolic. This function, which is passed to the macaw-symbolic initialization, constructs well-formedness predicates for all pointers used to access memory. Symbolic execution tasks that do not need to enforce this property can simply provide a function that never returns any predicates to check. Implementations that want a reasonable default can use the mkGlobalPointerValidityPred from Data.Macaw.Symbolic.Memory. The default implementation ensures that no reads or writes touch unmapped memory and that writes to static data never write to read-only segments. This change also converts the examples in macaw-symbolic haddocks to use doctest to ensure that they do not get out of date. These are checked as part of CI.	2020-02-11 09:58:53 -08:00