[
https://issues.apache.org/jira/browse/CAMEL-26437?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18136063#comment-18136063
]
shashank commented on CAMEL-26437:
----------------------------------
After the fix was merged, I also checked it with a JML specification proved by
OpenJML, as a test of the method that found the issue.
*What was proved*
* All six methods of {{FilterIterator}} verify against the specification: both
constructors, {{hasNext}}, {{next}}, {{remove}} and {{checkNext}} (6 valid, 0
invalid, no timeouts). The loop in {{checkNext}} keeps the invariant that
removal is allowed only while the wrapped iterator is still on the element
{{next()}} returned, and {{remove()}} removes exactly that element.
* The preconditions and exits of every method were checked to be reachable, so
the proof is not vacuous.
* Taking out only the one line of the fix ({{canRemove = false}} before
{{it.next()}} in {{checkNext}}) makes the loop-invariant check fail. Five other
mutants are rejected as well: a wrong constructor, a missing invalidation in
{{hasNext}}, a missing permission in {{next}}, and a {{remove}} that does not
delete.
* Dynamic checks of the same code pass: about 120,000 random operations, 2,000
differential sequences against a reference model, every rejected-tail length up
to 128, and the null and filter-exception cases.
*Assumptions and limits*
The wrapped iterator supports {{remove}}. The filter has no side effects and
may throw {{IllegalArgumentException}}. Other {{RuntimeException}} types,
concurrent use, changes to the collection from outside and subclasses are not
part of the proved result; the verifier reports internal warnings on the
broader exception specification, so that run is not counted. The fix itself
does not depend on the exception type, since it clears the permission before
the wrapped iterator moves.
The specification lives outside the Camel code base; nothing in Camel changes.
_Claude Code on behalf of allthingssecurity._
> camel-util - FilterIterator.remove after a failed next removes an element
> that next never returned
> --------------------------------------------------------------------------------------------------
>
> Key: CAMEL-26437
> URL: https://issues.apache.org/jira/browse/CAMEL-26437
> Project: Camel
> Issue Type: Bug
> Components: camel-core
> Reporter: shashank
> Assignee: shashank
> Priority: Minor
> Fix For: 4.24.0
>
>
> Follow-up of CAMEL-26290 (apache/camel#28643), which made
> {{FilterIterator.remove()}} throw {{IllegalStateException}} after a
> {{hasNext()}} look-ahead, because the look-ahead moves the wrapped iterator
> past the element {{next()}} returned.
> {{next()}} looks ahead in the same way when it has no element ready:
> {{checkNext()}} calls {{it.next()}} on the wrapped iterator until the filter
> accepts an element. If that does not end with an accepted element, {{next()}}
> fails, but the permission to remove from the previous successful {{next()}}
> is kept, while the wrapped iterator is now on another element. A {{remove()}}
> then removes that element, which {{next()}} never returned:
> {code:java}
> List<Integer> list = new ArrayList<>(List.of(1, 2));
> FilterIterator<Integer> it = new FilterIterator<>(list.iterator(), n -> n ==
> 1);
> it.next(); // 1
> it.next(); // looks at 2, rejects it, throws NoSuchElementException
> it.remove(); // removes 2; list is now [1]
> {code}
> The same happens when the filter throws while it looks at the next element,
> and when the elements left are null (they are skipped). The javadoc of
> {{remove()}} says it removes the last element returned by {{next()}}.
> Found by an OpenJML/JML verification pilot of the {{FilterIterator}} contract
> (the removal-safety condition failed on the original source and holds with
> the change below), then reproduced with plain JUnit tests.
> *Proposal*
> * In {{checkNext()}}, set {{canRemove = false}} right before each
> {{it.next()}}: once the wrapped iterator moves, the element returned last can
> no longer be removed. A successful {{next()}} sets it again. A {{next()}}
> that fails at the end of the wrapped iterator, without moving it, keeps the
> element returned before removable (as a list iterator does).
> * Tests: {{NoSuchElementException}} after a rejected tail, a throwing filter,
> a skipped null tail, and controls (end of the wrapped iterator, {{hasNext()}}
> before the failed {{next()}}).
> * Fold one paragraph into the existing 4.24 upgrade guide entry of
> CAMEL-26290.
> _Filed with Claude Code on behalf of allthingssecurity._
--
This message was sent by Atlassian Jira
(v10.3.26#10030026)
