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.

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

Failure while testing each #689

Closed
yav opened this issue Nov 4, 2024 · 1 comment · Fixed by #773
Closed

Failure while testing each #689

yav opened this issue Nov 4, 2024 · 1 comment · Fixed by #773
Assignees
Labels
CN spec testing cn CN-exec Related to CN executable spec generation, called using `cn instrument`

Comments

@yav
Copy link
Collaborator

yav commented Nov 4, 2024

When I try to generate tests for the following code, I get an exception:

void preserve(unsigned long size, int *p)                                           
/*@                                                                              
requires                                                                         
  take a1 = each(u64 i; i <= 0u64 && i < size) { Owned<int>(array_shift<int>(p,i)) };
ensures                                                                          
  take a2 = each(u64 i; i <= 0u64 && i < size) { Owned<int>(array_shift<int>(p,i)) };
@*/                                                                              
{                                                                                
} 

This throws:

 Failure("TODO rearrange_start_inequality at 6:25")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__Cn_internal_to_ail.generate_start_expr in file "backend/cn/lib/cn_internal_to_ail.ml", line 533, characters 11-53

Another example that leads to the same exception is if you make the size an int, and add a cast:

take a1 = each(u64 i; i <= 0u64 && i < (u64)size) { Owned<int>(array_shift<int>(p,i)) };

Another variation, if we remove the redundant 0 <= 0u64 constraint:

take a1 = each(u64 i; i < size) { Owned<int>(array_shift<int>(p,i)) };

This throws:

cn: internal error, uncaught exception:
    Failure("Not of correct form (unlikely case - i's not matching)")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__Cn_internal_to_ail.generate_start_expr in file "backend/cn/lib/cn_internal_to_ail.ml", line 530, characters 8-73

The only version I was able to run without exceptions is to use int as the size:

take a1 = each(i32 i; 0i32 <= i && i < size) { Owned<int>(array_shift<int>(p,i)) };

This, however, leads to warnings from cn saying that each expects a u64.

@podhrmic
Copy link
Contributor

podhrmic commented Dec 9, 2024

@ZippeyKeys12 bumping for visibility - as mentioned in #721 the OpenSUT code contains specs that are not compatible with the test generator. If you tell me how to change the specs such that they are more testing friendly I am happy to do that.

For example, this spec triggers the error: requires take tin = each(u64 i; i < 3u64) {Block<uint8_t[4]>(array_shift(trip, i))};

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CN spec testing cn CN-exec Related to CN executable spec generation, called using `cn instrument`
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants