Release GenMC v0.10.2

Signed-off-by: Michalis Kokologiannakis <[email protected]>

CHANGELOG.md

@@ -7,7 +7,24 @@ released.
 
 ## [Unreleased]
 
-- Documentation
+## [0.10.2] - 2024.09.11
+### Added
+
+- Support for LLVM 17/18
+- GenMC now warns when memory is not freed
+- Minor performance improvements
+- Landing page for doxygen + rudimentary development documentation
+
+### Changed
+
+- `__VERIFIER_assume()` and `__VERIFIER_spin_end()` now take a boolean argument (instead of int)
+- GenMC now uses the new LLVM pass manager
+- IMM performance may incur a minor penalty
+- Project layout under `src`
+
+### Fixes
+
+- Minor bug fixes
 
 ## [0.10.1] - 2024.02.22
 ### Fixes

Makefile.am

@@ -24,92 +24,72 @@ nobase_genmc_HEADERS = \
 
 noinst_LIBRARIES = libgenmc.a
 libgenmc_a_SOURCES = \
-  src/ASize.cpp src/ASize.hpp \
-  src/BisimilarityCheckerPass.cpp src/BisimilarityCheckerPass.hpp \
-  src/Bitmask.hpp \
-  src/BoundDecider.cpp src/BoundDecider.hpp \
-  src/CallInfoCollectionPass.cpp src/CallInfoCollectionPass.hpp \
-  src/CodeCondenserPass.cpp src/CodeCondenserPass.hpp \
-  src/ContextBoundDecider.cpp src/ContextBoundDecider.hpp \
-  src/Calculator.hpp \
-  src/CallInstWrapper.hpp \
-  src/ConfirmationAnnotationPass.cpp src/ConfirmationAnnotationPass.hpp \
-  src/Config.cpp src/Config.hpp \
-  src/DeclareInternalsPass.cpp src/DeclareInternalsPass.hpp \
-  src/DefineLibcFunsPass.cpp src/DefineLibcFunsPass.hpp \
-  src/DepExecutionGraph.cpp src/DepExecutionGraph.hpp \
-  src/DepInfo.cpp src/DepInfo.hpp \
-  src/DepTracker.hpp \
-  src/DepView.cpp src/DepView.hpp \
-  src/DriverFactory.hpp \
-  src/EliminateAnnotationsPass.cpp src/EliminateAnnotationsPass.hpp \
-  src/EliminateCASPHIsPass.cpp src/EliminateCASPHIsPass.hpp \
-  src/EliminateCastsPass.cpp src/EliminateCastsPass.hpp \
-  src/EliminateRedundantInstPass.cpp src/EliminateRedundantInstPass.hpp \
-  src/EliminateUnusedCodePass.cpp src/EliminateUnusedCodePass.hpp \
-  src/Error.hpp \
-  src/EscapeCheckerPass.cpp src/EscapeCheckerPass.hpp \
-  src/Event.cpp src/Event.hpp \
-  src/EventAttr.hpp \
-  src/EventLabel.cpp src/EventLabel.hpp \
-  src/Execution.cpp \
-  src/ExecutionGraph.cpp src/ExecutionGraph.hpp \
-  src/ExternalFunctions.cpp \
-  src/FunctionInlinerPass.cpp src/FunctionInlinerPass.hpp \
-  src/GenMCDriver.cpp src/GenMCDriver.hpp \
-  src/GraphIterators.hpp \
-  src/IMMDriver.cpp src/IMMDriver.hpp \
-  src/InstAnnotator.cpp src/InstAnnotator.hpp \
-  src/Interpreter.cpp Interpreter.h \
-  src/InterpreterEnumAPI.cpp src/InterpreterEnumAPI.hpp \
-  src/IntrinsicLoweringPass.cpp src/IntrinsicLoweringPass.hpp \
-  src/LabelVisitor.hpp \
-  src/LoadAnnotationPass.cpp src/LoadAnnotationPass.hpp \
-  src/LocalSimplifyCFGPass.cpp src/LocalSimplifyCFGPass.hpp \
-  src/Logger.hpp \
-  src/LLVMModule.cpp src/LLVMModule.hpp \
-  src/LLVMUtils.cpp src/LLVMUtils.hpp \
-  src/LoopUnrollPass.cpp src/LoopUnrollPass.hpp \
-  src/LoopJumpThreadingPass.cpp src/LoopJumpThreadingPass.hpp \
-  src/Matrix2D.hpp Matrix2D.tcc \
-  src/MaximalIterator.hpp \
-  src/MDataCollectionPass.hpp src/MDataCollectionPass.cpp \
-  src/MemAccess.hpp \
-  src/MMDetectorPass.cpp src/MMDetectorPass.hpp \
-  src/ModuleID.hpp \
-  src/ModuleInfo.cpp src/ModuleInfo.hpp \
-  src/NameInfo.cpp src/NameInfo.hpp \
-  src/Parser.cpp src/Parser.hpp \
-  src/PromoteMemIntrinsicPass.cpp src/PromoteMemIntrinsicPass.hpp \
-  src/PropagateAssumesPass.cpp src/PropagateAssumesPass.hpp \
-  src/RADriver.cpp src/RADriver.hpp \
-  src/RC11Driver.cpp src/RC11Driver.hpp \
-  src/Revisit.cpp src/Revisit.hpp \
-  src/RoundBoundDecider.cpp src/RoundBoundDecider.hpp \
-  src/SAddr.cpp src/SAddr.hpp \
-  src/SAddrAllocator.hpp \
-  src/SCDriver.cpp src/SCDriver.hpp \
-  src/SExpr.tcc src/SExpr.hpp \
-  src/SExprVisitor.tcc src/SExprVisitor.hpp \
-  src/Stamp.cpp src/Stamp.hpp \
-  src/SVal.cpp src/SVal.hpp \
-  src/SpinAssumePass.cpp src/SpinAssumePass.hpp \
-  src/WBIterator.hpp \
-  src/ThreadInfo.hpp \
-  src/ThreadPinner.cpp src/ThreadPinner.hpp \
-  src/ThreadPool.cpp src/ThreadPool.hpp \
-  src/TSODriver.cpp src/TSODriver.hpp \
-  src/WorkSet.hpp src/WorkSet.cpp \
-  src/value_ptr.hpp \
-  src/Verbosity.hpp src/Verbosity.cpp \
-  src/VectorClock.hpp src/VectorClock.cpp \
-  src/VerificationError.hpp src/VerificationError.cpp \
-  src/View.hpp src/View.cpp \
-  src/VSet.hpp src/VSet.tcc
+  src/ADT/DepView.cpp \
+  src/ADT/VectorClock.cpp \
+  src/ADT/View.cpp \
+  src/Config/Config.cpp \
+  src/Config/Verbosity.cpp \
+  src/ExecutionGraph/DepExecutionGraph.cpp \
+  src/ExecutionGraph/DepInfo.cpp \
+  src/ExecutionGraph/Event.cpp \
+  src/ExecutionGraph/EventLabel.cpp \
+  src/ExecutionGraph/ExecutionGraph.cpp \
+  src/ExecutionGraph/Stamp.cpp \
+  src/Runtime/Execution.cpp \
+  src/Runtime/ExternalFunctions.cpp \
+  src/Runtime/Interpreter.cpp \
+  src/Runtime/InterpreterEnumAPI.cpp \
+  src/Static/LLVMModule.cpp \
+  src/Static/LLVMUtils.cpp \
+  src/Static/ModuleInfo.cpp \
+  src/Static/Transforms/BisimilarityCheckerPass.cpp \
+  src/Static/Transforms/CallInfoCollectionPass.cpp \
+  src/Static/Transforms/CodeCondenserPass.cpp \
+  src/Static/Transforms/ConfirmationAnnotationPass.cpp \
+  src/Static/Transforms/DeclareInternalsPass.cpp \
+  src/Static/Transforms/DefineLibcFunsPass.cpp \
+  src/Static/Transforms/EliminateAnnotationsPass.cpp \
+  src/Static/Transforms/EliminateCASPHIsPass.cpp \
+  src/Static/Transforms/EliminateCastsPass.cpp \
+  src/Static/Transforms/EliminateRedundantInstPass.cpp \
+  src/Static/Transforms/EliminateUnusedCodePass.cpp \
+  src/Static/Transforms/EscapeCheckerPass.cpp \
+  src/Static/Transforms/FunctionInlinerPass.cpp \
+  src/Static/Transforms/InstAnnotator.cpp \
+  src/Static/Transforms/IntrinsicLoweringPass.cpp \
+  src/Static/Transforms/LoadAnnotationPass.cpp \
+  src/Static/Transforms/LocalSimplifyCFGPass.cpp \
+  src/Static/Transforms/LoopJumpThreadingPass.cpp \
+  src/Static/Transforms/LoopUnrollPass.cpp \
+  src/Static/Transforms/MDataCollectionPass.cpp \
+  src/Static/Transforms/MMDetectorPass.cpp \
+  src/Static/Transforms/PromoteMemIntrinsicPass.cpp \
+  src/Static/Transforms/PropagateAssumesPass.cpp \
+  src/Static/Transforms/SpinAssumePass.cpp \
+  src/Support/ASize.cpp \
+  src/Support/NameInfo.cpp \
+  src/Support/Parser.cpp \
+  src/Support/SAddr.cpp \
+  src/Support/SVal.cpp \
+  src/Support/ThreadPinner.cpp \
+  src/Support/ThreadPool.cpp \
+  src/Verification/GenMCDriver.cpp \
+  src/Verification/WorkSet.cpp \
+  src/Verification/VerificationError.cpp \
+  src/Verification/Revisit.cpp \
+  src/Verification/Consistency/BoundDecider.cpp \
+  src/Verification/Consistency/ContextBoundDecider.cpp \
+  src/Verification/Consistency/IMMDriver.cpp \
+  src/Verification/Consistency/RADriver.cpp \
+  src/Verification/Consistency/RC11Driver.cpp \
+  src/Verification/Consistency/RoundBoundDecider.cpp \
+  src/Verification/Consistency/SCDriver.cpp \
+  src/Verification/Consistency/TSODriver.cpp \
+  src/main.cpp
 
 TESTS=scripts/fast-driver.sh scripts/randomize-driver.sh
 
