Datalog backed relation analysis #708

DIvanov503 · 2024-08-07T12:22:41Z

No description provided.

* 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.

Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>

- Function-based analysis and passes now rely on local ids (e.g., for loop detection) for the most part. - Fixed problems in NormalizeLoops.java

…eon#689) Signed-off-by: Hernan Ponce de Leon <[email protected]>

* 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.

* 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]>

* 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

…eon#695) Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>

…oncedeleon#698)

Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>

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]>

…oncedeleon#700) Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>

Co-authored-by: Dmitry Ivanov <[email protected]>

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]>

hernanponcedeleon · 2024-08-07T13:00:09Z

FYI @DIvanov503 https://souffle-lang.github.io/install

DIvanov503 · 2024-08-08T13:49:04Z

dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java

@@ -82,7 +82,7 @@ private Dartagnan(Configuration config) throws InvalidConfigurationException {

    public static void main(String[] args) throws Exception {

-        initGitInfo();
+//        initGitInfo();


Suggested change

// initGitInfo();

initGitInfo();

DIvanov503 · 2024-08-08T13:49:22Z

dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java

@@ -39,6 +39,8 @@ public static void configure(Configuration config) throws InvalidConfigurationEx

    private static final boolean USE_TEST_PATH = isJUnitTest();

+    public static final boolean CHECK_DATALOG = true; // Enables comparing basic RA in datalog against native


Suggested change

public static final boolean CHECK_DATALOG = true; // Enables comparing basic RA in datalog against native

public static final boolean CHECK_DATALOG = false; // Enables comparing basic RA in datalog against native

DIvanov503 · 2024-08-08T13:53:01Z

dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java

        RelationAnalysis.Config c = new RelationAnalysis.Config(config);
+        c.method = RelationAnalysisMethod.DATALOG;


Suggested change

RelationAnalysis.Config c = new RelationAnalysis.Config(config);

c.method = RelationAnalysisMethod.DATALOG;

RelationAnalysis.Config c = new RelationAnalysis.Config(config);

hernanponcedeleon · 2024-08-09T05:56:29Z

@DIvanov503 I killed the pipeline after 14hs. There seems to be a problem with linux-kernel.cat. I still don't get why the timeout from AbstractLitmusTest is not triggering.

I tried a few examples manually and they all finished relatively fast. I tried specially the ones having large number of events or using RCU features which I thought could make the analysis harder. I guess we need a script to run examples one by one in the console to find out which test(s) are not finishing.

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]>

…ncedeleon#710) Co-authored-by: Natalia Gavrilenko <[email protected]>

ThomasHaas · 2024-08-13T14:12:35Z

I wouldn't try to fix the native RA in this PR (especially if the source of the problem is unclear). If you have a proper fix, put it into a separate PR.

DIvanov503 · 2024-08-13T15:06:13Z

I agree but I

want to know that my fix works before merging
don't want to write tests for my fix

Hence I want the pipeline to pass using the datalog RA for checking if both implementations compute the same results. Once it's done and I'm convinced about the fix, it can go to a different PR.

Co-authored-by: Natalia Gavrilenko <[email protected]>

hernanponcedeleon · 2024-10-08T07:56:29Z

As discussed with @DIvanov503, this was supersed by #743, this cloosing.

xeren and others added 21 commits May 27, 2024 21:53

Split 'addInto' stats into graph and cycle detection counters (hernan…

92d82b1

…poncedeleon#683)

Add support for memcpy_s (hernanponcedeleon#686)

184fab4

Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>

- Added Event.getLocalId/Event.setLocalId() (hernanponcedeleon#688)

28885e2

- 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…

929b15b

…eon#689) Signed-off-by: Hernan Ponce de Leon <[email protected]>

Fix size and offset computations of types (hernanponcedeleon#691)

6c8baa3

Fix inclusion updates in IBPA (hernanponcedeleon#694)

94f90c7

Easier handling of nondet choices (hernanponcedeleon#693)

8b8389a

Fix cttz bug (hernanponcedeleon#696)

2688e01

* 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]>

Better mem2reg (hernanponcedeleon#697)

075f03f

* 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

Model locks as spinloops to avoid wrong liveness bugs (hernanponcedel…

3291aa0

…eon#695) Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>

Assertion expressions (hernanponcedeleon#690)

489f608

Added TagSet, used in AbstractEvent to store tags of events. (hernanp…

d917401

…oncedeleon#698)

Avoid exception in SyntacticContextAnalysis (hernanponcedeleon#699)

fa5a226

Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>

Add loop bound annotation (hernanponcedeleon#687)

3771432

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]>

Automatically cancel previous CI when new commits are pushed (hernanp…

6356656

…oncedeleon#700) Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>

Update JavaSMT version (hernanponcedeleon#701)

9f44db5

Refactor relation analysis interface (hernanponcedeleon#702)

e87cb88

Co-authored-by: Dmitry Ivanov <[email protected]>

Fix an incorrect term pattern in SyncWith (hernanponcedeleon#706)

eb15f40

Co-authored-by: Dmitry Ivanov <[email protected]>

Extend loop normalization (hernanponcedeleon#705)

6582d4a

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]>

DIvanov503 commented Aug 8, 2024

View reviewed changes

natgavrilenko and others added 2 commits August 12, 2024 13:55

Spir-V frontend (hernanponcedeleon#703)

030b16b

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]>

Add memory effects to LLVM grammar and better error message (hernanpo…

cdc0689

…ncedeleon#710) Co-authored-by: Natalia Gavrilenko <[email protected]>

DIvanov503 force-pushed the datarel branch from 4272c85 to 3d84bfd Compare August 13, 2024 07:32

hernanponcedeleon mentioned this pull request Aug 13, 2024

[RA] Missing tuples in transitive closure #714

Closed

natgavrilenko and others added 22 commits August 13, 2024 21:12

Fix printer OutOfBoundsException (hernanponcedeleon#713)

618c3f7

Co-authored-by: Natalia Gavrilenko <[email protected]>

WIP

76521e7

Rebase

92df103

Rebase

1414686

Install Souffle

3201221

Temporary replace native with datalog

b096a3e

Import Souffle package

344ab63

Make Souffle use more verbose

2344b37

Add support for recursive relations

e0e4626

Small fixes

a9dabfc

Add missing PO dependency

a8b7de1

Stop using THREAD

4262425

Disable comparioson to native

9141274

Fix recursion in the name visitor

de6171e

Fix compilation error

5cc52a9

Try a closure fix

e6cb077

Delete datalog tempdir on exit

2491e53

Update the transitive closure implementation

0908b81

Typo

1ba36e3

Update the closure implementation

c5f997e

Use the native initializer

215a8d6

Disable datalog check

b781df6

DIvanov503 force-pushed the datarel branch from cfc8e9a to b781df6 Compare August 20, 2024 06:04

hernanponcedeleon force-pushed the development branch from 48d880d to 9a23ab0 Compare August 28, 2024 16:02

hernanponcedeleon closed this Oct 8, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Datalog backed relation analysis #708

Datalog backed relation analysis #708

DIvanov503 commented Aug 7, 2024

hernanponcedeleon commented Aug 7, 2024

DIvanov503 Aug 8, 2024

DIvanov503 Aug 8, 2024

DIvanov503 Aug 8, 2024

hernanponcedeleon commented Aug 9, 2024

ThomasHaas commented Aug 13, 2024

DIvanov503 commented Aug 13, 2024

hernanponcedeleon commented Oct 8, 2024

		@@ -39,6 +39,8 @@ public static void configure(Configuration config) throws InvalidConfigurationEx

		private static final boolean USE_TEST_PATH = isJUnitTest();

		public static final boolean CHECK_DATALOG = true; // Enables comparing basic RA in datalog against native

		RelationAnalysis.Config c = new RelationAnalysis.Config(config);
		c.method = RelationAnalysisMethod.DATALOG;

Datalog backed relation analysis #708

Datalog backed relation analysis #708

Conversation

DIvanov503 commented Aug 7, 2024

hernanponcedeleon commented Aug 7, 2024

DIvanov503 Aug 8, 2024

Choose a reason for hiding this comment

DIvanov503 Aug 8, 2024

Choose a reason for hiding this comment

DIvanov503 Aug 8, 2024

Choose a reason for hiding this comment

hernanponcedeleon commented Aug 9, 2024

ThomasHaas commented Aug 13, 2024

DIvanov503 commented Aug 13, 2024

hernanponcedeleon commented Oct 8, 2024