~lbnz/xr0

62 files changed, 2167 insertions(+), 1139 deletions(-)

M Makefile
M include/ast.h
M include/lex.h
M include/state.h
M include/value.h
A libx/assert.h
M libx/stdio.h
M libx/stdlib.h
M libx/string.h
M src/0v/ast/block.c
M src/0v/ast/expr/expr.c
M src/0v/ast/expr/expr.h
M src/0v/ast/expr/verify.c
M src/0v/ast/function/function.c
D src/0v/ast/function/paths.c
M src/0v/ast/gram.y
M src/0v/ast/lex.l
M src/0v/ast/literals.c
M src/0v/ast/literals.h
M src/0v/ast/stmt/stmt.c
M src/0v/ast/stmt/stmt.h
M src/0v/ast/stmt/verify.c
M src/0v/ast/type/type.c
M src/0v/main.c
M src/0v/object/object.c
M src/0v/state/heap.c
M src/0v/state/stack.c
M src/0v/state/stack.h
M src/0v/state/state.c
M src/0v/state/test.c
M src/0v/value/value.c
A tests/0-basic/140-FAIL-sync-free.x
A tests/0-basic/140-FAIL-sync-free.x.EXPECTED
R tests/1-branches/{000-trivial.x => 0000-trivial.x}
R tests/1-branches/{100-body-trivial.x => 0100-body-trivial.x}
R tests/1-branches/{200-conditional-allocation.x => 0200-conditional-allocation.x}
R tests/1-branches/{210-FAIL-conditional-allocation-body.x => 0210-FAIL-conditional-allocation-body.x}
R tests/1-branches/{210-FAIL-conditional-allocation-body.x.EXPECTED => 0210-FAIL-conditional-allocation-body.x.EXPECTED}
R tests/1-branches/{220-FAIL-conditional-allocation-body.x => 0220-FAIL-conditional-allocation-body.x}
R tests/1-branches/{220-FAIL-conditional-allocation-body.x.EXPECTED => 0220-FAIL-conditional-allocation-body.x.EXPECTED}
R tests/1-branches/{300-conditional-allocation-body.x => 0300-conditional-allocation-body.x}
R tests/1-branches/{310-FAIL-conditional-allocation-body.x => 0310-FAIL-conditional-allocation-body.x}
R tests/1-branches/{310-FAIL-conditional-allocation-body.x.EXPECTED => 0310-FAIL-conditional-allocation-body.x.EXPECTED}
R tests/1-branches/{320-FAIL-conditional-allocation-body.x => 0320-FAIL-conditional-allocation-body.x}
R tests/1-branches/{320-FAIL-conditional-allocation-body.x.EXPECTED => 0320-FAIL-conditional-allocation-body.x.EXPECTED}
R tests/1-branches/{400-strcmp-conditional-allocation.x => 0400-strcmp-conditional-allocation.x}
R tests/1-branches/{500-strcmp-conditional-allocation-body.x => 0500-strcmp-conditional-allocation-body.x}
R tests/1-branches/{600-indirect.x => 0600-indirect.x}
R tests/1-branches/{700-indirect.x => 0700-indirect.x}
R tests/1-branches/{800-indirect.x => 0800-indirect.x}
A tests/1-branches/0900-subsequent.x
A tests/1-branches/1000-chaining-functions.x
D tests/2-loops/002-loop-return-loc.x
D tests/2-loops/003-FAIL-return-after-free.x
D tests/2-loops/003-FAIL-return-after-free.x.EXPECTED
D tests/2-loops/006-FAIL-no-free-range.x
D tests/2-loops/006-FAIL-no-free-range.x.EXPECTED
D tests/2-loops/010-two-loops.x
D tests/2-loops/012-many-loops.x
D tests/4-linking/031-external-missing-definition.x
M tests/5-program/100-lex/parse.x
M tests/run
M Makefile => Makefile +1 -1
@@ 81,7 81,7 @@ PARSER = $(BUILD_DIR)/lex-gen

lex-gen:
	@$(XR0C) tests/3-program/100-lex/parse.x > build/parse.c
	@c89 -o $(PARSER) $(BUILD_DIR)/parse.c
	@c89 -g -o $(PARSER) $(BUILD_DIR)/parse.c
	@$(PARSER) > $(BUILD_DIR)/gen_firstchar
	@echo '%' > $(BUILD_DIR)/percent
	@diff $(BUILD_DIR)/gen_firstchar $(BUILD_DIR)/percent

M include/ast.h => include/ast.h +20 -4
@@ 14,6 14,9 @@ ast_expr_as_identifier(struct ast_expr *);
struct ast_expr *
ast_expr_constant_create(int);

struct ast_expr *
ast_expr_constant_create_char(char);

int
ast_expr_as_constant(struct ast_expr *expr);



@@ 172,6 175,11 @@ ast_expr_eval(struct ast_expr *, struct state *);
struct result *
ast_expr_absexec(struct ast_expr *, struct state *);

/* ast_expr_pf_reduce: Reduce an expression to "parameter form", in which its
 * only primitives are constants and parameters (vconsts). */
struct result *
ast_expr_pf_reduce(struct ast_expr *, struct state *);

struct ast_stmt;

struct ast_block;


@@ 187,7 195,7 @@ void
ast_block_destroy(struct ast_block *);

char *
ast_block_str(struct ast_block *);
ast_block_str(struct ast_block *, char *indent);

struct ast_block *
ast_block_copy(struct ast_block *b);


@@ 205,7 213,7 @@ struct ast_stmt **
ast_block_stmts(struct ast_block *b);

bool
ast_block_isterminal(struct ast_block *);
ast_block_isterminal(struct ast_block *, struct state *);

enum ast_jump_kind {
	JUMP_RETURN	= 1 << 0,


@@ 215,6 223,9 @@ struct ast_stmt;

struct lexememarker;

struct lexememarker *
ast_stmt_lexememarker(struct ast_stmt *);

struct ast_stmt *
ast_stmt_create_labelled(struct lexememarker *, char *label, struct ast_stmt *);



@@ 332,7 343,7 @@ struct preresult *
ast_stmt_preprocess(struct ast_stmt *, struct state *);

bool
ast_stmt_isterminal(struct ast_stmt *);
ast_stmt_isterminal(struct ast_stmt *, struct state *);

bool
ast_stmt_isselection(struct ast_stmt *);


@@ 364,6 375,11 @@ struct ast_variable_arr;
struct ast_type *
ast_type_create_struct(char *tag, struct ast_variable_arr *);

struct externals;

struct ast_type *
ast_type_struct_complete(struct ast_type *t, struct externals *ext);

struct ast_variable_arr *
ast_type_struct_members(struct ast_type *t);



@@ 389,7 405,7 @@ struct value;
struct externals;

struct value *
ast_type_vconst(struct ast_type *, struct externals *ext);
ast_type_vconst(struct ast_type *, struct state *s, char *comment, bool persist);

void
ast_type_destroy(struct ast_type *);

M include/lex.h => include/lex.h +3 -0
@@ 21,6 21,9 @@ lexememarker_copy(struct lexememarker *);
void
lexememarker_destroy(struct lexememarker *);

char *
lexememarker_str(struct lexememarker *);

extern int verbose;
extern struct ast *root;
extern struct map *table;

M include/state.h => include/state.h +3 -0
@@ 30,6 30,9 @@ state_create(char *func, struct externals *, struct ast_type *result_type);
struct state *
state_copy(struct state *);

struct state *
state_copywithname(struct state *, char *func_name);

void
state_destroy(struct state *state);


M include/value.h => include/value.h +26 -4
@@ 46,6 46,16 @@ value_sync_create(struct ast_expr *);
struct value *
value_struct_create(struct ast_type *);

bool
value_isstruct(struct value *v);

struct value *
value_struct_indefinite_create(struct ast_type *, struct state *,
		char *comment, bool persist);

struct value *
value_pf_augment(struct value *, struct ast_expr *root);

struct ast_type *
value_struct_membertype(struct value *, char *member);



@@ 67,8 77,11 @@ value_str(struct value *);
enum value_type
value_type(struct value *);

bool
value_islocation(struct value *);

struct location *
value_as_ptr(struct value *);
value_as_location(struct value *);

bool
value_referencesheap(struct value *, struct state *);


@@ 89,11 102,20 @@ struct ast_expr *
value_to_expr(struct value *);

bool
value_isliteral(struct value *v);

struct ast_expr *
value_as_literal(struct value *v);

bool
value_references(struct value *, struct location *, struct state *);

enum ast_binary_operator;

bool
values_comparable(struct value *v1, struct value *v2);

bool
value_equal(struct value *v1, struct value *v2);

/* value_assume: Returns false if contradiction encountered. */


@@ 139,9 161,9 @@ int
number_range_arr_append(struct number_range_arr *, struct number_range *);


enum number_knowledge_type {
	NUMBER_KNOWLEDGE_RANGES,
	NUMBER_KNOWLEDGE_SYNC_CONSTANT,
enum number_type {
	NUMBER_RANGES,
	NUMBER_COMPUTED,
};

struct number;

A libx/assert.h => libx/assert.h +7 -0
@@ 0,0 1,7 @@
#ifndef ASSERT_H
#define ASSERT_H

axiom void
assert(int);

#endif

M libx/stdio.h => libx/stdio.h +1 -0
@@ 1,5 1,6 @@
#ifndef STDIO_H
#define STDIO_H

#include <stddef.h>

typedef int FILE;

M libx/stdlib.h => libx/stdlib.h +2 -2
@@ 1,5 1,6 @@
#ifndef STDLIB_H
#define STDLIB_H

#include <stddef.h>

axiom void *


@@ 8,8 9,7 @@ malloc(int size) ~ [ .alloc result; ];
axiom void
free(void *ptr) ~ [ .dealloc ptr; ];

/* XXX: how to represent macros? */
axiom void
exit(int);
exit(int status);

#endif

M libx/string.h => libx/string.h +4 -0
@@ 1,5 1,6 @@
#ifndef STRING_H
#define STRING_H

#include <stddef.h>

axiom char *


@@ 12,6 13,9 @@ axiom size_t
strlen(char *s);

axiom int
strcmp(char *s1, char *s2);

axiom int
strncmp(char *s1, char *s2, size_t n);

#endif

M src/0v/ast/block.c => src/0v/ast/block.c +11 -6
@@ 15,6 15,10 @@ struct ast_block *
ast_block_create(struct ast_variable **decl, int ndecl, 
	struct ast_stmt **stmt, int nstmt)
{
	/* XXX: commented out in exec-branching work */
	/*assert(ndecl > 0 || !decl);*/
	assert(nstmt > 0 || !stmt);

	struct ast_block *b = malloc(sizeof(struct ast_block));
	b->decl = decl;
	b->ndecl = ndecl;


@@ 84,17 88,17 @@ copy_stmt_arr(int len, struct ast_stmt **stmt)
}

char *
ast_block_str(struct ast_block *b)
ast_block_str(struct ast_block *b, char *indent)
{
	struct strbuilder *sb = strbuilder_create();
	for (int i = 0; i < b->ndecl; i++) {
		char *s = ast_variable_str(b->decl[i]);
		strbuilder_printf(sb, "%s;\n", s);
		strbuilder_printf(sb, "%s%s;\n", indent, s);
		free(s);
	}
	for (int i = 0; i < b->nstmt; i++) {
		char *s = ast_stmt_str(b->stmt[i]);
		strbuilder_printf(sb, "%s\n", s);
		strbuilder_printf(sb, "%s%s\n", indent, s);
		free(s);
	}
	return strbuilder_build(sb);


@@ 109,7 113,8 @@ ast_block_ndecls(struct ast_block *b)
struct ast_variable **
ast_block_decls(struct ast_block *b)
{
	assert(b->ndecl > 0 || !b->decl);
	/* TODO: restore assert or fix structure */
	/*assert(b->ndecl > 0 || !b->decl);*/
	return b->decl;
}



@@ 127,10 132,10 @@ ast_block_stmts(struct ast_block *b)
}

bool
ast_block_isterminal(struct ast_block *b)
ast_block_isterminal(struct ast_block *b, struct state *s)
{
	for (int i = 0; i < b->nstmt; i++) {
		if (ast_stmt_isterminal(b->stmt[i])) {
		if (ast_stmt_isterminal(b->stmt[i], s)) {
			return true;
		}
	}

M src/0v/ast/expr/expr.c => src/0v/ast/expr/expr.c +195 -9
@@ 2,10 2,14 @@
#include <stdlib.h>
#include <assert.h>
#include <string.h>

#include "ast.h"
#include "ext.h"
#include "expr.h"
#include "math.h"
#include "state.h"
#include "stmt/stmt.h"
#include "util.h"
#include "expr.h"

static struct ast_expr *
ast_expr_create()


@@ 42,15 46,70 @@ ast_expr_constant_create(int k)
	/* TODO: generalise for all constant cases */
	struct ast_expr *expr = ast_expr_create();
	expr->kind = EXPR_CONSTANT;
	expr->u.constant = k;
	expr->u.constant.ischar = false;
	expr->u.constant.constant = k;
	return expr;
}

struct ast_expr *
ast_expr_constant_create_char(char c)
{
	/* TODO: generalise for all constant cases */
	struct ast_expr *expr = ast_expr_create();
	expr->kind = EXPR_CONSTANT;
	expr->u.constant.ischar = true;
	expr->u.constant.constant = c;
	return expr;
}

static char *
escape_str(char c);

static void
ast_expr_constant_str_build(struct ast_expr *expr, struct strbuilder *b)
{
	int constant = expr->u.constant.constant;
	if (!expr->u.constant.ischar) {
		strbuilder_printf(b, "%d", constant);
		return;
	}
	switch (constant) {
	case '\n': case '\t': case '\v': case '\b': case '\f':
	case '\a': case '\\': case '\?': case '\'': case '\"':
	case '\0':
		strbuilder_printf(b, "'%s'", escape_str(constant));
		break;
	default:
		strbuilder_printf(b, "'%c'", constant);
		break;
	}
}

static char *
escape_str(char c)
{
	switch (c) { 
	case '\n': return "\\n";
	case '\t': return "\\t";
	case '\v': return "\\v";
	case '\b': return "\\b";
	case '\f': return "\\f";
	case '\a': return "\\a";
	case '\\': return "\\\\";
	case '\?': return "\\?";
	case '\'': return "\\\'";
	case '\"': return "\\\"";
	/* TODO: handle octal and hex escapes */
	case '\0': return "\\0";
	default: assert(false);
	}
}

int
ast_expr_as_constant(struct ast_expr *expr)
{
	assert(expr->kind == EXPR_CONSTANT);
	return expr->u.constant;
	return expr->u.constant.constant;
}

struct ast_expr *


@@ 491,6 550,7 @@ ast_expr_assignment_create(struct ast_expr *root, struct ast_expr *value)
	return expr;
}


struct ast_expr *
ast_expr_assignment_lval(struct ast_expr *expr)
{


@@ 608,7 668,7 @@ ast_expr_str(struct ast_expr *expr)
		strbuilder_printf(b, expr->u.string);
		break;
	case EXPR_CONSTANT:
		strbuilder_printf(b, "%d", expr->u.constant);
		ast_expr_constant_str_build(expr, b);
		break;
	case EXPR_STRING_LITERAL:
		strbuilder_printf(b, "\"%s\"", expr->u.string);


@@ 654,7 714,9 @@ ast_expr_copy(struct ast_expr *expr)
	case EXPR_IDENTIFIER:
		return ast_expr_identifier_create(dynamic_str(expr->u.string));
	case EXPR_CONSTANT:
		return ast_expr_constant_create(expr->u.constant);
		return expr->u.constant.ischar
			? ast_expr_constant_create_char(expr->u.constant.constant)
			: ast_expr_constant_create(expr->u.constant.constant);
	case EXPR_STRING_LITERAL:
		return ast_expr_literal_create(dynamic_str(expr->u.string));
	case EXPR_BRACKETED:


@@ 715,7 777,7 @@ ast_expr_equal(struct ast_expr *e1, struct ast_expr *e2)
	}
	switch (e1->kind) {
	case EXPR_CONSTANT:
		return e1->u.constant == e2->u.constant;
		return e1->u.constant.constant == e2->u.constant.constant;
	case EXPR_IDENTIFIER:
		return strcmp(ast_expr_as_identifier(e1), ast_expr_as_identifier(e2)) == 0;
	case EXPR_STRING_LITERAL:


@@ 741,6 803,13 @@ ast_expr_equal(struct ast_expr *e1, struct ast_expr *e2)
			}
		}
		return ast_expr_equal(e1->root, e2->root);
	case EXPR_STRUCTMEMBER:
		return ast_expr_equal(
			ast_expr_member_root(e1),
			ast_expr_member_root(e2)
		) && (strcmp(
			ast_expr_member_field(e1), ast_expr_member_field(e2)
		) == 0);
	default:
		assert(false);
	}


