Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

HeapSeparator: Implement preprocessings, rework heap separation accordingly #295

Open
alexandernutz opened this issue Jan 12, 2018 · 0 comments

Comments

@alexandernutz
Copy link
Member

In order for the heap separator to make use of the map equality domain, and separate the heap-array, we need to apply a preprocessing to the input program.

Problem:
To get a good separation result, we cannot simply analyze which values a pointer variable may have at any location in the program, but we want to know which values it could have at any heap-write that reaches the read-location.

We would like to try two flavours, both introduce a preprocessing before the map equality domain is applied:

  1. "freeze-variables"
    at an array update l1: a[i] := v
    we add a nondeterministic update if (*) { frz_l1 := i }
    --> the analysis will derive all values that i can have during an update of a at location l1
  2. "memloc-array"
    introduce a special global array called memloc
    at an array update l1: a[i] := v
    for every program location li, introduce a literal lit_li
    we add the statement memloc[i] := lit_l1
    --> the analysis will derive for every memory location i, at which locations it may have been written

The map equality domain will run on the preprocessed program, and afterwards the heap separator will transform the original program based on the analysis result.

@alexandernutz alexandernutz self-assigned this Jan 12, 2018
alexandernutz added a commit that referenced this issue Jan 13, 2018
… ITransformulaTransformers anymore, introduced IcfgTransitionTransformer in order to be able to work on the IcfgEdges instead, rough implementation of StoreIndexFreezerIcfgTransformer
alexandernutz added a commit that referenced this issue Jan 13, 2018
…on: adding freeze var updates at array updates, initializing freeze vars with freeze var literals (still missing: initializing valid at freeze var literals), announcing freeze var literals to the equality domain
alexandernutz added a commit that referenced this issue Jan 18, 2018
…tle, the "downarrow" projection operator that is used to transform the program according to the heap separation result)
alexandernutz added a commit that referenced this issue Jan 19, 2018
alexandernutz added a commit that referenced this issue Jan 23, 2018
… in IcfgTransitionTransformer (scan created transformulas for fresh variables even when there is a corresponding formula in the old icfg)
alexandernutz added a commit that referenced this issue Jan 23, 2018
…valid-array; Use the symbol table-updating method of TransformedIcfgBuilder in IcfgTransitionTransformer
alexandernutz added a commit that referenced this issue Jan 26, 2018
…LocationBlocks must be relative to an ArrayGroup _and_ a dimension of the arrays in the group
alexandernutz added a commit that referenced this issue Jan 26, 2018
alexandernutz added a commit that referenced this issue Jan 26, 2018
alexandernutz added a commit that referenced this issue Jan 26, 2018
alexandernutz added a commit that referenced this issue Jan 27, 2018
…no write can have happend at this program point to this index"
alexandernutz added a commit that referenced this issue Jan 27, 2018
alexandernutz added a commit that referenced this issue Jan 27, 2018
alexandernutz added a commit that referenced this issue Jan 28, 2018
alexandernutz added a commit that referenced this issue Jan 28, 2018
…ongruenceClosure.assertHasOnlyWeqVarConstraints(..)
alexandernutz added a commit that referenced this issue Aug 24, 2018
…c-array updates, do the position-based substitution and the term-based substitution in one go (otherwise it is impossible to build Terms as they will have the wrong type)
alexandernutz added a commit that referenced this issue Aug 25, 2018
…rs, query for intermeditate eq state by edge of precprocessed graph, not the original one
alexandernutz added a commit that referenced this issue Aug 25, 2018
alexandernutz added a commit that referenced this issue Aug 25, 2018
…have to be normalized according to the given edge/transformula's invars/outvars..
alexandernutz added a commit that referenced this issue Aug 27, 2018
…n a loc-array is not touched during loc-array-preprocessing, but one of its values is queried, during partition computation
alexandernutz added a commit that referenced this issue Aug 28, 2018
…e formulas, too (only if they are in DNF, however)
alexandernutz added a commit that referenced this issue Sep 3, 2018
…all negative, to differentiate from normal StoreInfos)
alexandernutz added a commit that referenced this issue Sep 6, 2018
alexandernutz added a commit that referenced this issue Oct 3, 2018
alexandernutz added a commit that referenced this issue Oct 3, 2018
alexandernutz added a commit that referenced this issue Oct 3, 2018
alexandernutz added a commit that referenced this issue Oct 4, 2018
alexandernutz added a commit that referenced this issue Oct 8, 2018
alexandernutz added a commit that referenced this issue Oct 8, 2018
alexandernutz added a commit that referenced this issue Oct 9, 2018
… the corresponding array is guaranteed to be freshly havocced
alexandernutz added a commit that referenced this issue Oct 11, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants