Segfaults in Java bindings

svenkeidel commented 1 month ago

Hi, thank you for your hard work maintaining this library :+1:

I encountered several segfaults when using the Java interface of Elina.

The first is in file https://github.com/eth-sri/ELINA/blob/master/java_interface/elina/Test.java. The segfault occurs at the end of the test case for polyhedra when the finalizer is called (first_segfault.log):

ELINA Polyhedra
=========
...
expand: <universal>
fold: <universal>
chg-env: {  1t = 0 }
unify: {  1t = 0 }
rename: <universal>
min-env: ( i: { }, r: { } ) : <universal>
[thread 5458 also had an error]
#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x00007f3cfbe44393, pid=5425, tid=5436
#
# JRE version: OpenJDK Runtime Environment (19.0.2+7) (build 19.0.2+7-nixos)
# Java VM: OpenJDK 64-Bit Server VM (19.0.2+7-nixos, mixed mode, sharing, tiered, compressed oops, compressed class ptrs, g1 gc, linux-amd64)
# Problematic frame:
# C  [libpartitions.so+0x2393]  free_comp_list+0x23
---------------  T H R E A D  ---------------

Current thread (0x00007f3cfc12a2b0):  JavaThread "Finalizer" daemon [_thread_in_native, id=5436, stack(0x00007f3cd0ea6000,0x00007f3cd0fa6000)]

Stack: [0x00007f3cd0ea6000,0x00007f3cd0fa6000],  sp=0x00007f3cd0fa4300,  free space=1016k
Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code)
C  [libpartitions.so+0x2393]  free_comp_list+0x23

Java frames: (J=compiled Java code, j=interpreted, Vv=VM code)
j  apron.Abstract0.finalize()V+0
J 1420 c1 java.lang.System$2.invokeFinalize(Ljava/lang/Object;)V java.base@19.0.2 (5 bytes) @ 0x00007f3ce4e7c9c4 [0x00007f3ce4e7c8c0+0x0000000000000104]
j  java.lang.ref.Finalizer.runFinalizer(Ljdk/internal/access/JavaLangAccess;)V+115 java.base@19.0.2
j  java.lang.ref.Finalizer$FinalizerThread.run()V+29 java.base@19.0.2
v  ~StubRoutines::call_stub 0x00007f3cec137cc6

The second segfault occurs when getting the bound of an Mpq scalar (second_segfault.log):

import gmp.*;
import apron.*;
import elina.*;

public class ElinaTest {
    public static void main(String args[]) throws ApronException {
        Manager manager = new elina.OptPoly(false);
        Environment env = new Environment();
        Abstract1 abs1 = new Abstract1(manager, env);
        Interval iv = abs1.getBound(manager, new Texpr1Intern(env, new Texpr1CstNode(new MpqScalar(new Mpq(-100)))));
        System.out.println(iv);
    }
}

#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x00007f438de29340, pid=6825, tid=6826
#
# JRE version: OpenJDK Runtime Environment (19.0.2+7) (build 19.0.2+7-nixos)
# Java VM: OpenJDK 64-Bit Server VM (19.0.2+7-nixos, mixed mode, sharing, tiered, compressed oops, compressed class ptrs, g1 gc, linux-amd64)
# Problematic frame:
# V  [libjvm.so+0xe29340]  JVM_handle_linux_signal+0x1b0

---------------  T H R E A D  ---------------

Current thread (0x00007f4388018ec0):  JavaThread "main" [_thread_in_native, id=6826, stack(0x00007f438cf00000,0x00007f438d000000)]

Stack: [0x00007f438cf00000,0x00007f438d000000],  sp=0x00007f438cffdba0,  free space=1014k
Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code)
V  [libjvm.so+0xe29340]  JVM_handle_linux_signal+0x1b0
C  [libc.so.6+0x3deb0]

Java frames: (J=compiled Java code, j=interpreted, Vv=VM code)
j  apron.Abstract0.getBound(Lapron/Manager;Lapron/Texpr0Intern;)Lapron/Interval;+0
j  apron.Abstract1.getBound(Lapron/Manager;Lapron/Texpr1Intern;)Lapron/Interval;+17
j  sturdy.apron.ElinaTest.main([Ljava/lang/String;)V+60
v  ~StubRoutines::call_stub 0x00007f4378137cc6

svenkeidel commented 1 month ago

These problems seem to be specific to Elina's Polyhedra as they do not occur with Apron's Polyhedra.

svenkeidel commented 1 month ago

Here are the nix packaging files I used to build the Java interface for Elina:

To compile install the nix package manager and run nix build .#numerical-analysis-libraries from the directory of the flake file. The compiled binaries can be found in ./result/lib

eth-sri / ELINA

Segfaults in Java bindings #98