Merge pull request #382 from ethereum/smt_callback

Add callback kind to solc

Author: Leonardo

smtchecker.js

@@ -25,6 +25,18 @@ function handleSMTQueries (inputJSON, outputJSON, solver) {
   return inputJSON;
 }
 
+function smtCallback (solver) {
+  return function (query) {
+    try {
+      var result = solver(query);
+      return { contents: result };
+    } catch (err) {
+      return { error: err };
+    }
+  };
+}
+
 module.exports = {
-  handleSMTQueries: handleSMTQueries
+  handleSMTQueries: handleSMTQueries,
+  smtCallback: smtCallback
 };

smtsolver.js

@@ -46,7 +46,7 @@ function solve (query) {
       !solverOutput.startsWith('unsat') &&
       !solverOutput.startsWith('unknown')
     ) {
-      throw new Error('Failed solve SMT query. ' + e.toString());
+      throw new Error('Failed to solve SMT query. ' + e.toString());
     }
   }
   // Trigger early manual cleanup
@@ -55,5 +55,6 @@ function solve (query) {
 }
 
 module.exports = {
-  smtSolver: solve
+  smtSolver: solve,
+  availableSolvers: solvers.length
 };

test/index.js

@@ -3,6 +3,7 @@ const semver = require('semver');
 require('./linker.js');
 require('./translate.js');
 require('./compiler.js');
+require('./smtcallback.js');
 require('./smtchecker.js');
 require('./abi.js');
 

test/smtCheckerTests/smoke.sol

@@ -0,0 +1,5 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public pure {
+	}
+}

test/smtcallback.js

@@ -0,0 +1,165 @@
+const tape = require('tape');
+const fs = require('fs');
+const path = require('path');
+const semver = require('semver');
+const solc = require('../index.js');
+const smtchecker = require('../smtchecker.js');
+const smtsolver = require('../smtsolver.js');
+
+var pragmaSol = 'pragma solidity >=0.0;\n';
+var pragmaSMT = 'pragma experimental SMTChecker;\n';
+
+function collectErrors (solOutput) {
+  if (solOutput === undefined) {
+    return [];
+  }
+
+  var errors = [];
+  for (var i in solOutput.errors) {
+    var error = solOutput.errors[i];
+    if (error.message.includes('This is a pre-release compiler version')) {
+      continue;
+    }
+    errors.push(error.message);
+  }
+  return errors;
+}
+
+function expectErrors (errors, expectations) {
+  if (errors.length !== expectations.length) {
+    return false;
+  }
+
+  for (var i in errors) {
+    if (!errors[i].includes(expectations[i])) {
+      return false;
+    }
+  }
+
+  return true;
+}
+
+tape('SMTCheckerCallback', function (t) {
+  t.test('Interface via callback', function (st) {
+    if (!semver.gt(solc.semver(), '0.5.99')) {
+      st.skip('SMT callback not implemented by this compiler version.');
+      st.end();
+      return;
+    }
+
+    var satCallback = function (query) {
+      return { contents: 'sat\n' };
+    };
+    var unsatCallback = function (query) {
+      return { contents: 'unsat\n' };
+    };
+    var errorCallback = function (query) {
+      return { error: 'Fake SMT solver error.' };
+    };
+
+    var input = { 'a': { content: pragmaSol + pragmaSMT + 'contract C { function f(uint x) public pure { assert(x > 0); } }' } };
+    var inputJSON = JSON.stringify({
+      language: 'Solidity',
+      sources: input
+    });
+    var tests = [
+      { cb: satCallback, expectations: ['Assertion violation happens here'] },
+      { cb: unsatCallback, expectations: [] },
+      { cb: errorCallback, expectations: ['BMC analysis was not possible'] }
+    ];
+    for (var i in tests) {
+      var test = tests[i];
+      var output = JSON.parse(solc.compile(
+        inputJSON,
+        { smtSolver: test.cb }
+      ));
+      var errors = collectErrors(output);
+      st.ok(expectErrors(errors, test.expectations));
+    }
+    st.end();
+  });
+
+  t.test('Solidity smtCheckerTests', function (st) {
+    var testdir = path.resolve(__dirname, 'smtCheckerTests/');
+    if (!fs.existsSync(testdir)) {
+      st.skip('SMT checker tests not present.');
+      st.end();
+      return;
+    }
+
+    if (smtsolver.availableSolvers === 0) {
+      st.skip('No SMT solver available.');
+      st.end();
+      return;
+    }
+
+    var sources = [];
+
+    // BFS to get all test files
+    var dirs = [testdir];
+    var i;
+    while (dirs.length > 0) {
+      var dir = dirs.shift();
+      var files = fs.readdirSync(dir);
+      for (i in files) {
+        var file = path.join(dir, files[i]);
+        if (fs.statSync(file).isDirectory()) {
+          dirs.push(file);
+        } else {
+          sources.push(file);
+        }
+      }
+    }
+
+    // Read tests and collect expectations
+    var tests = [];
+    for (i in sources) {
+      st.comment('Collecting ' + sources[i] + '...');
+      var source = fs.readFileSync(sources[i], 'utf8');
+      var expected = [];
+      var delimiter = '// ----';
+      if (source.includes(delimiter)) {
+        expected = source.substring(source.indexOf('// ----') + 8, source.length).split('\n');
+        // Sometimes the last expectation line ends with a '\n'
+        if (expected.length > 0 && expected[expected.length - 1] === '') {
+          expected.pop();
+        }
+      }
+      tests[sources[i]] = {
+        expectations: expected,
+        solidity: { test: { content: pragmaSol + source } }
+      };
+    }
+
+    // Run all tests
+    for (i in tests) {
+      var test = tests[i];
+      var output = JSON.parse(solc.compile(
+        JSON.stringify({
+          language: 'Solidity',
+          sources: test.solidity
+        }),
+        { smtSolver: smtchecker.smtCallback(smtsolver.smtSolver) }
+      ));
+      st.ok(output);
+
+      // Collect obtained error messages
+      test.errors = collectErrors(output);
+
+      // These are errors in the SMTLib2Interface encoding.
+      if (test.errors.length > 0 && test.errors[test.errors.length - 1].includes('BMC analysis was not possible')) {
+        continue;
+      }
+
+      // These are due to CHC not being supported via SMTLib2Interface yet.
+      if (test.expectations.length !== test.errors.length) {
+        continue;
+      }
+
+      // Compare expected vs obtained errors
+      st.ok(expectErrors(test.expectations, test.errors));
+    }
+
+    st.end();
+  });
+});

