diff options
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 20 |
1 files changed, 15 insertions, 5 deletions
@@ -106,15 +106,21 @@ BBV_DIR?=../bbv C_WARNINGS ?= #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function -C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h) -C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_sim.c) +C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h riscv_softfloat.h) +C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_softfloat.c riscv_sim.c) # portability for MacPorts/MacOS C_SYS_INCLUDES = -I /opt/local/include C_SYS_LIBDIRS = -L /opt/local/lib -C_FLAGS = $(C_SYS_INCLUDES) -I $(SAIL_LIB_DIR) -I c_emulator -C_LIBS = $(C_SYS_LIBDIRS) -lgmp -lz +SOFTFLOAT_DIR = c_emulator/SoftFloat-3e +SOFTFLOAT_INCDIR = $(SOFTFLOAT_DIR)/source/include +SOFTFLOAT_LIBDIR = $(SOFTFLOAT_DIR)/build/Linux-x86_64-GCC +SOFTFLOAT_FLAGS = -I $(SOFTFLOAT_INCDIR) +SOFTFLOAT_LIBS = $(SOFTFLOAT_LIBDIR)/softfloat.a + +C_FLAGS = $(C_SYS_INCLUDES) -I $(SAIL_LIB_DIR) -I c_emulator $(SOFTFLOAT_FLAGS) +C_LIBS = $(C_SYS_LIBDIRS) -lgmp -lz $(SOFTFLOAT_LIBS) # The C simulator can be built to be linked against Spike for tandem-verification. # This needs the C bindings to Spike from https://github.com/SRI-CSL/l3riscv @@ -213,7 +219,10 @@ generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Make mkdir -p generated_definitions/c $(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@) -c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) Makefile +$(SOFTFLOAT_LIBS): + make -C $(SOFTFLOAT_LIBDIR) + +c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile gcc -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ generated_definitions/c/riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) model/main.sail Makefile @@ -374,6 +383,7 @@ clean: -rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/* -rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/* -rm -rf generated_definitions/for-rmem/* + -make -C $(SOFTFLOAT_LIBDIR) clean -rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 c_emulator/riscv_rvfi -rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp -rm -f *.gcno *.gcda |