runtest: accept all options from the prover/loader group

Fix #506

.github/workflows/ci.yml

@@ -35,7 +35,7 @@ jobs:
         opam pin add -n easycrypt .
         opam install --deps-only easycrypt
     - name: Compile EasyCrypt
-      run: opam config exec -- make
+      run: opam exec -- make
 
   compile-nix:
     name: EasyCrypt compilation (nix)
@@ -78,15 +78,15 @@ jobs:
         opam pin add -n easycrypt .
         opam install --deps-only easycrypt
     - name: Compile EasyCrypt
-      run: opam config exec -- make
+      run: opam exec -- make
     - name: Detect SMT provers
       run: |
         rm -f ~/.why3.conf
-        opam config exec -- ./ec.native why3config -why3 ~/.why3.conf
+        opam exec -- ./ec.native why3config -why3 ~/.why3.conf
     - name: Compile Library (${{ matrix.target }})
       env:
         TARGET: ${{ matrix.target }}
-      run: opam config exec -- make $TARGET
+      run: opam exec -- make $TARGET
     - uses: actions/upload-artifact@v3
       name: Upload report.log
       if: always()
@@ -105,7 +105,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        target: [ [ 'jasmin-eclib', 'jasmin-lang/jasmin', 'eclib', 'tests.config', 'jasmin', '-p [email protected] -p [email protected]' ] ]
+        target: [ [ 'jasmin-eclib', 'jasmin-lang/jasmin', 'eclib', 'tests.config', 'jasmin' ] ]
     steps:
     - uses: actions/checkout@v3
       with:
@@ -120,14 +120,14 @@ jobs:
         opam pin add -n easycrypt easycrypt
         opam install --deps-only easycrypt
     - name: Compile & Install EasyCrypt
-      run: opam config exec -- make -C easycrypt build install
+      run: opam exec -- make -C easycrypt build install
     - name: Detect SMT provers
       run: |
         rm -f ~/.why3.conf ~/.config/easycrypt/why3.conf
-        opam config exec -- easycrypt why3config
+        opam exec -- easycrypt why3config
     - name: Compile project
       working-directory: project/${{ matrix.target[2] }}
-      run: opam config exec -- ec-runtest ${{ matrix.target[5] }} ${{ matrix.target[3] }} ${{ matrix.target[4] }}
+      run: opam exec -- easycrypt runtest ${{ matrix.target[3] }} ${{ matrix.target[4] }}
     - uses: actions/upload-artifact@v3
       name: Upload report.log
       if: always()

Makefile

@@ -9,9 +9,11 @@ ECEXTRA   ?= --report=report.log
 ECPROVERS ?= [email protected] [email protected] [email protected]
 CHECKPY   ?=
 CHECK     := $(CHECKPY) scripts/testing/runtest
-CHECK     += --bin=./ec.native --bin-args="$(ECARGS)"
-CHECK     += --bin-args="$(ECPROVERS:%=-p %)"
-CHECK     += --timeout="$(ECTOUT)" --jobs="$(ECJOBS)"
+CHECK     += --bin=./ec.native
+CHECK     += --jobs="$(ECJOBS)"
+CHECK     += $(foreach prover,$(ECPROVERS),--bin-args=-p --bin-args="$(prover)")
+CHECK     += --bin-args=-timeout --bin-args="$(ECTOUT)"
+CHECK     += $(foreach arg,$(ECARGS),--bin-args="$(arg)")
 CHECK     += $(ECEXTRA) config/tests.config
 NIX       ?= nix --extra-experimental-features "nix-command flakes"
 

scripts/testing/runtest

@@ -92,14 +92,6 @@ def _options():
         default = [],
         help    = 'append ARGS to EasyCrypt command (cumulative)')
 
-    parser.add_option(
-        '', '--timeout',
-        action  = 'store',
-        default = None,
-        metavar = 'TIMEOUT',
-        type    = 'int',
-        help    = 'set the timeout option to pass to EasyCrypt')
-
     parser.add_option(
         '', '--jobs',
         action  = 'store',
@@ -114,20 +106,6 @@ def _options():
         default = False,
         help    = 'add timing statistics')
 
