examples/use_api/mlw_tree.ml

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2024 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 (*******************
  13
  14 This file builds some MLW modules, using parse trees instead of direct
  15 API calls
  16
  17 ******************)
  18
  19 (* BEGIN{buildenv} *)
  20 open Why3
  21 let config : Whyconf.config = Whyconf.init_config None
  22 let main : Whyconf.main = Whyconf.get_main config
  23 let env : Env.env = Env.create_env (Whyconf.loadpath main)
  24 open Ptree
  25 open Ptree_helpers
  26 (* END{buildenv} *)
  27
  28 (* declaration of
  29   BEGIN{source1}
  30 module M1
  31   use int.Int
  32   goal g : 2 + 2 = 4
  33 end
  34   END{source1}
  35  *)
  36
  37 (* BEGIN{code1} *)
  38 let mod_M1 =
  39   (* use int.Int *)
  40   let use_int_Int = use ~import:false (["int";"Int"]) in
  41   (* goal g : 2 + 2 = 4 *)
  42   let g =
  43     let two = tconst 2 in
  44     let four = tconst 4 in
  45     let add_int = qualid ["Int";Ident.op_infix "+"] in
  46     let two_plus_two = tapp add_int [two ; two] in
  47     let eq_int = qualid ["Int";Ident.op_infix "="] in
  48     let goal_term = tapp eq_int  [four ; two_plus_two] in
  49     Dprop(Decl.Pgoal, ident "g", goal_term)
  50   in
  51   (ident "M1",[use_int_Int ; g])
  52 (* END{code1} *)
  53
  54
  55 (* declaration of
  56   BEGIN{source2}
  57 module M2
  58   let f (x:int) : int
  59     requires { x=6 }
  60     ensures { result=42 }
  61    = x*7
  62 end
  63   END{source2}
  64  *)
  65
  66 (* BEGIN{code2} *)
  67 let eq_symb = qualid [Ident.op_infix "="]
  68 let int_type_id = qualid ["int"]
  69 let int_type = PTtyapp(int_type_id,[])
  70 let mul_int = qualid ["Int";Ident.op_infix "*"]
  71
  72 let mod_M2 =
  73   (* use int.Int *)
  74   let use_int_Int = use ~import:false (["int";"Int"]) in
  75   (* f *)
  76   let f =
  77     let id_x = ident "x" in
  78     let pre = tapp eq_symb [tvar (Qident id_x); tconst 6] in
  79     let result = ident "result" in
  80     let post = tapp eq_symb [tvar (Qident result); tconst 42] in
  81     let spec = {
  82       sp_pre = [pre];
  83       sp_post = [Loc.dummy_position,[pat_var result,post]];
  84       sp_xpost = [];
  85       sp_reads = [];
  86       sp_writes = [];
  87       sp_alias = [];
  88       sp_variant = [];
  89       sp_checkrw = false;
  90       sp_diverge = false;
  91       sp_partial = false;
  92     }
  93     in
  94     let body = eapp mul_int [evar (Qident id_x); econst 7] in
  95     let f =
  96       Efun(one_binder ~pty:int_type "x", None, pat Pwild,
  97            Ity.MaskVisible, spec, body)
  98     in
  99     Dlet(ident "f",false,Expr.RKnone, expr f)
 100   in
 101   (ident "M2",[use_int_Int ; f])
 102 (* END{code2} *)
 103
 104
 105 (* declaration of
 106   BEGIN{source3}
 107 module M3
 108   let f() : int
 109      requires { true }
 110      ensures { result >= 0 }
 111    = let x = ref 42 in !x
 112 end
 113   END{source3}
 114  *)
 115
 116 (* BEGIN{code3} *)
 117 let ge_int = qualid ["Int";Ident.op_infix ">="]
 118
 119 let mod_M3 =
 120   (* use int.Int *)
 121   let use_int_Int = use ~import:false (["int";"Int"]) in
 122   (* use ref.Ref *)
 123   let use_ref_Ref = use ~import:false (["ref";"Ref"]) in
 124   (* f *)
 125   let f =
 126     let result = ident "result" in
 127     let post = term(Tidapp(ge_int,[tvar (Qident result);tconst 0])) in
 128     let spec = {
 129       sp_pre = [];
 130       sp_post = [Loc.dummy_position,[pat_var result,post]];
 131       sp_xpost = [];
 132       sp_reads = [];
 133       sp_writes = [];
 134       sp_alias = [];
 135       sp_variant = [];
 136       sp_checkrw = false;
 137       sp_diverge = false;
 138       sp_partial = false;
 139     }
 140     in
 141     let body =
 142       let e1 = eapply (evar (qualid ["Ref";"ref"])) (econst 42) in
 143       let id_x = ident "x" in
 144       let qid = qualid ["Ref";Ident.op_prefix "!"] in
 145       let e2 = eapply (evar qid) (evar (Qident id_x)) in
 146       expr(Elet(id_x,false,Expr.RKnone,e1,e2))
 147     in
 148     let f = Efun(unit_binder (),None,pat Pwild,Ity.MaskVisible,spec,body)
 149     in
 150     Dlet(ident "f",false,Expr.RKnone, expr f)
 151   in
 152   (ident "M3",[use_int_Int ; use_ref_Ref ; f])
 153 (* END{code3} *)
 154
 155 (* declaration of
 156   BEGIN{source4}
 157 module M4
 158   let f (a:array int) : unit
 159     requires { a.length >= 1 }
 160     writes { a }
 161     ensures { a[0] = 42 }
 162    = a[0] <- 42
 163 end
 164   END{source4}
 165  *)
 166
 167 (* BEGIN{code4} *)
 168
 169 let array_int_type = PTtyapp(qualid ["Array";"array"],[int_type])
 170
 171 let length = qualid ["Array";"length"]
 172
 173 let array_get = qualid ["Array"; Ident.op_get ""]
 174
 175 let array_set = qualid ["Array"; Ident.op_set ""]
 176
 177 let mod_M4 =
 178   (* use int.Int *)
 179   let use_int_Int = use ~import:false (["int";"Int"]) in
 180   (* use array.Array *)
 181   let use_array_Array = use ~import:false (["array";"Array"]) in
 182   (* decl f *)
 183   let f =
 184     let id_a = ident "a" in
 185     let pre =
 186       tapp ge_int [tapp length [tvar (Qident id_a)]; tconst 1]
 187     in
 188     let post =
 189       tapp eq_symb [tapp array_get [tvar (Qident id_a); tconst 0];
 190                        tconst 42]
 191     in
 192     let spec = {
 193       sp_pre = [pre];
 194       sp_post = [Loc.dummy_position,[pat Pwild,post]];
 195       sp_xpost = [];
 196       sp_reads = [];
 197       sp_writes = [tvar (Qident id_a)];
 198       sp_alias = [];
 199       sp_variant = [];
 200       sp_checkrw = false;
 201       sp_diverge = false;
 202       sp_partial = false;
 203     }
 204     in
 205     let body =
 206       eapp array_set [evar (Qident id_a); econst 0; econst 42]
 207     in
 208     let f = Efun(one_binder ~pty:array_int_type "a",
 209                  None,pat Pwild,Ity.MaskVisible,spec,body)
 210     in
 211     Dlet(ident "f", false, Expr.RKnone, expr f)
 212   in
 213   (ident "M4",[use_int_Int ; use_array_Array ; f])
 214 (* END{code4} *)
 215
 216 (* The following example is not in the manual
 217  * it shows how to use Ptree API for global variable declaration
 218 module Mglob
 219   use int.Int
 220   val ref x : int
 221   let f () : unit = x <- x+1
 222 end
 223 *)
 224
 225 let mod_Mglob =
 226   (* use int.Int *)
 227   let use_int_Int = use ~import:false (["int";"Int"]) in
 228   (* x *)
 229   let id_x,decl_x = global_var_decl int_type "x" in
 230   (* f *)
 231   let decl_f =
 232     let spec = {
 233       sp_pre = [];
 234       sp_post = [];
 235       sp_xpost = [];
 236       sp_reads = [];
 237       sp_writes = [tvar (Qident id_x)];
 238       sp_alias = [];
 239       sp_variant = [];
 240       sp_checkrw = false;
 241       sp_diverge = false;
 242       sp_partial = false;
 243     }
 244     in
 245     let add_int = qualid ["Int";Ident.op_infix "+"] in
 246     let xp1 = eapp add_int [evar (Qident id_x) ; econst 1 ] in
 247     let body = expr (Eassign [ expr (Easref (Qident id_x)), None, xp1  ]) in
 248     let f = Efun(unit_binder (),None,pat Pwild,Ity.MaskVisible,spec,body) in
 249     Dlet(ident "f", false, Expr.RKnone, expr f)
 250
 251   in
 252   (ident "Mglob",[use_int_Int ; decl_x; decl_f])
 253
 254 (* The following example is not in the manual
 255  * it shows how to use Ptree API for scope/import declarations
 256 module Mscope
 257   scope S
 258       function f (x : int) : int = x
 259   end
 260
 261   import S
 262   goal g : f 2 = 2
 263 end
 264 *)
 265
 266 let mod_Mscope =
 267   (* use int.Int *)
 268   let use_int_Int = use ~import:false (["int";"Int"]) in
 269   (* scope S *)
 270   let scope_S =
 271     (* f *)
 272     let f =
 273       let logic = {
 274         ld_loc = Loc.dummy_position;
 275         ld_ident = ident "f";
 276         ld_params = [(Loc.dummy_position,Some (ident "x"),false,int_type)] ;
 277         ld_type = Some int_type;
 278         ld_def = Some (tvar (Qident (ident "x"))) ;
 279       } in
 280       Dlogic([logic])
 281     in
 282     Dscope(Loc.dummy_position,false,ident "S",[f])
 283   in
 284   (* import S *)
 285   let import_S = Dimport (qualid ["S"]) in
 286   (* goal g : f 2 = 2 *)
 287   let g =
 288     let two = tconst 2 in
 289     let eq_int = qualid ["Int";Ident.op_infix "="] in
 290     let f_of_two = tapp (qualid ["f"]) [two] in
 291     let goal_term = tapp eq_int [f_of_two ; two] in
 292     Dprop(Decl.Pgoal,ident "g",goal_term)
 293   in
 294   (ident "Mscope",[use_int_Int ; scope_S ; import_S ; g])
 295
 296 (* BEGIN{getmodules} *)
 297 let mlw_file = Modules [mod_M1 ; mod_M2 ; mod_M3 ; mod_M4]
 298 (* END{getmodules} *)
 299 let mlw_file_others = Modules [mod_Mglob ; mod_Mscope]
 300
 301 open Format
 302
 303 (* Printing back the mlw file *)
 304 (* BEGIN{mlwprinter} *)
 305 let () = printf "%a@." (Mlw_printer.pp_mlw_file ~attr:true) mlw_file
 306 (* END{mlwprinter} *)
 307
 308 let () = printf "%a@." (Mlw_printer.pp_mlw_file ~attr:true) mlw_file_others
 309
 310 (* BEGIN{topdownf} *)
 311 let mlw_file_F =
 312   let uc = F.create () in
 313   let uc = F.begin_module uc "M5" in
 314   let uc = F.use uc ~import:false ["int";"Int"] in
 315   let uc = F.use uc ~import:false ["array";"Array"] in
 316   let uc = F.begin_let uc "f" (one_binder ~pty:array_int_type "a") in
 317   let id_a = Qident (ident "a") in
 318   let pre = tapp ge_int [tapp length [tvar id_a]; tconst 1] in
 319   let uc = F.add_pre uc pre in
 320   let uc = F.add_writes uc [tvar id_a] in
 321   let post =
 322     tapp eq_symb [tapp array_get [tvar id_a; tconst 0];
 323                   tconst 42]
 324   in
 325   let uc = F.add_post uc post in
 326   let body = eapp array_set [evar id_a; econst 0; econst 42] in
 327   let uc = F.add_body uc body in
 328   let uc = F.end_module uc in
 329   F.get_mlw_file uc
 330 (* END{topdownf} *)
 331
 332 let () = printf "%a@." (Mlw_printer.pp_mlw_file ~attr:true) mlw_file_F
 333
 334 (* BEGIN{topdowni} *)
 335 let mlw_file_I =
 336   I.begin_module "M6";
 337   I.use ~import:false ["int";"Int"];
 338   I.use ~import:false ["array";"Array"];
 339   I.begin_let "f" (one_binder ~pty:array_int_type "a");
 340   let id_a = Qident (ident "a") in
 341   let pre = tapp ge_int [tapp length [tvar id_a]; tconst 1] in
 342   I.add_pre pre;
 343   I.add_writes [tvar id_a];
 344   let post =
 345     tapp eq_symb [tapp array_get [tvar id_a; tconst 0];
 346                   tconst 42]
 347   in
 348   I.add_post post;
 349   let body = eapp array_set [evar id_a; econst 0; econst 42] in
 350   I.add_body body;
 351   I.end_module ();
 352   I.get_mlw_file ()
 353 (* END{topdowni} *)
 354
 355 let () = printf "%a@." (Mlw_printer.pp_mlw_file ~attr:true) mlw_file_I
 356
 357 (* BEGIN{typemodules} *)
 358 let mods = Typing.type_mlw_file env [] "myfile.mlw" mlw_file
 359 (* END{typemodules} *)
 360 let mod_F = Typing.type_mlw_file env [] "myFfile.mlw" mlw_file_F
 361 let mod_I = Typing.type_mlw_file env [] "myIfile.mlw" mlw_file_I
 362 let mods_others = Typing.type_mlw_file env [] "myotherfile.mlw" mlw_file_others
 363
 364 (* BEGIN{typemoduleserror} *)
 365 let _mods =
 366   try
 367     Typing.type_mlw_file env [] "myfile.mlw" mlw_file
 368   with Loc.Located (loc, e) -> (* A located exception [e] *)
 369     let msg = asprintf "%a" Exn_printer.exn_printer e in
 370     printf "%a@."
 371       (Mlw_printer.with_marker ~msg loc (Mlw_printer.pp_mlw_file ~attr:true))
 372       mlw_file;
 373     exit 1
 374 (* END{typemoduleserror} *)
 375
 376 (* Checking the VCs *)
 377
 378 (* BEGIN{checkingvcs} *)
 379 let my_tasks : Task.task list =
 380   let mods =
 381     Wstdlib.Mstr.fold
 382       (fun _ m acc ->
 383        List.rev_append
 384          (Task.split_theory m.Pmodule.mod_theory None None) acc)
 385       mods []
 386   in List.rev mods
 387
 388
 389
 390 let provers : Whyconf.config_prover Whyconf.Mprover.t =
 391   Whyconf.get_provers config
 392
 393 (* default resource limits *)
 394 let limits =
 395   Call_provers.{empty_limits with
 396                 limit_time = Whyconf.timelimit main;
 397                 limit_mem = Whyconf.memlimit main }
 398
 399 let alt_ergo : Whyconf.config_prover =
 400   let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
 401   let provers = Whyconf.filter_provers config fp in
 402   if Whyconf.Mprover.is_empty provers then begin
 403     eprintf "Prover Alt-Ergo not installed or not configured@.";
 404     exit 1
 405   end else
 406     snd (Whyconf.Mprover.max_binding provers)
 407
 408 let alt_ergo_driver : Driver.driver =
 409   try
 410     Driver.load_driver_for_prover main env alt_ergo
 411   with e ->
 412     eprintf "Failed to load driver for alt-ergo: %a@."
 413       Exn_printer.exn_printer e;
 414     exit 1
 415
 416 let () =
 417   List.iteri (fun i t ->
 418       let call =
 419         Driver.prove_task ~limits ~config:main
 420           ~command:alt_ergo.Whyconf.command alt_ergo_driver t in
 421       let r = Call_provers.wait_on_call call in
 422       printf "@[On task %d, alt-ergo answers %a@." (succ i)
 423         (Call_provers.print_prover_result ?json:None) r)
 424     my_tasks
 425 (* END{checkingvcs} *)
 426
 427 (*
 428 Local Variables:
 429 compile-command: "make -C ../.. test-api-mlw_tree"
 430 End:
 431 *)