Makefile

PROJECT_NAME=klee
TARGET=$(PROJECT_NAME).hex
EXECUTABLE=$(PROJECT_NAME).elf
EXECOBJ=$(PROJECT_NAME).o
IROUT=$(PROJECT_NAME).bc

ifeq "$(MAKECMDGOALS)" "gcc"
# GCC
CC=arm-none-eabi-gcc
LD=arm-none-eabi-ld
AR=arm-none-eabi-ar
AS=arm-none-eabi-as
CP=arm-none-eabi-objcopy
OD=arm-none-eabi-objdump

else
# CLANG
CC=clang
LD=llvm-link
CC-native=arm-none-eabi-gcc
#LD-native=arm-none-eabi-ld
AR=llvm-ar
AS=arm-none-eabi-as
CP=arm-none-eabi-objcopy
OD=arm-none-eabi-objdump

endif

BIN=$(CP) -O ihex

# Debugging with OpenOCD
GDB = arm-none-eabi-gdb
OOCD = openocd
# General case, but now we need specifics
#OOCDFLAsyscalls = -f interface/stlink-v2-1.cfg -f board/stm32f7discovery.cfg
#OOCDFLAGS = -f interface/stlink-v2-1.cfg -f ocd_stm32f4.cfg

OOCDFLAGS = -f interface/stlink-v2-1.cfg -f stm32f4x.cfg

#DEFS = -DUSE_STDPERIPH_DRIVER -DSTM32F4XX -DMANGUSTA_DISCOVERY -DUSE_USB_OTG_FS -DHSE_VALUE=8000000
#DEFS = -DUSE_STDPERIPH_DRIVER -DSTM32F4XX -DSTM32F40XX -DHSE_VALUE=8000000

# STM32F4x7 custom
#DEFS = -DUSE_STDPERIPH_DRIVER -DSTM32F40XX -DSTM32F4XX -DHSE_VALUE=16000000

# STM32F401
ifeq "$(MAKECMDGOALS)" "rel"
DEFS = -DSTM32F40XX -DSTM32F401xE -DHSE_VALUE=8000000 -DTRACE -DOS_USE_TRACE_ITM 
else ifeq "$(MAKECMDGOALS)" "wcet"
DEFS = -DSTM32F40XX -DSTM32F401xE -DHSE_VALUE=8000000 -DTRACE -DOS_USE_TRACE_ITM -DKLEE_WCET
else
DEFS = -DSTM32F40XX -DSTM32F401xE -DHSE_VALUE=8000000 -DKLEE
endif

# Definitions
#ifeq "$(MAKECMDGOALS)" "debug"
#else
#DEFS = -DnoUSE_STDPERIPH_DRIVER -DHSE_VALUE=8000000 -DOS_USE_TRACE_ITM -DDEBUG -DxOS_USE_SEMIHOSTING -DTRACE -DxOS_USE_TRACE_SEMIHOSTING_DEBUG -DSTM32F746xx
#DEFS = -DnoUSE_STDPERIPH_DRIVER -DHSE_VALUE=8000000 -DxOS_USE_SEMIHOSTING -DxOS_USE_TRACE_SEMIHOSTING_DEBUG -DSTM32F746xx
#endif

# Optimize for size
#OPTIMIZE       = -Os
# No optimization at all
ifeq "$(MAKECMDGOALS)" "rel"
# GCC
OPTIMIZE = -O0
else ifeq "$(MAKECMDGOALS)" "wcet"
OPTIMIZE = -O0
else
# CLANG
OPTIMIZE = -O0 -Xclang -disable-O0-optnone
endif

#INCSEARCH = include
#SRCIGNORE =! -iname 'tiny_printf.c'
#INCLUDES := $(shell find $(INCSEARCH) -name '*.h' -exec dirname {} \; | uniq)
INCLUDES = -I"include" \
		   -I"/usr/arm-none-eabi/include" \
		   -I"system" \
		   -I"system/include/cmsis" \
		   -I"system/include/cmsis/stm32f4-hal"
		   #-I"Libraries/stm32f4-hal" \
		   #-I"Libraries/STM32F4xx_StdPeriph_Driver/inc"\
		   #-I"Libraries/CMSIS/Include"\
		   #-I"Libraries/Device/STM32F4xx/Include"

MCU = cortex-m4
TARGETTRIPLE = armv7m-none-eabi

