Memory transform

[sadrabt]

Transforms memory accesses to register assignments using the results of DSA when --memory-transform flag is set
(requires --simplify and --dsa norm)

• creates a global graph (single global region node) and uses it to propagate global constraints among graphs of all procedures
• replaces memory stores to stack only regions with local assignments
• replaces memory stores to global only regions with memory assignments
• Adds invariant to check unresolved expressions are only used in memory accesses that are unreachable
• transforms memory accesses by splitting the memory to disjoint regions using Data structure analysis results
• determines which values escape a procedure using DSA flags

[ailrst]

The variable names in the output aren't going to be valid boogie identifiers, they should probably be renamed in the transform

[ailrst]

If we are only checking in results from one lifter can we use the gtirb results rather than BAP

[sadrabt]

do i need to update ResolveSpec in IRtoBoogie to have the spec include accesses to globals which have been transformed to a scalar

[ailrst]

Yeah I think so

[ailrst]

Don't need to fix for this PR but afterward I have TODO

• Go through and fix incomplete match warnings for MemoryAssign, I think there'll be some fixup for simp pass as well to handle them correctly
• Make memoryassign unique in the il output text

[ailrst]

StackIdentification should be disabled by --memory-transform probably, its further splitting the memory but probably not soundly

BASIL/src/main/scala/util/RunUtils.scala

Lines 321 to 324 in 7a851c7

	if (config.staticAnalysis.isEmpty || (config.staticAnalysis.get.memoryRegions == MemoryRegionsMode.Disabled)) {
	val stackIdentification = StackSubstituter()
	stackIdentification.visitProgram(ctx.program)
	}

e.g. with mill run --load-directory-gtirb examples/cntlm-noduk/ --simplify --dsa norm --main-procedure-name acl_add --memory-transform --dump-il x --procedure-call-depth 2 --trim-early

It seems like DSA already splits it into stack and heap when it can't do the local stack variable transform with mem being stack so the stackIdentification is probably breaking it