Poly/ML November 2011

polyml@lists.polyml.org

9 participants
13 discussions

Printing arbitrary objects
by phil.clayton＠lineone.net 16 Nov '11

16 Nov '11

Ah. Perhaps PolyML.makestring then? On 16/11/11 18:11, Dave Thayer wrote: > No you have to know the type of the object to invoke a type specific pretty printer I want to print arbitrary objects it could be anything. (usually a small subset of anything) :) > > -----Original Message----- > From: Phil Clayton [mailto:phil.clayton@lineone.net] > Sent: Wednesday, November 16, 2011 10:09 AM > To: Dave Thayer > Cc: polyml(a)inf.ed.ac.uk > Subject: Re: [polyml] Printing arbitrary objects > > On 16/11/11 17:59, Dave Thayer wrote: >> I have searched the online docs (which are extraordinarily skimpy) for >> how I can print the structure of some arbitrary object and can find no >> info. Can anyone help please. > > Does this one help? > http://www.polyml.org/docs/PrettyPrint.html > > Phil > > >

1 0

Fortify detects buffer overflow
by andreas.lochbihler＠kit.edu 15 Nov '11

15 Nov '11

Hi David, I've tried a different x86_64 system with Ubuntu 11.10 and gcc 4.6.1, and the buffer overflow also occurs there (but only without --enable-debug), so I don't think gcc is to blame. Nevertheless, thanks for your efforts. Regards, Andreas > Hi Andreas, > Thanks for trying that. I've tried again but I still can't reproduce it. I did > find a problem with the hardening option to produce a position-independent > executable but that caused a segfault during start-up. > > I was really concerned in case there was a sprintf that was writing beyond its > buffer and, of course, it's possible there is. It may also be a false positive > which has been fixed in a later version of GCC. For the moment I'm inclined to > leave it especially as you've found a work-around. I'd be interested if anyone > else has this problem. > > Regards, > David > > On 15/11/2011 07:24, Andreas Lochbihler wrote: >> Hi David, >> >> when I add the --enable-debug to ./configure, the buffer overflow error >> disappears. ./configure --disable-shared leads to the same buffer >> overflow, but no more details. Is there anything else I could try? >> >> Best regards, >> Andreas >> >> Am 14.11.2011 18:05, schrieb David Matthews: >>> I've attempted to reproduce this without success. I'm running Ubuntu >>> 11.10 and >>> had to install the hardening packages manually do there may be some >>> difference. >>> I can't tell much from the backtrace because the function names within >>> the poly >>> library aren't being shown. Could you try rebuilding poly with >>> ./configure --enable-debug --disable-shared >>> That might provide some more useful information. >>> >>> Regards, >>> David >>> >>> On 11/11/2011 12:03, Andreas Lochbihler wrote: >>>> 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 >>>> -- 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: andreas.lochbihler(a)kit.edu http://pp.info.uni-karlsruhe.de KIT - Universit?t des Landes Baden-W?rttemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

1 0

Fortify detects buffer overflow
by andreas.lochbihler＠kit.edu 15 Nov '11

15 Nov '11

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: andreas.lochbihler(a)kit.edu http://pp.info.uni-karlsruhe.de KIT - Universit?t des Landes Baden-W?rttemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

2 2

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Poly/ML November 2011