Make a saw-script standard prelude

[brianhuffman]

We've talked about this internally for a while, so I'm making this ticket as a place to discuss the details. There are probably lots of boilerplate functions that would be good to have in a saw-script prelude.

[weaversa]

Here are two:

let alloc_init ty v = do {
    p <- crucible_alloc ty;
    crucible_points_to p v;
    return p;
};

let ptr_to_fresh n ty = do {
    x <- crucible_fresh_var n ty;
    p <- alloc_init ty (crucible_term x);
    return (x, p);
};

[jpziegler]

The names of those functions should probably be prepended with crucible_.

Relatedly:

let crucible_ptr_to_concrete ty v = do {
    p <- alloc_init ty (crucible_term v);
    return (x, p);
};

[atomb]

It's unlikely that we'll extend SAWScript to automatically import such a thing, but we're tracking a collection of commonly-used definitions here.

[RyanGlScott]

In the spirit of the "better-in-python" tag, it would be worth constructing a Python prelude in saw_client. The ptr_to_fresh function mentioned in https://github.com/GaloisInc/saw-script/issues/253#issuecomment-357036190 is a prime candidate for inclusion, as it is heavily featured in a demo I recently made (see https://github.com/GaloisInc/saw-demos/pull/8#discussion_r621669263). I'm biased, of course, but I'm far from the only person who's made use of ptr_to_fresh—in fact, the Python version alone is defined five separate times in saw_client's test suite alone!

The alloc_init function from https://github.com/GaloisInc/saw-script/issues/253#issuecomment-357036190 already exists in Python, as luck would have it, since the alloc() function already has an optional points_to keyword argument that allows specifying a value to point to after the pointer is allocated.

One design question: where should "prelude-like" functions such as ptr_to_fresh live? One option is to just put them alongside other definitions in saw_client.llvm. Alternatively, we could create a separate saw_client.llvm.prelude module for this purpose.

[bboston7]

Some learners wonder why pointer_to_fresh and friends aren't built in, given how useful they are. Maybe it's worth revisiting the "It's unlikely that we'll extend SAWScript to automatically import such a thing" assertion. Why not?