Change SMTChecker default settings #14053

leonardoalt · 2023-03-16T12:18:37Z

We're doing a few things here regarding the default values for the model checker settings:

Timeout has a default value of 1 second now. The SMTCheckerTests still need to use the old rlimit for reproducibility, which is done by overriding the timeout value in the settings
Only assertions are checked by default. The others need to be enabled explicitly, as already was the case for overflow and underflow.
If Eldarica is the chosen solver and the user has not explicitly set a value for divModNoSlacks we automatically make it true because that works better for Eldarica.

leonardoalt · 2023-03-16T12:20:29Z

test/cmdlineTests/model_checker_divModSlacks_default_all/args

@@ -1 +1 @@
--model-checker-engine all
+--model-checker-engine all --model-checker-targets divByZero


Had to add this now for this test and the ones below because divByZero is not checked by default anymore. That's the only extra target these tests need.

leonardoalt · 2023-03-16T12:21:07Z

test/cmdlineTests/model_checker_targets_default_all_engines/err

@@ -1,18 +1,3 @@
-Warning: CHC: Division by zero happens here.


These chunks were deleted from this test and the ones below because these properties are not checked by default anymore. This is fine for the tests because we have the same tests with targets = all which tests the whole set.

leonardoalt · 2023-03-16T12:21:32Z

test/cmdlineTests/model_checker_timeout_all/args

@@ -1 +1 @@
--model-checker-engine all --model-checker-timeout 1000
+--model-checker-engine all --model-checker-timeout 1000 --model-checker-targets all


Had to add this here because more properties are checked besides assertions. Same for the tests below.

leonardoalt · 2023-03-16T12:21:50Z

test/cmdlineTests/standard_model_checker_divModSlacks_default_all/input.json

@@ -16,6 +16,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["divByZero"],


Same case from the CLI tests.

leonardoalt · 2023-03-16T12:21:56Z

test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json

