Denis Merigoux denismerigoux
This file contains hidden or 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
| diff --git a/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst b/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst | |
| index e63032e..f0bc332 100644 | |
| --- a/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst | |
| +++ b/code/experimental/ed25519/Hacl.Impl.Ed25519.SecretExpand.fst | |
| @@ -10,10 +10,11 @@ val secret_expand: | |
| expanded:lbuffer uint8 64ul | |
| -> secret:lbuffer uint8 32ul -> | |
| Stack unit | |
| - (requires fun h -> live h expanded /\ live h secret) | |
| + (requires fun h -> live h expanded /\ live h secret /\ disjoint expanded secret) |
denismerigoux
/ example
Created
August 8, 2017 22:54
Example of ebb splitting that lead to differences in Ebb postorder
This file contains hidden or 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
| base_func { | |
| ebb0: | |
| brz ebb1 | |
| jump ebb2 | |
| ebb1: | |
| brz ebb3 | |
| jump ebb3 | |
| ebb2: | |
| jump ebb3 | |
| ebb3: |
denismerigoux
/ Loop statistics
Last active
August 9, 2017 21:57
Diverse Cretonne stats for translated WASM modules
This file contains hidden or 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
| Setup: the modules are translated into Cretonne IL using wasm2cretonne and the dummy runtime, | |
| then a full-fledge context is created (cfg, dominator tree, loop analysis) and the LICM pass | |
| is run. | |
| ===== cv-wasm.wasm ========== | |
| Loops: 16,978 | |
| Ebbs partially in a loop: 13,229 | |
| Ebb entirely in loop: 64,909 | |
| Ebb total: 162,640 | |
| Splits during analysis: 8 |
denismerigoux
/ int_exprs.wast.0.cton
Created
June 19, 2017 23:35
First translation from wasm to Cretonne IL
This file contains hidden or 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
| function %(i32, i32) -> i32 { | |
| ebb0(v0: i32, v1: i32): | |
| v2 = iconst.i32 1 | |
| v3 = iadd v2, v0 | |
| v4 = iconst.i32 1 | |
| v5 = iadd v4, v1 | |
| v6 = icmp slt v5, v3 | |
| v7 = sextend.i32 v6 | |
| return v7 | |
| } |
denismerigoux
/ gist:1f9659985ef09a7596b1b656dd8c1b65
Created
June 8, 2017 21:41
Effect of early sealing
This file contains hidden or 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
| // When sealing ebb1 before creating the v4 instruction | |
| function ""() { | |
| ebb0: | |
| v0 = iconst.i32 1 | |
| v1 = iconst.i32 2 | |
| v2 = iadd v0, v1 | |
| brnz v1, ebb1 | |
| v3 = iadd v0, v2 | |
| ebb1: |
NewerOlder