Merge branch 'JSON' into issue-21

Signed-off-by: Joydeep Tripathy <[email protected]>
joydeep049 · Jul 1, 2024 · e49bf8d · e49bf8d
2 parents 3bfd9f9 + 5b70681
commit e49bf8d
Show file tree

Hide file tree

Showing 131 changed files with 5,148 additions and 10,735 deletions.
diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml
@@ -22,13 +22,13 @@ jobs:
       run: eval $(opam env) && test/run_tests.sh
     - name: Upload test results
       if: always()
-      uses: actions/upload-artifact@v2
+      uses: actions/upload-artifact@v4
       with:
         name: tests.xml
         path: test/tests.xml
     - name: Upload event payload
       if: always()
-      uses: actions/upload-artifact@v2
+      uses: actions/upload-artifact@v4
       with:
         name: event.json
         path: ${{ github.event_path }}
diff --git a/.github/workflows/test-results.yml b/.github/workflows/test-results.yml
@@ -12,11 +12,11 @@ jobs:
     if: github.event.workflow_run.conclusion != 'skipped'
     steps:
     - name: Download artifacts
-      uses: actions/github-script@v3.1.0
+      uses: actions/github-script@v6
       with:
         script: |
           var fs = require('fs');
-          var artifacts = await github.actions.listWorkflowRunArtifacts({
+          var artifacts = await github.rest.actions.listWorkflowRunArtifacts({
              owner: context.repo.owner,
              repo: context.repo.repo,
              run_id: ${{github.event.workflow_run.id }},
@@ -27,7 +27,7 @@ jobs:
           var count = matchArtifacts.length;
           for (var i = 0; i < count; i++) {
             var matchArtifact = matchArtifacts[i];
-            var download = await github.actions.downloadArtifact({
+            var download = await github.rest.actions.downloadArtifact({
                owner: context.repo.owner,
                repo: context.repo.repo,
                artifact_id: matchArtifact.id,
@@ -43,7 +43,7 @@ jobs:
     - name: Extract event payload
       run: unzip event.json.zip
     - name: Publish test results
-      uses: EnricoMi/publish-unit-test-result-action@v1
+      uses: EnricoMi/publish-unit-test-result-action@v2
       with:
         commit: ${{ github.event.workflow_run.head_sha }}
         event_file: event.json

diff --git a/CODE_STYLE.md b/CODE_STYLE.md
@@ -15,6 +15,8 @@ Formatting
 
 * Block-level indentation uses two spaces
 
+* Tabs should not be used
+
 * There should be no trailing spaces on any lines
 
 * All files should end with a newline character

diff --git a/LICENCE b/LICENCE
@@ -5,25 +5,49 @@ directories except for the snapshots of the Lem and Sail libraries
 in the prover_snapshots directory (which include copies of their
 licences), is subject to the BSD two-clause licence below.
 
-Copyright (c) 2017-2023
-  Prashanth Mundkur
-  Rishiyur S. Nikhil and Bluespec, Inc.
-  Jon French
-  Brian Campbell
-  Robert Norton-Wright
-  Alasdair Armstrong
-  Thomas Bauereiss
-  Shaked Flur
-  Christopher Pulte
-  Peter Sewell
-  Alexander Richardson
-  Hesham Almatary
-  Jessica Clarke
-  Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo
-  Peter Rugg
-  Aril Computer Corp., for contributions by Scott Johnson
-  Philipp Tomsich
-  VRULL GmbH, for contributions by its employees
+Copyright (c) 2017-2024
+   ahadali5000
+   Alasdair Armstrong
+   Alexander Richardson
+   Aril Computer Corp., for contributions by Scott Johnson
+   Ben Marshall
+   Bicheng Yang
+   Bilal Sakhawat
+   Brian Campbell
+   Chris Casinghino
+   Christopher Pulte
+   Codasip, for contributions by Tim Hutt, Martin Berger and Ben Fletcher
+   dylux
+   eroom1966
+   Google LLC, for contributions by its employees
+   Hesham Almatary
+   Jan Henrik Weinstock
+   Jessica Clarke
+   Jon French
+   Martin Berger
+   Michael Sammler
+   Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo
+   Muhammad Bilal Sakhawat
+   Nathaniel Wesley Filardo
+   Paul A. Clarke
+   Peter Rugg
+   Peter Sewell
+   Philipp Tomsich
+   Prashanth Mundkur
+   Rafael Sene
+   Rishiyur S. Nikhil (Bluespec, Inc.)
+   Robert Norton-Wright
+   Scott Johnson (Aril Inc.)
+   Shaked Flur
+   Thibaut Pérami
+   Thomas Bauereiss
+   VRULL GmbH, for contributions by its employees
+   William McSpaddden
+   Xinlai Wan
+
+For a complete list of authors run this command:
+
+    git shortlog --summary --numbered --email
 
 All rights reserved.
 
@@ -42,6 +66,7 @@ This project has received funding from the European Research Council
 (ERC) under the European Union’s Horizon 2020 research and innovation
 programme (grant agreement 789108, ELVER).
 
+------------------------------------------------------------------
 
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions

diff --git a/Makefile b/Makefile
@@ -7,6 +7,9 @@ else ifeq ($(ARCH),64)
   override ARCH := RV64
 endif
 
+# Set OPAMCLI to 2.0 to supress warnings about opam config var
+export OPAMCLI := 2.0
+
 ifeq ($(ARCH),RV32)
   SAIL_XLEN := riscv_xlen32.sail
 else ifeq ($(ARCH),RV64)
@@ -24,11 +27,15 @@ SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext
 SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_cfext.sail
 SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_cdext.sail
 
+SAIL_DEFAULT_INST += riscv_insts_svinval.sail
+
 SAIL_DEFAULT_INST += riscv_insts_zba.sail
 SAIL_DEFAULT_INST += riscv_insts_zbb.sail
 SAIL_DEFAULT_INST += riscv_insts_zbc.sail
 SAIL_DEFAULT_INST += riscv_insts_zbs.sail
 
+SAIL_DEFAULT_INST += riscv_insts_zcb.sail
+
 SAIL_DEFAULT_INST += riscv_insts_zfh.sail
 # Zfa needs to be added after fext, dext and Zfh (as it needs
 # definitions from those)
@@ -68,18 +75,24 @@ SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdex
 SAIL_SYS_SRCS += riscv_csr_ext.sail         # access to CSR extensions
 SAIL_SYS_SRCS += riscv_sys_control.sail     # general exception handling
 
-SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail
-SAIL_RV64_VM_SRCS = riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_vmem_rv64.sail
+# SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail
+# SAIL_RV64_VM_SRCS = riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_vmem_rv64.sail
 
-SAIL_VM_SRCS = riscv_pte.sail riscv_ptw.sail riscv_vmem_common.sail riscv_vmem_tlb.sail
-ifeq ($(ARCH),RV32)
-SAIL_VM_SRCS += $(SAIL_RV32_VM_SRCS)
-else
-SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS)
-endif
+# SAIL_VM_SRCS = riscv_pte.sail riscv_ptw.sail riscv_vmem_common.sail riscv_vmem_tlb.sail
+# ifeq ($(ARCH),RV32)
+# SAIL_VM_SRCS += $(SAIL_RV32_VM_SRCS)
+# else
+# SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS)
+# endif
+
+SAIL_VM_SRCS += riscv_vmem_common.sail
+SAIL_VM_SRCS += riscv_vmem_pte.sail
+SAIL_VM_SRCS += riscv_vmem_ptw.sail
+SAIL_VM_SRCS += riscv_vmem_tlb.sail
+SAIL_VM_SRCS += riscv_vmem.sail
 
 # Non-instruction sources
-PRELUDE = prelude.sail prelude_mapping.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
+PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
 
 SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail
 SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail
@@ -96,16 +109,13 @@ SAIL_ARCH_SRCS += riscv_types_kext.sail    # Shared/common code for the cryptogr
 SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail
 RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail
 
-# Control inclusion of 64-bit only riscv_analysis
-ifeq ($(ARCH),RV32)
 SAIL_OTHER_SRCS     = $(SAIL_STEP_SRCS)
+ifeq ($(ARCH),RV32)
 SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv32.sail
 else
-SAIL_OTHER_SRCS     = $(SAIL_STEP_SRCS) riscv_analysis.sail
-SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv64.sail riscv_analysis.sail
+SAIL_OTHER_COQ_SRCS = riscv_termination_common.sail riscv_termination_rv64.sail
 endif
 
-
 PRELUDE_SRCS   = $(addprefix model/,$(PRELUDE))
 SAIL_SRCS      = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS)  $(SAIL_OTHER_SRCS))
 SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(SAIL_OTHER_SRCS))
@@ -125,14 +135,16 @@ export SAIL_DIR
 EXPLICIT_COQ_SAIL=yes
 else
 # Use sail from opam package
-SAIL_DIR:=$(shell opam config var sail:share)
+SAIL_DIR:=$(shell OPAMCLI=$(OPAMCLI) opam config var sail:share)
 SAIL:=sail
 endif
 SAIL_LIB_DIR:=$(SAIL_DIR)/lib
 export SAIL_LIB_DIR
 SAIL_SRC_DIR:=$(SAIL_DIR)/src
 
-LEM_DIR?=$(shell opam config var lem:share)
+ifndef LEM_DIR
+LEM_DIR:=$(shell OPAMCLI=$(OPAMCLI) opam config var lem:share)
+endif
 export LEM_DIR
 
 C_WARNINGS ?=
@@ -173,7 +185,7 @@ ifneq (,$(COVERAGE))
 C_FLAGS += --coverage -O1
 SAIL_FLAGS += -Oconstant_fold
 else
-C_FLAGS += -O3 -flto
+C_FLAGS += -O3 -flto=auto
 endif
 
 ifneq (,$(SAILCOV))
@@ -184,24 +196,22 @@ C_LIBS += $(SAIL_LIB_DIR)/coverage/libsail_coverage.a -lm -lpthread -ldl
 endif
 
 RISCV_EXTRAS_LEM_FILES = riscv_extras.lem mem_metadata.lem riscv_extras_fdext.lem
-# Feature detect if we are on the latest development version of Sail
-# and use an updated lem file if so. This is just until the opam
-# version catches up with changes to the barrier type.
-SAIL_LATEST := $(shell $(SAIL) -have_feature FEATURE_UNION_BARRIER 1>&2 2> /dev/null; echo $$?)
-ifeq ($(SAIL_LATEST),0)
-RISCV_EXTRAS_LEM = $(addprefix handwritten_support/0.11/,$(RISCV_EXTRAS_LEM_FILES))
-else
 RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))
-endif
 
 .PHONY:
 
-all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) riscv_isa riscv_coq riscv_hol riscv_rmem
+all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH)
 .PHONY: all
 
 json: $(SAIL_SRCS) model/main.sail Makefile
 	@sail -json $(SAIL_FLAGS) $(SAIL_SRCS)
 
+
+.PHONY: check-json
+check-json:
+	sail -json $(SAIL_FLAGS) $(SAIL_SRCS) | python3 -c "import json; import sys; j=json.load(sys.stdin)"
+
+
 output: $(SAIL_SRCS) model/main.sail Makefile
 	sail -output-sail $(SAIL_FLAGS) $(SAIL_SRCS)
 
@@ -261,9 +271,11 @@ gcovr:
 ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml
 	ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@
 
+c_preserve_fns=-c_preserve _set_Misa_C
+
 generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
 	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 $@)
