search

tracer-x / TracerX

TracerX Symbolic Virtual Machine
https://tracer-x.github.io/
Other
31 stars 11 forks source link

Debugging on TXWP TxWeakestPreCondition::PushUp() #403

Open alvin21mfmlai opened 11 months ago

alvin21mfmlai commented 11 months ago

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

pushUpOverview

18 Oct 23: Question 1: image Lines 419-422 -> any consideration for condition of "WPExpr->getWidth() == cond->getWidth()"

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

ArpitaDutta commented 11 months ago

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 commented 11 months ago

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 GitHubhttps://github.com/tracer-x/TracerX/issues/403#issuecomment-1767943873, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AQWH6QBDN7F3EM75ZKNVO43X76HCPAVCNFSM6AAAAAA6FB235SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONRXHE2DGOBXGM. You are receiving this because you authored the thread.Message ID: @.***>