Collect all symbolic execution theories and libraries we used for app…

…lications in src/tools/symbexec
kth-step · Aug 23, 2024 · 2660341 · 2660341
1 parent b52731b
commit 2660341
Show file tree

Hide file tree

Showing 22 changed files with 0 additions and 24 deletions.
diff --git a/examples/riscv/aes-unopt/Holmakefile b/examples/riscv/aes-unopt/Holmakefile
@@ -18,7 +18,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/aes/Holmakefile b/examples/riscv/aes/Holmakefile
@@ -18,7 +18,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/chacha/Holmakefile b/examples/riscv/chacha/Holmakefile
@@ -19,7 +19,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/common/Holmakefile b/examples/riscv/common/Holmakefile
diff --git a/examples/riscv/incr-mem/Holmakefile b/examples/riscv/incr-mem/Holmakefile
@@ -18,7 +18,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/incr/Holmakefile b/examples/riscv/incr/Holmakefile
@@ -18,7 +18,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/isqrt/Holmakefile b/examples/riscv/isqrt/Holmakefile
@@ -19,7 +19,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/mod2-mem/Holmakefile b/examples/riscv/mod2-mem/Holmakefile
@@ -18,7 +18,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/mod2/Holmakefile b/examples/riscv/mod2/Holmakefile
@@ -19,7 +19,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/modexp/Holmakefile b/examples/riscv/modexp/Holmakefile
@@ -18,7 +18,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/motor/Holmakefile b/examples/riscv/motor/Holmakefile
@@ -18,7 +18,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/perftest/Holmakefile b/examples/riscv/perftest/Holmakefile
@@ -18,7 +18,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/swap/Holmakefile b/examples/riscv/swap/Holmakefile
@@ -17,7 +17,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/symbexectests/Holmakefile b/examples/riscv/symbexectests/Holmakefile
@@ -18,7 +18,6 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
            $(HOLBADIR)/examples/tutorial/support \
            $(HOLBADIR)/src/tools/symbexec \
            $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/examples/riscv/common \
            $(HOLBADIR)/src
 
 all: $(DEFAULT_TARGETS)

diff --git a/examples/riscv/common/bir_predLib.sig → src/tools/symbexec/bir_predLib.sig b/examples/riscv/common/bir_predLib.sig → src/tools/symbexec/bir_predLib.sig
diff --git a/examples/riscv/common/bir_predLib.sml → src/tools/symbexec/bir_predLib.sml b/examples/riscv/common/bir_predLib.sml → src/tools/symbexec/bir_predLib.sml
diff --git a/...mples/common/bir_program_transfScript.sml → ...ols/symbexec/bir_program_transfScript.sml b/...mples/common/bir_program_transfScript.sml → ...ols/symbexec/bir_program_transfScript.sml
diff --git a/examples/riscv/common/bir_symbLib.sig → src/tools/symbexec/bir_symbLib.sig b/examples/riscv/common/bir_symbLib.sig → src/tools/symbexec/bir_symbLib.sig
diff --git a/examples/riscv/common/bir_symbLib.sml → src/tools/symbexec/bir_symbLib.sml b/examples/riscv/common/bir_symbLib.sml → src/tools/symbexec/bir_symbLib.sml
diff --git a/...cv/common/distribute_generic_stuffLib.sml → .../symbexec/distribute_generic_stuffLib.sml b/...cv/common/distribute_generic_stuffLib.sml → .../symbexec/distribute_generic_stuffLib.sml
diff --git a/...common/distribute_generic_stuffScript.sml → ...mbexec/distribute_generic_stuffScript.sml b/...common/distribute_generic_stuffScript.sml → ...mbexec/distribute_generic_stuffScript.sml
diff --git a/.../riscv/common/jgmt_rel_bir_contScript.sml → ...ools/symbexec/jgmt_rel_bir_contScript.sml b/.../riscv/common/jgmt_rel_bir_contScript.sml → ...ools/symbexec/jgmt_rel_bir_contScript.sml