From a8692a11f5c064e8f72741e506b836c47c95a324 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 24 Mar 2022 11:14:25 -0700 Subject: [PATCH] Fix precondition of `conditionalNegate()` `conditionalNegate()` was asserting that if we negate the input, then the input cannot correspond to `100...0`. However, this is problematic when the operation is used conditionally. This is for example necessary in `convertFloatToSBV()`, where we want to apply the negation if the result is not the safe overflow value. This commit removes the assertion and adds a comment to `conditionalNegate()` that documents why we cannot have an assertion there. Additionally, the commit makes `convertFloatToSBV()` safer by explicitly handling the safe overflow case. Previously, we negated such a value, even though it cannot be negated. This worked out in the cvc5 case (because it blindly computes `~x + 1` without asserting anything), but could be dangerous. --- core/convert.h | 26 ++++++++++++++++---------- core/operations.h | 8 ++++++-- 2 files changed, 22 insertions(+), 12 deletions(-) diff --git a/core/convert.h b/core/convert.h index 348ab59..fedbfcc 100644 --- a/core/convert.h +++ b/core/convert.h @@ -483,17 +483,23 @@ template // Put the result together bwt roundSigWidth(rounded.significand.getWidth()); + prop msbSet(rounded.significand.extract(roundSigWidth - 1, + roundSigWidth - 1).isAllOnes()); + // -2^{n-1} is the only safe "overflow" case + prop safeOverflow(input.getSign() && + msbSet && + rounded.significand.extract(roundSigWidth - 2, + 0).isAllZeros()); prop undefinedResult(earlyUndefinedResult || - rounded.incrementExponent || // Definite Overflow - (rounded.significand.extract(roundSigWidth - 1, - roundSigWidth - 1).isAllOnes() && - !(input.getSign() && rounded.significand.extract(roundSigWidth - 2, 0).isAllZeros()))); // -2^{n-1} is the only safe "overflow" case - - - sbv result(ITE(undefinedResult, - undefValue, - conditionalNegate(input.getSign(), rounded.significand.toSigned()))); - + rounded.incrementExponent || // Definite Overflow + (msbSet && !safeOverflow)); + + sbv definedResult( + ITE(safeOverflow, + rounded.significand.toSigned(), + conditionalNegate(input.getSign(), + rounded.significand.toSigned()))); + sbv result(ITE(undefinedResult, undefValue, definedResult)); return result; } diff --git a/core/operations.h b/core/operations.h index 41d8367..f61021e 100644 --- a/core/operations.h +++ b/core/operations.h @@ -134,8 +134,12 @@ namespace symfpu { bv conditionalNegate (const prop &p, const bv &b) { typename t::bwt w(b.getWidth()); PRECONDITION(w >= 2); - PRECONDITION(IMPLIES(p, !(b.extract(w - 1, w - 1).isAllOnes() && - b.extract(w - 2, 0).isAllZeros()))); + // We may be tempted to check that we are not trying to negate the smallest + // value that can be represented using two's complement (i.e., `100...0`). + // This is problematic, however, in cases where we apply + // `conditionalNegate()` conditionally (e.g., in `convertFloatToSBV()`), + // because the arguments to the branches are evaluated eagerly, so the + // assertion fails, even though the result is not used. return bv(ITE(p, -b, b)); }