From 3c04c325e4b43680e4a7b40a233e7e31dd78a29f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 23 Jul 2021 17:22:30 +0200
Subject: [PATCH] POC for autodetection and task printing
---
caisar.opam | 2 ++
config/dune | 4 ++++
config/provers_autodetection.conf | 12 ++++++++++++
dune-project | 4 +++-
src/detection.ml | 24 ++++++++++++++++++++++++
src/prove.ml | 17 ++++++++++++-----
6 files changed, 57 insertions(+), 6 deletions(-)
create mode 100644 config/dune
create mode 100644 config/provers_autodetection.conf
create mode 100644 src/detection.ml
diff --git a/caisar.opam b/caisar.opam
index 6f7f353f..7c53587d 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -5,6 +5,8 @@ synopsis: "Framework for neural network verification"
depends: [
"ocaml" {>= "4.10"}
"dune" {>= "2.9" & >= "2.9.0"}
+ "dune-site" {>= "2.9.0"}
+ "why3"
"base" {>= "v0.14.0"}
"cmdliner" {>= "1.0.4"}
"fmt" {>= "0.8.9"}
diff --git a/config/dune b/config/dune
new file mode 100644
index 00000000..1aabdf75
--- /dev/null
+++ b/config/dune
@@ -0,0 +1,4 @@
+(install
+ (section (site (caisar config)))
+ (files provers_autodetection.conf)
+(package caisar))
diff --git a/config/provers_autodetection.conf b/config/provers_autodetection.conf
new file mode 100644
index 00000000..688a4de8
--- /dev/null
+++ b/config/provers_autodetection.conf
@@ -0,0 +1,12 @@
+[ATP alt-ergo]
+name = "Alt-Ergo"
+exec = "alt-ergo"
+exec = "alt-ergo-2.4.0"
+version_switch = "--version"
+version_regexp = "^\\([0-9.]+\\)$"
+version_ok = "2.4.0"
+command = "%e --timelimit %t %f"
+command_steps = "%e --steps-bound %S %f"
+driver = "alt_ergo"
+editor = "altgr-ergo"
+use_at_auto_level = 1
diff --git a/dune-project b/dune-project
index e4049ba8..610e405c 100644
--- a/dune-project
+++ b/dune-project
@@ -15,6 +15,8 @@
(depends
(ocaml (>= 4.10))
(dune (>= 2.9.0))
+ (dune-site (>= 2.9.0))
+ why3
(base (>= v0.14.0))
(cmdliner (>= 1.0.4))
(fmt (>= 0.8.9))
@@ -25,7 +27,7 @@
(ppx_deriving_yojson (>= 3.6.1))
(csv (>= 2.4))
)
- (sites (lib stdlib))
+ (sites (share stdlib)(share config))
)
(package
diff --git a/src/detection.ml b/src/detection.ml
new file mode 100644
index 00000000..ed15cdc1
--- /dev/null
+++ b/src/detection.ml
@@ -0,0 +1,24 @@
+open Base
+module Sys = Caml.Sys
+
+let null = if Sys.unix then "/dev/null" else "NUL"
+
+let rec lookup_file l f =
+ match l with
+ | [] -> raise Caml.Not_found
+ | a :: l ->
+ let abs = Caml.Filename.concat a f in
+ if Sys.file_exists abs then abs else lookup_file l f
+
+let detect () =
+ Why3.Debug.set_flag Why3.Autodetection.debug;
+ let caisar_autodetection =
+ lookup_file Stdlib_path.Sites.config "provers_autodetection.conf"
+ in
+ let data =
+ Why3.Autodetection.Prover_autodetection_data.from_file caisar_autodetection
+ in
+ let config = Why3.Whyconf.init_config (Some null) in
+ let binaries = Why3.Autodetection.request_binaries_version config data in
+ let provers = Why3.Autodetection.compute_builtin_prover binaries data in
+ Why3.Whyconf.set_provers config provers
diff --git a/src/prove.ml b/src/prove.ml
index cc59ea6c..bdddcae4 100644
--- a/src/prove.ml
+++ b/src/prove.ml
@@ -3,13 +3,16 @@ open Base
let () = Language.register ()
let create_env loadpath =
+ let conf = Detection.detect () in
let stdlib = Stdlib_path.Sites.stdlib in
- let conf = Why3.Whyconf.init_config None in
- Why3.Env.create_env
- (loadpath @ stdlib @ Why3.Whyconf.loadpath (Why3.Whyconf.get_main conf))
+ ( Why3.Env.create_env
+ (loadpath @ stdlib @ Why3.Whyconf.loadpath (Why3.Whyconf.get_main conf)),
+ conf )
+
+let altergo = Why3.Whyconf.mk_filter_prover "Alt-Ergo"
let prove format loadpath file =
- let env = create_env loadpath in
+ let env, config = create_env loadpath in
let _, m =
match file with
| "-" ->
@@ -25,5 +28,9 @@ let prove format loadpath file =
Why3.Wstdlib.Mstr.iter
(fun _ th ->
let l = Why3.Task.split_theory th None None in
- List.iter l ~f:(Fmt.pr "%a" Why3.Pretty.print_task))
+ let prover = Why3.Whyconf.filter_one_prover config altergo in
+ let driver =
+ Why3.Whyconf.load_driver (Why3.Whyconf.get_main config) env prover
+ in
+ List.iter l ~f:(Fmt.pr "%a" (Why3.Driver.print_task driver)))
m
--
GitLab