+	$(SAIL) $(SAIL_FLAGS) $(c_preserve_fns) -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 $@)
 
 generated_definitions/c2/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
 	mkdir -p generated_definitions/c2
@@ -281,7 +293,7 @@ osim: ocaml_emulator/riscv_ocaml_sim_$(ARCH)
 rvfi: c_emulator/riscv_rvfi_$(ARCH)
 
 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 $@
+	$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
 
 # Note: We have to add -c_preserve since the functions might be optimized out otherwise
 rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
@@ -302,12 +314,12 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
 # sed -i isn't posix compliant, unfortunately
 generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile
 	mkdir -p generated_definitions/c
-	$(SAIL) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
+	$(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
 	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
-	gcc -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
+	$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
 
 latex: $(SAIL_SRCS) Makefile
 	mkdir -p generated_definitions/latex
@@ -331,12 +343,12 @@ endif
 
 generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile
 	mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH)
-	$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS)
+	$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS)
 	echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem
 
 # sed -i isn't posix compliant, unfortunately
 generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) Makefile
-	lem -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \
+	lem -wl ign -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \
 		$(RISCV_EXTRAS_LEM) \
 		generated_definitions/lem/$(ARCH)/riscv_types.lem \
 		generated_definitions/lem/$(ARCH)/riscv.lem
