FEC: add verif Makefile targets
@@ -9,6 +9,25 @@ $(OBJ): %.o
%.o: %.c
clang-6.0 $(CFLAGS) -O2 -fno-gnu-inline-asm -emit-llvm -c $< -o - | llc-6.0 -march=bpf -filetype=obj -o $@
+
+%_full.c: %.c
+ mkdir -p verif/"$$(dirname $@_tmp)"
+ gcc $(CFLAGS) -E $< > verif/$@_tmp
+ python3 ../../benchmarks/add_main_to_plugin.py verif/$@_tmp > verif/$@
+ find . -name "*_tmp" | xargs rm
+ docker run -ti -v $(CURDIR)/verif:/mount llvm2kittel $(basename $@)
+ sed -E -i 's/\|\|\s+\(nondet\(\)/\|\| \(nondet\(\) != 0/g' verif/$(basename $@).t2
+ sed -E -i 's/\&\&\s+\(nondet\(\)/\&\& \(nondet\(\) != 0/g' verif/$(basename $@).t2
+ sed -E -i 's/nondet\(\)\)\s+\|\|/nondet\(\) != 0\) \|\|/g' verif/$(basename $@).t2
+ sed -E -i 's/nondet\(\)\)\s+\&\&/nondet\(\) != 0\) \&\&/g' verif/$(basename $@).t2
+
+%_full.c.verif: %_full.c
+ docker run -v $(CURDIR)/verif:/mount t2_prod --input_t2=/mount/$(basename $<).t2 --timeout=300 --termination || true #--print_proof --log
+
+generate_verif: $(SRC:.c=_full.c)
+
+verif: generate_verif $(SRC:.c=_full.c.verif)
+
clean:
rm -rf $(OBJ)
