Add initial Concuerror integration

https://concuerror.com/

6 files changed, 190 insertions, 0 deletions

diff --git a/CHANGELOG.asciidoc b/CHANGELOG.asciidoc
index cdffb29..f0ff0e2 100644
--- a/CHANGELOG.asciidoc
+++ b/CHANGELOG.asciidoc
@@ -19,3 +19,7 @@
             `-lei` which is part of the Erlang/OTP Erl_Interface
             *application* but is built as a separate C library.
             The removal only applies to `-lerl_interface` itself.
+
+2020/06/18: Concuerror integration has been added. It is
+            currently minimal but usable. Experimentation
+            and feedback is welcome.
diff --git a/build.config b/build.config
index bcf2b9a..a0ab7a7 100644
--- a/build.config
+++ b/build.config
@@ -22,6 +22,7 @@ plugins/asciidoc
 plugins/bootstrap
 plugins/c_src
 plugins/ci
+plugins/concuerror
 plugins/ct
 plugins/dialyzer
 plugins/edoc
diff --git a/doc/src/guide/book.asciidoc b/doc/src/guide/book.asciidoc
index fa31fe3..7c4ee68 100644
--- a/doc/src/guide/book.asciidoc
+++ b/doc/src/guide/book.asciidoc
@@ -64,6 +64,8 @@ include::ci.asciidoc[Continuous integration]
 
 include::dialyzer.asciidoc[Dialyzer]
 
+include::concuerror.asciidoc[Concuerror]
+
 include::xref.asciidoc[Xref]
 
 [[plugins]]
