Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix size and offset computations of types #691

Merged
merged 4 commits into from
Jun 12, 2024

Conversation

ThomasHaas
Copy link
Collaborator

This PR improves computations of types sizes, alignments, and offsets.
Previously, we had wrong computations in many cases, however, it only rarely lead to issues in benchmarks that made use of offset_of compiler primitives or similar ways to compute pointer offsets without GEP.
As a result, issue #586 should also be resolved.

Copy link
Owner

@hernanponcedeleon hernanponcedeleon left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I could not spot anything fundamentally wrong, but there are way too many computations going on.

Can you add some basic tests with a structure where the compiler adds some padding. Maybe we can even have a second structure will the same members, but add __attribute__((packed)); to avoid the padding.

@ThomasHaas
Copy link
Collaborator Author

I could not spot anything fundamentally wrong, but there are way too many computations going on.

Can you add some basic tests with a structure where the compiler adds some padding.

All LLVM IR structs are padded by default but you won't see the padding in the IR expliclity. So in fact, many non-trivial benchmarks have padded structs and our internal type size computation was almost always wrong (it was always missing trailing padding). The difficult part is making those tests fail, because wrong size/offset computations simply do not matter unless you have offsetof somewhere. I will see what I can do.

Maybe we can even have a second structure will the same members, but add __attribute__((packed)); to avoid the padding.

IIRC, adding __attribute__((packed)) will result in IR code that we cannot handle, because the LLVM IR declaration of the struct uses extra brackets <...> (LangRef). We might parse the code, but we certainly ignore the packedness!

@ThomasHaas
Copy link
Collaborator Author

I added a test that breaks on development (if run without opt passes) but runs correctly on this PR.

@hernanponcedeleon
Copy link
Owner

I added a test that breaks on development (if run without opt passes) but runs correctly on this PR.

Great. Thanks!

@hernanponcedeleon hernanponcedeleon force-pushed the fixSizeOffsetComputations branch from 7973b5b to 6c54960 Compare June 12, 2024 12:51
@hernanponcedeleon hernanponcedeleon merged commit 6c8baa3 into development Jun 12, 2024
1 check passed
@hernanponcedeleon hernanponcedeleon deleted the fixSizeOffsetComputations branch June 12, 2024 17:58
tonghaining added a commit to tonghaining/Dat3M that referenced this pull request Sep 12, 2024
commit d8c8158
Merge: eb7ac78 951f326
Author: haining <[email protected]>
Date:   Wed Sep 11 23:43:08 2024 +0300

    Merge branch 'development' into opencl

commit eb7ac78
Author: haining <[email protected]>
Date:   Tue Sep 10 22:14:49 2024 +0300

    add default scope hierarchy and memory space

commit 45e1770
Author: Haining <[email protected]>
Date:   Fri Sep 6 17:25:04 2024 +0300

    update opencl cat

commit 3936ef7
Author: Hernan Ponce de Leon <[email protected]>
Date:   Thu Sep 5 15:30:19 2024 +0200

    Add unit test to compare C11 and OpenCL

commit e7330c6
Author: Haining <[email protected]>
Date:   Wed Sep 4 13:10:32 2024 +0300

    add WI tag to weak operations

commit 2181c2b
Merge: 67a82c3 9a23ab0
Author: Haining <[email protected]>
Date:   Tue Sep 3 15:16:12 2024 +0300

    Merge branch 'development' into opencl

commit 67a82c3
Author: Haining <[email protected]>
Date:   Tue Sep 3 14:47:22 2024 +0300

    add atomicity tag to IW

commit 0aa329c
Author: haining <[email protected]>
Date:   Mon Sep 2 23:23:48 2024 +0300

    Add support for Parametric

commit f9caeaf
Author: Haining <[email protected]>
Date:   Wed Jul 17 15:35:13 2024 +0300

    simplify opencl.cat

commit 8b8a722
Author: Haining <[email protected]>
Date:   Sat Jul 6 16:42:42 2024 +0300

    merge GPU scopes

commit 8854f37
Merge: d67224a 50f34c6
Author: Haining <[email protected]>
Date:   Thu Jun 20 16:15:17 2024 +0300

    Merge branch 'hernan-opencl' into opencl

