From c6364f2c5eae7e86e9e0a40548d427f3afc66799 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 17 Jun 2017 17:21:21 -0400 Subject: Add extra simplification to simplifier for adc --- src/Compilers/Z/ArithmeticSimplifier.v | 100 ++++++++++++++++++++------- src/Compilers/Z/ArithmeticSimplifierInterp.v | 20 +++++- 2 files changed, 95 insertions(+), 25 deletions(-) diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v index a43f963c1..a0dc75bf5 100644 --- a/src/Compilers/Z/ArithmeticSimplifier.v +++ b/src/Compilers/Z/ArithmeticSimplifier.v @@ -299,31 +299,47 @@ Section language. end | AddWithCarry TZ TZ TZ TZ as opc => fun args - => if convert_adc_to_sbb - then match interp_as_expr_or_const args with - | Some (const_of c, const_of x, const_of y) - => Op (OpConst (interp_op _ _ opc (c, x, y))) TT - | Some (c, gen_expr x, y) - => let y' := match y with - | const_of y => if (y Some y - | gen_expr _ => None - end in - match y' with - | Some y => Op (SubWithBorrow TZ TZ TZ TZ) - (match c with - | const_of c => Op (OpConst (-c)) TT - | neg_expr c => c - | gen_expr c => Op (Opp TZ TZ) c - end, - x, y)%expr - | None => Op opc args + => let first_pass + := match interp_as_expr_or_const args with + | Some (const_of c, const_of x, const_of y) + => Some (Op (OpConst (interp_op _ _ opc (c, x, y))) TT) + | Some (gen_expr e, const_of c1, const_of c2) + | Some (const_of c1, gen_expr e, const_of c2) + | Some (const_of c1, const_of c2, gen_expr e) + => if (c1 + c2 =? 0)%Z + then Some e + else None + | _ => None + end in + match first_pass with + | Some e => e + | None + => if convert_adc_to_sbb + then match interp_as_expr_or_const args with + | Some (const_of c, const_of x, const_of y) + => Op (OpConst (interp_op _ _ opc (c, x, y))) TT + | Some (c, gen_expr x, y) + => let y' := match y with + | const_of y => if (y Some y + | gen_expr _ => None + end in + match y' with + | Some y => Op (SubWithBorrow TZ TZ TZ TZ) + (match c with + | const_of c => Op (OpConst (-c)) TT + | neg_expr c => c + | gen_expr c => Op (Opp TZ TZ) c + end, + x, y)%expr + | None => Op opc args + end + | _ => Op opc args end - | _ => Op opc args - end - else Op opc args + else Op opc args + end | AddWithGetCarry bw TZ TZ TZ TZ TZ as opc => fun args => if convert_adc_to_sbb @@ -353,6 +369,42 @@ Section language. | _ => Op opc args end else Op opc args + | AddWithGetCarry bw (TWord bw1 as T1) (TWord bw2 as T2) (TWord bw3 as T3) (TWord bwout as Tout) Tout2 as opc + => fun args + => match interp_as_expr_or_const args with + | Some (const_of c, const_of x, const_of y) + => if ((c =? 0) && (x =? 0) && (y =? 0))%Z%bool + then Pair (Op (OpConst 0) TT) (Op (OpConst 0) TT) + else Op opc args + | Some (gen_expr e, const_of c1, const_of c2) + => match base_type_eq_semidec_transparent T1 Tout with + | Some pf + => if ((c1 =? 0) && (c2 =? 0) && (2^Z.of_nat bw1 <=? bw))%Z%bool + then Pair (eq_rect _ (fun t => exprf (Tbase t)) e _ pf) (Op (OpConst 0) TT) + else Op opc args + | None + => Op opc args + end + | Some (const_of c1, gen_expr e, const_of c2) + => match base_type_eq_semidec_transparent T2 Tout with + | Some pf + => if ((c1 =? 0) && (c2 =? 0) && (2^Z.of_nat bw2 <=? bw))%Z%bool + then Pair (eq_rect _ (fun t => exprf (Tbase t)) e _ pf) (Op (OpConst 0) TT) + else Op opc args + | None + => Op opc args + end + | Some (const_of c1, const_of c2, gen_expr e) + => match base_type_eq_semidec_transparent T3 Tout with + | Some pf + => if ((c1 =? 0) && (c2 =? 0) && (2^Z.of_nat bw3 <=? bw))%Z%bool + then Pair (eq_rect _ (fun t => exprf (Tbase t)) e _ pf) (Op (OpConst 0) TT) + else Op opc args + | None + => Op opc args + end + | _ => Op opc args + end | SubWithBorrow 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 8314b991e..e736f2631 100644 --- a/src/Compilers/Z/ArithmeticSimplifierInterp.v +++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v @@ -45,6 +45,16 @@ Local Ltac break_t_step := | progress break_innermost_match_step | progress break_match_hyps ]. +Local Ltac solve_word_small _ := + lazymatch goal with + | [ H : (2^Z.of_nat ?b <= ?bw)%Z |- (0 <= FixedWordSizes.wordToZ ?x < 2^?bw)%Z ] + => cut (0 <= FixedWordSizes.wordToZ x < 2^(Z.of_nat (2^b)%nat))%Z; + [ rewrite Z.pow_Zpow; cbn [Z.of_nat Pos.of_succ_nat Pos.succ]; + assert ((2^2^Z.of_nat b <= 2^bw)%Z) by auto with zarith; + auto with zarith + | apply FixedWordSizesEquality.wordToZ_range ] + end. + Definition interpf_as_expr_or_const {t} : interp_flat_type (@inverted_expr interp_base_type) t -> interp_flat_type interp_base_type t := SmartVarfMap @@ -118,6 +128,7 @@ Proof. | progress cbv [LetIn.Let_In Z.zselect IdfunWithAlt.id_with_alt] | progress subst | progress simpl in * + | progress Bool.split_andb | progress Z.ltb_to_lt | break_innermost_match_step | rewrite FixedWordSizesEquality.ZToWord_wordToZ @@ -127,7 +138,14 @@ Proof. | rewrite !Z.sub_with_borrow_to_add_get_carry | progress autorewrite with zsimplify_fast | progress cbv [cast_const ZToInterp interpToZ] - | nia ]. + | nia + | progress cbv [Z.add_with_carry] + | match goal with + | [ |- context[(?x mod ?m)%Z] ] + => rewrite (Z.mod_small x m) by solve_word_small () + | [ |- context[(?x / ?m)%Z] ] + => rewrite (Z.div_small x m) by solve_word_small () + end ]. Qed. Hint Rewrite @InterpSimplifyArith : reflective_interp. -- cgit v1.2.3