runstrat: try to write an automatic strategy in why3 as an independent project.

Try to use the way make do parallelism. It is able to
interact with the parallelism of make as sub-makes do.

Makefile.in

@@ -1181,6 +1181,7 @@ install_local: bin/why3doc
 
 bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
 	$(MAKE) test-api.@OCAMLBEST@
+	$(MAKE) test-runstrat.@OCAMLBEST@
 	sh bench/bench "bin/why3.@OCAMLBEST@"
 	@if test "@enable_coq_tactic@" = "yes"; then \
 	   echo "=== checking the Coq tactic ==="; \
@@ -1240,6 +1241,16 @@ test-api.opt: examples/use_api.ml src/why3.cmxa
 test-shape: src/why3.cma
 	ocaml -I src/ $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml
 
+#only test the compilation of runstrat
+test-runstrat.byte: $(LOCALWHY3LIB)/why3.cmxa $(LOCALWHY3LIB)/why3ml.cmxa $(LOCALWHY3LIB)/META
+	OCAMLPATH=$(PWD)/lib-ocaml $(MAKE) -C examples/runstrat clean
+	OCAMLPATH=$(PWD)/lib-ocaml $(MAKE) -C examples/runstrat byte
+
+test-runstrat.opt: $(LOCALWHY3LIB)/why3.cmxa $(LOCALWHY3LIB)/why3ml.cmxa $(LOCALWHY3LIB)/META
+	OCAMLPATH=$(PWD)/lib-ocaml $(MAKE) -C examples/runstrat clean
+	OCAMLPATH=$(PWD)/lib-ocaml $(MAKE) -C examples/runstrat opt
+
+test-runstrat: test-runstrat.$(OCAMLBEST)
 
 ################
 # documentation

examples/runstrat/Makefile

+
+BINDIR=/usr/local/bin
+
+OCAMLFIND = ocamlfind
+
+OCAMLFIND_OPT = $(addprefix -package ,$(PACKAGES)) -annot
+OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLFIND_OPT)
+OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLFIND_OPT)
+OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLFIND_OPT)
+
+PACKAGES = unix str
+
+all:makejob runstrat
+opt: makejob.opt runstrat.opt
+byte: makejob.byte runstrat.byte
+
+printconf:
+	echo $(OCAMLPATH)
+	ocamlfind printconf
+
+makeproto.cmo: makeproto.cmi
+makeproto.cmx: makeproto.cmi
+
+makejob.opt: makeproto.cmx makejob.ml
+makejob.byte: makeproto.cmo makejob.ml
+
+makejob: makejob.opt
+	@rm -f makejob
+	ln -s makejob.opt makejob
+
+runstrat.opt runstrat.byte: PACKAGES += why3 why3.ml
+runstrat.opt: makeproto.cmx runstrat.ml
+runstrat.byte: makeproto.cmo runstrat.ml
+
+runstrat: runstrat.opt
+	@rm -f runstrat
+	ln -s runstrat.opt runstrat
+
+install:
+	mkdir -p $(BINDIR)
+	cp runstrat.opt $(BINDIR)/runstrat
+	cp makejob.opt $(BINDIR)/makejob
+
+clean:
+	rm -f *.cmo *.cma *.cmx *.cmi *.o *.annot *.opt
+	rm -f runstrat makejob
+
+### Tests ###
+
+.PHONY: test_makejob %.test_makejob_aux
+
+TEST_MAKEJOB=$(addsuffix .test_makejob_aux , $(shell seq 5 -1 1))
+
+test_makejob: $(TEST_MAKEJOB)
+	@echo Done $(TEST_MAKEJOB)
+
+%.test_makejob_aux: makejob
+	@echo Run $*
+	+./run_wait.ml e 10 ./echo_wait.ml $*
+	@echo Done $*
+
+
+################
+# generic rules
+################
+
+%.cmi: %.mli
+	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $<
+
+%.cmo: %.ml
+	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $<
+
+%.cmx: %.ml
+	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $<
+
+%.dep: %.ml
+	$(if $(QUIET),@echo 'Ocamldep $<' &&) $(OCAMLDEP) $(DEPFLAGS) $< $<i > $@
+
+%.opt:
+	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -linkpkg -o $@ $^
+
+%.byte:
+	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -linkpkg -o $@ $^

