1

When crosshair finds no counterexamples, has it used the Z3 solver to prove that my contract holds?

The docs indicate that the absence of a counterexample doesn't guarantee that the property holds, but is that just because the translation or modeling could be incorrect?

Disclaimer: I am the the primary contributor for CrossHair (I'm just using stack overflow as a public way to record answers to questions I've previously been asked)

pschanely
  • 144
  • 1
  • 8
  • 1
    @wjandrea - Having a tag for CrossHair would be ideal, but I don't have the reputation to create it. And it seems like at least one tag is required. Do you know what people normally do for libraries/tools that don't have tags yet? UPDATE: I found some more tags, just had to get creative about what to search for. Thank you! – pschanely Mar 03 '20 at 01:05

1 Answers1

1

Apart from the likely many issues with unsound modeling, CrossHair does not provide this guarantee.

CrossHair is a wildly incomplete system. Internally, for each postcondition, it generates three possible results: "confirmed," "rejected," and "unknown." It only produces output for the "rejected" case; therefore, the absence of output does not indicate a verification of the statement.

Why does CrossHair work this way? Two reasons:

  1. CrossHair generates the "unknown" for all but the most trivial cases. The distinction between "unknown" and "confirmed" is not terribly actionable for most developers. (at least presently, refactoring your code to make it fully explorable by CrossHair will be impossible or ugly) Note however that CrossHair will attempt many execution paths before producing the "unknown" result - the result still provides some evidence that the condition holds.
  2. The confirmed-vs-unknown distinction will be highly unstable over time. CrossHair is designed, from the ground-up, to evolve. On average, SMT solvers will get better. CrossHair will get better. But both will get better on average; for individual cases, either could get worse. In an effort to avoid concerns about confirmed-vs-unknown regressions, this distinction is hidden by default.

It's best to think of CrossHair as a solver-assisted fuzz tester.

All that said, if you'd still like to see what properties are confirmable, you can request this output with a special "report all" option: crosshair check --report_all [TARGET].

pschanely
  • 144
  • 1
  • 8