-
Notifications
You must be signed in to change notification settings - Fork 29
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
Merge latest changes from rework #498
Commits on May 12, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 3403f77 - Browse repository at this point
Copy the full SHA 3403f77View commit details
Commits on May 13, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 3db9825 - Browse repository at this point
Copy the full SHA 3db9825View commit details
Commits on May 16, 2023
-
Configuration menu - View commit details
-
Copy full SHA for f9664d3 - Browse repository at this point
Copy the full SHA f9664d3View commit details -
Configuration menu - View commit details
-
Copy full SHA for 687b063 - Browse repository at this point
Copy the full SHA 687b063View commit details -
Configuration menu - View commit details
-
Copy full SHA for 505aa98 - Browse repository at this point
Copy the full SHA 505aa98View commit details -
Merge pull request #444 from hernanponcedeleon/initial_prototype
Initial prototype for rework
Configuration menu - View commit details
-
Copy full SHA for e4e527d - Browse repository at this point
Copy the full SHA e4e527dView commit details -
Added some Metadata classes (partially unused)
Updated Event to have SourceLocation metadata
Configuration menu - View commit details
-
Copy full SHA for 814bfcc - Browse repository at this point
Copy the full SHA 814bfccView commit details -
Configuration menu - View commit details
-
Copy full SHA for 0eb1815 - Browse repository at this point
Copy the full SHA 0eb1815View commit details
Commits on May 17, 2023
-
Improved documentation. Renamed ParseId back to OriginalId (not all programs are constructed by a parser).
Configuration menu - View commit details
-
Copy full SHA for e3e4d38 - Browse repository at this point
Copy the full SHA e3e4d38View commit details -
Merge pull request #445 from hernanponcedeleon/metadata
Add Metadata
Configuration menu - View commit details
-
Copy full SHA for bb836c9 - Browse repository at this point
Copy the full SHA bb836c9View commit details
Commits on May 19, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 7bcf52c - Browse repository at this point
Copy the full SHA 7bcf52cView commit details -
Configuration menu - View commit details
-
Copy full SHA for 9acc647 - Browse repository at this point
Copy the full SHA 9acc647View commit details -
Configuration menu - View commit details
-
Copy full SHA for 3ca1ed8 - Browse repository at this point
Copy the full SHA 3ca1ed8View commit details -
Configuration menu - View commit details
-
Copy full SHA for 14fa871 - Browse repository at this point
Copy the full SHA 14fa871View commit details
Commits on May 21, 2023
-
Merge pull request #447 from hernanponcedeleon/tags
Refactored Tags
Configuration menu - View commit details
-
Copy full SHA for a4bdcd7 - Browse repository at this point
Copy the full SHA a4bdcd7View commit details
Commits on May 26, 2023
-
Configuration menu - View commit details
-
Copy full SHA for cbb71bd - Browse repository at this point
Copy the full SHA cbb71bdView commit details -
Rename INonDet.getType() to .getNonDetType()
Configuration menu - View commit details
-
Copy full SHA for 80dc5bd - Browse repository at this point
Copy the full SHA 80dc5bdView commit details -
Configuration menu - View commit details
-
Copy full SHA for 4d02db9 - Browse repository at this point
Copy the full SHA 4d02db9View commit details -
Configuration menu - View commit details
-
Copy full SHA for 85c6e08 - Browse repository at this point
Copy the full SHA 85c6e08View commit details -
Configuration menu - View commit details
-
Copy full SHA for 8a7087b - Browse repository at this point
Copy the full SHA 8a7087bView commit details -
Replace INonDet(INonDetTypes,int) with INonDet(int,IntegerType,boolea…
…n,BigInteger,BigInteger)
Configuration menu - View commit details
-
Copy full SHA for 9e2dfd6 - Browse repository at this point
Copy the full SHA 9e2dfd6View commit details -
Configuration menu - View commit details
-
Copy full SHA for 0b51d7c - Browse repository at this point
Copy the full SHA 0b51d7cView commit details -
Configuration menu - View commit details
-
Copy full SHA for c4f8164 - Browse repository at this point
Copy the full SHA c4f8164View commit details -
Configuration menu - View commit details
-
Copy full SHA for c5e055c - Browse repository at this point
Copy the full SHA c5e055cView commit details -
Configuration menu - View commit details
-
Copy full SHA for 07bf04d - Browse repository at this point
Copy the full SHA 07bf04dView commit details
Commits on May 27, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 981d924 - Browse repository at this point
Copy the full SHA 981d924View commit details -
Merge pull request #448 from hernanponcedeleon/types0
[Rework] ExprInterface.getType()
Configuration menu - View commit details
-
Copy full SHA for 0a0f2f4 - Browse repository at this point
Copy the full SHA 0a0f2f4View commit details
Commits on Jun 2, 2023
-
Add Program.addConstant(INonDet) Add ProgramBuilder.newConstant(IntegerType,boolean) Add ProgramEncoder.encodeNondeterministicBounds() Add INonDet.setMin(BigInteger) Add INonDet.setMax(BigInteger) Add INonDet.setSourceName(String) Replace INonDet(int,IntegerType,boolean,BigInteger,BigInteger) with INonDet(int,IntegerType,boolean) Fix IllegalFormatConversionException in INonDet.toString()
Configuration menu - View commit details
-
Copy full SHA for b546501 - Browse repository at this point
Copy the full SHA b546501View commit details -
Register reads (rework) (#450)
* Renamed RegReaderData to RegReader Updated RegReader to return a set of (new) Register.Read objects. Updated all the users of RegReader Made MemEvent a RegReader. * Removed dead comments Updated some comments Simplified DynamicPureLoopCutting code Simplified ExecutionModel code * Improved Join.toString "Fixed" a problem in ExecutionModel * Removed unnecessary "implements RegReader" from Store and Xchg Replaced (few) tabs by whitespaces * Fixed Xchg not returning correct address dependencies. Added warnings when encountering reads of uninitialized registers in an execution.
Configuration menu - View commit details
-
Copy full SHA for 22b8bfa - Browse repository at this point
Copy the full SHA 22b8bfaView commit details -
Event as interface (rework) (#452)
* Renamed RegReaderData to RegReader Updated RegReader to return a set of (new) Register.Read objects. Updated all the users of RegReader Made MemEvent a RegReader. * Removed dead comments Updated some comments Simplified DynamicPureLoopCutting code Simplified ExecutionModel code * Improved Join.toString "Fixed" a problem in ExecutionModel * Removed unnecessary "implements RegReader" from Store and Xchg Replaced (few) tabs by whitespaces * Renamed Event to AbstractEvent * Introduced Event interface Renamed old abstract Event class to AbstractEvent Updated all code to work over the Event interface * Made RegReader and RegWriter extend new Event interface * Fixed Xchg not returning correcte address dependencies. Added warnings when encountering reads of uninitialized registers in an execution.
Configuration menu - View commit details
-
Copy full SHA for 3280019 - Browse repository at this point
Copy the full SHA 3280019View commit details
Commits on Jun 5, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 37e2909 - Browse repository at this point
Copy the full SHA 37e2909View commit details -
Configuration menu - View commit details
-
Copy full SHA for e6d0199 - Browse repository at this point
Copy the full SHA e6d0199View commit details -
Merge pull request #453 from hernanponcedeleon/types1
Program.getConstants() (rework)
Configuration menu - View commit details
-
Copy full SHA for 07c45f9 - Browse repository at this point
Copy the full SHA 07c45f9View commit details -
MemoryEvent as interface (#455)
* Replaced MemEvent by an interface MemoryEvent. The old MemEvent class is now AbstractMemoryEvent. * Removed MemoryEvent.canRace()
Configuration menu - View commit details
-
Copy full SHA for 7d1ffc4 - Browse repository at this point
Copy the full SHA 7d1ffc4View commit details -
Updated MemoryEvent to return MemoryAccess (work-in-progress) Changed AbstractMemoryEvent to SingleAddressMemoryEvent, which now serves as a common implementation for all single-address memory events.
Configuration menu - View commit details
-
Copy full SHA for eb1bfd5 - Browse repository at this point
Copy the full SHA eb1bfd5View commit details
Commits on Jun 6, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 7d77c20 - Browse repository at this point
Copy the full SHA 7d77c20View commit details -
Configuration menu - View commit details
-
Copy full SHA for a6465ee - Browse repository at this point
Copy the full SHA a6465eeView commit details -
Configuration menu - View commit details
-
Copy full SHA for 903db70 - Browse repository at this point
Copy the full SHA 903db70View commit details -
Configuration menu - View commit details
-
Copy full SHA for 94f2b07 - Browse repository at this point
Copy the full SHA 94f2b07View commit details -
Configuration menu - View commit details
-
Copy full SHA for 586ebc5 - Browse repository at this point
Copy the full SHA 586ebc5View commit details -
Configuration menu - View commit details
-
Copy full SHA for ca94c2e - Browse repository at this point
Copy the full SHA ca94c2eView commit details -
Configuration menu - View commit details
-
Copy full SHA for c125987 - Browse repository at this point
Copy the full SHA c125987View commit details
Commits on Jun 7, 2023
-
Made Init inherit from Store and simplified some code to uniformly ha…
…ndle Init and Store
Configuration menu - View commit details
-
Copy full SHA for 2b1578b - Browse repository at this point
Copy the full SHA 2b1578bView commit details -
Configuration menu - View commit details
-
Copy full SHA for ab9f9a8 - Browse repository at this point
Copy the full SHA ab9f9a8View commit details -
Configuration menu - View commit details
-
Copy full SHA for f4a64ae - Browse repository at this point
Copy the full SHA f4a64aeView commit details -
Configuration menu - View commit details
-
Copy full SHA for ee41011 - Browse repository at this point
Copy the full SHA ee41011View commit details -
Remove IValue.ONE and .ZERO Remove EventFactory.newFakeCtrlDep(Register,Label) Change signatures of some parser helper methods
Configuration menu - View commit details
-
Copy full SHA for 7e43c25 - Browse repository at this point
Copy the full SHA 7e43c25View commit details -
Configuration menu - View commit details
-
Copy full SHA for 540a2f3 - Browse repository at this point
Copy the full SHA 540a2f3View commit details -
Configuration menu - View commit details
-
Copy full SHA for a0d8caa - Browse repository at this point
Copy the full SHA a0d8caaView commit details
Commits on Jun 8, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 2547815 - Browse repository at this point
Copy the full SHA 2547815View commit details -
Configuration menu - View commit details
-
Copy full SHA for f3e27e6 - Browse repository at this point
Copy the full SHA f3e27e6View commit details
Commits on Jun 9, 2023
-
Configuration menu - View commit details
-
Copy full SHA for a242415 - Browse repository at this point
Copy the full SHA a242415View commit details -
Configuration menu - View commit details
-
Copy full SHA for 4ee0a6d - Browse repository at this point
Copy the full SHA 4ee0a6dView commit details -
Configuration menu - View commit details
-
Copy full SHA for 080e42c - Browse repository at this point
Copy the full SHA 080e42cView commit details -
Configuration menu - View commit details
-
Copy full SHA for a8e1449 - Browse repository at this point
Copy the full SHA a8e1449View commit details -
Configuration menu - View commit details
-
Copy full SHA for cf1bc8e - Browse repository at this point
Copy the full SHA cf1bc8eView commit details -
Configuration menu - View commit details
-
Copy full SHA for 6fceeb7 - Browse repository at this point
Copy the full SHA 6fceeb7View commit details
Commits on Jun 12, 2023
-
Merge ExpressionFactory.makeInteger(Expression,IntegerType) into .mak…
…eIntegerCast(Expression,IntegerType,boolean)
Configuration menu - View commit details
-
Copy full SHA for cc37d14 - Browse repository at this point
Copy the full SHA cc37d14View commit details -
Configuration menu - View commit details
-
Copy full SHA for 6df8223 - Browse repository at this point
Copy the full SHA 6df8223View commit details -
Configuration menu - View commit details
-
Copy full SHA for 32dc564 - Browse repository at this point
Copy the full SHA 32dc564View commit details -
Merge pull request #460 from hernanponcedeleon/memEventPrototype
[Prototype] Core memory events
Configuration menu - View commit details
-
Copy full SHA for 606142d - Browse repository at this point
Copy the full SHA 606142dView commit details -
Configuration menu - View commit details
-
Copy full SHA for ca9d64a - Browse repository at this point
Copy the full SHA ca9d64aView commit details -
Added MemoryOrder as metadata (for core events)
Removed MemoryEvent.getMo()
Configuration menu - View commit details
-
Copy full SHA for abaabb5 - Browse repository at this point
Copy the full SHA abaabb5View commit details -
Added event/common package that contains commonly shared code in the …
…form of abstract base classes. Updated most language-level events to use the new event/common package instead of inheriting from core events (work-in-progress) Added MemoryCoreEvent interface (not used yet).
Configuration menu - View commit details
-
Copy full SHA for 1b16c19 - Browse repository at this point
Copy the full SHA 1b16c19View commit details -
Merge pull request #457 from hernanponcedeleon/types2
ExpressionFactory
Configuration menu - View commit details
-
Copy full SHA for 222d28a - Browse repository at this point
Copy the full SHA 222d28aView commit details -
Added "withMo" methods to EventFactory to construct core events with …
…added MemoryOrder metadata attached
Configuration menu - View commit details
-
Copy full SHA for ff67fd4 - Browse repository at this point
Copy the full SHA ff67fd4View commit details -
Configuration menu - View commit details
-
Copy full SHA for 61005bb - Browse repository at this point
Copy the full SHA 61005bbView commit details
Commits on Jun 13, 2023
-
Configuration menu - View commit details
-
Copy full SHA for dcf23a8 - Browse repository at this point
Copy the full SHA dcf23a8View commit details -
Merge branch 'development_rework' into memoryAccess
# Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/lisa/RMW.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/tso/Xchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractMemoryEvent.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Init.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Load.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryEvent.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Store.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/rmw/RMWStore.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/rmw/RMWStoreExclusive.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicAbstract.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicCmpXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicLoad.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicStore.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLoad.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLock.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLockRead.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLockWrite.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMStore.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMUnlock.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWAbstract.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/SrcuSync.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmAbstractRMW.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmLoad.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmStore.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Create.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/InitLock.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Lock.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorBase.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorIMM.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorTso.java # dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java
Configuration menu - View commit details
-
Copy full SHA for 772a987 - Browse repository at this point
Copy the full SHA 772a987View commit details -
Configuration menu - View commit details
-
Copy full SHA for 191073b - Browse repository at this point
Copy the full SHA 191073bView commit details -
Cleaned up compilation schemes (removed mo for Power and some RISCV c…
…ompilations) Reformatted files
Configuration menu - View commit details
-
Copy full SHA for 0889492 - Browse repository at this point
Copy the full SHA 0889492View commit details -
Configuration menu - View commit details
-
Copy full SHA for d1a9b82 - Browse repository at this point
Copy the full SHA d1a9b82View commit details -
Configuration menu - View commit details
-
Copy full SHA for 0bfdf46 - Browse repository at this point
Copy the full SHA 0bfdf46View commit details -
Made SRCU a core event (temporarily)
Extended EventVisitor by visitMemCoreEvent Simplified SparseConditionalConstantPropagation again
Configuration menu - View commit details
-
Copy full SHA for b1417f5 - Browse repository at this point
Copy the full SHA b1417f5View commit details
Commits on Jun 15, 2023
-
Cleaned up formatting/commenting in compilation visitors.
Configuration menu - View commit details
-
Copy full SHA for 2fc8484 - Browse repository at this point
Copy the full SHA 2fc8484View commit details
Commits on Jun 18, 2023
-
Merge pull request #456 from hernanponcedeleon/memoryAccess
Add MemoryAccess and MemoryCoreEvents
Configuration menu - View commit details
-
Copy full SHA for 8e6158d - Browse repository at this point
Copy the full SHA 8e6158dView commit details
Commits on Jun 19, 2023
-
Added abstract "defaultString" method to events.
Added CustomStringify metadata (name is subject to change). Event.toString now uses the metadata of available and otherwise falls back to "defaultString"
Configuration menu - View commit details
-
Copy full SHA for 565156e - Browse repository at this point
Copy the full SHA 565156eView commit details -
Configuration menu - View commit details
-
Copy full SHA for 472cb7d - Browse repository at this point
Copy the full SHA 472cb7dView commit details -
Configuration menu - View commit details
-
Copy full SHA for e61654c - Browse repository at this point
Copy the full SHA e61654cView commit details -
Configuration menu - View commit details
-
Copy full SHA for 6fe1983 - Browse repository at this point
Copy the full SHA 6fe1983View commit details -
Added CoreCodeVerification pass to raise an error when encountering n…
…on-core code. This is temporarily used for debugging purposes.
Configuration menu - View commit details
-
Copy full SHA for b5767b1 - Browse repository at this point
Copy the full SHA b5767b1View commit details -
Improved error message of CoreCodeVerification
Configuration menu - View commit details
-
Copy full SHA for 48af79c - Browse repository at this point
Copy the full SHA 48af79cView commit details -
Made LLVMFence, LKMMFence and AtomicFence subclasses of FenceBase.
Made VisitorLKMM compile LKMMFence down to a core-level Fence.
Configuration menu - View commit details
-
Copy full SHA for 76b7b8e - Browse repository at this point
Copy the full SHA 76b7b8eView commit details -
Configuration menu - View commit details
-
Copy full SHA for 387b7d0 - Browse repository at this point
Copy the full SHA 387b7d0View commit details -
Configuration menu - View commit details
-
Copy full SHA for 31f12cc - Browse repository at this point
Copy the full SHA 31f12ccView commit details -
Configuration menu - View commit details
-
Copy full SHA for f456e42 - Browse repository at this point
Copy the full SHA f456e42View commit details -
Configuration menu - View commit details
-
Copy full SHA for 3de4fb3 - Browse repository at this point
Copy the full SHA 3de4fb3View commit details -
Made C11 AtomicLoad/Store and LLVM LlvmLoad/Store inherit from LoadBa…
…se resp. StoreBase. This reduces code duplication
Configuration menu - View commit details
-
Copy full SHA for 010cfbc - Browse repository at this point
Copy the full SHA 010cfbcView commit details -
Configuration menu - View commit details
-
Copy full SHA for 7f410e8 - Browse repository at this point
Copy the full SHA 7f410e8View commit details -
Improved printing of core-level RMWStores (to distinguish them from s…
…imple stores). Made LKMMUnlock non-core. Enabled CoreCodeVerification.
Configuration menu - View commit details
-
Copy full SHA for 2cc36ca - Browse repository at this point
Copy the full SHA 2cc36caView commit details -
Configuration menu - View commit details
-
Copy full SHA for 4ff91bd - Browse repository at this point
Copy the full SHA 4ff91bdView commit details -
Configuration menu - View commit details
-
Copy full SHA for e2264d1 - Browse repository at this point
Copy the full SHA e2264d1View commit details
Commits on Jun 20, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 6132740 - Browse repository at this point
Copy the full SHA 6132740View commit details -
Configuration menu - View commit details
-
Copy full SHA for 73774be - Browse repository at this point
Copy the full SHA 73774beView commit details -
Made CondJump, ExecutionStatus, EndAtomic, and RMWStore EventUsers Extended Event to be able to track users.
Configuration menu - View commit details
-
Copy full SHA for 62b24c7 - Browse repository at this point
Copy the full SHA 62b24c7View commit details -
Added missing Event.registerUser calls to EventUsers.
Cleaned up CondJumps usage "Label.getJumpSet"
Configuration menu - View commit details
-
Copy full SHA for b427850 - Browse repository at this point
Copy the full SHA b427850View commit details -
Configuration menu - View commit details
-
Copy full SHA for 6e13c0c - Browse repository at this point
Copy the full SHA 6e13c0cView commit details -
Configuration menu - View commit details
-
Copy full SHA for 55514bf - Browse repository at this point
Copy the full SHA 55514bfView commit details -
Merge pull request #462 from hernanponcedeleon/eventPrinter&reducedCore
Event printer & reduced core
Configuration menu - View commit details
-
Copy full SHA for 8fe4c67 - Browse repository at this point
Copy the full SHA 8fe4c67View commit details -
Added Event.detach and Event.tryDelete
Reduced usages of Event.setSuccessor and Event.getSuccessor to instead use Event.insertAfter if possible.
Configuration menu - View commit details
-
Copy full SHA for 08a5d03 - Browse repository at this point
Copy the full SHA 08a5d03View commit details -
Merge branch 'development_rework' into eventUser
# Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/CondJump.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java
Configuration menu - View commit details
-
Copy full SHA for 1a9255a - Browse repository at this point
Copy the full SHA 1a9255aView commit details -
Added a new error raised by ProgramBuilder.addChild when accidentally adding an already added event.
Configuration menu - View commit details
-
Copy full SHA for 9ed4fee - Browse repository at this point
Copy the full SHA 9ed4feeView commit details
Commits on Jun 21, 2023
-
Fixed and simplified implementations of EventUser.updateReferences vi…
…a new EventUser.moveUserReference helper function. Fixed CondJump automatically setting a thread on construction.
Configuration menu - View commit details
-
Copy full SHA for 8cd7717 - Browse repository at this point
Copy the full SHA 8cd7717View commit details -
Simplified Event.setSuccessor/getSuccessor: These should ONLY be used…
… under special circumstances. Added Event.forceDelete and replaced some usages by Event.tryDelete (work-in-progress)
Configuration menu - View commit details
-
Copy full SHA for abf11a4 - Browse repository at this point
Copy the full SHA abf11a4View commit details -
Configuration menu - View commit details
-
Copy full SHA for f785a15 - Browse repository at this point
Copy the full SHA f785a15View commit details -
Configuration menu - View commit details
-
Copy full SHA for f5bd595 - Browse repository at this point
Copy the full SHA f5bd595View commit details -
Merge pull request #464 from hernanponcedeleon/eventUser
Event user & more robust CFG handling
Configuration menu - View commit details
-
Copy full SHA for a331d02 - Browse repository at this point
Copy the full SHA a331d02View commit details
Commits on Jun 22, 2023
-
Merge branch 'development' into merge
# Conflicts: # dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/RMWAbstract.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/visitors/EventVisitor.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java # dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java
Configuration menu - View commit details
-
Copy full SHA for 1d46464 - Browse repository at this point
Copy the full SHA 1d46464View commit details -
Configuration menu - View commit details
-
Copy full SHA for 2db8ef7 - Browse repository at this point
Copy the full SHA 2db8ef7View commit details -
Merge pull request #468 from hernanponcedeleon/merge
Merge development into development_rework
Configuration menu - View commit details
-
Copy full SHA for 0e10cdd - Browse repository at this point
Copy the full SHA 0e10cddView commit details
Commits on Jun 24, 2023
-
Configuration menu - View commit details
-
Copy full SHA for e21ad42 - Browse repository at this point
Copy the full SHA e21ad42View commit details -
Configuration menu - View commit details
-
Copy full SHA for f6c5260 - Browse repository at this point
Copy the full SHA f6c5260View commit details -
Configuration menu - View commit details
-
Copy full SHA for 9d0b12a - Browse repository at this point
Copy the full SHA 9d0b12aView commit details -
Refactor & renaming of LKMM atomics.
Renamed RMWFetchOpBase.java to RMWOpResultBase to clearly communicate that it is more generally usable.
Configuration menu - View commit details
-
Copy full SHA for 3ff5e2a - Browse repository at this point
Copy the full SHA 3ff5e2aView commit details
Commits on Jun 25, 2023
-
Configuration menu - View commit details
-
Copy full SHA for b44f299 - Browse repository at this point
Copy the full SHA b44f299View commit details -
Configuration menu - View commit details
-
Copy full SHA for 9e502b3 - Browse repository at this point
Copy the full SHA 9e502b3View commit details -
Configuration menu - View commit details
-
Copy full SHA for 8b266bd - Browse repository at this point
Copy the full SHA 8b266bdView commit details -
Configuration menu - View commit details
-
Copy full SHA for 5d9b4c1 - Browse repository at this point
Copy the full SHA 5d9b4c1View commit details -
Configuration menu - View commit details
-
Copy full SHA for 7e5607b - Browse repository at this point
Copy the full SHA 7e5607bView commit details -
Configuration menu - View commit details
-
Copy full SHA for 2dde2f9 - Browse repository at this point
Copy the full SHA 2dde2f9View commit details -
Configuration menu - View commit details
-
Copy full SHA for c9b9da1 - Browse repository at this point
Copy the full SHA c9b9da1View commit details -
Merge pull request #475 from hernanponcedeleon/rmwBase
Rmw base classes & refactor
Configuration menu - View commit details
-
Copy full SHA for 6a254a7 - Browse repository at this point
Copy the full SHA 6a254a7View commit details -
Merge branch 'development' into test_merge
# Conflicts: # .github/workflows/maven.yml # dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java # dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/lisa/RMW.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/AtomOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/FenceWithId.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/RedOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/tso/Xchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/RMWAbstract.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicAbstract.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicCmpXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicLoad.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicStore.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicThreadFence.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFence.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLoad.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLock.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMStore.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMUnlock.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWAddUnless.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWCmpXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWFetchOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWOp.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWOpAndTest.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWOpReturn.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/RMWXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmAbstractRMW.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmCmpXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmXchg.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/event/visitors/EventVisitor.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadCondJumps.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorBase.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorIMM.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorTso.java # dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertBasic.java
Configuration menu - View commit details
-
Copy full SHA for ff5221b - Browse repository at this point
Copy the full SHA ff5221bView commit details
Commits on Jun 28, 2023
-
Generic Registers (Rework) (#471)
* Remove BExpr.isFalse(), BExpr.isTrue() Remove BConst.FALSE, BConst.TRUE * Remove IExpr.getBase() * Remove IExpr.isInteger() and .isBV() * Remove usage of IExpr * Register is no IExpr * Add encoding of boolean data * fixup! Fix GTE in makeGreaterOrEqual * Add ExpressionFactory.makeCast(Expression,Type) Rename .makeBoolean(Expression) into makeBooleanCast
Configuration menu - View commit details
-
Copy full SHA for e81e154 - Browse repository at this point
Copy the full SHA e81e154View commit details
Commits on Jun 29, 2023
-
Added functions + function-specific events (e.g. Return and Call) Simplified BoogieVisitor and related parsing classes.
Configuration menu - View commit details
-
Copy full SHA for f6cd58a - Browse repository at this point
Copy the full SHA f6cd58aView commit details
Commits on Jul 4, 2023
-
Parsing & thread creation (#479)
* Made FunctionType constructible via TypeFactory Added new Normalizer class to allow for normalization/canonicalization of object instances * Simplified ProgramBuilder and made it more robust Fixed PTX litmus test that referenced undefined threads. * Added ProgramBuilder factory methods All parser visitors now create a ProgramBuilder with correct source language and target architecture set. * Threads now always require a function type (automatically provided by the ProgramBuilder) * Added SymbolTable class (just a HashMap with String keys for now). Improved function validation done by ProgramBuilder. * Added VisitorBoogie.getOrNewEndOfScopeLabel and ProgramBuilder.getEndOfThreadLabel * Transformed helper classes to records and moved them to VisitorBoogie. * Removed VisitorBoogie.currentThread * Added Event.replaceAllUsages Use Event.replaceAllUsages in Compilation of pthread_create Removed matcher annotation events * Reworked pthread_create/join handling to more closely reflect their real semantics.
Configuration menu - View commit details
-
Copy full SHA for 7278dd2 - Browse repository at this point
Copy the full SHA 7278dd2View commit details -
Added proper type checks and conversions to avoid implicit casts: * Outline EncodingContext.makeVariable(String,Type) * SmackPredicates create integer casts * Start expects boolean register * RMWCmpXchgBase expects boolean register * Add Function.getOrNewRegister(String,Type) * Assertions use boolean registers * AtomicCmpXchg uses boolean registers * Add type-safety * Remove ambiguously-typed integer value factories. * Fix type-unsafe assignments in LKMM-related parser and compiler * Fix type-unsafe assignments in LKMMAddUnless and LKMMOpAndTest * Fix model value parser in WitnessGraph Fix type-unsafe assignments in VisitorLitmusLISA * Fixup --------- Co-authored-by: Thomas Haas <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 753837c - Browse repository at this point
Copy the full SHA 753837cView commit details
Commits on Jul 5, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 5f9027a - Browse repository at this point
Copy the full SHA 5f9027aView commit details
Commits on Jul 11, 2023
-
Inlining & Threading (rework) (#483)
* Add Inlining * Fixes Proper renaming in Inlining Deep copy of DirectFunctionCall * Inlining does not skip entry * Function is an Expression * Function expressions are used in the parser. Pthread_create and join are parsed and calls to them are generated as expected outside of inline mode. * Simplified/Generalized parsing of special functions. * Add LlvmCmpXchg.setStructRegister(int,Register) * Add ThreadCreation * Simplified Pthread.Start event * Some fixes in ThreadCreation pass * Reworked ThreadCreation * Made VisitorBoogie recognize more functions as user-declared Added new Events for passing parameters across threads, and updated ThreadCreation pass to generate them. Updated CoreCodeVerification to recognize new threading-related events. Updated inlining pass to generate annotations around inlined calls. * Made VisitorBoogie recognize more functions as user-declared Updated Alias analysis to recognize new threading-related events Refactor/renaming * Added Event.replaceBy(List<Event>) Added new thread events to EventFactory Updated ThreadCreation to not generate Pthread events Fixed issue in ExecutionModel with boolean valued memory accesses. * Added proper tid propagation to ThreadCreation (temporary solution) * Added .bpl files for three more unit tests. These tests run correctly with the new ThreadCreation pass, but still fail without, so they are disabled for now. * Some refactoring * Added handling for thread-local variables. Added new thread_local.c unit test * Proper naming of generated dummy registers for thread creation * Improved printing of threads. Better automatic naming for nameless threads. * Fixed minor issue with undefined initialize function * Improvements in ThreadCreation * Moved static memory initialization from the parser into a pass. * Removed thread creation from parser (commented out for testing) Adding logging to ThreadCreation * Added parsing error when encountering main without body. Adding missing StaticMemoryInitializer pass into ProcessingManager * Enabled 3 more unit tests. First cleanup pass of Parser code (removing inline mode). * Full cleanup of Boogie parser * Deleted now unused Pthread events * Fixed ExecutionModel not recognizing new ThreadArgument event (this caused only warnings, but no semantic errors). * Various Refactoring * Fixed accidental bug * Implemented first set of feedback changes. * Removed unused code. Added FIXME for recursion handling --------- Co-authored-by: Thomas Haas <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 0dd7003 - Browse repository at this point
Copy the full SHA 0dd7003View commit details
Commits on Jul 13, 2023
-
* Add IntrinsicsInlining * Added new nondet_loop.c code + unit test. --------- Co-authored-by: Thomas Haas <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 037ba25 - Browse repository at this point
Copy the full SHA 037ba25View commit details
Commits on Jul 15, 2023
-
Configuration menu - View commit details
-
Copy full SHA for a201493 - Browse repository at this point
Copy the full SHA a201493View commit details -
* Various minor fixes: - Add OIds in ThreadCreation - Copy metadata from call statements into marker events when inlining. - Fixed ExecutionModel printing warnings for ThreadArguments - Renamed FunCall/FunRet to FunCallMarker/FunReturnMarker to distinguish them from proper call/return events. - Made more internals of AbstractEvent private. * Fixed ExecutionStatus to work with boolean registers. * Removed unnecessary usages of ExecutionStatus. Use boolean type register for ExecutionStatus whenever possible. * Improved logging * Changed ExecutionGraphVisualizer to also create nodes for threading-related events. Increased weighting of po-edges * Added handling of pthread_exit * Changed heuristic to detect whether Smack created static initialization. Avoid creating memory for procedure address constants. * Refactoring. RelationAnalysis now logs #Relations and #Axioms
Configuration menu - View commit details
-
Copy full SHA for 0f327ea - Browse repository at this point
Copy the full SHA 0f327eaView commit details
Commits on Jul 27, 2023
-
Configuration menu - View commit details
-
Copy full SHA for b9db99c - Browse repository at this point
Copy the full SHA b9db99cView commit details
Commits on Jul 28, 2023
-
Function passes & Thread creation after unrolling (#492)
* Added FunctionProcessor interface. Transformed many ProgramProcessors to FunctionProcessors Moved ThreadCreation to after compilation and unrolling (can handle pthread_create in loops). * Included dat3m.h to some tests (+ regenerated their .bpl files). * Register now contains a Function rather than a functionId. Removed Register.NO_FUNCTION. * Renamed EventIdReassignment to IdReassignment. It now also reassigns function ids, making sure that threads get their Ids first. * Added Printer.Mode to only print threads, functions, or both. Also added short output for skipped init threads when printing.
Configuration menu - View commit details
-
Copy full SHA for 1b1dc70 - Browse repository at this point
Copy the full SHA 1b1dc70View commit details
Commits on Aug 3, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 7b07232 - Browse repository at this point
Copy the full SHA 7b07232View commit details -
Add proper control-flow dependencies between spawned threads and their spawners/creators
Configuration menu - View commit details
-
Copy full SHA for 16d4e0e - Browse repository at this point
Copy the full SHA 16d4e0eView commit details
Commits on Aug 8, 2023
-
* Generalized ThreadCreation to allow dynmaic joining. * Cleaned up ThreadCreation's handling of pthread_join. Removed unsound propagation code. Removed must-rf edges related to pthread_join (hard to establish and exploit with dynamic thread joins).
Configuration menu - View commit details
-
Copy full SHA for a89dd7e - Browse repository at this point
Copy the full SHA a89dd7eView commit details -
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 5378937 - Browse repository at this point
Copy the full SHA 5378937View commit details -
Remove LLVM grammar and parser
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for c5300f0 - Browse repository at this point
Copy the full SHA c5300f0View commit details -
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Configuration menu - View commit details
-
Copy full SHA for 1aa9033 - Browse repository at this point
Copy the full SHA 1aa9033View commit details