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 and 0<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 need b<c and c<d relations, and 0<a and a<b can be replaced with weighted <= operator as 0<{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.
• '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.