dartagnan: Expose method and bound options as envvars

Signed-off-by: Diogo Behrens <diogo.behrens@huawei.com>

CHANGELOG.md

@@ -2,17 +2,16 @@
 
 All notable changes to this project will be documented in this file.
 
-## [2.1.0] - 2024-04-19
+## [2.1.0] - 2024-04-21
 
 ### Changed
 
-- Added installation goal to Makefile
+- Added installation goal to Makefile (`PREFIX` envvar)
 - Added tools.RegEnv which requires envvars to be registered and documented
 
 ### Added
 
-- Dockerfile with GenMC v0.10.1-a (from open-s4c/genmc)
-- Dockerfile with Dat3m v4.0.1
+- Dockerfile with clang v14, GenMC v0.10.1-a (open-s4c/genmc) and Dartagnan v4.0.1
 - vsyncer docker command
 - Several configuration options (see `vsyncer -h`)
 - `vsyncer` releases with binaries for Linux, Windows and macOS

Dockerfile

@@ -35,16 +35,18 @@ RUN apt-get update \
 
 RUN cd /tmp \
  && git clone --depth 1 --branch "v0.9" \
-     https://github.com/open-s4c/genmc.git genmc9 \
- && cd genmc9 \
+     https://github.com/open-s4c/genmc.git genmc9
+
+RUN cd /tmp/genmc9 \
  && autoreconf --install \
  && ./configure --prefix=/usr/share/genmc9 \
  && make install -j8
 
 RUN cd /tmp \
  && git clone --depth 1 --branch "v0.10.1-a" \
-     https://github.com/open-s4c/genmc.git genmc10 \
- && cd genmc10 \
+     https://github.com/open-s4c/genmc.git genmc10
+
+RUN cd /tmp/genmc10 \
  && autoreconf --install \
  && ./configure --prefix=/usr/share/genmc10 \
  && make install -j8
@@ -65,10 +67,8 @@ RUN apt-get update  \
  && rm -rf /var/lib/apt/lists/*
 
 RUN cd /tmp \
- && git clone \
-     https://github.com/hernanponcedeleon/dat3m.git \
- && cd dat3m \
- && git checkout "8d22e4283f26473ed88e226480d84acaf09fad07"
+ && git clone --depth 1 --branch "4.0.1" \
+     https://github.com/hernanponcedeleon/dat3m.git
 
 RUN cd /tmp/dat3m \
  && mvn clean install -DskipTests \

checker/checker_dartagnan.go

@@ -30,6 +30,8 @@ func init() {
 	tools.RegEnv("DARTAGNAN_SET_OPTIONS", "",
 		"Options passed to Dartagnan, replacing the default options")
 	tools.RegEnv("DARTAGNAN_CAT_PATH", "", "Path to custom .cat files")
+	tools.RegEnv("DARTAGNAN_METHOD", "eager", "Backend method (values: eager | lazy)")
+	tools.RegEnv("DARTAGNAN_BOUND", "", "Unroll bound integer (default unset)")
 }
 
 // NewDartagnan creates a new checker using Dartagnan model checker.
@@ -95,6 +97,14 @@ func (c *DartagnanChecker) run(ctx context.Context, testFn string) (string, erro
 		opts = strings.Split(env, " ")
 	}
 
+	if env := tools.GetEnv("DARTAGNAN_METHOD"); env != "" {
+		opts = append(opts, fmt.Sprintf("--method=%s", env))
+	}
+
+	if env := tools.GetEnv("DARTAGNAN_BOUND"); env != "" {
+		opts = append(opts, fmt.Sprintf("--bound=%s", env))
+	}
+
 	dartagnanHome := tools.GetEnv("DARTAGNAN_HOME")
 	args := append([]string{"-jar",
 		dartagnanHome + "/dartagnan/target/dartagnan.jar",