Implement the 'flow' and 'full' SPARK modes in the runner

Move the handling of extra args completely to the runner.

compile_server/app/checker.py

@@ -46,11 +46,6 @@ from compile_server.app.views import CrossDomainResponse
 
 gnatprove_found = False
 
-ALLOWED_EXTRA_ARGS = {'spark-flow': "--mode=flow",
-                      'spark-report-all': "--report=all"}
-# We maintain a list of extra arguments that can be passed to the command
-# line. For security we don't want the user to pass arguments as-is.
-
 PROCESSES_LIMIT = 300  # The limit of processes that can be running
 
 RECEIVED_FILE_CHAR_LIMIT = 50 * 1000
@@ -173,14 +168,6 @@ def check_program(request):
     command = ["gnatprove", "-P", "main", "--checks-as-errors",
                "--level=0", "--no-axiom-guard"]
 
-    # Process extra_args
-    if 'extra_args' in received_json:
-        extra_args = received_json['extra_args']
-        if extra_args:
-            if extra_args not in ALLOWED_EXTRA_ARGS:
-                return CrossDomainResponse(
-                    {'identifier': '', 'message': "extra_args not known"})
-            command.append(ALLOWED_EXTRA_ARGS[extra_args])
     print " ".join(command)
     try:
         p = process_handling.SeparateProcess([command], tempd)

infrastructure/container_payload/run.py

@@ -118,8 +118,9 @@ def safe_run(workdir, mode):
 
     c(["echo"])
     try:
+        main = extract_main(workdir)
+
         if mode == "run":
-            main = extract_main(workdir)
             doctor_main_gpr(workdir, main, False)
 
             # In "run" mode, first build, and then launch the main
@@ -135,11 +136,22 @@ def safe_run(workdir, mode):
                 c(line)
 
         elif mode == "prove":
-            main = extract_main(workdir)
             doctor_main_gpr(workdir, main, spark_mode=True)
             line = ["gnatprove", "-P", "main", "--checks-as-errors",
                     "--level=0", "--no-axiom-guard"]
             c(line)
+        elif mode == "prove_flow":
+            doctor_main_gpr(workdir, main, spark_mode=True)
+            line = ["gnatprove", "-P", "main", "--checks-as-errors",
+                    "--level=0", "--no-axiom-guard", "--mode=flow"]
+            c(line)
+
+        elif mode == "prove_report_all":
+            doctor_main_gpr(workdir, main, spark_mode=True)
+            line = ["gnatprove", "-P", "main", "--checks-as-errors",
+                    "--level=0", "--no-axiom-guard", "--report=all"]
+            c(line)
+
         else:
             print "mode not implemented"
 
@@ -149,7 +161,8 @@ def safe_run(workdir, mode):
     finally:
         if os.path.isdir(workdir):
             time.sleep(0.2)  # Time for the filesystem to sync
-            c(["rm", "-rf", workdir])
+            if not DEBUG:
+                c(["rm", "-rf", workdir])
 
 
 if __name__ == '__main__':