Fix smtchecker callback tests and add Eldarica

Author: Leo Alt

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 arount 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
 };

solcjs

@@ -131,11 +131,15 @@ if (options.standardJson) {
   var output = reformatJsonIfRequested(solc.compile(input, callbacks));
 
   try {
-    var 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 {
+      var 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) {

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,83 @@
 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 theses 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();
+  });
+});
+
+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 errors = newOutput.errors;
+    st.equal(errors.length, 1);
+    st.equal(errors[0].errorCode, '6328');
+
     st.end();
   });
 });