Unexpectedly long run times on a short example containing floats

[SeanHeelan]

Expected vs actual behavior
I'm applying cover to the following code. It differs from the code in issue #242 in that that round(area, 2) is applied to area before returning it.

def triangle_area(a: int, b: int, c: int) -> float:
    if a + b <= c or a + c <= b or b + c <= a:
        return -1.0
    s = (a + b + c) / 2
    area = (s * (s - a) * (s - b) * (s - c)) ** 0.5
    area = round(area, 2)
    return area

When I run it via cover -v --example_output_format arg_dictionary triangle_area_with_round.triangle_area it runs indefinitely, constantly creating new formulae to send to z3. It seems z3 pretty quickly responds with 'Unknown' in each case. Based on this Z3 issue, I am assuming the problem here is due to incompleteness in Z3 when int and float types are mixed in non-linear arithmetic. What I was wondering is, should cover detect this and just terminate the path so that it doesn't run forever?

If I change the types of the arguments to all be floats then cover stalls at the first query to z3. I am guessing this is because z3 is entering a different solver, which doesn't return 'Unknown' but is just very slow.

e.g.

crosshair cover -v --example_output_format arg_dictionary  triangle_area_with_round.triangle_area
80635.074| |unwalled_main() CrossHair v0.0.48 on linux, Python 3.11.7
80635.074| |unwalled_main() Installed plugins: []
80635.074|  |cover() Begin cover on triangle_area
80635.076|    |explore_paths() Iteration  1
80635.076|      |pre_path_hook() No coverage biasing in effect. ( 0  code locations)
80635.076|     |condition_parser() Using parsers:  (AnalysisKind.PEP316, AnalysisKind.icontract, AnalysisKind.deal)
80635.077|     |gen_args() created proxy for a as type: SymbolicFloat 0x7fad839d8c90
80635.077|     |gen_args() created proxy for b as type: SymbolicFloat 0x7fad839d9490
80635.077|     |gen_args() created proxy for c as type: SymbolicFloat 0x7fad839d8290
80635.080|        |choose_possible() SMT chose: Not(a_2 + b_3 <= c_4) (chance: 0.75 )
80635.082|        |choose_possible() SMT chose: Not(a_2 + c_4 <= b_3) (chance: 0.75 )
80635.084|        |choose_possible() SMT chose: Not(b_3 + c_4 <= a_2) (chance: 0.75 )
80635.086|                   |choose_possible() SMT chose: Not(2 == 0) (chance: 1.0 )
80635.088|                |choose_possible() SMT chose: Not(And(((a_2 + b_3 + c_4)/2)*
        ((a_2 + b_3 + c_4)/2 - a_2)*
        ((a_2 + b_3 + c_4)/2 - b_3)*
        ((a_2 + b_3 + c_4)/2 - c_4) ==
        0,
        1/2 < 0)) (chance: 1.0 )
80635.100|                       |choose_possible() SMT chose: Not(100 == 0) (chance: 1.0 )

I've left this run for about 10 mins but not received a solution. I am guessing there isn't much you can do about this, but thought I'd report it anyway in case you see something odd that is fixable. Any suggestions on any changes I could make to the code, or to the arguments to cover to analyse this code?

One final question I had is, could you explain why adding in the call to round results in this code behaving differently to what I reported in #242 ?

Thanks!

[pschanely]

Interesting - I have a few things to investigate here. But at a minimum, crosshair cover isn't supposed to run forever, so something is up. I'll report back soon.

[pschanely]

When I run it via cover -v --example_output_format arg_dictionary triangle_area_with_round.triangle_area it runs indefinitely, constantly creating new formulae to send to z3. It seems z3 pretty quickly responds with 'Unknown' in each case. Based on this Z3 issue, I am assuming the problem here is due to incompleteness in Z3 when int and float types are mixed in non-linear arithmetic. What I was wondering is, should cover detect this and just terminate the path so that it doesn't run forever?

Yes, the fact that it doesn't terminate is a regression where we lost our default timeout for crosshair cover; I have a fix in and am releasing it in 0.0.49 right now. You've got the right intuition about why CrossHair struggles with this kind of problem, though.

I've left this run for about 10 mins but not received a solution. I am guessing there isn't much you can do about this, but thought I'd report it anyway in case you see something odd that is fixable. Any suggestions on any changes I could make to the code, or to the arguments to cover to analyse this code?

Looks like the pure float version gives me two paths now. Perhaps one piece of advice is to try and avoid int-float conversions. Another tactic is to call cover on variants of the function that supply some concrete values ... hopefully enough to remove the nonliear-ness of the problem.

CrossHair has some minimal support for falling back to concrete-symbolic hybrid runs, where only some arguments are symbolic. In theory, that strategy should be able to help with paths like this, but the heuristics that guide it are too primitive to help here. I've filed #245 for investigating this further.

One final question I had is, could you explain why adding in the call to round results in this code behaving differently to what I reported in #242 ?

In #242, we were taking the square root and then immediately returning it. In that situation, CrossHair first picks values tfor the arguments and then the return value. Sometimes, when the arguments are heavily constrained, z3 can solve the square root just by simplification, so that's what happens there. OTOH, when we have to execute round() first, we need to actually work with the symbolic result and then run into trouble.