aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-24 23:46:11 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-24 23:46:11 -0400
commitecff47dbc867261b81c6e268eca99e5b5ab28805 (patch)
tree5d57a76fcdbda8c763a84c5a8a4ec304a566e35a /src
parented4cb80a00f5f198e7fab3b7fbbbb531dc2bc91e (diff)
Convert adc to sbb when doing [0 - x]
Diffstat (limited to 'src')
-rw-r--r--src/Compilers/Z/ArithmeticSimplifier.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v
index 24072dc71..771a82de4 100644
--- a/src/Compilers/Z/ArithmeticSimplifier.v
+++ b/src/Compilers/Z/ArithmeticSimplifier.v
@@ -415,14 +415,14 @@ Section language.
(Op (OpConst v) TT, Op (OpConst c) TT)%expr
| Some (c, gen_expr x, y)
=> let y' := match y with
- | const_of y => if (y <? 0)%Z
+ | const_of y => if (y <=? 0)%Z
then Some (Op (OpConst (-y)) TT)
else None
| neg_expr y => Some y
| gen_expr _ => None
end in
let c' := match c with
- | const_of c => if (c <? 0)%Z
+ | const_of c => if (c <=? 0)%Z
then Some (Op (OpConst (-c)) TT)
else None
| neg_expr c => Some c