Concretize values based on seeds when available, remove --zero-seed-extension and improve/fix seeding code by ccadar · Pull Request #1663 · klee/klee

ccadar · 2023-10-20T21:11:58Z

Summary:

Concretize values based on seeds when available. The three commits handle the cases of concretizing an expression via toConstant, performing an external call with symbolic arguments and calling malloc with a symbolic argument, respectively.
Each case is accompanied by a test.

The PR is based on #1117 by @hoangmle

Checklist:

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

codecov · 2023-10-20T21:37:23Z

Codecov Report

Merging #1663 (4ee8690) into master (9edf8e8) will increase coverage by 0.12%.
Report is 1 commits behind head on master.
The diff coverage is 61.66%.

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #1663      +/-   ##
==========================================
+ Coverage   70.48%   70.61%   +0.12%     
==========================================
  Files         154      154              
  Lines       18870    18875       +5     
  Branches     4424     4426       +2     
==========================================
+ Hits        13301    13328      +27     
+ Misses       3654     3630      -24     
- Partials     1915     1917       +2

Files	Coverage Δ
include/klee/Expr/Assignment.h	`84.37% <100.00%> (ø)`
lib/Core/Executor.h	`77.27% <ø> (ø)`
lib/Core/SeedInfo.cpp	`11.53% <0.00%> (+0.69%)`	⬆️
lib/Core/Executor.cpp	`77.20% <69.23%> (+0.76%)`	⬆️

... and 1 file with indirect coverage changes

MartinNowack

@ccadar Thanks for reviving @hoangmle's PR and adding support for better seed handling.

I've added a more thorough comment to the first change.
Follow-up changes have similar issues.

In a nutshell, not every seed might lead to a constant expression, especially with changing pointers across runs plus patching up seeds.

lib/Core/Executor.cpp

ccadar · 2023-10-30T09:45:17Z

@MartinNowack thanks for the thorough review. My understanding was that @hoangmle 's contribution handled the most common case of a single seed -- see also the test cases. I was fine with that, and I think it's strictly better than what we have now. But let me think if the more complex cases could be easily handled as well.

ccadar · 2023-11-08T21:05:45Z

@MartinNowack thanks for the excellent review.
I have now extended the code to work with seed extension. In the process, I fixed a buffer overflow there and in general improved the code a bit. I have decided to remove --zero-seed-extension and merge it into --allow-seed-extension, as --zero-seed-extension, as implemented & documented, doesn't really make sense independently. Finally, I added two more test cases. Let me know if you have any other comments.

danielschemmel

I only went over the code, but did not try to semantically review the PR.

While some of the comments are stylistic choices, I also found a few instances of objects being copied as the loop variables of range-based for loops.

lib/Core/Executor.cpp

danielschemmel · 2023-11-20T22:15:56Z

lib/Core/Executor.cpp

