alexf91 / lean4-ctypes

FFI for Lean 4
Apache License 2.0
3 stars 0 forks source link

Valgrind reports errors #9

Closed alexf91 closed 8 months ago

alexf91 commented 8 months ago

Errors appear to originate in calls to generated test functions. Regardless of the original source, either the testcase itself or a C++ function, they should be fixed to produce a clean output when all tests succeed.

==551942== Memcheck, a memory error detector
==551942== Copyright (C) 2002-2022, and GNU GPL'd, by Julian Seward et al.
==551942== Using Valgrind-3.21.0 and LibVEX; rerun with -h for copyright info
==551942== Command: build/bin/tests --no-color
==551942== 
============================= test session starts =============================
Tests.CType ................
Tests.Basic.Function ==551942== Use of uninitialised value of size 8
==551942==    at 0x4854112: foo (library.c:5)
==551942==    by 0x48A34F5: ffi_call_unix64 (unix64.S:104)
==551942==    by 0x489FF5D: ffi_call_int.lto_priv.0 (ffi64.c:673)
==551942==    by 0x48A2B72: ffi_call (ffi64.c:710)
==551942==    by 0x7ABC81: Function::call(lean_object*) (function.cpp:98)
==551942==    by 0x7ABFBD: Function_call (function.cpp:123)
==551942==    by 0x626778: l_main___lambda__54 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x62762E: l_main___lambda__54___boxed (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x32A12C3: lean_apply_2 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x32A052C: lean_apply_1 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x6A720D: l_IO_withStderr___at_LTest_captureResult___spec__1___rarg (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x32A052C: lean_apply_1 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==  Uninitialised value was created by a stack allocation
==551942==    at 0x489FDF0: ffi_call_int.lto_priv.0 (ffi64.c:588)
==551942== 
==551942== Invalid write of size 4
==551942==    at 0x4854112: foo (library.c:5)
==551942==    by 0x48A34F5: ffi_call_unix64 (unix64.S:104)
==551942==    by 0x489FF5D: ffi_call_int.lto_priv.0 (ffi64.c:673)
==551942==    by 0x48A2B72: ffi_call (ffi64.c:710)
==551942==    by 0x7ABC81: Function::call(lean_object*) (function.cpp:98)
==551942==    by 0x7ABFBD: Function_call (function.cpp:123)
==551942==    by 0x626778: l_main___lambda__54 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x62762E: l_main___lambda__54___boxed (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x32A12C3: lean_apply_2 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x32A052C: lean_apply_1 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x6A720D: l_IO_withStderr___at_LTest_captureResult___spec__1___rarg (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x32A052C: lean_apply_1 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==  Address 0x7c59b08 is 136 bytes inside a block of size 256 free'd
==551942==    at 0x484475F: operator delete(void*) (vg_replace_malloc.c:1025)
==551942==    by 0x7AB1AC: std::__new_allocator<unsigned long>::deallocate(unsigned long*, unsigned long) (new_allocator.h:168)
==551942==    by 0x7AB167: deallocate (allocator.h:210)
==551942==    by 0x7AB167: deallocate (alloc_traits.h:516)
==551942==    by 0x7AB167: std::_Vector_base<unsigned long, std::allocator<unsigned long> >::_M_deallocate(unsigned long*, unsigned long) (stl_vector.h:387)
==551942==    by 0x7AB096: std::_Vector_base<unsigned long, std::allocator<unsigned long> >::~_Vector_base() (stl_vector.h:366)
==551942==    by 0x7AB03B: std::vector<unsigned long, std::allocator<unsigned long> >::~vector() (stl_vector.h:735)
==551942==    by 0x7C503C: CTypeArray::buffer(LeanValue const&) const (array.hpp:81)
==551942==    by 0x7ABADF: Function::call(lean_object*) (function.cpp:87)
==551942==    by 0x7ABFBD: Function_call (function.cpp:123)
==551942==    by 0x626778: l_main___lambda__54 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x62762E: l_main___lambda__54___boxed (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x32A12C3: lean_apply_2 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x32A052C: lean_apply_1 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==  Block was alloc'd at
==551942==    at 0x4841FC3: operator new(unsigned long) (vg_replace_malloc.c:472)
==551942==    by 0x7BBCED: std::__new_allocator<unsigned long>::allocate(unsigned long, void const*) (new_allocator.h:147)
==551942==    by 0x7BBB23: allocate (allocator.h:198)
==551942==    by 0x7BBB23: allocate (alloc_traits.h:482)
==551942==    by 0x7BBB23: std::_Vector_base<unsigned long, std::allocator<unsigned long> >::_M_allocate(unsigned long) (stl_vector.h:378)
==551942==    by 0x7BB711: void std::vector<unsigned long, std::allocator<unsigned long> >::_M_realloc_insert<unsigned long const&>(__gnu_cxx::__normal_iterator<unsigned long*, std::vector<unsigned long, std::allocator<unsigned long> > >, unsigned long const&) (vector.tcc:459)
==551942==    by 0x7BB57D: std::vector<unsigned long, std::allocator<unsigned long> >::push_back(unsigned long const&) (stl_vector.h:1289)
==551942==    by 0x7B9690: CType::get_offsets() const (ctype.cpp:174)
==551942==    by 0x7C4F13: CTypeArray::buffer(LeanValue const&) const (array.hpp:72)
==551942==    by 0x7ABADF: Function::call(lean_object*) (function.cpp:87)
==551942==    by 0x7ABFBD: Function_call (function.cpp:123)
==551942==    by 0x626778: l_main___lambda__54 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x62762E: l_main___lambda__54___boxed (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942==    by 0x32A12C3: lean_apply_2 (in /home/alex/projects/Lean/lean4-ctypes/build/bin/tests)
==551942== 
.............
Tests.Basic.Library .....
======================== 0 failed, 34 passed, 0 errors ========================
==551942== 
==551942== HEAP SUMMARY:
==551942==     in use at exit: 25,630,024 bytes in 351 blocks
==551942==   total heap usage: 32,871 allocs, 32,520 frees, 37,445,435 bytes allocated
==551942== 
==551942== LEAK SUMMARY:
==551942==    definitely lost: 0 bytes in 0 blocks
==551942==    indirectly lost: 0 bytes in 0 blocks
==551942==      possibly lost: 0 bytes in 0 blocks
==551942==    still reachable: 25,630,024 bytes in 351 blocks
==551942==         suppressed: 0 bytes in 0 blocks
==551942== Reachable blocks (those to which a pointer was found) are not shown.
==551942== To see them, rerun with: --leak-check=full --show-leak-kinds=all
==551942== 
==551942== For lists of detected and suppressed errors, rerun with: -s
==551942== ERROR SUMMARY: 64 errors from 2 contexts (suppressed: 0 from 0)
alexf91 commented 8 months ago

Array types are created as "phony" structs in libffi and cannot be passed or returned from functions. This is documented in the libffi documentation:

Note that arrays cannot be passed or returned by value in C – structure types created like this should only be used to refer to members of real FFI_TYPE_STRUCT objects. However, a phony array type like this will not cause any errors from libffi if you use it as an argument or return type. This may be confusing.

They should be disallowed as direct function arguments or return values. This is possible because we have a separate CType.array type. We could also convert them to pointers if they are used as arguments or return values, but keep the phony struct type when inside a struct.