Add support for variable-sized and variable-aligned allocations

[ThomasHaas]

This PR generalizes MemoryObject to be of variable size given by Expression size.
The encoding supports this now.
The reason the PR is marked as [DRAFT] is simply because it needs some minor cleanup and maybe more tests, but the functionality should be there.

Points of interest & possible pitfalls:

• Memory objects get two variables: address and size. The encoding enforces a deterministic memory layout as a function of the sizes of each object.
• We do not check if sizes/addresses are negative or if they overflow. This can cause different memory objects to get the same address.
• Dynamically allocated memory objects whose allocation sites were not executed still get a well-aligned address but receive size 0. As a consequence, these objects can actually overlap naturally but that should not matter I think.
• Somewhat in contrast to the above point, the current encoding always adds some non-zero offset to each address to ensure alignment even if the object happens to be aligned already (I don't encode a check to see if the alignment is already satisfied and unconditionally add some offset).

EDIT: I added a new feature, namely custom alignments for allocations. This even works for non-deterministic alignments.
The intrinsic aligned_alloc is now supported. However, we do not make any checks such as alignments must be positive and powers of two.

[ThomasHaas]

My newly added tests only work with the new alias analysis but RelationAnalysisTest seems to invoke the older one's, which causes an exception on those tests.
How should we go about this? Wait until #746 is fixed so that we can use the new analysis, or just exclude the tests?
If we exclude them, it would be easiest to just exclude the whole miscellaneous folder (e.g., by commenting out those test cases temporarily).

[hernanponcedeleon]

If we exclude them, it would be easiest to just exclude the whole miscellaneous folder (e.g., by commenting out those test cases temporarily).

You should rather create a new class for the new 2 tests and skip those in the RA test rather than (unnecessarily) removing all other miscellaneous tests.

[ThomasHaas]

It depends on what unnecessarily means. I could argue that RelationAnalysisTest already works around bug #746 but this workaround has become insufficient now and should thus be updated. And IMO workarounds should be as simple as possible.
I mean, do we really want to separate the two new tests into a separate folder and split the MiscellanousTest over two classes just to work around a bug? And then we undo this split once #746 is fixed? Or do we want to permanently establish separate tests for non-deterministic/variable-sized allocations?

[hernanponcedeleon]

Your point is fair. Let keep the RA test as it is.

Here are the results on the weaver benchmarks with a 15 min timeout, for reachability category, on commit d9abdfa

Statistics:            171 Files
  correct:              86
    correct true:       82
    correct false:       4
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:              85
  Score:               168 (max: 335)

Last year we solved 61 of the tasks.

Hopefully none of the latest commits changes things drastically in terms of what we can do with these benchmarks.

Is this still in DRAFT status or can it already be reviewed?

[ThomasHaas]

I think you can review it. I have changed the memory encoding as a whole so there might be regression on other benchmarks, though I kinda doubt it.

EDIT: Okay, there are 1 or 2 points I need to fix. DONE.