-AM_CXXFLAGS = -DINCLUDE_DIR=\"$(pkgincludedir)/$(pkg)/include\" -DSRC_INCLUDE_DIR=\"$(abs_top_srcdir)/include\" $(COVERAGE_CXXFLAGS)
+AM_CXXFLAGS = -I$(abs_top_srcdir)/src -DINCLUDE_DIR=\"$(pkgincludedir)/$(pkg)/include\" -DSRC_INCLUDE_DIR=\"$(abs_top_srcdir)/include\" $(COVERAGE_CXXFLAGS)
 bin_PROGRAMS = genmc
 genmc_SOURCES = src/main.cpp
 genmc_LDADD = libgenmc.a -lpthread $(COVERAGE_LDFLAGS)

README.md

@@ -1,7 +1,5 @@
-GenMC
+GenMC: Generic Model Checking for C Programs
 =====
-Generic Model Checking for C Programs
--------------------------------------
 
 GenMC is a stateless model checker for C programs that works on the
 level of LLVM Intermediate Representation.
@@ -90,7 +88,7 @@ For a default build issue:
 
 		./genmc [options] <file>
 
-* For more detailed usage examples please refer to the [manual](doc/manual.pdf).
+* For more detailed usage examples please refer to the [manual](doc/manual.md).
 
 
 <a name="troubleshooting">Troubleshooting</a>

