~lbnz/xr0

f4d890167ac4d5db58c64af7a794d978f6d47c9d — Xr0 Team 2 months ago 68e96dc v0.15.0
feat: track progress using stack program counter

resolves: https://github.com/xr0-org/xr0/issues/42
M Makefile => Makefile +8 -1
@@ 17,6 17,7 @@ SRC_0V_DIR = $(SRC_DIR)

EXT_DIR = $(SRC_0V_DIR)/ext
PROPS_DIR = $(SRC_0V_DIR)/props
PATH_DIR = $(SRC_0V_DIR)/path
STATE_DIR = $(SRC_0V_DIR)/state
OBJECT_DIR = $(SRC_0V_DIR)/object
VALUE_DIR = $(SRC_0V_DIR)/value


@@ 38,6 39,7 @@ LOCATION_OBJ = $(BUILD_DIR)/location.o
BLOCK_OBJ = $(BUILD_DIR)/block.o
EXT_OBJ = $(BUILD_DIR)/ext.o
PROPS_OBJ = $(BUILD_DIR)/props.o
PATH_OBJ = $(BUILD_DIR)/path.o
OBJECT_OBJ = $(BUILD_DIR)/object.o
VALUE_OBJ = $(BUILD_DIR)/value.o
MATH_OBJ = $(BUILD_DIR)/math.o


@@ 67,7 69,8 @@ STATE_OBJECTS = $(VALUE_OBJ) \
		$(STACK_OBJ) \
		$(STATIC_OBJ) \
		$(EXT_OBJ) \
		$(PROPS_OBJ)
		$(PROPS_OBJ) \
		$(PATH_OBJ)

OBJECTS = $(XR0_OBJECTS) $(STATE_OBJECTS)



@@ 122,6 125,10 @@ $(PROPS_OBJ): $(PROPS_DIR)/props.c
	@printf 'CC\t$@\n'
	@$(CC) $(CFLAGS) -o $@ -c $(PROPS_DIR)/props.c

$(PATH_OBJ): $(PATH_DIR)/path.c
	@printf 'CC\t$@\n'
	@$(CC) $(CFLAGS) -o $@ -c $(PATH_DIR)/path.c

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

M include/ast.h => include/ast.h +6 -0
@@ 551,6 551,9 @@ ast_function_destroy(struct ast_function *);
char *
ast_function_str(struct ast_function *f);

void
ast_function_setname(struct ast_function *f, char *name);

char *
ast_function_name(struct ast_function *f);



@@ 595,6 598,9 @@ ast_function_verify(struct ast_function *, struct externals *);

struct result;

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

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


A include/path.h => include/path.h +25 -0
@@ 0,0 1,25 @@
#ifndef XR0_PATH
#define XR0_PATH

#include <stdbool.h>

struct ast_function;
struct externals;
struct state;
struct error;

struct path;

struct path *
path_create(struct ast_function *, struct externals *);

void
path_destroy(struct path *);

bool
path_atend(struct path *);

struct error *
path_step(struct path *);

#endif

M include/state.h => include/state.h +14 -3
@@ 6,6 6,7 @@
#define KEYWORD_RETURN "return"

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


@@ 25,10 26,12 @@ struct value;
struct state;

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

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

struct state *


@@ 43,6 46,12 @@ state_destroy(struct state *state);
char *
state_str(struct state *);

bool
state_atend(struct state *);

struct error *
state_step(struct state *);

struct externals *
state_getext(struct state *);



@@ 53,11 62,13 @@ struct heap *
state_getheap(struct state *);

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

void
state_popframe(struct state *);


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


M src/ast/expr/verify.c => src/ast/expr/verify.c +12 -5
@@ 706,7 706,6 @@ expr_call_eval(struct ast_expr *expr, struct state *state)

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

	int nargs = ast_expr_call_nargs(expr);
	if (nargs != nparams) {


@@ 724,7 723,13 @@ expr_call_eval(struct ast_expr *expr, struct state *state)
		state
	);

	state_pushframe(state, dynamic_str(name), rtype);
	state_pushframe(
		state,
		ast_function_name(f),
		ast_function_abstract(f),
		ast_function_type(f),
		true
	);
	if ((err = prepare_parameters(nparams, params, args, name, state))) {
		return result_error_create(err);
	}


