The paper 'Random Testing for C and C++ Compilers with YARPGen' (to appear in OOPSLA) has a very nice table of operators that are not safe for random generation in certain conditions. While YARPGen uses these to decide when to substitute safe operators for unsafe operators, we can do something a bit more ACT-y: using known values to generate expressions with statically-known values.
For instance, we have the rule that x / y is safe if y is not 0 or -1 (with x being minimum int). We can then look up for variables whose known values are not 0 or -1, generate idempotent expressions over them, and plumb them into the expression. For things that also line up with atomic fetches, we could generate non-idempotent atomic fetches too.
Some of these rules are perhaps a little harder to express in this form, ie overflows; we might need to encode these in a special way (or as predicate functions, but this might be harder to extract candidate kvs from).
This would be a separate table from the algebra tables that we already have, which shouldn't intersect with unsafe operator instances.
The paper 'Random Testing for C and C++ Compilers with YARPGen' (to appear in OOPSLA) has a very nice table of operators that are not safe for random generation in certain conditions. While YARPGen uses these to decide when to substitute safe operators for unsafe operators, we can do something a bit more ACT-y: using known values to generate expressions with statically-known values.
For instance, we have the rule that
x / yis safe ifyis not0or-1(withxbeing minimum int). We can then look up for variables whose known values are not0or-1, generate idempotent expressions over them, and plumb them into the expression. For things that also line up with atomic fetches, we could generate non-idempotent atomic fetches too.Some of these rules are perhaps a little harder to express in this form, ie overflows; we might need to encode these in a special way (or as predicate functions, but this might be harder to extract candidate kvs from).
This would be a separate table from the algebra tables that we already have, which shouldn't intersect with unsafe operator instances.