commit d67224a
Author: Haining <[email protected]>
Date:   Mon Jun 10 14:36:23 2024 +0300

    permit fence to have multiple spaces

commit 50f34c6
Author: Hernan Ponce de Leon <[email protected]>
Date:   Wed Jun 19 10:40:24 2024 +0200

    More for opencl compilation

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

commit b645b64
Author: Hernan Ponce de Leon <[email protected]>
Date:   Tue Jun 18 11:56:06 2024 +0200

    Compile and demangle opencl code

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

commit 3291aa0
Author: Hernan Ponce de Leon <[email protected]>
Date:   Mon Jun 17 11:11:03 2024 +0200

    Model locks as spinloops to avoid wrong liveness bugs (hernanponcedeleon#695)

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

commit 075f03f
Author: Thomas Haas <[email protected]>
Date:   Fri Jun 14 12:57:34 2024 +0200

    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

commit 2688e01
Author: Hernan Ponce de Leon <[email protected]>
Date:   Thu Jun 13 17:32:21 2024 +0200

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

commit 8b8389a
Author: Thomas Haas <[email protected]>
Date:   Thu Jun 13 12:43:55 2024 +0200

    Easier handling of nondet choices (hernanponcedeleon#693)

commit 94f90c7
Author: René Maseli <[email protected]>
Date:   Thu Jun 13 10:25:52 2024 +0200

    Fix inclusion updates in IBPA (hernanponcedeleon#694)

commit 6c8baa3
Author: Thomas Haas <[email protected]>
Date:   Wed Jun 12 19:58:15 2024 +0200

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

commit 1afd208
Author: Thomas Haas <[email protected]>
Date:   Wed Jun 12 14:49:46 2024 +0200

    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.

commit 6ad93d5
Merge: 3231678 929b15b
Author: Haining <[email protected]>
Date:   Mon Jun 10 10:31:44 2024 +0300

    Merge branch 'development' into opencl

commit 929b15b
Author: Hernan Ponce de Leon <[email protected]>
Date:   Fri Jun 7 21:04:30 2024 +0200

    Add support for cttz (count trailing zeros) intrinsic (hernanponcedeleon#689)

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

commit 28885e2
Author: Thomas Haas <[email protected]>
Date:   Fri Jun 7 20:00:23 2024 +0200

    - 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

commit 3231678
Author: Haining <[email protected]>
Date:   Thu Jun 6 12:33:18 2024 +0300

    clean code

commit 773d404
Merge: 1e1005c 184fab4
Author: Haining <[email protected]>
Date:   Thu Jun 6 11:49:57 2024 +0300

    Merge branch 'development' into opencl

commit 1e1005c
Author: Haining <[email protected]>
Date:   Wed Jun 5 17:14:09 2024 +0300

    add OpenCLInit, update visitorLitmusC

commit 184fab4
Author: Hernan Ponce de Leon <[email protected]>
Date:   Mon Jun 3 18:48:25 2024 +0200

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

commit 016aaf4
Author: Thomas Haas <[email protected]>
Date:   Fri May 31 11:22:18 2024 +0200

    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.

commit 92d82b1
Author: René Maseli <[email protected]>
Date:   Mon May 27 21:53:09 2024 +0200

    Split 'addInto' stats into graph and cycle detection counters (hernanponcedeleon#683)

commit 9286ffe
Merge: e006a87 b4d33c9
Author: haining <[email protected]>
Date:   Sun May 19 10:12:54 2024 +0300

    Merge branch 'development' into opencl

commit e006a87
Author: Haining <[email protected]>
Date:   Mon May 13 20:26:25 2024 +0300

    fix LOCAL/GLOBAL tags, update scope

commit be14d7b
Author: Haining <[email protected]>
Date:   Sat May 11 20:34:09 2024 +0300

    add opencl race test

commit c20fda7
Merge: 936ec06 c48cc9f
Author: haining <[email protected]>
Date:   Fri May 10 18:40:20 2024 +0300

    Merge branch 'development' into opencl

commit 936ec06
Author: haining <[email protected]>
Date:   Mon Mar 4 17:19:50 2024 +0200

    add fromLocalObject to Register

commit e5f3f6b
Author: Haining <[email protected]>
Date:   Tue Feb 6 04:11:30 2024 +0200

    update opencl model

commit 393d523
Merge: 2f5856e 2685b3e
Author: Haining <[email protected]>
Date:   Tue Feb 6 03:44:41 2024 +0200

    Merge branch 'development' into opencl

commit 2f5856e
Author: Haining <[email protected]>
Date:   Tue Jan 30 11:49:12 2024 +0200

    update expectation based on VM

commit 1d157e9
Author: Haining <[email protected]>
Date:   Fri Jan 26 14:01:27 2024 +0200

    update opencl tests

commit c4eb49e
Author: haining <[email protected]>
Date:   Tue Jan 23 21:18:55 2024 +0200

    manually change CT_wsq2

commit 05f2682
Author: haining <[email protected]>
Date:   Tue Jan 23 18:06:22 2024 +0200

    update 2+2W test

commit 8f9357d
Author: haining <[email protected]>
Date:   Tue Jan 23 15:25:25 2024 +0200

    add partial sc

commit f7b6dc0
Merge: 7365171 77bc93b
Author: haining <[email protected]>
Date:   Tue Jan 23 14:38:12 2024 +0200

    Merge branch 'development' into opencl

commit 7365171
Author: Haining <[email protected]>
Date:   Tue Jan 23 13:11:24 2024 +0200

    add entry and exit fence for barrier

commit e6e4061
Author: haining <[email protected]>
Date:   Mon Jan 22 23:34:37 2024 +0200

    memory region -> memory space

commit b70912e
Author: haining <[email protected]>
Date:   Mon Jan 22 16:49:57 2024 +0200

    add oldOpenCLTests

commit d5d41e2
Merge: 25562eb 24cf37b
Author: haining <[email protected]>
Date:   Mon Jan 22 16:05:05 2024 +0200

    Merge branch 'development' into opencl

commit 25562eb
Author: haining <[email protected]>
Date:   Sat Jan 20 20:28:07 2024 +0200

    merge fence flag to memory region

commit 2b63f14
Author: haining <[email protected]>
Date:   Sat Jan 20 20:06:38 2024 +0200

    WEAK -> NA

commit cc4670f
Author: haining <[email protected]>
Date:   Sat Jan 20 20:04:18 2024 +0200

    add GLOBAL/LOCAL to opencl visitor

commit d046856
Author: haining <[email protected]>
Date:   Tue Jan 16 19:23:59 2024 +0200

    reuse swg from vulkan to opencl

commit 942044c
Author: Haining <[email protected]>
Date:   Tue Jan 16 12:24:43 2024 +0200

    update parser

commit a48c668
Author: haining <[email protected]>
Date:   Sun Jan 14 18:07:55 2024 +0200

    update barrier

commit 894965f
Author: haining <[email protected]>
Date:   Sun Jan 14 15:07:40 2024 +0200

    add barrier

commit ba1f9da
Author: haining <[email protected]>
Date:   Sun Jan 14 14:14:10 2024 +0200

    rmw to RMW

commit 600adc8
Author: haining <[email protected]>
Date:   Sun Jan 14 13:10:34 2024 +0200

    fix test assertions

commit ede2484
Author: Haining <[email protected]>
Date:   Fri Jan 12 16:48:05 2024 +0200

    add expectation to new tests

commit de725b5
Author: Haining <[email protected]>
Date:   Fri Jan 12 16:40:02 2024 +0200

    add missing test from herd testsuit

commit 10de296
Author: Haining <[email protected]>
Date:   Fri Jan 12 16:32:32 2024 +0200

    add opencl region and tests

commit 50ba29f
Author: Haining <[email protected]>
Date:   Fri Jan 12 15:04:58 2024 +0200

    add visitorOpenCL

commit 8e1da0e
Author: Haining <[email protected]>
Date:   Fri Jan 12 14:16:04 2024 +0200

    add fence tag transformer

commit 5cebf0d
Author: Haining <[email protected]>
Date:   Fri Jan 12 14:08:20 2024 +0200

    add scope to visitorLitmusC

commit 16c85e7
Author: Haining <[email protected]>
Date:   Fri Jan 12 13:11:22 2024 +0200

    add openclFence

commit ee47676
Author: haining <[email protected]>
Date:   Thu Jan 11 21:49:55 2024 +0200

    add null checker for threadScope

commit 913b0b2
Author: Haining <[email protected]>
Date:   Thu Jan 11 18:42:17 2024 +0200

    add scope to atomics

commit 14a6dfe
Author: Haining <[email protected]>
Date:   Thu Jan 11 18:24:28 2024 +0200

    add visitorOpenCL

commit 71897f0
Author: Haining <[email protected]>
Date:   Thu Jan 11 18:03:18 2024 +0200

    add openCLThreadScope

commit ad8d673
Author: Haining <[email protected]>
Date:   Thu Jan 11 16:48:06 2024 +0200

    add missing implicit C11 atomic operations

commit 880669c
Author: Haining <[email protected]>
Date:   Thu Jan 11 15:42:55 2024 +0200

    merge OpenCL into C

commit 00cac5a
Author: Haining <[email protected]>
Date:   Thu Jan 11 14:19:17 2024 +0200

    rm C11Lexer.tokens

commit 9d72f12
Merge: eea19f4 4b84cc8
Author: Haining <[email protected]>
Date:   Thu Jan 11 14:16:23 2024 +0200

    Merge branch 'development' into opencl

commit eea19f4
Author: Haining <[email protected]>
Date:   Thu Jan 11 14:14:41 2024 +0200

    add opencl thread scope

commit 2e2a7a3
Author: Haining <[email protected]>
Date:   Thu Jan 11 13:05:16 2024 +0200

    rename c11 explicit tokens

commit b779fd6
Author: Haining <[email protected]>
Date:   Thu Jan 11 12:00:04 2024 +0200

    update thread scope definition in test

commit 5e32d5f
Author: Haining <[email protected]>
Date:   Wed Jan 10 16:26:07 2024 +0200

    update opencl litmus test

commit 5087438
Author: Haining <[email protected]>
Date:   Wed Jan 10 16:03:16 2024 +0200

    update OpenCL grammar

commit b1f5419
Author: haining <[email protected]>
Date:   Tue Jan 9 00:11:54 2024 +0200

    add OpenCL Litmus

commit 42658b1
Author: haining <[email protected]>
Date:   Mon Jan 8 22:02:58 2024 +0200

    update atomic_compare_exchange

commit 9e49cd0
Author: haining <[email protected]>
Date:   Mon Jan 8 15:14:39 2024 +0200

    add context to fence

commit 824e873
Author: haining <[email protected]>
Date:   Mon Jan 8 11:39:07 2024 +0200

    change openclRMW encoding

commit 47976fc
Author: haining <[email protected]>
Date:   Sun Jan 7 14:02:34 2024 +0200

    add opencl visitor

commit 29e3ccc
Author: haining <[email protected]>
Date:   Sun Jan 7 13:04:23 2024 +0200

    remove WI from scope

commit 3ff7252
Author: haining <[email protected]>
Date:   Sun Jan 7 12:57:30 2024 +0200

    add opencl arch, reorder arch list

commit 26b36a8
Author: haining <[email protected]>
Date:   Sun Jan 7 12:46:16 2024 +0200

    reuse syncbar from spirv for opencl same_B

commit aeaa94c
Author: haining <[email protected]>
Date:   Sun Jan 7 12:44:55 2024 +0200

    change incl to use sr

commit 05faec4
Author: haining <[email protected]>
Date:   Sun Jan 7 12:29:03 2024 +0200

    add opencl tags, define swi with po

commit 17d0d9b
Author: haining <[email protected]>
Date:   Thu Jan 4 22:40:37 2024 +0200

    draft OpenCL litmus grammar

commit b347583
Author: haining <[email protected]>
Date:   Thu Jan 4 21:24:35 2024 +0200

    replace ^2 with *

commit 213854b
Author: Haining <[email protected]>
Date:   Wed Jan 3 16:38:01 2024 +0200

    update opencl cat

commit a8f8232
Author: Haining <[email protected]>
Date:   Wed Jan 3 16:24:57 2024 +0200

    use new incl relation

commit 171d66b
Merge: 5d271a0 c1371f9
Author: Haining <[email protected]>
Date:   Wed Jan 3 15:36:23 2024 +0200

    Merge branch 'development' into opencl

commit 5d271a0
Author: Haining <[email protected]>
Date:   Wed Dec 13 16:27:45 2023 +0200

    add opencl cat draft
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants