Interesting that the verification seems to be doing the right thing. Tweaking the bound up to 5 causes the verification to succeed, which is what I expect from a brief examination of the code.

Changing the solver doesn't seem to make any difference. Changing the path strategy to DFS generates other counterexample reports that are also wrong. It seems like there is something strange going on with the counterexample generation or rendering.

I think what's happening here is that the order of calls to crucible_int32_t in symbolic execution may be different than the order during concrete execution. So all of the results are "correct" in a sense, but they don't mean what they seem to mean.

Hypothesis: because of the break that depends on symbolic data, the number of times that fresh variables are created, and the order in which they appear is not obvious. We should probably generate a warning or even emit an error if we create a symbolic variable in the context of a branch, because then the results might be difficult/impossible to coordinate back to the source code.

Thinking about this some more, I think the correct way to handle this issue is to add an "in universe" event log where we can record events like the creation of fresh symbolic variables. This log will branch and merge in a similar way to how the write log for symbolic memory does.

When counterexamples are found, we can concretize and linearize this log (similar to how we do for memory logs), which will give an appropriate sequence of values for replay in a concrete run.

Update: PR #759 implements a new symbolic sequence type that I intend to use for event tracking. My plan was to have Crux add a new crucible global variable containing log event values of interest to crux. However, I now realize that these event logs actually need to be attached to proof obligations as assertions get made, so we properly capture the state of the log when assertions occur. This means they need to be incorporated somehow into the interface for Lang.Crucible.Backend. The way type information is piped around makes it pretty tricky to parameterize the event types according to the client, as that part of the backend code depends only on the sym, and not on the personality.

I'm going to scratch my head a bit about how to deal with this. I'm really reluctant to make this code depend on more type variables or such because the IsSymInterface constraint is quite pervasive and changing its shape would have wide-reaching downstream effects. On the other hand, finding a way to tuck this information down inside sym would probably require changes in What4 that address concerns that arise purely from a downstream client.

If each proof obligation is assigned a unique ID, and if the client (crux-llvm, if I understand the proposed solution) maintains a mapping from obligations to logs, would that solve the issue?

Kind of. That's pretty much what we are doing now for the "Bad behavior map" in crucible-llvm. The problem here is that this arises on a different axis of parameterization. The LLVM bad behaviors map is a language-specific mapping, and all the places where we make an assertion relevant to LLVM, crucible-llvm is in charge of doing that. Here, we want a layer of parameterization that is in the control of the downstream client (crux in this case), and we need to do some work at every assertion point (capture the current state of the log), even those that don't originate from inside the crux library.

This is basically why I opened #763.

#759 doesn't actually fix this issue

Worth noting with this issue: to reproduce with LLVM 11, I have to compile with -O0. With -O1, I have to turn on --path-sat or iteration bounds to get termination, and the resulting counterexample correctly aborts. shrug