diff --git a/lib/seahorn/BvOpSem2.cc b/lib/seahorn/BvOpSem2.cc index 8836b2c94..e9c48169b 100644 --- a/lib/seahorn/BvOpSem2.cc +++ b/lib/seahorn/BvOpSem2.cc @@ -2229,10 +2229,19 @@ APInt Bv2OpSem::agg(Type *aggTy, const std::vector &elements, const StructLayout *SL = getDataLayout().getStructLayout(STy); for (int i = 0 ; i < elements.size(); i++) { const GenericValue element = elements[i]; + Type *ElmTy = STy->getElementType(i); if (element.AggregateVal.empty()) { - next = element.IntVal; - } else { // assuming only dealing with int as terminal struct element - next = agg(STy->getElementType(i), element.AggregateVal, ctx); + // Assuming only dealing with Int or Pointer as struct terminal elements + if (ElmTy->isIntegerTy()) + next = element.IntVal; + else if (ElmTy->isPointerTy()){ + uint64_t ptrBv = reinterpret_cast(element.PointerVal); + next = APInt(getDataLayout().getTypeSizeInBits(ElmTy), ptrBv); + } else { + llvm_unreachable("Only support converting Int or Pointer in structs"); + } + } else { + next = agg(ElmTy, element.AggregateVal, ctx); } // Add padding to element int elOffset = SL->getElementOffset(i); diff --git a/lib/seahorn/BvOpSem2ConstEval.cc b/lib/seahorn/BvOpSem2ConstEval.cc index f4cd5164d..fb88b2dc4 100644 --- a/lib/seahorn/BvOpSem2ConstEval.cc +++ b/lib/seahorn/BvOpSem2ConstEval.cc @@ -505,35 +505,35 @@ Optional ConstantExprEvaluator::evaluate(const Constant *C) { llvm_unreachable("Unknown constant pointer type!"); } break; case Type::StructTyID: { - if (auto *STy = dyn_cast(C->getType())) { - auto *CS = dyn_cast(C); - // XXX the cast might fail. this must be handled better - if (!CS) return llvm::None; - unsigned int elemNum = STy->getNumElements(); - Result.AggregateVal.resize(elemNum); - // try populate all elements in the struct - for (unsigned int i = 0; i < elemNum; ++i) { - Type *ElemTy = STy->getElementType(i); - Constant *OPI = CS->getOperand(i); - if (isa(OPI)) { - // if field not defined, just return default garbage - if (ElemTy->isIntegerTy()) - Result.AggregateVal[i].IntVal = - APInt(ElemTy->getPrimitiveSizeInBits(), 0); - else if (ElemTy->isAggregateType()) { - const Constant *ElemUndef = UndefValue::get(ElemTy); - Result.AggregateVal[i] = evaluate(ElemUndef).getValue(); - } - } else { - if (ElemTy->isIntegerTy()) - Result.AggregateVal[i].IntVal = - cast(OPI)->getValue(); - else if (ElemTy->isAggregateType()) { - auto val = evaluate(OPI); - if (val.hasValue()) - Result.AggregateVal[i] = val.getValue(); - else return llvm::None; - } + 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; + unsigned int elemNum = STy->getNumElements(); + Result.AggregateVal.resize(elemNum); + // try populate all elements in the struct + for (unsigned int i = 0; i < elemNum; ++i) { + Type *ElemTy = STy->getElementType(i); + Constant *OPI = CS->getOperand(i); + if (isa(OPI)) { + // if field not defined, just return default garbage + if (ElemTy->isIntegerTy()) { + Result.AggregateVal[i].IntVal = + APInt(ElemTy->getPrimitiveSizeInBits(), 0); + } else if (ElemTy->isAggregateType()) { + const Constant *ElemUndef = UndefValue::get(ElemTy); + Result.AggregateVal[i] = evaluate(ElemUndef).getValue(); + } else if (ElemTy->isPointerTy()) { + Result.AggregateVal[i].PointerVal = nullptr; + } + } else { + if (ElemTy->isIntegerTy()) + Result.AggregateVal[i].IntVal = cast(OPI)->getValue(); + else if (ElemTy->isAggregateType() || ElemTy->isPointerTy()) { + auto val = evaluate(OPI); + if (val.hasValue()) + Result.AggregateVal[i] = val.getValue(); + else return llvm::None; } } } diff --git a/test/opsem/insert.extract.03.ll b/test/opsem/insert.extract.value.03.ll similarity index 100% rename from test/opsem/insert.extract.03.ll rename to test/opsem/insert.extract.value.03.ll diff --git a/test/opsem/insert.extract.value.04.ll b/test/opsem/insert.extract.value.04.ll new file mode 100644 index 000000000..60c736b9b --- /dev/null +++ b/test/opsem/insert.extract.value.04.ll @@ -0,0 +1,53 @@ +; RUN: %seabmc "%s" 2>&1 | %oc %s +; RUN: %seabmc --horn-bv2-lambdas --log=opsem3 "%s" 2>&1 | %oc %s +;; testing struct with pointer type fields +;; extracting a pointer from struct +; CHECK: ^sat$ +; ModuleID = 'test-insert-value' +source_filename = "/tmp/st.c" +target datalayout = "e-m:o-p:32:32-f64:32:64-f80:128-n8:16:32-S128" +target triple = "i386-apple-macosx10.13.0" + +%struct.s = type { i16*, i32 } ; struct with a ptr to i16 and a i32 int +declare void @verifier.assume.not(i1) +declare void @seahorn.fail() + + +; Function Attrs: noreturn +declare void @verifier.error() #0 + +; Function Attrs: noinline nounwind ssp uwtable +define i32 @main() local_unnamed_addr #2 { +entry: + %p = alloca i16, align 4 + store i16 24, i16* %p + %st = insertvalue %struct.s undef, i16* %p, 0 + %sp = extractvalue %struct.s %st, 0 + %v2 = load i16, i16* %p + store i16 42, i16* %sp + %v1 = load i16, i16* %sp + %cond = icmp eq i16 %v1, %v2 + + call void @verifier.assume.not(i1 %cond) + br label %verifier.error + +verifier.error: ; preds = %entry + call void @seahorn.fail() + br label %verifier.error.split + +verifier.error.split: ; preds = %verifier.error + ret i32 42 +} + +attributes #0 = { noreturn } +attributes #1 = { argmemonly nounwind } +attributes #2 = { noinline nounwind ssp uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="penryn" "target-features"="+cx16,+fxsr,+mmx,+sse,+sse2,+sse3,+sse4.1,+ssse3,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #3 = { nounwind } + +!llvm.module.flags = !{!0, !1, !2} +!llvm.ident = !{!3} + +!0 = !{i32 1, !"NumRegisterParameters", i32 0} +!1 = !{i32 1, !"wchar_size", i32 4} +!2 = !{i32 7, !"PIC Level", i32 2} +!3 = !{!"clang version 5.0.2 (tags/RELEASE_502/final)"} diff --git a/test/opsem/insert.extract.value.05.ll b/test/opsem/insert.extract.value.05.ll new file mode 100644 index 000000000..6623d5c57 --- /dev/null +++ b/test/opsem/insert.extract.value.05.ll @@ -0,0 +1,51 @@ +; RUN: %seabmc "%s" 2>&1 | %oc %s +; RUN: %seabmc --horn-bv2-lambdas --log=opsem3 "%s" 2>&1 | %oc %s +;; testing struct with pointer type fields +;; extracting a pointer from struct +; CHECK: ^unsat$ +; ModuleID = 'test-insert-value' +source_filename = "/tmp/st.c" +target datalayout = "e-m:o-p:32:32-f64:32:64-f80:128-n8:16:32-S128" +target triple = "i386-apple-macosx10.13.0" + +%struct.s = type { i16*, i32 } ; struct with a ptr to i16 and a i32 int +declare void @verifier.assume.not(i1) +declare void @seahorn.fail() + + +; Function Attrs: noreturn +declare void @verifier.error() #0 + +; Function Attrs: noinline nounwind ssp uwtable +define i32 @main() local_unnamed_addr #2 { +entry: + %p = alloca i16, align 4 + store i16 24, i16* %p + %st = insertvalue %struct.s undef, i16* %p, 0 + %sp = extractvalue %struct.s %st, 0 + %v1 = load i16, i16* %sp + %v2 = load i16, i16* %p + %cond = icmp eq i16 %v1, %v2 + call void @verifier.assume.not(i1 %cond) + br label %verifier.error + +verifier.error: ; preds = %entry + call void @seahorn.fail() + br label %verifier.error.split + +verifier.error.split: ; preds = %verifier.error + ret i32 42 +} + +attributes #0 = { noreturn } +attributes #1 = { argmemonly nounwind } +attributes #2 = { noinline nounwind ssp uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="penryn" "target-features"="+cx16,+fxsr,+mmx,+sse,+sse2,+sse3,+sse4.1,+ssse3,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" } +attributes #3 = { nounwind } + +!llvm.module.flags = !{!0, !1, !2} +!llvm.ident = !{!3} + +!0 = !{i32 1, !"NumRegisterParameters", i32 0} +!1 = !{i32 1, !"wchar_size", i32 4} +!2 = !{i32 7, !"PIC Level", i32 2} +!3 = !{!"clang version 5.0.2 (tags/RELEASE_502/final)"}