Hello Pierre,
These are all excellent questions -- I am currently writing a tutorial for Low*
are these served as good inspiration for the introduction. If CI goes through,
a work-in-progress version of the tutorial should be uploaded in the next few
hours at https://fstarlang.github.io/lowstar/ -- please read it and let me know
whether after browsing it, your questions have been answered.
In case the CI doesn't perform the upload, or the tutorial is unclear, the
essence of your issue is that your code is not Low*.
* the F* string and list types are F* values, i.e. concat has type string
-> string -> string; the only way to give you these semantics without requiring
the user to track allocations and lifetimes is to use a garbage-collector,
which C does not have
* the same goes for lists: compiling them to C with the current F* value
semantics would lead to a zillion uncollected list cell allocations.
What the C.String module provides is a bare-bones model of C string literals,
i.e. `const char *s = "my string literal";`, meaning that you should provide an
actual literal, e.g. `C.String.( print !$"hello, world\n" );`. This is very
limited, and does not allow you to do arbitrary string manipulation.
A proof-of-concept example exists that does that, in the test/ subdirectory of
KreMLin, and is called Server.fst. It models blitting C.String.t's into a
mutable buffer of C chars, tracking how much space remains in your buffer,
whether the buffer is live, etc. and rules out buffer overflows.
Naturally, it's a little involved for a hello world, but I guess that's the
reality of tracking temporal (liveness) and spatial safety (bounds) in C.
Let me know if that helps.
Cheers,
Jonathan
~ jonathan
________________________________
From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr> on behalf of Pierre
Beaucamp via fstar-club <fstar-club@lists.gforge.inria.fr>
Sent: Tuesday, May 1, 2018 9:48 AM
To: fstar-club@lists.gforge.inria.fr
Subject: [fstar-club] Trying to use List.Tot.map with Kremlin
Hi everyone,
I'm just playing a bit around with F-Star and Kremlin and I seem to be stuck at
a simple problem. I don't know if I'm missing something obvious or if this
might be a bug. My code looks like this:
let main () =
C.print_string (C.string_of_literal (String.concat ", " (List.Tot.map
string_of_int [1; 2; 3])));
C.exit_success
I expect this code to print `1, 2, 3` but instead I get the following runtime
error:
KreMLin abort at ./Main.c:9
This function was not extracted:
Failure("Cannot extract string_of_literal applied to a non-literal")
I tried some variations of the above program to see if I can reverse-engineer
what is going on, but as soon as I introduce `List.Tot.map`, the code breaks. I
know that there is also `C.Loops.map`, but I don't know if I really need to use
buffers to make it work.
Also, I'm generally interested in learning more about Kremlin / Low* / F*. If
there are any recommended resources or other helpful links, feel free to share
them with me.
Thank you and best regards,
--
Pierre Beaucamp
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-club&data=02%7C01%7Cprotz%40microsoft.com%7C445acbbb8a104079b70808d5af83d2b8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636607903120375441&sdata=WkxhslLqaMBwupJazX4IDfRaWwsqX6IIiuWZT8YrwFc%3D&reserved=0
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