@@ 798,15 867,15 @@ math_expr(struct ast_expr *e)
			math_atom_variable_create(dynamic_str(e->u.string))
		);
	case EXPR_CONSTANT:
		if (e->u.constant < 0) {
		if (e->u.constant.constant < 0) {
			return math_expr_neg_create(
				math_expr_atom_create(
					math_atom_nat_create(-e->u.constant)
					math_atom_nat_create(-e->u.constant.constant)
				)
			);
		}
		return math_expr_atom_create(
			math_atom_nat_create(e->u.constant)
			math_atom_nat_create(e->u.constant.constant)
		);
	case EXPR_BINARY:
		return math_expr_sum_create(


@@ 866,6 935,39 @@ ast_expr_getfuncs(struct ast_expr *expr)
	}
}

static struct ast_stmt_splits
call_splits(struct ast_expr *, struct state *);

static struct ast_stmt_splits
binary_splits(struct ast_expr *, struct state *);

struct ast_stmt_splits
ast_expr_splits(struct ast_expr *e, struct state *s)
{
	switch (ast_expr_kind(e)) {
	case EXPR_CALL:
		return call_splits(e, s);
	case EXPR_ASSIGNMENT:
		return ast_expr_splits(ast_expr_assignment_rval(e), s);
	case EXPR_UNARY:
		return ast_expr_splits(ast_expr_unary_operand(e), s);
	case EXPR_BINARY:
		return binary_splits(e, s);
	case EXPR_INCDEC:
		return ast_expr_splits(ast_expr_incdec_root(e), s);
	case EXPR_STRUCTMEMBER:
		return ast_expr_splits(ast_expr_member_root(e), s);
	case EXPR_CONSTANT:
	case EXPR_IDENTIFIER:
	case EXPR_STRING_LITERAL:
	case EXPR_ARBARG:
		return (struct ast_stmt_splits) { .n = 0, .cond = NULL };
	default:
		/*printf("expr: %s\n", ast_expr_str(e));*/
		assert(false);
	}
}

static struct string_arr *
ast_expr_call_getfuncs(struct ast_expr *expr)
{


@@ 883,4 985,88 @@ ast_expr_call_getfuncs(struct ast_expr *expr)
	return res;
}

static struct ast_stmt_splits
call_splits(struct ast_expr *expr, struct state *state)
{
	struct ast_expr *root = ast_expr_call_root(expr);
	/* TODO: function-valued-expressions */
	char *name = ast_expr_as_identifier(root);

	struct ast_function *f = externals_getfunc(state_getext(state), name);
	if (!f) {
		/* TODO: user error */
		fprintf(stdout, "function `%s' not found\n", name);
		assert(false);
	}

	int nparams = ast_function_nparams(f);
	struct ast_variable **params = ast_function_params(f);

	struct state *s_copy = state_copy(state);
	struct result_arr *args = prepare_arguments(
		ast_expr_call_nargs(expr),
		ast_expr_call_args(expr),
		nparams, params, s_copy
	);

	struct ast_type *ret_type = ast_function_type(f);
	state_pushframe(s_copy, dynamic_str(name), ret_type);

	struct error *err = prepare_parameters(
		nparams, params, args, name, s_copy
	);
	if (err) {
		fprintf(stderr, "err: %s\n", err->msg);
		assert(false);
	}

	int n = 0;
	struct ast_expr **cond = NULL;

	struct ast_block *abs = ast_function_abstract(f);

	int ndecls = ast_block_ndecls(abs);
	if (ndecls) {
		struct ast_variable **var = ast_block_decls(abs);
		for (int i = 0; i < ndecls; i++) {
			state_declare(s_copy, var[i], false);
		}
	}

	int nstmts = ast_block_nstmts(abs);
	struct ast_stmt **stmt = ast_block_stmts(abs);
	for (int i = 0; i < nstmts; i++) {
		struct ast_stmt_splits splits = ast_stmt_splits(stmt[i], s_copy);
		for (int j = 0; j < splits.n; j++) {
			cond = realloc(cond, sizeof(struct ast_expr *) * ++n);
			cond[n-1] = splits.cond[j];
		}
		/* XXX: for assignment statements and, well, spare us */
		ast_stmt_absexec(stmt[i], s_copy);
	}

	state_popframe(s_copy);
	result_arr_destroy(args);

	return (struct ast_stmt_splits) { .n = n, .cond = cond };
}

static struct ast_stmt_splits
binary_splits(struct ast_expr *e, struct state *s)
{
	struct ast_stmt_splits s1 = ast_expr_splits(ast_expr_binary_e1(e), s),
			       s2 = ast_expr_splits(ast_expr_binary_e2(e), s);

	int n = s1.n + s2.n;
	struct ast_expr **cond = malloc(sizeof(struct ast_expr *) * n);
	for (int i = 0; i < s1.n; i++) {
		cond[i] = s1.cond[i];
	}
	for (int i = 0; i < s2.n; i++) {
		cond[i+s1.n] = s2.cond[i];
	}

	return (struct ast_stmt_splits) { .n = n, .cond = cond };
}

#include "verify.c"

M src/0v/ast/expr/expr.h => src/0v/ast/expr/expr.h +33 -2
@@ 27,7 27,10 @@ struct ast_expr {
	struct ast_expr *root;
	union {
		char *string; /* identifier, literal, assertion */
		int constant;
		struct { 
			int constant;
			bool ischar;
		} constant;
		struct {
			int n;
			struct ast_expr **arg;


@@ 70,7 73,35 @@ ast_expr_binary_create(struct ast_expr *e1, enum ast_binary_operator,
		struct ast_expr *e2);

enum ast_binary_operator
ast_expr_binary_op(struct ast_expr *expr);
ast_expr_binary_op(struct ast_expr *);

struct ast_stmt_splits
ast_expr_splits(struct ast_expr *, struct state *);

struct result_arr {
	int n;
	struct result **res;
};

struct result_arr *
result_arr_create();

void
result_arr_destroy(struct result_arr *arr);

void
result_arr_append(struct result_arr *arr, struct result *res);


struct result_arr *
prepare_arguments(int nargs, struct ast_expr **arg, int nparams,
		struct ast_variable **param, struct state *state);

struct error *
prepare_parameters(int nparams, struct ast_variable **param, 
		struct result_arr *args, char *fname, struct state *state);



struct string_arr *
ast_expr_getfuncs(struct ast_expr *);

M src/0v/ast/expr/verify.c => src/0v/ast/expr/verify.c +414 -109
@@ 13,6 13,7 @@
#include "state.h"
#include "util.h"
#include "value.h"
#include "type/type.h"

static bool
expr_unary_decide(struct ast_expr *expr, struct state *state);


@@ 184,22 185,23 @@ expr_unary_lvalue(struct ast_expr *expr, struct state *state)
struct lvalue *
expr_structmember_lvalue(struct ast_expr *expr, struct state *state)
{
	struct lvalue *root = ast_expr_lvalue(ast_expr_member_root(expr), state);
	struct object *root_obj = lvalue_object(root);
	struct ast_expr *root = ast_expr_member_root(expr);
	struct lvalue *root_lval = ast_expr_lvalue(root, state);
	struct object *root_obj = lvalue_object(root_lval);
	assert(root_obj);
	struct object *obj = object_getmember(
		root_obj,
		lvalue_type(root),
		ast_expr_member_field(expr),
		state
	char *field = ast_expr_member_field(expr);
	struct object *member = object_getmember(
		root_obj, lvalue_type(root_lval), field, state
	);
	if (!member) {
		/* TODO: lvalue error */
		return lvalue_create(NULL, NULL);
	}
	struct ast_type *t = object_getmembertype(
		root_obj,
		lvalue_type(root),
		ast_expr_member_field(expr),
		state
		root_obj, lvalue_type(root_lval), field, state
	);
	return lvalue_create(t, obj);
	assert(t);
	return lvalue_create(t, member);
}




@@ 237,6 239,8 @@ expr_binary_decide(struct ast_expr *expr, struct state *state)

	assert(!result_iserror(root) && !result_iserror(last));

	/*printf("state: %s\n", state_str(state));*/
	/*printf("expr: %s\n", ast_expr_str(expr));*/
	return value_compare(
		result_as_value(root),
		ast_expr_binary_op(expr),


@@ 286,6 290,9 @@ expr_incdec_eval(struct ast_expr *expr, struct state *state);
static struct result *
expr_binary_eval(struct ast_expr *expr, struct state *state);

static struct result *
arbarg_eval(struct ast_expr *expr, struct state *state);

struct result *
ast_expr_eval(struct ast_expr *expr, struct state *state)
{


@@ 310,6 317,8 @@ ast_expr_eval(struct ast_expr *expr, struct state *state)
		return expr_incdec_eval(expr, state);
	case EXPR_BINARY:
		return expr_binary_eval(expr, state);
	case EXPR_ARBARG:
		return arbarg_eval(expr, state);
	default:
		assert(false);
	}


@@ 332,33 341,88 @@ expr_constant_eval(struct ast_expr *expr, struct state *state)
}

static struct result *
hack_identifier_builtin_eval(char *id, struct state *state);

static struct result *
expr_identifier_eval(struct ast_expr *expr, struct state *state)
{
	struct object *obj = state_getobject(state, ast_expr_as_identifier(expr));
	struct result *res = hack_identifier_builtin_eval(
		ast_expr_as_identifier(expr), state
	);
	if (!result_iserror(res) && result_hasvalue(res)) {
		return res;
	}

	char *id = ast_expr_as_identifier(expr);
	struct object *obj = state_getobject(state, id);
	if (!obj) {
		return result_error_create(error_create("no object"));
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(b, "unknown idenitfier `%s'", id);
		return result_error_create(error_create(strbuilder_build(b)));
	}
	struct value *val = object_as_value(obj);
	if (!val) {
		return result_error_create(error_create("no value"));
		printf("state: %s\n", state_str(state));
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(b, "`%s' has no value", id);
		return result_error_create(error_create(strbuilder_build(b)));
	}
	return result_value_create(value_copy(val));
}

static struct result *
hack_identifier_builtin_eval(char *id, struct state *state)
{
	if (state_getvconst(state, id) || strncmp(id, "ptr:", 4) == 0) {
		return result_value_create(
			value_sync_create(ast_expr_identifier_create(dynamic_str(id)))
		);
	}
	return result_error_create(error_create("not built-in"));
}

static struct ast_expr *
expr_to_binary(struct ast_expr *expr);

static struct result *
binary_deref_eval(struct ast_expr *expr, struct state *state);

static struct result *
expr_unary_eval(struct ast_expr *expr, struct state *state)
{
	assert(ast_expr_unary_op(expr) == UNARY_OP_DEREFERENCE);

	struct ast_expr *inner = ast_expr_unary_operand(expr); /* arr+offset */
	struct ast_expr *binary = expr_to_binary(ast_expr_unary_operand(expr));
	struct result *res = binary_deref_eval(binary, state);
	ast_expr_destroy(binary);
	return res;
}

static struct ast_expr *
expr_to_binary(struct ast_expr *expr)
{
	switch (ast_expr_kind(expr)) {
	case EXPR_BINARY:
		return ast_expr_copy(expr);
	default:
		return ast_expr_binary_create(
			ast_expr_copy(expr),
			BINARY_OP_ADDITION,
			ast_expr_constant_create(0)
		);
	}
}

	struct result *res = ast_expr_eval(ast_expr_binary_e1(inner), state);
static struct result *
binary_deref_eval(struct ast_expr *expr, struct state *state)
{
	struct result *res = ast_expr_eval(ast_expr_binary_e1(expr), state);
	if (result_iserror(res)) {
		return res;
	}
	struct value *arr = result_as_value(res);
	assert(arr);
	struct object *obj = state_deref(state, arr, ast_expr_binary_e2(inner));
	struct object *obj = state_deref(state, arr, ast_expr_binary_e2(expr));
	assert(obj);
	result_destroy(res);



@@ 371,17 435,24 @@ expr_unary_eval(struct ast_expr *expr, struct state *state)
static struct result *
expr_structmember_eval(struct ast_expr *expr, struct state *s)
{
	struct result *res = ast_expr_eval(ast_expr_member_root(expr), s);
	struct ast_expr *root = ast_expr_member_root(expr);
	struct result *res = ast_expr_eval(root, s);
	if (result_iserror(res)) {
		return res;
	}
	char *field = ast_expr_member_field(expr);
	struct object *member = value_struct_member(result_as_value(res), field);
	if (!member) {
		struct strbuilder *b = strbuilder_create();
		char *root_str = ast_expr_str(root);
		strbuilder_printf(
			b, "`%s' has no field `%s'", root_str, field
		);
		free(root_str);
		return result_error_create(error_create(strbuilder_build(b)));
	}
	struct value *obj_value = object_as_value(member);
	/* XXX */
	struct value *obj_value = object_as_value(
		value_struct_member(
			result_as_value(res),
			ast_expr_member_field(expr)
		)
	);
	struct value *v = obj_value ? value_copy(obj_value) : NULL;
	result_destroy(res);
	return result_value_create(v);


@@ 389,11 460,6 @@ expr_structmember_eval(struct ast_expr *expr, struct state *s)

/* expr_call_eval */

struct result_arr {
	int n;
	struct result **res;
};

struct result_arr *
result_arr_create()
{


@@ 416,16 482,19 @@ result_arr_append(struct result_arr *arr, struct result *res)
	arr->res[arr->n-1] = res;
}

static struct result_arr *
struct result_arr *
prepare_arguments(int nargs, struct ast_expr **arg, int nparams,
		struct ast_variable **param, struct state *state);

static struct error *
struct error *
prepare_parameters(int nparams, struct ast_variable **param, 
		struct result_arr *args, struct state *state);
		struct result_arr *args, char *fname, struct state *state);

static struct result *
call_result(struct ast_expr *expr, struct ast_function *, struct state *);
call_absexec(struct ast_expr *call, struct ast_function *, struct state *);

static struct result *
pf_augment(struct value *v, struct ast_expr *root, struct state *);

static struct result *
expr_call_eval(struct ast_expr *expr, struct state *state)


@@ 452,66 521,117 @@ expr_call_eval(struct ast_expr *expr, struct state *state)
	struct ast_type *ret_type = ast_function_type(f);
	state_pushframe(state, dynamic_str(name), ret_type);

	struct error *err = prepare_parameters(nparams, params, args, state);
	struct error *err = prepare_parameters(
		nparams, params, args, name, state
	);
	if (err) {
		return result_error_create(err);
	}

	struct result *res = ast_function_absexec(f, state);
	struct result *res = call_absexec(expr, f, state);
	if (result_iserror(res)) {
		return res;
	}
	if (result_hasvalue(res)) { /* preserve value through pop */
		res = result_value_create(value_copy(result_as_value(res)));
	} else {
		res = call_result(expr, f, state);
	/* copy to preserve value through popping of frame */
	struct value *v = NULL;
	if (result_hasvalue(res)) {
		v = value_copy(result_as_value(res));
	}

	state_popframe(state);

	result_arr_destroy(args);

	if (v) {
		return pf_augment(v, expr, state);
	}

	return res;
}

static bool
vconst_applyassumptions(struct value *v, struct ast_expr *call, struct state *state);
static struct result *
call_arbitraryresult(struct ast_expr *call, struct ast_function *, struct state *);

static struct result *
call_result(struct ast_expr *expr, struct ast_function *f, struct state *state)
call_absexec(struct ast_expr *expr, struct ast_function *f, struct state *state)
{
	/* declare vconst and get underlying value (i.e. the range) */
	struct value *vconst = state_vconst(
		state,
		ast_function_type(f),
		dynamic_str(ast_function_name(f)),
		false
	);
	struct ast_expr *sync = value_as_sync(vconst);
	struct value *v = state_getvconst(state, ast_expr_as_identifier(sync));

	bool ok = vconst_applyassumptions(v, expr, state);
	assert(ok);
	struct result *res = ast_function_absexec(f, state);
	if (result_iserror(res) || result_hasvalue(res)) {
		return res;
	}
	return call_arbitraryresult(expr, f, state);
}

	return result_value_create(vconst);
static struct result *
pf_augment(struct value *v, struct ast_expr *call, struct state *state)
{
	if (!value_isstruct(v)) {
		return result_value_create(value_copy(v));
	}
	struct result *res = ast_expr_pf_reduce(call, state);
	if (result_iserror(res)) {
		return res;
	}
	assert(result_hasvalue(res));
	return result_value_create(
		value_pf_augment(v, value_as_sync(result_as_value(res)))
	);
}

static bool
vconst_applyassumptions(struct value *v, struct ast_expr *expr, struct state *state)
static struct result *
call_to_computed_value(struct ast_function *, struct state *s);

static struct result *
call_arbitraryresult(struct ast_expr *expr, struct ast_function *f,
		struct state *state)
{
	struct props *p = state_getprops(state);
	if (props_get(p, expr)) {
		return value_assume(v, true);
	} else if (props_contradicts(p, expr)) {
		return value_assume(v, false);
	struct result *res = call_to_computed_value(f, state);
	if (result_iserror(res)) {
		return res;
	}
	return true;
	assert(result_hasvalue(res));
	return res;
}

static struct result *
prepare_argument(struct ast_expr *arg, struct ast_variable *param, struct state *);
call_to_computed_value(struct ast_function *f, struct state *s)
{
	/* TODO: function-valued root */
	char *root = ast_function_name(f);

static struct result_arr *
	int nparams = ast_function_nparams(f);
	struct ast_variable **uncomputed_param = ast_function_params(f);
	struct ast_expr **computed_param = malloc(
		sizeof(struct ast_expr *) * nparams
	);
	for (int i = 0; i < nparams; i++) {
		struct ast_expr *param = ast_expr_identifier_create(
			dynamic_str(ast_variable_name(uncomputed_param[i]))
		);
		struct result *res = ast_expr_eval(param, s);
		ast_expr_destroy(param);
		if (result_iserror(res)) {
			return res;
		}
		assert(result_hasvalue(res));
		struct value *v = result_as_value(res);
		if (value_islocation(v)) {
			computed_param[i] = ast_expr_identifier_create(value_str(v));
		} else {
			computed_param[i] = value_to_expr(v);
		}
	}

	return result_value_create(
		value_sync_create(
			ast_expr_call_create(
				ast_expr_identifier_create(dynamic_str(root)),
				nparams, computed_param
			)
		)
	);
}

struct result_arr *
prepare_arguments(int nargs, struct ast_expr **arg, int nparams,
		struct ast_variable **param, struct state *state)
{


@@ 519,29 639,16 @@ prepare_arguments(int nargs, struct ast_expr **arg, int nparams,

	struct result_arr *args = result_arr_create();
	for (int i = 0; i < nargs; i++) {
		result_arr_append(
			args, prepare_argument(arg[i], param[i], state)
		);
		result_arr_append(args, ast_expr_eval(arg[i], state));
	}
	return args;
}

static struct result *
prepare_argument(struct ast_expr *arg, struct ast_variable *p, struct state *s)
{
	if (ast_expr_kind(arg) != EXPR_ARBARG) {
		return ast_expr_eval(arg, s);
	}
	return result_value_create(state_vconst(
		s, ast_variable_type(p), dynamic_str(ast_variable_name(p)), true
	));
}

/* prepare_parameters: Allocate arguments in call expression and assign them to
 * their respective parameters. */
static struct error *
struct error *
prepare_parameters(int nparams, struct ast_variable **param, 
		struct result_arr *args, struct state *state)
		struct result_arr *args, char *fname, struct state *state)
{
	assert(nparams == args->n);



@@ 550,18 657,16 @@ prepare_parameters(int nparams, struct ast_variable **param,

		struct result *res = args->res[i];
		if (result_iserror(res)) {
			struct strbuilder *b = strbuilder_create();
			strbuilder_printf(
				b, "param `%s': ",
				ast_variable_name(param[i])
			);
			return error_prepend(
				result_as_error(res), strbuilder_build(b)
			);
			return result_as_error(res);
		}

		if (!result_hasvalue(res)) {
			continue;
			struct strbuilder *b = strbuilder_create();
			strbuilder_printf(
				b, "parameter `%s' of function `%s' has no value",
				ast_variable_name(param[i]), fname
			);
			return error_create(strbuilder_build(b));
		}

		struct ast_expr *name = ast_expr_identifier_create(


@@ 585,12 690,22 @@ expr_assign_eval(struct ast_expr *expr, struct state *state)
	if (result_iserror(res)) {
		return res;
	}
	if (result_hasvalue(res)) {
		/*printf("state: %s\n", state_str(state));*/
		struct object *obj = lvalue_object(ast_expr_lvalue(lval, state));
		assert(obj);
		object_assign(obj, value_copy(result_as_value(res)));
	if (!result_hasvalue(res)) {
		struct strbuilder *b = strbuilder_create();
		char *s = ast_expr_str(rval);
		strbuilder_printf(b, "`%s' has no value", s);
		free(s);
		return result_error_create(error_create(strbuilder_build(b)));
	}
	struct object *obj = lvalue_object(ast_expr_lvalue(lval, state));
	if (!obj) {
		struct strbuilder *b = strbuilder_create();
		char *s = ast_expr_str(lval);
		strbuilder_printf(b, "`%s' is not a valid object", s);
		free(s);
		return result_error_create(error_create(strbuilder_build(b)));
	}
	object_assign(obj, value_copy(result_as_value(res)));
	return res;
}



@@ 639,6 754,18 @@ expr_binary_eval(struct ast_expr *expr, struct state *state)
}

static struct result *
arbarg_eval(struct ast_expr *expr, struct state *state)
{
	return result_value_create(state_vconst(
		state,
		/* XXX: we will investigate type conversions later */
		ast_type_create_ptr(ast_type_create(TYPE_VOID, 0)),
		NULL,
		false
	));
}

static struct result *
assign_absexec(struct ast_expr *expr, struct state *state);

struct result *


@@ 668,44 795,201 @@ ast_expr_assume(struct ast_expr *expr, struct state *state)
}

static struct preresult *
identifier_assume(char *id, bool value, struct state *state);
identifier_assume(struct ast_expr *expr, bool value, struct state *state);

static struct preresult *
ast_expr_pf_reduce_assume(struct ast_expr *, bool value, struct state *);

static struct preresult *
irreducible_assume(struct ast_expr *, bool value, struct state *);

static struct preresult *
binary_assume(struct ast_expr *expr, bool value, struct state *);

static struct preresult *
reduce_assume(struct ast_expr *expr, bool value, struct state *s)
{
	switch (expr->kind) {
	case EXPR_IDENTIFIER:
		return identifier_assume(ast_expr_as_identifier(expr), value, s);
		return identifier_assume(expr, value, s);
	case EXPR_UNARY:
		assert(ast_expr_unary_op(expr) == UNARY_OP_BANG);
		return reduce_assume(ast_expr_unary_operand(expr), !value, s);
	case EXPR_BRACKETED:
		return reduce_assume(expr->root, value, s);
	case EXPR_CALL:
	case EXPR_STRUCTMEMBER:
		return ast_expr_pf_reduce_assume(expr, value, s);
	case EXPR_BINARY:
		return irreducible_assume(expr, value, s);
		return binary_assume(expr, value, s);
	default:
		assert(false);
	}
}

static struct preresult *
identifier_assume(char *id, bool value, struct state *state)
identifier_assume(struct ast_expr *expr, bool value, struct state *s)
{
	/* set value of variable corresponding to identifier != 0 */
	struct object *obj = state_getobject(state, id);
	struct ast_expr *sync = value_as_sync(object_as_value(obj));
	struct value *v = state_getvconst(state, ast_expr_as_identifier(sync));
	bool iscontradiction = !value_assume(v, value);
	if (iscontradiction) {
		return preresult_contradiction_create();
	struct state *s_copy = state_copy(s);
	struct result *res = ast_expr_eval(expr, s_copy);

	/* TODO: user errors */
	assert(!result_iserror(res) && result_hasvalue(res));

	state_destroy(s_copy);

	return irreducible_assume(value_as_sync(result_as_value(res)), value, s);
}

static struct preresult *
ast_expr_pf_reduce_assume(struct ast_expr *expr, bool value, struct state *s)
{
	struct result *res = ast_expr_pf_reduce(expr, s);
	/* TODO: user errors */
	assert(!result_iserror(res) && result_hasvalue(res));

	return irreducible_assume(value_as_sync(result_as_value(res)), value, s);
}

static struct result *
binary_pf_reduce(struct ast_expr *e1, enum ast_binary_operator,
		struct ast_expr *e2, struct state *);

static struct result *
unary_pf_reduce(struct ast_expr *, struct state *);

static struct result *
call_pf_reduce(struct ast_expr *, struct state *);

static struct result *
structmember_pf_reduce(struct ast_expr *, struct state *);

struct result *
ast_expr_pf_reduce(struct ast_expr *e, struct state *s)
{
	switch (ast_expr_kind(e)) {
	case EXPR_CONSTANT:
	case EXPR_STRING_LITERAL:
	case EXPR_IDENTIFIER:
		return ast_expr_eval(e, s);
	case EXPR_UNARY:
		return unary_pf_reduce(e, s);
	case EXPR_BINARY:
		return binary_pf_reduce(
			ast_expr_binary_e1(e),
			ast_expr_binary_op(e),
			ast_expr_binary_e2(e),
			s
		);
	case EXPR_CALL:
		return call_pf_reduce(e, s);
	case EXPR_STRUCTMEMBER:
		return structmember_pf_reduce(e, s);
	default:
		assert(false);
	}
	return preresult_empty_create();
}

static struct result *
unary_pf_reduce(struct ast_expr *e, struct state *s)
{
	/* TODO: reduce by actually dereferencing if expr is a deref and this is
	 * possible in the current state */
	struct result *res = ast_expr_pf_reduce(ast_expr_unary_operand(e), s);
	if (result_iserror(res)) {
		return res;
	}
	assert(result_hasvalue(res));
	return result_value_create(
		value_sync_create(
			ast_expr_unary_create(
				value_as_sync(result_as_value(res)),
				ast_expr_unary_op(e)
			)
		)
	);
}

static struct result *
binary_pf_reduce(struct ast_expr *e1, enum ast_binary_operator op,
		struct ast_expr *e2, struct state *s)
{
	struct result *res1 = ast_expr_pf_reduce(e1, s);
	if (result_iserror(res1)) {
		return res1;
	}
	assert(result_hasvalue(res1));
	struct result *res2 = ast_expr_pf_reduce(e2, s);
	if (result_iserror(res2)) {
		return res2;
	}
	assert(result_hasvalue(res2));
	return result_value_create(
		value_sync_create(
			ast_expr_binary_create(
				value_to_expr(result_as_value(res1)),
				op,
				value_to_expr(result_as_value(res2))
			)
		)
	);
}

static struct result *
call_pf_reduce(struct ast_expr *e, struct state *s)
{
	/* TODO: allow for exprs as root */
	char *root = ast_expr_as_identifier(ast_expr_call_root(e));

	int nargs = ast_expr_call_nargs(e);
	struct ast_expr **unreduced_arg = ast_expr_call_args(e);
	struct ast_expr **reduced_arg = malloc(sizeof(struct ast_expr *) *nargs);
	for (int i = 0; i < nargs; i++) {
		struct result *res = ast_expr_pf_reduce(unreduced_arg[i], s);
		if (result_iserror(res)) {
			return res;
		}
		assert(result_hasvalue(res));
		reduced_arg[i] = ast_expr_copy(value_to_expr(result_as_value(res)));
	}
	return result_value_create(
		value_sync_create(
			ast_expr_call_create(
				ast_expr_identifier_create(dynamic_str(root)),
				nargs, reduced_arg
			)
		)
	);
}

static struct result *
structmember_pf_reduce(struct ast_expr *expr, struct state *s)
{
	struct result *res = ast_expr_pf_reduce(ast_expr_member_root(expr), s);
	if (result_iserror(res)) {
		return res;
	}
	assert(result_hasvalue(res));
	char *field = ast_expr_member_field(expr);
	struct value *v = result_as_value(res);
	if (value_isstruct(v)) {
		struct object *obj = value_struct_member(v, field);
		struct value *obj_value = object_as_value(obj);
		assert(obj_value);
		return result_value_create(value_copy(obj_value));
	}
	assert(value_issync(v));
	return result_value_create(
		value_sync_create(
			ast_expr_member_create(
				value_as_sync(v),
				dynamic_str(field)
			)
		)
	);
}


static struct preresult *
irreducible_assume_actual(struct ast_expr *e, struct state *s);



@@ 728,3 1012,24 @@ irreducible_assume_actual(struct ast_expr *e, struct state *s)
	props_install(state_getprops(s), ast_expr_copy(e));
	return preresult_empty_create();
}

static struct preresult *
binary_assume(struct ast_expr *expr, bool value, struct state *s)
{
	struct result *r1 = ast_expr_pf_reduce(expr->u.binary.e1, s),
		      *r2 = ast_expr_pf_reduce(expr->u.binary.e2, s);

	/* TODO: user errors */
	struct value *v1 = result_as_value(r1),
		     *v2 = result_as_value(r2);

	return irreducible_assume(
		ast_expr_binary_create(
			value_to_expr(v1),
			expr->u.binary.op,
			value_to_expr(v2)
		),
		value,
		s
	);
}

M src/0v/ast/function/function.c => src/0v/ast/function/function.c +352 -70
@@ 10,6 10,8 @@
#include "object.h"
#include "props.h"
#include "state.h"
#include "type/type.h"
#include "stmt/stmt.h"
#include "ext.h"
#include "util.h"



@@ 69,23 71,30 @@ char *
ast_function_str(struct ast_function *f)
{
	struct strbuilder *b = strbuilder_create();
	strbuilder_printf(b, "func");
	if (f->isaxiom) {
		strbuilder_printf(b, " <axiom>");
		strbuilder_printf(b, "axiom ");
	}
	strbuilder_printf(b, " `%s'", f->name);
	char *ret = ast_type_str(f->ret);
	strbuilder_printf(b, " returns %s ", ret);
	strbuilder_printf(b, "%s\n", ret);
	free(ret);
	strbuilder_printf(b, "takes [");
	strbuilder_printf(b, "%s(", f->name);
	for (int i = 0; i < f->nparam; i++) {
		char *v = ast_variable_str(f->param[i]);
		char *space = (i + 1 < f->nparam) ? ", " : "";
		strbuilder_printf(b, "%s%s", v, space);
		free(v);
	}
	strbuilder_printf(b, "] has abstract:\n%s\n", ast_block_str(f->abstract));
	strbuilder_printf(b, "has body: %s\n", f->body ? ast_block_str(f->body) : "");
	char *abs = ast_block_str(f->abstract, "\t");
	strbuilder_printf(b, ") ~ [\n%s]", abs);
	free(abs);
	if (f->body) {
		char *body = ast_block_str(f->body, "\t");
		strbuilder_printf(b, "{\n%s}", body);
		free(body);
	} else {
		strbuilder_printf(b, ";");
	}
	strbuilder_printf(b, "\n");
	return strbuilder_build(b);
}



@@ 167,18 176,6 @@ ast_function_params(struct ast_function *f)
	return f->param;
}

struct error *
paths_verify(struct ast_function_arr *paths, struct externals *);

struct error *
ast_function_verify(struct ast_function *f, struct externals *ext)
{
	struct ast_function_arr *paths = paths_fromfunction(f);
	struct error *err = paths_verify(paths, ext);
	ast_function_arr_destroy(paths);
	return err;
}

struct ast_function *
ast_function_protostitch(struct ast_function *f, struct externals *ext)
{


@@ 192,52 189,38 @@ ast_function_protostitch(struct ast_function *f, struct externals *ext)
}

struct error *
path_verify_withstate(struct ast_function *f, struct externals *ext);
paths_verify(struct ast_function_arr *paths, struct externals *);

struct error *
paths_verify(struct ast_function_arr *paths, struct externals *ext)
{	
	int len = ast_function_arr_len(paths);
	struct ast_function **path = ast_function_arr_func(paths);
	for (int i = 0; i < len; i++) {
		struct error *err = NULL;
		if ((err = path_verify_withstate(path[i], ext))) {
			return err;
		}
	}
	return NULL;
}
static struct error *
path_verify_withstate(struct ast_function *f, struct state *);

struct error *
path_verify(struct ast_function *f, struct state *state, struct externals *);
static void
declare_parameters(struct state *s, struct ast_function *f);

struct error *
path_verify_withstate(struct ast_function *f, struct externals *ext)
ast_function_verify(struct ast_function *f, struct externals *ext)
{
	struct state *state = state_create(
		dynamic_str(ast_function_name(f)), ext, ast_function_type(f)
	);
	/*printf("state: %s\n", state_str(state));*/
	struct error *err = path_verify(f, state, ext);
	declare_parameters(state, f);
	struct error *err = path_verify_withstate(f, state);
	state_destroy(state);
	return err;
}

static struct error *
abstract_audit(struct ast_function *f, struct state *actual_state,
		struct externals *);
path_verify(struct ast_function *f, struct state *state, int index);

static struct preresult *
parameterise_state(struct state *s, struct ast_function *f);
install_props(struct state *s, struct ast_function *f);

struct error *
path_verify(struct ast_function *f, struct state *state, struct externals *ext)
static struct error *
path_verify_withstate(struct ast_function *f, struct state *state)
{
	struct error *err = NULL;

	struct ast_block *body = ast_function_body(f);

	struct preresult *r = parameterise_state(state, f);
	struct preresult *r = install_props(state, f);
	if (preresult_iserror(r)) {
		return preresult_as_error(r);
	} else if (preresult_iscontradiction(r)) {


@@ 251,27 234,53 @@ path_verify(struct ast_function *f, struct state *state, struct externals *ext)
		state_declare(state, var[i], false);
	}

	return path_verify(f, state, 0);
}

static struct error *
abstract_audit(struct ast_function *f, struct state *actual_state);

static struct error *
split_paths_verify(struct ast_function *f, struct state *, int index,
		struct ast_stmt_splits *splits);

static struct error *
path_verify(struct ast_function *f, struct state *state, int index)
{
	struct error *err = NULL;

	struct ast_block *body = ast_function_body(f);

	int nstmts = ast_block_nstmts(body);
	struct ast_stmt **stmt = ast_block_stmts(body);
	for (int i = 0; i < nstmts; i++) {
	for (int i = index; i < nstmts; i++) {
		/*printf("state: %s\n", state_str(state));*/
		/*printf("%s\n", ast_stmt_str(stmt[i]));*/
		struct ast_stmt_splits splits = ast_stmt_splits(stmt[i], state);
		if (splits.n) {
			assert(splits.cond);
			return split_paths_verify(f, state, i, &splits);
		}
		if ((err = ast_stmt_process(stmt[i], state))) {
			return err;
		}
		if (ast_stmt_isterminal(stmt[i])) {
		if (ast_stmt_isterminal(stmt[i], state)) {
			break;
		}
	}
	if (!state_hasgarbage(state)) {
		printf("actual: %s\n", state_str(state));
		return error_create("qed error: garbage on heap");
	}
	/* TODO: verify that `result' is of same type as f->result */
	if ((err = abstract_audit(f, state, ext))) {
	if ((err = abstract_audit(f, state))) {
		return error_prepend(err, "qed error: ");
	}
	return NULL;
}

static struct preresult *
parameterise_state(struct state *s, struct ast_function *f)
static void
declare_parameters(struct state *s, struct ast_function *f)
{
	/* declare params and locals in stack frame */
	struct ast_variable **param = ast_function_params(f);


@@ 287,7 296,11 @@ parameterise_state(struct state *s, struct ast_function *f)
			state_vconst(s, ast_variable_type(p), dynamic_str(name), true)
		);
	}
}

static struct preresult *
install_props(struct state *s, struct ast_function *f)
{
	struct ast_block *abs = ast_function_abstract(f);
	int nstmts = ast_block_nstmts(abs);
	struct ast_stmt **stmt = ast_block_stmts(abs);


@@ 297,48 310,212 @@ parameterise_state(struct state *s, struct ast_function *f)
			return r;
		}
	}

	return preresult_empty_create();
}

static struct error *
path_absverify(struct ast_function *, struct state *state, int index,
		struct state *actual_state);

static struct error *
abstract_audit(struct ast_function *f, struct state *actual_state,
		struct externals *ext)
{
	if (!state_hasgarbage(actual_state)) {
		printf("actual: %s\n", state_str(actual_state));
		return error_create("garbage on heap");
	}
abstract_auditwithstate(struct ast_function *f, struct state *alleged_state,
		struct state *actual_state);

static struct error *
abstract_audit(struct ast_function *f, struct state *actual_state)
{
	struct state *alleged_state = state_create(
		dynamic_str(ast_function_name(f)), ext, ast_function_type(f)
		dynamic_str(ast_function_name(f)),
		state_getext(actual_state),
		ast_function_type(f)
	);
	struct preresult *r = parameterise_state(alleged_state, f);
	assert(preresult_isempty(r));
	declare_parameters(alleged_state, f);
	struct error *err = abstract_auditwithstate(
		f, alleged_state, actual_state
	);
	state_destroy(alleged_state); /* actual_state handled by caller */ 
	return err;
}

static struct error *
abstract_auditwithstate(struct ast_function *f, struct state *alleged_state,
		struct state *actual_state)
{
	struct preresult *r = install_props(alleged_state, f);
	if (preresult_iscontradiction(r)) {
		return NULL;
	}

	int ndecls = ast_block_ndecls(f->abstract);
	if (ndecls) {
		struct ast_variable **var = ast_block_decls(f->abstract);
		for (int i = 0; i < ndecls; i++) {
			state_declare(alleged_state, var[i], false);
		}
	}

	return path_absverify(f, alleged_state, 0, actual_state);
}

static struct ast_function_arr *
body_paths(struct ast_function *f, int index, struct ast_expr *);

static struct error *
split_path_verify(struct ast_function *f, struct state *state, int index,
		struct ast_expr *cond);

	/* mutates alleged_state */
	struct result *res = ast_function_absexec(f, alleged_state);
	if (result_iserror(res)) {
		return result_as_error(res);
static struct error *
split_paths_verify(struct ast_function *f, struct state *state, int index,
		struct ast_stmt_splits *splits)
{
	struct error *err;
	for (int i = 0; i < splits->n; i++) {
		err = split_path_verify(f, state, index, splits->cond[i]);
		if (err) {
			return err;
		}
	}
	return NULL;
}

static struct error *
split_path_verify(struct ast_function *f, struct state *state, int index,
		struct ast_expr *cond)
{
	struct error *err = NULL;

	struct ast_function_arr *paths = body_paths(f, index, cond);
	int n = ast_function_arr_len(paths);
	assert(n == 2);
	struct ast_function **func = ast_function_arr_func(paths);
	for (int i = 0; i < n; i++) {
		struct state *s_copy = state_copywithname(
			state, ast_function_name(func[i])
		);
		struct preresult *r = ast_expr_assume(
			ast_expr_inverted_copy(cond, i==1), s_copy
		);
		if (preresult_iserror(r)) {
			return preresult_as_error(r);
		}
		if (!preresult_iscontradiction(r)) {
			/* only run if no contradiction because "ex falso" */
			if ((err = path_verify(func[i], s_copy, index))) {
				return err;
			}
		}
		/*state_destroy(s_copy);*/
	}
	return NULL;
}

static struct error *
split_paths_absverify(struct ast_function *f, struct state *alleged_state,
		int index, struct ast_stmt_splits *splits, struct state *actual_state);

static struct error *
path_absverify(struct ast_function *f, struct state *alleged_state, int index,
		struct state *actual_state)
{
	int nstmts = ast_block_nstmts(f->abstract);
	struct ast_stmt **stmt = ast_block_stmts(f->abstract);
	for (int i = index; i < nstmts; i++) {
		struct ast_stmt_splits splits = ast_stmt_splits(
			stmt[i], alleged_state
		);
		if (splits.n) {
			return split_paths_absverify(
				f, alleged_state, i, &splits, actual_state
			);
		}
		struct result *res = ast_stmt_absexec(stmt[i], alleged_state);
		if (result_iserror(res)) {
			return result_as_error(res);
		}
		result_destroy(res);
	}

	bool equiv = state_equal(actual_state, alleged_state);
	if (!equiv) {
		/* XXX: print states */
		printf("actual: %s\n", state_str(actual_state));
		printf("alleged: %s\n", state_str(alleged_state));
		return error_create("actual and alleged states differ");
	}

	state_destroy(alleged_state); /* actual_state handled by caller */ 
	return NULL;
}

static struct ast_function_arr *
abstract_paths(struct ast_function *f, int index, struct ast_expr *cond);

static struct error *
split_path_absverify(struct ast_function *f, struct state *alleged_state,
		int index, struct ast_expr *cond, struct state *actual_state);

static struct error *
split_paths_absverify(struct ast_function *f, struct state *alleged_state,
		int index, struct ast_stmt_splits *splits, struct state *actual_state)
{
	struct error *err;
	for (int i = 0; i < splits->n; i++) {
		err = split_path_absverify(
			f, alleged_state, index, splits->cond[i], actual_state
		);
		if (err) {
			return err;
		}
	}
	return NULL;
}

static struct error *
split_path_absverify(struct ast_function *f, struct state *alleged_state,
		int index, struct ast_expr *cond, struct state *actual_state)
{
	struct error *err = NULL;

	/* create two functions with abstracts and bodies
	 * adjusted accordingly */
	struct ast_function_arr *paths = abstract_paths(f, index, cond);
	int n = ast_function_arr_len(paths);
	assert(n == 2);
	struct ast_function **func = ast_function_arr_func(paths);
	for (int i = 0; i < n; i++) {
		struct state *alleged_copy = state_copywithname(
			alleged_state, ast_function_name(func[i])
		);
		struct state *actual_copy = state_copywithname(
			actual_state, ast_function_name(func[i])
		);
		struct preresult *r = ast_expr_assume(
			/* XXX */
			ast_expr_inverted_copy(cond, i==1), alleged_copy
		);
		if (preresult_iserror(r)) {
			return preresult_as_error(r);
		}
		if (!preresult_iscontradiction(r)) {
			/* only run if no contradiction because "ex falso" */
			if ((err = path_absverify(func[i], alleged_copy, index, actual_copy))) {
				return err;
			}
		}
		/*state_destroy(actual_copy);*/
		/*state_destroy(alleged_copy);*/
	}
	return NULL;
}

struct result *
ast_function_absexec(struct ast_function *f, struct state *state)
{
	int ndecls = ast_block_ndecls(f->abstract);
	if (ndecls) {
		struct ast_variable **var = ast_block_decls(f->abstract);
		for (int i = 0; i < ndecls; i++) {
			state_declare(state, var[i], false);
		}
	}

	int nstmts = ast_block_nstmts(f->abstract);
	struct ast_stmt **stmt = ast_block_stmts(f->abstract);
	for (int i = 0; i < nstmts; i++) {


@@ 426,5 603,110 @@ recurse_buildgraph(struct map *g, struct map *dedup, char *fname, struct externa
	map_set(g, dynamic_str(fname), val);
}

static char *
split_name(char *name, struct ast_expr *assumption);

static struct ast_block *
block_withassumption(struct ast_block *old, struct ast_expr *cond);

static struct ast_function_arr *
abstract_paths(struct ast_function *f, int index, struct ast_expr *cond)
{
	struct ast_function_arr *res = ast_function_arr_create();
	
	struct ast_function *f_true = ast_function_create(
		f->isaxiom,
		ast_type_copy(f->ret),
		split_name(f->name, cond),
		f->nparam,
		ast_variables_copy(f->nparam, f->param),
		block_withassumption(f->abstract, ast_expr_copy(cond)),
		ast_block_copy(f->body)
	);

	struct ast_expr *inv_assumption = ast_expr_inverted_copy(cond, true);
	struct ast_function *f_false = ast_function_create(
		f->isaxiom,
		ast_type_copy(f->ret),
		split_name(f->name, inv_assumption),
		f->nparam,
		ast_variables_copy(f->nparam, f->param),
		block_withassumption(f->abstract, inv_assumption),
		ast_block_copy(f->body)
	);
	
	ast_function_arr_append(res, f_true);
	ast_function_arr_append(res, f_false);
	return res;
}

static struct ast_function_arr *
body_paths(struct ast_function *f, int index, struct ast_expr *cond)
{
	struct ast_function_arr *res = ast_function_arr_create();
	
	struct ast_function *f_true = ast_function_create(
		f->isaxiom,
		ast_type_copy(f->ret),
		split_name(f->name, cond),
		f->nparam,
		ast_variables_copy(f->nparam, f->param),
		block_withassumption(f->abstract, ast_expr_copy(cond)),
		f->body
	);

	struct ast_expr *inv_assumption = ast_expr_inverted_copy(cond, true);
	struct ast_function *f_false = ast_function_create(
		f->isaxiom,
		ast_type_copy(f->ret),
		split_name(f->name, inv_assumption),
		f->nparam,
		ast_variables_copy(f->nparam, f->param),
		block_withassumption(f->abstract, inv_assumption),
		f->body
	);
	
	ast_function_arr_append(res, f_true);
	ast_function_arr_append(res, f_false);
	return res;
}

static struct ast_block *
block_withassumption(struct ast_block *old, struct ast_expr *cond)
{
	int ndecl = ast_block_ndecls(old);
	struct ast_variable **old_decl = ast_block_decls(old);
	struct ast_variable **decl = malloc(sizeof(struct ast_variable *) * ndecl); 
	for (int i = 0; i < ndecl; i++) {
		decl[i] = ast_variable_copy(old_decl[i]);
	}

	int old_nstmt = ast_block_nstmts(old);
	struct ast_stmt **old_stmt = ast_block_stmts(old);
	int nstmt = old_nstmt+1;
	struct ast_stmt **stmt = malloc(sizeof(struct ast_stmt *) * nstmt);
	for (int i = 0; i < old_nstmt; i++) {
		stmt[i+1] = ast_stmt_copy(old_stmt[i]);
	}

	/* assume: cond; */
	stmt[0] = ast_stmt_create_labelled(
		NULL, dynamic_str("assume"), ast_stmt_create_expr(NULL, cond)
	);

	struct ast_block *new = ast_block_create(decl, ndecl, stmt, nstmt);
	return new;
}


static char *
split_name(char *name, struct ast_expr *assumption)
{
	struct strbuilder *b = strbuilder_create();
	char *assumption_str = ast_expr_str(assumption);
	strbuilder_printf(b, "%s | %s", name, assumption_str);
	free(assumption_str);
	return strbuilder_build(b);
}

#include "arr.c"
#include "paths.c"

D src/0v/ast/function/paths.c => src/0v/ast/function/paths.c +0 -249
@@ 1,249 0,0 @@
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>

#include "ast.h"
#include "function.h"
#include "util.h"

static struct ast_function_arr *
abstract_paths(struct ast_function *f);

static struct ast_function_arr *
body_paths(struct ast_function *f);

struct ast_function_arr *
paths_fromfunction(struct ast_function *f)
{
	struct ast_function_arr *arr = ast_function_arr_create();

	struct ast_function_arr *abs_paths = abstract_paths(f);
	int abs_len = ast_function_arr_len(abs_paths);
	struct ast_function **abs_f = ast_function_arr_func(abs_paths);
	for (int i = 0; i < abs_len; i++) {
		struct ast_function_arr *body = body_paths(abs_f[i]);
		ast_function_arr_appendrange(arr, ast_function_arr_copy(body));
		ast_function_arr_destroy(body);
	}
	ast_function_arr_destroy(abs_paths);

	return arr;
}

static int
findsel(struct ast_block *b);

static struct ast_function *
abstract_immediate_split(struct ast_function *f, int i, bool enter);

static struct ast_function_arr *
abstract_paths(struct ast_function *f)
{
	struct ast_function_arr *arr = ast_function_arr_create();
	int sel = findsel(ast_function_abstract(f));
	if (sel != -1) {
		struct ast_function *t_p = abstract_immediate_split(f, sel, true),
				    *f_p = abstract_immediate_split(f, sel, false);

		struct ast_function_arr *t_paths = abstract_paths(t_p),
					*f_paths = abstract_paths(f_p);

		ast_function_arr_appendrange(arr, ast_function_arr_copy(t_paths));
		ast_function_arr_appendrange(arr, ast_function_arr_copy(f_paths));

		ast_function_arr_destroy(f_paths);
		ast_function_arr_destroy(t_paths);

		ast_function_destroy(f_p);
		ast_function_destroy(t_p);

	} else {
		ast_function_arr_append(arr, ast_function_copy(f));
	}
	return arr;
}

static struct ast_function *
immediate_split(struct ast_function *f, int i, bool enter);

static struct ast_function_arr *
body_paths(struct ast_function *f)
{
	struct ast_function_arr *arr = ast_function_arr_create();

	int sel = findsel(ast_function_body(f));
	if (sel != -1) {
		struct ast_function *t_p = immediate_split(f, sel, true),
				    *f_p = immediate_split(f, sel, false);

		struct ast_function_arr *t_paths = body_paths(t_p),
					*f_paths = body_paths(f_p);

		ast_function_arr_appendrange(arr, ast_function_arr_copy(t_paths));
		ast_function_arr_appendrange(arr, ast_function_arr_copy(f_paths));

		ast_function_arr_destroy(f_paths);
		ast_function_arr_destroy(t_paths);

		ast_function_destroy(f_p);
		ast_function_destroy(t_p);
	} else {
		ast_function_arr_append(arr, ast_function_copy(f));
	}

	return arr;
}

static int
findsel(struct ast_block *b)
{
	struct ast_stmt **stmt = ast_block_stmts(b);
	int nstmts = ast_block_nstmts(b);
	for (int i = 0; i < nstmts; i++) {
		if (ast_stmt_isselection(stmt[i])) {
			return i;
		}
	}
	return -1;
}

static char *
split_name(char *name, struct ast_expr *assumption);

static struct ast_block *
block_withassumption(struct ast_block *b, struct ast_expr *assumption);

static struct ast_block *
split_block_index(struct ast_block *b, int split_index, bool enter);

static struct ast_function *
abstract_immediate_split(struct ast_function *f, int split_index, bool enter)
{
	struct ast_block *abs = ast_function_abstract(f),
			 *body = ast_function_body(f);

	int nparam = ast_function_nparams(f);
	struct ast_variable **params = ast_function_params(f);

	/* TODO: check that cond is accessible in both abstract and body */
	struct ast_expr *assumption = ast_expr_inverted_copy(
		ast_stmt_sel_cond(ast_block_stmts(abs)[split_index]), !enter
	);

	return ast_function_create(
		false,
		ast_type_copy(ast_function_type(f)),
		split_name(ast_function_name(f), assumption),
		ast_function_nparams(f),
		ast_variables_copy(nparam, params),
		block_withassumption(
			split_block_index(abs, split_index, enter),
			assumption
		),
		ast_block_copy(body)
	);
}

static struct ast_function *
immediate_split(struct ast_function *f, int split_index, bool enter)
{
	struct ast_block *abs = ast_function_abstract(f),
			 *body = ast_function_body(f);

	int nparam = ast_function_nparams(f);
	struct ast_variable **params = ast_function_params(f);

	/* TODO: check that cond is accessible in both abstract and body */
	struct ast_expr *assumption = ast_expr_inverted_copy(
		ast_stmt_sel_cond(ast_block_stmts(body)[split_index]), !enter
	);

	return ast_function_create(
		false,
		ast_type_copy(ast_function_type(f)),
		split_name(ast_function_name(f), assumption),
		ast_function_nparams(f),
		ast_variables_copy(nparam, params),
		block_withassumption(abs, assumption),
		split_block_index(body, split_index, enter)
	);
}

static char *
split_name(char *name, struct ast_expr *assumption)
{
	struct strbuilder *b = strbuilder_create();
	char *assumption_str = ast_expr_str(assumption);
	strbuilder_printf(b, "%s | %s", name, assumption_str);
	free(assumption_str);
	return strbuilder_build(b);
}


static struct ast_block *
block_withassumption(struct ast_block *old, struct ast_expr *cond)
{
	int ndecl = ast_block_ndecls(old);
	struct ast_variable **old_decl = ast_block_decls(old);
	struct ast_variable **decl = malloc(sizeof(struct ast_variable *) * ndecl); 
	for (int i = 0; i < ndecl; i++) {
		decl[i] = ast_variable_copy(old_decl[i]);
	}

	int old_nstmt = ast_block_nstmts(old);
	struct ast_stmt **old_stmt = ast_block_stmts(old);
	int nstmt = old_nstmt+1;
	struct ast_stmt **stmt = malloc(sizeof(struct ast_stmt *) * nstmt);
	for (int i = 0; i < old_nstmt; i++) {
		stmt[i+1] = ast_stmt_copy(old_stmt[i]);
	}
	/* assume: cond; */
	stmt[0] = ast_stmt_create_labelled(
		NULL, dynamic_str("assume"), ast_stmt_create_expr(NULL, cond)
	);

	return ast_block_create(decl, ndecl, stmt, nstmt);
}

struct ast_stmt *
choose_split_path(struct ast_stmt *stmt, bool should_split, bool enter);

static struct ast_block *
split_block_index(struct ast_block *b, int split_index, bool enter)
{
	int nstmts = ast_block_nstmts(b);
	struct ast_stmt **old_stmt = ast_block_stmts(b);

	int n = 0;
	struct ast_stmt **stmt = NULL;
	for (int i = 0; i < nstmts; i++) {
		struct ast_stmt *s = choose_split_path(
			old_stmt[i], i == split_index, enter
		);
		if (!s) {
			continue;
		}
		stmt = realloc(stmt, sizeof(struct ast_stmt *) * ++n);
		stmt[n-1] = ast_stmt_copy(s);
	}

	int ndecl = ast_block_ndecls(b);
	struct ast_variable **old_decl = ast_block_decls(b);
	struct ast_variable **decl =
		old_decl
		? ast_variables_copy(ndecl, old_decl)
		: NULL;
	return ast_block_create(
		decl, ndecl,
		stmt, n
	);
}

struct ast_stmt *
choose_split_path(struct ast_stmt *stmt, bool should_split, bool enter)
{
	if (should_split) {
		return enter ? ast_stmt_sel_body(stmt) : NULL;
	}
	return stmt;
}

M src/0v/ast/gram.y => src/0v/ast/gram.y +4 -3
@@ 196,7 196,7 @@ primary_expression
	| CONSTANT
		{ $$ = ast_expr_constant_create(parse_int(yytext)); } /* XXX */
	| CHAR_LITERAL
		{ $$ = ast_expr_constant_create(parse_char(yytext)); }
		{ $$ = ast_expr_constant_create_char(parse_char(yytext)); }
	| STRING_LITERAL
		{ $$ = ast_expr_literal_create(strip_quotes(yytext)); }
	| '(' expression ')'


@@ 893,7 893,8 @@ yyerror(char *s)
	if (verbose) {
		fprintf(stderr, "\n%*s\n", marker.column, "^");
	}
	fprintf(stderr, "%s:%d:%d: %s\n",
		marker.filename, marker.linenum, marker.column, s);
	char *mark = lexememarker_str(&marker);
	fprintf(stderr, "%s: %s\n", mark, s);
	free(mark);
	exit(EXIT_FAILURE);
}

M src/0v/ast/lex.l => src/0v/ast/lex.l +9 -2
@@ 336,8 336,7 @@ lexememarker_create(int linenum, int column, char *filename,

struct lexememarker *
lexememarker_copy(struct lexememarker *loc)
{
	return lexememarker_create(
{ return lexememarker_create(
		loc->linenum,
		loc->column,
		dynamic_str(loc->filename),


@@ 351,3 350,11 @@ lexememarker_destroy(struct lexememarker *loc)
	free(loc->filename);
	free(loc);
}

char *
lexememarker_str(struct lexememarker *loc)
{
	struct strbuilder *b = strbuilder_create();
	strbuilder_printf(b, "%s:%d:%d", loc->filename, loc->linenum, loc->column);
	return strbuilder_build(b);
}

M src/0v/ast/literals.c => src/0v/ast/literals.c +1 -1
@@ 18,7 18,7 @@ parse_int(char *s)
int
parse_escape(char c);

int
char
parse_char(char *s)
{
	/* literal must be nonempty and begin in a quote */

M src/0v/ast/literals.h => src/0v/ast/literals.h +1 -1
@@ 4,7 4,7 @@
int
parse_int(char *s);

int
char
parse_char(char *s);

#endif

M src/0v/ast/stmt/stmt.c => src/0v/ast/stmt/stmt.c +91 -7
@@ 2,11 2,16 @@
#include <stdlib.h>
#include <assert.h>
#include <string.h>

#include "ast.h"
#include "expr/expr.h"
#include "intern.h"
#include "lex.h"
#include "util.h"
#include "props.h"
#include "state.h"
#include "stmt.h"
#include "../expr/expr.h"
#include "util.h"
#include "value.h"

struct ast_stmt {
	enum ast_stmt_kind kind;


@@ 41,6 46,12 @@ struct ast_stmt {
	struct lexememarker *loc;
};

struct lexememarker *
ast_stmt_lexememarker(struct ast_stmt *stmt)
{
	return stmt->loc;
}

static struct ast_stmt *
ast_stmt_create(struct lexememarker *loc)
{


@@ 150,7 161,7 @@ static void
ast_stmt_compound_sprint(struct ast_stmt *stmt, struct strbuilder *b)
{
	assert(stmt->kind == STMT_COMPOUND || stmt->kind == STMT_COMPOUND_V);
	char *s = ast_block_str(stmt->u.compound);
	char *s = ast_block_str(stmt->u.compound, "\t");
	strbuilder_printf(b, s);
	free(s);
}


@@ 178,23 189,38 @@ ast_stmt_create_jump(struct lexememarker *loc, enum ast_jump_kind kind,
struct ast_expr *
ast_stmt_jump_rv(struct ast_stmt *stmt)
{
	assert(ast_stmt_isterminal(stmt));
	return stmt->u.jump.rv;
}

static bool
sel_isterminal(struct ast_stmt *stmt, struct state *s);

bool
ast_stmt_isterminal(struct ast_stmt *stmt)
ast_stmt_isterminal(struct ast_stmt *stmt, struct state *s)
{
	switch (stmt->kind) {
	case STMT_JUMP:
		return stmt->u.jump.kind == JUMP_RETURN;
	case STMT_COMPOUND:
		return ast_block_isterminal(stmt->u.compound);
		return ast_block_isterminal(stmt->u.compound, s);
	case STMT_SELECTION:
		return sel_isterminal(stmt, s);
	default:
		return false;
	}
}

static bool
sel_isterminal(struct ast_stmt *stmt, struct state *s)
{
	struct decision dec = sel_decide(ast_stmt_sel_cond(stmt), s);
	assert(!dec.err);
	if (dec.decision) {
		return ast_stmt_isterminal(ast_stmt_sel_body(stmt), s);
	}
	return false;
}

bool
ast_stmt_isselection(struct ast_stmt *stmt)
{


@@ 433,7 459,7 @@ ast_stmt_iter_sprint(struct ast_stmt *stmt, struct strbuilder *b)
	     *iter = ast_expr_str(stmt->u.iteration.iter);

	char *abs = stmt->u.iteration.abstract ?
		ast_block_str(stmt->u.iteration.abstract) : "";
		ast_block_str(stmt->u.iteration.abstract, "\t") : "";

	strbuilder_printf(
		b,


@@ 708,6 734,34 @@ ast_stmt_getfuncs(struct ast_stmt *stmt)
	}
}

static struct ast_stmt_splits
stmt_sel_splits(struct ast_stmt *stmt, struct state *s);

struct ast_stmt_splits
ast_stmt_splits(struct ast_stmt *stmt, struct state *s)
{
	/* TODO: consider expressions with calls */
	switch (stmt->kind) {
	case STMT_EXPR:
		return ast_expr_splits(stmt->u.expr, s);
	case STMT_SELECTION:
		return stmt_sel_splits(stmt, s);
	case STMT_JUMP:
		if (stmt->u.jump.rv) {
			return ast_expr_splits(stmt->u.jump.rv, s);
		}
		return (struct ast_stmt_splits) { .n = 0, .cond = NULL };
	case STMT_ALLOCATION:
	case STMT_LABELLED:
	case STMT_ITERATION:
	case STMT_COMPOUND_V:
		/* disallowed splits for now */
		return (struct ast_stmt_splits) { .n = 0, .cond = NULL };
	default:
		assert(false);
	}
}

static struct string_arr *
ast_stmt_expr_getfuncs(struct ast_stmt *stmt)
{


@@ 773,4 827,34 @@ ast_stmt_compound_getfuncs(struct ast_stmt *stmt)
	return res;
}

static bool
condexists(struct ast_expr *cond, struct state *);

static struct ast_stmt_splits
stmt_sel_splits(struct ast_stmt *stmt, struct state *s)
{
	struct result *res = ast_expr_pf_reduce(stmt->u.selection.cond, s);
	struct ast_expr *r = value_to_expr(result_as_value(res));
	if (condexists(r, s)) {
		return (struct ast_stmt_splits) { .n = 0, .cond = NULL };
	}
	/*printf("cond: %s\n", ast_expr_str(r));*/
	struct ast_expr **cond = malloc(sizeof(struct ast_expr *));
	cond[0] = r;
	return (struct ast_stmt_splits) {
		.n    = 1,
		.cond = cond,
	};
}

static bool
condexists(struct ast_expr *cond, struct state *s)
{
	struct result *res = ast_expr_pf_reduce(cond, s);
	assert(!result_iserror(res) && result_hasvalue(res));
	struct ast_expr *reduced = value_to_expr(result_as_value(res));
	struct props *p = state_getprops(s);
	return props_get(p, reduced) || props_contradicts(p, reduced);
}

#include "verify.c"

M src/0v/ast/stmt/stmt.h => src/0v/ast/stmt/stmt.h +15 -0
@@ 28,4 28,19 @@ ast_stmt_isassume(struct ast_stmt *stmt);
struct string_arr *
ast_stmt_getfuncs(struct ast_stmt *stmt);

struct ast_stmt_splits {
	int n;
	struct ast_expr **cond;
};

struct ast_stmt_splits
ast_stmt_splits(struct ast_stmt *, struct state *);

struct state;
struct error;

/* TODO: change to more regular tuple */
struct decision { bool decision; struct error *err; }
sel_decide(struct ast_expr *control, struct state *state);

#endif

M src/0v/ast/stmt/verify.c => src/0v/ast/stmt/verify.c +83 -28
@@ 3,6 3,7 @@
#include <assert.h>
#include <string.h>
#include "ast.h"
#include "lex.h"
#include "intern.h"
#include "props.h"
#include "object.h"


@@ 18,11 19,23 @@ ast_stmt_process(struct ast_stmt *stmt, struct state *state)

	if (ast_stmt_kind(stmt) == STMT_COMPOUND_V) {
		if ((err = ast_stmt_verify(stmt, state))) {
			return error_prepend(err, "cannot verify statement: ");
			struct strbuilder *b = strbuilder_create();
			struct lexememarker *loc = ast_stmt_lexememarker(stmt); 
			assert(loc);
			char *m = lexememarker_str(loc);
			strbuilder_printf(b, "%s: %s", m, err->msg);
			free(m);
			return error_create(strbuilder_build(b));
		}
	}
	if ((err = ast_stmt_exec(stmt, state))) {
		return error_prepend(err, "cannot exec statement: ");
		struct strbuilder *b = strbuilder_create();
		struct lexememarker *loc = ast_stmt_lexememarker(stmt); 
		assert(loc);
		char *m = lexememarker_str(loc);
		strbuilder_printf(b, "%s: cannot exec statement: %s", m, err->msg);
		free(m);
		return error_create(strbuilder_build(b));
	}
	return NULL;
}


@@ 74,7 87,6 @@ ast_stmt_verify(struct ast_stmt *stmt, struct state *state)
	case STMT_ITERATION:
		return stmt_iter_verify(stmt, state);
	default:
		fprintf(stderr, "cannot verify stmt: %s\n", ast_stmt_str(stmt));
		assert(false);
	}
}


@@ 104,7 116,7 @@ stmt_expr_verify(struct ast_stmt *stmt, struct state *state)
	if (ast_expr_decide(expr, state)) {
		return NULL;
	}
	return error_create("cannot verify");
	return error_create("cannot verify statement");
}

static bool


@@ 152,6 164,9 @@ static struct error *
stmt_compound_exec(struct ast_stmt *stmt, struct state *state);

static struct error *
stmt_sel_exec(struct ast_stmt *stmt, struct state *state);

static struct error *
stmt_iter_exec(struct ast_stmt *stmt, struct state *state);

static struct error *


@@ 169,6 184,8 @@ ast_stmt_exec(struct ast_stmt *stmt, struct state *state)
		return NULL;
	case STMT_EXPR:
		return ast_expr_exec(ast_stmt_as_expr(stmt), state);
	case STMT_SELECTION:
		return stmt_sel_exec(stmt, state);
	case STMT_ITERATION:
		return stmt_iter_exec(stmt, state);
	case STMT_JUMP:


@@ 192,13 209,29 @@ stmt_compound_exec(struct ast_stmt *stmt, struct state *state)
		if (err) {
			return err;
		}
		if (ast_stmt_isterminal(stmts[i])) {
		if (ast_stmt_isterminal(stmts[i], state)) {
			break;
		}
	}
	return NULL;
}

/* stmt_sel_exec */

static struct error *
stmt_sel_exec(struct ast_stmt *stmt, struct state *state)
{
	struct decision dec = sel_decide(ast_stmt_sel_cond(stmt), state);
	if (dec.err) {
		return dec.err;
	}
	if (dec.decision) {
		return ast_stmt_exec(ast_stmt_sel_body(stmt), state);
	}
	assert(!ast_stmt_sel_nest(stmt));
	return NULL;
}

/* stmt_expr_eval */

static struct ast_stmt *


@@ 381,45 414,67 @@ hack_base_object_from_alloc(struct ast_stmt *alloc, struct state *state)
	return obj;
}

static bool
sel_decide(struct ast_expr *control, struct state *state);

static struct result *
sel_absexec(struct ast_stmt *stmt, struct state *state)
{
	if (sel_decide(ast_stmt_sel_cond(stmt), state)) {
	struct decision dec = sel_decide(ast_stmt_sel_cond(stmt), state);
	if (dec.err) {
		return result_error_create(dec.err);
	}
	if (dec.decision) {
		return ast_stmt_absexec(ast_stmt_sel_body(stmt), state);
	}
	assert(!ast_stmt_sel_nest(stmt));
	return result_value_create(NULL);
}

static struct value *
underlying_value(struct value *v, struct state *state);

static bool
struct decision
sel_decide(struct ast_expr *control, struct state *state)
{
	struct result *res = ast_expr_eval(control, state);
	assert(!result_iserror(res)); /* TODO: process error */
	/*printf("(sel_decide) state: %s\n", state_str(state));*/
	/*printf("(sel_decide) control: %s\n", ast_expr_str(control));*/
	struct result *res = ast_expr_pf_reduce(control, state);
	if (result_iserror(res)) {
		return (struct decision) { .err = result_as_error(res) };
	}
	assert(result_hasvalue(res)); /* TODO: user error */

	struct value *v = result_as_value(res);
	/*printf("(sel_decide) value: %s\n", value_str(v));*/
	if (value_issync(v)) {
		struct ast_expr *sync = value_as_sync(v);
		/*printf("state: %s\n", state_str(state));*/
		/*printf("sync: %s\n", ast_expr_str(sync));*/
		struct props *p = state_getprops(state);
		if (props_get(p, sync)) {
			return (struct decision) { .decision = true, .err = NULL };
		} else if (props_contradicts(p, sync)) {
			return (struct decision) { .decision = false, .err = NULL };
		}

	}

	struct value *zero = value_int_create(0);
	bool nonzero = !value_equal(
		zero, underlying_value(result_as_value(res), state)
	);
	value_destroy(zero);
	return nonzero;
}

static struct value *
underlying_value(struct value *v, struct state *state)
{
	if (value_issync(v)) {
		return state_getvconst(
			state, ast_expr_as_identifier(value_as_sync(v))
	if (!values_comparable(zero, v)) {
		struct strbuilder *b = strbuilder_create();
		char *c_str = ast_expr_str(control);
		char *v_str = value_str(v);
		strbuilder_printf(
			b, "`%s' with value `%s' is undecidable",
			c_str, v_str
		);
		free(v_str);
		free(c_str);
		return (struct decision) {
			.decision = false,
			.err      = error_create(strbuilder_build(b)),
		};
	}
	return v;

	bool nonzero = !value_equal(zero, v);
	value_destroy(zero);
	return (struct decision) { .decision = nonzero, .err = NULL };
}

static struct result *

M src/0v/ast/type/type.c => src/0v/ast/type/type.c +16 -2
@@ 4,6 4,7 @@
#include <string.h>
#include "ast.h"
#include "ext.h"
#include "state.h"
#include "type.h"
#include "util.h"
#include "value.h"


@@ 78,7 79,7 @@ ast_type_create_userdef(char *name)
}

struct value *
ast_type_vconst(struct ast_type *t, struct externals *ext)
ast_type_vconst(struct ast_type *t, struct state *s, char *comment, bool persist)
{
	switch (t->base) {
	case TYPE_INT:


@@ 88,8 89,10 @@ ast_type_vconst(struct ast_type *t, struct externals *ext)
		return value_ptr_indefinite_create();
	case TYPE_USERDEF:
		return ast_type_vconst(
			externals_gettypedef(ext, t->userdef), ext
			externals_gettypedef(state_getext(s), t->userdef), s, comment, persist
		);
	case TYPE_STRUCT:
		return value_struct_indefinite_create(t, s, comment, persist);
	default:
		assert(false);
	}


@@ 102,6 105,17 @@ ast_type_isstruct(struct ast_type *t)
	return t->base == TYPE_STRUCT;
}

struct ast_type *
ast_type_struct_complete(struct ast_type *t, struct externals *ext)
{
	if (ast_type_struct_members(t)) {
		return t;
	}
	char *tag = ast_type_struct_tag(t);
	assert(tag);
	return externals_getstruct(ext, tag);
}

struct ast_variable_arr *
ast_type_struct_members(struct ast_type *t)
{

M src/0v/main.c => src/0v/main.c +5 -2
@@ 179,10 179,13 @@ pass1(struct ast *root, struct externals *ext)
		}
		/* XXX: ensure that verified functions always have an abstract */
		assert(ast_function_abstract(f));

		printf("%s...\n", ast_function_name(f));
		if ((err = ast_function_verify(f, ext))) {
			fprintf(stderr, "%s", err->msg);
			fprintf(stderr, "%s\n", err->msg);
			exit(EXIT_FAILURE);
		}
		printf("done %s\n", ast_function_name(f));
	}
}



@@ 234,7 237,7 @@ proto_defisvalid(struct ast_function *proto, struct ast_function *def)
	struct ast_block *proto_abs = ast_function_abstract(proto),
			 *def_abs = ast_function_abstract(def);

	bool abs_match = strcmp(ast_block_str(proto_abs), ast_block_str(def_abs)) == 0,
	bool abs_match = strcmp(ast_block_str(proto_abs, ""), ast_block_str(def_abs, "")) == 0,
	     protoabs_only = proto_abs && ast_function_absisempty(def); 
	if (abs_match || protoabs_only) {
		return true;

M src/0v/object/object.c => src/0v/object/object.c +4 -18
@@ 181,7 181,7 @@ object_isdeallocand(struct object *obj, struct state *s)
{
	switch (obj->type) {
	case OBJECT_VALUE:
		return obj->value && state_isdeallocand(s, value_as_ptr(obj->value));
		return obj->value && state_isdeallocand(s, value_as_location(obj->value));
	case OBJECT_DEALLOCAND_RANGE:
		return range_isdeallocand(obj->range, s);
	default:


@@ 361,7 361,7 @@ object_upto(struct object *obj, struct ast_expr *excl_up, struct state *s)
		ast_expr_copy(obj->offset),
		range_create(
			ast_expr_difference_create(excl_up, lw),
			value_as_ptr(state_alloc(s))
			value_as_location(state_alloc(s))
		)
	);
}


@@ 405,7 405,7 @@ object_from(struct object *obj, struct ast_expr *incl_lw, struct state *s)
				up,
				ast_expr_copy(incl_lw)
			),
			value_as_ptr(state_alloc(s))
			value_as_location(state_alloc(s))
		)
	);
}


@@ 434,9 434,6 @@ object_getmember(struct object *obj, struct ast_type *t, char *member,
	return value_struct_member(getorcreatestruct(obj, t, s), member);
}

static struct ast_type *
usecomplete(struct ast_type *, struct state *);

static struct value *
getorcreatestruct(struct object *obj, struct ast_type *t, struct state *s)
{


@@ 444,24 441,13 @@ getorcreatestruct(struct object *obj, struct ast_type *t, struct state *s)
	if (v) {
		return v;
	}
	struct ast_type *complete = usecomplete(t, s);
	struct ast_type *complete = ast_type_struct_complete(t, state_getext(s));
	assert(complete);
	v = value_struct_create(complete);
	object_assign(obj, v);
	return v;
}

static struct ast_type *
usecomplete(struct ast_type *t, struct state *s)
{
	if (ast_type_struct_members(t)) {
		return t;
	}
	char *tag = ast_type_struct_tag(t);
	assert(tag);
	return externals_getstruct(state_getext(s), tag);
}

struct ast_type *
object_getmembertype(struct object *obj, struct ast_type *t, char *member,
		struct state *s)

M src/0v/state/heap.c => src/0v/state/heap.c +32 -3
@@ 236,14 236,15 @@ vconst_copy(struct vconst *old)
	return new;
}

static char *
vconst_id(struct map *varmap, struct map *persistmap, bool persist);

char *
vconst_declare(struct vconst *v, struct value *val, char *comment, bool persist)
{
	struct map *m = v->varmap;

	struct strbuilder *b = strbuilder_create();
	strbuilder_printf(b, "$%d", (int) m->n);
	char *s = strbuilder_build(b);
	char *s = vconst_id(m, v->persist, persist);

	map_set(m, dynamic_str(s), val);
	if (comment) {


@@ 254,6 255,34 @@ vconst_declare(struct vconst *v, struct value *val, char *comment, bool persist)
	return s;
}

static int
count_true(struct map *m);

static char *
vconst_id(struct map *varmap, struct map *persistmap, bool persist)
{
	int npersist = count_true(persistmap);
	struct strbuilder *b = strbuilder_create();
	if (persist) {
		strbuilder_printf(b, "$%d", (int) npersist);
	} else {
		strbuilder_printf(b, "#%d", (int) varmap->n - npersist);
	}
	return strbuilder_build(b);
}

static int
count_true(struct map *m)
{
	int n = 0;
	for (int i = 0; i < m->n; i++) {
		if (m->entry[i].value) {
			n++;
		}
	}
	return n;
}

struct value *
vconst_get(struct vconst *v, char *id)
{

M src/0v/state/stack.c => src/0v/state/stack.c +9 -0
@@ 89,6 89,15 @@ stack_copy(struct stack *stack)
	return copy;
}

struct stack *
stack_copywithname(struct stack *stack, char *new_name)
{
	struct stack *copy = stack_copy(stack);
	free(copy->name);
	copy->name = new_name;
	return copy;
}

static struct map *
varmap_copy(struct map *m)
{

M src/0v/state/stack.h => src/0v/state/stack.h +3 -0
@@ 18,6 18,9 @@ stack_destroy(struct stack *);
struct stack *
stack_copy(struct stack *);

struct stack *
stack_copywithname(struct stack *, char *new_name);

char *
stack_str(struct stack *, struct state *);


M src/0v/state/state.c => src/0v/state/state.c +49 -9
@@ 50,7 50,7 @@ struct state *
state_copy(struct state *state)
{
	struct state *copy = malloc(sizeof(struct state));
	assert(state);
	assert(copy);
	copy->ext = state->ext;
	copy->vconst = vconst_copy(state->vconst);
	copy->stack = stack_copy(state->stack);


@@ 59,6 59,19 @@ state_copy(struct state *state)
	return copy;
}

struct state *
state_copywithname(struct state *state, char *func_name)
{
	struct state *copy = malloc(sizeof(struct state));
	assert(copy);
	copy->ext = state->ext;
	copy->vconst = vconst_copy(state->vconst);
	copy->stack = stack_copywithname(state->stack, func_name);
	copy->heap = heap_copy(state->heap);
	copy->props = props_copy(state->props);
	return copy;
}

char *
state_str(struct state *state)
{


@@ 128,8 141,12 @@ state_declare(struct state *state, struct ast_variable *var, bool isparam)
struct value *
state_vconst(struct state *state, struct ast_type *t, char *comment, bool persist)
{
	struct value *v = ast_type_vconst(t, state, comment, persist);
	if (value_isstruct(v)) {
		return v;
	}
	char *c = vconst_declare(
		state->vconst, ast_type_vconst(t, state_getext(state)),
		state->vconst, v,
		comment, persist
	);
	return value_sync_create(ast_expr_identifier_create(c));


@@ 201,7 218,11 @@ state_getobject(struct state *state, char *id)
	}

	struct variable *v = stack_getvariable(state->stack, id);
	assert(v);
	if (!v) {
		printf("state: %s\n", state_str(state));
		printf("id: %s\n", id);
		assert(false);
	}

	return state_get(state, variable_location(v), true);
}


@@ 210,7 231,7 @@ state_getobject(struct state *state, char *id)
struct object *
state_deref(struct state *state, struct value *ptr_val, struct ast_expr *index)
{
	struct location *deref_base = value_as_ptr(ptr_val);
	struct location *deref_base = value_as_location(ptr_val);
	assert(deref_base);

	/* `*(ptr+offset)` */


@@ 231,7 252,7 @@ state_range_alloc(struct state *state, struct object *obj,
	}

	/* assume pointer */
	struct location *deref = value_as_ptr(arr_val);
	struct location *deref = value_as_location(arr_val);

	struct block *b = location_getblock(
		deref, state->vconst, state->stack, state->heap


@@ 256,7 277,10 @@ state_alloc(struct state *state)
struct error *
state_dealloc(struct state *state, struct value *val)
{
	return location_dealloc(value_as_ptr(val), state->heap);
	if (!value_islocation(val)) {
		return error_create("dealloc on non-location");
	}
	return location_dealloc(value_as_location(val), state->heap);
}




@@ 269,7 293,7 @@ state_range_dealloc(struct state *state, struct object *obj,
	if (!arr_val) {
		return error_create("no value");
	}
	struct location *deref = value_as_ptr(arr_val);
	struct location *deref = value_as_location(arr_val);
	return location_range_dealloc(deref, lw, up, state);
}



@@ 277,7 301,7 @@ bool
state_addresses_deallocand(struct state *state, struct object *obj)
{
	struct value *val = object_as_value(obj);
	struct location *loc = value_as_ptr(val); 
	struct location *loc = value_as_location(val); 
	
	return state_isdeallocand(state, loc);
}


@@ 303,7 327,7 @@ state_range_aredeallocands(struct state *state, struct object *obj,
	if (!arr_val) {
		return false;
	}
	struct location *deref = value_as_ptr(arr_val);
	struct location *deref = value_as_location(arr_val);
	
	struct block *b = location_getblock(
		deref, state->vconst, state->stack, state->heap


@@ 338,6 362,9 @@ state_eval(struct state *s, struct ast_expr *e)
static void
state_undeclarevars(struct state *s);

static void
state_popprops(struct state *s);

bool
state_equal(struct state *s1, struct state *s2)
{


@@ 345,10 372,16 @@ state_equal(struct state *s1, struct state *s2)
		     *s2_c = state_copy(s2);
	state_undeclarevars(s1_c);
	state_undeclarevars(s2_c);
	state_popprops(s1_c);
	state_popprops(s2_c);

	char *str1 = state_str(s1_c),
	     *str2 = state_str(s2_c);
	bool equal = strcmp(str1, str2) == 0;
	if (!equal) {
		printf("actual: %s\n", str1);
		printf("alleged: %s\n", str2);
	}
	free(str2);
	free(str1);



@@ 365,3 398,10 @@ state_undeclarevars(struct state *s)
	vconst_undeclare(s->vconst);
	stack_undeclare(s->stack, s);
}

static void
state_popprops(struct state *s)
{
	/* XXX: */
	s->props = props_create();
}

M src/0v/state/test.c => src/0v/state/test.c +1 -1
@@ 116,7 116,7 @@ test_value_ptr()
	}
	free(s);

	if (value_as_ptr(val) != loc) {
	if (value_as_location(val) != loc) {
		return false;
	}


M src/0v/value/value.c => src/0v/value/value.c +144 -32
@@ 170,7 170,7 @@ value_int_up(struct value *v)


struct number *
number_sync_create(struct ast_expr *);
number_computed_create(struct ast_expr *);

struct value *
value_sync_create(struct ast_expr *e)


@@ 178,7 178,7 @@ value_sync_create(struct ast_expr *e)
	struct value *v = malloc(sizeof(struct value));
	assert(v);
	v->type = VALUE_SYNC;
	v->n = number_sync_create(e);
	v->n = number_computed_create(e);
	return v;
}



@@ 226,6 226,78 @@ value_struct_create(struct ast_type *t)
	return v;
}

struct value *
value_struct_indefinite_create(struct ast_type *t, struct state *s,
		char *comment, bool persist)
{
	t = ast_type_struct_complete(t, state_getext(s));
	assert(ast_type_struct_members(t));

	struct value *v = value_struct_create(t);

	int n = ast_variable_arr_n(v->_struct.members);
	struct ast_variable **var = ast_variable_arr_v(v->_struct.members);
	for (int i = 0; i < n; i++) {
		char *field = ast_variable_name(var[i]);
		struct object *obj = map_get(v->_struct.m, field);
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(b, "%s.%s", comment, field);
		object_assign(
			obj,
			state_vconst(
				s,
				ast_variable_type(var[i]),
				strbuilder_build(b), /* comment */
				persist
			)
		);
	}

	return v;
}

struct value *
value_pf_augment(struct value *old, struct ast_expr *root)
{
	assert(value_isstruct(old));

	struct value *v = value_copy(old);

	int n = ast_variable_arr_n(v->_struct.members);
	struct ast_variable **var = ast_variable_arr_v(v->_struct.members);
	for (int i = 0; i < n; i++) {
		char *field = ast_variable_name(var[i]);
		struct object *obj = map_get(v->_struct.m, field);
		struct value *obj_value = object_as_value(obj);
		if (!obj_value) {
			continue;
		}
		if (!value_issync(obj_value)) {
			continue;
		}
		object_assign(
			obj,
			value_sync_create(
				ast_expr_member_create(
					ast_expr_copy(root), dynamic_str(field)
				)
			)
		);
	}
	/*printf("root: %s\n", ast_expr_str(root));*/
	/*printf("old: %s\n", value_str(old));*/
	/*printf("new: %s\n", value_str(v));*/

	/*assert(false);*/
	return v;
}

bool
value_isstruct(struct value *v)
{
	return v->type == VALUE_STRUCT;
}

static struct map *
frommembers(struct ast_variable_arr *members)
{


@@ 373,7 445,7 @@ value_int_sprint(struct value *v, struct strbuilder *b)
void
value_sync_sprint(struct value *v, struct strbuilder *b)
{
	strbuilder_printf(b, "sync:%s", number_str(v->n));
	strbuilder_printf(b, "comp:%s", number_str(v->n));
}

struct value *


@@ 470,10 542,16 @@ value_str(struct value *v)
	return strbuilder_build(b);
}

bool
value_islocation(struct value *v)
{
	return v->type == VALUE_PTR && !v->ptr.isindefinite;
}

struct location *
value_as_ptr(struct value *v)
value_as_location(struct value *v)
{
	assert(v->type == VALUE_PTR && !v->ptr.isindefinite);
	assert(value_islocation(v));
	return v->ptr.loc;
}



@@ 545,14 623,36 @@ struct ast_expr *
value_to_expr(struct value *v)
{
	switch (v->type) {
	case VALUE_PTR:
		return ast_expr_identifier_create(value_str(v));
	case VALUE_LITERAL:
		return ast_expr_copy(value_as_literal(v));
	case VALUE_SYNC:
		return ast_expr_copy(value_as_sync(v));
	case VALUE_INT:
		return number_to_expr(v->n);
	default:
		/*printf("v: %s\n", value_str(v));*/
		assert(false);
	}
}

bool
value_isliteral(struct value *v)
{
	if (v->type != VALUE_LITERAL) {
		return false;
	}
	return true;
}

struct ast_expr *
value_as_literal(struct value *v)
{
	assert(v->type == VALUE_LITERAL);
	return ast_expr_literal_create(v->s);
}

enum value_type
value_type(struct value *v)
{


@@ 594,13 694,23 @@ struct_references(struct value *v, struct location *loc, struct state *s)
bool
number_equal(struct number *n1, struct number *n2);


bool
values_comparable(struct value *v1, struct value *v2)
{
	return v1->type == v2->type;
}

bool
value_equal(struct value *v1, struct value *v2)
{
	assert(v1 && v2 && v1->type == v2->type);
	assert(v1->type == v2->type);

	switch (v1->type) {
	case VALUE_LITERAL:
		return strcmp(v1->s, v2->s) == 0;
	case VALUE_INT:
	case VALUE_SYNC:
		return number_equal(v1->n, v2->n);
	default:
		assert(false);


@@ 625,10 735,10 @@ value_assume(struct value *v, bool value)
}

struct number {
	enum number_knowledge_type type;
	enum number_type type;
	union {
		struct number_range_arr *ranges;
		struct ast_expr *sync_const;
		struct ast_expr *computation;
	};
};



@@ 636,7 746,7 @@ struct number *
number_ranges_create(struct number_range_arr *ranges)
{
	struct number *num = calloc(1, sizeof(struct number));
	num->type = NUMBER_KNOWLEDGE_RANGES;
	num->type = NUMBER_RANGES;
	num->ranges = ranges;
	return num;
}


@@ 668,11 778,11 @@ number_range_arr_single_create(int val)
}

struct number *
number_sync_create(struct ast_expr *e)
number_computed_create(struct ast_expr *e)
{
	struct number *num = calloc(1, sizeof(struct number));
	num->type = NUMBER_KNOWLEDGE_SYNC_CONSTANT;
	num->sync_const = e;
	num->type = NUMBER_COMPUTED;
	num->computation = e;
	return num;
}



@@ 768,11 878,11 @@ void
number_destroy(struct number *n)
{
	switch (n->type) {
	case NUMBER_KNOWLEDGE_RANGES:
	case NUMBER_RANGES:
		number_range_arr_destroy(n->ranges);
		break;
	case NUMBER_KNOWLEDGE_SYNC_CONSTANT:
		ast_expr_destroy(n->sync_const);
	case NUMBER_COMPUTED:
		ast_expr_destroy(n->computation);
		break;
	default:
		assert(false);


@@ 786,7 896,7 @@ number_range_str(struct number_range *r);
char *
number_ranges_sprint(struct number *num)
{
	assert(num->type == NUMBER_KNOWLEDGE_RANGES);
	assert(num->type == NUMBER_RANGES);

	struct strbuilder *b = strbuilder_create();
	int n = number_range_arr_n(num->ranges);


@@ 805,10 915,10 @@ char *
number_str(struct number *num)
{
	switch (num->type) {
	case NUMBER_KNOWLEDGE_RANGES:
	case NUMBER_RANGES:
		return number_ranges_sprint(num);
	case NUMBER_KNOWLEDGE_SYNC_CONSTANT:
		return ast_expr_str(num->sync_const);
	case NUMBER_COMPUTED:
		return ast_expr_str(num->computation);
	default:
		assert(false);
	}


@@ 823,8 933,10 @@ number_equal(struct number *n1, struct number *n2)
	assert(n1->type == n2->type);

	switch (n1->type) {
	case NUMBER_KNOWLEDGE_RANGES:
	case NUMBER_RANGES:
		return number_ranges_equal(n1, n2);
	case NUMBER_COMPUTED:
		return ast_expr_equal(n1->computation, n2->computation);
	default:
		assert(false);
	}


@@ 836,7 948,7 @@ number_range_equal(struct number_range *, struct number_range *);
bool
number_ranges_equal(struct number *n1, struct number *n2)
{
	assert(n1->type == n2->type && n1->type == NUMBER_KNOWLEDGE_RANGES);
	assert(n1->type == n2->type && n1->type == NUMBER_RANGES);

	int len = number_range_arr_n(n1->ranges);
	if (len != number_range_arr_n(n2->ranges)) {


@@ 863,7 975,7 @@ number_range_assumed_value(bool value);
static bool
number_assume(struct number *n, bool value)
{
	assert(n->type == NUMBER_KNOWLEDGE_RANGES);
	assert(n->type == NUMBER_RANGES);

	if (!number_range_arr_canbe(n->ranges, value)) {
		return false;


@@ 890,7 1002,7 @@ number_range_issingle(struct number_range *r);
bool
number_isconstant(struct number *n)
{
	assert(n->type == NUMBER_KNOWLEDGE_RANGES);
	assert(n->type == NUMBER_RANGES);

	return number_range_arr_n(n->ranges) == 1 &&
		number_range_issingle(number_range_arr_range(n->ranges)[0]);


@@ 902,7 1014,7 @@ number_range_as_constant(struct number_range *r);
int
number_as_constant(struct number *n)
{
	assert(n->type == NUMBER_KNOWLEDGE_RANGES
	assert(n->type == NUMBER_RANGES
			&& number_range_arr_n(n->ranges) == 1);

	return number_range_as_constant(number_range_arr_range(n->ranges)[0]);


@@ 911,15 1023,15 @@ number_as_constant(struct number *n)
bool
number_issync(struct number *n)
{
	return n->type == NUMBER_KNOWLEDGE_SYNC_CONSTANT;
	return n->type == NUMBER_COMPUTED;
}

struct ast_expr *
number_as_sync(struct number *n)
{
	assert(n->type == NUMBER_KNOWLEDGE_SYNC_CONSTANT);
	assert(n->type == NUMBER_COMPUTED);

	return n->sync_const;
	return n->computation;
}

struct ast_expr *


@@ 929,9 1041,9 @@ struct ast_expr *
number_to_expr(struct number *n)
{
	switch (n->type) {
	case NUMBER_KNOWLEDGE_RANGES:
	case NUMBER_RANGES:
		return number_ranges_to_expr(n->ranges);
	case NUMBER_KNOWLEDGE_SYNC_CONSTANT:
	case NUMBER_COMPUTED:
		return ast_expr_copy(number_as_sync(n));
	default:
		assert(false);


@@ 945,10 1057,10 @@ struct number *
number_copy(struct number *num)
{
	switch (num->type) {
	case NUMBER_KNOWLEDGE_RANGES:
	case NUMBER_RANGES:
		return number_ranges_create(number_range_arr_copy(num->ranges));
	case NUMBER_KNOWLEDGE_SYNC_CONSTANT:
		return number_sync_create(ast_expr_copy(num->sync_const));
	case NUMBER_COMPUTED:
		return number_computed_create(ast_expr_copy(num->computation));
	default:
		assert(false);
	}

A tests/0-basic/140-FAIL-sync-free.x => tests/0-basic/140-FAIL-sync-free.x +7 -0
@@ 0,0 1,7 @@
#include <stdlib.h>

void
unit(void *p)
{
	free(p);
}

A tests/0-basic/140-FAIL-sync-free.x.EXPECTED => tests/0-basic/140-FAIL-sync-free.x.EXPECTED +1 -0
@@ 0,0 1,1 @@
cannot exec statement: dealloc on non-location

R tests/1-branches/000-trivial.x => tests/1-branches/0000-trivial.x +0 -0
R tests/1-branches/100-body-trivial.x => tests/1-branches/0100-body-trivial.x +0 -0
R tests/1-branches/200-conditional-allocation.x => tests/1-branches/0200-conditional-allocation.x +0 -0
R tests/1-branches/210-FAIL-conditional-allocation-body.x => tests/1-branches/0210-FAIL-conditional-allocation-body.x +0 -0
R tests/1-branches/210-FAIL-conditional-allocation-body.x.EXPECTED => tests/1-branches/0210-FAIL-conditional-allocation-body.x.EXPECTED +0 -0
R tests/1-branches/220-FAIL-conditional-allocation-body.x => tests/1-branches/0220-FAIL-conditional-allocation-body.x +0 -0
R tests/1-branches/220-FAIL-conditional-allocation-body.x.EXPECTED => tests/1-branches/0220-FAIL-conditional-allocation-body.x.EXPECTED +0 -0
R tests/1-branches/300-conditional-allocation-body.x => tests/1-branches/0300-conditional-allocation-body.x +0 -0
R tests/1-branches/310-FAIL-conditional-allocation-body.x => tests/1-branches/0310-FAIL-conditional-allocation-body.x +0 -0
R tests/1-branches/310-FAIL-conditional-allocation-body.x.EXPECTED => tests/1-branches/0310-FAIL-conditional-allocation-body.x.EXPECTED +0 -0
R tests/1-branches/320-FAIL-conditional-allocation-body.x => tests/1-branches/0320-FAIL-conditional-allocation-body.x +0 -0
R tests/1-branches/320-FAIL-conditional-allocation-body.x.EXPECTED => tests/1-branches/0320-FAIL-conditional-allocation-body.x.EXPECTED +0 -0
R tests/1-branches/400-strcmp-conditional-allocation.x => tests/1-branches/0400-strcmp-conditional-allocation.x +2 -2
@@ 2,7 2,7 @@
#include <string.h>

void *
test(int x) ~ [
test(char *s) ~ [
	assume: strcmp(s, "yes") == 0;
	if (strcmp(s, "yes") == 0) {
		.alloc result;


@@ 12,7 12,7 @@ test(int x) ~ [
}

void *
test2(int x) ~ [
test2(char *s) ~ [
	assume: !(strcmp(s, "yes") == 0);
]{
	return NULL;

R tests/1-branches/500-strcmp-conditional-allocation-body.x => tests/1-branches/0500-strcmp-conditional-allocation-body.x +0 -0
R tests/1-branches/600-indirect.x => tests/1-branches/0600-indirect.x +2 -10
@@ 5,11 5,7 @@ alloc_if(int num) ~ [
	if (num) {
		.alloc result;
	}
];

void *
alloc_if(int num)
{
]{
	if (num) {
		return malloc(1);
	}


@@ 21,11 17,7 @@ test(int x) ~ [
	if (x) {
		.alloc result;
	}
];

void *
test(int x)
{
]{
	void *p;

	p = alloc_if(x);

R tests/1-branches/700-indirect.x => tests/1-branches/0700-indirect.x +0 -0
R tests/1-branches/800-indirect.x => tests/1-branches/0800-indirect.x +3 -5
@@ 16,13 16,11 @@ test(int x) ~ [
		.alloc result;
	}
]{
	int num;
	void *p;
	int n;

	num = number(x);
	p = alloc_if(num);
	n = x;

	return p;
	return alloc_if(number(n));
}

int

A tests/1-branches/0900-subsequent.x => tests/1-branches/0900-subsequent.x +52 -0
@@ 0,0 1,52 @@
#include <stdlib.h>

int
f(int param);

int
g(int param);

void *
alloc_if(int num) ~ [
	if (num) {
		.alloc result;
	}
];

void *
test(int x) ~ [
	if (f(g(x))) {
		.alloc result;
	}
]{
	int m;
	int n;
	int k;

	m = x;
	~ [ m == x; ]
	n = g(m);
	~ [ n == g(x); ]
	return alloc_if(f(n));
}

int
f(int param)
{
	return param;
}

int
g(int param)
{
	return param;
}

void *
alloc_if(int num)
{
	if (num) {
		return malloc(1);
	}
	return NULL;
}

A tests/1-branches/1000-chaining-functions.x => tests/1-branches/1000-chaining-functions.x +41 -0
@@ 0,0 1,41 @@
#include <stdlib.h>

struct tuple { int x; int y; };

struct tuple
tuple_create() ~ [
	result.x = $;
	result.y = $;
];

void *
conditional_alloc(int x) ~ [ if (x) .alloc result; ];

void *
test() ~ [ if (tuple_create().x) .alloc result; ]
{
	struct tuple t;

	t = tuple_create();

	return conditional_alloc(t.x);
}

struct tuple
tuple_create()
{
	struct tuple t;

	t.x = 0;
	t.y = 0;
	return t;
}

void *
conditional_alloc(int x)
{
	if (x) {
		return malloc(1);
	}
	return NULL;
}

D tests/2-loops/002-loop-return-loc.x => tests/2-loops/002-loop-return-loc.x +0 -31
@@ 1,31 0,0 @@
#include <stdlib.h>

void *
unit() ~ [ .alloc result; ]
{
	int i;
	void **p;
	void *q;
	void *r;

	p = malloc(5);

	for (i = 0; i != 5; i++) ~ [ .alloc p[i]; ] {
		p[i] = malloc(1);
	}
	for (i = 0; i != 3; i++) ~ [ .dealloc p[i]; ] {
		free(p[i]);
	}

	~ [ for (i = 0; i != 5; i++) { !@p[i]; }; ]

	q = p[3];
	r = p[4];

	free(p);

	free(q);

	return r;
}


D tests/2-loops/003-FAIL-return-after-free.x => tests/2-loops/003-FAIL-return-after-free.x +0 -36
@@ 1,36 0,0 @@
#include <stdlib.h>

void *
unit() ~ [ .alloc result; ]
{
	int i;
	int j;
	void **p;
	void *q;

	p = malloc(5);

	for (i = 0; i != 5; i++) ~ [
		for (j = 0; j != i; j++) { .alloc p[j]; }
		for (j = 0; j != 5; j++) { .alloc p[j]; }
	]{
		p[i] = malloc(1);
	}

	free(p[3]);

	for (i = 0; i != 3; i++) ~ [
		for (j = 0; j != i; j++) { .dealloc p[j]; }
		for (j = 0; j != 3; j++) { .dealloc p[j]; }
	]{
		free(p[i]);	
	}

	q = p[4];

	~ [ @p[4]; ]

	free(p);

	return q;
}

D tests/2-loops/003-FAIL-return-after-free.x.EXPECTED => tests/2-loops/003-FAIL-return-after-free.x.EXPECTED +0 -1
@@ 1,1 0,0 @@
cannot exec statement: no value

D tests/2-loops/006-FAIL-no-free-range.x => tests/2-loops/006-FAIL-no-free-range.x +0 -16
@@ 1,16 0,0 @@
#include <stdlib.h>

void *
unit() ~ [ .alloc result; ]
{
	int i;
	void **p;

	p = malloc(5);

	for (i = 0; i != 5; i++) ~ [ .alloc p[i]; ] {
		p[i] = malloc(1);
	}

	return p;
}

D tests/2-loops/006-FAIL-no-free-range.x.EXPECTED => tests/2-loops/006-FAIL-no-free-range.x.EXPECTED +0 -1
@@ 1,1 0,0 @@
qed error: garbage on heap

D tests/2-loops/010-two-loops.x => tests/2-loops/010-two-loops.x +0 -27
@@ 1,27 0,0 @@
#include <stdlib.h>

void
unit()
{
	int i;
	int j;
	void **p;

	p = malloc(9);

	for (i = 0; i != 9; i++) ~ [
		for (j = 0; j != i; j++) { .alloc p[j]; }
		for (j = 0; j != 9; j++) { .alloc p[j]; }
	] {
		p[i] = malloc(1);
	}

	for (i = 0; i != 9; i++) ~ [
		for (j = 0; j != i; j++) { .dealloc p[j]; }
		for (j = 0; j != 9; j++) { .dealloc p[j]; }
	] {
		free(p[i]);
	}

	free(p);
}

D tests/2-loops/012-many-loops.x => tests/2-loops/012-many-loops.x +0 -54
@@ 1,54 0,0 @@
#include <stdlib.h>

void
unit()
{
	int i;
	int j;
	void **p;

	p = malloc(9);

	~ [ @p; ]

	for (i = 0; i != 9; i++) ~ [
		for (j = 0; j != i; j++) { .alloc p[j]; }
		for (j = 0; j != 9; j++) { .alloc p[j]; }
	] {
		p[i] = malloc(1);
	}

	~ [ @p[4]; ]

	free(p[3]);

	free(p[6]);

	for (i = 0; i != 3; i++) ~ [
		for (j = 0; j != i; j++) { .dealloc p[j]; }
		for (j = 0; j != 3; j++) { .dealloc p[j]; }
	] {
		free(p[i]);
	}

	for (i = 5; i != 6; i++) ~ [
		for (j = 5; j != i; j++) { .dealloc p[j]; }
		for (j = 5; j != 6; j++) { .dealloc p[j]; }
	] {
		free(p[i]);
	}

	~ [ for (i = 7; i != 9; i++) { @p[i]; } ]

	for (i = 7; i != 9; i++) ~ [
		for (j = 7; j != i; j++) { .dealloc p[j]; }
		for (j = 7; j != 9; j++) { .dealloc p[j]; }
	] {
		free(p[i]);
	}


	free(p[4]);

	free(p);
}

D tests/4-linking/031-external-missing-definition.x => tests/4-linking/031-external-missing-definition.x +0 -4
@@ 1,4 0,0 @@
#include <stdlib.h>

void *
allocating() ~ [ .alloc result; ];

M tests/5-program/100-lex/parse.x => tests/5-program/100-lex/parse.x +514 -384
@@ 2,97 2,13 @@
#include <stdlib.h>
#include <string.h>
#include <ctype.h>
#include <assert.h>

#define true 1
#define false 0
#define true 1

char *
read_file(char *path) ~ [ .alloc result; ]
{
	FILE *f;
	char *str;
	int fsize; /* XXX: should be long */

	f = fopen(path, "rb");
	fseek(f, 0, SEEK_END);
	fsize = ftell(f);
	fseek(f, 0, SEEK_SET);  /* same as rewind(f); */
	str = malloc(fsize + 1);
	fread(str, fsize, 1, f);
	fclose(f);
	str[fsize] = '\0';
	return str;
}

int
main()
{
	char *file;
	/*struct lexer *l;*/

	file = read_file("/home/ubuntu/xr0/tests/3-program/100-lex/gen.l");

	/* XXX: temporarily framing #15
	l = parse(file);
	lexer_print(l);
	lexer_destroy(l);
	*/

	free(file);
}

struct pattern {
	char *name; char *pattern;
};

struct token {
	int isliteral;
	char *name; char *action;
};

struct pattern *
pattern_create(char *name, char *pattern) ~ [
	.alloc result;
	result->name = name;
	result->pattern = pattern;
]{
	struct pattern *p;

	p = malloc(sizeof(struct pattern));
	p->name = name;
	p->pattern = pattern;

	return p;
}

void
pattern_destroy(struct pattern *p) ~ [
	pre: p = pattern_create($, $);
	.dealloc p;
]{
	free(p);
}

struct token *
token_create(int isliteral, char *name, char *action) ~ [ .alloc result; ]
{
	struct token *tk;

	tk = malloc(sizeof(struct token));
	tk->isliteral = isliteral;
	tk->name = name;
	tk->action = action;

	return tk;
}

void
token_destroy(struct token *tk) ~ [
	pre: tk = token_create($, $, $);
	.dealloc tk;
]{
	free(tk);
}
read_file(char *path) ~ [ .alloc result; ];

struct lexer {
	char *pre; char *post;


@@ 103,304 19,188 @@ struct lexer {
struct lexer *
lexer_create(char *pre, char *post, int npat, struct pattern *pattern,
		int ntok, struct token *token) ~ [
	.alloc result;
	.alloc result; 
	result->pre = pre;
	result->post = post;
	result->pattern = pattern;
	result->token = token;
]{
	struct lexer *l;

	l = malloc(sizeof(struct lexer));
	l->pre = pre;
	l->post = post;
	l->pattern = pattern;
	l->npat = npat;
	l->token = token;
	l->ntok = ntok;

	return l;
}

void
lexer_destroy(struct lexer *l)
{
	free(l->pattern);
	free(l->token);
	free(l);
}

char *
substr(char *s, int n) ~ [ .alloc result; ]
{
	int len;
	char *ss;

	len = n + 1;
	ss = malloc(sizeof(char) * len);
	strncpy(ss, s, n);
	ss[n] = '\0';
	return ss;
}

char *
parse_id(char *input) ~ [ .alloc result; ]
{
	char *s;

	/*
	if (!isalpha(*input)) {
		fprintf(stderr, "id must begin with letter: '%s'", input);
		exit(1);
	}
	*/
	s = input + 1;
	/* XXX: '0' is a placeholder to allow this to parse */
	for (; isalpha(*s) || isdigit(*s) || *s == '_' ; 0) {
		s++;
	}
	return substr(input, s - input);
}

char *
skiplinespace(char *s) ~ [
	result = s; /* XXX */
]{
	for (; *s == ' ' || *s == '\t'; s++) {}
	return s;
}
];

#define KEYWORD_OPTION "%option"

char *
skipoptions(char *pos)
{
	char *id;
int
beginsdefs(char *s);

	if (strncmp(pos, KEYWORD_OPTION, strlen(KEYWORD_OPTION)) != 0) {
		return pos;
	}
	pos += strlen(KEYWORD_OPTION);
	pos = skiplinespace(pos);
	id = parse_id(pos);
	pos += strlen(id);
	free(id);
	return pos;
}
int
isboundary(char *s);

char *
parse_tonewline(char *input) ~ [ .alloc result; ]
{
struct stringresult {
	char *s;
	s = input; /* XXX: until loop is understood more */
	for (s = input; *s != '\n'; 0) {
		s++;
	}
	return substr(input, s - input);
}

struct patternresult {
	struct pattern *p;
	char *pos;
};

struct patternresult
parse_pattern(char *pos) ~ [
	result.p = pattern_create(malloc(1), malloc(1));
]{
	char *name; char *pattern;
	struct patternresult res;

	name = parse_id(pos);
	pos = pos + strlen(name);
	pos = skiplinespace(pos);
	pattern = parse_tonewline(pos);
	pos = pos + strlen(pattern); /* XXX: support pos += */
struct stringresult
parse_defsraw(char *input) ~ [
	.alloc result.s;
	result.pos = $;
];

	res.p = pattern_create(name, pattern);
	res.pos = pos;
	return res;
}
/* skipws: skip whitespace */
char *
skipws(char *s);

struct patternet {
struct lexer *
parse(char *pos) ~ [
	char *pre; char *post;
	struct pattern *pattern;
	int npat;
	char *pos;
};
	struct token *token;
	pre = malloc(1);
	pattern = malloc(1);
	token = malloc(1);
	post = malloc(1);
	result = lexer_create(pre, post, $, pattern, $, token);
];

char *
skipws(char *s)
{
	for (; isspace(*s); s++) {}
	return s;
}
void
lexer_destroy(struct lexer *l) ~ [
	pre: {
		l = lexer_create(
			malloc(1), malloc(1),
			$, malloc(1),
			$, malloc(1)
		);
	}

int
compute_npat(char *pos)
{
	int n;
	struct patternresult r;
	.dealloc l->pre;
	.dealloc l->post;
	.dealloc l->pattern;
	.dealloc l->token;
	.dealloc l;
];

	n = 0;
	for (; strncmp(pos, "%%", 2) != 0; n++) {
		r = parse_pattern(pos);
		pos = skipws(r.pos);
		/* TODO: clean up r.p */
void
lexer_print(struct lexer *l) ~ [
	pre: {
		l = lexer_create(
			$, $,
			$, malloc(1),
			$, malloc(1)
		);
	}
];

	return n;
}
int
main() ~ []
{
	char *file;
	struct lexer *l;

struct pattern *
parse_defs_n(char *pos, int npat) ~ [
	if (npat) {
		.alloc result;
	}
]{
	int i;
	struct pattern *p;
	struct patternresult parsed;
	file = read_file("tests/3-program/100-lex/gen.l");

	if (npat) {
		p = malloc(npat);
		for (i = 0; i < npat; i++) {
			parsed = parse_pattern(pos);
			p[i] = *parsed.p;
			pos = skipws(parsed.pos);
		}
		return p;
	}
	l = parse(file);
	lexer_print(l);
	lexer_destroy(l);

	return NULL;
	free(file);
}

struct patternet
parse_defsproper(char *pos) ~ [
	if (compute_npat(pos)) {
		.alloc result.pattern;
	}
]{
	struct patternet res;
char *
read_file(char *path)
{
	FILE *f;
	char *str;
	int fsize; /* XXX: should be long */

	res.npat = compute_npat(pos);
	res.pattern = parse_defs_n(pos, res.npat);
	res.pos = pos;
	return res;
	f = fopen(path, "rb");
	fseek(f, 0, SEEK_END);
	fsize = ftell(f);
	fseek(f, 0, SEEK_SET);  /* same as rewind(f); */
	str = malloc(fsize + 1);
	fread(str, fsize, 1, f);
	fclose(f);
	str[fsize] = '\0';
	return str;
}

struct rulesresult {
	struct token *token;
	int ntok;
	char *pos;
struct pattern {
	char *name; char *pattern;
};

struct tokenresult {
	struct token *tk;
	char *pos;
void
pattern_print(struct pattern *p) ~ [
	pre: p = pattern_create("", "");
];

struct token {
	int isliteral;
	char *name; char *action;
};

struct tokenresult
parse_token(char *pos);
void
token_print(struct token *t) ~ [
	pre: t = token_create(0, "", "");
];

int
compute_ntok(char *pos)
struct lexer *
lexer_create(char *pre, char *post, int npat, struct pattern *pattern,
		int ntok, struct token *token) 
{
	int n;
	struct tokenresult r;
	struct lexer *l;

	n = 0;
	for (; *pos != '\0' && strncmp(pos, "%%", 2) != 0 ; n++) {
		r = parse_token(pos);
		pos = skipws(r.pos);
		/* TODO: clean up r.tk */
	}
	l = malloc(sizeof(struct lexer));
	l->pre = pre;
	l->post = post;
	l->pattern = pattern;
	l->npat = npat;
	l->token = token;
	l->ntok = ntok;

	return n;
	return l;
}

struct token *
parse_rules_n(char *pos, int ntok) ~ [
	if (ntok) {
		.alloc result;
	}
]{
void
lexer_destroy(struct lexer *l)
{
	int i;
	struct token *t;
	struct tokenresult parsed;

	if (ntok) {
		t = malloc(ntok);
		for (i = 0; i < ntok; i++) {
			parsed = parse_token(pos);
			t[i] = *parsed.tk;
			pos = skipws(parsed.pos);
		}
		return t;
	}

	return NULL;
}

struct rulesresult
parse_rules(char *pos) ~ [
	if (compute_ntok(pos)) {
		.alloc result.token;
	free(l->pre);
	free(l->post);
	for (i = 0; i < l->npat; i++) {
		free(l->pattern[i].name);
		free(l->pattern[i].pattern);
	}
]{
	struct rulesresult res;

	res.ntok = compute_ntok(pos);
	res.token = parse_rules_n(pos, res.ntok);
	res.pos = pos;
	return res;
}


struct lexer;

struct lexer *
parse(char *input);

void
lexer_destroy(struct lexer *) ~ [
	pre: {
		l = lexer_create(
			$, $,
			$, malloc(1),
			$, malloc(1)
		);
	free(l->pattern);
	for (i = 0; i < l->ntok; i++) {
		free(l->token[i].name);
		free(l->token[i].action);
	}

	.dealloc l->pattern;
	.dealloc l->token;
	.dealloc l;
];

void
lexer_print(struct lexer *);

void
pattern_print(struct pattern *);

void
token_print(struct token *);
	free(l->token);
	free(l);
}

void
lexer_print(struct lexer *l)
{
	int i;

	printf("\tpre: %s\n", l->pre);
	printf("\tpost: %s\n", l->post);
	printf("\tpatterns:\n");
	puts("\tpre:");
	puts(l->pre);

	puts("\tpost:");
	puts(l->post);

	puts("\tpatterns:");
	for (i = 0; i < l->npat; i++) {
		printf("\t\t");
		putchar('\t');
		putchar('\t');
		pattern_print(&l->pattern[i]);
		printf("\n");
		putchar('\n');
	}
	printf("\ttokens:\n");
	puts("\ttokens:");
	for (i = 0; i < l->ntok; i++) {
		printf("\t\t");
		putchar('\t');
		putchar('\t');
		token_print(&l->token[i]);
		printf("\n");
		putchar('\n');
	}
}



@@ 411,51 211,162 @@ struct defsresult {
	char *pos;
};

char *
skipoptions(char *pos);

int
count_patterns(char *pos);

struct defsresult
parse_defs(char *pos);
parse_defs(char *pos) ~ [
	.alloc result.pre;
	.alloc result.pattern;
	result.pos = $;
	result.npat = $;
];

int
beginsdefs(char *s)
{
	return strncmp(s, "%{", 2) == 0;
}

struct rulesresult {
	struct token *token;
	int ntok;
	char *pos;
};

int
count_tokens(char *pos);

struct rulesresult
parse_rules(char *pos);
parse_rules(char *pos) ~ [
	.alloc result.token;
	result.pos = $;
	result.ntok = $;
];

char *
parse_toeof(char *input);
parse_toeof(char *input) ~ [ .alloc result; ];

struct lexer *
parse(char *pos)
{
	struct defsresult def;
	struct rulesresult res;
	struct defsresult defs;
	struct rulesresult rules;
	char *post;

	def = parse_defs(pos);
	pos = def.pos;
	if (strncmp(pos, "%%", 2) != 0) {
		fprintf(stderr, "invalid transition to rules: '%.*s'\n", 10,
			pos);
	defs = parse_defs(pos);
	pos = defs.pos;
	if (!isboundary(pos)) {
		puts("invalid transition to rules");
		exit(1);
	}
	pos = skipws(pos + 2); /* %% */
	res = parse_rules(pos);
	pos = res.pos;
	post = "";
	if (strncmp(pos, "%%", 2) == 0) {
		pos += 2;
		post = parse_toeof(pos);
	rules = parse_rules(pos);
	pos = rules.pos;
	post = parse_toeof(pos);
	return lexer_create(defs.pre, post, defs.npat, defs.pattern, rules.ntok,
		rules.token);
}

int
isboundary(char *s)
{
	return strncmp(s, "%%", 2) == 0;
}

char *
substr(char *s, int n) ~ [ .alloc result; ]
{
	int len;
	char *ss;

	len = n + 1;
	ss = malloc(sizeof(char) * len);
	strncpy(ss, s, len);
	ss[len-1] = '\0';
	return ss;
}

char *
skipws(char *s)
{
	for (; isspace(*s); s++) {}
	return s;
}

char *
skiplinespace(char *s)
{
	for (; *s == ' ' || *s == '\t'; s++) {}
	return s;
}

char *
parse_id(char *input) ~ [ .alloc result; ];

char *
skipoptions(char *pos)
{
	char *keyword;
	char *id;

	pos = skipws(pos);
	keyword = "%option";
	if (strncmp(pos, keyword, strlen(keyword)) != 0) {
		return pos;
	}
	pos += strlen(keyword);
	pos = skiplinespace(pos);
	id = parse_id(pos);
	pos += strlen(id);
	free(id);
	return skipws(pos);
}

char *
parse_id(char *input)
{
	char *s;

	if (!isalpha(*input)) {
		/* TODO: print to stderr */
		puts("id must begin with letter");
		exit(1);
	}
	s = input + 1;
	/* XXX: '0' is a placeholder to allow this to parse */
	for (; isalpha(*s) || isdigit(*s) || *s == '_' ; 0) {
		s++;
	}
	return lexer_create(def.pre, post, def.npat, def.pattern, res.ntok,
		res.token);
	return substr(input, s - input);
}

struct stringresult {
char *
parse_tonewline(char *input) ~ [ .alloc result; ]
{
	char *s;
	s = input; /* must be here because not seen with skip loop hack */
	for (; *s != '\n'; 0) {
		s++;
	}
	return substr(input, s - input);
}

struct patternet {
	struct pattern *pattern;
	int npat;
	char *pos;
};

struct stringresult
parse_defsraw(char *input);

struct patternet
parse_defsproper(char *pos);
parse_defsproper(char *input) ~ [
	.alloc result.pattern;
	result.npat = $;
	result.pos = $;
];

struct defsresult
parse_defs(char *pos)


@@ 466,14 377,12 @@ parse_defs(char *pos)

	pos = skipws(pos);
	if (*pos == '\0') {
		fprintf(stderr, "EOF in defs\n");
		puts("EOF in defs");
		exit(1);
	}
	raw = parse_defsraw(pos);
	pos = raw.pos;
	pos = skipws(pos);
	pos = skipoptions(pos);
	pos = skipws(pos);
	set = parse_defsproper(pos);

	res.pre = raw.s;


@@ 489,8 398,9 @@ parse_defsraw(char *input)
	char *pos;
	struct stringresult res;

	if (strncmp(input, "%{", 2) != 0) {
		res.s = "";
	if (!beginsdefs(input)) {
		res.s = malloc(1);
		res.s[0] = '\0';
		res.pos = input;
		return res;
	}


@@ 502,22 412,229 @@ parse_defsraw(char *input)
	return res;
}

struct pattern *
pattern_create(char *name, char *pattern) ~ [
	.alloc result;
	result->name = name;
	result->pattern = pattern;
]{
	struct pattern *p;

	p = malloc(sizeof(struct pattern));
	p->name = name;
	p->pattern = pattern;

	return p;
}

void
pattern_print(struct pattern *p)
{
	printf("%s\t\t%s", p->name, p->pattern);
	puts("pattern:");
	puts(p->name);
	puts(p->pattern);
	puts("end pattern");
}


struct patternresult {
	struct pattern *p;
	char *pos;
};

struct patternpos {
	struct pattern *p;
	char *pos;
};

struct patternpos
parse_defs_n(char *pos, int npat) ~ [
	.alloc result.p;
	result.pos = $;
];

struct patternet
parse_defsproper(char *input)
{
	struct patternet res;
	struct patternpos defs_n;

	res.npat = count_patterns(input);
	defs_n = parse_defs_n(input, res.npat);
	res.pattern = defs_n.p;
	res.pos = defs_n.pos;
	return res;
}

struct patternresult
parse_pattern(char *pos) ~ [
	result.p = pattern_create(malloc(1), malloc(1));
];

int
count_patterns(char *pos)
{
	int n;
	struct patternresult parsed;

	n = 0;
	for (; strncmp(pos, "%%", 2) != 0; n++) {
		parsed = parse_pattern(pos);
		pos = skipws(parsed.pos);
		free(parsed.p->name);
		free(parsed.p->pattern);
		free(parsed.p);
	}

	return n;
}

struct patternresult
parse_pattern(char *pos)
{
	char *name; char *pattern;
	struct patternresult res;

	name = parse_id(pos);
	pos = pos + strlen(name);
	pos = skiplinespace(pos);
	pattern = parse_tonewline(pos);
	pos += strlen(pattern);

	res.p = pattern_create(name, pattern);
	res.pos = pos;
	return res;
}

struct patternpos
parse_defs_n(char *pos, int npat)
{
	int i;
	struct pattern *p;
	struct patternresult parsed;
	struct patternpos res;

	if (!npat) {
		p = malloc(1);
	}
	if (npat) {