Refactoring Makefiles (#208)

Clean and restructure build files, particularly for C backend. Incorporate build shell scripts in makefiles.

Makefile

@@ -15,27 +15,19 @@ else
     TEST_FILTER_FLAG=
 endif
 
-MLANG_BIN=dune exec --no-print-director src/main.exe --
-
-MPP_FUNCTION?=compute_double_liquidation_pvro
-
-PRECISION?=double
-
 TEST_ERROR_MARGIN?=0.
 
-MLANG_DEFAULT_OPTS=\
-	--display_time --debug \
-	--precision $(PRECISION) \
-	--mpp_file=$(MPP_FILE) \
+MLANG_INTERPRETER_OPTS=\
 	--test_error_margin=$(TEST_ERROR_MARGIN) \
+	--mpp_file=$(MPP_FILE) \
 	--mpp_function=$(MPP_FUNCTION)
 
-MLANG=$(MLANG_BIN) $(MLANG_DEFAULT_OPTS) $(OPTIMIZE_FLAG) $(CODE_COVERAGE_FLAG)
+MLANG=$(MLANG_BIN) $(MLANG_DEFAULT_OPTS) $(MLANG_INTERPRETER_OPTS) $(CODE_COVERAGE_FLAG)
 
 default: build
 
 ##################################################
-# Building the compiler
+# Initializing the project
 ##################################################
 
 # Workaround for Opam 2.0 bug. Empty switch creation then installation could be a one line
@@ -53,6 +45,10 @@ deps:
 	opam switch reinstall --deps-only
 	git submodule update
 
+##################################################
+# Building the compiler
+##################################################
+
 format:
 	dune build @fmt --auto-promote | true
 
@@ -77,17 +73,17 @@ test: build
 tests: build
 	$(MLANG) $(MLANGOPTS) --run_all_tests=$(TESTS_DIR) $(TEST_FILTER_FLAG) $(SOURCE_FILES)
 
-test_java_backend:
+test_java_backend: build
 ifeq ($(OPTIMIZE), 0)
 	@echo "\033[0;31mWarning, non-optimized Java files cannot be executed for now (too many constants for the JVM)\033[0m"
 else
 endif
 	$(MAKE) -C examples/java/ run_tests
 
-test_dgfip_c_backend:
-	$(MAKE) -C examples/dgfip_c/ backend_tests
+test_dgfip_c_backend: build
+	$(MAKE) -C examples/dgfip_c/ml_primitif backend_tests
 
-quick_test:
+quick_test: build
 	$(MLANG) --backend interpreter --function_spec $(M_SPEC_FILE) $(SOURCE_FILES)
 
 all: tests test_java_backend test_dgfip_c_backend quick_test
@@ -96,12 +92,12 @@ all: tests test_java_backend test_dgfip_c_backend quick_test
 # Doc
 ##################################################
 
-doc: FORCE
+doc: FORCE build
 	dune build @doc
 	ln -fs $(shell pwd)/_build/default/_doc/_html/index.html doc/doc.html
 
 clean:
-	$(MAKE) -C examples/dgfip_c clean
+	$(MAKE) -C examples/dgfip_c/ml_primitif cleanall
 	$(MAKE) -C examples/java clean
 	rm -f doc/doc.html
 	dune clean

Makefile.config.template

@@ -1,4 +1,9 @@
-# Copy this file as Makefile.config and change some of these variables
+# Copy this file as Makefile.config
+# and change some of these variables to overwrite the default values.
+
+##################################################
+# Tax computation configuration
+##################################################
 
 # YEAR=2018
 
@@ -8,17 +13,43 @@
 
 # TESTS_DIR=$(SELF_DIR)/tests/2018/fuzzing/
 
-# Enable filter on tests filename (Keep only if name begins by an uppercase ASCII character)
+# Enable filter on tests filename (Keep only if name begins by an uppercase ASCII character)
 # TEST_FILTER=1
 
 # M_SPEC_FILE=$(SELF_DIR)/m_specs/complex_case_with_ins_outs_2018.m_spec
 
-# CC:=gcc
+# MPP_FUNCTION=compute_double_liquidation_pvro
 
-# TEST_ERROR_MARGIN=0.
+##################################################
+# Mlang configuration
+##################################################
+
+# General parameters
+# ---------------------------
 
 # PRECISION=double
 
+# OPTIMIZE=0
+
+# Interpreter instrumentation
+# ---------------------------
+
+# TEST_ERROR_MARGIN=0.
+
+# CODE_COVERAGE=1
+
+##################################################
+# Build configuration
+##################################################
+
 # DUNE_OPTIONS=
 
-# C_COMPILER=clang
+##################################################
+# C backend configuration
+##################################################
+# CC=gcc
+
+##################################################
+# Exports 
+##################################################
+# Export here variables you need in recursive make calls

Makefile.include

@@ -1,13 +1,15 @@
-# Create this file to overwrite typical variables (see Makefile.config.template)
-
 ##################################################
-# Variables
+# Local customization
 ##################################################
 
 SELF_DIR=$(realpath $(dir $(realpath $(lastword $(MAKEFILE_LIST)))))
 
 -include $(SELF_DIR)/Makefile.config
 
+##################################################
+# Tax computation configuration
+##################################################
+
 define source_dir
 	$(shell find $(1) -name \*.m ! -name err\*.m ! -name tgv\*.m | sort) $(1)errI.m $(1)tgvI.m
 endef
@@ -26,24 +28,60 @@ ifeq ($(YEAR), 2018)
 	MPP_FILE?=$(SELF_DIR)/mpp_specs/2018_6_7.mpp
 	TESTS_DIR?=$(SELF_DIR)/tests/2018/fuzzing/
 	M_SPEC_FILE?=$(SELF_DIR)/m_specs/complex_case_with_ins_outs_2018.m_spec
+	MPP_FUNCTION?=compute_double_liquidation_pvro
 else ifeq ($(YEAR), 2019)
 	SOURCE_FILES?=$(SOURCE_DIR_2019)
 	MPP_FILE?=$(SELF_DIR)/mpp_specs/2019_8_0.mpp
 	TESTS_DIR?=$(SELF_DIR)/tests/2019/fuzzing/
 	M_SPEC_FILE?=m_specs/complex_case_with_ins_outs_2019.m_spec
+	MPP_FUNCTION?=compute_double_liquidation_pvro
 else ifeq ($(YEAR), 2020)
 	SOURCE_FILES?=$(SOURCE_DIR_2020)
 	MPP_FILE?=$(SELF_DIR)/mpp_specs/2020_6_5.mpp
 	TESTS_DIR?=$(SELF_DIR)/tests/2020/fuzzing/
 	M_SPEC_FILE?=$(SELF_DIR)/m_specs/complex_case_with_ins_outs_2020.m_spec
+	MPP_FUNCTION?=compute_double_liquidation_pvro
 else
-    $(error Unsupported year: $(YEAR))
+ 	$(warning WARNING: there is no default configuration for year: $(YEAR))
+    $(warning WARNING: example specification files and fuzzer tests are not included for year: $(YEAR))
 endif
 
-C_COMPILER?=clang
+##################################################
+# Mlang configuration
+##################################################
 
 ifeq ($(OPTIMIZE), 0)
     OPTIMIZE_FLAG=
 else
     OPTIMIZE_FLAG=-O
 endif
+
+MLANG_BIN=dune exec $(SELF_DIR)/_build/default/src/main.exe --
+
+PRECISION?=double
+MLANG_DEFAULT_OPTS=\
+	--display_time --debug \
+	--precision $(PRECISION) \
+	$(OPTIMIZE_FLAG)
+
+##################################################
+# C backend configuration
+##################################################
+
+# CC is a GNU make default variable defined to CC
+# It so can't be overriden by conditional operator ?=
+# We check the origin of CC value to not override CL argument or explicit environment.
+ifeq ($(origin CC),default)
+    CC=clang
+endif
+
+##################################################
+# Exports to call backends from main Makefile
+##################################################
+
+# common
+export SOURCE_FILES TESTS_DIR MLANG_BIN MLANG_DEFAULT_OPTS
+# for C backend (Java compilation is year-independent)
+export YEAR CC
+# for Java backend (C overload these now)
+export MPP_FUNCTION MPP_FILE

examples/dgfip_c/.gitignore

@@ -4,4 +4,13 @@ ir_*.h
 *.o
 *.tmp
 *.bc
-ml_primitif/build.conf
+
+ml_primitif/calc/*
+ml_primitif/*.cm*
+ml_primitif/cal
+ml_primitif/vars.txt
+ml_primitif/*.output
+
+fuzz_findings/*
+fuzz_tests/*
+klee-*