M Makefile => Makefile +13 -1
@@ 33,8 33,10 @@ MAIN_0V_OBJ = $(BUILD_DIR)/0v.o
MAIN_0C_OBJ = $(BUILD_DIR)/0c.o
STATE_OBJ = $(BUILD_DIR)/state.o
+STATIC_OBJ = $(BUILD_DIR)/static.o
STACK_OBJ = $(BUILD_DIR)/stack.o
HEAP_OBJ = $(BUILD_DIR)/heap.o
+CLUMP_OBJ = $(BUILD_DIR)/clump.o
LOCATION_OBJ = $(BUILD_DIR)/location.o
BLOCK_OBJ = $(BUILD_DIR)/block.o
EXT_OBJ = $(BUILD_DIR)/ext.o
@@ 63,8 65,10 @@ STATE_OBJECTS = $(VALUE_OBJ) \
$(LOCATION_OBJ) \
$(OBJECT_OBJ) \
$(BLOCK_OBJ) \
+ $(CLUMP_OBJ) \
$(HEAP_OBJ) \
$(STACK_OBJ) \
+ $(STATIC_OBJ) \
$(EXT_OBJ) \
$(PROPS_OBJ)
@@ 75,7 79,7 @@ $(XR0V): $(MAIN_0V_OBJ) $(BIN_DIR)
@$(CC) $(CFLAGS) -o $@ $(MAIN_0V_OBJ) $(OBJECTS)
lex: $(XR0V)
- $(VALGRIND) $(XR0V) -I libx tests/5-program/100-lex/parse.x
+ $(VALGRIND) $(XR0V) -I libx tests/99-program/100-lex/parse.x
PARSER = $(BUILD_DIR)/lex-gen
@@ 129,6 133,14 @@ $(HEAP_OBJ): $(STATE_DIR)/heap.c $(BLOCK_OBJ)
@printf 'CC\t$@\n'
@$(CC) $(CFLAGS) -o $@ -c $(STATE_DIR)/heap.c
+$(CLUMP_OBJ): $(STATE_DIR)/clump.c $(BLOCK_OBJ)
+ @printf 'CC\t$@\n'
+ @$(CC) $(CFLAGS) -o $@ -c $(STATE_DIR)/clump.c
+
+$(STATIC_OBJ): $(STATE_DIR)/static.c $(BLOCK_OBJ)
+ @printf 'CC\t$@\n'
+ @$(CC) $(CFLAGS) -o $@ -c $(STATE_DIR)/static.c
+
$(BLOCK_OBJ): $(STATE_DIR)/block.c $(OBJECT_OBJ)
@printf 'CC\t$@\n'
@$(CC) $(CFLAGS) -o $@ -c $(STATE_DIR)/block.c
M editors/vim/syntax.vim => editors/vim/syntax.vim +1 -1
@@ 12,7 12,7 @@ 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 Include axiom alloc dealloc realloc
+syntax keyword Include axiom alloc dealloc realloc clump
syntax keyword Label case default
syntax keyword Boolean true false
syntax keyword Exception return result undefined
M include/ast.h => include/ast.h +53 -12
@@ 1,6 1,8 @@
#ifndef XR0_AST_H
#define XR0_AST_H
+
#include <stdbool.h>
+
#include "util.h"
struct ast_expr;
@@ 131,6 133,15 @@ struct ast_expr *
ast_expr_isdeallocand_assertand(struct ast_expr *expr);
struct ast_expr *
+ast_expr_isdereferencable_create(struct ast_expr *assertand);
+
+struct ast_expr *
+ast_expr_isdereferencable_assertand(struct ast_expr *expr);
+
+bool
+ast_expr_isisdereferencable(struct ast_expr *expr);
+
+struct ast_expr *
ast_expr_arbarg_create();
void
@@ 167,12 178,17 @@ struct preresult;
struct preresult *
ast_expr_assume(struct ast_expr *, struct state *);
-struct error *
-ast_expr_precondsverify(struct ast_expr *, struct state *);
+void
+ast_expr_varinfomap(struct map *, struct ast_expr *, struct state *s);
struct lvalue;
-struct lvalue *
+struct lvalue_res {
+ struct lvalue *lval;
+ struct error *err;
+};
+
+struct lvalue_res
ast_expr_lvalue(struct ast_expr *, struct state *);
struct result *
@@ 221,10 237,14 @@ ast_block_stmts(struct ast_block *b);
bool
ast_block_isterminal(struct ast_block *, struct state *);
-enum ast_jump_kind {
- JUMP_RETURN = 1 << 0,
+struct preconds_result {
+ struct ast_stmt *stmt;
+ struct error *err;
};
+struct preconds_result
+ast_block_preconds(struct ast_block *b);
+
struct ast_stmt;
struct lexememarker;
@@ 235,6 255,12 @@ ast_stmt_lexememarker(struct ast_stmt *);
struct ast_stmt *
ast_stmt_create_labelled(struct lexememarker *, char *label, struct ast_stmt *);
+bool
+ast_stmt_ispre(struct ast_stmt *);
+
+struct error *
+ast_stmt_preconds_validate(struct ast_stmt *);
+
char *
ast_stmt_labelled_label(struct ast_stmt *);
@@ 300,6 326,10 @@ ast_stmt_as_block(struct ast_stmt *);
struct ast_stmt *
ast_stmt_create_compound_v(struct lexememarker *, struct ast_block *);
+enum ast_jump_kind {
+ JUMP_RETURN = 1 << 0,
+};
+
struct ast_stmt *
ast_stmt_create_jump(struct lexememarker *, enum ast_jump_kind, struct ast_expr *rv);
@@ 312,11 342,14 @@ ast_stmt_create_alloc(struct lexememarker *, struct ast_expr *arg);
struct ast_stmt *
ast_stmt_create_dealloc(struct lexememarker *, struct ast_expr *arg);
+struct ast_stmt *
+ast_stmt_create_clump(struct lexememarker *, struct ast_expr *arg);
+
struct ast_expr *
ast_stmt_alloc_arg(struct ast_stmt *);
-bool
-ast_stmt_alloc_isalloc(struct ast_stmt *);
+enum ast_alloc_kind
+ast_stmt_alloc_kind(struct ast_stmt *);
void
ast_stmt_destroy(struct ast_stmt *);
@@ 361,8 394,10 @@ struct error *
ast_stmt_exec(struct ast_stmt *, struct state *);
struct result *
-ast_stmt_absexec(struct ast_stmt *stmt, struct state *state);
+ast_stmt_absexec(struct ast_stmt *stmt, struct state *, bool iscall);
+struct error *
+ast_stmt_setupabsexec(struct ast_stmt *stmt, struct state *);
struct ast_type;
@@ 370,10 405,16 @@ struct ast_type;
bool
ast_type_isint(struct ast_type *type);
+bool
+ast_type_ispointer(struct ast_type *type);
+
struct ast_type *
ast_type_create_ptr(struct ast_type *type);
struct ast_type *
+ast_type_create_voidptr();
+
+struct ast_type *
ast_type_create_arr(struct ast_type *type, int length);
struct ast_variable_arr;
@@ 521,9 562,12 @@ ast_function_nparams(struct ast_function *f);
struct ast_variable **
ast_function_params(struct ast_function *f);
-struct ast_stmt *
+struct preconds_result
ast_function_preconditions(struct ast_function *f);
+struct error *
+ast_function_initparams(struct ast_function *, struct state *);
+
struct externals;
struct error;
@@ 535,9 579,6 @@ 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 include/object.h => include/object.h +8 -1
@@ 45,14 45,21 @@ bool
object_referencesheap(struct object *, struct state *);
bool
+object_hasvalue(struct object *);
+
+bool
object_isvalue(struct object *);
struct value *
object_as_value(struct object *);
-void
+struct error *
object_assign(struct object *, struct value *);
+struct error *
+object_transfigure(struct object *obj, struct value *val, struct state *actual,
+ struct state *compare, bool islval);
+
bool
object_contains(struct object *, struct ast_expr *, struct state *);
M include/props.h => include/props.h +6 -0
@@ 19,6 19,12 @@ props_str(struct props *, char *indent);
struct ast_expr;
+int
+props_n(struct props *);
+
+struct ast_expr **
+props_prop(struct props *);
+
void
props_install(struct props *, struct ast_expr *);
M include/state.h => include/state.h +37 -2
@@ 28,6 28,10 @@ struct state *
state_create(char *func, struct externals *, struct ast_type *result_type);
struct state *
+state_create_withprops(char *func, struct externals *, struct ast_type *result_type,
+ struct props *props);
+
+struct state *
state_copy(struct state *);
struct state *
@@ 45,6 49,9 @@ state_getext(struct state *);
struct props *
state_getprops(struct state *);
+struct heap *
+state_getheap(struct state *);
+
void
state_pushframe(struct state *, char *func, struct ast_type *ret_type);
@@ 66,7 73,7 @@ state_getobjecttype(struct state *, char *id);
struct value *
state_getloc(struct state *state, char *id);
-struct object *
+struct object_res
state_deref(struct state *, struct value *ptr, struct ast_expr *index);
struct value *
@@ 94,6 101,18 @@ struct value *
state_vconst(struct state *, struct ast_type *, char *comment, bool persist);
struct value *
+state_static_init(struct state *, struct ast_expr *);
+
+struct value *
+state_clump(struct state *);
+
+bool
+state_islval(struct state *, struct value *);
+
+bool
+state_isalloc(struct state *, struct value *);
+
+struct value *
state_getvconst(struct state *, char *id);
bool
@@ 122,7 141,15 @@ location_references(struct location *l1, struct location *l2, struct state *);
bool
location_referencesheap(struct location *, struct state *);
-struct object *
+struct value *
+location_transfigure(struct location *, struct state *compare);
+
+struct object_res {
+ struct object *obj;
+ struct error *err;
+};
+
+struct object_res
state_get(struct state *state, struct location *loc, bool constructive);
@@ 134,4 161,12 @@ state_isdeallocand(struct state *s, struct location *loc);
bool
state_eval(struct state *, struct ast_expr *);
+struct block;
+
+void
+state_blockinstall(struct block *, struct object *);
+
+struct block *
+state_getblock(struct state *, struct location *);
+
#endif
M include/util.h => include/util.h +0 -3
@@ 55,7 55,6 @@ strbuilder_build(struct strbuilder *b);
char *
strbuilder_preview(struct strbuilder *b);
-
struct error {
char *msg;
struct error *inner;
@@ 101,6 100,4 @@ string_arr_contains(struct string_arr *, char *s);
char *
string_arr_str(struct string_arr *);
-struct externals;
-
#endif
M include/value.h => include/value.h +3 -0
@@ 34,6 34,9 @@ value_int_ne_create(int not_val);
struct value *
value_int_range_create(int lw, int excl_up);
+struct value *
+value_transfigure(struct value *, struct state *compare, bool islval);
+
int
value_int_lw(struct value *);
M libx/stdio.h => libx/stdio.h +1 -1
@@ 15,7 15,7 @@ axiom int
fputs(char *s, FILE *stream);
axiom int
-puts(char *s);
+puts(char *s) ~ [ pre: .clump s; ];
axiom FILE *
fopen(char *pathname, char *mode);
M src/0v/ast/ast.c => src/0v/ast/ast.c +0 -1
@@ 214,4 214,3 @@ ast_protostitch(struct ast_function *f, struct externals *ext)
{
return ast_function_protostitch(f, ext);
}
-
M src/0v/ast/block.c => src/0v/ast/block.c +19 -0
@@ 141,3 141,22 @@ ast_block_isterminal(struct ast_block *b, struct state *s)
}
return false;
}
+
+struct preconds_result
+ast_block_preconds(struct ast_block *b)
+{
+ int n = ast_block_nstmts(b);
+ struct ast_stmt **stmt = ast_block_stmts(b);
+ for (int i = 0; i < n; i++) {
+ /* XXX: either enforce one pre block or concat */
+ if (ast_stmt_ispre(stmt[i])) {
+ struct ast_stmt *preconds = ast_stmt_labelled_stmt(stmt[i]);
+ struct error *err = ast_stmt_preconds_validate(preconds);
+ if (err) {
+ return (struct preconds_result) { .stmt = NULL, .err = err };
+ }
+ return (struct preconds_result) { .stmt = preconds, .err = NULL };
+ }
+ }
+ return (struct preconds_result) { .stmt = NULL, .err = NULL };
+}
M src/0v/ast/expr/expr.c => src/0v/ast/expr/expr.c +75 -33
@@ 4,6 4,7 @@
#include <string.h>
#include "ast.h"
+#include "intern.h"
#include "ext.h"
#include "expr.h"
#include "math.h"
@@ 409,6 410,9 @@ ast_expr_unary_operand(struct ast_expr *expr)
bool
ast_expr_unary_isdereference(struct ast_expr *expr)
{
+ if (ast_expr_kind(expr) != EXPR_UNARY) {
+ return false;
+ }
return ast_expr_unary_op(expr) == UNARY_OP_DEREFERENCE;
}
@@ 606,6 610,28 @@ ast_expr_isdeallocand_assertand(struct ast_expr *expr)
return expr->root;
}
+struct ast_expr *
+ast_expr_isdereferencable_create(struct ast_expr *assertand)
+{
+ struct ast_expr *new = ast_expr_create();
+ new->kind = EXPR_ISDEREFERENCABLE;
+ new->root = assertand;
+ return new;
+}
+
+struct ast_expr *
+ast_expr_isdereferencable_assertand(struct ast_expr *expr)
+{
+ assert(expr->kind == EXPR_ISDEREFERENCABLE);
+ return expr->root;
+}
+
+bool
+ast_expr_isisdereferencable(struct ast_expr *expr)
+{
+ return expr->kind == EXPR_ISDEREFERENCABLE;
+}
+
static void
ast_expr_isdeallocand_str_build(struct ast_expr *expr, struct strbuilder *b)
{
@@ 614,6 640,14 @@ ast_expr_isdeallocand_str_build(struct ast_expr *expr, struct strbuilder *b)
free(root);
}
+static void
+ast_expr_isdereferencable_str_build(struct ast_expr *expr, struct strbuilder *b)
+{
+ char *root = ast_expr_str(expr->root);
+ strbuilder_printf(b, "$%s", root);
+ free(root);
+}
+
struct ast_expr *
ast_expr_arbarg_create()
{
@@ 658,6 692,9 @@ ast_expr_destroy(struct ast_expr *expr)
case EXPR_ISDEALLOCAND:
ast_expr_destroy(expr->root);
break;
+ case EXPR_ISDEREFERENCABLE:
+ ast_expr_destroy(expr->root);
+ break;
case EXPR_ARBARG:
break;
default:
@@ 704,6 741,9 @@ ast_expr_str(struct ast_expr *expr)
case EXPR_ISDEALLOCAND:
ast_expr_isdeallocand_str_build(expr, b);
break;
+ case EXPR_ISDEREFERENCABLE:
+ ast_expr_isdereferencable_str_build(expr, b);
+ break;
case EXPR_ARBARG:
strbuilder_putc(b, '$');
break;
@@ 760,6 800,10 @@ ast_expr_copy(struct ast_expr *expr)
return ast_expr_isdeallocand_create(
ast_expr_copy(expr->root)
);
+ case EXPR_ISDEREFERENCABLE:
+ return ast_expr_isdereferencable_create(
+ ast_expr_copy(expr->root)
+ );
case EXPR_ARBARG:
return ast_expr_arbarg_create();
default:
@@ 919,6 963,7 @@ ast_expr_getfuncs(struct ast_expr *expr)
case EXPR_STRING_LITERAL:
case EXPR_STRUCTMEMBER:
case EXPR_ISDEALLOCAND:
+ case EXPR_ISDEREFERENCABLE:
case EXPR_ARBARG:
return string_arr_create();
case EXPR_CALL:
@@ 968,42 1013,28 @@ ast_expr_splits(struct ast_expr *e, struct state *s)
case EXPR_IDENTIFIER:
case EXPR_STRING_LITERAL:
case EXPR_ARBARG:
- return (struct ast_stmt_splits) { .n = 0, .cond = NULL };
+ case EXPR_ISDEREFERENCABLE:
+ return (struct ast_stmt_splits) { .n = 0, .cond = NULL, .err = NULL };
default:
- /*printf("expr: %s\n", ast_expr_str(e));*/
assert(false);
}
}
-static struct string_arr *
-ast_expr_call_getfuncs(struct ast_expr *expr)
-{
- struct string_arr *res = string_arr_create();
- struct ast_expr *root = expr->root;
- assert(root->kind == EXPR_IDENTIFIER);
- string_arr_append(res, dynamic_str(root->u.string));
- for (int i = 0; i < expr->u.call.n; i++) {
- res = string_arr_concat(
- res,
- ast_expr_getfuncs(expr->u.call.arg[i])
- );
- /* XXX: leaks */
- }
- return res;
-}
-
static struct ast_stmt_splits
call_splits(struct ast_expr *expr, struct state *state)
{
+ struct error *err;
+
struct ast_expr *root = ast_expr_call_root(expr);
/* TODO: function-valued-expressions */
char *name = ast_expr_as_identifier(root);
struct ast_function *f = externals_getfunc(state_getext(state), name);
if (!f) {
- /* TODO: user error */
- fprintf(stdout, "function `%s' not found\n", name);
- assert(false);
+ struct strbuilder *b = strbuilder_create();
+ strbuilder_printf(b, "function: `%s' not found", name);
+ err = error_create(strbuilder_build(b));
+ return (struct ast_stmt_splits) { .n = 0, .cond = NULL, .err = err };
}
int nparams = ast_function_nparams(f);
@@ 1019,20 1050,15 @@ call_splits(struct ast_expr *expr, struct state *state)
struct ast_type *ret_type = ast_function_type(f);
state_pushframe(s_copy, dynamic_str(name), ret_type);
- struct error *err = prepare_parameters(
- nparams, params, args, name, s_copy
- );
- if (err) {
- fprintf(stderr, "err: %s\n", err->msg);
+ if ((err = prepare_parameters( nparams, params, args, name, s_copy))) {
/* Sometimes a param is uninitialised e.g.
*
* int c;
* scanf("%d", &c);
*
* */
- /* assert(false); */
- }
-
+ return (struct ast_stmt_splits) { .n = 0, .cond = NULL, .err = err };
+ }
int n = 0;
struct ast_expr **cond = NULL;
@@ 1055,13 1081,12 @@ call_splits(struct ast_expr *expr, struct state *state)
cond[n-1] = splits.cond[j];
}
/* XXX: for assignment statements and, well, spare us */
- ast_stmt_absexec(stmt[i], s_copy);
}
state_popframe(s_copy);
result_arr_destroy(args);
- return (struct ast_stmt_splits) { .n = n, .cond = cond };
+ return (struct ast_stmt_splits) { .n = n, .cond = cond, .err = NULL };
}
static struct ast_stmt_splits
@@ 1079,7 1104,24 @@ binary_splits(struct ast_expr *e, struct state *s)
cond[i+s1.n] = s2.cond[i];
}
- return (struct ast_stmt_splits) { .n = n, .cond = cond };
+ return (struct ast_stmt_splits) { .n = n, .cond = cond, .err = NULL };
+}
+
+static struct string_arr *
+ast_expr_call_getfuncs(struct ast_expr *expr)
+{
+ struct string_arr *res = string_arr_create();
+ struct ast_expr *root = expr->root;
+ assert(root->kind == EXPR_IDENTIFIER);
+ string_arr_append(res, dynamic_str(root->u.string));
+ for (int i = 0; i < expr->u.call.n; i++) {
+ res = string_arr_concat(
+ res,
+ ast_expr_getfuncs(expr->u.call.arg[i])
+ );
+ /* XXX: leaks */
+ }
+ return res;
}
#include "verify.c"
M src/0v/ast/expr/expr.h => src/0v/ast/expr/expr.h +2 -5
@@ 22,7 22,8 @@ struct ast_expr {
EXPR_ASSIGNMENT = 1 << 10,
EXPR_ISDEALLOCAND = 1 << 11,
- EXPR_ARBARG = 1 << 12,
+ EXPR_ISDEREFERENCABLE = 1 << 12,
+ EXPR_ARBARG = 1 << 13,
} kind;
struct ast_expr *root;
union {
@@ 78,9 79,6 @@ 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;
@@ 95,7 93,6 @@ result_arr_destroy(struct result_arr *arr);
void
result_arr_append(struct result_arr *arr, struct result *res);
-
struct result_arr *
prepare_arguments(int nargs, struct ast_expr **arg, int nparams,
struct ast_variable **param, struct state *state);
M src/0v/ast/expr/verify.c => src/0v/ast/expr/verify.c +209 -95
@@ 28,6 28,8 @@ bool
ast_expr_decide(struct ast_expr *expr, struct state *state)
{
switch (ast_expr_kind(expr)) {
+ case EXPR_CONSTANT:
+ return (bool) ast_expr_as_constant(expr);
case EXPR_UNARY:
return expr_unary_decide(expr, state);
case EXPR_ISDEALLOCAND:
@@ 107,9 109,11 @@ expr_isdeallocand_rangedecide(struct ast_expr *expr, struct ast_expr *lw,
ast_expr_destroy(j);
ast_expr_destroy(i);
- struct object *obj = lvalue_object(
- ast_expr_lvalue(ast_expr_binary_e1(acc), state)
- );
+ struct lvalue_res res = ast_expr_lvalue(ast_expr_binary_e1(acc), state);
+ if (res.err) {
+ assert(false);
+ }
+ struct object *obj = lvalue_object(res.lval);
assert(obj);
return state_range_aredeallocands(state, obj, lw, up);
@@ 122,20 126,20 @@ ast_expr_exec(struct ast_expr *expr, struct state *state)
if (result_iserror(res)) {
return result_as_error(res);
}
- result_destroy(res);
+ /* result_destroy(res); */
return NULL;
}
-struct lvalue *
+struct lvalue_res
expr_identifier_lvalue(struct ast_expr *expr, struct state *state);
-struct lvalue *
+struct lvalue_res
expr_unary_lvalue(struct ast_expr *expr, struct state *state);
-struct lvalue *
+struct lvalue_res
expr_structmember_lvalue(struct ast_expr *expr, struct state *state);
-struct lvalue *
+struct lvalue_res
ast_expr_lvalue(struct ast_expr *expr, struct state *state)
{
switch (ast_expr_kind(expr)) {
@@ 150,18 154,18 @@ ast_expr_lvalue(struct ast_expr *expr, struct state *state)
}
}
-struct lvalue *
+struct lvalue_res
expr_identifier_lvalue(struct ast_expr *expr, struct state *state)
{
char *id = ast_expr_as_identifier(expr);
- return lvalue_create(
- state_getobjecttype(state, id),
- state_getobject(state, id)
- );
+ return (struct lvalue_res) {
+ .lval = lvalue_create( state_getobjecttype(state, id), state_getobject(state, id)),
+ .err = NULL
+ };
}
-struct lvalue *
+struct lvalue_res
expr_unary_lvalue(struct ast_expr *expr, struct state *state)
{
assert(ast_expr_unary_op(expr) == UNARY_OP_DEREFERENCE);
@@ 170,45 174,73 @@ expr_unary_lvalue(struct ast_expr *expr, struct state *state)
/* XXX: expr for args (scanf()) in function not of form `*(ptr+offset)
* for some reason */
if (ast_expr_kind(inner) == EXPR_IDENTIFIER) {
- return ast_expr_lvalue(inner, state);
+ struct lvalue_res root_res = ast_expr_lvalue(inner, state);
+ if (root_res.err) {
+ return root_res;
+ }
+ struct object *root_obj = lvalue_object(root_res.lval);
+ if (!root_obj) { /* `root` freed */
+ return (struct lvalue_res) { .lval = NULL, .err = NULL };
+ }
+ struct ast_type *t = ast_type_ptr_type(lvalue_type(root_res.lval));
+ struct value *root_val = object_as_value(root_obj);
+ assert(root_val);
+ struct object_res res = state_deref(
+ state, root_val, ast_expr_constant_create(0)
+ );
+ if (res.err) {
+ return (struct lvalue_res) { .lval = NULL, .err = res.err };
+ }
+ return (struct lvalue_res) { .lval = lvalue_create(t, res.obj), .err = NULL };
}
- struct lvalue *root = ast_expr_lvalue(ast_expr_binary_e1(inner), state);
- struct object *root_obj = lvalue_object(root);
+ struct lvalue_res root_res = ast_expr_lvalue(ast_expr_binary_e1(inner), state);
+ if (root_res.err) {
+ return root_res;
+ }
+ struct object *root_obj = lvalue_object(root_res.lval);
if (!root_obj) { /* `root` freed */
- return NULL;
+ return (struct lvalue_res) { .lval = NULL, .err = NULL };
}
- struct ast_type *t = ast_type_ptr_type(lvalue_type(root));
+ struct ast_type *t = ast_type_ptr_type(lvalue_type(root_res.lval));
struct value *root_val = object_as_value(root_obj);
assert(root_val);
- struct object *obj = state_deref(
+ struct object_res res = state_deref(
state, root_val, ast_expr_binary_e2(inner)
);
-
- return lvalue_create(t, obj);
+ if (res.err) {
+ return (struct lvalue_res) { .lval = NULL, .err = NULL };
+ }
+ return (struct lvalue_res) { .lval = lvalue_create(t, res.obj), .err = NULL };
}
-struct lvalue *
+struct lvalue_res
expr_structmember_lvalue(struct ast_expr *expr, struct state *state)
{
struct ast_expr *root = ast_expr_member_root(expr);
- struct lvalue *root_lval = ast_expr_lvalue(root, state);
- struct object *root_obj = lvalue_object(root_lval);
+ struct lvalue_res root_res = ast_expr_lvalue(root, state);
+ struct object *root_obj = lvalue_object(root_res.lval);
assert(root_obj);
char *field = ast_expr_member_field(expr);
struct object *member = object_getmember(
- root_obj, lvalue_type(root_lval), field, state
+ root_obj, lvalue_type(root_res.lval), field, state
);
if (!member) {
/* TODO: lvalue error */
- return lvalue_create(NULL, NULL);
+ return (struct lvalue_res) {
+ .lval = NULL,
+ .err = error_create("lvalue error")
+ };
}
struct ast_type *t = object_getmembertype(
- root_obj, lvalue_type(root_lval), field, state
+ root_obj, lvalue_type(root_res.lval), field, state
);
assert(t);
- return lvalue_create(t, member);
+ return (struct lvalue_res) {
+ .lval = lvalue_create(t, member),
+ .err = NULL
+ };
}
@@ 219,7 251,11 @@ hack_object_from_assertion(struct ast_expr *expr, struct state *state)
struct ast_expr *assertand = ast_expr_isdeallocand_assertand(expr);
/* get `assertand' variable */
- struct object *obj = lvalue_object(ast_expr_lvalue(assertand, state));
+ struct lvalue_res res = ast_expr_lvalue(assertand, state);
+ if (res.err) {
+ assert(false);
+ }
+ struct object *obj = lvalue_object(res.lval);
assert(obj);
return obj;
}
@@ 246,8 282,6 @@ expr_binary_decide(struct ast_expr *expr, struct state *state)
assert(!result_iserror(root) && !result_iserror(last));
- /*printf("state: %s\n", state_str(state));*/
- /*printf("expr: %s\n", ast_expr_str(expr));*/
return value_compare(
result_as_value(root),
ast_expr_binary_op(expr),
@@ 303,8 337,6 @@ arbarg_eval(struct ast_expr *expr, struct state *state);
struct result *
ast_expr_eval(struct ast_expr *expr, struct state *state)
{
- /* TODO: verify preconditions of expr (statement) are satisfied */
- /* now add postconditions */
switch (ast_expr_kind(expr)) {
case EXPR_CONSTANT:
return expr_constant_eval(expr, state);
@@ 334,9 366,10 @@ ast_expr_eval(struct ast_expr *expr, struct state *state)
static struct result *
expr_literal_eval(struct ast_expr *expr, struct state *state)
{
- return result_value_create(
- value_literal_create(ast_expr_as_literal(expr))
+ struct result *res = result_value_create(
+ state_static_init(state, expr)
);
+ return res;
}
static struct result *
@@ 375,7 408,7 @@ expr_identifier_eval(struct ast_expr *expr, struct state *state)
if (!val) {
printf("state: %s\n", state_str(state));
struct strbuilder *b = strbuilder_create();
- strbuilder_printf(b, "`%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));
@@ 455,12 488,19 @@ binary_deref_eval(struct ast_expr *expr, struct state *state)
}
struct value *arr = result_as_value(res);
assert(arr);
- struct object *obj = state_deref(state, arr, ast_expr_binary_e2(expr));
- assert(obj);
+ struct object_res deref_res = state_deref(state, arr, ast_expr_binary_e2(expr));
+ if (deref_res.err) {
+ return result_error_create(deref_res.err);
+ }
+ if (!deref_res.obj) {
+ return result_error_create(error_create("undefined indirection (rvalue)"));
+ }
result_destroy(res);
- struct value *v = object_as_value(obj);
- assert(v);
+ struct value *v = object_as_value(deref_res.obj);
+ if (!v) {
+ return result_error_create(error_create("undefined indirection (rvalue)"));
+ }
return result_value_create(value_copy(v));
}
@@ 532,8 572,11 @@ struct error *
prepare_parameters(int nparams, struct ast_variable **param,
struct result_arr *args, char *fname, struct state *state);
+static struct error *
+call_setupverify(struct ast_function *, struct state *state);
+
static struct result *
-call_absexec(struct ast_expr *call, struct ast_function *, struct state *);
+call_absexec(struct ast_expr *call, struct state *);
static struct result *
pf_augment(struct value *v, struct ast_expr *root, struct state *);
@@ 541,6 584,8 @@ pf_augment(struct value *v, struct ast_expr *root, struct state *);
static struct result *
expr_call_eval(struct ast_expr *expr, struct state *state)
{
+ struct error *err;
+
struct ast_expr *root = ast_expr_call_root(expr);
/* TODO: function-valued-expressions */
char *name = ast_expr_as_identifier(root);
@@ 554,6 599,7 @@ expr_call_eval(struct ast_expr *expr, struct state *state)
int nparams = ast_function_nparams(f);
struct ast_variable **params = ast_function_params(f);
+ struct ast_type *rtype = ast_function_type(f);
struct result_arr *args = prepare_arguments(
ast_expr_call_nargs(expr),
@@ 561,20 607,22 @@ expr_call_eval(struct ast_expr *expr, struct state *state)
nparams, params, state
);
- struct ast_type *ret_type = ast_function_type(f);
- state_pushframe(state, dynamic_str(name), ret_type);
+ state_pushframe(state, dynamic_str(name), rtype);
+ if ((err = prepare_parameters(nparams, params, args, name, state))) {
+ return result_error_create(err);
+ }
- struct error *err = prepare_parameters(
- nparams, params, args, name, state
- );
- if (err) {
+ /* XXX: pass copy so we don't observe */
+ if ((err = call_setupverify(f, state_copy(state)))) {
return result_error_create(err);
}
- struct result *res = call_absexec(expr, f, state);
+ struct result *res = call_absexec(expr, state);
if (result_iserror(res)) {
return res;
}
+
+ /* XXX: pass copy so we don't observe */
/* copy to preserve value through popping of frame */
struct value *v = NULL;
if (result_hasvalue(res)) {
@@ 595,13 643,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 *s)
+call_absexec(struct ast_expr *expr, struct state *s)
{
- struct error *err = ast_function_precondsverify(f, s);
- if (err) {
- return result_error_create(err);
- }
+ struct ast_expr *root = ast_expr_call_root(expr);
+ /* TODO: function-valued-expressions */
+ char *name = ast_expr_as_identifier(root);
+ struct ast_function *f = externals_getfunc(state_getext(s), name);
+ if (!f) {
+ struct strbuilder *b = strbuilder_create();
+ strbuilder_printf(b, "function `%s' not found", name);
+ return result_error_create(error_create(strbuilder_build(b)));
+ }
struct result *res = ast_function_absexec(f, s);
if (result_iserror(res) || result_hasvalue(res)) {
return res;
@@ 609,6 662,78 @@ call_absexec(struct ast_expr *expr, struct ast_function *f, struct state *s)
return call_arbitraryresult(expr, f, s);
}
+static struct error *
+verify_paramspec(struct value *param, struct value *arg, struct state *param_state,
+ struct state *arg_state);
+
+static struct error *
+call_setupverify(struct ast_function *f, struct state *arg_state)
+{
+ struct error *err;
+
+ struct state *param_state = state_create(
+ dynamic_str(ast_function_name(f)),
+ state_getext(arg_state),
+ ast_function_type(f)
+ );
+ if ((err = ast_function_initparams(f, param_state))) {
+ return err;
+ }
+ int nparams = ast_function_nparams(f);
+ struct ast_variable **param = ast_function_params(f);
+
+ for (int i = 0; i < nparams; i++) {
+ char *id = ast_variable_name(param[i]);
+ struct value *param = state_getloc(param_state, id);
+ 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);
+ return error_create(strbuilder_build(b));
+ }
+ }
+ return NULL;
+}
+
+static struct error *
+verify_paramspec(struct value *param, struct value *arg, struct state *param_state,
+ struct state *arg_state)
+{
+ if (!state_islval(param_state, param)) {
+ return NULL;
+ }
+ if (!state_islval(arg_state, arg)) {
+ return error_create("must be lvalue");
+ }
+ if (state_isalloc(param_state, param) && !state_isalloc(arg_state, arg)) {
+ return error_create("must be heap allocated");
+ }
+ struct object_res param_res = state_get(
+ param_state, value_as_location(param), false
+ );
+ if (param_res.err) {
+ return param_res.err;
+ }
+ struct object_res arg_res = state_get(
+ arg_state, value_as_location(arg), false
+ );
+ if (arg_res.err) {
+ return arg_res.err;
+ }
+ assert(param_res.obj);
+ assert(arg_res.obj);
+ if (!object_hasvalue(param_res.obj)) {
+ return NULL;
+ }
+ if (!object_hasvalue(arg_res.obj)) {
+ return error_create("must be rvalue");
+ }
+ return verify_paramspec(
+ object_as_value(param_res.obj), object_as_value(arg_res.obj),
+ param_state, arg_state
+ );
+}
+
static struct result *
pf_augment(struct value *v, struct ast_expr *call, struct state *state)
{
@@ 720,7 845,11 @@ prepare_parameters(int nparams, struct ast_variable **param,
struct ast_expr *name = ast_expr_identifier_create(
dynamic_str(ast_variable_name(param[i]))
);
- struct object *obj = lvalue_object(ast_expr_lvalue(name, state));
+ struct lvalue_res lval_res = ast_expr_lvalue(name, state);
+ if (lval_res.err) {
+ return lval_res.err;
+ }
+ struct object *obj = lvalue_object(lval_res.lval);
ast_expr_destroy(name);
object_assign(obj, value_copy(result_as_value(res)));
@@ 739,26 868,20 @@ expr_assign_eval(struct ast_expr *expr, struct state *state)
return res;
}
if (!result_hasvalue(res)) {
- struct strbuilder *b = strbuilder_create();
- char *s = ast_expr_str(rval);
- strbuilder_printf(b, "`%s' has no value", s);
- free(s);
- return result_error_create(error_create(strbuilder_build(b)));
+ assert(false);
+ return result_error_create(error_create("undefined indirection (rvalue)"));
}
- struct object *obj = lvalue_object(ast_expr_lvalue(lval, state));
- if (!obj) {
- struct strbuilder *b = strbuilder_create();
- char *s = ast_expr_str(lval);
- strbuilder_printf(b, "`%s' is not a valid object", s);
- free(s);
- return result_error_create(error_create(strbuilder_build(b)));
+ struct lvalue_res lval_res = ast_expr_lvalue(lval, state);
+ if (lval_res.err) {
+ return result_error_create(lval_res.err);
}
- struct value *val = object_as_value(obj);
- while (val && value_islocation(val)) {
- obj = state_deref(state, val, ast_expr_constant_create(0));
- val = object_as_value(obj);
+ struct object *obj = lvalue_object(lval_res.lval);
+ if (!obj) {
+ return result_error_create(error_create("undefined indirection (lvalue)"));
}
+
object_assign(obj, value_copy(result_as_value(res)));
+
return res;
}
@@ 821,12 944,19 @@ arbarg_eval(struct ast_expr *expr, struct state *state)
static struct result *
assign_absexec(struct ast_expr *expr, struct state *state);
+static struct result *
+isdereferencable_absexec(struct ast_expr *expr, struct state *state);
+
struct result *
ast_expr_absexec(struct ast_expr *expr, struct state *state)
{
switch (ast_expr_kind(expr)) {
+ case EXPR_CALL:
+ return expr_call_eval(expr, state);
case EXPR_ASSIGNMENT:
return assign_absexec(expr, state);
+ case EXPR_ISDEREFERENCABLE:
+ return isdereferencable_absexec(expr, state);
default:
assert(false);
}
@@ 838,6 968,14 @@ assign_absexec(struct ast_expr *expr, struct state *state)
return expr_assign_eval(expr, state);
}
+static struct result *
+isdereferencable_absexec(struct ast_expr *expr, struct state *state)
+{
+ struct props *p = state_getprops(state);
+ props_install(p, expr);
+ return result_value_create(NULL);
+}
+
static struct preresult *
reduce_assume(struct ast_expr *, bool value, struct state *);
@@ 1088,27 1226,3 @@ 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));
-
- /* 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));
- return error_create(strbuilder_build(b));
- }
- return NULL;
-}
M src/0v/ast/function/function.c => src/0v/ast/function/function.c +213 -207
@@ 176,19 176,11 @@ ast_function_params(struct ast_function *f)
return f->param;
}
-struct ast_stmt *
-ast_function_preconds(struct ast_function *f)
+struct preconds_result
+ast_function_preconditions(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;
+ return ast_block_preconds(ast_function_abstract(f));
}
struct ast_function *
@@ 207,199 199,249 @@ struct error *
paths_verify(struct ast_function_arr *paths, struct externals *);
static struct error *
-path_verify_withstate(struct ast_function *f, struct state *);
+path_absverify_withstate(struct ast_function *f, struct state *);
-static void
-declare_parameters(struct state *s, struct ast_function *f);
+struct error *
+ast_function_initparams(struct ast_function *f, struct state *);
struct error *
ast_function_verify(struct ast_function *f, struct externals *ext)
{
+ struct error *err;
struct state *state = state_create(
dynamic_str(ast_function_name(f)), ext, ast_function_type(f)
);
- declare_parameters(state, f);
- struct error *err = path_verify_withstate(f, state);
+ if ((err = ast_function_initparams(f, state))) {
+ return err;
+ }
+ if ((err = path_absverify_withstate(f, state))) {
+ return err;
+ }
state_destroy(state);
- return err;
+ return NULL;
}
static struct error *
-path_verify(struct ast_function *f, struct state *state, int index);
-
-static struct preresult *
-install_props(struct state *s, struct ast_function *f);
+path_absverify(struct ast_function *f, struct state *state, int index);
static struct error *
-path_verify_withstate(struct ast_function *f, struct state *state)
+path_absverify_withstate(struct ast_function *f, struct state *state)
{
- struct ast_block *body = ast_function_body(f);
-
- struct preresult *r = install_props(state, f);
- if (preresult_iserror(r)) {
- return preresult_as_error(r);
- } else if (preresult_iscontradiction(r)) {
- /* ex falso quodlibet */
- return NULL;
- }
+ struct ast_block *abs = ast_function_abstract(f);
- int ndecls = ast_block_ndecls(body);
- struct ast_variable **var = ast_block_decls(body);
+ int ndecls = ast_block_ndecls(abs);
+ struct ast_variable **var = ast_block_decls(abs);
for (int i = 0; i < ndecls; i++) {
state_declare(state, var[i], false);
}
- return path_verify(f, state, 0);
+ return path_absverify(f, state, 0);
}
static struct error *
abstract_audit(struct ast_function *f, struct state *actual_state);
static struct error *
-split_paths_verify(struct ast_function *f, struct state *, int index,
+split_paths_absverify(struct ast_function *f, struct state *, int index,
struct ast_stmt_splits *splits);
static struct error *
-path_verify(struct ast_function *f, struct state *state, int index)
+path_absverify(struct ast_function *f, struct state *state, int index)
{
struct error *err = NULL;
- struct ast_block *body = ast_function_body(f);
+ struct ast_block *abs = ast_function_abstract(f);
- int nstmts = ast_block_nstmts(body);
- struct ast_stmt **stmt = ast_block_stmts(body);
+ int nstmts = ast_block_nstmts(abs);
+ struct ast_stmt **stmt = ast_block_stmts(abs);
for (int i = index; i < nstmts; i++) {
- /*printf("state: %s\n", state_str(state));*/
- /*printf("%s\n", ast_stmt_str(stmt[i]));*/
struct ast_stmt_splits splits = ast_stmt_splits(stmt[i], state);
+ if (splits.err) {
+ return splits.err;
+ }
if (splits.n) {
assert(splits.cond);
- return split_paths_verify(f, state, i, &splits);
+ return split_paths_absverify(f, state, i, &splits);
}
- if ((err = ast_stmt_process(stmt[i], state))) {
- return err;
- }
- if (ast_stmt_isterminal(stmt[i], state)) {
- break;
+ if (ast_stmt_ispre(stmt[i])) {
+ continue;
}
+ struct result *res = ast_stmt_absexec(stmt[i], state, true);
+ if (result_iserror(res)) {
+ return result_as_error(res);
+ }
+ /* result_destroy(res); */
}
- if (!state_hasgarbage(state)) {
- printf("actual: %s\n", state_str(state));
- return error_create("qed error: garbage on heap");
- }
+
/* TODO: verify that `result' is of same type as f->result */
if ((err = abstract_audit(f, state))) {
- return error_prepend(err, "qed error: ");
+ return err;
}
return NULL;
}
-static void
-declare_parameters(struct state *s, struct ast_function *f)
+static struct error *
+ast_function_precondsinit(struct ast_function *, struct state *);
+
+static struct error *
+inititalise_param(struct ast_variable *v, struct state *);
+
+struct error *
+ast_function_initparams(struct ast_function *f, struct state *s)
{
- /* declare params and locals in stack frame */
- struct ast_variable **param = ast_function_params(f);
+ struct error *err;
+ /* declare params and locals in stack frame */
int nparams = ast_function_nparams(f);
+ struct ast_variable **params = ast_function_params(f);
for (int i = 0; i < nparams; i++) {
- struct ast_variable *p = param[i];
- state_declare(s, p, true);
- char *name = ast_variable_name(p);
- struct object *obj = state_getobject(s, name);
- assert(obj);
- object_assign(
- obj,
- state_vconst(s, ast_variable_type(p), dynamic_str(name), true)
- );
+ state_declare(s, params[i], true);
+ }
+
+ if ((err = ast_function_precondsinit(f, s))) {
+ return err;
}
+
+ for (int i = 0; i < nparams; i++) {
+ if ((err = inititalise_param(params[i], s))) {
+ return err;
+ }
+ }
+ return NULL;
}
-static struct preresult *
-install_props(struct state *s, struct ast_function *f)
+static struct error *
+ast_function_precondsinit(struct ast_function *f, struct state *s)
{
- struct ast_block *abs = ast_function_abstract(f);
- int nstmts = ast_block_nstmts(abs);
- struct ast_stmt **stmt = ast_block_stmts(abs);
- for (int i = 0; i < nstmts; i++) {
- struct preresult *r = ast_stmt_preprocess(stmt[i], s);
- if (!preresult_isempty(r)) {
- return r;
- }
+ struct preconds_result pre = ast_function_preconditions(f);
+ if (pre.err) {
+ return pre.err;
+ }
+ if (!pre.stmt) {
+ return NULL;
+ }
+ struct result *res = ast_stmt_absexec(pre.stmt, s, true);
+ if (result_iserror(res)) {
+ return result_as_error(res);
+ }
+ return NULL;
+}
+
+static struct error *
+inititalise_param(struct ast_variable *param, struct state *state)
+{
+ char *name = ast_variable_name(param);
+ struct ast_type *t = ast_variable_type(param);
+
+ struct object *obj = state_getobject(state, name);
+ assert(obj);
+ if (object_hasvalue(obj)) {
+ /* must on the clump or heap */
+ struct value *val = object_as_value(obj);
+ //struct location *loc = value_as_location(val);
+ //assert(
+ // location_type(loc) == LOCATION_DEREFERENCABLE ||
+ // location_type(loc) == LOCATION_DYNAMIC
+ //);
+ } else {
+ /* variables that aren't talked about by the preconditions */
+ struct value *val = state_vconst(state, t, dynamic_str(name), true);
+ object_assign(obj, val);
}
- return preresult_empty_create();
+ return NULL;
}
static struct error *
-path_absverify(struct ast_function *, struct state *state, int index,
- struct state *actual_state);
+ast_function_setupabsexec(struct ast_function *f, struct state *state);
static struct error *
-abstract_auditwithstate(struct ast_function *f, struct state *alleged_state,
- struct state *actual_state);
+path_verify(struct ast_function *, struct state *state, int index,
+ struct state *abstract_state);
static struct error *
-abstract_audit(struct ast_function *f, struct state *actual_state)
+abstract_auditwithstate(struct ast_function *f, struct state *actual_state,
+ struct state *abstract_state);
+
+static struct error *
+abstract_audit(struct ast_function *f, struct state *abstract_state)
{
- struct state *alleged_state = state_create(
+ struct error *err;
+
+ struct state *actual_state = state_create_withprops(
dynamic_str(ast_function_name(f)),
- state_getext(actual_state),
- ast_function_type(f)
- );
- declare_parameters(alleged_state, f);
- struct error *err = abstract_auditwithstate(
- f, alleged_state, actual_state
+ state_getext(abstract_state),
+ ast_function_type(f),
+ state_getprops(abstract_state)
);
- state_destroy(alleged_state); /* actual_state handled by caller */
- return err;
+ if ((err = ast_function_initparams(f, actual_state))) {
+ assert(false);
+ }
+ if ((err = ast_function_setupabsexec(f, actual_state))) {
+ return err;
+ }
+ if ((err = abstract_auditwithstate(f, actual_state, abstract_state))) {
+ return err;
+ }
+ state_destroy(actual_state); /* actual_state handled by caller */
+ return NULL;
}
static struct error *
-abstract_auditwithstate(struct ast_function *f, struct state *alleged_state,
- struct state *actual_state)
+ast_function_setupabsexec(struct ast_function *f, struct state *state)
{
- struct preresult *r = install_props(alleged_state, f);
- if (preresult_iscontradiction(r)) {
- return NULL;
+ struct error *err;
+ int nstmts = ast_block_nstmts(f->abstract);
+ struct ast_stmt **stmt = ast_block_stmts(f->abstract);
+ for (int i = 0; i < nstmts; i++) {
+ if ((err = ast_stmt_setupabsexec(stmt[i], state))) {
+ return err;
+ }
}
+ return NULL;
+}
- int ndecls = ast_block_ndecls(f->abstract);
- if (ndecls) {
- struct ast_variable **var = ast_block_decls(f->abstract);
- for (int i = 0; i < ndecls; i++) {
- state_declare(alleged_state, var[i], false);
- }
+
+
+static struct error *
+abstract_auditwithstate(struct ast_function *f, struct state *actual_state,
+ struct state *abstract_state)
+{
+ int ndecls = ast_block_ndecls(f->body);
+ struct ast_variable **var = ast_block_decls(f->body);
+ for (int i = 0; i < ndecls; i++) {
+ state_declare(actual_state, var[i], false);
}
- return path_absverify(f, alleged_state, 0, actual_state);
+ return path_verify(f, actual_state, 0, abstract_state);
}
-static struct ast_function_arr *
-body_paths(struct ast_function *f, int index, struct ast_expr *);
-
static struct error *
-split_path_verify(struct ast_function *f, struct state *state, int index,
+split_path_absverify(struct ast_function *f, struct state *state, int index,
struct ast_expr *cond);
static struct error *
-split_paths_verify(struct ast_function *f, struct state *state, int index,
+split_paths_absverify(struct ast_function *f, struct state *state, int index,
struct ast_stmt_splits *splits)
{
struct error *err;
for (int i = 0; i < splits->n; i++) {
- err = split_path_verify(f, state, index, splits->cond[i]);
- if (err) {
+ if ((err = split_path_absverify(f, state, index, splits->cond[i]))) {
return err;
}
}
return NULL;
}
+static struct ast_function_arr *
+abstract_paths(struct ast_function *f, int index, struct ast_expr *cond);
+
static struct error *
-split_path_verify(struct ast_function *f, struct state *state, int index,
- struct ast_expr *cond)
+split_path_absverify(struct ast_function *f, struct state *state, int index, struct ast_expr *cond)
{
struct error *err = NULL;
- struct ast_function_arr *paths = body_paths(f, index, cond);
+ /* XXX: we are just changing function name now, makes sense to split
+ * state */
+ struct ast_function_arr *paths = abstract_paths(f, index, cond);
int n = ast_function_arr_len(paths);
assert(n == 2);
struct ast_function **func = ast_function_arr_func(paths);
@@ 414,68 456,72 @@ split_path_verify(struct ast_function *f, struct state *state, int index,
return preresult_as_error(r);
}
if (!preresult_iscontradiction(r)) {
- /* only run if no contradiction because "ex falso" */
- if ((err = path_verify(func[i], s_copy, index))) {
+ /* only run if no contradiction because "ex falso" */
+ if ((err = path_absverify(func[i], s_copy, index))) {
return err;
}
}
- /* XXX: error? */
-
/*state_destroy(s_copy);*/
}
return NULL;
}
static struct error *
-split_paths_absverify(struct ast_function *f, struct state *alleged_state,
- int index, struct ast_stmt_splits *splits, struct state *actual_state);
+split_paths_verify(struct ast_function *f, struct state *actual_state,
+ int index, struct ast_stmt_splits *splits, struct state *abstract_state);
static struct error *
-path_absverify(struct ast_function *f, struct state *alleged_state, int index,
- struct state *actual_state)
+path_verify(struct ast_function *f, struct state *actual_state, int index,
+ struct state *abstract_state)
{
- int nstmts = ast_block_nstmts(f->abstract);
- struct ast_stmt **stmt = ast_block_stmts(f->abstract);
+ struct error *err;
+
+ int nstmts = ast_block_nstmts(f->body);
+ struct ast_stmt **stmt = ast_block_stmts(f->body);
for (int i = index; i < nstmts; i++) {
struct ast_stmt_splits splits = ast_stmt_splits(
- stmt[i], alleged_state
+ stmt[i], actual_state
);
if (splits.n) {
- return split_paths_absverify(
- f, alleged_state, i, &splits, actual_state
+ return split_paths_verify(
+ f, actual_state, i, &splits, abstract_state
);
}
- struct result *res = ast_stmt_absexec(stmt[i], alleged_state);
- if (result_iserror(res)) {
- return result_as_error(res);
+ if ((err = ast_stmt_process(stmt[i], actual_state))) {
+ return err;
}
- result_destroy(res);
+ if (ast_stmt_isterminal(stmt[i], actual_state)) {
+ break;
+ }
+ /* result_destroy(res); */
}
-
- bool equiv = state_equal(actual_state, alleged_state);
+ if (state_hasgarbage(actual_state)) {
+ printf("actual: %s\n", state_str(actual_state));
+ return error_create("qed error: garbage on heap");
+ }
+
+ bool equiv = state_equal(actual_state, abstract_state);
if (!equiv) {
- /* XXX: print states */
- return error_create("actual and alleged states differ");
+ printf("actual: %s\n", state_str(actual_state));
+ printf("abstract: %s\n", state_str(abstract_state));
+ return error_create("qed error: actual and abstract states differ");
}
return NULL;
}
-static struct ast_function_arr *
-abstract_paths(struct ast_function *f, int index, struct ast_expr *cond);
-
static struct error *
-split_path_absverify(struct ast_function *f, struct state *alleged_state,
- int index, struct ast_expr *cond, struct state *actual_state);
+split_path_verify(struct ast_function *f, struct state *actual_state,
+ int index, struct ast_expr *cond, struct state *abstract_state);
static struct error *
-split_paths_absverify(struct ast_function *f, struct state *alleged_state,
- int index, struct ast_stmt_splits *splits, struct state *actual_state)
+split_paths_verify(struct ast_function *f, struct state *actual_state,
+ int index, struct ast_stmt_splits *splits, struct state *abstract_state)
{
struct error *err;
for (int i = 0; i < splits->n; i++) {
- err = split_path_absverify(
- f, alleged_state, index, splits->cond[i], actual_state
+ err = split_path_verify(
+ f, actual_state, index, splits->cond[i], abstract_state
);
if (err) {
return err;
@@ 484,40 530,42 @@ split_paths_absverify(struct ast_function *f, struct state *alleged_state,
return NULL;
}
+static struct ast_function_arr *
+body_paths(struct ast_function *f, int index, struct ast_expr *);
+
static struct error *
-split_path_absverify(struct ast_function *f, struct state *alleged_state,
- int index, struct ast_expr *cond, struct state *actual_state)
+split_path_verify(struct ast_function *f, struct state *actual_state,
+ int index, struct ast_expr *cond, struct state *abstract_state)
{
- struct error *err = NULL;
+ struct error *err;
/* create two functions with abstracts and bodies
* adjusted accordingly */
- struct ast_function_arr *paths = abstract_paths(f, index, cond);
+ struct ast_function_arr *paths = body_paths(f, index, cond);
int n = ast_function_arr_len(paths);
assert(n == 2);
struct ast_function **func = ast_function_arr_func(paths);
for (int i = 0; i < n; i++) {
- struct state *alleged_copy = state_copywithname(
- alleged_state, ast_function_name(func[i])
- );
struct state *actual_copy = state_copywithname(
actual_state, ast_function_name(func[i])
);
+ struct state *abstract_copy = state_copywithname(
+ abstract_state, ast_function_name(func[i])
+ );
struct preresult *r = ast_expr_assume(
- /* XXX */
- ast_expr_inverted_copy(cond, i==1), alleged_copy
+ ast_expr_inverted_copy(cond, i==1), actual_copy
);
if (preresult_iserror(r)) {
return preresult_as_error(r);
}
if (!preresult_iscontradiction(r)) {
/* only run if no contradiction because "ex falso" */
- if ((err = path_absverify(func[i], alleged_copy, index, actual_copy))) {
+ if ((err = path_verify(func[i], actual_copy, index, abstract_copy))) {
return err;
}
}
/*state_destroy(actual_copy);*/
- /*state_destroy(alleged_copy);*/
+ /*state_destroy(abstract_copy);*/
}
return NULL;
}
@@ 536,11 584,11 @@ ast_function_absexec(struct ast_function *f, struct state *state)
int nstmts = ast_block_nstmts(f->abstract);
struct ast_stmt **stmt = ast_block_stmts(f->abstract);
for (int i = 0; i < nstmts; i++) {
- struct result *res = ast_stmt_absexec(stmt[i], state);
+ struct result *res = ast_stmt_absexec(stmt[i], state, false);
if (result_iserror(res)) {
return res;
}
- result_destroy(res);
+ /* result_destroy(res); */
}
/* wrap result and return */
@@ 548,17 596,6 @@ ast_function_absexec(struct ast_function *f, struct state *state)
assert(obj);
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);
@@ 567,7 604,7 @@ ast_function_buildgraph(char *fname, struct externals *ext)
{
struct map *dedup = map_create(),
*g = map_create();
-
+
recurse_buildgraph(g, dedup, fname, ext);
return g;
@@ 615,7 652,7 @@ recurse_buildgraph(struct map *g, struct map *dedup, char *fname, struct externa
if (map_get(local_dedup, func[j]) != NULL) {
continue;
}
-
+
struct ast_function *f = externals_getfunc(ext, func[j]);
if (!f->isaxiom) {
string_arr_append(val, func[j]);
@@ 633,21 670,18 @@ recurse_buildgraph(struct map *g, struct map *dedup, char *fname, struct externa
static char *
split_name(char *name, struct ast_expr *assumption);
-static struct ast_block *
-block_withassumption(struct ast_block *old, struct ast_expr *cond);
-
static struct ast_function_arr *
abstract_paths(struct ast_function *f, int index, struct ast_expr *cond)
{
struct ast_function_arr *res = ast_function_arr_create();
-
+
struct ast_function *f_true = ast_function_create(
f->isaxiom,
ast_type_copy(f->ret),
split_name(f->name, cond),
f->nparam,
ast_variables_copy(f->nparam, f->param),
- block_withassumption(f->abstract, ast_expr_copy(cond)),
+ ast_block_copy(f->abstract),
ast_block_copy(f->body)
);
@@ 658,10 692,10 @@ abstract_paths(struct ast_function *f, int index, struct ast_expr *cond)
split_name(f->name, inv_assumption),
f->nparam,
ast_variables_copy(f->nparam, f->param),
- block_withassumption(f->abstract, inv_assumption),
+ ast_block_copy(f->abstract),
ast_block_copy(f->body)
);
-
+
ast_function_arr_append(res, f_true);
ast_function_arr_append(res, f_false);
return res;
@@ 671,14 705,14 @@ static struct ast_function_arr *
body_paths(struct ast_function *f, int index, struct ast_expr *cond)
{
struct ast_function_arr *res = ast_function_arr_create();
-
+
struct ast_function *f_true = ast_function_create(
f->isaxiom,
ast_type_copy(f->ret),
split_name(f->name, cond),
f->nparam,
ast_variables_copy(f->nparam, f->param),
- block_withassumption(f->abstract, ast_expr_copy(cond)),
+ ast_block_copy(f->abstract),
f->body
);
@@ 689,43 723,15 @@ body_paths(struct ast_function *f, int index, struct ast_expr *cond)
split_name(f->name, inv_assumption),
f->nparam,
ast_variables_copy(f->nparam, f->param),
- block_withassumption(f->abstract, inv_assumption),
+ ast_block_copy(f->abstract),
f->body
);
-
+
ast_function_arr_append(res, f_true);
ast_function_arr_append(res, f_false);
return res;
}
-static struct ast_block *
-block_withassumption(struct ast_block *old, struct ast_expr *cond)
-{
- int ndecl = ast_block_ndecls(old);
- struct ast_variable **old_decl = ast_block_decls(old);
- struct ast_variable **decl = malloc(sizeof(struct ast_variable *) * ndecl);
- for (int i = 0; i < ndecl; i++) {
- decl[i] = ast_variable_copy(old_decl[i]);
- }
-
- int old_nstmt = ast_block_nstmts(old);
- struct ast_stmt **old_stmt = ast_block_stmts(old);
- int nstmt = old_nstmt+1;
- struct ast_stmt **stmt = malloc(sizeof(struct ast_stmt *) * nstmt);
- for (int i = 0; i < old_nstmt; i++) {
- stmt[i+1] = ast_stmt_copy(old_stmt[i]);
- }
-
- /* assume: cond; */
- stmt[0] = ast_stmt_create_labelled(
- NULL, dynamic_str("assume"), ast_stmt_create_expr(NULL, cond)
- );
-
- struct ast_block *new = ast_block_create(decl, ndecl, stmt, nstmt);
- return new;
-}
-
-
static char *
split_name(char *name, struct ast_expr *assumption)
{
M src/0v/ast/gram.y => src/0v/ast/gram.y +6 -1
@@ 99,7 99,7 @@ variable_array_create(struct ast_variable *v)
%token ARB_ARG
%token CASE DEFAULT IF ELSE SWITCH WHILE DO FOR SOME GOTO CONTINUE BREAK RETURN
-%token ALLOC DEALLOC
+%token ALLOC DEALLOC CLUMP
%start translation_unit
@@ 248,6 248,9 @@ isdeallocand_expression
| ISDEALLOCAND_OP isdeallocand_expression {
$$ = ast_expr_isdeallocand_create($2);
}
+ | ARB_ARG isdeallocand_expression {
+ $$ = ast_expr_isdereferencable_create($2);
+ }
;
unary_expression
@@ 716,6 719,8 @@ allocation_statement
{ $$ = ast_stmt_create_alloc(lexloc(), $2); }
| DEALLOC postfix_expression ';'
{ $$ = ast_stmt_create_dealloc(lexloc(), $2); }
+ | CLUMP postfix_expression ';'
+ { $$ = ast_stmt_create_clump(lexloc(), $2); }
;
declaration_list
M src/0v/ast/lex.l => src/0v/ast/lex.l +1 -0
@@ 32,6 32,7 @@ check_type();
"/*" { comment(); }
".alloc" { count(); return(ALLOC); }
".dealloc" { count(); return(DEALLOC); }
+".clump" { count(); return(CLUMP); }
"auto" { count(); return(AUTO); }
"axiom" { count(); return(AXIOM); }
M src/0v/ast/stmt/stmt.c => src/0v/ast/stmt/stmt.c +115 -39
@@ 38,7 38,7 @@ struct ast_stmt {
struct ast_expr *rv;
} jump;
struct {
- bool isalloc;
+ enum ast_alloc_kind kind;
struct ast_expr *arg;
} alloc;
} u;
@@ 243,7 243,7 @@ ast_stmt_create_alloc(struct lexememarker *loc, struct ast_expr *arg)
{
struct ast_stmt *stmt = ast_stmt_create(loc);
stmt->kind = STMT_ALLOCATION;
- stmt->u.alloc.isalloc = true;
+ stmt->u.alloc.kind = ALLOC;
stmt->u.alloc.arg = arg;
return stmt;
}
@@ 253,7 253,17 @@ ast_stmt_create_dealloc(struct lexememarker *loc, struct ast_expr *arg)
{
struct ast_stmt *stmt = ast_stmt_create(loc);
stmt->kind = STMT_ALLOCATION;
- stmt->u.alloc.isalloc = false;
+ stmt->u.alloc.kind = DEALLOC;
+ stmt->u.alloc.arg = arg;
+ return stmt;
+}
+
+struct ast_stmt *
+ast_stmt_create_clump(struct lexememarker *loc, struct ast_expr *arg)
+{
+ struct ast_stmt *stmt = ast_stmt_create(loc);
+ stmt->kind = STMT_ALLOCATION;
+ stmt->u.alloc.kind= CLUMP;
stmt->u.alloc.arg = arg;
return stmt;
}
@@ 262,9 272,16 @@ static struct ast_stmt *
ast_stmt_copy_alloc(struct lexememarker *loc, struct ast_stmt *stmt)
{
struct ast_expr *arg = ast_expr_copy(stmt->u.alloc.arg);
- return stmt->u.alloc.isalloc
- ? ast_stmt_create_alloc(loc, arg)
- : ast_stmt_create_dealloc(loc, arg);
+ switch (stmt->u.alloc.kind) {
+ case ALLOC:
+ return ast_stmt_create_alloc(loc, arg);
+ case DEALLOC:
+ return ast_stmt_create_dealloc(loc, arg);
+ case CLUMP:
+ return ast_stmt_create_clump(loc, arg);
+ default:
+ assert(false);
+ }
}
static void
@@ 281,11 298,20 @@ ast_stmt_alloc_sprint(struct ast_stmt *stmt, struct strbuilder *b)
assert(stmt->kind == STMT_ALLOCATION);
char *arg = ast_expr_str(stmt->u.alloc.arg);
- strbuilder_printf(
- b, ".%s %s;",
- stmt->u.alloc.isalloc ? "alloc" : "dealloc",
- arg
- );
+
+ switch (stmt->u.alloc.kind) {
+ case ALLOC:
+ strbuilder_printf(b, ".%s %s;", "alloc", arg);
+ break;
+ case DEALLOC:
+ strbuilder_printf(b, ".%s %s;", "dealloc", arg);
+ break;
+ case CLUMP:
+ strbuilder_printf(b, ".%s %s;", "clump", arg);
+ break;
+ default:
+ assert(false);
+ }
free(arg);
}
@@ 293,16 319,14 @@ struct ast_expr *
ast_stmt_alloc_arg(struct ast_stmt *stmt)
{
assert(stmt->kind == STMT_ALLOCATION);
-
return stmt->u.alloc.arg;
}
-bool
-ast_stmt_alloc_isalloc(struct ast_stmt *stmt)
+enum ast_alloc_kind
+ast_stmt_alloc_kind(struct ast_stmt *stmt)
{
assert(stmt->kind == STMT_ALLOCATION);
-
- return stmt->u.alloc.isalloc;
+ return stmt->u.alloc.kind;
}
@@ 620,6 644,7 @@ ast_stmt_copy(struct ast_stmt *stmt)
char *
ast_stmt_str(struct ast_stmt *stmt)
{
+ assert(stmt);
struct strbuilder *b = strbuilder_create();
switch (stmt->kind) {
case STMT_LABELLED:
@@ 742,6 767,8 @@ ast_stmt_splits(struct ast_stmt *stmt, struct state *s)
{
/* TODO: consider expressions with calls */
switch (stmt->kind) {
+ case STMT_NOP:
+ return (struct ast_stmt_splits) { .n = 0, .cond = NULL };
case STMT_EXPR:
return ast_expr_splits(stmt->u.expr, s);
case STMT_SELECTION:
@@ 751,9 778,11 @@ ast_stmt_splits(struct ast_stmt *stmt, struct state *s)
return ast_expr_splits(stmt->u.jump.rv, s);
}
return (struct ast_stmt_splits) { .n = 0, .cond = NULL };
- case STMT_ALLOCATION:
case STMT_LABELLED:
+ return ast_stmt_splits(stmt->u.labelled.stmt, s);
+ case STMT_ALLOCATION:
case STMT_ITERATION:
+ case STMT_COMPOUND:
case STMT_COMPOUND_V:
/* disallowed splits for now */
return (struct ast_stmt_splits) { .n = 0, .cond = NULL };
@@ 762,6 791,37 @@ ast_stmt_splits(struct ast_stmt *stmt, struct state *s)
}
}
+static bool
+condexists(struct ast_expr *cond, struct state *);
+
+static struct ast_stmt_splits
+stmt_sel_splits(struct ast_stmt *stmt, struct state *s)
+{
+ struct result *res = ast_expr_pf_reduce(stmt->u.selection.cond, s);
+ struct value *v = result_as_value(res);
+ struct ast_expr *e = value_to_expr(v);
+ if (condexists(e, s) || value_isconstant(v)) {
+ return (struct ast_stmt_splits) { .n = 0, .cond = NULL };
+ }
+ /*printf("cond: %s\n", ast_expr_str(r));*/
+ struct ast_expr **cond = malloc(sizeof(struct ast_expr *));
+ cond[0] = e;
+ return (struct ast_stmt_splits) {
+ .n = 1,
+ .cond = cond,
+ };
+}
+
+static bool
+condexists(struct ast_expr *cond, struct state *s)
+{
+ struct result *res = ast_expr_pf_reduce(cond, s);
+ assert(!result_iserror(res) && result_hasvalue(res));
+ struct ast_expr *reduced = value_to_expr(result_as_value(res));
+ struct props *p = state_getprops(s);
+ return props_get(p, reduced) || props_contradicts(p, reduced);
+}
+
static struct string_arr *
ast_stmt_expr_getfuncs(struct ast_stmt *stmt)
{
@@ 827,34 887,50 @@ ast_stmt_compound_getfuncs(struct ast_stmt *stmt)
return res;
}
-static bool
-condexists(struct ast_expr *cond, struct state *);
+static struct error *
+preconds_selection_verify(struct ast_stmt *stmt);
-static struct ast_stmt_splits
-stmt_sel_splits(struct ast_stmt *stmt, struct state *s)
+static struct error *
+preconds_compound_verify(struct ast_stmt *);
+
+struct error *
+ast_stmt_preconds_validate(struct ast_stmt *stmt)
{
- struct result *res = ast_expr_pf_reduce(stmt->u.selection.cond, s);
- struct ast_expr *r = value_to_expr(result_as_value(res));
- if (condexists(r, s)) {
- return (struct ast_stmt_splits) { .n = 0, .cond = NULL };
+ switch (stmt->kind) {
+ case STMT_EXPR:
+ case STMT_ALLOCATION:
+ case STMT_ITERATION:
+ return NULL;
+ case STMT_SELECTION:
+ return preconds_selection_verify(stmt);
+ case STMT_COMPOUND:
+ return preconds_compound_verify(stmt);
+ default:
+ assert(false);
}
- /*printf("cond: %s\n", ast_expr_str(r));*/
- struct ast_expr **cond = malloc(sizeof(struct ast_expr *));
- cond[0] = r;
- return (struct ast_stmt_splits) {
- .n = 1,
- .cond = cond,
- };
}
-static bool
-condexists(struct ast_expr *cond, struct state *s)
+static struct error *
+preconds_selection_verify(struct ast_stmt *stmt)
{
- struct result *res = ast_expr_pf_reduce(cond, s);
- assert(!result_iserror(res) && result_hasvalue(res));
- struct ast_expr *reduced = value_to_expr(result_as_value(res));
- struct props *p = state_getprops(s);
- return props_get(p, reduced) || props_contradicts(p, reduced);
+ struct strbuilder *b = strbuilder_create();
+ struct lexememarker *l = ast_stmt_lexememarker(stmt);
+ strbuilder_printf(b, "%s setup preconditions must be decidable", lexememarker_str(l));
+ return error_create(strbuilder_build(b));
+}
+
+static struct error *
+preconds_compound_verify(struct ast_stmt *stmt)
+{
+ struct error *err;
+ struct ast_block *b = stmt->u.compound;
+ struct ast_stmt **stmts = ast_block_stmts(b);
+ for (int i = 0; i < ast_block_nstmts(b); i++) {
+ if ((err = ast_stmt_preconds_validate(stmts[i]))) {
+ return err;
+ }
+ }
+ return NULL;
}
#include "verify.c"
M src/0v/ast/stmt/stmt.h => src/0v/ast/stmt/stmt.h +10 -2
@@ 3,6 3,12 @@
#include "util.h"
+enum ast_alloc_kind {
+ ALLOC = 1 << 0,
+ DEALLOC = 1 << 1,
+ CLUMP = 1 << 2,
+};
+
enum ast_stmt_kind {
STMT_NOP = 1 << 0,
STMT_LABELLED = 1 << 1,
@@ 28,22 34,24 @@ ast_stmt_isassume(struct ast_stmt *stmt);
struct string_arr *
ast_stmt_getfuncs(struct ast_stmt *stmt);
+struct error;
+
struct ast_stmt_splits {
int n;
struct ast_expr **cond;
+ struct error *err;
};
struct ast_stmt_splits
ast_stmt_splits(struct ast_stmt *, struct state *);
struct state;
-struct error;
/* TODO: change to more regular tuple */
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 *);
+ast_stmt_precondsinit(struct ast_stmt *, struct state *);
#endif
M src/0v/ast/stmt/verify.c => src/0v/ast/stmt/verify.c +205 -107
@@ 15,7 15,7 @@
struct error *
ast_stmt_process(struct ast_stmt *stmt, struct state *state)
{
- struct error *err = NULL;
+ struct error *err;
if (ast_stmt_kind(stmt) == STMT_COMPOUND_V) {
if ((err = ast_stmt_verify(stmt, state))) {
@@ 46,13 46,7 @@ stmt_installprop(struct ast_stmt *stmt, struct state *state);
struct preresult *
ast_stmt_preprocess(struct ast_stmt *stmt, struct state *state)
{
- if (ast_stmt_ispre(stmt)) {
- struct error *err = ast_stmt_exec(stmt, state);
- if (err) {
- return preresult_error_create(err);
- }
- } else if (ast_stmt_isassume(stmt)) {
- printf("assume: %s\n", ast_stmt_str(stmt));
+ if (ast_stmt_isassume(stmt)) {
return stmt_installprop(stmt, state);
}
return preresult_empty_create();
@@ 177,6 171,8 @@ struct error *
ast_stmt_exec(struct ast_stmt *stmt, struct state *state)
{
switch (ast_stmt_kind(stmt)) {
+ case STMT_NOP:
+ return NULL;
case STMT_LABELLED:
return ast_stmt_exec(ast_stmt_labelled_stmt(stmt), state);
case STMT_COMPOUND:
@@ 248,7 244,7 @@ stmt_iter_exec(struct ast_stmt *stmt, struct state *state)
return NULL;
}
- struct result *res = ast_stmt_absexec(neteffect, state);
+ struct result *res = ast_stmt_absexec(neteffect, state, true);
if (result_iserror(res)) {
return result_as_error(res);
}
@@ 288,6 284,8 @@ iter_neteffect(struct ast_stmt *iter)
static struct error *
stmt_jump_exec(struct ast_stmt *stmt, struct state *state)
{
+ /* TODO: install propositions corresponding to dereferencability */
+
struct result *res = ast_expr_eval(ast_stmt_jump_rv(stmt), state);
if (result_iserror(res)) {
return result_as_error(res);
@@ 296,39 294,43 @@ stmt_jump_exec(struct ast_stmt *stmt, struct state *state)
struct object *obj = state_getresult(state);
assert(obj);
object_assign(obj, value_copy(result_as_value(res)));
- result_destroy(res);
+ /* destroy result if exists */
+
}
return NULL;
}
static struct result *
-sel_absexec(struct ast_stmt *stmt, struct state *state);
+labelled_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup);
+
+static struct result *
+sel_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup);
static struct result *
iter_absexec(struct ast_stmt *stmt, struct state *state);
static struct result *
-comp_absexec(struct ast_stmt *stmt, struct state *state);
+comp_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup);
static struct result *
alloc_absexec(struct ast_stmt *stmt, struct state *state);
struct result *
-ast_stmt_absexec(struct ast_stmt *stmt, struct state *state)
+ast_stmt_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup)
{
switch (ast_stmt_kind(stmt)) {
- case STMT_LABELLED:
- /* labelled statements are verified not executed when we
- * transitively call a function */
+ case STMT_NOP:
return result_value_create(NULL);
+ case STMT_LABELLED:
+ return labelled_absexec(stmt, state, should_setup);
case STMT_EXPR:
return ast_expr_absexec(ast_stmt_as_expr(stmt), state);
case STMT_SELECTION:
- return sel_absexec(stmt, state);
+ return sel_absexec(stmt, state, should_setup);
case STMT_ITERATION:
return iter_absexec(stmt, state);
case STMT_COMPOUND:
- return comp_absexec(stmt, state);
+ return comp_absexec(stmt, state, should_setup);
case STMT_ALLOCATION:
return alloc_absexec(stmt, state);
default:
@@ 336,6 338,91 @@ ast_stmt_absexec(struct ast_stmt *stmt, struct state *state)
}
}
+static struct result *
+labelled_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup)
+{
+ if (!ast_stmt_ispre(stmt)) {
+ assert(false);
+ }
+ struct ast_stmt *setup = ast_stmt_labelled_stmt(stmt);
+ if (!setup) {
+ assert(false);
+ }
+ if (!should_setup) {
+ /* if abstract is called we don't execute setup */
+ return result_value_create(NULL);
+ }
+ return ast_stmt_absexec(setup, state, should_setup);
+}
+
+static struct result *
+sel_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup)
+{
+ struct decision dec = sel_decide(ast_stmt_sel_cond(stmt), state);
+ if (dec.err) {
+ return result_error_create(dec.err);
+ }
+ if (dec.decision) {
+ return ast_stmt_absexec(ast_stmt_sel_body(stmt), state, should_setup);
+ }
+ assert(!ast_stmt_sel_nest(stmt));
+ return result_value_create(NULL);
+}
+
+struct decision
+sel_decide(struct ast_expr *control, struct state *state)
+{
+ /*printf("(sel_decide) state: %s\n", state_str(state));*/
+ /*printf("(sel_decide) control: %s\n", ast_expr_str(control));*/
+ struct result *res = ast_expr_pf_reduce(control, state);
+ if (result_iserror(res)) {
+ return (struct decision) { .err = result_as_error(res) };
+ }
+ assert(result_hasvalue(res)); /* TODO: user error */
+
+ struct value *v = result_as_value(res);
+ /*printf("(sel_decide) value: %s\n", value_str(v));*/
+ if (value_issync(v)) {
+ struct ast_expr *sync = value_as_sync(v);
+ /*printf("state: %s\n", state_str(state));*/
+ /*printf("sync: %s\n", ast_expr_str(sync));*/
+ struct props *p = state_getprops(state);
+ if (props_get(p, sync)) {
+ return (struct decision) { .decision = true, .err = NULL };
+ } else if (props_contradicts(p, sync)) {
+ return (struct decision) { .decision = false, .err = NULL };
+ }
+ }
+ if (value_isconstant(v)) {
+ if (value_as_constant(v)) {
+ return (struct decision) { .decision = true, .err = NULL };
+ }
+ return (struct decision) { .decision = false, .err = NULL };
+ }
+
+ struct value *zero = value_int_create(0);
+
+ if (!values_comparable(zero, v)) {
+ struct strbuilder *b = strbuilder_create();
+ char *c_str = ast_expr_str(control);
+ char *v_str = value_str(v);
+ strbuilder_printf(
+ b, "`%s' with value `%s' is undecidable",
+ c_str, v_str
+ );
+ free(v_str);
+ free(c_str);
+ return (struct decision) {
+ .decision = false,
+ .err = error_create(strbuilder_build(b)),
+ };
+ }
+
+ bool nonzero = !value_equal(zero, v);
+ value_destroy(zero);
+ return (struct decision) { .decision = nonzero, .err = NULL };
+}
+
static struct ast_stmt *
hack_alloc_from_neteffect(struct ast_stmt *);
@@ 373,10 460,15 @@ iter_absexec(struct ast_stmt *stmt, struct state *state)
result_destroy(result_up);
result_destroy(result_lw);
- if (ast_stmt_alloc_isalloc(alloc)) {
+ switch (ast_stmt_alloc_kind(alloc)) {
+ case ALLOC:
err = state_range_alloc(state, obj, res_lw, res_up);
- } else {
+ break;
+ case DEALLOC:
err = state_range_dealloc(state, obj, res_lw, res_up);
+ break;
+ default:
+ assert(false);
}
ast_expr_destroy(res_up);
@@ 409,83 501,22 @@ hack_base_object_from_alloc(struct ast_stmt *alloc, struct state *state)
struct ast_expr *i = ast_expr_identifier_create(dynamic_str("i"));
assert(ast_expr_equal(ast_expr_binary_e2(inner), i));
ast_expr_destroy(i);
- struct object *obj = lvalue_object(
- ast_expr_lvalue(ast_expr_binary_e1(inner), state)
- );
+ struct lvalue_res res = ast_expr_lvalue(ast_expr_binary_e1(inner), state);
+ if (res.err) {
+ assert(false);
+ }
+ struct object *obj = lvalue_object(res.lval);
assert(obj);
return obj;
}
static struct result *
-sel_absexec(struct ast_stmt *stmt, struct state *state)
-{
- struct decision dec = sel_decide(ast_stmt_sel_cond(stmt), state);
- if (dec.err) {
- return result_error_create(dec.err);
- }
- if (dec.decision) {
- return ast_stmt_absexec(ast_stmt_sel_body(stmt), state);
- }
- assert(!ast_stmt_sel_nest(stmt));
- return result_value_create(NULL);
-}
-
-struct decision
-sel_decide(struct ast_expr *control, struct state *state)
-{
- /*printf("(sel_decide) state: %s\n", state_str(state));*/
- /*printf("(sel_decide) control: %s\n", ast_expr_str(control));*/
- struct result *res = ast_expr_pf_reduce(control, state);
- if (result_iserror(res)) {
- return (struct decision) { .err = result_as_error(res) };
- }
- assert(result_hasvalue(res)); /* TODO: user error */
-
- struct value *v = result_as_value(res);
- /*printf("(sel_decide) value: %s\n", value_str(v));*/
- if (value_issync(v)) {
- struct ast_expr *sync = value_as_sync(v);
- /*printf("state: %s\n", state_str(state));*/
- /*printf("sync: %s\n", ast_expr_str(sync));*/
- struct props *p = state_getprops(state);
- if (props_get(p, sync)) {
- return (struct decision) { .decision = true, .err = NULL };
- } else if (props_contradicts(p, sync)) {
- return (struct decision) { .decision = false, .err = NULL };
- }
-
- }
-
- struct value *zero = value_int_create(0);
-
- if (!values_comparable(zero, v)) {
- struct strbuilder *b = strbuilder_create();
- char *c_str = ast_expr_str(control);
- char *v_str = value_str(v);
- strbuilder_printf(
- b, "`%s' with value `%s' is undecidable",
- c_str, v_str
- );
- free(v_str);
- free(c_str);
- return (struct decision) {
- .decision = false,
- .err = error_create(strbuilder_build(b)),
- };
- }
-
- bool nonzero = !value_equal(zero, v);
- value_destroy(zero);
- return (struct decision) { .decision = nonzero, .err = NULL };
-}
-
-static struct result *
-comp_absexec(struct ast_stmt *stmt, struct state *state)
+comp_absexec(struct ast_stmt *stmt, struct state *state, bool should_setup)
{
struct ast_block *b = ast_stmt_as_block(stmt);
struct ast_stmt **stmts = ast_block_stmts(b);
for (int i = 0; i < ast_block_nstmts(b); i++) {
- struct result *res = ast_stmt_absexec(stmts[i], state);
+ struct result *res = ast_stmt_absexec(stmts[i], state, should_setup);
if (result_iserror(res)) {
return res;
}
@@ 504,29 535,44 @@ alloc_absexec(struct ast_stmt *alloc, struct state *state)
return res;
}
if (result_hasvalue(res)) {
- struct object *obj = lvalue_object(
- ast_expr_lvalue(ast_stmt_alloc_arg(alloc), state)
- );
+ struct lvalue_res lval_res = ast_expr_lvalue(ast_stmt_alloc_arg(alloc), state);
+ if (lval_res.err) {
+ return result_error_create(lval_res.err);
+ }
+ struct object *obj = lvalue_object(lval_res.lval);
assert(obj);
object_assign(obj, value_copy(result_as_value(res)));
}
return res;
}
+static struct result *
+dealloc_process(struct ast_stmt *, struct state *);
+
/* operates at location level. It either creates an object on the heap and returns
* a location or gets the location pointed to by an lvalue and attempts to free
* possibly returning an error
* */
static struct result *
-alloc_process(struct ast_stmt *alloc, struct state *state)
+alloc_process(struct ast_stmt *stmt, struct state *state)
{
- if (ast_stmt_alloc_isalloc(alloc)) {
+ switch (ast_stmt_alloc_kind(stmt)) {
+ case ALLOC:
/* TODO: size needs to be passed in here when added to .alloc */
return result_value_create(state_alloc(state));
+ case DEALLOC:
+ return dealloc_process(stmt, state);
+ case CLUMP:
+ return result_value_create(state_clump(state));
+ default:
+ assert(false);
}
+}
- /* dealloc */
- struct ast_expr *arg = ast_stmt_alloc_arg(alloc);
+static struct result *
+dealloc_process(struct ast_stmt *stmt, struct state *state)
+{
+ struct ast_expr *arg = ast_stmt_alloc_arg(stmt);
/* arg is pointing at the heap location we want to free, so we want its
* value rather than location */
struct result *res = ast_expr_eval(arg, state);
@@ 544,33 590,85 @@ alloc_process(struct ast_stmt *alloc, struct state *state)
}
static struct error *
-ast_stmt_compound_precondsverify(struct ast_stmt *, struct state *);
+stmt_setupabsexec(struct ast_stmt *, struct state *);
+
+static struct error *
+labelled_setupabsexec(struct ast_stmt *, struct state *);
+
+static struct error *
+sel_setupabsexec(struct ast_stmt *, struct state *);
+
+static struct error *
+comp_setupabsexec(struct ast_stmt *, struct state *);
struct error *
-ast_stmt_precondsverify(struct ast_stmt *stmt, struct state *s)
+ast_stmt_setupabsexec(struct ast_stmt *stmt, struct state *state)
{
- switch (ast_stmt_kind(stmt)) {
+ if (ast_stmt_kind(stmt) != STMT_SELECTION) {
+ return NULL;
+ }
+ return stmt_setupabsexec(stmt, state);
+}
+
+static struct error *
+stmt_setupabsexec(struct ast_stmt *stmt, struct state *state)
+{
+ switch (ast_stmt_kind(stmt)) {
case STMT_EXPR:
- return ast_expr_precondsverify(ast_stmt_as_expr(stmt), s);
+ case STMT_ALLOCATION:
+ return NULL;
+ case STMT_LABELLED:
+ return labelled_setupabsexec(stmt, state);
+ case STMT_SELECTION:
+ return sel_setupabsexec(stmt, state);
case STMT_COMPOUND:
- return ast_stmt_compound_precondsverify(stmt, s);
+ return comp_setupabsexec(stmt, state);
default:
assert(false);
}
}
static struct error *
-ast_stmt_compound_precondsverify(struct ast_stmt *stmt, struct state *s)
+labelled_setupabsexec(struct ast_stmt *stmt, struct state *state)
{
- struct error *err;
+ /* XXX: dedupe the execution of setups */
+ struct result *res = ast_stmt_absexec(stmt, state, true);
+ if (result_iserror(res)) {
+ return result_as_error(res);
+ }
+ return NULL;
+}
+static struct error *
+sel_setupabsexec(struct ast_stmt *stmt, struct state *state)
+{
+ struct decision dec = sel_decide(ast_stmt_sel_cond(stmt), state);
+ if (dec.err) {
+ return dec.err;
+ }
+ if (dec.decision) {
+ return stmt_setupabsexec(ast_stmt_sel_body(stmt), state);
+ }
+ assert(!ast_stmt_sel_nest(stmt));
+ return NULL;
+}
+
+static struct error *
+comp_setupabsexec(struct ast_stmt *stmt, struct state *state)
+{
+ struct error *err;
struct ast_block *b = ast_stmt_as_block(stmt);
- int n = ast_block_nstmts(b);
+ assert(ast_block_ndecls(b) == 0);
+ int nstmt = 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;
+ for (int i = 0; i < nstmt; i++) {
+ if (ast_stmt_ispre(stmts[i])) {
+ if ((err = stmt_setupabsexec(stmts[i], state))) {
+ return err;
+ }
+ if (ast_stmt_isterminal(stmts[i], state)) {
+ break;
+ }
}
}
return NULL;
M src/0v/ast/type/type.c => src/0v/ast/type/type.c +14 -2
@@ 32,6 32,12 @@ ast_type_isint(struct ast_type *t)
return t->base == TYPE_INT;
}
+bool
+ast_type_ispointer(struct ast_type *t)
+{
+ return t->base == TYPE_POINTER;
+}
+
struct ast_type *
ast_type_create(enum ast_type_base base, enum ast_type_modifier mod)
{
@@ 52,6 58,14 @@ ast_type_create_ptr(struct ast_type *ref)
}
struct ast_type *
+ast_type_create_voidptr()
+{
+ struct ast_type *t = ast_type_create(TYPE_POINTER, 0);
+ t->ptr_type = TYPE_VOID;
+ return t;
+}
+
+struct ast_type *
ast_type_create_arr(struct ast_type *base, int length)
{
assert(base);
@@ 84,7 98,6 @@ ast_type_vconst(struct ast_type *t, struct state *s, char *comment, bool persist
switch (t->base) {
case TYPE_INT:
return value_int_indefinite_create();
- case TYPE_VOID:
case TYPE_POINTER:
return value_ptr_indefinite_create();
case TYPE_USERDEF:
@@ 98,7 111,6 @@ ast_type_vconst(struct ast_type *t, struct state *s, char *comment, bool persist
}
}
-
bool
ast_type_isstruct(struct ast_type *t)
{
M src/0v/ast/variable.c => src/0v/ast/variable.c +0 -1
@@ 47,7 47,6 @@ ast_variables_copy(int n, struct ast_variable **v)
return new;
}
-
char *
ast_variable_str(struct ast_variable *v)
{
M src/0v/object/object.c => src/0v/object/object.c +73 -2
@@ 162,12 162,20 @@ object_referencesheap(struct object *obj, struct state *s)
}
bool
+object_hasvalue(struct object *obj)
+{
+ if (object_isvalue(obj)) {
+ return obj->value;
+ }
+ return false;
+}
+
+bool
object_isvalue(struct object *obj)
{
return obj->type == OBJECT_VALUE;
}
-
struct value *
object_as_value(struct object *obj)
{
@@ 202,7 210,7 @@ object_references(struct object *obj, struct location *loc, struct state *s)
return v ? value_references(v, loc, s) : false;
}
-void
+struct error *
object_assign(struct object *obj, struct value *val)
{
assert(obj->type == OBJECT_VALUE);
@@ 211,6 219,7 @@ object_assign(struct object *obj, struct value *val)
* potentially */
obj->value = val;
+ return NULL;
}
static struct ast_expr *
@@ 457,6 466,68 @@ object_getmembertype(struct object *obj, struct ast_type *t, char *member,
);
}
+struct object_result {
+ struct object *val;
+ struct error *err;
+};
+
+
+struct object_result *
+object_result_error_create(struct error *err)
+{
+ assert(err);
+
+ struct object_result *r = malloc(sizeof(struct object_result));
+ r->val = NULL;
+ r->err = err;
+ return r;
+}
+
+struct object_result *
+object_result_value_create(struct object *val)
+{
+ struct object_result *r = malloc(sizeof(struct object_result));
+ r->val = val;
+ r->err = NULL;
+ return r;
+}
+
+void
+object_result_destroy(struct object_result *res)
+{
+ assert(!res->err);
+ if (res->val) {
+ object_destroy(res->val);
+ }
+ free(res);
+}
+
+bool
+object_result_iserror(struct object_result *res)
+{
+ return res->err;
+}
+
+struct error *
+object_result_as_error(struct object_result *res)
+{
+ assert(res->err);
+ return res->err;
+}
+
+struct object *
+object_result_as_value(struct object_result *res)
+{
+ assert(!res->err);
+ return res->val;
+}
+
+bool
+object_result_hasvalue(struct object_result *res)
+{
+ assert(!object_result_iserror(res));
+ return res->val; /* implicit cast */
+}
struct range {
struct ast_expr *size;
M src/0v/props/props.c => src/0v/props/props.c +12 -0
@@ 53,6 53,18 @@ props_str(struct props *p, char *indent)
return strbuilder_build(b);
}
+int
+props_n(struct props *p)
+{
+ return p->n;
+}
+
+struct ast_expr **
+props_props(struct props *p)
+{
+ return p->prop;
+}
+
void
props_install(struct props *p, struct ast_expr *e)
{
M src/0v/state/Makefile => src/0v/state/Makefile +12 -0
@@ 22,6 22,8 @@ LEX_OBJ = $(BUILD_DIR)/lex.o
GRAM_OBJ = $(BUILD_DIR)/gram.o
UTIL_OBJ = $(BUILD_DIR)/util.o
LOCATION_OBJ = $(BUILD_DIR)/location.o
+STATIC_OBJ = $(BUILD_DIR)/static.o
+CLUMP_OBJ = $(BUILD_DIR)/clump.o
HEAP_OBJ = $(BUILD_DIR)/heap.o
STACK_OBJ = $(BUILD_DIR)/stack.o
OBJECT_OBJ = $(BUILD_DIR)/object.o
@@ 33,7 35,9 @@ OBJECTS = $(XR0_OBJECTS) \
$(VALUE_OBJ) \
$(LOCATION_OBJ) \
$(BLOCK_OBJ) \
+ $(STATIC_OBJ) \
$(OBJECT_OBJ) \
+ $(CLUMP_OBJ) \
$(HEAP_OBJ) \
$(STACK_OBJ)
@@ 63,6 67,14 @@ $(HEAP_OBJ): heap.c $(BLOCK_OBJ)
@printf 'CC\t$@\n'
@$(CC) $(CFLAGS) -o $@ -c heap.c
+$(CLUMP_OBJ): clump.c $(BLOCK_OBJ)
+ @printf 'CC\t$@\n'
+ @$(CC) $(CFLAGS) -o $@ -c clump.c
+
+$(STATIC_OBJ): static.c $(BLOCK_OBJ)
+ @printf 'CC\t$@\n'
+ @$(CC) $(CFLAGS) -o $@ -c static.c
+
$(BLOCK_OBJ): block.c $(OBJECT_OBJ)
@printf 'CC\t$@\n'
@$(CC) $(CFLAGS) -o $@ -c block.c
A src/0v/state/clump.c => src/0v/state/clump.c +69 -0
@@ 0,0 1,69 @@
+#include <stdlib.h>
+#include <stdbool.h>
+#include <assert.h>
+
+#include "ast.h"
+#include "location.h"
+#include "block.h"
+#include "util.h"
+
+struct clump {
+ struct block_arr *blocks;
+};
+
+struct clump *
+clump_create()
+{
+ struct clump *c = malloc(sizeof(struct clump));
+ assert(c);
+ c->blocks = block_arr_create();
+ return c;
+}
+
+void
+clump_destroy(struct clump *c)
+{
+ block_arr_destroy(c->blocks);
+}
+
+char *
+clump_str(struct clump *c, char *indent)
+{
+ struct strbuilder *b = strbuilder_create();
+ int n = block_arr_nblocks(c->blocks);
+ struct block **arr = block_arr_blocks(c->blocks);
+ for (int i = 0; i < n; i++) {
+ char *block = block_str(arr[i]);
+ strbuilder_printf(b, "%s%d: %s\n", indent, i, block);
+ free(block);
+ }
+ return strbuilder_build(b);
+}
+
+struct clump *
+clump_copy(struct clump *c)
+{
+ struct clump *copy = malloc(sizeof(struct clump));
+ copy->blocks = block_arr_copy(c->blocks);
+ return copy;
+}
+
+int
+clump_newblock(struct clump *c)
+{
+ int address = block_arr_append(c->blocks, block_create());
+
+ int n = block_arr_nblocks(c->blocks);
+ assert(n > 0);
+
+ return address;
+}
+
+struct block *
+clump_getblock(struct clump *c, int address)
+{
+ if (address >= block_arr_nblocks(c->blocks)) {
+ return NULL;
+ }
+ return block_arr_blocks(c->blocks)[address];
+}
A src/0v/state/clump.h => src/0v/state/clump.h +28 -0
@@ 0,0 1,28 @@
+#ifndef CLUMP_H
+#define CLUMP_H
+
+#include "block.h"
+
+struct clump;
+
+struct clump *
+clump_create();
+
+void
+clump_destroy(struct clump *);
+
+char *
+clump_str(struct clump *, char * indent);
+
+struct clump *
+clump_copy(struct clump *);
+
+int
+clump_newblock(struct clump *);
+
+struct block;
+
+struct block *
+clump_getblock(struct clump *c, int address);
+
+#endif
M src/0v/state/heap.c => src/0v/state/heap.c +6 -1
@@ 131,6 131,12 @@ heap_deallocblock(struct heap *h, int address)
return NULL;
}
+bool
+heap_blockisfreed(struct heap *h, int address)
+{
+ return h->freed[address];
+}
+
void
heap_undeclare(struct heap *h, struct state *s)
{
@@ 339,7 345,6 @@ vconst_str(struct vconst *v, char *indent)
}
return strbuilder_build(b);
}
-
bool
vconst_eval(struct vconst *v, struct ast_expr *e)
{
M src/0v/state/heap.h => src/0v/state/heap.h +3 -0
@@ 33,6 33,9 @@ heap_getblock(struct heap *h, int block);
bool
heap_referenced(struct heap *h, struct state *);
+bool
+heap_blockisfreed(struct heap *h, int block);
+
struct error *
heap_deallocblock(struct heap *h, int block);
M src/0v/state/intern.h => src/0v/state/intern.h +1 -1
@@ 4,7 4,7 @@
struct location;
struct object;
-struct object *
+struct object_res
state_get(struct state *state, struct location *loc, bool constructive);
struct block *
M src/0v/state/location.c => src/0v/state/location.c +130 -16
@@ 4,6 4,8 @@
#include <assert.h>
#include "ast.h"
#include "block.h"
+#include "clump.h"
+#include "static.h"
#include "heap.h"
#include "intern.h"
#include "location.h"
@@ 16,18 18,18 @@
struct location {
enum location_type type;
union {
- int frame; /* LOCATION_AUTOMATIC */
+ int frame; /* LOCATION_AUTOMATIC */
} u;
int block;
struct ast_expr *offset;
};
struct location *
-location_create_dynamic(int block, struct ast_expr *offset)
+location_create_vconst(int block, struct ast_expr *offset)
{
struct location *loc = malloc(sizeof(struct location));
assert(loc);
- loc->type = LOCATION_DYNAMIC;
+ loc->type = LOCATION_VCONST;
loc->block = block;
assert(offset);
loc->offset = offset;
@@ 35,11 37,35 @@ location_create_dynamic(int block, struct ast_expr *offset)
}
struct location *
-location_create_vconst(int block, struct ast_expr *offset)
+location_create_dereferencable(int block, struct ast_expr *offset)
{
struct location *loc = malloc(sizeof(struct location));
assert(loc);
- loc->type = LOCATION_VCONST;
+ loc->type = LOCATION_DEREFERENCABLE;
+ loc->block = block;
+ assert(offset);
+ loc->offset = offset;
+ return loc;
+}
+
+struct location *
+location_create_static(int block, struct ast_expr *offset)
+{
+ struct location *loc = malloc(sizeof(struct location));
+ assert(loc);
+ loc->type = LOCATION_STATIC;
+ loc->block = block;
+ assert(offset);
+ loc->offset = offset;
+ return loc;
+}
+
+struct location *
+location_create_dynamic(int block, struct ast_expr *offset)
+{
+ struct location *loc = malloc(sizeof(struct location));
+ assert(loc);
+ loc->type = LOCATION_DYNAMIC;
loc->block = block;
assert(offset);
loc->offset = offset;
@@ 59,6 85,20 @@ location_create_automatic(int frame, int block, struct ast_expr *offset)
return loc;
}
+struct value *
+location_transfigure(struct location *loc, struct state *compare)
+{
+ switch (loc->type) {
+ case LOCATION_AUTOMATIC:
+ case LOCATION_DEREFERENCABLE:
+ return state_clump(compare);
+ case LOCATION_DYNAMIC:
+ return state_alloc(compare);
+ default:
+ assert(false);
+ }
+}
+
void
location_destroy(struct location *loc)
{
@@ 74,12 114,18 @@ location_str(struct location *loc)
{
struct strbuilder *b = strbuilder_create();
switch (loc->type) {
+ case LOCATION_STATIC:
+ strbuilder_printf(b, "static:");
+ break;
case LOCATION_AUTOMATIC:
strbuilder_printf(b, "stack[%d]:", loc->u.frame);
break;
case LOCATION_DYNAMIC:
strbuilder_printf(b, "heap:");
break;
+ case LOCATION_DEREFERENCABLE:
+ strbuilder_printf(b, "clump:");
+ break;
default:
assert(false);
}
@@ 123,10 169,18 @@ struct location *
location_copy(struct location *loc)
{
switch (loc->type) {
+ case LOCATION_STATIC:
+ return location_create_static(
+ loc->block, ast_expr_copy(loc->offset)
+ );
case LOCATION_VCONST:
return location_create_vconst(
loc->block, ast_expr_copy(loc->offset)
);
+ case LOCATION_DEREFERENCABLE:
+ return location_create_dereferencable(
+ loc->block, ast_expr_copy(loc->offset)
+ );
case LOCATION_AUTOMATIC:
return location_create_automatic(
loc->u.frame, loc->block, ast_expr_copy(loc->offset)
@@ 154,7 208,15 @@ location_with_offset(struct location *loc, struct ast_expr *offset)
}
bool
-location_isdeallocand(struct location *loc, struct heap *h)
+location_tostatic(struct location *loc, struct static_memory *sm)
+{
+ bool type_equal = loc->type == LOCATION_STATIC;
+ struct block *b = static_memory_getblock(sm, loc->block);
+ return type_equal && b;
+}
+
+bool
+location_toheap(struct location *loc, struct heap *h)
{
bool type_equal = loc->type == LOCATION_DYNAMIC;
struct block *b = heap_getblock(h, loc->block);
@@ 162,6 224,23 @@ location_isdeallocand(struct location *loc, struct heap *h)
}
bool
+location_tostack(struct location *loc, struct stack *s)
+{
+ bool type_equal = loc->type == LOCATION_AUTOMATIC;
+ /* XXX: should probably check that frame is greater than current frame */
+ struct block *b = stack_getblock(s, loc->block);
+ return type_equal && b;
+}
+
+bool
+location_toclump(struct location *loc, struct clump *c)
+{
+ bool type_equal = loc->type == LOCATION_DEREFERENCABLE;
+ struct block *b = clump_getblock(c, loc->block);
+ return type_equal && b;
+}
+
+bool
location_equal(struct location *l1, struct location *l2)
{
return l1->type == l2->type
@@ 190,30 269,65 @@ bool
location_referencesheap(struct location *l, struct state *s)
{
if (l->type == LOCATION_DYNAMIC) {
+ if (heap_blockisfreed(state_getheap(s), l->block)) {
+ return false;
+ }
return true;
}
- struct object *obj = state_get(s, l, false);
- return obj && object_referencesheap(obj, s);
+ struct object_res res = state_get(s, l, false);
+ if (res.err) {
+ assert(false);
+ }
+ return res.obj && object_referencesheap(res.obj, s);
}
-struct block *
-location_getblock(struct location *loc, struct vconst *v, struct stack *s,
- struct heap *h)
+static struct block_res
+location_auto_getblock(struct location *, struct stack *);
+
+struct block_res
+location_getblock(struct location *loc, struct static_memory *sm, struct vconst *v, struct stack *s,
+ struct heap *h, struct clump *c)
{
assert(s);
switch (loc->type) {
+ case LOCATION_STATIC:
+ return (struct block_res) {
+ .b = static_memory_getblock( sm, loc->block),
+ .err = NULL
+ };
case LOCATION_AUTOMATIC:
- return stack_getblock(
- stack_getframe(s, loc->u.frame),
- loc->block
- );
+ return location_auto_getblock(loc, s);
case LOCATION_DYNAMIC:
- return heap_getblock(h, loc->block);
+ return (struct block_res) {
+ .b = heap_getblock(h, loc->block),
+ .err = NULL
+ };
+ case LOCATION_DEREFERENCABLE:
+ return (struct block_res) {
+ .b = clump_getblock(c, loc->block),
+ .err = NULL
+ };
default:
assert(false);
}
}
+static struct block_res
+location_auto_getblock(struct location *loc, struct stack *s)
+{
+ struct stack *f = stack_getframe(s, loc->u.frame);
+ if (!f) {
+ return (struct block_res) {
+ .b = NULL,
+ .err = error_create("stack frame doesn't exist")
+ };
+ }
+ return (struct block_res) {
+ .b = stack_getblock(f, loc->block),
+ .err = NULL
+ };
+}
+
struct block *
location_getstackblock(struct location *loc, struct stack *s)
{
M src/0v/state/location.h => src/0v/state/location.h +46 -5
@@ 6,21 6,33 @@
struct ast_expr;
enum location_type {
- /* TODO: STATIC */
- LOCATION_VCONST, LOCATION_AUTOMATIC, LOCATION_DYNAMIC,
+ LOCATION_STATIC,
+ LOCATION_VCONST,
+ LOCATION_DEREFERENCABLE,
+ LOCATION_AUTOMATIC,
+ LOCATION_DYNAMIC,
};
struct location;
struct location *
+location_create_static(int block, struct ast_expr *offset);
+
+struct location *
location_create_vconst(int block, struct ast_expr *offset);
struct location *
+location_create_dereferencable(int block, struct ast_expr *offset);
+
+struct location *
location_create_dynamic(int block, struct ast_expr *offset);
struct location *
location_create_automatic(int frame, int block, struct ast_expr *offset);
+struct value *
+location_transfigure(struct location *, struct state *compare);
+
void
location_setframe(struct location *loc, int frame);
@@ 39,6 51,26 @@ location_str(struct location *);
bool
location_isauto(struct location *);
+struct static_memory;
+
+bool
+location_tostatic(struct location *, struct static_memory *);
+
+struct heap;
+
+bool
+location_toheap(struct location *, struct heap *);
+
+struct stack;
+
+bool
+location_tostack(struct location *, struct stack *);
+
+struct clump;
+
+bool
+location_toclump(struct location *, struct clump *);
+
bool
location_referencesheap(struct location *, struct state *);
@@ 61,17 93,26 @@ location_equal(struct location *loc1, struct location *loc2);
bool
location_references(struct location *loc1, struct location *loc2, struct state *);
+struct static_memory;
+
struct vconst;
-struct stack;
+struct clump;
struct stack;
+
struct object;
struct block;
-struct block *
-location_getblock(struct location *, struct vconst *, struct stack *, struct heap *);
+struct block_res {
+ struct block *b;
+ struct error *err;
+};
+
+struct block_res
+location_getblock(struct location *, struct static_memory *, struct vconst *, struct stack *,
+ struct heap *, struct clump *);
struct block *
location_getstackblock(struct location *loc, struct stack *s);
M src/0v/state/stack.c => src/0v/state/stack.c +16 -10
@@ 62,7 62,7 @@ stack_getframe(struct stack *s, int frame) {
return s;
}
if (!s->prev) {
- assert(false);
+ return NULL;
}
return stack_getframe(s->prev, frame);
}
@@ 164,7 164,7 @@ void
stack_declare(struct stack *stack, struct ast_variable *var, bool isparam)
{
char *id = ast_variable_name(var);
- assert(!map_get(stack->varmap, id));
+ assert(!map_get(stack->varmap, id)); /* XXX: user error */
map_set(
stack->varmap,
dynamic_str(id),
@@ 263,9 263,12 @@ variable_create(struct ast_type *type, struct stack *stack, bool isparam)
/* create block with uninitialised object at offset 0 */
v->loc = stack_newblock(stack);
- struct block *b = location_getblock(v->loc, NULL, stack, NULL);
- assert(b);
- block_install(b, object_value_create(ast_expr_constant_create(0), NULL));
+ struct block_res res = location_getblock(v->loc, NULL, NULL, stack, NULL, NULL);
+ if (res.err) {
+ assert(false);
+ }
+ assert(res.b);
+ block_install(res.b, object_value_create(ast_expr_constant_create(0), NULL));
return v;
}
@@ 295,12 298,15 @@ variable_abstractcopy(struct variable *old, struct state *s)
new->type = ast_type_copy(old->type);
new->isparam = old->isparam;
new->loc = location_copy(old->loc);
- struct object *obj = state_get(s, new->loc, false);
- assert(obj);
- if (object_isvalue(obj)) {
- struct value *v = object_as_value(obj);
+ struct object_res res = state_get(s, new->loc, false);
+ if (res.err) {
+ assert(false);
+ }
+ assert(res.obj);
+ if (object_isvalue(res.obj)) {
+ struct value *v = object_as_value(res.obj);
if (v) {
- object_assign(obj, value_abstractcopy(v, s));
+ object_assign(res.obj, value_abstractcopy(v, s));
}
}
return new;
M src/0v/state/state.c => src/0v/state/state.c +186 -24
@@ 5,19 5,24 @@
#include "ast.h"
#include "block.h"
+#include "clump.h"
#include "ext.h"
#include "heap.h"
+#include "static.h"
#include "location.h"
#include "object.h"
#include "props.h"
#include "stack.h"
#include "state.h"
+#include "static.h"
#include "util.h"
#include "value.h"
struct state {
struct externals *ext;
struct vconst *vconst;
+ struct static_memory *static_memory;
+ struct clump *clump;
struct stack *stack;
struct heap *heap;
struct props *props;
@@ 29,17 34,37 @@ state_create(char *func, struct externals *ext, struct ast_type *result_type)
struct state *state = malloc(sizeof(struct state));
assert(state);
state->ext = ext;
+ state->static_memory = static_memory_create();
state->vconst = vconst_create();
+ state->clump = clump_create();
state->stack = stack_create(func, NULL, result_type);
state->heap = heap_create();
state->props = props_create();
return state;
}
+struct state *
+state_create_withprops(char *func, struct externals *ext, struct ast_type *result_type,
+ struct props *props)
+{
+ struct state *state = malloc(sizeof(struct state));
+ assert(state);
+ state->ext = ext;
+ state->static_memory = static_memory_create();
+ state->vconst = vconst_create();
+ state->clump = clump_create();
+ state->stack = stack_create(func, NULL, result_type);
+ state->heap = heap_create();
+ state->props = props_copy(props);
+ return state;
+}
+
void
state_destroy(struct state *state)
{
/* vconst_destroy(state->vconst); */
+ static_memory_destroy(state->static_memory);
+ clump_destroy(state->clump);
stack_destroy(state->stack);
heap_destroy(state->heap);
props_destroy(state->props);
@@ 52,7 77,9 @@ state_copy(struct state *state)
struct state *copy = malloc(sizeof(struct state));
assert(copy);
copy->ext = state->ext;
+ copy->static_memory = static_memory_copy(state->static_memory);
copy->vconst = vconst_copy(state->vconst);
+ copy->clump = clump_copy(state->clump);
copy->stack = stack_copy(state->stack);
copy->heap = heap_copy(state->heap);
copy->props = props_copy(state->props);
@@ 65,7 92,9 @@ state_copywithname(struct state *state, char *func_name)
struct state *copy = malloc(sizeof(struct state));
assert(copy);
copy->ext = state->ext;
+ copy->static_memory = static_memory_copy(state->static_memory);
copy->vconst = vconst_copy(state->vconst);
+ copy->clump = clump_copy(state->clump);
copy->stack = stack_copywithname(state->stack, func_name);
copy->heap = heap_copy(state->heap);
copy->props = props_copy(state->props);
@@ 82,11 111,17 @@ state_str(struct state *state)
strbuilder_printf(b, "%s\n", ext);
}
free(ext);
+ char *static_mem = static_memory_str(state->static_memory, "\t");
+ strbuilder_printf(b, "%s\n", static_mem);
+ free(static_mem);
char *vconst = vconst_str(state->vconst, "\t");
if (strlen(vconst) > 0) {
strbuilder_printf(b, "%s\n", vconst);
}
free(vconst);
+ char *clump = clump_str(state->clump, "\t");
+ strbuilder_printf(b, "%s\n", clump);
+ free(clump);
char *stack = stack_str(state->stack, state);
strbuilder_printf(b, "%s\n", stack);
free(stack);
@@ 110,6 145,12 @@ state_getext(struct state *s)
return s->ext;
}
+struct heap *
+state_getheap(struct state *s)
+{
+ return s->heap;
+}
+
struct props *
state_getprops(struct state *s)
{
@@ 153,30 194,118 @@ state_vconst(struct state *state, struct ast_type *t, char *comment, bool persis
}
struct value *
+state_static_init(struct state *state, struct ast_expr *expr)
+{
+ char *lit = ast_expr_as_literal(expr);
+ struct location *loc = static_memory_checkpool(state->static_memory, lit);
+ if (loc) {
+ return value_ptr_create(loc);
+ }
+ int address = static_memory_newblock(state->static_memory);
+ loc = location_create_static(
+ address,
+ ast_expr_constant_create(0)
+ );
+ struct object_res res = state_get(state, loc, true);
+ if (res.err) {
+ assert(false);
+ }
+ if (!res.obj) {
+ assert(false);
+ }
+ object_assign(res.obj, value_literal_create(dynamic_str(lit)));
+
+ static_memory_stringpool(state->static_memory, lit, loc);
+
+ return value_ptr_create(loc);
+}
+
+struct value *
+state_clump(struct state *state)
+{
+ /* XXX: should type be associated with blocks for type checking when we
+ * assign? */
+ int address = clump_newblock(state->clump);
+ struct location *loc = location_create_dereferencable(
+ address,
+ ast_expr_constant_create(0)
+ );
+ return value_ptr_create(loc);
+}
+
+bool
+state_islval(struct state *state, struct value *v)
+{
+ assert(v);
+ if (!value_islocation(v)) {
+ return false;
+ }
+ struct location *loc = value_as_location(v);
+ struct object_res res= state_get(state, loc, true); /* put object there */
+ if (res.err) {
+ assert(false);
+ }
+ return location_tostatic(loc, state->static_memory) ||
+ location_toheap(loc, state->heap) ||
+ location_tostack(loc, state->stack) ||
+ location_toclump(loc, state->clump);
+}
+
+bool
+state_isalloc(struct state *state, struct value *v)
+{
+ assert(v);
+ if (!value_islocation(v)) {
+ return false;
+ }
+ struct location *loc = value_as_location(v);
+ struct object_res res = state_get(state, loc, true); /* put object there */
+ if (res.err) {
+ assert(false);
+ }
+ return location_toheap(loc, state->heap);
+}
+
+struct value *
state_getvconst(struct state *state, char *id)
{
return vconst_get(state->vconst, id);
}
-struct object *
+struct object_res
state_get(struct state *state, struct location *loc, bool constructive)
{
- struct block *b = location_getblock(
- loc, state->vconst, state->stack, state->heap
+ struct block_res res = location_getblock(
+ loc, state->static_memory, state->vconst, state->stack, state->heap, state->clump
);
- if (!b) {
- assert(location_type(loc) == LOCATION_DYNAMIC);
- return NULL;
+ if (res.err) {
+ return (struct object_res) { .obj = NULL, .err = res.err };
+ }
+ if (!res.b) {
+ assert(location_type(loc) == LOCATION_DYNAMIC ||
+ location_type(loc) == LOCATION_DEREFERENCABLE);
+ return (struct object_res) { .obj = NULL, .err = NULL };
}
- return block_observe(b, location_offset(loc), state, constructive);
+ struct object *obj = block_observe(res.b, location_offset(loc), state, constructive);
+ return (struct object_res) { .obj = obj, .err = NULL };
+}
+
+void
+state_blockinstall(struct block *b, struct object *obj)
+{
+ block_install(b, obj);
}
struct block *
state_getblock(struct state *state, struct location *loc)
{
- return location_getblock(
- loc, state->vconst, state->stack, state->heap
+ struct block_res res = location_getblock(
+ loc, state->static_memory, state->vconst, state->stack, state->heap, state->clump
);
+ if (res.err) {
+ assert(false);
+ }
+ return res.b;
}
struct object *
@@ 185,7 314,11 @@ state_getresult(struct state *state)
struct variable *v = stack_getresult(state->stack);
assert(v);
- return state_get(state, variable_location(v), true);
+ struct object_res res = state_get(state, variable_location(v), true);
+ if (res.err) {
+ assert(false);
+ }
+ return res.obj;
}
static struct ast_type *
@@ 231,19 364,30 @@ state_getobject(struct state *state, char *id)
assert(false);
}
- return state_get(state, variable_location(v), true);
+ struct object_res res = state_get(state, variable_location(v), true);
+ if (res.err) {
+ assert(false);
+ }
+ return res.obj;
}
-
-struct object *
+struct object_res
state_deref(struct state *state, struct value *ptr_val, struct ast_expr *index)
{
+ if (value_issync(ptr_val)) {
+ return (struct object_res) { .obj = NULL, .err = NULL};
+ }
struct location *deref_base = value_as_location(ptr_val);
assert(deref_base);
/* `*(ptr+offset)` */
struct location *deref = location_with_offset(deref_base, index);
- struct object *res = state_get(state, deref, true);
+ struct object_res res = state_get(state, deref, true);
+ if (res.err) {
+ struct strbuilder *b = strbuilder_create();
+ strbuilder_printf(b, "undefined indirection: %s", res.err->msg);
+ return (struct object_res) { .obj = NULL, .err = error_create(strbuilder_build(b))};
+ }
/*location_destroy(deref);*/
return res;
}
@@ 261,10 405,13 @@ state_range_alloc(struct state *state, struct object *obj,
/* assume pointer */
struct location *deref = value_as_location(arr_val);
- struct block *b = location_getblock(
- deref, state->vconst, state->stack, state->heap
+ struct block_res res = location_getblock(
+ deref, state->static_memory, state->vconst, state->stack, state->heap, state->clump
);
- if (!b) {
+ if (res.err) {
+ assert(false);
+ }
+ if (!res.b) {
return error_create("no block");
}
@@ 272,7 419,7 @@ state_range_alloc(struct state *state, struct object *obj,
assert(!ast_expr_equal(lw, up));
/* virtual block to represents range of values allocated */
- return block_range_alloc(b, lw, up, state->heap);
+ return block_range_alloc(res.b, lw, up, state->heap);
}
struct value *
@@ 290,7 437,6 @@ state_dealloc(struct state *state, struct value *val)
return location_dealloc(value_as_location(val), state->heap);
}
-
struct error *
state_range_dealloc(struct state *state, struct object *obj,
struct ast_expr *lw, struct ast_expr *up)
@@ 336,16 482,19 @@ state_range_aredeallocands(struct state *state, struct object *obj,
}
struct location *deref = value_as_location(arr_val);
- struct block *b = location_getblock(
- deref, state->vconst, state->stack, state->heap
+ struct block_res res = location_getblock(
+ deref, state->static_memory, state->vconst, state->stack, state->heap, state->clump
);
- return (bool) b && block_range_aredeallocands(b, lw, up, state);
+ if (res.err) {
+ assert(false);
+ }
+ return (bool) res.b && block_range_aredeallocands(res.b, lw, up, state);
}
bool
state_hasgarbage(struct state *state)
{
- return heap_referenced(state->heap, state);
+ return !heap_referenced(state->heap, state);
}
void
@@ 367,6 516,9 @@ state_eval(struct state *s, struct ast_expr *e)
}
static void
+state_undeclareliterals(struct state *s);
+
+static void
state_undeclarevars(struct state *s);
static void
@@ 377,6 529,8 @@ state_equal(struct state *s1, struct state *s2)
{
struct state *s1_c = state_copy(s1),
*s2_c = state_copy(s2);
+ state_undeclareliterals(s1_c);
+ state_undeclareliterals(s2_c);
state_undeclarevars(s1_c);
state_undeclarevars(s2_c);
state_popprops(s1_c);
@@ 399,6 553,14 @@ state_equal(struct state *s1, struct state *s2)
}
static void
+state_undeclareliterals(struct state *s)
+{
+ static_memory_destroy(s->static_memory);
+ /* XXX: map leaks */
+ s->static_memory = static_memory_create();
+}
+
+static void
state_undeclarevars(struct state *s)
{
heap_undeclare(s->heap, s);
@@ 409,6 571,6 @@ state_undeclarevars(struct state *s)
static void
state_popprops(struct state *s)
{
- /* XXX: */
+ props_destroy(s->props);
s->props = props_create();
}
A src/0v/state/static.c => src/0v/state/static.c +110 -0
@@ 0,0 1,110 @@
+#include <stdlib.h>
+#include <stdbool.h>
+#include <assert.h>
+
+#include "ast.h"
+#include "location.h"
+#include "block.h"
+#include "value.h"
+#include "util.h"
+
+struct static_memory {
+ struct block_arr *blocks;
+ struct map *pool;
+};
+
+struct static_memory *
+static_memory_create()
+{
+ struct static_memory *sm = malloc(sizeof(struct static_memory));
+ assert(sm);
+ sm->blocks = block_arr_create();
+ sm->pool = map_create();
+ return sm;
+}
+
+void
+static_memory_destroy(struct static_memory *sm)
+{
+ block_arr_destroy(sm->blocks);
+}
+
+char *
+static_memory_str(struct static_memory *sm, char *indent)
+{
+ struct strbuilder *b = strbuilder_create();
+ int n = block_arr_nblocks(sm->blocks);
+ struct block **arr = block_arr_blocks(sm->blocks);
+ for (int i = 0; i < n; i++) {
+ char *block = block_str(arr[i]);
+ strbuilder_printf(b, "%s%d: %s\n", indent, i, block);
+ free(block);
+ }
+ return strbuilder_build(b);
+}
+
+static struct map *
+pool_copy(struct map *);
+
+struct static_memory *
+static_memory_copy(struct static_memory *sm)
+{
+ struct static_memory *copy = malloc(sizeof(struct static_memory));
+ copy->blocks = block_arr_copy(sm->blocks);
+ copy->pool = pool_copy(sm->pool);
+ return copy;
+}
+
+static struct map *
+pool_copy(struct map *p)
+{
+ struct map *pcopy = map_create();
+ for (int i = 0; i < p->n; i++) {
+ struct entry e = p->entry[i];
+ map_set(
+ pcopy,
+ dynamic_str(e.key),
+ location_copy((struct location *) e.value)
+ );
+ }
+ return pcopy;
+
+}
+
+int
+static_memory_newblock(struct static_memory *sm)
+{
+ int address = block_arr_append(sm->blocks, block_create());
+
+ int n = block_arr_nblocks(sm->blocks);
+ assert(n > 0);
+ return address;
+}
+
+struct block *
+static_memory_getblock(struct static_memory *sm, int address)
+{
+ if (address >= block_arr_nblocks(sm->blocks)) {
+ return NULL;
+ }
+ return block_arr_blocks(sm->blocks)[address];
+}
+
+/* string pooling to write one string literal to static_memory and all subsequent
+ * literals reference it is used to avoid infinite loops in splitting logic with
+ * different literals per selection condition */
+void
+static_memory_stringpool(struct static_memory *sm, char *lit, struct location *loc)
+{
+ map_set(
+ sm->pool,
+ dynamic_str(lit),
+ location_copy(loc)
+ );
+}
+
+struct location *
+static_memory_checkpool(struct static_memory *sm, char *lit)
+{
+ return (struct location *) map_get(sm->pool, lit);
+}
A src/0v/state/static.h => src/0v/state/static.h +36 -0
@@ 0,0 1,36 @@
+#ifndef STATIC_H
+#define STATIC_H
+
+#include "block.h"
+
+struct static_memory;
+
+struct static_memory *
+static_memory_create();
+
+void
+static_memory_destroy(struct static_memory *);
+
+char *
+static_memory_str(struct static_memory *, char * indent);
+
+struct static_memory *
+static_memory_copy(struct static_memory *);
+
+struct value;
+
+int
+static_memory_newblock(struct static_memory *);
+
+struct block;
+
+struct block *
+static_memory_getblock(struct static_memory *, int address);
+
+void
+static_memory_stringpool(struct static_memory *sm, char *lit, struct location *);
+
+struct location *
+static_memory_checkpool(struct static_memory *, char *);
+
+#endif
M src/0v/value/value.c => src/0v/value/value.c +25 -2
@@ 31,8 31,7 @@ struct value {
struct map *m; /* maps to objects */
} _struct;
};
-};
-
+};
struct value *
value_ptr_create(struct location *loc)
{
@@ 110,6 109,30 @@ value_literal_create(char *lit)
return v;
}
+struct value *
+value_transfigure(struct value *v, struct state *compare, bool islval)
+{
+ switch (v->type) {
+ case VALUE_SYNC:
+ case VALUE_LITERAL:
+ return islval ? NULL: v;
+ case VALUE_STRUCT:
+ assert(false);
+ case VALUE_INT:
+ return islval ? NULL: state_vconst(
+ compare,
+ /* XXX: we will investigate type conversions later */
+ ast_type_create_voidptr(),
+ NULL,
+ false
+ );
+ case VALUE_PTR:
+ return location_transfigure(value_as_location(v), compare);
+ default:
+ assert(false);
+ }
+}
+
struct number *
number_ne_create(int not_val);
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 alleged states differ
+qed error: 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 alleged states differ
+qed error: actual and abstract states differ
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 alleged states differ
+qed error: actual and abstract states differ
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($);
+ pre: .alloc p;
.dealloc p;
]{
D tests/1-branches/0000-trivial.x => tests/1-branches/0000-trivial.x +0 -36
@@ 1,36 0,0 @@
-#include <stdlib.h>
-
-void *
-test(int x) ~ [
- assume: x;
- .alloc result;
-]{
- return malloc(1);
-}
-
-void *
-test2(int x) ~ [
- assume: !x;
- .alloc result;
-]{
- return malloc(1);
-}
-
-void *
-test3(int x) ~ [
- assume: x;
- assume: x;
- .alloc result;
-]{
- return malloc(1);
-}
-
-void *
-test4(int x) ~ [
- assume: x;
- assume: !x;
- /* should ignore everything after the contradiction */
- .alloc result;
-]{
- return NULL;
-}
M tests/1-branches/0200-conditional-allocation.x => tests/1-branches/0200-conditional-allocation.x +2 -10
@@ 2,20 2,12 @@
void *
test(int x) ~ [
- assume: x;
if (x) {
.alloc result;
}
-]{
- return malloc(1);
-}
-
-void *
-test2(int x) ~ [
- assume: !x;
- if (x) {
+ if (!x) {
.alloc result;
}
]{
- return NULL;
+ return malloc(1);
}
D tests/1-branches/0210-FAIL-conditional-allocation-body.x => tests/1-branches/0210-FAIL-conditional-allocation-body.x +0 -16
@@ 1,16 0,0 @@
-#include <stdlib.h>
-
-void *
-test(int x) ~ [
- assume: x;
- .alloc result;
-]{
- return NULL;
-}
-
-void *
-test2(int x) ~ [
- assume: !x;
-]{
- return NULL;
-}
D tests/1-branches/0210-FAIL-conditional-allocation-body.x.EXPECTED => tests/1-branches/0210-FAIL-conditional-allocation-body.x.EXPECTED +0 -1
@@ 1,1 0,0 @@
-qed error: actual and alleged states differ
D tests/1-branches/0220-FAIL-conditional-allocation-body.x => tests/1-branches/0220-FAIL-conditional-allocation-body.x +0 -16
@@ 1,16 0,0 @@
-#include <stdlib.h>
-
-void *
-test(int x) ~ [
- assume: x;
- .alloc result;
-]{
- return malloc(1);
-}
-
-void *
-test2(int x) ~ [
- assume: !x;
-]{
- return malloc(1);
-}
D tests/1-branches/0220-FAIL-conditional-allocation-body.x.EXPECTED => tests/1-branches/0220-FAIL-conditional-allocation-body.x.EXPECTED +0 -1
@@ 1,1 0,0 @@
-qed error: actual and alleged 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 alleged states differ
+qed error: 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 alleged states differ
+qed error: actual and abstract states differ
M tests/1-branches/0400-strcmp-conditional-allocation.x => tests/1-branches/0400-strcmp-conditional-allocation.x +3 -8
@@ 3,17 3,12 @@
void *
test(char *s) ~ [
- assume: strcmp(s, "yes") == 0;
if (strcmp(s, "yes") == 0) {
.alloc result;
}
+ if (!(strcmp(s, "yes") == 0)) {
+ .alloc result;
+ }
]{
return malloc(1);
}
-
-void *
-test2(char *s) ~ [
- assume: !(strcmp(s, "yes") == 0);
-]{
- return NULL;
-}
M tests/5-pass-by-ptr/000-basic.x => tests/5-pass-by-ptr/000-basic.x +1 -0
@@ 2,6 2,7 @@
void *
assign(void *p) ~ [
+ pre: .clump p;
*p = 1;
] {
/* TODO: internal verification */
D tests/6-preconditions/000-basic.x => tests/6-preconditions/000-basic.x +0 -47
@@ 1,47 0,0 @@
-#include <stdio.h>
-#include <stdlib.h>
-
-int
-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;
-}
-
-int
-main()
-{
- /* TODO: declarator lists are truncated, only first declared in state */
- int x;
- int y;
- int r;
-
- /* 11 is Maximum length of a 32 but integer including sign */
- /*char res[11];*/
- char *res;
-
- res = malloc(11);
-
- puts("Enter x: ");
- scanf("%d", &x);
- puts("Enter y: ");
- scanf("%d", &y);
-
- if (y == 0) {
- free(res);
- /* XXX: should be `exit'. should Xr0 ignore memory concerns on
- * `exit'? */
- return 1;
- }
-
- r = ratio(x, y);
-
- /* use sprintf to convert int to string */
- sprintf(res, "%d", r);
- puts(res);
-
- free(res);
- return 0;
-}
A tests/6-preconditions/100-FAIL-need-alloced-lval.x => tests/6-preconditions/100-FAIL-need-alloced-lval.x +16 -0
@@ 0,0 1,16 @@
+#include <stdlib.h>
+
+int
+func(int *x) ~ [
+ pre: .alloc x;
+ *x = 5;
+]{
+ *x = 5;
+}
+
+int
+main()
+{
+ int p;
+ func(&p); /* ERROR: spec requires heap */
+}
A tests/6-preconditions/100-FAIL-need-alloced-lval.x.EXPECTED => tests/6-preconditions/100-FAIL-need-alloced-lval.x.EXPECTED +1 -0
@@ 0,0 1,1 @@
+6-preconditions/100-FAIL-need-alloced-lval.x:15:10: cannot exec statement: parameter 'x' must be heap allocated
A tests/6-preconditions/101-FAIL-need-alloced-rval.x => tests/6-preconditions/101-FAIL-need-alloced-rval.x +22 -0
@@ 0,0 1,22 @@
+#include <stdlib.h>
+
+int
+func(int *x) ~ [
+ int i;
+ pre: {
+ .alloc x;
+ *x = $;
+ }
+ result = *x;
+]{
+ return *x;
+}
+
+int
+main()
+{
+ int p;
+ int q;
+ p = malloc(1);
+ q = func(p); /* ERROR: spec required rvalue */
+}
A tests/6-preconditions/101-FAIL-need-alloced-rval.x.EXPECTED => tests/6-preconditions/101-FAIL-need-alloced-rval.x.EXPECTED +1 -0
@@ 0,0 1,1 @@
+6-preconditions/101-FAIL-need-alloced-rval.x:21:13: cannot exec statement: parameter 'x' must be rvalue
A tests/6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x => tests/6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x +17 -0
@@ 0,0 1,17 @@
+#include <stdlib.h>
+
+int
+func(int *x) ~ [
+ pre: .clump x;
+]{
+}
+
+int
+main()
+{
+ int *p;
+ p = malloc(1);
+ free(p);
+
+ func(p); /* ERROR: spec required rvalue */
+}
A 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 -0
@@ 0,0 1,1 @@
+6-preconditions/102-FAIL-need-clump-lval-freed-ptr.x:16:9: cannot exec statement: parameter 'x' must be lvalue
A tests/6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x => tests/6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x +17 -0
@@ 0,0 1,17 @@
+#include <stdlib.h>
+
+int
+func(int *x) ~ [
+ pre: .clump x;
+]{
+
+}
+
+int
+main()
+{
+ int *p;
+ p = 5;
+
+ func(p); /* ERROR: spec required lvalue */
+}
A 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 -0
@@ 0,0 1,1 @@
+6-preconditions/103-FAIL-need-clump-lval-assigned-ptr.x:16:9: cannot exec statement: parameter 'x' must be lvalue
A tests/7-use-after-free/000-read-and-write.x => tests/7-use-after-free/000-read-and-write.x +26 -0
@@ 0,0 1,26 @@
+#include <stdlib.h>
+
+int *
+read_and_write_definite() ~ [ .alloc result; *result = 1; ]
+{
+ int *p;
+ p = malloc(1);
+ *p = 1;
+ return p;
+}
+
+int
+main()
+{
+ int *q;
+ int i;
+
+ q = read_and_write_definite();
+ i = *q; /* valid rvalue deref */
+ ~ [ *q == 1; ];
+ ~ [ i == 1; ]; /* i has definite value */
+ *q = 2; /* valid lvalue deref */
+ ~ [ *q == 2; ];
+
+ free(q);
+}
A tests/7-use-after-free/001-read-and-write-arbitrary.x => tests/7-use-after-free/001-read-and-write-arbitrary.x +28 -0
@@ 0,0 1,28 @@
+#include <stdlib.h>
+
+int *
+read_and_write_arbitrary() ~ [ .alloc result; *result = $; ]
+{
+ int *p;
+ p = malloc(1);
+ *p = 1;
+ return p;
+}
+
+int
+main()
+{
+ int *r;
+ int j;
+
+ r = read_and_write_arbitrary();
+ j = *r; /* valid rvalue deref */
+ // ~ [ *r == $; ];
+ // ~ [ j == $; ]; /* j has arbitrary value */
+ *r = 2; /* valid lvalue deref */
+ ~ [ *r == 2; ];
+
+ free(r);
+
+ return 0;
+}
A tests/7-use-after-free/002-pass-in-lvalue.x => tests/7-use-after-free/002-pass-in-lvalue.x +19 -0
@@ 0,0 1,19 @@
+void
+modify(int *q) ~ [
+ pre: {
+ .clump q;
+ }
+ *q = 2;
+] {
+ *q = 2;
+}
+
+int *
+main()
+{
+ int p;
+ p = 1;
+ ~ [ p == 1; ];
+ modify(&p);
+ ~ [ p == 2; ];
+}
A tests/7-use-after-free/003-pass-in-rvalue.x => tests/7-use-after-free/003-pass-in-rvalue.x +19 -0
@@ 0,0 1,19 @@
+int
+assign(int *q) ~ [
+ pre: {
+ .clump q; /* no side effect */
+ *q = $;
+ }
+] {
+ int p;
+ p = *q;
+}
+
+int *
+main()
+{
+ int p;
+ p = 1;
+ assign(&p);
+ ~ [ p == 1; ];
+}
A tests/7-use-after-free/004-mix-multiple-levels.x => tests/7-use-after-free/004-mix-multiple-levels.x +46 -0
@@ 0,0 1,46 @@
+int
+snapshot_and_change(int *arg) ~ [
+ pre: {
+ .clump arg;
+ *arg = $;
+ }
+ result = *arg;
+ *arg = 3;
+] {
+ int j;
+ j = *arg;
+ *arg = 3;
+ return j;
+}
+
+void
+modify(int *p, int *q) ~ [
+ int i;
+ pre: {
+ .clump p;
+ *p = $;
+ .clump q;
+ };
+ *q = 2;
+ *p = 3;
+ i = *p;
+] {
+ int i;
+ i = 0;
+ i = snapshot_and_change(p);
+ ~ [ *p == 3; ];
+
+ *q = 2;
+}
+
+int *
+main()
+{
+ int p;
+ int q;
+ p = 9;
+ ~ [ p == 9; ];
+ modify(&p, &q);
+ ~ [ p == 3; ];
+ ~ [ q == 2; ];
+}
A tests/7-use-after-free/005-conditions.x => tests/7-use-after-free/005-conditions.x +39 -0
@@ 0,0 1,39 @@
+void
+modify0(int *q, int x) ~ [
+ pre: .clump q;
+ if (x) {
+ *q = 1;
+ }
+] {
+ if (x) {
+ *q = 1;
+ }
+}
+
+void
+modify1(int *q, int x) ~ [
+ if (x) {
+ pre: .clump q;
+ *q = 2;
+ }
+] {
+ if (x) {
+ *q = 2;
+ }
+}
+
+int *
+main()
+{
+ int p;
+ p = 0;
+ ~ [ p == 0; ];
+ modify0(&p, 0);
+ ~ [ p == 0; ];
+ modify0(&p, 1);
+ ~ [ p == 1; ];
+ modify1(&p, 0);
+ ~ [ p == 1; ];
+ modify1(&p, 1);
+ ~ [ p == 2; ];
+}
A tests/7-use-after-free/100-FAIL-lvalue-use-after-free.x => tests/7-use-after-free/100-FAIL-lvalue-use-after-free.x +12 -0
@@ 0,0 1,12 @@
+#include <stdlib.h>
+
+void
+func()
+{
+ int *p;
+
+ p = malloc(1);
+ free(p);
+
+ *p = 1; /* ERROR: undefined indirection (lvalue) */
+}
A 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 -0
@@ 0,0 1,1 @@
+7-use-after-free/100-FAIL-lvalue-use-after-free.x:11:8: cannot exec statement: undefined indirection (lvalue)
A tests/7-use-after-free/101-FAIL-rvalue-use-after-free.x => tests/7-use-after-free/101-FAIL-rvalue-use-after-free.x +13 -0
@@ 0,0 1,13 @@
+#include <stdlib.h>
+
+void
+func()
+{
+ int *p;
+ int q;
+
+ p = malloc(1);
+ free(p);
+
+ q = *p; /* ERROR: undefined indirection (rvalue) */
+}
A 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 -0
@@ 0,0 1,1 @@
+7-use-after-free/101-FAIL-rvalue-use-after-free.x:12:8: cannot exec statement: undefined indirection (rvalue)
A tests/7-use-after-free/110-FAIL-freed-ptr-dangling-return.x =>