Ajout de why-cpulimit

Makefile.in

@@ -87,7 +87,9 @@ GENERATED = src/version.ml src/parser/parser.mli src/parser/parser.ml \
 BINARY=bin/why.$(OCAMLBEST)
 BINARYL=bin/whyl.$(OCAMLBEST)
 
-all: .depend $(BINARY) $(BINARYL)
+TOOLS=bin/why-cpulimit
+
+all: .depend $(BINARY) $(BINARYL) $(TOOLS)
 
 # refrain parallel make (-j nn) from starting ocaml compilation too early 
 *.cm*: .depend
@@ -160,7 +162,7 @@ bin/why.static: $(CMX) src/why.cmx
 bin/top: $(CMO)
 	ocamlmktop $(BFLAGS) -o $@ nums.cma $^
 
-test: bin/why.byte
+test: bin/why.byte  $(TOOLS)
 	mkdir -p output_why3
 	ocamlrun -bt bin/why.byte -I theories/ --driver drivers/why3.drv \
 		--output-dir output_why3 --all-goals src/test.why
@@ -189,6 +191,12 @@ bin/whyl.opt: $(WHYL_CMX)
 bin/whyl.byte: $(WHYL_CMO) 
 	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ nums.cma $^
 
+#tools
+######
+
+bin/why-cpulimit: src/tools/@CPULIMIT@.c
+	$(CC) -o $@ $^
+
 # graphical interface
 #####################
 
@@ -223,7 +231,7 @@ WHYVO=lib/coq/Why.vo
 bench/bench : bench/bench.in config.status
 	./config.status --file bench/bench
 
-bench:: $(BINARY) bench/bench
+bench:: $(BINARY) bench/bench $(TOOLS)
 	sh bench/bench "$(BINARY) -I theories/"
 
 BENCH_PLUGINS_CMO := helloworld.cmo simplify_array.cmo
@@ -232,7 +240,8 @@ BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)
 
 
 
-bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte
+bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte \
+	$(TOOLS)
 	bin/why.byte --driver bench/plugins/helloworld.drv -I theories/ \
         --output-file - --goal Test.G src/test.why
 	bin/why.$(OCAMLBEST) --driver bench/plugins/helloworld.drv -I theories/ \

src/driver/call_provers.ml

@@ -59,7 +59,9 @@ exception NoCommandlineProvided
 
 
 (* this should be replaced by a proper use of fork/waitpid() *)
-let cpulimit_commands = ["why-cpulimit"; "timeout"]
+let dirname = Filename.dirname Sys.argv.(0)
+let cpulimit_local = Filename.concat dirname "why-cpulimit"
+let cpulimit_commands = ["why-cpulimit"; cpulimit_local(* ; "timeout"*)]
 let cpulimit = ref (
   let tmp = ref "" in
   try

src/tools/cpulimit-win.c

+/**************************************************************************/
+/*                                                                        */
+/*  Copyright (C) 2008                                                    */
+/*    Dillon PARIENTE                                                     */
+/*                                                                        */
+/*  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, 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.                  */
+/*                                                                        */
+/**************************************************************************/
+
+/* $Id: cpulimit-win.c,v 1.3 2009-12-09 08:28:00 nrousset Exp $ */
+
+#include <windows.h>
+#include <stdio.h>
+#include <errno.h>
+
+int main(int argc, char *argv[]) {
+  STARTUPINFO si;
+  PROCESS_INFORMATION pi;
+  int i;
+  unsigned ex;
+  unsigned long s = 0; // length of args after concat
+  char * p; // command line parameter
+  ZeroMemory(&si, sizeof(si));
+  si.cb = sizeof(si);
+  ZeroMemory(&pi, sizeof(pi));
+  if (argc < 3) {
+    printf("Usage: %s <time limit in seconds> <command>\n", argv[0]);
+    return -1;
+  }
+  // concats argv[2..] into a single command line parameter
+  for (i = 2; i < argc; i++)
+    s += strlen(argv[i]) + 1;
+  // CreateProcess does not allow more than 32767 bytes for command line parameter
+  if (s > 32767) { 
+    printf("%s: Error: parameter's length exceeds CreateProcess limits\n", argv[0]);
+    return -1;
+  }
+  p = (char*) malloc(s);
+  if (p == NULL) {
+    printf("%s: Error: when allocating %d bytes in memory\n", argv[0], (int) s);
+    return -1;
+  }
+  for (i = 2; i < argc; i++) {
+    strncat(p, argv[i], strlen(argv[i])); 
+    if (i < argc - 1) strcat(p, " ");
+  }
+  // launches "child" process with command line parameter
+  if (!CreateProcess(NULL, p, NULL, NULL, FALSE, 0, NULL, NULL, &si, &pi)) {
+    printf( "%s: Error: failed when launching <%s>\n", argv[0], p);
+    return -1;
+  }
+  // waits, terminates and frees handles and malloc
+  int w = WaitForSingleObject(pi.hProcess, 1000 * atoi(argv[1]));
+  TerminateProcess(pi.hProcess, 10);
+  GetExitCodeProcess(pi.hProcess, (LPDWORD) &ex);
+  CloseHandle(pi.hProcess);
+  CloseHandle(pi.hThread);
+  free(p);
+  if (w == WAIT_TIMEOUT) return 152;
+  return ex;
+}
+
+// How to compile under Cygwin (needs make, gcc and win32api):
+// 		gcc -Wall -o cpulimit cpulimit.c

src/tools/cpulimit.c

+/**************************************************************************/
+/*                                                                        */
+/*  The Why platform for program certification                            */
+/*  Copyright (C) 2002-2008                                               */
+/*    Romain BARDOU                                                       */
+/*    Jean-Franois COUCHOT                                               */
+/*    Mehdi DOGGUY                                                        */
+/*    Jean-Christophe FILLITRE                                           */
+/*    Thierry HUBERT                                                      */
+/*    Claude MARCH                                                       */
+/*    Yannick MOY                                                         */
+/*    Christine PAULIN                                                    */
+/*    Yann RGIS-GIANAS                                                   */
+/*    Nicolas ROUSSET                                                     */
+/*    Xavier URBAIN                                                       */
+/*                                                                        */
+/*  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, 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.                  */
+/*                                                                        */
+/**************************************************************************/
+
+#include <sys/types.h>
+#include <sys/time.h>
+#include <sys/resource.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <unistd.h>
+#include <errno.h>
+
+
+int main(int argc, char *argv[]) {
+  int limit;
+  struct rlimit res;
+
+  if (argc < 3) {
+    fprintf(stderr,"usage: %s <time limit in seconds> <command>\n",argv[0]);
+    return 1;
+  }
+  /* get time limit in seconds from command line */
+  limit = atoi(argv[1]);
+
+  /* set the CPU limit */
+  getrlimit(RLIMIT_CPU,&res);
+  res.rlim_cur = limit;
+  setrlimit(RLIMIT_CPU,&res);
+    
+  /* exec the command */
+  execvp(argv[2],argv+2);
+  fprintf(stderr,"%s: %s:command not found",argv[0],argv[2]);
+  return errno;
+}