Poly/ML

polyml@lists.polyml.org

2 participants
698 discussions

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

Re: [quantomatic] Poly/ML Package for Sublime Text 2
by aleks0＠gmail.com 13 Oct '11

13 Oct '11

Oops! Poly path was still hard-coded. Added a setting 'poly_bin' in File Settings for setting up a custom path. Pull the latest version of the package, then go to "Sublime Text 2 > Preferences > File Settings - User", and add a line like this to the JSON: "poly_bin": "/usr/local/bin/poly", On 13 October 2011 06:30, Lucas Dixon <lucas.dixon(a)gmail.com> wrote: > Looks like a nice editor! > > I had a go at running build on the Quantomatic ROOT.ML file, I got > this error output (and an endless compiling ROOT.ML [ = ? ] thing), > the error in the console is: > > startup, version: 2126 osx x64 channel: stable > executable: /Applications/Sublime Text 2.app/Contents/MacOS/Sublime Text 2 > working dir: / > packages path: /Users/ldixon/Library/Application Support/Sublime Text 2/Packages > settings path: /Users/ldixon/Library/Application Support/Sublime Text 2/Settings > package /Applications/Sublime Text 2.app/Contents/MacOS/Pristine > Packages/ActionScript.sublime-package is newer than the installed > version (/Users/ldixon/Library/Application Support/Sublime Text > 2/Pristine Packages/ActionScript.sublime-package), running > PackageSetup > error parsing session: No data at: 0:0 > PackageSetup returned: -1 > catalogue loaded > found 3 files for base name Default.sublime-keymap > found 1 files for base name Default.sublime-mousemap > found 1 files for base name Main.sublime-menu > Generating syntax summary > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/comment.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/copy_path.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/delete_word.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/detect_indentation.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/duplicate_line.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/echo.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/exec.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/fold.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/font.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/goto_line.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/indentation.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/kill_ring.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/mark.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/new_templates.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/open_file_settings.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/paragraph.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/save_on_focus_lost.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/scroll.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/side_bar.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/sort.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/swap_line.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/switch_file.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/transform.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/transpose.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Default/trim_trailing_white_space.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/Diff/diff.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/HTML/encode_html_entities.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/HTML/html_completions.py > Reloading plugin /Users/ldixon/Library/Application Support/Sublime > Text 2/Packages/PolyML/run_poly.py > loading bindings > loading pointer bindings > found 1 files for base name Default.sublime-theme > theme loaded > app ready > pre session restore time: 4.33111 > startup time: 4.47067 > loaded 937 snippets > Traceback (most recent call last): > ?File "./sublime_plugin.py", line 259, in run_ > ?File "./run_poly.py", line 131, in run > ?File "./poly/__init__.py", line 45, in compile > ?File "./poly/__init__.py", line 36, in ensure_poly_running > ?File "./poly/process.py", line 201, in __init__ > ?File "/System/Library/Frameworks/Python.framework/Versions/2.6/lib/python2.6/subprocess.py", > line 595, in __init__ > ? ?errread, errwrite) > ?File "/System/Library/Frameworks/Python.framework/Versions/2.6/lib/python2.6/subprocess.py", > line 1106, in _execute_child > ? ?raise child_exception > OSError: [Errno 2] No such file or directory > Exception AttributeError: "PolyProcess instance has no attribute > 'pipe'" in <bound method PolyProcess.__del__ of > <poly.process.PolyProcess instance at 0x115590830>> ignored > Traceback (most recent call last): > ?File "./sublime_plugin.py", line 259, in run_ > ?File "./run_poly.py", line 131, in run > ?File "./poly/__init__.py", line 45, in compile > ?File "./poly/__init__.py", line 36, in ensure_poly_running > ?File "./poly/process.py", line 201, in __init__ > ?File "/System/Library/Frameworks/Python.framework/Versions/2.6/lib/python2.6/subprocess.py", > line 595, in __init__ > ? ?errread, errwrite) > ?File "/System/Library/Frameworks/Python.framework/Versions/2.6/lib/python2.6/subprocess.py", > line 1106, in _execute_child > ? ?raise child_exception > OSError: [Errno 2] No such file or directory > > > Any suggestions? > > best, > lucas > > > On 12 October 2011 13:02, Aleks Kissinger <aleks0(a)gmail.com> wrote: >> For those interested, I've been working on a Poly/ML package for Sublime Text 2. >> >> https://github.com/akissinger/sublime-polyml >> >> Sublime Text 2 is in some ways the "moral" successor to Textmate >> (which is essentially defunct). However, unlike Textmate, it's >> available for Mac, Linux, and Windows. It will be a paid app at some >> point, but currently it is in free beta. >> >> http://www.sublimetext.com/2 >> >> I've been using the package for a couple of weeks now. It's still a >> bit on the rough side, but basic highlighting, building, and error >> reporting is working pretty well. Please let me know if you have >> issues or want to contribute. >> >> >> Aleks >> >> -- >> You received this message because you are subscribed to the Google Groups "Quantomatic" group. >> To post to this group, send email to quantomatic(a)googlegroups.com. >> To unsubscribe from this group, send email to quantomatic+unsubscribe(a)googlegroups.com. >> For more options, visit this group at http://groups.google.com/group/quantomatic?hl=en. >> >> > > -- > You received this message because you are subscribed to the Google Groups "Quantomatic" group. > To post to this group, send email to quantomatic(a)googlegroups.com. > To unsubscribe from this group, send email to quantomatic+unsubscribe(a)googlegroups.com. > For more options, visit this group at http://groups.google.com/group/quantomatic?hl=en. > >

