[opsem]added handling of pointer type in struct; added tests

lib/seahorn/BvOpSem2.cc

@@ -2229,10 +2229,19 @@ APInt Bv2OpSem::agg(Type *aggTy, const std::vector<GenericValue> &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<uint64_t>(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);

lib/seahorn/BvOpSem2ConstEval.cc

@@ -505,35 +505,35 @@ Optional<GenericValue> ConstantExprEvaluator::evaluate(const Constant *C) {
     llvm_unreachable("Unknown constant pointer type!");
   } break;
   case Type::StructTyID: {
-    if (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) 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<UndefValue>(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<ConstantInt>(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<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;
+    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<UndefValue>(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<ConstantInt>(OPI)->getValue();
+        else if (ElemTy->isAggregateType() || ElemTy->isPointerTy()) {
+          auto val = evaluate(OPI);
+          if (val.hasValue())
+            Result.AggregateVal[i] = val.getValue();
+          else return llvm::None;
         }
       }
     }

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)"}

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)"}