~lbnz/xr0

cde35928f53188eb30503735f2b40abf06c62e58 — Xr0 Team 11 months ago d3c9271 chore/verify-no-switch
drop binary op
M include/ast.h => include/ast.h +23 -15
@@ 75,22 75,29 @@ ast_expr_unary_isdereference(struct ast_expr *);
struct ast_expr *
ast_expr_unary_operand(struct ast_expr *);

enum ast_binary_operator {
	BINARY_OP_EQ	= 1 << 0,
	BINARY_OP_NE	= 1 << 1,
struct ast_expr *
ast_expr_eq_create(struct ast_expr *, struct ast_expr *);

	BINARY_OP_LT	= 1 << 2,
	BINARY_OP_GT	= 1 << 3,
	BINARY_OP_LE	= 1 << 4,
	BINARY_OP_GE	= 1 << 5,
struct ast_expr *
ast_expr_ne_create(struct ast_expr *, struct ast_expr *);

	BINARY_OP_ADDITION	= 1 << 6,
	BINARY_OP_SUBTRACTION	= 1 << 7,
};
struct ast_expr *
ast_expr_lt_create(struct ast_expr *, struct ast_expr *);

struct ast_expr *
ast_expr_gt_create(struct ast_expr *, struct ast_expr *);

struct ast_expr *
ast_expr_le_create(struct ast_expr *, struct ast_expr *);

struct ast_expr *
ast_expr_binary_create(struct ast_expr *e1, enum ast_binary_operator,
		struct ast_expr *e2);
ast_expr_ge_create(struct ast_expr *, struct ast_expr *);

struct ast_expr *
ast_expr_sum_create(struct ast_expr *, struct ast_expr *);

struct ast_expr *
ast_expr_difference_create(struct ast_expr *, struct ast_expr *);

struct ast_expr *
ast_expr_binary_e1(struct ast_expr *);


@@ 98,9 105,6 @@ ast_expr_binary_e1(struct ast_expr *);
struct ast_expr *
ast_expr_binary_e2(struct ast_expr *);

enum ast_binary_operator
ast_expr_binary_op(struct ast_expr *);

struct ast_expr *
ast_expr_assignment_create(struct ast_expr *root, struct ast_expr *value);



