Skip to content

Instantly share code, notes, and snippets.

@talex5
Created May 31, 2013 15:40
Show Gist options
  • Save talex5/5685858 to your computer and use it in GitHub Desktop.
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.
%{#
#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"
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
// 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))
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