The is_constructible checks in a path filter are supposed to see whether a path can be constructed without constructing any paths. They do things like changing 'does this statement pass through an atomic block?' to 'are there any atomic blocks in the thread' and 'does this path terminate in an if statement?' to 'are there any if statements in the thread'.
When there is only one of these checks, constructibility checks are sound. However, its handling of conjunctions between filtering steps is not: 'does this statement pass through an atomic block, and is it an if statement?' becomes 'are there any atomic blocks, and are there any if statements?' instead of 'are there any if statements in atomic blocks?'. This is obviously unsound; it would claim that in
atomic { x = 0; }
if (x == 0) { y = 1; }
we can construct such a path, when we can't.
There are a few ways we can remedy this, I think:
Abandon constructibility checks entirely, and instead just treat payload generation failures as a rejection of the action. This is the simplest approach, and also eliminates a lot of the semantic duplication in the path filter (each filtering needs to be given both a full check and a constructibility check), but will result in a lot of unnecessary path-generation backtracking, and also masks any legitimate errors in the process.
Always handle constructibility by trying to construct a path. This would be sound, but would be slow (twice the path generation, and, with Base_quickcheck, the path generation would probably not terminate as soon as it finds one witness).
Co-opt the path generation code somehow to make it possible to go through most of the motions in constructing a path, but outside of the path generation monad, and with short-circuiting.
Make the existing constructibility checks partial (eg. bool option instead of bool), return None when unsound complex checks arise, and do one of the above 'slow path' options.
I think I'll explore option 3 for now and, if it's too slow, consider re-adding fast-path checks on option 4.
The
is_constructiblechecks in a path filter are supposed to see whether a path can be constructed without constructing any paths. They do things like changing 'does this statement pass through an atomic block?' to 'are there any atomic blocks in the thread' and 'does this path terminate in an if statement?' to 'are there any if statements in the thread'.When there is only one of these checks, constructibility checks are sound. However, its handling of conjunctions between filtering steps is not: 'does this statement pass through an atomic block, and is it an if statement?' becomes 'are there any atomic blocks, and are there any if statements?' instead of 'are there any if statements in atomic blocks?'. This is obviously unsound; it would claim that in
we can construct such a path, when we can't.
There are a few ways we can remedy this, I think:
Base_quickcheck, the path generation would probably not terminate as soon as it finds one witness).bool optioninstead ofbool), returnNonewhen unsound complex checks arise, and do one of the above 'slow path' options.I think I'll explore option 3 for now and, if it's too slow, consider re-adding fast-path checks on option 4.