2
$\begingroup$

I'm doing some work with static analysis and need to represent local variables as SMT formulas. In general this is fairly straight forward, depending on the domain of the static analysis. However, my question lies when needing to represent impossible or infeasible values, e.g., divide by zero paths from the static analysis under an integer domain. This is often referred to as the bottom element, ⊥.

I'm struggling to develop a formula which can represent these "impossible" (integer) values. Is there a way to do this?

I've been thinking along the lines as an impossible inequality, but I've been unsuccessful thus far. Similarly, I've thought about attempting to represent using divide by zero within an SMT formula, such as the following Z3/SMT formula:

(declare-const a Int)
(assert (= (/ a 0.0) 1.0))
(assert (= (/ a 0.0) 2.0))
(check-sat)

However, given the application, I'm not sure this is going to be helpful.

Application: I'm using this to compare results between two different static analyses between different domains.

tl;dr:

How to represent infeasible, bottom integer elements as SMT formula?

Edit

I didn't try this enough, maybe the question is more along the lines of "is there a more eloquent way to model a bottom value besides the following?":

(declare-const a Int)
(assert (and (>= a 0) (< a 0)))
(check-sat)

The above will yield unsat, as expected. And since I'm trying to compare results of different static analyses, I can formulate questions about locals as such (is a top value equal to a bottom value):

(declare-const a Int)
(declare-const b Int)
(assert (= (and (>= a 0) (< a 0))
           (or (>= b 0) (< b 0))))

(check-sat)

This will also yield unsat.

$\endgroup$

1 Answer 1

2
$\begingroup$

First, you need to figure out the semantics of your language: does divide-by-zero cause the program to abort/halt/throw an exception, or does execution proceed and the divide-by-zero returns a NaN?

If it causes the program to halt, then you should not try to represent $\bot$ values. Instead, treat division as a conditional statement, that first tests whether the divisor is zero, and if so, aborts/halts/etc.

If it returns a NaN, then one approach is to introduce an extra boolean variable associated with each program variable. This boolean indicates whether the corresponding program variable holds a NaN. You should be able to work out the appropriate constraints to ensure these boolean variables receive the appropriate values.

$\endgroup$
4
  • $\begingroup$ The semantics of the language, I don't think, are relevant. Divide by zero is an instance of an infeasible, bottom value when analyzing integer variables and arithmetic in a program. Static analysis needs a fixed point value for variables on invalid branches. What I need the SMT representation for is to compare the results of different static analyses. I like the idea of a boolean flag for NaN, however, I can't change the analysis I'm comparing against, so that is a nonstarter. $\endgroup$
    – kballou
    May 4, 2021 at 16:12
  • 1
    $\begingroup$ @kballou, I suspect it depends on the static analysis. It sounds like you have constraints that aren't mentioned in the question. Given that, we might not be able to help you. $\endgroup$
    – D.W.
    May 4, 2021 at 17:05
  • $\begingroup$ that's certainly fair. I wasn't as clear as I could have been when posing the question. I'll accept this answer because I think given the original posing of the question, this answer seems to add some good ideas. Thanks. $\endgroup$
    – kballou
    May 4, 2021 at 17:13
  • $\begingroup$ @kballou, if you're trying to extend some existing static analysis, maybe it'd be helpful to ask a new question where you describe that static analysis and ask how to extend it? Maybe there's a paper that describes the static analysis approach you're currently working with. $\endgroup$
    – D.W.
    May 4, 2021 at 17:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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