~lbnz/xr0

3a9adfdd13bed2f8fd2f041fee1b5cf2a9b4f8fe — Amisi Kiarie 2 months ago 7bc4cb3 feat/final-touches
checkpoint
30 files changed, 52 insertions(+), 38 deletions(-)

M editors/vim/syntax.vim
M src/ast/expr/verify.c
M src/ast/stmt/stmt.c
M src/ast/stmt/verify.c
M src/state/state.c
M tests/0-basic/140-FAIL-sync-free.x.EXPECTED
M tests/0-basic/200-free-param.x
M tests/5-pass-by-ptr/000-basic.x
M tests/6-preconditions/100-FAIL-need-alloced-lval.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
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
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/003-pass-in-rvalue.x
M tests/7-use-after-free/004-mix-multiple-levels.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
M tests/7-use-after-free/300-FAIL-struct-free-ptr-dangling.x
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
M editors/vim/syntax.vim => editors/vim/syntax.vim +1 -1
@@ 11,7 11,7 @@ syntax keyword	Operator        sizeof
syntax keyword	Keyword	        const exit
syntax keyword	Type	        unsigned int char double void bool size_t FILE
syntax keyword	Structure	struct enum union
syntax keyword	Conditional	if else for some while switch assume pre
syntax keyword	Conditional	if else for some while switch assume setup
syntax keyword	Include	        axiom malloc free realloc clump
syntax keyword	Label		case default
syntax keyword	Boolean		true false

M src/ast/expr/verify.c => src/ast/expr/verify.c +21 -8
@@ 492,14 492,14 @@ expr_identifier_eval(struct ast_expr *expr, struct state *state)
	struct object *obj = state_getobject(state, id);
	if (!obj) {
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(b, "unknown idenitfier `%s'", id);
		strbuilder_printf(b, "unknown idenitfier %s", id);
		return result_error_create(error_create(strbuilder_build(b)));
	}
	struct value *val = object_as_value(obj);
	if (!val) {
		printf("state: %s\n", state_str(state));
		v_printf("state: %s\n", state_str(state));
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(b, "undefined memory access: `%s' has no value", id);
		strbuilder_printf(b, "undefined memory access: %s has no value", id);
		return result_error_create(error_create(strbuilder_build(b)));
	}
	return result_value_create(value_copy(val));


@@ 584,13 584,21 @@ binary_deref_eval(struct ast_expr *expr, struct state *state)
		return result_error_create(deref_res.err);
	}
	if (!deref_res.obj) {
		return result_error_create(error_create("undefined indirection (rvalue)"));
		struct strbuilder *b = strbuilder_create();
		char *s = ast_expr_str(expr);
		strbuilder_printf(b, "undefined indirection: *(%s) has no value", s);
		free(s);
		return result_error_create(error_create(strbuilder_build(b)));
	}
	result_destroy(res);

	struct value *v = object_as_value(deref_res.obj);
	if (!v) {
		return result_error_create(error_create("undefined indirection (rvalue)"));
		struct strbuilder *b = strbuilder_create();
		char *s = ast_expr_str(expr);
		strbuilder_printf(b, "undefined indirection: *(%s) has no value", s);
		free(s);
		return result_error_create(error_create(strbuilder_build(b)));
	}

	return result_value_create(value_copy(v));


@@ 762,8 770,9 @@ call_setupverify(struct ast_function *f, struct state *arg_state)
{
	struct error *err;

	char *fname = ast_function_name(f);
	struct state *param_state = state_create(
		dynamic_str(ast_function_name(f)),
		dynamic_str(fname),
		state_getext(arg_state),
		ast_function_type(f)
	);


@@ 779,7 788,7 @@ call_setupverify(struct ast_function *f, struct state *arg_state)
		struct value *arg = state_getloc(arg_state, id);
		if ((err = verify_paramspec(param, arg, param_state, arg_state))) {
			struct strbuilder *b = strbuilder_create();
			strbuilder_printf(b, "parameter '%s' %s", id, err->msg);
			strbuilder_printf(b, "parameter %s of %s %s", id, fname, err->msg);
			return error_create(strbuilder_build(b));
		}
	}


