Merge branch 'master' of git.frama-c.com:laiser/caisar

src/autodetection.ml → src/autodetect.ml

@@ -4,20 +4,19 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Why3
 open Base
-module Sys = Caml.Sys
 
-let null = if Sys.unix then "/dev/null" else "NUL"
+let null = if Caml.Sys.unix then "/dev/null" else "NUL"
 
 let rec lookup_file dirs filename =
   match dirs with
   | [] -> raise Caml.Not_found
   | dir :: dirs ->
     let file = Caml.Filename.concat dir filename in
-    if Sys.file_exists file then file else lookup_file dirs filename
+    if Caml.Sys.file_exists file then file else lookup_file dirs filename
 
-let autodetect ?(debug = false) () =
-  let open Why3 in
+let autodetection ?(debug = false) () =
   if debug then Debug.set_flag Autodetection.debug;
   let caisar_conf =
     lookup_file Dirs.Sites.config "caisar-detection-data.conf"

src/autodetection.mli → src/autodetect.mli

@@ -4,7 +4,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val autodetect : ?debug:bool -> unit -> Why3.Whyconf.config
+val autodetection : ?debug:bool -> unit -> Why3.Whyconf.config
 (** Perform the autodetection of provers.
 
     @param debug activates debug information. *)

src/language.ml

@@ -4,6 +4,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Why3
 open Base
 
 (* -- Support for the NNet and ONNX neural network formats. *)
@@ -11,15 +12,14 @@ open Base
 type ioshape = {
   nb_inputs : int;
   nb_outputs : int;
-  ty_data : Why3.Ty.ty;
+  ty_data : Ty.ty;
   filename : string;
 }
 
-let loaded_nets = Why3.Term.Hls.create 10
-let lookup_loaded_nets = Why3.Term.Hls.find_opt loaded_nets
+let loaded_nets = Term.Hls.create 10
+let lookup_loaded_nets = Term.Hls.find_opt loaded_nets
 
 let register_astuple nb_inputs nb_outputs filename env =
-  let open Why3 in
   let net = Pmodule.read_module env [ "caisar" ] "IOShape" in
   let ioshape_input_type =
     Ty.ty_app Theory.(ns_find_ts net.mod_theory.th_export [ "input_type" ]) []
@@ -34,7 +34,7 @@ let register_astuple nb_inputs nb_outputs filename env =
       (List.init nb_inputs ~f)
       (Ty.ty_tuple (List.init nb_outputs ~f))
   in
-  Why3.Term.Hls.add loaded_nets ls_net_apply
+  Term.Hls.add loaded_nets ls_net_apply
     { filename; nb_inputs; nb_outputs; ty_data = ioshape_input_type };
   let th_uc =
     Pmodule.add_pdecl ~vc:false th_uc
@@ -43,25 +43,21 @@ let register_astuple nb_inputs nb_outputs filename env =
   Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
 
 let nnet_parser env _ filename _ =
-  let open Why3 in
   let model = Nnet.parse filename in
   match model with
   | Error s -> Loc.errorm "%s" s
   | Ok model -> register_astuple model.n_inputs model.n_outputs filename env
 
 let onnx_parser env _ filename _ =
-  let open Why3 in
   let model = Onnx.parse filename in
   match model with
   | Error s -> Loc.errorm "%s" s
   | Ok model -> register_astuple model.n_inputs model.n_outputs filename env
 
 let register_nnet_support () =
-  Why3.(
-    Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
-      "NNet" [ "nnet" ] nnet_parser)
+  Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
+    "NNet" [ "nnet" ] nnet_parser
 
 let register_onnx_support () =
-  Why3.(
-    Env.register_format ~desc:"ONNX format" Pmodule.mlw_language "ONNX"
-      [ "onnx" ] onnx_parser)
+  Env.register_format ~desc:"ONNX format" Pmodule.mlw_language "ONNX" [ "onnx" ]
+    onnx_parser

src/language.mli

@@ -4,14 +4,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Why3
+
 type ioshape = {
   nb_inputs : int;
   nb_outputs : int;
-  ty_data : Why3.Ty.ty;
+  ty_data : Ty.ty;
   filename : string;
 }
 