examples/runstrat/echo_wait.ml

+#!/usr/bin/env ocaml
+#load "unix.cma";;
+
+open Format
+
+let print_args fmt =
+  for i = 1 to Array.length Sys.argv - 1 do
+    fprintf fmt "%s" Sys.argv.(i);
+    if i <> Array.length Sys.argv - 1
+    then fprintf fmt " "
+  done
+
+let max_sleep =
+  try float_of_string (Sys.argv.(1))
+  with _ -> 1.0
+
+let () =
+  Random.self_init ();
+  let sleep = Random.float max_sleep in
+  printf "echo %f wait %t@." sleep print_args;
+  ignore (Unix.select [] [] [] sleep);
+  printf "echo done %t@." print_args

examples/runstrat/makejob.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2012                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Guillaume Melquiond                                                 *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software 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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** This simple program implement the client side of the make
+    jobserver protocole. It ask for a job token and release it after completion
+    of the command
+
+    http://mad-scientist.net/make/jobserver.html
+*)
+
+(** ./makejob fdid_in fdid_out command [command options]
+   fdid_in and fdid_out are valid filedescriptor given by the caller
+ *)
+
+open Format
+
+let print_usage fmt =
+  fprintf fmt "usage: %s fdid_in fdid_out command [command options]@."
+    Sys.argv.(0)
+
+
+(** Test there is enough arguments *)
+let () = if Array.length Sys.argv < 4
+  then begin
+    print_usage err_formatter; exit 1;
+  end
+
+let cmd,args = Sys.argv.(3),Array.sub Sys.argv 3 (Array.length Sys.argv - 3)
+
+(** How should I do that? *)
+let fd_of_int : int -> Unix.file_descr = Obj.magic
+
+(** parse the file descriptor *)
+let pipe =
+  let fdid_in, fdid_out =
+    try int_of_string Sys.argv.(1), int_of_string Sys.argv.(2)
+    with Invalid_argument _ ->
+      eprintf "The first two argument must be the number of a file descriptor%t"
+        print_usage;
+      exit 1
+  in
+  Makeproto.from_fd_id fdid_in fdid_out
+
+let run_job f =
+  Makeproto.wait_worker pipe;
+  try
+    let res = f () in
+    Makeproto.release_worker pipe;
+    res
+  with exn ->
+    Makeproto.release_worker pipe;
+    raise exn
+
+(** Execute the command *)
+let () =
+  let ps = run_job (fun () ->
+  let pid = Unix.create_process cmd args
+    Unix.stdin Unix.stdout Unix.stderr in
+  let rpid,ps = Unix.waitpid [] pid in
+  assert (pid = rpid);
+  ps) in
+  match ps with
+  | Unix.WEXITED i -> exit i
+  | Unix.WSIGNALED i ->
+    (** Should not appear on windows ? *)
+    Unix.kill (Unix.getpid ()) Sys.sigterm
+  | Unix.WSTOPPED _ ->
+    (** Not possible since we doesn't wait for that *)
+    assert false
+

examples/runstrat/makeproto.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2012                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Guillaume Melquiond                                                 *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software 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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Format
+
+(** Make protocol for parallelism **)
+type pipe = { pin : Unix.file_descr;
+              pout: Unix.file_descr }
+
+type t =
+ | Sequential
+ | Parallel of pipe
+
+exception Invalid_fd of Unix.file_descr * pipe
+exception Bad_IO of Unix.file_descr * pipe
+
+(** How should I do that? *)
+let fd_of_int : int -> Unix.file_descr = Obj.magic
+let int_of_fd : Unix.file_descr -> int = Obj.magic
+
+let print_fd fmt fd =
+  fprintf fmt "%i" (int_of_fd fd)
+
+let print_pipe fmt pipe =
+  fprintf fmt "%a,%a" print_fd pipe.pin print_fd pipe.pout
+
+let read_makeflags () =
+  (** slave *)
+  try
+    let flags = Sys.getenv "MAKEFLAGS" in
+    let r = Str.regexp "--jobserver-fds=\\([0-9]+\\),\\([0-9]+\\)" in
+    ignore (Str.search_forward r flags 0);
+    Parallel
+      {pin = fd_of_int (int_of_string  (Str.matched_group 1 flags));
+       pout = fd_of_int (int_of_string  (Str.matched_group 2 flags))}
+  with Not_found ->
+      (** No MAKEFLAGS or no --jobserver-fds: sequential*)
+    Sequential
+
+let make_jobserver j =
+  if j <= 1 then
+    invalid_arg "make_serverjob: number of worker must be greater than 1";
+  (** master *)
+  let pin,pout = Unix.pipe () in
+  let pipe = {pin = pin; pout = pout} in
+  let s = String.make 1 '|' in
+  for i = 1 to j do
+    ignore (Unix.write pipe.pout s 0 1)
+  done;
+  pipe
+
+let from_fd_id pin pout =
+  let pipe = {pin = fd_of_int pin; pout = fd_of_int pout} in
+  begin try ignore (Unix.select [pipe.pin] [] [] 0.)
+    with Unix.Unix_error (Unix.EBADF,_,_) ->
+      raise (Invalid_fd (pipe.pin,pipe));
+  end;
+  begin try ignore (Unix.select [] [pipe.pout] [] 0.)
+    with Unix.Unix_error (Unix.EBADF,_,_) ->
+      raise (Invalid_fd (pipe.pout,pipe))
+  end;
+  pipe
+
+(** Wait for a job token *)
+let wait_worker pipe =
+  let s = String.create 1 in
+  let n =
+    try Unix.read pipe.pin s 0 1
+    with Unix.Unix_error(Unix.EBADF,_,_) ->
+      raise (Invalid_fd (pipe.pin,pipe))
+  in
+  if n <> 1 then raise (Bad_IO (pipe.pin,pipe))
+
+(** Give back the job token *)
+let release_worker =
+  let s = String.make 1 '|' in
+  fun pipe ->
+  let n =
+    try Unix.write pipe.pout s 0 1
+    with Unix.Unix_error(Unix.EBADF,_,_) ->
+      raise (Invalid_fd (pipe.pout,pipe))
+  in
+  if n <> 1 then raise (Bad_IO (pipe.pout,pipe))
+
+let print_error fmt = function
+  | Invalid_fd (fd,pipe) ->
+    fprintf fmt "Invalid file descriptor given %a for the pipe (%a)"
+      print_fd fd print_pipe pipe
+  | Bad_IO (fd,pipe) ->
+    fprintf fmt "Bad io for the file descriptor given %a for the pipe (%a)"
+      print_fd fd print_pipe pipe
+  | exn -> raise exn

examples/runstrat/makeproto.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2012                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Guillaume Melquiond                                                 *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software 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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Make protocol for parallelism **)
+type pipe = { pin : Unix.file_descr;
+              pout: Unix.file_descr }
+
+type t =
+ | Sequential
+ | Parallel of pipe
+
+val print_pipe: Format.formatter -> pipe -> unit
+val print_fd: Format.formatter -> Unix.file_descr -> unit
+
+val read_makeflags: unit -> t
+(** Get from the environnement the jobserver created by make *)
+
+val make_jobserver: int -> pipe
+(** create a jobserver with the given number of worker *)
+
+val wait_worker: pipe -> unit
+(** wait for a free worker *)
+
+val release_worker: pipe -> unit
+(** release a worker *)
+
+val from_fd_id : int -> int -> pipe
+
+exception Invalid_fd of Unix.file_descr * pipe
+exception Bad_IO of Unix.file_descr * pipe
+
+val print_error: Format.formatter -> exn -> unit
+(** print the exceptions of this module *)