ifeq "$(MAKECMDGOALS)" "gcc"
# GCC

include Makefile_gcc

# End of the GCC block
else
# Start of the CLANG block

# CLANG
CLANGMCFLAGS = #-target $(TARGETTRIPLE) # -fno-integrated-as
# MCU Specific flags
#MCFLAGS = -mcpu=$(MCU) -mlittle-endian -mthumb -ffreestanding \
	#-fmessage-length=0 -fsigned-char -ffunction-sections -fdata-sections -mfpu=fpv4-sp-d16 -mfloat-abi=hard -fshort-enums \
	#-g3 -std=gnu11 -Wall -Wextra

ifeq "$(MAKECMDGOALS)" "rel"
TARGETHWFLAGS = -target $(TARGETTRIPLE) -mcpu=$(MCU) -mlittle-endian -mthumb -mfpu=fpv4-sp-d16 -mfloat-abi=hard
TARGETHWLDFLAGS =

else ifeq "$(MAKECMDGOALS)" "wcet"
TARGETHWFLAGS = -target $(TARGETTRIPLE) -mcpu=$(MCU) -mlittle-endian -mthumb -mfpu=fpv4-sp-d16 -mfloat-abi=hard
TARGETHWLDFLAGS =

else
TARGETHWFLAGS =
# Link for some triple, not really used, but needed for linking with interrupt vectors
TARGETHWLDFLAGS = -mtriple=$(TARGETTRIPLE) -march=thumb -mcpu=$(MCU) -float-abi=hard 
endif

MCFLAGS = -ffreestanding \
	-fmessage-length=0 -fsigned-char -ffunction-sections -fdata-sections \
	-fshort-enums -g3 -std=gnu11 -Wall -Wextra

# For creating object file from LLVM IR
LLCFLAGS = $(TARGETHWLDFLAGS) -filetype=obj

# Assembler flags (unnused)
ASFLAGS = -mcpu=$(MCU) -mlittle-endian -mthumb -mfpu=fpv4-sp-d16 -mfloat-abi=hard


# Linking options with -nostartfiles
#LDFLAGS = -T ldscripts/stm32f4_flash.ld  -nostdlib -nostartfiles -nostartupfiles  -gc-sections -print-gc-sections  -Map objects/$(EXECUTABLE).map
LDFLAGS = --specs=nosys.specs  -Wl,-T "ldscripts/flash.ld" -nostartfiles -Wl,-nostdlib,-print-gc-sections -Wl,-Map,objects/$(EXECUTABLE).map
# Not used:
#--specs=nano.specs --specs=nosys.specs  -lc -lnosys 

CLANGLDFLAGS = -flto
#or if you want .bc for each object: -save-temps=obj

# Build the compile command
CFLAGS	= $(CLANGMCFLAGS) $(TARGETHWFLAGS) $(MCFLAGS) $(OPTIMIZE) $(DEFS)


# Recursively add all .c files
#SRC := $(shell find $(SOURCEDIR) -name '*.c')

SRCSEARCH = src
SRCIGNORE =! -iname 'tiny_printf.c' ! -iname 'fsdata.c' ! -iname 'stm32f4xx_spi.c' ! -iname 'stm32f4xx_iwdg.c'
# Include the heap_4 RTOS_heap while excluding the other *_{1-5}
# Everything in src will be compiled
SRC := $(shell find $(SRCSEARCH) -name '*.c' $(SRCIGNORE) )

# Create dependency folders for object files
SRCDIRS := $(shell find $(SRCSEARCH) -name '*.c' $(SRCIGNORE) )
#SRCDIRS += $(shell find libs/dw1000/src -maxdepth 1 -name '*.c' -exec dirname {} \; | uniq)
SRCDIRS += startup

# Startup files
#STARTUP = startup/startup_stm32f40xx.s
#STARTUP = startup/startup_stm32f407xx.s
STARTUP = startup/startup_stm32f4.c

# Assembler file to facilitate printing of stack in case of hardfault
#HARDFAULT = startup/hardfault.s

# Create folder for storing all object files
OBJDIR = objects

OBJ    := $(patsubst %.c,$(OBJDIR)/%.bc,$(SRC))
#OBJASM := $(patsubst %.s,$(OBJDIR)/%.o,$(HARDFAULT))
OBJSTART := $(patsubst %.c,$(OBJDIR)/%.o,$(STARTUP))

