Future-proofing around issue 30

[msaaltink]

While issue #30 is still open, some compositional proofs succeed even though they use overrides that are logically too weak. In particular, SAW appears to infer framing conditions (that is, variable not mentioned in the postcondition are assumed to be unchanged). Or so it seems from some experiments.

When issue #30 is fixed, then, existing proofs are likely to fail. I'd like to guard against that, so want to write postconditions that contain all the information they will need to. So if there is a plan in the works to address issue #30, does it answer the following:

• Does SAW know that parameters marked const t * cannot be changed directly? Looking at the generated llvm bitcode, it is not clear to me whether that information is transferred from the C sources.

• Similarly, does SAW know which global variables are constant, and which might change?

• Will SAW continue to assume that any global not mentioned in a postcondition has not been modified?

• Will using crucible_alloc_readonly add a framing condition for the associated parameter, so that a caller is assured the corresponding parameter is not modified?

Guidelines in this area will be useful for two reasons: first to avoid falling into the area of unsoundness, by putting enough information in a specification, and second to avoid the proofs breaking when issue #30 is fixed.

[langston-barrett]

I can address some of these questions that are related to the handling of globals, I think.

After #311 is merged, Crucible-based LLVM specifications will have to explicitly initialize any global variables they use (otherwise, the proof script will raise an error about uninitialized memory). Those initializations become preconditions: SAW will not erroneously rewrite using those lemmas without checking that the global variables have the right values.

[weaversa]

I'm also very interested in a solution to this.

saw does have some understanding of const values, but I'm not sure exactly what it assumes. If global variables are labeled as const then they do not need to be declared in saw.

I like the crucible_alloc_readonly path, if it's viable.