@@ 798,9 803,11 @@ call_setupverify(struct ast_function *f, struct state *arg_state)

	char *fname = ast_function_name(f);
	struct state *param_state = state_create(
		dynamic_str(fname),
		state_getext(arg_state),
		ast_function_type(f)
		fname,
		ast_function_abstract(f),
		ast_function_type(f),
		true,
		state_getext(arg_state)
	);
	if ((err = ast_function_initparams(f, param_state))) {
		return err;

M src/ast/function/function.c => src/ast/function/function.c +16 -331
@@ 10,6 10,7 @@
#include "intern.h"
#include "object.h"
#include "props.h"
#include "path.h"
#include "state.h"
#include "type/type.h"
#include "stmt/stmt.h"


@@ 99,6 100,13 @@ ast_function_str(struct ast_function *f)
	return strbuilder_build(b);
}

void
ast_function_setname(struct ast_function *f, char *name)
{
	free(f->name);
	f->name = name;
}

char *
ast_function_name(struct ast_function *f)
{


@@ 197,90 205,16 @@ ast_function_protostitch(struct ast_function *f, struct externals *ext)
}

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

static struct error *
path_absverify_withstate(struct ast_function *f, struct state *);

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

struct error *
ast_function_verify(struct ast_function *f, struct externals *ext)
{
	struct error *err;
	struct state *state = state_create(
		dynamic_str(ast_function_name(f)), ext, ast_function_type(f)
	);
	if ((err = ast_function_initparams(f, state))) {
		return err;
	}
	if ((err = path_absverify_withstate(f, state))) {
		return err;
	}
	state_destroy(state);
	return NULL;
}

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

static struct error *
path_absverify_withstate(struct ast_function *f, struct state *state)
{
	struct ast_block *abs = ast_function_abstract(f);

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

	return path_absverify(f, state, 0);
}

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

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

static struct error *
path_absverify(struct ast_function *f, struct state *state, int index)
{
	struct ast_block *abs = ast_function_abstract(f);

	char *fname = ast_function_name(f);
	int nstmts = ast_block_nstmts(abs);
	struct ast_stmt **stmt = ast_block_stmts(abs);
	for (int i = index; i < nstmts; i++) {
		if (ast_stmt_ispre(stmt[i])) {
			continue;
		}
		struct state *prestate = state_copy(state);
		struct error *err = ast_stmt_absprocess(
			stmt[i], fname, state, true
		);
	struct path *path = path_create(f, ext);
	while (!path_atend(path)) {
		struct error *err = path_step(path);
		if (err) {
			struct error *uc_err = error_to_undecideable_cond(err);
			if (!uc_err) {
				return err;
			}
			return split_path_absverify(
				f, prestate, i,
				error_get_undecideable_cond(uc_err)
			);
		}	
		state_destroy(prestate);
		/* result_destroy(res); */
	}
	
	/* TODO: verify that `result' is of same type as f->result */
	struct error *err = NULL;
	if ((err = abstract_audit(f, state))) {
		return err;
			return err;
		}
	}
	path_destroy(path);
	return NULL;
}



@@ 364,42 298,8 @@ inititalise_param(struct ast_variable *param, struct state *state)
	return NULL;
}

static struct error *
ast_function_setupabsexec(struct ast_function *f, struct state *state);

static struct error *
path_verify(struct ast_function *, struct state *state, int index,
		struct state *abstract_state);

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

static struct error *
abstract_audit(struct ast_function *f, struct state *abstract_state)
{
	struct error *err = NULL;

	struct state *actual_state = state_create_withprops(
		dynamic_str(ast_function_name(f)),
		state_getext(abstract_state),
		ast_function_type(f),
		state_getprops(abstract_state)
	);
	if ((err = ast_function_initparams(f, actual_state))) {
		assert(false);
	}
	if ((err = ast_function_setupabsexec(f, actual_state))) {
		return err;
	}
	if ((err = abstract_auditwithstate(f, actual_state, abstract_state))) {
		return err;	
	}
	state_destroy(actual_state); /* actual_state handled by caller */ 
	return NULL;
}

