Fix smtchecker callback tests and add Eldarica

Author: Leo Alt

smtchecker.js

@@ -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,36 +3,44 @@ 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)
+  },
   {
     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, {
+      solver.command + ' ' + solver.params + ' ' + tmpFile.name, {
         stdio: 'pipe'
       }
     ).toString();
@@ -44,7 +52,9 @@ function solve (query) {
     if (
       !solverOutput.startsWith('sat') &&
       !solverOutput.startsWith('unsat') &&
-      !solverOutput.startsWith('unknown')
+      !solverOutput.startsWith('unknown') &&
+      !solverOutput.startsWith('(error') &&
+      !solverOutput.startsWith('error')
     ) {
       throw new Error('Failed to solve SMT query. ' + e.toString());
     }
@@ -56,5 +66,5 @@ function solve (query) {
 
 module.exports = {
   smtSolver: solve,
-  availableSolvers: solvers.length
+  availableSolvers: solvers
 };

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

@@ -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,22 @@ 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) }
+        { smtSolver: smtchecker.smtCallback(smtsolver.smtSolver, z3HornSolvers[0]) }
       ));
       st.ok(output);