Core Dump due to minisat running out of memory - Should show out of memory error

[jgwilson42]

The following code is taken from the openjdk regression suite:

/*
 * Copyright (c) 2007, 2013, Oracle and/or its affiliates. All rights reserved.
 * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
 *
 * This code is free software; you can redistribute it and/or modify it
 * under the terms of the GNU General Public License version 2 only, as
 * published by the Free Software Foundation.
 *
 * This code is distributed in the hope that it will be useful, but WITHOUT
 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
 * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
 * version 2 for more details (a copy is included in the LICENSE file that
 * accompanied this code).
 *
 * You should have received a copy of the GNU General Public License version
 * 2 along with this work; if not, write to the Free Software Foundation,
 * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
 *
 * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
 * or visit www.oracle.com if you need additional information or have any
 * questions.
 */

/* @test
   @summary Test AudioFloatInputStream getFormat method */

import java.io.*;

import javax.sound.sampled.*;

import com.sun.media.sound.*;

public class GetFormat {

    static float[] test_float_array;
    static byte[] test_byte_array;
    static AudioFormat format = new AudioFormat(44100, 16, 1, true, false);

    static AudioFloatInputStream getStream1()
    {
        return AudioFloatInputStream.getInputStream(format, test_byte_array, 0, test_byte_array.length);
    }

    static AudioFloatInputStream getStream2()
    {
        AudioInputStream strm = new AudioInputStream(new ByteArrayInputStream(test_byte_array), format, 1024);
        return AudioFloatInputStream.getInputStream(strm);
    }

    static void setUp() throws Exception {
        test_float_array = new float[1024];
        test_byte_array = new byte[1024*format.getFrameSize()];
        for (int i = 0; i < 1024; i++) {
            double ii = i / 1024.0;
            ii = ii * ii;
            test_float_array[i] = (float)Math.sin(10*ii*2*Math.PI);
            test_float_array[i] += (float)Math.sin(1.731 + 2*ii*2*Math.PI);
            test_float_array[i] += (float)Math.sin(0.231 + 6.3*ii*2*Math.PI);
            test_float_array[i] *= 0.3;
        }
        AudioFloatConverter.getConverter(format).toByteArray(test_float_array, test_byte_array);
    }

    public static void main(String[] args) throws Exception {
        setUp();
        if(!getStream1().getFormat().matches(format))
            throw new RuntimeException("Incorrect audio format returned.");
        if(!getStream2().getFormat().matches(format))
            throw new RuntimeException("Incorrect audio format returned.");
    }

}

When this is run with cbmc timeout 300 cbmc GetFormat.class The following output is given:

CBMC version 5.7 64-bit x86_64 linux
Parsing GetFormat.class
Java main class: GetFormat
failed to load class `java.lang.Exception'
failed to load class `java.lang.RuntimeException'
failed to load class `com.sun.media.sound.AudioFloatConverter'
failed to load class `java.lang.Math'
failed to load class `java.io.InputStream'
failed to load class `java.io.ByteArrayInputStream'
failed to load class `javax.sound.sampled.AudioInputStream'
failed to load class `com.sun.media.sound.AudioFloatInputStream'
failed to load class `javax.sound.sampled.AudioFormat'
failed to load class `java.lang.String'
failed to load class `java.lang.Object'
failed to load class `java.lang.Class'
Converting
Generating GOTO Program
Adding goto-destructor code on jump to pc28
Adding goto-destructor code on jump to pc53
Adding goto-destructor code on jump to pc142
Adding goto-destructor code on jump to pc25
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
**** WARNING: no body for function java::javax.sound.sampled.AudioFormat.<init>:(FIIZZ)V
Unwinding loop _start.0 iteration 1  thread 0
Unwinding loop _start.0 iteration 2  thread 0
Unwinding loop _start.0 iteration 3  thread 0
Unwinding loop _start.0 iteration 4  thread 0
Unwinding loop _start.0 iteration 5  thread 0
**** WARNING: no body for function java::javax.sound.sampled.AudioFormat.getFrameSize:()I
**** WARNING: no body for function java::java.lang.Math.sin:(D)D
Unwinding loop java::GetFormat.setUp:()V.0 iteration 1 file GetFormat.java line 53 function java::GetFormat.setUp:()V bytecode_index 79 thread 0
Unwinding loop java::GetFormat.setUp:()V.0 iteration 2 file GetFormat.java line 53 function java::GetFormat.setUp:()V bytecode_index 79 thread 0

<snip>

