~lbnz/xr0

7c4ed29b9eec28e759dc2c8d2edc2225387fcc05 — Xr0 Team 2 months ago 6c02b36
feat: debugger at parity

issue: https://github.com/xr0-org/xr0/issues/45
59 files changed, 2468 insertions(+), 728 deletions(-)

M Makefile
M include/ast.h
M include/path.h
M include/state.h
M include/util.h
M include/value.h
M src/ast/ast.c
M src/ast/block.c
M src/ast/expr/expr.c
M src/ast/expr/verify.c
M src/ast/function/function.c
M src/ast/gram.y
M src/ast/intern.h
M src/ast/stmt/stmt.c
M src/ast/stmt/stmt.h
M src/ast/stmt/verify.c
M src/ast/type/type.c
M src/main.c
M src/path/path.c
M src/props/props.c
M src/state/location.c
A src/state/program.c
A src/state/program.h
M src/state/stack.c
M src/state/stack.h
M src/state/state.c
M src/util/util.c
M src/value/value.c
M tests/0-basic/030-alloc.x
M tests/0-basic/130-FAIL-double-free.x.EXPECTED
M tests/0-basic/140-FAIL-sync-free.x.EXPECTED
M tests/0-basic/170-FAIL-double-free.x.EXPECTED
M tests/1-branches/0100-body-trivial.x
A tests/1-branches/1300-nested-branch-return.x
M tests/5-pass-by-ptr/000-basic.x
M tests/6-preconditions/100-FAIL-need-alloced-lval.x.EXPECTED
M tests/6-preconditions/101-FAIL-need-alloced-rval.x
M tests/6-preconditions/101-FAIL-need-alloced-rval.x.EXPECTED
M tests/6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x.EXPECTED
M tests/6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x.EXPECTED
M tests/7-use-after-free/002-pass-in-lvalue.x
M tests/7-use-after-free/005-conditions.x
M tests/7-use-after-free/100-FAIL-lvalue-use-after-free.x.EXPECTED
M tests/7-use-after-free/101-FAIL-rvalue-use-after-free.x.EXPECTED
M tests/7-use-after-free/110-FAIL-freed-ptr-dangling-return.x.EXPECTED
M tests/7-use-after-free/112-FAIL-freed-ptr-dangling-false-claim.x.EXPECTED
M tests/7-use-after-free/120-FAIL-freed-ptr-maybe-dangling-return.x.EXPECTED
M tests/7-use-after-free/200-FAIL-stack-frame-pop-dangling-return.x.EXPECTED
M tests/7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x.EXPECTED
M tests/7-use-after-free/300-FAIL-struct-free-ptr-dangling.x.EXPECTED
M tests/7-use-after-free/400-FAIL-conditions-in-setup.x.EXPECTED
M tests/8-uninitialised-memory/000-FAIL-uninitialised-memory-rval.x.EXPECTED
M tests/8-uninitialised-memory/001-FAIL-uninitialised-memory-rval.x.EXPECTED
M tests/8-uninitialised-memory/002-FAIL-uninitialised-memory-rval.x.EXPECTED
M tests/8-uninitialised-memory/003-FAIL-uninitialised-memory-rval.x.EXPECTED
M tests/8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x.EXPECTED
A tests/9-calls/complex-call-expressions.x
M tests/99-program/000-matrix.x
M tests/run
M Makefile => Makefile +7 -1
@@ 33,6 33,7 @@ MAIN_0V_OBJ = $(BUILD_DIR)/0v.o
STATE_OBJ = $(BUILD_DIR)/state.o
STATIC_OBJ = $(BUILD_DIR)/static.o
STACK_OBJ = $(BUILD_DIR)/stack.o
PROGRAM_OBJ = $(BUILD_DIR)/program.o
HEAP_OBJ = $(BUILD_DIR)/heap.o
CLUMP_OBJ = $(BUILD_DIR)/clump.o
LOCATION_OBJ = $(BUILD_DIR)/location.o


@@ 67,9 68,10 @@ STATE_OBJECTS = $(VALUE_OBJ) \
		$(CLUMP_OBJ) \
		$(HEAP_OBJ) \
		$(STACK_OBJ) \
		$(PROGRAM_OBJ) \
		$(PROPS_OBJ) \
		$(STATIC_OBJ) \
		$(EXT_OBJ) \
		$(PROPS_OBJ) \
		$(PATH_OBJ)

OBJECTS = $(XR0_OBJECTS) $(STATE_OBJECTS)


@@ 133,6 135,10 @@ $(STACK_OBJ): $(STATE_DIR)/stack.c $(BLOCK_OBJ)
	@printf 'CC\t$@\n'
	@$(CC) $(CFLAGS) -o $@ -c $(STATE_DIR)/stack.c

$(PROGRAM_OBJ): $(STATE_DIR)/program.c
	@printf 'CC\t$@\n'
	@$(CC) $(CFLAGS) -o $@ -c $(STATE_DIR)/program.c

$(HEAP_OBJ): $(STATE_DIR)/heap.c $(BLOCK_OBJ)
	@printf 'CC\t$@\n'
	@$(CC) $(CFLAGS) -o $@ -c $(STATE_DIR)/heap.c

M include/ast.h => include/ast.h +90 -18
@@ 64,6 64,9 @@ ast_expr_incdec_root(struct ast_expr *);
bool
ast_expr_incdec_pre(struct ast_expr *);

bool
ast_expr_incdec_inc(struct ast_expr *);

struct ast_expr *
ast_expr_member_create(struct ast_expr *, char *);



@@ 165,6 168,9 @@ ast_expr_alloc_arg(struct ast_expr *);
enum ast_alloc_kind
ast_expr_alloc_kind(struct ast_expr *);

struct ast_expr *
ast_expr_alloc_kind_create(struct ast_expr *arg, enum ast_alloc_kind);

struct state;

struct error *


@@ 227,6 233,24 @@ ast_expr_abseval(struct ast_expr *, struct state *);
struct result *
ast_expr_pf_reduce(struct ast_expr *, struct state *);

struct value;

struct result *
ast_expr_pf_augment(struct value *, struct ast_expr *, struct state *);

struct ast_function;

struct value *
ast_expr_call_arbitrary(struct ast_expr *, struct ast_function *,
	struct state *);

struct ast_block;
struct lexememarker;

struct ast_expr *
ast_expr_geninstr(struct ast_expr *, struct lexememarker *,
	struct ast_block *, struct state *);

struct ast_stmt;

struct ast_block;


@@ 247,6 271,9 @@ ast_block_str(struct ast_block *, int indent_level);
char *
ast_block_absstr(struct ast_block *b, int indent_level);

char *
ast_block_render(struct ast_block *, int index, bool indecls);

struct ast_block *
ast_block_copy(struct ast_block *b);



@@ 263,15 290,30 @@ struct ast_stmt **
ast_block_stmts(struct ast_block *b);

bool
ast_block_empty(struct ast_block *b);

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

struct ast_type;

struct ast_expr *
ast_block_call_create(struct ast_block *, struct lexememarker *,
	struct ast_type *, struct ast_expr *);

void
ast_block_append_decl(struct ast_block *, struct ast_variable *);

void
ast_block_append_stmt(struct ast_block *, struct ast_stmt *);

struct preconds_result {
	struct ast_stmt *stmt;
	struct ast_block *b;
	struct error *err;
};

struct preconds_result
ast_block_preconds(struct ast_block *b);
ast_block_setups(struct ast_block *b, struct state *);

struct ast_stmt;



@@ 295,6 337,9 @@ ast_stmt_labelled_label(struct ast_stmt *);
struct ast_stmt *
ast_stmt_labelled_stmt(struct ast_stmt *);

struct ast_block *
ast_stmt_labelled_as_block(struct ast_stmt *);

struct ast_stmt *
ast_stmt_create_nop(struct lexememarker *);



@@ 373,6 418,21 @@ ast_stmt_create_dealloc(struct lexememarker *, struct ast_expr *arg);
struct ast_stmt *
ast_stmt_create_clump(struct lexememarker *, struct ast_expr *arg);

struct ast_stmt *
ast_stmt_register_call_create(struct lexememarker *, struct ast_expr *call);

struct ast_stmt *
ast_stmt_register_mov_create(struct lexememarker *, struct ast_variable *v);

struct ast_expr *
ast_stmt_register_call(struct ast_stmt *);

struct ast_variable *
ast_stmt_register_mov(struct ast_stmt *);

bool
ast_stmt_register_iscall(struct ast_stmt *);

void
ast_stmt_destroy(struct ast_stmt *);



@@ 395,13 455,15 @@ ast_stmt_as_v_block(struct ast_stmt *);
struct ast_expr *
ast_stmt_as_expr(struct ast_stmt *);

enum execution_mode;

struct error *
ast_stmt_process(struct ast_stmt *, char *fname, struct state *);
ast_stmt_linearise(struct ast_stmt *, struct state *, enum execution_mode);

struct preresult;
bool
ast_stmt_linearisable(struct ast_stmt *);

struct preresult *
ast_stmt_preprocess(struct ast_stmt *, struct state *);
struct preresult;

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


@@ 416,10 478,16 @@ struct error *
ast_stmt_exec(struct ast_stmt *, struct state *);

struct error *
ast_stmt_absprocess(struct ast_stmt *stmt, char *fname, struct state *, bool iscall);
ast_stmt_process(struct ast_stmt *, struct state *);

struct error *
ast_stmt_absprocess(struct ast_stmt *stmt, struct state *);

struct error *
ast_stmt_absprocess_nosetup(struct ast_stmt *stmt, struct state *);

struct error *
ast_stmt_setupabsexec(struct ast_stmt *stmt, struct state *);
ast_stmt_buildsetup(struct ast_stmt *, struct state *, struct ast_block *);

struct ast_type;



@@ 434,6 502,9 @@ struct ast_type *
ast_type_create_ptr(struct ast_type *type);

struct ast_type *
ast_type_create_void();

struct ast_type *
ast_type_create_voidptr();

struct ast_type *


@@ 470,7 541,9 @@ ast_type_isstruct(struct ast_type *);
bool
ast_type_istypedef(struct ast_type *);

struct value;
bool
ast_type_isvoid(struct ast_type *);

struct externals;

struct value *


@@ 534,7 607,6 @@ ast_variable_name(struct ast_variable *);
struct ast_type *
ast_variable_type(struct ast_variable *);

struct ast_function;

/* ast_function_create: name must be allocated on the heap */
struct ast_function *


@@ 572,6 644,9 @@ ast_function_isproto(struct ast_function *f);
bool
ast_function_absisempty(struct ast_function *f);

bool
ast_function_isvoid(struct ast_function *f);

struct ast_type *
ast_function_type(struct ast_function *f);



@@ 587,25 662,22 @@ ast_function_nparams(struct ast_function *f);
struct ast_variable **
ast_function_params(struct ast_function *f);

struct preconds_result
ast_function_preconditions(struct ast_function *f);

struct error *
ast_function_initparams(struct ast_function *, struct state *);

struct error *
ast_function_initsetup(struct ast_function *, struct state *);

struct externals;
struct error;

struct error *
ast_function_verify(struct ast_function *, struct externals *);

struct result;

struct error *
ast_function_setupabsexec(struct ast_function *f, struct state *state);
ast_function_debug(struct ast_function *, struct externals *);

struct result *
ast_function_absexec(struct ast_function *, struct state *state);
struct result;

struct ast_externdecl;


M include/path.h => include/path.h +3 -0
@@ 22,4 22,7 @@ path_atend(struct path *);
struct error *
path_step(struct path *);

struct error *
path_next(struct path *);

#endif

M include/state.h => include/state.h +79 -7
@@ 7,6 7,7 @@

/* ast */
struct ast_function;
struct ast_block;
struct ast_type;
struct ast_variable;
struct ast_expr;


@@ 25,14 26,27 @@ struct value;

struct state;

enum execution_mode {
	EXEC_ABSTRACT,
	EXEC_ABSTRACT_NO_SETUP,
	EXEC_ACTUAL,
	EXEC_SETUP,
	EXEC_VERIFY
};

enum frame_kind {
	FRAME_NESTED,
	FRAME_INTERMEDIATE,
	FRAME_CALL
};

struct frame;

struct state *
state_create(char *name, struct ast_block *, struct ast_type *result_type,
		bool abstract, struct externals *);
state_create(struct frame *, struct externals *);

struct state *
state_create_withprops(char *name, struct ast_block *,
		struct ast_type *result_type, bool abstract, struct externals *,
		struct props *props);
state_create_withprops(struct frame *, struct externals *, struct props *props);

struct state *
state_copy(struct state *);


@@ 58,16 72,26 @@ state_getext(struct state *);
struct props *
state_getprops(struct state *);

char *
state_programtext(struct state *);

int
state_programindex(struct state *);

int
state_frameid(struct state *);

struct heap *
state_getheap(struct state *);

void
state_pushframe(struct state *, char *name, struct ast_block *b,
		struct ast_type *, bool abstract);
state_pushframe(struct state *, struct frame *);

void
state_popframe(struct state *);

void
state_unnest(struct state *);

void
state_declare(struct state *, struct ast_variable *var, bool isparam);


@@ 102,6 126,12 @@ state_range_dealloc(struct state *, struct object *,
		struct ast_expr *lw, struct ast_expr *up);

bool
state_islinear(struct state *);

enum execution_mode
state_execmode(struct state *);

bool
state_addresses_deallocand(struct state *, struct object *);

bool


@@ 132,6 162,48 @@ state_hasgarbage(struct state *);
bool
state_equal(struct state *s1, struct state *s2);

struct value *
state_popregister(struct state *);

struct value *
state_readregister(struct state *);

void
state_writeregister(struct state *, struct value *);

void
state_clearregister(struct state *);

void
state_initsetup(struct state *s, int frameid);

enum execution_mode
state_next_execmode(struct state *s);

struct error *
state_stacktrace(struct state *, struct error *);

void
state_return(struct state *);

struct ast_expr *
state_framecall(struct state *);


/* FRAME DTO */

struct frame *
frame_call_create(char *name, struct ast_block *, struct ast_type *,
		enum execution_mode, struct ast_expr *, struct ast_function *);

struct frame *
frame_block_create(char *name, struct ast_block *, enum execution_mode);

struct frame *
frame_setup_create(char *name, struct ast_block *, enum execution_mode);

struct frame *
frame_intermediate_create(char *name, struct ast_block *, enum execution_mode);

/* USED BY VALUE */


M include/util.h => include/util.h +14 -1
@@ 95,12 95,19 @@ strbuilder_build(struct strbuilder *b);
char *
strbuilder_preview(struct strbuilder *b);

enum loglevel {
	LOG_NONE	= 1 << 0,
	LOG_INFO	= 1 << 1,
	LOG_DEBUG	= 1 << 2
};

int
d_printf(char *fmt, ...);

/* v_printf: Print if Xr0 is in verbose mode. */
int
v_printf(char *fmt, ...);


struct error;

struct error *


@@ 117,6 124,12 @@ error_to_undecideable_cond(struct error *);
struct ast_expr *
error_get_undecideable_cond(struct error *);

struct error *
error_return();

struct error *
error_to_return(struct error *);

char *
error_str(struct error *);


M include/value.h => include/value.h +2 -0
@@ 1,6 1,8 @@
#ifndef VALUE_H
#define VALUE_H

#include <stdbool.h>

enum value_type {
	VALUE_SYNC,
	VALUE_PTR,

M src/ast/ast.c => src/ast/ast.c +62 -0
@@ 203,6 203,68 @@ preresult_iscontradiction(struct preresult *r)
	return r->iscontradiction;
}

struct iresult {
	struct ast_expr *val;
	struct error *err;
};

struct iresult *
iresult_error_create(struct error *err)
{
	assert(err);

	struct iresult *r = malloc(sizeof(struct iresult));
	r->val = NULL;
	r->err = err;
	return r;
}

struct iresult *
iresult_expr_create(struct ast_expr *val)
{
	struct iresult *r = malloc(sizeof(struct iresult));
	r->val = val;
	r->err = NULL;
	return r;
}

void
iresult_destroy(struct iresult *res)
{
	assert(!res->err);
	if (res->val) {
		ast_expr_destroy(res->val);
	}
	free(res);
}

bool
iresult_iserror(struct iresult *res)
{
	return res->err;
}

struct error *
iresult_as_error(struct iresult *res)
{
	assert(res->err);
	return res->err;
}

struct ast_expr *
iresult_as_expr(struct iresult *res)
{
	assert(!res->err);
	return res->val;
}

bool
iresult_hasexpr(struct iresult *res)
{
	assert(!iresult_iserror(res));
	return res->val; /* implicit cast */
}

struct string_arr *
ast_topological_order(char *fname, struct externals *ext)
{

M src/ast/block.c => src/ast/block.c +91 -14
@@ 9,6 9,7 @@ struct ast_block {
	int ndecl, nstmt;
	struct ast_variable **decl;
	struct ast_stmt **stmt;
	int tempcount;
};

struct ast_block *


@@ 24,6 25,7 @@ ast_block_create(struct ast_variable **decl, int ndecl,
	b->ndecl = ndecl;
	b->stmt = stmt;
	b->nstmt = nstmt;
	b->tempcount = 0;
	return b;
}



@@ 127,6 129,31 @@ ast_block_absstr(struct ast_block *b, int indent)
	return ast_block_str_div(b, indent, '[', ']');
}