@@ 968,7 977,11 @@ expr_assign_eval(struct ast_expr *expr, struct state *state)
	}
	struct object *obj = lvalue_object(lval_res.lval);
	if (!obj) {
		return result_error_create(error_create("undefined indirection (lvalue)"));
		struct strbuilder *b = strbuilder_create();
		char *s = ast_expr_str(lval);
		strbuilder_printf(b, "undefined indirection: %s is not an lvalue", s);
		free(s);
		return result_error_create(error_create(strbuilder_build(b)));
	}

	object_assign(obj, value_copy(result_as_value(res)));

M src/ast/stmt/stmt.c => src/ast/stmt/stmt.c +1 -1
@@ 91,7 91,7 @@ bool
ast_stmt_ispre(struct ast_stmt *stmt)
{
	return stmt->kind == STMT_LABELLED
		&& strcmp(stmt->u.labelled.label, "pre") == 0;
		&& strcmp(stmt->u.labelled.label, "setup") == 0;
}

bool

M src/ast/stmt/verify.c => src/ast/stmt/verify.c +1 -0
@@ 342,6 342,7 @@ static struct result *
labelled_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup)
{
	if (!ast_stmt_ispre(stmt)) {
		printf("stmt: %s\n", ast_stmt_str(stmt));
		assert(false);
	}
	struct ast_stmt *setup = ast_stmt_labelled_stmt(stmt);

M src/state/state.c => src/state/state.c +1 -1
@@ 436,7 436,7 @@ struct error *
state_dealloc(struct state *state, struct value *val)
{
	if (!value_islocation(val)) {
		return error_create("dealloc on non-location");
		return error_create("undefined free of value not pointing at heap");
	}
	return location_dealloc(value_as_location(val), state->heap);
}

M tests/0-basic/140-FAIL-sync-free.x.EXPECTED => tests/0-basic/140-FAIL-sync-free.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
0-basic/140-FAIL-sync-free.x:6:9:unit: cannot exec statement: dealloc on non-location
0-basic/140-FAIL-sync-free.x:6:9:unit: cannot exec statement: undefined free of value not pointing at heap

M tests/0-basic/200-free-param.x => tests/0-basic/200-free-param.x +1 -1
@@ 2,7 2,7 @@

void
unit(void *p) ~ [
	pre: p = .malloc(1);
	setup: p = .malloc(1);

	.free(p);
]{

M tests/5-pass-by-ptr/000-basic.x => tests/5-pass-by-ptr/000-basic.x +1 -1
@@ 2,7 2,7 @@

void *
assign(void *p) ~ [
	pre: p = .clump(1);
	setup: p = .clump(1);
	*p = 1;
] {
	/* TODO: internal verification */

M tests/6-preconditions/100-FAIL-need-alloced-lval.x => tests/6-preconditions/100-FAIL-need-alloced-lval.x +1 -1
@@ 2,7 2,7 @@

int
func(int *x) ~ [ 
	pre: x = .malloc(1);
	setup: x = .malloc(1);
	*x = 5;
]{
	*x = 5;	

M tests/6-preconditions/100-FAIL-need-alloced-lval.x.EXPECTED => tests/6-preconditions/100-FAIL-need-alloced-lval.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
6-preconditions/100-FAIL-need-alloced-lval.x:15:10:main: cannot exec statement: parameter 'x' must be heap allocated
6-preconditions/100-FAIL-need-alloced-lval.x:15:10:main: cannot exec statement: parameter x of func must be heap allocated

M tests/6-preconditions/101-FAIL-need-alloced-rval.x => tests/6-preconditions/101-FAIL-need-alloced-rval.x +1 -1
@@ 3,7 3,7 @@
int
func(int *x) ~ [ 
	int i;
	pre: {
	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 +1 -1
@@ 1,1 1,1 @@
6-preconditions/101-FAIL-need-alloced-rval.x:21:13:main: cannot exec statement: parameter 'x' must be rvalue
6-preconditions/101-FAIL-need-alloced-rval.x:21:13:main: cannot exec statement: parameter x of func must be rvalue

M tests/6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x => tests/6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x +1 -1
@@ 2,7 2,7 @@

int
func(int *x) ~ [ 
	pre: x = .clump(1);
	setup: x = .clump(1);
]{
}


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 +1 -1
@@ 1,1 1,1 @@
6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x:16:9:main: cannot exec statement: parameter 'x' must be lvalue
6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x:16:9:main: cannot exec statement: parameter x of func must be lvalue

M tests/6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x => tests/6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x +1 -1
@@ 2,7 2,7 @@

int
func(int *x) ~ [ 
	pre: x = .clump(1);
	setup: x = .clump(1);
]{
	
}

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 +1 -1
@@ 1,1 1,1 @@
6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x:16:9:main: cannot exec statement: parameter 'x' must be lvalue
6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x:16:9:main: cannot exec statement: parameter x of func must be lvalue

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

M tests/7-use-after-free/003-pass-in-rvalue.x => tests/7-use-after-free/003-pass-in-rvalue.x +1 -1
@@ 1,6 1,6 @@
void
assign(int *q) ~ [
	pre: {
	setup: {
		q = .clump(sizeof(int));
		*q = $;
	}

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


@@ 16,7 16,7 @@ snapshot_and_change(int *arg) ~ [
void
modify(int *p, int *q) ~ [
	int i;
	pre: {
	setup: {
		p = .clump(sizeof(int));
		*p = $;
		q = .clump(sizeof(int));

M tests/7-use-after-free/005-conditions.x => tests/7-use-after-free/005-conditions.x +2 -2
@@ 1,6 1,6 @@
void
modify0(int *q, int x) ~ [
	pre: q = .clump(1);
	setup: q = .clump(1);
	if (x) {
		*q = 1;
	}


@@ 13,7 13,7 @@ modify0(int *q, int x) ~ [
void
modify1(int *q, int x) ~ [
	if (x) {
		pre: q = .clump(1);
		setup: q = .clump(1);
		*q = 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: cannot exec statement: undefined indirection (lvalue)
7-use-after-free/100-FAIL-lvalue-use-after-free.x:11:8:func: cannot exec statement: undefined indirection: *(p) is not an lvalue

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: cannot exec statement: undefined indirection (rvalue)
7-use-after-free/101-FAIL-rvalue-use-after-free.x:12:8:func: cannot exec statement: undefined indirection: *(p+0) has no value

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: cannot exec statement: undefined indirection (rvalue)
7-use-after-free/110-FAIL-freed-ptr-dangling-return.x:21:8:main: cannot exec statement: undefined indirection: *(i+0) has no value

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: cannot exec statement: undefined indirection (rvalue)
7-use-after-free/112-FAIL-freed-ptr-dangling-false-claim.x:21:8:main: cannot exec statement: undefined indirection: *(i+0) has no value

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: cannot exec statement: undefined indirection (lvalue)
7-use-after-free/120-FAIL-freed-ptr-maybe-dangling-return.x:34:8:main: cannot exec statement: undefined indirection: *(j) is not an lvalue

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,2 1,2 @@
7-use-after-free/200-FAIL-stack-frame-pop-dangling-return.x:19:8:main: cannot exec statement: undefined indirection (rvalue)
7-use-after-free/200-FAIL-stack-frame-pop-dangling-return.x:19:8:main: cannot exec statement: undefined indirection: *(p+0) has no value


M tests/7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x => tests/7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x +1 -1
@@ 4,7 4,7 @@ void
dangling_assign(int **i) ~ [
	int j;

	pre: i = .clump(sizeof(int *));
	setup: i = .clump(sizeof(int *));

	j = 5;
 	*i = &j;

M tests/7-use-after-free/300-FAIL-struct-free-ptr-dangling.x => tests/7-use-after-free/300-FAIL-struct-free-ptr-dangling.x +1 -1
@@ 15,7 15,7 @@ struct score *
create_score(char *subject, int grade) ~ [
	struct score *s;

	pre: subject = .malloc(sizeof(char *) * 100);
	setup: subject = .malloc(sizeof(char *) * 100);

	s = .malloc(sizeof(struct score));
	s->subject = subject;

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 +1 -1
@@ 1,1 1,1 @@
7-use-after-free/300-FAIL-struct-free-ptr-dangling.x:45:18:create_report: cannot exec statement: parameter 's' must be lvalue
7-use-after-free/300-FAIL-struct-free-ptr-dangling.x:45:18:create_report: cannot exec statement: parameter s must be lvalue

M tests/7-use-after-free/400-FAIL-conditions-in-setup.x => tests/7-use-after-free/400-FAIL-conditions-in-setup.x +1 -1
@@ 1,6 1,6 @@
void
modify2(int *q, int x) ~ [
	pre: if (x) { q = .clump(1); } /* ERROR: setup must be decidable */
	setup: if (x) { q = .clump(1); } /* ERROR: setup must be decidable */
	if (x) {
		*q = 2;
	}