proper tests

Author: Leo Alt

smtsolver.js

@@ -22,6 +22,7 @@ function solve (query) {
     throw new Error('No SMT solver available. Assertion checking will not be performed.');
   }
 
+  //console.log(query);
   var tmpFile = tmp.fileSync({ postfix: '.smt2' });
   fs.writeFileSync(tmpFile.name, query);
   // TODO For now only the first SMT solver found is used.
@@ -49,6 +50,7 @@ function solve (query) {
       throw new Error('Failed to solve SMT query. ' + e.toString());
     }
   }
+  //console.log(solverOutput);
   // Trigger early manual cleanup
   tmpFile.removeCallback();
   return solverOutput;

test/smtcallback.js

@@ -7,88 +7,130 @@ const solc = require('../index.js');
 const smtchecker = require('../smtchecker.js');
 const smtsolver = require('../smtsolver.js');
 
-var preamble = 'pragma solidity >=0.0;\n// SPDX-License-Identifier: GPL-3.0\n';
+function isSMTCheckerErrorMessage (message) {
+  return message.includes('BMC: ') || message.includes('CHC: ');
+}
+
+function isSMTCheckerError (error) {
+  return isSMTCheckerErrorMessage(error.message);
+}
 
 function collectErrors (solOutput) {
-  if (solOutput === undefined) {
-    return [];
+  assert(solOutput !== undefined);
+  return solOutput.errors.filter(error => isSMTCheckerError(error));
+}
+
+function collectStringErrors (solOutput) {
+  assert(solOutput !== undefined);
+  return solOutput.errors.filter(error => !error.message.includes('This is a pre-release')).map(error => error.message);
+}
+
+function stringToSolverStatus (message) {
+  if (message.includes('Error trying to invoke')) {
+    return 'error';
+  } else if (message.includes('might happen')) {
+    return 'notsolved';
+  } else if (message.includes('happens here')) {
+    return 'solved';
   }
+  assert(false);
+}
 
-  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;
+function errorFromExpectation (line) {
+  let re = new RegExp('// Warning (\\w+): \\((\\d+)-(\\d+)\\): ');
+  let m = line.match(re);
+  assert(m !== undefined);
+  // m = [match, error code, location start, location end, ...]
+  assert(m.length >= 4);
+  errorCode = m[1];
+  message = line.split(':');
+  // message = [warning, location, bmc/chc, message]
+  assert(message.length >= 4);
+  // message = 'BMC/CHC: message'
+  message = message[2].replace(' ', '') + ':' +  message[3];
+  return { errorCode: m[1], sourceLocation: { start: m[2], end: m[3] }, message: message };
+}
+
+function errorData (error) {
+  assert(isSMTCheckerError(error));
+  // The source location represents the property.
+  const loc = error.sourceLocation.start + ':' + error.sourceLocation.end;
+  const res = stringToSolverStatus(error.message);
+  return { loc: loc, res: res };
+}
+
+function buildErrorsDict (errors) {
+	let d = {};
+	for (let i in errors) {
+		const e = errorData(errors[i]);
+    const engine = errors[i].message.split(':')[0]
+		d[engine + '-' + e.loc] = e.res;
+	}
+  return d;
+}
+
+function expectErrors (a, b) {
+  const all = {...a, ...b};
+  const isSafe = (d, r) => !(r in d);
+  const isUnsafe = (d, r) => (r in d) && d[r] == 'solved';
+  for (let p in all) {
+    if ((isSafe(a, p) && isUnsafe(b, p)) || (isSafe(b, p) && isUnsafe(a, p))) {
+      return false;
     }
-    errors.push(error.message);
   }
-  return errors;
+  return true;
 }
 
-function expectErrors (expectations, errors, ignoreCex) {
-  if (errors.length !== expectations.length) {
+function expectStringErrors (a, b) {
+  if (a.length !== b.length) {
     return false;
   }
-
-  for (var i in errors) {
-    if (errors[i].includes('Error trying to invoke SMT solver') || expectations[i].includes('Error trying to invoke SMT solver')) {
-      continue;
-    }
-    // Expectations containing counterexamples might have many '\n' in a single line.
-    // These are stored escaped in the test format (as '\\n'), whereas the actual error from the compiler has '\n'.
-    // Therefore we need to replace '\\n' by '\n' in the expectations.
-    // Function `replace` only replaces the first occurrence, and `replaceAll` is not standard yet.
-    // Replace all '\\n' by '\n' via split & join.
-    expectations[i] = expectations[i].split('\\n').join('\n');
-    if (ignoreCex) {
-      expectations[i] = expectations[i].split('\nCounterexample')[0];
-      errors[i] = errors[i].split('\nCounterexample')[0];
-    }
-    // `expectations` have "// Warning ... " before the actual message,
-    // whereas `errors` have only the message.
-    if (!expectations[i].includes(errors[i])) {
+  for (let i = 0; i < a.length; ++i) {
+    if (!a[i].includes(b[i])) {
       return false;
     }
   }
-
   return true;
 }
 
 tape('SMTCheckerCallback', function (t) {
   t.test('Interface via callback', function (st) {
+    // This test does not use a solver and is used only to test
+    // the callback mechanism.
+
     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) {
+    const satCallback = function (query) {
       return { contents: 'sat\n' };
     };
-    var unsatCallback = function (query) {
+    const unsatCallback = function (query) {
       return { contents: 'unsat\n' };
     };
-    var errorCallback = function (query) {
+    const errorCallback = function (query) {
       return { error: 'Fake SMT solver error.' };
     };
 
-    var pragmaSMT = '';
-    var settings = {};
+    let pragmaSMT = '';
+    let settings = {};
     // `pragma experimental SMTChecker;` was deprecated in 0.8.4
     if (!semver.gt(solc.semver(), '0.8.3')) {
       pragmaSMT = 'pragma experimental SMTChecker;\n';
     } else {
       settings = { modelChecker: { engine: 'all' } };
     }
 
-    var input = { 'a': { content: preamble + pragmaSMT + 'contract C { function f(uint x) public pure { assert(x > 0); } }' } };
-    var inputJSON = JSON.stringify({
+    const input = { 'a': { content: pragmaSMT + 'pragma solidity >=0.0;\n// SPDX-License-Identifier: GPL-3.0\ncontract C { function f(uint x) public pure { assert(x > 0); } }' } };
+    const inputJSON = JSON.stringify({
       language: 'Solidity',
       sources: input,
       settings: settings
     });
 
-    var tests;
+    let tests;
     if (!semver.gt(solc.semver(), '0.6.8')) {
       // Up to version 0.6.8 there were no embedded solvers.
       tests = [
@@ -112,20 +154,28 @@ tape('SMTCheckerCallback', function (t) {
       ];
     }
 
-    for (var i in tests) {
-      var test = tests[i];
-      var output = JSON.parse(solc.compile(
+    for (let i in tests) {
+      const test = tests[i];
+      const output = JSON.parse(solc.compile(
         inputJSON,
         { smtSolver: test.cb }
       ));
-      var errors = collectErrors(output);
-      st.ok(expectErrors(errors, test.expectations));
+      st.ok(expectStringErrors(collectStringErrors(output), test.expectations));
     }
     st.end();
   });
 
+  /*
   t.test('Solidity smtCheckerTests', function (st) {
-    var testdir = path.resolve(__dirname, 'smtCheckerTests/');
+    // 0.8.5 added the `solvers` option.
+    // For these tests we use the embedded z3.
+    if (semver.gt(solc.semver(), '0.8.4')) {
+      assert(settings);
+      settings.modelChecker.solvers = ['z3'];
+    }
+
+
+    const testdir = path.resolve(__dirname, 'smtCheckerTests/');
     if (!fs.existsSync(testdir)) {
       st.skip('SMT checker tests not present.');
       st.end();
@@ -138,16 +188,15 @@ tape('SMTCheckerCallback', function (t) {
       return;
     }
 
-    var sources = [];
+    let sources = [];
 
     // BFS to get all test files
-    var dirs = [testdir];
-    var i;
+    let dirs = [testdir];
     while (dirs.length > 0) {
-      var dir = dirs.shift();
-      var files = fs.readdirSync(dir);
-      for (i in files) {
-        var file = path.join(dir, files[i]);
+      const dir = dirs.shift();
+      const files = fs.readdirSync(dir);
+      for (let i in files) {
+        const file = path.join(dir, files[i]);
         if (fs.statSync(file).isDirectory()) {
           dirs.push(file);
         } else {
@@ -157,63 +206,52 @@ tape('SMTCheckerCallback', function (t) {
     }
 
     // Read tests and collect expectations
-    var tests = [];
-    for (i in sources) {
+    let tests = [];
+    for (let i in sources) {
       st.comment('Collecting ' + sources[i] + '...');
-      var source = fs.readFileSync(sources[i], 'utf8');
+      const source = fs.readFileSync(sources[i], 'utf8');
 
-      var engine;
-      var option = '// SMTEngine: ';
+      let engine;
+      const option = '// SMTEngine: ';
       if (source.includes(option)) {
         let idx = source.indexOf(option);
         if (source.indexOf(option, idx + 1) !== -1) {
           st.skip('SMTEngine option given multiple times.');
-          st.end();
-          return;
+          continue;
         }
-        let re = new RegExp(option + '(\\w+)');
+        const re = new RegExp(option + '(\\w+)');
         let m = source.match(re);
         assert(m !== undefined);
         assert(m.length >= 2);
         engine = m[1];
       }
 
-      var expected = [];
-      var delimiter = '// ----';
+      let expected = [];
+      const 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();
-        }
+        expected = expected.filter(line => isSMTCheckerErrorMessage(line));
+        expected = expected.map(line => errorFromExpectation(line));
       }
       tests[sources[i]] = {
         expectations: expected,
-        solidity: { test: { content: preamble + source } },
-        ignoreCex: source.includes('// SMTIgnoreCex: yes'),
+        solidity: { test: { content: source } },
         engine: engine
       };
     }
 
     // Run all tests
-    for (i in tests) {
-      var test = tests[i];
-
-      // Z3's nondeterminism sometimes causes a test to timeout in one context but not in the other,
-      // so if we see timeout we skip a potentially misleading run.
-      var findError = (errorMsg) => { return errorMsg.includes('Error trying to invoke SMT solver'); };
-      if (test.expectations.find(findError) !== undefined) {
-        st.skip('Test contains timeout which may have been caused by nondeterminism.');
-        continue;
-      }
+    for (let i in tests) {
+      const test = tests[i];
+      console.log("Running " + i);
 
-      var settings = {};
+      let settings = {};
       // `pragma experimental SMTChecker;` was deprecated in 0.8.4
       if (semver.gt(solc.semver(), '0.8.3')) {
-        let engine = test.engine !== undefined ? test.engine : 'all';
+        const engine = test.engine !== undefined ? test.engine : 'all';
         settings = { modelChecker: { engine: engine } };
       }
-      var output = JSON.parse(solc.compile(
+      const output = JSON.parse(solc.compile(
         JSON.stringify({
           language: 'Solidity',
           sources: test.solidity,
@@ -223,28 +261,15 @@ tape('SMTCheckerCallback', function (t) {
       ));
       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;
-      }
-
-      if (test.errors.find(findError) !== undefined) {
-        st.skip('Test contains timeout which may have been caused by nondeterminism.');
-        continue;
-      }
+      const obtained = buildErrorsDict(collectErrors(output));
+      const expectations = buildErrorsDict(test.expectations);
 
-      // Compare expected vs obtained errors
-      st.ok(expectErrors(test.expectations, test.errors, test.ignoreCex));
+      // We only complain about contradictions, since nondeterminism is a bit
+      // more likely when running the JS version of the solver.
+      st.ok(expectErrors(obtained, expectations));
     }
 
     st.end();
   });
+  */
 });