Leo

Improve DataFlowAnalyzer's performance

6

- [ ] Check if the call to `SyntacticallyEqual::operator()` can be made more efficienty - [ ] Check `yul::valueOfNumberLiteral` (cache it) - [ ] In `DataFlowAnalyzer`, don't always use `m_memory`...

``` pragma solidity ^0.8.6; import "ds-test/test.sol"; contract HevmbugTest is DSTest { // Passes function prove_dog(uint8[255] memory dog) public {} // Reverts function prove_cat(uint8[256] memory cat) public {} // Passes function...

SMT backend multi transaction counterexample

1

``` constructor of C interface constructor() creates uint x := 0 invariants x < 2 behaviour f of C interface f() case x == 0: storage x => 1 behaviour...

``` constructor of LValue interface constructor() creates uint x := 0 uint y := 2 invariants y == 2 behaviour f of LValue interface f() storage x => 0y =>...

Document the language

1

We should go through the structure of the language and each section

Loop invariants

1

@wilcoxjay and I talked today, and he suggested the idea of also expressing loop invariants in the spec. The challenge there is that loops don't have an interface, so how...

Oyente-based Bounded Model Checker (OBMC)

7

Hi, I've been working on a bounded model checker (I've been calling it OBMC) based on Oyente (it's in my fork, branch master). The approach is different from Oyente's, in...

Currently tests that use SMTEngine are skipped.

Proper SMT CHC tests

6

Depends on https://github.com/ethereum/solidity/pull/11421 This PR adds *proper* SMTChecker tests. Currently, the SMTChecker tests are actually broken, many tests are ignored, and the smtlib version of the SMTCheckre encoding is not...