Constants can't depend on globals

[glguy]

Constants need to be able to assume that globals are allocated.

I believe that we either need to stop assuming that constants can always be allocated or start assuming that globals are always allocated.

This statement is filtering out non-constant globals just before it tries to initialize all constants.

saw-script/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs

Lines 1762 to 1763 in f648b72

	mem <- Crucible.populateConstGlobals bak (view Crucible.globalInitMap mtrans)
	=<< Crucible.initializeMemoryConstGlobals bak ctx llvm_mod

Here's an example.

example.c

char gstuff[] = "stuff";
char* const p = &gstuff[2];
void noop() {}

clang -c example.c -emit-llvm

example.saw

m <- llvm_load_module "example.bc";
llvm_verify m "noop" [] false (llvm_execute_func []) rme;

AssertionFailure :1:0: error: in _start
Global symbol not allocated
Details:
  Global symbol "gstuff" has no associated allocation

[RyanGlScott]

The reason that SAW uses initializeMemoryConstGlobals to only populate immutable globals is an attempt to avoid a potential source of unsoundness when verifying functions that use mutable global variables. This potential source of unsoundness is described in more detail here, but to summarize, SAW's solution to prevent this unsoundness requires that users explicitly allocate (using llvm_alloc_global) and initialize (using llvm_points_to) mutable globals when verifying a function.

As part of the current implementation of this part of SAW, it simply does not allocate or initialize any mutable globals at all upon loading the LLVM module, instead deferring these steps until SAW interprets the LLVM spec during verification. This has an unfortunate interaction with translating constants, however, which is something that happens during module loading. Because SAW does not allocate mutable globals when translating the module, the constant translation crashes when it encounters a mutable global that has not yet been allocated (e.g., the mutable global gstuff, used in the definition of the p constant in the program above).

#2623 proposes to fix this by always allocating mutable globals upon loading the LLVM module. I am reluctant to do this, as it means that users would no longer be required to write llvm_alloc_global in their specs. That, in turn, makes it much harder to tell which mutable globals are actually involved in the specification of a function—if everything is allocated, then potentially any mutable global could be written to. That makes certain static checks that SAW performs much harder, such as the check it performs to see if there are any underspecified mutable global variables in the postconditions of a compositional override.

Talking with @glguy about this some more, there is a potential middle ground: allocate and populate all global variables for the sake of translating constants (so that translating p would succeed), but when verifying a function in isolation, assume that each mutable global variable cannot be written to unless declared using llvm_alloc_global, and assume that each mutable global variable cannot be read from unless declared using llvm_points_to. This would achieve the best of both worlds.

[glguy]

A simpler solution would be to add a toggle to always allocate all globals. Verifications of files that don't have constants that depend on allocated globals would continue to be more convenient to verify, and ones that do have them would just need to be more explicit about maintaining global variable state, but they'd still be sound.

Doing this would probably be a much smaller change that trying to adapt the compositional verification logic to try and prevent people from assigning globals that weren't mentioned in an llvm_alloc_global

[RyanGlScott]

That would work, I suppose, although it's a fairly crude solution. Perhaps we should hide this behind an experimental enable_* feature so that only power users reach for it (similar to enable_lax_loads_and_stores)?

[glguy]

I updated the PR to make this a configurable, experimental knob.

To do something fancier we'd need to be quite certain that someone couldn't get backdoor access to a global that we were pretending wasn't available via a constant that took its address. I don't really have time to be fancy and I don't want to implement something unsound in a rush

[sauclovian-g]

I finally figured out what I don't like about that check: it's papering over an internal bug, which is that the spec with no assertion in the postcondition is interpreted differently in different contexts: verification treats the value as unspecified but overrides treat it as unchanged.

I think if we fixed that such that you can't write to anything that doesn't have a value bound in the postcondition, it would also eliminate this problem: the code under verification wouldn't be able to write to a global unless all of the stuff needed to assert a postcondition value appeared in the spec. However, that's even fancier :-|

[sauclovian-g]

ISTM if you need an immediate fix, do the quick thing, mark it experimental, and note in its documentation/help text that it's an ad hoc solution to a specific problem. Leave this issue open and we'll get it fixed properly later; the cost of that is that probably having to adjust your stuff later too.