~lbnz/xr0

f6343ea7036409f5d270b48ab8340738ecf048ab — Xr0 Team 4 months ago 3df6aa9 feat/check-preconditions
feat: add caller precondition checking
M include/ast.h => include/ast.h +3 -0
@@ 30,6 30,9 @@ struct ast_expr *
ast_expr_bracketed_create(struct ast_expr *);

struct ast_expr *
ast_expr_bracketed_root(struct ast_expr *);

struct ast_expr *
ast_expr_iteration_create();

struct ast_expr *

M src/0v/ast/expr/expr.c => src/0v/ast/expr/expr.c +7 -0
@@ 144,6 144,13 @@ ast_expr_bracketed_create(struct ast_expr *root)
	return expr;
}

struct ast_expr *
ast_expr_bracketed_root(struct ast_expr *expr)
{
	assert(expr->kind == EXPR_BRACKETED);
	return expr->root;
}

static void
ast_expr_bracketed_str_build(struct ast_expr *expr, struct strbuilder *b)
{

M src/0v/ast/expr/verify.c => src/0v/ast/expr/verify.c +21 -3
@@ 361,6 361,10 @@ expr_identifier_eval(struct ast_expr *expr, struct state *state)
	}

	char *id = ast_expr_as_identifier(expr);
	if (id[0] == '#') {
		return result_value_create(value_literal_create(id));
	}

	struct object *obj = state_getobject(state, id);
	if (!obj) {
		struct strbuilder *b = strbuilder_create();


@@ 397,12 401,16 @@ 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);
	case UNARY_OP_ADDRESS:
		return address_eval(expr, state);
	case UNARY_OP_BANG:
		/* hack because we stmt_exec pre as a preproces to verify
		 * constructors, this breaks any preconditions like: pre: !(p ==
		 * 0) */
		return result_value_create(value_literal_create("hi"));
	default:
		assert(false);
	}


@@ 930,6 938,8 @@ ast_expr_pf_reduce(struct ast_expr *e, struct state *s)
		return call_pf_reduce(e, s);
	case EXPR_STRUCTMEMBER:
		return structmember_pf_reduce(e, s);
	case EXPR_BRACKETED:
		return ast_expr_pf_reduce(ast_expr_bracketed_root(e), s);
	default:
		assert(false);
	}


@@ 1085,8 1095,16 @@ 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);
	
	/* XXX: hack ignore m = matrix_create($, $) */
	if (ast_expr_kind(e) == EXPR_ASSIGNMENT) {
		return NULL;
	}
		
	struct result *red = ast_expr_pf_reduce(e, s);
	struct value *v = result_as_value(red);
	struct ast_expr *red_e = value_to_expr(v);
	bool valid = props_get(p, red_e);
	if (!valid) {
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(b, "prop: %s is not present in state", ast_expr_str(e));

M src/0v/ast/function/function.c => src/0v/ast/function/function.c +0 -3
@@ 399,7 399,6 @@ 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);


@@ 408,11 407,9 @@ 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);
		}

M src/0v/ast/stmt/verify.c => src/0v/ast/stmt/verify.c +1 -3
@@ 52,6 52,7 @@ ast_stmt_preprocess(struct ast_stmt *stmt, struct state *state)
			return preresult_error_create(err);
		}
	} else if (ast_stmt_isassume(stmt)) {
		printf("assume: %s\n", ast_stmt_str(stmt));
		return stmt_installprop(stmt, state);
	}
	return preresult_empty_create();


@@ 175,8 176,6 @@ 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);


@@ 550,7 549,6 @@ 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);

M tests/6-preconditions/000-basic.x => tests/6-preconditions/000-basic.x +9 -7
@@ 2,8 2,9 @@
#include <stdlib.h>

int
ratio(int x, int y) ~ [
	pre: y != 0;
ratio(int x, int y) ~ [ 
	/* XXX: need logic engine to phrase nicely i.e. y != 0; */
	pre: !(y == 0);
	result = x/y;
]{
	return x/y;


@@ 28,12 29,13 @@ main()
	puts("Enter y: ");
        scanf("%d", &y);

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

	r = ratio(x, y);

	/* use sprintf to convert int to string */


@@ 41,5 43,5 @@ main()
        puts(res);

	free(res);
	return 1;
	return 0;
}