Page MenuHomePhabricator

[analyzer] Introduce minor refactoring of SVal::getSubKind function
ClosedPublic

Authored by ASDenysPetrov on Jul 31 2020, 6:02 AM.

Details

Summary

BaseMask occupies the lowest bits. Effect of applying the mask is neutralized by right shift operation, thus making it useless.
Also change mask init value from hex to bin since it's more natural for mask.

Fix: Remove a redundant bitwise operation.

P.S. It hurts my eyes everytime I see it. I gave up.

Diff Detail

Event Timeline

ASDenysPetrov created this revision.Jul 31 2020, 6:02 AM
ASDenysPetrov requested review of this revision.Jul 31 2020, 6:02 AM
steakhal accepted this revision.Jul 31 2020, 10:45 AM

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 
This revision is now accepted and ready to land.Jul 31 2020, 10:45 AM

Hey, nice catch!
However, I'm going to complain about commit messages again ๐Ÿ˜… I would prefer having imperative mood in the message, something like "Refactor ..." or "Introduce minor refactoring..."

NoQ accepted this revision.Jul 31 2020, 5:26 PM

That's a fair point.

ASDenysPetrov retitled this revision from [analyzer] Minor refactoring of SVal::getSubKind function to [analyzer] Introduce minor refactoring of SVal::getSubKind function.Aug 2 2020, 4:22 PM

@vsavchenko:

However, I'm going to complain about commit messages again ๐Ÿ˜… I would prefer having imperative mood in the message, something like "Refactor ..." or "Introduce minor refactoring..."

Changed title.

Thank you, guys!