Fix smtchecker callback tests and add Eldarica #565

leonardoalt · 2021-11-18T10:37:29Z

Besides fixing things, the nicest thing this PR enables is to use alternative solvers much more easily in a different script, like this:
https://gist.github.com/leonardoalt/70d659eb0ec2f0e82b1fa5681d5ce3e8

leonardoalt · 2021-11-18T10:38:21Z

smtchecker.js

  return function (query) {
    try {
-      var result = solver(query);
+      var result = solverFunction(query, solver);


This makes it possible to choose the solver from the callers side.

leonardoalt · 2021-11-18T10:38:39Z

smtsolver.js

+    name: 'Eldarica',
+    command: 'eld',
+    params: '-horn -t:' + (timeout / 1000)
+  },


Just adding Eldarica for easy future use, it's currently not used for the tests.

leonardoalt · 2021-11-18T10:39:30Z

test/smtcallback.js

-      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) {


Not to change things too much, we require z3 to run these tests.

I think we should make it opt-out instead of opt-in. With some equivalent of the --no-smt flag. Otherwise it's too easy for such tests to never run in CI.

leonardoalt · 2021-11-18T10:39:48Z

test/smtcallback.js

@@ -167,9 +169,8 @@ tape('SMTCheckerCallback', function (t) {
      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;


This was actually making none of the actual smtcheckertests to run lol

This is the main fix, I reckon?

The solverFunction and solver fixes in smtsolver.js too, solvers were actually not run

leonardoalt · 2021-11-18T10:40:02Z

test/smtcallback.js

-        settings = { modelChecker: { engine: engine } };
+        settings = { modelChecker: {
+          engine: engine,
+          solvers: [ 'smtlib2' ]


This was also wrong before, we need to force the callback to be used.

test/smtcallback.js

coveralls · 2021-11-18T10:44:33Z

Coverage decreased (-0.8%) to 85.347% when pulling 40d563f on smt_fix_tests into f2fdcfb on master.

smtsolver.js

test/smtcallback.js

leonardoalt · 2022-01-20T12:11:13Z

@cameel @axic I added the requested comments, plus added a piece of code I had locally that increases the output buffer of the child solver process. This is needed when a solver outputs a huge counterexample or proof.

smtsolver.js

README.md

axic · 2022-01-24T17:02:40Z

I'm leaning towards going in with the breaking changes, because the SMT Checker is still experimental. We can also change this code after merging to be backwards compatible before the next solc-js release.

cc @chriseth @cameel

axic

Code-wise this looks good to me, but we may need to revisit keeping "backwards compatibility" before the next release (0.8.12).

README.md

cameel · 2022-01-24T18:35:32Z

README.md

-  solc.compile(JSON.stringify(input), { smtSolver: smt.smtSolver })
+  solc.compile(
+    JSON.stringify(input),
+    { smtSolver: smtchecker.smtCallback(smtsolver.smtSolver, smtsolver.availableSolvers[0]) }


Maybe we should show an example of how to pass in a custom function as a callback?

Otherwise, if user is expected to use smtCallback(), why don't we just expect its parameters instead of a full callback?

It's just way more convenient, there's 3 layers of different stuff here

Then maybe we should show both. I mean, this is the only reference doc we have for the library. Having an easy to run example is good but we should also say something about what the callback looks like. Looking quickly at README, I don't think it even mentions what args the actual callback takes. Only the args of this helper.

Ok, makes sense. Next PR tho? :D

Fine. Let's get this one merged :)

smtsolver.js

cameel · 2022-01-24T18:46:27Z

test/smtcallback.js

-      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) {


I think we should make it opt-out instead of opt-in. With some equivalent of the --no-smt flag. Otherwise it's too easy for such tests to never run in CI.

test/smtchecker.js

leonardoalt · 2022-01-24T18:50:52Z

@cameel

I think we should make it opt-out instead of opt-in. With some equivalent of the --no-smt flag. Otherwise it's too easy for such tests to never run in CI.

The annoying part about this is that the solc-js CI tests run a bunch of old versions that have no idea about this, I think it'd look quite ugly to just disable it in all of them

test/smtchecker.js

cameel · 2022-01-24T19:07:46Z

The annoying part about this is that the solc-js CI tests run a bunch of old versions that have no idea about this, I think it'd look quite ugly to just disable it in all of them

Maybe we could just have it wrapped in some helper that gets a version and tells us if it supports a modern version of the SMT stuff?

In any case, that's not a huge blocker for me, could be done separately. Would be nice to have but this PR has been waiting long enough :)

cameel

I found mostly typos and added a some suggestions about overall I see nothing wrong here.

As I said in one of my comments, I'd recommend testing it against solc-js tests in the main repo before we merge to avoid breakage.

leonardoalt · 2022-01-24T19:17:41Z

Updated the small things.
I would prefer to leave the --no-smt flag to a different PR to get this one merged. The tests are working with a pre-release binary.

axic · 2022-01-24T19:44:07Z

Please rebase now after #587 was merged (also likely need to run yarn lint:fix).

cameel · 2022-01-24T20:08:23Z

LGTM

leonardoalt force-pushed the smt_fix_tests branch from 5f84390 to 72221c3 Compare November 18, 2021 10:37

leonardoalt commented Nov 18, 2021

View reviewed changes

test/smtcallback.js Show resolved Hide resolved

leonardoalt requested a review from axic November 18, 2021 10:50

leonardoalt force-pushed the smt_fix_tests branch 2 times, most recently from 5e1ea98 to 5e037da Compare November 21, 2021 20:39

axic force-pushed the smt_fix_tests branch 2 times, most recently from 45ae5fe to 29d2b8b Compare January 19, 2022 17:09

axic reviewed Jan 19, 2022

View reviewed changes

smtsolver.js Show resolved Hide resolved

axic reviewed Jan 19, 2022

View reviewed changes

smtsolver.js Outdated Show resolved Hide resolved

axic reviewed Jan 19, 2022

View reviewed changes

test/smtcallback.js Show resolved Hide resolved

axic mentioned this pull request Jan 19, 2022

Proper SMT CHC tests #524

Closed

axic reviewed Jan 20, 2022

View reviewed changes

smtsolver.js Outdated Show resolved Hide resolved

leonardoalt force-pushed the smt_fix_tests branch from 1363a9d to f6fa111 Compare January 20, 2022 22:16

axic mentioned this pull request Jan 23, 2022

Typescript Base Support #566

Merged

axic reviewed Jan 23, 2022

View reviewed changes

README.md Outdated Show resolved Hide resolved

axic reviewed Jan 23, 2022

View reviewed changes

README.md Outdated Show resolved Hide resolved

axic reviewed Jan 23, 2022

View reviewed changes

README.md Show resolved Hide resolved

leonardoalt force-pushed the smt_fix_tests branch 5 times, most recently from 0017ffa to 8ed2597 Compare January 24, 2022 16:12

axic reviewed Jan 24, 2022

View reviewed changes

README.md Outdated Show resolved Hide resolved

leonardoalt force-pushed the smt_fix_tests branch from 8ed2597 to 96f47c3 Compare January 24, 2022 17:15

axic approved these changes Jan 24, 2022

View reviewed changes

cameel reviewed Jan 24, 2022

View reviewed changes

test/smtchecker.js Outdated Show resolved Hide resolved

cameel reviewed Jan 24, 2022

View reviewed changes

test/smtchecker.js Outdated Show resolved Hide resolved

cameel reviewed Jan 24, 2022

View reviewed changes

test/smtchecker.js Outdated Show resolved Hide resolved

cameel approved these changes Jan 24, 2022

View reviewed changes

leonardoalt force-pushed the smt_fix_tests branch from 96f47c3 to 9a893e7 Compare January 24, 2022 19:17

leonardoalt force-pushed the smt_fix_tests branch from 9a893e7 to 08d4aa8 Compare January 24, 2022 19:20

Leo Alt added 2 commits January 24, 2022 20:50

README changes

7767606

Fix smtchecker callback tests and add Eldarica

40d563f

axic force-pushed the smt_fix_tests branch from 08d4aa8 to 40d563f Compare January 24, 2022 19:52

axic requested a review from cameel January 24, 2022 19:52

leonardoalt merged commit a3ab8e1 into master Jan 24, 2022

leonardoalt deleted the smt_fix_tests branch January 24, 2022 20:24

cameel mentioned this pull request Jan 25, 2022

Fix the import of tmp in smtsolver.ts #592

Merged

This comment was marked as spam.

Sign in to view

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix smtchecker callback tests and add Eldarica #565

Fix smtchecker callback tests and add Eldarica #565

leonardoalt commented Nov 18, 2021 •

edited

Loading

leonardoalt Nov 18, 2021

leonardoalt Nov 18, 2021

leonardoalt Nov 18, 2021

cameel Jan 24, 2022

leonardoalt Nov 18, 2021

axic Jan 19, 2022

leonardoalt Jan 19, 2022

leonardoalt Nov 18, 2021

coveralls commented Nov 18, 2021 •

edited

Loading

leonardoalt commented Jan 20, 2022

axic commented Jan 24, 2022

axic left a comment

cameel Jan 24, 2022

leonardoalt Jan 24, 2022

cameel Jan 24, 2022

leonardoalt Jan 24, 2022

cameel Jan 24, 2022

cameel Jan 24, 2022

leonardoalt commented Jan 24, 2022

cameel commented Jan 24, 2022

cameel left a comment

leonardoalt commented Jan 24, 2022

axic commented Jan 24, 2022

cameel commented Jan 24, 2022

This comment was marked as spam.

Fix smtchecker callback tests and add Eldarica #565

Fix smtchecker callback tests and add Eldarica #565

Conversation

leonardoalt commented Nov 18, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

coveralls commented Nov 18, 2021 • edited Loading

leonardoalt commented Jan 20, 2022

axic commented Jan 24, 2022

axic left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

leonardoalt commented Jan 24, 2022

cameel commented Jan 24, 2022

cameel left a comment

Choose a reason for hiding this comment

leonardoalt commented Jan 24, 2022

axic commented Jan 24, 2022

cameel commented Jan 24, 2022

This comment was marked as spam.

leonardoalt commented Nov 18, 2021 •

edited

Loading

coveralls commented Nov 18, 2021 •

edited

Loading