[Doli] Removing the Doli project

Summary:
The purpose of this project was to enable writing models in textual form.

The first part involves defining function signatures to intercept function call, following the syntax of the source language.
We are removing this first part here, as it is not in use and not fully completed. Instead, we can continue using
the DSL in ProcnameDispatcher.mli.

The second part of the Doli project is about writing body of models in textual form. It carries on in the Textual
project.

  viking_goodbye

Reviewed By: geralt-encore

Differential Revision:
D49537532

Privacy Context Container: L1208441

fbshipit-source-id: 0b2f3336b7e53aaa52b134b174de933cb65e0b93

Makefile

@@ -247,10 +247,6 @@ DIRECT_TESTS += \
   java_starvation-dedup \
   java_starvation-whole-program \
   java_topl \
-  sil_doli-capture  \
-  sil_doli-parsing \
-  sil_java-and-doli \
-  sil_sil-and-doli \
   sil_pulse \
   sil_verif \
 

infer/man/man1/infer-full.txt

@@ -2107,13 +2107,6 @@ INTERNAL OPTIONS
            Deactivates: capture and translate source files into infer's
            intermediate language for analysis (Conversely: --capture)
 
-       --capture-doli +path
-           Generate a SIL program from doli representations given in .doli
-           files.
-
-       --capture-doli-reset
-           Set --capture-doli to the empty list.
-
        --capture-textual +path
            Generate a SIL program from a textual representation given in .sil
            files.
@@ -2640,13 +2633,6 @@ INTERNAL OPTIONS
        --oom-threshold-reset
            Cancel the effect of --oom-threshold.
 
-       --parse-doli path
-           Perform parsing on given a .doli file -- no checks on textual, no
-           capture.
-
-       --parse-doli-reset
-           Cancel the effect of --parse-doli.
-
        --print-buckets
            Activates: Show the internal bucket of Infer reports in their
            textual description (Conversely: --no-print-buckets)

infer/src/base/Config.ml

@@ -995,11 +995,6 @@ and capture_block_list =
        analyzed either. Clang and Java only." )
 
 
-and capture_doli =
-  CLOpt.mk_path_list ~long:"capture-doli" ~meta:"path"
-    "Generate a SIL program from doli representations given in .doli files."
-
-
 and capture_textual =
   CLOpt.mk_path_list ~long:"capture-textual" ~meta:"path"
     "Generate a SIL program from a textual representation given in .sil files."
@@ -2148,11 +2143,6 @@ and oom_threshold =
      Only for use on Linux."
 
 
-and parse_doli =
-  CLOpt.mk_path_opt ~long:"parse-doli" ~meta:"path"
-    "Perform parsing on given a .doli file -- no checks on textual, no capture."
-
-
 and pmd_xml =
   CLOpt.mk_bool ~long:"pmd-xml"
     ~in_help:InferCommand.[(Run, manual_generic)]
@@ -3760,8 +3750,6 @@ and capture = !capture
 
 and capture_block_list = match capture_block_list with k, r -> (k, !r)
 
-and capture_doli = RevList.to_list !capture_doli
-
 and capture_textual = RevList.to_list !capture_textual
 
 and censor_report =
@@ -4114,8 +4102,6 @@ and oom_threshold = !oom_threshold
 
 and only_cheap_debug = !only_cheap_debug
 
-and parse_doli = !parse_doli
-
 and pmd_xml = !pmd_xml
 
 and preanalysis_html = !preanalysis_html

infer/src/base/Config.mli

@@ -238,8 +238,6 @@ val capture : bool
 
 val capture_block_list : string * Yojson.Basic.t
 
-val capture_doli : string list
-
 val capture_textual : string list
 
 val censor_report : ((bool * Str.regexp) * (bool * Str.regexp) * string) list
@@ -539,8 +537,6 @@ val oom_threshold : int option
 
 val only_cheap_debug : bool
 
-val parse_doli : string option
-
 val pmd_xml : bool
 
 val preanalysis_html : bool

infer/src/infer.ml

@@ -151,8 +151,6 @@ let () =
       if Config.java_source_parser_experimental then
         JSourceLocations.debug_on_file (Option.value_exn Config.java_debug_source_file_info)
       else JSourceFileInfo.debug_on_file (Option.value_exn Config.java_debug_source_file_info)
-  | _ when Option.is_some Config.parse_doli ->
-      DoliParser.just_parse (Option.value_exn Config.parse_doli)
   | Analyze ->
       run Driver.Analyze
   | Capture | Compile | Run ->

infer/src/integration/Driver.ml

@@ -152,15 +152,6 @@ let capture ~changed_files mode =
       |> Out_channel.write_lines infer_deps_file ;
       () )
     else
-      let dolifiles = Config.capture_doli in
-      ( match dolifiles with
-      | [] ->
-          ()
-      | _ :: _ ->
-          let dfiles =
-            List.map dolifiles ~f:(fun x -> TextualParser.TextualFile.StandaloneFile x)
-          in
-          TextualParser.capture ~capture:DoliCapture dfiles ) ;
       match mode with
       | Analyze ->
           ()
@@ -237,10 +228,8 @@ let capture ~changed_files mode =
           L.progress "Capturing in hackc mode...@." ;
           Hack.capture ~prog ~args
       | Textual {textualfiles} ->
-          let tfiles =
-            List.map textualfiles ~f:(fun x -> TextualParser.TextualFile.StandaloneFile x)
-          in
-          TextualParser.capture ~capture:TextualCapture tfiles
+          List.map textualfiles ~f:(fun x -> TextualParser.TextualFile.StandaloneFile x)
+          |> TextualParser.capture
       | XcodeBuild {prog; args} ->
           L.progress "Capturing in xcodebuild mode...@." ;
           XcodeBuild.capture ~prog ~args

infer/src/pulse/Pulse.ml

@@ -514,10 +514,7 @@ module PulseTransferFunctions = struct
     else proc_name_opt
 
 
-  type model_search_result =
-    | DoliModel of Procname.t
-    | OcamlModel of (PulseModelsImport.model * Procname.t)
-    | NoModel
+  type model_search_result = OcamlModel of (PulseModelsImport.model * Procname.t) | NoModel
 
   (* When Hack traits are involved, we need to compute and pass an additional argument that is a
      token to find the right class name for [self].
@@ -787,14 +784,9 @@ module PulseTransferFunctions = struct
     in
     let model =
       match callee_pname with
-      | Some callee_pname -> (
-        match DoliToTextual.matcher callee_pname with
-        | Some procname ->
-            DoliModel procname
-        | None ->
-            PulseModels.dispatch tenv callee_pname func_args
-            |> Option.value_map ~default:NoModel ~f:(fun model -> OcamlModel (model, callee_pname))
-        )
+      | Some callee_pname ->
+          PulseModels.dispatch tenv callee_pname func_args
+          |> Option.value_map ~default:NoModel ~f:(fun model -> OcamlModel (model, callee_pname))
       | None ->
           (* unresolved function pointer, etc.: skip *)
           NoModel
@@ -820,15 +812,6 @@ module PulseTransferFunctions = struct
               ; ret }
               astate
           , `KnownCall )
-      | DoliModel callee_pname ->
-          L.d_printfln "Found doli model %a for call@\n" Procname.pp callee_pname ;
-          PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
-          let r =
-            interprocedural_call analysis_data path ret (Some callee_pname) call_exp func_args
-              call_loc flags astate
-          in
-          PerfEvent.(log (fun logger -> log_end_event logger ())) ;
-          r
       | NoModel ->
           PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
           let r =