Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

State explosion checking for overflow/underflow #844

Open
lwli11 opened this issue Jan 28, 2025 · 6 comments
Open

State explosion checking for overflow/underflow #844

lwli11 opened this issue Jan 28, 2025 · 6 comments
Labels
cn performance

Comments

@lwli11
Copy link

lwli11 commented Jan 28, 2025

I don't know why this code takes longer and longer to verify depending on how many elements of the struct example_t. Here are the measurements we took so far, with 3 elements (as shown below) taking a reasonable time, but as we uncomment additional checks, the time to verify gets very long:

3 variables:
real 4m40.465s
user 0m8.705s
sys 0m3.681s

4 variables:
real 37m31.307s
user 1m11.905s
sys 0m30.957s

5 variables:
Killed

real 371m52.417s
user 8m14.805s
sys 3m15.159s

#include <stdint.h>

extern int pow(int a, int b);
/*@
        spec pow(i32 a, i32 b);
        requires true;
        ensures true;
@*/

typedef struct {
    uint16_t x;
    uint16_t y;
    uint16_t z;
    uint16_t a;
    uint16_t b;
} example_t;
int calculate_distance(example_t* p1,example_t* p2)
/*@
        requires take x = Owned<example_t>(p1);
        take y = Owned<example_t>(p2);
        ensures take x2 = Owned<example_t>(p1);
        take y2 = Owned<example_t>(p2);
@*/
{
    int distance = 0;
    if (!((int)p2->x > 0 && (int)p1->x< INT_MIN + (int)p2->x) && !((int)p2->x <0 && (int)p1->x > INT_MAX +  (int)p2->x)){
        distance += pow((int)p1->x - (int)p2->x, 2);
    }
    if (!((int)p2->y > 0 && (int)p1->y < INT_MIN + (int)p2->y) && !((int)p2->y <0 && (int)p1->y > INT_MAX +  (int)p2->y)){

        int tmp = pow((int)p1->y - (int)p2->y, 2);
        if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) {
        distance +=tmp;
        }
    }

    if (!((int)p2->z > 0 && (int)p1->z < INT_MIN + (int)p2->z) && !((int)p2->z <0 && (int)p1->z > INT_MAX +  (int)p2->z)){
        int tmp = pow((int)p1->z - (int)p2->z, 2);

        if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) {
        distance +=tmp;
        }

    }
/*
    if (!((int)p2->a > 0 && (int)p1->a < INT_MIN + (int)p2->a) && !((int)p2->a <0 && (int)p1->a > INT_MAX +  (int)p2->a)){
      int tmp = pow((int)p1->a - (int)p2->a, 2);

      if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) {
        distance +=tmp;
      }
    }
   if (!((int)p2->b > 0 && (int)p1->b < INT_MIN + (int)p2->b) && !((int)p2->b <0 && (int)p1->b > INT_MAX +  (int)p2->b)){
      int tmp = pow((int)p1->b - (int)p2->b, 2);

      if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) {
        distance +=tmp;
      }
    }

*/
        return distance;

}
@septract
Copy link
Collaborator

The 4-variable version of this doesn't seem to be stuck on long-running solver queries, but instead is generating a lot of small queries, each of which is resolved quickly.

@cp526 @yav any thoughts what might be going on?

@septract septract mentioned this issue Feb 12, 2025
Merged
@septract
Copy link
Collaborator

Ha, I tried to run the 4-variable version and it crashed after 7 hours:

cn verify --solver-type=cvc5 --solver-logging=overflow_timeout_4var_log broken/error-timeout/overflow_timeout_4var.c
cn: internal error, uncaught exception:
    Sys_error("overflow_timeout_4var_log/model_send_92151.smt: Too many open files")
    Raised by primitive operation at Stdlib.open_out_gen in file "stdlib.ml", line 329, characters 29-55
    Called from Stdlib.open_out in file "stdlib.ml" (inlined), line 334, characters 2-74
    Called from Cn__Solver.Logger.make.get_file in file "backend/cn/lib/solver.ml", line 1233, characters 6-83
    Called from Cn__Solver.model_evaluator.model_evaluator in file "backend/cn/lib/solver.ml", line 1348, characters 34-53
    Called from Cn__Solver.provable.model_from in file "backend/cn/lib/solver.ml", line 1412, characters 15-38
    Called from Cn__ResourceInference.General.predicate_request.resource_scan in file "backend/cn/lib/resourceInference.ml", line 201, characters 20-47
    Called from Cn__Typing.map_and_fold_resources_internal.(fun) in file "backend/cn/lib/typing.ml", line 618, characters 27-35
    Called from Stdlib__List.fold_right in file "list.ml", line 126, characters 16-37
    Called from Stdlib__List.fold_right in file "list.ml", line 126, characters 16-37
    Called from Stdlib__List.fold_right in file "list.ml", line 126, characters 16-37
    Called from Stdlib__List.fold_right in file "list.ml", line 126, characters 16-37
    Called from Stdlib__List.fold_right in file "list.ml", line 126, characters 16-37
    Called from Stdlib__List.fold_right in file "list.ml", line 126, characters 16-37
    Called from Cn__Typing.map_and_fold_resources_internal in file "backend/cn/lib/typing.ml", line 616, characters 4-1023
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.sandbox in file "backend/cn/lib/typing.ml", line 86, characters 10-13
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.run_from_pause in file "backend/cn/lib/typing.ml", line 68, characters 50-55
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 164, characters 6-573
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 186, characters 4-69
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

@cp526
Copy link
Collaborator

cp526 commented Feb 13, 2025

The 4-variable version of this doesn't seem to be stuck on long-running solver queries, but instead is generating a lot of small queries, each of which is resolved quickly.

@cp526 @yav any thoughts what might be going on?

My guess would be that this leads to too many control-flow paths: each time there's a && in the condition, control splits and CN has to separately analyse the short-circuiting path and the non-short-circuiting. Here the number of paths will quickly multiply.

@septract
Copy link
Collaborator

That makes sense. Is there a way to solve in the proof this to make CN pass such a case?

I guess if we just break out each if into a subfunction, the path explosion wouldn't happen.

@cp526
Copy link
Collaborator

cp526 commented Feb 14, 2025

I guess if we just break out each if into a subfunction, the path explosion wouldn't happen.

That should work. Probably CN should let the user put pre/postconditions in arbitrary places, then one could use that to merge control-flow paths in CN's analysis.

Another option, but that's a hack really, is to maybe replace && with *, which I'd expect to have the same effect.

@septract septract mentioned this issue Feb 14, 2025
Open
@septract
Copy link
Collaborator

Here's another example from @lwli11 where the code takes an excessively long time: #357 (comment)

I would guess this is also caused by a control-flow path explosion.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
cn performance
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@septract @cp526 @ZippeyKeys12 @lwli11