[SMTChecker] Error with CHC engine, non-zero timeout and an assert: `thread constructor failed: Resource temporarily unavailable`
- Dominant language
- TypeScript
- Stars
- 1.5k
- Forks
- 349
- Avg merge
- 8m
- Merged PRs (30d)
- 1
Description
When I try to run SMTChecker with a piece of code that contains `assert(true)` or `assert(false)`, I get a weird error:
```
Unknown exception during compilation: thread constructor failed: Resource temporarily unavailable
```
It does not happen if I remove `"engine": "chc"` or `"timeout"` or use a timeout of zero. Seems to be a JS problem because the same input works fine with `solc`.
### `input.json`
```json
{
"language": "Solidity",
"settings": {
"modelChecker": {
"engine": "chc",
"timeout": 20000
}
},
"sources": {
"C.sol": {
"content": "contract C { function f() public { assert(true); } }"
}
}
}
```
### `solcjs` output
Compiler version: 0.8.6
```bash
cat input.json | ./solcjs --standard-json
```
```json
{
"errors": [
{
"component": "general",
"formattedMessage": "Unknown exception during compilation: thread constructor failed: Resource temporarily unavailable",
"message": "Unknown exception during compilation: thread constructor failed: Resource temporarily unavailable",
"severity": "error",
"type": "Exception"
}
],
"sources": {
"C.sol": {
"id": 0
}
}
}
```
### `solc` output
The problem does not happen with `solc`.
```bash
cat input.json | solc --standard-json
```
Compiler version: 0.8.6
```json
{
"errors": [
{
"component": "general",
"errorCode": "1878",
"formattedMessage": "Warning: SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing \"SPDX-License-Identifier: \" to each source file. Use \"SPDX-License-Identifier: UNLICENSED\" for non-open-source code. Please see https://spdx.org for more information.\n--> C.sol\n\n",
"message": "SPDX license identifier not provided in source file. Before publishing, consider adding a comment containing \"SPDX-License-Identifier: \" to each source file. Use \"SPDX-License-Identifier: UNLICENSED\" for non-open-source code. Please see https://spdx.org for more information.",
"severity": "warning",
"sourceLocation": {
"end": -1,
"file": "C.sol",
"start": -1
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "3420",
"formattedMessage": "Warning: Source file does not specify required compiler version! Consider adding \"pragma solidity ^0.8.6;\"\n--> C.sol\n\n",
"message": "Source file does not specify required compiler version! Consider adding \"pragma solidity ^0.8.6;\"",
"severity": "warning",
"sourceLocation": {
"end": -1,
"file": "C.sol",
"start": -1
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "2018",
"formattedMessage": "Warning: Function state mutability can be restricted to pure\n --> C.sol:1:14:\n |\n1 | contract C { function f() public { assert(true); } }\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n",
"message": "Function state mutability can be restricted to pure",
"severity": "warning",
"sourceLocation": {
"end": 50,
"file": "C.sol",
"start": 13
},
"type": "Warning"
},
{
"component": "general",
"errorCode": "6328",
"formattedMessage": "Warning: CHC: Assertion violation might happen here.\n --> C.sol:1:36:\n |\n1 | contract C { function f() public { assert(true); } }\n | ^^^^^^^^^^^^\n\n",
"message": "CHC: Assertion violation might happen here.",
"severity": "warning",
"sourceLocation": {
"end": 47,
"file": "C.sol",
"start": 35
},
"type": "Warning"
}
],
"sources": {
"C.sol": {
"id": 0
}
}
}
```
Contributor guide
No contributing guide indexed for this repository
Research direction
Reproduce the failure with the provided input.json by piping it to ./solcjs --standard-json, then compare the result with solc --standard-json. Trace the solcjs standard-json entry point and the SMTChecker CHC path involved by the engine and timeout settings; done means the assert input no longer reports the thread-constructor exception and retains the expected compiler diagnostics.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- solidity, typescript
- Domain
- compilers, tooling
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100