Page MenuHomePhabricator

Added InstCombine transform for pattern "(A & B) ^ ((A ^ C) | B) -> (~A)".
AcceptedPublic

Authored by sonamkumari on Aug 8 2014, 4:04 AM.

Details

Summary

This patch implements transform for pattern "(A ^ B) | ((~A) ^ B) -> True".

Please help in reviewing the same.

Thanks,
Sonam.

Diff Detail

Event Timeline

sonamkumari updated this revision to Diff 12302.Aug 8 2014, 4:04 AM
sonamkumari retitled this revision from to Added InstCombine transform for pattern "(A & B) ^ ((A ^ C) | B) -> (~A)"..
sonamkumari updated this object.
sonamkumari edited the test plan for this revision. (Show Details)
sonamkumari added a subscriber: Unknown Object (MLST).
majnemer added inline comments.
lib/Transforms/InstCombine/InstCombineAndOrXor.cpp
2519–2522

This is incorrect, it should be something like:

// (A & B) ^ ((A ^ C) | B) -> (B | C) ^ A
if (match(Op0I, m_And(m_Value(A), m_Value(B))) &&
    match(Op1I, m_Or(m_Xor(m_Specific(A), m_Value(C)), m_Specific(B))))
  return BinaryOperator::CreateXor(Builder->CreateOr(B, C), A);
suyog edited edge metadata.Aug 8 2014, 10:48 AM

Hi Sonam,

I would strongly suggest you to include a link like http://rise4fun.com/Z3/Evslo along with any identities just to verify that no errors are slipping through? It's an easy way to increase confidence in correctness.

Z3 is pretty easy to use and has a good tutorial http://rise4fun.com/Z3/tutorial/guide . You don't need to read all of it, just skip to the "bit vectors" section for the list of operations and just reuse the boilerplate in my link. Basically, if your identity is "foo == bar", then what you ask Z3 to do is check that the statement "foo != bar" is unsatisfiable. The online Z3 "permalink" feature is what gives you a URL like the above.

sonamkumari edited edge metadata.

Hi David,Suyog,

Thanks David for pointing out the mistake.I have submitted the patch related to the expression you mentioned.

Thanks Suyog for this valuable information.I have attached the Z3 link for this expression.

Z3 Link : http://rise4fun.com/Z3/kOaU

Please help in reviewing the patch.

Regards,
Sonam.

Gentle Ping !!

Patch won't take much time to review :)

majnemer accepted this revision.Aug 20 2014, 8:40 PM
majnemer added a reviewer: majnemer.

LGTM.

This revision is now accepted and ready to land.Aug 20 2014, 8:40 PM

Hi David,

Can you please commit this patch as I don't have the access. :)

Regards,
Sonam.

Gentle Ping !

asl added a subscriber: asl.Sep 4 2014, 11:11 PM

Please provide the information asked in other thread for similar pattern:

  1. How often this transformation triggers in LLVM testsuite. Where, in which tests.
  2. How often this transformation triggers in SPEC. Where, in which tests.
suyog resigned from this revision.Mar 26 2015, 12:00 PM
suyog removed a reviewer: suyog.
silvas resigned from this revision.Jul 8 2016, 11:49 PM
silvas removed a reviewer: silvas.
dexonsmith resigned from this revision.Jul 11 2016, 6:40 PM
dexonsmith removed a reviewer: dexonsmith.
espindola edited reviewers, added: espindola; removed: rafael.Mar 14 2018, 4:58 PM