Implement and support the gnatprove mode

Factor some code in the runner.

compile_server/app/checker.py

@@ -107,10 +107,10 @@ def check_output(request):
                                     'message': "completed"})
 
 
-def get_example(received_json):
+def get_example():
     """Return the example found in the received json, if any"""
 
-    matches = Example.objects.filter(name=received_json['example_name'])
+    matches = Example.objects.filter(name="Inline Code")
     if not matches:
         return None
     return matches[0]
@@ -152,7 +152,7 @@ def check_program(request):
             {'identifier': '', 'message': "gnatprove not found"})
 
     received_json = json.loads(request.body)
-    e = get_example(received_json)
+    e = get_example()
     if not e:
         return CrossDomainResponse(
             {'identifier': '', 'message': "example not found"})
@@ -199,7 +199,7 @@ def check_program(request):
 @api_view(['POST'])
 def run_program(request):
     received_json = json.loads(request.body)
-    e = get_example(received_json)
+    e = get_example()
     if not e:
         return CrossDomainResponse(
             {'identifier': '', 'message': "example not found"})
@@ -208,7 +208,8 @@ def run_program(request):
     if message:
         return CrossDomainResponse({'identifier': '', 'message': message})
 
-    mode = "run"  # TODO
+    print received_json
+    mode = received_json['mode']
 
     # Check whether we have too many processes running
     if not resources_available():

infrastructure/container_payload/run.py

@@ -80,6 +80,26 @@ def doctor_main_gpr(tempd, main="", spark_mode=False):
         f.write(contents)
 
 
+def extract_main(workdir):
+    """Return the main if it is found in workdir, empty string otherwise"""
+    # Current heuristics for finding the main:
+    # find the .adb that doesn't have a .ads.
+
+    names = [os.path.basename(f)
+             for f in glob.glob(os.path.join(workdir, "*.ad[sb]"))]
+    bases = set([b[:-4] for b in names])
+    mains = [b for b in bases if b + '.ads' not in names]
+    if mains:
+        main = mains[-1]
+        if DEBUG and len(mains) > 1:
+            print "multiple mains found"
+        return main
+    else:
+        if DEBUG:
+            print "No main found"
+        return ''
+
+
 def safe_run(workdir, mode):
     def c(cl=[]):
         """Aux procedure, run the given command line and output to stdout"""
@@ -99,20 +119,7 @@ def safe_run(workdir, mode):
     c(["echo"])
     try:
         if mode == "run":
-            # Current heuristics for finding the main:
-            # find the .adb that doesn't have a .ads.
-            names = [os.path.basename(f)
-                     for f in glob.glob(os.path.join(workdir, "*.ad[sb]"))]
-            bases = set([b[:-4] for b in names])
-            mains = [b for b in bases if b + '.ads' not in names]
-            if mains:
-                main = mains[-1]
-                if DEBUG and len(mains) > 1:
-                    print "multiple mains found"
-            else:
-                print "No main found"
-
-            # Doctor the gpr to put the name of the main in there
+            main = extract_main(workdir)
             doctor_main_gpr(workdir, main, False)
 
             # In "run" mode, first build, and then launch the main
@@ -127,6 +134,15 @@ def safe_run(workdir, mode):
                           os.path.join(workdir, main.split('.')[0]))]
                 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)
+        else:
+            print "mode not implemented"
+
     except Exception:
         traceback.print_exc()