2 1

Poly/ML Package for Sublime Text 2
by aleks0＠gmail.com 12 Oct '11

12 Oct '11

For those interested, I've been working on a Poly/ML package for Sublime Text 2. https://github.com/akissinger/sublime-polyml Sublime Text 2 is in some ways the "moral" successor to Textmate (which is essentially defunct). However, unlike Textmate, it's available for Mac, Linux, and Windows. It will be a paid app at some point, but currently it is in free beta. http://www.sublimetext.com/2 I've been using the package for a couple of weeks now. It's still a bit on the rough side, but basic highlighting, building, and error reporting is working pretty well. Please let me know if you have issues or want to contribute. Aleks

1 0

remove the very first > prompt
by supernovas.hf＠gmail.com 09 Oct '11

09 Oct '11

> Rob's suggestion of using the export should do what you want: > > PolyML.export("noprint-poly", > ?(fn () => (PolyML.print_depth 0; > ? ? ? ? ? ?PolyML.Compiler.prompt1 := ""; > ? ? ? ? ? ?PolyML.Compiler.prompt2 := ""; > ? ? ? ? ? ?PolyML.rootFunction ())) > ); > > Then you can run to make the new ml binary: > ?cc -o empty-top-level-poly noprint-poly.o -lpolymain -lpolyml Sorry, I can not reproduce this on my computer, the compiling yields: ,------------------------------------------------------------- [hf@mail ~]$ cc -o empty-top-level-poly noprint-poly.o -lpolymain -lpolyml /usr/bin/ld: cannot find -lpolymain `------------------------------------------------------------- Regards, Hong

2 2

readline library available?
by supernovas.hf＠gmail.com 06 Oct '11

06 Oct '11

