Skip to content

Draft: BAM SMG (mostly for discussion)

Петров Олег Максимович requested to merge smg-bam into smg-master

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.
Edited by Петров Олег Максимович

Merge request reports