Merge pull request #3 from rems-project/prepare-litmus-toml-translator

Add litmus toml translator

.github/workflows/ci.yml

@@ -4,6 +4,7 @@ on:
   push:
     branches:
       - master
+      - prepare-litmus-toml-translator
   # pull_request: {}
 
 # cancel in-progress job when a new push is performed
@@ -23,22 +24,64 @@ jobs:
 
     timeout-minutes: 5
     steps:
+    - run: mkdir -p rems-project litmus-tests
+
     - uses: actions/checkout@v3
+      with:
+        path: rems-project/system-litmus-harness
 
     - name: System dependencies (ubuntu)
       run: |
         sudo apt update
         sudo apt install build-essential gcc-aarch64-linux-gnu qemu-system-aarch64
 
+    - name: Get rust toolchain
+      uses: actions-rs/toolchain@v1
+      with:
+        profile: minimal
+        toolchain: stable
+
+    - name: Setup rems-project dependencies
+      working-directory: rems-project
+      run: |
+        git clone https://github.com/rems-project/isla
+        git clone https://github.com/rems-project/isla-snapshots
+
+    - name: Setup litmus-tests org dependencies
+      working-directory: litmus-tests
+      run: |
+        git clone https://github.com/litmus-tests/litmus-tests-armv8a-system-vmsa/
+
     - name: Build harness
+      working-directory: rems-project/system-litmus-harness
       run: |
         make build
 
     - name: Check for compiler warnings
+      working-directory: rems-project/system-litmus-harness
       run: |
         make -B -s check
 
     - name: Run unittests
+      working-directory: rems-project/system-litmus-harness
       run: |
         ./qemu_unittests --no-test-linear-concretization | tee log
         [ $(tail -c -2 log) -eq 0 ]
+
+    - name: Build tools
+      working-directory: rems-project/system-litmus-harness
+      run: |
+        make tools
+
+    - name: Run TOML translator
+      working-directory: rems-project/system-litmus-harness
+      run: |
+        make translate-toml-tests
+
+    - name: Compile translated tests
+      working-directory: rems-project/system-litmus-harness
+      run: |
+        # should automatically discover and build new tests
+        make build
+        # validate by checking an arbitrarily-picked test was actually compiled
+        [ -f ./bin/litmus/litmus_tests/generated/pgtable/CoWinvT+po.litmus.toml.o ]

Makefile

@@ -1,14 +1,15 @@
 define USAGE
 Simple Usage:
-   make	build		builds qemu and kvm targets
-   make	check		runs the compiler warning checks but doesn't compile
-   make docker		builds docker container and runs the unittests
-   make clean		remove built files in bin/
-   make deepclean	clean everything. No really.
-   make publish		publish doc/ folder to gh-pages
+   make	build     	builds qemu and kvm targets
+   make	check    	runs the compiler warning checks but doesn't compile
+   make docker   	builds docker container and runs the unittests
+   make clean    	remove built files in bin/
+   make deepclean 	clean everything. No really.
+   make publish   	publish doc/ folder to gh-pages
    make hw-results	collect hardware results from known sources
-   make test		run the unittests in QEMU
-   make run			run the litmus tests in QEMU
+   make test      	run the unittests in QEMU
+   make run       	run the litmus tests in QEMU
+   make tools      	build supporting tooling
 endef
 
 define ADV_USAGE
@@ -19,6 +20,10 @@ Advanced Usage:
    	Runs qemu_unittests.exe in the background and attaches gdb
    make build-unittests
    	Builds the unittests and generates qemu_unittests.exe
+   make tools
+   	Builds associated tooling
+   make translate-toml-tests
+   	Runs the automated TOML test translator
    make lint
    	Runs automated linter against all litmus test C files and quits
    	See LINTER option below
@@ -27,6 +32,8 @@ Advanced Usage:
    	See LITMUS_TESTS and MAKE_TEST_LIST_CMD options below
    make cleanlibs
    	remove built harness objects but leave compiled tests alone
+   make cleantools
+   	remove built tool files
    make cleantests
    	remove auto-generated test files in litmus/
    make docker-interact
@@ -112,6 +119,12 @@ OBJDUMP = $(PREFIX)objdump
 QEMU = qemu-system-aarch64
 GDB = $(PREFIX)gdb
 
