Skip to content

Commit 85f5cb1

Browse files
michael-schwarzmichael-schwarz
authored
Merge pull request #54 from goblint/setjmp
Add setjmp benchmarks
2 parents 6fd37cf + 25b5315 commit 85f5cb1

15 files changed

Lines changed: 194465 additions & 0 deletions

‎.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,3 +21,5 @@ increment/
2121
result/
2222
cfgs/
2323
.goblint/
24+
*.prec
25+

‎setjmp/README.md‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
# Long Jumps Falling Short - Control-Flow Tracking & Misuse Detection for Non-Local Jumps in C
2+
3+
This page gives additional information on the experiments & implementation
4+
that accompanies our manuscript.
5+
6+
# Basic Setup
7+
8+
On top of this repository, the Goblint Static Analyzer is needed.
9+
The relevant tag is this one: https://github.com/goblint/analyzer/tree/v2.1.0-longjmp
10+
11+
Please follow the installation guide given in https://github.com/goblint/analyzer/tree/v2.1.0-longjmp#readme
12+
13+
# Small Litmus Tests
14+
## General
15+
16+
The set of 40-ish small examples is integrated into the set of regression tests for the Goblint.
17+
To run all regression tests, one may simply (in the analyzer directory) call
18+
19+
~~~console
20+
make test
21+
~~~
22+
23+
In order to run one specific example, one may run
24+
25+
~~~console
26+
./regtest.sh 68 NN
27+
~~~
28+
29+
where `NN` is the number at the beginning of the testcase in folder `tests/regression/68-longjmp/NN-one.c`.
30+
One may then inspect a visual representation of the results by serving the
31+
`result` directory and accessing it via a browser. For details, refer to https://goblint.readthedocs.io/en/latest/user-guide/inspecting/.
32+
The runtime for all these litmus tests is negligible.
33+
34+
## Abstract Stack Unwinding
35+
36+
We would like to particularly point out test `68/22` that demonstrates the need for abstract stack unwinding:
37+
- `main` calls `setjmp`
38+
- A pointer to `val` is passed to `fun` which sets `val` to `1`.
39+
- `fun` then calls `foo`. `foo` is not passed a pointer to `val`, and thus `val` does not appear in its local state.
40+
- `foo` causes a `longjmp` back to `main`
41+
42+
Here, in order to account for the modification of `val`, it is necessary to pass values up the callstack, and calling $\textsf{combine}^\sharp$ while unwinding the stack.
43+
44+
# `Libpng` example
45+
46+
## Current Version
47+
48+
We have used Goblint's support for compilation DBs and the merger that comes with CIL to produce a single program, making it easier to run these tests.
49+
50+
This program can be found inside the libpng folder.
51+
52+
To run the program, execute from within this folder/
53+
54+
~~~console
55+
../path/to/analyzer/repo/goblint pngtest_combined.c --conf config.json &> pngtest_out.log
56+
~~~
57+
58+
Such a run takes about 55min and 26GB of RAM.
59+
60+
Among other warnings about internal issues of the analyzer related to precision loss, six warnings related to the usage of
61+
setjmp/longjmp are produced.
62+
63+
- The warnings that we believe to be indicative of a real bug are the two warnings `[Warning][Behavior > Undefined > Other] Reading poisonous variable row_buf`.
64+
- The three warnings about longjmps leading to potentially invalid targets start with `[Warning][Behavior > Undefined > Other] Longjmp to potentially invalid target [...]` or `[Warning][Imprecise] Longjmp to potentially invalid target [...]`.
65+
- The warning about jumping to a jump buffer that may receive its value by copying memory is `[Warning][Behavior > Undefined > Other] The jump buffer *(png_ptr->jmp_buf_ptr) contains values that were copied here instead of being set by setjmp. This is Undefined Behavior.`.
66+
67+
## Bug Injection
68+
69+
We have also injected a bug akin to the one in ImageMagick described in
70+
[this blog post](https://patrakov.blogspot.com/2009/07/dangers-of-setjmplongjmp.html).
71+
The corresponding program is also in the libpng folder (`pngtest_seeded_bug.c`).
72+
To understand the way in which the bug was introduced, it may be helpful to use a diff tool and compare
73+
`pngtest_combined.c` and `pngtest_seeded_bug.c`.
74+
75+
Goblint can be run on it in the same way as the unmodified program.
76+
77+
The inserted bug is that the variable `png_pixels` is accessed when it has indeterminate value.
78+
This is reflected in the extra warnings `[Warning][Unknown] accessing poisonous variable png_pixels`.
79+
80+
81+
82+
# Helpful Links
83+
84+
- https://goblint.readthedocs.io/
85+
- https://goblint.in.tum.de/

‎setjmp/libpng/LICENSE‎

Lines changed: 134 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,134 @@
1+
COPYRIGHT NOTICE, DISCLAIMER, and LICENSE
2+
=========================================
3+
4+
PNG Reference Library License version 2
5+
---------------------------------------
6+
7+
* Copyright (c) 1995-2022 The PNG Reference Library Authors.
8+
* Copyright (c) 2018-2022 Cosmin Truta.
9+
* Copyright (c) 2000-2002, 2004, 2006-2018 Glenn Randers-Pehrson.
10+
* Copyright (c) 1996-1997 Andreas Dilger.
11+
* Copyright (c) 1995-1996 Guy Eric Schalnat, Group 42, Inc.
12+
13+
The software is supplied "as is", without warranty of any kind,
14+
express or implied, including, without limitation, the warranties
15+
of merchantability, fitness for a particular purpose, title, and
16+
non-infringement. In no event shall the Copyright owners, or
17+
anyone distributing the software, be liable for any damages or
18+
other liability, whether in contract, tort or otherwise, arising
19+
from, out of, or in connection with the software, or the use or
20+
other dealings in the software, even if advised of the possibility
21+
of such damage.
22+
23+
Permission is hereby granted to use, copy, modify, and distribute
24+
this software, or portions hereof, for any purpose, without fee,
25+
subject to the following restrictions:
26+
27+
1. The origin of this software must not be misrepresented; you
28+
must not claim that you wrote the original software. If you
29+
use this software in a product, an acknowledgment in the product
30+
documentation would be appreciated, but is not required.
31+
32+
2. Altered source versions must be plainly marked as such, and must
33+
not be misrepresented as being the original software.
34+
35+
3. This Copyright notice may not be removed or altered from any
36+
source or altered source distribution.
37+
38+
39+
PNG Reference Library License version 1 (for libpng 0.5 through 1.6.35)
40+
-----------------------------------------------------------------------
41+
42+
libpng versions 1.0.7, July 1, 2000, through 1.6.35, July 15, 2018 are
43+
Copyright (c) 2000-2002, 2004, 2006-2018 Glenn Randers-Pehrson, are
44+
derived from libpng-1.0.6, and are distributed according to the same
45+
disclaimer and license as libpng-1.0.6 with the following individuals
46+
added to the list of Contributing Authors:
47+
48+
Simon-Pierre Cadieux
49+
Eric S. Raymond
50+
Mans Rullgard
51+
Cosmin Truta
52+
Gilles Vollant
53+
James Yu
54+
Mandar Sahastrabuddhe
55+
Google Inc.
56+
Vadim Barkov
57+
58+
and with the following additions to the disclaimer:
59+
60+
There is no warranty against interference with your enjoyment of
61+
the library or against infringement. There is no warranty that our
62+
efforts or the library will fulfill any of your particular purposes
63+
or needs. This library is provided with all faults, and the entire
64+
risk of satisfactory quality, performance, accuracy, and effort is
65+
with the user.
66+
67+
Some files in the "contrib" directory and some configure-generated
68+
files that are distributed with libpng have other copyright owners, and
69+
are released under other open source licenses.
70+
71+
libpng versions 0.97, January 1998, through 1.0.6, March 20, 2000, are
72+
Copyright (c) 1998-2000 Glenn Randers-Pehrson, are derived from
73+
libpng-0.96, and are distributed according to the same disclaimer and
74+
license as libpng-0.96, with the following individuals added to the
75+
list of Contributing Authors:
76+
77+
Tom Lane
78+
Glenn Randers-Pehrson
79+
Willem van Schaik
80+
81+
libpng versions 0.89, June 1996, through 0.96, May 1997, are
82+
Copyright (c) 1996-1997 Andreas Dilger, are derived from libpng-0.88,
83+
and are distributed according to the same disclaimer and license as
84+
libpng-0.88, with the following individuals added to the list of
85+
Contributing Authors:
86+
87+
John Bowler
88+
Kevin Bracey
89+
Sam Bushell
90+
Magnus Holmgren
91+
Greg Roelofs
92+
Tom Tanner
93+
94+
Some files in the "scripts" directory have other copyright owners,
95+
but are released under this license.
96+
97+
libpng versions 0.5, May 1995, through 0.88, January 1996, are
98+
Copyright (c) 1995-1996 Guy Eric Schalnat, Group 42, Inc.
99+
100+
For the purposes of this copyright and license, "Contributing Authors"
101+
is defined as the following set of individuals:
102+
103+
Andreas Dilger
104+
Dave Martindale
105+
Guy Eric Schalnat
106+
Paul Schmidt
107+
Tim Wegner
108+
109+
The PNG Reference Library is supplied "AS IS". The Contributing
110+
Authors and Group 42, Inc. disclaim all warranties, expressed or
111+
implied, including, without limitation, the warranties of
112+
merchantability and of fitness for any purpose. The Contributing
113+
Authors and Group 42, Inc. assume no liability for direct, indirect,
114+
incidental, special, exemplary, or consequential damages, which may
115+
result from the use of the PNG Reference Library, even if advised of
116+
the possibility of such damage.
117+
118+
Permission is hereby granted to use, copy, modify, and distribute this
119+
source code, or portions hereof, for any purpose, without fee, subject
120+
to the following restrictions:
121+
122+
1. The origin of this source code must not be misrepresented.
123+
124+
2. Altered versions must be plainly marked as such and must not
125+
be misrepresented as being the original source.
126+
127+
3. This Copyright notice may not be removed or altered from any
128+
source or altered source distribution.
129+
130+
The Contributing Authors and Group 42, Inc. specifically permit,
131+
without fee, and encourage the use of this source code as a component
132+
to supporting the PNG file format in commercial products. If you use
133+
this source code in a product, acknowledgment is not required but would
134+
be appreciated.

‎setjmp/libpng/config.json‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
{
2+
"ana" : {
3+
"base" : {
4+
"context" : {
5+
"non-ptr" : false
6+
}
7+
},
8+
"malloc" : {
9+
"wrappers" : ["png_malloc","png_malloc_warn","png_malloc_default",
10+
"png_malloc_base","png_malloc_array","png_malloc_array_checked",
11+
"png_calloc","png_zalloc","png_create_png_struct"],
12+
"unique_address_count" : 1
13+
},
14+
"dead-code" :{
15+
"branches" : false
16+
}
17+
},
18+
"sem": {
19+
"unknown_function" : {
20+
"spawn" : false,
21+
"invalidate" : {
22+
"globals" : false,
23+
"args" : false
24+
}
25+
}
26+
},
27+
"dbg" : {
28+
"timing" : {
29+
"enabled" : true
30+
}
31+
},
32+
"exp" : {
33+
"volatiles_are_top" : false
34+
},
35+
"warn" : {
36+
"info" : false,
37+
"imprecise" : true,
38+
"behavior" : true
39+
}
40+
}

0 commit comments

Comments
 (0)