z3: how to convert a boolean sort into a bit vector sort

Question

I am doing symbolic interpretation of x86 instructions. For the cmp instruction for instance, the sign of the comparison and whether operands are equal or not is stored in two bits of the eflags register.

Here is my code:

/* s1,s2 are source operands of sort bit-vector
 *       of 32 bits (defined somewhere else)
 * ctx is the context (defined somewhere else)
 * eflags is of sort bit-vector of 32 bits (initialized somewhere else)
 */

#define ZF_INDEX 6

Z3_ast ZF,OF,CF;              /* eflags bits */
ZF = Z3_mk_eq(ctx,s1,s2);
Z3_ast zf_mask = Z3_mk_rotate_left(ctx, ZF_INDEX ,Z3_mk_zero_ext(ctx,31,ZF));
eflags = Z3_mk_bvand(ctx,eflags, zf_mask);

The problem is that I don't find any function in z3 API to convert an (assumed) boolean sort (ZF in my example) into a bit-vector (of any length).

I have thought about creating a function with an ite statement on ZF which would return a bit-vector, but I would like to know the traditional way of doing this.

Thanks,

Heyji.

Answer 1

The ite approach you described is the traditional way.