[cmdline] Marked dataset option as deprecated

src/main.ml

@@ -222,7 +222,8 @@ let verify_cmd =
   in
   let dataset =
     let doc =
-      "Dataset $(docv) (CSV format only). Deprecated, will be removed in \
+      "Dataset $(docv) (CSV format only). Deprecated, directly specify the \
+       dataset in the file or with the --define option. Will be removed in\n\
        version 4.0."
     in
     Arg.(value & opt (some file) None & info [ "dataset" ] ~doc ~docv:"FILE")

src/saver.ml

@@ -32,16 +32,11 @@ let re_abstraction = Re__.Core.(compile (str "%{abstraction}"))
 let re_perturbation = Re__.Core.(compile (str "%{perturbation}"))
 let re_perturbation_param = Re__.Core.(compile (str "%{perturbation_param}"))
 
-type perturbation =
-  | L_inf of Dataset.eps option
-  | From_file of string
+type perturbation = From_file of string
 
-let string_of_perturbation = function
-  | L_inf _ -> "l_inf"
-  | From_file _ -> "from_file"
+let string_of_perturbation = function From_file _ -> "from_file"
 
 let string_of_perturbation_param = function
-  | L_inf eps -> Option.(value (map ~f:Dataset.string_of_eps eps)) ~default:"0"
   | From_file filename -> Unix.realpath filename
 
 let build_command config_prover ?(abstraction = "hybrid") ~svm ~dataset
@@ -85,89 +80,9 @@ let re_saver_output =
    [re_saver_output]. *)
 let re_group_number_dataset_size = 1
 
