From aa907655cd9ec030036424acf88d9cb41a93a93b Mon Sep 17 00:00:00 2001 From: Samuel Judson Date: Wed, 8 Dec 2021 01:42:47 -0500 Subject: [PATCH] Add fp to smt printer. --- include/klee/util/ExprSMTLIBPrinter.h | 14 +- lib/Expr/ExprSMTLIBPrinter.cpp | 225 +++++++++++++++++++------- 2 files changed, 174 insertions(+), 65 deletions(-) diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index e90a49f1..956d2a9e 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -116,8 +116,8 @@ class ExprSMTLIBPrinter { ABBR_NAMED ///< Abbreviate with :named annotations. }; - /// Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV - enum SMTLIB_SORT { SORT_BITVECTOR, SORT_BOOL }; + /// Different supported SMTLIBv2 sorts (a.k.a type) in QF_FPABV + enum SMTLIB_SORT { SORT_BITVECTOR, SORT_BOOL, SORT_FP }; /// Allows the way Constant bitvectors are printed to be changed. /// This setting is persistent across queries. @@ -238,7 +238,7 @@ class ExprSMTLIBPrinter { SMTLIB_SORT getSort(const ref &e); /// Print an expression but cast it to a particular SMTLIBv2 sort first. - void printCastToSort(const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT sort); + void printCastToSort(const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT sort, ExprSMTLIBPrinter::SMTLIB_SORT constSort = SORT_BITVECTOR); // Resets various internal objects for a new query void reset(); @@ -278,14 +278,14 @@ class ExprSMTLIBPrinter { /// Print a Constant in the format specified by the current "Constant Display /// Mode" - void printConstant(const ref &e); + void printConstant(const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT constSort = SORT_BITVECTOR); /// Recursively print expression /// \param e is the expression to print /// \param expectedSort is the sort we want. If "e" is not of the right type a /// cast will be performed. /// \param abbrMode the abbreviation mode to use for this expression - void printExpression(const ref &e, SMTLIB_SORT expectedSort); + void printExpression(const ref &e, SMTLIB_SORT expectedSort, ExprSMTLIBPrinter::SMTLIB_SORT constSort = SORT_BITVECTOR); /// Scan Expression recursively for Arrays in expressions. Found arrays are /// added to @@ -323,7 +323,7 @@ class ExprSMTLIBPrinter { // For the set of operators that take sort "s" arguments void printSortArgsExpr(const ref &e, - ExprSMTLIBPrinter::SMTLIB_SORT s); + ExprSMTLIBPrinter::SMTLIB_SORT s, ExprSMTLIBPrinter::SMTLIB_SORT c = SORT_BITVECTOR); /// For the set of operators that come in two sorts (e.g. (and () ()) (bvand /// () ()) ) @@ -369,7 +369,7 @@ class ExprSMTLIBPrinter { getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option); /// Print expression without top-level abbreviations - void printFullExpression(const ref &e, SMTLIB_SORT expectedSort); + void printFullExpression(const ref &e, SMTLIB_SORT expectedSort, ExprSMTLIBPrinter::SMTLIB_SORT constSort = SORT_BITVECTOR); /// Print an assert statement for the given expr. void printAssert(const ref &e); diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index e8e9a253..10d2926e 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -10,6 +10,7 @@ #include "llvm/Support/CommandLine.h" #include "llvm/Support/ErrorHandling.h" #include "klee/util/ExprSMTLIBPrinter.h" +#include "klee/util/APFloatEval.h" #include @@ -106,7 +107,7 @@ bool ExprSMTLIBPrinter::setConstantDisplayMode(ConstantDisplayMode cdm) { return true; } -void ExprSMTLIBPrinter::printConstant(const ref &e) { +void ExprSMTLIBPrinter::printConstant(const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT c) { /* Handle simple boolean constants */ if (e->isTrue()) { @@ -130,6 +131,27 @@ void ExprSMTLIBPrinter::printConstant(const ref &e) { */ unsigned int zeroPad = 0; + /* Special case to print FP constants */ + if (c == SORT_FP) { + e->toString(value, 10); + + std::string delimit = "E+"; + if (value.find(delimit) == std::string::npos) { + unsigned long long i = std::strtoull(value.c_str(), NULL, 10); + double d; + + memcpy(&d, &i, sizeof(&d)); + + llvm::APFloat asF(d); + llvm::SmallVector result; + asF.toString(result, /*FormatPrecision=*/0, /*FormatMaxPadding=*/0); + value = std::string(result.begin(), result.end()); + } + + *p << "((_ to_fp 11 53) RNE " << value.substr(0, value.find(delimit)) << " " << value.substr(value.find(delimit) + 2) << ")"; + return; + } + switch (cdm) { case BINARY: e->toString(value, 2); @@ -156,6 +178,7 @@ void ExprSMTLIBPrinter::printConstant(const ref &e) { case DECIMAL: e->toString(value, 10); + *p << "(_ bv" << value << " " << e->getWidth() << ")"; break; @@ -164,11 +187,10 @@ void ExprSMTLIBPrinter::printConstant(const ref &e) { } } -void ExprSMTLIBPrinter::printExpression( - const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) { +void ExprSMTLIBPrinter::printExpression(const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort, ExprSMTLIBPrinter::SMTLIB_SORT constSort) { // check if casting might be necessary if (getSort(e) != expectedSort) { - printCastToSort(e, expectedSort); + printCastToSort(e, expectedSort, constSort); return; } @@ -190,7 +212,7 @@ void ExprSMTLIBPrinter::printExpression( if (i != bindings.end()) { if (i->second > 0) { *p << "(! "; - printFullExpression(e, expectedSort); + printFullExpression(e, expectedSort, constSort); *p << " :named ?B" << i->second << ")"; i->second = -i->second; } else { @@ -202,14 +224,13 @@ void ExprSMTLIBPrinter::printExpression( } } - printFullExpression(e, expectedSort); + printFullExpression(e, expectedSort, constSort); } -void ExprSMTLIBPrinter::printFullExpression( - const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) { +void ExprSMTLIBPrinter::printFullExpression(const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort, ExprSMTLIBPrinter::SMTLIB_SORT constSort) { switch (e->getKind()) { case Expr::Constant: - printConstant(cast(e)); + printConstant(cast(e), constSort); return; // base case case Expr::NotOptimized: @@ -261,6 +282,24 @@ void ExprSMTLIBPrinter::printFullExpression( printAShrExpr(cast(e)); return; + case Expr::FOEq: + case Expr::FOLt: + case Expr::FOLe: + case Expr::FOGt: + case Expr::FOGe: + case Expr::FAdd: + case Expr::FSub: + case Expr::FMul: + case Expr::FDiv: + case Expr::IsNaN: + case Expr::IsInfinite: + case Expr::IsNormal: + case Expr::IsSubnormal: + case Expr::FSqrt: + case Expr::FAbs: + printSortArgsExpr(e, SORT_FP, SORT_FP); // if one of the operands to an FP op is a constant, we need to print it as an FP + return; + default: /* The remaining operators (Add,Sub...,Ult,Ule,..) * Expect SORT_BITVECTOR arguments @@ -468,6 +507,39 @@ const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref &e) { case Expr::Sge: return "bvsge"; + case Expr::FOEq: + return "fp.eq"; + case Expr::FOLt: + return "fp.lt"; + case Expr::FOLe: + return "fp.leq"; + case Expr::FOGt: + return "fp.gt"; + case Expr::FOGe: + return "fp.geq"; + + case Expr::FAdd: + return "fp.add RNE"; + case Expr::FSub: + return "fp.sub RNE"; + case Expr::FMul: + return "fp.mul RNE"; + case Expr::FDiv: + return "fp.div RNE"; + + case Expr::IsNaN: + return "fp.isNaN"; + case Expr::IsInfinite: + return "fp.isInfinite"; + case Expr::IsNormal: + return "fp.isNormal"; + case Expr::IsSubnormal: + return "fp.isSubnormal"; + case Expr::FSqrt: + return "fp.sqrt RNE"; + case Expr::FAbs: + return "fp.abs RNE"; + default: llvm_unreachable("Conversion from Expr to SMTLIB keyword failed"); } @@ -541,10 +613,10 @@ void ExprSMTLIBPrinter::printSetLogic() { *o << "(set-logic "; switch (logicToUse) { case QF_ABV: - *o << "QF_ABV"; + *o << "ALL"; break; case QF_AUFBV: - *o << "QF_AUFBV"; + *o << "ALL"; break; } *o << " )\n"; @@ -946,8 +1018,26 @@ ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref &e) { case Expr::Ule: case Expr::Ugt: case Expr::Uge: + case Expr::FOEq: + case Expr::FOLt: + case Expr::FOLe: + case Expr::FOGt: + case Expr::FOGe: + case Expr::IsNaN: + case Expr::IsInfinite: + case Expr::IsNormal: + case Expr::IsSubnormal: return SORT_BOOL; + // Float ops return floats. + case Expr::FAdd: + case Expr::FSub: + case Expr::FMul: + case Expr::FDiv: + case Expr::FSqrt: + case Expr::FAbs: + return SORT_FP; + // These may be bitvectors or bools depending on their width (see // printConstant and printLogicalOrBitVectorExpr). case Expr::Constant: @@ -964,56 +1054,76 @@ ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref &e) { } void ExprSMTLIBPrinter::printCastToSort(const ref &e, - ExprSMTLIBPrinter::SMTLIB_SORT sort) { + ExprSMTLIBPrinter::SMTLIB_SORT sort, ExprSMTLIBPrinter::SMTLIB_SORT constSort) { + switch (sort) { - case SORT_BITVECTOR: - if (humanReadable) { - p->breakLineI(); - *p << ";Performing implicit bool to bitvector cast"; - p->breakLine(); + case SORT_FP: { + if (e->getKind() == SORT_BITVECTOR) { + // if the internal expression is a constant we'll let the constSort take care of it so we can skip the cast + if ( e->getKind() != Expr::Constant ) *p << "((_ to_fp 11 53) RNE "; + printExpression(e, SORT_BITVECTOR, constSort); + if ( e->getKind() != Expr::Constant ) *p << ")"; + } else { // SORT_BOOL + llvm_unreachable("Unsupported cast"); } - // We assume the e is a bool that we need to cast to a bitvector sort. - *p << "(ite"; - p->pushIndent(); - printSeperator(); - printExpression(e, SORT_BOOL); - printSeperator(); - *p << "(_ bv1 1)"; - printSeperator(); // printing the "true" bitvector - *p << "(_ bv0 1)"; - p->popIndent(); - printSeperator(); // printing the "false" bitvector - *p << ")"; - break; - case SORT_BOOL: { - /* We make the assumption (might be wrong) that any bitvector whose unsigned - * decimal value is is zero is interpreted as "false", otherwise it is - * true. - * - * This may not be the interpretation we actually want! - */ - Expr::Width bitWidth = e->getWidth(); - if (humanReadable) { - p->breakLineI(); - *p << ";Performing implicit bitvector to bool cast"; - p->breakLine(); + } break; + case SORT_BITVECTOR: { + if (e->getKind() == SORT_BOOL) { + if (humanReadable) { + p->breakLineI(); + *p << ";Performing implicit bool to bitvector cast"; + p->breakLine(); + } + // We assume the e is a bool that we need to cast to a bitvector sort. + *p << "(ite"; + p->pushIndent(); + printSeperator(); + printExpression(e, SORT_BOOL, constSort); + printSeperator(); + *p << "(_ bv1 1)"; + printSeperator(); // printing the "true" bitvector + *p << "(_ bv0 1)"; + p->popIndent(); + printSeperator(); // printing the "false" bitvector + *p << ")"; + } else { // SORT_FP + *p << "((_ fp.to_ubv 64) RNE "; + printExpression(e, SORT_FP, constSort); + *p << ")"; } - *p << "(bvugt"; - p->pushIndent(); - printSeperator(); - // We assume is e is a bitvector - printExpression(e, SORT_BITVECTOR); - printSeperator(); - *p << "(_ bv0 " << bitWidth << ")"; - p->popIndent(); - printSeperator(); // Zero bitvector of required width - *p << ")"; + } break; + case SORT_BOOL: { + if (e->getKind() == SORT_BITVECTOR) { + /* We make the assumption (might be wrong) that any bitvector whose unsigned + * decimal value is is zero is interpreted as "false", otherwise it is + * true. + * + * This may not be the interpretation we actually want! + */ + Expr::Width bitWidth = e->getWidth(); + if (humanReadable) { + p->breakLineI(); + *p << ";Performing implicit bitvector to bool cast"; + p->breakLine(); + } + *p << "(bvugt"; + p->pushIndent(); + printSeperator(); + // We assume is e is a bitvector + printExpression(e, SORT_BITVECTOR, constSort); + printSeperator(); + *p << "(_ bv0 " << bitWidth << ")"; + p->popIndent(); + printSeperator(); // Zero bitvector of required width + *p << ")"; - if (bitWidth != Expr::Bool) - llvm::errs() + if (bitWidth != Expr::Bool) + llvm::errs() << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length " << bitWidth << ") to bool!\n"; - + } else { // SORT_FP + llvm_unreachable("Unsupported cast"); + } } break; default: llvm_unreachable("Unsupported cast"); @@ -1048,15 +1158,14 @@ void ExprSMTLIBPrinter::printSelectExpr(const ref &e, *p << ")"; } -void ExprSMTLIBPrinter::printSortArgsExpr(const ref &e, - ExprSMTLIBPrinter::SMTLIB_SORT s) { +void ExprSMTLIBPrinter::printSortArgsExpr(const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT s, ExprSMTLIBPrinter::SMTLIB_SORT c) { *p << "(" << getSMTLIBKeyword(e) << " "; p->pushIndent(); // add indent for recursive call // loop over children and recurse into each expecting they are of sort "s" for (unsigned int i = 0; i < e->getNumKids(); i++) { printSeperator(); - printExpression(e->getKid(i), s); + printExpression(e->getKid(i), s, c); } p->popIndent(); // pop indent added for recursive call