Unwinding loop java::GetFormat.setUp:()V.0 iteration 1024 file GetFormat.java line 53 function java::GetFormat.setUp:()V bytecode_index 79 thread 0
**** WARNING: no body for function java::com.sun.media.sound.AudioFloatConverter.getConverter:(Ljavax/sound/sampled/AudioFormat;)Lcom/sun/media/sound/AudioFloatConverter;
**** WARNING: no body for function java::com.sun.media.sound.AudioFloatConverter.toByteArray:([F[B)[B
**** WARNING: no body for function java::com.sun.media.sound.AudioFloatInputStream.getInputStream:(Ljavax/sound/sampled/AudioFormat;[BII)Lcom/sun/media/sound/AudioFloatInputStream;
**** WARNING: no body for function java::com.sun.media.sound.AudioFloatInputStream.getFormat:()Ljavax/sound/sampled/AudioFormat;
**** WARNING: no body for function java::javax.sound.sampled.AudioFormat.matches:(Ljavax/sound/sampled/AudioFormat;)Z
**** WARNING: no body for function java::java.lang.RuntimeException.<init>:(Ljava/lang/String;)V
**** WARNING: no body for function java::java.io.ByteArrayInputStream.<init>:([B)V
**** WARNING: no body for function java::javax.sound.sampled.AudioInputStream.<init>:(Ljava/io/InputStream;Ljavax/sound/sampled/AudioFormat;J)V
**** WARNING: no body for function java::com.sun.media.sound.AudioFloatInputStream.getInputStream:(Ljavax/sound/sampled/AudioInputStream;)Lcom/sun/media/sound/AudioFloatInputStream;
size of program expression: 37206 steps
simple slicing removed 164 assignments
Generated 14340 VCC(s), 7169 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
terminate called after throwing an instance of 'Minisat::OutOfMemoryException'
Post-processing
timeout: the monitored command dumped core

CBMC should handle memory exceptions from minisat in a more graceful way. Ideally for this code we should not be needing >10Gb of memory to process it.

[jgwilson42]

The following code (also from the openjdk regression suite) generates the same behaviour:

/*
 * Copyright (c) 2007, 2013, Oracle and/or its affiliates. All rights reserved.
 * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
 *
 * This code is free software; you can redistribute it and/or modify it
 * under the terms of the GNU General Public License version 2 only, as
 * published by the Free Software Foundation.
 *
 * This code is distributed in the hope that it will be useful, but WITHOUT
 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
 * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
 * version 2 for more details (a copy is included in the LICENSE file that
 * accompanied this code).
 *
 * You should have received a copy of the GNU General Public License version
 * 2 along with this work; if not, write to the Free Software Foundation,
 * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
 *
 * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
 * or visit www.oracle.com if you need additional information or have any
 * questions.
 */

/* @test
   @summary Test AudioFloatInputStream getFrameLength method */

import java.io.*;

import javax.sound.sampled.*;

import com.sun.media.sound.*;

public class GetFrameLength {

    static float[] test_float_array;
    static byte[] test_byte_array;
    static AudioFormat format = new AudioFormat(44100, 16, 1, true, false);

    static AudioFloatInputStream getStream1()
    {
        return AudioFloatInputStream.getInputStream(format, test_byte_array, 0, test_byte_array.length);
    }

    static AudioFloatInputStream getStream2()
    {
        AudioInputStream strm = new AudioInputStream(new ByteArrayInputStream(test_byte_array), format, 1024);
        return AudioFloatInputStream.getInputStream(strm);
    }

    static void setUp() throws Exception {
        test_float_array = new float[1024];
        test_byte_array = new byte[1024*format.getFrameSize()];
        for (int i = 0; i < 1024; i++) {
            double ii = i / 1024.0;
            ii = ii * ii;
            test_float_array[i] = (float)Math.sin(10*ii*2*Math.PI);
            test_float_array[i] += (float)Math.sin(1.731 + 2*ii*2*Math.PI);
            test_float_array[i] += (float)Math.sin(0.231 + 6.3*ii*2*Math.PI);
            test_float_array[i] *= 0.3;
        }
        AudioFloatConverter.getConverter(format).toByteArray(test_float_array, test_byte_array);
    }

    public static void main(String[] args) throws Exception {
        setUp();
        if(getStream1().getFrameLength() != 1024L)
            throw new RuntimeException("Incorrect frame length returned.");
        if(getStream2().getFrameLength() != 1024L)
            throw new RuntimeException("Incorrect frame length returned.");
    }

}

[martin-cs]

On Wed, 2017-03-29 at 11:50 -0700, James Wilson wrote:

The following code is taken from the openjdk regression suite:

CBMC should handle memory exceptions from minisat in a more graceful way.

What would you suggest; beyond throwing an exception / terminating there isn't much we can do.

Ideally for this code we should not be needing >10Gb of memory to process it.

Double precision multiplies are expensive. Without the exact command line you ran I can't say how many you have but it looks like lots.

Try --slice-formula and --refine; they might help. If not, assign to me.

[jgwilson42]

Terminating in a more graceful way i.e. giving a user friendly error message makes sense to me.

[martin-cs]

The problem is ... what do we say? We've run out of memory, there are a number of possible reasons, we can't get you the results, try again with a smaller problem of some kind.

The error message can definitely be improved beyond that it's hard to give anything specific.

[martin-cs]

What /should/ happen is cbmc/cbmc_parse_options.cpp:773 should catch the std::bad_alloc exception, print a message and gracefully topple over. I have my doubts over whether the output will require memory allocation and thus cause an uncaught exception to be raised from there. If this behaviour is repeatable then it should be pretty easy to catch this case by commenting out the output or using puts or some such that goes straight (no buffering) to stderr.

[jgwilson42]

The following files from openjdk regression suite also exhibited the same issue: http://hg.openjdk.java.net/jdk8/jdk8/jdk/file/687fd7c7986d/test/java/util/NavigableMap/LockStep.java http://hg.openjdk.java.net/jdk8/jdk8/jdk/file/687fd7c7986d/test/java/net/ProxySelector/MultiThreadedSystemProxies.java

[tautschnig]

I'm not entirely sure what this issue is about: the possibly not as user-friendly error message or the fact that CBMC runs out of memory at all? I'd suggest that the subject of this issue be amended accordingly. (Yet if it is the latter: there are infinitely many examples where CBMC will be running out of memory.)

[jgwilson42]

@tautschnig in this case the issue is that the out of memory error is not being passed back to the calling program.