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 ec0adc90b5..d19d2e8a0c 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. @@ -437,7 +438,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 80024e9b6f..cd6cf7d3ee 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..c69ab863c1 --- /dev/null +++ b/src/app/formalVerification.js @@ -0,0 +1,39 @@ +var $ = require('jquery'); + +function FormalVerification (outputElement, renderer) { + this.outputElement = outputElement; + this.renderer = renderer; +} + +FormalVerification.prototype.compiling = function () { + $('#formalVerificationInput', this.outputElement) + .val('') + .hide(); + $('#formalVerificationErrors').empty(); +}; + +FormalVerification.prototype.compilationFinished = function (compilationResult) { + 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; + 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,