Open
Description
This issue contains all TODOs, so as not to forget them. If you complete any todo from this list, don't forget to add a link to the report in some form.
TODOs
- Benchmark different ways of collecting a guard in the
HeapRefSplittingUtil::filter
. - Make a single ite not only for symbolic heap refs, but for concrete heap refs too.
- Compare eager and lazy
UModel
performance. - Structure source files into packages. Fixed in Restructure packages #13
- Add simplifying
UFlatUpdates
inUComposer
(case composing on UModel, where stores are concretized and we expect a concrete reading returns a concrete value). Added in IntroduceUExprTranslator
,UModelBase
and revise regions composition #9 -
mkDistinct
with concrete heap refs. - Interning
URegionId
s. - Choose constant names carefully in
UExprTranslator
. - Deal with big arrays in composition. Idea: we can create a ranged update node with copy from big array and apply it to heap.
- Localized map in memory regions compostion.
- Refactor
UHeap
to generic implementation withgetMemoryRegion(regionId: URegionId)
. - Fix
Type
/ArrayType
inconsistence. - Make recursive-free implementations in
UFlatUpdates
. - Implement
UMemory::memset
. Added in Malloc with initializer & memset #17 - Revision and design
UComponents
and DI inusvm
. - Implement approximations for
Throwable
. - Choose a better way to place
close
function, related to this PR. - Refactor namings in
RegionTree
and all usages. Fixed in Region tree renaming and fix #26 - Fix equals for update nodes and add related tests.
- Think again about array casts and type elations with their elements.
- Think about region refinement with bv constraints and their interaction with memory regions (eager vs lazy style).
includesConcretely
,includesSymbolically
look like good extension points. - Fix translator cache usage in lazy models. Fixed in Fix and refactor decoder and translator #28
- Make cache in
DfsIterator
optional - Refactor the splitting read mechanism.
Metadata
Metadata
Assignees
Labels
No labels