char *
ast_block_render(struct ast_block *b, int index, bool indecls)
{
	struct strbuilder *sb = strbuilder_create();
	for (int i = 0; i < b->ndecl; i++) {
		char *s = ast_variable_str(b->decl[i]);
		if (i == index && indecls) {
			strbuilder_printf(sb, "-->\t%s;\n", s);
		} else {
			strbuilder_printf(sb, "\t%s;\n", s);
		}
		free(s);
	}
	for (int i = 0; i < b->nstmt; i++) {
		char *s = ast_stmt_str(b->stmt[i], 1);
		if (i == index && !indecls) {
			strbuilder_printf(sb, "-->\t%s\n", s);
		} else {
			strbuilder_printf(sb, "\t%s\n", s);
		}
		free(s);
	}
	return strbuilder_build(sb);
}

int
ast_block_ndecls(struct ast_block *b)
{


@@ 165,21 192,71 @@ ast_block_isterminal(struct ast_block *b, struct state *s)
	return false;
}

bool
ast_block_empty(struct ast_block *b)
{
	return b->ndecl == 0 && b->nstmt == 0;
}

void
block_append_decl(struct ast_block *b, struct ast_variable *v)
{
	b->decl = realloc(b->decl, sizeof(struct ast_variable *) * ++b->ndecl);
	b->decl[b->ndecl-1] = v;
}

void
ast_block_append_stmt(struct ast_block *b, struct ast_stmt *v)
{
	b->stmt = realloc(b->stmt, sizeof(struct ast_stmt *) * ++b->nstmt);
	b->stmt[b->nstmt-1] = v;
}

struct preconds_result
ast_block_preconds(struct ast_block *b)
{
	int n = ast_block_nstmts(b);
	struct ast_stmt **stmt = ast_block_stmts(b);
	for (int i = 0; i < n; i++) {
		/* XXX: either enforce one pre block or concat */
		if (ast_stmt_ispre(stmt[i])) {
			struct ast_stmt *preconds = ast_stmt_labelled_stmt(stmt[i]);
			struct error *err = ast_stmt_preconds_validate(preconds);
			if (err) {
				return (struct preconds_result) { .stmt = NULL, .err = err };
			}
			return (struct preconds_result) { .stmt = preconds, .err = NULL };
ast_block_setups(struct ast_block *abs, struct state *state)
{
	struct ast_block *setups = ast_block_create(NULL, 0, NULL, 0);
	int nstmts = ast_block_nstmts(abs);
	struct ast_stmt **stmts = ast_block_stmts(abs);
	for (int i = 0; i < nstmts; i++) {
		struct error *err = ast_stmt_buildsetup(stmts[i], state, setups);		
		if (err) {
			return (struct preconds_result) { .b = NULL, .err = err };
		}
	}
	return (struct preconds_result) { .stmt = NULL, .err = NULL };
	return (struct preconds_result) { .b = setups, .err = NULL };
}

static char *
generate_tempvar(int tempid);

struct ast_expr *
ast_block_call_create(struct ast_block *b, struct lexememarker *loc,
		struct ast_type *rtype, struct ast_expr *expr)
{
	struct ast_stmt *call = ast_stmt_register_call_create(
		loc, ast_expr_copy(expr)
	);
	ast_block_append_stmt(b, call);

	if (!ast_type_isvoid(rtype)) {
		char *tvar = generate_tempvar(b->tempcount++);
		struct ast_stmt *read = ast_stmt_register_mov_create(
			loc,
			ast_variable_create(
				dynamic_str(tvar), ast_type_copy(rtype)
			)
		);
		ast_block_append_stmt(b, read);
		return ast_expr_identifier_create(dynamic_str(tvar));
	}
	return NULL;
}

static char *
generate_tempvar(int tempid)
{
	struct strbuilder *b = strbuilder_create();
	strbuilder_printf(b, "<t%d>", tempid);
	return strbuilder_build(b);
}

M src/ast/expr/expr.c => src/ast/expr/expr.c +26 -0
@@ 272,6 272,14 @@ ast_expr_incdec_pre(struct ast_expr *expr)
	return expr->u.incdec.pre;
}

bool
ast_expr_incdec_inc(struct ast_expr *expr)
{
	assert(expr->kind == EXPR_INCDEC);

	return expr->u.incdec.inc;
}

struct ast_expr *
ast_expr_incdec_root(struct ast_expr *expr)
{


@@ 692,6 700,21 @@ ast_expr_clump_create(struct ast_expr *arg)
	return expr;
}

struct ast_expr *
ast_expr_alloc_kind_create(struct ast_expr *arg, enum ast_alloc_kind kind)
{
	switch (kind) {
	case ALLOC:
		return ast_expr_alloc_create(arg);
	case DEALLOC:
		return ast_expr_dealloc_create(arg);
	case CLUMP:
		return ast_expr_clump_create(arg);
	default:
		assert(false);
	}
}

static struct ast_expr *
ast_expr_alloc_copy(struct ast_expr *expr)
{


@@ 958,6 981,9 @@ ast_expr_equal(struct ast_expr *e1, struct ast_expr *e2)
		) && (strcmp(
			ast_expr_member_field(e1), ast_expr_member_field(e2)
		) == 0);
	case EXPR_ALLOCATION:
		return ast_expr_alloc_kind(e1) == ast_expr_alloc_kind(e2) && 
			ast_expr_equal(ast_expr_alloc_arg(e1), ast_expr_alloc_arg(e2));
	default:
		assert(false);
	}

M src/ast/expr/verify.c => src/ast/expr/verify.c +302 -75
@@ 459,7 459,6 @@ ast_expr_eval(struct ast_expr *expr, struct state *state)
	case EXPR_ARBARG:
		return arbarg_eval(expr, state);
	default:
		/*printf("expr: %s\n", ast_expr_str(expr));*/
		assert(false);
	}
}


@@ 682,13 681,7 @@ prepare_parameters(int nparams, struct ast_variable **param,
		struct result_arr *args, char *fname, struct state *state);

static struct error *
call_setupverify(struct ast_function *, struct state *state);

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

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

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


@@ 723,73 716,28 @@ expr_call_eval(struct ast_expr *expr, struct state *state)
		state
	);

	state_pushframe(
		state,
	struct frame *call_frame = frame_call_create(
		ast_function_name(f),
		ast_function_abstract(f),
		ast_function_type(f),
		true
		state_next_execmode(state),
		ast_expr_copy(expr),
		f
	);
	state_pushframe(state, call_frame);

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

	/* XXX: pass copy so we don't observe */
	if ((err = call_setupverify(f, state_copy(state)))) {
		return result_error_create(
			error_printf(
				"`%s' precondition failure\n"
				"\t%w",
				name, err
			)
		);
	}

	struct result *res = call_absexec(expr, state);
	if (result_iserror(res)) {
	if ((err = call_setupverify(f, ast_expr_copy(expr), state_copy(state)))) {
		return result_error_create(
			error_printf("\n\t%w", result_as_error(res))
			error_printf("precondition failure: %w", err)
		);
	}

	/* XXX: pass copy so we don't observe */
	/* 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 struct result *
call_arbitraryresult(struct ast_expr *call, struct ast_function *, struct state *);

static struct result *
call_absexec(struct ast_expr *expr, struct state *s)
{
	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(s), name);
	if (!f) {
		return result_error_create(
			error_printf("function `%s' not found", name)
		);
	}
	struct result *res = ast_function_absexec(f, s);
	if (result_iserror(res) || result_hasvalue(res)) {
		return res;
	}
	return call_arbitraryresult(expr, f, s);
	return result_value_create(NULL);
}

static struct error *


@@ 797,21 745,30 @@ verify_paramspec(struct value *param, struct value *arg, struct state *param_sta
		struct state *arg_state);

static struct error *
call_setupverify(struct ast_function *f, struct state *arg_state)
call_setupverify(struct ast_function *f, struct ast_expr *call, struct state *arg_state)
{
	struct error *err;

	char *fname = ast_function_name(f);
	struct state *param_state = state_create(
	struct frame *setupframe = frame_call_create(
		fname,
		ast_function_abstract(f),
		ast_function_type(f),
		true,
		EXEC_ABSTRACT_NO_SETUP,
		ast_expr_copy(call),
		f
	);
	struct state *param_state = state_create(
		setupframe,
		state_getext(arg_state)
	);
	if ((err = ast_function_initparams(f, param_state))) {
		return err;
	}
	if ((err = ast_function_initsetup(f, param_state))) {
		assert(false);
	}

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



@@ 867,8 824,8 @@ verify_paramspec(struct value *param, struct value *arg, struct state *param_sta
	);
}

static struct result *
pf_augment(struct value *v, struct ast_expr *call, struct state *state)
struct result *
ast_expr_pf_augment(struct value *v, struct ast_expr *call, struct state *state)
{
	if (!value_isstruct(v)) {
		return result_value_create(value_copy(v));


@@ 886,16 843,16 @@ pf_augment(struct value *v, struct ast_expr *call, 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 value *
ast_expr_call_arbitrary(struct ast_expr *expr, struct ast_function *f,
		struct state *state)
{
	struct result *res = call_to_computed_value(f, state);
	if (result_iserror(res)) {
		return res;
		assert(false);
	}
	assert(result_hasvalue(res));
	return res;
	return result_as_value(res);
}

static struct result *


@@ 1084,6 1041,9 @@ static struct result *
isdereferencable_absexec(struct ast_expr *, struct state *);

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

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

struct result *


@@ 1096,10 1056,11 @@ ast_expr_abseval(struct ast_expr *expr, struct state *state)
		return isdereferencable_absexec(expr, state);
	case EXPR_ALLOCATION:
		return alloc_absexec(expr, state);
	case EXPR_CALL:
		return call_absexec(expr, state);
	case EXPR_IDENTIFIER:
	case EXPR_CONSTANT:
	case EXPR_UNARY:
	case EXPR_CALL:
	case EXPR_STRUCTMEMBER:
	case EXPR_ARBARG:
		return ast_expr_eval(expr, state);	


@@ 1109,6 1070,63 @@ ast_expr_abseval(struct ast_expr *expr, struct state *state)
}

static struct result *
call_absexec(struct ast_expr *expr, struct state *state)
{
	struct error *err;

	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) {
		return result_error_create(error_printf("`%s' not found\n", name));
	}

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

	int nargs = ast_expr_call_nargs(expr);
	if (nargs != nparams) {
		return result_error_create(
			error_printf(
				"`%s' given %d arguments instead of %d\n",
				name, nargs, nparams
			)
		);
	}

	struct result_arr *args = prepare_arguments(
		nargs, ast_expr_call_args(expr),
		nparams, params,
		state
	);

	struct frame *call_frame = frame_call_create(
		ast_function_name(f),
		ast_function_abstract(f),
		ast_function_type(f),
		state_next_execmode(state),
		ast_expr_copy(expr),
		f
	);
	state_pushframe(state, call_frame);

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

	/* XXX: pass copy so we don't observe */
	if ((err = call_setupverify(f, ast_expr_copy(expr), state_copy(state)))) {
		return result_error_create(
			error_printf("precondition failure: %w", err)
		);
	}

	return result_value_create(NULL);
}

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

/* operates at location level. It either creates an object on the heap and returns


@@ 1118,17 1136,28 @@ dealloc_process(struct ast_expr *, struct state *);
static struct result *
alloc_absexec(struct ast_expr *expr, struct state *state)
{
	struct result *res;
	switch (ast_expr_alloc_kind(expr)) {
	case ALLOC:
		/* TODO: size needs to be passed in here when added to .alloc */
		return result_value_create(state_alloc(state));
		res = result_value_create(state_alloc(state));
		break;
	case DEALLOC:
		return dealloc_process(expr, state);
		res = dealloc_process(expr, state);
		break;
	case CLUMP:
		return result_value_create(state_clump(state));
		res = result_value_create(state_clump(state));
		break;
	default:
		assert(false);
	}
	if (result_iserror(res)) {
		return res;
	}
	if (result_hasvalue(res)) {
		state_writeregister(state, result_as_value(res));
	}
	return res;
}

static struct result *


@@ 1437,3 1466,201 @@ binary_assume(struct ast_expr *expr, bool value, struct state *s)
		s
	);
}

/*
given f(x)

want:
	<rtype> t0 = f(x);


given f(g(x), y);

want:
	<rtype g> t0 = g(x);
	<rtype f> t1 = f(t0, y);
 */

static struct ast_expr *
unary_geninstr(struct ast_expr *, struct lexememarker *, struct ast_block *,
		struct state *);

static struct ast_expr *
binary_geninstr(struct ast_expr *, struct lexememarker *, struct ast_block *,
		struct state *);

static struct ast_expr *
incdec_geninstr(struct ast_expr *, struct lexememarker *, struct ast_block *,
		struct state *);

static struct ast_expr *
alloc_geninstr(struct ast_expr *, struct lexememarker *, struct ast_block *,
		struct state *);

static struct ast_expr *
assign_geninstr(struct ast_expr *, struct lexememarker *, struct ast_block *,
		struct state *);

static struct ast_expr *
call_geninstr(struct ast_expr *, struct lexememarker *, struct ast_block *,
		struct state *);

static struct ast_expr *
structmember_geninstr(struct ast_expr *, struct lexememarker *, struct ast_block *,
		struct state *);

static struct ast_expr *
bracketed_geninstr(struct ast_expr *, struct lexememarker *, struct ast_block *,
		struct state *);

struct ast_expr *
ast_expr_geninstr(struct ast_expr *expr, struct lexememarker *loc,
		struct ast_block *b, struct state *s) 
{
	switch (ast_expr_kind(expr)) {
	case EXPR_CONSTANT:
	case EXPR_ISDEALLOCAND:
	case EXPR_IDENTIFIER:
	case EXPR_STRING_LITERAL:
	case EXPR_ARBARG:
		return expr;
	case EXPR_UNARY:
		return unary_geninstr(expr, loc, b, s);	
	case EXPR_BINARY:
		return binary_geninstr(expr, loc, b, s);
	case EXPR_INCDEC:
		return incdec_geninstr(expr, loc, b, s);
	case EXPR_ALLOCATION:
		return alloc_geninstr(expr, loc, b, s);	
	case EXPR_ASSIGNMENT:
		return assign_geninstr(expr, loc, b, s);
	case EXPR_CALL:
		return call_geninstr(expr, loc, b, s);
	case EXPR_STRUCTMEMBER:
		return structmember_geninstr(expr, loc, b, s);
	case EXPR_BRACKETED:
		return bracketed_geninstr(expr, loc, b, s);
	default:
		printf("expr: %s\n", ast_expr_str(expr));
		assert(false);
	}
}

static struct ast_expr *
unary_geninstr(struct ast_expr *expr, struct lexememarker *loc, struct ast_block *b,
		struct state *s)
{
	struct ast_expr *gen_operand = ast_expr_geninstr(
		ast_expr_unary_operand(expr), loc, b, s
	);
	return ast_expr_unary_create(gen_operand, ast_expr_unary_op(expr));
}

static struct ast_expr *
binary_geninstr(struct ast_expr *expr, struct lexememarker *loc, struct ast_block *b,
		struct state *s)
{
	struct ast_expr *gen_e1 = ast_expr_geninstr(ast_expr_binary_e1(expr), loc, b, s),
			*gen_e2 = ast_expr_geninstr(ast_expr_binary_e2(expr), loc, b, s);
	return ast_expr_binary_create(gen_e1, ast_expr_binary_op(expr), gen_e2);
}

static struct ast_expr *
incdec_geninstr(struct ast_expr *expr, struct lexememarker *loc, struct ast_block *b,
		struct state *s)
{
	struct ast_expr *gen_root = ast_expr_geninstr(
		ast_expr_incdec_root(expr), loc, b, s
	);
	return ast_expr_incdec_create(
		gen_root, ast_expr_incdec_inc(expr), ast_expr_incdec_pre(expr)
	);
}

static struct ast_expr *
alloc_geninstr(struct ast_expr *expr, struct lexememarker *loc, struct ast_block *b,
		struct state *s)
{
	struct ast_expr	*gen_arg = ast_expr_geninstr(ast_expr_alloc_arg(expr), loc, b, s);
	enum ast_alloc_kind kind = ast_expr_alloc_kind(expr);

	struct ast_expr *alloc = ast_expr_alloc_kind_create(gen_arg, kind);
	struct ast_type *rtype = kind == DEALLOC
		? ast_type_create_void()
		: ast_type_create_voidptr();
	return ast_block_call_create(b, loc, rtype, alloc);
}

static struct ast_expr *
assign_geninstr(struct ast_expr *expr, struct lexememarker *loc, struct ast_block *b,
		struct state *s)
{
	struct ast_expr *lval = ast_expr_assignment_lval(expr),
			*rval = ast_expr_assignment_rval(expr);
	assert(
		ast_expr_kind(lval) == EXPR_IDENTIFIER ||
		ast_expr_kind(lval) == EXPR_UNARY ||
		ast_expr_kind(lval) == EXPR_STRUCTMEMBER
	);
	struct ast_expr *gen_rval = ast_expr_geninstr(rval, loc, b, s);
	if (!gen_rval) {
		assert(false); /* XXX: user error void func */
	}
	struct ast_expr *assign = ast_expr_assignment_create(
		ast_expr_copy(lval), gen_rval
	);
	ast_block_append_stmt(b, ast_stmt_create_expr(loc, assign));
	return lval;
}