wrapper.js

@@ -3,6 +3,7 @@ var translate = require('./translate.js');
 var requireFromString = require('require-from-string');
 var https = require('https');
 var MemoryStream = require('memorystream');
+var semver = require('semver');
 
 function setupMethods (soljson) {
   var version;
@@ -37,8 +38,21 @@ function setupMethods (soljson) {
 
   var wrapCallback = function (callback) {
     assert(typeof callback === 'function', 'Invalid callback specified.');
-    return function (path, contents, error) {
-      var result = callback(soljson.Pointer_stringify(path));
+    return function (data, contents, error) {
+      var result = callback(soljson.Pointer_stringify(data));
+      if (typeof result.contents === 'string') {
+        copyString(result.contents, contents);
+      }
+      if (typeof result.error === 'string') {
+        copyString(result.error, error);
+      }
+    };
+  };
+
+  var wrapCallbackWithKind = function (callback) {
+    assert(typeof callback === 'function', 'Invalid callback specified.');
+    return function (kind, data, contents, error) {
+      var result = callback(soljson.Pointer_stringify(kind), soljson.Pointer_stringify(data));
       if (typeof result.contents === 'string') {
         copyString(result.contents, contents);
       }
@@ -49,25 +63,55 @@ function setupMethods (soljson) {
   };
 
   // This calls compile() with args || cb
-  var runWithReadCallback = function (readCallback, compile, args) {
-    if (readCallback) {
-      assert(typeof readCallback === 'object', 'Invalid callback object specified.');
-      readCallback = readCallback.import;
+  var runWithCallbacks = function (callbacks, compile, args) {
+    if (callbacks) {
+      assert(typeof callbacks === 'object', 'Invalid callback object specified.');
+    } else {
+      callbacks = {};
     }
 
+    var readCallback = callbacks.import;
     if (readCallback === undefined) {
-      readCallback = function (path) {
+      readCallback = function (data) {
         return {
           error: 'File import callback not supported'
         };
       };
     }
 
+    var singleCallback;
+    if (semver.gt(versionToSemver(), '0.5.99')) {
+      // After 0.6.x multiple kind of callbacks are supported.
+      var smtSolverCallback = callbacks.smtSolver;
+      if (smtSolverCallback === undefined) {
+        smtSolverCallback = function (data) {
+          return {
+            error: 'SMT solver callback not supported'
+          };
+        };
+      }
+
+      singleCallback = function (kind, data) {
+        if (kind === 'source') {
+          return readCallback(data);
+        } else if (kind === 'smt-query') {
+          return smtSolverCallback(data);
+        } else {
+          assert(false, 'Invalid callback kind specified.');
+        }
+      };
+
+      singleCallback = wrapCallbackWithKind(singleCallback);
+    } else {
+      // Old Solidity version only supported imports.
+      singleCallback = wrapCallback(readCallback);
+    }
+
     // This is to support multiple versions of Emscripten.
     var addFunction = soljson.addFunction || soljson.Runtime.addFunction;
     var removeFunction = soljson.removeFunction || soljson.Runtime.removeFunction;
 
-    var cb = addFunction(wrapCallback(readCallback));
+    var cb = addFunction(singleCallback);
     var output;
     try {
       args.push(cb);
@@ -94,21 +138,21 @@ function setupMethods (soljson) {
   if ('_compileJSONCallback' in soljson) {
     var compileInternal = soljson.cwrap('compileJSONCallback', 'string', ['string', 'number', 'number']);
     compileJSONCallback = function (input, optimize, readCallback) {
-      return runWithReadCallback(readCallback, compileInternal, [ input, optimize ]);
+      return runWithCallbacks(readCallback, compileInternal, [ input, optimize ]);
     };
   }
 
   var compileStandard = null;
   if ('_compileStandard' in soljson) {
     var compileStandardInternal = soljson.cwrap('compileStandard', 'string', ['string', 'number']);
     compileStandard = function (input, readCallback) {
-      return runWithReadCallback(readCallback, compileStandardInternal, [ input ]);
+      return runWithCallbacks(readCallback, compileStandardInternal, [ input ]);
     };
   }
   if ('_solidity_compile' in soljson) {
     var solidityCompile = soljson.cwrap('solidity_compile', 'string', ['string', 'number']);
-    compileStandard = function (input, readCallback) {
-      return runWithReadCallback(readCallback, solidityCompile, [ input ]);
+    compileStandard = function (input, callbacks) {
+      return runWithCallbacks(callbacks, solidityCompile, [ input ]);
     };
   }