From 4441785fb44b88bb6943ddbf639d872c8c903281 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 16 Jan 2019 00:24:19 -0500 Subject: Constant-propogate 0+x and x+0 after bounds After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m22.67s | Total | 21m28.24s || -0m05.56s | -0.43% -------------------------------------------------------------------------------------------- 4m09.95s | PushButtonSynthesis.vo | 4m14.76s || -0m04.81s | -1.88% 3m07.95s | p384_32.c | 3m11.17s || -0m03.21s | -1.68% 2m06.43s | Rewriter.vo | 2m06.15s || +0m00.28s | +0.22% 1m55.83s | RewriterWf2.vo | 1m56.15s || -0m00.32s | -0.27% 1m52.36s | RewriterRulesGood.vo | 1m52.34s || +0m00.01s | +0.01% 1m46.52s | RewriterRulesInterpGood.vo | 1m45.70s || +0m00.82s | +0.77% 0m46.56s | RewriterInterpProofs1.vo | 0m46.72s || -0m00.15s | -0.34% 0m45.04s | ExtractionHaskell/word_by_word_montgomery | 0m45.33s || -0m00.28s | -0.63% 0m39.17s | p521_32.c | 0m39.07s || +0m00.10s | +0.25% 0m32.40s | p521_64.c | 0m32.64s || -0m00.24s | -0.73% 0m31.13s | ExtractionHaskell/unsaturated_solinas | 0m30.88s || +0m00.25s | +0.80% 0m24.20s | ExtractionHaskell/saturated_solinas | 0m24.27s || -0m00.07s | -0.28% 0m23.72s | RewriterWf1.vo | 0m23.42s || +0m00.29s | +1.28% 0m17.52s | ExtractionOCaml/word_by_word_montgomery | 0m17.10s || +0m00.41s | +2.45% 0m13.39s | secp256k1_32.c | 0m13.29s || +0m00.10s | +0.75% 0m13.08s | p256_32.c | 0m13.26s || -0m00.17s | -1.35% 0m11.49s | p484_64.c | 0m11.18s || +0m00.31s | +2.77% 0m10.68s | ExtractionOCaml/unsaturated_solinas | 0m10.64s || +0m00.03s | +0.37% 0m10.11s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.10s || +0m00.00s | +0.09% 0m07.96s | ExtractionOCaml/saturated_solinas | 0m07.95s || +0m00.00s | +0.12% 0m06.81s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.76s || +0m00.04s | +0.73% 0m06.30s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.26s || +0m00.04s | +0.63% 0m06.07s | p224_32.c | 0m05.94s || +0m00.12s | +2.18% 0m06.06s | BoundsPipeline.vo | 0m06.08s || -0m00.02s | -0.32% 0m05.46s | p384_64.c | 0m05.30s || +0m00.16s | +3.01% 0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.18s || +0m00.10s | +1.93% 0m04.97s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.99s || -0m00.02s | -0.40% 0m04.13s | ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.03s | +0.73% 0m02.34s | curve25519_32.c | 0m02.21s || +0m00.12s | +5.88% 0m01.59s | curve25519_64.c | 0m01.47s || +0m00.12s | +8.16% 0m01.46s | CLI.vo | 0m01.48s || -0m00.02s | -1.35% 0m01.15s | secp256k1_64.c | 0m01.03s || +0m00.11s | +11.65% 0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88% 0m01.14s | StandaloneHaskellMain.vo | 0m01.09s || +0m00.04s | +4.58% 0m01.14s | StandaloneOCamlMain.vo | 0m01.12s || +0m00.01s | +1.78% 0m01.09s | p256_64.c | 0m00.98s || +0m00.11s | +11.22% 0m01.06s | p224_64.c | 0m01.00s || +0m00.06s | +6.00% --- src/arith_with_casts_rewrite_head.out | 123 +++++++++++++++++++++++++++++++++- 1 file changed, 121 insertions(+), 2 deletions(-) (limited to 'src/arith_with_casts_rewrite_head.out') diff --git a/src/arith_with_casts_rewrite_head.out b/src/arith_with_casts_rewrite_head.out index 053110d89..a179fff11 100644 --- a/src/arith_with_casts_rewrite_head.out +++ b/src/arith_with_casts_rewrite_head.out @@ -949,6 +949,126 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with else None | None => None end + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t1 idc1) x2) => + args <- invert_bind_args idc1 Raw.ident.Z_cast; + args0 <- invert_bind_args idc0 Raw.ident.Literal; + _ <- invert_bind_args idc Raw.ident.Z_add; + match + pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype + ((projT1 args0) -> s1)%ptype option (fun x3 : option => x3) + with + | Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + ((projT1 args0) -> s1)%ptype + then + xv <- ident.unify pattern.ident.Literal ##(projT2 args0); + v <- type.try_make_transport_cps s1 ℤ; + fv <- (x3 <- (if + ((let (x3, _) := xv in x3) =? 0) && + (ZRange.normalize args <=? + ZRange.normalize range)%zrange + then + Some + (#(Z_cast args)%expr @ + v (Compile.reflect x2))%expr_pat + else None); + Some (Base x3)); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) (@expr.App _ _ _ s1 _ ($_)%expr _) | + @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) + (@expr.App _ _ _ s1 _ (@expr.Abs _ _ _ _ _ _) _) | @expr.App _ _ _ s + _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) + (@expr.App _ _ _ s1 _ (_ @ _)%expr_pat _) | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) + (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _) => None + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) #(_)%expr_pat | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) ($_)%expr | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) (@expr.Abs _ _ _ _ _ _) | @expr.App _ + _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) (@expr.LetIn _ _ _ _ _ _ _) => None + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) + (@expr.Ident _ _ _ t1 idc1) => + args <- invert_bind_args idc1 Raw.ident.Literal; + args0 <- invert_bind_args idc0 Raw.ident.Z_cast; + _ <- invert_bind_args idc Raw.ident.Z_add; + match + pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype + (s1 -> (projT1 args))%ptype option (fun x3 : option => x3) + with + | Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (s1 -> (projT1 args))%ptype + then + v <- type.try_make_transport_cps s1 ℤ; + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + fv <- (x3 <- (if + ((let (x3, _) := xv in x3) =? 0) && + (ZRange.normalize args0 <=? + ZRange.normalize range)%zrange + then + Some + (#(Z_cast args0)%expr @ + v (Compile.reflect x2))%expr_pat + else None); + Some (Base x3)); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) ($_)%expr | + @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) + (@expr.Abs _ _ _ _ _ _) | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) + (_ @ _)%expr_pat | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) + (@expr.LetIn _ _ _ _ _ _ _) => None + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ ($_)%expr _)) _ | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Abs _ _ _ _ _ _) _)) _ | @expr.App _ _ + _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (_ @ _)%expr_pat _)) _ | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _)) _ => None + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) ($_)%expr) _ | + @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Abs _ _ _ _ _ _)) _ | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.LetIn _ _ _ _ _ _ _)) _ => None | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t idc) x2) x1) x0 => @@ -985,8 +1105,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _) _) _ => None - | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ #(_)%expr_pat _) _ | - @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App + | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => None -- cgit v1.2.3