-val lookup_loaded_nets : Why3.Term.lsymbol -> ioshape option
+val lookup_loaded_nets : Term.lsymbol -> ioshape option
 (** @return the filename of a nnet Why3 representation. *)
 
 val register_nnet_support : unit -> unit

src/main.ml

@@ -55,7 +55,7 @@ let config detect () =
     Logs.debug (fun m -> m "Automatic detection.");
     let config =
       let debug = match Logs.level () with Some Debug -> true | _ -> false in
-      Autodetection.autodetect ~debug ()
+      Autodetect.autodetection ~debug ()
     in
     let open Why3 in
     let provers = Whyconf.get_provers config in

src/printers/marabou.ml

@@ -4,32 +4,32 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Why3
+
 type info = {
-  le : Why3.Term.lsymbol;
-  ge : Why3.Term.lsymbol;
-  lt : Why3.Term.lsymbol;
-  gt : Why3.Term.lsymbol;
-  info_syn : Why3.Printer.syntax_map;
-  variables : string Why3.Term.Hls.t;
+  le : Term.lsymbol;
+  ge : Term.lsymbol;
+  lt : Term.lsymbol;
+  gt : Term.lsymbol;
+  info_syn : Printer.syntax_map;
+  variables : string Term.Hls.t;
 }
 
 let number_format =
   {
-    Why3.Number.long_int_support = `Default;
-    Why3.Number.negative_int_support = `Default;
-    Why3.Number.dec_int_support = `Default;
-    Why3.Number.hex_int_support = `Unsupported;
-    Why3.Number.oct_int_support = `Unsupported;
-    Why3.Number.bin_int_support = `Unsupported;
-    Why3.Number.negative_real_support =
-      `Custom (fun fmt f -> Fmt.pf fmt "-%t" f);
-    Why3.Number.dec_real_support = `Default;
-    Why3.Number.hex_real_support = `Unsupported;
-    Why3.Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
+    Number.long_int_support = `Default;
+    Number.negative_int_support = `Default;
+    Number.dec_int_support = `Default;
+    Number.hex_int_support = `Unsupported;
+    Number.oct_int_support = `Unsupported;
+    Number.bin_int_support = `Unsupported;
+    Number.negative_real_support = `Custom (fun fmt f -> Fmt.pf fmt "-%t" f);
+    Number.dec_real_support = `Default;
+    Number.hex_real_support = `Unsupported;
+    Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
   }
 
 let rec print_term info fmt t =
-  let open Why3 in
   match t.Term.t_node with
   | Tbinop ((Timplies | Tiff | Tor), _, _)
   | Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
@@ -46,7 +46,6 @@ let rec print_term info fmt t =
       | _ -> Printer.unsupportedTerm t "Unknown variable(s)"))
 
 let rec print_top_level_term info fmt t =
-  let open Why3 in
   (* Don't print things we don't know. *)
   let t_is_known =
     Term.t_s_all
@@ -67,7 +66,6 @@ let rec print_top_level_term info fmt t =
   | _ -> if t_is_known t then Fmt.pf fmt "%a@." (print_term info) t
 
 let rec negate_term info t =
-  let open Why3 in
   match t.Term.t_node with
   | Tquant _ -> Printer.unsupportedTerm t "Quantification"
   | Tbinop (Tand, _, _) -> Printer.unsupportedTerm t "Conjunction"
@@ -87,7 +85,6 @@ let rec negate_term info t =
   | _ -> Printer.unsupportedTerm t "Cannot negate such term"
 
 let print_decl info fmt d =
-  let open Why3 in
   match d.Decl.d_node with
   | Dtype _ -> ()
   | Ddata _ -> ()
@@ -100,7 +97,6 @@ let print_decl info fmt d =
     print_top_level_term info fmt (negate_term info f)
 
 let rec print_tdecl info fmt task =
-  let open Why3 in
   match task with
   | None -> ()
   | Some { Task.task_prev; task_decl; _ } -> (
@@ -121,7 +117,6 @@ let rec print_tdecl info fmt task =
     | Decl d -> print_decl info fmt d)
 
 let print_task args ?old:_ fmt task =
-  let open Why3 in
   let th = Env.read_theory args.Printer.env [ "ieee_float" ] "Float64" in
   let le = Theory.ns_find_ls th.th_export [ "le" ] in
   let lt = Theory.ns_find_ls th.th_export [ "lt" ] in
