From 317c180aee08f34f11b2fdc7b5ad091d1fd41438 Mon Sep 17 00:00:00 2001
From: Nicolas Setton <setton@adacore.com>
Date: Tue, 5 Jun 2018 12:54:01 -0400
Subject: [PATCH] R525-028 Add support for editors with just a 'Run' button

Enable the running backend (in completely unsafe mode for now)
Code cleanup in editors.js.

For inline editors, do not require an AJAX request to get the
example base, assume everything is provided inline.

Add support for providing shadow files: these will not be displayed
in editors but will be transmitted to the backend.
---
 compile_server/app/checker.py                 |  49 ++-
 compile_server/app/static/editors.js          | 288 ++++++++++--------
 resources/templates/ada_main/example.yaml     |   2 +
 resources/templates/ada_main/main.gpr         |  13 +
 .../spark_main/gnatprove/abdasd.adb.stderr    |   1 -
 .../spark_main/gnatprove/abdasd.adb.stdout    |   0
 .../spark_main/gnatprove/gnatprove.out        |   1 -
 .../templates/spark_main/gnatprove/why3.conf  |  71 -----
 8 files changed, 202 insertions(+), 223 deletions(-)
 create mode 100644 resources/templates/ada_main/example.yaml
 create mode 100644 resources/templates/ada_main/main.gpr
 delete mode 100644 resources/templates/spark_main/gnatprove/abdasd.adb.stderr
 delete mode 100644 resources/templates/spark_main/gnatprove/abdasd.adb.stdout
 delete mode 100644 resources/templates/spark_main/gnatprove/gnatprove.out
 delete mode 100644 resources/templates/spark_main/gnatprove/why3.conf

diff --git a/compile_server/app/checker.py b/compile_server/app/checker.py
index 2d6d2db..ff57ac4 100644
--- a/compile_server/app/checker.py
+++ b/compile_server/app/checker.py
@@ -19,7 +19,7 @@ from compile_server.app.views import CrossDomainResponse
 gnatprove_found = False
 gnatemulator_found = False
 
-ALLOW_RUNNING_PROGRAMS_EVEN_THOUGH_IT_IS_NOT_SECURE = False
+ALLOW_RUNNING_PROGRAMS_EVEN_THOUGH_IT_IS_NOT_SECURE = True
 # TODO: right now, executables are run through gnatemulator. We have not
 # yet done the due diligence to sandbox this, though, so deactivating the
 # run feature through this boolean.
@@ -35,16 +35,6 @@ def check_gnatprove():
     return gnatprove_found
 
 
-def check_gnatemulator():
-    """Check that gnatemulator is found on the PATH"""
-    # Do the check once, for performance
-    global gnatemulator_found
-    if gnatemulator_found:
-        return True
-    gnatemulator_found = distutils.spawn.find_executable("arm-eabi-gnatemu")
-    return gnatemulator_found
-
-
 @api_view(['POST'])
 def check_output(request):
     """Check the output of a running process."""
@@ -153,30 +143,39 @@ def run_program(request):
 
     # Sanity check for the existence of gnatprove
 
-    if not check_gnatemulator():
-        return CrossDomainResponse({'identifier': '',
-                                    'message': "gnatemulator not found"})
-
     received_json = json.loads(request.body)
     e = get_example(received_json)
-    received_json = json.loads(request.body)
-
-    if not e.main:
-        return CrossDomainResponse(
-            {'identifier': '',
-             'message': "example does not have a main"})
-
-    tempd = prep_example_directory(e, received_json)
-    if not tempd:
+    if not e:
         return CrossDomainResponse(
             {'identifier': '', 'message': "example not found"})
 