+# dependency roots
+# by default we assume rems-project/ repos are siblings to this one
+# and litmus-tests/ org repos are a sibling to rems-project
+REMSORGDIR = ../
+LITMUSORGDIR = ../../litmus-tests/
+
 # use `taskset` to force QEMU to exist only on some cores
 # e.g. for big.LITTLE implementations
 #
@@ -189,7 +202,7 @@ CFLAGS = -O0 -nostdlib \
 		$(CFLAGS_DEPS) \
 		-ffreestanding -fno-omit-frame-pointer -fno-pie -fno-pic \
 		-mstrict-align \
-		-march=armv8-a+nofp \
+		-march=armv8.5-a+nofp \
 		-Wall $(addprefix -Wno-,$(CCNOWARN)) $(addprefix -Werror=,$(CCERRORS)) \
 		-Wextra -Wno-unused-parameter -Wno-sign-compare \
 		-Wshadow \
@@ -215,6 +228,16 @@ LINTER_ARGS = $(foreach e,$(LINTER_EXCLUDES),-e $(e))
 
 NO_LINT = 0
 
+# toml-translator arguments:
+# TOML_TESTS: list of tests or @all file to translate.
+# TOML_TRANSLATOR_ISLA_CONFIG: isla architecture config toml file.
+# TOML_TRANSLATOR_ISLA_ARCH: isla architecture ir (or irx) file.
+# TOML_TRANSLATOR_IGNORE_LIST: txt file with list of toml tests to ignore.
+TOML_TESTS = $(LITMUSORGDIR)/litmus-tests-armv8a-system-vmsa/tests/@all
+TOML_TRANSLATOR_ISLA_CONFIG = $(REMSORGDIR)/isla/configs/armv8p5.toml
+TOML_TRANSLATOR_ISLA_ARCH = $(REMSORGDIR)/isla-snapshots/armv8p5.ir
+TOML_TRANSLATOR_IGNORE_LIST = ./tools/litmus-toml-translator/toml-tests-ignore.txt
+
 ifneq ($(findstring help,$(filter-out --%,$(MAKECMDGOALS))),)
    TARGET_HELP = 1
 endif
@@ -231,6 +254,7 @@ include mk/docs.mk
 include mk/qemu.mk
 include mk/build.mk
 include mk/docker.mk
