diff --git a/.gitmodules b/.gitmodules index 32ba47b83..7f5dd3116 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,3 @@ [submodule "sea-dsa"] path = sea-dsa - url = https://github.com/seahorn/sea-dsa.git + url = https://github.com/shaobo-he/sea-dsa.git diff --git a/bin/versions b/bin/versions index 135be2470..1fdf40477 100644 --- a/bin/versions +++ b/bin/versions @@ -5,6 +5,6 @@ BOOGIE_VERSION="2.15.7" CORRAL_VERSION="1.1.8" SYMBOOGLIX_COMMIT="ccb2e7f2b3" LOCKPWN_COMMIT="12ba58f1ec" -LLVM_SHORT_VERSION="14" -LLVM_FULL_VERSION="14.0.0" +LLVM_SHORT_VERSION="15" +LLVM_FULL_VERSION="15.0.6" RUST_VERSION="nightly-2022-08-12" diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h index 06e77157c..16bcc6045 100644 --- a/include/smack/BoogieAst.h +++ b/include/smack/BoogieAst.h @@ -605,7 +605,7 @@ class ProcDecl : public Decl, public CodeContainer { ParameterList params; ParameterList rets; - SpecificationList requires; + SpecificationList requires_; SpecificationList ensures; public: @@ -622,9 +622,9 @@ class ProcDecl : public Decl, public CodeContainer { ParameterList &getReturns() { return rets; } typedef SpecificationList::iterator spec_iterator; - spec_iterator requires_begin() { return requires.begin(); } - spec_iterator requires_end() { return requires.end(); } - SpecificationList &getRequires() { return requires; } + spec_iterator requires_begin() { return requires_.begin(); } + spec_iterator requires_end() { return requires_.end(); } + SpecificationList &getRequires() { return requires_; } spec_iterator ensures_begin() { return ensures.begin(); } spec_iterator ensures_end() { return ensures.end(); } diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index 44dfe7fe5..02626e9b5 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -172,8 +172,9 @@ class SmackRep { const Stmt *alloca(llvm::AllocaInst &i); const Stmt *memcpy(const llvm::MemCpyInst &msi); const Stmt *memset(const llvm::MemSetInst &msi); - const Expr *load(const llvm::Value *P); + const Expr *load(const llvm::Value *P, const llvm::Type *T); const Stmt *store(const llvm::Value *P, const llvm::Value *V); + const Stmt *store(const llvm::Value *P, const llvm::Type *T, const Expr *V); const Stmt *store(const llvm::Value *P, const Expr *V); const Stmt *valueAnnotation(const llvm::CallInst &CI); diff --git a/include/smack/VectorOperations.h b/include/smack/VectorOperations.h index ea6ce07a4..7a4f84723 100644 --- a/include/smack/VectorOperations.h +++ b/include/smack/VectorOperations.h @@ -38,8 +38,8 @@ class VectorOperations { FuncDecl *shuffle(Type *T, Type *U, std::vector mask); FuncDecl *insert(Type *T, Type *IT); FuncDecl *extract(Type *T, Type *IT); - FuncDecl *load(const Value *V); - FuncDecl *store(const Value *V); + FuncDecl *load(const Value *V, Type *ET); + FuncDecl *store(const Value *V, Type *ET); }; } // namespace smack diff --git a/lib/smack/AddTiming.cpp b/lib/smack/AddTiming.cpp index 9d46affb9..52c03c998 100644 --- a/lib/smack/AddTiming.cpp +++ b/lib/smack/AddTiming.cpp @@ -26,6 +26,7 @@ #include "llvm/IR/Function.h" #include "llvm/IR/Instructions.h" #include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/Operator.h" #include "llvm/IR/Value.h" #include "llvm/Pass.h" #include "llvm/Support/Alignment.h" @@ -137,7 +138,7 @@ InstructionCost AddTiming::getInstructionCost(const Instruction *I) const { switch (I->getOpcode()) { case Instruction::GetElementPtr: { - Type *ValTy = I->getOperand(0)->getType()->getPointerElementType(); + Type *ValTy = cast(I)->getSourceElementType(); return TTI->getAddressComputationCost(ValTy); } @@ -189,16 +190,14 @@ InstructionCost AddTiming::getInstructionCost(const Instruction *I) const { Type *ValTy = SI->getValueOperand()->getType(); assert(!ValTy->isStructTy() && "Timing annotations do not currently work for struct sized stores"); - return TTI->getMemoryOpCost(I->getOpcode(), ValTy, - Align(SI->getAlignment()), + return TTI->getMemoryOpCost(I->getOpcode(), ValTy, SI->getAlign(), SI->getPointerAddressSpace()); } case Instruction::Load: { const LoadInst *LI = cast(I); assert(!I->getType()->isStructTy() && "Timing annotations do not currently work for struct sized loads"); - return TTI->getMemoryOpCost(I->getOpcode(), I->getType(), - Align(LI->getAlignment()), + return TTI->getMemoryOpCost(I->getOpcode(), I->getType(), LI->getAlign(), LI->getPointerAddressSpace()); } case Instruction::ZExt: diff --git a/lib/smack/BoogieAst.cpp b/lib/smack/BoogieAst.cpp index 15781ac6f..20221a567 100644 --- a/lib/smack/BoogieAst.cpp +++ b/lib/smack/BoogieAst.cpp @@ -644,9 +644,10 @@ void ProcDecl::print(std::ostream &os) const { os << "\n"; print_seq(os, mods, " modifies ", ", ", ";"); } - if (requires.size() > 0) { + if (requires_.size() > 0) { os << "\n"; - print_seq(os, requires, " requires ", ";\n requires ", ";"); + print_seq(os, requires_, " requires ", ";\n requires ", + ";"); } if (ensures.size() > 0) { os << "\n"; diff --git a/lib/smack/CodifyStaticInits.cpp b/lib/smack/CodifyStaticInits.cpp index 7b1e09ef5..7bf1a21d5 100644 --- a/lib/smack/CodifyStaticInits.cpp +++ b/lib/smack/CodifyStaticInits.cpp @@ -24,6 +24,30 @@ namespace smack { using namespace llvm; +namespace { +using StaticInitItem = std::tuple>; + +void enqueueGlobal(GlobalVariable *G, std::deque &worklist, + std::set &seen) { + if (!G || !G->hasInitializer() || !seen.insert(G).second) + return; + worklist.push_back( + std::make_tuple(G->getInitializer(), G, std::vector())); +} + +void enqueueReferencedGlobals(Constant *C, std::deque &worklist, + std::set &seen) { + if (auto *G = dyn_cast(C->stripPointerCasts())) { + enqueueGlobal(G, worklist, seen); + return; + } + + for (Use &O : C->operands()) + if (auto *SubC = dyn_cast(O.get())) + enqueueReferencedGlobals(SubC, worklist, seen); +} +} // namespace + bool CodifyStaticInits::runOnModule(Module &M) { TD = &M.getDataLayout(); LLVMContext &C = M.getContext(); @@ -36,26 +60,27 @@ bool CodifyStaticInits::runOnModule(Module &M) { BasicBlock *B = BasicBlock::Create(C, "entry", F); IRBuilder<> IRB(B); - std::deque>> worklist; + std::deque worklist; + std::set seen; for (auto &G : M.globals()) if (G.hasInitializer() && DSA->isRead(&G)) - worklist.push_back( - std::make_tuple(G.getInitializer(), &G, std::vector())); + enqueueGlobal(&G, worklist, seen); while (worklist.size()) { Constant *V = std::get<0>(worklist.front()); Constant *P = std::get<1>(worklist.front()); std::vector I = std::get<2>(worklist.front()); worklist.pop_front(); + enqueueReferencedGlobals(V, worklist, seen); if (V->getType()->isIntegerTy() || V->getType()->isPointerTy() || V->getType()->isFloatingPointTy() || V->getType()->isVectorTy()) - IRB.CreateStore( - V, - IRB.CreateGEP(P->getType()->getScalarType()->getPointerElementType(), - P, ArrayRef(I))); + IRB.CreateStore(V, IRB.CreateGEP(cast( + P->stripPointerCastsAndAliases()) + ->getValueType(), + P, ArrayRef(I))); else if (ArrayType *AT = dyn_cast(V->getType())) for (unsigned i = AT->getNumElements(); i-- > 0;) { diff --git a/lib/smack/DSAWrapper.cpp b/lib/smack/DSAWrapper.cpp index 2968fc1e1..9696cd916 100644 --- a/lib/smack/DSAWrapper.cpp +++ b/lib/smack/DSAWrapper.cpp @@ -11,6 +11,7 @@ #include "smack/SmackOptions.h" #include "llvm/IR/InstIterator.h" #include "llvm/IR/IntrinsicInst.h" +#include "llvm/IR/Operator.h" #include "llvm/Support/FileSystem.h" #include @@ -22,6 +23,43 @@ namespace smack { using namespace llvm; +namespace { +Type *inferPointeeType(const Value *V) { + V = V->stripPointerCastsAndAliases(); + + if (const auto *AI = dyn_cast(V)) + return AI->getAllocatedType(); + if (const auto *GV = dyn_cast(V)) + return GV->getValueType(); + if (const auto *GEP = dyn_cast(V)) + return GEP->getResultElementType(); + + Type *Evidence = nullptr; + for (const User *U : V->users()) { + Type *Candidate = nullptr; + if (const auto *LI = dyn_cast(U)) { + if (LI->getPointerOperand()->stripPointerCastsAndAliases() == V) + Candidate = LI->getType(); + } else if (const auto *SI = dyn_cast(U)) { + if (SI->getPointerOperand()->stripPointerCastsAndAliases() == V) + Candidate = SI->getValueOperand()->getType(); + } else if (const auto *GEP = dyn_cast(U)) { + if (GEP->getPointerOperand()->stripPointerCastsAndAliases() == V) + Candidate = GEP->getSourceElementType(); + } + + if (!Candidate) + continue; + if (!Evidence) + Evidence = Candidate; + else if (Evidence != Candidate) + return nullptr; + } + + return Evidence; +} +} // namespace + void DSAWrapper::getAnalysisUsage(llvm::AnalysisUsage &AU) const { AU.setPreservesAll(); AU.addRequiredTransitive(); @@ -92,8 +130,10 @@ bool DSAWrapper::isRead(const Value *V) { } unsigned DSAWrapper::getPointedTypeSize(const Value *v) { - if (llvm::PointerType *t = llvm::dyn_cast(v->getType())) { - llvm::Type *pointedType = t->getElementType(); + if (v->getType()->isPointerTy()) { + llvm::Type *pointedType = inferPointeeType(v); + if (!pointedType) + return UINT_MAX; if (pointedType->isSized()) return dataLayout->getTypeStoreSize(pointedType); else diff --git a/lib/smack/MemorySafetyChecker.cpp b/lib/smack/MemorySafetyChecker.cpp index 9d84d8936..1a25c6fd7 100644 --- a/lib/smack/MemorySafetyChecker.cpp +++ b/lib/smack/MemorySafetyChecker.cpp @@ -80,21 +80,14 @@ Value *accessSizeAsPointer(Module &M, Type *T) { PointerType::getUnqual(Type::getInt8Ty(M.getContext()))); } -Value *accessSizeAsPointer(Module &M, Value *V) { - auto T = dyn_cast(V->getType()); - assert(T && "expected pointer type"); - - return accessSizeAsPointer(M, T->getPointerElementType()); -} - Value *accessSizeAsPointer(LoadInst &I) { auto &M = *I.getParent()->getParent()->getParent(); - return accessSizeAsPointer(M, I.getPointerOperand()); + return accessSizeAsPointer(M, I.getType()); } Value *accessSizeAsPointer(StoreInst &I) { auto &M = *I.getParent()->getParent()->getParent(); - return accessSizeAsPointer(M, I.getPointerOperand()); + return accessSizeAsPointer(M, I.getValueOperand()->getType()); } } // namespace @@ -113,10 +106,14 @@ bool MemorySafetyChecker::visitSplitAggregateAccess(Value *addr, if (auto *GEP = dyn_cast(addr)) { base = GEP->getPointerOperand(); T = GEP->getSourceElementType(); + } else if (auto *LI = dyn_cast(I)) { + T = LI->getType(); + } else if (auto *SI = dyn_cast(I)) { + T = SI->getValueOperand()->getType(); } else { auto *PT = dyn_cast(addr->getType()); assert(PT && "expected pointer type"); - T = PT->getPointerElementType(); + T = Type::getInt8Ty(M.getContext()); } insertMemoryAccessCheck(base, accessSizeAsPointer(M, T), I); diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp index deb5891c1..a2b03d807 100644 --- a/lib/smack/Prelude.cpp +++ b/lib/smack/Prelude.cpp @@ -1187,7 +1187,7 @@ void PtrOpGen::generatePtrNumConvs(std::stringstream &s) const { // e.g., function {:inline} $p2i.ref.i8(p: ref) returns (i8) { // $trunc.i64.i8(p) } - for (unsigned i = 8; i <= 64; i <<= 1) { + for (auto i : IntOpGen::INTEGER_SIZES) { s << Decl::function( indexedName("$p2i", {Naming::PTR_TYPE, prelude.rep.intType(i)}), {{"p", Naming::PTR_TYPE}}, prelude.rep.intType(i), diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index 04474d1e3..9f367983f 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -5,12 +5,60 @@ #include "smack/DSAWrapper.h" #include "smack/Debug.h" #include "smack/SmackOptions.h" +#include "llvm/ADT/APInt.h" #include "llvm/IR/GetElementPtrTypeIterator.h" +#include "llvm/IR/Operator.h" #define DEBUG_TYPE "regions" namespace smack { +namespace { +Type *inferPointeeType(const Value *V) { + V = V->stripPointerCastsAndAliases(); + + if (const auto *AI = dyn_cast(V)) + return AI->getAllocatedType(); + if (const auto *GV = dyn_cast(V)) + return GV->getValueType(); + if (const auto *GEP = dyn_cast(V)) + return GEP->getResultElementType(); + + Type *Evidence = nullptr; + for (const User *U : V->users()) { + Type *Candidate = nullptr; + if (const auto *LI = dyn_cast(U)) { + if (LI->getPointerOperand()->stripPointerCastsAndAliases() == V) + Candidate = LI->getType(); + } else if (const auto *SI = dyn_cast(U)) { + if (SI->getPointerOperand()->stripPointerCastsAndAliases() == V) + Candidate = SI->getValueOperand()->getType(); + } else if (const auto *GEP = dyn_cast(U)) { + if (GEP->getPointerOperand()->stripPointerCastsAndAliases() == V) + Candidate = GEP->getSourceElementType(); + } + + if (!Candidate) + continue; + if (!Evidence) + Evidence = Candidate; + else if (Evidence != Candidate) + return nullptr; + } + + return Evidence; +} + +Type *firstAggregateElementType(Type *T) { + if (auto *AT = dyn_cast(T)) + return AT->getElementType(); + if (auto *ST = dyn_cast(T)) + if (ST->getNumElements() > 0) + return ST->getElementType(0); + return nullptr; +} +} // namespace + const DataLayout *Region::DL = nullptr; DSAWrapper *Region::DSA = nullptr; @@ -21,6 +69,10 @@ void Region::init(Module &M, Pass &P) { bool Region::isSingleton(const Value *v, unsigned length) { // TODO can we do something for non-global nodes? + if (Type *T = inferPointeeType(v)) + if (T->isAggregateType()) + return false; + auto node = DSA->getNode(v); return !isAllocated(node) && DSA->getNumGlobals(node) == 1 && @@ -39,12 +91,28 @@ bool Region::isComplicated(const seadsa::Node *N) { void Region::init(const Value *V, unsigned length) { Type *T = V->getType(); assert(T->isPointerTy() && "Expected pointer argument."); - T = T->getPointerElementType(); + T = inferPointeeType(V); + if (!T) + T = Type::getInt8Ty(V->getContext()); + if (DL && isa(V->stripPointerCastsAndAliases())) + if (Type *ElemTy = firstAggregateElementType(T)) + if (ElemTy->isSized() && length == DL->getTypeStoreSize(ElemTy)) + T = ElemTy; context = &V->getContext(); representative = (DSA && !dyn_cast(V)) ? DSA->getNode(V) : nullptr; this->type = T; this->offset = DSA ? DSA->getOffset(V) : 0; + bool variableGEP = false; + if (DL) + if (const auto *GEP = dyn_cast(V)) { + for (const Use &I : GEP->indices()) + variableGEP |= !isa(I.get()); + APInt offset(DL->getPointerSizeInBits(), 0); + if (!variableGEP && GEP->accumulateConstantOffset(*DL, offset) && + !offset.isNegative()) + this->offset = offset.getZExtValue(); + } this->length = length; singleton = DL && representative && isSingleton(V, length); @@ -54,7 +122,8 @@ void Region::init(const Value *V, unsigned length) { (!representative || !DSA->isTypeSafe(V)) || T->isIntegerTy(8)); incomplete = !representative || representative->isIncomplete(); complicated = !representative || isComplicated(representative); - collapsed = !representative || representative->isOffsetCollapsed(); + collapsed = + !representative || representative->isOffsetCollapsed() || variableGEP; } Region::Region(const Value *V) { @@ -292,7 +361,10 @@ void Regions::visitCallInst(CallInst &I) { if (auto I = dyn_cast(N)) { const unsigned bound = I->getZExtValue(); - const unsigned size = T->getElementType()->getIntegerBitWidth() / 8; + Type *ElemTy = inferPointeeType(P); + const unsigned size = ElemTy && ElemTy->isIntegerTy() + ? ElemTy->getIntegerBitWidth() / 8 + : 1; const unsigned length = bound * size; idx(P, length); diff --git a/lib/smack/RustFixes.cpp b/lib/smack/RustFixes.cpp index e9c000eeb..e69432b46 100644 --- a/lib/smack/RustFixes.cpp +++ b/lib/smack/RustFixes.cpp @@ -7,6 +7,7 @@ #include "smack/RustFixes.h" #include "smack/Naming.h" +#include "llvm/IR/Constants.h" #include "llvm/IR/InstIterator.h" #include "llvm/IR/Instructions.h" #include "llvm/IR/Module.h" diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index d798bedad..14210627a 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -483,18 +483,17 @@ void SmackInstGenerator::visitAllocaInst(llvm::AllocaInst &ai) { void SmackInstGenerator::visitLoadInst(llvm::LoadInst &li) { processInstruction(li); auto P = li.getPointerOperand(); - auto T = dyn_cast(P->getType()); - assert(T && "expected pointer type"); + assert(P->getType()->isPointerTy() && "expected pointer type"); // TODO what happens with aggregate types? // assert (!li.getType()->isAggregateType() && "Unexpected load value."); const Expr *E; - if (isa(T->getElementType())) { - auto D = VectorOperations(rep).load(P); + if (isa(li.getType())) { + auto D = VectorOperations(rep).load(P, li.getType()); E = Expr::fn(D->getName(), {Expr::id(rep->memPath(P)), rep->expr(P)}); } else { - E = rep->load(P); + E = rep->load(P, li.getType()); } emit(Stmt::assign(rep->expr(&li), E)); @@ -515,7 +514,7 @@ void SmackInstGenerator::visitStoreInst(llvm::StoreInst &si) { assert(!V->getType()->isAggregateType() && "Unexpected store value."); if (isa(V->getType())) { - auto D = VectorOperations(rep).store(P); + auto D = VectorOperations(rep).store(P, V->getType()); auto M = Expr::id(rep->memPath(P)); auto E = Expr::fn(D->getName(), {M, rep->expr(P), rep->expr(V)}); emit(Stmt::assign(M, E)); @@ -529,12 +528,8 @@ void SmackInstGenerator::visitStoreInst(llvm::StoreInst &si) { if (SmackOptions::SourceLocSymbols) { if (const llvm::GlobalVariable *G = llvm::dyn_cast(P)) { - if (const llvm::PointerType *t = - llvm::dyn_cast(G->getType())) { - if (!t->getElementType()->isPointerTy() && G->hasName()) { - emit(recordProcedureCall(V, - {Attr::attr("cexpr", G->getName().str())})); - } + if (!G->getValueType()->isPointerTy() && G->hasName()) { + emit(recordProcedureCall(V, {Attr::attr("cexpr", G->getName().str())})); } } } @@ -551,11 +546,12 @@ void SmackInstGenerator::visitStoreInst(llvm::StoreInst &si) { void SmackInstGenerator::visitAtomicCmpXchgInst(llvm::AtomicCmpXchgInst &i) { processInstruction(i); const Expr *res = rep->expr(&i); - const Expr *mem = rep->load(i.getOperand(0)); + const Expr *mem = + rep->load(i.getOperand(0), i.getCompareOperand()->getType()); const Expr *cmp = rep->expr(i.getOperand(1)); const Expr *swp = rep->expr(i.getOperand(2)); emit(Stmt::assign(res, mem)); - emit(rep->store(i.getOperand(0), + emit(rep->store(i.getOperand(0), i.getNewValOperand()->getType(), Expr::ifThenElse(Expr::eq(mem, cmp), swp, mem))); } @@ -563,11 +559,12 @@ void SmackInstGenerator::visitAtomicRMWInst(llvm::AtomicRMWInst &i) { using llvm::AtomicRMWInst; processInstruction(i); const Expr *res = rep->expr(&i); - const Expr *mem = rep->load(i.getPointerOperand()); + const Expr *mem = + rep->load(i.getPointerOperand(), i.getValOperand()->getType()); const Expr *val = rep->expr(i.getValOperand()); auto valT = rep->type(i.getValOperand()->getType()); emit(Stmt::assign(res, mem)); - emit(rep->store(i.getPointerOperand(), + emit(rep->store(i.getPointerOperand(), i.getValOperand()->getType(), i.getOperation() == AtomicRMWInst::Xchg ? val : Expr::fn(indexedName(Naming::ATOMICRMWINST_TABLE.at( diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index d9fe57086..f5b249b76 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -12,6 +12,7 @@ #include "smack/Naming.h" #include "smack/Regions.h" #include "smack/SmackWarnings.h" +#include "llvm/IR/Operator.h" #include #include @@ -48,6 +49,47 @@ std::list findCallers(Function *F) { return callers; } + +Type *inferPointeeType(const Value *V) { + V = V->stripPointerCastsAndAliases(); + + if (const auto *AI = dyn_cast(V)) + return AI->getAllocatedType(); + if (const auto *GV = dyn_cast(V)) + return GV->getValueType(); + if (const auto *GEP = dyn_cast(V)) + return GEP->getResultElementType(); + + Type *evidence = nullptr; + for (const User *U : V->users()) { + Type *candidate = nullptr; + if (const auto *LI = dyn_cast(U)) { + if (LI->getPointerOperand()->stripPointerCastsAndAliases() == V) + candidate = LI->getType(); + } else if (const auto *SI = dyn_cast(U)) { + if (SI->getPointerOperand()->stripPointerCastsAndAliases() == V) + candidate = SI->getValueOperand()->getType(); + } else if (const auto *GEP = dyn_cast(U)) { + if (GEP->getPointerOperand()->stripPointerCastsAndAliases() == V) + candidate = GEP->getSourceElementType(); + } + + if (!candidate) + continue; + if (!evidence) + evidence = candidate; + else if (evidence != candidate) + return nullptr; + } + + return evidence; +} + +Type *inferPointeeTypeOrI8(const Value *V) { + if (Type *T = inferPointeeType(V)) + return T; + return Type::getInt8Ty(V->getContext()); +} } // namespace namespace smack { @@ -122,20 +164,21 @@ std::list SmackRep::auxiliaryDeclarations() { } std::string SmackRep::getString(const llvm::Value *v) { - if (const llvm::ConstantExpr *constantExpr = - llvm::dyn_cast(v)) - if (constantExpr->getOpcode() == llvm::Instruction::GetElementPtr) - if (const llvm::GlobalValue *cc = llvm::dyn_cast( - constantExpr->getOperand(0))) - if (const llvm::ConstantDataSequential *cds = - llvm::dyn_cast( - cc->getOperand(0))) - return cds->getAsCString().str(); + v = v->stripPointerCastsAndAliases(); + if (const auto *GEP = dyn_cast(v)) + v = GEP->getPointerOperand()->stripPointerCastsAndAliases(); + + if (const auto *GV = dyn_cast(v)) + if (GV->hasInitializer()) + if (const auto *cds = + dyn_cast(GV->getInitializer())) + return cds->getAsCString().str(); + return ""; } unsigned SmackRep::getElementSize(const llvm::Value *v) { - return getSize(v->getType()->getPointerElementType()); + return getSize(inferPointeeTypeOrI8(v)); } unsigned SmackRep::getIntSize(const llvm::Value *v) { @@ -395,7 +438,7 @@ const Stmt *SmackRep::valueAnnotation(const CallInst &CI) { if ((A = dyn_cast(V))) { auto PT = dyn_cast(A->getType()); assert(PT && "Expected pointer argument."); - T = PT->getElementType(); + T = inferPointeeTypeOrI8(A); addr = expr(A); } else if (auto GEP = dyn_cast(V)) { @@ -412,7 +455,7 @@ const Stmt *SmackRep::valueAnnotation(const CallInst &CI) { assert(A->hasName() && "Expected named argument."); auto PT = dyn_cast(V->getType()); assert(PT && "Expected pointer type result of load instruction."); - T = PT->getElementType(); + T = inferPointeeTypeOrI8(V); addr = ptrArith(GEP); } else { @@ -499,32 +542,40 @@ bool SmackRep::isUnsafeFloatAccess(const Type *elemTy, const Type *resultTy) { return false; } -const Expr *SmackRep::load(const llvm::Value *P) { - const PointerType *T = dyn_cast(P->getType()); - assert(T && "Expected pointer type."); - const unsigned R = regions->idx(P); +const Expr *SmackRep::load(const llvm::Value *P, const Type *T) { + assert(P->getType()->isPointerTy() && "Expected pointer type."); + unsigned length = T && T->isSized() + ? targetData->getTypeStoreSize(const_cast(T)) + : std::numeric_limits::max(); + const unsigned R = regions->idx(P, length); bool bytewise = regions->get(R).bytewiseAccess(); bool singleton = regions->get(R).isSingleton(); const Type *resultTy = regions->get(R).getType(); const Expr *M = Expr::id(memPath(R)); std::string N = Naming::LOAD + "." + - (bytewise - ? "bytes." - : (isUnsafeFloatAccess(T->getElementType(), resultTy) ? "unsafe." - : "")) + - type(T->getElementType()); + (bytewise ? "bytes." + : (isUnsafeFloatAccess(T, resultTy) ? "unsafe." : "")) + + type(T); return singleton ? M : Expr::fn(N, M, SmackRep::expr(P)); } const Stmt *SmackRep::store(const Value *P, const Value *V) { - return store(P, expr(V)); + return store(P, V->getType(), expr(V)); } const Stmt *SmackRep::store(const Value *P, const Expr *V) { - const PointerType *T = dyn_cast(P->getType()); - assert(T && "Expected pointer type."); - return store(regions->idx(P), T->getElementType(), expr(P), V); + return store(P, regions->get(regions->idx(P)).getType(), V); +} + +const Stmt *SmackRep::store(const Value *P, const Type *T, const Expr *V) { + assert(P->getType()->isPointerTy() && "Expected pointer type."); + if (!T) + T = Type::getInt8Ty(P->getContext()); + unsigned length = T->isSized() + ? targetData->getTypeStoreSize(const_cast(T)) + : std::numeric_limits::max(); + return store(regions->idx(P, length), T, expr(P), V); } const Stmt *SmackRep::store(unsigned R, const Type *T, const Expr *P, @@ -1215,7 +1266,7 @@ const Stmt *SmackRep::inverseFPCastAssume(const StoreInst *si) { const Value *P = si->getPointerOperand(); const PointerType *PT = dyn_cast(P->getType()); assert(PT && "Expected pointer type."); - const Type *T = PT->getElementType(); + const Type *T = si->getValueOperand()->getType(); unsigned R = regions->idx(P); if (!T->isFloatingPointTy() || !regions->get(R).bytewiseAccess() || regions->get(R).isSingleton()) { @@ -1253,10 +1304,9 @@ Decl *SmackRep::getInitFuncs() { void SmackRep::addAllocSizeAttr(const llvm::GlobalVariable *G, std::list &ax) { - auto T = dyn_cast(G->getType()); - assert(T && "Global variables should have pointer types!"); - if (T->getElementType()->isSized()) { - auto allocSize = targetData->getTypeAllocSize(T->getElementType()); + auto T = G->getValueType(); + if (T->isSized()) { + auto allocSize = targetData->getTypeAllocSize(T); ax.push_back(Attr::attr("allocSize", allocSize)); } } @@ -1282,19 +1332,11 @@ std::list SmackRep::globalDecl(const llvm::GlobalValue *v) { const Constant *init = g->getInitializer(); unsigned numElems = numElements(init); - // NOTE: all global variables have pointer type in LLVM - if (const PointerType *t = dyn_cast(g->getType())) { - - // in case we can determine the size of the element type ... - if (t->getElementType()->isSized()) - size = storageSize(t->getElementType()); - - // otherwise (e.g. for function declarations), use a default size - else - size = 1024; - - } else - size = storageSize(g->getType()); + auto *t = g->getValueType(); + if (t->isSized()) + size = storageSize(t); + else + size = 1024; if (!g->hasName() || !STRING_CONSTANT.match(g->getName().str())) { if (numElems > 1) diff --git a/lib/smack/SplitAggregateValue.cpp b/lib/smack/SplitAggregateValue.cpp index 53b056a19..dbdadda8d 100644 --- a/lib/smack/SplitAggregateValue.cpp +++ b/lib/smack/SplitAggregateValue.cpp @@ -107,8 +107,8 @@ Value *SplitAggregateValue::splitAggregateLoad(Type *T, Value *P, for (auto &e : info) { IndexT idxs = std::get<0>(e); Value *p = irb.CreateGEP(T, P, ArrayRef(getFirsts(idxs))); - auto *load = irb.CreateLoad( - p->getType()->getScalarType()->getPointerElementType(), p); + auto *load = + irb.CreateLoad(cast(p)->getResultElementType(), p); markSplitAggregateAccess(load, checkWholeAccess); checkWholeAccess = false; V = irb.CreateInsertValue(V, load, ArrayRef(getSeconds(idxs))); @@ -125,7 +125,7 @@ void SplitAggregateValue::splitAggregateStore(Value *P, Value *V, IndexT idxs = std::get<0>(e); Constant *c = std::get<1>(e); std::vector vidxs = getFirsts(idxs); - Type *T = P->getType()->getScalarType()->getPointerElementType(); + Type *T = V->getType(); Value *p = irb.CreateGEP(T, P, ArrayRef(vidxs)); StoreInst *store; if (c) diff --git a/lib/smack/VectorOperations.cpp b/lib/smack/VectorOperations.cpp index dbcd7ae4f..fe773f78c 100644 --- a/lib/smack/VectorOperations.cpp +++ b/lib/smack/VectorOperations.cpp @@ -281,10 +281,9 @@ FuncDecl *VectorOperations::extract(Type *T, Type *IT) { return F; } -FuncDecl *VectorOperations::load(const Value *V) { +FuncDecl *VectorOperations::load(const Value *V, Type *ET) { auto PT = dyn_cast(V->getType()); assert(PT && "expected pointer type"); - auto ET = PT->getElementType(); type(ET); auto R = rep->regions->idx(V); @@ -301,10 +300,9 @@ FuncDecl *VectorOperations::load(const Value *V) { return F; } -FuncDecl *VectorOperations::store(const Value *V) { +FuncDecl *VectorOperations::store(const Value *V, Type *ET) { auto PT = dyn_cast(V->getType()); assert(PT && "expected pointer type"); - auto ET = PT->getElementType(); type(ET); auto R = rep->regions->idx(V); diff --git a/lib/utils/Devirt.cpp b/lib/utils/Devirt.cpp index 6afeab897..49f4cc597 100644 --- a/lib/utils/Devirt.cpp +++ b/lib/utils/Devirt.cpp @@ -58,11 +58,12 @@ castTo (Value * V, Type * Ty, std::string Name, Value * InsertPt) { if (V->getType() == Ty) return V; - // - // If it's a constant, just create a constant expression. - // + Instruction::CastOps Op = CastInst::getCastOpcode(V, false, Ty, false); + if (!CastInst::castIsValid(Op, V->getType(), Ty)) + return nullptr; + if (Constant * C = dyn_cast(V)) { - Constant * CE = ConstantExpr::getZExtOrBitCast (C, Ty); + Constant * CE = ConstantExpr::getCast(Op, C, Ty); return CE; } @@ -70,17 +71,19 @@ castTo (Value * V, Type * Ty, std::string Name, Value * InsertPt) { // Otherwise, insert a cast instruction. // if (auto I = dyn_cast(InsertPt)) - return CastInst::CreateZExtOrBitCast (V, Ty, Name, I); + return CastInst::Create(Op, V, Ty, Name, I); else if (auto B = dyn_cast(InsertPt)) - return CastInst::CreateZExtOrBitCast (V, Ty, Name, B); + return CastInst::Create(Op, V, Ty, Name, B); else llvm_unreachable("Unexpected insertion point."); } -static inline bool isZExtOrBitCastable(Value* V, Type* T) { - return CastInst::castIsValid(Instruction::ZExt, V->getType(), T) || - CastInst::castIsValid(Instruction::BitCast, V->getType(), T); +static inline bool isCastable(Value* V, Type* T) { + if (V->getType() == T) + return true; + Instruction::CastOps Op = CastInst::getCastOpcode(V, false, T, false); + return CastInst::castIsValid(Op, V->getType(), T); } static inline bool match(CallBase *CS, const Function &F) { @@ -102,7 +105,7 @@ static inline bool match(CallBase *CS, const Function &F) { for (unsigned i=0; igetArgOperand(i); auto PT = T->getParamType(i); - if (A->getType() != PT && !isZExtOrBitCastable(A, PT)) + if (!isCastable(A, PT)) return false; } @@ -120,7 +123,7 @@ static inline bool checkArgs(const CallBase *CS, const Function *F) { for (unsigned i=0; igetArgOperand(i); auto PT = T->getParamType(i+1); - if (A->getType() != PT && !isZExtOrBitCastable(A, PT)) + if (!isCastable(A, PT)) return false; } return true; @@ -163,9 +166,7 @@ Devirtualize::findInCache (const CallBase *CS, if (CS->getCalledOperand()->stripPointerCastsAndAliases()->getType() != PT) continue; - FunctionType* FT = dyn_cast(PT->getElementType()); - assert(FT); - if (FT->isVarArg() && !checkArgs(CS, bounceFunc)) + if (!checkArgs(CS, bounceFunc)) continue; // @@ -252,8 +253,14 @@ Devirtualize::buildBounce (CallBase *CS, std::vector& Targets) FunctionType::param_iterator T, TE; for (P = std::next(F->arg_begin()), PE = F->arg_end(), T = FT->param_begin(), TE = FT->param_end(); - P != PE && T != TE; ++P, ++T) - Args.push_back(castTo(&*P, *T, "", BL)); + P != PE && T != TE; ++P, ++T) { + Value *Arg = castTo(&*P, *T, "", BL); + if (!Arg) { + F->eraseFromParent(); + return nullptr; + } + Args.push_back(Arg); + } Value* directCall = CallInst::Create (const_cast(FL), Args, @@ -263,8 +270,14 @@ Devirtualize::buildBounce (CallBase *CS, std::vector& Targets) // Add the return instruction for the basic block if (CS->getType()->isVoidTy()) ReturnInst::Create (M->getContext(), BL); - else - ReturnInst::Create (M->getContext(), directCall, BL); + else { + Value *Ret = castTo(directCall, CS->getType(), "", BL); + if (!Ret) { + F->eraseFromParent(); + return nullptr; + } + ReturnInst::Create (M->getContext(), Ret, BL); + } } // @@ -293,6 +306,10 @@ Devirtualize::buildBounce (CallBase *CS, std::vector& Targets) // Type * VoidPtrType = getVoidPtrType (M->getContext()); Value * FArg = castTo (&*F->arg_begin(), VoidPtrType, "", InsertPt); + if (!FArg) { + F->eraseFromParent(); + return nullptr; + } BasicBlock * tailBB = failBB; for (unsigned index = 0; index < Targets.size(); ++index) { // @@ -303,6 +320,10 @@ Devirtualize::buildBounce (CallBase *CS, std::vector& Targets) VoidPtrType, "", InsertPt); + if (!TargetInt) { + F->eraseFromParent(); + return nullptr; + } // // Create a new basic block that compares the function pointer to the @@ -387,6 +408,8 @@ Devirtualize::makeDirectCall (CallBase *CS) { if (!NF) { // Build the bounce function and add it to the cache NF = buildBounce (CS, Targets); + if (!NF) + return; bounceCache[NF] = targetSet; } @@ -397,9 +420,11 @@ Devirtualize::makeDirectCall (CallBase *CS) { std::vector Params; Params.push_back(CI->getCalledOperand()); for (unsigned i=0; iarg_size(); i++) { - Params.push_back( - castTo(CI->getArgOperand(i), NF->getFunctionType()->getParamType(i+1), "", CS) - ); + Value *Arg = castTo(CI->getArgOperand(i), + NF->getFunctionType()->getParamType(i+1), "", CS); + if (!Arg) + return; + Params.push_back(Arg); } std::string name = CI->hasName() ? CI->getName().str() + ".dv" : ""; @@ -412,10 +437,13 @@ Devirtualize::makeDirectCall (CallBase *CS) { } else if (InvokeInst* CI = dyn_cast(CS)) { std::vector Params; Params.push_back(CI->getCalledOperand()); - for (unsigned i=0; iarg_size(); i++) - Params.push_back( - castTo(CI->getArgOperand(i), NF->getFunctionType()->getParamType(i+1), "", CS) - ); + for (unsigned i=0; iarg_size(); i++) { + Value *Arg = castTo(CI->getArgOperand(i), + NF->getFunctionType()->getParamType(i+1), "", CS); + if (!Arg) + return; + Params.push_back(Arg); + } std::string name = CI->hasName() ? CI->getName().str() + ".dv" : ""; InvokeInst* CN = InvokeInst::Create(const_cast(NF), CI->getNormalDest(), diff --git a/lib/utils/MergeGEP.cpp b/lib/utils/MergeGEP.cpp index 3f78f5221..ef268d562 100644 --- a/lib/utils/MergeGEP.cpp +++ b/lib/utils/MergeGEP.cpp @@ -120,16 +120,14 @@ static void simplifyGEP(GetElementPtrInst *GEP) { PtrOp->getName()+".sum",GEP); } - // Update the GEP in place if possible. if (Src->getNumOperands() == 2) { - GEP->setOperand(0, Src->getOperand(0)); - GEP->setOperand(1, Sum); - numMerged++; - return; + Indices.push_back(Sum); + Indices.append(GEP->op_begin()+2, GEP->op_end()); + } else { + Indices.append(Src->op_begin()+1, Src->op_end()-1); + Indices.push_back(Sum); + Indices.append(GEP->op_begin()+2, GEP->op_end()); } - Indices.append(Src->op_begin()+1, Src->op_end()-1); - Indices.push_back(Sum); - Indices.append(GEP->op_begin()+2, GEP->op_end()); } else if (isa(GEP->idx_begin()) && cast(GEP->idx_begin())->isNullValue() && Src->getNumOperands() != 1) { @@ -140,6 +138,8 @@ static void simplifyGEP(GetElementPtrInst *GEP) { if (!Indices.empty()){ Type *SourceElementType = Src->getSourceElementType(); + if (!GetElementPtrInst::getIndexedType(SourceElementType, Indices)) + return; GetElementPtrInst *GEPNew = (GEP->isInBounds() && Src->isInBounds()) ? GetElementPtrInst::CreateInBounds(SourceElementType, Src->getOperand(0), Indices, diff --git a/lib/utils/SimplifyExtractValue.cpp b/lib/utils/SimplifyExtractValue.cpp index 7a4c14fbf..9cadf2f8b 100644 --- a/lib/utils/SimplifyExtractValue.cpp +++ b/lib/utils/SimplifyExtractValue.cpp @@ -134,8 +134,8 @@ bool SimplifyEV::runOnModule(Module& M) { Indices.push_back(ConstantInt::get(Int32Ty, *I)); } - GetElementPtrInst *GEP = GetElementPtrInst::CreateInBounds(LI->getOperand(0)->getType()->getScalarType()->getPointerElementType(), - LI->getOperand(0), Indices, + GetElementPtrInst *GEP = GetElementPtrInst::CreateInBounds(LI->getType(), + LI->getOperand(0), Indices, LI->getName(), LI) ; LoadInst *LINew = new LoadInst(GEP->getResultElementType(), GEP, "", LI); EV->replaceAllUsesWith(LINew); diff --git a/lib/utils/SimplifyInsertValue.cpp b/lib/utils/SimplifyInsertValue.cpp index 44acc9391..2a4fff24a 100644 --- a/lib/utils/SimplifyInsertValue.cpp +++ b/lib/utils/SimplifyInsertValue.cpp @@ -80,8 +80,8 @@ bool SimplifyIV::runOnModule(Module& M) { I != E; ++I) { Indices.push_back(ConstantInt::get(Int32Ty, *I)); } - GetElementPtrInst *GEP = GetElementPtrInst::CreateInBounds(SI->getOperand(1)->getType()->getScalarType()->getPointerElementType(), - SI->getOperand(1), Indices, + GetElementPtrInst *GEP = GetElementPtrInst::CreateInBounds(SI->getValueOperand()->getType(), + SI->getOperand(1), Indices, SI->getName(), SI) ; new StoreInst(IV->getInsertedValueOperand(), GEP, SI); IV = dyn_cast(IV->getAggregateOperand()); diff --git a/sea-dsa b/sea-dsa index 78db35706..85ef2bd02 160000 --- a/sea-dsa +++ b/sea-dsa @@ -1 +1 @@ -Subproject commit 78db35706f1bed40758ae47b03b82eac5c5e9d39 +Subproject commit 85ef2bd020da46478fca616b5d6c91350528acb0 diff --git a/share/smack/include/smack.h b/share/smack/include/smack.h index e8136d17d..f7dfe5e69 100644 --- a/share/smack/include/smack.h +++ b/share/smack/include/smack.h @@ -24,8 +24,8 @@ extern "C" { #define __builtin_expect __builtinx_expect // For handling of va macros -void __builtinx_va_start(char *, char *); -void *__builtinx_va_arg(char *); +void __builtinx_va_start(__builtin_va_list, ...); +void *__builtinx_va_arg(__builtin_va_list); #endif void __SMACK_code(const char *fmt, ...); @@ -35,7 +35,7 @@ void __SMACK_top_decl(const char *fmt, ...); typedef struct smack_value { void *dummy; -} * smack_value_t; +} *smack_value_t; smack_value_t __SMACK_value(); smack_value_t __SMACK_values(void *ary, unsigned count); smack_value_t __SMACK_return_value(void); diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index 218fa0503..1e9f8e65a 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -33,7 +33,7 @@ * */ -void *__builtinx_va_arg(char *x) { +void *__builtinx_va_arg(__builtin_va_list x) { __SMACK_code("assume false;"); return 0; } diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py index 1650922bb..6f050266b 100644 --- a/share/smack/svcomp/utils.py +++ b/share/smack/svcomp/utils.py @@ -6,8 +6,47 @@ from shutil import copyfile import smack.top import smack.frontend +from smack.utils import temporary_file from .toSVCOMPformat import smackJsonToXmlGraph +def rewrite_nondet_int_pointer_assignments(input_file, args): + pointer_vars = set() + pointer_decl_re = re.compile(r'\*\s*([A-Za-z_]\w*)\s*(?=[,;=])') + assignment_re = re.compile( + r'^(\s*)([A-Za-z_]\w*)(\s*=\s*)' + r'(__VERIFIER_nondet_(?:u?int|unsigned_int|signed_int)\s*\(\s*\))' + r'(\s*;)') + + with open(input_file, 'r') as f: + lines = f.readlines() + + for line in lines: + if ';' not in line or '(' in line.split(';', 1)[0]: + continue + for match in pointer_decl_re.finditer(line): + pointer_vars.add(match.group(1)) + + changed = False + rewritten = [] + for line in lines: + match = assignment_re.match(line) + if match and match.group(2) in pointer_vars: + indent, lhs, assign, call, semi = match.groups() + line = '%s%s%s(__typeof__(%s))%s%s\n' % ( + indent, lhs, assign, lhs, call, semi) + changed = True + rewritten.append(line) + + if not changed: + return input_file + + _, ext = os.path.splitext(input_file) + rewritten_file = temporary_file(os.path.basename(input_file), ext, args) + with open(rewritten_file, 'w') as f: + f.write('#line 1 "%s"\n' % input_file.replace('\\', '\\\\').replace('"', '\\"')) + f.writelines(rewritten) + return rewritten_file + def svcomp_frontend(input_file, args): """Generate Boogie code from SVCOMP-style C-language source(s).""" @@ -42,7 +81,8 @@ def svcomp_frontend(input_file, args): # Ensure clang runs the preprocessor, even with .i extension. args.clang_options += " -x c" - bc = smack.frontend.clang_frontend(args.input_files[0], args) + svcomp_input = rewrite_nondet_int_pointer_assignments(args.input_files[0], args) + bc = smack.frontend.clang_frontend(svcomp_input, args) # run with no extra smack libraries libs = set() @@ -162,4 +202,3 @@ def write_error_file(args, status, verifier_output): if error is not None: with open(args.error_file, 'w') as f: f.write(error.decode('utf-8')) - diff --git a/test/llvm/inttoptr-i1.ll b/test/llvm/inttoptr-i1.ll new file mode 100644 index 000000000..349d11511 --- /dev/null +++ b/test/llvm/inttoptr-i1.ll @@ -0,0 +1,20 @@ +; @expect verified +; @checkbpl grep "function .*\$i2p\.i1\.ref" +; @checkbpl grep ":= \$i2p\.i1\.ref" + +source_filename = "inttoptr-i1" +target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +define i32 @main() { +entry: + %b = call i1 @__VERIFIER_nondet_bool() + %p = inttoptr i1 %b to ptr + call void @opaque_sink(ptr %p) + call void @__VERIFIER_assert(i32 1) + ret i32 0 +} + +declare i1 @__VERIFIER_nondet_bool() +declare void @opaque_sink(ptr) +declare void @__VERIFIER_assert(i32)