Merge pull request #565 from ethereum/smt_fix_tests

Fix smtchecker callback tests and add Eldarica

Author: Leo

README.md

@@ -144,36 +144,54 @@ for (var contractName in output.contracts['test.sol']) {
 }
 ```
 
-The ``smtSolver`` callback function is used to solve SMT queries generated by
+Since version 0.5.1, the ``smtSolver`` callback function is used to solve SMT queries generated by
 Solidity's SMTChecker.  If you have an SMT solver installed locally, it can
 be used to solve the given queries, where the callback must synchronously
 return either an error or the result from the solver.  A default
-``smtSolver`` callback is distributed by ``solc-js``, which relies on either
-Z3 or CVC4 being installed locally.
+``smtSolver`` callback is included in this package via the module
+``smtchecker.js`` which exports the ``smtCallback`` function that takes 1) a
+function that takes queries and returns the solving result, and 2) a solver
+configuration object. The module ``smtsolver.js`` has a few predefined solver
+configurations, and relies on Z3, Eldarica or CVC4 being installed locally.  It
+exports the list of locally found solvers and a function that invokes a given
+solver.
+
+The API of the SMT callback is **experimental** and can change at any time.
+The last change was in version 0.8.11.
 
 #### Example usage with smtSolver callback
 
 ```javascript
 var solc = require('solc');
