ChenfengWei0 / esbmc

The efficient SMT-based bounded model checker
http://esbmc.org/
Other
0 stars 1 forks source link

solidity known bug #5

Open ChenfengWei0 opened 1 year ago

ChenfengWei0 commented 1 year ago
assert((data2 >> 16) == bytes2(0x7465));

Fixed

ChenfengWei0 commented 1 year ago
pragma solidity >=0.5.0;

contract Base {
    bytes16 data1;
    bytes4 data2;

    constructor() {
        data1 = "test";
        data2 = 0x74657374; // "test"
    }

    function test() public {
        assert(data1[1] == data2[1]);

        assert(data1[0] == 0x74);
        assert(data1[1] == 0x65);
        assert(data1[11] == 0x00); // error here
        assert(data1[6] == 0x00);

        assert(data2[1] == 0x65);
    }
}

contract Dreive {
    Base x = new Base();

    function test1() public {
        x.test();
    }
}
ChenfengWei0 commented 1 year ago
pragma solidity >=0.7.0;

contract IntegerOverflowUnderflow {
    uint256  counter = 2 ;
    constructor()
    {
        counter = 1;
    }
    function test() public {

        bytes16 x="test";
        for(uint i =0;i<=32;i++)
        {
            x[i];
        }
    }

}
ChenfengWei0 commented 1 year ago
//SPDX-License-Identifier: GPL-2.0
pragma solidity >=0.7.0;

contract IntegerOverflowUnderflow {
    uint256  counter = 2 ;
    constructor()
    {
        counter = 1;
    }
    function test() public {

        assert(counter == 0);
    }

}

Fixed

ChenfengWei0 commented 1 year ago
pragma solidity ^0.8.0;

contract Derived {
    uint x = 1;

    function test() public {
        assert(x == 1);
    }
}

contract Base {
    uint x = 0;

}

Bug: insert the state variable incorrectly

ChenfengWei0 commented 1 year ago
pragma solidity ^0.8.0;

contract Derived {
    uint x = 1;
    Base y = new Base();

    function test() public {
        assert(x == 1);
    }
}

contract Base {
    uint x = 0;
}

Conversion Error

ChenfengWei0 commented 1 year ago

if we do not enable solidity frontend, we should not be able to call option "contract"

ChenfengWei0 commented 1 year ago

constructor name error?

ChenfengWei0 commented 1 year ago
ChenfengWei0 commented 1 year ago
ChenfengWei0 commented 1 year ago
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.6.0;

contract Base {
    uint[] public a;

    function SelectionSort(uint array_size) public {
        uint i;
        uint j;
        uint min;
        uint temp;
        for (i = 0; i < array_size - 1; ++i) {
            min = i;
            for (j = i + 1; j < array_size; ++j) {
                if (a[j] < a[min]) min = j;
            }
            temp = a[i];
            a[i] = a[min];
            a[min] = temp;
        }
    }

    function test() public {
        uint array_size = 100;
        SelectionSort(array_size);
    }
}
ChenfengWei0 commented 1 year ago
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.6.0;

contract Base {
    function isOdd(uint n) public returns (uint) {
        if (n == 0) {
            return 0;
        } else if (n == 1) {
            return 1;
        } else {
            return isEven(n - 1);
        }
    }

    function isEven(uint n) public returns (uint) {
        if (n == 0) {
            return 1;
        } else if (n == 1) {
            return 0;
        } else {
            return isOdd(n - 1);
        }
    }

    function test() public {
        uint n = 20;
        uint result = isOdd(n);
        uint mod = n % 2;
        if (result < 0 || result == mod) {
            assert(n == result);
        }
    }
}
ChenfengWei0 commented 1 year ago
contract Base {
    uint public N = 3;
    uint[3] a;

    function quicksort(uint m, uint n) public {
        uint i;
        uint j;
        uint pivot;
        uint tmp;
        if (m < n) {
            pivot = a[n];
            i = m;
            j = n;
            while (i <= j) {
                while (a[i] < pivot) 
                {
                    i++;
                }
                while (a[j] > pivot) 
                {
                    j--;
                }
                if (i <= j) {
                    tmp = a[i];
                    a[i] = a[j];
                    a[j] = tmp;
                    i++;
                    j--;
                }
            }
            quicksort(m, j);
            quicksort(i, n);
        }
    }

    function test() public {
        uint i;
        for (i = 0; i < N; i++) 
        {
            a[i] = i;
        }
        quicksort(0, N - 1);
        assert(a[i] == i);
    }
}
ChenfengWei0 commented 1 year ago
// SPDX-License-Identifier: MIT
pragma solidity >=0.6.0;

contract Base {
    uint32 x;
    uint32 y;

    uint32[10] z;

    function h(uint32 w) public {
        x = x + 1;
        y = y + 1;
    }

    function strict_sorted(uint32 len, uint32 s) public view returns (bool) {
        uint32 i;
        for (i = s; i < len - 1; i++) {
            if (z[i] >= z[i + 1]) return false;
        }
        return true;
    }

    function sorted(uint32 len, uint32 s) public view returns (bool) {
        uint32 i;
        for (i = s; i < len - 1; i++) {
            if (z[i] > z[i + 1]) {
                return false;
            }
        }
        return true;
    }

    function g(uint32 w) public {
        uint32 i;
        assert(w >= 1);
        x = w;
        w--;
        y = w;
        for (i = 0; i < 10; i++) {
            z[i] = i;
        }
        assert(strict_sorted(10, 0) != false); // failed
        assert(x > y);
    }

    function f(uint32 j, uint32 k) public {
        assert(j > k);
        assert(j >= 0);
        assert((k > 10) && (k < 20));
        j -= k;
        g(j);
        j = k;
        y = k;
        g(j);
        h(j);
        assert(sorted(10, 5)); 
        assert(x >= y);
    }

    function test(uint32 x, uint32 y) public {
        require(x > y);
        require(x >= 0);
        require((y > 15) && (y < 18));
        f(x, y);
    }
}
ChenfengWei0 commented 1 year ago
contract BTX { 2
mapping (address => uint) public balance; 3
4 5 6 7 8 9
10 11 12 13 14
15 16
17 18 19 20
21 }
uint public totalSupply; constructor () {
totalSupply = 10000; balance[msg.sender] = 10000; }
function transfer (address to, uint value) { require (balance[msg.sender] >= value); balance[msg.sender] -= value; balance[to] += value; // Safe
}
function transferFrom (address from, address to, uint value) {
require (balance[from] >= value); balance[to] += value; // Safe balance[from] -= value;
}