[PATCH] D85026: [analyzer] Minor refactoring of SVal::getSubKind function

[Balázs Benics via Phabricator via cfe-commits]

steakhal accepted this revision.
steakhal added a comment.
This revision is now accepted and ready to land.

I like the change.
I also proved the equivalence, just for fun really :D

  from z3 import *
  
  def proof_equality(F, G):
    s = Solver()
    s.add(Not(F == G))
    r = s.check()
    if r == unsat:
      print("proved")
    else:
      print("counterexample")
      print(s.model())
  
  
  Kind = BitVec('Kind', 32)
  BaseMask = BitVecVal(0b11, 32)
  BaseBits = BitVecVal(2, 32)
  
  Before = (Kind & ~BaseMask) >> BaseBits
  After = Kind >> BaseBits
  
  proof_equality(Before, After)
  # prints: proved 


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D85026/new/

https://reviews.llvm.org/D85026