bundled version of l3 riscv model and step from trindemossen-1

kth-step · Dec 5, 2024 · 1558506 · 1558506
1 parent 6a11ebe
commit 1558506
Show file tree

Hide file tree

Showing 50 changed files with 39,365 additions and 74 deletions.
diff --git a/examples/aes/Holmakefile b/examples/aes/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \

diff --git a/examples/aes/exec/Holmakefile b/examples/aes/exec/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/tools/lifter \

diff --git a/examples/aes/lifter/Holmakefile b/examples/aes/lifter/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/tools/exec \
            $(HOLBADIR)/src/tools/lifter
 

diff --git a/examples/aes/wp/Holmakefile b/examples/aes/wp/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \

diff --git a/examples/bsl-wp-smt/Holmakefile b/examples/bsl-wp-smt/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared/smt \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \

diff --git a/examples/nic/Holmakefile b/examples/nic/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared/smt \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \

diff --git a/examples/riscv/aes-unopt/Holmakefile b/examples/riscv/aes-unopt/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/aes/Holmakefile b/examples/riscv/aes/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/chacha/Holmakefile b/examples/riscv/chacha/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/chachapoly/Holmakefile b/examples/riscv/chachapoly/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/ifelse/Holmakefile b/examples/riscv/ifelse/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/incr-mem/Holmakefile b/examples/riscv/incr-mem/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/incr/Holmakefile b/examples/riscv/incr/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/isqrt/Holmakefile b/examples/riscv/isqrt/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/kernel/Holmakefile b/examples/riscv/kernel/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/mod2-mem/Holmakefile b/examples/riscv/mod2-mem/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/mod2/Holmakefile b/examples/riscv/mod2/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/modexp/Holmakefile b/examples/riscv/modexp/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/motor/Holmakefile b/examples/riscv/motor/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/perftest/Holmakefile b/examples/riscv/perftest/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/poly1305-inlined/Holmakefile b/examples/riscv/poly1305-inlined/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/poly1305/Holmakefile b/examples/riscv/poly1305/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/swap/Holmakefile b/examples/riscv/swap/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/riscv/symbexectests/Holmakefile b/examples/riscv/symbexectests/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \
            $(HOLBADIR)/src/theory/program_logic \

diff --git a/examples/tutorial/2-lift/Holmakefile b/examples/tutorial/2-lift/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \

diff --git a/examples/tutorial/4-bir-to-arm/Holmakefile b/examples/tutorial/4-bir-to-arm/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \

diff --git a/examples/tutorial/5-wp/Holmakefile b/examples/tutorial/5-wp/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \

diff --git a/examples/tutorial/6-smt/Holmakefile b/examples/tutorial/6-smt/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \

diff --git a/examples/tutorial/7-composition/Holmakefile b/examples/tutorial/7-composition/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/theory/bir \
            $(HOLBADIR)/src/theory/bir-support \

diff --git a/examples/tutorial/8-symbexec/Holmakefile b/examples/tutorial/8-symbexec/Holmakefile
@@ -3,8 +3,8 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLDIR)/examples/l3-machine-code/arm8/step \
            $(HOLDIR)/examples/l3-machine-code/m0/model \
            $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLDIR)/examples/l3-machine-code/riscv/model \
-           $(HOLDIR)/examples/l3-machine-code/riscv/step \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
+           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
            $(HOLBADIR)/src/shared \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/examples/tutorial/2-lift \

diff --git a/src/shared/l3-machine-code/COPYRIGHT b/src/shared/l3-machine-code/COPYRIGHT
@@ -0,0 +1,32 @@
+HOL COPYRIGHT NOTICE, LICENSE AND DISCLAIMER.
+
+Copyright 1985--2023 by the HOL4 CONTRIBUTORS
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+  * Redistributions of source code must retain the above copyright
+    notice, this list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above copyright
+    notice, this list of conditions and the following disclaimer in
+    the documentation and/or other materials provided with the
+    distribution.
+
+  * The names of the copyright holders and contributors may not be
+    used to endorse or promote products derived from this software
+    without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS
+OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR
+TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
+USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGE.