Split SMTChecker and SMTSolver

Author: axic

package.json

@@ -28,6 +28,7 @@
     "index.js",
     "linker.js",
     "smtchecker.js",
+    "smtsolver.js",
     "solcjs",
     "soljson.js",
     "translate.js",

smtchecker.js

@@ -1,40 +1,9 @@
-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) {
+function handleSMTQueries (inputJSON, outputJSON, solver) {
   var auxInputReq = outputJSON.auxiliaryInputRequested;
   if (!auxInputReq) {
     return null;
@@ -45,13 +14,9 @@ function handleSMTQueries (inputJSON, outputJSON) {
     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]);
+    responses[query] = solver(queries[query]);
   }
 
   // Note: all existing solved queries are replaced.

smtsolver.js

@@ -0,0 +1,38 @@
+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) {
+  if (solvers.length === 0) {
+    throw new Error('No SMT solver available. Assertion checking will not be performed.');
+  }
+
+  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();
+}
+
+module.exports = {
+  smtSolver: solve
+};

solcjs

@@ -7,6 +7,7 @@ var fs = require('fs-extra');
 var path = require('path');
 var solc = require('./index.js');
 var smtchecker = require('./smtchecker.js');
+var smtsolver = require('./smtsolver.js');
 // FIXME: remove annoying exception catcher of Emscripten
 //        see https://github.com/chriseth/browser-solidity/issues/167
 process.removeAllListeners('uncaughtException');
@@ -56,7 +57,7 @@ if (argv['standard-json']) {
   var output = solc.compileStandardWrapper(input);
 
   try {
-    var inputJSON = smtchecker.handleSMTQueries(JSON.parse(input), JSON.parse(output));
+    var inputJSON = smtchecker.handleSMTQueries(JSON.parse(input), JSON.parse(output), smtsolver.smtSolver);
     if (inputJSON) {
       output = solc.compileStandardWrapper(JSON.stringify(inputJSON));
     }