[analyzer] Rework SValBuilder::evalCast function into maintainable and clear way

[ASDenysPetrov]

Summary

Refactor SValBuilder::evalCast function. Make the function clear and get rid of redundant and repetitive code. Unite SValBuilder::evalCast, SimpleSValBuilder::dispatchCast, SimpleSValBuilder::evalCastFromNonLoc and SimpleSValBuilder::evalCastFromLoc functions into single SValBuilder::evalCast.

P.S. Inspired by D89055.

Now I'm going to make unittests for SValBuilder::evalCast. Let me ask you to offer me some examples of casts to check. As many cases we can collect as robust the test would be. E.g.

int x; // case 1
float y;
x = y;

int x; // case 2
(void)x;
...

[martong]

Now I'm going to make unittests for SValBuilder::evalCast. Let me ask you to offer me some examples of casts to check. As many cases we can collect as robust the test would be. E.g.

This is not going to be easy. I guess we should cover both implicit and explicit type conversions. C++ is ridiculously complex in these domains. For maximal precision I'd suggest to systematically go through the below pages and try to cover each major case:
https://en.cppreference.com/w/cpp/language/explicit_cast
https://en.cppreference.com/w/cpp/language/implicit_conversion

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h

105

+1 for this kind of splitting, makes the code cleaner for me.

[steakhal]

In D90157#2356170, @martong wrote:

Now I'm going to make unittests for SValBuilder::evalCast. Let me ask you to offer me some examples of casts to check. As many cases we can collect as robust the test would be. E.g.

This is not going to be easy. I guess we should cover both implicit and explicit type conversions. C++ is ridiculously complex in these domains. For maximal precision I'd suggest to systematically go through the below pages and try to cover each major case:
https://en.cppreference.com/w/cpp/language/explicit_cast
https://en.cppreference.com/w/cpp/language/implicit_conversion

@martong Keep in mind that we try hard not to emit casts - even if that would require. Check D85528, exactly touching this topic.

---

By the same token, I think you should run the test-suite using the Z3 refutation and/or Z3 constraint solver to check if this introduces any regression.
You can do that by installing Z3, adding the cmake options: -DLLVM_ENABLE_Z3_SOLVER=ON, -DLLVM_Z3_INSTALL_DIR=/path/to/z3
After this, you should be able to run the lit-test:
./bin/llvm-lit -sv --show-unsupported --show-xfail /home/elnbbea/git/llvm-project/clang/test/Analysis --param USE_Z3_SOLVER=1
Run it before and after your fix and you should expect no new failures/crashes.

[ASDenysPetrov]

Who can confirm if this is correct or somewhere it needs fixes? Here is a generated result of evalCast from the origin branch(before the patch):

void foo(int* x,  // &SymRegion{reg_$0<int * x>}
         int** y, // &SymRegion{reg_$1<int ** y>}
         int***z) // &SymRegion{reg_$2<int *** z>}
{
 (void*)x;    // &SymRegion{reg_$0<int * x>}
 (void*)y;    // &SymRegion{reg_$1<int ** y>}
 (void*)z;    // &SymRegion{reg_$2<int *** z>}
 (void**)x;   // &Element{SymRegion{reg_$0<int * x>},0 S64b,void *}
 (void**)y;   // &SymRegion{reg_$1<int ** y>}
 (void**)z;   // &SymRegion{reg_$2<int *** z>}
 (void***)x;  // &Element{SymRegion{reg_$0<int * x>},0 S64b,void **}
 (void***)y;  // &Element{SymRegion{reg_$1<int ** y>},0 S64b,void **}
 (void***)z;  // &SymRegion{reg_$2<int *** z>}
 (void****)x; // &Element{SymRegion{reg_$0<int * x>},0 S64b,void ***}
 (void****)y; // &Element{SymRegion{reg_$1<int ** y>},0 S64b,void ***}
 (void****)z; // &Element{SymRegion{reg_$2<int *** z>},0 S64b,void ***}
}

@martong

https://en.cppreference.com/w/cpp/language/explicit_cast
https://en.cppreference.com/w/cpp/language/implicit_conversion

Thanks for the links.
@steakhal

By the same token, I think you should run the test-suite using the Z3 refutation and/or Z3 constraint solver to check if this introduces any regression.

