Merge pull request diffblue#8158 from tautschnig/cleanup/remove-jsil

Remove JSIL front-end
remi-delmas-3000 · Jan 15, 2024 · caf9768 · caf9768
2 parents fd28cb2 + 67be193
commit caf9768
Show file tree

Hide file tree

Showing 51 changed files with 5 additions and 3,603 deletions.
diff --git a/.gitignore b/.gitignore
@@ -91,10 +91,6 @@ src/ansi-c/ansi_c_y.tab.cpp
 src/ansi-c/ansi_c_y.tab.h
 src/assembler/assembler_lex.yy.cpp
 src/crangler/c_lex.yy.cpp
-src/jsil/jsil_lex.yy.cpp
-src/jsil/jsil_y.output
-src/jsil/jsil_y.tab.cpp
-src/jsil/jsil_y.tab.h
 src/json/json_lex.yy.cpp
 src/json/json_y.output
 src/json/json_y.tab.cpp

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -256,7 +256,6 @@ cprover_default_properties(
     goto-symex
     goto-synthesizer
     goto-synthesizer-lib
-    jsil
     json
     json-symtab-language
     langapi

diff --git a/CODEOWNERS b/CODEOWNERS
@@ -56,7 +56,6 @@
 /src/goto-inspect/ @diffblue/diffblue-opensource
 /src/goto-synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
 /src/goto-diff/ @tautschnig @peterschrammel
-/src/jsil/ @kroening @tautschnig
 /src/memory-analyzer/ @tautschnig @kroening
 /jbmc/src/jbmc/ @peterschrammel @TGWDB
 /jbmc/src/janalyzer/ @peterschrammel @TGWDB

diff --git a/doc/architectural/folder-walkthrough.md b/doc/architectural/folder-walkthrough.md
@@ -32,7 +32,6 @@ containing the code for a different part of the system.
   * C: \ref ansi-c
   * C++: \ref cpp
   * Java: \ref java_bytecode
-  * JavaScript: \ref jsil
 
 - Tools
 
@@ -155,7 +154,6 @@ digraph directory_dependencies {
     ansi_c [label = "ansi-c", URL = "\ref ansi-c"];
     langapi [URL = "\ref langapi"];
     cpp [URL = "\ref cpp"];
-    jsil [URL = "\ref jsil"];
     java_bytecode [URL = "\ref java_bytecode"];  
   }
 
@@ -174,15 +172,14 @@ digraph directory_dependencies {
   JBMC -> { CBMC, java_bytecode };
   jdiff -> { goto_diff, java_bytecode };
   janalyzer -> { goto_analyzer, java_bytecode };
-  CBMC -> { goto_instrument, jsil };
+  CBMC -> { goto_instrument };
   goto_diff -> { goto_instrument };
-  goto_analyzer -> { analyses, jsil, cpp };
+  goto_analyzer -> { analyses, cpp };
   goto_instrument -> { goto_symex, cpp };
-  goto_cc -> { cpp, jsil };
+  goto_cc -> { cpp };
   smt2_solver -> solvers;
 
   java_bytecode -> { analyses, miniz };
-  jsil -> linking;
   cpp -> ansi_c;
   ansi_c -> langapi;
   langapi -> goto_programs;

diff --git a/jbmc/src/janalyzer/Makefile b/jbmc/src/janalyzer/Makefile
@@ -34,11 +34,6 @@ CLEANFILES = janalyzer$(EXEEXT)
 
 all: janalyzer$(EXEEXT)
 
-ifneq ($(wildcard ../jsil/Makefile),)
-  OBJ += ../jsil/jsil$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JSIL
-endif
-
 ###############################################################################
 
 janalyzer$(EXEEXT): $(OBJ)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -99,7 +99,6 @@ add_subdirectory(goto-checker)
 add_subdirectory(goto-programs)
 add_subdirectory(goto-symex)
 add_subdirectory(goto-inspect)
-add_subdirectory(jsil)
 add_subdirectory(json)
 add_subdirectory(json-symtab-language)
 add_subdirectory(langapi)

diff --git a/src/Makefile b/src/Makefile
@@ -17,7 +17,6 @@ DIRS = analyses \
        goto-programs \
        goto-symex \
        goto-synthesizer \
-       jsil \
        json \
        json-symtab-language \
        langapi \
@@ -82,7 +81,7 @@ crangler.dir: util.dir json.dir
 
 languages: util.dir langapi.dir \
            cpp.dir ansi-c.dir xmllang.dir assembler.dir \
-           jsil.dir json.dir json-symtab-language.dir statement-list.dir
+           json.dir json-symtab-language.dir statement-list.dir
 
 solvers.dir: util.dir
 

diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt
@@ -29,7 +29,6 @@ target_link_libraries(cbmc-lib
 )
 
 add_if_library(cbmc-lib bv_refinement)
-add_if_library(cbmc-lib jsil)
 
 # Executable
 add_executable(cbmc cbmc_main.cpp)

diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
@@ -60,11 +60,6 @@ ifneq ($(wildcard ../bv_refinement/Makefile),)
   CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
 endif
 
-ifneq ($(wildcard ../jsil/Makefile),)
-  OBJ += ../jsil/jsil$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JSIL
-endif
-
 ###############################################################################
 
 cbmc$(EXEEXT): $(OBJ)

diff --git a/src/cbmc/cbmc_languages.cpp b/src/cbmc/cbmc_languages.cpp
@@ -18,18 +18,10 @@ Author: Daniel Kroening, [email protected]
 #include <json-symtab-language/json_symtab_language.h>
 #include <statement-list/statement_list_language.h>
 
-#ifdef HAVE_JSIL
-#  include <jsil/jsil_language.h>
-#endif
-
 void cbmc_parse_optionst::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_statement_list_language);
   register_language(new_cpp_language);
   register_language(new_json_symtab_language);
-
-#ifdef HAVE_JSIL
-  register_language(new_jsil_language);
-#endif
 }
