Created
May 31, 2013 15:40
-
-
Save talex5/5685858 to your computer and use it in GitHub Desktop.
My attampt at implementing runenv.py in ATS. This works, but some of the external declarations aren't quite right (e.g. returning strings rather than strptrs). Looks like proper versions of the support code (null_array, json) will be in ATS 2. The main function at the end of runenv.dats is where the real code is.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
%{# | |
#include "json/json.h" | |
%} | |
absviewtype json_object_vtype (l:addr) = ptr | |
viewtypedef json_object (l:addr) = json_object_vtype l | |
viewtypedef json_object0 = [l:addr] json_object_vtype l | |
viewtypedef json_object1 = [l:addr;l>null] json_object_vtype l | |
absviewtype array_list_vtype (l:addr,n:int) = [l>null] ptr | |
viewtypedef array_list (n:int) = [l:addr | l > null; n >= 0] array_list_vtype (l, n) | |
fun json_tokener_parse | |
(s: string): [l:addr] json_object(l) = "mac#json_tokener_parse" | |
fun json_object_to_json_string | |
(json: !json_object1): string = "mac#json_object_to_json_string" | |
fun json_ptr_is_null {l:addr} (p: !json_object(l)):<> bool (l <= null) = "mac#atspre_ptr_is_null" | |
// TODO: could return NULL | |
fun json_object_get_array {l:addr} | |
(json: !json_object1): [n:nat] ( | |
minus (json_object1, array_list n) | |
| array_list n | |
) = "mac#json_object_get_array" | |
fun json_array_list_free {n:nat} | |
(array: array_list n): void = "mac#array_list_free" | |
fun json_object_put | |
(json: json_object0): void = "mac#json_object_put" | |
fun array_list_get_length{n:nat}(a: !array_list n): int(n) = "mac#array_list_length" | |
// Borrow? | |
fun json_array_list_get_idx{n:nat}{i:nat;i < n}(a: !array_list n, i: int(i)): json_object1 = "mac#array_list_get_idx" | |
// Borrow? | |
fun json_object_get_string(json: json_object1): string = "mac#json_object_get_string" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
staload "json.sats" | |
staload _ = "prelude/DATS/array.dats" | |
//staload "prelude/SATS/sizetype.sats" | |
staload _ = "prelude/SATS/pointer.sats" | |
staload "libc/SATS/string.sats" | |
staload "null_array.sats" | |
#define ATS_STALOADFLAG 0 | |
#define ATS_DYNLOADFLAG 0 | |
extern castfn string_of_ptr(p: ptr): [n:nat] string n | |
// A string is also a pointer | |
extern prfun str_is_ptr {m:addr} (pf: string? @ m): ptr @ m | |
// A pointer is also an uninitialised string | |
extern prfun ptr_is_maybe_string {m:addr} (pf: ptr @ m): string? @ m | |
implement string_array_alloc | |
{n} | |
(n: size_t(n)): | |
[a:addr] (free_gc_v(string?, n + 1, a), string_array_v(string?, a, n) | ptr a) = let | |
val (must_free, contents | p) = array_ptr_alloc<string>(n + 1) | |
// Divide the array into the body and the null terminator | |
val (pr_null_offset | null_offset) = n szmul2 sizeof<string> | |
prval (body_uninitialised, pr_tail) = array_v_split{string?}{n + 1}{n}(pr_null_offset, contents) | |
prval pr_tail = array_v_unsing(pr_tail) | |
prval pr_ptr = str_is_ptr(pr_tail) | |
val nullp = p + null_offset | |
val () = !nullp := null | |
in | |
(must_free, string_array_cons{string?}(body_uninitialised, pr_null_offset, pr_ptr, n) | p) | |
end | |
implement string_array_free | |
{n} | |
{m} | |
(pr_free: free_gc_v(string?, n + 1, m), pr: string_array_v(string, m, n) | p: ptr m): void = let | |
prval string_array_cons(contents, pr_mul, pr_null, n) = pr | |
prval pr_null = ptr_is_maybe_string(pr_null) | |
prval pr_null = array_v_sing(pr_null) | |
prval whole_array = array_v_unsplit{string?}(pr_mul, contents, pr_null) | |
in | |
array_ptr_free(pr_free, whole_array | p) | |
end | |
prfn string_array_take_contents {a:type} {l:addr} {n:nat} (pr: string_array_v(a, l, n)): | |
(@[a][n] @ l, borrowed_string_array_v(l, n)) = let | |
prval string_array_cons(contents, pr_mul, pr_null, n) = pr | |
in | |
(contents, borrowed_string_array_cons(pr_mul, pr_null, n)) | |
end | |
prfn string_array_return_contents {a:type} {l:addr} {n:nat} | |
(contents: @[a][n] @ l, borrowed_string_array: borrowed_string_array_v(l, n)): | |
(string_array_v(a, l, n)) = let | |
prval borrowed_string_array_cons(pr_mul, pr_null, n) = borrowed_string_array | |
in | |
string_array_cons(contents, pr_mul, pr_null, n) | |
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// an array of n strings, followed by a null | |
dataview string_array_v (type, addr, int) = | |
| {a:type} {l:addr} {m:addr} {n:int} string_array_cons (a, l, n) of ( | |
@[a][n] @ l, | |
MUL(n, sizeof string, m - l), | |
ptr(null) @ m, | |
size_t n) | |
fun string_array_alloc | |
{n:nat} | |
(n: size_t(n)): | |
[a:addr] (free_gc_v(string?, n + 1, a), string_array_v(string?, a, n) | ptr a) | |
fun string_array_free | |
{n:nat} | |
{m:addr} | |
(pr_free: free_gc_v(string?, n + 1, m), pr: string_array_v(string, m, n) | p: ptr m): void | |
dataview borrowed_string_array_v (addr, int) = | |
| {l:addr} {m:addr} {n:int} borrowed_string_array_cons (l, n) of ( | |
MUL(n, sizeof string, m - l), | |
ptr(null) @ m, | |
size_t n) | |
prfun string_array_take_contents {a:type} {l:addr} {n:nat} (pr: string_array_v(a, l, n)): | |
(@[a][n] @ l, borrowed_string_array_v(l, n)) | |
prfun string_array_return_contents {a:type} {l:addr} {n:nat} | |
(contents: @[a][n] @ l, borrowed_string_array: borrowed_string_array_v(l, n)): | |
(string_array_v(a, l, n)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
staload _ = "prelude/DATS/pointer.dats" | |
staload "libc/SATS/stdlib.sats" | |
staload "json.sats" | |
staload "null_array.sats" | |
// It's always safe to treat a stropt as a generic pointer | |
extern castfn ptr_of_stropt {n:nat} (x: stropt n):<> ptr | |
// Better definition for strrchr: | |
// If a non-null pointer is returned, then it is a pointer to a non-empty null-terminated string. | |
extern fun strrchr(s: string, c: c1har): [n:int; n == ~1 | n > 0] stropt n = "mac#strrchr" | |
// Skip the first few characters of a string. Returns a pointer into the original string. | |
fn skip_chars {l:addr; n:nat; i:nat; i <= n} (s: stropt(n), i: int(i)): string (n - i) = let | |
val p = ptr_of_stropt(s) + i | |
in | |
__cast(p) where { extern castfn __cast(p: ptr): string (n - i) } | |
end | |
// Same as standard function, but take views and pointers rather than references. | |
extern fun array_copy_tsz | |
{a:t@ype} {n:nat} {d:addr} {s:addr} ( | |
pf_src: ! @[a][n] @ s, | |
pf_dest: ! @[a?][n] @ d >> @[a][n] @ d | |
| | |
src: ptr s, | |
dest: ptr d, | |
n: size_t n, | |
tsz: sizeof_t a | |
) :<> void = "atspre_array_ptr_copy_tsz" | |
/* The execv in the ATS standard library (unistd.sats) has a strange type signature (it | |
* just takes an array of pointers, not an array of strings). | |
* I think this one is better. | |
*/ | |
extern fun execv {n:pos} {m:addr} {t:addr} | |
{size:int} ( | |
pr: ! string_array_v(string,m,n) | |
| | |
path: string, argv: ptr m): int = "mac#execv" | |
// Copy string args from JSON into target_argv | |
fun initialise_prog_args | |
{m:addr} | |
{n_args:nat} | |
( | |
pr_target: @[string?][n_args] @ m | |
| | |
target: ptr m, | |
n_prog_args: size_t(n_args), | |
prog_args: !array_list(n_args) | |
): (@[string][n_args] @ m | void) = let | |
fun loop {n:nat} {l:addr} {n_args:nat} {n <= n_args} .<n>. | |
(pf: array_v (string?, n, l) | prog_args: !array_list(n_args), p: ptr l, n: size_t n, n_args: size_t(n_args)) | |
: (array_v (string, n, l) | void) = | |
if n > 0 then let | |
prval (pf1, pf2) = array_v_uncons {string?} (pf) | |
val str_obj = json_array_list_get_idx(prog_args, int1_of_size1(n_args - n)) | |
val () = !p := json_object_get_string(str_obj) | |
val (pf2 | ans) = loop (pf2 | prog_args, p+sizeof<string>, n-1, n_args) | |
in | |
(array_v_cons {string} (pf1, pf2) | ans) | |
end else let | |
prval () = array_v_unnil {string?} (pf) | |
in | |
(array_v_nil {string} () | ()) | |
end | |
in | |
loop(pr_target | prog_args, target, n_prog_args, n_prog_args) | |
end | |
fun initialise_array | |
{npa:nat} | |
{nua:nat} | |
{l:addr} | |
{m:addr} | |
{term_offset:int} | |
(argv_uninitialised: !string_array_v(string?,m,npa + nua) >> string_array_v(string,m,npa+nua), | |
user_args_pr: ! @[string][nua] @ l | |
| | |
target_argv: ptr m, | |
n_prog_args: size_t(npa), | |
prog_args: !array_list(npa), | |
n_user_args: size_t(nua), | |
user_args: ptr l | |
): void = let | |
// Get the main string array out (excluding the null pointer) | |
prval (argv_body_uninitialised, borrowed_string_array) = string_array_take_contents(argv_uninitialised) | |
// Divide the array into prog_args and user_args segments | |
val (prmul | offset_user_args) = n_prog_args szmul2 sizeof<string> | |
prval (prog_args_uninitialised, user_args_uninitialised) = array_v_split{string?}{npa + nua}{npa}(prmul, argv_body_uninitialised) | |
// Fill in each segment | |
val (prog_args_initialised | ()) = initialise_prog_args(prog_args_uninitialised | target_argv, n_prog_args, prog_args) | |
val () = array_copy_tsz{string}(user_args_pr, user_args_uninitialised | user_args, target_argv + offset_user_args, n_user_args, sizeof<string>) | |
prval user_args_initialised = user_args_uninitialised | |
// Go back to considering prog_args + user_args as a single array | |
prval argv_body_initialised = array_v_unsplit{string}(prmul, prog_args_initialised, user_args_initialised) | |
prval () = argv_uninitialised := string_array_return_contents(argv_body_initialised, borrowed_string_array) | |
in | |
() | |
end | |
extern castfn unsafe_string_of_strptr (x: !Strptr1):<> string | |
exception Missing_EnvironmentVar of () | |
// Get an environment variable or raise an exception if it's not set. | |
// Returns a copy of the string, which you need to free. | |
fn safe_getenv(env_name: !strptr1): strptr1 = let | |
val (dont_free_it | value) = getenv(unsafe_string_of_strptr(env_name)) | |
in | |
if strptr_isnot_null(value) then | |
let | |
val copy = strptr_dup(value) // getenv result only valid until the next call, so copy | |
prval () = dont_free_it(value) | |
in | |
copy | |
end | |
else | |
let | |
prval () = dont_free_it(value) | |
in | |
$raise Missing_EnvironmentVar() | |
end | |
end | |
/* | |
* Get the environment variable name from argv[0] and read its value. | |
* For some reason, doing argv.[0] in main gives the wrong pointer. | |
*/ | |
fn get_json {n:pos} {m:addr} (argv: ! @[string][n] @ m | p: ptr m): strptr1 = let | |
prval (head, tail) = array_v_uncons(argv) | |
val self_path = ptr_get_t<string>(head | p) | |
prval () = argv := array_v_cons(head, tail) | |
val last_slash = strrchr(self_path, '/') | |
val basename = if stropt_is_some(last_slash) then | |
skip_chars(last_slash, 1) | |
else | |
string1_of_string self_path | |
val env_name = strptr_of_strbuf(string1_append("0install-runenv-", basename)) | |
val json_str = safe_getenv(env_name) | |
val () = strptr_free(env_name) | |
in | |
json_str | |
end | |
exception InvalidJSON of () | |
// Parse some JSON. Raise an exception if invalid. | |
fn checked_json_tokener_parse(s: string): json_object1 = let | |
val json_root = json_tokener_parse(s) | |
in | |
if json_ptr_is_null(json_root) then | |
(prerrf("Bad JSON: %s\n", @(s)); $raise InvalidJSON()) | |
else | |
json_root | |
end | |
// The main function | |
implement main_argc_argv(argc, argv): void = let | |
// Examine the command-line arguments | |
// Get JSON string from the environment | |
val prog_args_json = get_json(view@ argv | &argv) | |
// Skip argv[0] | |
val n_user_args = argc - 1 | |
prval (pr_self, pr_user_args) = array_v_uncons(view@ argv) | |
val user_args: ptr = (&argv) + sizeof<string> | |
// Parse the JSON | |
val json_root = checked_json_tokener_parse(string1_of_strptr prog_args_json) | |
val (borrowed_json | json_array) = json_object_get_array(json_root) | |
val n_prog_args = array_list_get_length(json_array) | |
val () = assert(n_prog_args > 0) | |
// Allocate the target_argv vector to be passed to execv | |
// It will contain prog_args + user_args (plus a null, added by string_array_alloc) | |
val argv_len = n_prog_args + n_user_args | |
val (must_free_argv, str_array_v | target_argv) = string_array_alloc (size1_of_int1 argv_len) | |
// Populate target_argv from json_array and user_args | |
val () = initialise_array(str_array_v, pr_user_args | target_argv, | |
size1_of_int1 n_prog_args, json_array, | |
size1_of_int1 n_user_args, user_args) | |
// Extract the program name from target_argv | |
// This is just a long way of writing "target_prog = target_argv[0]" | |
prval (argv_initialised, borrowed_string_array) = string_array_take_contents(str_array_v) | |
prval (head, tail) = array_v_uncons(argv_initialised) | |
val target_prog: string = ptr_get_t<string>(head | target_argv) | |
prval argv_initialised = array_v_cons(head, tail) | |
prval () = str_array_v := string_array_return_contents(argv_initialised, borrowed_string_array) | |
// Exec the target program if possible | |
val error_code = execv(str_array_v | target_prog, target_argv) | |
val () = print("Failed to execv\n") | |
// Cleanup (only reached on failure) | |
prval () = minus_addback(borrowed_json, json_array | json_root) // Don't need json_array any longer | |
val () = json_object_put(json_root) // Free JSON object | |
val () = string_array_free(must_free_argv, str_array_v | target_argv) // Free target_argv | |
prval () = view@ argv := array_v_cons(pr_self, pr_user_args) // Rejoin argv[0] with argv[1:] | |
in | |
exit(1) | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment