[datalog] removing project

Summary: this project has not been used for a while. No plans to use it in the future. Some external users who do not use the Java frontend complain also about this (mandatory) project. Let's delete everything. Reviewed By: geralt-encore Differential Revision: D59227747 fbshipit-source-id: 09fe92b3b1d16bf9ef62b6fb18ec834502b01e24
matt-j-griffin · Jul 3, 2024 · e02b2ac · e02b2ac
1 parent a883163
commit e02b2ac
Show file tree

Hide file tree

Showing 55 changed files with 10 additions and 3,040 deletions.
diff --git a/.gitignore b/.gitignore
@@ -62,7 +62,6 @@ duplicates.txt
 /infer/tests/codetoanalyze/erlang/**/_build
 infer/tests/codetoanalyze/objcpp/fb-pulse/*.mm
 infer/tests/codetoanalyze/objcpp/fb-pulse/issues.exp
-/infer/src/datalog/**/_build
 /_release
 /infer-source
 META-INF
@@ -153,7 +152,6 @@ buck-out/
 /infer/lib/specs/clean_models
 /infer/etc/clang_ast.dict
 /infer/src/toplevel.mlpack
-/infer/src/datalog/**/*.jar
 
 /external_repo
 

diff --git a/Makefile b/Makefile
@@ -244,7 +244,6 @@ DIRECT_TESTS += \
   java_biabduction \
   java_bufferoverrun \
   java_checkers \
-  java_datalog \
   java_dependencies \
   java_hoisting \
   java_hoistingExpensive \

diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt
@@ -83,14 +83,6 @@ OPTIONS
            Deactivates: Suppress printing function pointers in cost reports
            (Conversely: --cost-suppress-func-ptr)
 
