From 325b950ba6ec476da01112514514575d55eae23a Mon Sep 17 00:00:00 2001
From: Aymeric Varasse <aymeric.varasse@cea.fr>
Date: Wed, 6 Apr 2022 18:23:19 +0200
Subject: [PATCH] [aimos] Add AIMOS as a prover and basic answer_aimos.
---
src/AIMOS.ml | 83 +++++++++++++++++++++++++++++++++++++++++++++
src/AIMOS.mli | 31 +++++++++++++++++
src/prover.ml | 7 ++--
src/prover.mli | 1 +
src/verification.ml | 37 ++++++++++++++++++++
5 files changed, 157 insertions(+), 2 deletions(-)
create mode 100644 src/AIMOS.ml
create mode 100644 src/AIMOS.mli
diff --git a/src/AIMOS.ml b/src/AIMOS.ml
new file mode 100644
index 0000000..f4e0c73
--- /dev/null
+++ b/src/AIMOS.ml
@@ -0,0 +1,83 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Why3
+open Base
+
+let aimos_file = Re__Core.(compile (str "%{aimos_file}"))
+
+let build_command config_prover aimos_filename =
+ let command = Whyconf.get_complete_command ~with_steps:false config_prover in
+ Re__Core.replace_string aimos_file ~by:aimos_filename command
+
+let re_aimos_output = Re__Pcre.regexp "((,\\s)(\\d+\\.\\d+))"
+
+let build_answer predicate_kind prover_result =
+ let threshold =
+ match predicate_kind with
+ | Dataset.MetaRobust f -> Float.of_string (Dataset.string_of_eps f)
+ | _ -> failwith "Unsupported property"
+ in
+ match prover_result.Call_provers.pr_answer with
+ | Call_provers.HighFailure -> (
+ let pr_output = prover_result.pr_output in
+ match Re__Core.exec_opt re_aimos_output pr_output with
+ | Some re_group ->
+ (* The regex matches the only group (the 3rd one) that contains
+ dot-separated numerical values that follow a comma and a space. This is
+ not ideal as there might be edge cases where the regex matches other
+ parts of the output that are not supposed to be matched. This will be
+ fixed later on, but for now is good enough. *)
+ let res_aimos = Float.of_string (Re__Core.Group.get re_group 3) in
+ let prover_answer =
+ if Float.( >= ) res_aimos threshold
+ then Call_provers.Valid
+ else Call_provers.Invalid
+ in
+ prover_answer
+ | None -> failwith "Cannot interpret the output provided by AIMOS")
+ | _ ->
+ (* Any other answer than HighFailure should never happen as we do not define
+ anything in AIMOS's driver. *)
+ assert false
+
+let call_prover limit config config_prover
+ (predicate : (Language.nn_shape, string) Dataset.predicate) aimos_config =
+ let command = build_command config_prover aimos_config in
+ let prover_call =
+ let res_parser =
+ {
+ Call_provers.prp_regexps =
+ [ ("NeverMatch", Call_provers.Failure "Should not happen in CAISAR") ];
+ prp_timeregexps = [];
+ prp_stepregexps = [];
+ prp_exitcodes = [];
+ 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)
+ in
+ let prover_result = Call_provers.wait_on_call prover_call in
+ build_answer predicate.property prover_result
diff --git a/src/AIMOS.mli b/src/AIMOS.mli
new file mode 100644
index 0000000..724e072
--- /dev/null
+++ b/src/AIMOS.mli
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(* *)
+(* This file is part of CAISAR. *)
+(* *)
+(* Copyright (C) 2022 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Why3
+
+val call_prover :
+ Call_provers.resource_limit ->
+ Whyconf.main ->
+ Whyconf.config_prover ->
+ (Language.nn_shape, string) Dataset.predicate ->
+ string ->
+ Call_provers.prover_answer
diff --git a/src/prover.ml b/src/prover.ml
index 4954c7d..ee7908d 100644
--- a/src/prover.ml
+++ b/src/prover.ml
@@ -24,11 +24,12 @@ type t =
| Marabou
| Pyrat [@name "PyRAT"]
| Saver [@name "SAVer"]
+ | Aimos [@name "AIMOS"]
| CVC5 [@name "cvc5"]
| Nnenum [@name "nnenum"]
[@@deriving yojson, show]
-let list_available () = [ Marabou; Pyrat; Saver; CVC5; Nnenum ]
+let list_available () = [ Marabou; Pyrat; Saver; Aimos; CVC5; Nnenum ]
let of_string prover =
let prover = String.lowercase_ascii prover in
@@ -36,6 +37,7 @@ let of_string prover =
| "marabou" -> Some Marabou
| "pyrat" -> Some Pyrat
| "saver" -> Some Saver
+ | "aimos" -> Some Aimos
| "cvc5" -> Some CVC5
| "nnenum" -> Some Nnenum
| _ -> None
@@ -44,9 +46,10 @@ let to_string = function
| Marabou -> "Marabou"
| Pyrat -> "PyRAT"
| Saver -> "SAVer"
+ | Aimos -> "AIMOS"
| CVC5 -> "CVC5"
| Nnenum -> "nnenum"
let has_vnnlib_support = function
| Pyrat -> true
- | Marabou | Saver | CVC5 | Nnenum -> false
+ | Marabou | Saver | Aimos | CVC5 | Nnenum -> false
diff --git a/src/prover.mli b/src/prover.mli
index e59e5d4..38b0203 100644
--- a/src/prover.mli
+++ b/src/prover.mli
@@ -24,6 +24,7 @@ type t = private
| Marabou
| Pyrat [@name "PyRAT"]
| Saver [@name "SAVer"]
+ | Aimos [@name "AIMOS"]
| CVC5 [@name "cvc5"]
| Nnenum [@name "nnenum"]
[@@deriving yojson, show]
diff --git a/src/verification.ml b/src/verification.ml
index d91151d..a0e4a02 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -203,6 +203,37 @@ let answer_dataset limit config env prover config_prover driver dataset task =
in
(prover_answer, additional_info)
+let answer_aimos limit config env config_prover dataset task aimos_config =
+ let predicate =
+ let on_model ls =
+ let message = Fmt.str "No NN model found as %a" Pretty.print_ls ls in
+ Option.value_exn ~message (Language.lookup_loaded_nets ls)
+ in
+ let on_dataset _ls =
+ match dataset with
+ | None -> invalid_arg "No dataset provided"
+ | Some filename ->
+ if String.is_suffix filename ~suffix:".csv"
+ then filename
+ else
+ invalid_arg
+ (Fmt.str "File '%s' has an unsupported extension" filename)
+ in
+ Dataset.interpret_predicate env ~on_model ~on_dataset task
+ in
+ let aimos_filename =
+ match aimos_config with
+ (* WARNING: change this path if you're not me, and make sure to have an
+ absolute path *)
+ | None -> "/home/aymeric/caisar/aimos_config.yml"
+ | Some s -> s
+ in
+ let answer =
+ AIMOS.call_prover limit config config_prover predicate aimos_filename
+ in
+ let additional_info = Some "" in
+ (answer, additional_info)
+
let answer_generic limit config env prover config_prover driver task =
let task = Proof_strategy.apply_native_nn_prover env task in
let task = Driver.prepare_task driver task in
@@ -235,6 +266,12 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
answer_saver limit config env config_prover dataset task
in
(prover_answer, Generic additional_info)
+ | Aimos ->
+ let prover_answer, additional_info =
+ (* TODO: add real config file *)
+ answer_aimos limit config env config_prover dataset task None
+ in
+ (prover_answer, Generic additional_info)
| (Marabou | Pyrat | Nnenum) when Option.is_some dataset ->
let dataset = Unix.realpath (Option.value_exn dataset) in
let prover_answer, additional_info =
--
GitLab