search

pschanely / CrossHair

An analysis tool for Python that blurs the line between testing and type systems.
Other
1.03k stars 49 forks source link

cover command error: (AttributeError("'AlgebraicNumRef' object has no attribute 'as_fraction'") #242

Closed SeanHeelan closed 8 months ago

SeanHeelan commented 8 months ago

(Nice project!)

Expected vs actual behavior When applied to the following code the cover finds a single input that hits the return -1 path. It should find two inputs, covering two paths. 

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
    return area
$ crosshair cover --example_output_format arg_dictionary  triangle_area.triangle_area
{"a": 1, "b": 0, "c": 0}

When I ran in verbose mode the following error appears, which seems relevant. 

$ crosshair cover -v --example_output_format arg_dictionary  triangle_area.triangle_area
79969.383| |unwalled_main() CrossHair v0.0.48 on linux, Python 3.11.7
79969.383| |unwalled_main() Installed plugins: []
79969.383|  |cover() Begin cover on triangle_area
79969.384|    |explore_paths() Iteration  1
79969.384|      |pre_path_hook() No coverage biasing in effect. ( 0  code locations)
79969.385|     |condition_parser() Using parsers:  (AnalysisKind.PEP316, AnalysisKind.icontract, AnalysisKind.deal)
79969.385|     |gen_args() created proxy for a as type: SymbolicInt 0x7fe62d71d290
79969.385|     |gen_args() created proxy for b as type: SymbolicInt 0x7fe62d71c990
79969.385|     |gen_args() created proxy for c as type: SymbolicInt 0x7fe62d71dcd0
79969.388|        |choose_possible() SMT chose: Not(a_2 + b_3 <= c_4) (chance: 0.75 )
79969.390|        |choose_possible() SMT chose: Not(a_2 + c_4 <= b_3) (chance: 0.75 )
79969.392|        |choose_possible() SMT chose: Not(b_3 + c_4 <= a_2) (chance: 0.75 )
79969.394|                      |choose_possible() SMT chose: Not(2 == 0) (chance: 1.0 )
79969.397|                |choose_possible() SMT chose: Not(And((ToReal(a_2 + b_3 + c_4)/2)*
        (ToReal(a_2 + b_3 + c_4)/2 - ToReal(a_2))*
        (ToReal(a_2 + b_3 + c_4)/2 - ToReal(b_3))*
        (ToReal(a_2 + b_3 + c_4)/2 - ToReal(c_4)) ==
        0,
        1/2 < 0)) (chance: 1.0 )
79969.409|      |detach_path() Detached from search tree
79969.429|     |on_path_complete() Skipping path (failed to realize values) (AttributeError("'AlgebraicNumRef' object has no attribute 'as_fraction'"), [<FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/path_cover.py, line 92 in on_path_complete>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/core.py, line 557 in eval_friendly_format>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/core.py, line 545 in deep_realize>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/copyext.py, line 37 in deepcopyext>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/libimpl/builtinslib.py, line 1230 in __ch_realize__>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/statespace.py, line 927 in find_model_value>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/statespace.py, line 151 in model_value_to_python>])
79969.429|    |explore_paths() Verification status: CONFIRMED

Here is the full output log. 

$ crosshair cover -v --example_output_format arg_dictionary  triangle_area.triangle_area
79969.383| |unwalled_main() CrossHair v0.0.48 on linux, Python 3.11.7
79969.383| |unwalled_main() Installed plugins: []
79969.383|  |cover() Begin cover on triangle_area
79969.384|    |explore_paths() Iteration  1
79969.384|      |pre_path_hook() No coverage biasing in effect. ( 0  code locations)
79969.385|     |condition_parser() Using parsers:  (AnalysisKind.PEP316, AnalysisKind.icontract, AnalysisKind.deal)
79969.385|     |gen_args() created proxy for a as type: SymbolicInt 0x7fe62d71d290
79969.385|     |gen_args() created proxy for b as type: SymbolicInt 0x7fe62d71c990
79969.385|     |gen_args() created proxy for c as type: SymbolicInt 0x7fe62d71dcd0
79969.388|        |choose_possible() SMT chose: Not(a_2 + b_3 <= c_4) (chance: 0.75 )
79969.390|        |choose_possible() SMT chose: Not(a_2 + c_4 <= b_3) (chance: 0.75 )
79969.392|        |choose_possible() SMT chose: Not(b_3 + c_4 <= a_2) (chance: 0.75 )
79969.394|                      |choose_possible() SMT chose: Not(2 == 0) (chance: 1.0 )
79969.397|                |choose_possible() SMT chose: Not(And((ToReal(a_2 + b_3 + c_4)/2)*
        (ToReal(a_2 + b_3 + c_4)/2 - ToReal(a_2))*
        (ToReal(a_2 + b_3 + c_4)/2 - ToReal(b_3))*
        (ToReal(a_2 + b_3 + c_4)/2 - ToReal(c_4)) ==
        0,
        1/2 < 0)) (chance: 1.0 )
79969.409|      |detach_path() Detached from search tree
79969.429|     |on_path_complete() Skipping path (failed to realize values) (AttributeError("'AlgebraicNumRef' object has no attribute 'as_fraction'"), [<FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/path_cover.py, line 92 in on_path_complete>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/core.py, line 557 in eval_friendly_format>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/core.py, line 545 in deep_realize>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/copyext.py, line 37 in deepcopyext>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/libimpl/builtinslib.py, line 1230 in __ch_realize__>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/statespace.py, line 927 in find_model_value>, <FrameSummary file /home/sean/.virtualenvs/nostradamus/lib64/python3.11/site-packages/crosshair/statespace.py, line 151 in model_value_to_python>])
79969.429|    |explore_paths() Verification status: CONFIRMED
79969.432|     |bubble_status()  |     RootNode {CONFIRMED:1}
79969.432|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize a_2) {CONFIRMED:1}
79969.432|     |bubble_status()  |  -> NodeStem() {}
79969.432|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize b_3) {CONFIRMED:1}
79969.432|     |bubble_status()  |  -> NodeStem() {}
79969.432|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize c_4) {CONFIRMED:1}
79969.432|     |bubble_status()  |  -> NodeStem() {}
79969.432|     |bubble_status() n|\ y  *WorstResultNode(a_2 + b_3 <= c_4) {CONFIRMED:1}
79969.432|     |bubble_status()  |  -> NodeStem() {}
79969.432|     |bubble_status() n|\ y  *WorstResultNode(a_2 + c_4 <= b_3) {CONFIRMED:1}
79969.432|     |bubble_status()  |  -> NodeStem() {}
79969.432|     |bubble_status() n|\ y  *WorstResultNode(b_3 + c_4 <= a_2) {CONFIRMED:1}
79969.432|     |bubble_status()  |  -> NodeStem() {}
79969.433|     |bubble_status()  |     *DeatchedPathNode {CONFIRMED:1}
79969.433|     |bubble_status() n|\ y  *ModelValueNode(1 == a_2) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.433|     |bubble_status()  | n|\ y  *ModelValueNode(1 == b_3) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.433|     |bubble_status()  |  |  -> *SearchLeaf(CONFIRMED) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.433|     |bubble_status()  |  -> NodeStem() {}
79969.433|     |bubble_status()  -> NodeStem() {}
79969.433|    |explore_paths() Path tree stats {CONFIRMED:1}
79969.433|    |explore_paths() Iteration  2
79969.434|      |pre_path_hook() No coverage biasing in effect. ( 3  code locations)
79969.434|     |condition_parser() Using parsers:  (AnalysisKind.PEP316, AnalysisKind.icontract, AnalysisKind.deal)
79969.434|     |gen_args() created proxy for a as type: SymbolicInt 0x7fe61b8e2890
79969.434|     |gen_args() created proxy for b as type: SymbolicInt 0x7fe61b8e3e50
79969.435|     |gen_args() created proxy for c as type: SymbolicInt 0x7fe61b8e05d0
79969.436|        |choose_possible() SMT chose: Not(a_2 + b_3 <= c_4) (chance: 0.75 )
79969.437|        |choose_possible() SMT chose: Not(a_2 + c_4 <= b_3) (chance: 0.75 )
79969.438|        |choose_possible() SMT chose: b_3 + c_4 <= a_2 (chance: 1.0 )
79969.438|      |detach_path() Detached from search tree
79969.457|     |on_path_complete() Realized args: {"a": 1, "b": 0, "c": 0}
79969.457|     |on_path_complete() Realized return: -1.0
79969.457|    |explore_paths() Verification status: CONFIRMED
79969.460|     |bubble_status()  |     RootNode {CONFIRMED:2}
79969.460|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize a_2) {CONFIRMED:2}
79969.460|     |bubble_status()  |  -> NodeStem() {}
79969.460|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize b_3) {CONFIRMED:2}
79969.460|     |bubble_status()  |  -> NodeStem() {}
79969.460|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize c_4) {CONFIRMED:2}
79969.460|     |bubble_status()  |  -> NodeStem() {}
79969.460|     |bubble_status() n|\ y  *WorstResultNode(a_2 + b_3 <= c_4) {CONFIRMED:2}
79969.460|     |bubble_status()  |  -> NodeStem() {}
79969.460|     |bubble_status() n|\ y  *WorstResultNode(a_2 + c_4 <= b_3) {CONFIRMED:2}
79969.460|     |bubble_status()  |  -> NodeStem() {}
79969.460|     |bubble_status() n|\ y  *WorstResultNode(b_3 + c_4 <= a_2 : exhausted) {CONFIRMED:2}
79969.461|     |bubble_status()  |  |     *DeatchedPathNode {CONFIRMED:1}
79969.461|     |bubble_status()  | n|\ y  *ModelValueNode(1 == a_2) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.461|     |bubble_status()  |  | n|\ y  *ModelValueNode(0 == b_3) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.461|     |bubble_status()  |  |  |  -> *SearchLeaf(CONFIRMED) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.461|     |bubble_status()  |  |  -> NodeStem() {}
79969.461|     |bubble_status()  |  -> NodeStem() {}
79969.461|     |bubble_status()  |     DeatchedPathNode {CONFIRMED:1}
79969.461|     |bubble_status() n|\ y  ModelValueNode(1 == a_2) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.461|     |bubble_status()  | n|\ y  ModelValueNode(1 == b_3) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.461|     |bubble_status()  |  |  -> SearchLeaf(CONFIRMED) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.461|     |bubble_status()  |  -> NodeStem() {}
79969.461|     |bubble_status()  -> NodeStem() {}
79969.461|    |explore_paths() Path tree stats {CONFIRMED:2}
79969.461|    |explore_paths() Iteration  3
79969.462|      |pre_path_hook() No coverage biasing in effect. ( 3  code locations)
79969.462|     |condition_parser() Using parsers:  (AnalysisKind.PEP316, AnalysisKind.icontract, AnalysisKind.deal)
79969.462|     |gen_args() created proxy for a as type: SymbolicInt 0x7fe61b8fdd50
79969.462|     |gen_args() created proxy for b as type: SymbolicInt 0x7fe61b8fdb50
79969.462|     |gen_args() created proxy for c as type: SymbolicInt 0x7fe61b8fde90
79969.463|        |choose_possible() SMT chose: Not(a_2 + b_3 <= c_4) (chance: 0.75 )
79969.465|        |choose_possible() SMT chose: a_2 + c_4 <= b_3 (chance: 1.0 )
79969.466|      |detach_path() Detached from search tree
79969.484|     |on_path_complete() Realized args: {"a": 0, "b": 1, "c": 0}
79969.484|     |on_path_complete() Realized return: -1.0
79969.484|    |explore_paths() Verification status: CONFIRMED
79969.487|     |bubble_status()  |     RootNode {CONFIRMED:3}
79969.487|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize a_2) {CONFIRMED:3}
79969.487|     |bubble_status()  |  -> NodeStem() {}
79969.487|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize b_3) {CONFIRMED:3}
79969.487|     |bubble_status()  |  -> NodeStem() {}
79969.487|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize c_4) {CONFIRMED:3}
79969.487|     |bubble_status()  |  -> NodeStem() {}
79969.487|     |bubble_status() n|\ y  *WorstResultNode(a_2 + b_3 <= c_4) {CONFIRMED:3}
79969.487|     |bubble_status()  |  -> NodeStem() {}
79969.487|     |bubble_status() n|\ y  *WorstResultNode(a_2 + c_4 <= b_3 : exhausted) {CONFIRMED:3}
79969.487|     |bubble_status()  |  |     *DeatchedPathNode {CONFIRMED:1}
79969.487|     |bubble_status()  | n|\ y  *ModelValueNode(0 == a_2) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.487|     |bubble_status()  |  | n|\ y  *ModelValueNode(1 == b_3) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.487|     |bubble_status()  |  |  | n|\ y  *ModelValueNode(0 == c_4) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.487|     |bubble_status()  |  |  |  |  -> *SearchLeaf(CONFIRMED) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.488|     |bubble_status()  |  |  |  -> NodeStem() {}
79969.488|     |bubble_status()  |  |  -> NodeStem() {}
79969.488|     |bubble_status()  |  -> NodeStem() {}
79969.488|     |bubble_status() n|\ y  WorstResultNode(b_3 + c_4 <= a_2 : exhausted) {CONFIRMED:2}
79969.488|    |explore_paths() Path tree stats {CONFIRMED:3}
79969.488|    |explore_paths() Iteration  4
79969.488|      |pre_path_hook() No coverage biasing in effect. ( 3  code locations)
79969.488|     |condition_parser() Using parsers:  (AnalysisKind.PEP316, AnalysisKind.icontract, AnalysisKind.deal)
79969.489|     |gen_args() created proxy for a as type: SymbolicInt 0x7fe61b920e50
79969.489|     |gen_args() created proxy for b as type: SymbolicInt 0x7fe61b920d10
79969.489|     |gen_args() created proxy for c as type: SymbolicInt 0x7fe61b920c90
79969.490|        |choose_possible() SMT chose: a_2 + b_3 <= c_4 (chance: 1.0 )
79969.490|      |detach_path() Detached from search tree
79969.510|     |on_path_complete() Realized args: {"a": 0, "b": 0, "c": 0}
79969.510|     |on_path_complete() Realized return: -1.0
79969.510|    |explore_paths() Verification status: CONFIRMED
79969.513|     |bubble_status()  |     RootNode {CONFIRMED:4}
79969.513|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize a_2) {CONFIRMED:4}
79969.513|     |bubble_status()  |  -> NodeStem() {}
79969.513|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize b_3) {CONFIRMED:4}
79969.513|     |bubble_status()  |  -> NodeStem() {}
79969.513|     |bubble_status()  |\    *ParallelNode(false_pct=1.0, premature realize c_4) {CONFIRMED:4}
79969.513|     |bubble_status()  |  -> NodeStem() {}
79969.513|     |bubble_status() n|\ y  *WorstResultNode(a_2 + b_3 <= c_4 : exhausted) {CONFIRMED:4}
79969.513|     |bubble_status()  |  |     *DeatchedPathNode {CONFIRMED:1}
79969.513|     |bubble_status()  | n|\ y  *ModelValueNode(0 == a_2) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.513|     |bubble_status()  |  | n|\ y  *ModelValueNode(0 == b_3) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.513|     |bubble_status()  |  |  | n|\ y  *ModelValueNode(0 == c_4) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.513|     |bubble_status()  |  |  |  |  -> *SearchLeaf(CONFIRMED) {CONFIRMED:1, realize_c_4:1, realize_b_3:1, realize_a_2:1}
79969.513|     |bubble_status()  |  |  |  -> NodeStem() {}
79969.513|     |bubble_status()  |  |  -> NodeStem() {}
79969.513|     |bubble_status()  |  -> NodeStem() {}
79969.513|     |bubble_status() n|\ y  WorstResultNode(a_2 + c_4 <= b_3 : exhausted) {CONFIRMED:3}
79969.513|    |explore_paths() Path tree stats {CONFIRMED:4}
79969.513|    |explore_paths() Stopping due to path exhaustion
79969.514|   |path_cover() Next best path covers these opcode offsets: {2, 4, 6, 10, 12, 18, 20, 22, 24, 28, 30, 36, 38, 40, 42, 46, 48, 54, 56, 58}
79969.514|   |path_cover() Next best path covers these opcode offsets: {2, 4, 36, 6, 58, 10, 12, 18, 20, 22, 24, 56, 28, 30}
{"a": 1, "b": 0, "c": 0}
pschanely commented 8 months ago

This is a great bug report -- thank you! I can confirm that the error you noticed is a bug, and will be able to ship a fix in the next few days. I uncertain that the immediate fix will make additional progress on the original coverage task, however: I'll need to investigate and get back to you. Please stand by!

pschanely commented 8 months ago

v0.0.49 should find both paths now. Let me know how it goes!