-
Notifications
You must be signed in to change notification settings - Fork 56
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Improve speed in MessageDigest and Hmac #54
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -193,7 +193,7 @@ public static interface StateSupplier<S> extends Supplier<S> { | |
//@ public invariant bufferStateConsistent(bufferState, firstData); | ||
|
||
//@ normal_behavior | ||
//@ requires 0 <= capacity; | ||
//@ requires 0 < capacity; | ||
//@ ensures bytesReceived == 0; | ||
//@ ensures bytesProcessed == 0; | ||
//@ ensures bufferState == BufferState.Uninitialized; | ||
|
@@ -203,8 +203,8 @@ public static interface StateSupplier<S> extends Supplier<S> { | |
//@ signals_only IllegalArgumentException; | ||
//@ pure | ||
InputBuffer(final int capacity) { | ||
if (capacity < 0) { | ||
throw new IllegalArgumentException("Capacity must be non-negative"); | ||
if (capacity <= 0) { | ||
throw new IllegalArgumentException("Capacity must be positive"); | ||
} | ||
//@ set bufferState = BufferState.Uninitialized; | ||
buff = new AccessibleByteArrayOutputStream(0, capacity); | ||
|
@@ -379,6 +379,49 @@ private boolean fillBuffer(final byte[] arr, final int offset, final int length) | |
return true; | ||
} | ||
|
||
/*@ private normal_behavior | ||
@ requires canTakeData(bufferState); | ||
@ {| | ||
@ requires buffSize - buff.count >= 1; | ||
@ assignable buff.count, bytesReceived, bufferState; | ||
@ ensures \result; | ||
@ ensures bytesReceived == \old(bytesReceived) + 1; | ||
@ ensures buff.count == \old(buff.count) + 1; | ||
@ ensures \old(bufferState) == BufferState.Ready | ||
@ ==> bufferState == BufferState.DataIn; | ||
@ ensures \old(bufferState) != BufferState.Ready | ||
@ ==> bufferState == \old(bufferState); | ||
@ also | ||
@ requires buffSize - buff.count < 1; | ||
@ assignable \nothing; | ||
@ ensures !\result; | ||
@ |} | ||
@ also | ||
@ private exceptional_behavior | ||
@ requires buff.count <= buffSize - 1; | ||
@ assignable \nothing; | ||
@ signals_only ArrayIndexOutOfBoundsException; | ||
@*/ | ||
/** | ||
* Copies all requested data from {@code arr} into {@link #buff} if an only if there is | ||
SalusaSecondus marked this conversation as resolved.
Show resolved
Hide resolved
|
||
* sufficient space. Returns {@code true} if the data was copied. | ||
* @return {@code true} if there was sufficient space in the buffer and data was copied. | ||
*/ | ||
private boolean fillBuffer(final byte val) { | ||
// Overflow safe comparison. | ||
if (buffSize - buff.size() < 1) { | ||
return false; | ||
} | ||
try { | ||
buff.write(val); | ||
} catch (IndexOutOfBoundsException ex) { | ||
throw new ArrayIndexOutOfBoundsException(ex.toString()); | ||
} | ||
//@ set bytesReceived = bytesReceived + 1; | ||
//@ set bufferState = (bufferState == BufferState.Ready) ? BufferState.DataIn : bufferState; | ||
return true; | ||
} | ||
|
||
/*@ private normal_behavior | ||
@ old int length = src.remaining(); | ||
@ requires canTakeData(bufferState); | ||
|
@@ -564,6 +607,32 @@ public void update(final byte[] src, final int offset, final int length) { | |
//@ set bytesReceived = bytesReceived + length; | ||
} | ||
|
||
/*@ public normal_behavior | ||
@ requires canTakeData(bufferState); | ||
@ requires arrayUpdater != null; | ||
@ assignable state, state.*, buff.count, firstData, bytesProcessed, | ||
@ bytesReceived, bufferState; | ||
@ ensures bytesReceived == \old(bytesReceived) + 1; | ||
@ ensures canTakeData(bufferState); | ||
@ also | ||
@ public exceptional_behavior | ||
@ requires buff.count <= buffSize - 1; | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why are we throwing exceptions when the buffer count is within the buffer size? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is not Java exceptions but for the formal verification. The listed line requires that the buffer count be valid. |
||
@ assignable \nothing; | ||
@ signals_only ArrayIndexOutOfBoundsException; | ||
@*/ | ||
public void update(final byte val) { | ||
if (fillBuffer(val)) { | ||
return; | ||
} | ||
processBuffer(false); | ||
if (fillBuffer(val)) { | ||
return; | ||
} | ||
|
||
// We explicitly do not support capacities of zero where we cannot even append a single byte. | ||
throw new AssertionError("Unreachable code. Cannot buffer even a single byte"); | ||
} | ||
|
||
//@ public normal_behavior | ||
//@ requires canTakeData(bufferState); | ||
//@ requires arrayUpdater != null && finalHandler != null; | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm a little confused by this. The behavior here is not documented in the javadoc (which appears to have been copied from a different function) and doesn't really make sense to me either; in particular, this appears to be an equivalent condition (modulo overflow) to the one on 385.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These are for formal proofs of correctness. It has been slightly modified to take into account the hard coded length (of 1). We do not currently have this system running, but I'm avoiding bit-rot.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we know if these proofs are correct? The requires conditions seem to overlap to me, unless I'm missing something.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
They were and we need to figure out how to reenable running of them. They have have drifted even separate from this PR. I'm trying to keep them as close to correct as possible.