-
Notifications
You must be signed in to change notification settings - Fork 131
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(opsem): use memmssa api to define memin, memout reg for bvopsem2 #304
base: dev10
Are you sure you want to change the base?
Conversation
793d714
to
4c2b69e
Compare
include/seahorn/BvOpSem2.hh
Outdated
|
||
public: | ||
Bv2OpSem(ExprFactory &efac, Pass &pass, const DataLayout &dl, | ||
TrackLevel trackLvl = MEM); | ||
Bv2OpSem(ExprFactory &efac, Pass &pass, seadsa::SeaMemorySSA *smssa, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
pass by const reference
lib/seahorn/BvOpSem2.cc
Outdated
if (UseMemSSA) { | ||
seadsa::SeaMemoryAccess *ma = | ||
m_sem.getSeaMemSSA().getMemoryAccessForShadow(&inst); | ||
if (auto *pMemUse = dyn_cast<seadsa::SeaMemoryUse>(ma)) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
assert(isa<seadsa::SeaMemoryUse>(ma));
auto *pMemUse = cast<seadsa::SeaMemoryUse>(ma);
lib/seahorn/BvOpSem2.cc
Outdated
m_ctx.setMemTrsfrReadReg(reg); | ||
m_ctx.setMemScalar(false /* TODO: Make this work */); | ||
} else { | ||
LOG("opsem", errs() << "Expected load but sea-dsa does not agree!\n"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
same as prior comment. turn into assert
lib/seahorn/BvOpSem2.cc
Outdated
m_ctx.setMemWriteRegister(memOut); | ||
m_ctx.setMemScalar(false /* TODO: Make this work */); | ||
} else { | ||
LOG("opsem", errs() |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
assert, same as before
if (Expr r = getRegister(access)) { | ||
return r; | ||
} | ||
Expr reg; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
add a comment about handling unique scalars
@@ -553,7 +554,7 @@ public: | |||
virtual PtrSortTy mkPtrRegisterSort(const GlobalVariable &gv) const = 0; | |||
|
|||
/// \brief Returns sort of memory-holding register for an instruction | |||
virtual MemSortTy mkMemRegisterSort(const Instruction &inst) const = 0; | |||
virtual Expr mkMemRegisterSort(const Value &value) const = 0; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
return type should be MemSortTy
. Comment needs to be updated because it talks about instruction.
I would prefer to to not have mkMemRegisterSort
for Value
. It is easy to abuse and get wrong
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok, I see why you are using Value
. Add assertions to make sure that only MemSSA
or Instruciton
are allowed as arguments and nothing else.
Use seamemoryaccess objects to point to the right memory aaray to use instead of relying on shadowmem calls. Currently we use the shadowmem calss as keyto get to seamemoryaccess objects. Also added seamemoryaccess as a terminal
4c2b69e
to
f2d0f95
Compare
Use seamemoryaccess objects to point to the right memory aaray to use instead of relying on shadowmem calls. Currently we use the shadowmem calss as keyto get to seamemoryaccess objects. Also added seamemoryaccess as a terminal