~lbnz/xr0

3df6aa98c765baabb82c83fa93f1a2ecadf62c49 — Claude Betz 4 months ago ea3e616
far along
M include/ast.h => include/ast.h +9 -0
@@ 164,6 164,9 @@ struct preresult;
struct preresult *
ast_expr_assume(struct ast_expr *, struct state *);

struct error *
ast_expr_precondsverify(struct ast_expr *, struct state *);

struct lvalue;

struct lvalue *


@@ 515,6 518,9 @@ ast_function_nparams(struct ast_function *f);
struct ast_variable **
ast_function_params(struct ast_function *f);

struct ast_stmt *
ast_function_preconditions(struct ast_function *f);

struct externals;
struct error;



@@ 526,6 532,9 @@ struct result;
struct result *
ast_function_absexec(struct ast_function *, struct state *state);

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

struct ast_externdecl;

struct ast_externdecl *

M src/0v/ast/expr/expr.h => src/0v/ast/expr/expr.h +3 -0
@@ 78,6 78,9 @@ ast_expr_binary_op(struct ast_expr *);
struct ast_stmt_splits
ast_expr_splits(struct ast_expr *, struct state *);

struct error *
ast_expr_precondsverify(struct ast_expr *, struct state *);

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

M src/0v/ast/expr/verify.c => src/0v/ast/expr/verify.c +26 -3
@@ 397,6 397,7 @@ address_eval(struct ast_expr *, struct state *);
static struct result *
expr_unary_eval(struct ast_expr *expr, struct state *state)
{
	printf("expr: %s\n", ast_expr_str(expr));
	switch (ast_expr_unary_op(expr)) {
	case UNARY_OP_DEREFERENCE:
		return dereference_eval(expr, state);


@@ 542,6 543,7 @@ expr_call_eval(struct ast_expr *expr, struct state *state)
		strbuilder_printf(b, "function `%s' not found", name);
		return result_error_create(error_create(strbuilder_build(b)));
	}

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



@@ 585,13 587,18 @@ static struct result *
call_arbitraryresult(struct ast_expr *call, struct ast_function *, struct state *);

static struct result *
call_absexec(struct ast_expr *expr, struct ast_function *f, struct state *state)
call_absexec(struct ast_expr *expr, struct ast_function *f, struct state *s)
{
	struct result *res = ast_function_absexec(f, state);
	struct error *err = ast_function_precondsverify(f, s);
	if (err) {
		return result_error_create(err);
	}

	struct result *res = ast_function_absexec(f, s);
	if (result_iserror(res) || result_hasvalue(res)) {
		return res;
	}
	return call_arbitraryresult(expr, f, state);
	return call_arbitraryresult(expr, f, s);
}

static struct result *


@@ 1071,3 1078,19 @@ binary_assume(struct ast_expr *expr, bool value, struct state *s)
		s
	);
}

struct error *
ast_expr_precondsverify(struct ast_expr *e, struct state *s)
{
	struct props *p = state_getprops(s);

	assert(!props_contradicts(p, e));

	bool valid = props_get(p, e);
	if (!valid) {
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(b, "prop: %s is not present in state", ast_expr_str(e));
		return error_create(strbuilder_build(b));		
	}
	return NULL;
}

M src/0v/ast/function/function.c => src/0v/ast/function/function.c +30 -0
@@ 176,6 176,21 @@ ast_function_params(struct ast_function *f)
	return f->param;
}

struct ast_stmt *
ast_function_preconds(struct ast_function *f)
{
	/* XXX: should we allow multiple pre tags */
	struct ast_block *b = ast_function_abstract(f);	
	int n = ast_block_nstmts(b);
	struct ast_stmt **stmt = ast_block_stmts(b);
	for (int i = 0; i < n; i++) {
		if (ast_stmt_ispre(stmt[i])) {
			return ast_stmt_labelled_stmt(stmt[i]);
		}							
	}
	return NULL;
}

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


@@ 384,6 399,7 @@ split_path_verify(struct ast_function *f, struct state *state, int index,
{
	struct error *err = NULL;

	printf("func: %s\n", ast_function_str(f));
	struct ast_function_arr *paths = body_paths(f, index, cond);
	int n = ast_function_arr_len(paths);
	assert(n == 2);


@@ 392,9 408,11 @@ split_path_verify(struct ast_function *f, struct state *state, int index,
		struct state *s_copy = state_copywithname(
			state, ast_function_name(func[i])
		);
		printf("state (before): %s\n", state_str(s_copy));
		struct preresult *r = ast_expr_assume(
			ast_expr_inverted_copy(cond, i==1), s_copy
		);
		printf("state (after): %s\n", state_str(s_copy));
		if (preresult_iserror(r)) {
			return preresult_as_error(r);
		}


@@ 404,6 422,8 @@ split_path_verify(struct ast_function *f, struct state *state, int index,
				return err;
			}
		}
		/* XXX: error? */

		/*state_destroy(s_copy);*/
	}
	return NULL;


@@ 532,6 552,16 @@ ast_function_absexec(struct ast_function *f, struct state *state)
	return result_value_create(object_as_value(obj));
}

