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

fantazio · fantazio · commit c3c458788914 · 2026-01-23T13:07:15.000+01:00
Rather than removing the `.pp` extension in `Utils.unit`, it is directly removed from the sourcepaths read in `.cmt` files. This way, compilation units remain consistent; and file paths read in locations are now also consistent with the sourcepaths. More details on why this fixes the observed FN and FP below. 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. This is coherent with the few computations of the cmts' sourcepaths (once per `.cmt` read) vs the amount of time the compilation unit is computed (on every potentially meaningful location). 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 is sufficient in most cases. However, in the case of optional arguments, some computations relied on finding whether a location belongs to the current or a previously analyzed sourcefile, or if it belongs to an unknown (potentially analyzed later) sourcefile. In particular, `VdNode.eof` relies on this to discard "internal" locations and, thus, dissociate them from their corresponding "external" locations. 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. Because of this inconsistency, the internal and external locations are not dissociated at the end of the analysis of a `.cmt`, leading to the observed FN and FP.
diff --git a/check/classic/classic.ref b/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.%
diff --git a/check/internal/internal.ref b/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.%
diff --git a/check/threshold-1/threshold-1.ref b/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.%
diff --git a/check/threshold-3-0.5/threshold-3-0.5.ref b/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.%
diff --git a/src/state/file_infos.ml b/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;
diff --git a/src/utils.ml b/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)
 
diff --git a/src/utils.mli b/src/utils.mli
@@ -1 +1,3 @@
+val remove_pp : string -> string
+
 val unit : string -> string

Original file line number	Diff line number	Diff line change
`@@ -1 +1,3 @@`
	`1`	`+val remove_pp : string -> string`
	`2`	`+`
`1`	`3`	`val unit : string -> string`