VeriSol currently targets ConcurrencyExplorer tool to view traces generated through Corral. Support option to view traces through SdvDefectViewer distributed as part of Windows Static Driver Verifier.

Currently only expect uint/int and not types such as (a) int_const (b) uint32 etc.

Currently, we have to express 0 as 0x0 to distinguish it from the 0 as integer. Perhaps some kind of context based inference (e.g. argument to address(0)) should promote this to an address.

Crashes since string shows up as string memory.

Linked to #31

VeriSol does not model that unsigned values are non-negative. This can lead to false alarms.

Verisol crashes when it finds a "delete a[I];"

Add support for running the regression tests when building verisol.

While translating a method Foo in a contract C, we put an assumption that the dynamic type of this is C. We need to include all subtypes declared in the program.

To make installation and maintenance easier, it would be recommendable to include the project dependencies (i.e., Boogie, Corral, etc) as git submodules. It is important that each submodule refers to the the last commit that has been tested for this tool.

VeriSol does not currently support structs.

Debug.Assert(currentStmtList != null);
fails in TranslateStatement()

Exception happened in GetFuncDefintionsInContract()
0x0e3f73d56f4c2d0422412c035abccc2df90562f9.txt

There are various issues:

1. bugs related to import in directory structure (per @cs0317)
2. solc.exe does not build on mac properly

Once the regression script is up, we can switch over to newer compiler. All this would mean is to update the instructions.

See https://github.com/Microsoft/verisol/blob/master/Test/regressions/UsingFor.sol

Unhandled Exception: System.SystemException: Unknown form of function call expr: uint256/address
at SolToBoogie.TransUtils.GetFuncNameFromFuncCallExpr(Expression expr)

Examples:
uint8 public decimals = 18;
...
totalSupply = 200000000 * 10 ** uint256(decimals);

