Skip to content

Input validation problems with --function-pointer-restrictions-file #6368

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
Closed
avanhatt opened this issue Sep 28, 2021 · 7 comments · Fixed by #6376
Closed

Input validation problems with --function-pointer-restrictions-file #6368

avanhatt opened this issue Sep 28, 2021 · 7 comments · Fixed by #6376
Assignees
@tautschnig @avanhatt
Labels
aws Bugs or features of importance to AWS CBMC users aws-high pending merge

Comments

@avanhatt
Copy link

avanhatt commented Sep 28, 2021 •
edited
Loading

CBMC version: 5.30.1 (cbmc-5.30.1)
Operating system: Ubuntu 20.04.2
Exact command line resulting in the issue:

goto-instrument --function-pointer-restrictions-file restrictions (within the context of the RMC tool).

What behaviour did you expect:

CBMC to restrict function pointer branch analysis to the cases specified, as described in the documentation for function pointer descriptions here.

What happened instead:

I am running into two related problems with the --function-pointer-restrictions-file flag.

(1) Casting

The functions I would like to restrict are a different type than the call site due to a cast in the source code to a function that takes a void pointer. The source code looks roughly like this:

// function pointer creation
.field=(int (*)(void *))_Animal_noise // struct field 

// function pointer use
var_5.vtable->field(var_1);

However, if I try to pass _Animal_noise as a restriction, I get this error:

Reason: type mismatch: `main.function_pointer_call.1' points to `int (void *)', but restriction `_Animal_noise' has type `int (struct _10007873221718841048 *self)'

However, if I try and include the cast in the restrictions file, it fails to parse:

Invalid restriction
Reason: symbol not found: (int (*)(void *))_Animal_noise

The pointer itself does not have a symbol name to my understanding, because it is a struct field.

(2) . in function name wrong error, see below

In a different example, some of my restricted function have .. in the name, and fail to parse:

Example:

  "_ZN80_$LT$devices..virtio..mmio..MmioTransport$u20$as$u20$devices..bus..BusDevice$GT$5write17h533d97e6e2ca6db0E.function_pointer_call.1": [
    "_ZN7devices6virtio6device12VirtioDevice20ack_features_by_page17hbff58082681c1a52E_wrapper",
    "_ZN7devices6virtio6device12VirtioDevice20ack_features_by_page17h2c20fca1a3ee805eE_wrapper",
    "_ZN7devices6virtio6device12VirtioDevice20ack_features_by_page17h1668e8cac23d16f1E_wrapper"
  ],

Error:

Reading GOTO program from 'parse_harness1/a.out'
file restrictions: syntax error
failed to read function pointer restrictions from restrictions

This is despite CBMC analyzing the file with these names fine without restrictions.
@danielsn danielsn added aws Bugs or features of importance to AWS CBMC users aws-high labels Sep 28, 2021
@tautschnig
Copy link
Collaborator

Taking a look.

@tautschnig
Copy link
Collaborator

@avanhatt Could you please share the goto binary and the restrictions file? The type casts I'm able to make sense of and am working to fix, but the syntax error I cannot immediately relate to the use of ...

@avanhatt
Copy link
Author

Ah, I'm so sorry, looks like I was reading the error message in the 2nd issue wrong - the problem was I was passing the wrong file path, which failed to read function pointer restrictions from restrictions was trying to tell me.

Updating the description and working on attaching a standalone binary.

@jimgrundy
Copy link
Collaborator

@remi-delmas-3000 Do you have thoughts on this given your experiences with function pointer resolution?

@remi-delmas-3000
Copy link
Collaborator

The documentation seems to say that function pointer restriction instructions must be function identifiers and not arbitrary expressions involving casts. So it does not look surprising that the replacement file fails to load.

However, automatic function pointer removal (as opposed to manual restriction discussed here) is able to insert type casts on arguments (and also return values ?) when the replacement does not fully match the function pointer type being removed.

Maybe casts could be inserted as needed when restriction is performed ?

tautschnig added a commit to tautschnig/cbmc that referenced this issue Sep 30, 2021
@tautschnig
Use remove-function-pointers code for restricted function pointers
e4bf3fb 
We had two instances of code generating an if-else sequence of function
calls for function pointers. The code used with
--restrict-function-pointer, however, was not able to cope with type
mismatches. Make the code from remove_function_pointers re-usable in
both contexts, enabling support for additional type casts.

Fixes: diffblue#6368
@tautschnig tautschnig mentioned this issue Sep 30, 2021
Merged
4 tasks
@tautschnig
Copy link
Collaborator

[...]

However, automatic function pointer removal (as opposed to manual restriction discussed here) is able to insert type casts on arguments (and also return values ?) when the replacement does not fully match the function pointer type being removed.

Maybe casts could be inserted as needed when restriction is performed ?

This is now implemented in #6376.

tautschnig added a commit to tautschnig/cbmc that referenced this issue Sep 30, 2021
@tautschnig
Use remove-function-pointers code for restricted function pointers
0cdc654 
We had two instances of code generating an if-else sequence of function
calls for function pointers. The code used with
--restrict-function-pointer, however, was not able to cope with type
mismatches. Make the code from remove_function_pointers re-usable in
both contexts, enabling support for additional type casts.

Fixes: diffblue#6368
@avanhatt
Copy link
Author

avanhatt commented Oct 1, 2021

Core fix of allowing function pointer casts in restrictions works for me in #6376! 🎉

Before:

/usr/bin/goto-instrument --version
5.30.1 (cbmc-5.30.1)
firecracker (block-device) $ /usr/bin/goto-instrument --function-pointer-restrictions-file restrictions-manual --drop-unused-functions --reachability-slice build/cargo_target/x86_64-unknown-linux-gnu/debug/deps/parse_harness3/a.out build/cargo_target/x86_64-unknown-linux-gnu/debug/deps/parse_harness3/b.out
Reading GOTO program from 'build/cargo_target/x86_64-unknown-linux-gnu/debug/deps/parse_harness3/a.out'
Invalid restriction
Reason: type mismatch: `restriction4794klvv2c6mv9drdevices_32.function_pointer_call.1' points to `_Bool (void *)', but restriction `_ZN95_$LT$devices..virtio..block..device..Block$u20$as$u20$devices..virtio..device..VirtioDevice$GT$12is_activated17hd81576bdb7d3385bE' has type `_Bool (struct _220066741243748023 *self)'

