From 208f034530d51c9eceae9fd1d0b1aec8b9568745 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 9 Mar 2023 10:38:45 +0100
Subject: [PATCH] Several updates following the new Why3 (version 1.6.0) API
changes.
Fix issue #26.
---
.ocamlformat | 2 +-
caisar.opam | 2 +-
dune-project | 2 +-
src/AIMOS.ml | 6 ++----
src/SAVer.ml | 6 ++----
src/verification.ml | 23 +++++++++++++----------
6 files changed, 20 insertions(+), 21 deletions(-)
diff --git a/.ocamlformat b/.ocamlformat
index f4273f4..f99ed8e 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,4 +1,4 @@
-version=0.23.0
+version=0.25.1
exp-grouping=parens
if-then-else=keyword-first
max-indent=2
diff --git a/caisar.opam b/caisar.opam
index 1057e0b..6747b51 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -29,7 +29,7 @@ depends: [
"menhirLib" {>= "20210310"}
"ppx_deriving_yojson" {>= "3.6.1"}
"csv" {>= "2.4"}
- "why3" {= "1.5.1"}
+ "why3" {>= "1.6.0"}
"re" {>= "1.10.4"}
"caisar-nnet" {= version}
"caisar-ovo" {= version}
diff --git a/dune-project b/dune-project
index e72f7f9..1776737 100644
--- a/dune-project
+++ b/dune-project
@@ -82,7 +82,7 @@
(menhirLib (>= 20210310))
(ppx_deriving_yojson (>= 3.6.1))
(csv (>= 2.4))
- (why3 (= 1.5.1))
+ (why3 (>= 1.6.0))
(re (>= 1.10.4))
(caisar-nnet (= :version))
(caisar-ovo (= :version))
diff --git a/src/AIMOS.ml b/src/AIMOS.ml
index 1588dd3..50d2caf 100644
--- a/src/AIMOS.ml
+++ b/src/AIMOS.ml
@@ -74,10 +74,8 @@ let call_prover limit config config_prover
prp_model_parser = Model_parser.lookup_model_parser "no_model";
}
in
- Call_provers.call_on_buffer ~libdir:(Whyconf.libdir config)
- ~datadir:(Whyconf.datadir config) ~command ~limit ~res_parser
- ~filename:" " ~get_counterexmp:false ~gen_new_file:false
- ~printing_info:Printer.default_printing_info (Buffer.create 10)
+ Call_provers.call_on_buffer ~command ~config ~limit ~res_parser
+ ~filename:" " ~get_model:None ~gen_new_file:false (Buffer.create 10)
in
let prover_result = Call_provers.wait_on_call prover_call in
build_answer predicate.property prover_result
diff --git a/src/SAVer.ml b/src/SAVer.ml
index 40511c6..c86a8b1 100644
--- a/src/SAVer.ml
+++ b/src/SAVer.ml
@@ -131,10 +131,8 @@ let call_prover limit config config_prover predicate =
prp_model_parser = Model_parser.lookup_model_parser "no_model";
}
in
- Call_provers.call_on_buffer ~libdir:(Whyconf.libdir config)
- ~datadir:(Whyconf.datadir config) ~command ~limit ~res_parser
- ~filename:" " ~get_counterexmp:false ~gen_new_file:false
- ~printing_info:Printer.default_printing_info (Buffer.create 10)
+ Call_provers.call_on_buffer ~command ~config ~limit ~res_parser
+ ~filename:" " ~get_model:None ~gen_new_file:false (Buffer.create 10)
in
let prover_result = Call_provers.wait_on_call prover_call in
build_answer predicate.property prover_result
diff --git a/src/verification.ml b/src/verification.ml
index 1f9a37d..8fe43e4 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -78,7 +78,7 @@ let create_env ?(debug = false) loadpath =
let config = Autodetect.autodetection ~debug () in
let config =
let main = Whyconf.get_main config in
- let dft_timelimit = 20 (* 20 seconds *) in
+ let dft_timelimit = 20.0 (* 20 seconds *) in
let dft_memlimit = 4000 (* 4 GB *) in
let main =
Whyconf.(
@@ -163,8 +163,7 @@ let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
let call_prover_on_task limit config command driver task =
let prover_call =
- Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)
- ~datadir:(Whyconf.datadir config) ~command ~limit driver task
+ Driver.prove_task_prepared ~command ~config ~limit driver task
in
let prover_result = Call_provers.wait_on_call prover_call in
prover_result.pr_answer
@@ -282,7 +281,10 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
let main = Whyconf.get_main config in
let limit =
let memlimit = Option.value memlimit ~default:(Whyconf.memlimit main) in
- let timelimit = Option.value timelimit ~default:(Whyconf.timelimit main) in
+ let timelimit =
+ Option.value_map timelimit ~f:Float.of_int
+ ~default:(Whyconf.timelimit main)
+ in
let def = Call_provers.empty_limit in
{
Call_provers.limit_time = timelimit;
@@ -318,27 +320,28 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
invalid_arg
(Fmt.str "No prover corresponds to %s%a" prover
(if String.equal altern ""
- then Fmt.nop
- else Fmt.(any " " ++ parens string))
+ then Fmt.nop
+ else Fmt.(any " " ++ parens string))
altern)
| Whyconf.ProverAmbiguity _ ->
invalid_arg
(Fmt.str "More than one prover correspond to %s%a" prover
(if String.equal altern ""
- then Fmt.nop
- else Fmt.(any " " ++ parens string))
+ then Fmt.nop
+ else Fmt.(any " " ++ parens string))
altern)
in
let driver =
match String.chop_prefix ~prefix:"caisar_drivers/" config_prover.driver with
- | None -> Whyconf.(load_driver (get_main config) env config_prover)
+ | None -> Driver.load_driver_for_prover main env config_prover
| Some file ->
let file =
Filename.concat
(Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
file
in
- Driver.load_driver_absolute env file config_prover.extra_drivers
+ Driver.load_driver_file_and_extras main env file
+ config_prover.extra_drivers
in
Wstdlib.Mstr.map
(fun theory ->
--
GitLab