-       --datalog
-           Activates: datalog checker: Experimental datalog-based points-to
-           analysis. (Conversely: --no-datalog)
-
-       --datalog-only
-           Activates: Enable datalog and disable all other checkers
-           (Conversely: --no-datalog-only)
-
        --debug,-g
            Activates: Debug mode (also sets --debug-level 2,
            --developer-mode, --print-buckets, --print-types,

diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt
@@ -484,16 +484,6 @@ OPTIONS
            without being reported as dead stores.
            See also infer-analyze(1).
 
-       --datalog
-           Activates: datalog checker: Experimental datalog-based points-to
-           analysis. (Conversely: --no-datalog)
-           See also infer-analyze(1).
-
-       --datalog-only
-           Activates: Enable datalog and disable all other checkers
-           (Conversely: --no-datalog-only)
-           See also infer-analyze(1).
-
        --debug,-g
            Activates: Debug mode (also sets --debug-level 2,
            --developer-mode, --print-buckets, --print-types,
@@ -625,7 +615,6 @@ OPTIONS
              Cannot_star (enabled by default),
              DANGLING_POINTER_DEREFERENCE (disabled by default),
              DANGLING_POINTER_DEREFERENCE_MAYBE (disabled by default),
-             DATALOG_FACT (enabled by default),
              DATA_FLOW_TO_SINK (disabled by default),
              DEADLOCK (enabled by default),
              DEAD_STORE (enabled by default),
@@ -2841,10 +2830,6 @@ INTERNAL OPTIONS
        --java-jar-compiler-reset
            Cancel the effect of --java-jar-compiler.
 
-       --java-reflection
-           Activates: Print usages of reflection in the log. (Conversely:
-           --no-java-reflection)
-
        --java-source-parser-experimental
            Activates: The experimental Java source parser for declaration
            locations. (Conversely: --no-java-source-parser-experimental)

diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt
@@ -145,7 +145,6 @@ OPTIONS
              Cannot_star (enabled by default),
              DANGLING_POINTER_DEREFERENCE (disabled by default),
              DANGLING_POINTER_DEREFERENCE_MAYBE (disabled by default),
-             DATALOG_FACT (enabled by default),
              DATA_FLOW_TO_SINK (disabled by default),
              DEADLOCK (enabled by default),
              DEAD_STORE (enabled by default),

diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt
@@ -484,16 +484,6 @@ OPTIONS
            without being reported as dead stores.
            See also infer-analyze(1).
 
-       --datalog
-           Activates: datalog checker: Experimental datalog-based points-to
-           analysis. (Conversely: --no-datalog)
-           See also infer-analyze(1).
-
-       --datalog-only
-           Activates: Enable datalog and disable all other checkers
-           (Conversely: --no-datalog-only)
-           See also infer-analyze(1).
-
        --debug,-g
            Activates: Debug mode (also sets --debug-level 2,
            --developer-mode, --print-buckets, --print-types,
@@ -625,7 +615,6 @@ OPTIONS
              Cannot_star (enabled by default),
              DANGLING_POINTER_DEREFERENCE (disabled by default),
              DANGLING_POINTER_DEREFERENCE_MAYBE (disabled by default),
-             DATALOG_FACT (enabled by default),
              DATA_FLOW_TO_SINK (disabled by default),
              DEADLOCK (enabled by default),
              DEAD_STORE (enabled by default),

diff --git a/infer/src/IR/Procname.ml b/infer/src/IR/Procname.ml
@@ -734,14 +734,6 @@ let is_java t = match t with Java _ -> true | _ -> false
 
 let is_python t = match t with Python _ -> true | _ -> false
 
-let as_java_exn ~explanation t =
-  match t with
-  | Java java ->
-      java
-  | _ ->
-      Logging.die InternalError "Expected Java procname: %s" explanation
-
-
 (* TODO: deprecate this unfortunately named function and use is_clang instead *)
 let is_c_method t = match t with ObjC_Cpp _ -> true | _ -> false
 

diff --git a/infer/src/IR/Procname.mli b/infer/src/IR/Procname.mli
@@ -376,9 +376,6 @@ val is_java : t -> bool
 val is_python : t -> bool
 (** Check if this is a Python procedure name. *)
 
-val as_java_exn : explanation:string -> t -> Java.t
-(** Converts to a Java.t. Throws if [is_java] is false *)
-
 val objc_cpp_replace_method_name : t -> string -> t
 
 val is_infer_undefined : t -> bool

diff --git a/infer/src/Makefile b/infer/src/Makefile
@@ -154,7 +154,7 @@ $(INFER_BIN_ALIASES): Makefile $(BIN_DIR)/$(INFER_MAIN)
 	$(QUIET)touch $@
 
 roots:=Infer
-clusters:=absint al atd backend base biabduction bufferoverrun checkers clang clang_stubs concurrency cost c_stubs datalog deadcode integration IR istd java labs dotnet llvm opensource pulse python scripts test_determinator topl unit
+clusters:=absint al atd backend base biabduction bufferoverrun checkers clang clang_stubs concurrency cost c_stubs deadcode integration IR istd java labs dotnet llvm opensource pulse python scripts test_determinator topl unit
 
 ml_src_files:=$(shell find . -not -path "./*stubs*" -regex '\./[a-zA-Z].*\.ml\(i\)*')
 inc_flags:=$(foreach dir,$(shell find . -not -path './_build*' -type d),-I $(dir))

diff --git a/infer/src/backend/dune b/infer/src/backend/dune
@@ -41,9 +41,7 @@
    -open
    Concurrency
    -open
-   Labs
-   -open
-   Datalog))
+   Labs))
  (libraries
   core
   memtrace
@@ -60,7 +58,6 @@
   Topllib
   Concurrency
   Labs
-  Datalog
   Textuallib)
  (preprocess
   (pps ppx_compare ppx_fields_conv ppx_hash ppx_yojson_conv)))

diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml
@@ -179,10 +179,6 @@ let all_checkers =
          ; (pulse, Java)
          ; (pulse, CIL)
          ; (pulse, Python) ] ) }
-  ; { checker= Datalog
-    ; callbacks=
-        (let datalog = intraprocedural DatalogAnalysis.checker in
-         [(datalog, Java)] ) }
   ; { checker= Impurity
     ; callbacks=
         (let impurity =

diff --git a/infer/src/backend/tests/dune b/infer/src/backend/tests/dune
@@ -43,8 +43,6 @@
    -open
    Labs
    -open
-   Datalog
-   -open
    Backend))
  (libraries
   fmt
@@ -64,7 +62,6 @@
   Topllib
   Concurrency
   Labs
-  Datalog
   Textuallib)
  (preprocess
   (pps ppx_expect)))
diff --git a/infer/src/base/Checker.ml b/infer/src/base/Checker.ml
@@ -16,7 +16,6 @@ type t =
   | BufferOverrunChecker
   | ConfigImpactAnalysis
   | Cost
-  | Datalog
   | DisjunctiveDemo
   | FragmentRetainsView
   | Impurity