static struct ast_expr *
call_geninstr(struct ast_expr *expr, struct lexememarker *loc,
		struct ast_block *b, struct state *s)
{
	int nargs = ast_expr_call_nargs(expr);
	struct ast_expr **args = ast_expr_call_args(expr);

	struct ast_expr **gen_args = malloc(sizeof(struct ast_expr *) * nargs);

	for (int i = 0; i < nargs; i++) {
		struct ast_expr *gen_arg = ast_expr_geninstr(args[i], loc, b, s);
		if (!gen_arg) {
			assert(false); /* XXX: user error void func */
		}
		gen_args[i] = gen_arg;
	}

	struct ast_expr *root = ast_expr_call_root(expr);
	/* XXX: handle root thats a call */
	char *name = ast_expr_as_identifier(root);
	struct ast_function *f = externals_getfunc(state_getext(s), name);
	assert(f);
	struct ast_type *rtype = ast_function_type(f);
	struct ast_expr *call = ast_expr_call_create(
		ast_expr_copy(root), nargs, gen_args
	);
	return ast_block_call_create(b, loc, rtype, call);
}

static struct ast_expr *
structmember_geninstr(struct ast_expr *expr, struct lexememarker *loc, struct ast_block *b,
		struct state *s)
{
	struct ast_expr *root_gen = ast_expr_geninstr(
		ast_expr_member_root(expr), loc, b, s
	);
	if (!root_gen) {
		assert(false); /* XXX: user error void root */
	}
	return ast_expr_member_create(root_gen, dynamic_str(ast_expr_member_field(expr)));
}

static struct ast_expr *
bracketed_geninstr(struct ast_expr *expr, struct lexememarker *loc, struct ast_block *b,
		struct state *s)
{
	struct ast_expr *gen_root = ast_expr_geninstr(
		ast_expr_bracketed_root(expr), loc, b, s
	);
	return ast_expr_bracketed_create(gen_root);
}

M src/ast/function/function.c => src/ast/function/function.c +87 -73
@@ 145,6 145,12 @@ ast_function_isproto(struct ast_function *f)
}

bool
ast_function_isvoid(struct ast_function *f)
{
	return ast_type_isvoid(f->ret);
}

bool
ast_function_absisempty(struct ast_function *f)
{
	return ast_block_ndecls(f->abstract) == 0 && ast_block_nstmts(f->abstract) == 0;


@@ 185,13 191,6 @@ ast_function_params(struct ast_function *f)
	return f->param;
}

struct preconds_result
ast_function_preconditions(struct ast_function *f)
{
	/* XXX: should we allow multiple pre tags */
	return ast_block_preconds(ast_function_abstract(f));	
}

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


@@ 219,7 218,77 @@ ast_function_verify(struct ast_function *f, struct externals *ext)
}

static struct error *
ast_function_precondsinit(struct ast_function *, struct state *);
next(struct path *);

struct error *
ast_function_debug(struct ast_function *f, struct externals *ext)
{
	struct path *path = path_create(f, ext);
	while (!path_atend(path)) {
		struct error *err = next(path);
		if (err) {
			return err;
		}
	}
	path_destroy(path);
	return NULL;
}

enum command {
	COMMAND_STEP,
	COMMAND_NEXT,
	COMMAND_QUIT,
};

static enum command
getcmd();

static struct error *
next(struct path *p)
{
	printf("(0db) ");
	switch (getcmd()) {
	case COMMAND_STEP:
		return path_step(p);
	case COMMAND_NEXT:
		return path_next(p);
	case COMMAND_QUIT:
		exit(0);
	default:
		assert(false);
	}
}

#define LINELEN 1000

static enum command
getcmd()
{
	char line[LINELEN];
	if (!fgets(line, LINELEN, stdin)) {
		fprintf(stderr, "error: cannot read\n");
		return getcmd();
	}
	if (strlen(line) != 2) {
		fprintf(stderr, "input must be single char\n");
		return getcmd();
	}
	if (line[1] != '\n') {
		fprintf(stderr, "input must be end with newline\n");
		return getcmd();
	}
	switch (*line) {
	case 's':
		return COMMAND_STEP;
	case 'n':
		return COMMAND_NEXT;
	case 'q':
		return COMMAND_QUIT;
	default:
		fprintf(stderr, "unknown command `%c'", *line);
		return getcmd();
	}
}

static struct error *
inititalise_param(struct ast_variable *v, struct state *);


@@ 235,10 304,6 @@ ast_function_initparams(struct ast_function *f, struct state *s)
		state_declare(s, params[i], true);
	}

	if ((err = ast_function_precondsinit(f, s))) {
		return err;
	}
	
	for (int i = 0; i < nparams; i++) {
		if ((err = inititalise_param(params[i], s))) {
			return err;


@@ 247,30 312,23 @@ ast_function_initparams(struct ast_function *f, struct state *s)
	return NULL;
}

static struct error *
ast_function_precondsinit(struct ast_function *f, struct state *s)
struct error *
ast_function_initsetup(struct ast_function *f, struct state *s)
{
	struct preconds_result pre = ast_function_preconditions(f);
	struct preconds_result pre = ast_block_setups(ast_function_abstract(f), s);
	if (pre.err) {
		return pre.err;
	}
	if (!pre.stmt) {
	if (!pre.b) {
		return NULL;
	}
	struct error *err = ast_stmt_absprocess(
		pre.stmt, ast_function_name(f), s, true
	struct frame *setupframe = frame_setup_create(
		"setup",
		pre.b,
		EXEC_SETUP
	);
	if (err) {
		struct lexememarker *loc = ast_stmt_lexememarker(pre.stmt); 
		assert(loc);
		char *m = lexememarker_str(loc);
		struct error *e = error_printf(
			"%s:%s: %w", 
			m, ast_function_name(f), err
		);
		free(m);
		return e;
	}
	state_pushframe(s, setupframe);
	state_initsetup(s, state_frameid(s));
	return NULL;
}



@@ 298,50 356,6 @@ inititalise_param(struct ast_variable *param, struct state *state)
	return NULL;
}


struct error *
ast_function_setupabsexec(struct ast_function *f, struct state *state)
{
	struct error *err;
	int nstmts = ast_block_nstmts(f->abstract);
	struct ast_stmt **stmt = ast_block_stmts(f->abstract);
	for (int i = 0; i < nstmts; i++) {
		if ((err = ast_stmt_setupabsexec(stmt[i], state))) {
			return err;
		}
	}
	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);
		}
	}

	char *fname = ast_function_name(f);
	int nstmts = ast_block_nstmts(f->abstract);
	struct ast_stmt **stmt = ast_block_stmts(f->abstract);
	for (int i = 0; i < nstmts; i++) {
		struct error *err = ast_stmt_absprocess(
			stmt[i], fname, state, false
		);
		if (err) {
			return result_error_create(err);
		}
	}

	/* wrap result and return */ 
	struct object_res res = state_getresult(state);
	assert(!res.err);
	return result_value_create(object_as_value(res.obj));
}

static void
recurse_buildgraph(struct map *g, struct map *dedup, char *fname, struct externals *ext);


M src/ast/gram.y => src/ast/gram.y +2 -2
@@ 877,7 877,7 @@ function_definition
#include <stdio.h>

extern struct lexememarker marker; 
extern int VERBOSE_MODE;
extern enum loglevel LOG_LEVEL;

int
yyerror(char *s)


@@ 887,7 887,7 @@ yyerror(char *s)
		fprintf(stderr, "error: %s with no lexeme marker\n", s);
		exit(EXIT_FAILURE);
	}
	if (VERBOSE_MODE) {
	if (LOG_LEVEL == LOG_INFO) {
		fprintf(stderr, "\n%*s\n", marker.column, "^");
	}
	char *mark = lexememarker_str(&marker);

M src/ast/intern.h => src/ast/intern.h +23 -0
@@ 69,4 69,27 @@ preresult_as_error(struct preresult *);
bool
preresult_iscontradiction(struct preresult *);

struct iresult;

struct iresult *
iresult_error_create(struct error *err);

struct iresult *
iresult_expr_create(struct ast_expr *val);

void
iresult_destroy(struct iresult *);

bool
iresult_iserror(struct iresult *);

struct error *
iresult_as_error(struct iresult *);

struct ast_expr *
iresult_as_expr(struct iresult *);

bool
iresult_hasexpr(struct iresult *);

#endif

M src/ast/stmt/stmt.c => src/ast/stmt/stmt.c +119 -3
@@ 41,6 41,13 @@ struct ast_stmt {
			enum ast_alloc_kind kind;
			struct ast_expr *arg;
		} alloc;
		struct {
			bool iscall;
			union {
				struct ast_expr *call;
				struct ast_variable *temp;
			} op;
		} _register;
	} u;

	struct lexememarker *loc;


@@ 87,6 94,34 @@ ast_stmt_labelled_stmt(struct ast_stmt *stmt)
	return stmt->u.labelled.stmt;
}

static struct ast_block *
ast_stmt_to_block(struct ast_stmt *);

struct ast_block *
ast_stmt_labelled_as_block(struct ast_stmt *stmt)
{
	assert(ast_stmt_ispre(stmt));
	struct ast_stmt *setup = ast_stmt_labelled_stmt(stmt);
	switch (setup->kind) {
	case STMT_EXPR:
		return ast_stmt_to_block(ast_stmt_copy(setup));
	case STMT_COMPOUND:
		return ast_block_copy(ast_stmt_as_block(setup));
	default:
		assert(false);
	}
}

static struct ast_block *
ast_stmt_to_block(struct ast_stmt *stmt)
{
	struct ast_block *b = ast_block_create(NULL, 0, NULL, 0);
	ast_block_append_stmt(b, stmt);
	return b;
}



bool
ast_stmt_ispre(struct ast_stmt *stmt)
{


@@ 377,9 412,15 @@ struct ast_expr *
ast_stmt_iter_lower_bound(struct ast_stmt *stmt)
{
	assert(stmt->kind == STMT_ITERATION);
	struct ast_stmt *init = stmt->u.iteration.init;
	assert(init->kind == STMT_EXPR);
	return ast_expr_assignment_rval(init->u.expr);
	struct ast_expr *init = ast_stmt_as_expr(stmt->u.iteration.init);
	switch (ast_expr_kind(init)) {
	case EXPR_IDENTIFIER:
		return init;
	case EXPR_ASSIGNMENT:
		return ast_expr_assignment_rval(init);
	default:
		assert(false);
	}
}

struct ast_expr *


@@ 391,6 432,45 @@ ast_stmt_iter_upper_bound(struct ast_stmt *stmt)
	return ast_expr_binary_e2(cond->u.expr);
}

struct ast_stmt *
ast_stmt_register_call_create(struct lexememarker *loc, struct ast_expr *call) {
	struct ast_stmt *stmt = ast_stmt_create(loc);
	stmt->kind = STMT_REGISTER;
	stmt->u._register.iscall = true;
	stmt->u._register.op.call = call;
	return stmt;
}

struct ast_stmt *
ast_stmt_register_mov_create(struct lexememarker *loc, struct ast_variable *temp) {
	struct ast_stmt *stmt = ast_stmt_create(loc);
	stmt->kind = STMT_REGISTER;
	stmt->u._register.iscall = false;
	stmt->u._register.op.temp = temp;
	return stmt;
}

bool
ast_stmt_register_iscall(struct ast_stmt *stmt)
{
	assert(stmt->kind == STMT_REGISTER);
	return stmt->u._register.iscall;
}

struct ast_expr *
ast_stmt_register_call(struct ast_stmt *stmt)
{
	assert(stmt->kind == STMT_REGISTER);
	return stmt->u._register.op.call;
}

struct ast_variable *
ast_stmt_register_mov(struct ast_stmt *stmt)
{
	assert(stmt->kind == STMT_REGISTER);
	return stmt->u._register.op.temp;
}

static struct ast_stmt *
ast_stmt_copy_iter(struct ast_stmt *stmt)
{


@@ 456,6 536,19 @@ ast_stmt_jump_sprint(struct ast_stmt *stmt, struct strbuilder *b)
	free(rv);
}

static void
ast_stmt_register_sprint(struct ast_stmt *stmt, struct strbuilder *b)
{
	assert(stmt->kind == STMT_REGISTER);
	if (stmt->u._register.iscall) {
		char *call = ast_expr_str(stmt->u._register.op.call);
		strbuilder_printf(b, "call %s;", call);
	} else {
		char *tempvar = ast_variable_name(stmt->u._register.op.temp);
		strbuilder_printf(b, "movret %s;", tempvar);
	}
}

static struct ast_expr *
ast_expr_copy_ifnotnull(struct ast_expr *expr)
{


@@ 558,6 651,10 @@ ast_stmt_copy(struct ast_stmt *stmt)
			loc, stmt->u.jump.kind,
			ast_expr_copy_ifnotnull(stmt->u.jump.rv)
		);
	case STMT_REGISTER:
		return stmt->u._register.iscall
			? ast_stmt_register_call_create(loc, stmt->u._register.op.call)
			: ast_stmt_register_mov_create(loc, stmt->u._register.op.temp);
	default:
		assert(false);
	}


@@ 596,6 693,9 @@ ast_stmt_str(struct ast_stmt *stmt, int indent_level)
	case STMT_JUMP:
		ast_stmt_jump_sprint(stmt, b);
		break;
	case STMT_REGISTER:
		ast_stmt_register_sprint(stmt, b);
		break;
	default:
		assert(false);
	}


@@ 619,6 719,22 @@ ast_stmt_equal(struct ast_stmt *s1, struct ast_stmt *s2)
	}
}

bool
ast_stmt_linearisable(struct ast_stmt *stmt)
{
	switch (stmt->kind) {
	case STMT_NOP:
	case STMT_LABELLED:
	case STMT_COMPOUND:
	case STMT_COMPOUND_V:
	case STMT_ITERATION_E:
	case STMT_ITERATION:
		return false;
	default:
		return true;
	}
}

