search

AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
766 stars 97 forks source link

Consider the new 2-phase memory model #1030

Open nunoplopes opened 5 months ago

nunoplopes commented 5 months ago 
A Two-Phase Infinite/Finite Low-Level Memory Model
Reconciling integer–pointer casts, finite space, and undef at the LLVM IR level of abstraction

CALVIN BECK, University of Pennsylvania, USA
IRENE YOON, University of Pennsylvania, USA
HANXI CHEN, University of Pennsylvania, USA
YANNICK ZAKOWSKI, Inria & LIP (UMR CNRS/ENS Lyon/UCB Lyon1/INRIA), France
STEVE ZDANCEWIC, University of Pennsylvania, USA

https://arxiv.org/pdf/2404.16143

A quick read wasn't enough to understand if this could be implemented in Alive2 and/or useful for int2ptr support.

nunoplopes commented 5 months ago

See also https://github.com/AliveToolkit/alive2/issues/754, https://github.com/AliveToolkit/alive2/issues/777, https://github.com/AliveToolkit/alive2/issues/732

regehr commented 5 months ago

nice. I really like it when authors work hard to make things understandable for people who aren't notation-first sort of thinkers. this seems intuitively appealing, but I only spent about 20 minutes on it.