DEPS    := $(patsubst %.bc,%.d,$(OBJ))
DEPS    += $(patsubst %.o,%.d,$(OBJASM))

DEPENDS  = -MT $@ -MD -MP -MF $(subst .o,.d,$@)
SHELL    = /bin/bash

.PHONY: all clean distclean


debugbuild: buildrepo $(EXECUTABLE)

all: buildrepo $(EXECUTABLE)

rel: buildrepo $(EXECUTABLE)

wcet: buildrepo $(EXECUTABLE)

# Link native code into final executable
#$(EXECUTABLE): $(EXECOBJ) $(OBJASM)
ifeq "$(MAKECMDGOALS)" "rel"
$(EXECUTABLE): $(EXECOBJ) $(OBJSTART)
	$(CC-native) $(INCLUDES) $(MCFLAGS) $(LDFLAGS) $^ -o $@
else ifeq "$(MAKECMDGOALS)" "wcet"
$(EXECUTABLE): $(EXECOBJ) $(OBJSTART)
	$(CC-native) $(INCLUDES) $(MCFLAGS) $(LDFLAGS) $^ -o $@
else
$(EXECUTABLE): $(EXECOBJ)
	echo "Not doing final ARM linking."
endif

# Specially compile the startup code with GCC since CLANG does not understand linker scripts
$(OBJSTART):
	$(CC-native) $(MCFLAGS) $(OPTIMIZE) $(DEFS) $(DEPENDS) -c $(STARTUP) $^ -o $@ $(INCLUDES) 

# Link LLVM-code into native code
$(EXECOBJ): $(IROUT)
	llc $(LLCFLAGS) $(IROUT) -o $@

$(IROUT): $(OBJ)
	llvm-link $^ -o $@

# Source files "-c" is to not link
$(OBJDIR)/%.bc: %.c
	$(CC) $(CFLAGS) -c $(CLANGLDFLAGS) $(DEPENDS) $< -o $@ $(INCLUDES)

# Assembler files "-c" is to not link
# Clang assembler files
#$(OBJDIR)/%.o: %.s
#	$(CC) $(CLANGMCFLAGS) -c $(CLANGLDFLAGS) $< -o $@ $(INCLUDES)

$(OBJDIR)/%.o: %.s
	$(CC-native) $(MCFLAGS) $(OPTIMIZE) $(DEFS) $(DEPENDS) $(STARTUP) $< -o $@ $(INCLUDES) 

# End of the CLANG block
endif

clean:
	$(RM) -r $(OBJDIR) $(EXECOBJ) $(IR) $(IROUT)

cleanall:
	$(RM) -r $(OBJDIR) $(EXECOBJ) $(IR) $(IROUT) klee-last klee-out* $(EXECUTABLE)

distclean: clean
	$(RM) $(EXECUTABLE)

buildrepo:
	@$(call make-repo)

flash: $(EXECUTABLE)
	$(OOCD) $(OOCDFLAGS) \
	  -c "init" -c "targets" -c "reset halt" \
	  -c "flash write_image erase $<" -c "verify_image $<" \
	  -c "reset run" -c "shutdown"

debug: $(EXECUTABLE)
	$(GDB) -n -iex 'target extended | $(OOCD) $(OOCDFLAGS) -c "gdb_port pipe"' \
	-iex 'mon halt' $<

klee: buildrepo $(EXECUTABLE)
	mkdir -p output; cp $(IROUT) output/; cd output; klee -emit-all-errors $(IROUT); cd ..

run: buildrepo $(EXECUTABLE)
	arm-none-eabi-gdb -q -x klee_stm_gdb.py $(EXECUTABLE)

bench: buildrepo $(EXECUTABLE)
	make clean; make; make klee; make clean; make wcet; make run; cp profiling_db_parser.py output/; cd output; python profiling_db_parser.py klee_profiling.db;

define make-repo
   for dir in $(SRCDIRS); \
   do \
    mkdir -p $(OBJDIR)/$$dir; \
   done
endef

ifneq "$(MAKECMDGOALS)" "distclean"
ifneq "$(MAKECMDGOALS)" "clean"
-include $(DEPS)
endif
endif

cleanold:
	rm -f Startup.lst  $(TARGET)  $(TARGET).lst $(OBJ) $(AUTOGEN)  $(TARGET).out  $(TARGET).hex  $(TARGET).map  $(TARGET).dmp  $(TARGET).elf