Merge pull request #303 from ethereum/smt_wrapper

Run SMT solver on requested queries

Author: axic

package.json

@@ -39,11 +39,13 @@
   },
   "homepage": "https://github.com/ethereum/solc-js#readme",
   "dependencies": {
+    "command-exists": "^1.2.8",
     "fs-extra": "^0.30.0",
     "keccak": "^1.0.2",
     "memorystream": "^0.3.1",
     "require-from-string": "^2.0.0",
     "semver": "^5.5.0",
+    "tmp": "0.0.33",
     "yargs": "^11.0.0"
   },
   "devDependencies": {

smtchecker.js

@@ -0,0 +1,65 @@
+var commandExistsSync = require('command-exists').sync;
+var execSync = require('child_process').execSync;
+var fs = require('fs-extra');
+var tmp = require('tmp');
+
+var potentialSolvers = [
+  {
+    name: 'z3',
+    params: ''
+  },
+  {
+    name: 'cvc4',
+    params: '--lang=smt2'
+  }
+];
+var solvers = potentialSolvers.filter(solver => commandExistsSync(solver.name));
+
+function solve (query) {
+  var tmpFile = tmp.fileSync();
+  fs.writeFileSync(tmpFile.name, query);
+  // TODO For now only the first SMT solver found is used.
+  // At some point a computation similar to the one done in
+  // SMTPortfolio::check should be performed, where the results
+  // given by different solvers are compared and an error is
+  // reported if solvers disagree (i.e. SAT vs UNSAT).
+  var solverOutput = execSync(solvers[0].name + ' ' + solvers[0].params + ' ' + tmpFile.name);
+  // Trigger early manual cleanup
+  tmpFile.removeCallback();
+  return solverOutput.toString();
+}
+
+// This function checks the standard JSON output for auxiliaryInputRequested,
+// where smtlib2queries represent the queries created by the SMTChecker.
+// The function runs an SMT solver on each query and adjusts the input for
+// another run.
+// Returns null if no solving is requested.
+function handleSMTQueries (inputJSON, outputJSON) {
+  var auxInputReq = outputJSON.auxiliaryInputRequested;
+  if (!auxInputReq) {
+    return null;
+  }
+
+  var queries = auxInputReq.smtlib2queries;
+  if (!queries || Object.keys(queries) === 0) {
+    return null;
+  }
+
+  if (solvers.length === 0) {
+    throw new Error('No SMT solver available. Assertion checking will not be performed.');
+  }
+
+  var responses = {};
+  for (var query in queries) {
+    responses[query] = solve(queries[query]);
+  }
+
+  // Note: all existing solved queries are replaced.
+  // This assumes that all neccessary queries are quested above.
+  inputJSON.auxiliaryInput = { smtlib2responses: responses };
+  return inputJSON;
+}
+
+module.exports = {
+  handleSMTQueries: handleSMTQueries
+};

solcjs

@@ -6,6 +6,7 @@ var originalUncaughtExceptionListeners = process.listeners("uncaughtException");
 var fs = require('fs-extra');
 var path = require('path');
 var solc = require('./index.js');
+var smtchecker = require('./smtchecker.js');
 // FIXME: remove annoying exception catcher of Emscripten
 //        see https://github.com/chriseth/browser-solidity/issues/167
 process.removeAllListeners('uncaughtException');
@@ -51,8 +52,32 @@ function abort (msg) {
 }
 
 if (argv['standard-json']) {
-  var input = fs.readFileSync(process.stdin.fd);
-  console.log(solc.compile(input.toString('utf8')))
+  var input = fs.readFileSync(process.stdin.fd).toString('utf8');
+  var output = solc.compileStandardWrapper(input);
+
+  try {
+    var inputJSON = smtchecker.handleSMTQueries(JSON.parse(input), JSON.parse(output));
+    if (inputJSON) {
+      output = solc.compileStandardWrapper(JSON.stringify(inputJSON));
+    }
+  }
+  catch (e) {
+    var addError = {
+      component: "general",
+      formattedMessage: e.toString(),
+      message: e.toString(),
+      type: "Warning"
+    };
+
+    var outputJSON = JSON.parse(output);
+    if (!outputJSON.errors) {
+      outputJSON.errors = []
+    }
+    outputJSON.errors.push(addError);
+    output = JSON.stringify(outputJSON);
+  }
+
+  console.log(output);
   process.exit(0);
 } else if (files.length === 0) {
   console.error('Must provide a file');