What4 has the capacity to turn symbolic values into plausible "concrete" (/"ground") values, given a model from the SMT solver (GroundEvalFn). This commit builds on this feature to enable concretizing more complex Crucible types.
A possible use-case is to present concrete instances where safety assertions fail, e.g. when symbolically executing the following function:
int f(int x, int y) { return x / (y - 2); }
it would be nice to say which particular values of x and y would cause either signed underflow (y < INT_MIN + 2) or division by zero (y == 2). This particular case could be handled by existing What4 functionality, but the same motivation applies to more complex cases involving Crucible-specific types.
What4 has the capacity to turn symbolic values into plausible "concrete" (/"ground") values, given a model from the SMT solver (
GroundEvalFn). This commit builds on this feature to enable concretizing more complex Crucible types.A possible use-case is to present concrete instances where safety assertions fail, e.g. when symbolically executing the following function:
it would be nice to say which particular values of
xandywould cause either signed underflow (y < INT_MIN + 2) or division by zero (y == 2). This particular case could be handled by existing What4 functionality, but the same motivation applies to more complex cases involving Crucible-specific types.