theory_init.c File Reference

#include <rz_il/rz_il_opcodes.h>
#include <rz_il/rz_il_vm.h>

Go to the source code of this file.

Functions
void *	rz_il_handler_ite (RzILVM *vm, RzILOpPure *op, RzILTypePure *type)
void *	rz_il_handler_var (RzILVM *vm, RzILOpPure *op, RzILTypePure *type)
void *	rz_il_handler_let (RzILVM *vm, RzILOpPure *op, RzILTypePure *type)
void *	rz_il_handler_pure_unimplemented (RzILVM *vm, RzILOpPure *op, RzILTypePure *type)
bool	rz_il_handler_effect_unimplemented (RzILVM *vm, RzILOpEffect *op)

Function Documentation

rz_il_handler_effect_unimplemented()

bool rz_il_handler_effect_unimplemented	(	RzILVM *	vm,
		RzILOpEffect *	op
	)

Definition at line 76 of file theory_init.c.

                                                                      {
    rz_return_val_if_fail(vm && op, NULL);
    RZ_LOG_ERROR("RzIL: unimplemented op handler (%d).\n", (int)op->code);
    return false;
}

References op::code, NULL, RZ_LOG_ERROR, and rz_return_val_if_fail.

rz_il_handler_ite()

void* rz_il_handler_ite	(	RzILVM *	vm,
		RzILOpPure *	op,
		RzILTypePure *	type
	)

Definition at line 7 of file theory_init.c.

                                                                        {
    rz_return_val_if_fail(vm && op && type, NULL);
 
    RzILOpArgsIte *op_ite = &op->op.ite;
 
    RzILBool *condition = rz_il_evaluate_bool(vm, op_ite->condition);
    if (!condition) {
        return NULL;
    }
    RzILVal *ret;
    if (condition->b) {
        ret = rz_il_evaluate_pure(vm, op_ite->x, type); // true branch
    } else {
        ret = rz_il_evaluate_pure(vm, op_ite->y, type); // false branch
    }
    rz_il_bool_free(condition);
    return ret;
}

References rz_il_bool_t::b, rz_il_op_args_ite_t::condition, NULL, rz_il_bool_free(), rz_il_evaluate_bool(), rz_il_evaluate_pure(), rz_return_val_if_fail, type, rz_il_op_args_ite_t::x, and rz_il_op_args_ite_t::y.

rz_il_handler_let()

void* rz_il_handler_let	(	RzILVM *	vm,
		RzILOpPure *	op,
		RzILTypePure *	type
	)

Definition at line 57 of file theory_init.c.

                                                                        {
    rz_return_val_if_fail(vm && op && type, NULL);
    RzILOpArgsLet *args = &op->op.let;
    RzILVal *v = rz_il_evaluate_val(vm, args->exp);
    if (!v) {
        return NULL;
    }
    RzILLocalPurePrev prev = rz_il_vm_push_local_pure_var(vm, args->name, v);
    void *r = rz_il_evaluate_pure(vm, args->body, type);
    rz_il_vm_pop_local_pure_var(vm, args->name, prev);
    return r;
}

References args, NULL, r, rz_il_evaluate_pure(), rz_il_evaluate_val(), rz_il_vm_pop_local_pure_var(), rz_il_vm_push_local_pure_var(), rz_return_val_if_fail, type, and v.

rz_il_handler_pure_unimplemented()

void* rz_il_handler_pure_unimplemented	(	RzILVM *	vm,
		RzILOpPure *	op,
		RzILTypePure *	type
	)

Definition at line 70 of file theory_init.c.

                                                                                       {
    rz_return_val_if_fail(vm && op && type, NULL);
    RZ_LOG_ERROR("RzIL: unimplemented op handler (%d).\n", (int)op->code);
    return NULL;
}

References op::code, NULL, RZ_LOG_ERROR, rz_return_val_if_fail, and type.

rz_il_handler_var()

void* rz_il_handler_var	(	RzILVM *	vm,
		RzILOpPure *	op,
		RzILTypePure *	type
	)

Definition at line 26 of file theory_init.c.

                                                                        {
    rz_return_val_if_fail(vm && op && type, NULL);
 
    RzILOpArgsVar *var_op = &op->op.var;
    RzILVal *val = rz_il_vm_get_var_value(vm, var_op->kind, var_op->v);
    if (!val) {
        RZ_LOG_ERROR("RzIL: reading value of variable \"%s\" of kind %s failed.\n",
            var_op->v, rz_il_var_kind_name(var_op->kind));
        return NULL;
    }
 
    if (var_op->kind == RZ_IL_VAR_KIND_GLOBAL) {
        rz_il_vm_event_add(vm, rz_il_event_var_read_new(var_op->v, val));
    }
 
    void *ret = NULL;
    switch (val->type) {
    case RZ_IL_TYPE_PURE_BOOL:
        *type = RZ_IL_TYPE_PURE_BOOL;
        ret = rz_il_bool_new(val->data.b->b);
        break;
    case RZ_IL_TYPE_PURE_BITVECTOR:
        *type = RZ_IL_TYPE_PURE_BITVECTOR;
        ret = rz_bv_dup(val->data.bv);
        break;
    default:
        break;
    }
    return ret;
}

References rz_il_op_args_var_t::kind, NULL, rz_bv_dup(), rz_il_bool_new(), rz_il_event_var_read_new(), RZ_IL_TYPE_PURE_BITVECTOR, RZ_IL_TYPE_PURE_BOOL, RZ_IL_VAR_KIND_GLOBAL, rz_il_var_kind_name(), rz_il_vm_event_add(), rz_il_vm_get_var_value(), RZ_LOG_ERROR, rz_return_val_if_fail, type, rz_il_op_args_var_t::v, and val.