Unsafe features

Unsafe features

[Florian Weimer]

Has Ocaml any unsafe features?  With "unsafe", I mean constructs
which, when (ab)used in certain ways, make further reasoning about the
behavior of the program impossible (and neither the compiler nor the
run-time system provides a diagnosis).  Examples in other languages
are out-of-bounds array access, null pointer dereference, integer
arithmetic overflow, premature deallocation of heap objects, wrong
type declarations -- you get the idea.

The C language interface falls into this category.  Are there any
other problematic areas?

Re: [Caml-list] Unsafe features

[Damien Bobillot]

[-- Attachment #1: Type: text/plain, Size: 796 bytes --]


Le 2 sept. 05 à 14:02, Florian Weimer a écrit :

> Has Ocaml any unsafe features?  With "unsafe", I mean constructs
> which, when (ab)used in certain ways, make further reasoning about the
> behavior of the program impossible (and neither the compiler nor the
> run-time system provides a diagnosis).  Examples in other languages
> are out-of-bounds array access, null pointer dereference, integer
> arithmetic overflow, premature deallocation of heap objects, wrong
> type declarations -- you get the idea.
>
> The C language interface falls into this category.  Are there any
> other problematic areas?

The Obj.magic function. I don't know exactly what it does, but I  
think it does arbitrary type conversions.

-- 
Damien alias Schmurtz
aim:goim?screenname=schmuuurtz


[-- Attachment #2: smime.p7s --]
[-- Type: application/pkcs7-signature, Size: 2375 bytes --]

Re: [Caml-list] Unsafe features

[Erik de Castro Lopo]

Florian Weimer wrote:

> Has Ocaml any unsafe features?  With "unsafe", I mean constructs
> which, when (ab)used in certain ways, make further reasoning about the
> behavior of the program impossible (and neither the compiler nor the
> run-time system provides a diagnosis).  Examples in other languages
> are out-of-bounds array access, null pointer dereference, integer
> arithmetic overflow, premature deallocation of heap objects, wrong
> type declarations -- you get the idea.
> 
> The C language interface falls into this category.  Are there any
> other problematic areas?

The Marshall module.

Erik
-- 
+-----------------------------------------------------------+
  Erik de Castro Lopo  nospam@mega-nerd.com (Yes it's valid)
+-----------------------------------------------------------+
"The beauty of religious mania is that it has the power to
explain everything. Once God (or Satan) is accepted as the first
cause of everything which happens in the mortal world, nothing
is left to chance...logic can be happily tossed out the window."
- Stephen King

Re: [Caml-list] Unsafe features

[Florian Weimer]

* Damien Bobillot:

>> The C language interface falls into this category.  Are there any
>> other problematic areas?
>
> The Obj.magic function. I don't know exactly what it does, but I  
> think it does arbitrary type conversions.

Apparently, it creates a bit-wise copy of a value and assigns it a new
type.

I discovered that there are also a couple of undocumented unsafe_*
functions, such as String.unsafe_set, which behave the way their names
imply (no bound schecks).

Re: [Caml-list] Unsafe features

[Jon Harrop]

On Saturday 03 September 2005 10:40, Florian Weimer wrote:
> * Damien Bobillot:
> >> The C language interface falls into this category.  Are there any
> >> other problematic areas?
> >
> > The Obj.magic function. I don't know exactly what it does, but I
> > think it does arbitrary type conversions.
>
> Apparently, it creates a bit-wise copy of a value and assigns it a new
> type.
>
> I discovered that there are also a couple of undocumented unsafe_*
> functions, such as String.unsafe_set, which behave the way their names
> imply (no bound schecks).

Yes, there is also the "-unsafe" command line option to turn off bounds 
checking.

There is never any need to use Obj (although the alternatives can be quite 
tedious or inefficient).

The marshalled format is likely to change between compiler versions in the 
future so it should only be used for short-term storage anyway.

The C interface is very error prone and is (in general and IMHO) the most 
likely cause of unsafeness. Programmers writing OCaml-only programs can 
happily stick to the safe core of the language. However, programmers wishing 
to use external libraries are likely to encounter problems. I have had 
segfaults with code using LablGL and the FFTW bindings, for example.

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
Objective CAML for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists

Re: [Caml-list] Unsafe features

[yoann padioleau]

On 3 sept. 05, at 11:40, Florian Weimer wrote:

> * Damien Bobillot:
>
>
>>> The C language interface falls into this category.  Are there any
>>> other problematic areas?
>>>
>>
>> The Obj.magic function. I don't know exactly what it does, but I
>> think it does arbitrary type conversions.
>>
>
> Apparently, it creates a bit-wise copy of a value and assigns it a new
> type.

Are you sure ? I thought it was just a function to get rid temporary  
of the typing system,
a kind of cast operator.

But is is bad to use it, very bad, shame on you if you use it
(i just put this statement to be sure that xavier leroy will not  
shout over me).

>
> I discovered that there are also a couple of undocumented unsafe_*
> functions, such as String.unsafe_set, which behave the way their names
> imply (no bound schecks).
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

Re: [Caml-list] Unsafe features

[Florian Weimer]

* yoann padioleau:

>> Apparently, it creates a bit-wise copy of a value and assigns it a new
>> type.
>
> Are you sure ? I thought it was just a function to get rid temporary
> of the typing system, a kind of cast operator.

It is, but how would you define such a operator?  At a more abstract
level, there is no obvious choice for a map a -> b between arbitrary
types.

I gave it a try and got:

# let x : int = Obj.magic "x";;
val x : int = 67381588
# x;;
- : int = 67381588
# 

The "67381588" is just half the integral value of a heap address
(because of the tag bit, I presume).  And looking at the ltrace
output, it seems that it is indeed close to the storage area of that
string.

> But is is bad to use it, very bad, shame on you if you use it
> (i just put this statement to be sure that xavier leroy will not  
> shout over me).

Yes, and my question was to avoid such unsafe language features.

Re: [Caml-list] Unsafe features

[yoann padioleau]

On 3 sept. 05, at 16:28, Florian Weimer wrote:

> * yoann padioleau:
>
>
>>> Apparently, it creates a bit-wise copy of a value and assigns it  
>>> a new
>>> type.
>>>
>>
>> Are you sure ? I thought it was just a function to get rid temporary
>> of the typing system, a kind of cast operator.
>>
>
> It is, but how would you define such a operator?

obj.ml contains:
   external magic: 'a -> 'b = "%identity"

So I guess there is no bit-wise copy involved.

>
>
>> But is is bad to use it, very bad, shame on you if you use it
>> (i just put this statement to be sure that xavier leroy will not
>> shout over me).
>>
>
> Yes, and my question was to avoid such unsafe language features.
>

I know :) It is just that I have the feeling that the ocaml team does  
not like when someone talk
about Obj.magic,  so I put a disclaimer.

>

Re: [Caml-list] Unsafe features

[Florian Weimer]

* yoann padioleau:

>>> Are you sure ? I thought it was just a function to get rid temporary
>>> of the typing system, a kind of cast operator.
>>>
>>
>> It is, but how would you define such a operator?
>
> obj.ml contains:
>   external magic: 'a -> 'b = "%identity"
>
> So I guess there is no bit-wise copy involved.

Ahem, "%identity" means just that, I think.

Re: [Caml-list] Unsafe features

[Florian Weimer]

* Florian Weimer:

> * yoann padioleau:
>
>>>> Are you sure ? I thought it was just a function to get rid temporary
>>>> of the typing system, a kind of cast operator.
>>>>
>>>
>>> It is, but how would you define such a operator?
>>
>> obj.ml contains:
>>   external magic: 'a -> 'b = "%identity"
>>
>> So I guess there is no bit-wise copy involved.
>
> Ahem, "%identity" means just that, I think.

I should add that I meant a copy of the reference to the object, not
the object itself.  We're probably in violent agreement.

Re: [Caml-list] Unsafe features

[yoann padioleau]

On 3 sept. 05, at 16:51, Florian Weimer wrote:

> * Florian Weimer:
>
>
>> * yoann padioleau:
>>
>>
>>>>> Are you sure ? I thought it was just a function to get rid  
>>>>> temporary
>>>>> of the typing system, a kind of cast operator.
>>>>>
>>>>>
>>>>
>>>> It is, but how would you define such a operator?
>>>>
>>>
>>> obj.ml contains:
>>>   external magic: 'a -> 'b = "%identity"
>>>
>>> So I guess there is no bit-wise copy involved.
>>>
>>
>> Ahem, "%identity" means just that, I think.
>>
>
> I should add that I meant a copy of the reference to the object, not
> the object itself.

Ok.
I assumed that when one talks about bit-wise copy it means   
implicitly a bit-wise deep copy,
that is a copy, no sharing.
In Obj.magic there is some sharing, so no copy.
Maybe I am wrong.


> We're probably in violent agreement.
>

I am not very good in english  but I guess we were in violent  
disagreement instead  :)

>

Re: [Caml-list] Unsafe features

[Jacques Garrigue]

From: Florian Weimer <fw@deneb.enyo.de>
> I gave it a try and got:
> 
> # let x : int = Obj.magic "x";;
> val x : int = 67381588
> # x;;
> - : int = 67381588
> # 
> 
> The "67381588" is just half the integral value of a heap address
> (because of the tag bit, I presume).  And looking at the ltrace
> output, it seems that it is indeed close to the storage area of that
> string.

You are right indeed. Here is another way to see that this only
changes the apparent type of the underlying value:

# let x : int = Obj.magic (String.create 3);;
val x : int = 67389852
# Gc.full_major();;
- : unit = ()
# x;;
- : int = 68129330

Oops, here is an integer that changes with the GC...

Worse:
# let y = x+13;;
val y : int = 67407805
# Gc.full_major();;
Segmentation fault

Jacques

Integral solutions of rational linear equations

[Thomas Gazagnaire]

Hello,

in my one of my Ocaml programs, I need to find all integers solutions of 
a rational equation systems. This algo uses Gauss reduction and Hermite 
normal form, and need to know if a rational is an integer or not (ie. I 
don't want to use numerical approximation : (1/3) * 3 is an integer but 
0,333333*3 we don't know). I didn't find any integer algebra package for 
ocaml, so I tried to implement Gauss elimination (easy) and Hermite 
normal form (more difficult...). But I didn't implement optimized 
version of these algorithms...

So my question is : do you know if exists a native ocaml module or an 
interface with a C library which is able to do integer/rational matrix 
manipulation (essentialy the Hermite normal form) in an efficient way ?

Thomas

Re: [Caml-list] Integral solutions of rational linear equations

[Sebastian Egner]

[-- Attachment #1: Type: text/plain, Size: 2625 bytes --]

Thomas,

Ocaml comes with a library for arbitrary-precision rational arithmetics;
the library is called 'Num' and its documentation can be found from here:

        http://caml.inria.fr/pub/docs/manual-ocaml/manual036.html

Now for computing integer solutions of rational equations you might
want to keep in mind that Gauss reduction suffers from exponential
growth of the entries because every row operation on the matrix
can---and usually does---double the number of bits in the numbers.
For this reason, Gaussian elimination and simple Hermite NF algorithms
are only useful if the number of equations is very low (<< 10, say).

Otherwise, you need to use more advanced algorithms (e.g. solving
several "mod m" images of the equation and reconstructing using the
Chinese Remainder Theorem), but I am not aware of any 'off the shelf'
implementation of this functionality in Ocaml.

As an entry point for the algorithms consider this page from the manual
of the computer algebra system Magma:

        http://magma.maths.usyd.edu.au/magma/htmlhelp/text602.htm#5489

Sebastian.

----
Dr. Sebastian Egner
Senior Scientist
Philips Research Laboratories
Prof. Holstlaan 4 (WDC 1-051, 1st floor, room 51)
5656 AA Eindhoven
The Netherlands
tel:       +31 40 27-43166
fax:      +31 40 27-44004
email: sebastian.egner@philips.com








Thomas Gazagnaire <thomas.gazagnaire@irisa.fr> 
Sent by:
caml-list-bounces@yquem.inria.fr
29-11-2005 19:46

To
caml-list@yquem.inria.fr
cc

Subject
[Caml-list] Integral solutions of rational linear equations
Classification







Hello,

in my one of my Ocaml programs, I need to find all integers solutions of 
a rational equation systems. This algo uses Gauss reduction and Hermite 
normal form, and need to know if a rational is an integer or not (ie. I 
don't want to use numerical approximation : (1/3) * 3 is an integer but 
0,333333*3 we don't know). I didn't find any integer algebra package for 
ocaml, so I tried to implement Gauss elimination (easy) and Hermite 
normal form (more difficult...). But I didn't implement optimized 
version of these algorithms...

So my question is : do you know if exists a native ocaml module or an 
interface with a C library which is able to do integer/rational matrix 
manipulation (essentialy the Hermite normal form) in an efficient way ?

Thomas


_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs


[-- Attachment #2: Type: text/html, Size: 4505 bytes --]

Re: [Caml-list] Integral solutions of rational linear equations

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 1722 bytes --]

Thomas Gazagnaire a écrit :
> Hello,
> 
> in my one of my Ocaml programs, I need to find all integers solutions of
> a rational equation systems. This algo uses Gauss reduction and Hermite
> normal form, and need to know if a rational is an integer or not (ie. I
> don't want to use numerical approximation : (1/3) * 3 is an integer but
> 0,333333*3 we don't know). I didn't find any integer algebra package for
> ocaml, so I tried to implement Gauss elimination (easy) and Hermite
> normal form (more difficult...). But I didn't implement optimized
> version of these algorithms...
> 
> So my question is : do you know if exists a native ocaml module or an
> interface with a C library which is able to do integer/rational matrix
> manipulation (essentialy the Hermite normal form) in an efficient way ?
> 

you did not look very hard ? OCaml is distributed with the bignum
library in standard which does both int and rationnal ...

$ ocaml nums.cma
        Objective Caml version 3.09.0

# open Num

let rec fact n = if n = 0 then Int 1 else fact (n-1) */ Int n
      ;;
val fact : int -> Num.num = <fun>
# fact 100;;
- : Num.num = Big_int <abstr>
# string_of_num (fact 100);;
- : string =
"93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000"

> Thomas
> 
> 
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 894 bytes --]

Re: [Caml-list] Integral solutions of rational linear equations

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 1416 bytes --]

Christophe Raffalli a écrit :
> Thomas Gazagnaire a écrit :
> 
>>Hello,
>>
>>in my one of my Ocaml programs, I need to find all integers solutions of
>>a rational equation systems. This algo uses Gauss reduction and Hermite
>>normal form, and need to know if a rational is an integer or not (ie. I
>>don't want to use numerical approximation : (1/3) * 3 is an integer but
>>0,333333*3 we don't know). I didn't find any integer algebra package for
>>ocaml, so I tried to implement Gauss elimination (easy) and Hermite
>>normal form (more difficult...). But I didn't implement optimized
>>version of these algorithms...
>>
>>So my question is : do you know if exists a native ocaml module or an
>>interface with a C library which is able to do integer/rational matrix
>>manipulation (essentialy the Hermite normal form) in an efficient way ?
>>
> 
> 
> you did not look very hard ? OCaml is distributed with the bignum
> library in standard which does both int and rationnal ...
> 

Sorry, I did not read the matrix word ...

Thks to the one who made me notice ...

>>_______________________________________________
>>Caml-list mailing list. Subscription management:
>>http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
>>Archives: http://caml.inria.fr
>>Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>>Bug reports: http://caml.inria.fr/bin/caml-bugs
> 
> 


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 894 bytes --]

Re: [Caml-list] Integral solutions of rational linear equations

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 1046 bytes --]

Christophe Raffalli a écrit :
> Thomas Gazagnaire a écrit :
> 
>>Hello,
>>
>>in my one of my Ocaml programs, I need to find all integers solutions of
>>a rational equation systems. This algo uses Gauss reduction and Hermite
>>normal form, and need to know if a rational is an integer or not (ie. I
>>don't want to use numerical approximation : (1/3) * 3 is an integer but
>>0,333333*3 we don't know). I didn't find any integer algebra package for
>>ocaml, so I tried to implement Gauss elimination (easy) and Hermite
>>normal form (more difficult...). But I didn't implement optimized
>>version of these algorithms...
>>
>>So my question is : do you know if exists a native ocaml module or an
>>interface with a C library which is able to do integer/rational matrix
>>manipulation (essentialy the Hermite normal form) in an efficient way ?
>>
> 
> 
And by the way, my library on formal computation would give you an
algorithm using conjugate gradient ... look at:

http://www.lama.univ-savoie.fr/~raffalli/formel.html



[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 894 bytes --]