cprover
goto-instrument/README.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \defgroup goto-instrument goto-instrument
3 
4 # Folder goto-instrument
5 
6 \author Martin Brain
7 
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`.
23 
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.
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`.