Dat3M 4.3.1 is out!

What’s New

• Support for unary predicates in .cat
• Support for the memtrack property of SVCOMP
• Support for more SPIRV instructions
• Allow functions other than main as the entry point

What's Changed

• Make GEPToAddition recursive to handle nested GEPExpr by @marcrobm in #922
• Slightly better memory encoding by @ThomasHaas in #925
• Allow unknown annotations in spirv files by @natgavrilenko in #926
• Better program printing by @ThomasHaas in #924
• Re-enable RelationAnalysis tests by @hernanponcedeleon in #929
• Add action to enforce PRs go to development branch by @hernanponcedeleon in #930
• [SPIRV] Add support for OpNot by @hernanponcedeleon in #928
• [SPIRV] Add support for OpBitCount by @hernanponcedeleon in #931
• [SPIRV] Add support for GLSL extensions FindILsb by @hernanponcedeleon in #932
• No static relation encoding by default + removed unnecessary code by @ThomasHaas in #934
• [SPIRV] Fix support for OpShiftRightArithmetic by @hernanponcedeleon in #933
• Consider if axioms are flagged in their toString() method by @hernanponcedeleon in #936
• Add option to select entry point by @hernanponcedeleon in #935
• [SPIRV] Add support for OpUnreachable by @hernanponcedeleon in #938
• [RA] Fix propagation for negated/flagged axioms by @hernanponcedeleon in #939
• [SPIRV] Validate return type of external instructions by @natgavrilenko in #940
• [SPIRV] Add support for SRem, SMax, UMax, SMin and UMin by @hernanponcedeleon in #937
• [LLVM] Fix warning msg when asm parser fails by @hernanponcedeleon in #943
• Devirtualization with proper addresses by @ThomasHaas in #944
• Support unary predicates in cat by @xeren in #908
• Add all Vulkan storage classes by @natgavrilenko in #945
• Add EncodingUtils class by @ThomasHaas in #942
• Update LKMM model and compilation by @hernanponcedeleon in #893
• Added missing storage class combination by @natgavrilenko in #949
• Fix Extended Relation Analysis by @xeren in #951
• AutoCloseable IREvaluator by @xeren in #952
• Fix#955: Zero extension on integer encoding now makes value positive by @ThomasHaas in #956
• Remove non-determinism in Llvm parser and Internal representation by @xeren in #953
• Implement visitTagSet in LazyEncodeSets by @hernanponcedeleon in #959
• Remove outdated code in RefinementSolver by @hernanponcedeleon in #961

New Contributors

• @marcrobm made their first contribution in #922

Full Changelog: 4.3.0...4.3.1

Dat3M 4.3.0 is out!

What’s New

• Added support for mixed size accesses (currently only used for aarch64)
• Added support for non-termination in the presence of side-effects
• Better support for SPIR-V (including its OpenCL flavor)
• Added support for hierarchical forward progress models
• Detection of undefined / external functions being called
• Added support for clang / llvm 19
• Better support for LKMM intrinsics in C code

What's Changed

