Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Cmov using sbb when possible #1596

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Cmov using sbb when possible #1596

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion src/Rewriter/Rules.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -395,6 +395,13 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list (
y ∈ ry -> y = Z.ones (Z.succ (Z.log2 y))
-> cstZ rv (cstZ ry ('y) &' cstZ rx x) = cstZ rx x)
]%Z%zrange
; mymap
do_again
[ (forall c M rv r0 rM, 0 ∈ r0 -> M ∈ rM -> M ∈ rv -> 2^Z.log2 (M+1) = M + 1 -> 1 <= M ->
cstZ rv (Z.zselect (cstZ r[0~>1] c) (cstZ r0 ('0)) (cstZ rM ('M)))
= (dlet vc := cstZZ rv r[0~>1] (Z.sub_with_get_borrow_full ('(M+1)) (cstZ r[0~>1] c) 0 0) in
cstZ rv (fst vc)))
]
; mymap
do_again
[ (* [do_again], so that we can trigger add/sub rules on the output *)
Expand Down Expand Up @@ -1213,7 +1220,8 @@ Section with_bitwidth.
:= Eval cbv [myapp mymap myflatten] in
mymap
dont_do_again
[(* no-op rule to prevent firing on selects between 0 and mask (since
[
(* no-op rule to prevent firing on selects between 0 and mask (since
these can be succinctly expressed as 0-c *)
(forall rc c,
singlewidth (Z.zselect (cstZ rc c)
Expand Down
5 changes: 5 additions & 0 deletions src/Rewriter/RulesProofs.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -571,6 +571,11 @@ Proof using Type.
all: repeat interp_good_t_step_arith.
all: remove_casts; try fin_with_nia.
all: try (reflect_hyps; lia).

{ (* cmov c 0 -1 -> sbb 0 0 c *)
enough (- c mod (M + 1) = M) as E by (rewrite E; remove_casts; trivial).
match goal with H5 : _ |- _ => apply unfold_is_bounded_by_bool in H5; cbn in H5 end.
rewrite Z.mod_opp_l_nz; rewrite ?Z.mod_small; nia. }
Qed.

Lemma strip_literal_casts_rewrite_rules_proofs
Expand Down