argotorg / argotorg/solc-js

[SMTChecker] Error with CHC engine, non-zero timeout and an assert: `thread constructor failed: Resource temporarily unavailable`

Open
#535 2 comments 0 reactions 0 assignees View on GitHub
bug :bug:
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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.