Never worked with Z3 before. I'll try.

[steakhal]

In D90157#2361773, @ASDenysPetrov wrote:

Who can confirm if this is correct or somewhere it needs fixes? Here is a generated result of evalCast from the origin branch(before the patch):

void foo(int* x,  // &SymRegion{reg_$0<int * x>}
         int** y, // &SymRegion{reg_$1<int ** y>}
         int***z) // &SymRegion{reg_$2<int *** z>}
{
 (void*)x;    // &SymRegion{reg_$0<int * x>}
 (void*)y;    // &SymRegion{reg_$1<int ** y>}
 (void*)z;    // &SymRegion{reg_$2<int *** z>}
 (void**)x;   // &Element{SymRegion{reg_$0<int * x>},0 S64b,void *}
 (void**)y;   // &SymRegion{reg_$1<int ** y>}
 (void**)z;   // &SymRegion{reg_$2<int *** z>}
 (void***)x;  // &Element{SymRegion{reg_$0<int * x>},0 S64b,void **}
 (void***)y;  // &Element{SymRegion{reg_$1<int ** y>},0 S64b,void **}
 (void***)z;  // &SymRegion{reg_$2<int *** z>}
 (void****)x; // &Element{SymRegion{reg_$0<int * x>},0 S64b,void ***}
 (void****)y; // &Element{SymRegion{reg_$1<int ** y>},0 S64b,void ***}
 (void****)z; // &Element{SymRegion{reg_$2<int *** z>},0 S64b,void ***}
}

AFAIK, Element regions represent the reinterpret casts, and static-casts doesn't require anything to do as the loading from the region would be cast to the appropriate type.
So these dumps seem to be correct.

BTW, this dispatching logic should be done with an SValVisitor IMO. That way you could make it even more cleaner. @ASDenysPetrov

@steakhal

By the same token, I think you should run the test-suite using the Z3 refutation and/or Z3 constraint solver to check if this introduces any regression.

Never worked with Z3 before. I'll try.

---

I've run the baseline and your patch as well on 15 projects, both with and without Z3 refutation enabled.

The reports for these 13 projects did not change at all:

Bitcoin_v0.20.1
Curl_curl-7_66_0
Memchached_1.6.8
OpenSSL_openssl-3.0.0-alpha7
PostgreSQL_REL_13_0
Redis_5.0.6
SQLite_version-3.33.0
TinyXML2_8.0.0
Vim_v8.2.1920
Xerces_v3.2.3
libWebM_libwebm-1.0.0.27
protobuf_v3.13.0
tmux_3.0

However, for twin, it introduced a new unique report:

server/socketalien.h @ Line 64	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound

And for the FFMPEG, 2 unique reports were lost without Z3 refutation:

vf_edgedetect.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
mpc8.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound

3 unique reports were lost with Z3 refutation:

utvideodec.c 	7th function call argument is an uninitialized value 	core.CallAndMessage
utvideodec.c 	The left operand of '-' is a garbage value 	core.UndefinedBinaryOperatorResult
xan.c 	Arguments must not be overlapping buffers 	alpha.unix.cstring.BufferOverlap

And introduced 35 unique new ones without Z3 refutation, only 34 with refutation:

lpc.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound   (Z3 refutation filters this)
on2avc.c 	Memory copy function accesses out-of-bound array element 	alpha.unix.cstring.OutOfBounds
bytestream.h 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
ws-snd1.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264qpel_template.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
des.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
012v.c 	Memory copy function accesses out-of-bound array element 	alpha.unix.cstring.OutOfBounds
012v.c 	Memory copy function accesses out-of-bound array element 	alpha.unix.cstring.OutOfBounds
brenderpix.c 	Division by zero 	core.DivideZero
h264_cavlc.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
h264_cavlc.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
bytestream.h 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
rtpenc_h263.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
rtpenc_h263.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound
avc.c 	Access out-of-bound array element (buffer overflow) 	alpha.security.ArrayBound

All in all, I'm still in favor of this change, but I'm really curious why did we observe such changes. Debugging the cause seems really tricky to me.
Maybe dumping the exploded graph in both cases and diffing them could show something useful to narrow this down the problem space to a pair of states.
What do you think @ASDenysPetrov ?

[ASDenysPetrov]

