~lbnz/xr0

6fa96f5d5e77959d8a50401d8e1ac711cd57a213 — Claude Betz a month ago 7b59a93
feat: breakpoints and continue command

issue: https://github.com/xr0-org/xr0/issues/45
M Makefile => Makefile +9 -2
@@ 45,6 45,8 @@ OBJECT_OBJ = $(BUILD_DIR)/object.o
VALUE_OBJ = $(BUILD_DIR)/value.o
MATH_OBJ = $(BUILD_DIR)/math.o

BREAKPOINT_OBJ = $(BUILD_DIR)/breakpoint.o

AST_OBJ = $(BUILD_DIR)/ast.o
LEX_OBJ = $(BUILD_DIR)/lex.o
UTIL_OBJ = $(BUILD_DIR)/util.o


@@ 59,7 61,8 @@ XR0_OBJECTS = $(AST_OBJ) \
	      $(GRAM_OBJ) \
	      $(STATE_OBJ) \
	      $(UTIL_OBJ) \
	      $(MATH_OBJ)
	      $(MATH_OBJ) \
	      $(BREAKPOINT_OBJ)

STATE_OBJECTS = $(VALUE_OBJ) \
		$(LOCATION_OBJ) \


@@ 135,10 138,14 @@ $(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
$(PROGRAM_OBJ): $(STATE_DIR)/program.c $(BREAKPOINT_OBJ)
	@printf 'CC\t$@\n'
	@$(CC) $(CFLAGS) -o $@ -c $(STATE_DIR)/program.c

$(BREAKPOINT_OBJ): $(AST_DIR)/breakpoint.c
	@printf 'CC\t$@\n'
	@$(CC) $(CFLAGS) -o $@ -c $(AST_DIR)/breakpoint.c

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

A include/breakpoint.h => include/breakpoint.h +23 -0
@@ 0,0 1,23 @@
#ifndef BREAKPOINT_H
#define BREAKPOINT_H

struct breakpoint;

char *
breakpoint_list();

struct error *
breakpoint_set(char *filename, int linenum);

struct error *
breakpoint_delete(int id);

struct lexememarker;

bool
breakpoint_shouldbreak(struct lexememarker *);

void
breakpoint_reset();

#endif

M include/lex.h => include/lex.h +6 -0
@@ 17,6 17,12 @@ struct lexememarker {
struct lexememarker *
lexloc();

int
lexememarker_linenum(struct lexememarker *);

char *
lexememarker_filename(struct lexememarker *);

struct lexememarker *
lexememarker_copy(struct lexememarker *);


M include/path.h => include/path.h +11 -2
@@ 16,6 16,9 @@ path_create(struct ast_function *, struct externals *);
void
path_destroy(struct path *);

char *
path_str(struct path *);

bool
path_atend(struct path *);



@@ 25,7 28,13 @@ path_step(struct path *);
struct error *
path_next(struct path *);

char *
path_str(struct path *);
struct error *
path_setbreakpoint(struct path *);

struct lexememarker *
path_lexememarker(struct path *);

int
path_frameid(struct path *);

#endif

M include/state.h => include/state.h +3 -0
@@ 138,6 138,9 @@ state_execmode_str(enum execution_mode);
enum execution_mode
state_execmode(struct state *);

struct lexememarker *
state_lexememarker(struct state *);

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


M src/ast/ast.c => src/ast/ast.c +1 -2
@@ 72,8 72,7 @@ void
result_destroy(struct result *res)
{
	assert(!res->err);
	if (res->val) {
		value_destroy(res->val);
	if (res->val) { value_destroy(res->val);
	}
	free(res);
}

A src/ast/breakpoint.c => src/ast/breakpoint.c +133 -0
@@ 0,0 1,133 @@
#include<stdlib.h>
#include<stdio.h>
#include<string.h>
#include<stdbool.h>
#include<assert.h>

#include "breakpoint.h"
#include "util.h"
#include "lex.h"

#define MAX_BREAKPOINTS 100

/* XXX: validation of filenames and lengths for breakpoints */

struct breakpoint {
	bool enabled;
	bool reached;
	// char *filename;
	int linenumber;
};

struct breakpoint breakpoints[MAX_BREAKPOINTS];
int breakpoint_count = 0;

static char *
breakpoint_str(struct breakpoint);

char *
breakpoint_list()
{
	struct strbuilder *b = strbuilder_create();
	strbuilder_printf(b, "Num\tType\tEnabled\tReached\tWhat\n");
	for (int i = 0; i < breakpoint_count; i++) {
		struct breakpoint bp = breakpoints[i];
		strbuilder_printf( b,
			"%d\tbreak\t%s\t%s\t%s\n",
			i,
			bp.enabled ? dynamic_str("y") : dynamic_str("n"),
			bp.reached ? dynamic_str("y") : dynamic_str("n"),
			breakpoint_str(bp)
		);
	}
	return strbuilder_build(b);
}

static char *
breakpoint_str(struct breakpoint bp)
{
	if (bp.enabled) {
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(b, "%d", bp.linenumber);
		return strbuilder_build(b);
	}
	return dynamic_str("");
}

static int
breakpoint_exists(struct breakpoint);

struct error *
breakpoint_set(char *filename, int linenumber)
{
	struct breakpoint bp = (struct breakpoint) {
		.enabled = true, .linenumber = linenumber
	};
	if (breakpoint_count > MAX_BREAKPOINTS) {
		return error_printf("Maximum number of breakpoints reached\n");
	}
	int id = breakpoint_exists(bp);
	if (id != -1) {
		return error_printf(
			"Note: breakpoint %s is already set as %d\n", breakpoint_str(bp), id
		);
	}
	breakpoints[breakpoint_count] = bp;
	breakpoint_count++;
	return NULL;
}

static bool
breakpoint_equal(struct breakpoint bp1, struct breakpoint bp2);

static int
breakpoint_exists(struct breakpoint bp)
{
	for (int i = 0; i < breakpoint_count; i++) {
		if (breakpoint_equal(bp, breakpoints[i]) && !breakpoints[i].reached) {
			breakpoints[i].reached = true;
			return i;
		}
	}
	return -1;
}

static bool
breakpoint_equal(struct breakpoint bp1, struct breakpoint bp2)
{
	return bp1.linenumber == bp2.linenumber;
}

struct error *
breakpoint_delete(int id)
{
	if (breakpoints[id].enabled) {
		breakpoints[id].enabled = false;
		return NULL;
	}
	return error_printf("No breakpoint with id: %d", id);
}

bool
breakpoint_shouldbreak(struct lexememarker *loc)
{
	// char *fname = lexememarker_filename(loc);
	int linenum = lexememarker_linenum(loc);

	struct breakpoint bp = (struct breakpoint) {
		.linenumber = linenum,
	};
	int index = breakpoint_exists(bp);
	if (index == -1) {
		return false;
	}
	return true;
}

void
breakpoint_reset()
{
	for (int i = 0; i < breakpoint_count; i++) {
		breakpoints[i].reached = false;
	}
}

M src/ast/expr/verify.c => src/ast/expr/verify.c +3 -0
@@ 4,6 4,7 @@
#include <string.h>

#include "ast.h"
#include "breakpoint.h"
#include "expr.h"
#include "ext.h"
#include "intern.h"


@@ 1082,6 1083,8 @@ ast_expr_abseval(struct ast_expr *expr, struct state *state)
static struct result *
call_absexec(struct ast_expr *expr, struct state *state)
{
	breakpoint_reset();

	struct error *err;

	struct ast_expr *root = ast_expr_call_root(expr);

M src/ast/function/function.c => src/ast/function/function.c +297 -26
@@ 2,6 2,7 @@
#include <stdlib.h>
#include <assert.h>
#include <string.h>
#include <ctype.h>

#include "ast.h"
#include "lex.h"


@@ 16,6 17,7 @@
#include "stmt/stmt.h"
#include "ext.h"
#include "util.h"
#include "breakpoint.h"

struct ast_function {
	bool isaxiom;


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

static struct error *
next(struct path *);
next_command(struct path *);

struct error *
ast_function_debug(struct ast_function *f, struct externals *ext)


@@ 226,7 228,7 @@ ast_function_debug(struct ast_function *f, struct externals *ext)
	struct path *path = path_create(f, ext);
	while (!path_atend(path)) {
		d_printf("%s\n", path_str(path));
		struct error *err = next(path);
		struct error *err = next_command(path);
		if (err) {
			return err;
		}


@@ 235,62 237,332 @@ ast_function_debug(struct ast_function *f, struct externals *ext)
	return NULL;
}

enum command {
enum command_kind {
	COMMAND_STEP,
	COMMAND_NEXT,
	COMMAND_CONTINUE,
	COMMAND_QUIT,
	COMMAND_BREAKPOINT_SET,
	COMMAND_BREAKPOINT_LIST,
};

static enum command
struct command {
	enum command_kind kind;
	struct string_arr *args;
};

static struct command *
command_create(enum command_kind kind)
{
	struct command *cmd = malloc(sizeof(struct command));	
	cmd->kind = kind;
	cmd->args = string_arr_create();
	return cmd;
}

static struct command *
command_create_withargs(enum command_kind kind, struct string_arr *args)
{
	struct command *cmd = malloc(sizeof(struct command));	
	cmd->kind = kind;
	cmd->args = args;
	return cmd;
}

static void
command_destroy(struct command *cmd)
{
	string_arr_destroy(cmd->args);
	free(cmd);
}


bool should_continue = false;

static struct command *
getcmd();

static struct error *
next(struct path *p)
command_continue(struct path *);

static struct error *
next_command(struct path *p)
{
	printf("(0db) ");
	switch (getcmd()) {
	if (should_continue) {
		should_continue = false;
		return command_continue(p);
	}
	struct command *cmd = getcmd();
	switch (cmd->kind) {
	case COMMAND_STEP:
		return path_step(p);
	case COMMAND_NEXT:
		return path_next(p);
		return path_next(p);	
	case COMMAND_CONTINUE:
		return command_continue(p);
	case COMMAND_QUIT:
		exit(0);
	case COMMAND_BREAKPOINT_SET:
	case COMMAND_BREAKPOINT_LIST:
		return NULL;
	default:
		assert(false);
	}
}

#define LINELEN 1000

static enum command
static struct error *
command_continue(struct path *p)
{
	while (!path_atend(p)) {
		struct error *err = path_step(p);
		if (err) {
			return err;
		}
		struct lexememarker *loc = path_lexememarker(p);
		if (loc && breakpoint_shouldbreak(loc)) {
			return NULL;
		}
	}
	should_continue = true;
	return NULL;
}


/* getcmd() */

#define MAX_COMMANDLEN 100
#define MAX_LINELEN 1000
#define MAX_ARGSLEN 100

static struct command *
process_command(char *cmd);

static struct command *
process_commandwithargs(char *cmd, char *args);

static struct command *
getcmd()
{
	char line[LINELEN];
	if (!fgets(line, LINELEN, stdin)) {
	printf("(0db) ");
	char line[MAX_LINELEN];
	char cmd[MAX_COMMANDLEN];
	char args[MAX_ARGSLEN];
	if (!fgets(line, MAX_LINELEN, stdin)) {
		fprintf(stderr, "error: cannot read\n");
		return getcmd();
	}
	if (strlen(line) != 2) {
		fprintf(stderr, "input must be single char\n");
	char *space = strchr(line, ' ');
	if (space == NULL) {
		/* ⊢ command no args */
		strcpy(cmd, line);
		cmd[strcspn(cmd, "\n")] = '\0';
		return process_command(cmd);
	} else {
		/* ⊢ command with args */
		*space = '\0';
		strcpy(cmd, line);
		strcpy(args, space+1);
		args[strcspn(args, "\n")] = '\0';
		return process_commandwithargs(cmd, args);	
	}
}

static bool
command_isstep(char *cmd);

static bool
command_isnext(char *cmd);

static bool
command_iscontinue(char *cmd);

static bool
command_isquit(char *cmd);

static struct command *
process_command(char *cmd)
{
	if (command_isstep(cmd)) {
		return command_create(COMMAND_STEP);
	} else if (command_isnext(cmd)) {
		return command_create(COMMAND_NEXT);
	} else if (command_iscontinue(cmd)){
		return command_create(COMMAND_CONTINUE);
	} else if (command_isquit(cmd)) {
		return command_create(COMMAND_QUIT);
	} else {
		fprintf(stderr, "unknown command `%s'\n", cmd);
		return getcmd();
	}
	if (line[1] != '\n') {
		fprintf(stderr, "input must be end with newline\n");
}

static bool
command_isstep(char *cmd)
{
	return strcmp(cmd, "s") == 0 || strcmp(cmd, "step") == 0;
}

static bool
command_isnext(char *cmd)
{
	return strcmp(cmd, "n") == 0 || strcmp(cmd, "next") == 0;
}

static bool
command_iscontinue(char *cmd)
{
	return strcmp(cmd, "c") == 0 || strcmp(cmd, "continue") == 0;
}

static bool
command_isquit(char *cmd)
{
	return strcmp(cmd, "q") == 0 || strcmp(cmd, "quit") == 0;
}

static struct string_arr *
args_tokenise(char *args);

static bool
command_isbreak(char *cmd);

static struct command *
command_break(struct string_arr *args);

static struct command *
process_commandwithargs(char *cmd, char *args)
{
	struct string_arr *args_tk = args_tokenise(args);
	if (args_tk == NULL) {
		fprintf(stderr, "invalid command args: %s\n", args);
		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);
	if (command_isbreak(cmd)) {
		return command_break(args_tk);	
	}
	assert(false);
}

static struct string_arr *
args_tokenise(char *args)
{
	struct string_arr *arg_arr = string_arr_create();
	char *token;
	token = strtok(args, " ");
	while (token != NULL) {
		string_arr_append(arg_arr, dynamic_str(token));	
		token = strtok(NULL, " ");
	}
	return arg_arr;
}

static bool
command_isbreak(char *cmd)
{
	return strcmp(cmd, "b") == 0 || strcmp(cmd, "break") == 0;
}

static bool
break_argisset(char *arg);

static bool
break_argislist(char *arg);

static struct command *
break_set(char *arg);

static struct command *
break_list();

static struct command *
command_break(struct string_arr *args)
{
	if (string_arr_n(args) != 1) {
		fprintf(stderr, "`break' expects single argument\n");
		return getcmd();
	}
	char *arg = string_arr_s(args)[0];
	if (break_argisset(arg)) {
		return break_set(arg);
	} else if (break_argislist(arg)) {
		return break_list();
	} else {
		fprintf(stderr, "`break' received unknown argument\n");
		return getcmd();
	}
}


static bool
isint(const char *str) {
	if (str == NULL || *str == '\0') {
		return false;
	}
	while (*str) {
		if (!isdigit(*str)) {
			return false;
		}
		str++;
	}
	return true;
}

static bool
break_argisset(char *arg)
{
	return isint(arg);
}

static bool
break_argislist(char *arg)
{
	return strcmp(arg, "list") == 0;
}

static struct string_arr *
break_argsplit(char *arg);

static struct command *
break_set(char *arg)
{
	int linenum = atoi(arg);
	struct error *err = breakpoint_set("", linenum);
	if (err) {
		fprintf(stderr, "could not set breakpoint: %s", error_str(err));
		return getcmd();
	}
	return command_create(COMMAND_BREAKPOINT_SET);
}

static struct string_arr *
break_argsplit(char *arg)
{
	struct string_arr *split = string_arr_create();

	char fname[MAX_ARGSLEN];
	char linenum[MAX_ARGSLEN];
	char *colon = strchr(arg, ':');
	if (colon == NULL) {
		return NULL;
	} else {
		*colon = '\0';
		strcpy(fname, arg);
		strcpy(linenum, colon+1);
		linenum[strcspn(linenum, "\n")] = '\0';
	}
	string_arr_append(split, dynamic_str(fname));
	string_arr_append(split, dynamic_str(linenum));
	return split;
}

static struct command *
break_list()
{
	printf("%s\n", breakpoint_list());
	return getcmd();
}

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



@@ 304,7 576,6 @@ ast_function_initparams(struct ast_function *f, struct state *s)
	for (int i = 0; i < nparams; i++) {
		state_declare(s, params[i], true);
	}

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

M src/ast/gram.y => src/ast/gram.y +11 -6
@@ 110,6 110,7 @@ variable_array_create(struct ast_variable *v)
	struct ast_expr *expr;
	struct ast_externdecl *externdecl;
	struct ast_function *function;
	struct lexememarker *lexememarker;
	struct ast_stmt *statement;
	struct ast_type *type;
	struct ast_variable *variable;


@@ 177,6 178,7 @@ variable_array_create(struct ast_variable *v)
%type <statement> statement expression_statement selection_statement jump_statement 
%type <statement> labelled_statement iteration_statement for_iteration_statement
%type <statement> iteration_effect_statement
%type <lexememarker> selection_statement_if
%type <stmt_array> statement_list
%type <string> identifier direct_declarator
%type <type> declaration_specifiers type_specifier struct_or_union_specifier 


@@ 742,16 744,19 @@ expression_statement
	;

selection_statement
	: IF '(' expression ')' statement
		{ $$ = ast_stmt_create_sel(lexloc(), false, $3, ast_stmt_as_compound($5), NULL); }
	| IF '(' expression ')' statement ELSE statement
		{ $$ = ast_stmt_create_sel(
			lexloc(), false, $3, ast_stmt_as_compound($5), ast_stmt_as_compound($7)
		); }
	: selection_statement_if '(' expression ')' statement
		{ $$ = ast_stmt_create_sel($1, false, $3, ast_stmt_as_compound($5), NULL); }
	| selection_statement_if '(' expression ')' statement ELSE statement
		{ $$ = ast_stmt_create_sel($1, false, $3, ast_stmt_as_compound($5), ast_stmt_as_compound($7));
		}
	| SWITCH '(' expression ')' statement
		{ assert(false); }
	;

selection_statement_if
	: IF { $$ = lexloc(); }
	;

for_some
	: FOR
	| SOME

M src/ast/lex.l => src/ast/lex.l +14 -1
@@ 351,7 351,8 @@ strip_iflibx(char *filename)

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


@@ 366,6 367,18 @@ lexememarker_destroy(struct lexememarker *loc)
	free(loc);
}

int
lexememarker_linenum(struct lexememarker *loc)
{
	return loc->linenum;
}

char *
lexememarker_filename(struct lexememarker *loc)
{
	return loc->filename;
}

char *
lexememarker_str(struct lexememarker *loc)
{

M src/ast/stmt/verify.c => src/ast/stmt/verify.c +1 -2
@@ 611,8 611,7 @@ iter_absexec(struct ast_stmt *stmt, struct state *state)
	if ((err = ast_expr_alloc_rangeprocess(alloc, lw, up, state))) {
		return err;
	}
	return NULL;
}
	return NULL; }

static struct ast_expr *
hack_alloc_from_neteffect(struct ast_stmt *stmt)

M src/main.c => src/main.c +0 -1
@@ 25,7 25,6 @@
#define ERROR_NO_INPUT		"must provide input as string"
#define ERROR_NO_SORTFUNC	"supply function to `-t' flag to evaluate dependencies for"


int
yyparse();


M src/path/path.c => src/path/path.c +238 -269
@@ 51,18 51,6 @@ path_arr_destroy(struct path_arr *arr)
	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)
{


@@ 106,96 94,77 @@ path_destroy(struct path *p)
	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)
{
	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++;	
	}
}
char *
path_abstract_str(struct path *);

static struct ast_function *
copy_withcondname(struct ast_function *, struct ast_expr *cond); 
char *
path_actual_str(struct path *);

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

static struct path *
path_copywithcond(struct path *old, struct ast_expr *cond)
char *
path_str(struct path *p)
{
	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) {
	switch (p->path_state) {
	case PATH_STATE_UNINIT:
		return dynamic_str("path init abstract 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;
		return path_abstract_str(p);
	case PATH_STATE_HALFWAY:
		return dynamic_str("path init actual state");
	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;
		return path_actual_str(p);
	case PATH_STATE_AUDIT:
		return dynamic_str("path audit");
	case PATH_STATE_SPLIT:
		return path_split_str(p);
	case PATH_STATE_ATEND:
		return dynamic_str("path at end");
	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)
char *
path_abstract_str(struct path *p)
{
	struct preresult *r = ast_expr_assume(cond, s);
	assert(!preresult_iserror(r));
	return !preresult_iscontradiction(r);
	struct strbuilder *b = strbuilder_create();
	strbuilder_printf(
		b, "mode: %s\n", state_execmode_str(state_execmode(p->abstract))
	);
	strbuilder_printf(b, "text:\n%s\n", state_programtext(p->abstract));
	strbuilder_printf(b, "%s\n", state_str(p->abstract));
	return strbuilder_build(b);
}

static char *
split_name(char *name, struct ast_expr *cond);
char *
path_actual_str(struct path *p)
{
	struct strbuilder *b = strbuilder_create();
	strbuilder_printf(
		b, "mode: %s\n", state_execmode_str(state_execmode(p->actual))
	);
	strbuilder_printf(b, "text:\n%s\n", state_programtext(p->actual));
	strbuilder_printf(b, "%s\n", state_str(p->actual));
	return strbuilder_build(b);
}

static struct ast_function *
copy_withcondname(struct ast_function *old, struct ast_expr *cond)
char *
path_split_str(struct path *p)
{
	struct ast_function *f = ast_function_copy(old);
	ast_function_setname(f, split_name(ast_function_name(f), cond));
	return f;
	struct path *branch = p->paths->paths[p->branch_index];
	return path_str(branch);
}

static char *
split_name(char *name, struct ast_expr *assumption)
static void
path_nextbranch(struct path *p)
{
	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);
	assert(p->paths->n >= 2);
	int index = p->branch_index;
	if (index < p->paths->n - 1) {
		p->branch_index++;	
	}
}

bool


@@ 211,6 180,9 @@ path_atend(struct path *p)
	}
}


/* path_step */

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



@@ 252,48 224,39 @@ 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)
path_init_abstract(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);
	struct error *err;

	struct frame *f = frame_call_create(
		ast_function_name(p->f),
		ast_function_abstract(p->f),
		ast_function_type(p->f),
		EXEC_ABSTRACT,
		ast_expr_identifier_create(dynamic_str("base abs")), /* XXX */
		p->f
	);
	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;
}

static bool
path_continue(struct path *, enum path_state og_state, int og_frame,
		int og_index);
static void
path_split(struct path *p, struct ast_expr *cond);

static struct error *
path_next_abstract(struct path *p)
{
path_step_abstract(struct path *p, bool print)
{	
	if (state_atend(p->abstract) && state_frameid(p->abstract) == 0) {
		p->path_state = PATH_STATE_HALFWAY;
		return path_step(p);
	}
	struct error *err = state_next(p->abstract);

	struct error *err = state_step(p->abstract);
	if (!err) {
		return NULL;
	}


@@ 305,129 268,90 @@ path_next_abstract(struct path *p)
	return state_stacktrace(p->abstract, err);
}

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 path *
path_copywithcond(struct path *old, struct ast_expr *cond);

static struct error *
branch_next(struct path *parent, struct path *branch)
static void
path_split(struct path *p, struct ast_expr *cond)
{
	d_printf("branch: %d\n", parent->branch_index);
	if (path_atend(branch)) {
		path_nextbranch(parent);
		return NULL;
	}
	return path_next(branch);
	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 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 struct ast_function *
copy_withcondname(struct ast_function *, struct ast_expr *cond); 

/* state_assume: return false if contradiction encountered. */
static bool
path_insamestate(struct path *p, enum path_state og_state)
{
	return p->path_state == og_state;
}
state_assume(struct state *, struct ast_expr *cond);

static bool
path_inlowerframe(struct path *p, enum path_state og_state, int og_frame)
static struct path *
path_copywithcond(struct path *old, struct ast_expr *cond)
{
	switch (og_state) {
	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:
		return og_frame < state_frameid(p->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:
		return og_frame < state_frameid(p->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
path_insamestmt(struct path *p, enum path_state og_state, int og_frame, int og_index)
state_assume(struct state *s, struct ast_expr *cond)
{
	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);
	struct preresult *r = ast_expr_assume(cond, s);
	assert(!preresult_iserror(r));
	return !preresult_iscontradiction(r);
}

static struct error *
path_next_actual(struct path *p)
static char *
split_name(char *name, struct ast_expr *cond);

static struct ast_function *
copy_withcondname(struct ast_function *old, struct ast_expr *cond)
{
	if (state_atend(p->actual) && state_frameid(p->actual) == 0) {
		p->path_state = PATH_STATE_AUDIT;
		return path_step(p);
	}
	struct error *err = state_next(p->actual);
	if (!err) {
		return NULL;
	}
	struct error *uc_err = error_to_undecideable_cond(err);
	if (uc_err) {
		path_split(p, error_get_undecideable_cond(uc_err));
		return NULL;
	}
	return state_stacktrace(p->actual, err);
	struct ast_function *f = ast_function_copy(old);
	ast_function_setname(f, split_name(ast_function_name(f), cond));
	return f;
}

static struct error *
path_init_abstract(struct path *p)
static char *
split_name(char *name, struct ast_expr *assumption)
{
	struct error *err;

	struct frame *f = frame_call_create(
		ast_function_name(p->f),
		ast_function_abstract(p->f),
		ast_function_type(p->f),
		EXEC_ABSTRACT,
		ast_expr_identifier_create(dynamic_str("base abs")), /* XXX */
		p->f
	);
	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;
	struct strbuilder *b = strbuilder_create();
	char *assumption_str = ast_expr_str(assumption);
	strbuilder_printf(b, "%s | %s", name, assumption_str);
	free(assumption_str);
	return strbuilder_build(b);
}



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


@@ 458,26 382,6 @@ path_init_actual(struct path *p)
}

static struct error *
path_step_abstract(struct path *p, bool print)
{	
	if (state_atend(p->abstract) && state_frameid(p->abstract) == 0) {
		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) {
		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, bool print)
{	
	if (state_atend(p->actual) && state_frameid(p->actual) == 0) {


@@ 546,65 450,130 @@ branch_step(struct path *parent, struct path *branch)
	return path_step(branch);
}

char *
path_abstract_str(struct path *);

char *
path_actual_str(struct path *);
/* path_next */

char *
path_split_str(struct path *);
static struct error *
path_next_abstract(struct path *);

char *
path_str(struct path *p)
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 dynamic_str("path init abstract state");
		return path_step(p);
	case PATH_STATE_ABSTRACT:
		return path_abstract_str(p);
		return path_next_abstract(p);
	case PATH_STATE_HALFWAY:
		return dynamic_str("path init actual state");
		return path_step(p);
	case PATH_STATE_ACTUAL:
		return path_actual_str(p);
		return path_next_actual(p);
	case PATH_STATE_AUDIT:
		return dynamic_str("path audit");
		return path_audit(p);
	case PATH_STATE_SPLIT:
		return path_split_str(p);
		return path_next_split(p);
	case PATH_STATE_ATEND:
		return dynamic_str("path at end");
	default:
		assert(false);
	}
}

char *
path_abstract_str(struct path *p)
static struct error *
path_next_abstract(struct path *p)
{
	struct strbuilder *b = strbuilder_create();
	strbuilder_printf(
		b, "mode: %s\n", state_execmode_str(state_execmode(p->abstract))
	);
	strbuilder_printf(b, "text:\n%s\n", state_programtext(p->abstract));
	strbuilder_printf(b, "%s\n", state_str(p->abstract));
	return strbuilder_build(b);
	if (state_atend(p->abstract) && state_frameid(p->abstract) == 0) {
		p->path_state = PATH_STATE_HALFWAY;
		return path_step(p);
	}
	struct error *err = state_next(p->abstract);
	if (!err) {
		return NULL;
	}
	struct error *uc_err = error_to_undecideable_cond(err);
	if (uc_err) {
		path_split(p, error_get_undecideable_cond(uc_err));
		return NULL;
	}
	return state_stacktrace(p->abstract, err);
}

char *
path_actual_str(struct path *p)
static struct error *
path_next_actual(struct path *p)
{
	struct strbuilder *b = strbuilder_create();
	strbuilder_printf(
		b, "mode: %s\n", state_execmode_str(state_execmode(p->actual))
	);
	strbuilder_printf(b, "text:\n%s\n", state_programtext(p->actual));
	strbuilder_printf(b, "%s\n", state_str(p->actual));
	return strbuilder_build(b);
	if (state_atend(p->actual) && state_frameid(p->actual) == 0) {
		p->path_state = PATH_STATE_AUDIT;
		return path_step(p);
	}
	struct error *err = state_next(p->actual);
	if (!err) {
		return NULL;
	}
	struct error *uc_err = error_to_undecideable_cond(err);
	if (uc_err) {
		path_split(p, error_get_undecideable_cond(uc_err));
		return NULL;
	}
	return state_stacktrace(p->actual, err);
}

char *
path_split_str(struct path *p)
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 struct lexememarker *
path_split_lexememarker(struct path *);

struct lexememarker *
path_lexememarker(struct path *p)
{
	switch (p->path_state) {
	case PATH_STATE_ABSTRACT:
		return state_lexememarker(p->abstract);
	case PATH_STATE_ACTUAL:
		return state_lexememarker(p->actual);	
	case PATH_STATE_SPLIT:
		return path_split_lexememarker(p);
	case PATH_STATE_UNINIT:
	case PATH_STATE_HALFWAY:
	case PATH_STATE_AUDIT:
	case PATH_STATE_ATEND:
		return NULL;
	default:
		assert(false);
	}
}

static struct lexememarker *
path_split_lexememarker(struct path *p)
{
	struct path *branch = p->paths->paths[p->branch_index];
	return path_str(branch);
	return path_lexememarker(branch);
}

M src/state/program.c => src/state/program.c +20 -2
@@ 3,6 3,7 @@
#include <assert.h>

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


@@ 64,7 65,8 @@ program_destroy(struct program *p)
	free(p);
}

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


@@ 167,7 169,9 @@ program_step(struct program *p, struct state *s)
	case PROGRAM_COUNTER_STMTS:
		return program_stmt_step(p, s);
	case PROGRAM_COUNTER_ATEND:
		state_popframe(s);
		if (state_frameid(s) != 0) {
			state_popframe(s);
		}
		return NULL;
	default:
		assert(false);


@@ 266,3 270,17 @@ program_loc(struct program *p)
		assert(false);
	}
}

struct lexememarker *
program_lexememarker(struct program *p)
{
	switch (p->s) {
	case PROGRAM_COUNTER_STMTS:
		return ast_stmt_lexememarker(ast_block_stmts(p->b)[p->index]);
	case PROGRAM_COUNTER_DECLS:
	case PROGRAM_COUNTER_ATEND:
		return NULL;
	default:
		assert(false);
	}
}

M src/state/program.h => src/state/program.h +3 -0
@@ 44,4 44,7 @@ program_next(struct program *, struct state *);
char *
program_loc(struct program *);

struct lexememarker *
program_lexememarker(struct program *);

#endif

M src/state/stack.c => src/state/stack.c +6 -0
@@ 319,6 319,12 @@ stack_execmode(struct stack *s)
	return s->mode;
}

struct lexememarker *
stack_lexememarker(struct stack *s)
{
	return program_lexememarker(s->p);
}

bool
stack_atend(struct stack *s)
{

M src/state/stack.h => src/state/stack.h +3 -0
@@ 50,6 50,9 @@ stack_islinear(struct stack *);
enum execution_mode
stack_execmode(struct stack *);

struct lexememarker *
stack_lexememarker(struct stack *);

bool
stack_atend(struct stack *);


M src/state/state.c => src/state/state.c +6 -0
@@ 177,6 177,12 @@ state_execmode(struct state *s)
	return stack_execmode(s->stack);
}

struct lexememarker *
state_lexememarker(struct state *s)
{
	return stack_lexememarker(s->stack);
}

bool
state_atend(struct state *s)
{