Draft: BAM SMG (mostly for discussion)
Adapt Symbolic Memory Graphs analysis to Block Abstraction Memoization. Work in progress.
SMG models program memory as a graph with edges between objects in memory and symbolic values: "has value" edge maps an object to a value in that memory and "points to" edge maps a value to an object with that address (edges also have respective offsets and sizes).
BAM uses given analysis to make summary of a function block or a loop block and then applies the block summary when analysis enters a block similar enough. Entry state is reduced (trimmed of info unneccessary for the block) and hashed to use in cache.
-
implement basic functionality (hash reduced state as is, make BAM possible to run) -
test entry and exit for function and loop blocks with simple tests - (see directory tests/programs/smg-bam)
-
test cache hits -
compare features on/off
Features
-
mimic memory allocation: - If block allocates memory, allocate similar memory anew (new values point to new objects with same size) next time the block summary is used.
-
Add out-of-block references. Analysis needs to know, if an object is still referenced. -
reduce stack -
Use reduced stack as default option. This increases cache hits slightly in programs from integration-smg test set.
-
-
reduce predicates and relations - Removing relations with values removed by
reduce()
seems to do little (at least for programs from integration-smg test set). - While most common case is empty path predicate and not-equals relation, keeping full information might be redundant.
-
Discard path predicate and not-equals. Keeping explicits seems to be neccessary (too many false positives otherwise). -
Trivial reduce. Might significantly increase cache hits, as a<=a
and0<10
are quite common. -
Smart reduce for relations. Example: if 0<a<b<c<d
is the full predicate, and only 0 and b are present in the SMG edges, we do not needb<c
andc<d
relations, and0<a
anda<b
can be replaced with weighted<=
operator as0<{2}=b
, where 2 stands for required difference. It seems quite tricky to reduce info from symbolic-to-explicit map, path predicate and not-equals this way, so I will return to this later.
- Removing relations with values removed by
-
'metasymbolic values': make a summary once, then use it with same SMG topology even with different symbolic values - Values are ordered by Has-Value SMG edges, the index is the metasymbolic value.
- Will work better with smart-reduce (see above). For now, path predicate and not-equals contain symbolic values, so if they are not discarded, hash will be different.
-
Maybe replace symbolic-to-explicit map with metasymbolic-to-explicit.