@steakhal
Thank you for your invaluable analysis!

What do you think @ASDenysPetrov ?

I think if there is any difference then I have to inspect the changes deeper. I tryed to make this changes in a way of not changing any behaviour.
Let me back to this patch a bit later. Currently have another important task.

[ASDenysPetrov]

@steakhal
I've precisely inspected your reports and find the bug. I've fixed it. I also verified all the rest and find some other vulnerabilities and fixed them as well.
Thank you for your testing, and I would ask you to run these tests again on my fix.

[ASDenysPetrov]

Thank to @steakhal for the new tests.
All previous result differences have gone in FFMPEG and twin but a new one appeared in PostgreSQL.

/src/common/d2s.c  Line 895 Memory copy function overflows the destination buffer alpha.unix.cstring.OutOfBounds

Here is an original link to the report: https://codechecker-demo.eastus.cloudapp.azure.com/Default?run=D90157&items-per-page=100 (login: demo, pass: demo)

I'm going to work on the patch to remove this single difference.

[ASDenysPetrov]

Unfortunately I wasn't able to reproduce the singe difference in PostgreSQL project. So I revised the patch in a part of the difference nature.
This update passed all of CodeChecker's tests without any difference.
So for now the patch looks like ready to be accepted.
Please, welcome for review.

[steakhal]

Please @ASDenysPetrov, give full context with the option -U99999999 when you export the diff from git.
I would like to quickly swipe through the code before I accept this.

[ASDenysPetrov]

@steakhal
Oh, sure. Updated.

[steakhal]

What you are basically doing is a visitation on the kind of the SVal.
Why don't you use the SValVisitor instead? That way you could focus on the leaf nodes in the hierarchy, leaving you an even cleaner solution.

class CastEvaluator : public SValVisitor<CastEvaluator, SVal> {
public:
  CastEvaluator(QualType CastTy, QualType OriginalTy /*etc.*/)
  SVal VisitPointerToMember(nonloc::PointerToMember V) { return V; }
  SVal VisitGotoLabel(loc::GotoLabel V) { /*impl.*/ }
  /* etc. */
};

Comments should be punctuated and the variables should start with an uppercase letter in general.
About the correctness: I think it still needs a bit more confidence. I'm gonna run this on LLVM itself and see if anything changes.

I really like where this is going. Keep up the good work.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h

105–127

Why are all of these public?
I would expect only the first overload to be public.

clang/lib/StaticAnalyzer/Core/SValBuilder.cpp

642–686

Arrays decay to a pointer to the first element, but in this case, you return Unknown.
Why?

675–676

nit

746–750

Just call immediately that lambda and assign that value to a const llvm::APSInt CastedValue.

836–839

Presumably what?

[ASDenysPetrov]

@steakhal

Why don't you use the SValVisitor instead?

I simply didn't know of its exsistence. We can try to transform this patch using SValVisitor in the next revision to make the review easier and avoid additional complexity.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h

105–127

Great catch. I'll do it.

clang/lib/StaticAnalyzer/Core/SValBuilder.cpp

642–686

This is just how evalCast worked before the patch. I didn't think of why. I've just tried to replicate previous cast logic. If I'd change anything, you'd catch a bunch of differences in CodeChecker. That's what I didn't want the most.

675–676

Thanks! I'll check all for the naming rules.

746–750

I just wanted to make this lazy. Otherwise this set of calls will be invoked unnecessarily in some cases. I'd prefer to leave it as it is.

836–839

We assume that this condition presents a type which is opposite to float (aka non-float). But it may happen that it is also opposite to some other types. So naming it non-float could be a bit incomplete and we are dealing with some other type. Yes, I feel this embarrassing. I'll remove (presumably).

[steakhal]

clang/lib/StaticAnalyzer/Core/SValBuilder.cpp

642–686

I agree, you should not change any behavior in this patch.

746–750

Maybe rename it then. What about GetCastedValue(x)?

[ASDenysPetrov]

Updated. Naming fixes. Member access changes.

[steakhal]

In D90157#2519800, @ASDenysPetrov wrote:

Updated. Naming fixes. Member access changes.

Looks great!

IMO we are sort-of late to commit this into clang-12 with confidence.
We should land it after we tag that release.
What do you think @xazax.hun?

[ASDenysPetrov]