@@ -166,14 +165,6 @@ let config_unsafe checker =
       ; cli_flags= Some {deprecated= []; show_in_help= true}
       ; enabled_by_default= false
       ; activates= [BufferOverrunAnalysis; PurityAnalysis] }
-  | Datalog ->
-      { id= "datalog"
-      ; kind= UserFacing {title= "Datalog-based points-to analysis"; markdown_body= ""}
-      ; support= mk_support_func ~java:ExperimentalSupport ()
-      ; short_documentation= "Experimental datalog-based points-to analysis."
-      ; cli_flags= Some {deprecated= []; show_in_help= true}
-      ; enabled_by_default= false
-      ; activates= [] }
   | DisjunctiveDemo ->
       { id= "disjunctive-demo"
       ; kind= Internal

diff --git a/infer/src/base/Checker.mli b/infer/src/base/Checker.mli
@@ -15,7 +15,6 @@ type t =
   | BufferOverrunChecker
   | ConfigImpactAnalysis
   | Cost
-  | Datalog
   | DisjunctiveDemo
   | FragmentRetainsView
   | Impurity

diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
@@ -1956,8 +1956,6 @@ and java_jar_compiler =
     ~meta:"path" "Specify the Java compiler jar used to generate the bytecode"
 
 
-and java_reflection = CLOpt.mk_bool ~long:"java-reflection" "Print usages of reflection in the log."
-
 and java_source_parser_experimental =
   CLOpt.mk_bool ~long:"java-source-parser-experimental"
     "The experimental Java source parser for declaration locations."
@@ -4282,8 +4280,6 @@ and java_debug_source_file_info = !java_debug_source_file_info
 
 and java_jar_compiler = !java_jar_compiler
 
-and java_reflection = !java_reflection
-
 and java_source_parser_experimental = !java_source_parser_experimental
 
 and java_version = !java_version

diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
@@ -460,8 +460,6 @@ val java_debug_source_file_info : string option
 
 val java_jar_compiler : string option
 
-val java_reflection : bool
-
 val java_source_parser_experimental : bool
 
 val java_version : int option

diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml
@@ -892,11 +892,6 @@ let data_flow_to_sink =
     ~user_documentation:"A flow of data was detected to a sink."
 
 
-let datalog_fact =
-  register ~category:NoCategory ~id:"DATALOG_FACT" Info Datalog
-    ~user_documentation:"Datalog fact used as input for a datalog solver."
-
-
 let regex_op_on_ui_thread =
   register ~category:PerfRegression Warning ~id:"REGEX_OP_ON_UI_THREAD" Starvation
     ~user_documentation:

diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli
@@ -177,8 +177,6 @@ val dangling_pointer_dereference_maybe : t
 
 val data_flow_to_sink : t
 
-val datalog_fact : t
-
 val dead_store : t
 
 val deadlock : t

diff --git a/infer/src/base/ResultsDirEntryName.ml b/infer/src/base/ResultsDirEntryName.ml
@@ -26,7 +26,6 @@ type id =
   | CaptureDependencies
   | ChangedFunctions
   | ChangedFunctionsTempResults
-  | DatalogFacts
   | DBWriterSocket
   | Debug
   | Differential
@@ -178,12 +177,6 @@ let of_id = function
       ; before_incremental_analysis= Keep
       ; before_caching_capture= Delete
       ; before_new_capture= Delete }
-  | DatalogFacts ->
-      { rel_path= "facts"
-      ; kind= Directory
-      ; before_incremental_analysis= Delete
-      ; before_caching_capture= Delete
-      ; before_new_capture= Delete }
   | GlobalTypeEnvironment ->
       { rel_path= ".global.tenv"
       ; kind= File

diff --git a/infer/src/base/ResultsDirEntryName.mli b/infer/src/base/ResultsDirEntryName.mli
@@ -27,7 +27,6 @@ type id =
   | CaptureDependencies  (** list of infer-out/ directories that contain capture artefacts *)
   | ChangedFunctions  (** results of the clang test determinator *)
   | ChangedFunctionsTempResults  (** a directory for temporary [ChangedFunctions] files *)
-  | DatalogFacts  (** directory for datalog facts *)
   | DBWriterSocket  (** socket to the DBWriter process for serializing writes to SQLite *)
   | Debug  (** directory containing debug data *)
   | Differential  (** contains the results of [infer reportdiff] *)

diff --git a/infer/src/datalog/Analysis.dl b/infer/src/datalog/Analysis.dl