@@ -372,17 +384,17 @@ riscv_hol_build: generated_definitions/hol4/$(ARCH)/riscvTheory.uo
 .PHONY: riscv_hol riscv_hol_build
 
 ifdef BBV_DIR
-  EXPLICIT_COQ_BBV = yes
+  EXPLICIT_COQ_BBV := yes
 else
-  EXPLICIT_COQ_BBV = $(shell if opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
+  EXPLICIT_COQ_BBV := $(shell if OPAMCLI=$(OPAMCLI) opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
   ifeq ($(EXPLICIT_COQ_BBV),yes)
     #Coq BBV library hopefully checked out in directory above us
     BBV_DIR = ../bbv
   endif
 endif
 
 ifndef EXPLICIT_COQ_SAIL
-  EXPLICIT_COQ_SAIL = $(shell if opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
+  EXPLICIT_COQ_SAIL := $(shell if OPAMCLI=$(OPAMCLI) opam config var coq-sail:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
 endif
 
 COQ_LIBS = -R generated_definitions/coq Riscv -R generated_definitions/coq/$(ARCH) $(ARCH) -R handwritten_support Riscv_common
@@ -457,7 +469,7 @@ 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)) $(sort $(wildcard handwritten_support/0.11/*.lem)) $(RMEM_FILES)
+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)
 sail-riscv.install: FORCE
 	echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install
 	echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install