Datalog backed relation analysis #708
Commits on May 27, 2024
Commits on May 31, 2024
-
UI update (hernanponcedeleon#684)
* Updated witness generation functions to return the generated File. * Improved UI: - can select property to check for (only one property at a time) - can generate and render the violation witness in the UI - UI can be scaled with 'ctrl' + '+/-' - Added simple zoom option to displayed witnesses * Added ability to pass configuration options via the UI. * UI programs now get a unified name. Fixed witness generation for programs without names or without file suffix.
Commits on Jun 3, 2024
-
Add support for memcpy_s (hernanponcedeleon#686)
Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
Commits on Jun 7, 2024
-
- Added Event.getLocalId/Event.setLocalId() (hernanponcedeleon#688)
- Function-based analysis and passes now rely on local ids (e.g., for loop detection) for the most part. - Fixed problems in NormalizeLoops.java
-
Add support for cttz (count trailing zeros) intrinsic (hernanponcedel…
…eon#689) Signed-off-by: Hernan Ponce de Leon <[email protected]>
Commits on Jun 12, 2024
-
Fix addresses in witnesses (hernanponcedeleon#692)
* Added memory layout information to ExecutionModel. * Fixed ExecutionGraphVisualizer printing odd addresses sometimes. * Fix address string computation. * Added better out-of-bounds tagging. * Fixed RefinementSolver.analyzeInconclusiveness.
Commits on Jun 13, 2024
-
-
-
Fix cttz bug (hernanponcedeleon#696)
* Fix copy paste error * Add unit tests --------- Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
Commits on Jun 14, 2024
-
Better mem2reg (hernanponcedeleon#697)
* Added RemoveDeadNullChecks pass * Added TypeFactory.decomposeIntoPrimitives Improved MemToReg to also work on complex allocations. * Avoid Mem2Reg on allocations that are used in RMWs. * Added loop check to avoid unsoundness
Commits on Jun 17, 2024
-
Model locks as spinloops to avoid wrong liveness bugs (hernanponcedel…
…eon#695) Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
Commits on Jun 19, 2024
Commits on Jul 1, 2024
-
Avoid exception in SyntacticContextAnalysis (hernanponcedeleon#699)
Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
Commits on Jul 2, 2024
-
Add loop bound annotation (hernanponcedeleon#687)
Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Thomas Haas <[email protected]>
3 people authoredJul 2, 2024
Commits on Jul 4, 2024
-
Automatically cancel previous CI when new commits are pushed (hernanp…
…oncedeleon#700) Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
Commits on Jul 22, 2024
-
-
Refactor relation analysis interface (hernanponcedeleon#702)
Co-authored-by: Dmitry Ivanov <[email protected]>
Commits on Jul 29, 2024
-
Fix an incorrect term pattern in SyncWith (hernanponcedeleon#706)
Co-authored-by: Dmitry Ivanov <[email protected]>
Commits on Aug 3, 2024
-
Extend loop normalization (hernanponcedeleon#705)
Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Thomas Haas <[email protected]>
3 people authoredAug 3, 2024
Commits on Aug 12, 2024
-
Spir-V frontend (hernanponcedeleon#703)
Co-authored-by: Natalia Gavrilenko <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: haining <[email protected]> Co-authored-by: Thomas Haas <[email protected]>
5 people authoredAug 12, 2024 -
Add memory effects to LLVM grammar and better error message (hernanpo…
…ncedeleon#710) Co-authored-by: Natalia Gavrilenko <[email protected]>
Commits on Aug 13, 2024
-
Fix printer OutOfBoundsException (hernanponcedeleon#713)
Co-authored-by: Natalia Gavrilenko <[email protected]>