1
$\begingroup$

I'm currently working on a static analysis work in which I need to check whether a given formula is met or not. I hope the following example clarifies my requirement.

Suppose we have a list of three-addressed expressions whose operators are simple arithmetic and bit-wise operators (such as add, sub, and, xor). Each expression could have constant literals or variable symbols. For example, consider the following list:

a = b + 1
c = d
c = c xor d
a = a + c
a = a + 4

What I need is that to see whether a given formula is established or not. For example, the following formulas:

a == b + <some_constants>   # In this example: Yes, because a == b + 5
a == d + <some_constants>   # In this example: No

So can a SMT solver (Z3 for example) help me in this situation? If not, could you please point me out if there is a suitable tool applicable for this requirement?

$\endgroup$
  • 1
    $\begingroup$ Did you have a look at Z3's documentation? It seems to me that this application is covered in the tutorial $\endgroup$ – adrianN May 23 '16 at 11:51
  • $\begingroup$ @adrianN Yes I looked, but my problem is a bit different than those examples. In my problem the formula to be checked isn't deterministic (we don't know what <some_constants> is. But we do know that it's a constant number). Additionally, if the formula for all possible variables (i.e. a, b, etc.) is established, I need to know what that unknown constant is. So, Does Z3 support this kind of application? $\endgroup$ – Hi I'm Frogatto May 23 '16 at 12:12
2
$\begingroup$

Yes, absolutely. SMT solvers are actually quite well suited for such problems. Unfortunately, the input language to them (SMTLib) is rather machine-oriented, but there are many "high-level" interfaces to many solvers, Z3 itself providing a Python interface, for instance.

For this problem, I'll use the Haskell SBV library, which translates your constraints more or less directly to Z3. Note that I've put the equations into SSA form (single-static assignment), as is usual in such analyses. The whole problem is:

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV

q = do k1 <- sInt32 "k1"
       k2 <- sInt32 "k2"

       a0 :: SInt32 <- forall "a"
       b0 :: SInt32 <- forall "b"
       c0 :: SInt32 <- forall "c"
       d0 :: SInt32 <- forall "d"

       let a1 = b0 + 1
           c1 = d0
           c2 = c1 `xor` d0
           a2 = a1 + c2
           a3 = a2 + 4

       constrain $ a3 .== b0 + k1
       constrain $ a3 .== d0 + k2

Also note that I (arbitrarily) picked 32-bit integers, though you can go with other types as well as needed. As stated, we get:

*Main> sat q
Unsatisfiable

Meaning that there's no such k1/k2 that satisfy your equations, as you yourself observed. If we let go of the second constraint (by commenting out the very last line in the definition of q), we get:

*Main> sat q
Satisfiable. Model:
  k1 = 5 :: Int32
  k2 = 0 :: Int32

Here's the solver picked the arbitrary value of 0 for k2 since there are no constraints on it; but k1 became 5 as you predicted.

Long story short, yes; this sort of reasoning is absolutely possible with SMT-solvers; and there are high-level language bindings that let you express them rather concisely.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.