[P4Testgen] Generate NoMatch for selects without default

[vlstill]

Previously, the testgen would generate NoMatch exception in parser only if it was caused by explicitly set value, but not when it was an implicit option based on symbolic input. This is now fixed. If there is no default a new successor (guarded by composite missCondition) will be added to the select expression.

I've opted to implementing this explicitly in the stepper as opposed to adding the HandleNoMatch midend pass as the latter would explicitly set the error instead of raising the exception. Note that for header stack overflow, testgen already uses a midend pass that sets the error using verify and this might be wrong.

@fruffy, I'm not sure if I need to change anything else (e.g. P4ProgramDCGCreator::preorder(const IR::SelectExpression *selectExpression). Also, I don't know how to test this automatically, is there a way for testgen test to check that coverage is 1?

[fruffy]

Could you add an example program that exhibits this problem? Just so I can verify myself. I need to check whether this complies with P4 specification behavior

[vlstill]

@fruffy, I've modified one of the BMV2 examples for this: bmv2_parse_nomatch.p4.

This is the result of testgen with this branch:

$ ./p4testgen --max-tests 32 --track-coverage STATEMENTS --target bmv2 --test-backend STF bmv2_parse_nomatch.p4
warning: Ingress parser exception handler not fully implemented
============ Test 0: Nodes covered: 0.5 (3/6) ============
============ Test 1: Nodes covered: 1 (6/6) ============
============ Test 2: Nodes covered: 1 (6/6) ============
============ Test 3: Nodes covered: 1 (6/6) ============
============ Test 4: Nodes covered: 1 (6/6) ============

The test 3 is the one with NoMatch.

with main:

warning: Ingress parser exception handler not fully implemented
============ Test 0: Nodes covered: 0.5 (3/6) ============
============ Test 1: Nodes covered: 1 (6/6) ============
============ Test 2: Nodes covered: 1 (6/6) ============
============ Test 3: Nodes covered: 1 (6/6) ============

… the NoMatch test is missing.

[vlstill]

This is the generated test that is missing in main: bmv2_parse_nomatch_3.stf. The important part is:

# [State] start
# [MethodCall]: pkt.extract<ethernet_t>(hdr.eth_hdr);
# [ExtractSuccess] hdr.eth_hdr@0 | Condition: |*packetLen_bits(bit<32>)| >= 112; | Extract Size: 112 -> hdr.eth_hdr.dst_addr = 0x0000_0000_0000 | hdr.eth_hdr.src_addr = 0x0000_0000_0000 | hdr.eth_hdr.eth_type = 0x2000
# [P4Testgen MethodCall]: *.copy_out(p);

[fruffy]

Suggested change

	// generate implicit NoMatch
	if (!hasDefault) {
	auto &nextState = state.clone();
	nextState.replaceTopBody(Continuation::Exception::NoMatch);
	result->emplace_back(missCondition, state, nextState);
	}
	// Generate implicit NoMatch.
	if (!hasDefault) {
	auto &nextState = state.clone();
	nextState.replaceTopBody(Continuation::Exception::NoMatch);
	result->emplace_back(missCondition, state, nextState);
	}

[fruffy]

Can you add a trace event for NoMatch? I would use Generic for that. Unfortunately, we do not have access to the parser state label here.

[vlstill]

@fruffy, I've added trace and refactored the code a bit to use stepNoMatch since I've noticed it is virtual and therefore could theoretically be used in descendants. I have hat to change its signature though, but at lest those using override will notice something changed (if there is such a backend somewhere).

Does it makes sense to have this virtual though -- I thought the errors are already parametrizable by the exception handlers and there would be no reason to parametrize them this way.

[vlstill]

I forgot to include the test fragment:

# [State] start
# [MethodCall]: pkt.extract<ethernet_t>(hdr.eth_hdr);
# [ExtractSuccess] hdr.eth_hdr@0 | Condition: |*packetLen_bits(bit<32>)| >= 112; | Extract Size: 112 -> hdr.eth_hdr.dst_addr = 0x0000_0000_0000 | hdr.eth_hdr.src_addr = 0x0000_0000_0000 | hdr.eth_hdr.eth_type = 0x2000
# [NoMatch]: Parser select expression did not match any alternatives.
# [P4Testgen MethodCall]: *.copy_out(p);

[fruffy]

Does it makes sense to have this virtual though -- I thought the errors are already parametrizable by the exception handlers and there would be no reason to parametrize them this way.

This might be an artifact from the early days of the implementation. I do not recall any particular use of overriding stepNoMatch.

[vlstill]

This one could be checked automatically with #4304.