-
Notifications
You must be signed in to change notification settings - Fork 30
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Implementing a less memory intensive read function #101
Comments
Sorry for taking so long to get to this - is it possible to have a complete repro case for this? flexlink is creaking somewhat with more recent Windows link libraries as well (a significant amount of the time flexlink spends appears to be parsing the CRT and Windows .a files). |
I'm experiencing similar issues when trying to build Repro caseI made a minimal repro case at z3-ocaml-build. It is best to use it on a windows virtual machine that has limited amount of RAM and swap space or on Github Actions (The repository contains a workflow). I will refer to the root of the repository as BuildThe repository contains a
This script does the following:
Inspecting the errorWe can execute the failing command in a more vebose way as follows:
We can now run the command with the
Which produces following output on my virtual machine with 4GB of RAM:
Some notes
|
This is fantastic, thanks @NielsMommen! |
Note that recently |
After some further investigation, I found out that Working buildAs mentioned before, I'm able to build Explain output
Failing build
Explain output
The difference is that each object is prefixed by libz3_dll_ and the objects where each symbol is found keeps on growing for each symbol. This pattern keeps repeating: one entry for the first symbol, two entries for the second, ..., n entries for the last. This explains why Debugging
|
let rec read_member () = | |
let buf = read ic (pos_in ic) 60 in | |
let base = pos_in ic in | |
let size = int_of_string (strz (Bytes.sub buf 48 10) 0 ' ') in | |
let name = strz (Bytes.sub buf 0 16) 0 ' ' in | |
begin match name with | |
| "/" | "" -> () | |
| "//" -> strtbl := read ic (pos_in ic) size | |
| s when s.[0] = '/' -> | |
let ofs = | |
try Scanf.sscanf s "/%u%!" (fun x -> x) | |
with Scanf.Scan_failure _ | |
| Failure _ | |
| End_of_file -> -1 | |
in | |
(* Ignore special sections which we don't know about *) | |
if ofs >= 0 then | |
obj size (strz !strtbl ofs '\000') | |
| s when s.[String.length s - 1] = '/' -> | |
let s = String.sub s 0 (String.length s - 1) in | |
obj size s | |
| s -> | |
Printf.ksprintf failwith "Cannot parse archive member %s" s | |
end; | |
seek_in ic (base + size + size mod 2); | |
read_member () | |
in | |
(try read_member () with End_of_file -> ()); | |
!objects,!imports |
objdump
objdump -t libz3.dll.a
confirms that objects are prefixed with libz3_dll_ when built with binutils >2.37:
objdump - z3 built with binutils 2.37
d031590.o: file format pe-i386
SYMBOL TABLE:
[ 0](sec 1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .text
[ 1](sec 2)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$7
[ 2](sec 3)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$5
[ 3](sec 4)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$4
[ 4](sec 5)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$6
[ 5](sec -1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000001 @feat.00
[ 6](sec 1)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __ZplRK8rationali
[ 7](sec 3)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __imp___ZplRK8rationali
[ 8](sec 0)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __head_libz3_dll
d031589.o: file format pe-i386
SYMBOL TABLE:
[ 0](sec 1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .text
[ 1](sec 2)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$7
[ 2](sec 3)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$5
[ 3](sec 4)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$4
[ 4](sec 5)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$6
[ 5](sec -1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000001 @feat.00
[ 6](sec 1)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __ZplRK8rationalS1_
[ 7](sec 3)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __imp___ZplRK8rationalS1_
[ 8](sec 0)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __head_libz3_dll
d031588.o: file format pe-i386
SYMBOL TABLE:
[ 0](sec 1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .text
[ 1](sec 2)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$7
[ 2](sec 3)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$5
[ 3](sec 4)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$4
[ 4](sec 5)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$6
[ 5](sec -1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000001 @feat.00
[ 6](sec 1)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __ZplRK16inf_int_rationalS1_
[ 7](sec 3)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __imp___ZplRK16inf_int_rationalS1_
[ 8](sec 0)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __head_libz3_dll
...
objdump - z3 built with binutils >2.37
libz3_dll_d031590.o: file format pe-i386
SYMBOL TABLE:
[ 0](sec 1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .text
[ 1](sec 2)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$7
[ 2](sec 3)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$5
[ 3](sec 4)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$4
[ 4](sec 5)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$6
[ 5](sec -1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000001 @feat.00
[ 6](sec 1)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __ZplRK8rationali
[ 7](sec 3)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __imp___ZplRK8rationali
[ 8](sec 0)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __head_libz3_dll
libz3_dll_d031589.o: file format pe-i386
SYMBOL TABLE:
[ 0](sec 1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .text
[ 1](sec 2)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$7
[ 2](sec 3)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$5
[ 3](sec 4)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$4
[ 4](sec 5)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$6
[ 5](sec -1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000001 @feat.00
[ 6](sec 1)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __ZplRK8rationalS1_
[ 7](sec 3)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __imp___ZplRK8rationalS1_
[ 8](sec 0)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __head_libz3_dll
libz3_dll_d031588.o: file format pe-i386
SYMBOL TABLE:
[ 0](sec 1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .text
[ 1](sec 2)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$7
[ 2](sec 3)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$5
[ 3](sec 4)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$4
[ 4](sec 5)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000000 .idata$6
[ 5](sec -1)(fl 0x00)(ty 0)(scl 3) (nx 0) 0x00000001 @feat.00
[ 6](sec 1)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __ZplRK16inf_int_rationalS1_
[ 7](sec 3)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __imp___ZplRK16inf_int_rationalS1_
[ 8](sec 0)(fl 0x00)(ty 0)(scl 2) (nx 0) 0x00000000 __head_libz3_dll
...
objdump-z3_build_binutils_2.37.txt
objdump-z3_build_binutils_2.39.txt
Thanks for the detective work @NielsMommen! Could you upload the failing |
Never mind, I was able to to obtain it. I have a tentative fix over at https://github.com/nojb/flexdll/tree/longnames_newline. Can you try it? Thanks! |
Works like a charm! thanks! |
Thanks for the confirmation! Submitted as PR now: #117 |
When building the ocaml bibindings for Z3, it attempts to allocate ~10GiB before an oom error. This exceedingly high memory usage occurs while reading the import library (libz3.dll.a), and before the actual linker is called.
I don't know if there's a more efficient way to store these strings, or if it's possible to implement it such as to save results to disk and continue reading if memory usage is becoming too high. It seems very improbable that 33 GiB of strings are needed to make ~500KiB to 1.3MiB libraries.
The most pertinent information from the ctf is likely:
The CTF is here, if you'd like to view it, though.
https://gist.github.com/EmmaJaneBonestell/98fda00c93a8d09ea09bada08972761d
Edit: I used a GCP server, and it took about 33 GiB of RAM and a total of 46 GiB of allocations to build.
Edit 2: UCRT had nothing to do with it, but rather, it seems to have the excessive memory usage with any of the MSYS2 environments' built dlls. If the dll is built with Cygwin's MinGW toolchain, rather than MSYS2's MINGW toolchain, it doesn't have a problem. E.g. libz3.dll.a built with Cygwin's MinGW, vs MSYS2's, won't consume excessive RAM.
The text was updated successfully, but these errors were encountered: