Hey guys,
I'm trying to express the condition gathered from a conditional jump. My program instrumentation is performed at the byte level so in the case of a conditional based on a word or dword I need to concatenate the constituent bytes into a new variable before making the comparison. It is this concatenation that is giving trouble. The following is a quick test I just wrote to see how the concat operator worked.
I am aiming to make the formula unsatisfiable by constraining i0 and i1 to 0 and then expressing c1 as the concatenation of these variables; I then ask the solver if it is possible for c1 to equal 22. (I'm using the latest public version of Z3 for Windows)
(benchmark test
:status unknown
:logic QF_BV
:extrafuns ((i0 BitVec)(i1 BitVec)(c1 BitVec[16]))
:assumption (and (= i0 bv0)(= i1 bv0)(concat i0 i1 c1))
:formula ((= c1 bv22[16])) )
Z3 tells me this is satisfiable, and the model it returns is as follows:
partitions:
*2 (i1 i0) -> 0:bv8
*3 (c1) -> 22:bv16
Which seems to indicate it isn't considering the effect of restricting i0/i1 to 0 when assigning a value to c1. Is there something obviously wrong with the SMT-LIB input I'm using? Or am I misinterpreting how to use 'concat'?
Thanks for your time, Sean
Yes you are miss-interpreting how to use concat.Concat is a function not a relation. It returns a bit-vector.
Below is the correct specification.
(benchmark test :status unknown :logic QF_BV :extrafuns ((i0 BitVec )(i1 BitVec )(c1 BitVec[16])) :assumption (and (= i0 bv0 )(= i1 bv0 ) (= (concat i0 i1) c1)) :formula ((= c1 bv22[16])) )
Z3 v1.3 does not type check specifications unless you specify TYPE_CHECK=true as part of the command-line arguments.We will include type checking by default in our next releases.