+include mk/tools.mk
 
 define INSTALL
 $(call run_cmd,INSTALL,./$(2),\
@@ -267,6 +291,7 @@ cleantests:
 	$(call CLEAN,-f,litmus/test_list.txt)
 	$(call CLEAN,-f,litmus/group_list.txt)
 	$(call CLEAN,-f,litmus/linter.log)
+	$(call CLEAN,-rf,litmus/litmus_tests/generated)
 
 # list of PHONY targets that will need
 # files in the litmus/litmus_tests/ dir
@@ -434,6 +459,10 @@ LITMUS_TARGETS += run
 include mk/litmus.mk
 include mk/unittests.mk
 
+# target populated by mk/tools.mk
+.PHONY: tools
+tools:
+
 # provide a list of all the potential build- targets
 .PHONY: list
 list:

inc/litmus/litmus_asm_in_macros.h

@@ -45,8 +45,14 @@
 #define STRINGIFY_4(a, ...) STRINGIFY_1(a), STRINGIFY_3(__VA_ARGS__)
 #define STRINGIFY_5(a, ...) STRINGIFY_1(a), STRINGIFY_4(__VA_ARGS__)
 #define STRINGIFY_6(a, ...) STRINGIFY_1(a), STRINGIFY_5(__VA_ARGS__)
-#define STRINGIFY_N(a, b, c, d, e, f, n, ...) STRINGIFY_##n(a, b, c, d, e, f)
-#define STRINGIFY(...) STRINGIFY_N(__VA_ARGS__, 6, 5, 4, 3, 2, 1)
+#define STRINGIFY_7(a, ...) STRINGIFY_1(a), STRINGIFY_6(__VA_ARGS__)
+#define STRINGIFY_8(a, ...) STRINGIFY_1(a), STRINGIFY_7(__VA_ARGS__)
+#define STRINGIFY_9(a, ...) STRINGIFY_1(a), STRINGIFY_8(__VA_ARGS__)
+#define STRINGIFY_10(a, ...) STRINGIFY_1(a), STRINGIFY_9(__VA_ARGS__)
+#define STRINGIFY_11(a, ...) STRINGIFY_1(a), STRINGIFY_10(__VA_ARGS__)
+#define STRINGIFY_12(a, ...) STRINGIFY_1(a), STRINGIFY_11(__VA_ARGS__)
+#define STRINGIFY_N(a, b, c, d, e, f, g, h, i, j, k, l, n, ...) STRINGIFY_##n(a, b, c, d, e, f, g, h, i, j, k, l)
+#define STRINGIFY(...) STRINGIFY_N(__VA_ARGS__, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1)
 
 #define HUMANIZE_1(a, ...) HUMAN(a)
 #define HUMANIZE_2(a, ...) HUMANIZE_1(a), HUMANIZE_1(__VA_ARGS__)

litmus/linter.py

@@ -28,7 +28,7 @@
     r"litmus_test_t\s+(?P<cname>.+?)\s*=\s*\{"
     r"\s*\"(?P<human_name>.+?)\"\s*,"
     r'\s*MAKE_THREADS\((?P<no_threads>\d+)\)\s*?,'
-    r'\s*MAKE_VARS\(VARS\)\s*?,'
+    r'\s*MAKE_VARS\(VARS(\s*,\s*pa\d+)*\)\s*?,'
     r'\s*MAKE_REGS\(REGS\)\s*?,'
     r'(?P<fields>[\s\S]*?)'
     r'\s*\}\s*;'
@@ -58,7 +58,7 @@
 C_FUN_PAT = (
     r"void (?P<fname>.+)\(.+\)\s*\{"
     r"(?P<body>[\s\S]*?)"
-    r"\s*\}"
+    r"^}"
 )
 
 C_INIT_ST = (
@@ -73,7 +73,7 @@
 def get_reg_names(asm):
     if not asm:
         return []
-    return ['x{}'.format(i) for i in re.findall(r'(?<=(?<!\%\[)[xw])\d+', asm['code'])]
+    return ['x{}'.format(i) for i in re.findall(r'(?<=(?<!.0|\%\[)[xwXW])\d+', asm['code'])]
 
 def parse_litmus_code(path, c_code):
     match = re.search(LITMUS_TEST_T_PAT_NEW, c_code, re.MULTILINE)
@@ -155,7 +155,13 @@ def check_uniq_names(litmuses):
 
 def check_human_match_path(l):
     p = pathlib.Path(l['path']).stem
-    if l['human_name'] != str(p):
+
+    # for toml-translator generated names, strip the .toml.c
+    if p.endswith(".litmus.toml"):
+        p = p[:-len(".litmus.toml")]
+        pass
+
+    if l['human_name'] != p:
         warn(l, "File name and Litmus name mismatch.")
 
 

litmus/main_match_and_run.c

@@ -73,10 +73,10 @@ static u8 __match_and_run_test(const litmus_test_group* grp, re_t* arg) {
 void match_and_run(const litmus_test_group* grp, re_t* arg) {
   u8 found = 0;
 
-  if (*arg->original_expr == '@') {
+  found = __match_and_run_test(grp, arg);
+
+  if (!found) {
     found = __match_and_run_group(grp, arg);
-  } else {
-    found = __match_and_run_test(grp, arg);
   }
 
   if (!found) {

litmus/makegroups.py

@@ -83,10 +83,10 @@ def __init__(self, root, force, includes):
         self.force = force
         self.includes = includes
 
-        self.all_tests = GroupMap("all")
-        self.already_seen = GroupMap("all")
-        self.matching_tests = GroupMap("all")
-        self.updated_tests = GroupMap("all")
+        self.all_tests = GroupMap()
+        self.already_seen = GroupMap()
+        self.matching_tests = GroupMap()
+        self.updated_tests = GroupMap()
 
     def updated_groups(self):
         return not self.updated_tests.is_empty() or self.force or not (root / 'groups.c').exists()
@@ -181,7 +181,7 @@ def get_tests(self, d, extra_includes=[], groups=[]):
 
 group_template = """
 const litmus_test_group grp_%s = {
-  .name="@%s",
+  .name="%s",
   .tests = (const litmus_test_t*[]){
     %s
   },
@@ -191,17 +191,37 @@ def get_tests(self, d, extra_includes=[], groups=[]):
 };\
 """
 
+def build_at_name(g, prefix):
+    # special case: top-level is called just @all
+    if g.name == "":
+        assert not prefix
+        return "@all"
+
+    return "/".join(prefix + (g.name,)) + "/@all"
+
+def build_c_name(g, prefix):
+    # special case: top-level is called just all
+    if g.name == "":
+        assert not prefix
+        return "all"
+
+    return build_at_name(g, prefix).replace("/", "_").replace("_@all", "")
+
+def build_group_defs(matching, prefix=()):
+    if matching.name:
+        next_prefix = prefix + (matching.name,)
+    else:
+        # Ugh! top-level group is "" so the prefix actually starts here.
+        next_prefix = prefix
 
-def build_group_defs(matching):
     for g in matching.groups.values():
-        yield from build_group_defs(g)
+        yield from build_group_defs(g, next_prefix)
 
-    name = matching.name
     test_refs = ['&{}'.format(t.test.ident) for t in sorted(matching.tests, key=lambda t: t.test.name)]
-    grp_refs = sorted('&grp_{}'.format(grp_name) for grp_name in matching.groups)
+    grp_refs = sorted('&grp_{}'.format(build_c_name(g, next_prefix)) for g in matching.groups.values())
     test_refs.append('NULL')
     grp_refs.append('NULL')
-    yield group_template % (name, name, ',\n    '.join(test_refs), ',\n    '.join(grp_refs))
+    yield group_template % (build_c_name(matching, prefix), build_at_name(matching, prefix), ',\n    '.join(test_refs), ',\n    '.join(grp_refs))
 
 
 def build_externs(matching):

mk/deepclean.mk

@@ -1,2 +1,2 @@
 .PHONY: deepclean
-deepclean: clean cleanlibs cleantests
+deepclean: clean cleanlibs cleantests cleantools

mk/litmus.mk

@@ -3,6 +3,7 @@
 .PHONY: debug-litmus
 .PHONY: collect-litmus
 .PHONY: count-litmus-tests
+.PHONY: translate-toml-tests
 
 LITMUS_TARGETS += lint collect-litmus debug-litmus count-litmus-tests check
 
@@ -141,4 +142,19 @@ debug-litmus: qemu_litmus
 
 count-litmus-tests:
 	@echo Found `cat litmus/test_list.txt | wc -l` tests
-	@echo With `cat litmus/test_list.txt | awk '{print gensub(/^(.+\/)+(.+)\+(.+)$$/,"\\\\2","g",$$2)}' | sort | uniq | wc -l` unique shapes
+	@echo With `cat litmus/test_list.txt | awk '{print gensub(/^(.+\/)+(.+)\+(.+)$$/,"\\\\2","g",$$2)}' | sort | uniq | wc -l` unique shapes
+
+TOML_TRANSLATOR_ARGS = \
+	-A $(TOML_TRANSLATOR_ISLA_ARCH) \
+	-C $(TOML_TRANSLATOR_ISLA_CONFIG) \
+	-o litmus/litmus_tests/generated
+
+ifneq ($(TOML_TRANSLATOR_IGNORE_LIST),)
+  TOML_TRANSLATOR_ARGS += -x $(TOML_TRANSLATOR_IGNORE_LIST)
+endif
+
+translate-toml-tests: $(TOML_TRANSLATOR)
+	@mkdir -p litmus/litmus_tests/generated
+	$(call run_cmd,TOML_TRANSLATE,$(TOML_TESTS),\
+		$(TOML_TRANSLATOR) $(TOML_TRANSLATOR_ARGS) $(TOML_TESTS) \
+	)

mk/tools.mk

@@ -0,0 +1,16 @@
+.PHONY: cleantools
+
+TOOLS_DIR = tools/
+
+TOML_TRANSLATOR_ROOT = ./tools/litmus-toml-translator
+TOML_TRANSLATOR = $(TOML_TRANSLATOR_ROOT)/target/release/litmus-toml-translator
+
+$(TOML_TRANSLATOR):
+	$(call run_cmd,CARGO,tools/litmus-toml-translator,cd tools/litmus-toml-translator && cargo build --profile=release)
+TOOLS += $(TOML_TRANSLATOR)
+.PHONY: $(TOML_TRANSLATOR)
+
+cleantools:
+	$(call run_cmd,CLEAN,tools/litmus-toml-translator,cd tools/litmus-toml-translator && cargo clean)
+
+tools: $(TOOLS)

tools/litmus-toml-translator/.gitignore

@@ -0,0 +1,2 @@
+/target
+*.irx