-    parser.add_option(
-        '-p', '--provers',
-        action  = 'append',
-        metavar = 'PROVERS',
-        default = None,
-        help    = 'Add a prover to the set of activated provers')
-
-    parser.add_option(
-        '', '--why3',
-        action  = 'store',
-        metavar = 'WHY3',
-        default = None,
-        help    = 'Why3 configuration file')
-
     parser.add_option(
         '', '--report',
         action  = 'store',
@@ -140,20 +118,13 @@ def _options():
     if len(args) < 1:
         parser.error('this program takes at least one argument')
 
-    if cmdopt.timeout is not None:
-        if cmdopt.timeout <= 0:
-            parser.error('timeout must be positive')
-
     if cmdopt.jobs is not None:
         if cmdopt.jobs < 0:
             parser.error('jobs must be non-negative')
 
     options = Object(scenarios = dict())
-    options.timeout  = cmdopt.timeout
     options.timing   = cmdopt.timing
-    options.why3     = cmdopt.why3
     options.jobs     = cmdopt.jobs
-    options.provers  = cmdopt.provers
     options.report   = cmdopt.report
 
     defaults = dict(
@@ -189,8 +160,7 @@ def _options():
         options.report = config.get('default', 'report', fallback = None)
 
     if cmdopt.bin_args:
-        options.args.extend(itertools.chain.from_iterable( \
-          x.split() for x in cmdopt.bin_args))
+        options.args.extend(cmdopt.bin_args)
 
     def _parse_timeout(x):
         m = re.search(r'^(.*):(\d+)$', x)
@@ -695,13 +665,6 @@ async def _run_all(options, allscripts, listener : Listener):
     async def runcheck(config):
         async with semaphore:
             command = [options.bin] + options.args + config.args
-            if options.timeout:
-                command.extend(['-timeout', str(options.timeout)])
-            if options.provers:
-                for prover in options.provers:
-                    command.extend(['-p', prover])
-            if options.why3:
-                command.extend(['-why3', options.why3])
             if options.timing:
                 tfilename = os.path.join(
                     TIMING_DIR, os.path.splitext(config.filename)[0] + '.stats')

src/ec.ml

@@ -197,16 +197,101 @@ let main () =
           | None ->
               Sites.commands in
         let cmd  = Filename.concat root "runtest" in
+
+        let ecargs =
+          let maxjobs =
+            input.runo_provers.prvo_maxjobs
+            |> omap (fun i -> ["-max-provers"; string_of_int i])
+            |> odfl [] in
+
+          let timeout =
+            input.runo_provers.prvo_timeout
+            |> omap (fun i -> ["-timeout"; string_of_int i])
+            |> odfl [] in
+
+          let cpufactor =
+            input.runo_provers.prvo_cpufactor
+            |> omap (fun i -> ["-cpu-factor"; string_of_int i])
+            |> odfl [] in
+
+          let ppwidth =
+            input.runo_provers.prvo_ppwidth
+            |> omap (fun i -> ["-pp-width"; string_of_int i])
+            |> odfl [] in
+
+          let provers =
+            odfl [] input.runo_provers.prvo_provers
+            |> List.map (fun prover -> ["-p"; prover])
+            |> List.flatten in
+
+          let pragmas =
+            input.runo_provers.prvo_pragmas
+            |> List.map (fun pragmas -> ["-pragmas"; pragmas])
+            |> List.flatten  in
+
+          let checkall =
+            if input.runo_provers.prvo_checkall then
+              ["-check-all"]
+            else [] in
+
+          let profile =
+            if input.runo_provers.prvo_profile then
+              ["-profile"]
+            else [] in
+
+          let iterate =
+            if input.runo_provers.prvo_iterate then
+              ["-iterate"]
+            else [] in
+
+          let why3srv =
+            input.runo_provers.prvo_why3server
+            |> omap (fun server -> ["-server"; server])
+            |> odfl [] in
+
+          let why3 =
+            options.o_options.o_why3
+            |> omap (fun why3 -> ["-why3"; why3])
+            |> odfl [] in
+
+          let reloc =
+            if options.o_options.o_reloc then
+              ["-reloc"]
+            else [] in
+
+          let noevict =
+            options.o_options.o_ovrevict
+            |> List.map (fun p -> ["-no-evict"; p])
+            |> List.flatten in
+
+          let boot =
+            if options.o_options.o_loader.ldro_boot then
+              ["-boot"]
+            else [] in
+
+          let idirs =
+            options.o_options.o_loader.ldro_idirs
+            |> List.map (fun (pfx, name, rec_) ->
+                 let pfx = odfl "" (omap (fun pfx -> pfx ^ ":") pfx) in
+                 let opt = if rec_ then "-R" else "-I" in
+                 [opt; pfx ^ name])
+            |> List.flatten in
+
+
+          List.flatten [
+            maxjobs; timeout; cpufactor; ppwidth;
+            provers; pragmas; checkall ; profile;
+            iterate; why3srv; why3     ; reloc  ;
+            noevict; boot   ; idirs    ;
+          ]
+        in
+
         let args =
             [
               "runtest";
               Format.sprintf "--bin=%s" Sys.executable_name;
             ]
-          @ (List.flatten
-               (List.map
-                  (fun x -> ["-p"; x])
-                  (odfl [] input.runo_provers)))
-          @ (otolist (omap (Format.sprintf "--why3=%s") options.o_options.o_why3))
+          @ List.map (Format.sprintf "--bin-args=%s") ecargs
           @ [input.runo_input]
           @ input.runo_scenarios
         in
@@ -451,9 +536,9 @@ let main () =
             (* Initialize global scope *)
             let checkmode = {
               EcCommands.cm_checkall  = prvopts.prvo_checkall;
-              EcCommands.cm_timeout   = prvopts.prvo_timeout;
-              EcCommands.cm_cpufactor = prvopts.prvo_cpufactor;
-              EcCommands.cm_nprovers  = prvopts.prvo_maxjobs;
+              EcCommands.cm_timeout   = odfl 3 (prvopts.prvo_timeout);
+              EcCommands.cm_cpufactor = odfl 1 (prvopts.prvo_cpufactor);
+              EcCommands.cm_nprovers  = odfl 4 (prvopts.prvo_maxjobs);
               EcCommands.cm_provers   = prvopts.prvo_provers;
               EcCommands.cm_profile   = prvopts.prvo_profile;
               EcCommands.cm_iterate   = prvopts.prvo_iterate;