static struct error *
struct error *
ast_function_setupabsexec(struct ast_function *f, struct state *state)
{
	struct error *err;


@@ 413,147 313,6 @@ ast_function_setupabsexec(struct ast_function *f, struct state *state)
	return NULL;
}

static struct error *
abstract_auditwithstate(struct ast_function *f, struct state *actual_state,
		struct state *abstract_state)
{
	int ndecls = ast_block_ndecls(f->body);
	struct ast_variable **var = ast_block_decls(f->body);
	for (int i = 0; i < ndecls; i++) {
		state_declare(actual_state, var[i], false);
	}

	return path_verify(f, actual_state, 0, abstract_state);
}

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

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

	/* XXX: we are just changing function name now, makes sense to split
	 * state */
	struct ast_function_arr *paths = abstract_paths(f, index, cond);
	int n = ast_function_arr_len(paths);
	assert(n == 2);
	struct ast_function **func = ast_function_arr_func(paths);
	for (int i = 0; i < n; i++) {
		struct state *s_copy = state_copywithname(
			state, ast_function_name(func[i])
		);
		struct preresult *r = ast_expr_assume(
			ast_expr_inverted_copy(cond, i==1), s_copy
		);
		if (preresult_iserror(r)) {
			return preresult_as_error(r);
		}
		if (!preresult_iscontradiction(r)) {
			/* only run if no contradiction because "ex falso" */	
			if ((err = path_absverify(func[i], s_copy, index))) {
				return err;
			}
		}
		/*state_destroy(s_copy);*/
	}
	return NULL;
}

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

static struct error *
path_verify(struct ast_function *f, struct state *actual_state, int index,
		struct state *abstract_state)
{
	char *fname = ast_function_name(f);
	int nstmts = ast_block_nstmts(f->body);
	struct ast_stmt **stmt = ast_block_stmts(f->body);
	for (int i = index; i < nstmts; i++) {
		struct state *prestate = state_copy(actual_state);
		struct error *err = ast_stmt_process(
			stmt[i], fname, actual_state
		);
		if (err) {
			struct error *uc_err = error_to_undecideable_cond(err);
			if (!uc_err) {
				return err;
			}
			return split_path_verify(
				f, prestate, i,
				error_get_undecideable_cond(uc_err),
				abstract_state
			);
		}
		state_destroy(prestate);
		if (ast_stmt_isterminal(stmt[i], actual_state)) {
			break;
		}
		/* result_destroy(res); */
	}
	if (state_hasgarbage(actual_state)) {
		v_printf("actual: %s", state_str(actual_state));
		return error_printf(
			"%s: garbage on heap", ast_function_name(f)
		);
	}
	
	bool equiv = state_equal(actual_state, abstract_state);
	if (!equiv) {
		/*v_printf("actual: %s\n", state_str(actual_state));*/
		/*v_printf("abstract: %s\n", state_str(abstract_state));*/
		return error_printf(
			"%s: actual and abstract states differ",
			ast_function_name(f)
		);
	}

	return NULL;
}

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

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

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

