General Solution For Cex Reconstruction #334
Labels
enhancement
New feature or request
Comments
d-xo
added a commit
that referenced
this issue
Jul 28, 2023
Sometimes we get back a model that does not mention all variables that are present in the input calldata buffer. This can happen if those variables are not relevant to the branch that we are producing a model for. In this case we can simply set the values that remain symbolic afters subsituting in our cex to some default value. We will still have issues here if we have lost some constraints over those variables during simplification, but it's better than what we're doing now (i.e. just printing "Any" if we can't get a fully concrete model for calldata out). A fully general (and hopefully correct) approach could look like: #334
d-xo
added a commit
that referenced
this issue
Jul 28, 2023
Sometimes we get back a model that does not mention all variables that are present in the input calldata buffer. This can happen if those variables are not relevant to the branch that we are producing a model for. In this case we can simply set the values that remain symbolic afters subsituting in our cex to some default value. We will still have issues here if we have lost some constraints over those variables during simplification, but it's better than what we're doing now (i.e. just printing "Any" if we can't get a fully concrete model for calldata out). A fully general (and hopefully correct) approach could look like: #334
4 tasks
d-xo
added a commit
that referenced
this issue
Jul 28, 2023
Sometimes we get back a model that does not mention all variables that are present in the input calldata buffer. This can happen if those variables are not relevant to the branch that we are producing a model for. In this case we can simply set the values that remain symbolic afters subsituting in our cex to some default value. We will still have issues here if we have lost some constraints over those variables during simplification, but it's better than what we're doing now (i.e. just printing "Any" if we can't get a fully concrete model for calldata out). A fully general (and hopefully correct) approach could look like: #334
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Right now we have some fairly ad hoc solutions to reconstruct proper Cexs when we have lost information due to simplification.
A more general approach that would work for all cases could look like this:
a == a || b == 6intoTrue, we lost information thatb == 6).Sat, declare all variables from step 1 that are not present in the current query, assert concrete values for any variables mentioned in the cex, assert all facts that were simplified away in step 2.check-sat, now we should have a full and valid cex for that branchThe text was updated successfully, but these errors were encountered: