migrating a c project to ats

[Martin DeMello]

Has anyone migrated a C project to ATS in an open source repo that I can look at? I'd love to follow along with the piecewise evolution.

martin

[Chris Double]

I didn't migrate the whole thing but I did one function of OpenSSL,
integrated into the build system, described here:

<http://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html>

I also wrote a bit about converting a C HTTP server here:

<http://bluishcoder.co.nz/2011/04/24/converting-c-programs-to-ats.html>

--
http://bluishcoder.co.nz

[Martin DeMello]

thanks! those are both excellent.

martin

--
http://bluishcoder.co.nz

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CALn1vHFrHL6zfM6QfAvhOn014AoxoYRPT-Y%2BtcykgiQL7C6eMw%40mail.gmail.com.

[gmhwxi]

Try to do this in stages (even if you wrote the original C code).

At the beginning, please try to ignore error-handling. Instead, you
can use assertloc and $UN.cast to get a value of some needed type.

Overly using if-then-else to handle errors is often a sure sign of failure
in waiting.

[Yannick Duchêne]

Please, what is `assertloc`?

Le mercredi 19 novembre 2014 03:17:06 UTC+1, gmhwxi a écrit :

Try to do this in stages (even if you wrote the original C code).

At the beginning, please try to ignore error-handling. Instead, you

can use *assertloc* and $UN.cast to get a value of some needed type.

[Hongwei Xi]

loc in assertloc means location.

If assertloc fails, it prints out the location of the line so as to help debugging.

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/f4a2444e-1ddd-4fc5-99a7-3253c5085c5a%40googlegroups.com.

[Brandon Barker]

It is a dynamic check that returns a proof that its single argument evaluates to true (otherwise the program exits).

I think there are a number of discussions that touch on it indirectly in the google group.

On Fri, Nov 28, 2014 at 9:16 PM, 'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> wrote:

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/f4a2444e-1ddd-4fc5-99a7-3253c5085c5a%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

[gmhwxi]

$extfcall allows external functions to be conveniently
called inside ATS code.

When translating ATS code into C, one may want to make
extensive use of $extfcall during the first phase. Let
me use a example to show how $extfcall is typically used.

Say that you want to print out the content of the enviroment
variable HOME, and you know that the function getenv in stdlib.h
can do the work. The following code calls [getenv] externally:

(* ****** ****** *)
//
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)

staload "libc/SATS/stdlib.sats"

(* ****** ****** *)

implement
main0 () =
{
//
val HOME =
  $extfcall(string, "getenv", "HOME")
//
val ((*void*)) = println! ("${HOME} = ", HOME)
//
} (* end of [main0] *)

(* ****** ****** *)

Essentially, the expression $extfcall(string, "getenv", "HOME")
translates into getenv("HOME"), and its type is *assumed* to be
string.

Say that you realize later that getenv may return a NULL pointer
(in the case where HOME is undefined). Then you can change a bit:

$extfcall(Stropt0, "getenv", "HOME")

This change may result in type-errors that need to be fixed.

If you read the doc on getenv carefully, then you probably realize that what is returned by
getenv is not a stropt-value in the usual (functional) sense. A common way to handle it is
to assign it the following linear type vStrptr0:

vtypedef vStrptr(l:addr) = [l:addr] (strptr(l) -<prf> void | strptr(l))

Basically, vStrptr0 means a "borrowed string". The above code can now be written as follows:

implement
main0 () =
{
//
val (fpf | HOME) =
  $extfcall(vStrptr0, "getenv", "HOME")
//
val () = assertloc(isneqz(HOME)) // HOME is not NULL
//
val ((*void*)) = println! ("${HOME} = ", HOME)
//
prval ((*void*)) = fpf (HOME) // returning the borrowed string
//
} (* end of [main0] *)

After introducing the following declaration:

extern fun getenv  : string -> vStrptr0 = "mac#"

you can replace $exfcall(...) with getenv("HOME")

On Tuesday, November 18, 2014 5:24:14 PM UTC-5, Martin DeMello wrote:

[gmhwxi]

By the way, you can also use $UN.cast, which is less safe but very convenient:

(* ****** ****** *)
//
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)

staload UN = $UNSAFE

(* ****** ****** *)

staload "libc/SATS/stdlib.sats"

(* ****** ****** *)

implement
main0 () =
{
//
val HOME =

  $extfcall(ptr, "getenv", "HOME")

val () = assertloc(isneqz(HOME))
//

val ((*void*)) = println! ("${HOME} = ", $UN.cast{string}(HOME))

//
} (* end of [main0] *)

Program-first program verification puts the construction of a program first.

On Tuesday, November 18, 2014 5:24:14 PM UTC-5, Martin DeMello wrote: