Skip to content

Assume or execute concretely support #69

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

Merged
merged 1 commit into from
Jun 21, 2022

Conversation

CaelmBleidd
Copy link
Member

@CaelmBleidd CaelmBleidd commented May 30, 2022

Closes #64.

Implemented a new class Assumption that contains required constraints for the symbolic execution, but which not nessesarily should be satisfied in real (concrete) execution.

Now UtSolver has three types of constraints:

  1. Hard constraints -- they must be satisfied at any point of the analysis;
  2. Soft constraints -- the solver tries to satisfy them, but they will be dropped if it is impossible or we couldn't determine if it possible during the timeout
  3. Assumptions -- they must be satisfied during the symbolic execution, but if at some point of the analysis we will receive unsat status from the solver, one of the assumptions will be in the produced unsat core and without it the request to the solver is SAT, we will run concrete execution from that point.

There were added corresponding tests for it and changes in utbot-api module.

Note: I've tried to remove all the assume instructions from the preconditionChecks of the wrappers, but seems like it is impossible because of untimely contradiction raised in the preconditionCheck analysis of the UtHashMap and UtHashSet (in the cycle). More details you can find in the design doc docs/AssumptionsMechanism.md

@CaelmBleidd CaelmBleidd changed the title Caelmbleidd/assume or execute concretely support Assume or execute concretely support May 30, 2022
@CaelmBleidd CaelmBleidd force-pushed the caelmbleidd/assume_or_execute_concretely_support branch from 60de996 to a09f1e7 Compare May 30, 2022 13:50
@CaelmBleidd CaelmBleidd marked this pull request as ready for review May 31, 2022 14:10
@CaelmBleidd CaelmBleidd marked this pull request as draft May 31, 2022 14:10
@CaelmBleidd CaelmBleidd force-pushed the caelmbleidd/assume_or_execute_concretely_support branch 8 times, most recently from 4a98de0 to 207c081 Compare June 7, 2022 15:38
@CaelmBleidd CaelmBleidd marked this pull request as ready for review June 7, 2022 20:29
@CaelmBleidd CaelmBleidd force-pushed the caelmbleidd/assume_or_execute_concretely_support branch 2 times, most recently from 6a349cf to c08b3bc Compare June 8, 2022 15:00
@CaelmBleidd CaelmBleidd force-pushed the caelmbleidd/assume_or_execute_concretely_support branch from c08b3bc to 8835a63 Compare June 14, 2022 14:48
@CaelmBleidd CaelmBleidd force-pushed the caelmbleidd/assume_or_execute_concretely_support branch 2 times, most recently from 6674975 to d7b0fd6 Compare June 19, 2022 14:19
@CaelmBleidd CaelmBleidd force-pushed the caelmbleidd/assume_or_execute_concretely_support branch from d7b0fd6 to 6dfec3f Compare June 21, 2022 08:29
@CaelmBleidd CaelmBleidd merged commit 339cdf6 into main Jun 21, 2022
@CaelmBleidd CaelmBleidd deleted the caelmbleidd/assume_or_execute_concretely_support branch June 21, 2022 11:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

AssumeOrExecuteConcretely support
4 participants