From f9b611c43c4ef7202a275188886c1bc4158c0710 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 20 May 2017 00:08:13 -0400 Subject: Add compiler optimization for [Zselect (-x) _ _] Since x = 0 <-> -x = 0, we can eliminate the negative on the borrow-bit in freeze. After | File Name | Before || Change -------------------------------------------------------------------------------- 5m01.81s | Total | 4m55.75s || +0m06.05s -------------------------------------------------------------------------------- 0m29.05s | Compilers/Z/ArithmeticSimplifierInterp | 0m24.85s || +0m04.19s 0m28.68s | Compilers/Z/ArithmeticSimplifierWf | 0m25.88s || +0m02.80s 2m18.19s | Specific/IntegrationTestLadderstep | 2m19.51s || -0m01.31s 0m53.86s | Specific/IntegrationTestLadderstep130 | 0m53.64s || +0m00.21s 0m15.40s | Specific/IntegrationTestFreeze | 0m15.30s || +0m00.09s 0m11.85s | Specific/IntegrationTestMul | 0m11.72s || +0m00.12s 0m10.72s | Specific/IntegrationTestSub | 0m10.47s || +0m00.25s 0m08.97s | Specific/IntegrationTestSquare | 0m09.15s || -0m00.17s 0m02.78s | Compilers/Z/Bounds/Pipeline/Definition | 0m02.81s || -0m00.03s 0m00.75s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.75s || +0m00.00s 0m00.60s | Compilers/Z/Bounds/Pipeline | 0m00.62s || -0m00.02s 0m00.60s | Compilers/Z/ArithmeticSimplifier | 0m00.65s || -0m00.05s 0m00.36s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.41s || -0m00.04s --- src/Compilers/Z/ArithmeticSimplifier.v | 34 ++++++++++++++++++++++++++++ src/Compilers/Z/ArithmeticSimplifierInterp.v | 5 ++-- 2 files changed, 37 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v index 8f63e815b..a1775011d 100644 --- a/src/Compilers/Z/ArithmeticSimplifier.v +++ b/src/Compilers/Z/ArithmeticSimplifier.v @@ -48,6 +48,19 @@ Section language. end end. + Fixpoint uninterp_expr_or_const {t} : interp_flat_type inverted_expr t -> exprf (var:=var) t + := match t with + | Tbase T => fun e => match e with + | const_of v => Op (OpConst v) TT + | gen_expr e => e + | neg_expr e => Op (Opp _ _) e + end + | Unit => fun _ => TT + | Prod A B => fun (ab : interp_flat_type _ A * interp_flat_type _ B) + => Pair (@uninterp_expr_or_const A (fst ab)) + (@uninterp_expr_or_const B (snd ab)) + end. + Definition simplify_op_expr {src dst} (opc : op src dst) : exprf (var:=var) src -> exprf (var:=var) dst := match opc in op src dst return exprf src -> exprf dst with @@ -177,6 +190,27 @@ Section language. | _ => Op opc args end + | Zselect TZ TZ TZ TZ as opc + => fun args + => match interp_as_expr_or_const args with + | Some (const_of c, x, y) + => match (c =? 0)%Z, x, y with + | true, const_of c, _ + | false, _, const_of c + => Op (OpConst c) TT + | true, gen_expr e, _ + | false, _, gen_expr e + => e + | true, neg_expr e, _ + | false, _, neg_expr e + => Op (Opp TZ TZ) e + end + | Some (neg_expr e, x, y) + => let x := uninterp_expr_or_const (t:=Tbase _) x in + let y := uninterp_expr_or_const (t:=Tbase _) y in + Op (Zselect TZ TZ TZ TZ) (e, x, y)%expr + | _ => Op opc args + end | AddWithCarry TZ TZ TZ TZ as opc => fun args => if convert_adc_to_sbb diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v index 3dc11aa9e..6db34f1b8 100644 --- a/src/Compilers/Z/ArithmeticSimplifierInterp.v +++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v @@ -151,7 +151,7 @@ Proof. apply InterpRewriteOp; intros; unfold simplify_op_expr. break_innermost_match; repeat first [ fin_t - | progress cbv [LetIn.Let_In] + | progress cbv [LetIn.Let_In Z.zselect] | progress simpl in * | progress subst | progress subst_prod @@ -162,7 +162,8 @@ Proof. | progress Z.ltb_to_lt | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r | rewrite !Z.sub_with_borrow_to_add_get_carry - | progress autorewrite with zsimplify_fast ]. + | progress autorewrite with zsimplify_fast + | break_innermost_match_step ]. Qed. Hint Rewrite @InterpSimplifyArith : reflective_interp. -- cgit v1.2.3