examples/runstrat/run_wait.ml

+#!/usr/bin/env ocaml
+
+(** a mini-mini-make or mini-mini-sub-make
+    just the protocole for parallelism
+*)
+
+#load "unix.cma";;
+#load "str.cma";;
+
+open Format
+
+
+let print_args fmt arr =
+  for i = 1 to Array.length arr - 1 do
+    fprintf fmt "%s" arr.(i);
+    if i <> Array.length arr - 1
+    then fprintf fmt " "
+  done
+
+let add_id = true
+let create_process cmd args id =
+  if add_id then args.(Array.length args - 1) <- string_of_int id;
+  Unix.create_process cmd args Unix.stdin Unix.stdout Unix.stderr
+
+let cmd = Sys.argv.(3)
+let args =
+  let add_arg = if add_id then 1 else 0 in
+  let t = Array.make (Array.length Sys.argv + add_arg - 3) "" in
+  Array.blit Sys.argv 3 t 0 (Array.length Sys.argv - 3);
+  t
+
+
+let nb_run = max (int_of_string Sys.argv.(2)) 1
+let nb_j = Sys.argv.(1)
+
+type pipe = { pin : Unix.file_descr;
+              pout: Unix.file_descr }
+
+(** How should I do that? *)
+let fd_of_int : int -> Unix.file_descr = Obj.magic
+let int_of_fd : Unix.file_descr -> int = Obj.magic
+
+let pipe =
+  if nb_j = "e" then
+    (** slave *)
+    try
+      let flags = Sys.getenv "MAKEFLAGS" in
+      let r = Str.regexp "--jobserver-fds=\\([0-9]+\\),\\([0-9]+\\)" in
+      ignore (Str.search_forward r flags 0);
+      {pin = fd_of_int (int_of_string  (Str.matched_group 1 flags));
+       pout = fd_of_int (int_of_string  (Str.matched_group 2 flags))}
+    with Not_found ->
+        (** No MAKEFLAGS or no --jobserver-fds: sequential*)
+      for i = 1 to nb_run do
+        let pid = create_process cmd args i in
+        ignore (Unix.waitpid [] pid);
+      done;
+      exit 0
+  else (** number of worker as argument *)
+    (** master *)
+      let pj = try int_of_string nb_j
+        with _ ->
+          eprintf
+            "The first argument must be 'e' or the number of simultaneous \
+         workers@.";
+          exit 1
+      in
+      let pj = max pj 1 in
+      let pin,pout = Unix.pipe () in
+      let pipe = {pin = pin; pout = pout} in
+      let s = String.make 1 '|' in
+      for i = 1 to pj - 1 do (* one for run_wait.ml *)
+        ignore (Unix.write pipe.pout s 0 1)
+      done;
+      pipe
+
+let makejob = "./makejob"
+
+let makejob_args =
+  let t = Array.make (Array.length args + 3) "" in
+  Array.blit args 0 t 3 (Array.length args);
+  t.(0) <- makejob;
+  t.(1) <- string_of_int (int_of_fd pipe.pin);
+  t.(2) <- string_of_int (int_of_fd pipe.pout);
+  t
+
+(* let () = *)
+(*   eprintf "Sys.argv:%a@.args:%a@.makejobs_args:%a@." *)
+(*     print_args Sys.argv *)
+(*     print_args args *)
+(*     print_args makejob_args *)
+
+let () =
+  for i = 1 to nb_run - 1 do
+    ignore (create_process cmd args i)
+  done;
+  ignore (create_process cmd args nb_run);
+  eprintf "run_wait: *** Attente des tâches non terminées....@.";
+  let remaining_child = ref nb_run in
+  while !remaining_child <> 0 do
+    ignore (Unix.wait ()); decr remaining_child;
+  done
+
+
+(*
+
+(** If the arguments are e and e then we should read ourself --jobserver-fds *)
+let () = if Sys.argv.(1) = "d" && Sys.argv.(2) = "d" then
+    try
+      Unix.execv cmd args
+    with Unix.Unix_error(err,_,_) ->
+      eprintf "Can't run exec the program %s:%s@." cmd (Unix.error_message err);
+      exit 1
+
+*)