@@ -141,5 +136,5 @@ let print_task args ?old:_ fmt task =
   print_tdecl info fmt task
 
 let init () =
-  Why3.Printer.register_printer ~desc:"Printer for the Marabou prover."
-    "marabou" print_task
+  Printer.register_printer ~desc:"Printer for the Marabou prover." "marabou"
+    print_task

src/printers/pyrat.ml

@@ -4,28 +4,25 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type info = {
-  info_syn : Why3.Printer.syntax_map;
-  variables : string Why3.Term.Hls.t;
-}
+open Why3
+
+type info = { info_syn : Printer.syntax_map; variables : string Term.Hls.t }
 
 let number_format =
   {
-    Why3.Number.long_int_support = `Default;
-    Why3.Number.negative_int_support = `Default;
-    Why3.Number.dec_int_support = `Default;
-    Why3.Number.hex_int_support = `Unsupported;
-    Why3.Number.oct_int_support = `Unsupported;
-    Why3.Number.bin_int_support = `Unsupported;
-    Why3.Number.negative_real_support =
-      `Custom (fun fmt f -> Fmt.pf fmt "-%t" f);
-    Why3.Number.dec_real_support = `Default;
-    Why3.Number.hex_real_support = `Unsupported;
-    Why3.Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
+    Number.long_int_support = `Default;
+    Number.negative_int_support = `Default;
+    Number.dec_int_support = `Default;
+    Number.hex_int_support = `Unsupported;
+    Number.oct_int_support = `Unsupported;
+    Number.bin_int_support = `Unsupported;
+    Number.negative_real_support = `Custom (fun fmt f -> Fmt.pf fmt "-%t" f);
+    Number.dec_real_support = `Default;
+    Number.hex_real_support = `Unsupported;
+    Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
   }
 
 let rec print_base_term info fmt t =
-  let open Why3 in
   match t.Term.t_node with
   | Tbinop ((Tand | Tor), _, _) -> assert false
   | Tbinop ((Timplies | Tiff), _, _)
@@ -42,7 +39,6 @@ let rec print_base_term info fmt t =
       | _ -> Printer.unsupportedTerm t "Unknown variable(s)"))
 
 let rec print_term ~sep info fmt t =
-  let open Why3 in
   (* Don't print things we don't know. *)
   let t_is_known =
     Term.t_s_all
@@ -66,7 +62,6 @@ let rec print_term ~sep info fmt t =
   | _ -> if t_is_known t then Fmt.pf fmt "%a%(%)" (print_base_term info) t sep
 
 let print_decl info fmt d =
-  let open Why3 in
   match d.Decl.d_node with
   | Dtype _ -> ()
   | Ddata _ -> ()
@@ -81,7 +76,6 @@ let print_decl info fmt d =
   | Dprop (Decl.Pgoal, _, f) -> print_term ~sep:"" info fmt f
 
 let rec print_tdecl info fmt task =
-  let open Why3 in
   match task with
   | None -> ()
   | Some { Task.task_prev; task_decl; _ } -> (
@@ -102,7 +96,6 @@ let rec print_tdecl info fmt task =
     | Decl d -> print_decl info fmt d)
 
 let print_task args ?old:_ fmt task =
