[src][sourcepath] remove .pp extension from sourcepath

As mentionned in f090928, there was a difference between the compilation
unit of a preprocessed file and the one of an unpreprocessed file.
Forcing them to have the same compilation unit by removing the `.pp`
extension works in most cases.
However, in the case of optional arguments, some computations relied on
finding whether a location belonged to the current or a previously
analyzed compilation unit or if it belongs to an unknown (potentially
analyzed later) compilation unit.
This property is checked in `DeadCommon.VdNode.seen` by verifying if the
location has a corresponding sourcepath in the `DeadCommon.abspath`
table. This table associates compilation units (as obtained by
`Utils.unit`) with sourcepaths (read in the `.cmi` and `.cmt` files) and
is filled when starting the analysis of either a `.cmi` or a `.cmt`.
Verifying that a location belongs to a known file is done by checking if
its filename is a suffix of one of the sourcepaths associated with its
compilation unit.
The sourcepath of a `.cmt` file may end with `.pp.ml`, while locaitons
found in the typedtree will not contain the `.pp` part. Therefore, the
inconsistency observed in f090928 still remains for sourcepaths.

Rather than removing the `.pp` extension in `Utils.unit`, it is directly
removed from the sourcepaths read in `.cmt` files. This ways,
compilation units are consistent and file paths read in locations are
also consisten with the sourcepaths.

