From 256712dfda2a754ee88895a67ca7c58ce0d40ce4 Mon Sep 17 00:00:00 2001 From: Nicolas Setton Date: Fri, 25 Jan 2019 11:24:40 -0500 Subject: [PATCH] Move the doctoring of .gpr / definition of main to the runner One more step to simplify the handling being done at the server level. --- compile_server/app/checker.py | 69 +---------------------- infrastructure/container_payload/run.py | 75 +++++++++++++++++++++++-- 2 files changed, 71 insertions(+), 73 deletions(-) diff --git a/compile_server/app/checker.py b/compile_server/app/checker.py index 6633dfd..559001d 100644 --- a/compile_server/app/checker.py +++ b/compile_server/app/checker.py @@ -56,23 +56,6 @@ PROCESSES_LIMIT = 300 # The limit of processes that can be running RECEIVED_FILE_CHAR_LIMIT = 50 * 1000 # The limit in number of characters of files to accept -COMMON_ADC = """ -pragma Restrictions (No_Specification_of_Aspect => Import); -pragma Restrictions (No_Use_Of_Pragma => Import); -pragma Restrictions (No_Use_Of_Pragma => Interface); -pragma Restrictions (No_Dependence => System.Machine_Code); -pragma Restrictions (No_Dependence => Machine_Code); -""" - -SPARK_ADC = """ -pragma Profile(GNAT_Extended_Ravenscar); -pragma Partition_Elaboration_Policy(Sequential); -pragma SPARK_Mode (On); -pragma Warnings (Off, "no Global contract available"); -pragma Warnings (Off, "subprogram * has no effect"); -pragma Warnings (Off, "file name does not match"); -""" - def check_gnatprove(): """Check that gnatprove is found on the PATH""" @@ -159,46 +142,6 @@ def prep_example_directory(example, received_json): return (tempd, None) -def get_main(received_json): - """Retrieve the main information from the json""" - - # Figure out which is the main - if 'main' not in received_json: - return None - - return received_json['main'] - - -def doctor_main_gpr(tempd, main="", spark_mode=False): - """Doctor the main.gpr to replace the placeholder with the name of the - main, and the .adc configuration file for SPARK. - - See template "inline_code". - """ - # In the temporary directory, doctor the project file to know about the - # main. - - project_file = os.path.join(tempd, "main.gpr") - with codecs.open(project_file, "rb", encoding="utf-8") as f: - project_str = f.read() - - if main: - project_str = project_str.replace( - "--MAIN_PLACEHOLDER--", - 'for Main use ("{}");'.format(main)) - - with codecs.open(project_file, "wb", encoding="utf-8") as f: - f.write(project_str) - - # Create the main.adc file - adc_file = os.path.join(tempd, "main.adc") - contents = COMMON_ADC - if spark_mode: - contents += '\n' + SPARK_ADC - with open(adc_file, "wb") as f: - f.write(contents) - - @api_view(['POST']) def check_program(request): @@ -224,7 +167,6 @@ def check_program(request): if message: return CrossDomainResponse({'identifier': '', 'message': message}) - main = get_main(received_json) doctor_main_gpr(tempd, main, True) # Run the command(s) to check the program @@ -266,21 +208,14 @@ def run_program(request): if message: return CrossDomainResponse({'identifier': '', 'message': message}) - main = get_main(received_json) mode = "run" # TODO - if not main: - return CrossDomainResponse( - {'identifier': '', 'message': "main not specified"}) - # Check whether we have too many processes running if not resources_available(): return CrossDomainResponse( {'identifier': '', 'message': "the machine is busy processing too many requests"}) - doctor_main_gpr(tempd, main) - # Push the code to the container try: @@ -299,8 +234,8 @@ def run_program(request): # Run the program ["lxc", "exec", "safecontainer", "--", "su", "runner", "-c", - "python /workspace/run.py /workspace/sessions/{} {} {}".format( - os.path.basename(tempd), mode, main)] + "python /workspace/run.py /workspace/sessions/{} {}".format( + os.path.basename(tempd), mode)] ] print "\n".join(" ".join(c) for c in commands) diff --git a/infrastructure/container_payload/run.py b/infrastructure/container_payload/run.py index a4a0e78..4eb65e7 100644 --- a/infrastructure/container_payload/run.py +++ b/infrastructure/container_payload/run.py @@ -8,6 +8,8 @@ """ import os +import codecs +import glob import time import sys import subprocess @@ -19,6 +21,24 @@ INTERRUPT_RETURNCODE = 124 DEBUG = False +COMMON_ADC = """ +pragma Restrictions (No_Specification_of_Aspect => Import); +pragma Restrictions (No_Use_Of_Pragma => Import); +pragma Restrictions (No_Use_Of_Pragma => Interface); +pragma Restrictions (No_Dependence => System.Machine_Code); +pragma Restrictions (No_Dependence => Machine_Code); +""" + +SPARK_ADC = """ +pragma Profile(GNAT_Extended_Ravenscar); +pragma Partition_Elaboration_Policy(Sequential); +pragma SPARK_Mode (On); +pragma Warnings (Off, "no Global contract available"); +pragma Warnings (Off, "subprogram * has no effect"); +pragma Warnings (Off, "file name does not match"); +""" + + def run(command): if DEBUG: print ">", " ".join(command) @@ -30,7 +50,37 @@ def run(command): return output -def safe_run(workdir, mode, main): +def doctor_main_gpr(tempd, main="", spark_mode=False): + """Doctor the main.gpr to replace the placeholder with the name of the + main, and the .adc configuration file for SPARK. + + See template "inline_code". + """ + # In the temporary directory, doctor the project file to know about the + # main. + + project_file = os.path.join(tempd, "main.gpr") + with codecs.open(project_file, "rb", encoding="utf-8") as f: + project_str = f.read() + + if main: + project_str = project_str.replace( + "--MAIN_PLACEHOLDER--", + 'for Main use ("{}");'.format(main)) + + with codecs.open(project_file, "wb", encoding="utf-8") as f: + f.write(project_str) + + # Create the main.adc file + adc_file = os.path.join(tempd, "main.adc") + contents = COMMON_ADC + if spark_mode: + contents += '\n' + SPARK_ADC + with open(adc_file, "wb") as f: + f.write(contents) + + +def safe_run(workdir, mode): def c(cl=[]): """Aux procedure, run the given command line and output to stdout""" try: @@ -49,9 +99,25 @@ def safe_run(workdir, mode, main): 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[0] + if DEBUG and len(mains) > 1: + print "multiple mains found" + + # Doctor the gpr to put the name of the main in there + doctor_main_gpr(workdir, main, False) + # In "run" mode, first build, and then launch the main if c(["gprbuild", "-q", "-P", "main"]): - if main: + main = None + + for main in mains: # We run: # - as user 'unprivileged' that has no write access # - under a timeout @@ -76,11 +142,8 @@ if __name__ == '__main__': # be launched interactively workdir = sys.argv[1] mode = sys.argv[2] - main = "" - if len(sys.argv) > 3: - main = sys.argv[3] # This is where the compiler is installed os.environ["PATH"] = "/gnat/bin:{}".format(os.environ["PATH"]) - safe_run(workdir, mode, main) + safe_run(workdir, mode)