@@ -1,44 +1,6 @@
 {
    "errors":
    [
-        {


Same case from the CLI tests.

leonardoalt · 2023-03-16T12:22:24Z

test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json

@@ -3,7 +3,8 @@
    {
        "smtlib2queries":
        {
-            "0x75b95497d56c30e254a59358d72ddd4e78f9e90db621cfe677e85d05b2252411": "(set-option :produce-models true)
+            "0x1709577b0e186388ed08c2cf085f20c115c4c94745fb102c5be552ff2e4c7028": "(set-option :produce-models true)


The hashes changed because the timeout is now added by default, which in smtlib have their own specific command (set-timeout).

leonardoalt · 2023-03-16T12:22:34Z

test/cmdlineTests/standard_model_checker_timeout_all/input.json

@@ -11,6 +11,7 @@
 	{
 		"modelChecker":
 		{
+			"targets": ["assert", "divByZero"],


Same case from the CLI tests.

nikola-matic · 2023-03-16T14:27:30Z

docs/smtchecker.rst

@@ -34,16 +33,27 @@ The other verification targets that the SMTChecker checks at compile time are:
 - Out of bounds index access.
 - Insufficient funds for a transfer.

-All the targets above are automatically checked by default if all engines are
-enabled, except underflow and overflow for Solidity >=0.8.7.
+By default, for Solidity >=0.8.20 only assertions are checked.  For Solidity


Suggested change

By default, for Solidity >=0.8.20 only assertions are checked. For Solidity

By default, for Solidity >=0.8.20 only assertions are checked. For Solidity

nikola-matic · 2023-03-16T14:27:45Z

docs/smtchecker.rst

-enabled, except underflow and overflow for Solidity >=0.8.7.
+By default, for Solidity >=0.8.20 only assertions are checked.  For Solidity
+>=0.8.7 all the targets above are checked by default except for underflow and
+overflow.  Underflow and overflow are also in the default set for Solidity


Suggested change

overflow. Underflow and overflow are also in the default set for Solidity

overflow. Underflow and overflow are also in the default set for Solidity

nikola-matic · 2023-03-16T14:28:20Z

docs/smtchecker.rst

+By default, for Solidity >=0.8.20 only assertions are checked.  For Solidity
+>=0.8.7 all the targets above are checked by default except for underflow and
+overflow.  Underflow and overflow are also in the default set for Solidity
+<0.8.7.  The above only applies for the default targets which can be


Suggested change

<0.8.7. The above only applies for the default targets which can be

<0.8.7. The above only applies for the default targets, which can be

Now I'm kinda curious. Are you using double whitespaces on purpose?

No, I just use vim's automated gq which aligns the lines and ends up adding extra whitespaces sometimes

libsolidity/formal/ModelCheckerSettings.h

test/libsolidity/SMTCheckerTest.cpp

libsolidity/interface/CompilerStack.cpp

github-actions · 2023-04-02T12:04:35Z

This pull request is stale because it has been open for 14 days with no activity.
It will be closed in 7 days unless the stale label is removed.

github-actions · 2023-05-08T12:04:16Z

This pull request is stale because it has been open for 14 days with no activity.
It will be closed in 7 days unless the stale label is removed.

github-actions · 2023-05-23T12:04:12Z

This pull request is stale because it has been open for 14 days with no activity.
It will be closed in 7 days unless the stale label is removed.

github-actions · 2023-06-19T12:04:28Z

This pull request is stale because it has been open for 14 days with no activity.
It will be closed in 7 days unless the stale label is removed.

github-actions · 2023-06-26T12:04:59Z

This pull request was closed due to a lack of activity for 7 days after it was stale.

leonardoalt commented Mar 16, 2023

View reviewed changes

leonardoalt requested review from nikola-matic and ekpyron March 16, 2023 12:22

nikola-matic reviewed Mar 16, 2023

View reviewed changes

github-actions bot added the stale The issue/PR was marked as stale because it has been open for too long. label Apr 2, 2023

nikola-matic removed the stale The issue/PR was marked as stale because it has been open for too long. label Apr 2, 2023

NunoFilipeSantos assigned leonardoalt Apr 17, 2023

cameel added the smt label Apr 24, 2023

github-actions bot added the stale The issue/PR was marked as stale because it has been open for too long. label May 8, 2023

leonardoalt removed the stale The issue/PR was marked as stale because it has been open for too long. label May 8, 2023

github-actions bot added the stale The issue/PR was marked as stale because it has been open for too long. label May 23, 2023

leonardoalt removed the stale The issue/PR was marked as stale because it has been open for too long. label May 24, 2023

leonardoalt added 2 commits May 24, 2023 12:03

change SMTChecker default settings

e698a22

emscripten z3

3e76fd4

leonardoalt force-pushed the smt_default_timeout branch from f3f3e7d to 3e76fd4 Compare May 24, 2023 10:05

github-actions bot added the stale The issue/PR was marked as stale because it has been open for too long. label Jun 19, 2023

github-actions bot added the closed-due-inactivity label Jun 26, 2023

github-actions bot closed this Jun 26, 2023

leonardoalt mentioned this pull request Nov 6, 2023

change SMTChecker default settings #14666

Closed

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Change SMTChecker default settings #14053

Change SMTChecker default settings #14053

leonardoalt commented Mar 16, 2023

leonardoalt Mar 16, 2023

leonardoalt Mar 16, 2023

leonardoalt Mar 16, 2023

leonardoalt Mar 16, 2023

leonardoalt Mar 16, 2023

leonardoalt Mar 16, 2023

leonardoalt Mar 16, 2023

nikola-matic Mar 16, 2023

nikola-matic Mar 16, 2023

nikola-matic Mar 16, 2023

leonardoalt Mar 17, 2023

github-actions bot commented Apr 2, 2023

github-actions bot commented May 8, 2023

github-actions bot commented May 23, 2023

github-actions bot commented Jun 19, 2023

github-actions bot commented Jun 26, 2023

		@@ -1 +1 @@
		--model-checker-engine all
		--model-checker-engine all --model-checker-targets divByZero

		@@ -1,18 +1,3 @@
		Warning: CHC: Division by zero happens here.

	By default, for Solidity >=0.8.20 only assertions are checked. For Solidity
	By default, for Solidity >=0.8.20 only assertions are checked. For Solidity

	overflow. Underflow and overflow are also in the default set for Solidity
	overflow. Underflow and overflow are also in the default set for Solidity

	<0.8.7. The above only applies for the default targets which can be
	<0.8.7. The above only applies for the default targets, which can be

Change SMTChecker default settings #14053

Change SMTChecker default settings #14053

Conversation

leonardoalt commented Mar 16, 2023

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

github-actions bot commented Apr 2, 2023

github-actions bot commented May 8, 2023

github-actions bot commented May 23, 2023

github-actions bot commented Jun 19, 2023

github-actions bot commented Jun 26, 2023