Redirecting control-flow inside atomic block
The following recently added benchmarks in the weaver
folder
popl20-figure3.wvr.yml
popl20-mult-4.wvr.yml
test-easy8.wvr.yml
violate the specification of atomic_begin/end
because they use assume_abort_if_not
inside the block:
"The verifiers are instructed to assume that the execution between those calls is not interrupted. The two calls need to occur within the same control-flow block; nesting or interleaving of those function calls is not allowed."
The three benchmarks have this pattern
__VERIFIER_atomic_begin();
assume_abort_if_not(assumption);
rest of the block;
__VERIFIER_atomic_end();
and thus I think the following modification should keep the intended semantics without breaking the control flow
bool local_assumption = false;
__VERIFIER_atomic_begin();
local_assumption = assumption // it is important to use a local variable so no one else can change the value
if (local_assumption) {
rest of the block;
}
__VERIFIER_atomic_end();
assume_abort_if_not(local_assumption)
@klumppdo if you agree, I can do the changes and create a MR.
Edited by Hernan Ponce de Leon