Hi, guys!
Does anyone can review this item, except @steakhal (thanks him)? Please, look.

[NoQ]

I'm catching up and these changes look great.

In D90157#2433657, @steakhal wrote:

I've run the baseline and your patch as well on 15 projects, both with and without Z3 refutation enabled.
(...)
All in all, I'm still in favor of this change, but I'm really curious why did we observe such changes. Debugging the cause seems really tricky to me.

If testing on a large codebase uncovered changes in behavior that weren't caught by our LIT test suite it often make sense to update our LIT test suite to include those tests in order to avoid similar regressions in the future. Regressions like this are easy to auto-reduce with tools like creduce because there's no functional change intended in the patch so there's a 100% formal reduction criterion "any change in diagnostics is observed" which can be easily fed to creduce. Even though NFC commits don't require tests, this doesn't mean they shouldn't add them!

[ASDenysPetrov]

@NoQ

Even though NFC commits don't require tests, this doesn't mean they shouldn't add them!

While developing this, I wasn't able to reproduce any regression or unpassed cases on the projects from CodeChecker list (Bitcoin_v0.20.1, Curl_curl-7_66_0, Memchached_1.6.8, OpenSSL_openssl-3.0.0-alpha7, etc.) due to my platform. I use Windows and those projects either don't compile or need hard effort to set them up.
But anyway I was able to detect some different diagnostics in existing tests casts.cpp using Z3 refutation option. That actually helped to make corrections.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h

public:
   bool haveSameType(QualType Ty1, QualType Ty2) {
     // FIXME: Remove the second disjunct when we support symbolic
     // truncation/extension.
     return (Context.getCanonicalType(Ty1) == Context.getCanonicalType(Ty2) ||
             (Ty1->isIntegralOrEnumerationType() &&
              Ty2->isIntegralOrEnumerationType()));
   }
 
-  SVal evalCast(SVal val, QualType castTy, QualType originalType);
+  SVal evalCast(SVal V, QualType CastTy, QualType OriginalTy);
+  SVal evalCastKind(UndefinedVal V, QualType CastTy, QualType OriginalTy);
+  SVal evalCastKind(UnknownVal V, QualType CastTy, QualType OriginalTy);
+  SVal evalCastKind(Loc V, QualType CastTy, QualType OriginalTy);
+  SVal evalCastKind(NonLoc V, QualType CastTy, QualType OriginalTy);
+  SVal evalCastSubKind(loc::ConcreteInt V, QualType CastTy,
+                       QualType OriginalTy);
+  SVal evalCastSubKind(loc::GotoLabel V, QualType CastTy, QualType OriginalTy);
+  SVal evalCastSubKind(loc::MemRegionVal V, QualType CastTy,
+                       QualType OriginalTy);
+  SVal evalCastSubKind(nonloc::CompoundVal V, QualType CastTy,
+                       QualType OriginalTy);
+  SVal evalCastSubKind(nonloc::ConcreteInt V, QualType CastTy,
+                       QualType OriginalTy);
+  SVal evalCastSubKind(nonloc::LazyCompoundVal V, QualType CastTy,
+                       QualType OriginalTy);
+  SVal evalCastSubKind(nonloc::LocAsInteger V, QualType CastTy,
+                       QualType OriginalTy);
+  SVal evalCastSubKind(nonloc::SymbolVal V, QualType CastTy,
+                       QualType OriginalTy);
+  SVal evalCastSubKind(nonloc::PointerToMember V, QualType CastTy,
+                       QualType OriginalTy);
 
   // Handles casts of type CK_IntegralCast.
   SVal evalIntegralCast(ProgramStateRef state, SVal val, QualType castTy,
                         QualType originalType);
 
   virtual SVal evalMinus(NonLoc val) = 0;
 
   virtual SVal evalComplement(NonLoc val) = 0;
 

clang/lib/StaticAnalyzer/Core/SValBuilder.cpp

SVal SValBuilder::evalIntegralCast(ProgramStateRef state, SVal val,
   if (!IsNotTruncated && IsTruncated) {
     // Symbol is truncated so we evaluate it as a cast.
     NonLoc CastVal = makeNonLoc(se, originalTy, castTy);
     return CastVal;
   }
   return evalCast(val, castTy, originalTy);
 }
 
