~lbnz/xr0

7bc4cb3e316c09190cc3bbc5397561815d7b9bc3 — Amisi Kiarie 3 months ago 5e4586d
checkpoint
32 files changed, 54 insertions(+), 41 deletions(-)

M include/ast.h
M src/ast/function/function.c
M src/ast/stmt/verify.c
M src/state/state.c
M tests/0-basic/000-FAIL-naked-alloc.x.EXPECTED
M tests/0-basic/010-FAIL-non-returned-alloc.x.EXPECTED
M tests/0-basic/020-FAIL-annotation.x.EXPECTED
M tests/0-basic/041-FAIL-false-alloc-void.x.EXPECTED
M tests/0-basic/060-FAIL-two-allocs.x.EXPECTED
M tests/0-basic/130-FAIL-double-free.x.EXPECTED
M tests/0-basic/140-FAIL-sync-free.x.EXPECTED
M tests/0-basic/170-FAIL-double-free.x.EXPECTED
M tests/0-basic/180-FAIL-alloc-freed.x.EXPECTED
M tests/1-branches/0310-FAIL-conditional-allocation-body.x.EXPECTED
M tests/1-branches/0320-FAIL-conditional-allocation-body.x.EXPECTED
M tests/6-preconditions/100-FAIL-need-alloced-lval.x.EXPECTED
M tests/6-preconditions/101-FAIL-need-alloced-rval.x.EXPECTED
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.EXPECTED
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.EXPECTED
M tests/7-use-after-free/300-FAIL-struct-free-ptr-dangling.x.EXPECTED
M tests/8-uninitialised-memory/000-FAIL-uninitialised-memory-rval.x.EXPECTED
M tests/8-uninitialised-memory/001-FAIL-uninitialised-memory-rval.x.EXPECTED
M tests/8-uninitialised-memory/002-FAIL-uninitialised-memory-rval.x.EXPECTED
M tests/8-uninitialised-memory/003-FAIL-uninitialised-memory-rval.x.EXPECTED
M tests/8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x.EXPECTED
M include/ast.h => include/ast.h +1 -1
@@ 390,7 390,7 @@ struct ast_expr *
ast_stmt_as_expr(struct ast_stmt *);

struct error *
ast_stmt_process(struct ast_stmt *, struct state *);
ast_stmt_process(struct ast_stmt *, char *fname, struct state *);

struct preresult;