struct result *
ast_function_absexec(struct ast_function *f, struct state *state)
{


@@ 582,6 341,7 @@ ast_function_absexec(struct ast_function *f, struct state *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);



@@ 653,79 413,4 @@ recurse_buildgraph(struct map *g, struct map *dedup, char *fname, struct externa
	map_set(g, dynamic_str(fname), val);
}

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

static struct ast_function_arr *
abstract_paths(struct ast_function *f, int index, struct ast_expr *cond)
{
	struct ast_function_arr *res = ast_function_arr_create();

	struct ast_function *f_true = ast_function_create(
		f->isaxiom,
		ast_type_copy(f->ret),
		split_name(f->name, cond),
		f->nparam,
		ast_variables_copy(f->nparam, f->param),
		ast_block_copy(f->abstract),
		ast_block_copy(f->body)
	);

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

	ast_function_arr_append(res, f_true);
	ast_function_arr_append(res, f_false);
	return res;
}

static struct ast_function_arr *
body_paths(struct ast_function *f, int index, struct ast_expr *cond)
{
	struct ast_function_arr *res = ast_function_arr_create();

	struct ast_function *f_true = ast_function_create(
		f->isaxiom,
		ast_type_copy(f->ret),
		split_name(f->name, cond),
		f->nparam,
		ast_variables_copy(f->nparam, f->param),
		ast_block_copy(f->abstract),
		f->body
	);

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

	ast_function_arr_append(res, f_true);
	ast_function_arr_append(res, f_false);
	return res;
}

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

#include "arr.c"

M src/ast/stmt/verify.c => src/ast/stmt/verify.c +0 -1
@@ 317,7 317,6 @@ ast_stmt_absprocess(struct ast_stmt *stmt, char *fname, struct state *state,
	assert(loc);
	char *m = lexememarker_str(loc);
	struct error *e = error_printf("%s:%s: %w", m, fname, err);
	free(m);
	return e;
}


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

/* XXX */
#define INCLUDE_ENVVAR		"XR0_INCLUDES"
#define OUTPUT_PATH		"0.c"

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

#include "ast.h"
#include "lex.h"
#include "object.h"
#include "state.h"
#include "path.h"

struct path {
	enum path_state {
		PATH_STATE_UNINIT,
		PATH_STATE_ABSTRACT,
		PATH_STATE_HALFWAY,
		PATH_STATE_ACTUAL,
		PATH_STATE_AUDIT,
		PATH_STATE_SPLIT,
		PATH_STATE_ATEND,
	} path_state;
	struct state *abstract, *actual;
	struct path *p_true, *p_false;

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

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->path_state = PATH_STATE_UNINIT;
	return p;
}

void
path_destroy(struct path *p)
{
	assert(path_atend(p));

	/*state_destroy(p->abstract);*/
	/*state_destroy(p->actual);*/
	ast_function_destroy(p->f);
	free(p);
}

static struct path *
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));
	/* TODO: destroy abstract and actual */
	p->abstract = NULL;
	p->actual = NULL;
	p->path_state = PATH_STATE_SPLIT;
}

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

/* state_assume: return false if contradiction encountered. */
static bool
state_assume(struct state *, struct ast_expr *cond);

static struct path *
path_copywithcond(struct path *old, struct ast_expr *cond)
{
	struct path *p = path_create(copy_withcondname(old->f, cond), old->ext);
	char *fname = ast_function_name(p->f);
	p->path_state = old->path_state;
	switch (old->path_state) {
	case PATH_STATE_ABSTRACT:
		p->abstract = state_copywithname(old->abstract, fname);
		if (!state_assume(p->abstract, cond)) {
			p->path_state = PATH_STATE_ATEND;
		}
		break;
	case PATH_STATE_ACTUAL:
		p->abstract = state_copywithname(old->abstract, fname);
		p->actual = state_copywithname(old->actual, fname);
		if (!state_assume(p->actual, cond)) {
			p->path_state = PATH_STATE_ATEND;
		}
		break;
	default:
		assert(false);
	}
	return p;
}

bool
preresult_iserror(struct preresult *);

bool
preresult_iscontradiction(struct preresult *);

static bool
state_assume(struct state *s, struct ast_expr *cond)
{
	struct preresult *r = ast_expr_assume(cond, s);
	assert(!preresult_iserror(r));
	return !preresult_iscontradiction(r);
}

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

static struct ast_function *
copy_withcondname(struct ast_function *old, struct ast_expr *cond)
{
	struct ast_function *f = ast_function_copy(old);
	ast_function_setname(f, split_name(ast_function_name(f), cond));
	return f;
}

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

bool
path_atend(struct path *p)
{
	switch (p->path_state) {
	case PATH_STATE_SPLIT:
		return path_atend(p->p_true) && path_atend(p->p_false);
	case PATH_STATE_ATEND:
		return true;
	default:
		return false;
	}
}

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

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

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

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

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

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

struct error *
path_step(struct path *p)
{
	switch (p->path_state) {
	case PATH_STATE_UNINIT:
		return path_init_abstract(p);
	case PATH_STATE_ABSTRACT:
		return path_step_abstract(p);
	case PATH_STATE_HALFWAY:
		return path_init_actual(p);
	case PATH_STATE_ACTUAL:
		return path_step_actual(p);
	case PATH_STATE_AUDIT:
		return path_audit(p);
	case PATH_STATE_SPLIT:
		return path_step_split(p);
	case PATH_STATE_ATEND:
	default:
		assert(false);
	}
}

