Skip to content

Commit 524eec9

Browse files
NlightNFotisNlightNFotis
committed
Add some usage examples into the goto-instrument readme file.
1 parent dbd6988 commit 524eec9

File tree

1 file changed

+159
-0
lines changed

1 file changed

+159
-0
lines changed

‎src/goto-instrument/README.md

Lines changed: 159 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@
55

66
\author Martin Brain
77

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