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

Fix longjmp crash on Uninitialized #1210

Merged
merged 4 commits into from
Oct 16, 2023
Merged

Fix longjmp crash on Uninitialized #1210

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
fd5237a
Add 68-longjmp/56-longjmp-top extracted from concrat
sim642 Oct 9, 2023
2224e86
Fix longjmp crash on Uninitialized
sim642 Oct 9, 2023
a4261de
Add final message for unknown ignored longjmp
sim642 Oct 16, 2023
5948ca4
Mark longjmp-top reachability test as TODO
sim642 Oct 16, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 9 additions & 2 deletions src/analyses/base.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1217,9 +1217,16 @@ struct
if copied then
M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
x
| y -> failwith (GobPretty.sprintf "problem?! is %a %a:\n state is %a" CilType.Exp.pretty e VD.pretty y D.pretty ctx.local)
| Top
| Bot ->
JmpBufDomain.JmpBufSet.top ()
| y ->
M.debug ~category:Imprecise "EvalJmpBuf %a is %a, not JmpBuf." CilType.Exp.pretty e VD.pretty y;
JmpBufDomain.JmpBufSet.top ()
end
| _ -> failwith "problem?!"
| _ ->
M.debug ~category:Imprecise "EvalJmpBuf is not Address";
JmpBufDomain.JmpBufSet.top ()
end
| Q.EvalInt e ->
query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e
Expand Down
21 changes: 21 additions & 0 deletions tests/regression/68-longjmp/56-longjmp-top.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
// Extracted from concrat/pigz.
#include <setjmp.h>
#include <pthread.h>
#include <goblint.h>

pthread_key_t buf_key;

int main() {
jmp_buf buf;
pthread_setspecific(buf_key, &buf);

if (!setjmp(buf)) {
jmp_buf *buf_ptr;
buf_ptr = pthread_getspecific(buf_key);
longjmp(*buf_ptr, 1); // NO CRASH: problem?!
}
else {
__goblint_check(1); // reachable
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The crash on longjmp is fixed but apparently this doesn't still become reachable?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Returning top here doesn't make code that is otherwise unreachable reachable iirc... I think this is a fundamental limitation that I am not sure how to address best.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I thought a top jmpbuf would just jump back to every setjmp without filtering by node/context, but apparently all we do is warn:

analyzer/src/framework/constraints.ml

Lines 1664 to 1666 in 5cc4811

let handle_target target = match target with
| JmpBufDomain.BufferEntryOrTop.AllTargets ->
M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env

Maybe we should have an option to do that?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem is a bit where one wants to propagate things to... Just up the call stack, assuming the invocation was not UB? Also down the callstack because someone might be trying to implement co-routines? Also to completely unrelated places?
The other problem is that quite often the local state propagated somewhere because of an unknown longjmp will not be suitable for incorporation by join, as it is incorporated into an unsuitable function. This might lead to a huge precision loss.
My idea would be to leave this as is, but make this type of warning one of the severe top-level warnings that is reported separately at the end of the analysis (in the sense of #1190 ).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem is a bit where one wants to propagate things to... Just up the call stack, assuming the invocation was not UB? Also down the callstack because someone might be trying to implement co-routines? Also to completely unrelated places?

To the same places we normally do: in the same function and up the call stack. It could just be that all setjmps incorporate the unknown jump target instead of the same node and context check that normally happens. So unknown jump buffer would mean "all jumpbuffers that we normally could jump to".

The other problem is that quite often the local state propagated somewhere because of an unknown longjmp will not be suitable for incorporation by join, as it is incorporated into an unsuitable function. This might lead to a huge precision loss.

Of course it would be very imprecise, but I'm not sure if it'd cause anything incompatible per se. Ambiguous longjmps to multiple possible targets should be similar. The compatibility is ensured by each upwards propagation of the jumps doing the appropriate returns and combine_envs.

My idea would be to leave this as is, but make this type of warning one of the severe top-level warnings that is reported separately at the end of the analysis (in the sense of #1190 ).

I added that, so let's leave it at that.

Copy link
Member

@michael-schwarz michael-schwarz Oct 16, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To the same places we normally do: in the same function and up the call stack.

In this case, the clean solution would be to warn and then replace the top set of possible targets with the set of legal jumptargets (which we have at hand anyway), which indeed seems reasonable and also prevents any issues with propagation to ill-suited locations.

}
return 0;
}
Loading