Hi,

I tried to build Isabelle 2011-1 with the repository version 1352 of PolyML on Ubuntu 10.04 and x86_64. g++ seems to include its fortify checks automatically in the compiled code. When I build Isabelle's Pure session, it detects a buffer overrun and aborts PolyML. Is this a bug in PolyML? Or does PolyML not work with Fortify? Or is it just a misconfiguration on my side? If I disable fortify with -D_FORTIFY_SOURCE=0 when compiling PolyML, everything works fine again.

At the end of this mail, I have included the stack trace and memory map for the buffer overflow.

Best regards,
Andreas


*** buffer overflow detected ***: /afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/poly terminated
======= Backtrace: =========
/lib/libc.so.6(__fortify_fail+0x37)[0x2b7f00448217]
/lib/libc.so.6(+0xfe0d0)[0x2b7f004470d0]
/lib/libc.so.6(+0xfd539)[0x2b7f00446539]
/lib/libc.so.6(_IO_default_xsputn+0xcc)[0x2b7f003bed1c]
/lib/libc.so.6(_IO_vfprintf+0x3d34)[0x2b7f003920d4]
/lib/libc.so.6(__vsprintf_chk+0x99)[0x2b7f004465d9]
/lib/libc.so.6(__sprintf_chk+0x7f)[0x2b7f0044651f]
/afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/libpolyml.so.3(+0x37b5d)[0x2b7eff0afb5d]
/afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/libpolyml.so.3(_Z18foreign_dispatch_cP8TaskDataP12SaveVecEntryS2_+0x9f)[0x2b7eff0ade7f]
/afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/libpolyml.so.3(_ZN12X86Dependent7CallIO2EP8TaskDataPFP12SaveVecEntryS1_S3_S3_E+0x63)[0x2b7eff0ce4d3]
/afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/libpolyml.so.3(_Z13EnterPolyCodeP8TaskData+0x3b6)[0x2b7eff0bc656]
/afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/libpolyml.so.3(+0x2833d)[0x2b7eff0a033d]
/lib/libpthread.so.0(+0x69ca)[0x2b7eff3169ca]
/lib/libc.so.6(clone+0x6d)[0x2b7f0042f70d]
======= Memory map: ========
00400000-00d7f000 r-xp 00000000 00:14 142910404 /afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/poly 00f7e000-00f7f000 r-xp 0097e000 00:14 142910404 /afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/poly 00f7f000-00fc7000 rwxp 0097f000 00:14 142910404 /afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/poly
01889000-018c5000 rwxp 00000000 00:00 0                                  [heap]
2b7efee56000-2b7efee76000 r-xp 00000000 08:01 3966324 /lib/ld-2.11.1.so
2b7efee76000-2b7efee78000 rwxp 00000000 00:00 0
2b7eff075000-2b7eff076000 r-xp 0001f000 08:01 3966324 /lib/ld-2.11.1.so 2b7eff076000-2b7eff077000 rwxp 00020000 08:01 3966324 /lib/ld-2.11.1.so
2b7eff077000-2b7eff078000 rwxp 00000000 00:00 0
2b7eff078000-2b7eff0e7000 r-xp 00000000 00:14 142910358 /afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/libpolyml.so.3.0.1 2b7eff0e7000-2b7eff2e7000 ---p 0006f000 00:14 142910358 /afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/libpolyml.so.3.0.1 2b7eff2e7000-2b7eff2eb000 r-xp 0006f000 00:14 142910358 /afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/libpolyml.so.3.0.1 2b7eff2eb000-2b7eff2ed000 rwxp 00073000 00:14 142910358 /afs/info.uni-karlsruhe.de/user/lochbihl/isabelle/polyml/polyml/polyml/x86_64-linux/libpolyml.so.3.0.1
2b7eff2ed000-2b7eff2ef000 rwxp 00000000 00:00 0
2b7eff2ef000-2b7eff2f0000 rwxs 00000000 00:14 142910704 /afs/info.uni-karlsruhe.de/user/lochbihl/.polyml/poly-stats-7711
2b7eff30f000-2b7eff310000 rwxp 00000000 00:00 0
2b7eff310000-2b7eff328000 r-xp 00000000 08:01 3966337 /lib/libpthread-2.11.1.so 2b7eff328000-2b7eff527000 ---p 00018000 08:01 3966337 /lib/libpthread-2.11.1.so 2b7eff527000-2b7eff528000 r-xp 00017000 08:01 3966337 /lib/libpthread-2.11.1.so 2b7eff528000-2b7eff529000 rwxp 00018000 08:01 3966337 /lib/libpthread-2.11.1.so
2b7eff529000-2b7eff52d000 rwxp 00000000 00:00 0
2b7eff52d000-2b7eff58c000 r-xp 00000000 08:01 3992662 /usr/lib/libgmp.so.3.5.2 2b7eff58c000-2b7eff78b000 ---p 0005f000 08:01 3992662 /usr/lib/libgmp.so.3.5.2 2b7eff78b000-2b7eff78c000 r-xp 0005e000 08:01 3992662 /usr/lib/libgmp.so.3.5.2 2b7eff78c000-2b7eff78d000 rwxp 0005f000 08:01 3992662 /usr/lib/libgmp.so.3.5.2 2b7eff78d000-2b7eff794000 r-xp 00000000 08:01 3966327 /lib/librt-2.11.1.so 2b7eff794000-2b7eff993000 ---p 00007000 08:01 3966327 /lib/librt-2.11.1.so 2b7eff993000-2b7eff994000 r-xp 00006000 08:01 3966327 /lib/librt-2.11.1.so 2b7eff994000-2b7eff995000 rwxp 00007000 08:01 3966327 /lib/librt-2.11.1.so
2b7eff995000-2b7eff996000 rwxp 00000000 00:00 0
2b7eff996000-2b7effa18000 r-xp 00000000 08:01 3964972 /lib/libm-2.11.1.so 2b7effa18000-2b7effc17000 ---p 00082000 08:01 3964972 /lib/libm-2.11.1.so 2b7effc17000-2b7effc18000 r-xp 00081000 08:01 3964972 /lib/libm-2.11.1.so 2b7effc18000-2b7effc19000 rwxp 00082000 08:01 3964972 /lib/libm-2.11.1.so 2b7effc19000-2b7effc1b000 r-xp 00000000 08:01 3966343 /lib/libdl-2.11.1.so 2b7effc1b000-2b7effe1b000 ---p 00002000 08:01 3966343 /lib/libdl-2.11.1.so 2b7effe1b000-2b7effe1c000 r-xp 00002000 08:01 3966343 /lib/libdl-2.11.1.so 2b7effe1c000-2b7effe1d000 rwxp 00003000 08:01 3966343 /lib/libdl-2.11.1.so 2b7effe1d000-2b7efff13000 r-xp 00000000 08:01 3993196 /usr/lib/libstdc++.so.6.0.13 2b7efff13000-2b7f00113000 ---p 000f6000 08:01 3993196 /usr/lib/libstdc++.so.6.0.13 2b7f00113000-2b7f0011a000 r-xp 000f6000 08:01 3993196 /usr/lib/libstdc++.so.6.0.13 2b7f0011a000-2b7f0011c000 rwxp 000fd000 08:01 3993196 /usr/lib/libstdc++.so.6.0.13
2b7f0011c000-2b7f00132000 rwxp 00000000 00:00 0
2b7f00132000-2b7f00148000 r-xp 00000000 08:01 3965007 /lib/libgcc_s.so.1 2b7f00148000-2b7f00347000 ---p 00016000 08:01 3965007 /lib/libgcc_s.so.1 2b7f00347000-2b7f00348000 r-xp 00015000 08:01 3965007 /lib/libgcc_s.so.1 2b7f00348000-2b7f00349000 rwxp 00016000 08:01 3965007 /lib/libgcc_s.so.1 2b7f00349000-2b7f004c3000 r-xp 00000000 08:01 3966339 /lib/libc-2.11.1.soPure FAILED (see also /afs/info.uni-karlsruhe.de/user/lochbihl/.isabelle/Isabelle2011-1/heaps/polyml-5.4.0_x86_64-linux/log/Pure)

signature PROOF_GENERAL =
  sig
    val test_markupN : string
    val sendback : string -> Pretty.T list -> unit
    val init : bool -> unit
    structure ThyLoad : sig val add_path : string -> unit end
  end
structure ProofGeneral : PROOF_GENERAL
val it = (): unit


--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: [email protected]
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Reply via email to