[P4Testgen] Remove complete from the model, make it part of the evaluation step instead. #4015
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
fruffy
force-pushed
the
fruffy/remove_complete
branch
from
b3c2597
to
a9b29d0
Compare
fruffy-bfn
force-pushed
the
fruffy/remove_complete
branch
from
17f4942
to
c7b4538
Compare
fruffy
changed the title
pkotikal
reviewed
Jun 9, 2023
| uint16_t numAllocatedPacketVariables = 0; | ||
|
|
||
| /// Helper function to create a new, unique symbolic packet variable. | ||
| /// Keeps track of the allocated packet variables by incrementing @ref |
There was a problem hiding this comment.
Nit: No ref in this context.
There was a problem hiding this comment.
It's a doxygen ref to the member value in the execution state. But I think we have not been writing doxygen comments right 😅 .
pkotikal
reviewed
Jun 9, 2023
| const IR::Expression *programPacket) { | ||
| // First propagate taint and simplify the packet. | ||
| const auto *taintedPacket = programPacket->apply(TaintPropagator(varMap)); | ||
| // Then create the mask based on the remaining expressions. | ||
| const auto *mask = taintedPacket->apply(MaskBuilder()); | ||
| // Produce the evaluated literal. The hex expression should only have 0 or f. | ||
| return completedModel->evaluate(mask); | ||
| return evaluatedModel->evaluate(mask, false); |
There was a problem hiding this comment.
There are only few places where this is false, so can't we make it a default argument as true?
There was a problem hiding this comment.
I have been thinking about this and I would rather make this explicit to force users to think about whether they want to autocomplete values or not.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The
completestep, which assigns default variables to symbolic variables that are not present in the Z3 model, is redundant. It requires us to keep track of symbolic variables in the execution state, which cost additional memory. Instead, we can just lazily complete a variable at the moment we evaluate it. We simply add a parameter to the evaluate function.With these changes we can both simplify the model and the execution state. For example, since we do not need to track variable creation any more we will not need the call
ExecutionState::createSymbolicVariableand can directly callToolsVariables::getSymbolicVariable. This means we do not always need an execution state to create a new symbolic variable.@vlstill With this change, use
ToolsVariables::getSymbolicVariableinstead ofnextState.createSymbolicVariable. Now there will not be an error anymore if one uses the wrong call to create a symbolic variable.