From 624fd757de6753d778daaf482c4833ae88db5b16 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 9 Sep 2024 17:00:12 +0200
Subject: [PATCH] [wp] -wp-par defaults to number of logical cores
---
src/plugins/wp/cores.c | 45 +++++++++++++++++++++++++++++++++
src/plugins/wp/dune | 1 +
src/plugins/wp/wp_parameters.ml | 4 ++-
3 files changed, 49 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/wp/cores.c
diff --git a/src/plugins/wp/cores.c b/src/plugins/wp/cores.c
new file mode 100644
index 00000000000..2a4d0e6c995
--- /dev/null
+++ b/src/plugins/wp/cores.c
@@ -0,0 +1,45 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2024 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include <caml/memory.h>
+#include <caml/mlvalues.h>
+
+#ifdef _WIN32
+#include <windows.h>
+#else
+#include <unistd.h>
+#endif
+
+int cores(void) {
+#ifdef WIN32
+ SYSTEM_INFO sysinfo;
+ GetSystemInfo(&sysinfo);
+ return sysinfo.dwNumberOfProcessors;
+#else
+ return sysconf(_SC_NPROCESSORS_CONF);
+#endif
+}
+
+CAMLprim value caml_cores(value unit) {
+ CAMLparam1(unit);
+ CAMLreturn(Val_int(cores()));
+}
diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune
index 763e5af8cbc..6f393270237 100644
--- a/src/plugins/wp/dune
+++ b/src/plugins/wp/dune
@@ -44,6 +44,7 @@
(select wp_eva.ml from
(frama-c-eva.core -> wp_eva.enabled.ml)
( -> wp_eva.disabled.ml)))
+ (foreign_stubs (language c) (names cores))
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx)))
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 9268c9e87a8..efb064a639d 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -885,12 +885,14 @@ module TimeMargin =
(default: %s)." default
end)
+external cores : unit -> int = "caml_cores"
+
let () = Parameter_customize.set_group wp_prover
module Procs =
Int(struct
let option_name = "-wp-par"
let arg_name = "p"
- let default = 4
+ let default = cores ()
let help =
Printf.sprintf
"Number of parallel proof process (default: %d)" default
--
GitLab