M src/ast/function/function.c => src/ast/function/function.c +15 -6
@@ 476,6 476,7 @@ path_verify(struct ast_function *f, struct state *actual_state, int index,
{
	struct error *err;

	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++) {


@@ 487,7 488,7 @@ path_verify(struct ast_function *f, struct state *actual_state, int index,
				f, actual_state, i, &splits, abstract_state
			);
		}
		if ((err = ast_stmt_process(stmt[i], actual_state))) {
		if ((err = ast_stmt_process(stmt[i], fname, actual_state))) {
			return err;
		}
		if (ast_stmt_isterminal(stmt[i], actual_state)) {


@@ 496,15 497,23 @@ path_verify(struct ast_function *f, struct state *actual_state, int index,
		/* result_destroy(res); */
	}
	if (state_hasgarbage(actual_state)) {
		v_printf("actual: %s\n", state_str(actual_state));
		return error_create("qed error: garbage on heap");
		v_printf("actual: %s", state_str(actual_state));
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(
			b, "%s: garbage on heap", ast_function_name(f)
		);
		return error_create(strbuilder_build(b));
	}
	
	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_create("qed error: actual and abstract states differ");
		/*v_printf("actual: %s\n", state_str(actual_state));*/
		/*v_printf("abstract: %s\n", state_str(abstract_state));*/
		struct strbuilder *b = strbuilder_create();
		strbuilder_printf(
			b, "%s: actual and abstract states differ", ast_function_name(f)
		);
		return error_create(strbuilder_build(b));
	}

	return NULL;

M src/ast/stmt/verify.c => src/ast/stmt/verify.c +2 -2
@@ 13,7 13,7 @@
#include "value.h"

struct error *
ast_stmt_process(struct ast_stmt *stmt, struct state *state)
ast_stmt_process(struct ast_stmt *stmt, char *fname, struct state *state)
{
	struct error *err;



@@ 33,7 33,7 @@ ast_stmt_process(struct ast_stmt *stmt, struct state *state)
		struct lexememarker *loc = ast_stmt_lexememarker(stmt); 
		assert(loc);
		char *m = lexememarker_str(loc);
		strbuilder_printf(b, "%s: cannot exec statement: %s", m, err->msg);
		strbuilder_printf(b, "%s:%s: cannot exec statement: %s", m, fname, err->msg);
		free(m);
		return error_create(strbuilder_build(b));
	}

M src/state/state.c => src/state/state.c +8 -4
@@ 112,7 112,9 @@ state_str(struct state *state)
	}
	free(ext);
	char *static_mem = static_memory_str(state->static_memory, "\t");
	strbuilder_printf(b, "%s\n", static_mem);
	if (strlen(static_mem) > 0) {
		strbuilder_printf(b, "%s\n", static_mem);
	}
	free(static_mem);
	char *vconst = vconst_str(state->vconst, "\t");
	if (strlen(vconst) > 0) {


@@ 120,7 122,9 @@ state_str(struct state *state)
	}
	free(vconst);
	char *clump = clump_str(state->clump, "\t");
	strbuilder_printf(b, "%s\n", clump);
	if (strlen(clump) > 0) {
		strbuilder_printf(b, "%s\n", clump);
	}
	free(clump);
	char *stack = stack_str(state->stack, state);
	strbuilder_printf(b, "%s\n", stack);


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

M tests/0-basic/000-FAIL-naked-alloc.x.EXPECTED => tests/0-basic/000-FAIL-naked-alloc.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
qed error: garbage on heap
leak: garbage on heap

M tests/0-basic/010-FAIL-non-returned-alloc.x.EXPECTED => tests/0-basic/010-FAIL-non-returned-alloc.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
qed error: garbage on heap
leak: garbage on heap

M tests/0-basic/020-FAIL-annotation.x.EXPECTED => tests/0-basic/020-FAIL-annotation.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
qed error: actual and abstract states differ
leak: actual and abstract states differ

M tests/0-basic/041-FAIL-false-alloc-void.x.EXPECTED => tests/0-basic/041-FAIL-false-alloc-void.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
qed error: actual and abstract states differ
unit: actual and abstract states differ

M tests/0-basic/060-FAIL-two-allocs.x.EXPECTED => tests/0-basic/060-FAIL-two-allocs.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
qed error: garbage on heap
leak: garbage on heap

M tests/0-basic/130-FAIL-double-free.x.EXPECTED => tests/0-basic/130-FAIL-double-free.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
0-basic/130-FAIL-double-free.x:10:9: cannot exec statement: double free
0-basic/130-FAIL-double-free.x:10:9:unit: cannot exec statement: double free

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: cannot exec statement: dealloc on non-location
0-basic/140-FAIL-sync-free.x:6:9:unit: cannot exec statement: dealloc on non-location

M tests/0-basic/170-FAIL-double-free.x.EXPECTED => tests/0-basic/170-FAIL-double-free.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
0-basic/170-FAIL-double-free.x:11:9: cannot exec statement: double free
0-basic/170-FAIL-double-free.x:11:9:unit: cannot exec statement: double free

M tests/0-basic/180-FAIL-alloc-freed.x.EXPECTED => tests/0-basic/180-FAIL-alloc-freed.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
qed error: actual and abstract states differ
unit: actual and abstract states differ

M tests/1-branches/0310-FAIL-conditional-allocation-body.x.EXPECTED => tests/1-branches/0310-FAIL-conditional-allocation-body.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
qed error: actual and abstract states differ
test | $0: actual and abstract states differ

M tests/1-branches/0320-FAIL-conditional-allocation-body.x.EXPECTED => tests/1-branches/0320-FAIL-conditional-allocation-body.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
qed error: actual and abstract states differ
test | !($0): actual and abstract states differ

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: 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' must be heap allocated

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: cannot exec statement: parameter 'x' must be rvalue
6-preconditions/101-FAIL-need-alloced-rval.x:21:13:main: cannot exec statement: parameter 'x' must be rvalue

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: 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' must be lvalue

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: 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' must be lvalue

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: 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 (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: 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 (rvalue)

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: 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 (rvalue)

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: 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 (rvalue)

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: 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 (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: 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 (rvalue)


M tests/7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x.EXPECTED => tests/7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x:27:8: cannot exec statement: undefined indirection: stack frame doesn't exist
7-use-after-free/210-FAIL-stack-frame-pop-dangling-assign.x:27:8:main: cannot exec statement: undefined indirection: stack frame doesn't exist

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: 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/8-uninitialised-memory/000-FAIL-uninitialised-memory-rval.x.EXPECTED => tests/8-uninitialised-memory/000-FAIL-uninitialised-memory-rval.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
8-uninitialised-memory/000-FAIL-uninitialised-memory-rval.x:7:7: cannot exec statement: undefined memory access: `j' has no value
8-uninitialised-memory/000-FAIL-uninitialised-memory-rval.x:7:7:main: cannot exec statement: undefined memory access: `j' has no value

M tests/8-uninitialised-memory/001-FAIL-uninitialised-memory-rval.x.EXPECTED => tests/8-uninitialised-memory/001-FAIL-uninitialised-memory-rval.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
8-uninitialised-memory/001-FAIL-uninitialised-memory-rval.x:7:8: cannot exec statement: undefined memory access: `p' has no value
8-uninitialised-memory/001-FAIL-uninitialised-memory-rval.x:7:8:undefined_memory1: cannot exec statement: undefined memory access: `p' has no value

M tests/8-uninitialised-memory/002-FAIL-uninitialised-memory-rval.x.EXPECTED => tests/8-uninitialised-memory/002-FAIL-uninitialised-memory-rval.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
8-uninitialised-memory/002-FAIL-uninitialised-memory-rval.x:9:8: cannot exec statement: undefined indirection (rvalue)
8-uninitialised-memory/002-FAIL-uninitialised-memory-rval.x:9:8:undefined_memory2: cannot exec statement: undefined indirection (rvalue)

M tests/8-uninitialised-memory/003-FAIL-uninitialised-memory-rval.x.EXPECTED => tests/8-uninitialised-memory/003-FAIL-uninitialised-memory-rval.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
8-uninitialised-memory/003-FAIL-uninitialised-memory-rval.x:10:8: cannot exec statement: undefined indirection (rvalue)
8-uninitialised-memory/003-FAIL-uninitialised-memory-rval.x:10:8:undefined_memory3: cannot exec statement: undefined indirection (rvalue)

M tests/8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x.EXPECTED => tests/8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x.EXPECTED +1 -1
@@ 1,1 1,1 @@
8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x:12:9: cannot exec statement: undefined memory access: `i' has no value
8-uninitialised-memory/004-FAIL-uninitialised-memory-rval.x:12:9:main: cannot exec statement: undefined memory access: `i' has no value