c++ - Z3 solver context error when expressions are loaded out of memory - Stack Overflow

admin管理员组

文章数量:1026989

Does anyone know why I can't just load a pointer to a z3 expression into my memory and then query it again later? When I do I get context errors and it says not to compare these expressions. When i switch *zero with just z it works fine.

i am using clang version 15.0.7 as my compliler.

llvm::DenseMap<llvm::Value*, z3::expr*> map_end_address;
z3::expr x = context->bv_const("x", 32);
    z3::expr y = context->bv_const("y", 32);
    z3::expr z = context->bv_const("z", 32);
    map_end_address->insert({llvm::dyn_cast<llvm::Value>(mallocCallInstruction), &z});
    z3::expr *zero = map_end_address->lookup(llvm::dyn_cast<llvm::Value>(mallocCallInstruction));

    solver->add(x == 4);
    solver->add(y == 2);

    solver->add(*zero == z3::shl(x, y));

This is solved by using shared_pointers, but I really wouldn't understand why these resources would already be released if I just write away the pointer to this object to memory.

llvm::DenseMap<llvm::Value*, std::shared_ptr<z3::expr>> map_end_address;

    z3::expr x = context->bv_const("x", 32);
    z3::expr y = context->bv_const("y", 32);
    std::shared_ptr<z3::expr> z = std::make_shared<z3::expr>(context->bv_const("z", 32));

    map_end_address.insert({llvm::dyn_cast<llvm::Value>(mallocCallInstruction), z});
    z3::expr *zero = map_end_address.lookup(llvm::dyn_cast<llvm::Value>(mallocCallInstruction)).get();

    solver->add(x == 4);
    solver->add(y == 2);

    solver->add(*zero == z3::shl(x, y));

Does anyone know why I can't just load a pointer to a z3 expression into my memory and then query it again later? When I do I get context errors and it says not to compare these expressions. When i switch *zero with just z it works fine.

i am using clang version 15.0.7 as my compliler.

llvm::DenseMap<llvm::Value*, z3::expr*> map_end_address;
z3::expr x = context->bv_const("x", 32);
    z3::expr y = context->bv_const("y", 32);
    z3::expr z = context->bv_const("z", 32);
    map_end_address->insert({llvm::dyn_cast<llvm::Value>(mallocCallInstruction), &z});
    z3::expr *zero = map_end_address->lookup(llvm::dyn_cast<llvm::Value>(mallocCallInstruction));

    solver->add(x == 4);
    solver->add(y == 2);

    solver->add(*zero == z3::shl(x, y));

This is solved by using shared_pointers, but I really wouldn't understand why these resources would already be released if I just write away the pointer to this object to memory.

llvm::DenseMap<llvm::Value*, std::shared_ptr<z3::expr>> map_end_address;

    z3::expr x = context->bv_const("x", 32);
    z3::expr y = context->bv_const("y", 32);
    std::shared_ptr<z3::expr> z = std::make_shared<z3::expr>(context->bv_const("z", 32));

    map_end_address.insert({llvm::dyn_cast<llvm::Value>(mallocCallInstruction), z});
    z3::expr *zero = map_end_address.lookup(llvm::dyn_cast<llvm::Value>(mallocCallInstruction)).get();

    solver->add(x == 4);
    solver->add(y == 2);

    solver->add(*zero == z3::shl(x, y));

本文标签： cZ3 solver context error when expressions are loaded out of memoryStack Overflow