britikovki/aeval

ADT-processing for test generation

About

A functional synthesis tool based on the Z3 SMT solver. It expects single-invocation specifications over linear integer/real arithmetic, encoded as forall-exists formulas, and aims at generating witnessing Skolem functions for (possibly, many) existentially-quantified variables. See the VMCAI'19 paper for more details.

Installation

Compiles with gcc-7 (on Linux) and clang-900 (on Mac). Assumes preinstalled Gmp (with the --enable-cxx flag) and Boost 1.71 packages.

• cd aeval ; mkdir build ; cd build
• cmake ../
• make to build dependencies (i.e., it needs a particular version of Z3 and installs it automatically)
• make to build AE-VAL

The binary of AE-VAL can be found in build/tools/aeval/.

Usage

The tool takes as input formulas in SMT-LIB v2, e.g., the following specification for the max function:

(assert (forall ((x1 Int) (x2 Int))
    (exists ((y Int))
        (and (>= y x1) (>= y x2) (or (= y x1) (= y x2))))))

Running aeval --skol max.smt2 yields the realizability result valid and the extracted Skolem for the y variable:

Iter: 2; Result: valid
(define-fun y ((x1 Int)(x2 Int)) Int
    (ite (<= (+ x1 (- x2)) 0) x2 x1))

aeval's Issues

[BUG]: In some cases when analysing CHCs index_cycle_chc is empty

Bug report

Bug description

When running a chc-encoded version of three contracts, connected in inheritance chain, it is possible that tg-nonlin will fail due to the fact that it can't fund any index_cycles.

To reproduce

For following files:

• Solidity
• CHC

TGNonlin follows this behavior:

1. Tries to find any index_cycles (lines 564-575 of HornNonlin.hpp), fails to find any
2. Reverts at line 577

Expected behaviour

Based on the CHC analysis it should be able to find at least some cases, where CHC destination is also a source for some other CHC predicate, even for the case when there are no functions and only constructors in the contract.

Files or input data

The running comand:

tgnonlin --keys contract_Cv1_131:state,msg.value,msg.sender constructor_state_variable_init_updated.smt2

Additional context

Same problem holds for a set of constructor_state_variable benchmarks:

• Solidity
• CHC
• Solidity
• CHC

I suppose it is connected with a fact that there are no functions in the contracts.

[BUG] TG-Nonlin: using "const-array" in generating tests for the regression benchmarks

Describe the bug
Aeval creates tests for the loops/while_nested_break.sol. The tests it creates contain const-array and INT values as a part of the input parameters for the tested function.

To Reproduce
Steps to reproduce the behavior:

1. Go to the core directory of the Solidity Testgen
2. Run python3 ./scripts/SolidityTestGen.py -i script/loops/while_nested_break.sol
3. See error

Or, if you have while_nested_break_updated.smt2

1. Go to the build directory of the tg-nonlin
2. Run ./tools/nonlin/tgnonlin --keys contract_C_78:^f__77:x,y,b,c /Users/konstantin.britikov/Documents/SMT/rand_proj/sandbox/while_nested_break_updated.smt2
3. See error

Expected behavior
A test which consists only out of int and bool values, no arrays.

Screenshots

Additional context

[BUG?]: Some issue with seemingly trivial constructor

Bug report

Bug description

It is not necessarily a bug, but just a behaviour curiosity. TgNonlin can produce tests for the whole constructors set of benchmarks except for one: constructor_4.sol. For this contract solving never reaches generating any tests.

This curious behavior may be connected to the unique architecture of the constructor, as constructor also calls a constructor of it's parent, passing as an input value a function call execution of his parent. This contract compiles though, so supposedly this behaviour is correct from the blockchain standpoint.

To reproduce

For a following file:
*Solidity
*CHC

TGNonlin follows this behavior:

1. Proceeds with a solving but never finds any tests

Expected behaviour

Multiple tests are generated to cover function f behaviour.

Files or input data

Execution command:

tgnonlin --keys contract_C4_91:state,msg.value,msg.sender^f__90:state,msg.value,msg.sender,a constructor_4_updated.smt2

Additional context

[BUG] TG-Nonlin: generates tests with incorrect constructor ABIs

Bug report

Bug description

TGNonlin seems to sometimes do not catch the correct interfaces. Specifically, there is a case when it cannot find and assign a correct variable to the constructor, but still somehow produces the model for the tests.

To reproduce

For following files:

• Solidity
• CHC

TGNonlin follows this behavior:

1. Receives a call to run the testgen for contract B:

./build/tgnonlin --keys contract_B3_94:state,msg.value,msg.sender,b^f3__75:state,msg.value,msg.sender^g3__93:state,msg.value,msg.sender /Users/konstantin.britikov/Documents/SMT/solidity_testgen/sandbox/constructor_3_updated.smt2

2. Finds a satisfying model, tries to assign at least some values.
3. At lines 659-661 of NonlinCHCsolver.cpp it can't find variable b. Based on the printed tree_map, variable b is not encountered at all.

Expected behaviour

Based on the CHC analysis it should be able to find the value for variable b, because it is a required variable to call a constructor of the B contract.

Files or input data

The running comand:

./build/tgnonlin --keys contract_B3_94:state,msg.value,msg.sender,b^f3__75:state,msg.value,msg.sender^g3__93:state,msg.value,msg.sender /Users/konstantin.britikov/Documents/SMT/solidity_testgen/sandbox/constructor_3_updated.smt2

Additional context

Reason behind this behaviour might be the fact that there are two contracts in the file being tested, and tgnonlin is being confused by the fact, which one to use (partially because one is inherited by another one). This can be because of the encoding...
Constructor is found in the tree map and it has a vars instead of bs, B constructor calls on constructor of A, but still, it receives int b as an input, it might be some simplification on the encoding site, but I doubt it tbh

Screenshots

[BUG]: SegFault while trying get_set()

Bug report

Bug description

An execution of tgnonlin on some encodings may cause segfault due to the exception in the get_set function.

To reproduce

For a following file:

• Solidity
• CHC

Run command:
tgnonlin --keys contract_Ownable_75:state,msg.value,msg.sender,initialOwner^owner__60:state,msg.value,msg.sender ./Ownable_updated.smt2

Run command:

Another example:

• Solidity
• CHC

Run command:
tgnonlin --keys contract_Ownable_75:state,msg.value,msg.sender,initialOwner^owner__60:state,msg.value,msg.sender ./Ownable_updated.smt2

TGNonlin follows this behavior:

1. NonlinCHCSolver is executed until line 564
2. On the call t->get_set, get_set function recurres
3. Recursion ends up in the SegFault(as for some specific node there are no children)

Expected behaviour

File is processed correctly.

[FEAT]: TGNonlin should support byte operations

Feature request

Feature Description

Currently we can't support any contracts that do even the simplest operations with bytes and bitvectors, we should add the capabilities of tgnonlin to handle them.

Required changes

Requirements which implemented feature should support:

1. (_ int2bv 256) should be supported by the marshaling/unmarshaling
2. int2bv can be encoded as UF possibly

Examples

This is the industrial contract which we can't currently support due to the lack of int2bv:

• Solidity
• CHC

This is the minimized version of this problem:

• Solidity
• CHC

Additional context