-(* Regexp group number as matched by [re_saver_output] for each predicate. *)
-let re_group_number_of_predicate = function
-  | Dataset.Correct -> 2
-  | Robust _ -> 3
-  | CondRobust _ -> 4
-  | MetaRobust _ | MetaRobustMin _ | MetaRobustDiff _ ->
-    Logging.user_error (fun m ->
-      m "Unsupported metamorphic robustness predicate")
-
-let negative_answer = function
-  | Dataset.Correct ->
-    (* SAVer is complete wrt [Correct] predicate. *)
-    Call_provers.Invalid
-  | Robust _ | CondRobust _ -> Call_provers.Unknown ""
-  | MetaRobust _ | MetaRobustMin _ | MetaRobustDiff _ ->
-    Logging.user_error (fun m ->
-      m "Unsupported metamorphic robustness predicate")
-
-let build_answer_on_dataset_predicate predicate_kind prover_result =
-  match prover_result.Call_provers.pr_answer with
-  | Call_provers.Unknown _ -> (
-    let pr_output = prover_result.pr_output in
-    match Re__.Core.exec_opt re_saver_output pr_output with
-    | Some re_group ->
-      let nb_total =
-        Int.of_string
-          (Re__.Core.Group.get re_group re_group_number_dataset_size)
-      in
-      let nb_proved =
-        let re_group_number = re_group_number_of_predicate predicate_kind in
-        Int.of_string (Re__.Core.Group.get re_group re_group_number)
-      in
-      let prover_answer =
-        if nb_total = nb_proved
-        then Call_provers.Valid
-        else negative_answer predicate_kind
-      in
-      { prover_answer; nb_total; nb_proved }
-    | None ->
-      Logging.code_error ~src (fun m ->
-        m "Cannot interpret the output provided by SAVer"))
-  | unexpected_pr_answer ->
-    (* Any other answer than HighFailure should never happen as we do not define
-       anything in SAVer's driver. *)
-    Logging.code_error ~src (fun m ->
-      m "Unexpected SAVer prover answer '%a'"
-        Why3.Call_provers.print_prover_answer unexpected_pr_answer)
-
-let call_prover_on_dataset_predicate limit config config_prover predicate =
-  let command =
-    let svm = predicate.Dataset.model.Language.filename in
-    let dataset = predicate.dataset in
-    let eps =
-      match predicate.property with
-      | Dataset.Correct -> None
-      | Robust e | CondRobust e -> Some e
-      | MetaRobust _ | MetaRobustMin _ | MetaRobustDiff _ ->
-        Logging.user_error (fun m ->
-          m "Unsupported metamorphic robustness predicate")
-    in
-    build_command config_prover ~svm ~dataset (L_inf eps)
-  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 ~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_on_dataset_predicate predicate.property prover_result
-
 let build_answer prover_result =
   match prover_result.Call_provers.pr_answer with
-  | Call_provers.Unknown s -> (
-      Logs.debug (fun m -> m "%s" s);
+  | Call_provers.Unknown _ -> (
     let pr_output = prover_result.pr_output in
     match Re__.Core.exec_opt re_saver_output pr_output with
     | Some re_group ->

src/saver.mli

@@ -26,13 +26,6 @@ type answer = {
   nb_proved : int;  (** Number of data points verifying the property. *)
 }
 
-val call_prover_on_dataset_predicate :
-  Why3.Call_provers.resource_limit ->
-  Why3.Whyconf.main ->
-  Why3.Whyconf.config_prover ->
-  (Language.svm_shape, string) Dataset.predicate ->
-  answer
-
 val call_prover :
   Why3.Call_provers.resource_limit ->
   Why3.Whyconf.main ->

src/verification.ml

@@ -87,59 +87,6 @@ let write_ovo_as_onnx onnx_out_dir =
       Logging.user_error (fun m ->
         m "@[Cannot write SVM as ONNX in folder '%s': '%s'@]" onnx_out_dir msg))
 
-let answer_saver_on_dataset limit config env config_prover ~dataset task =
-  let id = Task.task_goal task in
-  let dataset_predicate =
-    let on_model ls =
-      Option.value_or_thunk
-        ~default:(fun () ->
-          invalid_arg
-            (Fmt.str "No SVM model found as logic symbol %a" Pretty.print_ls ls))
-        (Language.lookup_loaded_svms ls)
-    in
-    let on_dataset _ls =
-      if String.is_suffix dataset ~suffix:".csv"
-      then dataset
-      else
-        invalid_arg (Fmt.str "File '%s' has an unsupported extension" dataset)
-    in
-    Dataset.interpret_predicate env ~on_model ~on_dataset task
-  in
-  let answer =
-    Saver.call_prover_on_dataset_predicate limit config config_prover
-      dataset_predicate
-  in
-  let percentage_valid proved total =
-    Some Float.(of_int proved /. of_int total)
-  in
-  match answer.prover_answer with
-  | Call_provers.Unknown "" ->
-    let additional_info =
-      Some (Fmt.str "%d/%d" answer.nb_proved answer.nb_total)
-    in
-    Verification_types.Answer.LegacyDatasetAnswer
-      {
-        id;
-        prover_answer = Call_provers.Unknown "";
-        percentage_valid = percentage_valid answer.nb_proved answer.nb_total;
-        dataset_results = [];
-        additional_info;
-      }
-  | Call_provers.Unknown _ ->
-    assert false (* By construction of SAVer's Unknown answer. *)
-  | prover_answer ->
-    let additional_info =
-      Some (Fmt.str "(%d/%d)" answer.nb_proved answer.nb_total)
-    in
-    Verification_types.Answer.LegacyDatasetAnswer
-      {
-        id;
-        prover_answer;
-        percentage_valid = percentage_valid answer.nb_proved answer.nb_total;
-        dataset_results = [];
-        additional_info;
-      }
-
 let answer_aimos limit config env config_prover dataset task =
   let id = Task.task_goal task in
   let predicate =
@@ -386,10 +333,7 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
 let call_prover ~cwd ~limit config env prover config_prover driver ?dataset
   definitions task =
   match prover with
-  | Prover.Saver when Option.is_some dataset ->
-    let dataset = Option.value_exn dataset in
-    answer_saver_on_dataset limit config env config_prover ~dataset task
-  | Saver ->
+  | Prover.Saver ->
     let task = Interpreter.interpret_task ~cwd env ~definitions task in
     let proof_strategy = Proof_strategy.apply_svm_prover_strategy in
     answer_saver limit config env config_prover ~proof_strategy task