Merge pull request #140 from ethereum/formal

Provide formal verification input.

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;
 }

index.html

@@ -65,6 +65,7 @@
 						<li class="envView" title="Environment"><i class="fa fa-cube"></i></li>
 						<li class="publishView" title="Publish" ><i class="fa fa-cloud-upload"></i></li>
 						<li class="debugView" title="Debugger"><i class="fa fa-bug"></i></li>
+						<li class="verificationView" title="Formal Verification"><i class="fa fa-check"></i></li>
 						<li id="helpButton"><a href="https://solidity.readthedocs.org" target="_blank" title="Open Documentation" class="fa fa-question"></a></li>
 					</ul>
 					<img id="solIcon" title="Solidity realtime compiler and runtime" src="assets/img/sol.svg" alt="Solidity realtime compiler and runtime">
@@ -125,6 +126,19 @@
 					<div id="debugView">
 						<div id="debugger" ></div>
 					</div>
+					<div id="verificationView">
+						<p>This tab provides support for <b>formal verification</b> of Solidity contracts.<br/>
+						This feature is still in development and thus also not yet well documented,
+						but you can find some information
+						<a href="http://solidity.readthedocs.io/en/latest/security-considerations.html#formal-verification">here</a>.
+						The compiler generates input to be verified
+						(or report errors). Please paste the text below into
+						<a href="http://why3.lri.fr/try/">http://why3.lri.fr/try/</a>
+						to actually perform the verification.
+						We plan to support direct integration in the future.</p>
+						<textarea id="formalVerificationInput" readonly="readonly"></textarea>
+						<div id="formalVerificationErrors"></div>
+					</div>
 				</div>
 			</div>
 			<div id="output"></div>

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) {

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);
     }
   }
 

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;

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 = $('<pre />').text(message);
     var $error = $('<div class="sol ' + type + '"><div class="close"><i class="fa fa-close"></i></div></div>').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,