• Add OpUMod by @natgavrilenko in #781
• Removed SpecId decoration by @natgavrilenko in #779
• Add support for encoding tuples (Tuple theory) by @ThomasHaas in #775
• Fix CI tests by @CapZTr in #784
• Add domain identities to CAAT & remove dangerous fallback code in ExecutionGraph by @ThomasHaas in #785
• Litmus vulkan cleanup by @natgavrilenko in #787
• Improve spinloop detection by @ThomasHaas in #786
• Use conditional jump in spirv structured control flow by @natgavrilenko in #788
• New Execution Model by @CapZTr in #783
• Fix parsing of atomic_exchange for litmus C by @hernanponcedeleon in #791
• Add filter spec to spirv tests by @natgavrilenko in #795
• Use alignment information in VisitorLlvm.visitAllocaInst() by @hernanponcedeleon in #796
• Visitor for OpExtension by @natgavrilenko in #799
• Fix race condition in model.evaluate() by @natgavrilenko in #801
• Unrolling control barriers by @natgavrilenko in #797
• Move axiom from AddInitReadHandling to stdlib.cat by @hernanponcedeleon in #804
• Added PTX litmus tests by @natgavrilenko in #806
• Streamline CF encoding of jumps and Cbs by @ThomasHaas in #808
• Fix nasty encoding bug related to XRA by @ThomasHaas in #807
• Simplify IR Manipulation operations & Update existing code by @ThomasHaas in #803
• Update vulkan model by @natgavrilenko in #805
• Parallel execution of tests in the CI by @tonghaining in #810
• Add support for OpenCL SPIR-V by @tonghaining in #792
• Add support for inline asm by @StefanoDalMas in #802
• Add dartagnan script by @db7 in #811
• Use ExtractExpr for spirv OpCompositeExtract by @natgavrilenko in #815
• Add spirv bitwise ops for composite types by @natgavrilenko in #816
• Added source code of clients for ck tests by @StefanoDalMas in #819
• Fix MemToReg by @xeren in #814
• update opencl barrier to use single event by @tonghaining in #818
• Improved automatic data type conversion along rf-edges (+ related improvements) by @ThomasHaas in #820
• Improved expressions package by @ThomasHaas in #822
• Side-effectful Nontermination by @ThomasHaas in #772
• Fix nontermination detection by @ThomasHaas in #824
• Use LEFT_TO_RIGHT when enforcing same value in encoding of final valu… by @hernanponcedeleon in #825
• Fix bug with InsertExpr by @ThomasHaas in #826
• New client for ck's stack_empty benchmark by @StefanoDalMas in #823
• scripts: Add -bound option to dartagnan script by @db7 in #827
• Tag AbortIf events as EXCEPTIONAL_TERMINATION by @hernanponcedeleon in #830
• Fix arm visitor for ck/ebr client by @StefanoDalMas in #831
• Cleanup spirv tests by @natgavrilenko in #832
• Fix wrong must-set computation for IDD by @ThomasHaas in #833
• General BlockingEvent interface by @ThomasHaas in #834
• Add -solver option to dartagnan script by @db7 in #836
• Fallback to System::loadLibrary if sosy's loader fails by @db7 in #835
• RISCV and PPC visitors by @StefanoDalMas in #828
• Add SVCOMP support for nontermination by @hernanponcedeleon in #837
• using record class for CmpInstruction in litmusAArch64 and LitmusPPC visitors by @StefanoDalMas in #839
• Model pthread_join() as spinloop by @CapZTr in #841
• Fix first event of threads missing in witness graphs by @ThomasHaas in #842
• Fixes bug introduced in #833 by @ThomasHaas in #844
• Run weekly on development by @hernanponcedeleon in #846
• Using GEPExpression in spirv access chain and code cleanup by @natgavrilenko in #843
• Hierarchical scheduling by @ThomasHaas in #848
• Add debug mode to dartagnan script. Off by default by @hernanponcedeleon in #851
• Always include DAT3M_HOME/include when compiling code by @hernanponcedeleon in #854
• Use proper exit codes by @hernanponcedeleon in #853
• Add logger to NonTerminationEncoder by @hernanponcedeleon in #857
• LOBE Progress Model by @ThomasHaas in #858
• Deprecate *.spv.dis. Use *.spvasm instead by @hernanponcedeleon in #859
• Add support for Barrier Inlining by @tonghaining in #856
• Add missing KHR definitions by @natgavrilenko in #863
• Add support for vectors in OpsArithmetic by @hernanponcedeleon in #862
• Add new OpsComposite, OpConversion support by @tonghaining in #861
• Spir-V parser: Multiline string literal and minor updates by @natgavrilenko in #865
• Fix parser tests by @hernanponcedeleon in #867
• Add missing tests to CI by @hernanponcedeleon in #866
• Add leading zeros when formatting milliseconds by @tcherrou in #868
• Fix parsing of default value for progress models by @ThomasHaas in #860
• Treat calls to unknown functions as assert(0) by @hernanponcedeleon in #871
• Add support for OpVectorShuffle by @hernanponcedeleon in #870
• Add OpenCL ThreadGrid by @tonghaining in #855
• Add benchmarks from MICRO 2024 ScopeAdvice paper by @hernanponcedeleon in #873
• Regenerate OpenCL tests with keeping the variable names by @tonghaining in #874
• Fix wrong simplification of ExtractExpr by @ThomasHaas in #876
• Better support for IR-level threading and better handling of pthread_join by @ThomasHaas in #847
• LLVM Debug Records by @xeren in #879
• Sound detection of non-terminating loops containing control barriers by @ThomasHaas in #877
• OpCompositeConstruct and vector and aggregate values on memory operations by @hernanponcedeleon in #864
• Add Entrypoint class to describe the entry point of a Program by @ThomasHaas in #881
• Fix direct data and addr dependency extraction for witness by @CapZTr in #875
• Add support for SPV_KHR_storage_buffer_storage_class by @hernanponcedeleon in #884
• Unifying SMT Formulas & Expressions: TypedFormula & more by @ThomasHaas in #869
• Throw descriptive erro...

