recursive make lifting setup

src/test/make/lift-directories.mk

@@ -0,0 +1,30 @@
+
+.EXPORT_ALL_VARIABLES:
+NAME=$(shell basename $(PWD))
+
+CC=aarch64-linux-gnu-gcc
+#CFLAGS=-fno-pic -fno-plt
+TARGET=aarch64-linux-gnu
+
+BAP=bap-aslp
+READELF=aarch64-linux-gnu-readelf
+BASIL=$(realpath ../../../../target/scala-3.3.1/wptool-boogie-assembly-0.0.1.jar)
+
+C_SOURCE=$(realpath $(wildcard *.c))
+SPEC=$(realpath $(wildcard *.spec))
+EXTRA_SPEC=$(realpath $(wildcard *.bpl))
+BASIL_FLAGS=--boogie-use-lambda-stores
+BOOGIE_FLAGS=/proverOpt:O:smt.array.extensional=false
+
+LIFT_ARTEFACTS=$(NAME).adt $(NAME).bir $(NAME).relf
+
+SUBDIRS := $(wildcard */.)
+
+TARGETS := all verify
+.PHONY : $(TARGETS) $(SUBDIRS)
+
+$(TARGETS): $(SUBDIRS)
+
+$(SUBDIRS):
+	-$(MAKE) -C $@ $(MAKECMDGOALS)
+

src/test/make/lift.mk

@@ -0,0 +1,18 @@
+
+$(NAME).bpl: $(LIFT_ARTEFACTS)
+	echo $(BASIL)
+	java -jar $(BASIL) $(BASIL_FLAGS) --adt $(NAME).adt --relf $(NAME).relf -o $(NAME).bpl --spec $(SPEC)
+
+$(LIFT_ARTEFACTS): a.out
+	$(BAP) a.out -d adt:$(NAME).adt -d bir:$(NAME).bir
+	$(READELF) -s -r -W a.out > $(NAME).relf
+
+a.out: $(C_SOURCE)
+	$(CC) $(CFLAGS) $(C_SOURCE)
+
+.PHONY=verify
+verify: $(NAME)_result.txt
+
+$(NAME)_result.txt: $(NAME).bpl $(EXTRA_SPEC)
+	boogie $(NAME).bpl $(EXTRA_SPEC) $(BOOGIE_FLAGS) | tee $(NAME)_result.txt
+