challenge 06 desync issues

[robdockins]

The simplified challenge 06 example also suffers from control-flow desync issues, as of 0d80f8d and with the programtargets patch 41765a26fd93c58bd4f0c34233c2f2b29ba96f9e

cabal run pate -- -o ~/code/programtargets/challenge06-simplified/build/program_c -p ~/code/programtargets/challenge06-simplified/build/program_c.patched -V Debug --log-file ch06.log --strongestpost -b ~/code/programtargets/challenge06-simplified/build/challenge06.toml

ConcreteAddress 0x1065c (original) vs. ConcreteAddress 0x10698 (patched) program control flow desynchronized
  Original: 0x10680 analysis failure Just (0x1067c,"0x1067c: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
  Patched:  0x106bc analysis failure Just (0x106b8,"0x106b8: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
ConcreteAddress 0x1065c (original) vs. ConcreteAddress 0x10698 (patched) program control flow desynchronized
  Original: 0x10680 analysis failure Just (0x1067c,"0x1067c: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
  Patched:  0x106bc analysis failure Just (0x106b8,"0x106b8: BX_A1(0001xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 14, cond 0, QuasiMask0 QuasiMask\"(\"12): 4095")
ConcreteAddress 0x10a84 (original) vs. ConcreteAddress 0x10ac0 (patched) program control flow desynchronized
  Original: 0x10554 function call Just (0x10ab4,"0x10ab4: BLX_r_A1(0011xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 3, cond 14, QuasiMask0 QuasiMask\"(\"12): 4095")
  Patched:  0x10588 function call Just (0x10af0,"0x10af0: BLX_r_A1(0011xxxx.IIIIIIII.0010IIII.xxxx0001) Rm 3, cond 14, QuasiMask0 QuasiMask\"(\"12): 4095")
Overall verification verdict: Inequivalent

The BLX is an indirect call, I think, which might be kind of tricky. Perhaps the constant-propagation pass will help.

[travitch]

That is likely the memcpy that was called by function pointer. Constant propagation could (in principle) help there. More generally, we could be in trouble with function pointers. I guess the WP verifier was super unsound around those anyway, but doing it well will be challenging. The mitigation to that complexity is #269.

[robdockins]

Backing up to c0f3626 does not seem like it makes a difference for this example.