diff --git a/doc/src/guide/concuerror.asciidoc b/doc/src/guide/concuerror.asciidoc
new file mode 100644
index 0000000..160af74
--- /dev/null
+++ b/doc/src/guide/concuerror.asciidoc
@@ -0,0 +1,77 @@
+[[concuerror]]
+== Concuerror
+
+https://concuerror.com/[Concuerror] is a stateless model
+checking tool for Erlang programs. It can be used to detect
+and debug concurrency errors, such as deadlocks and errors
+due to race conditions. The key property of such errors is
+that they only occur on few, specific schedulings of the
+program. Moreover, unlike tools based on randomisation,
+Concuerror can verify the absence of such errors, because
+it tests the program systematically.
+
+Erlang.mk provides a wrapper around Concuerror.
+
+=== Configuration
+
+The `CONCUERROR_TESTS` variable must be defined in order to
+use Concuerror. It lists the Concuerror test cases. There
+is currently no way to detect test cases automatically. The
+tests must be listed as `module:function` separated by
+whitespace. For example:
+
+[source,make]
+CONCUERROR_TESTS = ranch_concuerror:start_stop ranch_concuerror:info
+
+Concuerror will output some information directly on the
+screen when run, but errors will only be written to a file.
+This is because the error output can be very large. By
+default Erlang.mk instructs Concuerror to save log files
+in the 'logs/' directory (shared with Common Test). This
+can be changed by setting `CONCUERROR_LOGS_DIR`:
+
+[source,make]
+CONCUERROR_LOGS_DIR = $(CURDIR)/path/to/logs
+
+Concuerror options can be specified using the
+`CONCUERROR_OPTS` variable:
+
+[source,make]
+CONCUERROR_OPTS = -k
+
+Note that options may also be specified on a per-module
+basis using the `-concuerror_options([]).` attribute.
+
+=== Writing tests
+
+Concuerror tests are a simple 0-arity function that must
+be exported. For example:
+
+[source,erlang]
+----
+-export([info/0]).
+
+info() →
+    %% Ensure we can call ranch:info/1 after starting a listener.
+    SupPid = do_start(),
+    {ok, _} = ranch:start_listener(?FUNCTION_NAME,
+        ranch_erlang_transport, #{
+            num_acceptors ⇒ 1
+        },
+        echo_protocol, []),
+    #{} = ranch:info(?FUNCTION_NAME),
+    do_stop(SupPid).
+----
+
+Do not forget to add the function to `CONCUERROR_TESTS`
+as well.
+
+=== Usage
+
+To run Concuerror:
+
+[source,bash]
+$ make concuerror
+
+Erlang.mk will create an index of all the test logs in
+the '$(CONCUERROR_LOGS_DIR)/concuerror.html' file.
diff --git a/plugins/concuerror.mk b/plugins/concuerror.mk
new file mode 100644
index 0000000..ef63add
--- /dev/null
+++ b/plugins/concuerror.mk
@@ -0,0 +1,67 @@
+# Copyright (c) 2020, Loïc Hoguin <[email protected]>
+# This file is part of erlang.mk and subject to the terms of the ISC License.
+
+ifdef CONCUERROR_TESTS
+
+.PHONY: concuerror distclean-concuerror
+
+# Configuration
+
+CONCUERROR_LOGS_DIR ?= $(CURDIR)/logs
+CONCUERROR_OPTS ?=
+
+# Core targets.
+
+check:: concuerror
+
+ifndef KEEP_LOGS
+distclean:: distclean-concuerror
+endif
+
+# Plugin-specific targets.
+
+$(ERLANG_MK_TMP)/Concuerror/bin/concuerror: | $(ERLANG_MK_TMP)
+	$(verbose) git clone https://github.com/parapluu/Concuerror $(ERLANG_MK_TMP)/Concuerror
+	$(verbose) make -C $(ERLANG_MK_TMP)/Concuerror
+
+$(CONCUERROR_LOGS_DIR):
+	$(verbose) mkdir -p $(CONCUERROR_LOGS_DIR)
+
+define concuerror_html_report
+<!DOCTYPE html>
+<html lang="en">
+<head>
+<meta charset="utf-8">
+<title>Concuerror HTML report</title>
+</head>
+<body>
+<h1>Concuerror HTML report</h1>
+<p>Generated on $(concuerror_date)</p>
+<ul>
+$(foreach t,$(concuerror_targets),<li><a href="$(t).txt">$(t)</a></li>)
+</ul>
+</body>
+</html>
+endef
+
+concuerror: $(addprefix concuerror-,$(subst :,-,$(CONCUERROR_TESTS)))
+	$(eval concuerror_date := $(shell date))
+	$(eval concuerror_targets := $^)
+	$(verbose) $(call core_render,concuerror_html_report,$(CONCUERROR_LOGS_DIR)/concuerror.html)
+
+define concuerror_target
+.PHONY: concuerror-$1-$2
+
+concuerror-$1-$2: test-build | $(ERLANG_MK_TMP)/Concuerror/bin/concuerror $(CONCUERROR_LOGS_DIR)
+	$(ERLANG_MK_TMP)/Concuerror/bin/concuerror \
+		--pa $(CURDIR)/ebin --pa $(TEST_DIR) \
+		-o $(CONCUERROR_LOGS_DIR)/concuerror-$1-$2.txt \
+		$$(CONCUERROR_OPTS) -m $1 -t $2
+endef
+
+$(foreach test,$(CONCUERROR_TESTS),$(eval $(call concuerror_target,$(firstword $(subst :, ,$(test))),$(lastword $(subst :, ,$(test))))))
+
+distclean-concuerror:
+	$(gen_verbose) rm -rf $(CONCUERROR_LOGS_DIR)
+
+endif
diff --git a/test/plugin_concuerror.mk b/test/plugin_concuerror.mk
new file mode 100644
index 0000000..f1b9288
--- /dev/null
+++ b/test/plugin_concuerror.mk
@@ -0,0 +1,39 @@
+# Concuerror plugin.
+
+CONCUERROR_TARGETS = $(call list_targets,concuerror)
+
+.PHONY: concuerror $(CONCUERROR_TARGETS)
+
+concuerror: $(CONCUERROR_TARGETS)
+
+concuerror-app: init
+
+	$i "Bootstrap a new OTP application named $(APP)"
+	$t mkdir $(APP)/
+	$t cp ../erlang.mk $(APP)/
+	$t $(MAKE) -C $(APP) -f erlang.mk bootstrap $v
+
+	$i "Create a test module with a function that returns immediately"
+	$t mkdir $(APP)/test
+	$t printf "%s\n" \
+		"-module(concuerror_success)." \
+		"-export([test/0])." \
+		"test() -> ok." > $(APP)/test/concuerror_success.erl
+
+	$i "Add the test case to CONCUERROR_TESTS"
+	$t perl -ni.bak -e 'print;if ($$.==1) {print "CONCUERROR_TESTS += concuerror_success:test\n"}' $(APP)/Makefile
+
+	$i "Confirm that Concuerror completes successfully"
+	$t $(MAKE) -C $(APP) concuerror $v
+
+	$i "Create a test module with a function that has no local return"
+	$t printf "%s\n" \
+		"-module(concuerror_error)." \
+		"-export([test/0])." \
+		"test() -> 1 = 2, ok." > $(APP)/test/concuerror_error.erl
+
+	$i "Add the test case to CONCUERROR_TESTS"
+	$t perl -ni.bak -e 'print;if ($$.==1) {print "CONCUERROR_TESTS += concuerror_error:test\n"}' $(APP)/Makefile
+
+	$i "Confirm that Concuerror errors out"
+	$t ! $(MAKE) -C $(APP) concuerror $v