diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-10 20:52:21 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-08-10 21:46:31 -0400 |
| commit | fe67ae4b75b17cd3190ec72a7fa1135466ab62e6 (patch) | |
| tree | c624782a53b0f8e03818f6aa7900dd2dee07db48 /_CoqProject | |
| parent | 6d564bd34d1a48fab192e1a4ad16ab8606ac2507 (diff) | |
Don't guarantee anything about casting outside of range
We used to claim that casts brought values into the intersection of the
known range and the casted range. This is absurd, in the same way that
it's absurd to claim that attempting to dereference a pointer guarantees
that it's non-null. Instead, we pass through bounds that fit soundly
within the casted range, and otherwise guarantee nothing about the
bounds of the resulting code.
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
17m52.74s | Total | 17m53.29s || -0m00.55s | -0.05%
--------------------------------------------------------------------------------------------------------------------
4m33.01s | Experiments/NewPipeline/Toplevel1 | 4m31.90s || +0m01.11s | +0.40%
5m55.30s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m55.05s || +0m00.25s | +0.07%
1m36.16s | Experiments/NewPipeline/Toplevel2 | 1m35.88s || +0m00.28s | +0.29%
0m38.71s | Experiments/NewPipeline/AbstractInterpretationWf | 0m39.10s || -0m00.39s | -0.99%
0m38.52s | p521_32.c | 0m39.13s || -0m00.60s | -1.55%
0m37.12s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m37.32s || -0m00.20s | -0.53%
0m34.93s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m34.65s || +0m00.28s | +0.80%
0m32.10s | p521_64.c | 0m32.70s || -0m00.60s | -1.83%
0m23.76s | p384_32.c | 0m23.69s || +0m00.07s | +0.29%
0m20.25s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m20.70s || -0m00.44s | -2.17%
0m18.64s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m18.99s || -0m00.34s | -1.84%
0m13.72s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m13.78s || -0m00.05s | -0.43%
0m12.55s | Experiments/NewPipeline/CStringification | 0m12.58s || -0m00.02s | -0.23%
0m10.42s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m10.56s || -0m00.14s | -1.32%
0m08.64s | p384_64.c | 0m08.44s || +0m00.20s | +2.36%
0m08.59s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.51s || +0m00.08s | +0.94%
0m05.52s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.32s || +0m00.19s | +3.75%
0m05.34s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.47s || -0m00.12s | -2.37%
0m04.04s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m04.02s || +0m00.02s | +0.49%
0m04.00s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m03.84s || +0m00.16s | +4.16%
0m03.99s | secp256k1_32.c | 0m03.82s || +0m00.17s | +4.45%
0m03.89s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.02s || -0m00.12s | -3.23%
0m03.81s | p256_32.c | 0m03.83s || -0m00.02s | -0.52%
0m03.21s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.30s || -0m00.08s | -2.72%
0m02.14s | p224_32.c | 0m02.26s || -0m00.11s | -5.30%
0m02.11s | curve25519_32.c | 0m02.09s || +0m00.02s | +0.95%
0m01.73s | p224_64.c | 0m01.54s || +0m00.18s | +12.33%
0m01.66s | secp256k1_64.c | 0m01.64s || +0m00.02s | +1.21%
0m01.58s | p256_64.c | 0m01.68s || -0m00.09s | -5.95%
0m01.38s | curve25519_64.c | 0m01.47s || -0m00.09s | -6.12%
0m01.37s | Experiments/NewPipeline/CLI | 0m01.45s || -0m00.07s | -5.51%
0m01.25s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.20s || +0m00.05s | +4.16%
0m01.21s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.28s || -0m00.07s | -5.46%
0m01.06s | Experiments/NewPipeline/CompilersTestCases | 0m01.07s || -0m00.01s | -0.93%
0m01.04s | Experiments/NewPipeline/AbstractInterpretation | 0m01.02s || +0m00.02s | +1.96%
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions