英文:
How can I translate z3::expr(bv_val) into a bit representation of a number?
问题
static inline bool calculate_parity(z3::context& z3c, z3::expr** even_bits, z3::expr** dst)
{
z3::expr num = z3c.bv_val(42, 64); // 42 in 64-bit binary representation
for (int i = 63; i >= 0; i--) {
z3::expr bit = num.extract(i, i);
std::cout << bit << " ";
}
std::cout << std::endl;
return true;
}
英文:
I am trying to translate Z3::expr into a bit representation of a number in order to find out how many bits 1 the number contains and if the number of bits 1 is even, then I raise the flag.
I wrote the implementation below, but it doesn't work the way I need.
static inline bool calculate_parity(z3::context& z3c, z3::expr** even_bits, z3::expr** dst)
{
z3::expr num = z3c.bv_val(42, 64); // 42 in 64-bit binary representation
for (int i = 31; i >= 0; i--) {
z3::expr bit = num.extract(i, i);
std::cout << bit << " ";
}
std::cout << std::endl;
return true;
}
The implementation of the task can be compared with raising the pf flag in the x86_64 assembler.
Something like this:
static inline void translate_add(z3::context& z3c, x8664_ctx& old_state, x8664_ctx& new_state, ZydisDisassembledInstruction ins)
{
if (ins.info.operand_count_visible == 2)
{
auto& op1 = ins.operands[0];
auto& op2 = ins.operands[1];
z3::expr e1 = **Z3SystemTranslateFuncs::get_val_expr(z3c, old_state, op1);
z3::expr e2 = **Z3SystemTranslateFuncs::get_val_expr(z3c, old_state, op2);
z3::expr** dst = Z3SystemTranslateFuncs::get_val_expr(z3c, new_state, op1);
*dst = new z3::expr(z3c, e1 + e2);
new_state.zf = new z3::expr(**dst == 0);
new_state.of = new z3::expr(((e1 ^ e2) & 0x7FFFFFFF) == 0 && ((e1 ^ **dst) & 0x7FFFFFFF) != 0);
new_state.cf = new z3::expr((e1 + e2).simplify() < e1.simplify());
***new_state.pf = new z3::expr(z3c.bool_val(Z3SystemTranslateFuncs::calculate_parity(z3c, dst, dst)));***
new_state.sf = new z3::expr(**dst < 0);
z3::expr bit3 = (e1 + e2).extract(3, 3);
z3::expr bit4 = (e1 + e2).extract(4, 4);
new_state.af = new z3::expr((bit3 ^ bit4) != 0);
}
else
throw std::exception("bad operand count in translate_add function");
}
答案1
得分: 1
以下是翻译的代码部分：
// 计算奇偶校验的基本 C++ 函数如下：
expr parity64(context &ctx, expr x) {
expr res = ctx.bv_val(0, 1);
for (int i = 0; i < 64; i++)
{
res = res ^ x.extract(i, i);
}
return res;
}
请注意，我只提供了代码的翻译部分，没有包括其他内容。
英文:
The basic c++ function to compute the parity would be:
// Check if #of 1's is even. This can be achieved
// by xor'ing all the bits, if even 1's then result will be 0
// otherwise it'll be 1
expr parity64(context &ctx, expr x) {
expr res = ctx.bv_val(0, 1);
for (int i = 0; i < 64; i++)
{
res = res ^ x.extract(i, i);
}
return res;
}
Looks like you're trying to do this in the context of a larger framework. You might be able to translate the above to that system, or you should tag your question with appropriate tags so people who are familiar with that system can answer your question. (If there are any on stack-overflow, that is!)
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论