-  let open Why3 in
   let info =
     {
       info_syn = Discriminate.get_syntax_map task;
@@ -113,5 +106,5 @@ let print_task args ?old:_ fmt task =
   print_tdecl info fmt task
 
 let init () =
-  Why3.Printer.register_printer ~desc:"Printer for the PyRAT prover." "pyrat"
+  Printer.register_printer ~desc:"Printer for the PyRAT prover." "pyrat"
     print_task

src/transformations/native_nn_prover.ml

@@ -4,29 +4,29 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Why3
 open Base
 
 let meta_input =
-  Why3.Theory.(
+  Theory.(
     register_meta "caisar_input"
       ~desc:"Indicates the input position in the neural network"
       [ MTlsymbol; MTint ])
 
 let meta_output =
-  Why3.Theory.(
+  Theory.(
     register_meta "caisar_output"
       ~desc:"Indicates the output position in the neural network"
       [ MTlsymbol; MTint ])
 
 let meta_nn_filename =
-  Why3.Theory.(
+  Theory.(
     register_meta_excl "caisar_nnet_or_onnx"
       ~desc:"Indicates the filename of the network" [ MTstring ])
 
 (* Retrieve the (input) variables appearing, as arguments, after an 'nnet_apply'
    symbol. *)
 let get_input_variables =
-  let open Why3 in
   let rec aux acc (term : Term.term) =
     match term.t_node with
     | Term.Tapp (ls, args) -> (
@@ -48,7 +48,6 @@ let get_input_variables =
 (* Create logic symbols for output variables and simplify the formula. *)
 (* TODO: [Reduction_engine] is probably an overkill and should be replaced. *)
 let simplify_goal env input_variables =
-  let open Why3 in
   let rec aux meta hls (term : Term.term) =
     match term.t_node with
     | Term.Tapp (ls, _) -> (
@@ -115,9 +114,9 @@ let simplify_goal env input_variables =
     None
 
 let native_nn_prover env =
-  Why3.(Trans.seq [ Trans.bind get_input_variables (simplify_goal env) ])
+  Trans.seq [ Trans.bind get_input_variables (simplify_goal env) ]
 
 let init () =
-  Why3.Trans.register_env_transform
+  Trans.register_env_transform
     ~desc:"Transformation for provers that support loading neural networks."
     "native_nn_prover" native_nn_prover

src/transformations/native_nn_prover.mli

@@ -4,14 +4,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Why3
+
 val init : unit -> unit
 (** Register the transformation. *)
 
-val meta_input : Why3.Theory.meta
+val meta_input : Theory.meta
 (** Indicate the input position. *)
 
-val meta_output : Why3.Theory.meta
+val meta_output : Theory.meta
 (** Indicate the output position. *)
 
-val meta_nn_filename : Why3.Theory.meta
+val meta_nn_filename : Theory.meta
 (** The filename of the nnet or onnx model. *)

src/transformations/vars_on_lhs.ml

@@ -4,10 +4,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Why3
 open Base
 
 let make_rt env =
-  let open Why3 in
   let th = Env.read_theory env [ "ieee_float" ] "Float64" in
   let t = Theory.ns_find_ts th.th_export [ "t" ] in
   let le = Theory.ns_find_ls th.th_export [ "le" ] in
@@ -43,10 +43,10 @@ let make_rt env =
 
 let vars_on_lhs env =
   let rt, task = make_rt env in
-  Why3.Trans.rewrite rt task
+  Trans.rewrite rt task
 
 let init () =
-  Why3.Trans.register_env_transform
+  Trans.register_env_transform
     ~desc:
       "Transformation for provers that need variables on the left-hand-side of \
        logic symbols."

src/verification.ml

@@ -4,6 +4,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Why3
 open Base
 module Filename = Caml.Filename
 
@@ -12,8 +13,7 @@ let () =
   Language.register_onnx_support ()
 
 let create_env loadpath =
-  let config = Autodetection.autodetect ~debug:true () in
-  let open Why3 in
+  let config = Autodetect.autodetection ~debug:true () in
   let config =
     let main = Whyconf.get_main config in
     let dft_memlimit = 4000 (* 4 GB *) in
@@ -28,18 +28,15 @@ let create_env loadpath =
       (loadpath @ stdlib @ Whyconf.loadpath (Whyconf.get_main config)),
     config )
 
-let nnet_or_onnx = Re.compile (Re.str "%{nnet-onnx}")
+let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
 
 let combine_prover_answers answers =
-  let open Why3 in
   List.fold_left answers ~init:Call_provers.Valid ~f:(fun acc r ->
     match (acc, r) with
     | Call_provers.Valid, r | r, Call_provers.Valid -> r
     | _ -> acc)
 
-let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver task
-    =
-  let open Why3 in
+let call_prover ~limit config (prover : Whyconf.config_prover) driver task =
   let task_prepared = Driver.prepare_task driver task in
   let tasks =
     (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
@@ -70,7 +67,6 @@ let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver task
     Call_provers.print_prover_answer answer
 
 let verify ?(debug = false) format loadpath ?memlimit ?timeout ~prover file =
-  let open Why3 in
   if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
   let env, config = create_env loadpath in
   let steplimit = None in