From 519dbe2d4a1536568b98df8b4cd9f9763dc7687f Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 22 Jul 2016 14:09:32 +0200 Subject: [PATCH 1/2] Provide formal verification input. --- assets/css/browser-solidity.css | 6 ++++++ index.html | 14 ++++++++++++++ src/app.js | 4 +++- src/app/compiler.js | 6 +++++- src/app/formalVerification.js | 30 ++++++++++++++++++++++++++++++ src/app/renderer.js | 9 ++++++--- 6 files changed, 64 insertions(+), 5 deletions(-) create mode 100644 src/app/formalVerification.js diff --git a/assets/css/browser-solidity.css b/assets/css/browser-solidity.css index b6b31f0cf8..1e3f5d4ca0 100644 --- a/assets/css/browser-solidity.css +++ b/assets/css/browser-solidity.css @@ -209,6 +209,7 @@ body { #header #optionViews.publishView #publishView { display: block; } #header #optionViews.envView #envView { display: block; } #header #optionViews.debugView #debugView { display: block; } +#header #optionViews.verificationView #verificationView { display: block; } #header #optionViews.txView input, #header #optionViews.txView select { @@ -273,6 +274,11 @@ body { float: left; } +#formalVerificationInput { + height: 4.5em; + width: 100%; +} + .contract.hide { padding-bottom: 0; } diff --git a/index.html b/index.html index ce27d99a5e..ed660a6058 100644 --- a/index.html +++ b/index.html @@ -65,6 +65,7 @@
    • +
    • Solidity realtime compiler and runtime @@ -125,6 +126,19 @@
    +
    +

    This tab provides support for formal verification of Solidity contracts.
    + This feature is still in development and thus also not yet well documented, + but you can find some information + here. + The compiler generates input to be verified + (or report errors). Please paste the text below into + http://why3.lri.fr/try/ + to actually perform the verification. + We plan to support direct integration in the future.

    + +
    +
    diff --git a/src/app.js b/src/app.js index 3a2b613075..c1bb982944 100644 --- a/src/app.js +++ b/src/app.js @@ -14,6 +14,7 @@ var Renderer = require('./app/renderer'); var Compiler = require('./app/compiler'); var ExecutionContext = require('./app/execution-context'); var Debugger = require('./app/debugger'); +var FormalVerification = require('./app/formalVerification'); // The event listener needs to be registered as early as possible, because the // parent will send the message upon the "load" event. @@ -431,7 +432,8 @@ var run = function () { selectTab($('ul#options li.debugView')); }; var renderer = new Renderer(editor, executionContext, updateFiles, transactionDebugger); - var compiler = new Compiler(editor, renderer, queryParams, handleGithubCall, $('#output'), getHidingRHP, updateFiles); + var formalVerification = new FormalVerification($('#verificationView'), renderer); + var compiler = new Compiler(editor, renderer, queryParams, handleGithubCall, $('#output'), getHidingRHP, formalVerification, updateFiles); executionContext.setCompiler(compiler); function setVersionText (text) { diff --git a/src/app/compiler.js b/src/app/compiler.js index c3de62713c..26bf69e41e 100644 --- a/src/app/compiler.js +++ b/src/app/compiler.js @@ -5,7 +5,7 @@ var utils = require('./utils'); var Base64 = require('js-base64').Base64; -function Compiler (editor, renderer, queryParams, handleGithubCall, outputField, hidingRHP, updateFiles) { +function Compiler (editor, renderer, queryParams, handleGithubCall, outputField, hidingRHP, formalVerification, updateFiles) { var compileJSON; var compilerAcceptsMultipleFiles; @@ -37,6 +37,9 @@ function Compiler (editor, renderer, queryParams, handleGithubCall, outputField, var compile = function (missingInputs) { editor.clearAnnotations(); outputField.empty(); + if (formalVerification) { + formalVerification.compiling(); + } var input = editor.getValue(); editor.setCacheFileContent(input); @@ -114,6 +117,7 @@ function Compiler (editor, renderer, queryParams, handleGithubCall, outputField, compile(missingInputs); } else if (noFatalErrors && !hidingRHP()) { renderer.contracts(data, editor.getValue()); + formalVerification.compilationFinished(data); } } diff --git a/src/app/formalVerification.js b/src/app/formalVerification.js new file mode 100644 index 0000000000..381098a981 --- /dev/null +++ b/src/app/formalVerification.js @@ -0,0 +1,30 @@ +var $ = require('jquery'); + +function FormalVerification (outputElement, renderer) { + this.outputElement = outputElement; + this.renderer = renderer; +} + +FormalVerification.prototype.compiling = function () { + $('#formalVerificationInput', this.outputElement).val(''); + $('#formalVerificationErrors').empty(); +}; + +FormalVerification.prototype.compilationFinished = function (compilationResult) { + if (compilationResult.formal !== undefined) { + if (compilationResult.formal['why3'] !== undefined) { + $('#formalVerificationInput', this.outputElement).val( + '(* copy this to http://why3.lri.fr/try/ *)' + + compilationResult.formal['why3'] + ); + } + if (compilationResult.formal.errors !== undefined) { + var errors = compilationResult.formal.errors; + for (var i = 0; i < errors.length; i++) { + this.renderer.error(errors[i], $('#formalVerificationErrors'), true); + } + } + } +}; + +module.exports = FormalVerification; diff --git a/src/app/renderer.js b/src/app/renderer.js index c82e7551db..808a347590 100644 --- a/src/app/renderer.js +++ b/src/app/renderer.js @@ -7,17 +7,20 @@ var utils = require('./utils'); function Renderer (editor, executionContext, updateFiles, transactionDebugger) { var detailsOpen = {}; - function renderError (message) { + function renderError (message, container, noAnnotations) { var type = utils.errortype(message); var $pre = $('
    ').text(message);
     var $error = $('
    ').prepend($pre);
-    $('#output').append($error);
+    if (container === undefined) {
+      container = $('#output');
+    }
+    container.append($error);
     var err = message.match(/^([^:]*):([0-9]*):(([0-9]*):)? /);
     if (err) {
       var errFile = err[1];
       var errLine = parseInt(err[2], 10) - 1;
       var errCol = err[4] ? parseInt(err[4], 10) : 0;
-      if (errFile === '' || errFile === utils.fileNameFromKey(editor.getCacheFile())) {
+      if (!noAnnotations && (errFile === '' || errFile === utils.fileNameFromKey(editor.getCacheFile()))) {
         editor.addAnnotation({
           row: errLine,
           column: errCol,

From fe02fd80ab8aeda806aeeaeb850bbf584f5dde0a Mon Sep 17 00:00:00 2001
From: chriseth 
Date: Tue, 26 Jul 2016 15:50:18 +0200
Subject: [PATCH 2/2] Hide textarea and show error for old version.

---
 src/app/formalVerification.js | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/app/formalVerification.js b/src/app/formalVerification.js
index 381098a981..c69ab863c1 100644
--- a/src/app/formalVerification.js
+++ b/src/app/formalVerification.js
@@ -6,17 +6,26 @@ function FormalVerification (outputElement, renderer) {
 }
 
 FormalVerification.prototype.compiling = function () {
-  $('#formalVerificationInput', this.outputElement).val('');
+  $('#formalVerificationInput', this.outputElement)
+    .val('')
+    .hide();
   $('#formalVerificationErrors').empty();
 };
 
 FormalVerification.prototype.compilationFinished = function (compilationResult) {
-  if (compilationResult.formal !== undefined) {
+  if (compilationResult.formal === undefined) {
+    this.renderer.error(
+      'Formal verification not supported by this compiler version.',
+      $('#formalVerificationErrors'),
+      true
+    );
+  } else {
     if (compilationResult.formal['why3'] !== undefined) {
       $('#formalVerificationInput', this.outputElement).val(
         '(* copy this to http://why3.lri.fr/try/ *)' +
         compilationResult.formal['why3']
-      );
+      )
+      .show();
     }
     if (compilationResult.formal.errors !== undefined) {
       var errors = compilationResult.formal.errors;