Add assert and assume mode for testgen. #3775
Conversation
| @@ -65,6 +65,14 @@ class TestgenOptions : public AbstractP4cToolOptions { | |||
| /// for statement reachability analysis. | |||
| bool dcg = false; | |||
|
|
|||
| /// Add conditions defined in assert/assume to the path conditions. | |||
| /// Only tests which satisfy these conditions can be generated. | |||
| bool enforceAssumptions = false; | |||
There was a problem hiding this comment.
Do you plan on there being a way to only add conditions for assume, but not for assert?
I could imagine one might want to enforce assume conditions in tests created, but at the same time try to find tests that violate assert conditions.
Why? assume would be conditions of "I am telling you I will be operating in an environment where these conditions are true, for reasons that are not necessarily possible to infer from the P4 source code, e.g. because I know I am operating in an environment where I will never see these protocol/NextHeader values.", but assert statements would be conditions of "I am hoping these conditions are always true, but want the tools to catch me if I am wrong in this hope."
There was a problem hiding this comment.
Yes, this is still in draft mode. Currently, we have two flags.
- If only
enforceAssumptionsis active, P4Testgen will only generate tests that satisfy all assert and assume conditions. - If also
genAssertionViolationsis active, P4Testgen will try to only produce tests that violate assertions also including assumptions in assume calls. - If only
genAssertionViolationsis active, P4Testgen will not add assumptions to the path and only generate tests that violate asserts.
The tricky part is generating only violating tests while exploring the full program(i.e., not stopping at the first violating assert).
There was a problem hiding this comment.
This feature is now ready and can be co-developed with p4lang/p4-spec#1207. Testgen can implement the specified functionality with assumption and assertion mode. The question is how to write tests here.
fruffy-bfn
force-pushed
the
testgen_assert_assume
branch
2 times, most recently
from
cca73e2
to
b74c29e
Compare
fruffy-bfn
requested review from
fruffy,
pkotikal,
vhavel,
jnfoster and
mihaibudiu
as code owners
fruffy-bfn
force-pushed
the
testgen_assert_assume
branch
from
b74c29e
to
1fbdfeb
Compare
fruffy
force-pushed
the
testgen_assert_assume
branch
3 times, most recently
from
27f69c0
to
b747f2a
Compare
fruffy
force-pushed
the
testgen_assert_assume
branch
3 times, most recently
from
9847a1f
to
ad4e7d4
Compare
There was a problem hiding this comment.
I suggest we make --assumption-mode always active, or at least default.
Imagine a situation, where P4 programmer adds assume() calls to instruct a P4 compiler that only certain match key combinations are valid, and the P4 compiler uses this information to optimize, but generates "incorrect" code for control plane setup where the assumption doesn't hold. I think it would be surprising if testgen generated tests which trigger this "undefined behavior".
Or do you expect use cases where testcases which do not satisfy all assume conditions are wanted?
| // If assertion mode is active, ignore any test that does not trigger an assertion. | ||
| if (TestgenOptions::get().assertionModeEnabled) { | ||
| if (!executionState->getProperty<bool>("assertionTriggered")) { | ||
| return testCount > maxTests - 1; |
| @@ -110,6 +110,14 @@ bool TestBackEnd::run(const FinalState &state) { | |||
| auto *solver = state.getSolver()->to<Z3Solver>(); | |||
| CHECK_NULL(solver); | |||
|
|
|||
| // If assertion mode is active, ignore any test that does not trigger an assertion. | |||
| if (TestgenOptions::get().assertionModeEnabled) { | |||
There was a problem hiding this comment.
What if withOutputPacket is also active, how these two options should interact? Shouldn't the if-condition with withOutputPacket come first?
fruffy-bfn
force-pushed
the
testgen_assert_assume
branch
from
ad4e7d4
to
8cf7951
Compare
fruffy-bfn
force-pushed
the
testgen_assert_assume
branch
from
8cf7951
to
01462bc
Compare
This PR adds assert and assume mode to P4Testgen. These modes can be enabled via the
--assumption-modeand--assertion-modeflags.--assumption-modeis active, P4Testgen will only generate tests that satisfy all assert and assume conditions.--assertion-modeis active, P4Testgen will try to only produce tests that violate assertions also including assumptions in assume calls.--assertion-modeis active, P4Testgen will not add assumptions to the path and only generate tests that violate asserts.