diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-20 22:38:59 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-20 22:38:59 -0400 |
| commit | eb26511aeebef91592e36813ba8e2796107990f5 (patch) | |
| tree | 60ced0a2cb5defbe66e2aeea9aac9ccb7f739f4b | |
| parent | 3cbfa40974ce0c90ec73df532496b5ea9156ed2b (diff) | |
Also key adc->sbb on the carry-bit being negative
This is needed when we're subtracting 0 >.>
| -rw-r--r-- | src/Compilers/Z/ArithmeticSimplifier.v | 36 |
1 files changed, 26 insertions, 10 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v index 8f5ca7c9e..6cafa3230 100644 --- a/src/Compilers/Z/ArithmeticSimplifier.v +++ b/src/Compilers/Z/ArithmeticSimplifier.v @@ -419,16 +419,32 @@ Section language. | neg_expr y => Some y | gen_expr _ => None end in - match y' with - | Some y => LetIn (Op (SubWithGetBorrow bw TZ 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) - (fun '(v, c) => (Var v, Op (Opp TZ TZ) (Var c))%expr) - | None => Op opc args + let c' := match c with + | const_of c => if (c <? 0)%Z + then Some (Op (OpConst (-c)) TT) + else None + | neg_expr c => Some c + | gen_expr _ => None + end in + match c', y' with + | _, Some y => LetIn (Op (SubWithGetBorrow bw TZ 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) + (fun '(v, c) => (Var v, Op (Opp TZ TZ) (Var c))%expr) + | Some c, _ => LetIn (Op (SubWithGetBorrow bw TZ TZ TZ TZ TZ) + (c, + x, + match y with + | const_of y => Op (OpConst (-y)) TT + | neg_expr y => y + | gen_expr y => Op (Opp TZ TZ) y + end)%expr) + (fun '(v, c) => (Var v, Op (Opp TZ TZ) (Var c))%expr) + | None, None => Op opc args end | _ => Op opc args end |