Skip to content

Commit

Permalink
added better handling of exceptions
Browse files Browse the repository at this point in the history
  • Loading branch information
danblitzhou committed Oct 18, 2019
1 parent b44f154 commit 7e45928
Show file tree
Hide file tree
Showing 3 changed files with 40 additions and 13 deletions.
2 changes: 1 addition & 1 deletion include/seahorn/BvOpSem2.hh
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ public:
/// \brief Deprecated
Expr lookup(SymStore &s, const Value &v) { llvm_unreachable(nullptr); }
/// Convert aggregate GenericValue to APInt
APInt agg(Type *ty, const std::vector<GenericValue> &elements,
Optional<APInt> agg(Type *ty, const std::vector<GenericValue> &elements,
seahorn::details::Bv2OpSemContext &ctx);
using gep_type_iterator = generic_gep_type_iterator<>;
/// \brief Returns symbolic representation of the gep offset
Expand Down
30 changes: 23 additions & 7 deletions lib/seahorn/BvOpSem2.cc
Original file line number Diff line number Diff line change
Expand Up @@ -1810,11 +1810,15 @@ Expr Bv2OpSemContext::getConstantValue(const llvm::Constant &c) {
if (GVO.hasValue()) {
GenericValue gv = GVO.getValue();
if (gv.AggregateVal.size() > 0) {
APInt aggBv = m_sem.agg(c.getType(), gv.AggregateVal, *this);
expr::mpz_class k = toMpz(aggBv);
return alu().si(k, aggBv.getBitWidth());
auto aggBvO = m_sem.agg(c.getType(), gv.AggregateVal, *this);
if (aggBvO.hasValue()) {
APInt aggBv = aggBvO.getValue();
expr::mpz_class k = toMpz(aggBv);
return alu().si(k, aggBv.getBitWidth());
}
}
}
LOG("opsem", WARN << "unhandled constant struct " << c;);
} else if (c.getType()->isPointerTy()) {
LOG("opsem", WARN << "unhandled constant pointer " << c;);
} else {
Expand Down Expand Up @@ -2218,7 +2222,7 @@ void Bv2OpSem::execBr(const BasicBlock &src, const BasicBlock &dst,
intraBr(ctx, dst);
}

APInt Bv2OpSem::agg(Type *aggTy, const std::vector<GenericValue> &elements,
Optional<APInt> Bv2OpSem::agg(Type *aggTy, const std::vector<GenericValue> &elements,
details::Bv2OpSemContext &ctx) {
APInt res;
APInt next;
Expand All @@ -2235,13 +2239,25 @@ APInt Bv2OpSem::agg(Type *aggTy, const std::vector<GenericValue> &elements,
if (ElmTy->isIntegerTy())
next = element.IntVal;
else if (ElmTy->isPointerTy()){
uint64_t ptrBv = reinterpret_cast<uint64_t>(element.PointerVal);
auto ptrBv = reinterpret_cast<intptr_t>(GVTOP(element));
next = APInt(getDataLayout().getTypeSizeInBits(ElmTy), ptrBv);
} else {
llvm_unreachable("Only support converting Int or Pointer in structs");
// this should be handled in constant evaluation step
LOG("opsem",
WARN << "Unsupported type " << *ElmTy << " to convert in aggregate. \n";);
llvm_unreachable("Only support converting Int or Pointer in aggregates");
return llvm::None;
}
} else {
next = agg(ElmTy, element.AggregateVal, ctx);
auto AIO = agg(ElmTy, element.AggregateVal, ctx);
if (AIO.hasValue())
next = AIO.getValue();
else {
LOG("opsem",
WARN << "Nested struct conversion failed \n";);
llvm_unreachable();
return llvm::None;
}
}
// Add padding to element
int elOffset = SL->getElementOffset(i);
Expand Down
21 changes: 16 additions & 5 deletions lib/seahorn/BvOpSem2ConstEval.cc
Original file line number Diff line number Diff line change
Expand Up @@ -508,7 +508,10 @@ Optional<GenericValue> ConstantExprEvaluator::evaluate(const Constant *C) {
auto *STy = dyn_cast<StructType>(C->getType());
auto *CS = dyn_cast<ConstantStruct>(C);
// XXX the cast might fail. this must be handled better
if (!CS || !STy) return llvm::None;
if (!CS || !STy) {
LOG("opsem", WARN << "Casting failed when trying to evaluate a struct! \n";);
return llvm::None;
}
unsigned int elemNum = STy->getNumElements();
Result.AggregateVal.resize(elemNum);
// try populate all elements in the struct
Expand All @@ -527,13 +530,21 @@ Optional<GenericValue> ConstantExprEvaluator::evaluate(const Constant *C) {
Result.AggregateVal[i].PointerVal = nullptr;
}
} else {
if (ElemTy->isIntegerTy())
Result.AggregateVal[i].IntVal = cast<ConstantInt>(OPI)->getValue();
else if (ElemTy->isAggregateType() || ElemTy->isPointerTy()) {
if (ElemTy->isAggregateType() ||
ElemTy->isIntegerTy() ||
ElemTy->isPointerTy()) {
auto val = evaluate(OPI);
if (val.hasValue())
Result.AggregateVal[i] = val.getValue();
else return llvm::None;
else {
LOG("opsem",
WARN << "Evaluating struct, no value set on this index:" << i << "\n";);
return llvm::None;
}
} else {
LOG("opsem",
WARN << "Unsupported element type " << *ElemTy << " in const struct. \n";);
return llvm::None;
}
}
}
Expand Down

0 comments on commit 7e45928

Please sign in to comment.