enum ast_stmt_kind
ast_stmt_kind(struct ast_stmt *stmt)
{

M src/ast/stmt/stmt.h => src/ast/stmt/stmt.h +1 -0
@@ 14,6 14,7 @@ enum ast_stmt_kind {
	STMT_ITERATION_E	= 1 << 7,
	STMT_JUMP		= 1 << 8,
	STMT_ALLOCATION		= 1 << 9,
	STMT_REGISTER		= 1 << 10,
};

enum ast_stmt_kind

M src/ast/stmt/verify.c => src/ast/stmt/verify.c +315 -171
@@ 12,54 12,123 @@
#include "util.h"
#include "value.h"

static struct error *
expr_linearise(struct ast_stmt *, struct ast_block *, struct lexememarker *,
		struct state *);

static struct error *
jump_linearise(struct ast_stmt *, struct ast_block *, struct lexememarker *,
		struct state *);

static struct error *
selection_linearise(struct ast_stmt *, struct ast_block *, struct lexememarker *,
		struct state *);

static struct error *
ast_stmt_linearise_proper(struct ast_stmt *, struct ast_block *, struct lexememarker *,
		struct state *);

struct error *
ast_stmt_process(struct ast_stmt *stmt, char *fname, struct state *state)
ast_stmt_linearise(struct ast_stmt *stmt, struct state *state,
		enum execution_mode mode)
{
	struct error *err;

	if (ast_stmt_kind(stmt) == STMT_COMPOUND_V) {
		if ((err = ast_stmt_verify(stmt, state))) {
			struct lexememarker *loc = ast_stmt_lexememarker(stmt); 
			assert(loc);
			char *m = lexememarker_str(loc);
			struct error *e = error_printf("%s: %w", m, err);
			free(m);
			return e;
		}
	}
	if ((err = ast_stmt_exec(stmt, state))) {
		struct lexememarker *loc = ast_stmt_lexememarker(stmt); 
		assert(loc);
		char *m = lexememarker_str(loc);
		struct error *e = error_printf("%s:%s: %w", m, fname, err);
		free(m);
		return e;
	struct lexememarker *loc = ast_stmt_lexememarker(stmt);
	struct ast_block *b = ast_block_create(NULL, 0, NULL, 0);
	struct error *err = ast_stmt_linearise_proper(
		stmt, b, lexememarker_copy(loc), state
	);
	if (err) {
		return err;
	}
	struct frame *inter_frame = frame_intermediate_create(
		dynamic_str("inter"), b, mode
	);
	state_pushframe(state, inter_frame);
	return NULL;
}

static struct preresult *
stmt_installprop(struct ast_stmt *stmt, struct state *state);

struct preresult *
ast_stmt_preprocess(struct ast_stmt *stmt, struct state *state)
static struct error *
ast_stmt_linearise_proper(struct ast_stmt *stmt, struct ast_block *b,
		struct lexememarker *loc, struct state *state)
{
	if (ast_stmt_isassume(stmt)) {
		return stmt_installprop(stmt, state);
	switch (ast_stmt_kind(stmt)) {
	case STMT_EXPR:
		return expr_linearise(stmt, b, loc, state);
	case STMT_JUMP:
		return jump_linearise(stmt, b, loc, state);
	case STMT_SELECTION:
		return selection_linearise(stmt, b, loc, state);
	default:
		assert(false);
	}
	return preresult_empty_create();
}

static struct preresult *
stmt_installprop(struct ast_stmt *stmt, struct state *state)
static struct error *
expr_linearise(struct ast_stmt *stmt, struct ast_block *b,
		struct lexememarker *loc, struct state *state)
{
	return ast_expr_assume(ast_stmt_as_expr(ast_stmt_labelled_stmt(stmt)), state);
	struct ast_expr *expr = ast_expr_geninstr(
		ast_expr_copy(ast_stmt_as_expr(stmt)),
		lexememarker_copy(loc),
		b,
		state
	);
	return NULL;
}

/* stmt_verify */
static struct error *
jump_linearise(struct ast_stmt *stmt, struct ast_block *b, struct lexememarker *loc,
		struct state *state)
{
	struct ast_expr *rv = ast_stmt_jump_rv(stmt);

	struct ast_expr *gen = ast_expr_geninstr(
		rv, lexememarker_copy(loc), b, state
	);
	struct ast_stmt *newjump = ast_stmt_create_jump(
		lexememarker_copy(loc), JUMP_RETURN, gen
	);
	ast_block_append_stmt(b, newjump);
	return NULL;
}

static struct error *
stmt_v_block_verify(struct ast_stmt *stmt, struct state *state);
selection_linearise(struct ast_stmt *stmt, struct ast_block *b, struct lexememarker *loc,
		struct state *state)
{
	struct ast_expr *cond = ast_stmt_sel_cond(stmt);
	struct ast_stmt *body = ast_stmt_sel_body(stmt),
			*nest = ast_stmt_sel_nest(stmt);
	
	struct ast_expr *newcond = ast_expr_geninstr(
		cond, lexememarker_copy(loc), b, state
	);
	struct ast_stmt *newsel = ast_stmt_create_sel(
		lexememarker_copy(loc),
		false,
		newcond,
		ast_stmt_copy(body),
		nest ? ast_stmt_copy(nest) : NULL
	);
	ast_block_append_stmt(b, newsel);
	return NULL;
}

struct error *
ast_stmt_process(struct ast_stmt *stmt, struct state *state)
{
	struct error *err;

	if (ast_stmt_ispre(stmt)) {
		return NULL;
	}
	if ((err = ast_stmt_exec(stmt, state))) {
		return err;
	}
	return NULL;
}

/* stmt_verify */

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


@@ 73,8 142,8 @@ ast_stmt_verify(struct ast_stmt *stmt, struct state *state)
	switch (ast_stmt_kind(stmt)) {
	case STMT_NOP:
		return NULL;
	case STMT_COMPOUND_V:
		return stmt_v_block_verify(stmt, state);
	case STMT_REGISTER:
		return ast_stmt_exec(stmt, state);
	case STMT_EXPR:
		return stmt_expr_verify(stmt, state);
	case STMT_ITERATION:


@@ 84,22 153,6 @@ ast_stmt_verify(struct ast_stmt *stmt, struct state *state)
	}
}

static struct error *
stmt_v_block_verify(struct ast_stmt *v_block_stmt, struct state *state)
{
	struct ast_block *b = ast_stmt_as_v_block(v_block_stmt);
	assert(ast_block_ndecls(b) == 0); /* C89: declarations at beginning of function */
	int nstmts = ast_block_nstmts(b);
	struct ast_stmt **stmt = ast_block_stmts(b);
	for (int i = 0; i < nstmts; i++) {
		struct error *err = ast_stmt_verify(stmt[i], state);
		if (err) {
			return err;
		}
	}
	return NULL;
}

/* stmt_expr_verify */

static struct error *


@@ 154,6 207,9 @@ iter_empty(struct ast_stmt *stmt, struct state *state)
/* stmt_exec */

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

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

static struct error *


@@ 165,6 221,9 @@ stmt_iter_exec(struct ast_stmt *stmt, struct state *state);
static struct error *
stmt_jump_exec(struct ast_stmt *stmt, struct state *state);

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

struct error *
ast_stmt_exec(struct ast_stmt *stmt, struct state *state)
{


@@ 172,11 231,11 @@ ast_stmt_exec(struct ast_stmt *stmt, struct state *state)
	case STMT_NOP:
		return NULL;
	case STMT_LABELLED:
		return ast_stmt_exec(ast_stmt_labelled_stmt(stmt), state);
		assert(false);
	case STMT_COMPOUND:
		return stmt_compound_exec(stmt, state);
	case STMT_COMPOUND_V:
		return NULL;
		return stmt_compoundv_exec(stmt, state);
	case STMT_EXPR:
		return ast_expr_exec(ast_stmt_as_expr(stmt), state);
	case STMT_SELECTION:


@@ 185,29 244,34 @@ ast_stmt_exec(struct ast_stmt *stmt, struct state *state)
		return stmt_iter_exec(stmt, state);
	case STMT_JUMP:
		return stmt_jump_exec(stmt, state);
	case STMT_REGISTER:
		return stmt_register_exec(stmt, state);
	default:
		assert(false);
	}
}

/* stmt_compound_exec */
static struct error *
stmt_compoundv_exec(struct ast_stmt *stmt, struct state *state)
{
	struct frame *block_frame = frame_block_create(
		dynamic_str("verification block"),
		ast_stmt_as_block(stmt),
		EXEC_VERIFY
	);
	state_pushframe(state, block_frame);
	return NULL;
}

static struct error *
stmt_compound_exec(struct ast_stmt *stmt, struct state *state)
{
	struct ast_block *b = ast_stmt_as_block(stmt);
	assert(ast_block_ndecls(b) == 0);
	int nstmt = ast_block_nstmts(b);
	struct ast_stmt **stmts = ast_block_stmts(b);
	for (int i = 0; i < nstmt; i++) {
		struct error *err = ast_stmt_exec(stmts[i], state);
		if (err) {
			return err;
		}
		if (ast_stmt_isterminal(stmts[i], state)) {
			break;
		}
	}
	struct frame *block_frame = frame_block_create(
		dynamic_str("block"),
		ast_stmt_as_block(stmt),
		EXEC_ACTUAL
	);
	state_pushframe(state, block_frame);
	return NULL;
}



@@ 219,6 283,7 @@ stmt_sel_exec(struct ast_stmt *stmt, struct state *state)
	struct ast_expr *cond = ast_stmt_sel_cond(stmt);
	struct ast_stmt *body = ast_stmt_sel_body(stmt),
			*nest = ast_stmt_sel_nest(stmt);

	struct decision dec = sel_decide(cond, state);
	if (dec.err) {
		return dec.err;


@@ 237,7 302,7 @@ static struct ast_stmt *
iter_neteffect(struct ast_stmt *);

static struct error *
ast_stmt_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup);
ast_stmt_absexec(struct ast_stmt *stmt, struct state *state);

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


@@ 249,7 314,7 @@ stmt_iter_exec(struct ast_stmt *stmt, struct state *state)
		return NULL;
	}

	struct error *err = ast_stmt_absexec(neteffect, state, true);
	struct error *err = ast_stmt_absexec(neteffect, state);
	if (err) {
		return err;
	}


@@ 289,93 354,179 @@ iter_neteffect(struct ast_stmt *iter)
static struct error *
stmt_jump_exec(struct ast_stmt *stmt, struct state *state)
{
	/* TODO: install propositions corresponding to dereferencability */
	struct ast_expr *rv = ast_stmt_jump_rv(stmt);

	struct result *res = ast_expr_eval(ast_stmt_jump_rv(stmt), state);
	if (rv) {
		struct result *res = ast_expr_eval(rv, state);
		if (result_iserror(res)) {
			return result_as_error(res);
		}
		if (result_hasvalue(res)) {
			state_writeregister(state, result_as_value(res));
		}
	}
	return error_return();
}

static struct error *
register_call_exec(struct ast_expr *call, struct state *);

static struct error *
register_mov_exec(struct ast_variable *temp, struct state *);

static struct error *
stmt_register_exec(struct ast_stmt *stmt, struct state *state)
{
	/* XXX: assert we are in intermediate frame */
	if (ast_stmt_register_iscall(stmt)) {
		return register_call_exec(ast_stmt_register_call(stmt), state);
	} else {
		return register_mov_exec(ast_stmt_register_mov(stmt), state);
	}
}

static struct error *
register_call_exec(struct ast_expr *call, struct state *state)
{
	struct result *res = ast_expr_abseval(call, state);
	if (result_iserror(res)) {
		return result_as_error(res);
	}
	if (result_hasvalue(res)) {
		struct object_res obj_res = state_getresult(state); 
		assert(!obj_res.err);
		object_assign(obj_res.obj, value_copy(result_as_value(res)));
		/* destroy result if exists */
		
	return NULL;
}

static struct result *
hack_default_values(struct state *);

static struct error *
register_mov_exec(struct ast_variable *temp, struct state *state)
{
	state_declare(state, temp, false);

	struct result *res = hack_default_values(state);
	if (result_iserror(res)) {
		return result_as_error(res);
	}
	struct value *v = result_as_value(res);

	struct ast_expr *name = ast_expr_identifier_create(
		dynamic_str(ast_variable_name(temp))
	);
	struct lvalue_res lval_res = ast_expr_lvalue(name, state);
	if (lval_res.err) {
		return lval_res.err;
	}
	struct object *obj = lvalue_object(lval_res.lval);
	object_assign(obj, v);
	return NULL;
}

static struct result *
hack_default_values(struct state *state)
{
	struct ast_expr *expr = state_framecall(state);
	struct value *v = state_popregister(state);
	if (!v) {
		return result_value_create(NULL);
	}
	return ast_expr_pf_augment(v, expr, state);
}

struct error *
ast_stmt_absprocess(struct ast_stmt *stmt, struct state *state)
{
	/* XXX: reject undefined things for this */
	return ast_stmt_absexec(stmt, state);
}

static struct error *
ast_stmt_absexecnosetup(struct ast_stmt *, struct state *);

struct error *
ast_stmt_absprocess(struct ast_stmt *stmt, char *fname, struct state *state,
		bool should_setup)
ast_stmt_absprocess_nosetup(struct ast_stmt *stmt, struct state *state)
{
	/* XXX: reject undefined things for this */
	return ast_stmt_absexecnosetup(stmt, state);
}

static struct error *
ast_stmt_absexecnosetup(struct ast_stmt *stmt, struct state *state)
{
	struct error *err = ast_stmt_absexec(stmt, state, should_setup);
	if (!err) {
	switch (ast_stmt_kind(stmt)) {
	case STMT_LABELLED:
		return NULL;
	case STMT_NOP:
	case STMT_EXPR:
	case STMT_SELECTION:
	case STMT_ITERATION:
	case STMT_COMPOUND:
	case STMT_JUMP:
	case STMT_REGISTER:
		return ast_stmt_absexec(stmt, state);
	default:
		assert(false);
	}
	struct lexememarker *loc = ast_stmt_lexememarker(stmt); 
	assert(loc);
	char *m = lexememarker_str(loc);
	struct error *e = error_printf("%s:%s: %w", m, fname, err);
	return e;
}

static struct error *
expr_absexec(struct ast_expr *expr, struct state *state);
labelled_absexec(struct ast_stmt *, struct state *);

static struct error *
labelled_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup);
expr_absexec(struct ast_expr *, struct state *);

static struct error *
sel_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup);
sel_absexec(struct ast_stmt *stmt, struct state *);

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

static struct error *
comp_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup);
comp_absexec(struct ast_stmt *stmt, struct state *);

static struct error *
jump_absexec(struct ast_stmt *, struct state *);

static struct error *
ast_stmt_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup)
ast_stmt_absexec(struct ast_stmt *stmt, struct state *state)
{
	switch (ast_stmt_kind(stmt)) {
	case STMT_NOP:
		return NULL;
	case STMT_LABELLED:
		return labelled_absexec(stmt, state, should_setup);
		return labelled_absexec(stmt, state);
	case STMT_EXPR:
		return expr_absexec(ast_stmt_as_expr(stmt), state);
	case STMT_SELECTION:
		return sel_absexec(stmt, state, should_setup);
		return sel_absexec(stmt, state);
	case STMT_ITERATION:
		return iter_absexec(stmt, state);
	case STMT_COMPOUND:
		return comp_absexec(stmt, state, should_setup);
		return comp_absexec(stmt, state);
	case STMT_JUMP:
		return jump_absexec(stmt, state);
	case STMT_REGISTER:
		return stmt_register_exec(stmt, state);
	default:
		assert(false);
	}
}

static struct error *
labelled_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup)
labelled_absexec(struct ast_stmt *stmt, struct state *state)
{
	if (!ast_stmt_ispre(stmt)) {
		assert(false);
	}
	struct ast_stmt *setup = ast_stmt_labelled_stmt(stmt);
	if (!setup) {
		assert(false);
	}
	if (!should_setup) {
		/* if abstract is called we don't execute setup */
		return NULL;
	}
	return ast_stmt_absexec(setup, state, should_setup);
	assert(ast_stmt_ispre(stmt));
	struct ast_stmt *inner = ast_stmt_labelled_stmt(stmt);
	if (ast_stmt_kind(inner) == STMT_SELECTION) {
		return error_printf("setup preconditions must be decidable");
	}
	struct ast_block *b = ast_stmt_labelled_as_block(stmt);	
	struct frame *setup_frame = frame_block_create(
		dynamic_str("setup"),
		b,
		state_next_execmode(state)
	);
	state_pushframe(state, setup_frame);
	return NULL;
}

static struct error *


@@ 389,7 540,7 @@ expr_absexec(struct ast_expr *expr, struct state *state)
}

static struct error *
sel_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup)
sel_absexec(struct ast_stmt *stmt, struct state *state)
{
	struct ast_expr *cond = ast_stmt_sel_cond(stmt);
	struct ast_stmt *body = ast_stmt_sel_body(stmt),


@@ 399,9 550,9 @@ sel_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup)
		return dec.err;
	}
	if (dec.decision) {
		return ast_stmt_absexec(body, state, should_setup);
		return ast_stmt_absexec(body, state);
	} else if (nest) {
		return ast_stmt_absexec(nest, state, should_setup);
		return ast_stmt_absexec(nest, state);
	}
	return NULL;
}


@@ 475,117 626,110 @@ hack_alloc_from_neteffect(struct ast_stmt *stmt)
}

static struct error *
comp_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup)
comp_absexec(struct ast_stmt *stmt, struct state *state)
{
	struct ast_block *b = ast_stmt_as_block(stmt);
	struct ast_stmt **stmts = ast_block_stmts(b);
	for (int i = 0; i < ast_block_nstmts(b); i++) {
		struct error *err = ast_stmt_absexec(stmts[i], state, should_setup);
		if (err) {
			return err;
		}
	}
	struct frame *block_frame = frame_block_create(
		dynamic_str("block"),
		ast_stmt_as_block(stmt),
		state_next_execmode(state)
	);
	state_pushframe(state, block_frame);
	return NULL;
}

static struct error *
jump_absexec(struct ast_stmt *stmt, struct state *state)
{
	return expr_absexec(
		ast_expr_assignment_create(
			ast_expr_identifier_create(KEYWORD_RETURN),
			ast_stmt_jump_rv(stmt)
		), 
		state
	);
}
	struct ast_expr *rv = ast_stmt_jump_rv(stmt);

static struct error *
stmt_setupabsexec(struct ast_stmt *, struct state *);
	if (rv) {
		struct result *res = ast_expr_abseval(rv, state);
		if (result_iserror(res)) {
			return result_as_error(res);
		}
		if (result_hasvalue(res)) {
			state_writeregister(state, result_as_value(res));
		}
	}
	return error_return();
}

static struct error *
labelled_setupabsexec(struct ast_stmt *, struct state *);
labelled_buildsetup(struct ast_stmt *, struct state *, struct ast_block *);

static struct error *
sel_setupabsexec(struct ast_stmt *, struct state *);
sel_buildsetup(struct ast_stmt *, struct state *, struct ast_block *);

static struct error *
comp_setupabsexec(struct ast_stmt *, struct state *);
comp_buildsetup(struct ast_stmt *, struct state *, struct ast_block *);

struct error *
ast_stmt_setupabsexec(struct ast_stmt *stmt, struct state *state)
{
	if (ast_stmt_kind(stmt) != STMT_SELECTION) {
		return NULL;
	}
	return stmt_setupabsexec(stmt, state);
}

