Support providing different overrides to the original vs. patched target

[thebendavis]

• Step 1. write the override for socket receive. behavior: constrain bytes 4 and 5 to be <= 0x300 in the "patched" version
• Step 2. write the override for the "transmit buffer" function: if bytes 4 and 5 exceed 0x300, emit an observable event representing the "crash" behavior
• Step 3. see if our equivalence condition extraction works, using the path/mux version (rather than the control flow version we've been using more recently). seems fair to add a special tag/term of what to use here, representing operator insight into what they want to check about the patch
• Step 4. wire up the "capture in equivalence condition" action in the UI. we already have a version of this we use in the scada example, but it's using the control-flow equiv-cond thing, we should also add the option to use the path/mux version; we use terminology "use intra block path conditions" or similar elsewhere

[lcasburn]

From @danmatichuk

• Step 1 is implemented. Verifier picks up stub and executes. Get symbolic semantics that is expected, however, there's significant performance bottleneck during memory address concretization leading to execution time that's >10mins.

Proposed next steps

• Simplify read stub semantics to avoid large mux.
• If concretization is still slow, add hint within stub to tell verifier that pointer term is not concrete, do not attempt to concretize it. Tagging is already well supported in What4.
• Try another solver with arrayCopy primitive and concrete bound

Conclusion: 7/8/24

• Added simplifying assumption that reduces read operation to large bitvector read representing entire length. No longer have large mux of operations.

[lcasburn]

From @danmatichuk

Currently between step 1 and Step 2. Cannot carry domain information from step 1 into step2. There's step missing that we need to address.

At the point we have a non-trivial equivalence domain with pointer that cannot be re-scoped, we can try to assume particular concrete value for link register.

• Either this would allow global pointer to be resolved to concrete value (and thus trivially rescoped) or we have more symbolic information that needs to be concretized.

Alternatively, change stub definition to ignore the buffer that we give it. Hardcode some global value and use that in the stubs to ignore the buffer. Dan decided this is the easiest step to take first.

Update 7/10/24:

• This approach of hardcoding global value didn't work, because lack of pointer aliasing information meant that we don't know for any symbolic pointer whether it would alias that global value we invented. Instead, we allocate fresh buffer. Challenge will be to ensure that the consumer and producer stub use the same buffer.

[lcasburn]

From @danmatichuk

The verifier now identifies a potential difference in memory but it's not observable, it's trying to put this in the equivalence domain. However, it cannot properly rescope that variable. However, because the difference isn't observable, it doesn't trigger the mechanism to prompt the user for an assertion. Without the assertion we get an error/warning about how the verifier needed to introduce unsoundness to continue.

Without adding equivalence condition, we quickly run into memory separation issues (see #419). We could manually add an assertion (i.e. add an equivalence condition as an assumption) needed to bypass this issue.

However, writing consumer stub first likely enables us to leverage infrastructure that lets user add assertions (i.e. add an equivalence condition as an assumption).

Next step: Add consumer stub that introduces observable event that checks for size mismatch.

• Challenge: Ensuring producer and consumer stub use the same buffer. We would know that buffers are same without the conditional memory allocation.

[lcasburn]

From @danmatichuk:

Added stub/spec that introduced pre-condition that we needed to prove. PR #409 closes this ticket.

This example illustrates there's only so far we can get in trying to infer specifications. In the future, we could introduce more general pattern where user somehow provides functional specification.