Debugging on TXWP TxWeakestPreCondition::PushUp()

[alvin21mfmlai]

Started debugging process for TxWeakestPreCondition::PushUp() function.

18 Oct 23:
Question 1:

Lines 419-422 -> any consideration for condition of "WPExpr->getWidth() == cond->getWidth()"

Question 2:

Lines 447-450 -> any consideration for condition of "WPExpr->getWidth() < negCond->getWidth()"

[ArpitaDutta]

Hi Alvin,
In both the questions, when the width of the WPExpr is equal to the cond/negCond expr width, then there is no need to zero extension and we can directly do the And of the exprs.

[alvin21mfmlai]

Hi Arpi, Thanks for your fast response. May we have a zoom meeting tmr morning at 10am? I am not able to attend tonight's call due to some work issue that I need to sort out tonight. I do not fully understand the mechanics for the four conditions built into the push-up function, as summarized in my simple flowchart below. Once I have some level of understanding for the purpose of the four in-built conditions, I can better debug on the three benchmark cases which are giving the problem. Thank you. Alvin [cid:8740f46b-19d6-445d-9dd0-ac75b37427a4]

…

________________________________ From: Arpita Dutta ***@***.***> Sent: Wednesday, October 18, 2023 4:26 PM To: tracer-x/TracerX ***@***.***> Cc: Chew Wei Ze Alvin ***@***.***>; Author ***@***.***> Subject: Re: [tracer-x/TracerX] Debugging on TXWP TxWeakestPreCondition::PushUp() (Issue #403) - External Email - Hi Alvin, In both the questions, when the width of the WPExpr is equal to the cond/negCond expr width, then there is no need to zero extension and we can directly do the And of the exprs. — Reply to this email directly, view it on GitHub<#403 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AQWH6QBDN7F3EM75ZKNVO43X76HCPAVCNFSM6AAAAAA6FB235SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONRXHE2DGOBXGM>. You are receiving this because you authored the thread.Message ID: ***@***.***>