Skip to content

Commit

Permalink
fix: memhavoc should be mem def
Browse files Browse the repository at this point in the history
  • Loading branch information
@priyasiddharth
priyasiddharth committed Sep 17, 2023
1 parent 4faf58f commit aaaa30e
Showing 1 changed file with 36 additions and 35 deletions.
71 changes: 36 additions & 35 deletions lib/seadsa/ShadowMem.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -494,11 +494,12 @@ class ShadowMemImpl : public InstVisitor<ShadowMemImpl> {
CallInst &mkStoreFnCall(IRBuilder<> &B, const dsa::Cell &c, AllocaInst *v,
llvm::Optional<unsigned> bytes) {

auto *ci = mkShadowCall(B, c, m_memStoreFn,
{m_B->getInt32(getFieldId(c)),
m_B->CreateLoad(v->getType()->getPointerElementType(), v),
getUniqueScalar(*m_llvmCtx, B, c)},
"sm");
auto *ci =
mkShadowCall(B, c, m_memStoreFn,
{m_B->getInt32(getFieldId(c)),
m_B->CreateLoad(v->getType()->getPointerElementType(), v),
getUniqueScalar(*m_llvmCtx, B, c)},
"sm");
markDefCall(ci, bytes);
return *ci;
}
Expand Down Expand Up @@ -536,10 +537,11 @@ class ShadowMemImpl : public InstVisitor<ShadowMemImpl> {
mkShadowMemTrsfr(IRBuilder<> &B, const dsa::Cell &dst, const dsa::Cell &src,
llvm::Optional<unsigned> bytes) {
// insert memtrfr.load for the read access
auto *loadCI = mkShadowCall(B, src, m_memTrsfrLoadFn,
{B.getInt32(getFieldId(src)),
B.CreateLoad(m_Int32Ty, getShadowForField(src)),
getUniqueScalar(*m_llvmCtx, B, src)});
auto *loadCI =
mkShadowCall(B, src, m_memTrsfrLoadFn,
{B.getInt32(getFieldId(src)),
B.CreateLoad(m_Int32Ty, getShadowForField(src)),
getUniqueScalar(*m_llvmCtx, B, src)});
markUseCall(loadCI, bytes);

// insert normal mem.store for the write access
Expand All @@ -553,8 +555,8 @@ class ShadowMemImpl : public InstVisitor<ShadowMemImpl> {
unsigned id = getFieldId(c);
auto *ci =
mkShadowCall(B, c, m_argRefFn,
{B.getInt32(id), m_B->CreateLoad(m_Int32Ty, v), m_B->getInt32(idx),
getUniqueScalar(*m_llvmCtx, B, c)});
{B.getInt32(id), m_B->CreateLoad(m_Int32Ty, v),
m_B->getInt32(idx), getUniqueScalar(*m_llvmCtx, B, c)});
markUseCall(ci, bytes);
return *ci;
}
Expand All @@ -564,10 +566,11 @@ class ShadowMemImpl : public InstVisitor<ShadowMemImpl> {
AllocaInst *v = getShadowForField(c);
unsigned id = getFieldId(c);

auto *ci = mkShadowCall(B, c, argFn,
{B.getInt32(id), B.CreateLoad(m_Int32Ty, v), B.getInt32(idx),
getUniqueScalar(*m_llvmCtx, B, c)},
"sh");
auto *ci =
mkShadowCall(B, c, argFn,
{B.getInt32(id), B.CreateLoad(m_Int32Ty, v),
B.getInt32(idx), getUniqueScalar(*m_llvmCtx, B, c)},
"sh");

B.CreateStore(ci, v);
markDefCall(ci, bytes);
Expand All @@ -585,10 +588,11 @@ class ShadowMemImpl : public InstVisitor<ShadowMemImpl> {

CallInst &mkMarkOut(IRBuilder<> &B, const dsa::Cell &c, unsigned idx,
llvm::Optional<unsigned> bytes) {
auto *ci = mkShadowCall(
B, c, m_markOut,
{B.getInt32(getFieldId(c)), B.CreateLoad(m_Int32Ty, getShadowForField(c)),
B.getInt32(idx), getUniqueScalar(*m_llvmCtx, B, c)});
auto *ci =
mkShadowCall(B, c, m_markOut,
{B.getInt32(getFieldId(c)),
B.CreateLoad(m_Int32Ty, getShadowForField(c)),
B.getInt32(idx), getUniqueScalar(*m_llvmCtx, B, c)});
markUseCall(ci, bytes);
return *ci;
}
Expand Down Expand Up @@ -648,12 +652,12 @@ class ShadowMemImpl : public InstVisitor<ShadowMemImpl> {
bool mayClobber(CallInst &memDef, CallInst &memUse, AllocSitesCache &cache);

public:
ShadowMemImpl(dsa::GlobalAnalysis &dsa,
ShadowMemImpl(dsa::GlobalAnalysis &dsa,
TargetLibraryInfoWrapperPass &tliWrapper, CallGraph *cg,
Pass &pass, bool splitDsaNodes, bool computeReadMod,
bool memOptimizer, bool useTBAA, bool useSNAAA)
: m_dsa(dsa), m_tliWrapper(tliWrapper), m_dl(nullptr),
m_callGraph(cg), m_pass(pass), m_splitDsaNodes(splitDsaNodes),
: m_dsa(dsa), m_tliWrapper(tliWrapper), m_dl(nullptr), m_callGraph(cg),
m_pass(pass), m_splitDsaNodes(splitDsaNodes),
m_computeReadMod(computeReadMod), m_memOptimizer(memOptimizer),
m_useTBAA(useTBAA), m_useSNAAA(useSNAAA) {}

Expand Down Expand Up @@ -697,11 +701,8 @@ class ShadowMemImpl : public InstVisitor<ShadowMemImpl> {
void visitFree(CallBase &I);
void visitDsaCallSite(dsa::DsaCallSite &CS);

void
visitSetShadowMem(CallBase &CB);
void
visitGetShadowMem(CallBase &CB);

void visitSetShadowMem(CallBase &CB);
void visitGetShadowMem(CallBase &CB);

/// \brief Returns a reference to the global sea-dsa analysis.
GlobalAnalysis &getDsaAnalysis() { return m_dsa; }
Expand Down Expand Up @@ -934,7 +935,7 @@ bool ShadowMemImpl::runOnFunction(Function &F) {
if (exit->size() > 1) {
exit = llvm::SplitBlock(exit, ret,
// these two passes will not be preserved if null
(DominatorTree*)nullptr /*DominatorTree*/,
(DominatorTree *)nullptr /*DominatorTree*/,
nullptr /*LoopInfo*/);
ret = exit->getTerminator();
}
Expand Down Expand Up @@ -1080,7 +1081,6 @@ void ShadowMemImpl::visitCallBase(CallBase &I) {
!(callee->getName().startswith("seahorn.bounce")))
return;


LOG("shadow_cs", errs() << "Call: " << I << "\n";);

if (callee->getName().equals("calloc")) {
Expand All @@ -1104,12 +1104,12 @@ void ShadowMemImpl::visitCallBase(CallBase &I) {
}

if (callee->getName().equals("sea.set_shadowmem")) {
visitSetShadowMem(I);
visitSetShadowMem(I);
return;
}

if (callee->getName().equals("sea.get_shadowmem")) {
visitGetShadowMem(I);
visitGetShadowMem(I);
return;
}

Expand Down Expand Up @@ -1251,9 +1251,10 @@ void ShadowMemImpl::visitMemhavoc(CallBase &I) {
}

m_B->SetInsertPoint(&I);
CallInst &memUse =
mkShadowLoad(*m_B, cell, dsa::getTypeSizeInBytes(*ptr.getType(), *m_dl));
associateConcretePtr(memUse, ptr, &I);
CallInst &memDef = mkShadowStore(
*m_B, cell,
dsa::getTypeSizeInBytes(*ptr.getType(), *m_dl) /* bytes to access */);
associateConcretePtr(memDef, ptr, &I);
}

void ShadowMemImpl::visitIsModified(CallBase &I) {
Expand Down Expand Up @@ -1857,7 +1858,7 @@ void ShadowMemImpl::solveUses(Function &F) {
}

/** ShadowMem class **/
ShadowMem::ShadowMem(GlobalAnalysis &dsa, AllocSiteInfo &asi/*unused*/,
ShadowMem::ShadowMem(GlobalAnalysis &dsa, AllocSiteInfo &asi /*unused*/,
llvm::TargetLibraryInfoWrapperPass &tli,
llvm::CallGraph *cg, llvm::Pass &pass, bool splitDsaNodes,
bool computeReadMod, bool memOptimizer, bool useTBAA,
Expand Down

0 comments on commit aaaa30e

Please sign in to comment.