Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

libs2eplugins: optionally create test cases when forking states #20

Merged
merged 1 commit into from Jul 7, 2020

Conversation

sebastianpoeplau
Copy link

Add an option ".generateOnStateFork" to the test-case generator (default false).
If enabled, a new test case with suffix "fork" is generated for each newly
forked execution state.

@@ -162,6 +170,12 @@ void TestCaseGenerator::onSegFault(S2EExecutionState *state, uint64_t pid, uint6
generateTestCases(state, ss.str(), TC_FILE);
}

void TestCaseGenerator::onStateFork(S2EExecutionState *state, const std::vector<S2EExecutionState*>& newStates, const std::vector<klee::ref<klee::Expr>>& newConditions) {
for (auto *state : newStates) {
Copy link
Member

@vitalych vitalych Jul 7, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

s/state/newState/ to avoid hiding the function parameter.
Also you need to have if (newState != state) otherwise, if, e.g., state 0 forks many times, you will create a new test case for state 0 on every fork (newStates contains state). Though you may have the case where state 0 never terminates, so you would have to handle this too somehow.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Another corner case is that plugins can call state->addConstraint(...) manually, which may recompute concolic inputs for the state. We may want and updated test case in this situation. That sounds more complex to implement however, maybe it can be skipped.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

s/state/newState/ to avoid hiding the function parameter.

Will do.

Also you need to have if (newState != state) otherwise, if, e.g., state 0 forks many times, you will create a new test case for state 0 on every fork (newStates contains state). Though you may have the case where state 0 never terminates, so you would have to handle this too somehow.

Hmm, I wasn't aware that newStates also contains the old state. I'll add the check. I think the case where state 0 never terminates isn't a problem because I usually know its input.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Another corner case is that plugins can call state->addConstraint(...) manually, which may recompute concolic inputs for the state. We may want and updated test case in this situation. That sounds more complex to implement however, maybe it can be skipped.

Wow, that one sounds more tricky to handle. Is it common for plugins to call that method?

Copy link
Member

@vitalych vitalych Jul 7, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

newStates is probably a misleading name. You can check in S2EExecutor::notifyFork how the vector is built.
S2E doesn't fork more than one state at a time, so the vector is pretty much always of size 2 (although plugins should not assume that). The first entry is the state where the fork condition is true, the second where it is false.

Regarding addConstraint(), you can ignore it. If someone needs to support it, they will fix it :)

@vitalych
Copy link
Member

vitalych commented Jul 7, 2020

Please squash the clang-format fix and do git push -f.

Add an option ".generateOnStateFork" to the test-case generator (default false).
If enabled, a new test case with suffix "fork" is generated for each newly
forked execution state.
@sebastianpoeplau
Copy link
Author

Pushed and squashed all changes as you suggested.

@vitalych vitalych merged commit 8eae6e3 into S2E:master Jul 7, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
2 participants