configure.ac

@@ -1,4 +1,4 @@
-AC_INIT([GenMC], [0.10.1], [[email protected]], [genmc], [https://plv.mpi-sws.org/genmc])
+AC_INIT([GenMC], [0.10.2], [[email protected]], [genmc], [https://plv.mpi-sws.org/genmc])
 
 m4_include([m4/ax_llvm.m4])
 m4_include([m4/ax_clang.m4])

doc/Doxyfile

@@ -906,7 +906,10 @@ WARN_LOGFILE           =
 # spaces. See also FILE_PATTERNS and EXTENSION_MAPPING
 # Note: If this tag is empty the current directory is searched.
 
-INPUT                  = $(SRCDIR)/src
+INPUT                  = $(SRCDIR)/src \
+                         $(SRCDIR)/README.md \
+                         $(SRCDIR)/doc/manual.md \
+                         $(SRCDIR)/doc/development.md
 
 # This tag can be used to specify the character encoding of the source files
 # that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses
@@ -1104,7 +1107,7 @@ FILTER_SOURCE_PATTERNS =
 # (index.html). This can be useful if you have a project on for instance GitHub
 # and want to reuse the introduction page also for the doxygen output.
 
-USE_MDFILE_AS_MAINPAGE =
+USE_MDFILE_AS_MAINPAGE = $(SRCDIR)/README.md
 
 #---------------------------------------------------------------------------
 # Configuration options related to source browsing

doc/development.md

@@ -0,0 +1,25 @@
+# Modifying GenMC
+
+## Adding new label types
+
+To add a new label, follow these steps:
+
+1. Add a number and a name for the new label in Instruction.def
+2. Add a class for the new label in ExecutionGraph/EventLabel.hpp.
+   Macros are provided for dummy labels and standard subclasses
+3. Add a case for the new label in LabelVisitor.hpp
+4. Define how the label should be printed in EventLabel.cpp
+   (optionally: LabelPrinterBase too)
+5. Create a handler for the new label in GenMCDriver.{hpp,cpp}
+   (if necessary), and at DriverHandlerDispatcher
+6. In case a new LLVM-IR function leads to the creation of
+   the new label:
+   - Add a number and a name for the internal function in
+   Runtime/InternalFunction.def.
+   - Define a function that dispatches the driver at
+   Runtime/Execution.cpp
+
+*Note:* the procedure above describes the bare minimum, and works well
+for dummy labels or subclasses of existing labels. If e.g., the new
+label has attributes like location then extra changes might be
+required to ensure that iterators, etc still work.