Correctly update symbolic variables that have been changed externally

Before, external changes to symbolic variables have not been propagated back to their internal representation.

Do a byte-by-byte comparison and potential update if required.

The test case is based on the example provided by Mingyi Liu from the mailing list.

Summary:

Checklist:

• [x] The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
• [x] The PR is divided into a logical sequence of commits OR a single commit is sufficient.
• [x] There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
• [x] Each commit has a meaningful message documenting what it does.
• [x] All messages added to the codebase, all comments, as well as commit messages are spellchecked.
• [x] The code is commented OR not applicable/necessary.
• [x] The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
• [x] There are test cases for the code you added or modified OR no such test cases are required.

May 11 '21 23:05 MartinNowack

Codecov Report

Merging #1407 (7021a89) into master (a01f46c) will increase coverage by 0.01%. The diff coverage is 70.96%.

@@            Coverage Diff             @@
##           master    #1407      +/-   ##
==========================================
+ Coverage   70.19%   70.21%   +0.01%     
==========================================
  Files         162      162              
  Lines       19395    19405      +10     
  Branches     4630     4634       +4     
==========================================
+ Hits        13615    13625      +10     
- Misses       3741     3743       +2     
+ Partials     2039     2037       -2     

May 11 '21 23:05 codecov[bot]

@MartinNowack thanks for this. I have finally looked at this patch, which is a bit tricky (in particular, I find the ObjectState class to be poorly documented, I'm currently doing a pass over it).

Here's how I would fix this: if the object was modified by the external call (if (memcmp(address, os->concreteStore, mo->size) != 0)) then we just need to mark it as fully concrete from then on and copy all the bytes. So essentially I would add before the existing memcpy(wos->concreteStore, address, mo->size); a call to wos->initializeToZero();.

Does this make sense?

Nov 03 '21 16:11 ccadar

@ccadar Thanks for the review and suggestion. One goal of the implementation was to keep as much symbolic information as possible. I was thinking about this, the downside from this suggestion is if larger memory objects are used for the external functions call, i.e. pointers into larger pre-allocated buffers. Of course, with external functions anyway, we loose some of the symbolic information in the first place.

Jan 05 '22 16:01 MartinNowack

That one is ready to be merged.

Feb 05 '24 10:02 MartinNowack

@ccadar Please merge this.

Feb 17 '24 10:02 MartinNowack

Hi @MartinNowack, thanks for this patch and sorry for the delay. However, this patch is not straightforward at all, despite its small size.

As I said, to me the straightforward solution I suggested in https://github.com/klee/klee/pull/1407#issuecomment-959724602 makes most sense, but you seem to suggest that a more complex one is needed, and I want to understand why.

Let me start by adding some review comments.

Feb 17 '24 12:02 ccadar

@ccadar Thanks for the review, I added a comment to the location of interest.

Feb 17 '24 19:02 MartinNowack

Thanks, @MartinNowack , great changes. Only a few minor issues left, see comments. The only bigger request, if feasible, would be for a test case demonstrating the bug you fixed.

Feb 28 '24 09:02 ccadar

Thanks, @MartinNowack, let's merge this one for v3.1, and keep in mind my remaining comments for future work involving external calls.

Feb 29 '24 19:02 ccadar