-// FIXME: should rewrite according to the cast kind.
-SVal SValBuilder::evalCast(SVal val, QualType castTy, QualType originalTy) {
-  castTy = Context.getCanonicalType(castTy);
-  originalTy = Context.getCanonicalType(originalTy);
-  if (val.isUnknownOrUndef() || castTy == originalTy)
-    return val;
+//===----------------------------------------------------------------------===//
+// Cast methods.
+// `evalCast` is the main method
+// `evalCastKind` and `evalCastSubKind` are helpers
+//===----------------------------------------------------------------------===//
 
-  if (castTy->isBooleanType()) {
-    if (val.isUnknownOrUndef())
-      return val;
-    if (val.isConstant())
-      return makeTruthVal(!val.isZeroConstant(), castTy);
-    if (!Loc::isLocType(originalTy) &&
-        !originalTy->isIntegralOrEnumerationType() &&
-        !originalTy->isMemberPointerType())
-      return UnknownVal();
-    if (SymbolRef Sym = val.getAsSymbol(true)) {
-      BasicValueFactory &BVF = getBasicValueFactory();
-      // FIXME: If we had a state here, we could see if the symbol is known to
-      // be zero, but we don't.
-      return makeNonLoc(Sym, BO_NE, BVF.getValue(0, Sym->getType()), castTy);
-    }
-    // Loc values are not always true, they could be weakly linked functions.
-    if (Optional<Loc> L = val.getAs<Loc>())
-      return evalCastFromLoc(*L, castTy);
+SVal SValBuilder::evalCast(SVal V, QualType CastTy, QualType OriginalTy) {
+  // FIXME: Move this check to the most appropriate evalCastKind/evalCastSubKind
+  // function.
+  // For const casts, casts to void, just propagate the value.
+  if (!CastTy->isVariableArrayType() && !OriginalTy->isVariableArrayType())
+    if (shouldBeModeledWithNoOp(Context, Context.getPointerType(CastTy),
+                                Context.getPointerType(OriginalTy)))
+      return V;
+
+  // Cast SVal according to kinds.
+  switch (V.getBaseKind()) {
+  case SVal::UndefinedValKind:
+    return evalCastKind(V.castAs<UndefinedVal>(), CastTy, OriginalTy);
+  case SVal::UnknownValKind:
+    return evalCastKind(V.castAs<UnknownVal>(), CastTy, OriginalTy);
+  case SVal::LocKind:
+    return evalCastKind(V.castAs<Loc>(), CastTy, OriginalTy);
+  case SVal::NonLocKind:
+    return evalCastKind(V.castAs<NonLoc>(), CastTy, OriginalTy);
+  default:
+    llvm_unreachable("Unknown SVal kind");
+  }
+}
 
-    Loc L = val.castAs<nonloc::LocAsInteger>().getLoc();
-    return evalCastFromLoc(L, castTy);
-  }
+SVal SValBuilder::evalCastKind(UndefinedVal V, QualType CastTy,
+                               QualType OriginalTy) {
+  return V;
 
-  // For const casts, casts to void, just propagate the value.
-  if (!castTy->isVariableArrayType() && !originalTy->isVariableArrayType())
-    if (shouldBeModeledWithNoOp(Context, Context.getPointerType(castTy),
-                                         Context.getPointerType(originalTy)))
-      return val;
+SVal SValBuilder::evalCastKind(UnknownVal V, QualType CastTy,
+                               QualType OriginalTy) {
+  return V;
+}
+
+SVal SValBuilder::evalCastKind(Loc V, QualType CastTy, QualType OriginalTy) {
+  switch (V.getSubKind()) {
+  case loc::ConcreteIntKind:
+    return evalCastSubKind(V.castAs<loc::ConcreteInt>(), CastTy, OriginalTy);
+  case loc::GotoLabelKind:
+    return evalCastSubKind(V.castAs<loc::GotoLabel>(), CastTy, OriginalTy);
+  case loc::MemRegionValKind:
+    return evalCastSubKind(V.castAs<loc::MemRegionVal>(), CastTy, OriginalTy);
+  default:
+    llvm_unreachable("Unknown SVal kind");
+  }
+}
 
-  // Check for casts from pointers to integers.
-  if (castTy->isIntegralOrEnumerationType() && Loc::isLocType(originalTy))
-    return evalCastFromLoc(val.castAs<Loc>(), castTy);
-
-  // Check for casts from integers to pointers.
-  if (Loc::isLocType(castTy) && originalTy->isIntegralOrEnumerationType()) {
-    if (Optional<nonloc::LocAsInteger> LV = val.getAs<nonloc::LocAsInteger>()) {
-      if (const MemRegion *R = LV->getLoc().getAsRegion()) {
-        StoreManager &storeMgr = StateMgr.getStoreManager();
-        R = storeMgr.castRegion(R, castTy);
-        return R ? SVal(loc::MemRegionVal(R)) : UnknownVal();
-      }
-      return LV->getLoc();
-    }
-    return dispatchCast(val, castTy);
+SVal SValBuilder::evalCastKind(NonLoc V, QualType CastTy, QualType OriginalTy) {
+  switch (V.getSubKind()) {
+  case nonloc::CompoundValKind:
+    return evalCastSubKind(V.castAs<nonloc::CompoundVal>(), CastTy, OriginalTy);
+  case nonloc::ConcreteIntKind:
+    return evalCastSubKind(V.castAs<nonloc::ConcreteInt>(), CastTy, OriginalTy);
+  case nonloc::LazyCompoundValKind:
+    return evalCastSubKind(V.castAs<nonloc::LazyCompoundVal>(), CastTy,
+                           OriginalTy);
+  case nonloc::LocAsIntegerKind:
+    return evalCastSubKind(V.castAs<nonloc::LocAsInteger>(), CastTy,
+                           OriginalTy);
+  case nonloc::SymbolValKind:
+    return evalCastSubKind(V.castAs<nonloc::SymbolVal>(), CastTy, OriginalTy);
+  case nonloc::PointerToMemberKind:
+    return evalCastSubKind(V.castAs<nonloc::PointerToMember>(), CastTy,
+                           OriginalTy);
+  default:
+    llvm_unreachable("Unknown SVal kind");
+
+SVal SValBuilder::evalCastSubKind(loc::ConcreteInt V, QualType CastTy,
+                                  QualType OriginalTy) {
+  // Pointer to bool.
+  if (CastTy->isBooleanType())
+    return makeTruthVal(V.getValue().getBoolValue(), CastTy);
+
+  // Pointer to integer.
+  if (CastTy->isIntegralOrEnumerationType()) {
+    llvm::APSInt value = V.getValue();
+    BasicVals.getAPSIntType(CastTy).apply(value);
+    return makeIntVal(value);
   }
 
-  // Just pass through function and block pointers.
-  if (originalTy->isBlockPointerType() || originalTy->isFunctionPointerType()) {
-    assert(Loc::isLocType(castTy));
-    return val;
-  }
+  // Pointer to any pointer.
+  if (Loc::isLocType(CastTy))
+    return V;
+
+  // Pointer to whatever else.
+  return UnknownVal();
 
-  // Check for casts from array type to another type.
-  if (const auto *arrayT =
-          dyn_cast<ArrayType>(originalTy.getCanonicalType())) {
-    // We will always decay to a pointer.
-    QualType elemTy = arrayT->getElementType();
-    val = StateMgr.ArrayToPointer(val.castAs<Loc>(), elemTy);
+SVal SValBuilder::evalCastSubKind(loc::GotoLabel V, QualType CastTy,
+                                  QualType OriginalTy) {
+  // Pointer to bool.
+  if (CastTy->isBooleanType())
+    // Labels are always true.
+    return makeTruthVal(true, CastTy);
+
+  // Pointer to integer.
+  if (CastTy->isIntegralOrEnumerationType()) {
+    const unsigned BitWidth = Context.getIntWidth(CastTy);
+    return makeLocAsInteger(V, BitWidth);
+  }
+
+  // Array to pointer.
+  if (isa<ArrayType>(OriginalTy))
+    if (CastTy->isPointerType() || CastTy->isReferenceType())
+      return UnknownVal();
 
-    // Are we casting from an array to a pointer?  If so just pass on
-    // the decayed value.
-    if (castTy->isPointerType() || castTy->isReferenceType())
-      return val;
+  // Pointer to any pointer.
+  if (Loc::isLocType(CastTy))
+    return V;
 
-    // Are we casting from an array to an integer?  If so, cast the decayed
-    // pointer value to an integer.
-    assert(castTy->isIntegralOrEnumerationType());
-
-    // FIXME: Keep these here for now in case we decide soon that we
-    // need the original decayed type.
-    //    QualType elemTy = cast<ArrayType>(originalTy)->getElementType();
-    //    QualType pointerTy = C.getPointerType(elemTy);
-    return evalCastFromLoc(val.castAs<Loc>(), castTy);
-  }
-
-  // Check for casts from a region to a specific type.
-  if (const MemRegion *R = val.getAsRegion()) {
-    // Handle other casts of locations to integers.
-    if (castTy->isIntegralOrEnumerationType())
-      return evalCastFromLoc(loc::MemRegionVal(R), castTy);
+  // Pointer to whatever else.
+  return UnknownVal();
+}
 
-    // FIXME: We should handle the case where we strip off view layers to get
-    //  to a desugared type.
-    if (!Loc::isLocType(castTy)) {
-      // FIXME: There can be gross cases where one casts the result of a function
-      // (that returns a pointer) to some other value that happens to fit
-      // within that pointer value.  We currently have no good way to
-      // model such operations.  When this happens, the underlying operation
-      // is that the caller is reasoning about bits.  Conceptually we are
-      // layering a "view" of a location on top of those bits.  Perhaps
-      // we need to be more lazy about mutual possible views, even on an
-      // SVal?  This may be necessary for bit-level reasoning as well.
-      return UnknownVal();
-    }
-
+SVal SValBuilder::evalCastSubKind(loc::MemRegionVal V, QualType CastTy,
+                                  QualType OriginalTy) {
+  // Pointer to bool.
+  if (CastTy->isBooleanType()) {
+    const MemRegion *R = V.getRegion();
+    if (const FunctionCodeRegion *FTR = dyn_cast<FunctionCodeRegion>(R))
+      if (const FunctionDecl *FD = dyn_cast<FunctionDecl>(FTR->getDecl()))
+        if (FD->isWeak())
+          // FIXME: Currently we are using an extent symbol here,
+          // because there are no generic region address metadata
+          // symbols to use, only content metadata.
+          return nonloc::SymbolVal(SymMgr.getExtentSymbol(FTR));
+
+    if (const SymbolicRegion *SymR = R->getSymbolicBase())
+      return makeNonLoc(SymR->getSymbol(), BO_NE,
+                        BasicVals.getZeroWithPtrWidth(), CastTy);
+    // Non-symbolic memory regions are always true.
+    return makeTruthVal(true, CastTy);
+  }
+
+  // Pointer to integer.
+  if (CastTy->isIntegralOrEnumerationType()) {
+    const unsigned BitWidth = Context.getIntWidth(CastTy);
+    return makeLocAsInteger(V, BitWidth);
+  }
+
+  // Array to pointer.
+  if (const auto *ArrayT = dyn_cast<ArrayType>(OriginalTy.getCanonicalType()))
+    if (CastTy->isPointerType() || CastTy->isReferenceType()) {
+      // We will always decay to a pointer.
+      QualType ElemTy = ArrayT->getElementType();
+      return StateMgr.ArrayToPointer(V, ElemTy);
+    }
+
+  // Pointer to pointer.
+  if (Loc::isLocType(CastTy)) {
+    // Just pass through function and block pointers.
+    if (OriginalTy->isBlockPointerType() || OriginalTy->isFunctionPointerType())
+      return V;
+    const MemRegion *R = V.getRegion();
     // We get a symbolic function pointer for a dereference of a function
     // pointer, but it is of function type. Example:
 
     //  struct FPRec {
     //    void (*my_func)(int * x);
     //  };
     //
     //  int bar(int x);
     //
     //  int f1_a(struct FPRec* foo) {
     //    int x;
     //    (*foo->my_func)(&x);
     //    return bar(x)+1; // no-warning
     //  }
 
-    assert(Loc::isLocType(originalTy) || originalTy->isFunctionType() ||
-           originalTy->isBlockPointerType() || castTy->isReferenceType());
+    // Get the result of casting a region to a different type.
+    if ((R = StateMgr.getStoreManager().castRegion(R, CastTy)))
+      return loc::MemRegionVal(R);
+  }
 
-    StoreManager &storeMgr = StateMgr.getStoreManager();
+  // Pointer to whatever else.
+  return UnknownVal();
+}
 
-    // Delegate to store manager to get the result of casting a region to a
-    // different type.  If the MemRegion* returned is NULL, this expression
-    // Evaluates to UnknownVal.
-    R = storeMgr.castRegion(R, castTy);
-    return R ? SVal(loc::MemRegionVal(R)) : UnknownVal();
-  }
+SVal SValBuilder::evalCastSubKind(nonloc::CompoundVal V, QualType CastTy,
+                                  QualType OriginalTy) {
+  // Compound to whatever.
+  return UnknownVal();
+}
+
+SVal SValBuilder::evalCastSubKind(nonloc::ConcreteInt V, QualType CastTy,
+                                  QualType OriginalTy) {
+  auto castedValue = [V, CastTy, this]() {
+    llvm::APSInt value = V.getValue();
+    BasicVals.getAPSIntType(CastTy).apply(value);
+    return value;
+  };
+
+  // Integer to bool.
+  if (CastTy->isBooleanType())
+    return makeTruthVal(V.getValue().getBoolValue(), CastTy);
+
+  // Integer to pointer.
+  if (CastTy->isIntegralOrEnumerationType())
+    return makeIntVal(castedValue());
+
+  // Integer to pointer.
+  if (Loc::isLocType(CastTy))
+    return makeIntLocVal(castedValue());
+
+  // Pointer to whatever else.
+  return UnknownVal();
+}
+
+SVal SValBuilder::evalCastSubKind(nonloc::LazyCompoundVal V, QualType CastTy,
+                                  QualType OriginalTy) {
+  // Compound to whatever.
+  return UnknownVal();
+}
+
+SVal SValBuilder::evalCastSubKind(nonloc::LocAsInteger V, QualType CastTy,
+                                  QualType OriginalTy) {
+  Loc L = V.getLoc();
+
+  // Pointer as integer to bool.
+  if (CastTy->isBooleanType())
+    // Pass to Loc function.
+    return evalCastKind(L, CastTy, OriginalTy);
+
+  // Pointer as integer with region to integer/pointer.
+  const MemRegion *R = L.getAsRegion();
+  if (R)
+    // Pass to MemRegion function.
+    return evalCastSubKind(loc::MemRegionVal(R), CastTy, OriginalTy);
+
+  // Pointer as integer without region to pointer.
+  if (Loc::isLocType(CastTy))
+    return L;
+
+  // Pointer as integer to whatever else.
+  return UnknownVal();
+}
+
+SVal SValBuilder::evalCastSubKind(nonloc::SymbolVal V, QualType CastTy,
+                                  QualType OriginalTy) {
+  SymbolRef SE = V.getSymbol();
+
+  // Symbol to bool.
+  if (CastTy->isBooleanType() && (Loc::isLocType(OriginalTy) ||
+                                  OriginalTy->isIntegralOrEnumerationType() ||
+                                  OriginalTy->isMemberPointerType())) {
+    SymbolRef SE = V.getSymbol();
+    BasicValueFactory &BVF = getBasicValueFactory();
+    return makeNonLoc(SE, BO_NE, BVF.getValue(0, SE->getType()), CastTy);
+  }
+
+  // Symbol to integer.
+  QualType T = Context.getCanonicalType(SE->getType());
+  // If types are the same or both are integers, ignore the cast.
+  // FIXME: Remove this hack when we support symbolic truncation/extension.
+  // HACK: If both castTy and T are integers, ignore the cast.  This is
+  // not a permanent solution.  Eventually we want to precisely handle
+  // extension/truncation of symbolic integers.  This prevents us from losing
+  // precision when we assign 'x = y' and 'y' is symbolic and x and y are
+  // different integer types.
+  if (haveSameType(T, CastTy))
+    return V;
+  if (!Loc::isLocType(CastTy))
+    return makeNonLoc(SE, T, CastTy);
+
+  // Symbol to pointer and whatever else.
+  return UnknownVal();
 
-  return dispatchCast(val, castTy);
+SVal SValBuilder::evalCastSubKind(nonloc::PointerToMember V, QualType CastTy,
+                                  QualType OriginalTy) {
+  // Member pointer to whatever.
+  return V;
 }