struct error *
ast_function_precondsverify(struct ast_function *f, struct state *s)
{
	struct ast_stmt *stmt = ast_function_preconds(f);
	if (!stmt) {
		return NULL;
	}
	return ast_stmt_precondsverify(stmt, s);
}

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


M src/0v/ast/stmt/stmt.h => src/0v/ast/stmt/stmt.h +3 -0
@@ 43,4 43,7 @@ struct error;
struct decision { bool decision; struct error *err; }
sel_decide(struct ast_expr *control, struct state *state);

struct error *
ast_stmt_precondsverify(struct ast_stmt *, struct state *);

#endif

M src/0v/ast/stmt/verify.c => src/0v/ast/stmt/verify.c +39 -42
@@ 175,6 175,8 @@ stmt_jump_exec(struct ast_stmt *stmt, struct state *state);
struct error *
ast_stmt_exec(struct ast_stmt *stmt, struct state *state)
{
	printf("stmt: %s\n", ast_stmt_str(stmt));
	printf("state: %s\n", state_str(state));
	switch (ast_stmt_kind(stmt)) {
	case STMT_LABELLED:
		return ast_stmt_exec(ast_stmt_labelled_stmt(stmt), state);


@@ 301,9 303,6 @@ stmt_jump_exec(struct ast_stmt *stmt, struct state *state)
}

static struct result *
labelled_absexec(struct ast_stmt *stmt, struct state *state);

static struct result *
sel_absexec(struct ast_stmt *stmt, struct state *state);

static struct result *


@@ 320,7 319,9 @@ ast_stmt_absexec(struct ast_stmt *stmt, struct state *state)
{
	switch (ast_stmt_kind(stmt)) {
	case STMT_LABELLED:
		return labelled_absexec(stmt, state);
		/* labelled statements are verified not executed when we
		 * transitively call a function */
		return result_value_create(NULL);
	case STMT_EXPR:
		return ast_expr_absexec(ast_stmt_as_expr(stmt), state);
	case STMT_SELECTION:


@@ 336,44 337,6 @@ ast_stmt_absexec(struct ast_stmt *stmt, struct state *state)
	}
}

static struct result *
verify_precondition(struct ast_stmt *stmt, struct state *state)
{
	struct props *p = state_getprops(state);
	struct ast_expr *e = ast_stmt_as_expr(stmt);
	bool valid = props_get(p, e);
	if (!valid) {
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(b, "prop: %s is not present in state", ast_expr_str(e));
		return result_error_create(error_create(strbuilder_build(b)));		
	}
	return result_value_create(NULL);
}

static struct result *
labelled_compound_absexec(struct ast_stmt *stmt, struct state *state);

static struct result *
labelled_absexec(struct ast_stmt *stmt, struct state *state)
{
	struct ast_stmt *nest = ast_stmt_labelled_stmt(stmt);

	switch (ast_stmt_kind(nest)) {
	case STMT_EXPR:
		return verify_precondition(nest, state);
	case STMT_COMPOUND:
		return labelled_compound_absexec(nest, state);	
	default:
		assert(false);
	}
}

static struct result *
labelled_compound_absexec(struct ast_stmt *stmt, struct state *state)
{
	assert(false);	
}

static struct ast_stmt *
hack_alloc_from_neteffect(struct ast_stmt *);



@@ 580,3 543,37 @@ alloc_process(struct ast_stmt *alloc, struct state *state)
	value_destroy(val);
	return result_value_create(NULL);
}

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

struct error *
ast_stmt_precondsverify(struct ast_stmt *stmt, struct state *s)
{
	/* TODO: converge pre: and pre: { ... } in ast */
	switch (ast_stmt_kind(stmt)) {
	case STMT_EXPR:
		return ast_expr_precondsverify(ast_stmt_as_expr(stmt), s);
	case STMT_COMPOUND:
		return ast_stmt_compound_precondsverify(stmt, s);
	default:
		assert(false);
	}
}

static struct error *
ast_stmt_compound_precondsverify(struct ast_stmt *stmt, struct state *s)
{
	struct error *err;

	struct ast_block *b = ast_stmt_as_block(stmt);
	int n = ast_block_nstmts(b);
	struct ast_stmt **stmts = ast_block_stmts(b);

	for (int i = 0; i < n; i++) {
		if ((err = ast_stmt_precondsverify(stmts[i], s))) {
			return err;
		}
	}
	return NULL;
}

M tests/6-preconditions/000-basic.x => tests/6-preconditions/000-basic.x +7 -0
@@ 27,6 27,12 @@ main()
        scanf("%d", &x);
	puts("Enter y: ");
        scanf("%d", &y);

	if (y != 0) {
		free(res); 
		/* XXX: should be `exit'. ignore memory concerns for `exit'? */
		return 0;
	}
	
	r = ratio(x, y);



@@ 35,4 41,5 @@ main()
        puts(res);

	free(res);
	return 1;
}