+    tempd = prep_example_directory(e, received_json)
+
+    # Figure out which is the main
+    if 'main' not in received_json:
+        return CrossDomainResponse(
+            {'identifier': '', 'message': "main not specified"})
+
+    main = received_json['main']
+
+    # 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()
+    with codecs.open(project_file, "wb", encoding="utf-8") as f:
+        f.write(project_str.replace('@MAIN@', main))
+
     # Run the command(s) to check the program
     commands = [
                 ["gprbuild", "-q", "-P", "main"],
-                ["arm-eabi-gnatemu", "-P", "main", e.main],
+                # TODO: implement a safe execute in a container
+                [os.path.join(tempd, main[:-4])],
                ]
 
+    print commands
+
     try:
         p = process_handling.SeparateProcess(commands, tempd)
         message = "running gnatprove"
diff --git a/compile_server/app/static/editors.js b/compile_server/app/static/editors.js
index 72539a0..eb6258f 100644
--- a/compile_server/app/static/editors.js
+++ b/compile_server/app/static/editors.js
@@ -117,6 +117,7 @@ function query_operation_result(container, example_name, editors, output_area, o
 
     files = []
 
+    // Grab the contents from actual editors
     editors.forEach(function (e) {
         files.push({
             'basename': e.basename,
@@ -124,11 +125,23 @@ function query_operation_result(container, example_name, editors, output_area, o
         })
     })
 
+    // Grab the contents from shadow files
+    if (container.shadow_files){
+      container.shadow_files.forEach(function (e){
+        files.push({
+            'basename': e.basename,
+            'contents': e.contents
+            });
+      });
+    }
+
     data = {
         "example_name": example_name,
-        "files": files
+        "files": files,
+        "main": container.attr("main")
     }
 
+
     // request the examples
     $.ajax({
             url: container.example_server + operation_url,
@@ -425,144 +438,169 @@ function create_editor(resource, container, content, editors, counter) {
 
 var unique_id = 0
 
+function fill_editor_from_contents(container, example_name, example_server,
+                                   resources, main) {
+
+   is_inline = container.attr("inline")
+
+   // First create the tabs
+
+   if (!is_inline){
+      var ul = $('<ul class="nav nav-tabs" role="tablist">')
+      ul.appendTo(container);
+
+      var counter = 0;
+
+      json.resources.forEach(function (resource) {
+          counter++;
+          var the_id = "tab_" + container.attr("the_id") + "-" + counter
+
+          var li = $('<li role="presentation" class="' +
+              (counter == 1 ? 'active' : '') +
+              '">').appendTo(ul);
+          $('<a href="#' + the_id + '" aria-controls="' +
+              the_id + '" ' +
+              'id="' + the_id + '-tab"' +
+              'role="tab" data-toggle="tab">' +
+              resource.basename + '</a>').appendTo(li)
+      })
+   }
+
+   // Then fill the contents of the tabs
+
+   var content = $('<div class="tab-content">')
+   content.appendTo(container);
+
+   counter = 0;
+
+   var editors = []
+
+   resources.forEach(function (resource) {
+       counter++;
+       editor = create_editor(resource, container, content, editors, counter)
+       // Append the editor to the list of editors
+       editors.push(editor)
+   })
+
+   var row = $('<div class="row output_row">')
+   row.appendTo(container)
+
+   // create the buttons
+
+   var buttons_div = $('<div class="col-md-3">')
+   buttons_div.appendTo(row)
+
+   var output_div = $('<div class="col-md-9">')
+   output_div.appendTo(row)
+
+   var output_area = $('<div class="output_area">')
+   output_area.appendTo(output_div)
+
+   if (container.attr("prove_button") || container.attr("run_button")){
+      var reset_button = $('<button type="button" class="btn btn-secondary">').text("Reset").appendTo(buttons_div)
+      reset_button.editors = editors;
+      reset_button.on('click', function (x) {
+          output_area.empty();
+          output_area.error_count = 0;
+
+          reset_button.editors.forEach(function (x) {
+              x.setValue(x.initial_contents);
+              x.gotoLine(1);
+          })
+      })
+   }
+
+   if (container.attr("prove_button")){
+      var check_button = $('<button type="button" class="btn btn-primary">').text("Prove").appendTo(buttons_div)
+      check_button.editors = editors;
+      check_button.on('click', function (x) {
+          output_area.empty();
+          output_area.error_count = 0;
+
+          var div = $('<div class="output_info">');
+          div.text("Proving...");
+          div.appendTo(output_area);
+          query_operation_result(container, example_name, check_button.editors, output_area, "/check_program/");
+       })
+   }
+
+   if (container.attr("run_button")){
+       var run_button = $('<button type="button" class="btn btn-primary">').text("Run").appendTo(buttons_div);
+       run_button.editors = editors;
+       run_button.on('click', function (x) {
+           output_area.empty();
+           output_area.error_count = 0;
+
+           var div = $('<div class="output_info">');
+           div.text("Running...");
+           div.appendTo(output_area);
+           query_operation_result(container, example_name, run_button.editors, output_area, "/run_program/");
+       })
+   }
+}
+
 function fill_editor(container, example_name, example_server) {
     unique_id++;
     container.attr("the_id", unique_id);
     container.example_server = example_server;
 
+    is_inline = container.attr("inline");
 
-    // request the examples
-    $.ajax({
-            url: container.example_server + "/example/" + example_name,
-            data: {},
-            type: "GET",
-            // dataType : "json",
-            contentType: 'text/plain',
-            crossDomain: true,
-            //      headers: { "Origin": "http://www.adacore.com" }
+    if (is_inline){
+       // In inline mode, just assume all the sources are here, do not
+       // request them in AJAX
 
-        })
-        .done(function (json) {
-            // On success, create editors for each of the resources
+       // List the "file" divs, add these as resources
+       var resources = []
+       $(container).children(".file").each(function () {
+          // Create a fake resource for each 'file' div
+          a = Object();
+          a.basename = $(this).attr("basename");
+          a.contents = $(this).text();
+          $(this).text('');
+          resources.push(a);
+       })
 
-            $(container).children(".file").each(function () {
-                // Create a fake resource for each 'file' div
-                a = Object();
-                a.basename = $(this).attr("basename");
-                a.contents = $(this).text();
-                $(this).text('');
-                json.resources.push(a);
-            })
+       // List the contents of the ".shadow_file" divs
+       container.shadow_files = []
+       $(container).children(".shadow_file").each(function () {
+          // Create a fake resource for each 'file' div
+          a = Object();
+          a.basename = $(this).attr("basename");
+          a.contents = $(this).text();
+          $(this).text('');
+          container.shadow_files.push(a);
+       })
 
-            // First create the tabs
-            is_inline = container.attr("inline")
+       fill_editor_from_contents(container, example_name, example_server,
+                                 resources, container.attr("main"));
+    } else {
 
-            if (!is_inline){
-               var ul = $('<ul class="nav nav-tabs" role="tablist">')
-               ul.appendTo(container);
+       // request the examples
+       $.ajax({
+               url: container.example_server + "/example/" + example_name,
+               data: {},
+               type: "GET",
+               // dataType : "json",
+               contentType: 'text/plain',
+               crossDomain: true,
+               //      headers: { "Origin": "http://www.adacore.com" }
 
-               var counter = 0;
+           })
+           .done(function (json) {
+               // On success, create editors for each of the resources
 
-               json.resources.forEach(function (resource) {
-                   counter++;
-                   var the_id = "tab_" + container.attr("the_id") + "-" + counter
+               fill_editor_from_contents(container, example_name, example_server,
+                                         json.resources, json.main);
 
-                   var li = $('<li role="presentation" class="' +
-                       (counter == 1 ? 'active' : '') +
-                       '">').appendTo(ul);
-                   $('<a href="#' + the_id + '" aria-controls="' +
-                       the_id + '" ' +
-                       'id="' + the_id + '-tab"' +
-                       'role="tab" data-toggle="tab">' +
-                       resource.basename + '</a>').appendTo(li)
                })
-            }
-
-            // Then fill the contents of the tabs
-
-            var content = $('<div class="tab-content">')
-            content.appendTo(container);
-
-            counter = 0;
-
-            var editors = []
-
-            json.resources.forEach(function (resource) {
-                counter++;
-                editor = create_editor(resource, container, content, editors, counter)
-                // Append the editor to the list of editors
-                editors.push(editor)
-            })
-
-            var row = $('<div class="row output_row">')
-            row.appendTo(container)
-
-            // create the buttons
-
-            var buttons_div = $('<div class="col-md-3">')
-            buttons_div.appendTo(row)
-
-            var reset_button = $('<button type="button" class="btn btn-secondary">').text("Reset").appendTo(buttons_div)
-            reset_button.editors = editors
-
-            var check_button = $('<button type="button" class="btn btn-primary">').text("Prove").appendTo(buttons_div)
-            check_button.editors = editors
-            // Create the output area
-
-            if (json.main) {
-                run_button = $('<button type="button" class="btn btn-primary">').text("Run").appendTo(buttons_div)
-                run_button.editors = editors
-            }
-
-            var output_div = $('<div class="col-md-9">')
-            output_div.appendTo(row)
-
-            var output_area = $('<div class="output_area">')
-            output_area.appendTo(output_div)
-
-            // Connect the buttons
-            reset_button.on('click', function (x) {
-                output_area.empty()
-                output_area.error_count = 0
-
-                reset_button.editors.forEach(function (x) {
-                    x.setValue(x.initial_contents)
-                    x.gotoLine(1)
-                })
-            })
-
-            check_button.on('click', function (x) {
-                output_area.empty()
-                output_area.error_count = 0
-
-                var div = $('<div class="output_info">')
-                div.text("Proving...")
-                div.appendTo(output_area)
-                query_operation_result(container, example_name, check_button.editors, output_area, "/check_program/")
-            })
-
-            if (json.main) {
-                run_button.on('click', function (x) {
-                    output_area.empty()
-                    output_area.error_count = 0
-
-                    var div = $('<div class="output_info">')
-                    div.text("Running...")
-                    div.appendTo(output_area)
-                    query_operation_result(container, example_name, check_button.editors, output_area, "/run_program/")
-                })
-            }
-        })
-        .fail(function (xhr, status, errorThrown) {
-            //
-            alert("could not download the example");
-            console.log("Error: " + errorThrown);
-            console.log("Status: " + status);
-            console.dir(xhr);
-        });
-    // Code to run regardless of success or failure;
-    // commented for now - just so I remember how it's done
-    // .always(function( xhr, status ) {});
+           .fail(function (xhr, status, errorThrown) {
+               alert("could not download the example");
+               console.log("Error: " + errorThrown);
+               console.log("Status: " + status);
+               console.dir(xhr);
+           });
+        }
 }
 
 
diff --git a/resources/templates/ada_main/example.yaml b/resources/templates/ada_main/example.yaml
new file mode 100644
index 0000000..772e99a
--- /dev/null
+++ b/resources/templates/ada_main/example.yaml
@@ -0,0 +1,2 @@
+name: Ada Main
+description: Simple overrideable runnable main
diff --git a/resources/templates/ada_main/main.gpr b/resources/templates/ada_main/main.gpr
new file mode 100644
index 0000000..6537074
--- /dev/null
+++ b/resources/templates/ada_main/main.gpr
@@ -0,0 +1,13 @@
+project Main is
+
+   for Main use ("@MAIN@");
+
+   package Compiler is
+      for Switches ("ada") use ("-g");
+   end Compiler;
+
+   package Builder is
+      for Switches ("ada") use ("-g", "-O0");
+   end Builder;
+
+end Main;
diff --git a/resources/templates/spark_main/gnatprove/abdasd.adb.stderr b/resources/templates/spark_main/gnatprove/abdasd.adb.stderr
deleted file mode 100644
index 09b0a52..0000000
--- a/resources/templates/spark_main/gnatprove/abdasd.adb.stderr
+++ /dev/null
@@ -1 +0,0 @@
-abdasd.adb:1:01: compilation unit expected
diff --git a/resources/templates/spark_main/gnatprove/abdasd.adb.stdout b/resources/templates/spark_main/gnatprove/abdasd.adb.stdout
deleted file mode 100644
index e69de29..0000000
diff --git a/resources/templates/spark_main/gnatprove/gnatprove.out b/resources/templates/spark_main/gnatprove/gnatprove.out
deleted file mode 100644
index 8b13789..0000000
--- a/resources/templates/spark_main/gnatprove/gnatprove.out
+++ /dev/null
@@ -1 +0,0 @@
-
diff --git a/resources/templates/spark_main/gnatprove/why3.conf b/resources/templates/spark_main/gnatprove/why3.conf
deleted file mode 100644
index b3c4b2b..0000000
--- a/resources/templates/spark_main/gnatprove/why3.conf
+++ /dev/null
@@ -1,71 +0,0 @@
-[main]
-magic =  14
-memlimit =  0
-[editor coqide]
-name = "CoqIDE"
-command = "coqide -I %l/coq-tactic -R %o/why3_libs/coq Why3 %f"
-[prover]
-command = "alt-ergo -max-split 5 %f"
-command_steps = "alt-ergo -steps-bound %S -max-split 5 %f"
-driver = "alt-ergo_gnatprove.drv"
-name = "altergo"
-shortcut = "altergo"
-version = "1.30-gnatprove"
-[prover]
-command = "cvc4 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
-command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
-driver = "cvc4_gnatprove.drv"
-name = "CVC4"
-shortcut = "cvc4"
-version = "1.6-gnatprove"
-[prover]
-command = "cvc4 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
-command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
-driver = "cvc4_gnatprove_extra_axioms.drv"
-name = "CVC4_More_Axioms"
-shortcut = "cvc4_axioms"
-version = "1.6-gnatprove"
-[prover]
-command = "cvc4 --lang=smt2 --stats --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
-command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 %f"
-driver = "cvc4_gnatprove_qf.drv"
-name = "CVC4_QF"
-shortcut = "cvc4_qf"
-version = "1.6-gnatprove"
-[prover]
-command = "cvc4 --tlimit-per=%t000 --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 --macros-quant --quiet %f"
-command_steps = "cvc4 --rlimit=%S --lang=smt2 --stats --no-cond-rewrite-quant --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 --macros-quant --quiet %f"
-driver = "cvc4_gnatprove_ce.drv"
-name = "CVC4_CE"
-shortcut = "cvc4_ce"
-version = "1.6-gnatprove"
-[prover]
-command = "z3 -smt2 -st %f"
-command_steps = "z3 rlimit=%S -smt2 -st %f"
-driver = "z3_gnatprove.drv"
-name = "Z3"
-shortcut = "z3"
-version = "4.5.1-gnatprove"
-[prover]
-command = "z3 -smt2 -st %f"
-command_steps = "z3 rlimit=%S -smt2 -st %f"
-driver = "z3_no_quant.drv"
-name = "Z3_noquant"
-shortcut = "z3_noquant"
-version = "4.5.1-gnatprove"
-[prover]
-command = "z3 -t:%t -smt2 -st %f"
-command_steps = "z3 rlimit=%S -smt2 -st %f"
-driver = "z3_gnatprove_ce.drv"
-name = "z3_ce"
-shortcut = "z3_ce"
-version = "4.5.1-gnatprove"
-[prover]
-command = "coqtop -batch -I %l/coq-tactic -R %o/why3_libs/coq Why3 -l %f"
-driver = "coq_gnatprove.drv"
-name = "Coq"
-shortcut = "coq"
-version = "8.5pl2"
-interactive = true
-editor = "coqide"
-in_place = false