Contradictions between keep soft select and keep soft

TL;DR

When trying to constrain minimum and maximum payload size, the constraints in the test wouldn't be obeyed, due to a bad interaction between keep soft and keep soft ... select ==

The issue

We had the following code in our tests:

extend SEMI_RANDOM eth_seq {
    packet_size_mode : [ALL_JUMBO,MIX,NO_JUMBO,ALL_64];

    keep gen(packet_size_mode) before(min_payload_size,max_payload_size);

    keep packet_size_mode == ALL_64 => min_payload_size == 10;
    keep packet_size_mode == ALL_64 => max_payload_size == 10;
    keep packet_size_mode == ALL_JUMBO => min_payload_size == 1500;
    keep packet_size_mode == ALL_JUMBO => max_payload_size == 12000;
    keep packet_size_mode == MIX => min_payload_size == 1024;
    keep packet_size_mode == MIX => max_payload_size == 12000;
    keep packet_size_mode == NO_JUMBO => min_payload_size == 10;
    keep packet_size_mode == NO_JUMBO => max_payload_size == 1500;
    keep soft packet_size_mode == select {
        30 : ALL_JUMBO;
        30 : NO_JUMBO;
        60 : MIX;
        40 : ALL_64;
    };
};

In the sequence we had the following:

keep soft min_payload_size == 10;
keep soft max_payload_size == 1500;

This code was still part of our code base since before our move to IntelliGen. With IntelliGen, keep gen(...) before(...), is not taken into consideration anymore.

The current code caused IntelliGen to always select NO_JUMBO as that would obey all constraints. This would become even weirder, when we would comment out the other options from the soft select.

Solution

To solve the given issue, we need to call reset_soft() on the min and max payload size from the test, thereby disregarding the soft constraints in the sequence. The other option, which seems to be saner, is to demand users not to put soft constraints in the sequence. Constraints in sequences should only specify the legal boundaries of the sequence. Soft constraints should ONLY be used when the legal boundaries are too large for the default random tests.

I decided to go with the second option. Therefore I patched the sequence lib, file as such:

+    min_payload_size                    : uint [0..12228];
+    max_payload_size                    : uint [0..12228];
-    min_payload_size                    : uint;
-    max_payload_size                    : uint;

+    keep min_payload_size <= max_payload_size;
-    keep soft min_payload_size  == 10;
-    keep soft max_payload_size  == 1500;

This way we force the legal values, and allow soft constraints from the test to select any specific values.