examples/runstrat/runstrat.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2012                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Guillaume Melquiond                                                 *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software 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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Format
+open Why3
+open Util
+open Whyconf
+open Theory
+open Task
+open Driver
+
+let debug = Debug.register_info_flag
+  ~desc:"information on the run of the stategie" "runstrat"
+
+let () = Exn_printer.register Makeproto.print_error
+
+let usage_msg = sprintf
+  "Usage: %s [options] [[file|-]"
+  (Filename.basename Sys.argv.(0))
+
+let version_msg = sprintf "Why3 personal strat example"
+
+let opt_queue = Queue.create ()
+
+let add_opt_file x =
+  Queue.add x opt_queue
+
+let opt_config = ref None
+let opt_extra = ref []
+let opt_parser = ref None
+
+let opt_provers = ref []
+let add_opt_prover x =
+  opt_provers := x::!opt_provers
+
+let opt_loadpath = ref []
+
+let opt_timelimit = ref None
+let opt_memlimit = ref None
+
+let opt_j = ref None
+
+let option_list = Arg.align [
+  "-", Arg.Unit (fun () -> add_opt_file "-"),
+      " Read the input file from stdin";
+  "-C", Arg.String (fun s -> opt_config := Some s),
+      "<file> Read configuration from <file>";
+  "--config", Arg.String (fun s -> opt_config := Some s),
+      " same as -C";
+  "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
+      "<file> Read additional configuration from <file>";
+  "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
+      "<dir> Add <dir> to the library search path";
+  "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
+      " same as -L";
+  "-I", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
+      " same as -L (obsolete)";
+  "-P", Arg.String add_opt_prover,
+      "<prover> Try to prove the goals with this prover";
+  "--prover", Arg.String add_opt_prover,
+      " same as -P";
+  "-F", Arg.String (fun s -> opt_parser := Some s),
+      "<format> Select input format (default: \"why\")";
+  "--format", Arg.String (fun s -> opt_parser := Some s),
+      " same as -F";
+  "-t", Arg.Int (fun i -> opt_timelimit := Some i),
+      "<sec> Set the prover's time limit (default=10, no limit=0)";
+  "--timelimit", Arg.Int (fun i -> opt_timelimit := Some i),
+      " same as -t";
+  "-m", Arg.Int (fun i -> opt_memlimit := Some i),
+      "<MiB> Set the prover's memory limit (default: no limit)";
+  "--memlimit", Arg.Int (fun i -> opt_timelimit := Some i),
+      " same as -m";
+  "-j", Arg.Int (fun i -> opt_j := Some i),
+  "<int> Set the number of worker to use (default:1)";
+  Debug.Opt.desc_debug_list;
+  Debug.Opt.desc_debug_all;
+  Debug.Opt.desc_debug;
+]
+
+type runnable_prover =
+  { rp_command : string;
+    rp_driver : Driver.driver;
+    rp_prover : Whyconf.prover }
+
+let env,provers = try
+  Arg.parse option_list add_opt_file usage_msg;
+
+  (** Configuration *)
+  let config = read_config !opt_config in
+  let config = List.fold_left merge_config config !opt_extra in
+  let main = get_main config in
+  Whyconf.load_plugins main;
+
+  Debug.Opt.set_flags_selected ();
+
+  (** listings*)
+
+  let opt_list = ref false in
+  opt_list :=  Debug.Opt.option_list () || !opt_list;
+  if !opt_list then exit 0;