-var smt = require('smtsolver');
+const smtchecker = require('solc/smtchecker');
+const smtsolver = require('solc/smtsolver');
 // Note that this example only works via node and not in the browser.
 
 var input = {
   language: 'Solidity',
   sources: {
     'test.sol': {
-      content: 'pragma experimental SMTChecker; contract C { function f(uint x) public { assert(x > 0); } }'
+      content: 'contract C { function f(uint x) public { assert(x > 0); } }'
+    }
+  },
+  settings: {
+    modelChecker: {
+      engine: "chc",
+      solvers: [ "smtlib2" ]
     }
   }
 };
 
 var output = JSON.parse(
-  solc.compile(JSON.stringify(input), { smtSolver: smt.smtSolver })
+  solc.compile(
+    JSON.stringify(input),
+    { smtSolver: smtchecker.smtCallback(smtsolver.smtSolver, smtsolver.availableSolvers[0]) }
+  )
 );
 
 ```
 The assertion is clearly false, and an ``assertion failure`` warning
-should be returned.
+should be returned, together with a counterexample.
 
 #### Low-level API
 

smtchecker.js

@@ -3,7 +3,7 @@
 // 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, solver) {
+function handleSMTQueries (inputJSON, outputJSON, solverFunction, solver) {
   const auxInputReq = outputJSON.auxiliaryInputRequested;
   if (!auxInputReq) {
     return null;
@@ -16,7 +16,7 @@ function handleSMTQueries (inputJSON, outputJSON, solver) {
 
   const responses = {};
   for (const query in queries) {
-    responses[query] = solver(queries[query]);
+    responses[query] = solverFunction(queries[query], solver);
   }
 
   // Note: all existing solved queries are replaced.
@@ -25,10 +25,10 @@ function handleSMTQueries (inputJSON, outputJSON, solver) {
   return inputJSON;
 }
 
-function smtCallback (solver) {
+function smtCallback (solverFunction, solver) {
   return function (query) {
     try {
-      const result = solver(query);
+      const result = solverFunction(query, solver);
       return { contents: result };
     } catch (err) {
       return { error: err };

smtsolver.js

@@ -3,37 +3,48 @@ const execSync = require('child_process').execSync;
 const fs = require('fs');
 const tmp = require('tmp');
 
+// Timeout in ms.
 const timeout = 10000;
 
 const potentialSolvers = [
   {
     name: 'z3',
+    command: 'z3',
     params: '-smt2 rlimit=20000000 rewriter.pull_cheap_ite=true fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false'
   },
+  {
+    name: 'Eldarica',
+    command: 'eld',
+    params: '-horn -t:' + (timeout / 1000) // Eldarica takes timeout in seconds.
+  },
   {
     name: 'cvc4',
+    command: 'cvc4',
     params: '--lang=smt2 --tlimit=' + timeout
   }
 ];
-const 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.');
+const solvers = potentialSolvers.filter(solver => commandExistsSync(solver.command));
+
+function solve (query, solver) {
+  if (solver === undefined) {
+    if (solvers.length === 0) {
+      throw new Error('No SMT solver available. Assertion checking will not be performed.');
+    } else {
+      solver = solvers[0];
+    }
   }
 
   const tmpFile = tmp.fileSync({ postfix: '.smt2' });
   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).
   let solverOutput;
   try {
     solverOutput = execSync(
-      solvers[0].name + ' ' + solvers[0].params + ' ' + tmpFile.name, {
-        stdio: 'pipe'
+      solver.command + ' ' + solver.params + ' ' + tmpFile.name, {
+        encoding: 'utf8',
+        maxBuffer: 1024 * 1024 * 1024,
+        stdio: 'pipe',
+        timeout: timeout // Enforce timeout on the process, since solvers can sometimes go around it.
       }
     ).toString();
   } catch (e) {
@@ -44,7 +55,9 @@ function solve (query) {
     if (
       !solverOutput.startsWith('sat') &&
       !solverOutput.startsWith('unsat') &&
-      !solverOutput.startsWith('unknown')
+      !solverOutput.startsWith('unknown') &&
+      !solverOutput.startsWith('(error') && // Eldarica reports errors in an sexpr, for example: '(error "Failed to reconstruct array model")'
+      !solverOutput.startsWith('error')
     ) {
       throw new Error('Failed to solve SMT query. ' + e.toString());
     }
@@ -56,5 +69,5 @@ function solve (query) {
 
 module.exports = {
   smtSolver: solve,
-  availableSolvers: solvers.length
+  availableSolvers: solvers
 };

solc.js

@@ -129,10 +129,14 @@ if (options.standardJson) {
   let output = reformatJsonIfRequested(solc.compile(input, callbacks));
 
   try {
-    const inputJSON = smtchecker.handleSMTQueries(JSON.parse(input), JSON.parse(output), smtsolver.smtSolver);
-    if (inputJSON) {
-      if (program.verbose) { console.log('>>> Retrying compilation with SMT:\n' + toFormattedJson(inputJSON) + '\n'); }
-      output = reformatJsonIfRequested(solc.compile(JSON.stringify(inputJSON), callbacks));
+    if (smtsolver.availableSolvers.length === 0) {
+      console.log('>>> Cannot retry compilation with SMT because there are no SMT solvers available.');
+    } else {
+      const inputJSON = smtchecker.handleSMTQueries(JSON.parse(input), JSON.parse(output), smtsolver.smtSolver, smtsolver.availableSolvers[0]);
+      if (inputJSON) {
+        if (program.verbose) { console.log('>>> Retrying compilation with SMT:\n' + toFormattedJson(inputJSON) + '\n'); }
+        output = reformatJsonIfRequested(solc.compile(JSON.stringify(inputJSON), callbacks));
+      }
     }
   } catch (e) {
     const addError = {

test/smtCheckerTests/loop.sol

@@ -0,0 +1,8 @@
+contract C {
+	function f(uint x) public pure {
+		uint i = 0;
+		while (i < x)
+			++i;
+		assert(i == x);
+	}
+}

test/smtcallback.js

@@ -119,7 +119,7 @@ tape('SMTCheckerCallback', function (t) {
         { smtSolver: test.cb }
       ));
       const errors = collectErrors(output);
-      st.ok(expectErrors(errors, test.expectations));
+      st.ok(expectErrors(errors, test.expectations, false));
     }
     st.end();
   });
@@ -132,8 +132,10 @@ tape('SMTCheckerCallback', function (t) {
       return;
     }
 
-    if (smtsolver.availableSolvers === 0) {
-      st.skip('No SMT solver available.');
+    // For these tests we actually need z3/Spacer.
+    const z3HornSolvers = smtsolver.availableSolvers.filter(solver => solver.command === 'z3');
+    if (z3HornSolvers.length === 0) {
+      st.skip('z3/Spacer not available.');
       st.end();
       return;
     }
@@ -167,9 +169,8 @@ tape('SMTCheckerCallback', function (t) {
       if (source.includes(option)) {
         const idx = source.indexOf(option);
         if (source.indexOf(option, idx + 1) !== -1) {
-          st.skip('SMTEngine option given multiple times.');
-          st.end();
-          return;
+          st.comment('SMTEngine option given multiple times.');
+          continue;
         }
         const re = new RegExp(option + '(\\w+)');
         const m = source.match(re);
@@ -211,15 +212,23 @@ tape('SMTCheckerCallback', function (t) {
       // `pragma experimental SMTChecker;` was deprecated in 0.8.4
       if (semver.gt(solc.semver(), '0.8.3')) {
         const engine = test.engine !== undefined ? test.engine : 'all';
-        settings = { modelChecker: { engine: engine } };
+        settings = {
+          modelChecker: {
+            engine: engine,
+            solvers: [
+              'smtlib2'
+            ]
+          }
+        };
       }
       const output = JSON.parse(solc.compile(
         JSON.stringify({
           language: 'Solidity',
           sources: test.solidity,
           settings: settings
         }),
-        { smtSolver: smtchecker.smtCallback(smtsolver.smtSolver) }
+        // This test needs z3 specifically.
+        { smtSolver: smtchecker.smtCallback(smtsolver.smtSolver, z3HornSolvers[0]) }
       ));
       st.ok(output);
 

test/smtchecker.js

@@ -1,25 +1,104 @@
 const tape = require('tape');
+const semver = require('semver');
+const solc = require('../index.js');
 const smtchecker = require('../smtchecker.js');
+const smtsolver = require('../smtsolver.js');
 
+const preamble = 'pragma solidity >=0.0;\n// SPDX-License-Identifier: GPL-3.0\n';
+//
 tape('SMTChecker', function (t) {
+  // We use null for `solverFunction` and `solver` when calling `handleSMTQueries`
+  // because these tests do not call a solver.
+
   t.test('smoke test with no axuiliaryInputRequested', function (st) {
     const input = {};
     const output = {};
-    st.equal(smtchecker.handleSMTQueries(input, output), null);
+    st.equal(smtchecker.handleSMTQueries(input, output, null, null), null);
     st.end();
   });
 
   t.test('smoke test with no smtlib2queries', function (st) {
     const input = {};
     const output = { auxiliaryInputRequested: {} };
-    st.equal(smtchecker.handleSMTQueries(input, output), null);
+    st.equal(smtchecker.handleSMTQueries(input, output, null, null), null);
     st.end();
   });
 
   t.test('smoke test with empty smtlib2queries', function (st) {
     const input = {};
     const output = { auxiliaryInputRequested: { smtlib2queries: { } } };
-    st.equal(smtchecker.handleSMTQueries(input, output), null);
+    st.equal(smtchecker.handleSMTQueries(input, output, null, null), null);
+    st.end();
+  });
+
+  t.test('smtCallback should return type function', (st) => {
+    const response = smtchecker.smtCallback(() => {});
+    st.equal(typeof response, 'function');
+    st.end();
+  });
+
+  t.test('smtCallback should error when passed parser fails', (st) => {
+    const cbFun = smtchecker.smtCallback((content) => { throw new Error(content); });
+    const response = cbFun('expected-error-message');
+
+    st.deepEqual(response, { error: new Error('expected-error-message') });
+    st.end();
+  });
+
+  t.test('smtCallback should return content when passed parser does not fail', (st) => {
+    const cbFun = smtchecker.smtCallback((content) => { return content; });
+    const response = cbFun('expected-content-message');
+
+    st.deepEqual(response, { contents: 'expected-content-message' });
+    st.end();
+  });
+});
+
+tape('SMTCheckerWithSolver', function (t) {
+  // In these tests we require z3 to actually run the solver.
+  // This uses the SMT double run mechanism instead of the callback.
+
+  t.test('Simple test with axuiliaryInputRequested', function (st) {
+    const z3 = smtsolver.availableSolvers.filter(solver => solver.command === 'z3');
+    if (z3.length === 0) {
+      st.skip('Test requires z3.');
+      st.end();
+      return;
+    }
+
+    if (semver.lt(solc.semver(), '0.8.7')) {
+      st.skip('This test requires Solidity 0.8.7 to enable all SMTChecker options.');
+      st.end();
+      return;
+    }
+
+    const settings = {
+      modelChecker: {
+        engine: 'chc',
+        solvers: ['smtlib2']
+      }
+    };
+
+    const source = { a: { content: preamble + '\ncontract C { function f(uint x) public pure { assert(x > 0); } }' } };
+
+    const input = {
+      language: 'Solidity',
+      sources: source,
+      settings: settings
+    };
+
+    const output = JSON.parse(solc.compile(JSON.stringify(input)));
+    st.ok(output);
+
+    const newInput = smtchecker.handleSMTQueries(input, output, smtsolver.smtSolver, z3[0]);
+    st.notEqual(newInput, null);
+
+    const newOutput = JSON.parse(solc.compile(JSON.stringify(newInput)));
+    st.ok(newOutput);
+
+    const smtErrors = newOutput.errors.filter(e => e.errorCode === '6328');
+    st.equal(smtErrors.length, 1);
+
     st.end();
   });
 });