Simplifications of consecutive Load and Store

[didriklundberg]

When generating weakest preconditions for programs containing many BExp_Loads and BExp_Stores - meaning any programs which uses the stack and not only purely registers - the multiple memory updates cause an explosion of the WP size (increasingly so for larger bit sizes).

Memory is something that must eventually be handled in an efficient manner. Therefore we must be able to simplify this to a tractable size and smart format for the final proving step.

[totorigolo]

One simple optimization would be to use FUPDATE_EQ, but only works with non simplified WP (i.e. too late). For simplified WP, I guess that something along those lines can be proved:

∀mem0 addr val1 val2.
  (mem1 = store (mem0, addr, val1)) /\ (mem2 = store (mem1, addr, val2))
  ==>
  (store (mem0, addr, val2) = mem2)

Is this what you had in mind?