With #6376:

firecracker (block-device) $ which goto-instrument 
/home/ubuntu/cbmc/build/bin/goto-instrument
firecracker (block-device) $ goto-instrument --function-pointer-restrictions-file restrictions-manual --drop-unused-functions --reachability-slice build/cargo_target/x86_64-unknown-linux-gnu/debug/deps/parse_harness3/a.out build/cargo_target/x86_64-unknown-linux-gnu/debug/deps/parse_harness3/b.out
Reading GOTO program from 'build/cargo_target/x86_64-unknown-linux-gnu/debug/deps/parse_harness3/a.out'
replacing function pointer by 4 possible targets
# ...
Writing GOTO program to 'build/cargo_target/x86_64-unknown-linux-gnu/debug/deps/parse_harness3/b.out'

However, I noticed the function name and call site were dropped from the cbmc assertion message:

Before:

[assertion.129] dereferenced function pointer at _ZN4core3ptr117drop_in_place$LT$alloc..boxed..Box$LT$dyn$u20$std..error..Error$u2b$core..marker..Send$u2b$core..marker..Sync$GT$$GT$17h527418d374008dddE.function_pointer_call.1 must be one of …

With #6376:

[pointer_dereference.2] dereferenced function pointer at must be one of [_ZN4core3ptr45drop_in_place$LT$serde_json..error..Error$GT$17h24c4eb9268bc5828E, _ZN4core3ptr226drop_in_place$LT$std..error..$LT$impl$u20$core..convert..From$LT$alloc..string..String$GT$$u20$for$u20$alloc..boxed..Box$LT$dyn$u20$std..error..Error$u2b$core..marker..Send$u2b$core..marker..Sync$GT$$GT$..from..StringError$GT$17hf5b344376f4d1ab0E]: FAILURE
[pointer_dereference.3] no candidates for dereferenced function pointer: FAILURE

It would be great if both of these asserts had the location.

tautschnig added a commit to tautschnig/cbmc that referenced this issue Oct 1, 2021
@tautschnig
Use remove-function-pointers code for restricted function pointers
bec1d91 
We had two instances of code generating an if-else sequence of function
calls for function pointers. The code used with
--restrict-function-pointer, however, was not able to cope with type
mismatches. Make the code from remove_function_pointers re-usable in
both contexts, enabling support for additional type casts.

Fixes: diffblue#6368
tautschnig added a commit to tautschnig/cbmc that referenced this issue Nov 11, 2021
@tautschnig
Use remove-function-pointers code for restricted function pointers
d6fa9bd 
We had two instances of code generating an if-else sequence of function
calls for function pointers. The code used with
--restrict-function-pointer, however, was not able to cope with type
mismatches. Make the code from remove_function_pointers re-usable in
both contexts, enabling support for additional type casts.

Fixes: diffblue#6368
tautschnig added a commit to tautschnig/cbmc that referenced this issue Nov 11, 2021
@tautschnig
Use remove-function-pointers code for restricted function pointers
74bc2fe 
We had two instances of code generating an if-else sequence of function
calls for function pointers. The code used with
--restrict-function-pointer, however, was not able to cope with type
mismatches. Make the code from remove_function_pointers re-usable in
both contexts, enabling support for additional type casts.

Fixes: diffblue#6368
tautschnig added a commit to tautschnig/cbmc that referenced this issue Dec 1, 2021
@tautschnig
Use remove-function-pointers code for restricted function pointers
d825d04 
We had two instances of code generating an if-else sequence of function
calls for function pointers. The code used with
--restrict-function-pointer, however, was not able to cope with type
mismatches. Make the code from remove_function_pointers re-usable in
both contexts, enabling support for additional type casts.

Fixes: diffblue#6368
vmihalko pushed a commit to vmihalko/cbmc that referenced this issue Jan 24, 2022
@tautschnig @vmihalko
Use remove-function-pointers code for restricted function pointers
0ecebd2 
We had two instances of code generating an if-else sequence of function
calls for function pointers. The code used with
--restrict-function-pointer, however, was not able to cope with type
mismatches. Make the code from remove_function_pointers re-usable in
both contexts, enabling support for additional type casts.

Fixes: diffblue#6368
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@tautschnig tautschnig

@avanhatt avanhatt

Labels
aws Bugs or features of importance to AWS CBMC users aws-high pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Use remove-function-pointers code for restricted function pointers tautschnig/cbmc
5 participants
@tautschnig @remi-delmas-3000 @danielsn @avanhatt @jimgrundy