From 49d848e794e2997c63607b14da638d07d95ed6ea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 10 Jan 2025 11:30:31 +0100
Subject: [PATCH] [Eva] New parameter -eva-memory-footprint to configure the
ocaml gc.
---
src/plugins/eva/engine/analysis.ml | 17 +++++++++++------
src/plugins/eva/parameters.ml | 14 ++++++++++++++
src/plugins/eva/parameters.mli | 2 ++
3 files changed, 27 insertions(+), 6 deletions(-)
diff --git a/src/plugins/eva/engine/analysis.ml b/src/plugins/eva/engine/analysis.ml
index 3ba7dcb4234..5bf496db627 100644
--- a/src/plugins/eva/engine/analysis.ml
+++ b/src/plugins/eva/engine/analysis.ml
@@ -177,16 +177,21 @@ let () =
~user_only:true (fun _ -> reset_analyzer ());
Project.register_after_global_load_hook reset_analyzer
-let tune_gc () =
- if Sys.ocaml_release.major >= 5 then
- let minor_heap_size = 8192000 in
- let space_overhead = 40 in
- Gc.(set { (get ()) with minor_heap_size; space_overhead; })
+(* Configure the OCaml Garbage Collector according to the
+ -eva-memory-footprint parameter (only if it has been set). *)
+let configure_ocaml_gc () =
+ if Parameters.MemoryFootprint.is_set () then
+ let gc_control = Gc.get () in
+ let n = Parameters.MemoryFootprint.get () in
+ let values = [| 24; 30; 40; 60; 90; 120; 150; 190; 240; 300 |] in
+ let space_overhead = values.(n-1) in
+ if space_overhead <> gc_control.space_overhead then
+ Gc.set { gc_control with space_overhead }
(* Builds the analyzer if needed, and run the analysis. *)
let force_compute () =
+ configure_ocaml_gc ();
Ast.compute ();
- tune_gc ();
Parameters.configure_precision ();
if not (Kernel.AuditCheck.is_empty ()) then
Eva_audit.check_configuration (Kernel.AuditCheck.get ());
diff --git a/src/plugins/eva/parameters.ml b/src/plugins/eva/parameters.ml
index 620f41b7048..06b181cb86f 100644
--- a/src/plugins/eva/parameters.ml
+++ b/src/plugins/eva/parameters.ml
@@ -398,6 +398,20 @@ module JoinResults =
let default = true
end)
+let () = Parameter_customize.set_group performance
+module MemoryFootprint =
+ Int
+ (struct
+ let default = 6
+ let option_name = "-eva-memory-footprint"
+ let arg_name = "n"
+ let help =
+ "Control the memory usage of the analysis. \
+ With smaller values, the analysis consumes much less memory but is \
+ also slightly slower. Must be between 1 and 10; default is 6."
+ end)
+let () = MemoryFootprint.set_range ~min:1 ~max:10
+
(* ------------------------------------------------------------------------- *)
(* --- Non-standard alarms --- *)
(* ------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/parameters.mli b/src/plugins/eva/parameters.mli
index 90225279e44..ca654e78209 100644
--- a/src/plugins/eva/parameters.mli
+++ b/src/plugins/eva/parameters.mli
@@ -58,6 +58,8 @@ module ResultsAll: Parameter_sig.Bool
module JoinResults: Parameter_sig.Bool
+module MemoryFootprint: Parameter_sig.Int
+
module WarnSignedConvertedDowncast: Parameter_sig.Bool
module WarnPointerSubstraction: Parameter_sig.Bool
module WarnCopyIndeterminate: Parameter_sig.Kernel_function_set
--
GitLab