scribble icon indicating copy to clipboard operation
scribble copied to clipboard

Support multiple properties in `#try`

Open cd1m0 opened this issue 4 years ago • 0 comments

In #112 we added the new #try annotation that can guide underlying tools (e.g. Harvey) by giving them vacuous target branches to flip. Currently #try accepts a single predicate:

#try x == 1;

To express multiple predicates to try independently, we need multiple tries:

#try x == 1;
#try y == 2;
#try z == 3;

It would be a little cleaner to allow #try to take multiple predicates, where the semantics is the same as if there were multiple tries, one per predicate. So the above would be equivalently expressed as:

#try x ==1, y==2, z== 3;

Note that these shouldn't just be treated as one giant disjunction x == 1 || y ==2 || z ==3. If we transpile them as such, then due to short-circuiting of the compiler, certain truth combinations will not be explored. For example if x==1, the emitted code will not even evaluate y==2 || z ==3, so for example the fuzzer will not explore x == 1 && y == 2 and x == 1 && y != 2.

cd1m0 avatar Nov 16 '21 23:11 cd1m0