diff --git a/include/seahorn/BvOpSem2.hh b/include/seahorn/BvOpSem2.hh index 084913be2..e21471395 100644 --- a/include/seahorn/BvOpSem2.hh +++ b/include/seahorn/BvOpSem2.hh @@ -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 &elements, + Optional agg(Type *ty, const std::vector &elements, seahorn::details::Bv2OpSemContext &ctx); using gep_type_iterator = generic_gep_type_iterator<>; /// \brief Returns symbolic representation of the gep offset diff --git a/lib/seahorn/BvOpSem2.cc b/lib/seahorn/BvOpSem2.cc index e9c48169b..ff4b8e5d2 100644 --- a/lib/seahorn/BvOpSem2.cc +++ b/lib/seahorn/BvOpSem2.cc @@ -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 { @@ -2218,7 +2222,7 @@ void Bv2OpSem::execBr(const BasicBlock &src, const BasicBlock &dst, intraBr(ctx, dst); } -APInt Bv2OpSem::agg(Type *aggTy, const std::vector &elements, +Optional Bv2OpSem::agg(Type *aggTy, const std::vector &elements, details::Bv2OpSemContext &ctx) { APInt res; APInt next; @@ -2235,13 +2239,25 @@ APInt Bv2OpSem::agg(Type *aggTy, const std::vector &elements, if (ElmTy->isIntegerTy()) next = element.IntVal; else if (ElmTy->isPointerTy()){ - uint64_t ptrBv = reinterpret_cast(element.PointerVal); + auto ptrBv = reinterpret_cast(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); diff --git a/lib/seahorn/BvOpSem2ConstEval.cc b/lib/seahorn/BvOpSem2ConstEval.cc index fb88b2dc4..bcb9acb80 100644 --- a/lib/seahorn/BvOpSem2ConstEval.cc +++ b/lib/seahorn/BvOpSem2ConstEval.cc @@ -508,7 +508,10 @@ Optional ConstantExprEvaluator::evaluate(const Constant *C) { auto *STy = dyn_cast(C->getType()); auto *CS = dyn_cast(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 @@ -527,13 +530,21 @@ Optional ConstantExprEvaluator::evaluate(const Constant *C) { Result.AggregateVal[i].PointerVal = nullptr; } } else { - if (ElemTy->isIntegerTy()) - Result.AggregateVal[i].IntVal = cast(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; } } }