2 \defgroup goto-instrument goto-instrument
4 # Folder goto-instrument
8 The `goto-instrument/` directory contains a number of tools, one per
9 file, that are built into the `goto-instrument` program. All of them
10 take in a goto-program (produced by `goto-cc`) and either modify it or
11 perform some analysis. Examples include `nondet_static.cpp` which
12 initialises static variables to a non-deterministic value,
13 `nondet_volatile.cpp` which assigns a non-deterministic value to any
14 volatile variable before it is read and `weak_memory.h` which performs
15 the necessary transformations to reason about weak memory models. The
16 exception to the “one file for each piece of functionality” rule are the
17 program instrumentation options (mostly those given as “Safety checks”
18 in the `goto-instrument` help text) which are included in the
19 `goto-program/` directory. An example of this is
20 `goto-program/stack_depth.h` and the general rule seems to be that
21 transformations and instrumentation that `cbmc` uses should be in
22 `goto-program/`, others should be in `goto-instrument`.
24 `goto-instrument` is a very good template for new analysis tools. New
25 developers are advised to copy the directory, remove all files apart
26 from `main.*`, `parseoptions.*` and the `Makefile` and use these as the
27 skeleton of their application. The `doit()` method in `parseoptions.cpp`
28 is the preferred location for the top level control for the program.
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:
43 ### Function pointer removal ###
45 As an example of a transformation pass being run, imagine you have a file
46 called `function_pointers.c` with the following content:
53 int (* const fptbl1[][2])(void) = {
61 int (* const fptbl2[])(void) = {
65 int func(int id1, int id2)
68 t = fptbl1[id1][id2]();
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:
77 Reading GOTO program from `function_pointers.goto'
78 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
81 // 0 file function_pointer.c line 20 function func
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
89 // 4 file function_pointer.c line 23 function func
91 // 5 file function_pointer.c line 23 function func
93 // 6 file function_pointer.c line 24 function func
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:
101 Reading GOTO program from `function_pointers_modified.goto'
102 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
105 // 0 file function_pointer.c line 20 function func
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
123 // 9 file function_pointer.c line 21 function func
125 // 10 file function_pointer.c line 21 function func
127 // 11 file function_pointer.c line 21 function func
129 // 12 file function_pointer.c line 21 function func
131 // 13 file function_pointer.c line 21 function func
133 // 14 file function_pointer.c line 21 function func
135 // 15 file function_pointer.c line 21 function func
137 // 16 file function_pointer.c line 21 function func
139 // 17 file function_pointer.c line 21 function func
141 // 18 file function_pointer.c line 21 function func
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
151 // 23 file function_pointer.c line 22 function func
153 // 24 file function_pointer.c line 22 function func
155 // 25 file function_pointer.c line 23 function func
157 // 26 file function_pointer.c line 23 function func
159 // 27 file function_pointer.c line 24 function func
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.
168 This is an example of a command line flag that requires only one argument,
169 specifying the input file.
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:
173 Reading GOTO program from `a.out'
174 Function Pointer Removal
175 Virtual function removal
176 Cleaning inline assembler statements
178 __CPROVER__start -> __CPROVER_initialize
179 __CPROVER__start -> main
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`.