static struct error *
stmt_setupabsexec(struct ast_stmt *stmt, struct state *state)
{
ast_stmt_buildsetup(struct ast_stmt *stmt, struct state *state, struct ast_block *setups) {
	switch (ast_stmt_kind(stmt)) {	
	case STMT_EXPR:
	case STMT_ALLOCATION:
	case STMT_NOP:
	case STMT_JUMP:
	case STMT_REGISTER:
	case STMT_EXPR:
	case STMT_ITERATION:
		return NULL;
	case STMT_LABELLED:
		return labelled_setupabsexec(stmt, state);
		return labelled_buildsetup(stmt, state, setups);
	case STMT_SELECTION:
		return sel_setupabsexec(stmt, state);
		return sel_buildsetup(stmt, state, setups);
	case STMT_COMPOUND:
		return comp_setupabsexec(stmt, state);
		return comp_buildsetup(stmt, state, setups);
	default:
		assert(false);
	}
}

static struct error *
labelled_setupabsexec(struct ast_stmt *stmt, struct state *state)
labelled_buildsetup(struct ast_stmt *stmt, struct state *state, struct ast_block *setups)
{
	/* XXX: dedupe the execution of setups */
	struct error *err = ast_stmt_absexec(stmt, state, true);
	if (err) {
		return err;
	struct ast_block *b = ast_stmt_labelled_as_block(stmt);
	assert(ast_block_ndecls(b) == 0);
	int nstmts = ast_block_nstmts(b);
	struct ast_stmt **stmts = ast_block_stmts(b);
	for (int i = 0; i < nstmts; i++) {
		if (ast_stmt_kind(stmts[i]) == STMT_SELECTION) {
			return error_printf("setup preconditions must be decidable");
		}
		ast_block_append_stmt(setups, ast_stmt_copy(stmts[i]));	
	}
	return NULL;
}

static struct error *
sel_setupabsexec(struct ast_stmt *stmt, struct state *state)
sel_buildsetup(struct ast_stmt *stmt, struct state *state, struct ast_block *setups)
{
	struct ast_expr *cond = ast_stmt_sel_cond(stmt);
	struct ast_stmt *body = ast_stmt_sel_body(stmt),
			*nest = ast_stmt_sel_nest(stmt);
	struct decision dec = sel_decide(cond, state);
	if (dec.err) {
		return dec.err;
		v_printf("setup branch decision error: %s\n", error_str(dec.err));
		/* XXX: if error is `undecidable', must be decidable in some other branch */
		return NULL;
	}
	if (dec.decision) {
		return stmt_setupabsexec(body, state);
		return ast_stmt_buildsetup(body, state, setups);
	} else if (nest) {
		return stmt_setupabsexec(nest, state);
		return ast_stmt_buildsetup(nest, state, setups);
	}
	return NULL;
}

static struct error *
comp_setupabsexec(struct ast_stmt *stmt, struct state *state)
comp_buildsetup(struct ast_stmt *stmt, struct state *state, struct ast_block *setups)
{
	struct error *err;
	struct ast_block *b = ast_stmt_as_block(stmt);
	assert(ast_block_ndecls(b) == 0);
	int nstmt = ast_block_nstmts(b);
	int nstmts = ast_block_nstmts(b);
	struct ast_stmt **stmts = ast_block_stmts(b);
	for (int i = 0; i < nstmt; i++) {
		if (ast_stmt_ispre(stmts[i])) {
			if ((err = stmt_setupabsexec(stmts[i], state))) {
				return err;
			}
			if (ast_stmt_isterminal(stmts[i], state)) {
				break;
			}
	for (int i = 0; i < nstmts; i++) {
		struct error *err = ast_stmt_buildsetup(stmts[i], state, setups);
		if (err) {
			return err;
		}
	}
	}	
	return NULL;
}

M src/ast/type/type.c => src/ast/type/type.c +12 -0
@@ 38,6 38,12 @@ ast_type_ispointer(struct ast_type *t)
	return t->base == TYPE_POINTER;
}

bool
ast_type_isvoid(struct ast_type *t)
{
	return t->base == TYPE_VOID;
}

struct ast_type *
ast_type_create(enum ast_type_base base, enum ast_type_modifier mod)
{


@@ 58,6 64,12 @@ ast_type_create_ptr(struct ast_type *ref)
}

struct ast_type *
ast_type_create_void()
{
	return ast_type_create(TYPE_VOID, 0);
}

struct ast_type *
ast_type_create_voidptr()
{
	struct ast_type *t = ast_type_create(TYPE_POINTER, 0);

M src/main.c => src/main.c +37 -8
@@ 14,6 14,7 @@
#include "state.h"
#include "util.h"
#include "verify.h"
#include "signal.h"

/* XXX */
#define INCLUDE_ENVVAR		"XR0_INCLUDES"


@@ 40,6 41,7 @@ struct config {

	char *sortfunc;
	enum sortmode sortmode;
	bool debug;
};

static struct string_arr *


@@ 58,11 60,12 @@ parse_config(int argc, char *argv[])
{
	enum execmode mode = EXECMODE_VERIFY;
	bool verbose = false;
	bool debug = false;
	struct sortconfig sortconf = sortconfig_create(SORTMODE_NONE, "");
	struct string_arr *includedirs = default_includes();
	char *outfile = OUTPUT_PATH;
	int opt;
	while ((opt = getopt(argc, argv, "vso:t:x:I:")) != -1) {
	while ((opt = getopt(argc, argv, "vso:t:x:I:d")) != -1) {
		switch (opt) {
		case 'I':
			string_arr_append(includedirs, dynamic_str(optarg));


@@ 82,6 85,9 @@ parse_config(int argc, char *argv[])
		case 'x':
			sortconf = sortconfig_create(SORTMODE_VERIFY, optarg);
			break;
		case 'd':
			debug = true;
			break;
		default:
			fprintf(stderr, "Usage: %s [-I libx] input_file\n", argv[0]);
			exit(EXIT_FAILURE);


@@ 99,6 105,7 @@ parse_config(int argc, char *argv[])
		.verbose	= verbose,
		.sortmode	= sortconf.mode,
		.sortfunc	= sortconf.sortfunc,
		.debug		= debug
	};
}



@@ 110,7 117,6 @@ sortconfig_create(enum sortmode mode, char *sortfunc)
		return (struct sortconfig) {
			.mode = mode, .sortfunc = sortfunc,
		};

	case SORTMODE_SORT:
	case SORTMODE_VERIFY:
		if (!sortfunc) {


@@ 227,8 233,11 @@ pass0(struct ast *root, struct externals *ext)
	}
}

static struct error *
handle_debug(struct ast_function *, struct externals *, bool debug);

void
pass1(struct ast *root, struct externals *ext)
pass1(struct ast *root, struct externals *ext, bool debug)
{
	struct error *err;
	for (int i = 0; i < root->n; i++) {


@@ 242,8 251,7 @@ pass1(struct ast *root, struct externals *ext)
		}
		/* XXX: ensure that verified functions always have an abstract */
		assert(ast_function_abstract(f));

		if ((err = ast_function_verify(f, ext))) {
		if ((err = handle_debug(f, ext, debug))) {
			fprintf(stderr, "%s\n", error_str(err));
			exit(EXIT_FAILURE);
		}


@@ 251,6 259,22 @@ pass1(struct ast *root, struct externals *ext)
	}
}

static struct error *
handle_debug(struct ast_function *f, struct externals *ext, bool debug)
{
	struct error *err;
	if (debug) {
		if ((err = ast_function_debug(f, ext))) {
			return err;	
		}
	} else {
		if ((err = ast_function_verify(f, ext))) {
			return err;
		}
	}
	return NULL;
}

void
pass_inorder(struct string_arr *order, struct externals *ext)
{


@@ 340,10 364,15 @@ strip(struct config *c);
int
main(int argc, char *argv[])
{
	extern int VERBOSE_MODE;
	extern int LOG_LEVEL;

	struct config c = parse_config(argc, argv);
	VERBOSE_MODE = c.verbose;
	if (c.verbose) {
		LOG_LEVEL = LOG_INFO;
	}
	if (c.debug) {
		LOG_LEVEL = LOG_DEBUG;
	}

	switch (c.mode) {
	case EXECMODE_VERIFY:


@@ 378,7 407,7 @@ verify(struct config *c)
	struct string_arr *order;
	switch (c->sortmode) {
	case SORTMODE_NONE:
		pass1(root, ext);
		pass1(root, ext, c->debug);
		break;
	case SORTMODE_SORT:
		order = ast_topological_order(c->sortfunc, ext);

M src/path/path.c => src/path/path.c +290 -38
@@ 7,6 7,7 @@
#include "object.h"
#include "state.h"
#include "path.h"
#include "value.h"

struct path {
	enum path_state {


@@ 19,18 20,77 @@ struct path {
		PATH_STATE_ATEND,
	} path_state;
	struct state *abstract, *actual;
	struct path *p_true, *p_false;
	
	int branch_index;
	struct path_arr *paths;

	struct ast_function *f;
	struct externals *ext;
};

struct path_arr {
	int n;
	struct path **paths;
};

static struct path_arr *
path_arr_create()
{
	struct path_arr *arr = calloc(1, sizeof(struct path_arr));
	assert(arr);
	return arr;
}

static void
path_arr_destroy(struct path_arr *arr)
{
	for (int i = 0; i < arr->n; i++) {
		path_destroy(arr->paths[i]);
	}
	free(arr->paths);
	free(arr);
}

static struct path **
path_arr_s(struct path_arr *arr)
{
	return arr->paths;
}

static int
path_arr_n(struct path_arr *arr)
{
	return arr->n;
}

static int
path_arr_append(struct path_arr *arr, struct path *p)
{
	arr->paths = realloc(arr->paths, sizeof(struct path_arr) * ++arr->n);
	assert(arr->paths);
	int loc = arr->n-1;
	arr->paths[loc] = p;
	return loc;
}

static bool
path_arr_atend(struct path_arr *arr)
{
	for (int i = 0; i < arr->n; i++) {
		if (!path_atend(arr->paths[i])) {
			return false;	
		}
	}
	return true;
}

struct path *
path_create(struct ast_function *f, struct externals *ext)
{
	struct path *p = calloc(1, sizeof(struct path));
	p->f = ast_function_copy(f);
	p->ext = ext;
	p->paths = path_arr_create();
	p->path_state = PATH_STATE_UNINIT;
	return p;
}


@@ 52,14 112,24 @@ path_copywithcond(struct path *old, struct ast_expr *cond);
static void
path_split(struct path *p, struct ast_expr *cond)
{
	p->p_true = path_copywithcond(p, cond);
	p->p_false = path_copywithcond(p, ast_expr_inverted_copy(cond, true));
	path_arr_append(p->paths, path_copywithcond(p, cond));
	path_arr_append(p->paths, path_copywithcond(p, ast_expr_inverted_copy(cond, true)));
	/* TODO: destroy abstract and actual */
	p->abstract = NULL;
	p->actual = NULL;
	p->path_state = PATH_STATE_SPLIT;
}

static void
path_nextbranch(struct path *p)
{
	assert(p->paths->n >= 2);
	int index = p->branch_index;
	if (index < p->paths->n - 1) {
		p->branch_index++;	
	}
}

static struct ast_function *
copy_withcondname(struct ast_function *, struct ast_expr *cond); 



@@ 133,7 203,7 @@ path_atend(struct path *p)
{
	switch (p->path_state) {
	case PATH_STATE_SPLIT:
		return path_atend(p->p_true) && path_atend(p->p_false);
		return path_arr_atend(p->paths);
	case PATH_STATE_ATEND:
		return true;
	default:


@@ 145,13 215,13 @@ static struct error *
path_init_abstract(struct path *p);

static struct error *
path_step_abstract(struct path *p);
path_step_abstract(struct path *p, bool print);

static struct error *
path_init_actual(struct path *p);

static struct error *
path_step_actual(struct path *p);
path_step_actual(struct path *p, bool print);

static struct error *
path_step_split(struct path *p);


@@ 166,11 236,11 @@ path_step(struct path *p)
	case PATH_STATE_UNINIT:
		return path_init_abstract(p);
	case PATH_STATE_ABSTRACT:
		return path_step_abstract(p);
		return path_step_abstract(p, true);
	case PATH_STATE_HALFWAY:
		return path_init_actual(p);
	case PATH_STATE_ACTUAL:
		return path_step_actual(p);
		return path_step_actual(p, true);
	case PATH_STATE_AUDIT:
		return path_audit(p);
	case PATH_STATE_SPLIT:


@@ 182,19 252,177 @@ path_step(struct path *p)
}

static struct error *
path_next_abstract(struct path *);

static struct error *
path_next_actual(struct path *);

static struct error *
path_next_split(struct path *);

struct error *
path_next(struct path *p)
{
	switch (p->path_state) {
	case PATH_STATE_UNINIT:
		return path_step(p);
	case PATH_STATE_ABSTRACT:
		return path_next_abstract(p);
	case PATH_STATE_HALFWAY:
		return path_step(p);
	case PATH_STATE_ACTUAL:
		return path_next_actual(p);
	case PATH_STATE_AUDIT:
		return path_audit(p);
	case PATH_STATE_SPLIT:
		return path_next_split(p);
	case PATH_STATE_ATEND:
	default:
		assert(false);
	}
}

static bool
path_continue(struct path *, enum path_state og_state, int og_frame,
		int og_index);

static struct error *
path_next_abstract(struct path *p)
{
	struct error *err;

	int og_frame = state_frameid(p->abstract);
	int og_index = state_programindex(p->abstract);
	if ((err = path_step(p))) {
		return err;
	}
	while (path_continue(p, PATH_STATE_ABSTRACT, og_frame, og_index)) {
		if ((err = path_step_abstract(p, false))) {
			return err;
		}
	}
	return NULL;
}

static struct error *
branch_next(struct path *parent, struct path *branch);

static struct error *
path_next_split(struct path *p)
{
	assert(!path_arr_atend(p->paths));
	struct path_arr *p_arr = p->paths;
	struct error *err = branch_next(p, p_arr->paths[p->branch_index]);
	if (err) {
		return err;
	}
	return NULL;
}

static struct error *
branch_next(struct path *parent, struct path *branch)
{
	d_printf("branch: %d\n", parent->branch_index);
	if (path_atend(branch)) {
		path_nextbranch(parent);
		return NULL;
	}
	return path_next(branch);
}

static bool
path_insamestate(struct path *, enum path_state og_state);

static bool
path_inlowerframe(struct path *p, enum path_state og_state, int og_frameid);

static bool
path_insamestmt(struct path *p, enum path_state og_state, int og_frameid,
		int og_program_index);

static bool
path_continue(struct path *p, enum path_state og_state, int og_frame,
		int og_index)
{
	return path_insamestate(p, og_state) &&
		(path_inlowerframe(p, og_state, og_frame) ||
		path_insamestmt(p, og_state, og_frame, og_index));
}

static bool
path_insamestate(struct path *p, enum path_state og_state)
{
	return p->path_state == og_state;
}

static bool
path_inlowerframe(struct path *p, enum path_state og_state, int og_frame)
{
	switch (og_state) {
	case PATH_STATE_ABSTRACT:
		return og_frame < state_frameid(p->abstract);
	case PATH_STATE_ACTUAL:
		return og_frame < state_frameid(p->actual);
	default:
		assert(false);
	}
}

static bool
path_insamestmt(struct path *p, enum path_state og_state, int og_frame, int og_index)
{
	struct state *s;
	switch (og_state) {
	case PATH_STATE_ABSTRACT:
		s = p->abstract;
		break;
	case PATH_STATE_ACTUAL:
		s = p->actual;
		break;
	default:
		assert(false);
	}
	return og_frame == state_frameid(s) &&
		og_index == state_programindex(s);
}

static struct error *
path_next_actual(struct path *p)
{
	struct error *err;

	int og_frame = state_frameid(p->actual);
	int og_index = state_programindex(p->actual);
	if ((err = path_step(p))) {
		return err;
	}
	while (path_continue(p, PATH_STATE_ACTUAL, og_frame, og_index)) {
		if ((err = path_step_actual(p, false))) {
			return err;
		}
	}
	return NULL;
}

static struct error *
path_init_abstract(struct path *p)
{
	p->abstract = state_create(
	struct error *err;

	d_printf("init abstract state\n");
	struct frame *f = frame_call_create(
		ast_function_name(p->f),
		ast_function_abstract(p->f),
		ast_function_type(p->f),
		true,
		p->ext
		EXEC_ABSTRACT,
		ast_expr_identifier_create(dynamic_str("base abs")), /* XXX */
		p->f
	);
	struct error *err = ast_function_initparams(p->f, p->abstract);
	if (err) {
	p->abstract = state_create(f, p->ext);
	if ((err = ast_function_initparams(p->f, p->abstract))) {
		return err;
	}
	state_clearregister(p->abstract);
	p->path_state = PATH_STATE_ABSTRACT;
	return NULL;
}


@@ 202,30 430,42 @@ path_init_abstract(struct path *p)
static struct error *
path_init_actual(struct path *p)
{
	p->actual = state_create_withprops(
	struct error *err;
	d_printf("init actual state\n");
	/* if body empty just apply setup */
	struct frame *f = frame_call_create(
		ast_function_name(p->f),
		ast_function_body(p->f),
		ast_function_type(p->f),
		false,
		EXEC_ACTUAL,
		ast_expr_identifier_create(dynamic_str("base act")), /* xxx */
		p->f
	);
	p->actual = state_create_withprops(
		f,
		p->ext,
		state_getprops(p->abstract)
	);
	struct error *err = ast_function_initparams(p->f, p->actual);
	if (err) {
	if ((err = ast_function_initparams(p->f, p->actual))) {
		return err;
	}
	err = ast_function_setupabsexec(p->f, p->actual);
	if (err) {
	if ((err = ast_function_initsetup(p->f, p->actual))) {
		return err;
	}
	state_clearregister(p->actual);
	p->path_state = PATH_STATE_ACTUAL;
	return NULL;
}

static struct error *
path_step_abstract(struct path *p)
path_step_abstract(struct path *p, bool print)
{
	if (state_atend(p->abstract)) {
	if (print) {
		d_printf("mode:%d\n", state_execmode(p->abstract));
		d_printf("text:\n%s\n", state_programtext(p->abstract));
		d_printf("abstract: %s\n", state_str(p->abstract));
	}
	if (state_atend(p->abstract) && state_frameid(p->abstract) == 0) {
		p->path_state = PATH_STATE_HALFWAY;
		return path_step(p);
	}


@@ 235,17 475,22 @@ path_step_abstract(struct path *p)
		return NULL;
	}
	struct error *uc_err = error_to_undecideable_cond(err);
	if (!uc_err) {
		return err;
	if (uc_err) {
		path_split(p, error_get_undecideable_cond(uc_err));
		return NULL;
	}
	path_split(p, error_get_undecideable_cond(uc_err));
	return NULL;
	return state_stacktrace(p->abstract, err);
}

static struct error *
path_step_actual(struct path *p)
path_step_actual(struct path *p, bool print)
{
	if (state_atend(p->actual)) {
	if (print) {
		d_printf("mode:%d\n", state_execmode(p->actual));
		d_printf("text:\n%s\n", state_programtext(p->actual));
		d_printf("actual: %s\n", state_str(p->actual));
	}
	if (state_atend(p->actual) && state_frameid(p->actual) == 0) {
		p->path_state = PATH_STATE_AUDIT;
		return path_step(p);
	}


@@ 255,18 500,19 @@ path_step_actual(struct path *p)
		return NULL;
	}
	struct error *uc_err = error_to_undecideable_cond(err);
	if (!uc_err) {
		return err;
	if (uc_err) {
		path_split(p, error_get_undecideable_cond(uc_err));
		return NULL;
	}
	path_split(p, error_get_undecideable_cond(uc_err));
	return NULL;
	return state_stacktrace(p->actual, err);
}

static struct error *
path_audit(struct path *p)
{
	d_printf("audit\n");
	if (state_hasgarbage(p->actual)) {
		v_printf("actual: %s", state_str(p->actual));
		d_printf("actual: %s", state_str(p->actual));
		return error_printf(
			"%s: garbage on heap", ast_function_name(p->f)
		);


@@ 284,23 530,29 @@ path_audit(struct path *p)
}

static struct error *
path_trystep(struct path *p);
branch_step(struct path *parent, struct path *branch);

static struct error *
path_step_split(struct path *p)
{
	/* path_atend holds this invariant whenever this function is called */ 
	assert(!path_atend(p->p_true) || !path_atend(p->p_false));
	assert(!path_arr_atend(p->paths));

	struct error *err = path_trystep(p->p_true);
	struct path_arr *p_arr = p->paths;
	struct error *err = branch_step(p, p_arr->paths[p->branch_index]);
	if (err) {
		return err;
	}
	return path_trystep(p->p_false);
	return NULL;	
}

static struct error *
path_trystep(struct path *p)
branch_step(struct path *parent, struct path *branch)
{
	return path_atend(p) ? NULL : path_step(p);
	d_printf("branch: %d\n", parent->branch_index);
	if (path_atend(branch)) {
		path_nextbranch(parent);
		return NULL;
	}
	return path_step(branch);
}

M src/props/props.c => src/props/props.c +1 -1
@@ 82,7 82,7 @@ props_get(struct props *p, struct ast_expr *e)
		if (ast_expr_equal(e, p->prop[i])) {
			return true;
		}
	}
	}	
	return false;
}


M src/state/location.c => src/state/location.c +5 -1
@@ 228,9 228,13 @@ location_toheap(struct location *loc, struct heap *h)
bool
location_tostack(struct location *loc, struct stack *s)
{
	if (loc->type != LOCATION_AUTOMATIC) {
		return false;
	}
	bool type_equal = loc->type == LOCATION_AUTOMATIC;
	/* XXX: should probably check that frame is greater than current frame */
	struct block *b = stack_getblock(s, loc->block);
	struct stack *frame = stack_getframe(s, loc->u.frame);
	struct block *b = stack_getblock(frame, loc->block);
	return type_equal && b;
}


A src/state/program.c => src/state/program.c +238 -0
@@ 0,0 1,238 @@
#include <stdlib.h>
#include <stdio.h>
#include <assert.h>

#include "ast.h"
#include "lex.h"
#include "program.h"
#include "state.h"
#include "util.h"

struct program {
	struct ast_block *b;
	enum program_state {
		PROGRAM_COUNTER_DECLS,
		PROGRAM_COUNTER_STMTS,
		PROGRAM_COUNTER_ATEND,
	} s;
	int index;
	struct lexememarker *loc;
};

static enum program_state
program_state_init(struct ast_block *);

struct program *
program_create(struct ast_block *b)
{
	struct program *p = malloc(sizeof(struct program));
	p->b = b;
	p->s = program_state_init(b);
	p->index = 0;
	p->loc = NULL;
	return p;
}

void
program_setatend(struct program *p)
{
	p->s = PROGRAM_COUNTER_ATEND;
}

void
program_storeloc(struct program *p)
{
	if (ast_block_nstmts(p->b) > 0) {
		p->loc = ast_stmt_lexememarker(ast_block_stmts(p->b)[p->index]);
	}
}

static enum program_state
program_state_init(struct ast_block *b)
{
	return ast_block_ndecls(b)
		? PROGRAM_COUNTER_DECLS
		: ast_block_nstmts(b)
		? PROGRAM_COUNTER_STMTS
		: PROGRAM_COUNTER_ATEND;
}

void
program_destroy(struct program *p)
{
	/* no ownership of block */
	free(p);
}

struct program *
program_copy(struct program *old)
{
	struct program *new = program_create(old->b);
	new->s = old->s;
	new->index = old->index;
	return new;
}

char *
program_str(struct program *p)
{
	struct strbuilder *b = strbuilder_create();
	strbuilder_printf(b, "%s\n", ast_block_str(p->b, 1));
	return strbuilder_build(b);
}

int
program_index(struct program *p)
{
	return p->index;
}

char *
program_render(struct program *p)
{
	struct strbuilder *b = strbuilder_create();
	switch (p->s) {
	case PROGRAM_COUNTER_DECLS:
		strbuilder_printf(b, "%s", ast_block_render(p->b, p->index, true));
		break;
	case PROGRAM_COUNTER_STMTS:
		strbuilder_printf(b, "%s", ast_block_render(p->b, p->index, false));
		break;
	case PROGRAM_COUNTER_ATEND:
		strbuilder_printf(b, "\t<end of frame>");
		break;
	default:
		assert(false);
	}
	return strbuilder_build(b);
}

bool
program_atend(struct program *p)
{
	return p->s == PROGRAM_COUNTER_ATEND;
}

struct ast_expr *
program_prevcall(struct program *p)
{
	assert(p->s == PROGRAM_COUNTER_STMTS);
	struct ast_stmt *c = ast_block_stmts(p->b)[p->index-1];
	return ast_expr_copy(ast_stmt_register_call(c));
}

static void
program_nextdecl(struct program *p)
{
	assert(p->s == PROGRAM_COUNTER_DECLS);

	if (++p->index >= ast_block_ndecls(p->b)) {
		p->s = ast_block_nstmts(p->b)
			? PROGRAM_COUNTER_STMTS
			: PROGRAM_COUNTER_ATEND;
		p->index = 0;
	}
}

static bool
program_stmt_atend(struct program *, struct state *);

static void
program_nextstmt(struct program *p, struct state *s)
{
	assert(p->s == PROGRAM_COUNTER_STMTS);

	++p->index;
	if (program_stmt_atend(p, s)) {
		p->s = PROGRAM_COUNTER_ATEND;
	}
}

static bool
program_stmt_atend(struct program *p, struct state *s)
{
	return p->index >= ast_block_nstmts(p->b);
}

static struct error *
program_stmt_step(struct program *, enum execution_mode, struct state *);

struct error *
program_exec(struct program *p, enum execution_mode mode, struct state *s)
{
	switch (p->s) {
	case PROGRAM_COUNTER_DECLS:
		state_declare(s, ast_block_decls(p->b)[p->index], false);
		program_nextdecl(p);
		return NULL;
	case PROGRAM_COUNTER_STMTS:
		return program_stmt_step(p, mode, s);
	case PROGRAM_COUNTER_ATEND:
		state_popframe(s);
		return NULL;
	default:
		assert(false);
	}
}

static struct error *
program_stmt_process(struct program *p, enum execution_mode mode, struct state *s);

static struct error *
program_stmt_step(struct program *p, enum execution_mode mode, struct state *s)
{
	struct error *err = program_stmt_process(p, mode, s);
	if (!err) {
		program_nextstmt(p, s);
		return NULL;
	}
	struct error *return_err = error_to_return(err);
	if (return_err) {
		state_return(s);
		return NULL;
	}
	return err;
}

static struct error *
program_stmt_process(struct program *p, enum execution_mode mode, struct state *s)
{
	struct ast_stmt *stmt = ast_block_stmts(p->b)[p->index];
	if (!state_islinear(s) && ast_stmt_linearisable(stmt)) {
		return ast_stmt_linearise(stmt, s, mode);
	}
	switch (mode) {
	case EXEC_ABSTRACT:
		return ast_stmt_absprocess(stmt, s);
	case EXEC_ABSTRACT_NO_SETUP:
	case EXEC_SETUP:
		return ast_stmt_absprocess_nosetup(stmt, s);
	case EXEC_ACTUAL:
		return ast_stmt_process(stmt, s);
	case EXEC_VERIFY:
		return ast_stmt_verify(stmt, state_copy(s));
	default:
		assert(false);
	}
}

char *
program_loc(struct program *p)
{
	if (p->loc) {
		return lexememarker_str(p->loc);
	}
	switch (p->s) {
	case PROGRAM_COUNTER_STMTS:
		return lexememarker_str(
			ast_stmt_lexememarker(ast_block_stmts(p->b)[p->index])
		);
	case PROGRAM_COUNTER_ATEND:
		assert(p->index && ast_block_stmts(p->b)); /* i.e., it's nonzero */
		return lexememarker_str(
			ast_stmt_lexememarker(ast_block_stmts(p->b)[p->index-1])
		);
	default:
		assert(false);
	}
}

A src/state/program.h => src/state/program.h +44 -0
@@ 0,0 1,44 @@
#ifndef PROGRAM_H
#define PROGRAM_H

struct program;

struct program *
program_create(struct ast_block *);

struct program *
program_copy(struct program *);

void
program_destroy(struct program *);

char *
program_str(struct program *);

int
program_index(struct program *);

void
program_storeloc(struct program *);

char *
program_render(struct program *);

void
program_setatend(struct program *);

bool
program_atend(struct program *);

struct ast_expr *
program_prevcall(struct program *);

enum execution_mode;

struct error *
program_exec(struct program *, enum execution_mode, struct state *);

char *
program_loc(struct program *);

#endif

M src/state/stack.c => src/state/stack.c +302 -223
@@ 11,48 11,39 @@
#include "object.h"
#include "value.h"
#include "util.h"
#include "program.h"

struct program_counter;

static struct program_counter *
program_counter_create(struct ast_block *, char *name);

static struct program_counter *
program_counter_copy(struct program_counter *);

static void
program_counter_destroy(struct program_counter *);

static char *
program_counter_name(struct program_counter *);

static void
program_counter_changename(struct program_counter *, char *);

static bool
program_counter_atend(struct program_counter *);

static struct error *
program_counter_exec(struct program_counter *, bool abstract, struct state *);
struct frame;

struct stack {
	struct program_counter *pc;
	bool abstract;

	struct block_arr *frame;

	/* lvalues of blocks in frame */
	struct map *varmap;
	struct variable *result;

	int id;
	struct program *p;
	struct block_arr *memory;
	struct map *varmap;		/* lvalues of blocks in frame */
	struct stack *prev;

	char *name;
	enum execution_mode mode;
	enum frame_kind kind;
	struct ast_expr *call;
	struct ast_function *f;
};

struct frame {
	char *name;
	struct ast_block *b;
	struct ast_type *ret_type;
	enum execution_mode mode;
	enum frame_kind kind;
	struct ast_expr *call;
	struct ast_function *f;
	bool advance;
};

struct location *
stack_newblock(struct stack *stack)
{
	int address = block_arr_append(stack->frame, block_create());
	int address = block_arr_append(stack->memory, block_create());
	struct location *loc = location_create_automatic(
		stack->id, address, ast_expr_constant_create(0)
	);


@@ 60,27 51,36 @@ stack_newblock(struct stack *stack)
}

struct stack *
stack_create(char *name, struct ast_block *b, struct ast_type *ret_type,
		bool abstract, struct stack *prev)
stack_create(struct frame *f, struct stack *prev)
{
	struct stack *stack = calloc(1, sizeof(struct stack));
	assert(stack);

	assert(b);
	stack->pc = program_counter_create(b, name);
	stack->abstract = abstract;
	stack->frame = block_arr_create();

	assert(f->b);
	stack->p = program_create(f->b);
	stack->memory = block_arr_create();
	stack->varmap = map_create();

	stack->prev = prev;
	stack->id = prev ? prev->id + 1 : 0;

	stack->result = variable_create(ret_type, stack, false);
	stack->name = f->name;
	stack->mode = f->mode;
	stack->kind = f->kind;
	if (stack->kind == FRAME_CALL) {
		stack->call = f->call;
		stack->f = f->f;
	}

	return stack;
}

int
stack_id(struct stack *s)
{
	assert(s);
	return s->id;
}

struct stack *
stack_getframe(struct stack *s, int frame)
{


@@ 96,10 96,46 @@ stack_getframe(struct stack *s, int frame)
	return stack_getframe(s->prev, frame);
}

char *
stack_programtext(struct stack *s)
{
	return program_render(s->p);
}

int
stack_programindex(struct stack *s)
{
	return program_index(s->p);
}

void
stack_return(struct stack *s)
{
	program_setatend(s->p);
	if (s->prev && s->kind != FRAME_CALL) {
		stack_return(s->prev);
	}
}

struct ast_expr *
stack_framecall(struct stack *s)
{
	switch (s->kind) {
	case FRAME_CALL:
		assert(s->call);
		return s->call;
	case FRAME_INTERMEDIATE:
		return program_prevcall(s->p);
	default:
		assert(false);
	}
	return NULL;
}

void
stack_destroy(struct stack *stack)
{
	block_arr_destroy(stack->frame);
	block_arr_destroy(stack->memory);

	struct map *m = stack->varmap;
	for (int i = 0; i < m->n; i++) {


@@ 107,9 143,9 @@ stack_destroy(struct stack *stack)
	}
	map_destroy(m);

	variable_destroy(stack->result);
	/* XXX: call expr leak */

	program_counter_destroy(stack->pc);
	program_destroy(stack->p);
	free(stack);
}



@@ 126,26 162,44 @@ struct stack *
stack_copy(struct stack *stack)
{
	struct stack *copy = calloc(1, sizeof(struct stack));
	copy->abstract = stack->abstract;
	copy->pc = program_counter_copy(stack->pc);
	copy->frame = block_arr_copy(stack->frame);
	copy->mode = stack->mode;
	copy->p = program_copy(stack->p);
	copy->memory = block_arr_copy(stack->memory);
	copy->varmap = varmap_copy(stack->varmap);
	copy->id = stack->id;
	copy->result = variable_copy(stack->result);
	if (stack->prev) {
		copy->prev = stack_copy(stack->prev);
	}
	copy->name = dynamic_str(stack->name);
	copy->kind = stack->kind;
	if (stack->kind == FRAME_CALL) {
		copy->call = ast_expr_copy(stack->call);
		copy->f = ast_function_copy(stack->f);
	}
	return copy;
}

static void
rename_lowestframe(struct stack *, char *new_name);

struct stack *
stack_copywithname(struct stack *stack, char *new_name)
{
	struct stack *copy = stack_copy(stack);
	program_counter_changename(copy->pc, new_name);
	rename_lowestframe(copy, new_name);
	return copy;
}

static void
rename_lowestframe(struct stack *s, char *new_name)
{
	if (s->prev) {
		rename_lowestframe(s->prev, new_name);
	} else {
		s->name = new_name;
	}
}

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


@@ 173,15 227,12 @@ stack_str(struct stack *stack, struct state *state)
		free(var);
		strbuilder_putc(b, '\n');
	}
	char *result = variable_str(stack->result, stack, state);
	strbuilder_printf(b, "\treturn: %s\n", result);
	free(result);
	strbuilder_printf(b, "\t");
	/* TODO: fix length of line */
	for (int i = 0, len = 30; i < len-2; i++ ) {
		strbuilder_putc(b, '-');
	}
	strbuilder_printf(b, " %s\n", program_counter_name(stack->pc));
	strbuilder_printf(b, " %s\n", stack->name);
	if (stack->prev) {
		char *prev = stack_str(stack->prev, state);
		strbuilder_printf(b, prev);


@@ 191,15 242,33 @@ stack_str(struct stack *stack, struct state *state)
}

bool
stack_islinear(struct stack *s)
{
	return s->kind == FRAME_INTERMEDIATE;
}

enum execution_mode
stack_execmode(struct stack *s)
{
	return s->mode;
}

bool
stack_atend(struct stack *s)
{
	return !s->prev && program_counter_atend(s->pc);
	return program_atend(s->p);
}

struct error *
stack_step(struct stack *s, struct state *state)
{
	return program_counter_exec(s->pc, s->abstract, state);
	return program_exec(s->p, s->mode, state);
}

void
stack_storeloc(struct stack *s)
{
	program_storeloc(s->p);
}

void


@@ 220,10 289,6 @@ variable_abstractcopy(struct variable *v, struct state *s);
void
stack_undeclare(struct stack *stack, struct state *state)
{
	struct variable *old_result = stack->result;
	stack->result = variable_abstractcopy(old_result, state);
	variable_destroy(old_result);

	struct map *m = stack->varmap;
	stack->varmap = map_create();
	for (int i = 0; i < m->n; i++) {


@@ 240,10 305,79 @@ stack_undeclare(struct stack *stack, struct state *state)
	map_destroy(m);
}

struct variable *
stack_getresult(struct stack *s)
static bool
stack_iscall(struct stack *s)
{
	return s->kind == FRAME_CALL;
}

bool
stack_isnested(struct stack *s)
{
	return s->kind == FRAME_NESTED;
}

static char *
stack_propername(struct stack *);

static char *
stack_context(struct stack *);

struct error *
stack_trace(struct stack *s, struct error *err)
{
	if (s->kind != FRAME_CALL) {
		assert(s->prev);
		return stack_trace(s->prev, err);
	}

	struct strbuilder *b = strbuilder_create();

	char *loc = program_loc(s->p);
	char *err_str = error_str(err);
	strbuilder_printf(b, "%s: %s (%s)", loc, err_str, stack_propername(s));
	free(err_str);
	free(loc);
	if (s->prev) {
		char *context = stack_context(s->prev);
		if (strlen(context)) {
			strbuilder_printf(b, "%s", context);
		}
		free(context);

		char *msg = strbuilder_build(b);
		struct error *trace_err = error_printf("%s", msg);
		free(msg);
		return trace_err;
	}
	char *msg = strbuilder_build(b);
	struct error *e = error_printf("%s", msg);
	free(msg);
	return e;
}

static char *
stack_propername(struct stack *s)
{
	return s->result;
	return s->kind == FRAME_CALL ? s->name : stack_propername(s->prev);
}

static char *
stack_context(struct stack *s)
{
	struct strbuilder *b = strbuilder_create();
	if (s->kind == FRAME_CALL) {
		char *loc = program_loc(s->p);
		strbuilder_printf(b, "\t%s (%s)", loc, stack_propername(s));
		free(loc);
	}
	if (s->prev) {
		char *prev = stack_context(s->prev);
		if (strlen(prev)) {
			strbuilder_printf(b, "\n%s", prev);
		}
	}
	return strbuilder_build(b);
}

struct map *


@@ 257,15 391,35 @@ stack_getvariable(struct stack *s, char *id)
{
	assert(strcmp(id, KEYWORD_RETURN) != 0);

	return map_get(s->varmap, id);
	struct variable *v = map_get(s->varmap, id);
	if (!v && !stack_iscall(s)) {
		/* ⊢ block */
		return stack_getvariable(s->prev, id);
	}
	return v;
}

void
stack_popprep(struct stack *s, struct state *state)
{
	if (s->kind == FRAME_CALL && !ast_function_isvoid(s->f)) {
		struct value *v = state_readregister(state);
		if (!v) {
			state_writeregister(
				state,
				ast_expr_call_arbitrary(s->call, s->f, state)
			);
		}
	}
}

bool
stack_references(struct stack *s, struct location *loc, struct state *state)
{
	/* TODO: check globals */
	struct variable *result = stack_getresult(s);
	if (result && variable_references(result, loc, state)) {
	struct value *result = state_popregister(state);
	struct circuitbreaker *c = circuitbreaker_create();
	if (result && value_references(result, loc, state, c)) {
		return true;
	}



@@ 283,9 437,90 @@ stack_references(struct stack *s, struct location *loc, struct state *state)
struct block *
stack_getblock(struct stack *s, int address)
{
	assert(address < block_arr_nblocks(s->frame));
	assert(address < block_arr_nblocks(s->memory));

	return block_arr_blocks(s->memory)[address];
}

static struct frame *
frame_create(char *n, struct ast_block *b, struct ast_type *r, enum execution_mode mode,
		enum frame_kind kind)
{
	struct frame *f = malloc(sizeof(struct frame));
	f->name = dynamic_str(n);
	f->b = ast_block_copy(b);
	if (kind == FRAME_CALL) {
		assert(r);
		f->ret_type = ast_type_copy(r);
	}
	f->mode = mode;
	f->kind = kind;
	f->call = NULL;
	f->f = NULL;
	f->advance = true;
	return f;
}

	return block_arr_blocks(s->frame)[address];
struct frame *
frame_call_create(char *n, struct ast_block *b, struct ast_type *r, enum execution_mode mode, struct ast_expr *call, struct ast_function *func)
{
	struct frame *f = frame_create(n, b, r, mode, FRAME_CALL);
	f->call = call;
	f->f = func;
	return f;
}

struct frame *
frame_block_create(char *n, struct ast_block *b, enum execution_mode mode)
{
	return frame_create(n, b, NULL, mode, FRAME_NESTED);
}

struct frame *
frame_setup_create(char *n, struct ast_block *b, enum execution_mode mode)
{
	struct frame* f = frame_create(n, b, NULL, mode, FRAME_NESTED);
	f->advance = false;
	return f;
}

struct frame *
frame_intermediate_create(char *n, struct ast_block *b, enum execution_mode mode)
{
	return frame_create(n, b, NULL, mode, FRAME_INTERMEDIATE);
}

bool
frame_advance(struct frame *f)
{
	return f->advance;
}

static struct frame *
frame_copy(struct frame *f)
{
	if (f->kind == FRAME_CALL) {
		assert(f->ret_type);
	}
	struct frame *copy = frame_create(
		dynamic_str(f->name),
		ast_block_copy(f->b),
		f->ret_type ? ast_type_copy(f->ret_type) : NULL,
		f->mode,
		f->kind
	); 
	if (f->kind == FRAME_CALL) {
		copy->f = ast_function_copy(f->f);
		copy->call = ast_expr_copy(f->call);
	}
	copy->advance = f->advance;
	return copy;
}

static void
frame_destroy(struct frame *f)
{
	assert(false);
}




@@ 414,159 649,3 @@ variable_isparam(struct variable *v)
{
	return v->isparam;
}


struct program_counter {
	struct ast_block *b;
	enum program_counter_state {
		PROGRAM_COUNTER_DECLS,
		PROGRAM_COUNTER_STMTS,
		PROGRAM_COUNTER_ATEND,
	} s;
	char *name;
	int index;
};

static enum program_counter_state
program_counter_state_init(struct ast_block *);

struct program_counter *
program_counter_create(struct ast_block *b, char *name)
{
	struct program_counter *pc = malloc(sizeof(struct program_counter));
	pc->b = b;
	pc->s = program_counter_state_init(b);
	pc->index = 0;
	pc->name = dynamic_str(name);
	return pc;
}

static enum program_counter_state
program_counter_state_init(struct ast_block *b)
{
	return ast_block_ndecls(b)
		? PROGRAM_COUNTER_DECLS
		: ast_block_nstmts(b)
		? PROGRAM_COUNTER_STMTS
		: PROGRAM_COUNTER_ATEND;
}

static void
program_counter_destroy(struct program_counter *pc)
{
	/* no ownership of block */
	free(pc->name);
	free(pc);
}

static struct program_counter *
program_counter_copy(struct program_counter *old)
{
	struct program_counter *new = program_counter_create(old->b, old->name);
	new->s = old->s;
	new->index = old->index;
	return new;
}

static char *
program_counter_name(struct program_counter *pc)
{
	return pc->name;
}

static void
program_counter_changename(struct program_counter *pc, char *new_name)
{
	free(pc->name);
	pc->name = dynamic_str(new_name);
}

static bool
program_counter_atend(struct program_counter *pc)
{
	return pc->s == PROGRAM_COUNTER_ATEND;
}

static void
program_counter_nextdecl(struct program_counter *pc)
{
	assert(pc->s == PROGRAM_COUNTER_DECLS);

	if (++pc->index >= ast_block_ndecls(pc->b)) {
		pc->s = ast_block_nstmts(pc->b)
			? PROGRAM_COUNTER_STMTS
			: PROGRAM_COUNTER_ATEND;
		pc->index = 0;
	}
}

static bool
program_counter_stmt_atend(struct program_counter *, struct state *);

static void
program_counter_nextstmt(struct program_counter *pc, struct state *s)
{
	assert(pc->s == PROGRAM_COUNTER_STMTS);

	if (program_counter_stmt_atend(pc, s)) {
		pc->s = PROGRAM_COUNTER_ATEND;
	}
}

static bool
program_counter_stmt_atend(struct program_counter *pc, struct state *s)
{
	return ast_stmt_isterminal(ast_block_stmts(pc->b)[pc->index], s)
		|| ++pc->index >= ast_block_nstmts(pc->b);
}


static struct error *
program_counter_stmt_step(struct program_counter *pc, bool abstract, 
		struct state *s);

static struct error *
program_counter_exec(struct program_counter *pc, bool abstract, struct state *s)
{
	switch (pc->s) {
	case PROGRAM_COUNTER_DECLS:
		state_declare(s, ast_block_decls(pc->b)[pc->index], false);
		program_counter_nextdecl(pc);
		return NULL;
	case PROGRAM_COUNTER_STMTS:
		return program_counter_stmt_step(pc, abstract, s);
	case PROGRAM_COUNTER_ATEND:
	default:
		assert(false);
	}
}

static struct error *
program_counter_stmt_process(struct program_counter *pc, bool abstract, 
		struct state *s);

static struct error *
program_counter_stmt_step(struct program_counter *pc, bool abstract, 
		struct state *s)
{
	struct error *err = program_counter_stmt_process(pc, abstract, s);
	if (err) {
		return err;
	}
	program_counter_nextstmt(pc, s);
	return NULL;
}

static struct error *
program_counter_stmt_process(struct program_counter *pc, bool abstract, 
		struct state *s)
{
	struct ast_stmt *stmt = ast_block_stmts(pc->b)[pc->index];
	if (abstract) {
		if (ast_stmt_ispre(stmt)) {
			return NULL;
		}
		return ast_stmt_absprocess(stmt, pc->name, s, true);
	}
	return ast_stmt_process(stmt, pc->name, s);
}

M src/state/stack.h => src/state/stack.h +43 -6
@@ 6,15 6,31 @@

struct stack;

struct frame;

struct stack *
stack_create(char *name, struct ast_block *, struct ast_type *ret_type,
		bool abstract, struct stack *prev);
stack_create(struct frame *, struct stack *prev);

struct stack *
stack_getframe(struct stack *s, int frame);
stack_getframe(struct stack *, int frame);

char *
stack_programtext(struct stack *);

int
stack_programindex(struct stack *);

void
stack_return(struct stack *);

struct ast_expr *
stack_framecall(struct stack *);

int
stack_id(struct stack *);

struct location *
stack_newblock(struct stack *stack);
stack_newblock(struct stack *);

void
stack_destroy(struct stack *);


@@ 29,22 45,40 @@ char *
stack_str(struct stack *, struct state *);

bool
stack_islinear(struct stack *);

enum execution_mode
stack_execmode(struct stack *);

bool
stack_atend(struct stack *);

struct error *
stack_step(struct stack *, struct state *);

void
stack_nextstmt(struct stack *s, struct state *state);

struct stack *
stack_prev(struct stack *);

void
stack_popprep(struct stack *, struct state *);

void
stack_storeloc(struct stack *);

void
stack_declare(struct stack *, struct ast_variable *var, bool isparam);

void
stack_undeclare(struct stack *stack, struct state *state);

struct variable *
stack_getresult(struct stack *);
bool
stack_isnested(struct stack *);

struct error *
stack_trace(struct stack *, struct error *);

struct map *
stack_getvarmap(struct stack *);


@@ 60,6 94,9 @@ struct ast_expr;
struct block *
stack_getblock(struct stack *, int address);


/* variable */

struct ast_type;

struct variable;

M src/state/state.c => src/state/state.c +146 -35
@@ 26,11 26,11 @@ struct state {
	struct stack *stack;
	struct heap *heap;
	struct props *props;
	struct value *reg;
};

struct state *
state_create(char *name, struct ast_block *block, struct ast_type *ret_type,
		bool abstract, struct externals *ext)
state_create(struct frame *f, struct externals *ext)
{
	struct state *state = malloc(sizeof(struct state));
	assert(state);


@@ 38,18 38,18 @@ state_create(char *name, struct ast_block *block, struct ast_type *ret_type,
	state->static_memory = static_memory_create();
	state->vconst = vconst_create();
	state->clump = clump_create();
	state->stack = stack_create(name, block, ret_type, abstract, NULL);
	state->stack = stack_create(f, NULL);
	state->heap = heap_create();
	state->props = props_create();
	state->reg = NULL;
	return state;
}

struct state *
state_create_withprops(char *name, struct ast_block *block,
		struct ast_type *ret_type, bool abstract, struct externals *ext,
state_create_withprops(struct frame *f, struct externals *ext,
		struct props *props)
{
	struct state *state = state_create(name, block, ret_type, abstract, ext);
	struct state *state = state_create(f, ext);
	state->props = props_copy(props);
	return state;
}


@@ 78,6 78,7 @@ state_copy(struct state *state)
	copy->stack = stack_copy(state->stack);
	copy->heap = heap_copy(state->heap);
	copy->props = props_copy(state->props);
	copy->reg = state->reg ? value_copy(state->reg) : NULL;
	return copy;
}



@@ 99,6 100,11 @@ state_str(struct state *state)
		strbuilder_printf(b, "%s\n", ext);
	}
	free(ext);
	strbuilder_printf(
		b,
		"\treturn: {<type> := {%s}}\n\n",
		state->reg ? value_str(state->reg) : "empty"
	);
	char *static_mem = static_memory_str(state->static_memory, "\t");
	if (strlen(static_mem) > 0) {
		strbuilder_printf(b, "%s\n", static_mem);


@@ 134,6 140,18 @@ state_str(struct state *state)
}

bool
state_islinear(struct state *s)
{
	return stack_islinear(s->stack);
}

enum execution_mode
state_execmode(struct state *s)
{
	return stack_execmode(s->stack);
}

bool
state_atend(struct state *s)
{
	return stack_atend(s->stack);


@@ 145,7 163,6 @@ state_step(struct state *s)
	return stack_step(s->stack, s);
}


struct externals *
state_getext(struct state *s)
{


@@ 164,16 181,36 @@ state_getprops(struct state *s)
	return s->props;
}

char *
state_programtext(struct state *s)
{
	return stack_programtext(s->stack);
}

int
state_programindex(struct state *s)
{
	return stack_programindex(s->stack);
}

int
state_frameid(struct state *s)
{
	return stack_id(s->stack);
}

void
state_pushframe(struct state *state, char *name, struct ast_block *b,
		struct ast_type *t, bool abstract)
state_pushframe(struct state *state, struct frame *f)
{
	state->stack = stack_create(name, b, t, abstract, state->stack);
	stack_storeloc(state->stack);
	state->stack = stack_create(f, state->stack);
}

void
state_popframe(struct state *state)
{
	stack_popprep(state->stack, state);

	struct stack *old = state->stack;
	state->stack = stack_prev(old); /* pop */
	assert(state->stack);


@@ 202,6 239,82 @@ state_vconst(struct state *state, struct ast_type *t, char *comment, bool persis
}

struct value *
state_popregister(struct state *state)
{
	//v_printf("reading from register: %s\n", state->reg ? value_str(state->reg) : "NULL");
	if (!state->reg) {
		return NULL;
	}
	struct value *v = value_copy(state->reg);
	if (state_frameid(state) != 0) {
		state->reg = NULL;
	}
	return v;
}

struct value *
state_readregister(struct state *state)
{
	//v_printf("reading from register: %s\n", state->reg ? value_str(state->reg) : "NULL");
	return state->reg;
}

void
state_writeregister(struct state *state, struct value *v)
{
	assert(!state->reg);
	//v_printf("writing to register: %s\n", v ? value_str(v) : "NULL");
	state->reg = v;
}

void
state_clearregister(struct state *state)
{
	/* XXX: used after initing the actual state */
	state->reg = NULL;
}

void
state_initsetup(struct state *s, int frameid)
{
	struct error *err;
	
	assert(state_execmode(s) == EXEC_SETUP);
	while (!(state_atend(s) && state_frameid(s) == frameid)) {
		if ((err = state_step(s))) {
			assert(false);
		}
	}
}

enum execution_mode
state_next_execmode(struct state *s)
{
	if (stack_execmode(s->stack) == EXEC_ABSTRACT) {
		return EXEC_ABSTRACT;
	}
	return EXEC_ABSTRACT_NO_SETUP;
}

struct error *
state_stacktrace(struct state *s, struct error *err)
{
	return stack_trace(s->stack, err);
}

void
state_return(struct state *s)
{
	stack_return(s->stack);	
}

struct ast_expr *
state_framecall(struct state *s)
{
	return stack_framecall(s->stack);
}

struct value *
state_static_init(struct state *state, struct ast_expr *expr)
{
	char *lit = ast_expr_as_literal(expr);


@@ 321,33 434,12 @@ state_getblock(struct state *state, struct location *loc)
	return res.b;
}

struct object_res
state_getresult(struct state *state)
{
	struct variable *v = stack_getresult(state->stack);
	assert(v);

	struct object_res res = state_get(state, variable_location(v), true);
	if (res.err) {
		assert(false);
	}
	return res;
}

static struct ast_type *
state_getresulttype(struct state *state)
{
	struct variable *v = stack_getresult(state->stack);
	assert(v);

	return variable_type(v);
}

struct ast_type *
state_getobjecttype(struct state *state, char *id)
{
	if (strcmp(id, KEYWORD_RETURN) == 0) {
		return state_getresulttype(state);
		assert(false);
		//return state_getresulttype(state);
	}

	struct variable *v = stack_getvariable(state->stack, id);


@@ 369,7 461,8 @@ struct object_res
state_getobject(struct state *state, char *id)
{
	if (strcmp(id, KEYWORD_RETURN) == 0) {
		return state_getresult(state);
		assert(false);
		/*return state_getresult(state);*/
	}

	struct variable *v = stack_getvariable(state->stack, id);


@@ 538,11 631,16 @@ state_undeclarevars(struct state *s);
static void
state_popprops(struct state *s);

void
state_unnest(struct state *s);

bool
state_equal(struct state *s1, struct state *s2)
{
	struct state *s1_c = state_copy(s1),
		     *s2_c = state_copy(s2);
	state_unnest(s1_c);
	state_unnest(s2_c);
	state_undeclareliterals(s1_c);
	state_undeclareliterals(s2_c);
	state_undeclarevars(s1_c);


@@ 576,9 674,14 @@ state_undeclareliterals(struct state *s)

static void
state_undeclarevars(struct state *s)
{
{	
	heap_undeclare(s->heap, s);
	vconst_undeclare(s->vconst);
	struct value *v = state_readregister(s);
	if (v) {
		/* XXX: avoid state_writeregister assert */
		s->reg = value_abstractcopy(v, s);
	}
	stack_undeclare(s->stack, s);
}



@@ 588,3 691,11 @@ state_popprops(struct state *s)
	props_destroy(s->props);
	s->props = props_create();
}

void
state_unnest(struct state *s)
{
	while (stack_isnested(s->stack)) {
		state_popframe(s);
	}
}

M src/util/util.c => src/util/util.c +34 -3
@@ 288,14 288,27 @@ string_arr_str(struct string_arr *string_arr)
	return strbuilder_build(b);
}

int VERBOSE_MODE;
enum loglevel LOG_LEVEL;

/* d_printf: Print if Xr0 is in debug mode. */
int
d_printf(char *fmt, ...)
{
	if (LOG_LEVEL != LOG_DEBUG) {
		return 0;
	}
	va_list ap;
	va_start(ap, fmt);
	int r = vfprintf(stderr, fmt, ap);
	va_end(ap);
	return r;
}

/* v_printf: Print if Xr0 is in verbose mode. */
int
v_printf(char *fmt, ...)
{
	if (!VERBOSE_MODE) {
	if (LOG_LEVEL != LOG_INFO) {
		return 0;
	}
	va_list ap;


@@ 309,6 322,7 @@ struct error {
	enum error_type {
		ERROR_PRINTF,
		ERROR_UNDECIDEABLE_COND,
		ERROR_RETURN,
	} type;
	union error_contents {
		char *printf;


@@ 320,6 334,7 @@ struct error {
static struct error *
error_to(struct error *err, enum error_type t)
{
	assert(err);
	if (err->type == t) {
		return err;
	}


@@ 425,17 440,33 @@ error_get_undecideable_cond(struct error *err)
	return err->contents.undecidable_cond;
}

struct error *
error_return()
{
	struct error *err = calloc(1, sizeof(struct error));
	err->type = ERROR_RETURN;
	return err;
}

struct error *
error_to_return(struct error *err)
{
	return error_to(err, ERROR_RETURN);
}

char *
error_str(struct error *err)
{
	char *error_type_str[] = {
		[ERROR_UNDECIDEABLE_COND] = "undecideable condition"
		[ERROR_UNDECIDEABLE_COND] = "undecideable condition",
		[ERROR_RETURN] = "returned",
	};

	switch (err->type) {
	case ERROR_PRINTF:
		return dynamic_str(err->contents.printf);
	case ERROR_UNDECIDEABLE_COND:
	case ERROR_RETURN:
		return dynamic_str(error_type_str[err->type]);
	default:
		assert(false);

M src/value/value.c => src/value/value.c +2 -0
@@ 474,6 474,7 @@ value_sync_sprint(struct value *v, struct strbuilder *b)
struct value *
value_copy(struct value *v)
{
	assert(v);
	switch (v->type) {
	case VALUE_SYNC:
		return value_sync_copy(v);


@@ 744,6 745,7 @@ values_comparable(struct value *v1, struct value *v2)
bool
value_equal(struct value *v1, struct value *v2)
{
	assert(v1 && v2);
	assert(v1->type == v2->type);

	switch (v1->type) {

M tests/0-basic/030-alloc.x => tests/0-basic/030-alloc.x +1 -1
@@ 6,6 6,6 @@ unit() ~ [ return .malloc(1); ]
	void *p;

	p = malloc(1);
	~ [ @p; ]
	//~ [ @p; ]
	return p;
}

M tests/0-basic/130-FAIL-double-free.x.EXPECTED => tests/0-basic/130-FAIL-double-free.x.EXPECTED +2 -2
@@ 1,2 1,2 @@
0-basic/130-FAIL-double-free.x:10:9:unit: 
	stdlib.h:10:31:free: double free
stdlib.h:10:31: double free (free)
	0-basic/130-FAIL-double-free.x:10:9 (unit)

M tests/0-basic/140-FAIL-sync-free.x.EXPECTED => tests/0-basic/140-FAIL-sync-free.x.EXPECTED +2 -2
@@ 1,2 1,2 @@
0-basic/140-FAIL-sync-free.x:6:9:unit: 
	stdlib.h:10:31:free: undefined free of value not pointing at heap
stdlib.h:10:31: undefined free of value not pointing at heap (free)
	0-basic/140-FAIL-sync-free.x:6:9 (unit)

M tests/0-basic/170-FAIL-double-free.x.EXPECTED => tests/0-basic/170-FAIL-double-free.x.EXPECTED +2 -2
@@ 1,2 1,2 @@
0-basic/170-FAIL-double-free.x:11:9:unit: 
	stdlib.h:10:31:free: double free
stdlib.h:10:31: double free (free)
	0-basic/170-FAIL-double-free.x:11:9 (unit)

M tests/1-branches/0100-body-trivial.x => tests/1-branches/0100-body-trivial.x +1 -1
@@ 6,5 6,5 @@ test(int x) ~ [ return .malloc(1); ]
	if (x) {
		return malloc(1);
	}
	return malloc(1);
	return malloc(2);
}

A tests/1-branches/1300-nested-branch-return.x => tests/1-branches/1300-nested-branch-return.x +22 -0
@@ 0,0 1,22 @@
#include <stdlib.h>

void
foo(int a, int b)
{
       int *p;
       p = malloc(1);
       if (a) {
               free(p);
               if (b) {
                       return NULL;
               }
       }
       if (b) {
               free(p);
       }
       if (!a) {
               if (!b) {
                       free(p);
               }
       }
}

M tests/5-pass-by-ptr/000-basic.x => tests/5-pass-by-ptr/000-basic.x +1 -1
@@ 1,6 1,6 @@
#include <stdlib.h>

void *
void
assign(void *p) ~ [
	setup: p = .clump(1);
	*p = 1;

M tests/6-preconditions/100-FAIL-need-alloced-lval.x.EXPECTED => tests/6-preconditions/100-FAIL-need-alloced-lval.x.EXPECTED +2 -2
@@ 1,2 1,2 @@
6-preconditions/100-FAIL-need-alloced-lval.x:15:10:main: `func' precondition failure
	parameter `x' of `func' must be heap allocated
6-preconditions/100-FAIL-need-alloced-lval.x:5:23: precondition failure: parameter `x' of `func' must be heap allocated (func)
	6-preconditions/100-FAIL-need-alloced-lval.x:15:10 (main)

M tests/6-preconditions/101-FAIL-need-alloced-rval.x => tests/6-preconditions/101-FAIL-need-alloced-rval.x +0 -1
@@ 2,7 2,6 @@

int
func(int *x) ~ [ 
	int i;
	setup: {
		x = .malloc(1);
		*x = $;

M tests/6-preconditions/101-FAIL-need-alloced-rval.x.EXPECTED => tests/6-preconditions/101-FAIL-need-alloced-rval.x.EXPECTED +2 -2
@@ 1,2 1,2 @@
6-preconditions/101-FAIL-need-alloced-rval.x:21:13:main: `func' precondition failure
	parameter `x' of `func' must be rvalue
6-preconditions/101-FAIL-need-alloced-rval.x:8:2: precondition failure: parameter `x' of `func' must be rvalue (func)
	6-preconditions/101-FAIL-need-alloced-rval.x:20:13 (main)

M tests/6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x.EXPECTED => tests/6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x.EXPECTED +2 -2
@@ 1,2 1,2 @@
6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x:16:9:main: `func' precondition failure
	parameter `x' of `func' must be lvalue
6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x:5:22: precondition failure: parameter `x' of `func' must be lvalue (func)
	6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x:16:9 (main)

M tests/6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x.EXPECTED => tests/6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x.EXPECTED +2 -2
@@ 1,2 1,2 @@
6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x:16:9:main: `func' precondition failure
	parameter `x' of `func' must be lvalue
6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x:5:22: precondition failure: parameter `x' of `func' must be lvalue (func)
	6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x:16:9 (main)

M tests/7-use-after-free/002-pass-in-lvalue.x => tests/7-use-after-free/002-pass-in-lvalue.x +1 -3
@@ 1,8 1,6 @@
void
modify(int *q) ~ [
	setup: {
		q = .clump(sizeof(int));
	}
	setup: q = .clump(sizeof(int));
	*q = 2;
] {
	*q = 2;

M tests/7-use-after-free/005-conditions.x => tests/7-use-after-free/005-conditions.x +5 -5
@@ 27,13 27,13 @@ main()
{
	int p;
	p = 0;
	~ [ p == 0; ];
	~ [ p == 0; ]
	modify0(&p, 0);
	~ [ p == 0; ];
	~ [ p == 0; ]
	modify0(&p, 1);
	~ [ p == 1; ];
	~ [ p == 1; ]
	modify1(&p, 0);
	~ [ p == 1; ];
	~ [ p == 1; ]
	modify1(&p, 1);
	~ [ p == 2; ];
	~ [ p == 2; ]
}

M tests/7-use-after-free/100-FAIL-lvalue-use-after-free.x.EXPECTED => tests/7-use-after-free/100-FAIL-lvalue-use-after-free.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
7-use-after-free/100-FAIL-lvalue-use-after-free.x:11:8:func: undefined indirection: *(p) is not an lvalue
7-use-after-free/100-FAIL-lvalue-use-after-free.x:11:8: undefined indirection: *(p) is not an lvalue (func)

M tests/7-use-after-free/101-FAIL-rvalue-use-after-free.x.EXPECTED => tests/7-use-after-free/101-FAIL-rvalue-use-after-free.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
7-use-after-free/101-FAIL-rvalue-use-after-free.x:12:8:func: undefined indirection: *(p+0) has no value
7-use-after-free/101-FAIL-rvalue-use-after-free.x:12:8: undefined indirection: *(p+0) has no value (func)

M tests/7-use-after-free/110-FAIL-freed-ptr-dangling-return.x.EXPECTED => tests/7-use-after-free/110-FAIL-freed-ptr-dangling-return.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
7-use-after-free/110-FAIL-freed-ptr-dangling-return.x:21:8:main: undefined indirection: *(i+0) has no value
7-use-after-free/110-FAIL-freed-ptr-dangling-return.x:21:8: undefined indirection: *(i+0) has no value (main)

M tests/7-use-after-free/112-FAIL-freed-ptr-dangling-false-claim.x.EXPECTED => tests/7-use-after-free/112-FAIL-freed-ptr-dangling-false-claim.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
7-use-after-free/112-FAIL-freed-ptr-dangling-false-claim.x:21:8:main: undefined indirection: *(i+0) has no value
7-use-after-free/112-FAIL-freed-ptr-dangling-false-claim.x:21:8: undefined indirection: *(i+0) has no value (main)

M tests/7-use-after-free/120-FAIL-freed-ptr-maybe-dangling-return.x.EXPECTED => tests/7-use-after-free/120-FAIL-freed-ptr-maybe-dangling-return.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
7-use-after-free/120-FAIL-freed-ptr-maybe-dangling-return.x:34:8:main: undefined indirection: *(j) is not an lvalue
7-use-after-free/120-FAIL-freed-ptr-maybe-dangling-return.x:34:8: undefined indirection: *(j) is not an lvalue (main)

M tests/7-use-after-free/200-FAIL-stack-frame-pop-dangling-return.x.EXPECTED => tests/7-use-after-free/200-FAIL-stack-frame-pop-dangling-return.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
7-use-after-free/200-FAIL-stack-frame-pop-dangling-return.x:19:8:main: undefined indirection: *(p+0) has no value
7-use-after-free/200-FAIL-stack-frame-pop-dangling-return.x:19:8: undefined indirection: *(p+0) has no value (main)

M tests/7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x.EXPECTED => tests/7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x:27:8:main: undefined indirection: stack frame doesn't exist
7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x:27:8: undefined indirection: stack frame doesn't exist (main)

M tests/7-use-after-free/300-FAIL-struct-free-ptr-dangling.x.EXPECTED => tests/7-use-after-free/300-FAIL-struct-free-ptr-dangling.x.EXPECTED +2 -2
@@ 1,2 1,2 @@
7-use-after-free/300-FAIL-struct-free-ptr-dangling.x:45:18:create_report: `puts' precondition failure
	parameter `s' of `puts' must be lvalue
stdio.h:18:39: precondition failure: parameter `s' of `puts' must be lvalue (puts)
	7-use-after-free/300-FAIL-struct-free-ptr-dangling.x:45:18 (create_report)

M tests/7-use-after-free/400-FAIL-conditions-in-setup.x.EXPECTED => tests/7-use-after-free/400-FAIL-conditions-in-setup.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
7-use-after-free/400-FAIL-conditions-in-setup.x:4:3 setup preconditions must be decidable
7-use-after-free/400-FAIL-conditions-in-setup.x:4:3: setup preconditions must be decidable (modify2)

M tests/8-uninitialised-memory/000-FAIL-uninitialised-memory-rval.x.EXPECTED => tests/8-uninitialised-memory/000-FAIL-uninitialised-memory-rval.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
8-uninitialised-memory/000-FAIL-uninitialised-memory-rval.x:7:7:main: undefined memory access: `j' has no value
8-uninitialised-memory/000-FAIL-uninitialised-memory-rval.x:7:7: undefined memory access: `j' has no value (main)

M tests/8-uninitialised-memory/001-FAIL-uninitialised-memory-rval.x.EXPECTED => tests/8-uninitialised-memory/001-FAIL-uninitialised-memory-rval.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
8-uninitialised-memory/001-FAIL-uninitialised-memory-rval.x:7:8:undefined_memory1: undefined memory access: `p' has no value
8-uninitialised-memory/001-FAIL-uninitialised-memory-rval.x:7:8: undefined memory access: `p' has no value (undefined_memory1)

M tests/8-uninitialised-memory/002-FAIL-uninitialised-memory-rval.x.EXPECTED => tests/8-uninitialised-memory/002-FAIL-uninitialised-memory-rval.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
8-uninitialised-memory/002-FAIL-uninitialised-memory-rval.x:9:8:undefined_memory2: undefined indirection: *(q+0) has no value
8-uninitialised-memory/002-FAIL-uninitialised-memory-rval.x:9:8: undefined indirection: *(q+0) has no value (undefined_memory2)

M tests/8-uninitialised-memory/003-FAIL-uninitialised-memory-rval.x.EXPECTED => tests/8-uninitialised-memory/003-FAIL-uninitialised-memory-rval.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
8-uninitialised-memory/003-FAIL-uninitialised-memory-rval.x:10:8:undefined_memory3: undefined indirection: *(p+0) has no value
8-uninitialised-memory/003-FAIL-uninitialised-memory-rval.x:10:8: undefined indirection: *(p+0) has no value (undefined_memory3)

M tests/8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x.EXPECTED => tests/8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x.EXPECTED +2 -1
@@ 1,1 1,2 @@
8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x:12:9:main: undefined memory access: `i' has no value
8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x:3:10: undefined memory access: `i' has no value (func)
	8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x:12:9 (main)

A tests/9-calls/complex-call-expressions.x => tests/9-calls/complex-call-expressions.x +28 -0
@@ 0,0 1,28 @@
#include <stdlib.h>

int
f(int x, int y) ~ [ return 0; ]
{
	return 0;
}

int
g(int x) ~ [ return 1; ]
{
	return 1;
}

int
h(int x, int y) ~ [ return 2; ]
{
	return 2;
}

void *
test(int x, int y) ~ [ return .malloc(1); ]
{
	if (f(g(x), h(f(x, y), f(g(x), y)))) {
		return malloc(1);
	}
	return malloc(1);
}

M tests/99-program/000-matrix.x => tests/99-program/000-matrix.x +2 -6
@@ 7,7 7,7 @@ struct matrix {
};

struct matrix *
matrix_create(int rows, int cold) ~ [
matrix_create(int rows, int cols) ~ [
	struct matrix *m;
	int i;



@@ 19,11 19,7 @@ matrix_create(int rows, int cold) ~ [
		m->data[i] = .malloc(sizeof(int));	
	}
	return m;
];

struct matrix *
matrix_create(int rows, int cols)
{
]{
	int i;
	struct matrix *m;


M tests/run => tests/run +0 -1
@@ 19,7 19,6 @@ cd tests
length=$(ls */*.x | awk '{ print length, $0 }' | sort -n -s | cut -d' ' -f2- |
	tail -1 | wc -c)


for f in */*.x
do
	ntests=$((ntests+1))