With this change, I measured a gain of ~10s (from ~22s to ~12s) when
running the analyzer with `-v --all` on [Frama-C 31.0]
(https://git.frama-c.com/pub/frama-c/-/tree/31.0?ref_type=tags) on my
machine.

Author: fantazio

check/classic/classic.ref

@@ -243,13 +243,12 @@ Nothing else to report in this section
 .> OPTIONAL ARGUMENTS: ALWAYS:
 =============================
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?always
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?internally: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?internally
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:59: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:64: ?always
-./examples/using_dune/preprocessed_lib/preprocessed.ml:69: ?always: Should not be detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?always: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?externally: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?always: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?always
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?externally
+./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:59: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:64: ?always
@@ -388,15 +387,14 @@ Nothing else to report in this section
 
 .> OPTIONAL ARGUMENTS: NEVER:
 ============================
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?externally: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?externally
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:59: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:64: ?never
-./examples/using_dune/preprocessed_lib/preprocessed.ml:69: ?never: Should not be detected
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:84: ?opt
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?internally: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?never: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?never: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?internally
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?never
+./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:59: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:64: ?never
@@ -552,7 +550,7 @@ Nothing else to report in this section
 --------------------------------------------------------------------------------
 
 
-Total: 479
-Success: 469
-Failed: 10
-Ratio: 97.9123173278%
+Total: 477
+Success: 477
+Failed: 0
+Ratio: 100.%

check/internal/internal.ref

@@ -210,13 +210,12 @@ Nothing else to report in this section
 .> OPTIONAL ARGUMENTS: ALWAYS:
 =============================
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?always
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?internally: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?internally
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:59: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:64: ?always
-./examples/using_dune/preprocessed_lib/preprocessed.ml:69: ?always: Should not be detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?always: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?externally: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?always: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?always
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?externally
+./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:59: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:64: ?always
@@ -355,15 +354,14 @@ Nothing else to report in this section
 
 .> OPTIONAL ARGUMENTS: NEVER:
 ============================
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?externally: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?externally
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:59: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:64: ?never
-./examples/using_dune/preprocessed_lib/preprocessed.ml:69: ?never: Should not be detected
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:84: ?opt
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?internally: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?never: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?never: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?internally
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?never
+./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:59: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:64: ?never
@@ -519,7 +517,7 @@ Nothing else to report in this section
 --------------------------------------------------------------------------------
 
 
-Total: 448
-Success: 438
-Failed: 10
-Ratio: 97.7678571429%
+Total: 446
+Success: 446
+Failed: 0
+Ratio: 100.%

check/threshold-1/threshold-1.ref

@@ -518,13 +518,12 @@ Nothing else to report in this section
 .> OPTIONAL ARGUMENTS: ALWAYS:
 =============================
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?always
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?internally: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?internally
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:59: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:64: ?always
-./examples/using_dune/preprocessed_lib/preprocessed.ml:69: ?always: Should not be detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?always: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?externally: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?always: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?always
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?externally
+./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:59: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:64: ?always
@@ -663,15 +662,14 @@ Nothing else to report in this section
 
 .> OPTIONAL ARGUMENTS: NEVER:
 ============================
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?externally: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?externally
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:59: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:64: ?never
-./examples/using_dune/preprocessed_lib/preprocessed.ml:69: ?never: Should not be detected
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:84: ?opt
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?internally: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?never: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?never: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?internally
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?never
+./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:59: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:64: ?never
@@ -827,7 +825,7 @@ Nothing else to report in this section
 --------------------------------------------------------------------------------
 
 
-Total: 719
-Success: 709
-Failed: 10
-Ratio: 98.6091794159%
+Total: 717
+Success: 717
+Failed: 0
+Ratio: 100.%

check/threshold-3-0.5/threshold-3-0.5.ref

@@ -711,13 +711,12 @@ Nothing else to report in this section
 .> OPTIONAL ARGUMENTS: ALWAYS:
 =============================
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?always
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?internally: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?internally
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:59: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:64: ?always
-./examples/using_dune/preprocessed_lib/preprocessed.ml:69: ?always: Should not be detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?always: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?externally: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?always: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?always
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?externally
+./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:59: ?always
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:64: ?always
@@ -854,12 +853,9 @@ Nothing else to report in this section
 
 .>->  OPTIONAL ARGUMENTS: ALMOST ALWAYS: Except 1 time(s):
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?externally   (1/2 calls): Should not be detected
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?internally   (1/2 calls): Should not be detected
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:59: ?sometimes   (1/2 calls)
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:64: ?sometimes   (1/2 calls)
-./examples/using_dune/preprocessed_lib/preprocessed.ml:69: ?sometimes   (1/2 calls): Should not be detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?sometimes   (1/2 calls): Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?sometimes   (1/2 calls)
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?externally   (1/2 calls)
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?internally   (1/2 calls)
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:59: ?sometimes   (1/2 calls)
@@ -955,15 +951,14 @@ Nothing else to report in this section
 
 .> OPTIONAL ARGUMENTS: NEVER:
 ============================
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?externally: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?externally
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:59: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:64: ?never
-./examples/using_dune/preprocessed_lib/preprocessed.ml:69: ?never: Should not be detected
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:84: ?opt
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?internally: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?never: Not detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?never: Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?internally
+./examples/using_dune/preprocessed_lib/preprocessed.mli:31: ?never
+./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:59: ?never
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:64: ?never
@@ -1070,12 +1065,9 @@ Nothing else to report in this section
 
 .>->  OPTIONAL ARGUMENTS: ALMOST NEVER: Except 1 time(s):
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?externally   (1/2 calls): Should not be detected
-./examples/using_dune/preprocessed_lib/preprocessed.ml:53: ?internally   (1/2 calls): Should not be detected
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:59: ?sometimes   (1/2 calls)
 ./examples/using_dune/preprocessed_lib/preprocessed.ml:64: ?sometimes   (1/2 calls)
-./examples/using_dune/preprocessed_lib/preprocessed.ml:69: ?sometimes   (1/2 calls): Should not be detected
-./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?sometimes   (1/2 calls): Not detected
+./examples/using_dune/preprocessed_lib/preprocessed.mli:44: ?sometimes   (1/2 calls)
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?externally   (1/2 calls)
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:53: ?internally   (1/2 calls)
 ./examples/using_dune/preprocessed_lib/preprocessed_no_intf.ml:59: ?sometimes   (1/2 calls)
@@ -1202,7 +1194,7 @@ Nothing else to report in this section
 --------------------------------------------------------------------------------
 
 
-Total: 1022
-Success: 1004
-Failed: 18
-Ratio: 98.2387475538%
+Total: 1014
+Success: 1014
+Failed: 0
+Ratio: 100.%

src/state/file_infos.ml

@@ -23,7 +23,8 @@ let empty = {
 let init_from_cmt_infos cmt_infos cmt_file =
   let builddir = cmt_infos.Cmt_format.cmt_builddir in
   let sourcepath =
-    Option.map (Filename.concat builddir) cmt_infos.cmt_sourcefile
+    Option.map Utils.remove_pp cmt_infos.cmt_sourcefile
+    |> Option.map (Filename.concat builddir)
   in
   let modname = cmt_infos.cmt_modname in
   {empty with cmti_file = cmt_file;

src/utils.ml

@@ -1,6 +1,10 @@
+let remove_pp fn =
+  let ext = Filename.extension fn in
+  let no_ext = Filename.remove_extension fn in
+  match Filename.extension no_ext with
+  | ".pp" -> Filename.remove_extension no_ext ^ ext
+  | _ -> fn
+
 let unit fn =
-  let u = Filename.remove_extension (Filename.basename fn) in
-  match Filename.extension u with
-  | ".pp" -> Filename.remove_extension u
-  | _ -> u
+  Filename.remove_extension (Filename.basename fn)
 

src/utils.mli

@@ -1 +1,3 @@
+val remove_pp : string -> string
+
 val unit : string -> string