_transfer (msg.sender, address(this), totalSupply);
...
function _transfer(address _from, address _to, uint _value) internal {

pragma solidity ^0.4.24;
contract Tuple {
function testTuple() public pure{
(uint a, uint b) = (1, 3);
assert (a == 1);
assert (b == 3);
}
}

VeriSol ignores assignments that are done for state variables outside of the constructor.

This is a new operation recently added.

We also need the fact that for the reset state, all Boogie maps are zero/null/false initialized.

contract A {uint x; }
contract B {constructor (A a){ assert (a.x() == 0);}}

We give wrong results when there are deeply nested expressions such as

a[b].Foo(); 

It is fairly common to use keccak256 to compare strings:

return keccak256(string1) == keccak256(string2);

If we have certain kind of line breaks, then the line number calculation from AST spans gets confused. We need to have a solution.

The script setup_windows.cmd and run_verisol_win.cmd refer to a folder VERISOL_DEPENDENCIES_DIR which seems to be "\verisol_dependencies".
However, there is no such folder in the repository and no information about what files should be included there.

NestedArray.sol in regressions.

pragma solidity ^0.4.24;

contract B{
   function foo() returns (uint) {return 33;}
}

contract A {
   B[] a;
   constructor() public {
        B b = new B();
        a.push(b);
        assert (a[0].foo() == 33);       
   }
}

The translated Boogie program has syntax error on return expression statements. One simple example is

contract C {
    function foo() returns (uint a) {
        return 1;
    }
}

The bug is triggered when return parameters are named. Instead of setting a to 1, the translator emits __ret := 1 but variable __ret is not defined.

Also, for return statements with expressions, the translator fails to emit "return" after the assignment, which is problematic if the return statement is not at the end of the function body.

VeriSol would crash for the following example:

Unhandled Exception: System.ArgumentNullException: Value cannot be null. This was masked by the bug for missing constructors. For the case of an implicit constructor, we need to update "currentFunction" inside the implementation, as it is null, when trying to add some initialization code. @rongpan @Yuepeng-Wang

pragma solidity ^0.4.24;

contract Mapping {

    mapping (string => uint) m;

    function test() public {
        m["aa"] = 11;
        m["bb"] = 21;
        assert (m["aa"] == 11);
        assert (m["bb"] == 21);
    }

}

Test/regressions/Modifier.sol
Test/regressions/InternalRecursiveFunctionCall.sol

Unhandled Exception: System.SystemException: Unknown elementary type name: bytes32/bytes/uint64/uint16/uint8
at SolToBoogie.TransUtils.GetBoogieTypeFromSolidityTypeName(TypeName type)

a**b is not supported

This code:
`pragma solidity ^0.4.24;

contract Power {
function test1() public {
uint a = 2**3-1;
assert (a == 7);
}
}`

yield the following exception: Unhandled Exception: System.SystemException: Unknown binary operator: **
at SolToBoogie.ProcedureTranslator.Visit(BinaryOperation node) in .\verisol\Sources\SolToBoogie\ProcedureTranslator.cs:line 1866

Essentially, the function Convert.ToInt32 cannot handle "2**32-1".

Today, VeriSol just prints the error message

Unhandled Exception: System.SystemException: Unknown form of function call expr: address
when it crashes, without providing any hint of which line number or AST element being processed.

pragma solidity ^0.4.24;
contract A {
    address a;   
    constructor() public
    {
        a = address(0);
    }
}

VeriSol does not support modeling of payable contracts and attributes such as balance, and operations such as send, transfer, msg.value etc.

In the following code, foo(1) causes an exception in InferFunctionSignature because the type "int_const 1" is not supported.

pragma solidity ^0.4.24;
contract PublicPreviewMembers {
    constructor() public {      
          bool tmp= foo(1);  
    }

    function foo(uint x) internal returns (bool) {
           return true;
   }
}

A modifier invoking a helper function fails to to parse.
The error seems to be related to not having the field currentContract instantiated.

Unhandled Exception: System.ArgumentNullException: Value cannot be null.
Parameter name: key
at System.ThrowHelper.ThrowArgumentNullException(ExceptionArgument argument)
at System.Collections.Generic.Dictionary2.FindEntry(TKey key) at System.Collections.Generic.Dictionary2.ContainsKey(TKey key)
at SolToBoogie.TranslatorContext.HasEventNameInContract(ContractDefinition contract, String eventName) in .\verisol\Sources\SolToBoogie\TranslatorContext.cs:line 279
at SolToBoogie.ProcedureTranslator.Visit(FunctionCall node) in C:\Users\diegog\Source\Repos\verisol\Sources\SolToBoogie\ProcedureTranslator.cs:line 1254

pragma solidity ^0.4.24; contract ModifierFunc { function isValid(uint id) public view returns (bool) { return (id > 0); } modifier valid(uint id) { require(isValid(id), "id is not valid"); // this invocation produces an exception _; } }

The tool cannot support returning multiple values. For example,

    function foo() public returns (uint r1, uint r2) {
        return (1, 2);
    }

    function bar() public {
        uint a;
        uint b;
        (a, b) = foo();
        assert (a == 1);
        assert (b == 2);
    }

Verisol crashes:

Unhandled Exception: System.NullReferenceException: Object reference not set to an instance of an object.

since it is unable to find the function x() inside A.

pragma solidity ^0.4.24;

contract A {
    address public x;
}

contract B {
    A a;
    function Foo() public {
        a = new A();
        address y = a.x();
    }
}

System.ArgumentNullException: Value cannot be null.
Parameter name: key
at System.ThrowHelper.ThrowArgumentNullException(ExceptionArgument argument)
at System.Collections.Generic.Dictionary2.FindEntry(TKey key) at System.Collections.Generic.Dictionary2.get_Item(TKey key)

Happens in:
file: ProcedureTranslator.cs
method: CreateDistinctArrayMappingAddress()
line: functionToLocalVarsMap[currentFunction].Add(tmpVar);

Example:
Test/regressions/LoopContinue.sol

contract A {
    uint public y;
    function helper() private view returns (uint) {return 1;}
    constructor(A a) {y = helper(); assert (y == 1);}
}

generates ill-formed boogie program since assignment to y is a map assignment, and Boogie only allows assigning to scalars in a call return. This has to be broken up into a temporary.

Currently, the tool only prints:

at System.Diagnostics.Debug.Assert(Boolean condition, String message, String detailMessage)

which is not meaningful when running VeriSol from command line.

pragma solidity ^0.4.24;
interface IFoo {
function activate() external;
function getAddress() external view returns (address);
}

SolToBoogie reports:
Unhandled Exception: System.Exception: Contract IFoo does not have any constructors

We need to support deep copy of arrays for (a) passing arrays as arguments and returns, and (b) assignment between two storage arrays and other cases.