diff --git a/src/cbmc/module_dependencies.txt b/src/cbmc/module_dependencies.txt
@@ -6,7 +6,6 @@ goto-checker
 goto-instrument
 goto-programs
 goto-symex
-jsil
 json
 json-symtab-language
 langapi # should go away

diff --git a/src/cprover/CMakeLists.txt b/src/cprover/CMakeLists.txt
@@ -29,7 +29,6 @@ target_link_libraries(cprover-lib
 )
 
 add_if_library(cprover-lib bv_refinement)
-add_if_library(cprover-lib jsil)
 
 # Executable
 add_executable(cprover cprover_main.cpp)

diff --git a/src/goto-analyzer/CMakeLists.txt b/src/goto-analyzer/CMakeLists.txt
@@ -22,8 +22,6 @@ target_link_libraries(goto-analyzer-lib
     util
 )
 
-add_if_library(goto-analyzer-lib jsil)
-
 # Executable
 add_executable(goto-analyzer goto_analyzer_main.cpp)
 target_link_libraries(goto-analyzer goto-analyzer-lib)

diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile
@@ -36,11 +36,6 @@ CLEANFILES = goto-analyzer$(EXEEXT)
 
 all: goto-analyzer$(EXEEXT)
 
-ifneq ($(wildcard ../jsil/Makefile),)
-  OBJ += ../jsil/jsil$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JSIL
-endif
-
 ###############################################################################
 
 goto-analyzer$(EXEEXT): $(OBJ)

diff --git a/src/goto-analyzer/goto_analyzer_languages.cpp b/src/goto-analyzer/goto_analyzer_languages.cpp
@@ -16,16 +16,8 @@ Author: Martin Brain, [email protected]
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
 
-#ifdef HAVE_JSIL
-#  include <jsil/jsil_language.h>
-#endif
-
 void goto_analyzer_parse_optionst::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
-
-#ifdef HAVE_JSIL
-  register_language(new_jsil_language);
-#endif
 }
diff --git a/src/goto-analyzer/module_dependencies.txt b/src/goto-analyzer/module_dependencies.txt
@@ -7,6 +7,5 @@ goto-checker
 goto-programs
 java_bytecode # will go away
 langapi # should go away
-jsil
 json
 util
diff --git a/src/goto-cc/CMakeLists.txt b/src/goto-cc/CMakeLists.txt
@@ -20,8 +20,6 @@ target_link_libraries(goto-cc-lib
     langapi
 )
 
-add_if_library(goto-cc-lib jsil)
-
 # Executable
 add_executable(goto-cc goto_cc_main.cpp)
 target_link_libraries(goto-cc goto-cc-lib)

diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile
@@ -51,11 +51,6 @@ else
 all: goto-gcc$(EXEEXT)
 endif
 
-ifneq ($(wildcard ../jsil/Makefile),)
-  OBJ += ../jsil/jsil$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JSIL
-endif
-
 ###############################################################################
 
 goto-gcc$(EXEEXT): goto-cc$(EXEEXT)

diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
@@ -141,7 +141,7 @@ static file_typet detect_file_type(
   if(
     ext == "c" || ext == "cc" || ext == "cp" || ext == "cpp" || ext == "CPP" ||
     ext == "c++" || ext == "C" || ext == "i" || ext == "ii" || ext == "class" ||
-    ext == "jar" || ext == "jsil")
+    ext == "jar")
   {
     return file_typet::SOURCE_FILE;
   }

diff --git a/src/goto-cc/goto_cc_languages.cpp b/src/goto-cc/goto_cc_languages.cpp
@@ -16,16 +16,8 @@ Author: CM Wintersteiger
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
 
-#ifdef HAVE_JSIL
-#  include <jsil/jsil_language.h>
-#endif
-
 void goto_cc_modet::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
-
-#ifdef HAVE_JSIL
-  register_language(new_jsil_language);
-#endif
 }
diff --git a/src/goto-cc/module_dependencies.txt b/src/goto-cc/module_dependencies.txt
@@ -2,7 +2,6 @@ ansi-c
 cpp
 goto-cc
 goto-programs
-jsil
 json
 langapi # should go away
 linking

diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt
@@ -23,8 +23,6 @@ target_link_libraries(goto-diff-lib
     solvers
 )
 
-add_if_library(goto-diff-lib jsil)
-
 # Executable
 add_executable(goto-diff goto_diff_main.cpp)
 target_link_libraries(goto-diff goto-diff-lib)

diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
@@ -43,7 +43,6 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
       symbol_pair.second.type.id() == ID_code &&
       (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
        symbol_pair.second.mode == ID_java ||
-       symbol_pair.second.mode == "jsil" ||
        symbol_pair.second.mode == ID_statement_list))
     {
       symbol_list.push_back(symbol_pair.first);

diff --git a/src/jsil/CMakeLists.txt b/src/jsil/CMakeLists.txt
diff --git a/src/jsil/Makefile b/src/jsil/Makefile
diff --git a/src/jsil/README.md b/src/jsil/README.md
diff --git a/src/jsil/expr2jsil.cpp b/src/jsil/expr2jsil.cpp
diff --git a/src/jsil/expr2jsil.h b/src/jsil/expr2jsil.h
-Original file line number
+Diff line change
@@ Expand Up / @@ -2,7 +2,6 @@ ansi-c @@
     cpp
     goto-cc
     goto-programs
-    jsil
     json
     langapi # should go away
     linking
@@ Expand Down @@