vorpal-research / kex Goto Github PK

private suspend fun collectTrace(method: Method, parameters: Parameters<Descriptor>): ExecutionResult? = try {
    val generator = UnsafeGenerator(ctx, method, testNameGenerator.generateName(method, parameters))
    generator.generate(parameters)
    val testFile = generator.emit()

    compilerHelper.compileFile(testFile)
    collectTrace(generator.testKlassName)
} catch (e: Exception) {
    log.debug(e.stackTraceToString())
    null
}

public final class ListConcolicTests<E> extends AbstractBagDecorator<E> {
    
    private static final long serialVersionUID = -2560033712679053143L;

    public static <E> Bag<E> collectionBag(final Bag<E> bag) {
        return new ListConcolicTests<>(bag);
    }
    public ListConcolicTests(final Bag<E> bag) {
        super(bag);
    }
    private void writeObject(final ObjectOutputStream out) throws IOException {
        out.defaultWriteObject();
        out.writeObject(decorated());
    }
    @SuppressWarnings("unchecked") // will throw CCE, see Javadoc
    private void readObject(final ObjectInputStream in) throws IOException, ClassNotFoundException {
        in.defaultReadObject();
        setCollection((Collection<E>) in.readObject());
    }
    @Override
    public boolean containsAll(final Collection<?> coll) {
        return coll.stream().allMatch(this::contains);
    }
    @Override
    public boolean add(final E object) {
        return add(object, 1);
    }

    @Override
    public boolean addAll(final Collection<? extends E> coll) {
        boolean changed = false;
        for (final E current : coll) {
            final boolean added = add(current, 1);
            changed = changed || added;
        }
        return changed;
    }
    @Override
    public boolean remove(final Object object) {
        return remove(object, 1);
    }
    @Override
    public boolean removeAll(final Collection<?> coll) {
        if (coll != null) {
            boolean result = false;
            for (final Object obj : coll) {
                final boolean changed = remove(obj, getCount(obj));
                result = result || changed;
            }
            return result;
        }
        // let the decorated bag handle the case of null argument
        return decorated().removeAll(null);
    }
    @Override
    public boolean retainAll(final Collection<?> coll) {
        if (coll != null) {
            boolean modified = false;
            final Iterator<E> e = iterator();
            while (e.hasNext()) {
                if (!coll.contains(e.next())) {
                    e.remove();
                    modified = true;
                }
            }
            return modified;
        }
        // let the decorated bag handle the case of null argument
        return decorated().retainAll(null);
    }
    @Override
    public boolean add(final E object, final int count) {
        decorated().add(object, count);
        return true;
    }
}

<dependency>
    <groupId>org.apache.commons</groupId>
    <artifactId>commons-collections4</artifactId>
    <version>4.4</version>
</dependency>

    public void foo(char[][] a) {
        if (a.length > 10) {
            if (a[0].length < 2) {
                System.out.println("s");
            }
        }
    }

./kex.sh --jar fescar-core-0.1.0-SNAPSHOT.jar --target com.alibaba.fescar.core.*

#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x00007fc4d5664cc0, pid=3034021, tid=0x00007fc51f6f0700
#
# JRE version: OpenJDK Runtime Environment (8.0_242-b08) (build 1.8.0_242-b08)
# Java VM: OpenJDK 64-Bit Server VM (25.242-b08 mixed mode linux-amd64 compressed oops)
# Problematic frame:
# C  [libz3.so+0x1f7cc0]  Z3_mk_fpa_to_fp_float+0x60
#
# Core dump written. Default location: /home/abdullin/workspace/kex/core or core.3034021
#
# An error report file with more information is saved as:
# /home/abdullin/workspace/kex/hs_err_pid3034021.log
#
# If you would like to submit a bug report, please visit:
#   http://bugreport.java.com/bugreport/crash.jsp
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.
#

[loop]
derollCount = 3
maxDerollCount = 0

(BEGIN
 <OR> (
  @P arg$0 = 1
  @S %1 = 0
),  <OR> (
  @P arg$0 = 3
  @S %1 = 1
),  <OR> (
  @P arg$0 !in (0, 1, 2, 3)
  @S %1 = 10
) END) -> (
  @S <retval> = %1
)