static struct error *
path_init_abstract(struct path *p)
{
	p->abstract = state_create(
		ast_function_name(p->f),
		ast_function_abstract(p->f),
		ast_function_type(p->f),
		true,
		p->ext
	);
	struct error *err = ast_function_initparams(p->f, p->abstract);
	if (err) {
		return err;
	}
	p->path_state = PATH_STATE_ABSTRACT;
	return NULL;
}

static struct error *
path_init_actual(struct path *p)
{
	p->actual = state_create_withprops(
		ast_function_name(p->f),
		ast_function_body(p->f),
		ast_function_type(p->f),
		false,
		p->ext,
		state_getprops(p->abstract)
	);
	struct error *err = ast_function_initparams(p->f, p->actual);
	if (err) {
		return err;
	}
	err = ast_function_setupabsexec(p->f, p->actual);
	if (err) {
		return err;
	}
	p->path_state = PATH_STATE_ACTUAL;
	return NULL;
}

static struct error *
path_step_abstract(struct path *p)
{
	if (state_atend(p->abstract)) {
		p->path_state = PATH_STATE_HALFWAY;
		return path_step(p);
	}

	struct error *err = state_step(p->abstract);
	if (!err) {
		return NULL;
	}
	struct error *uc_err = error_to_undecideable_cond(err);
	if (!uc_err) {
		return err;
	}
	path_split(p, error_get_undecideable_cond(uc_err));
	return NULL;
}

static struct error *
path_step_actual(struct path *p)
{
	if (state_atend(p->actual)) {
		p->path_state = PATH_STATE_AUDIT;
		return path_step(p);
	}

	struct error *err = state_step(p->actual);
	if (!err) {
		return NULL;
	}
	struct error *uc_err = error_to_undecideable_cond(err);
	if (!uc_err) {
		return err;
	}
	path_split(p, error_get_undecideable_cond(uc_err));
	return NULL;
}

static struct error *
path_audit(struct path *p)
{
	if (state_hasgarbage(p->actual)) {
		v_printf("actual: %s", state_str(p->actual));
		return error_printf(
			"%s: garbage on heap", ast_function_name(p->f)
		);
	}
	if (!state_equal(p->actual, p->abstract)) {
		/* unequal states are printed by state_equal so that the user
		 * can see the states with undeclared vars */
		return error_printf(
			"%s: actual and abstract states differ",
			ast_function_name(p->f)
		);
	}
	p->path_state = PATH_STATE_ATEND;
	return NULL;
}

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

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));

	struct error *err = path_trystep(p->p_true);
	if (err) {
		return err;
	}
	return path_trystep(p->p_false);
}

static struct error *
path_trystep(struct path *p)
{
	return path_atend(p) ? NULL : path_step(p);
}

M src/state/stack.c => src/state/stack.c +207 -9
@@ 12,8 12,33 @@
#include "value.h"
#include "util.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 stack {
	char *name;
	struct program_counter *pc;
	bool abstract;

	struct block_arr *frame;

	/* lvalues of blocks in frame */


@@ 35,12 60,15 @@ stack_newblock(struct stack *stack)
}

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

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

	stack->varmap = map_create();


@@ 48,13 76,14 @@ stack_create(char *name, struct stack *prev, struct ast_type *return_type)
	stack->prev = prev;
	stack->id = prev ? prev->id + 1 : 0;

	stack->result = variable_create(return_type, stack, false);
	stack->result = variable_create(ret_type, stack, false);

	return stack;
}