Dat3M 4.2.0 is out!

What's Changed

• Update README.md by @hernanponcedeleon in #707
• add support to show source location in witness graph for spirv by @CapZTr in #738
• Pass the C file to the svcomp runner rather than the optimized llvm by @hernanponcedeleon in #739
• Add support for atomic_exchange_explicit in litmus code by @hernanponcedeleon in #740
• Backwards reaching definitions by @xeren in #726
• Better may set for sync barrier by @natgavrilenko in #745
• Fix UI parsing by @ThomasHaas in #747
• Relation analysis with immutable and lazy data structures by @natgavrilenko in #743
• Updated model in spirv tests by @natgavrilenko in #749
• Support for Apple silicon by @hernanponcedeleon in #748
• Some improvements to aarch64 pseudo-assembly by @hernanponcedeleon in #741
• Add support for show statement in cat parser by @hernanponcedeleon in #742
• Introduce stdlib.cat by @hernanponcedeleon in #751
• Add support for variable-sized and variable-aligned allocations by @ThomasHaas in #750
• Require the existence of violation node when validate violation witness by @hernanponcedeleon in #754
• Add OpenCL Model by @tonghaining in #744
• Fix overlap queries in Alias Analysis by @xeren in #753
• Configuration files and management by @xeren in #752
• Svcomp config by @hernanponcedeleon in #756
• Fix #757 by @ThomasHaas in #758
• Allow bounds to be saved to and loaded from files by @hernanponcedeleon in #759
• Improve PPC grammar and visitor by @hernanponcedeleon in #762
• Fix usages of non-determinism in intrinsics by @ThomasHaas in #763
• Improvements for SVCOMP 2025 by @hernanponcedeleon in #765
• Check if events may alias when deriving RA knowledge from witnesses (… by @hernanponcedeleon in #766
• Fix witnesses excluding the rf edges they enforce. by @xeren in #771
• Spirv OpUndef by @natgavrilenko in #769
• Remove svcomp specific options by @hernanponcedeleon in #773
• Support explicitly defined offsets in aggregate type by @natgavrilenko in #770
• Remove empty tag from vulkan litmus tests by @natgavrilenko in #774
• Support of Showing Local Events Location in Spirv by @CapZTr in #761
• Fix handling of empty type by @ThomasHaas in #776
• Further changes for SVCOMP 2025 by @hernanponcedeleon in #777
• Update to version 4.2.0 by @hernanponcedeleon in #782

New Contributors

• @CapZTr made their first contribution in #738

Full Changelog: 4.1.0...4.2.0

Dat3M 4.1.0 is out!

What's Changed

• Lazy method supports dataraces/cat_spec by @ThomasHaas in #660
• Option to get dartagnan version by @hernanponcedeleon in #662
• New Pointer Analysis by @xeren in #616
• Add vmm version 0.9.1 by @hernanponcedeleon in #664
• Log a warning instead of throwing an exception when opt is not availa… by @hernanponcedeleon in #666
• Propagate correct memory order tags when compiling to C11 by @hernanponcedeleon in #665
• Fix collectSideEffects for manually annotated spinloops by @hernanponcedeleon in #669
• New AssignmentInlining pass by @ThomasHaas in #667
• Streamline witness options by @hernanponcedeleon in #670
• Add atomicity axiom to sc.cat by @hernanponcedeleon in #671
• Add 4 litmus tests demonstrating unordered failing cmpxchg. by @hernanponcedeleon in #672
• Check all three properties by default by @hernanponcedeleon in #675
• Add some missing LKMM tests by @hernanponcedeleon in #677
• Remove support for LISA format by @hernanponcedeleon in #678
• Support fences as inline assembly by @hernanponcedeleon in #679
• Fix performance issue in DominatorTree.computePredecessorMap by @ThomasHaas in #680
• Lazy cycle detection in inclusion based ailas analysis by @xeren in #676
• Replace several back jumps with via forward jumping by @hernanponcedeleon in #681

Full Changelog: 4.0.1...4.1.0

Dat3M 4.0.1 is out!

This release does not contain major new features. It is mostly code refactoring, bug fixing and improving usability of the tool.

Dat3M 4.0.0 is out!

These are the main changes of this version:

• More precise support of the C language (function pointers, dynamic memory allocation, dynamic thread creation, and recursion)
• Support llvm files as input
• Remove boogie as supported input format
• Remove dependencies on smack and atomic-replace pass
• Implement static analysis of memory models, as described in the OOSPLA’23 paper
• Support for PTX (v6.0 and v7.5) and vulkan memory models
• Several changes related to SVCOMP 2024 participation
• Support for many intrinsics (pthread, llvm, UBSAN)
• Update JavaSMT to version 4.1.0
• Fix unsoundness of symmetry learning
• Optimize memory consumption for RA sets
• Bound refining (CAAT)
• Update LKMM to latest version
• Support SRCU for LKMM
• Allow to update relations in cat
• Improve user output (lines of code and call stack related to violations / witnesses)
• Add coverage report
• Make semantics of pthread events closer to reality
• Force addresses to be even (as in reality)
• Fix / improve liveness encoding
• Improve performance of alias analysis
• Improve / fix compilation schemes
• Replace constant propagation by sparse conditional constant propagation
• Improve most program transformation passes
• Fix refinement cutting
• Add support for ARM-based MacOS
• Move to java 17
• Several refactors / bug fixing

Dat3M 3.1.1 is out!

This release contains our submission for SVCOMP 2023.

It mostly contains changes related to code refactoring and bug fixing for SVCOMP.

Dat3M 3.1.0 is out!

These are the main changes of this version:

• Implements the theory solver for CAAT (Consistency as a Theory) as described in the OOSPLA’22 paper
• Adds support for checking liveness
• Adds support to RC11, IMM and RISCV memory models
• Updates the support to the latests version of LKMM (including data races)
• Implements the compilation schemes from LKMM to hardware models
• Adds macro __VERIFIER_loop_bound to use different unrolling bounds for specific loops
• Adds option encoding.wmm.idl2sat to encode acyclicity constraint using SAT instead of IDL
• Adds option witness.graphviz to generate violation graphs
• Updates JavaSMT version to 3.13.3
• Several bug fixing and performance improvements

Dat3M 3.0.0 is out!

This new major version contains several improvements:

• Support for several SMT solvers based on JavaSMT
• Several performance improvements
• New docker container for easy use
• Extended compilation scheme for more instructions and architectures
• Support for validation of violation witnesses
• Drop support for IDL and KLEENE encodings
• Drop support for Porthos
• Bug fixing

This is the version participating in SVCOMP 2022.

Dat3M 2.0.7 is out!

This is the version participating in SVCOMP 2021. The main new features are listed below.

• Support for bit-vectors
• Improved (machine readable) witness generation
• Checking different properties: currently reachability and no-data-race