Skip to content

Commit

Permalink
Rename c_emulator directory to just emulator
Browse files Browse the repository at this point in the history
It's the only emulator now so there's no need to distinguish it from the OCaml emulator.
  • Loading branch information
Timmmm committed Jan 2, 2025
1 parent fbd3aa6 commit b1c6beb
Show file tree
Hide file tree
Showing 488 changed files with 303 additions and 37 deletions.
2 changes: 1 addition & 1 deletion .pre-commit-config.yaml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# See https://pre-commit.com for more information
# See https://pre-commit.com/hooks.html for more hooks
exclude: '^(prover_snapshots)|(generated_definitions)|(c_emulator/SoftFloat-3e)'
exclude: '^(prover_snapshots)|(generated_definitions)|(emulator/SoftFloat-3e)'
minimum_pre_commit_version: 2.10.0
repos:
- repo: https://github.com/pre-commit/pre-commit-hooks
Expand Down
24 changes: 12 additions & 12 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -147,10 +147,10 @@ export LEM_DIR

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 riscv_softfloat.h)
C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_softfloat.c riscv_sim.c)
C_INCS = $(addprefix emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h riscv_softfloat.h)
C_SRCS = $(addprefix emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_softfloat.c riscv_sim.c)

SOFTFLOAT_DIR = c_emulator/SoftFloat-3e
SOFTFLOAT_DIR = emulator/SoftFloat-3e
SOFTFLOAT_INCDIR = $(SOFTFLOAT_DIR)/source/include
SOFTFLOAT_LIBDIR = $(SOFTFLOAT_DIR)/build/Linux-RISCV-GCC
SOFTFLOAT_FLAGS = -I $(SOFTFLOAT_INCDIR)
Expand All @@ -165,7 +165,7 @@ GMP_LIBS = $(shell pkg-config --libs gmp || echo -lgmp)
ZLIB_FLAGS = $(shell pkg-config --cflags zlib)
ZLIB_LIBS = $(shell pkg-config --libs zlib)

C_FLAGS = -I $(SAIL_LIB_DIR) -I c_emulator $(GMP_FLAGS) $(ZLIB_FLAGS) $(SOFTFLOAT_FLAGS)
C_FLAGS = -I $(SAIL_LIB_DIR) -I emulator $(GMP_FLAGS) $(ZLIB_FLAGS) $(SOFTFLOAT_FLAGS)
C_LIBS = $(GMP_LIBS) $(ZLIB_LIBS) $(SOFTFLOAT_LIBS)

# The C simulator can be built to be linked against Spike for tandem-verification.
Expand Down Expand Up @@ -215,7 +215,7 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))

.PHONY:

all: c_emulator/riscv_sim_$(ARCH)
all: emulator/riscv_sim_$(ARCH)
.PHONY: all

# the following ensures empty sail-generated .c files don't hang around and
Expand Down Expand Up @@ -249,11 +249,11 @@ $(SOFTFLOAT_LIBS):

# convenience target
.PHONY: csim
csim: c_emulator/riscv_sim_$(ARCH)
csim: emulator/riscv_sim_$(ARCH)
.PHONY: rvfi
rvfi: c_emulator/riscv_rvfi_$(ARCH)
rvfi: emulator/riscv_rvfi_$(ARCH)

c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS_WRAPPED) -o $@

# Note: We have to add -c_preserve since the functions might be optimized out otherwise
Expand All @@ -278,7 +278,7 @@ generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main
sed -e '/^[[:space:]]*$$/d' $@ > $@.new
mv $@.new $@

c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS_WRAPPED) -o $@

latex: $(SAIL_SRCS) Makefile
Expand Down Expand Up @@ -408,17 +408,17 @@ generated_definitions/for-rmem/riscv.defs: $(SAIL_RMEM_SRCS)

FORCE:

SHARE_FILES:=$(sort $(wildcard model/*.sail)) $(sort $(wildcard c_emulator/*.c)) $(sort $(wildcard c_emulator/*.h)) $(sort $(wildcard handwritten_support/*.lem)) $(sort $(wildcard handwritten_support/hgen/*.hgen)) $(RMEM_FILES)
SHARE_FILES:=$(sort $(wildcard model/*.sail)) $(sort $(wildcard emulator/*.c)) $(sort $(wildcard emulator/*.h)) $(sort $(wildcard handwritten_support/*.lem)) $(sort $(wildcard handwritten_support/hgen/*.hgen)) $(RMEM_FILES)
sail-riscv.install: FORCE
echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install
echo 'bin: ["emulator/riscv_sim_RV64" "emulator/riscv_sim_RV32"]' > sail-riscv.install
echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install

clean:
-rm -rf 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_RV32 c_emulator/riscv_rvfi_RV64
-rm -f emulator/riscv_sim_RV32 emulator/riscv_sim_RV64 emulator/riscv_rvfi_RV32 emulator/riscv_rvfi_RV64
-rm -f *.gcno *.gcda
-rm -f z3_problems
-Holmake cleanAll
Expand Down
10 changes: 5 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ Install [Sail](https://github.com/rems-project/sail/). On Linux you can download
$ make
```

will build the simulator in `c_emulator/riscv_sim_RV64`.
will build the simulator in `emulator/riscv_sim_RV64`.

If you get an error message saying `sail: unknown option '--require-version'.` it's because your Sail compiler is too old. You need version 0.18 or later.

Expand All @@ -63,7 +63,7 @@ built using:
$ ARCH=RV32 make
```

which creates the simulator in `c_emulator/riscv_sim_RV32`.
which creates the simulator in `emulator/riscv_sim_RV32`.

The Makefile targets `riscv_isa_build`, `riscv_coq_build`, and
`riscv_hol_build` invoke the respective prover to process the
Expand All @@ -82,7 +82,7 @@ corresponding prover libraries in the Sail directory
The simulator can be used to execute small test binaries.

```
$ ./c_emulator/riscv_sim_<arch> <elf-file>
$ ./emulator/riscv_sim_<arch> <elf-file>
```

A suite of RV32 and RV64 test programs derived from the
Expand All @@ -93,7 +93,7 @@ can be run using `test/run_tests.sh`.
### Configuring platform options

Information on configuration options for the simulator is available from
`./c_emulator/riscv_sim_<arch> -h`.
`./emulator/riscv_sim_<arch> -h`.

Some useful options are: configuring whether misaligned accesses trap
(`--enable-misaligned`), and
Expand Down Expand Up @@ -339,7 +339,7 @@ sail-riscv
- latex
- prover_snapshots // snapshots of generated theorem prover definitions
- handwritten_support // prover support files
- c_emulator // supporting platform files for C emulator
- emulator // supporting platform files for C emulator
- doc // documentation, including a reading guide
- test // test files
- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo
Expand Down
4 changes: 2 additions & 2 deletions build_simulators.sh
Original file line number Diff line number Diff line change
Expand Up @@ -10,5 +10,5 @@ function test_build () {
fi
}

test_build make ARCH=RV32 c_emulator/riscv_sim_RV32
test_build make ARCH=RV64 c_emulator/riscv_sim_RV64
test_build make ARCH=RV32 emulator/riscv_sim_RV32
test_build make ARCH=RV64 emulator/riscv_sim_RV64
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
Loading

0 comments on commit b1c6beb

Please sign in to comment.