Skip to content

Commit 9c5bb20

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #2793 from NlightNFotis/goto_instrument_readme
Add some usage examples into the goto-instrument readme file. [DOC-41]
2 parents f466751 + 2819f60 commit 9c5bb20

File tree

1 file changed

+155
-0
lines changed

1 file changed

+155
-0
lines changed

‎src/goto-instrument/README.md

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,3 +26,158 @@ developers are advised to copy the directory, remove all files apart
2626
from `main.*`, `parseoptions.*` and the `Makefile` and use these as the
2727
skeleton of their application. The `doit()` method in `parseoptions.cpp`
2828
is the preferred location for the top level control for the program.
29+
30+
### Main usage ###
31+
32+
For most of the transformations, `goto-instrument` takes one or two
33+
arguments and any number of options. The two file arguments are
34+
a goto-binary that it uses
35+
as an input for the transformation, and then *another goto binary* that
36+
it uses to write the result of the transformation. This is important
37+
because many times, if you don't supply a second filename for the
38+
goto-binary to be written to, you get the equivalent of the `--help`
39+
option output, with no indication of what has gone wrong. Some of the options
40+
can work with just an input file and not output file. For more specific
41+
examples, take a look at the demonstrations below:
42+
43+
### Function pointer removal ###
44+
45+
As an example of a transformation pass being run, imagine you have a file
46+
called `function_pointers.c` with the following content:
47+
48+
int f1(void);
49+
int f2(void);
50+
int f3(void);
51+
int f4(void);
52+
53+
int (* const fptbl1[][2])(void) = {
54+
{ f1, f2 },
55+
{ f3, f4 },
56+
};
57+
58+
int g1(void);
59+
int g2(void);
60+
61+
int (* const fptbl2[])(void) = {
62+
g1, g2
63+
};
64+
65+
int func(int id1, int id2)
66+
{
67+
int t;
68+
t = fptbl1[id1][id2]();
69+
t = fptbl2[id1]();
70+
return t;
71+
}
72+
73+
Then, assuming you have compiled it to a goto-binary with `goto-cc`, called
74+
`function_pointers.goto`, you could see the output of the
75+
`--show-goto-functions` flag on the unmodified program:
76+
77+
Reading GOTO program from `function_pointers.goto'
78+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
79+
80+
func /* func */
81+
// 0 file function_pointer.c line 20 function func
82+
signed int t;
83+
// 1 file function_pointer.c line 21 function func
84+
t=fptbl1[(signed long int)id1][(signed long int)id2]();
85+
// 2 file function_pointer.c line 22 function func
86+
t=fptbl2[(signed long int)id1]();
87+
// 3 file function_pointer.c line 23 function func
88+
return t;
89+
// 4 file function_pointer.c line 23 function func
90+
dead t;
91+
// 5 file function_pointer.c line 23 function func
92+
GOTO 1
93+
// 6 file function_pointer.c line 24 function func
94+
1: END_FUNCTION
95+
96+
97+
Then, you can run a transformation pass with `goto-instrument --remove-function-pointers function_pointers.goto function_pointers_modified.goto`,
98+
and then ask to show the result of the transformation through
99+
showing the goto-functions again:
100+
101+
Reading GOTO program from `function_pointers_modified.goto'
102+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
103+
104+
func /* func */
105+
// 0 file function_pointer.c line 20 function func
106+
signed int t;
107+
// 1 file function_pointer.c line 21 function func
108+
fptbl1[(signed long int)id1][(signed long int)id2];
109+
// 2 file function_pointer.c line 21 function func
110+
IF fptbl1[(signed long int)id1][(signed long int)id2] == f3 THEN GOTO 1
111+
// 3 file function_pointer.c line 21 function func
112+
IF fptbl1[(signed long int)id1][(signed long int)id2] == f2 THEN GOTO 2
113+
// 4 file function_pointer.c line 21 function func
114+
IF fptbl1[(signed long int)id1][(signed long int)id2] == f1 THEN GOTO 3
115+
// 5 file function_pointer.c line 21 function func
116+
IF fptbl1[(signed long int)id1][(signed long int)id2] == f4 THEN GOTO 4
117+
// 6 file function_pointer.c line 21 function func
118+
IF fptbl1[(signed long int)id1][(signed long int)id2] == g1 THEN GOTO 5
119+
// 7 file function_pointer.c line 21 function func
120+
IF fptbl1[(signed long int)id1][(signed long int)id2] == g2 THEN GOTO 6
121+
// 8 file function_pointer.c line 21 function func
122+
1: t=f3();
123+
// 9 file function_pointer.c line 21 function func
124+
GOTO 7
125+
// 10 file function_pointer.c line 21 function func
126+
2: t=f2();
127+
// 11 file function_pointer.c line 21 function func
128+
GOTO 7
129+
// 12 file function_pointer.c line 21 function func
130+
3: t=f1();
131+
// 13 file function_pointer.c line 21 function func
132+
GOTO 7
133+
// 14 file function_pointer.c line 21 function func
134+
4: t=f4();
135+
// 15 file function_pointer.c line 21 function func
136+
GOTO 7
137+
// 16 file function_pointer.c line 21 function func
138+
5: t=g1();
139+
// 17 file function_pointer.c line 21 function func
140+
GOTO 7
141+
// 18 file function_pointer.c line 21 function func
142+
6: t=g2();
143+
// 19 file function_pointer.c line 22 function func
144+
7: fptbl2[(signed long int)id1];
145+
// 20 file function_pointer.c line 22 function func
146+
IF fptbl2[(signed long int)id1] == g1 THEN GOTO 8
147+
// 21 file function_pointer.c line 22 function func
148+
IF fptbl2[(signed long int)id1] == g2 THEN GOTO 9
149+
// 22 file function_pointer.c line 22 function func
150+
8: t=g1();
151+
// 23 file function_pointer.c line 22 function func
152+
GOTO 10
153+
// 24 file function_pointer.c line 22 function func
154+
9: t=g2();
155+
// 25 file function_pointer.c line 23 function func
156+
10: return t;
157+
// 26 file function_pointer.c line 23 function func
158+
dead t;
159+
// 27 file function_pointer.c line 24 function func
160+
END_FUNCTION
161+
162+
You can now see that the function pointer (indirect) call (resulting from
163+
the array indexing of the array containing the function pointers)
164+
has now been substituted by direct, conditional calls.
165+
166+
### Call Graph ###
167+
168+
This is an example of a command line flag that requires only one argument,
169+
specifying the input file.
170+
171+
You can see the call graph of a particular goto-binary by issuing `goto-instrument --call-graph <goto_binary>`. This gives a result similar to this:
172+
173+
Reading GOTO program from `a.out'
174+
Function Pointer Removal
175+
Virtual function removal
176+
Cleaning inline assembler statements
177+
main -> fun
178+
__CPROVER__start -> __CPROVER_initialize
179+
__CPROVER__start -> main
180+
fun -> malloc
181+
182+
The interesting part of the output in the above text is the last four lines,
183+
that show that `main` is calling `fun`, `__CPROVER__start` is calling `__CPROVER_initialize` and `main` and that `fun` is calling `malloc`.

0 commit comments

Comments
 (0)