Still can not disable the very first > system prompt ... :( another question: any way to support the GNU readline library under the SML system for user interaction? Best, Hong Feng

3 2

any way to turn off the Poly/ML system prompt?
by supernovas.hf＠gmail.com 04 Oct '11

04 Oct '11

Hello, I am trying to write a simple CGI program using Poly/ML. Is it possible to turn off the Poly/ML's type prompt message in the output? Best, Hong Feng

3 5

local specifications in signatures
by ramana.kumar＠gmail.com 01 Oct '11

01 Oct '11

The syntax reference here http://www.csci.csusb.edu/dick/samples/ml.syntax.html#Specification suggests that I should be able to write signature foo = sig local open CharVectorSlice in val baz : vector -> slice end end (making use of "other_spec" in the syntax reference above) But PolyML complains when it hits the "local" Poly/ML 5.4.1 Release > use"foo.sig"; Error- in 'foo.sig', line 2. end expected but local was found Am I wrong in thinking that that is a valid signature specification? Is there an official reference for the syntax of the language PolyML compiles? Do I have to keep repeating LongStructureName.type_i_want in my specifications? Or maybe it is typical to just export types liberally (because I could do type v = CharVectorSlice.vector at the top of that signature, etc.)

2 1

Dud exception traces
by aleks0＠gmail.com 26 Sep '11

26 Sep '11

Howdy, I'm trying to track down a bug, but PolyML.exception_trace doesn't seem to be working right. See the following example. % test_exp.ML exception test_exp; fun f () = raise test_exp; fun g () = (2 + (f ())); fun h () = 2 * (g ()); bash> poly --use test_exp.ML Poly/ML 5.4.2 Testing exception test_exp val f = fn: unit -> 'a val g = fn: unit -> int val h = fn: unit -> int > h (); Exception- test_exp raised > PolyML.exception_trace h; Exception trace for exception - test_exp raised in test_stuff.ML line 2 End of trace Exception- test_exp raised > I'm using the latest Poly/ML SVN version. a

2 3

Memory consumption profiling in PolyML
by Thomas.Sewell＠nicta.com.au 24 Sep '11

24 Sep '11

Hello to the PolyML users mailing list. I'm an Isabelle/HOL user from the L4.verified project at NICTA, and we're having some issues with Isabelle using far too much memory. I have a feature request that would be useful in diagnosing the problem. The current implementation of PolyML provides an object profiling mechanism PolyML.objProfile which analyses memory consumed by a given object, decomposed by size. As a trivial issue, there doesn't seem to be a good way to profile all the heap, since threading may make some objects inaccessible from the current root function. The big issue is that the profile doesn't tell me anything useful at all. ML> PolyML.objProfile (Thy_Info.get_theory "Nat"); Immutable object sizes and counts 1 229872 2 2557083 3 756596 4 1283875 5 811230 6 24521 7 102914 8 9200 9 9452 10 20660 ... The development is too big for me to have a chance of identifying which objects of size 2, 4 and 5 are consuming all the memory. By comparison, an object profile could be really valuable if it were decomposed by type (or possible type and/or closure). This would hopefully make it straightforward to hunt down the worst-offending modules. On a related note, Don Stewart gave a talk about his experience in Haskell working at Galois recently, and pointed out that profiling by types in their runtime effectively eliminated their problems with the famous Haskell space-leak issue. It seems to me this would be roughly compatible with the existing objProfile algorithm. I had a look at the code and got as far as realising I had no hope of understanding how PolyML encodes types internally. Does this seem like a reasonable feature request? Yours, Thomas.

2 2

Memory consumption profiling in PolyML
by Thomas.Sewell＠nicta.com.au 23 Sep '11

23 Sep '11

I may have overstated Don's point. I didn't mean that it was no longer a problem with the language - I was saying that this was an effective way to eliminate the problem within a given program. Space leaks are certainly a huge problem with the language. For novice/casual users the runtime is effectively a black box and space leaks are a showstopper. Don was pointing out that if your process involves using these tools routinely (such as at Galois) then the problem diminishes greatly. Yours, Thomas. On 23/09/11 16:10, Paul A. Steckler wrote: > On Fri, Sep 23, 2011 at 2:58 PM, Thomas Sewell > <Thomas.Sewell(a)nicta.com.au> wrote: >> On a related note, Don Stewart gave a talk about his experience in Haskell >> working at Galois recently, and pointed out that profiling by types in their >> runtime effectively eliminated their problems with the famous Haskell >> space-leak issue. > Do you mean, they now have a good idea where to stuff seq's in their code? > > Still a bother to have to routinely run the memory profiler on your code. > > -- Paul

1 0

← Newer
1
...
36
37
38
39
40
41
42
...
70
Older →

Jump to page:

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