@@ 148,6 152,8 @@ ast_expr_rangedecide(struct ast_expr *, struct ast_expr *lw,
struct error *
ast_expr_exec(struct ast_expr *, struct state *);

struct lvalue;

struct lvalue *
ast_expr_lvalue(struct ast_expr *, struct state *);



@@ 498,6 504,8 @@ struct error;
struct error *
ast_function_verify(struct ast_function *, struct externals *);

struct result;

struct result *
ast_function_absexec(struct ast_function *, struct state *state);


M include/value.h => include/value.h +1 -1
@@ 84,7 84,7 @@ value_references(struct value *, struct location *, struct state *);
enum ast_binary_operator;

bool
value_compare(struct value *v1, enum ast_binary_operator, struct value *v2);
value_equal(struct value *v1, struct value *v2);

enum number_value_type {
	NUMBER_VALUE_CONSTANT,

M src/ast/ast.c => src/ast/ast.c +0 -2
@@ 137,5 137,3 @@ lvalue_object(struct lvalue *l)
{
	return l->obj;
}



M src/ast/expr/expr.c => src/ast/expr/expr.c +48 -0
@@ 371,6 371,54 @@ ast_expr_binary_create(struct ast_expr *e1, enum ast_binary_operator op,
}

struct ast_expr *
ast_expr_eq_create(struct ast_expr *e1, struct ast_expr *e2)
{
	return ast_expr_binary_create(e1, BINARY_OP_EQ, e2);
}

struct ast_expr *
ast_expr_ne_create(struct ast_expr *e1, struct ast_expr *e2)
{
	return ast_expr_binary_create(e1, BINARY_OP_NE, e2);
}

struct ast_expr *
ast_expr_lt_create(struct ast_expr *e1, struct ast_expr *e2)
{
	return ast_expr_binary_create(e1, BINARY_OP_LT, e2);
}

struct ast_expr *
ast_expr_gt_create(struct ast_expr *e1, struct ast_expr *e2)
{
	return ast_expr_binary_create(e1, BINARY_OP_GT, e2);
}

struct ast_expr *
ast_expr_le_create(struct ast_expr *e1, struct ast_expr *e2)
{
	return ast_expr_binary_create(e1, BINARY_OP_LE, e2);
}

struct ast_expr *
ast_expr_ge_create(struct ast_expr *e1, struct ast_expr *e2)
{
	return ast_expr_binary_create(e1, BINARY_OP_GE, e2);
}

struct ast_expr *
ast_expr_sum_create(struct ast_expr *e1, struct ast_expr *e2)
{
	return ast_expr_binary_create(e1, BINARY_OP_ADDITION, e2);
}

struct ast_expr *
ast_expr_difference_create(struct ast_expr *e1, struct ast_expr *e2)
{
	return ast_expr_binary_create(e1, BINARY_OP_SUBTRACTION, e2);
}

struct ast_expr *
ast_expr_binary_e1(struct ast_expr *expr)
{
	assert(expr->kind == EXPR_BINARY);

M src/ast/expr/expr.h => src/ast/expr/expr.h +16 -1
@@ 42,7 42,18 @@ struct ast_expr {
			UNARY_OP_BANG			= 1 << 5,
		} unary_op;
		struct {
			enum ast_binary_operator op;
			enum ast_binary_operator {
				BINARY_OP_EQ	= 1 << 0,
				BINARY_OP_NE	= 1 << 1,

				BINARY_OP_LT	= 1 << 2,
				BINARY_OP_GT	= 1 << 3,
				BINARY_OP_LE	= 1 << 4,
				BINARY_OP_GE	= 1 << 5,

				BINARY_OP_ADDITION	= 1 << 6,
				BINARY_OP_SUBTRACTION	= 1 << 7,
			} op;
			struct ast_expr *e1, *e2;
		} binary;
		struct ast_expr *assignment_value;


@@ 52,4 63,8 @@ struct ast_expr {
enum ast_expr_kind
ast_expr_kind(struct ast_expr *);

struct ast_expr *
ast_expr_binary_create(struct ast_expr *e1, enum ast_binary_operator,
		struct ast_expr *e2);

#endif

M src/ast/expr/verify.c => src/ast/expr/verify.c +16 -0
@@ 231,6 231,9 @@ struct result *
ast_expr_eval(struct ast_expr *expr, struct state *state);

static bool
value_compare(struct value *, enum ast_binary_operator, struct value *);

static bool
expr_binary_decide(struct ast_expr *expr, struct state *state)
{
	struct result *root = ast_expr_eval(ast_expr_binary_e1(expr), state),


@@ 245,6 248,19 @@ expr_binary_decide(struct ast_expr *expr, struct state *state)
	);
}

static bool
value_compare(struct value *v1, enum ast_binary_operator op, struct value *v2)
{
	switch (op) {
	case BINARY_OP_EQ:
		return value_equal(v1, v2);
	case BINARY_OP_NE:
		return !value_compare(v1, BINARY_OP_EQ, v2);
	default:
		assert(false);
	}
}

/* ast_expr_eval */

static struct result *

M src/ast/stmt/verify.c => src/ast/stmt/verify.c +0 -1
@@ 242,7 242,6 @@ stmt_jump_exec(struct ast_stmt *stmt, struct state *state)
}



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


M src/object/object.c => src/object/object.c +24 -26
@@ 208,9 208,8 @@ object_lower(struct object *obj)
struct ast_expr *
object_upper(struct object *obj)
{
	return ast_expr_binary_create(
	return ast_expr_sum_create(
		ast_expr_copy(obj->offset),
		BINARY_OP_ADDITION,
		object_size(obj)
	);
}


@@ 222,11 221,11 @@ object_contains(struct object *obj, struct ast_expr *offset, struct state *s)
			*up = object_upper(obj),
			*of = offset;

	struct ast_expr *e1 = ast_expr_binary_create(
		ast_expr_copy(lw), BINARY_OP_LE, ast_expr_copy(of)
	struct ast_expr *e1 = ast_expr_le_create(
		ast_expr_copy(lw), ast_expr_copy(of)
	);
	struct ast_expr *e2 = ast_expr_binary_create(
		ast_expr_copy(of), BINARY_OP_LT, ast_expr_copy(up)
	struct ast_expr *e2 = ast_expr_lt_create(
		ast_expr_copy(of), ast_expr_copy(up)
	);
	ast_expr_destroy(up);
	


@@ 253,12 252,12 @@ object_contains_upperincl(struct object *obj, struct ast_expr *offset,

	return
		/* lw ≤ of */
		state_eval(s, ast_expr_binary_create(lw, BINARY_OP_LE, of))
		state_eval(s, ast_expr_le_create(lw, of))

		&&

		/* of ≤ up */
		state_eval(s, ast_expr_binary_create(of, BINARY_OP_LE, up));
		state_eval(s, ast_expr_le_create(of, up));
}

bool


@@ 267,7 266,7 @@ object_isempty(struct object *obj, struct state *s)
	struct ast_expr *lw = obj->offset,
			*up = object_upper(obj);

	return state_eval(s, ast_expr_binary_create(lw, BINARY_OP_EQ, up));
	return state_eval(s, ast_expr_eq_create(lw, up));
}

bool


@@ 276,7 275,7 @@ object_contig_precedes(struct object *before, struct object *after,
{
	struct ast_expr *lw = object_upper(before),
			*up = after->offset;
	return state_eval(s, ast_expr_binary_create(lw, BINARY_OP_EQ, up));
	return state_eval(s, ast_expr_eq_create(lw, up));
}

bool


@@ 285,12 284,12 @@ object_issingular(struct object *obj, struct state *s)
	struct ast_expr *lw = obj->offset,
			*up = object_upper(obj);

	struct ast_expr *lw_succ = ast_expr_binary_create(
		lw, BINARY_OP_ADDITION, ast_expr_constant_create(1)
	struct ast_expr *lw_succ = ast_expr_sum_create(
		lw, ast_expr_constant_create(1)
	);

	/* lw + 1 == up */
	return state_eval(s, ast_expr_binary_create(lw_succ, BINARY_OP_EQ, up));
	return state_eval(s, ast_expr_eq_create(lw_succ, up));
}

struct object *


@@ 299,14 298,14 @@ object_upto(struct object *obj, struct ast_expr *excl_up, struct state *s)
	struct ast_expr *lw = obj->offset,
			*up = object_upper(obj);

	struct ast_expr *prop0 = ast_expr_binary_create(
		ast_expr_copy(lw), BINARY_OP_LE, ast_expr_copy(excl_up)
	struct ast_expr *prop0 = ast_expr_le_create(
		ast_expr_copy(lw), ast_expr_copy(excl_up)
	);
	struct ast_expr *prop1 = ast_expr_binary_create(
		ast_expr_copy(lw), BINARY_OP_EQ, ast_expr_copy(excl_up)
	struct ast_expr *prop1 = ast_expr_eq_create(
		ast_expr_copy(lw), ast_expr_copy(excl_up)
	);
	struct ast_expr *prop2 = ast_expr_binary_create(
		ast_expr_copy(up), BINARY_OP_EQ, ast_expr_copy(excl_up)
	struct ast_expr *prop2 = ast_expr_eq_create(
		ast_expr_copy(up), ast_expr_copy(excl_up)
	);

	bool e0 = state_eval(s, prop0),


@@ 333,7 332,7 @@ object_upto(struct object *obj, struct ast_expr *excl_up, struct state *s)
	return object_range_create(
		ast_expr_copy(obj->offset),
		range_create(
			ast_expr_binary_create(excl_up, BINARY_OP_SUBTRACTION, lw),
			ast_expr_difference_create(excl_up, lw),
			value_as_ptr(state_alloc(s))
		)
	);


@@ 345,11 344,11 @@ object_from(struct object *obj, struct ast_expr *incl_lw, struct state *s)
	struct ast_expr *lw = obj->offset,
			*up = object_upper(obj);

	struct ast_expr *prop0 = ast_expr_binary_create(
		ast_expr_copy(incl_lw), BINARY_OP_GE, ast_expr_copy(up)
	struct ast_expr *prop0 = ast_expr_ge_create(
		ast_expr_copy(incl_lw), ast_expr_copy(up)
	);
	struct ast_expr *prop1 = ast_expr_binary_create(
		ast_expr_copy(incl_lw), BINARY_OP_EQ, ast_expr_copy(lw)
	struct ast_expr *prop1 = ast_expr_eq_create(
		ast_expr_copy(incl_lw), ast_expr_copy(lw)
	);

	bool e0 = state_eval(s, prop0),


@@ 374,9 373,8 @@ object_from(struct object *obj, struct ast_expr *incl_lw, struct state *s)
	return object_range_create(
		ast_expr_copy(incl_lw),
		range_create(
			ast_expr_binary_create(
			ast_expr_difference_create(
				up,
				BINARY_OP_SUBTRACTION,
				ast_expr_copy(incl_lw)
			),
			value_as_ptr(state_alloc(s))

M src/state/block.c => src/state/block.c +4 -8
@@ 85,9 85,8 @@ block_observe(struct block *b, struct ast_expr *offset, struct state *s,

	/* range around observand at offset */
	struct ast_expr *lw = ast_expr_copy(offset);
	struct ast_expr *up = ast_expr_binary_create(
	struct ast_expr *up = ast_expr_sum_create(
		ast_expr_copy(offset),
		BINARY_OP_ADDITION,
		ast_expr_constant_create(1)
	);
 


@@ 141,9 140,8 @@ block_range_alloc(struct block *b, struct ast_expr *lw, struct ast_expr *up,
		object_range_create(
			ast_expr_copy(lw),
			range_create(
				ast_expr_binary_create(
				ast_expr_difference_create(
					ast_expr_copy(up),
					BINARY_OP_SUBTRACTION,
					ast_expr_copy(lw)
				),
				heap_newblock(heap)


@@ 204,10 202,8 @@ hack_first_object_is_exactly_bounds(struct block *b, struct ast_expr *lw,
		return false;
	}

	struct ast_expr *same_lw =
		ast_expr_binary_create(lw, BINARY_OP_EQ, object_lower(obj)),
			*same_up =
		ast_expr_binary_create(up, BINARY_OP_EQ, object_upper(obj));
	struct ast_expr *same_lw = ast_expr_eq_create(lw, object_lower(obj)),
			*same_up = ast_expr_eq_create(up, object_upper(obj));

	return state_eval(s, same_lw) && state_eval(s, same_up);
}

M src/value/value.c => src/value/value.c +0 -16
@@ 440,22 440,6 @@ struct_references(struct value *v, struct location *loc, struct state *s)
}

bool
value_equal(struct value *v1, struct value *v2);

bool
value_compare(struct value *v1, enum ast_binary_operator op, struct value *v2)
{
	switch (op) {
	case BINARY_OP_EQ:
		return value_equal(v1, v2);
	case BINARY_OP_NE:
		return !value_compare(v1, BINARY_OP_EQ, v2);
	default:
		assert(false);
	}
}

bool
number_equal(struct number *n1, struct number *n2);

bool