Merge pull request #431 from ethereum/master_060

Merge 'master_060' into 'master'

Author: axic

README.md

@@ -50,8 +50,6 @@ of them are resolved.
 
 Starting 0.5.12 it also accepts an object in place of the callback to supply different kind of callbacks, however only file imports are supported.
 
-_Note_: as an intermittent backwards compatibility feature, between versions 0.5.0 and 0.5.2, `compileStandard` and `compileStandardWrapper` also exists and behave like `compile` does.
-
 #### Example usage without the import callback
 
 Example:

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/compiler.js

@@ -193,7 +193,7 @@ function runTests (solc, versionText) {
             return { error: 'File not found' };
           }
         }
-        var output = JSON.parse(solc.lowlevel.compileCallback(JSON.stringify({sources: input}), 0, findImports));
+        var output = JSON.parse(solc.lowlevel.compileCallback(JSON.stringify({sources: input}), 0, { import: findImports }));
         var B = getBytecode(output, 'b.sol', 'B');
         st.ok(typeof B === 'string');
         st.ok(B.length > 0);
@@ -217,7 +217,7 @@ function runTests (solc, versionText) {
         function findImports (path) {
           return { error: 'File not found' };
         }
-        var output = JSON.parse(solc.lowlevel.compileCallback(JSON.stringify({sources: input}), 0, findImports));
+        var output = JSON.parse(solc.lowlevel.compileCallback(JSON.stringify({sources: input}), 0, { import: findImports }));
         st.plan(3);
         st.ok('errors' in output);
         // Check if the ParserError exists, but allow others too
@@ -248,7 +248,7 @@ function runTests (solc, versionText) {
           throw new Error('Could not implement this interface properly...');
         }
         st.throws(function () {
-          solc.lowlevel.compileCallback(JSON.stringify({sources: input}), 0, findImports);
+          solc.lowlevel.compileCallback(JSON.stringify({sources: input}), 0, { import: findImports });
         }, /^Error: Could not implement this interface properly.../);
         st.end();
       });
@@ -266,7 +266,7 @@ function runTests (solc, versionText) {
         };
         st.throws(function () {
           solc.lowlevel.compileCallback(JSON.stringify({sources: input}), 0, "this isn't a callback");
-        }, /Invalid callback specified./);
+        }, /Invalid callback object specified./);
         st.end();
       });
 
@@ -418,7 +418,7 @@ function runTests (solc, versionText) {
           }
         }
 
-        var output = JSON.parse(solc.lowlevel.compileStandard(JSON.stringify(input), findImports));
+        var output = JSON.parse(solc.lowlevel.compileStandard(JSON.stringify(input), { import: findImports }));
         st.ok(bytecodeExists(output, 'a.sol', 'A'));
         st.ok(bytecodeExists(output, 'b.sol', 'B'));
         st.end();
@@ -513,6 +513,12 @@ function runTests (solc, versionText) {
         }
 
         var isVersion6 = semver.gt(solc.semver(), '0.5.99');
+        var source;
+        if (isVersion6) {
+          source = 'abstract contract C { function f() public virtual; }';
+        } else {
+          source = 'contract C { function f() public; }';
+        }
 
         var input = {
           'language': 'Solidity',
@@ -525,7 +531,7 @@ function runTests (solc, versionText) {
           },
           'sources': {
             'c.sol': {
-              'content': (isVersion6 ? 'abstract ' : '') + 'contract C { function f() public; }'
+              'content': source
             }
           }
         };
@@ -570,50 +576,6 @@ function runTests (solc, versionText) {
           }
         }
 
-        var output = JSON.parse(solc.compile(JSON.stringify(input), findImports));
-        st.ok(expectNoError(output));
-        var A = getBytecodeStandard(output, 'a.sol', 'A');
-        st.ok(typeof A === 'string');
-        st.ok(A.length > 0);
-        var B = getBytecodeStandard(output, 'b.sol', 'B');
-        st.ok(typeof B === 'string');
-        st.ok(B.length > 0);
-        st.ok(Object.keys(linker.findLinkReferences(B)).length === 0);
-        st.end();
-      });
-
-      t.test('compiling standard JSON (with imports + new callback API)', function (st) {
-        // <0.2.1 doesn't have this
-        if (!solc.features.importCallback) {
-          st.skip('Not supported by solc');
-          st.end();
-          return;
-        }
-
-        var input = {
-          'language': 'Solidity',
-          'settings': {
-            'outputSelection': {
-              '*': {
-                '*': [ 'evm.bytecode' ]
-              }
-            }
-          },
-          'sources': {
-            'b.sol': {
-              'content': 'import "a.sol"; contract B is A { function g() public { f(); } }'
-            }
-          }
-        };
-
-        function findImports (path) {
-          if (path === 'a.sol') {
-            return { contents: 'contract A { function f() public returns (uint) { return 7; } }' };
-          } else {
-            return { error: 'File not found' };
-          }
-        }
-
         var output = JSON.parse(solc.compile(JSON.stringify(input), { import: findImports }));
         st.ok(expectNoError(output));
         var A = getBytecodeStandard(output, 'a.sol', 'A');
@@ -622,6 +584,7 @@ function runTests (solc, versionText) {
         var B = getBytecodeStandard(output, 'b.sol', 'B');
         st.ok(typeof B === 'string');
         st.ok(B.length > 0);
+        st.ok(Object.keys(linker.findLinkReferences(B)).length === 0);
         st.end();
       });
 
@@ -821,14 +784,6 @@ function runTests (solc, versionText) {
         });
       });
     });
-
-    tape('API backwards compatibility', function (t) {
-      t.test('compileStandard and compileStandardWrapper exists', function (st) {
-        st.equal(solc.compile, solc.compileStandard);
-        st.equal(solc.compile, solc.compileStandardWrapper);
-        st.end();
-      });
-    });
   }
 }
 

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