search

stanford-centaur / pono

Pono: A flexible and extensible SMT-based model checker
Other
68 stars 31 forks source link

Exclude state variables without update functions in simple path check #341

Closed CyanoKobalamyne closed 1 month ago

CyanoKobalamyne commented 1 month ago

If there are state variables that are, e.g., used in the property, but do not have an update function, the simple path check in k-induction and BMC will never succeed. This is because we can always pick an arbitrary (new) value for this variable and thus construct a "new" state, even if, in reality, we are in a loop.

Such variables should in reality be inputs. However, such a transformation is not completely straightforward, as they could still have an initial value. For now, as a simple solution, we simply exclude them from the simple path checks.

CyanoKobalamyne commented 1 month ago

It took me a while to update everything correctly, but now it should be computed whenever the rest of the internal structures are updated.

Also, it seems that with this change k-induction (and BMC with simple path checking) can now prove the property in InterpWinTests.

ahmed-irfan commented 1 month ago

Cool feature!

One suggestion: I think this feature should be independent of whether Cone of Influence (COI) is enabled or not. Currently, if I am not mistaken, it is tied to rebuilding the transition system with COI.

Great job!!!

On Wed, Aug 21, 2024 at 2:48 PM Áron Ricardo Perez-Lopez < @.***> wrote:

It took me a while to update everything correctly, but now it should be computed whenever the rest of the internal structures are updated.

Also, it seems that with this change k-induction (and BMC with simple path checking) can now prove the property in InterpWinTests.

— Reply to this email directly, view it on GitHub https://github.com/stanford-centaur/pono/pull/341#issuecomment-2303068219, or unsubscribe https://github.com/notifications/unsubscribe-auth/AKI2LLXBEDNRGOTAGGX65S3ZSUDMTAVCNFSM6AAAAABM4SO7NGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGMBTGA3DQMRRHE . You are receiving this because you are subscribed to this thread.Message ID: @.***>

CyanoKobalamyne commented 1 month ago

This should actually work regardless of whether COI analysis is enabled. But I also changed the COI rebuilding process so that it rebuilds the list of state variables with no next states, otherwise this would break when static COI analysis is enabled.