search

aws / aws-database-encryption-sdk-dynamodb

AWS Database Encryption SDK for DynamoDB in Java
Apache License 2.0
20 stars 11 forks source link

feat: Optimize sort by `Below` #1457

Open seebees opened 3 weeks ago

seebees commented 3 weeks ago

The Below function is in the hot path. The slice (x[1..]) operation is not optimized in Dafny. This optimizes this function by turning the recursive slice into a loop over an index into the seq. Further, a bounded integer version is also included.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

texastony commented 3 weeks ago

Dafny Verifier crashed on 4dfd05d:

2024-10-22T20:11:35.9801750Z Fatal error. System.AccessViolationException: Attempted to read or write protected memory. This is often an indication that other memory is corrupt.
2024-10-22T20:11:35.9811410Z    at Microsoft.Boogie.ReadOnlyVisitor.Visit(Microsoft.Boogie.Absy)
2024-10-22T20:11:35.9824210Z    at Microsoft.Boogie.ReadOnlyVisitor.VisitDeclarationList(System.Collections.Generic.List`1<Microsoft.Boogie.Declaration>)
2024-10-22T20:11:35.9828510Z    at Microsoft.Boogie.ReadOnlyVisitor.VisitProgram(Microsoft.Boogie.Program)
2024-10-22T20:11:35.9832780Z    at Microsoft.Boogie.BasicTypeVisitor..ctor(Microsoft.Boogie.Absy)
2024-10-22T20:11:35.9843010Z    at Microsoft.Boogie.Checker.Target(Microsoft.Boogie.Program, Microsoft.Boogie.ProverContext, VC.Split)
2024-10-22T20:11:35.9846800Z    at VC.CheckerPool.PrepareChecker(Microsoft.Boogie.Program, VC.Split, Microsoft.Boogie.Checker)
2024-10-22T20:11:35.9849590Z    at VC.CheckerPool+<FindCheckerFor>d__7.MoveNext()
2024-10-22T20:11:35.9852360Z    at System.Threading.ExecutionContext.RunFromThreadPoolDispatchLoop(System.Threading.Thread, System.Threading.ExecutionContext, System.Threading.ContextCallback, System.Object)
2024-10-22T20:11:35.9861690Z    at System.Runtime.CompilerServices.AsyncTaskMethodBuilder`1+AsyncStateMachineBox`1[[System.__Canon, System.Private.CoreLib, Version=6.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[VC.CheckerPool+<FindCheckerFor>d__7, Boogie.VCGeneration, Version=3.2.3.0, Culture=neutral, PublicKeyToken=null]].MoveNext(System.Threading.Thread)
2024-10-22T20:11:35.9877740Z    at System.Threading.ThreadPoolWorkQueue.Dispatch()
2024-10-22T20:11:35.9880970Z    at System.Threading.PortableThreadPool+WorkerThread.WorkerThreadStart()
2024-10-22T20:11:35.9885100Z    at System.Threading.Thread.StartCallback()
2024-10-22T20:11:36.1982370Z make: *** [verify_service] Abort trap: 6
2024-10-22T20:11:36.3739850Z ##[error]Process completed with exit code 2.