+    auto found = seedMap.find(&state);
+    if (found != seedMap.end()) {


Suggested change

auto found = seedMap.find(&state);

if (found != seedMap.end()) {

if (auto found = seedMap.find(&state); found != seedMap.end()) {

lib/Core/SeedInfo.cpp

danielschemmel · 2023-11-20T22:18:24Z

lib/Core/SeedInfo.cpp

+    auto a = assignment.bindings.find(array);
+    if (a != assignment.bindings.end()) {


Suggested change

auto a = assignment.bindings.find(array);

if (a != assignment.bindings.end()) {

if (auto a = assignment.bindings.find(array); a != assignment.bindings.end()) {

…ts (w/ and w/o seed extension) based on FP concretization.

…able. Added a test case.

…on. This reworked logic also fixes a buffer overflow which could be triggered during seed extension.

… of queries

ccadar · 2023-11-23T09:14:47Z

@danielschemmel thanks for the additional suggestions; I have applied most of them.

@MartinNowack can you merge this, unless you have additional concerns?

251 · 2023-11-23T12:27:55Z

lib/Core/Executor.cpp

+  ref<Expr> value;
+  if (auto found = seedMap.find(&state); found != seedMap.end())
+    value = getValueFromSeeds(found->second, e);
+  /* If no seed evaluation results in a constant, call the solver */


Is there are reason for using C-style comments? It makes it harder to comment out blocks (due to nesting) and is not recommended by the LLVM coding standard:

https://llvm.org/docs/CodingStandards.html#comment-formatting

No particular reason, and I think we can live with both. I guess I could change it, but I'm not convinced it matters. And looking at the code, we seem to use both types of comments.
To comment out code, I recommend #if 0 / #endif which should work with both types of comments.

To comment out code, I recommend #if 0 / #endif which should work with both types of comments.

Common IDEs only support the traditional line/block comment via shortcuts but ok.

MartinNowack

@ccadar Thanks a lot for the changes. I'm mostly happy with it.

The only major issue I found is the newly introduced function getValueFromSeeds.
I would recommend changing it to simplify the code on the call side.

MartinNowack · 2023-11-24T07:46:10Z

lib/Core/Executor.h

+  /// first one that results in a constant, if such a seed exist.  Otherwise,
+  /// return the non-constant evaluation of the expression under one of the
+  /// seeds.
+  ref<klee::Expr> getValueFromSeeds(std::vector<SeedInfo> &seeds,


I would suggest to change the API of this call to use the current state as an argument and return a constant expression.

ref<klee::ConstantExpr> getValueFromSeeds(ExecutionState& state, const ref<Expr> &e);

As it stands now, all of the calls togetValueFromSeeds are guarded by a look-up of the seed vector with a subsequent check if the returned value is a constant expr.
Moving that lookup into the function itself makes that function easier to use.

This would simplify the code around quite a lot.

MartinNowack · 2023-11-24T07:49:18Z

lib/Core/Executor.cpp

-      assert(success && "FIXME: Unhandled solver failure");
-      (void) success;
-      ce->toMemory(&args[wordIndex]);
+      ref<ConstantExpr> cvalue;


This would become

ref<ConstantExpr> value = getValueFromSeeds(state, *ai); if (!value) { // do solver call }

… its callers

ccadar · 2023-12-04T23:13:49Z

Thanks for the extra feedback, @MartinNowack , I have refactored that function now.

MartinNowack

@ccadar Thanks a lot for the changes. Let's go for this one.
And also big thanks @hoangmle for the initial PR - highly appreciated.

ccadar mentioned this pull request Oct 20, 2023

Force concretization to follow seeds #1117

Closed

MartinNowack requested changes Oct 29, 2023

View reviewed changes

lib/Core/Executor.cpp Outdated Show resolved Hide resolved

lib/Core/Executor.cpp Outdated Show resolved Hide resolved

lib/Core/Executor.cpp Outdated Show resolved Hide resolved

lib/Core/Executor.cpp Outdated Show resolved Hide resolved

lib/Core/Executor.cpp Outdated Show resolved Hide resolved

ccadar mentioned this pull request Oct 30, 2023

Support for LLLVM 15 16 #1664

Merged

8 tasks

ccadar force-pushed the seed_concretization branch 7 times, most recently from 35b638b to 760b500 Compare November 8, 2023 19:43

ccadar changed the title ~~Concretize values based on seeds when available~~ Concretize values based on seeds when available, remove --zero-seed-extension and improve/fix seeding code Nov 8, 2023

danielschemmel requested changes Nov 20, 2023

View reviewed changes

ccadar force-pushed the seed_concretization branch from f5e6cc2 to dde390b Compare November 22, 2023 22:18

ccadar added 3 commits November 22, 2023 22:44

Concretize constants using seed values, when available. Added two tes…

edb3b20

…ts (w/ and w/o seed extension) based on FP concretization.

Concretize arguments to external function calls using seeds, if avail…

8394f8d

…able. Added a test case.

On a symbolic allocation, retrieve size from a seed, if available

9f57485

ccadar force-pushed the seed_concretization branch from dde390b to 345d4b1 Compare November 22, 2023 22:59

ccadar added 5 commits November 22, 2023 23:00

Refactored some code related to seeding.

912967a

Removed --zero-seed-extension, and merge it with --allow-seed-extensi…

bb1df23

…on. This reworked logic also fixes a buffer overflow which could be triggered during seed extension.

Added a test for --allow-seed-extension

a5b5bd6

Add checks to the seed concretization tests about the expected number…

c06e483

… of queries

Make Assignment::evaluate be const

1f9944b

ccadar force-pushed the seed_concretization branch from 345d4b1 to 1f9944b Compare November 22, 2023 23:00

251 reviewed Nov 23, 2023

View reviewed changes

MartinNowack reviewed Nov 24, 2023

View reviewed changes

Modify getValueFromSeeds() to include more functionality and simplify…

4ee8690

… its callers

MartinNowack approved these changes Jan 30, 2024

View reviewed changes

MartinNowack merged commit cb5e898 into klee:master Jan 30, 2024

		auto found = seedMap.find(&state);
		if (found != seedMap.end()) {

	auto found = seedMap.find(&state);
	if (found != seedMap.end()) {
	if (auto found = seedMap.find(&state); found != seedMap.end()) {

		auto a = assignment.bindings.find(array);
		if (a != assignment.bindings.end()) {

	auto a = assignment.bindings.find(array);
	if (a != assignment.bindings.end()) {
	if (auto a = assignment.bindings.find(array); a != assignment.bindings.end()) {

Conversation

ccadar commented Oct 20, 2023

Summary:

Checklist:

Uh oh!

codecov bot commented Oct 20, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

MartinNowack left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ccadar commented Oct 30, 2023

Uh oh!

ccadar commented Nov 8, 2023

Uh oh!

danielschemmel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

danielschemmel Nov 20, 2023

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

danielschemmel Nov 20, 2023

Choose a reason for hiding this comment

Uh oh!

ccadar commented Nov 23, 2023

Uh oh!

251 Nov 23, 2023

Choose a reason for hiding this comment

Uh oh!

ccadar Nov 23, 2023

Choose a reason for hiding this comment

Uh oh!

251 Nov 23, 2023

Choose a reason for hiding this comment

Uh oh!

MartinNowack left a comment

Choose a reason for hiding this comment

Uh oh!

MartinNowack Nov 24, 2023

Choose a reason for hiding this comment

Uh oh!

MartinNowack Nov 24, 2023

Choose a reason for hiding this comment

Uh oh!

ccadar commented Dec 4, 2023

Uh oh!

MartinNowack left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

codecov bot commented Oct 20, 2023 •

edited

Loading