struct stack *
stack_getframe(struct stack *s, int frame) {
stack_getframe(struct stack *s, int frame)
{
	assert(s);
	assert(frame >= 0);



@@ 80,6 109,7 @@ stack_destroy(struct stack *stack)

	variable_destroy(stack->result);

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



@@ 96,7 126,8 @@ struct stack *
stack_copy(struct stack *stack)
{
	struct stack *copy = calloc(1, sizeof(struct stack));
	copy->name = dynamic_str(stack->name);
	copy->abstract = stack->abstract;
	copy->pc = program_counter_copy(stack->pc);
	copy->frame = block_arr_copy(stack->frame);
	copy->varmap = varmap_copy(stack->varmap);
	copy->id = stack->id;


@@ 111,8 142,7 @@ struct stack *
stack_copywithname(struct stack *stack, char *new_name)
{
	struct stack *copy = stack_copy(stack);
	free(copy->name);
	copy->name = new_name;
	program_counter_changename(copy->pc, new_name);
	return copy;
}



@@ 151,7 181,7 @@ stack_str(struct stack *stack, struct state *state)
	for (int i = 0, len = 30; i < len-2; i++ ) {
		strbuilder_putc(b, '-');
	}
	strbuilder_printf(b, " %s\n", stack->name);
	strbuilder_printf(b, " %s\n", program_counter_name(stack->pc));
	if (stack->prev) {
		char *prev = stack_str(stack->prev, state);
		strbuilder_printf(b, prev);


@@ 160,6 190,18 @@ stack_str(struct stack *stack, struct state *state)
	return strbuilder_build(b);
}

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

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

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


@@ 369,3 411,159 @@ 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 +8 -1
@@ 7,7 7,8 @@
struct stack;

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

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


@@ 27,6 28,12 @@ stack_copywithname(struct stack *, char *new_name);
char *
stack_str(struct stack *, struct state *);

bool
stack_atend(struct stack *);

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

struct stack *
stack_prev(struct stack *);


M src/state/state.c => src/state/state.c +24 -22
@@ 29,7 29,8 @@ struct state {
};

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


@@ 37,24 38,18 @@ state_create(char *func, struct externals *ext, struct ast_type *result_type)
	state->static_memory = static_memory_create();
	state->vconst = vconst_create();
	state->clump = clump_create();
	state->stack = stack_create(func, NULL, result_type);
	state->stack = stack_create(name, block, ret_type, abstract, NULL);
	state->heap = heap_create();
	state->props = props_create();
	return state;
}

struct state *
state_create_withprops(char *func, struct externals *ext, struct ast_type *result_type,
state_create_withprops(char *name, struct ast_block *block,
		struct ast_type *ret_type, bool abstract, struct externals *ext,
		struct props *props)
{
	struct state *state = malloc(sizeof(struct state));
	assert(state);
	state->ext = ext;
	state->static_memory = static_memory_create();
	state->vconst = vconst_create();
	state->clump = clump_create();
	state->stack = stack_create(func, NULL, result_type);
	state->heap = heap_create();
	struct state *state = state_create(name, block, ret_type, abstract, ext);
	state->props = props_copy(props);
	return state;
}


@@ 89,15 84,8 @@ state_copy(struct state *state)
struct state *
state_copywithname(struct state *state, char *func_name)
{
	struct state *copy = malloc(sizeof(struct state));
	assert(copy);
	copy->ext = state->ext;
	copy->static_memory = static_memory_copy(state->static_memory);
	copy->vconst = vconst_copy(state->vconst);
	copy->clump = clump_copy(state->clump);
	struct state *copy = state_copy(state);
	copy->stack = stack_copywithname(state->stack, func_name);
	copy->heap = heap_copy(state->heap);
	copy->props = props_copy(state->props);
	return copy;
}



@@ 145,6 133,19 @@ state_str(struct state *state)
	return strbuilder_build(b);
}

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

struct error *
state_step(struct state *s)
{
	return stack_step(s->stack, s);
}


struct externals *
state_getext(struct state *s)
{


@@ 164,9 165,10 @@ state_getprops(struct state *s)
}

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

void


@@ 552,8 554,8 @@ state_equal(struct state *s1, struct state *s2)
	     *str2 = state_str(s2_c);
	bool equal = strcmp(str1, str2) == 0;
	if (!equal) {
		v_printf("actual: %s", str1);
		v_printf("abstract: %s", str2);
		v_printf("actual: %s", str1);
	}
	free(str2);
	free(str1);

M tests/7-use-after-free/004-mix-multiple-levels.x => tests/7-use-after-free/004-mix-multiple-levels.x +3 -1
@@ 1,11 1,13 @@
int
snapshot_and_change(int *arg) ~ [
	int j;
	setup: {
		arg = .clump(sizeof(int));
		*arg = $;
	}
	return *arg;
	j = *arg;
	*arg = 3;
	return j;
] {
	int j;
	j = *arg;