Skip to content

Commit

Permalink
[analyzer] Create generic SMT Expr class
Browse files Browse the repository at this point in the history 
Summary:
New base class for all future SMT Exprs.

No major changes except moving `areEquivalent` and `getFloatSemantics` outside of `Z3Expr` to keep the class minimal.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

Differential Revision: https://reviews.llvm.org/D49551

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@337917 91177308-0d34-0410-b5e6-96231b3b80d8
  • Loading branch information
@mikhailramalho
mikhailramalho committed Jul 25, 2018
1 parent 143e570 commit 9a5865c
Show file tree
Hide file tree
Showing 2 changed files with 101 additions and 53 deletions.
57 changes: 57 additions & 0 deletions include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
//== SMTExpr.h --------------------------------------------------*- C++ -*--==//
//
// The LLVM Compiler Infrastructure
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
//
// This file defines a SMT generic Expr API, which will be the base class
// for every SMT solver expr specific class.
//
//===----------------------------------------------------------------------===//

#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H

#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"

namespace clang {
namespace ento {

class SMTExpr {
public:
SMTExpr() = default;
virtual ~SMTExpr() = default;

bool operator<(const SMTExpr &Other) const {
llvm::FoldingSetNodeID ID1, ID2;
Profile(ID1);
Other.Profile(ID2);
return ID1 < ID2;
}

virtual void Profile(llvm::FoldingSetNodeID &ID) const {
static int Tag = 0;
ID.AddPointer(&Tag);
}

friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
return LHS.equal_to(RHS);
}

virtual void print(raw_ostream &OS) const = 0;

LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }

protected:
virtual bool equal_to(SMTExpr const &other) const = 0;
};

using SMTExprRef = std::shared_ptr<SMTExpr>;

} // namespace ento
} // namespace clang

#endif
97 changes: 44 additions & 53 deletions lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"

#include "clang/Config/config.h"
Expand Down Expand Up @@ -162,40 +163,25 @@ class Z3Sort : public SMTSort {
}
}; // end class Z3Sort

class Z3Expr {
friend class Z3Model;
class Z3Expr : public SMTExpr {
friend class Z3Solver;

Z3Context &Context;

Z3_ast AST;

Z3Expr(Z3Context &C, Z3_ast ZA) : Context(C), AST(ZA) {
assert(C.Context != nullptr);
Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
Z3_inc_ref(Context.Context, AST);
}

// Determine whether two float semantics are equivalent
static bool areEquivalent(const llvm::fltSemantics &LHS,
const llvm::fltSemantics &RHS) {
return (llvm::APFloat::semanticsPrecision(LHS) ==
llvm::APFloat::semanticsPrecision(RHS)) &&
(llvm::APFloat::semanticsMinExponent(LHS) ==
llvm::APFloat::semanticsMinExponent(RHS)) &&
(llvm::APFloat::semanticsMaxExponent(LHS) ==
llvm::APFloat::semanticsMaxExponent(RHS)) &&
(llvm::APFloat::semanticsSizeInBits(LHS) ==
llvm::APFloat::semanticsSizeInBits(RHS));
}

public:
/// Override implicit copy constructor for correct reference counting.
Z3Expr(const Z3Expr &Copy) : Context(Copy.Context), AST(Copy.AST) {
Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
Z3_inc_ref(Context.Context, AST);
}

/// Provide move constructor
Z3Expr(Z3Expr &&Move) : Context(Move.Context), AST(nullptr) {
Z3Expr(Z3Expr &&Move) : SMTExpr(), Context(Move.Context), AST(nullptr) {
*this = std::move(Move);
}

Expand All @@ -215,40 +201,18 @@ class Z3Expr {
Z3_dec_ref(Context.Context, AST);
}

/// Get the corresponding IEEE floating-point type for a given bitwidth.
static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
switch (BitWidth) {
default:
llvm_unreachable("Unsupported floating-point semantics!");
break;
case 16:
return llvm::APFloat::IEEEhalf();
case 32:
return llvm::APFloat::IEEEsingle();
case 64:
return llvm::APFloat::IEEEdouble();
case 128:
return llvm::APFloat::IEEEquad();
}
}

void Profile(llvm::FoldingSetNodeID &ID) const {
void Profile(llvm::FoldingSetNodeID &ID) const override {
ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));
}

bool operator<(const Z3Expr &Other) const {
llvm::FoldingSetNodeID ID1, ID2;
Profile(ID1);
Other.Profile(ID2);
return ID1 < ID2;
}

/// Comparison of AST equality, not model equivalence.
bool operator==(const Z3Expr &Other) const {
bool equal_to(SMTExpr const &Other) const override {
assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
Z3_get_sort(Context.Context, Other.AST)) &&
Z3_get_sort(Context.Context,
static_cast<const Z3Expr &>(Other).AST)) &&
"AST's must have the same sort");
return Z3_is_eq_ast(Context.Context, AST, Other.AST);
return Z3_is_eq_ast(Context.Context, AST,
static_cast<const Z3Expr &>(Other).AST);
}

/// Override implicit move constructor for correct reference counting.
Expand All @@ -259,11 +223,9 @@ class Z3Expr {
return *this;
}

void print(raw_ostream &OS) const {
void print(raw_ostream &OS) const override {
OS << Z3_ast_to_string(Context.Context, AST);
}

LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Expr

class Z3Model {
Expand Down Expand Up @@ -312,6 +274,36 @@ class Z3Model {
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Model

/// Get the corresponding IEEE floating-point type for a given bitwidth.
static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
switch (BitWidth) {
default:
llvm_unreachable("Unsupported floating-point semantics!");
break;
case 16:
return llvm::APFloat::IEEEhalf();
case 32:
return llvm::APFloat::IEEEsingle();
case 64:
return llvm::APFloat::IEEEdouble();
case 128:
return llvm::APFloat::IEEEquad();
}
}

// Determine whether two float semantics are equivalent
static bool areEquivalent(const llvm::fltSemantics &LHS,
const llvm::fltSemantics &RHS) {
return (llvm::APFloat::semanticsPrecision(LHS) ==
llvm::APFloat::semanticsPrecision(RHS)) &&
(llvm::APFloat::semanticsMinExponent(LHS) ==
llvm::APFloat::semanticsMinExponent(RHS)) &&
(llvm::APFloat::semanticsMaxExponent(LHS) ==
llvm::APFloat::semanticsMaxExponent(RHS)) &&
(llvm::APFloat::semanticsSizeInBits(LHS) ==
llvm::APFloat::semanticsSizeInBits(RHS));
}

class Z3Solver {
friend class Z3ConstraintManager;

Expand Down Expand Up @@ -812,14 +804,13 @@ class Z3Solver {

llvm::APSInt Int(Sort.getFloatSortSize(), true);
const llvm::fltSemantics &Semantics =
Z3Expr::getFloatSemantics(Sort.getFloatSortSize());
getFloatSemantics(Sort.getFloatSortSize());
Z3Sort BVSort = getBitvectorSort(Sort.getFloatSortSize());
if (!toAPSInt(BVSort, AST, Int, true)) {
return false;
}

if (useSemantics &&
!Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) {
if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
assert(false && "Floating-point types don't match!");
return false;
}
Expand Down

0 comments on commit 9a5865c

Please sign in to comment.